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 |