I'm exploring the 'hackneyed' example of length-indexed vectors, code adapted from Richard Eisenberg's thesis section 3.1
{-# LANGUAGE GADTs, TypeFamilies, DataKinds, KindSignatures,
TypeOperators, ScopedTypeVariables #-}
-- PatternSignatures -- deprecated
import GHC.Types (Type)
data Nat = Zero | Succ Nat
data Vec :: Type -> Nat -> Type where
Nil :: Vec a Zero -- E has 'Zero
(:>) :: a -> Vec a n -> Vec a (Succ n) -- E has 'Succ
infixr 5 :>
type family (+) (n :: Nat) (m :: Nat) :: Nat where
(+) Zero m = m
(+) (Succ n') m = Succ (n' + m)
append :: Vec a n -> Vec a m -> Vec a (n + m)
append (Nil :: Vec aa Zero) (w :: Vec aa mm) = w :: Vec aa (Zero + mm)
append (x :> (v :: Vec a n')) (w :: Vec a m) = x :> ((append v w) :: Vec a (n' + m))
The append Nil ...
equation is rejected (GHC 8.6.5)
* Couldn't match type `m' with `n + m'
`m' is a rigid type variable bound by
the type signature for:
append :: forall a (n :: Nat) (m :: Nat).
Vec a n -> Vec a m -> Vec a (n + m)
at ...
Expected type: Vec a (n + m)
Actual type: Vec a ('Zero + m)
Giving the result type as :: Vec aa mm
is also rejected.
Expected type: Vec a (n + m)
Actual type: Vec a m
weird because that's accepted (see below).
What I'm really trying to do is use PatternSignatures
for the arguments to append
. But that extension is deprecated, I have to use ScopedTypeVariables
. And that means the tyvars from the signature for append
are in scope in the equations. So I've used fresh tyvar names.
The GADT gives Nil :: Vec a Zero
, so I give that as its pattern signature (with a fresh aa
). But it seems GHC can't unify the n
from append
's signature with the Zero
. If I change that equation to either of these, all is happy:
append (Nil :: Vec aa nn) (w :: Vec aa mm) = w :: Vec aa (nn + mm)
append (Nil :: Vec aa nn) (w :: Vec aa mm) = w :: Vec aa (mm)
To validate those, GHC must be figuring out that Nil :: Vec a Zero
and that Zero + m = m
from the type family equation for +
. So why is it grumpy about the pattern signature with Zero
?
(I was originally trying to give the equations for append
purely with PatternSignatures
, to see if GHC could infer the signature. That didn't get off the ground.)
The first thing to notice is that the error you're showing is not the only error you're getting, and actually, it's not the important one. The other error you should see is:
The key part here is "When checking that the pattern signature fits the type of its context". Indeed, the type of the pattern
Nil
is not simplyVec a Zero
; it's actually something like() => (n ~ Zero) => Vec a n
. This type says that the pattern may match on anything of the typeVec a n
, and if it matches, then the constraintn ~ Zero
is brought into scope. On the other hand, a pattern with the typeVec a Zero
is type-restricted to only be applicable to typesVec a Zero
. In your definition ofappend
, the input has typeVec a n
, so a pattern of typeVec a Zero
won't match.(You can read more about pattern synonym types, which may be enlightening, in the docs.)
This may be easier to see with an even simpler example and the use of pattern synonyms.
Consider this type and function:
All is well. But, if we change the sixth line to
then we will get an error very much like the one you're seeing in
append
. Let's play around with pattern synonyms now. What if we had a pattern synonym aroundBar
with the simple typeFoo Int
:If we use that in
doFoo
, we get the same error that the pattern type doesn't match. This really does make sense, because this pattern is only defined for inputs of typeFoo Int
and not generically onFoo a
. Let's try another variation:Note the use of
<-
here instead of=
, making this a unidirectional pattern synonym instead of a bidirectional one. We must do this because while we can "forget" aboutInt
and go from aFoo Int
to aFoo a
, we cannot do the reverse. But, what happens if we try usingBarA
indoFoo
? Now we get an error like this:This pattern is loose enough to be accepted, but after the pattern match, we still have no knowledge about
a
, so we can't return anInt
.To really recreate the
Bar
pattern, we'd need to write:Here, our pattern type indicates that there is no restriction ahead of time to applying the pattern (the initial
() =>
), after the match we'll knowa ~ Int
, and this pattern can match on anything of the formFoo a
.