Open andreasabel opened 1 month ago
This exploit also works for inductive types:
open import Agda.Builtin.Nat
f : Nat → Nat
f x = x' where x' = suc (suc x)
diverge : Nat → Nat
diverge zero = zero
diverge (suc n) = diverge (f n)
Accepted by TBT.
And BOOM!
I did finally manage to show the current size-preservation analysis inconsistent:
{-# OPTIONS --type-based-termination #-}
data ⊥ : Set where
record _×_ (A B : Set) : Set where
field
fst : A
snd : B
open _×_
record U : Set where
coinductive; constructor delay
field force : U × ⊥
open U
f : U → U × ⊥
f u = u' .force where u' = u
u : U
u .force = f u
absurd : ⊥
absurd = u .force .snd
TBT accepts f
as size-preserving yet it is not.
The use of with
is (expectedly) also affected, you can swap f
for this implementation:
f : U → U × ⊥
f u with u
... | u' = u' .force
Postmortem:
I had an optimisation where I did not record constraints of the form i ≤ ∞
. Seems reasonable, but if i
is a contravariant size variable, then the constraint should be reversed, and it starts making sense.
TBT accepts a non-productive definition, which we can exploit to make the Agda loop:
ATTN: @knisht