Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

case in a lambda is broken #324

Open
MarcelineVQ opened this issue Apr 25, 2020 · 0 comments
Open

case in a lambda is broken #324

MarcelineVQ opened this issue Apr 25, 2020 · 0 comments

Comments

@MarcelineVQ
Copy link
Contributor

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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant