Why does removing an empty constraint cause a compiler error?

user_4040600 0
Viewed 59

I observed some behavior I don't quite understand. Here's a MWE

{-# Language PatternSynonyms, GADTs #-}
module Test where

data Succ a
data Zero

data Vec n a where
  EmptyVec :: Vec Zero a
  (:+) :: a -> Vec n a -> Vec (Succ n) a

newtype Comp f g a = Comp (f (g a))

pattern CEv :: () => (n ~ Zero) => Comp (Vec n) g a
pattern CEv = Comp EmptyVec

t :: Comp (Vec m) (Vec n) r -> Bool
t (Comp (_ :+ _)) = True
t CEv = False

This compiles. However we might notices that CEv has two constraints, () => and (n ~ Zero) =>. Since one of these is empty there can't be any harm in removing it right? Well if we remove it t breaks.

pattern CEv :: (n ~ Zero) => Comp (Vec n) g a
pattern CEv = Comp EmptyVec


/XXXXXXX/src/Test.hs:18:3: error:
    • Couldn't match type ‘m’ with ‘Zero’ arising from a pattern
      ‘m’ is a rigid type variable bound by
        the type signature for:
          t :: forall m n r. Comp (Vec m) (Vec n) r -> Bool
        at src/Test.hs:16:1-35
    • In the pattern: CEv
      In an equation for ‘t’: t CEv = False
    • Relevant bindings include
        t :: Comp (Vec m) (Vec n) r -> Bool (bound at src/Test.hs:17:1)
   |
18 | t CEv = False
   |   ^^^

I really don't know what's going on here. Why does removing an empty constraint cause this to break? What is the difference between the two types?

pattern-matching haskell
1 Answers

Pattern synonyms have two sets of constraints: required and provided constraints.

pattern P :: Req => Prov => T

If there is only one constraint (i.e., one "=>" arrow), it is interpreted as a required constraint:

pattern P :: Req => T  -- means  Req => () => T, with an empty Prov = ()

So if you have an empty required constraint, there is no abbreviation for it:

pattern P :: () => Prov => T

Removing () there turns the Prov constraint into a required constraint, which has a different meaning (cf. the GHC user guide section on Pattern synonyms).

user_68637490
Related