[GHC] #9226: Internal error when using equality constraint in pattern synonyms

[GHC]

#9226: Internal error when using equality constraint in pattern synonyms
-------------------------------------+-------------------------------------
       Reporter:  Iceland_jack       |             Owner:
           Type:  bug                |            Status:  new
       Priority:  lowest             |         Milestone:
      Component:  Compiler           |           Version:  7.8.2
       Keywords:  renamer, pattern   |  Operating System:  Linux
  synonyms, GADTs                    |   Type of failure:  GHC rejects
   Architecture:  x86                |  valid program
     Difficulty:  Unknown            |         Test Case:
     Blocked By:                     |          Blocking:
Related Tickets:                     |
-------------------------------------+-------------------------------------
 While going through [http://www.andres-loeh.de/dgp2005.pdf 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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9226>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler