Incorrect rejection of erased irrefutable patterns

[ohad]

trafficstars

(spotted by locria)

Steps to Reproduce

f : (0 x : (a,b)) -> Nat
f x =
  let 0 (u,v) = x in
  0

Expected Behavior

Type-check fine, with 0 u : a and 0 v : b in scope inside the let body.

Observed Behavior

     While processing right hand side of f. x is not accessible in this
     context.
     
      09 | f : (0 x : (a,b)) -> Nat
      10 | f x =
      11 |   let 0 (u,v) = x in                           ^

If we change 0 to 1, this type-checks fine:

f : (1 x : (a,b)) -> Nat
f x =
  let 1 (u,v) = x in
  0

So you'd expect consistent behaviour between the two quantities.

[iacore]

Here is a test case: https://github.com/locriacyber/idris2-sorted-ds/blob/05386b6f242432d21ea3ad1a6addf696b9403823/src/Data/BinaryTree.idr#L84

This should compile when the bug is fixed.

[gallais]

The crux is here IMO:

https://github.com/idris-lang/Idris2/blob/d786b5d1533bf509ab867b2eb4bef03fb85e61e9/src/Idris/Desugar.idr#L219-L222

PCase does not carry a RigCount which means that you cannot state which quantity to use to check the scrutinee hence the discarding of rig. Idris tries to guess instead and inevitably will make mistakes.

Two possible avenues to a fix:

• Try to elaborate let 0 pat = e in b to let 0 x = e in case x of pat => b where x is a fresh machine name with the hope that Idris will adequately guess 0 now that the scrutinee is a variable known to be 0.
• Add a RigCount field to PCase (and so probably to ICase too), propagate it here and use it during elaboration instead of guessing.

If someone wants to have a go at it, I'm happy to answer the questions that may arise.

[ohad]

@gallais @dunhamsteve Does theRigCount on ICase need to be a Maybe RigCount?

We don't always know the ambient rigcount during desugaring, and maybe that means we need to keep guessing in those cases.

(But I haven't yet delved into the details of quantity checking, so maybe the elaborator can deal with that.)

[dunhamsteve]

Yeah, I wasn't sure what to do in the non-PLet cases, so I just put top in there tentatively. In Case.idr, I kinda followed what Binders.idr was doing for ILet and did |*| between the ICase's rig and what I think is the ambient one (the first arg to checkCase).

I didn't realize this broke the build of contrib, or I wouldn't have pushed up to github yet. Make wasn't rebuilding contrib locally.

[ohad]

I'm glad you pushed to github --- means we get to talk about it :).

[dunhamsteve]

Last night (UTC-7) I figured out that the allow in Case.idr was lifting x back up from Rig0 to Rig1, which is why I put that if statement in there. That got everything working, or so I thought.