Internal error when using equality constraint in pattern synonyms

While going through Extensible datatypes I had the following code:

{-# LANGUAGE GADTs, PatternSynonyms, ScopedTypeVariables, Rank2Types #-}

data Rep a where
  RUnit   :: Rep ()
  RInt    :: Rep Int
  RChar   :: Rep Char
  REither :: Rep a -> Rep b -> Rep (Either a b)
  RPair   :: Rep a -> Rep b -> Rep (a, b)

foo :: (Rep a, a) -> Bool
foo (RUnit, ()) = True

And I wanted to make a pattern synonyms matching (RUnit, ()) in foo, my initial attempt was:

pattern PUnit1 = (RUnit, ())

gives the error (punit1.log) while writing

pattern PUnit2 = (RUnit, ()) :: (Rep (), ())

compiles but can't be used in foo.

Trying:

pattern PUnit3 = (RUnit, ()) :: (a ~ ()) => (Rep a, a)

gives a GHC internal error (punit3.log). I tried various other patterns such as:

pattern PUnit4 <- (RUnit, ())
pattern PUnit5 <- (RUnit, ()) :: (Rep (), ())
pattern PUnit6 <- (RUnit, ()) :: (a ~ ()) => (Rep a, a)
pattern PUnit7 =  (RUnit, ()) :: forall a. (a ~ ()) => (Rep a, a)
pattern PUnit8 <- (RUnit, ()) :: forall a. (a ~ ()) => (Rep a, a)
...

None of which work. The final goal was to rewrite:

eq :: Rep a -> a -> a -> Bool
eq rep a b = case (rep, a, b) of
  (RUnit, (), ())                 -> True
  (RInt, n1, n2)                  -> n1 == n2
  (RChar, c1, c2)                 -> c1 == c2
  (REither l r, Left a, Left b)   -> eq l a b
  (REither l r, Right a, Right b) -> eq r a b
  (REither{}, _, _)               -> False
  (RPair l r, (a1, a2), (b1, b2)) -> eq l a1 b1 && eq r a2 b2

as something like

pattern PUnit  = (RUnit, ())        -- (a ~ ())  => (Rep a, a)
pattern PInt n = (RInt, n)          -- (a ~ Int) => (Rep a, a)
-- ... 

eq :: Rep a -> a -> a -> Bool
eq rep a b = case ((rep, a), (rep, b)) of
  (PUnit,           PUnit)           -> True
  (PInt n1,         PInt n2)         -> n1 == n2
  (PChar c1,        PChar c2)        -> c1 == c2
  (PLeft l l1,      PLeft l l2)      -> eq l l1 l2
  (PRight r r1,     PRight r r2)     -> eq r r1 r2
  ((REither{}, _),  _)               -> False
  (PFst l (a1, b1), PSnd r (a2, b2)) -> eq l a1 b1 && eq r a2 b2

where one can avoid pattern matching against the Rep constructor directly.

Trac metadata

Trac field	Value
Version	7.8.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	lowest
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture