[Agda] internal error with sized types

[Samuel Gélineau]

> - -- a non-dependent case for sized Nat
> case : {i : Size} → N {↑ i} →
>       {C : Set} → C -> (N {i} -> C) -> C
> case z     y f = y
> case (s x) y f = f x
>
> bla x = case x tt (\ y -> bla y)
>
> The function bla is well-defined for all natural numbers, but it is not
> strongly normalizing.  Hence, we have to reject it.  This is why Agda
> does not pass the following typing of bla.
>
> bla : {i : Size} → N {i} → ⊤
> bla {↑ i} x = case {i} x tt (\ y -> bla {i} y)
>
> How would you make precise the difference between your function, which
> is ok since the pattern matching is bound to block reduction, and "bla"?

I apparently don't understand how sized types work. I thought size
inference translated the above definitions into something like this:

-- a non-magical version of Size
data S : Set where
  z : S
  ⇑_ : S → S

-- a version of N which uses S instead of Size
data M : {i : S} → Set where
  z : {i : S} → M {⇑ i}
  s : {i : S} → M {i} → M {⇑ i}

-- a version of case which uses M instead of N
case-m : {i : S} → M {⇑ i} →
         {C : Set} → C -> (M {i} -> C) -> C
case-m z     y f = y
case-m (s x) y f = f x

-- a version of bla which uses case-m instead of case
bla-m : {i : S} → M {i} → ⊤
bla-m {z} ()
bla-m {⇑ i} x  = case-m x tt (\ y -> bla-m)

The above translation is accepted by agda as terminating, because it
is structurally recursive on its implicit argument. But as you've
mentioned, the same example with sized types isn't accepted. Why?

– Samuel