Interaction between GADTs and ScopedTypeVariables/PatternSignatures

Question

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.)

user_14802384 · Answer

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:

    * Couldn't match type `n' with 'Zero
      `n' 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
        Actual type: Vec a 'Zero
    * When checking that the pattern signature: Vec a 'Zero
        fits the type of its context: Vec a n
      In the pattern: Nil :: Vec a Zero

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 simply Vec a Zero; it's actually something like () => (n ~ Zero) => Vec a n. This type says that the pattern may match on anything of the type Vec a n, and if it matches, then the constraint n ~ Zero is brought into scope. On the other hand, a pattern with the type Vec a Zero is type-restricted to only be applicable to types Vec a Zero. In your definition of append, the input has type Vec a n, so a pattern of type Vec 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:

data Foo a where
  Bar :: Foo Int
  Baz :: Foo Char

doFoo :: Foo a -> a
doFoo Bar = 1
doFoo Baz = 'c'

All is well. But, if we change the sixth line to

doFoo (Bar :: Foo Int) = 1

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 around Bar with the simple type Foo Int:

{-# LANGUAGE PatternSynonyms #-}
pattern BarInt :: Foo Int
pattern BarInt = Bar

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 type Foo Int and not generically on Foo a. Let's try another variation:

pattern BarA :: Foo a
pattern BarA <- Bar

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" about Int and go from a Foo Int to a Foo a, we cannot do the reverse. But, what happens if we try using BarA in doFoo? Now we get an error like this:

    * Couldn't match expected type `a' with actual type `Int'
      `a' is a rigid type variable bound by
        the type signature for:
          dofoo :: forall a. Foo a -> a

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 an Int.

To really recreate the Bar pattern, we'd need to write:

pattern Bar' :: () => (a ~ Int) => Foo a
pattern Bar' = Bar

Here, our pattern type indicates that there is no restriction ahead of time to applying the pattern (the initial () =>), after the match we'll know a ~ Int, and this pattern can match on anything of the form Foo a.

Interaction between GADTs and ScopedTypeVariables/PatternSignatures

1 Answers