Strange type inference behaviour with GADT type (for fixed length vectors)

Question

I have the following GADT

data Vec n a where
    T    :: Vec VZero a
    (:.) :: (VNat n) => a -> (Vec n a) -> (Vec (VSucc n) a)

to model fixed length vectors, using the class

class VNat n

data VZero
instance VNat VZero

data VSucc n
instance (VNat n) => VNat (VSucc n)

I tried to programm an append-function on vectors:

vAppend :: Vec n b -> Vec m b -> Vec nm b
vAppend T T = T   -- nonsense, -- its just a minimal def for testing purposes

The type checker doesnt like it:

 Could not deduce (nm ~ VZero)
    from the context (n ~ VZero)
      bound by a pattern with constructor
                 T :: forall a. Vec VZero a,
               in an equation for `vAppend'
      at VArrow.hs:20:9
    or from (m ~ VZero)
      bound by a pattern with constructor
                 T :: forall a. Vec VZero a,
               in an equation for `vAppend'
      at VArrow.hs:20:11
      `nm' is a rigid type variable bound by
           the type signature for vAppend :: Vec n b -> Vec m b -> Vec nm b
           at VArrow.hs:20:1
    Expected type: Vec nm b
      Actual type: Vec VZero b
    In the expression: T
    In an equation for `vAppend': vAppend T T = T
Failed, modules loaded: Vectors.

Can anyone explain GHCs problems with the type variable nm? And what exactly means the ~ in the error message?

Answer 1

As it stands you are saying you can get a vector of any length by appending any two vectors. If you scrap the signature ghc infers that vAppend is supposed to yield vector of length VZero given any two vectors -- that makes sense but isn't what you want. You need a Plus type associated with your VNats to constrain the result type of vAppend on vectors. The natural way would be a type family of some sort, but I couldn't get it under the VNat class. In any case, this whole sort of idea is much more clearly realized with the promoted types of the DataKinds extension (in ghc-7.4 and later) -- though maybe you were deliberately trying to avoid that extension? This gets rid of the obnoxious unclosed character of VSucc, which admits VSucc Char etc. If you weren't trying to avoid DataKinds, then your module might look something like this:

{-#LANGUAGE  GADTs, TypeFamilies, DataKinds, TypeOperators#-}

data Vec n a where                 -- or: data Vec :: VNat -> * -> * where
    T    :: Vec VZero a
    (:.) :: a -> Vec n a -> Vec (VSucc n) a 
                                   -- no class constraint

data VNat  =  VZero |  VSucc VNat  -- standard naturals

type family n :+ m :: VNat         -- note the kind of a ":+" is a promoted VNat
type instance VZero :+ n = n
type instance VSucc n :+ m = VSucc (n :+ m)

vAppend :: Vec n b -> Vec m b -> Vec (n :+ m) b
vAppend T v = v  
vAppend (a :. u) v  = a :. (vAppend u v)

Edit: It occurs to me, looking at this, that the line for the Plus- or :+- type family should have explicitly constrained the kinds of the arguments

type family (n::VNat) :+ (m::VNat) :: VNat

to keep out garbage types like Char :+ VZero and so on -- that is, on the same principle used to prefer DataKinds to types like data VSucc n. Also, then we can see that the two instances specify it completely, though I don't know how much use the compiler can make of this.