TBT: Bug in size preservation regarding postulates

[andreasabel]

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