[Agda] internal error with sized types

[Andreas Abel]

The code you give below indexes data structures by natural numbers.   
You can always do so to add more information for the termination  
checker.  But sizes are the tree heights of data structures, which can  
be transfinite in case of infinitely branching trees.

data Tree : {_ : Size} -> Set  where
   leaf : forall {i} -> Tree {↑ i}
   node : forall {i} -> (ℕ -> Tree {i}) -> Tree {↑ i}

Sized types offer you an unbounded size ∞ and subtyping wrt. sizes.

The reason why "bla" has to be rejected is ∞, which matches against   
↑ i  with solution i = ∞.

On Feb 12, 2009, at 2:50 AM, Samuel Gélineau wrote:

>> - -- 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
>