[Agda] Help, I'm failing at sized types.

[Andreas Abel]

Hi Conor,

sorry for the bad interface to sized types, it dates from 2008 when no 
big syntax invasions were wanted.  Thus, Agda silently accepts an 
"old-style" sized type (as you tried to implement with Foo) if it has 
the right format, otherwise it treats it as ordinary type.  [The 
new-style sized types Andrea explained are a bit less fragile.]

In particular, if you want an old-style sized type, every constructor 
has to target "Foo (up i)".  The following should work:

data Foo : Size -> Set where
   boo : {i : Size} -> Foo (up i)
   coo : {i : Size} -> Foo i -> Foo (up i)

subtype? : {i : Size} -> Foo i -> Foo infty
subtype? t = t

On 13.03.2015 12:51, Conor McBride wrote:
> Hi
>
> Sorry to be a nuisance.
>
> I’m trying to do some stuff with sized types, but I think I’m failing at basic stuff like finding
> the on-switch. Specifically…
>
> ****************************************
> {-# OPTIONS --sized-types #-}
>
> module SizeFail where
>
> open import Agda.Primitive
> postulate
>    Size : Set
>    Size<_ : Size -> Set
>    up : Size -> Size
>    infty : Size
> {-# BUILTIN SIZE Size #-}
> {-# BUILTIN SIZELT Size<_ #-}
> {-# BUILTIN SIZESUC up #-}
> {-# BUILTIN SIZEINF infty #-}
>
> data Foo : Size -> Set where
>    boo : {i : Size} -> Foo i
>    coo : {i : Size} -> Foo i -> Foo (up i)
>
> subtype? : {i : Size} -> Foo i -> Foo infty
> subtype? t = t
> ****************************************
>
> …results in the complaint...
>
> .i != infty of type Size
> when checking that the expression t has type Foo infty
>
> …whether the pragmas are present or not.
>
> Any light gratefully received.
>
> (Longer term, I want to do some syntactic mangling in which renaming is obviously size-preserving, so I can apply a renaming to a substructure before I do a recursive call on it.)
>
> Cheers
>
> Conor_______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


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

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/