When using %auto_lazy off, type checking sometimes accepts programs where a strict value is passed instead of a lazy value and vice versa. Examples:
%auto_lazy off
n : Nat
n = 1
m : Nat
m = delay n
k : Nat
k = force n
%auto_lazy off
main : IO ()
main = putStrLn "Hello" >> putStrLn {io=IO} "world"
The second argument of (>>) is lazy. Without delay typechecker throws
Error: While processing right hand side of main. Can't find an implementation for HasIO ?io
but accepts if you explicitly pass IO.
%auto_lazy off
data X = A
f : Lazy X -> X
f x@A = x
main : IO ()
main = ignore $ pure $ f A
This code successfully passes the type-check but throws an error when generating Scheme code:
Exception: attempt to reference unbound identifier pat0C-58-0 at line 648, char 47 of /project/directory/build/exec/_tmpchez_app/_tmpchez.ss
Expected Behavior
Error during type checking, like
Error: While processing right hand side of m. Can't solve constraint between: Lazy Nat and Nat.
Steps to Reproduce
When using
%auto_lazy off, type checking sometimes accepts programs where a strict value is passed instead of a lazy value and vice versa. Examples:The second argument of
(>>)is lazy. Withoutdelaytypechecker throwsError: While processing right hand side of main. Can't find an implementation for HasIO ?iobut accepts if you explicitly passIO.This code successfully passes the type-check but throws an error when generating Scheme code:
Expected Behavior
Error during type checking, like
Observed Behavior
Successfully passes the type-check.