[Agda] internal error with sized types

[Andreas Abel]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Samuel Gélineau wrote:
> On Mon, Feb 9, 2009 at 9:04 AM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
>> 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. 

Sorry that is a typo, I meant to write "case {i} x".  The point is the
information loss from x : N {i} to x : N {↑ i}.

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

This is problematic.  Look at the following code:

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

Cheers,
Andreas

- --
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFJkX4IPMHaDxpUpLMRAvVRAKCv2qMyS9ZjgK18nP+SZeEzYqcbRQCglUZ6
CJnAERREeRXeXmHYrmMfNqo=
=n0ZC
-----END PGP SIGNATURE-----