[GHC] #11700: pattern match bug

Mon Jun 13 22:18:11 UTC 2016

#11700: pattern match bug
-------------------------------------+-------------------------------------
        Reporter:  TobyGoodwin       |                Owner:
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.10.3
  checker)                           |
      Resolution:  fixed             |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
                                     |  typecheck/should_compile/T11700,
                                     |  ExPat, ExPatFail
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * testcase:   => typecheck/should_compile/T11700, ExPat, ExPatFail
 * status:  new => closed
 * resolution:   => fixed

Comment:

 Well that has been lurking a long time.

 It was caused by the fact that when the pattern binds dictionaries (which
 this one does), we make an implication constraint, and bump the `TcLevel`.
 Normally that doesn't happen because GHC complains about a pattern binding
 that binds existential variables.  But this one doesn't!  It only binds
 constraints!

 Anyway it demonstrated to me that the way we were dealing with
 existentials in pattern bindings was all wrong... better to ''use'' the
 machinery of implication constraints, rather than cut across it.  Here's
 the new method (a Note in `TcBinds`).  Much nicer!  And it actually allows
 more programs too.
 {{{
 {- Note [Existentials in pattern bindings]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider (typecheck/should_compile/ExPat):
   data T where
     MkT :: Integral a => a -> Int -> T

 and suppose t :: T.  Which of these pattern bindings are ok?

   E1. let { MkT p _ = t } in <body>

   E2. let { MkT _ q = t } in <body>

   E3. let { MkT (toInteger -> r) _ = t } in <body>

 Well (E1) is clearly wrong becuase the existential 'a' escapes.
 What type could 'p' possibly have?

 But (E2) is fine, despite the existential pattern, because
 q::Int, and nothing escapes.

 Even (E3) is fine.  The existential pattern binds a dictionary
 for (Integral a) which the view pattern can use to convert the
 a-valued field to an Integer, so r :: Integer.

 An easy way to see all three is to imagine the desugaring.
 For (2) it would look like
     let q = case t of MkT _ q' -> q'
     in <body>

 We typecheck pattern bindings as follows:
   1. In tcLhs we bind q'::alpha, for each varibable q bound by the
      pattern, where q' is a fresh name, and alpha is a fresh
      unification variable; it will be the monomorphic verion of q that
      we later generalise

      It's very important that these fresh unification variables
      alpha are born here, not deep under implications as would happen
      if we allocated them when we encountered q during tcPat.

   2. Still in tcLhs, we build a little environment mappting "q" ->
      q':alpha, and pass that to tcLetPet.

   3. Then tcLhs invokes tcLetPat to typecheck the patter as usual:
      - When tcLetPat finds an existential constructor, it binds fresh
        type variables and dictionaries as usual, and emits an
        implication constraint.

      - When tcLetPat finds a variable (TcPat.tcPatBndr) it looks it up
        in the little environment, which should always succeed.  And
        uses tcSubTypeET to connect the type of that variable with the
        expected type of the pattern.

 And that's it!  The implication constraints check for the skolem
 escape.  It's quite simple and neat, and more exressive than before
 e.g. GHC 8.0 rejects (E2) and (E3).
 }}}

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