Names received using as-matching are not reduced under case

[buzden]

Steps to Reproduce

Consider the following piece of code:

v : (Nat, Nat)

g : Unit
g = do
  let xx@(x, y) = v
  let prf1 = the (fst xx = x) Refl
  let _ = case () of
            _ => do
              let prf2 = the (fst xx = x) Refl
              ()
  ()

It contains similar proofs of equality, basically checking that fst xx indeed reduces to its value.

Expected Behavior

I'd expect both of the proofs to typecheck.

Observed Behavior

First one typechecks but the second fails with

Error: While processing right hand side of g. Can't solve constraint between: x and fst xx.

DoesntReduceUnderCase:9:43--9:47
 5 |   let xx@(x, y) = v
 6 |   let prf1 = the (fst xx = x) Refl
 7 |   let _ = case () of
 8 |             _ => do
 9 |               let prf2 = the (fst xx = x) Refl
                                               ^^^^

showing that fst xx did not reduce.

Analysis

Lengthy thoughts

My guess is that this behaviour is due to the coding of case expressions as functions, and that this coding ignores as-matches. I.e., g is translated to something like

caseFunction : (Nat, Nat) -> Nat -> Nat -> Unit -> Unit
caseFunction xx x y _ = do
  let prf2 = the (fst xx = x) Refl
  ()

g : Unit
g = do
  let xx@(x, y) = v
  let prf1 = the (fst xx = x) Refl
  let _ = caseFunction xx x y ()
  ()

My guess is that repeating as-pattern match could be useful (however, I don't know if this is generally possible, e.g. inside with-clauses), i.e. to be coded something like this:

caseFunction : (Nat, Nat) -> Unit -> Unit
caseFunction xx@(x, y) _ = do
  let prf2 = the (fst xx = x) Refl
  ()

g : Unit
g = do
  let xx@(x, y) = v
  let prf1 = the (fst xx = x) Refl
  let _ = caseFunction xx ()
  ()

or this (to not to do repeated runtime pattern matching):

caseFunction : (xx : (Nat, Nat)) -> (x : Nat) -> (y : Nat) -> (0 _ : xx = (x, y)) -> Unit -> Unit
caseFunction xx@(x, y) x y Refl _ = do
  let prf2 = the (fst xx = x) Refl
  ()

g : Unit
g = do
  let xx@(x, y) = v
  let prf1 = the (fst xx = x) Refl
  let _ = caseFunction xx x y Refl ()
  ()