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

[Conor McBride]

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