Sized types allow defining inconsistent data #7178
Description
Consider the following data type:
{-# OPTIONS --sized-types #-}
module _ where
open import Agda.Builtin.Size
data ⊥ : Set where
record SPN (i j : Size) : Set
data SPM (i j : Size) : Set
data SPM i j where
inj : ∀ {k : Size< j} → SPN i k → SPM i j
record SPN i j where
coinductive
field
rec : {k : Size< i} → SPM k j
open SPN
spn : {i : Size} → SPN i ∞
spn .rec = inj spn
spm : {i : Size} → SPM ∞ i → ⊥
spm (inj x) = spm (x .rec)
boom : ⊥
boom = spm (spn .rec)Yet again an inconsistency with sized types, but I believe that this one is of a new kind. Both spn and spm are legal, and ∞ < ∞ is not abused anywhere.
I think the problem here is that SPM and SPN can be expressed neither as νY.μX.Y nor as μX.νY.X, which messes with the theory. It is unclear how to forbid such definitions though.