Opened 3 years ago

Closed 3 years ago

Last modified 2 years ago

#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)

punit1.log (961 bytes) - added by Iceland_jack 3 years ago.
punit3.log (449 bytes) - added by Iceland_jack 3 years ago.

Download all attachments as: .zip

Change History (8)

Changed 3 years ago by Iceland_jack

Attachment: punit1.log added

Changed 3 years ago by Iceland_jack

Attachment: punit3.log added

comment:1 Changed 3 years ago by simonpj

Cc: cactus added

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 has PatSynSig, but the parser does not recognise them, nor does the typechechecker do anything with them. Notably, in tcPatSynDecl 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

pattern PUnit1 = (RUnit, ()) :: (Rep a, a)

crashes with

T9226.hs:15:38:
    GHC internal error: ‘a’ is not in scope during type checking, but it passed the renamer

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

comment:2 Changed 3 years ago by kosmikus

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 Iceland_jack

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 simonpj

I'd forgotten all about #8968. Yes, this ticket is really a dup of #8968.

comment:5 Changed 3 years ago by cactus

Resolution: duplicate
Status: newclosed

comment:6 Changed 2 years ago by cactus

Keywords: PatternSynonyms added; pattern synonyms removed
Note: See TracTickets for help on using tickets.