#9226 closed bug (duplicate)
Internal error when using equality constraint in pattern synonyms
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | lowest | Milestone: | |
Component: | Compiler | Version: | 7.8.2 |
Keywords: | renamer, PatternSynonyms, GADTs | Cc: | cactus |
Operating System: | Linux | Architecture: | x86 |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #8968 | Differential Rev(s): | |
Wiki Page: |
Description
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.
Attachments (2)
Change History (8)
Changed 3 years ago by
Attachment: | punit1.log added |
---|
Changed 3 years ago by
Attachment: | punit3.log added |
---|
comment:1 Changed 3 years ago by
Cc: | cactus added |
---|
comment:2 Changed 3 years ago by
Related Tickets: | → #8968 |
---|
Also see #8968 for my own experiences trying to use pattern synonyms for GADTs and lots of discussion.
comment:3 Changed 3 years ago by
The example wasn't anything serious so I can cope.
Seeing how I've filed 4 reports about pattern synonyms in such a short time I seem to be abusing the extension somehow :) the response time here is jolly good, thank you for your efforts
comment:4 Changed 3 years ago by
comment:5 Changed 3 years ago by
Resolution: | → duplicate |
---|---|
Status: | new → closed |
comment:6 Changed 2 years ago by
Keywords: | PatternSynonyms added; pattern synonyms removed |
---|
You are absolutely right; there is a gaping hole in the pattern-synonym implementation.
Gergo, the issue is this. When typechecking anything to do with GADTs, we need a type signature. The wiki page describes signatures for pattern synonyms, but they are not implemented. the
HsBinds.Sig
type hasPatSynSig
, but the parser does not recognise them, nor does the typechechecker do anything with them. Notably, intcPatSynDecl
we'll need to implement different code to check that the synonym has a specified type than to infer the type it has.While fixing this, I found another crash. This
crashes with
Would you like to look at this Gergo? I'm happy to help.
Meanwhile, iceland_jack, I think you're stalled till we do this. Thanks for reporting it.
Simon