Inconsistent %auto_lazy off behavior

[spcfox]

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:

1.  %auto_lazy off
    
    n : Nat
    n = 1
    
    m : Nat
    m = delay n
    
    k : Nat
    k = force n

2.  %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.

3.  %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 generates 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.

Observed Behavior

Successfully passes the type-check.