Erased functions splitting on erased arguments are compiled incorrectly

[Z-snails]

-- bug.idr
0
foo : (0 a : Type) -> a -> a
foo Int x = x + 10
foo _ x = x

0
test : foo Nat (the Nat 7) = (the Nat 7)
test = Refl

Steps to Reproduce

> idris2 bug.idr

Expected Behavior

Typechecks

Observed Behavior

Warning: Unreachable clause: foo _ x

what:4:1--4:8
 1 | 0
 2 | foo : (0 a : Type) -> a -> a
 3 | foo Int x = x + 10
 4 | foo _ x = x
     ^^^^^^^

Error: While processing right hand side of test. Can't
solve constraint
between: 7 and prim__add_Int (the Nat 7) 10.

what:8:8--8:12
 4 | foo _ x = x
 5 |
 6 | 0
 7 | test : foo Nat (the Nat 7) = (the Nat 7)
 8 | test = Refl

[dunhamsteve]

This issue also occurs when splitting on Char. It does not occur when splitting on Bool or Nat.

0
foo : (0 a : Char) -> Nat
foo 'a' = 1
foo _  = 0

0
test : foo 'b' = 0
test = Refl

[dunhamsteve]

The case builder is dropping the second two cases in the following code:

0
foo : (0 a : Char) -> Nat
foo 'a' = 1
foo 'c' = 2
foo _  = 0

The case tree is just 1.

This is happening in getClauseType where it decides that a case is VarClause if it is rig0. I believe it needs to not do that if the Phase is CompileTime Rig0 (there is a similar condition earlier in the code).

Unfortunately, that change breaks test reg049:

1/1: Building lettype (lettype.idr)
Error: Linearity checking failed on (Main.fails2 (Builtin.MkPair [__] [__] m[1] k[0])) ((Main.case block in $resolved2701 (Builtin.MkPair [__] [__] m[1] k[0])) not a function type)

lettype:15:1--15:20
 11 | 
 12 | fails2 : (n : (Nat, Nat)) ->
 13 |          let (m, k) = n in
 14 |              {y : Bool} -> (z : Bool) -> String
 15 | fails2 (m, k) {y} z = ?h3
      ^^^^^^^^^^^^^^^^^^^

That test is running a case in a type signature. I need to look into it further, but I believe that previously it was throwing out the assignment entirely (due to the above issue) - but that wasn't noticed because m and k were not used. Now it looks like it's getting stuck on the case.

Since n doesn't exist to eliminate, I'm not sure this is something that can be made to work properly. (I think you'd need fst / snd if you want to take apart a tuple up there.)

[dunhamsteve]

My change breaks other stuff as well. It seems fine if I back off and only deal with PConst, but that doesn't solve the original issue. If I add type constructors, some other things break. (e.g. coverage errors in a paper.)