search

edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

case in a lambda is broken #324

Open MarcelineVQ opened 4 years ago

MarcelineVQ commented 4 years ago

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