Refactor typechecking of pattern bindings

This patch fixes a regression introduced, post 8.0.1, by
this major commit:

     commit 15b9bf4ba4ab47e6809bf2b3b36ec16e502aea72
     Author: Simon Peyton Jones <simonpj@microsoft.com>
     Date:   Sat Jun 11 23:49:27 2016 +0100

         Improve typechecking of let-bindings

         This major commit was initially triggered by #11339, but it
         spiraled into a major review of the way in which type
         signatures for bindings are handled, especially partial type
         signatures.

I didn't get the typechecking of pattern bindings right, leading
to Trac #12427.

In fixing this I found that this program doesn't work:

  data T where
    T :: a -> ((forall b. [b]->[b]) -> Int) -> T

  h1 y = case y of T _ v -> v

Works in 7.10, but not in 8.0.1.

There's a happy ending. I found a way to fix this, and improve
pattern bindings too.  Not only does this fix #12427, but it also
allows

In particular,we now can accept

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

  ... let { MkT _ q = t } in ...

Previously this elicited "my head exploded" but it's really
fine since q::Int.

The approach is described in detail in TcBinds
   Note [Typechecking pattern bindings]
Super cool.  And not even a big patch!

5 files changed, 299 insertions, 177 deletions

diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index 9191667ee9..f2717fcf94 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -1284,69 +1284,81 @@ data TcMonoBind         -- Half completed; LHS done, RHS not done
   | TcPatBind [MonoBindInfo] (LPat TcId) (GRHSs Name (LHsExpr Name)) TcSigmaType
 
 tcLhs :: TcSigFun -> LetBndrSpec -> HsBind Name -> TcM TcMonoBind
+-- Only called with plan InferGen (LetBndrSpec = LetLclBndr)
+--                    or NoGen    (LetBndrSpec = LetGblBndr)
+-- CheckGen is used only for functions with a complete type signature,
+--          and tcPolyCheck doesn't use tcMonoBinds at all
+
 tcLhs sig_fn no_gen (FunBind { fun_id = L nm_loc name, fun_matches = matches })
-  = do { mono_info <- tcLhsId sig_fn no_gen name
+  | Just (TcIdSig sig) <- sig_fn name
+  = -- There is a type signature.
+    -- It must be partial; if complete we'd be in tcPolyCheck!
+    --    e.g.   f :: _ -> _
+    --           f x = ...g...
+    --           Just g = ...f...
+    -- Hence always typechecked with InferGen
+    do { mono_info <- tcLhsSigId no_gen (name, sig)
+       ; return (TcFunBind mono_info nm_loc matches) }
+
+  | otherwise  -- No type signature
+  = do { mono_ty <- newOpenFlexiTyVarTy
+       ; mono_id <- newLetBndr no_gen name mono_ty
+       ; let mono_info = MBI { mbi_poly_name = name
+                             , mbi_sig       = Nothing
+                             , mbi_mono_id   = mono_id }
        ; return (TcFunBind mono_info nm_loc matches) }
 
 tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss })
-  = do  { let bndr_names = collectPatBinders pat
-        ; mbis <- mapM (tcLhsId sig_fn no_gen) bndr_names
-            -- See Note [Existentials in pattern bindings]
+  = -- See Note [Typechecking pattern bindings]
+    do  { sig_mbis <- mapM (tcLhsSigId no_gen) sig_names
 
         ; let inst_sig_fun = lookupNameEnv $ mkNameEnv $
-                             bndr_names `zip` map mbi_mono_id mbis
+                             [ (mbi_poly_name mbi, mbi_mono_id mbi)
+                             | mbi <- sig_mbis ]
+
+            -- See Note [Existentials in pattern bindings]
+        ; ((pat', nosig_mbis), pat_ty)
+            <- addErrCtxt (patMonoBindsCtxt pat grhss) $
+               tcInferInst $ \ exp_ty ->
+               tcLetPat inst_sig_fun no_gen pat exp_ty $
+               mapM lookup_info nosig_names
+
+        ; let mbis = sig_mbis ++ nosig_mbis
 
         ; traceTc "tcLhs" (vcat [ ppr id <+> dcolon <+> ppr (idType id)
                                 | mbi <- mbis, let id = mbi_mono_id mbi ]
                            $$ ppr no_gen)
 
-        ; ((pat', _), pat_ty) <- addErrCtxt (patMonoBindsCtxt pat grhss) $
-                                 tcInferNoInst $ \ exp_ty ->
-                                 tcLetPat inst_sig_fun pat exp_ty $
-                                 return () -- mapM (lookup_info inst_sig_fun) bndr_names
-
         ; return (TcPatBind mbis pat' grhss pat_ty) }
+  where
+    bndr_names = collectPatBinders pat
+    (nosig_names, sig_names) = partitionWith find_sig bndr_names
+
+    find_sig :: Name -> Either Name (Name, TcIdSigInfo)
+    find_sig name = case sig_fn name of
+                      Just (TcIdSig sig) -> Right (name, sig)
+                      _                  -> Left name
+
+      -- After typechecking the pattern, look up the binder
+      -- names that lack a signature, which the pattern has brought
+      -- into scope.
+    lookup_info :: Name -> TcM MonoBindInfo
+    lookup_info name
+      = do { mono_id <- tcLookupId name
+           ; return (MBI { mbi_poly_name = name
+                         , mbi_sig       = Nothing
+                         , mbi_mono_id   = mono_id }) }
 
 tcLhs _ _ other_bind = pprPanic "tcLhs" (ppr other_bind)
         -- AbsBind, VarBind impossible
 
 -------------------
-data LetBndrSpec
-  = LetLclBndr            -- We are going to generalise, and wrap in an AbsBinds
-                          -- so clone a fresh binder for the local monomorphic Id
-
-  | LetGblBndr TcPragEnv  -- Generalisation plan is NoGen, so there isn't going
-                          -- to be an AbsBinds; So we must bind the global version
-                          -- of the binder right away.
-                          -- And here is the inline-pragma information
-
-instance Outputable LetBndrSpec where
-  ppr LetLclBndr      = text "LetLclBndr"
-  ppr (LetGblBndr {}) = text "LetGblBndr"
-
-tcLhsId :: TcSigFun -> LetBndrSpec -> Name -> TcM MonoBindInfo
-tcLhsId sig_fn no_gen name
-  | Just (TcIdSig sig) <- sig_fn name
-  = -- A partial type signature on a FunBind, in a mixed group
-    --    e.g.   f :: _ -> _
-    --           f x = ...g...
-    --           Just g = ...f...
-    -- Hence always typechecked with InferGen; hence LetLclBndr
-    --
-    -- A compelete type sig on a FunBind is checked with CheckGen
-    -- and does not go via tcLhsId
-    do { inst_sig <- tcInstSig sig
-       ; the_id <- newSigLetBndr no_gen name inst_sig
+tcLhsSigId :: LetBndrSpec -> (Name, TcIdSigInfo) -> TcM MonoBindInfo
+tcLhsSigId no_gen (name, sig)
+  = do { inst_sig <- tcInstSig sig
+       ; mono_id <- newSigLetBndr no_gen name inst_sig
        ; return (MBI { mbi_poly_name = name
                      , mbi_sig       = Just inst_sig
-                     , mbi_mono_id   = the_id }) }
-
-  | otherwise
-  = -- No type signature, plan InferGen (LetLclBndr) or NoGen (LetGblBndr)
-    do { mono_ty <- newOpenFlexiTyVarTy
-       ; mono_id <- newLetBndr no_gen name mono_ty
-       ; return (MBI { mbi_poly_name = name
-                     , mbi_sig       = Nothing
                      , mbi_mono_id   = mono_id }) }
 
 ------------
@@ -1357,20 +1369,6 @@ newSigLetBndr (LetGblBndr prags) name (TISI { sig_inst_sig = id_sig })
 newSigLetBndr no_gen name (TISI { sig_inst_tau = tau })
   = newLetBndr no_gen name tau
 
-newLetBndr :: LetBndrSpec -> Name -> TcType -> TcM TcId
--- In the polymorphic case when we are going to generalise
---    (plan InferGen, no_gen = LetLclBndr), generate a "monomorphic version"
---    of the Id; the original name will be bound to the polymorphic version
---    by the AbsBinds
--- In the monomorphic case when we are not going to generalise
---    (plan NoGen, no_gen = LetGblBndr) there is no AbsBinds,
---    and we use the original name directly
-newLetBndr LetLclBndr name ty
-  = do { mono_name <- cloneLocalName name
-       ; return (mkLocalId mono_name ty) }
-newLetBndr (LetGblBndr prags) name ty
-  = addInlinePrags (mkLocalId name ty) (lookupPragEnv prags name)
-
 -------------------
 tcRhs :: TcMonoBind -> TcM (HsBind TcId)
 tcRhs (TcFunBind info@(MBI { mbi_sig = mb_sig, mbi_mono_id = mono_id })
@@ -1439,9 +1437,13 @@ getMonoBindInfo tc_binds
     get_info (TcFunBind info _ _)    rest = info : rest
     get_info (TcPatBind infos _ _ _) rest = infos ++ rest
 
-{- Note [Existentials in pattern bindings]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider (typecheck/should_compile/ExPat):
+
+{- Note [Typechecking pattern bindings]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Look at:
+   - typecheck/should_compile/ExPat
+   - Trac #12427, typecheck/should_compile/T12427{a,b}
+
   data T where
     MkT :: Integral a => a -> Int -> T
 
@@ -1453,48 +1455,96 @@ and suppose t :: T.  Which of these pattern bindings are ok?
 
   E3. let { MkT (toInteger -> r) _ = t } in <body>
 
-Well (E1) is clearly wrong because the existential 'a' escapes.
-What type could 'p' possibly have?
+* (E1) is clearly wrong because the existential 'a' escapes.
+  What type could 'p' possibly have?
 
-But (E2) is fine, despite the existential pattern, because
-q::Int, and nothing escapes.
+* (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.
+* 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
+For (E2) 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 variable 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.
+We typecheck pattern bindings as follows.  First tcLhs does this:
+
+  1. Take each type signature q :: ty, partial or complete, and
+     instantiate it (with tcLhsSigId) to get a MonoBindInfo.  This
+     gives us a fresh "mono_id" qm :: instantiate(ty), where qm has
+     a fresh name.
+
+     Any fresh unification variables in instiatiate(ty) 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.
+  2. Build a little environment mapping "q" -> "qm" for those Ids
+     with signatures (inst_sig_fun)
 
-  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.
+  3. Invoke tcLetPat to typecheck the pattern.
 
-     - 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.
+     - We pass in the current TcLevel.  This is captured by
+       TcPat.tcLetPat, and put into the pc_lvl field of PatCtxt, in
+       PatEnv.
 
+     - When tcPat finds an existential constructor, it binds fresh
+       type variables and dictionaries as usual, increments the TcLevel,
+       and emits an implication constraint.
+
+     - When we come to a binder (TcPat.tcPatBndr), it looks it up
+       in the little environment (the pc_sig_fn field of PatCtxt).
+
+         Success => There was a type signature, so just use it,
+                    checking compatibility with the expected type.
+
+         Failure => No type sigature.
+             Infer case: (happens only outside any constructor pattern)
+                         use a unification variable
+                         at the outer level pc_lvl
+
+             Check case: use promoteTcType to promote the type
+                         to the outer level pc_lvl.  This is the
+                         place where we emit a constraint that'll blow
+                         up if existential capture takes place
+
+       Result: the type of the binder is always at pc_lvl. This is
+       crucial.
+
+  4. Throughout, when we are making up an Id for the pattern-bound variables
+     (newLetBndr), we have two cases:
+
+     - If we are generalising (generalisation plan is InferGen or
+       CheckGen), then the let_bndr_spec will be LetLclBndr.  In that case
+       we want to bind a cloned, local version of the variable, with the
+       type given by the pattern context, *not* by the signature (even if
+       there is one; see Trac #7268). The mkExport part of the
+       generalisation step will do the checking and impedance matching
+       against the signature.
+
+     - If for some some reason we are not generalising (plan = NoGen), the
+       LetBndrSpec will be LetGblBndr.  In that case we must bind the
+       global version of the Id, and do so with precisely the type given
+       in the signature.  (Then we unify with the type from the pattern
+       context type.)
+
+ 
 And that's it!  The implication constraints check for the skolem
-escape.  It's quite simple and neat, and more exressive than before
+escape.  It's quite simple and neat, and more expressive than before
 e.g. GHC 8.0 rejects (E2) and (E3).
 
+Example for (E1), starting at level 1.  We generate
+     p :: beta:1, with constraints (forall:3 a. Integral a => a ~ beta)
+The (a~beta) can't float (because of the 'a'), nor be solved (because
+beta is untouchable.)
+
+Example for (E2), we generate
+     q :: beta:1, with constraint (forall:3 a. Integral a => Int ~ beta)
+The beta is untoucable, but floats out of the constraint and can
+be solved absolutely fine.
 
 ************************************************************************
 *                                                                      *
diff --git a/compiler/typecheck/TcPat.hs b/compiler/typecheck/TcPat.hs
index 7900d6c592..5a1cbfadc6 100644
--- a/compiler/typecheck/TcPat.hs
+++ b/compiler/typecheck/TcPat.hs
@@ -9,7 +9,7 @@ TcPat: Typechecking patterns
 {-# LANGUAGE CPP, RankNTypes, TupleSections #-}
 {-# LANGUAGE FlexibleContexts #-}
 
-module TcPat ( tcLetPat
+module TcPat ( tcLetPat, newLetBndr, LetBndrSpec(..)
              , tcPat, tcPat_O, tcPats
              , addDataConStupidTheta, badFieldCon, polyPatSig ) where
 
@@ -19,6 +19,7 @@ import {-# SOURCE #-}   TcExpr( tcSyntaxOp, tcSyntaxOpGen, tcInferSigma )
 
 import HsSyn
 import TcHsSyn
+import TcSigs( TcPragEnv, lookupPragEnv, addInlinePrags )
 import TcRnMonad
 import Inst
 import Id
@@ -58,15 +59,20 @@ import ListSetOps ( getNth )
 -}
 
 tcLetPat :: (Name -> Maybe TcId)
+         -> LetBndrSpec
          -> LPat Name -> ExpSigmaType
          -> TcM a
          -> TcM (LPat TcId, a)
-tcLetPat sig_fn pat pat_ty thing_inside
-  = tc_lpat pat pat_ty penv thing_inside
-  where
-    penv = PE { pe_lazy = True
-              , pe_ctxt = LetPat sig_fn
-              , pe_orig = PatOrigin }
+tcLetPat sig_fn no_gen pat pat_ty thing_inside
+  = do { bind_lvl <- getTcLevel
+       ; let ctxt = LetPat { pc_lvl    = bind_lvl
+                           , pc_sig_fn = sig_fn
+                           , pc_new    = no_gen }
+             penv = PE { pe_lazy = True
+                       , pe_ctxt = ctxt
+                       , pe_orig = PatOrigin }
+
+       ; tc_lpat pat pat_ty penv thing_inside }
 
 -----------------
 tcPats :: HsMatchContext Name
@@ -109,7 +115,14 @@ tcPat_O ctxt orig pat pat_ty thing_inside
     penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = orig }
 
 
------------------
+{-
+************************************************************************
+*                                                                      *
+                PatEnv, PatCtxt, LetBndrSpec
+*                                                                      *
+************************************************************************
+-}
+
 data PatEnv
   = PE { pe_lazy :: Bool        -- True <=> lazy context, so no existentials allowed
        , pe_ctxt :: PatCtxt     -- Context in which the whole pattern appears
@@ -122,7 +135,29 @@ data PatCtxt
 
   | LetPat   -- Used only for let(rec) pattern bindings
              -- See Note [Typing patterns in pattern bindings]
-       (Name -> Maybe TcId)    -- Tells the expected type for this binder
+       { pc_lvl    :: TcLevel
+                   -- Level of the binding group
+
+       , pc_sig_fn :: Name -> Maybe TcId
+                   -- Tells the expected type
+                   -- for binders with a signature
+
+       , pc_new :: LetBndrSpec
+                -- How to make a new binder
+       }        -- for binders without signatures
+
+data LetBndrSpec
+  = LetLclBndr            -- We are going to generalise, and wrap in an AbsBinds
+                          -- so clone a fresh binder for the local monomorphic Id
+
+  | LetGblBndr TcPragEnv  -- Generalisation plan is NoGen, so there isn't going
+                          -- to be an AbsBinds; So we must bind the global version
+                          -- of the binder right away.
+                          -- And here is the inline-pragma information
+
+instance Outputable LetBndrSpec where
+  ppr LetLclBndr      = text "LetLclBndr"
+  ppr (LetGblBndr {}) = text "LetGblBndr"
 
 makeLazy :: PatEnv -> PatEnv
 makeLazy penv = penv { pe_lazy = True }
@@ -141,101 +176,75 @@ tcPatBndr :: PatEnv -> Name -> ExpSigmaType -> TcM (HsWrapper, TcId)
 -- (coi, xp) = tcPatBndr penv x pat_ty
 -- Then coi : pat_ty ~ typeof(xp)
 --
-tcPatBndr penv@(PE { pe_ctxt = LetPat lookup_sig
-                   , pe_orig = orig })
-          bndr_name pat_ty
-          -- See Note [Typing patterns in pattern bindings]
-  | Just bndr_id <- lookup_sig bndr_name
-  = do { wrap <- tcSubTypePat penv orig pat_ty (idType bndr_id)
-       ; traceTc "tcPatBndr(lsl,sig)" (ppr bndr_id $$ ppr (idType bndr_id) $$ ppr pat_ty)
+tcPatBndr penv@(PE { pe_ctxt = LetPat { pc_lvl    = bind_lvl
+                                      , pc_sig_fn = sig_fn
+                                      , pc_new    = no_gen } })
+          bndr_name exp_pat_ty
+  -- For the LetPat cases, see
+  -- Note [Typechecking pattern bindings] in TcBinds
+
+  | Just bndr_id <- sig_fn bndr_name   -- There is a signature
+  = do { wrap <- tcSubTypePat penv exp_pat_ty (idType bndr_id)
+           -- See Note [Subsumption check at pattern variables]
+       ; traceTc "tcPatBndr(sig)" (ppr bndr_id $$ ppr (idType bndr_id) $$ ppr exp_pat_ty)
        ; return (wrap, bndr_id) }
 
-  | otherwise  -- No signature
-  = pprPanic "tcPatBndr" (ppr bndr_name)
-
-tcPatBndr (PE { pe_ctxt = _lam_or_proc }) bndr_name pat_ty
+  | otherwise                          -- No signature
+  = do { (co, bndr_ty) <- case exp_pat_ty of
+             Check pat_ty    -> promoteTcType bind_lvl pat_ty
+             Infer infer_res -> ASSERT( bind_lvl == ir_lvl infer_res )
+                                -- If we were under a constructor that bumped
+                                -- the level, we'd be in checking mode
+                                do { bndr_ty <- inferResultToType infer_res
+                                   ; return (mkTcNomReflCo bndr_ty, bndr_ty) }
+       ; bndr_id <- newLetBndr no_gen bndr_name bndr_ty
+       ; traceTc "tcPatBndr(nosig)" (vcat [ ppr bind_lvl
+                                          , ppr exp_pat_ty, ppr bndr_ty, ppr co
+                                          , ppr bndr_id ])
+       ; return (mkWpCastN co, bndr_id) }
+
+tcPatBndr _ bndr_name pat_ty
   = do { pat_ty <- expTypeToType pat_ty
        ; traceTc "tcPatBndr(not let)" (ppr bndr_name $$ ppr pat_ty)
        ; return (idHsWrapper, mkLocalId bndr_name pat_ty) }
                -- Whether or not there is a sig is irrelevant,
                -- as this is local
 
+newLetBndr :: LetBndrSpec -> Name -> TcType -> TcM TcId
+-- Make up a suitable Id for the pattern-binder.
+-- See Note [Typechecking pattern bindings], item (4) in TcBinds
+--
+-- In the polymorphic case when we are going to generalise
+--    (plan InferGen, no_gen = LetLclBndr), generate a "monomorphic version"
+--    of the Id; the original name will be bound to the polymorphic version
+--    by the AbsBinds
+-- In the monomorphic case when we are not going to generalise
+--    (plan NoGen, no_gen = LetGblBndr) there is no AbsBinds,
+--    and we use the original name directly
+newLetBndr LetLclBndr name ty
+  = do { mono_name <- cloneLocalName name
+       ; return (mkLocalId mono_name ty) }
+newLetBndr (LetGblBndr prags) name ty
+  = addInlinePrags (mkLocalId name ty) (lookupPragEnv prags name)
+
 tcSubTypePat :: PatEnv -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
 -- tcSubTypeET with the UserTypeCtxt specialised to GenSigCtxt
 -- Used when typechecking patterns
 tcSubTypePat penv t1 t2 = tcSubTypeET (pe_orig penv) GenSigCtxt t1 t2
 
-{- Note [Partial signatures for pattern bindings]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider a function binding and a pattern binding, both
-with a partial type signature
-
-   f1 :: (True, _) -> Char
-   f1 = \x -> x
-
-   f2 :: (True, _) -> Char
-   Just f2 = Just (\x->x)
+{- Note [Subsumption check at pattern variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we come across a variable with a type signature, we need to do a
+subsumption, not equality, check against the context type.  e.g.
 
-Obviously, both should be rejected.  That happens naturally for the
-function binding, f1, because we typecheck the RHS with "expected"
-type '(True, apha) -> Char', which correctly fails.
-
-But what of the pattern binding for f2?  We infer the type of the
-pattern, and check tha the RHS has that type.  So we must feed in the
-type of f2 when inferring the type of the pattern!  We do this right
-here, in tcPatBndr, for a LetLclBndr. The signature already has fresh
-unification variables for the wildcards (if any).
-
-Extra notes
-
-* For /complete/ type signatures, we could im principle ignore all this
-  and just infer the most general type for f2, and check (in
-  TcBinds.mkExport) whether it has the claimed type.
-
-  But not so for /partial/ signatures; to get the wildcard unification
-  variables into the game we really must inject them here. If we don't
-  we never get /any/ value assigned to the wildcards; and programs that
-  are bogus, like f2, are accepted.
-
-  Moreover, by feeding in the expected type we do less fruitless
-  creation of unification variables, and improve error messages.
-
-* We need to do a subsumption, not equality, check.  If
-      data T = MkT (forall a. a->a)
+    data T = MkT (forall a. a->a)
       f :: forall b. [b]->[b]
       MkT f = blah
-  Since 'blah' returns a value of type T, its payload is a polymorphic
-  function of type (forall a. a->a).  And that's enough to bind the
-  less-polymorphic function 'f', but we need some impedence matching
-  to witness the instantiation.
-
-Note [Typing patterns in pattern bindings]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we are typing a pattern binding
-    pat = rhs
-Then the PatCtxt will be (LetPat sig_fn).
-
-There can still be signatures for the binders:
-     data T = MkT (forall a. a->a) Int
-     x :: forall a. a->a
-     y :: Int
-     MkT x y = <rhs>
-
-Two cases, dealt with by the LetPat case of tcPatBndr
-
- * If we are generalising (generalisation plan is InferGen or
-   CheckGen), then the let_bndr_spec will be LetLclBndr.  In that case
-   we want to bind a cloned, local version of the variable, with the
-   type given by the pattern context, *not* by the signature (even if
-   there is one; see Trac #7268). The mkExport part of the
-   generalisation step will do the checking and impedance matching
-   against the signature.
-
- * If for some some reason we are not generalising (plan = NoGen), the
-   LetBndrSpec will be LetGblBndr.  In that case we must bind the
-   global version of the Id, and do so with precisely the type given
-   in the signature.  (Then we unify with the type from the pattern
-   context type.)
+
+Since 'blah' returns a value of type T, its payload is a polymorphic
+function of type (forall a. a->a).  And that's enough to bind the
+less-polymorphic function 'f', but we need some impedence matching
+to witness the instantiation.
 
 
 ************************************************************************
@@ -1124,7 +1133,7 @@ Lazy patterns can't bind existentials.  They arise in two ways:
 The pe_lazy field of PatEnv says whether we are inside a lazy
 pattern (perhaps deeply)
 
-See also Note [Existentials in pattern bindings] in TcBinds
+See also Note [Typechecking pattern bindings] in TcBinds
 -}
 
 maybeWrapPatCtxt :: Pat Name -> (TcM a -> TcM b) -> TcM a -> TcM b
diff --git a/testsuite/tests/typecheck/should_compile/T12427a.hs b/testsuite/tests/typecheck/should_compile/T12427a.hs
new file mode 100644
index 0000000000..1cbf7c5c27
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T12427a.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE GADTs, RankNTypes #-}
+
+-- Test pattern bindings, existentials, and higher rank
+
+module T12427a where
+
+data T where
+  T1 :: a -> ((forall b. [b]->[b]) -> Int) -> T
+  T2 :: ((forall b. [b]->[b]) -> Int) -> T
+
+-- Inference
+-- Worked in 7.10 (probably wrongly)
+-- Failed in 8.0.1
+-- Fails in 8.2 because v is polymorphic
+--     and the T1 pattern match binds existentials,
+--     and hence bumps levels
+h11 y = case y of T1 _ v -> v
+
+-- Worked in 7.10 (probably wrongly)
+-- Failed in 8.0.1
+-- Succeeds in 8.2 because the pattern match has
+--   no existentials, so it doesn't matter than
+--   v is polymoprhic
+h12 y = case y of T2 v -> v
+
+-- Inference
+-- Same results as for h11 and h12 resp
+T1 _ x1 = undefined
+T2 x2 = undefined
+
+-- Works in all versions
+h2 :: T -> (forall b. [b] -> [b]) -> Int
+h2 y = case y of T1 _ v -> v
+
+-- Checking
+-- Fails in 7.10  (head exploded)
+-- Fails in 8.0.1 (ditto)
+-- Succeeds in 8.2
+x3 :: (forall a. a->a) -> Int
+T1 _ x3 = undefined
diff --git a/testsuite/tests/typecheck/should_compile/T12427b.hs b/testsuite/tests/typecheck/should_compile/T12427b.hs
new file mode 100644
index 0000000000..11413dc5e5
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T12427b.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE GADTs, RankNTypes #-}
+
+module T12427b where
+
+newtype Acquire a = Acquire {unAcquire :: (forall b. b -> b) -> IO a}
+
+instance Functor Acquire where
+    fmap = undefined
+
+instance Applicative Acquire where
+    pure = undefined
+    (<*>) = undefined
+
+instance Monad Acquire where
+    Acquire f >>= g' = Acquire $ \restore -> do
+        x <- f restore
+        let Acquire g = g' x
+        -- let g = unAcquire (g' x)
+        g restore
+
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index f107ba16d6..9f32b44d31 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -533,3 +533,6 @@ test('T12185', normal, compile, [''])
 test('T12133', normal, compile, [''])
 test('T12381', normal, compile, [''])
 test('T12082', normal, compile, [''])
+test('T12427a', normal, compile_fail, [''])
+test('T12427b', normal, compile, [''])
+