Laziness subtyping(?) unsound

[ziman]

Steps to Reproduce

bools : List Bool
bools = [True, False]

main : IO ()
main = printLn $ or (map id bools)

main2 : IO ()
main2 = printLn $ or (map (\x => x) bools)

main3 : IO ()
main3 = printLn $ or (map (\x => Delay x) bools)

main4 : IO ()
main4 = printLn $ or bools

{-
$ idris2 z.idr -x main
Exception in vector-ref: #<procedure at _tmpchez.ss:8757> is not a vector
$ idris2 z.idr -x main2
Exception in vector-ref: #<procedure at _tmpchez.ss:8758> is not a vector
$ idris2 z.idr -x main3
True
$ idris2 z.idr -x main4
Exception in vector-ref: #<procedure at _tmpchez.ss:8758> is not a vector
-}

Expected Behavior

Either rejection by the compiler or printing True in all four cases. (I think main4 and main should be rejected, while there's probably a plausible way to elaborate main2.)

Observed Behavior

Outputs as shown above.