Opened 17 months ago

Closed 16 months ago

Last modified 16 months ago

#11224 closed bug (fixed)

Program doesn't preserve semantics after pattern synonym inlining.

Reported by: anton.dubovik Owned by:
Priority: highest Milestone: 8.0.1
Component: Compiler Version: 7.10.2
Keywords: PatternSynonyms Cc: mpickering
Operating System: Windows Architecture: x86_64 (amd64)
Type of failure: Incorrect result at runtime Test Case: patsyn/should_run/T11224
Blocked By: Blocking:
Related Tickets: #11225 Differential Rev(s): Phab:D1632
Wiki Page:

Description

{-# language
   PatternSynonyms
 , ViewPatterns
 #-}

import Text.Read

-- pattern PRead :: () => Read a => a -> String
pattern PRead a <- (readMaybe -> Just a)

foo :: String -> Int
foo (PRead x)  = (x::Int)
foo (PRead xs) = sum (xs::[Int])
foo _ = 666

bar :: String -> Int
bar (readMaybe -> Just x)  = (x::Int)
bar (readMaybe -> Just xs) = sum (xs::[Int])
bar _ = 666

main :: IO ()
main = do
  print $ foo "1"       -- 1
  print $ foo "[1,2,3]" -- 666 -- ???
  print $ foo "xxx"     -- 666

  print $ bar "1"       -- 1
  print $ bar "[1,2,3]" -- 6
  print $ bar "xxx"     -- 666

I'm expecting that semantics of the function foo would not change if I inline pattern synonym.

However it does. bar successfully matches string against list of ints, whereas foo apperently skips this pattern and fall back to the catch-all case.

Reproducible both in GHCi and GHC.

Change History (29)

comment:1 Changed 17 months ago by bgamari

Indeed this looks fishy.

Phab:D1622 adds a testcase for this issue.

comment:2 Changed 17 months ago by bgamari

Cc: mpickering added
Milestone: 8.0.1

comment:3 Changed 17 months ago by mpickering

I'm a bit out of my depth here but an immediate problem is that it's not possible to write down the correct type signature for PRead.

I think it should be pattern PRead :: Read a => a -> String which GHC rejects because the required constraints mention the existentially quantified a.

It is even more baffling though that with this type signature that GHC still fails to typecheck the code, it only typechecks with the inferred type. I'm doing a bit more investigating now but I think only Richard or Simon will be able to give a better account.

comment:4 Changed 17 months ago by mpickering

Here is the result of the trace statement tc_patsyn_finish.

tc_patsyn_finish {
  PRead
  (readMaybe -> Just a_aqs)
  ([a_a2aU[sk]], [Read a_a2aU[sk]], EvBindsVar<a2b0>, [$dRead_a2FA])
  ([], [], [], EvBinds{}, [])
  [(a_aqs, <>)]
  String

which is from

        traceTc "tc_patsyn_finish {" $
           ppr (unLoc lname) $$ ppr (unLoc lpat') $$
           ppr (univ_tvs, req_theta, req_ev_binds, req_dicts) $$
           ppr (ex_tvs, subst, prov_theta, prov_ev_binds, prov_dicts) $$
           ppr wrapped_args $$
           ppr pat_ty

So here, the a is inferred to be *universally* quantified even though it doesn't appear in the result type. Which explains why adding a type signature which says that a is existentially quantified causes the program to fail to compile.

comment:5 Changed 17 months ago by mpickering

I think the problem is in this part of tcTySig

       ; let (_, pat_ty) = tcSplitFunTys ty'
             univ_set = tyCoVarsOfType pat_ty
             (univ_tvs, ex_tvs) = partition (`elemVarSet` univ_set) qtvs'

Maybe the correct solution is to avoid splitting tyvars into ex/univ at this stage as it's impossible to tell which they are without looking at the pattern.

comment:6 Changed 17 months ago by mpickering

comment:7 Changed 17 months ago by goldfire

Oh dear. This example illustrates that I, for one, don't have a grasp on pattern synonym signatures. I had assumed that the universals were precisely those variables mentioned in the result. But that's not true here, because a really is a universal, not an existential. So I'm clearly confused. And that sad state of affairs isn't going to be fixed at 11pm at night, so perhaps I'll return to this tomorrow.

comment:8 Changed 17 months ago by goldfire

OK. So here's my current stream of thought:

  • The universals are those variables that appear in either the result or in the required context.

Except that's not quite right in pathological cases, like this:

data Ex = forall a. Ex a
magic :: Ex -> a
magic _ = undefined

pattern Silly x <- (magic -> x)

As I understand it, the signature for Silly should be

pattern type Silly :: a -> Ex

Here, a is universal. But a is mentioned neither in the result nor in the required context. Compare to

pattern type Sensible :: a -> Ex
pattern Sensible x = Ex x

Here, a is existential. But the pattern signature is otherwise identical! So we can't infer the universal/existential decision from the signature.

I thus propose the following revision to pattern signatures:

  • Allow explicit quantification in two places, according to this schema:
    pattern type Syn :: forall <<univs>>. <<req>> => forall <<exs>>. <<prov>> => <<args>> -> <<result>>
    
  • In the absence of explicit quantification, universals are inferred to be the variables mentioned in either the result or the required context. Existentials are the remaining variables.
  • It is against the rules for existentials to shadow universals.

According to these rules, the signature given for Silly above would be rejected, as a is inferred to be existential, but in the pattern synonym, it really is universal. Instead, the user would have to write

pattern type Silly :: forall a. a -> Ex

What's terribly unfortunate here is that this new, revised signature for Silly seems to add simply a redundant forall... the sort of thing Haskell infers all the time. Except here it says "a is universal". Contrast to the explicit form of Sensible's signature:

pattern type Sensible :: () => forall a. a -> Ex

which is quite ugly.

This all makes me want the incredibly verbose syntax in comment:5:ticket:10928, repeated here for convenience:

pattern type P :: { universals = ...
                  , existentials = ...
                  , provided = ...
                  , required = ...
                  , arguments = ...
                  , result = ... }

A worked out example appears in that comment. We would allow a short-hand in common cases (yet to be worked out). This syntax is annoying to write, but surely a pleasure to read. And it reminds readers that the thing to the right of pattern type Blah :: is not a type.

comment:9 Changed 17 months ago by goldfire

Priority: normalhighest

Bumping priority as whatever our decision is, we should make it and implement it soon, as it will likely not be fully backward compatible, and I don't want this sand shifting between 7.10 and 8.0 and then again between 8.0 and 8.2.

comment:10 Changed 17 months ago by mpickering

That sounds right Richard but there is also another bug here that inlining the synonym changes the semantics. That shouldn't get lost either.

comment:11 Changed 17 months ago by mpickering

Keywords: PatternSynonyms added

comment:12 in reply to:  10 Changed 17 months ago by goldfire

Replying to mpickering:

That sounds right Richard but there is also another bug here that inlining the synonym changes the semantics. That shouldn't get lost either.

Yes. We need to test that. But I think the problem is due to universal/existential confusion when implementing pattern synonyms, and that sorting it out will fix the original bug. This assumption could very well be wrong.

comment:13 Changed 17 months ago by mpickering

I think the solution you propose is very confusing to users. I think we should be able to do better inferring whether a type variable univ/ex especially as GHC already manages to infer the correct signature. Doing so would require looking at the pattern synonym itself but I don't think this is too bad?

comment:14 Changed 17 months ago by mpickering

The original report triggers a core lint error.

*** Core Lint errors : in result of Desugar (before optimization) ***
T11224.hs:12:12: warning:
    [RHS of xs_aqv :: [Int]]
    The type of this binder doesn't match the type of its RHS: xs_aqv
    Binder's type: [Int]
    Rhs type: Int
*** Offending Program ***
Rec {
$dRead_a2FJ :: Read Int
[LclId, Str=DmdType]
$dRead_a2FJ = $dRead_a148

$dRead_a2FO :: Read [Int]
[LclId, Str=DmdType]
$dRead_a2FO = $dRead_a14j

$dRead_a14j :: Read [Int]
[LclId, Str=DmdType]
$dRead_a14j = $fRead[] @ Int $dRead_a148

$dRead_a148 :: Read Int
[LclId, Str=DmdType]
$dRead_a148 = $fReadInt

$dFoldable_a2FR :: Foldable []
[LclId, Str=DmdType]
$dFoldable_a2FR = $dFoldable_a21o

$dFoldable_a21o :: Foldable []
[LclId, Str=DmdType]
$dFoldable_a21o = $fFoldable[]

$dNum_a2FV :: Num Int
[LclId, Str=DmdType]
$dNum_a2FV = $dNum_a2aM

$dNum_a2aM :: Num Int
[LclId, Str=DmdType]
$dNum_a2aM = $fNumInt

$dMonad_a2QC :: Monad IO
[LclId, Str=DmdType]
$dMonad_a2QC = $dMonad_a2Gj

$dMonad_a2Ql :: Monad IO
[LclId, Str=DmdType]
$dMonad_a2Ql = $dMonad_a2Gj

$dMonad_a2Q4 :: Monad IO
[LclId, Str=DmdType]
$dMonad_a2Q4 = $dMonad_a2Gj

$dMonad_a2PN :: Monad IO
[LclId, Str=DmdType]
$dMonad_a2PN = $dMonad_a2Gj

$dMonad_a2Gj :: Monad IO
[LclId, Str=DmdType]
$dMonad_a2Gj = $fMonadIO

$dShow_a2QT :: Show Int
[LclId, Str=DmdType]
$dShow_a2QT = $dShow_a2PG

$dShow_a2QM :: Show Int
[LclId, Str=DmdType]
$dShow_a2QM = $dShow_a2PG

$dShow_a2Qv :: Show Int
[LclId, Str=DmdType]
$dShow_a2Qv = $dShow_a2PG

$dShow_a2Qe :: Show Int
[LclId, Str=DmdType]
$dShow_a2Qe = $dShow_a2PG

$dShow_a2PX :: Show Int
[LclId, Str=DmdType]
$dShow_a2PX = $dShow_a2PG

$dShow_a2PG :: Show Int
[LclId, Str=DmdType]
$dShow_a2PG = $fShowInt

bar :: String -> Int
[LclId, Str=DmdType]
bar =
  letrec {
    bar_aLd :: String -> Int
    [LclId, Str=DmdType]
    bar_aLd =
      \ (ds_d3jj :: String) ->
        let {
          fail_d3kF :: Void# -> Int
          [LclId, Str=DmdType]
          fail_d3kF =
            \ (ds_d3kG [OS=OneShot] :: Void#) ->
              let {
                fail_d3kD :: Void# -> Int
                [LclId, Str=DmdType]
                fail_d3kD = \ (ds_d3kE [OS=OneShot] :: Void#) -> I# 666# } in
              let {
                ds_d3kC :: Maybe [Int]
                [LclId, Str=DmdType]
                ds_d3kC = readMaybe @ [Int] $dRead_a14j ds_d3jj } in
              case ds_d3kC of wild_00 {
                __DEFAULT -> fail_d3kD void#;
                Just xs_azI -> sum @ [] $dFoldable_a21o @ Int $dNum_a2aM xs_azI
              } } in
        let {
          ds_d3kB :: Maybe Int
          [LclId, Str=DmdType]
          ds_d3kB = readMaybe @ Int $dRead_a148 ds_d3jj } in
        case ds_d3kB of wild_00 {
          __DEFAULT -> fail_d3kF void#;
          Just x_azH -> x_azH
        }; } in
  bar_aLd

$mPRead
  :: forall (rlev_a2FC :: Levity) (r_a2FD :: TYPE rlev_a2FC) a_a2aV.
     Read a_a2aV =>
     String -> (a_a2aV -> r_a2FD) -> (Void# -> r_a2FD) -> r_a2FD
[LclIdX[PatSynId], Str=DmdType]
$mPRead =
  \ (@ (rlev_a2FC :: Levity))
    (@ (r_a2FD :: TYPE rlev_a2FC))
    (@ a_a2aV)
    ($dRead_a2FB :: Read a_a2aV)
    (scrut_a2FE :: String)
    (cont_a2FF :: a_a2aV -> r_a2FD)
    (fail_a2FG :: Void# -> r_a2FD) ->
    let {
      $dRead_a2aX :: Read a_a2aV
      [LclId, Str=DmdType]
      $dRead_a2aX = $dRead_a2FB } in
    let {
      ds_d3kH :: String
      [LclId, Str=DmdType]
      ds_d3kH = scrut_a2FE } in
    let {
      fail_d3kL :: Void# -> r_a2FD
      [LclId, Str=DmdType]
      fail_d3kL =
        \ (ds_d3kM [OS=OneShot] :: Void#) -> fail_a2FG void# } in
    let {
      ds_d3kK :: Maybe a_a2aV
      [LclId, Str=DmdType]
      ds_d3kK = readMaybe @ a_a2aV $dRead_a2aX ds_d3kH } in
    case ds_d3kK of wild_00 {
      __DEFAULT -> fail_d3kL void#;
      Just a_aqt -> cont_a2FF a_aqt
    }

foo :: String -> Int
[LclId, Str=DmdType]
foo =
  letrec {
    foo_a2FH :: String -> Int
    [LclId, Str=DmdType]
    foo_a2FH =
      \ (ds_d3kN :: String) ->
        let {
          fail_d3m5 :: Void# -> Int
          [LclId, Str=DmdType]
          fail_d3m5 = \ (ds_d3m6 [OS=OneShot] :: Void#) -> I# 666# } in
        $mPRead
          @ 'Lifted
          @ Int
          @ Int
          $dRead_a2FJ
          ds_d3kN
          (\ (x_aqu :: Int) ->
             let {
               xs_aqv :: [Int]
               [LclId, Str=DmdType]
               xs_aqv = x_aqu } in
             x_aqu)
          (\ (void_0E :: Void#) -> fail_d3m5 void#); } in
  foo_a2FH

main :: IO ()
[LclIdX, Str=DmdType]
main =
  letrec {
    main_a2G0 :: IO ()
    [LclId, Str=DmdType]
    main_a2G0 =
      >>
        @ IO
        $dMonad_a2Gj
        @ ()
        @ ()
        ($ @ 'Lifted
           @ Int
           @ (IO ())
           (print @ Int $dShow_a2PG)
           (foo (unpackCString# "1"#)))
        (>>
           @ IO
           $dMonad_a2PN
           @ ()
           @ ()
           ($ @ 'Lifted
              @ Int
              @ (IO ())
              (print @ Int $dShow_a2PX)
              (foo (unpackCString# "[1,2,3]"#)))
           (>>
              @ IO
              $dMonad_a2Q4
              @ ()
              @ ()
              ($ @ 'Lifted
                 @ Int
                 @ (IO ())
                 (print @ Int $dShow_a2Qe)
                 (foo (unpackCString# "xxx"#)))
              (>>
                 @ IO
                 $dMonad_a2Ql
                 @ ()
                 @ ()
                 ($ @ 'Lifted
                    @ Int
                    @ (IO ())
                    (print @ Int $dShow_a2Qv)
                    (bar (unpackCString# "1"#)))
                 (>>
                    @ IO
                    $dMonad_a2QC
                    @ ()
                    @ ()
                    ($ @ 'Lifted
                       @ Int
                       @ (IO ())
                       (print @ Int $dShow_a2QM)
                       (bar (unpackCString# "[1,2,3]"#)))
                    ($ @ 'Lifted
                       @ Int
                       @ (IO ())
                       (print @ Int $dShow_a2QT)
                       (bar (unpackCString# "xxx"#))))))); } in
  main_a2G0

$trModule :: Module
[LclIdX[ReflectionId], Str=DmdType]
$trModule = Module (TrNameS "main"#) (TrNameS "Main"#)

main :: IO ()
[LclIdX, Str=DmdType]
main = runMainIO @ () main
end Rec }

*** End of Offense ***

comment:15 Changed 17 months ago by mpickering

The relevant function which is definitely wrong..

foo :: String -> Int
[LclId, Str=DmdType]
foo =
  letrec {
    foo_a2FH :: String -> Int
    [LclId, Str=DmdType]
    foo_a2FH =
      \ (ds_d3kN :: String) ->
        let {
          fail_d3m5 :: Void# -> Int
          [LclId, Str=DmdType]
          fail_d3m5 = \ (ds_d3m6 [OS=OneShot] :: Void#) -> I# 666# } in
        $mPRead
          @ 'Lifted
          @ Int
          @ Int
          $dRead_a2FJ
          ds_d3kN
          (\ (x_aqu :: Int) ->
             let {
               xs_aqv :: [Int]
               [LclId, Str=DmdType]
               xs_aqv = x_aqu } in
             x_aqu)
          (\ (void_0E :: Void#) -> fail_d3m5 void#); } in
  foo_a2FH

comment:16 Changed 17 months ago by Matthew Pickering <matthewtpickering@…>

In a701694b/ghc:

Add testcase for #11224

Test Plan: Validate

Reviewers: austin, mpickering

Reviewed By: mpickering

Subscribers: mpickering, thomie

Differential Revision: https://phabricator.haskell.org/D1622

GHC Trac Issues: #11224

comment:17 Changed 17 months ago by mpickering

Differential Rev(s): Phab:D1632

comment:18 Changed 17 months ago by rvion

Hello,

will expressions like:

module Data.Aeson.Types.AsJs where
import qualified Data.Aeson.Types as I
pattern JsOptions a b c d e <- I.Options a b c d e

keep working correctly after this fix ?

I use patterns a lot to automatically reexport "qualified" modules. (WIP project) see example here: https://github.com/rvion/ride/blob/94767d043b33fa5702852fba384b4e6dcf4007a5/jetpack/src/Data/Aeson/Types/AsJs.hs#L38 or here: https://github.com/rvion/ride/blob/94767d043b33fa5702852fba384b4e6dcf4007a5/jetpack/src/Codec/Archive/Tar/AsTar.hs#L44

Otherwise, according to http://mpickering.github.io/posts/2015-12-12-pattern-synonyms-8.html, most of my remaining issues seems to be solved in HEAD, thanks very much for all those great enhancements!

comment:19 Changed 17 months ago by mpickering

Which fix are you talking about? This ticket is quite muddled, we have mainly discussed #11225 but I have now fixed this ticket.

However, your usecase looks quite simple and I suspect unrelated to this ticket.

comment:20 in reply to:  19 Changed 17 months ago by rvion

Replying to mpickering:

Which fix are you talking about? This ticket is quite muddled, we have mainly discussed #11225 but I have now fixed this ticket.

Sorry, I didn't read this ticket correctly. Don't mind my previous message.

However, your usecase looks quite simple and I suspect unrelated to this ticket.

Yes, you're right, my bad.

comment:21 Changed 17 months ago by simonpj

rvion: if there's an issue, and it's not the issue in this ticket, would you like to open a ticket of your own?

comment:22 Changed 17 months ago by simonpj

OK, back to this ticket. I think we were just getting ourselves confused.

  • The type of PRead is definitely
    pattern PRead :: Read a => () => a -> String
    
    That is, (Read a) is required (to perform the match), not provided (by being bound by the match). And a is certainly not existential.
  • The existential type variables are simply the ones bound existentially by the actual pattern. As Matthew says, we can't work out which ones they are by looking at the type (that was a hefalump trap, which I fell into). In this example, there are no existential variables.
  • We have a perfectly good function that discovers which the existential variables are, called tcCollectEx. It's used in the inference case and we can certainly use it in the checking case too.
  • Since we can't tell which is which before tcCheckPatSyn, we should not split them up in TcBinds.tcTySig. They can all be in one list in the TPSI record.
  • Looking at tcCheckPatSyn it's a good deal more complicated than necessary. I'll fix that.

comment:23 Changed 17 months ago by goldfire

But how should we tell universals from existentials? If I say

pattern type P :: a -> String

is a universal or existential? It seems mpickering wants the answer to be "it depends on the definition for P". That may well be implementable, but it negates a critical property of type signatures: that they give a specification of how a pattern synonym behaves absent its definition. We somehow have to be able to specify this in the signature itself.

I don't have much perspective on Simon's comment:22. It's about implementation, and I'm still stuck on design.

comment:24 Changed 17 months ago by simonpj

Right. To typecheck a program involving P we absolutely need to know the universal/existential split.

Above, I was thinking that we could use the pattern type signature to specify the "shape" of the type, but work out the univ/existential split from the definition itself. A bit like a type with wildcards. But that would mean that you could not typecheck uses of a pattern synonym solely from its signature; because the signature does not say enough. Like wildcards, inference would be involved. But that's obviously unsatisfactory; for example, you could not put a pattern synonym signature in a hs-boot file.

So, if we want signatures to be fully precise (i.e. say everything), and I think that is a solidly good goal, we'd need to require the user to specify the required/provided split for type variables too.

Terminology:

  • "Universal" for type variables lines up with "required" for the constraints
  • "Existential" for type variables lines up with "provided" for the constraints

Now, we need syntax for expressing the split. I suppose we can use the same nested structure as we do for required/provided, like this:

pattern type P1 :: forall a. a -> T a        -- a is universal

pattern type P2 :: forall a. Eq a => a -> T  -- a is universal, (Eq a) is required

pattern type P3 :: forall a. Eq a =>         -- a is universal, (Eq a) is required
                   forall b. a -> b -> T a   -- b is existential

pattern type P3 :: forall a. Eq a =>         -- a is universal, (Eq a) is required
                   forall b. Ord b =>        -- b is existential, (Ord b) is provided
                   a -> b -> T a

Note:

  • I think we could safely leave out the leading (universal) forall, in the usual way. That is, the free vars of the entire type are considered universal.
  • You can never leave out the existential forall, if it binds any variables.
  • How can you distinguish the existential forall if the universal forall and context are absent? Only by putting in the universal forall or the required context; e.g.
    pattern type P5 :: forall. forall b. b -> T
    pattern type P6 :: () => forall b. b -> T
    

The only downside of this is that you might say that given

pattern type P :: a -> (a->Int) -> T

the a is almost certain to be existential. After all this is the type we'd give to a data constructor:

data T where
  MkT :: (a->Int) -> a -> T

So why do we need explicitly-specified existentials in a pattern synonym, but not in a data constructor? Because a view pattern could make it universal. Degenerately in this case:

pattern Q :: a -> (a->Int) -> String
pattern Q x y <- (odd_fun -> (x,y))

odd_fun :: String -> (a, a->Int)
odd_fun _ = (undefined, const 2)

Conclusion: we need the possibility of explicitly-specified existentials.

However, rather than insisting that you always specify the existential forall, here is a rule that would catch the common cases: if you don't specify the existential forall, you get:

  • the free vars of the arg-tys
  • plus the free vars of the provided constraints (if any),
  • minus
    • the universal forall'd vars, if there is a universal forall
    • or the free vars of the result ty, plus required constraints (if any), otherwise

If neither forall is given, we compute the existential variables using the above rule; then the universals are the remaining free variables.

So in the signatures that started this ticket

pattern Q1 :: () => Read a => a -> String
pattern Q2 :: Read a => a -> String

would behave as if you had written

pattern Q1 :: () => forall a. Read a => a -> String
pattern Q2 :: forall a. Read a => a -> String

The advantage of this rule is that is allows you to omit both foralls in all but the most degenerate cases like Q above.

How does that sound? I think it is more or less what Richard was proposing in comment:8, but it's taken me a while to catch up.

comment:25 Changed 17 months ago by goldfire

If I understand correctly, Simon's comment:24 proposes precisely this, copied from comment:8:

  • Allow explicit quantification in two places, according to this schema:
        pattern type Syn :: forall <<univs>>. <<req>> => forall <<exs>>. <<prov>> => <<args>> -> <<result>>
    
  • In the absence of explicit quantification, universals are inferred to be the variables mentioned in either the result or the required context. Existentials are the remaining variables.
  • It is against the rules for existentials to shadow universals.

Simon, do you agree that we're saying the same thing? If so, then let's do it!

comment:26 Changed 16 months ago by Ben Gamari <ben@…>

In f40e122/ghc:

Fix typechecking for pattern synonym signatures

Various tickets have revealed bad shortcomings in the typechecking of
pattern type synonyms.  Discussed a lot in (the latter part of)
Trac #11224.

This patch fixes the most complex issues:

- Both parser and renamer now treat pattern synonyms as an
  ordinary LHsSigType.  Nothing special.  Hooray.

- tcPatSynSig (now in TcPatSyn) typechecks the signature, and
  decomposes it into its pieces.
  See Note [Pattern synonym signatures]

- tcCheckPatSyn has had a lot of refactoring.
  See Note [Checking against a pattern signature]

The result is a lot tidier and more comprehensible.
Plus, it actually works!

NB: this patch doesn't actually address the precise
    target of #11224, namely "inlining pattern synonym
    does not preserve semantics".  That's an unrelated
    bug, with a separate patch.

ToDo: better documentation in the user manual

Test Plan: Validate

Reviewers: austin, hvr, goldfire

Subscribers: goldfire, mpickering, thomie, simonpj

Differential Revision: https://phabricator.haskell.org/D1685

GHC Trac Issues: #11224

comment:27 Changed 16 months ago by mpickering

Resolution: fixed
Status: newclosed

comment:28 Changed 16 months ago by simonpj

Test Case: patsyn/should_run/T11224

comment:29 Changed 16 months ago by simonpj

This commit is the one that fixes the original (semantic) problem

29928f29d53cfc7aceb7e8ab81967f784cf06159
 compiler/deSugar/Match.hs | 86 +++++++++++++++++++++++++++++------------------
 1 file changed, 54 insertions(+), 32 deletions(-)

diff --git a/compiler/deSugar/Match.hs b/compiler/deSugar/Match.hs index f551fa4..b5a50e7 100644
--- a/compiler/deSugar/Match.hs
+++ b/compiler/deSugar/Match.hs
@@ -196,15 +196,15 @@ match vars@(v:_) ty eqns    -- Eqns *can* be empty
     match_group [] = panic "match_group"
     match_group eqns@((group,_) : _)
         = case group of
-            PgCon _    -> matchConFamily  vars ty (subGroup [(c,e) | (PgCon c, e) <- eqns])
-            PgSyn _    -> matchPatSyn     vars ty (dropGroup eqns)
-            PgLit _    -> matchLiterals   vars ty (subGroup [(l,e) | (PgLit l, e) <- eqns])
-            PgAny      -> matchVariables  vars ty (dropGroup eqns)
-            PgN _      -> matchNPats      vars ty (dropGroup eqns)
-            PgNpK _    -> matchNPlusKPats vars ty (dropGroup eqns)
-            PgBang     -> matchBangs      vars ty (dropGroup eqns)
-            PgCo _     -> matchCoercion   vars ty (dropGroup eqns)
-            PgView _ _ -> matchView       vars ty (dropGroup eqns)
+            PgCon {}  -> matchConFamily  vars ty (subGroup [(c,e) | (PgCon c, e) <- eqns])
+            PgSyn {}  -> matchPatSyn     vars ty (dropGroup eqns)
+            PgLit {}  -> matchLiterals   vars ty (subGroup [(l,e) | (PgLit l, e) <- eqns])
+            PgAny     -> matchVariables  vars ty (dropGroup eqns)
+            PgN {}    -> matchNPats      vars ty (dropGroup eqns)
+            PgNpK {}  -> matchNPlusKPats vars ty (dropGroup eqns)
+            PgBang    -> matchBangs      vars ty (dropGroup eqns)
+            PgCo {}   -> matchCoercion   vars ty (dropGroup eqns)
+            PgView {} -> matchView       vars ty (dropGroup eqns)
             PgOverloadedList -> matchOverloadedList vars ty (dropGroup eqns)
 
     -- FIXME: we should also warn about view patterns that should be @@ -789,7 +789,7 @@ data PatGroup
   = PgAny               -- Immediate match: variables, wildcards,
                         --                  lazy patterns
   | PgCon DataCon       -- Constructor patterns (incl list, tuple)
-  | PgSyn PatSyn
+  | PgSyn PatSyn [Type] -- See Note [Pattern synonym groups]
   | PgLit Literal       -- Literal patterns
   | PgN   Literal       -- Overloaded literals
   | PgNpK Literal       -- n+k patterns
@@ -828,7 +828,28 @@ subGroup group
     -- pg_map :: Map a [EquationInfo]
     -- Equations seen so far in reverse order of appearance
 
-{-
+{- Note [Pattern synonym groups]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we see
+  f (P a) = e1
+  f (P b) = e2
+    ...
+where P is a pattern synonym, can we put (P a -> e1) and (P b -> e2) in 
+the same group?  We can if P is a constructor, but /not/ if P is a pattern synonym.
+Consider (Trac #11224)
+   -- readMaybe :: Read a => String -> Maybe a
+   pattern PRead :: Read a => () => a -> String
+   pattern PRead a <- (readMaybe -> Just a)
+
+   f (PRead (x::Int))  = e1
+   f (PRead (y::Bool)) = e2
+This is all fine: we match the string by trying to read an Int; if that 
+fails we try to read a Bool. But clearly we can't combine the two into 
+a single match.
+
+Conclusion: we can combine when we invoke PRead /at the same type/.  
+Hence in PgSyn we record the instantiaing types, and use them in sameGroup.
+
 Note [Take care with pattern order]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In the subGroup function we must be very careful about pattern re-ordering, @@ -841,14 +862,15 @@ sameGroup :: PatGroup -> PatGroup -> Bool
 -- Same group means that a single case expression
 -- or test will suffice to match both, *and* the order
 -- of testing within the group is insignificant.
-sameGroup PgAny      PgAny      = True
-sameGroup PgBang     PgBang     = True
-sameGroup (PgCon _)  (PgCon _)  = True          -- One case expression
-sameGroup (PgSyn p1) (PgSyn p2) = p1==p2
-sameGroup (PgLit _)  (PgLit _)  = True          -- One case expression
-sameGroup (PgN l1)   (PgN l2)   = l1==l2        -- Order is significant
-sameGroup (PgNpK l1) (PgNpK l2) = l1==l2        -- See Note [Grouping overloaded literal patterns]
-sameGroup (PgCo t1)  (PgCo t2)  = t1 `eqType` t2
+sameGroup PgAny         PgAny         = True
+sameGroup PgBang        PgBang        = True
+sameGroup (PgCon _)     (PgCon _)     = True    -- One case expression
+sameGroup (PgSyn p1 t1) (PgSyn p2 t2) = p1==p2 && eqTypes t1 t2
+                                                -- eqTypes: See Note [Pattern synonym groups]
+sameGroup (PgLit _)     (PgLit _)     = True    -- One case expression
+sameGroup (PgN l1)      (PgN l2)      = l1==l2  -- Order is significant
+sameGroup (PgNpK l1)    (PgNpK l2)    = l1==l2  -- See Note [Grouping overloaded literal patterns]
+sameGroup (PgCo t1)     (PgCo t2)     = t1 `eqType` t2
         -- CoPats are in the same goup only if the type of the
         -- enclosed pattern is the same. The patterns outside the CoPat
         -- always have the same type, so this boils down to saying that @@ -956,19 +978,19 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2
     eq_list eq (x:xs) (y:ys) = eq x y && eq_list eq xs ys
 
 patGroup :: DynFlags -> Pat Id -> PatGroup
-patGroup _      (WildPat {})                  = PgAny
-patGroup _      (BangPat {})                  = PgBang
-patGroup _      (ConPatOut { pat_con = con }) = case unLoc con of
-    RealDataCon dcon -> PgCon dcon
-    PatSynCon psyn -> PgSyn psyn
-patGroup dflags (LitPat lit)                  = PgLit (hsLitKey dflags lit)
-patGroup _      (NPat (L _ olit) mb_neg _)
-                                     = PgN   (hsOverLitKey olit (isJust mb_neg))
-patGroup _      (NPlusKPat _ (L _ olit) _ _)  = PgNpK (hsOverLitKey olit False)
-patGroup _      (CoPat _ p _)                 = PgCo  (hsPatType p) -- Type of innelexp pattern
-patGroup _      (ViewPat expr p _)            = PgView expr (hsPatType (unLoc p))
-patGroup _      (ListPat _ _ (Just _))        = PgOverloadedList
-patGroup _      pat                           = pprPanic "patGroup" (ppr pat)
+patGroup _ (ConPatOut { pat_con = L _ con
+                      , pat_arg_tys = tys })
+ | RealDataCon dcon <- con              = PgCon dcon
+ | PatSynCon psyn <- con                = PgSyn psyn tys
+patGroup _ (WildPat {})                 = PgAny
+patGroup _ (BangPat {})                 = PgBang
+patGroup _ (NPat (L _ olit) mb_neg _)   = PgN   (hsOverLitKey olit (isJust mb_neg))
+patGroup _ (NPlusKPat _ (L _ olit) _ _) = PgNpK (hsOverLitKey olit False)
+patGroup _ (CoPat _ p _)                = PgCo  (hsPatType p) -- Type of innelexp pattern
+patGroup _ (ViewPat expr p _)           = PgView expr (hsPatType (unLoc p))
+patGroup _ (ListPat _ _ (Just _))       = PgOverloadedList
+patGroup dflags (LitPat lit)            = PgLit (hsLitKey dflags lit)
+patGroup _ pat                          = pprPanic "patGroup" (ppr pat)
 
 {-
 Note [Grouping overloaded literal patterns]
Note: See TracTickets for help on using tickets.