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

[Andrea Vezzosi]

The subtyping only works when Foo is recognized as having the right
polarity, I don't know the details of the implementation but the Size<
version seems to work out right:

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

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


On Fri, Mar 13, 2015 at 12:51 PM, Conor McBride
<conor at strictlypositive.org> 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