Idris2-boot icon indicating copy to clipboard operation
Idris2-boot copied to clipboard

case in a lambda is broken

Open MarcelineVQ opened this issue 5 years ago • 0 comments

Idris 2, version 0.1.0-19426ecd1 I've included a lambda of case and a lambdacase to show it's not specific to one.

Steps to Reproduce

foo1 : ()
foo1 = (\dx => case dx of () => ()) ()
foo2 : ()
foo2 = (\case () => ()) ()

Expected Behavior

Typechecking completes.

Observed Behavior

1/1: Building Case (Case.idr)
Case.idr:2:8--4:1:While processing right hand side of foo1 at Case.idr:2:1--4:1:
Can't solve constraint between:
	?delayTy [no locals in scope]
and
	()
Case.idr:5:8--11:1:While processing right hand side of foo2 at Case.idr:5:1--11:1:
Can't solve constraint between:
	?delayTy [no locals in scope]
and
	()
Error(s) building file tests/idris2/case001/Case.idr: tests/idris2/case001/Case.idr:2:1--4:1:When elaborating right hand side of Main.foo1:
tests/idris2/case001/Case.idr:2:8--4:1:?Main.{delayTy:170}_[$resolved1135] and $resolved1132 are not equal
tests/idris2/case001/Case.idr:5:1--11:1:When elaborating right hand side of Main.foo2:
tests/idris2/case001/Case.idr:5:8--11:1:?Main.{delayTy:181}_[$resolved1135] and $resolved1132 are not equal

MarcelineVQ avatar Apr 25 '20 20:04 MarcelineVQ