Sized types allow defining inconsistent data

[knisht]

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.

[andreasabel]

Yeah, here you are defining two sizes that run through the same structure (SPN/SPM) but in opposite directions: The structure is supposed to be antitone in the first index and monotone in the second, but as you say, the structure is superpositioned between mu-nu and nu-mu.

Agda does not check whether the size assignment makes sense.