The syntax-based termination checker forbids T because it makes Agda loop.
{-# OPTIONS --type-based-termination #-}
{-# OPTIONS --sized-types #-}
module TypeBasedTermination.BoundedSizeNoMatch where
open import Agda.Builtin.Size
open import Agda.Builtin.Equality
-- The following should not termination check,
-- otherwise eta expansion can loop
T : Size → Set
T i = (j : Size< i) → T j
-- This loops:
loops : (i : Size) (x y : T i) → x ≡ y
loops i x y = refl
TBT currently accepts T which sends the type-checker into infinite eta-expansion for loops.
The syntax-based termination checker forbids
T
because it makes Agda loop.TBT currently accepts
T
which sends the type-checker into infinite eta-expansion forloops
.