case in a lambda is broken

[edwinb]

Issue by MarcelineVQ
Saturday Apr 25, 2020 at 20:46 GMT
Originally opened as edwinb/Idris2-boot#324

---

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

[jdevuyst]

Not sure if this is a meaningful difference but I ran into a similar error with this example:

T : Bool -> Bool -> Type
T True  b = () -> if b then String else Double
T False _ = Int

f : (x : Bool ** (y : Bool) -> T x y)
f = (True ** \y => \() => case y of
                             True  => ""
                             False => 0)

The error is:

Can't solve constraint between:
	String
and
	?caseTy [no locals in scope]

The difference is that this message has a hole named ?caseTy rather than ?delayTy.

When I make T not return a function type, it works fine, so I was surprised to find this ticket with such a trivial example. :)

I have another, more complicated, example where there are names in scope. Let me know if it would be useful to have.