[Agda] internal error with sized types

[Andreas Abel]

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

Hi Samuel,

thanks for the bug report.  I have poked around in the Agda sources and
managed to spot the bug.

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

Here, in order to call "case", one has to lose some size information via
the subtyping relation

  N {i} <= N {↑ i}

Yet this piece of information is then lacking when one wants to
termination check.

Also note that your code is not strongly normalizing, so it ought not
termination check:

  anno x --> case x ...  anno y
         --> case x ...  case y ... anno y'

thus, there is infinite unfolding of anno.  The same function written
with pattern matching is strongly normalizing, since unmatched patterns
block further unfolding.

Cheers,
Andreas

Samuel Gélineau wrote:
> Hi,
> 
> I know that sized types can be used to tag transformations which don't
> increase the size. Can they also be used to tag transformations which
> strictly decrease the size? I've tried to figure out using the code
> below, but it caused an internal error. So I guess this message
> doubles as a bug report.
> 
> – Samuel Gélineau
> 
> 
> {-# OPTIONS --sized-types #-}
> module Main where
> 
> open import Size
> open import Data.Unit
> open import Data.Sum
> 
> -- Nat, but with sized types
> data N : {i : Size} → Set where
>   z : {i : Size} → N {↑ i}
>   s : {i : Size} → N {i} → N {↑ i}
> 
> -- strictly decreasing!
> case : {i : Size} → N {↑ i} → ⊤ ⊎ N {i}
> case z = inj₁ tt
> case (s x) = inj₂ x
> 
> -- doesn't pass termination checking, but compiles.
> -- notice that the size annotation is commented out.
> pass : {i : Size} → N {-i-} → ⊤
> pass x with case x
> ... | {- z -}   inj₁ _ = tt
> ... | {- s y -} inj₂ y = pass y
> 
> -- same function, but making use of the size annotation.
> -- should hopefully pass termination checking, but crashes:
> --   An internal error has occurred. Please report this as a bug.
> --   Location of the error: src/full/Agda/TypeChecking/Constraints.hs:103
> fail : {i : Size} → N {i} → ⊤
> fail x with case x
> ... | {- z -}   inj₁ _ = tt
> ... | {- s y -} inj₂ y = fail y
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 


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

iD8DBQFJkDfvPMHaDxpUpLMRAjYNAKCJ+vkV80oRN4XQGwQY3p3hq4iwPgCfUHcj
BSLT7ThAmqkJnmkavarkhMA=
=7Wt4
-----END PGP SIGNATURE-----