TBT accepts this, but this is questionable, since it seems to assume too much about postulates:
{-# OPTIONS --type-based-termination #-}
record U : Set where
coinductive
field force : U
open U
postulate d : U → U
-- f is classified as size preserving, but is not, since d is unknown
-- Counterexamples: d = id; d u = u .force
f : U → U
f u = d u .force
-- This should not pass:
u : U
u .force = f u
I failed to exploit this bug, because TBT does not accept the same if we replace d by a module parameter (which we later could instantiate to something evil).
ATTN: @knisht
TBT accepts this, but this is questionable, since it seems to assume too much about postulates:
I failed to exploit this bug, because TBT does not accept the same if we replace
dby a module parameter (which we later could instantiate to something evil). ATTN: @knisht