idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.53k stars 378 forks source link

Cannot infer type after case in lazy lambda #3418

Open spcfox opened 5 days ago

spcfox commented 5 days ago

Steps to Reproduce

foo : Lazy (() -> ())
foo = \x => the () $ case x of () => ()

bar : Lazy (() -> ())
bar = \x => case x of () => ()

Expected Behavior

Both functions will pass the type check

Observed Behavior

foo successfully passes type checking, but bar doesn't:

Error: While processing right hand side of bar. Can't solve constraint between: () and ?caseTy [no locals in scope].

Test:7:29--7:31
 3 | foo : Lazy (() -> ())
 4 | foo = \x => the () $ case x of () => ()
 5 | 
 6 | bar : Lazy (() -> ())
 7 | bar = \x => case x of () => ()
                                 ^^
spcfox commented 4 days ago

This function also successful typechecking

baz : Lazy (() -> ())
baz = the (_ -> _) $ \x => case x of () => ()