[Agda] internal error with sized types

[Samuel Gélineau]

On Mon, Feb 9, 2009 at 9:04 AM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> thanks for the bug report.  I have poked around in the Agda sources and
> managed to spot the bug.

Thanks, that was quick!

> To answer your question, yes, you may strictly decrease the size.
> However, your code as you wrote it cannot termination check.  If I take
> the code of "fail" and put in the hidden arguments, the only possible
> annotation I see is:
>
> anno : {i : Size} → N {i} → ⊤
> anno {i} x with case {↑ i} x
> ... | {- z -}   inj₁ _ = tt
> ... | {- s y -} inj₂ y = anno y

Why do you call case with {↑ i}? The type of x is N {i}, so case needs
to be called with {pred i} or above. {↑ i} is certainly above, but
it's way too high. What I need agda to infer is the following:

-- duplicating the code in order to obtain {i} from x's constructors
anno2 : {i : Size} → N {i} → ⊤
anno2 .{↑ i} (z {i}) with case {i} (z {i})
... | {- z -}   inj₁ _ = tt
... | {- s y -} inj₂ y = anno2 {i} y
anno2 .{↑ i} (s {i} x) with case {i} (s {i} x)
... | {- z -}   inj₁ _ = tt
... | {- s y -} inj₂ y = anno2 {i} y

In the above code, anno2's argument (that is, (z {i}) in the first
branch and (s {i} x) in the second) has type N {↑ i}, and therefore
case needs to be called with {i} or above. case then provides us with
a value of type N {i}, which I can use to recur without fear of
non-termination.

Since agda accepts the above code as terminating, my question turned
bug report now turns into a feature request: could agda be made to
infer annotations such as the ones I have provided in anno2, rather
than the overly-conservative annotations of anno?

thanks,
– Samuel