`Lazy` allows for the construction of `Void`

[42triangles]

Steps to Reproduce

Compile the following:

https://gist.github.com/42triangles/40052a0e58b0a8396943a1f28cc62352 (the same as the code below)

%default total

data Recursive : (Lazy Type -> Type) -> Type where
  Recursing : t (delay (Recursive t)) -> Recursive t

F : Type
F = Recursive (\x => Not x)

notF : Not F
notF f@(Recursing nF) = nF f

f : F
f = Recursing notF

argh : Void
argh = notF f

(adapted from gallais' example for data Recursive : (Type -> Type) -> Type where Recursing : t (Recursive t) -> Recursive t (which is not accepted) allowing Void to be derived)

Expected Behavior

Does not compile

Observed Behavior

Does compile

[ProofOfKeags]

Humble observer here.. Isn't this expected? Isn't a nonterminating value bottom?

[gallais]

Lazy should not allow non termination. Its only impact should be the evaluation strategy being used.

[42triangles]

Specifically the issue is that argh is marked as total thanks to %default total, which means it shouldn't be able to be Void