Top-level lazy functions don't typecheck

[mb64]

Steps to Reproduce

Make a top-level declaration with a lazy type that can't be inferred:

foo : Inf (Unit -> Unit)
foo = \x => x

bar : Inf (Unit -> Unit)
bar = Delay (\x => x)

Expected Behavior

They should type check fine.

Observed Behavior

Error: Not a function name in pattern LHS

t.idr:2:1--2:14
   |
 2 | foo = \x => x
   | ^^^^^^^^^^^^^

Error: While processing right hand side of bar. Can't infer delay type

t.idr:5:7--5:20
   |
 5 | bar = Delay \x => x
   |       ^^^^^^^^^^^^^

[gallais]

Note that Lazy and Inf are not the same thing.

[mb64]

That is true. In this case, changing Inf to Lazy gives exactly the same output, hence the lowercase-L "lazy" -- sorry for not making that clear.

[iacore]

Note that Lazy and Inf are not the same thing.

@gallais Can you elaborate? I was recently testing Inf but discovered that it can do the same thing as Lazy in the following code:

record Foo where
    constructor MkFoo
    bar : Lazy Foo -- could be Inf Foo
    baz : Nat


print_rec : Foo -> Nat -> IO ()
print_rec ff Z = pure ()
print_rec ff (S remaining) = do
    putStrLn (show ff.baz)
    print_rec ff.bar remaining


aa : Foo
bb : Foo
aa = MkFoo bb 1
bb = MkFoo aa 2
selfrec = MkFoo selfrec 3


main : IO ()
main =
    do
        let cc = { baz := 42 } aa
        let dd = { baz := 20 } bb
        print_rec cc 10
        print_rec dd 10
        print_rec selfrec 4

I was also confused by Delay in REPL. Sometimes Delay a show up where Lazy a should in REPL.

Main> :ti aa.bar
aa .bar : Inf Foo
Main> :ti Foo.bar
Main.Foo.bar : Foo -> Inf Foo
Main> aa
MkFoo (Delay bb) 1

# now change  Lazy Foo  to  Inf Foo

Main> :r
1/1: Building inf (inf.idr)
Loaded file inf.idr
Main> aa
MkFoo (Delay bb) 1
Main> :ti Foo.bar
Main.Foo.bar : Foo -> Lazy Foo

[ohad]

👍 for this issue.
Does anyone know why it's happening?
Since this is potentially blocking me, I might be able to try and fix it with some assistance.

[iacore]

+1 for this issue. Does anyone know why it's happening? Since this is potentially blocking me, I might be able to try and fix it with some assistance.

Avoid this feature. Use a normal function or something.

[ohad]

@iacore wrote:

Avoid this feature. Use a normal function or something.

I can't, see #2936