## val singleton

Regardez:

data Nat :: * where

Z :: Nat

S :: Nat -> Nat

deriving (SheSingleton)

data Vec :: {Nat} -> * -> * where

VNil :: Vec {Z} x

(:>) :: x -> Vec {n} x -> Vec {S n} x

Now you can write stuff like.

vec :: forall x. pi (n :: Nat). x -> Vec {n} x

vec {Z} x = VNil

vec {S n} x = x :> vec {n} x

Mumsie! Have the terms broken through the colon? Of course not. ‘pi (n :: Nat).’ is short for ‘forall n. SheSingleton Nat n ->’, which computes by tactical grace to ‘forall n. SheSingNat n ->’, where ‘SheSingNat’ is a GADT with ‘SheWitZ :: SheSingNat {Z}’ and ‘SheWitS :: pi (n :: Nat). SheSingNat {S n}’. Phew! The braces in terms turn ordinary constructors into their SheWitty versions, demanding the corresponding values at the type level.

This is an annoying hack: SheSingleton is a *type* family, when it would be
nicer to make it a *data* family defined GADT-style: this slicker coding already
works in 6.11, but not in 6.10.