[Haskell-cafe] GADTs: the plot thickens?

[Conor McBride]

Hi folks

A puzzle for you (and for me too). I just tried to translate an old 
Epigram favourite (which predates Epigram by some time) into GADT-speak. 
It went wrong. I had a feeling it might. I wonder how to fix it: I 
imagine it's possible to fix it, but that some cunning may be necessary. 
Here it is:

Type-level Nat

 > data Z = Z
 > data S x = S x

Finite sets: Fin Z is empty, Fin (S n) has one more element than Fin n

 > data Fin :: * -> * where
 >   Fz :: Fin (S n)
 >   Fs :: Fin n -> Fin (S n)

The "thinning" function: thin i is the order-preserving embedding from 
Fin n to Fin (S n) which never returns i.

 > thin :: Fin (S n) -> Fin n -> Fin (S n)
 > thin Fz      i       = Fs i
 > thin (Fs i)  Fz      = Fz
 > thin (Fs i)  (Fs j)  = Fs (thin i j)

Its partial inverse, "thickening" has the spec

thicken i i = Nothing
thicken i (thin i j) = Just j

 > thicken :: Fin (S n) -> Fin (S n) -> Maybe (Fin n)
 > thicken Fz      Fz      = Nothing
 > thicken Fz      (Fs j)  = Just j
 > thicken (Fs i)  Fz      = Just Fz
 > thicken (Fs i)  (Fs j)  = fmap Fs (thicken i j)

The trouble is that whilst thin compiles, thicken does not. GHC rightly 
complains

Thicken.lhs:18:32:
    Couldn't match expected type `n' (a rigid variable)
       against inferred type `S n1'
      `n' is bound by the type signature for `thicken'
    at Thicken.lhs:15:19
      Expected type: Fin n
      Inferred type: Fin (S n1)
    In the first argument of `Just', namely `Fz'
    In the expression: Just Fz

The trouble is that (Fs i) is only known to be of some type Fin (S n), 
so we need to return the Fz :: Fin n, and there ain't no such beast.

The question is how to explain that this program actually does make some 
sense.

One to ponder.

Cheers

Conor