More WIP; basically done now.wip/T11224

12 files changed, 243 insertions, 143 deletions

diff --git a/compiler/parser/Parser.y b/compiler/parser/Parser.y
index 06be056575..18386b4bb8 100644
--- a/compiler/parser/Parser.y
+++ b/compiler/parser/Parser.y
@@ -1190,29 +1190,10 @@ where_decls :: { Located ([AddAnn]
                                           ,sL1 $3 (snd $ unLoc $3)) }
 
 pattern_synonym_sig :: { LSig RdrName }
-        : 'pattern' con '::' ptype
+        : 'pattern' con '::' sigtype
                    {% ams (sLL $1 $> $ PatSynSig $2 (mkLHsSigType $4))
                           [mj AnnPattern $1, mu AnnDcolon $3] }
 
-ptype   :: { LHsType RdrName }
-        : 'forall' tv_bndrs '.' ptype
-                   {% hintExplicitForall (getLoc $1) >>
-                      ams (sLL $1 $> $
-                           HsForAllTy { hst_bndrs = $2
-                                      , hst_body = $4 })
-                          [mu AnnForall $1, mj AnnDot $3] }
-
-        | context '=>' context '=>' type
-                   {% ams (sLL $1 $> $
-                           HsQualTy { hst_ctxt = $1, hst_body = sLL $3 $> $
-                           HsQualTy { hst_ctxt = $3, hst_body = $5 } })
-                           [mu AnnDarrow $2, mu AnnDarrow $4] }
-        | context '=>' type
-                   {% ams (sLL $1 $> $
-                           HsQualTy { hst_ctxt = $1, hst_body = $3 })
-                           [mu AnnDarrow $2] }
-        | type     { $1 }
-
 -----------------------------------------------------------------------------
 -- Nested declarations
 
diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs
index ed12eff883..d82dc41215 100644
--- a/compiler/typecheck/Inst.hs
+++ b/compiler/typecheck/Inst.hs
@@ -155,7 +155,7 @@ deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
 
 deeplyInstantiate orig ty
   | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
-  = do { (subst, tvs') <- tcInstTyVars tvs
+  = do { (subst, tvs') <- newMetaTyVars tvs
        ; ids1  <- newSysLocalIds (fsLit "di") (substTys subst arg_tys)
        ; let theta' = substTheta subst theta
        ; wrap1 <- instCall orig (mkTyVarTys tvs') theta'
@@ -246,7 +246,7 @@ instDFunType dfun_id dfun_inst_tys
       = do { (subst', tys) <- go (extendTCvSubst subst tv ty) tvs mb_tys
            ; return (subst', ty : tys) }
     go subst (tv:tvs) (Nothing : mb_tys)
-      = do { (subst', tv') <- tcInstTyVarX subst tv
+      = do { (subst', tv') <- newMetaTyVarX subst tv
            ; (subst'', tys) <- go subst' tvs mb_tys
            ; return (subst'', mkTyVarTy tv' : tys) }
     go _ _ _ = pprPanic "instDFunTypes" (ppr dfun_id $$ ppr dfun_inst_tys)
diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index 8c4c4dba9a..1096649e49 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -19,7 +19,8 @@ module TcBinds ( tcLocalBinds, tcTopBinds, tcRecSelBinds,
 
 import {-# SOURCE #-} TcMatches ( tcGRHSsPat, tcMatchesFun )
 import {-# SOURCE #-} TcExpr  ( tcMonoExpr )
-import {-# SOURCE #-} TcPatSyn ( tcInferPatSynDecl, tcCheckPatSynDecl, tcPatSynBuilderBind )
+import {-# SOURCE #-} TcPatSyn ( tcInferPatSynDecl, tcCheckPatSynDecl
+                               , tcPatSynBuilderBind, tcPatSynSig )
 import DynFlags
 import HsSyn
 import HscTypes( isHsBootOrSig )
@@ -60,9 +61,7 @@ import FastString
 import Type(mkStrLitTy, tidyOpenType)
 import PrelNames( mkUnboundName, gHC_PRIM )
 import TcValidity (checkValidType)
-import Pair( Pair(..) )
 import Control.Monad
-import Data.List( partition )
 
 #include "HsVersions.h"
 
@@ -1683,76 +1682,8 @@ tcTySig (L loc (TypeSig names sig_ty))
        ; return (map TcIdSig sigs) }
 
 tcTySig (L loc (PatSynSig (L _ name) sig_ty))
-  | HsIB { hsib_vars = implicit_hs_tvs
-         , hsib_body = hs_ty }  <- sig_ty
-  , (univ_hs_tvs, hs_req,  hs_ty1) <- splitLHsSigmaTy hs_ty
-  , (ex_hs_tvs,   hs_prov, hs_ty2) <- splitLHsSigmaTy hs_ty1
-  , (hs_arg_tys, hs_body_ty)       <- splitHsFunType  hs_ty2
   = setSrcSpan loc $
-    do { (implicit_tvs, (univ_tvs, req, ex_tvs, prov, arg_tys, body_ty))
-           <- solveEqualities $
-              tcImplicitTKBndrs implicit_hs_tvs $
-              tcHsTyVarBndrs univ_hs_tvs  $ \ univ_tvs ->
-              tcHsTyVarBndrs ex_hs_tvs    $ \ ex_tvs   ->
-              do { req     <- tcHsContext hs_req
-                 ; prov    <- tcHsContext hs_prov
-                 ; arg_tys <- mapM tcHsOpenType (hs_arg_tys :: [LHsType Name])
-                 ; body_ty <- tcHsLiftedType hs_body_ty
-                 ; let bound_tvs
-                         = unionVarSets [ allBoundVariabless req
-                                        , allBoundVariabless prov
-                                        , allBoundVariabless (body_ty : arg_tys)
-                                        ]
-                 ; return ( (univ_tvs, req, ex_tvs, prov, arg_tys, body_ty)
-                          , bound_tvs) }
-
-       -- These are /signatures/ so we zonk to squeeze out any kind
-       -- unification variables.
-       -- ToDo: checkValidType?
-       ; implicit_tvs <- mapM zonkTcTyCoVarBndr implicit_tvs
-       ; univ_tvs     <- mapM zonkTcTyCoVarBndr univ_tvs
-       ; ex_tvs       <- mapM zonkTcTyCoVarBndr ex_tvs
-       ; req          <- zonkTcTypes req
-       ; prov         <- zonkTcTypes prov
-       ; arg_tys      <- zonkTcTypes arg_tys
-       ; body_ty      <- zonkTcType  body_ty
-
-       -- Kind generalisation; c.f. kindGeneralise
-       ; let free_kvs = tyCoVarsOfTelescope (implicit_tvs ++ univ_tvs ++ ex_tvs) $
-                        tyCoVarsOfTypes (body_ty : req ++ prov ++ arg_tys)
-
-       ; kvs <- quantifyTyVars emptyVarSet $
-                Pair free_kvs emptyVarSet
-
-       ; let bad_tvs = filter (`elemVarSet` tyCoVarsOfType body_ty) ex_tvs
-
-       ; unless (null bad_tvs) $ addErr $
-         hang (ptext (sLit "The result type") <+> quotes (ppr body_ty))
-            2 (ptext (sLit "mentions existential type variable") <> plural bad_tvs
-               <+> pprQuotedList bad_tvs)
-
-       ; let univ_fvs = closeOverKinds $
-                        (tyCoVarsOfTypes (body_ty : req) `extendVarSetList` univ_tvs)
-             (extra_univ, extra_ex) = partition (`elemVarSet` univ_fvs) $
-                                      kvs ++ implicit_tvs
-       ; traceTc "tcTySig }" $
-         vcat [ text "implicit_tvs" <+> ppr implicit_tvs
-              , text "kvs" <+> ppr kvs
-              , text "extra_univ" <+> ppr extra_univ
-              , text "univ_tvs" <+> ppr univ_tvs
-              , text "req" <+> ppr req
-              , text "extra_ex" <+> ppr extra_ex
-              , text "ex_tvs_" <+> ppr ex_tvs
-              , text "prov" <+> ppr prov
-              , text "arg_tys" <+> ppr arg_tys
-              , text "body_ty" <+> ppr body_ty ]
-       ; let tpsi = TPSI { patsig_name = name
-                         , patsig_univ_tvs = extra_univ ++ univ_tvs
-                         , patsig_req      = req
-                         , patsig_ex_tvs   = extra_ex   ++ ex_tvs
-                         , patsig_prov     = prov
-                         , patsig_arg_tys  = arg_tys
-                         , patsig_body_ty  = body_ty }
+    do { tpsi <- tcPatSynSig name sig_ty
        ; return [TcPatSynSig tpsi] }
 
 tcTySig _ = return []
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index a7c4795a48..8a3a4b86c5 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -840,15 +840,15 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
 
               mk_inst_ty :: TCvSubst -> (TyVar, TcType) -> TcM (TCvSubst, TcType)
               -- Deals with instantiation of kind variables
-              --   c.f. TcMType.tcInstTyVars
+              --   c.f. TcMType.newMetaTyVars
               mk_inst_ty subst (tv, result_inst_ty)
                 | is_fixed_tv tv   -- Same as result type
                 = return (extendTCvSubst subst tv result_inst_ty, result_inst_ty)
                 | otherwise        -- Fresh type, of correct kind
-                = do { (subst', new_tv) <- tcInstTyVarX subst tv
+                = do { (subst', new_tv) <- newMetaTyVarX subst tv
                      ; return (subst', mkTyVarTy new_tv) }
 
-        ; (result_subst, con1_tvs') <- tcInstTyVars con1_tvs
+        ; (result_subst, con1_tvs') <- newMetaTyVars con1_tvs
         ; let result_inst_tys = mkTyVarTys con1_tvs'
 
         ; (scrut_subst, scrut_inst_tys) <- mapAccumLM mk_inst_ty emptyTCvSubst
@@ -1325,7 +1325,7 @@ tc_infer_id orig lbl id_name
        --   * No need to deeply instantiate because type has all foralls at top
        = do { let wrap_id           = dataConWrapId con
                   (tvs, theta, rho) = tcSplitSigmaTy (idType wrap_id)
-            ; (subst, tvs') <- tcInstTyVars tvs
+            ; (subst, tvs') <- newMetaTyVars tvs
             ; let tys'   = mkTyVarTys tvs'
                   theta' = substTheta subst theta
                   rho'   = substTy subst rho
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 47a37d90ae..186453014a 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -827,7 +827,7 @@ tcInstBinderX mb_kind_info subst binder
   | Just tv <- binderVar_maybe binder
   = case lookup_tv tv of
       Just ki -> return (extendTCvSubst subst tv ki, ki)
-      Nothing -> do { (subst', tv') <- tcInstTyVarX subst tv
+      Nothing -> do { (subst', tv') <- newMetaTyVarX subst tv
                     ; return (subst', mkTyVarTy tv') }
 
      -- This is the *only* constraint currently handled in types.
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 10248c4354..f7b44dd311 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -27,7 +27,7 @@ module TcMType (
   cloneMetaTyVar,
   newFmvTyVar, newFskTyVar,
 
-  newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
+  readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
   newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar,
 
   --------------------------------
@@ -47,7 +47,7 @@ module TcMType (
 
   --------------------------------
   -- Instantiation
-  tcInstTyVars, tcInstTyVarX,
+  newMetaTyVars, newMetaTyVarX, newMetaSigTyVars,
   newSigTyVar,
   tcInstType,
   tcInstSkolTyVars, tcInstSkolTyVarsLoc, tcInstSuperSkolTyVarsX,
@@ -437,19 +437,6 @@ mkMetaTyVarName :: Unique -> FastString -> Name
 -- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
 mkMetaTyVarName uniq str = mkSysTvName uniq str
 
-newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
--- Make a new meta tyvar out of thin air
-newMetaTyVar meta_info kind
-  = do  { uniq <- newUnique
-        ; let name = mkMetaTyVarName uniq s
-              s = case meta_info of
-                        ReturnTv    -> fsLit "r"
-                        TauTv       -> fsLit "t"
-                        FlatMetaTv  -> fsLit "fmv"
-                        SigTv       -> fsLit "a"
-        ; details <- newMetaDetails meta_info
-        ; return (mkTcTyVar name kind details) }
-
 newSigTyVar :: Name -> Kind -> TcM TcTyVar
 newSigTyVar name kind
   = do { details <- newMetaDetails SigTv
@@ -615,8 +602,21 @@ coercion variables, except for the special case of the promoted Eq#. But,
 that can't ever appear in user code, so we're safe!
 -}
 
+newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
+-- Make a new meta tyvar out of thin air
+newAnonMetaTyVar meta_info kind
+  = do  { uniq <- newUnique
+        ; let name = mkMetaTyVarName uniq s
+              s = case meta_info of
+                        ReturnTv    -> fsLit "r"
+                        TauTv       -> fsLit "t"
+                        FlatMetaTv  -> fsLit "fmv"
+                        SigTv       -> fsLit "a"
+        ; details <- newMetaDetails meta_info
+        ; return (mkTcTyVar name kind details) }
+
 newFlexiTyVar :: Kind -> TcM TcTyVar
-newFlexiTyVar kind = newMetaTyVar TauTv kind
+newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
 
 newFlexiTyVarTy  :: Kind -> TcM TcType
 newFlexiTyVarTy kind = do
@@ -627,7 +627,7 @@ newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
 
 newReturnTyVar :: Kind -> TcM TcTyVar
-newReturnTyVar kind = newMetaTyVar ReturnTv kind
+newReturnTyVar kind = newAnonMetaTyVar ReturnTv kind
 
 newReturnTyVarTy :: Kind -> TcM TcType
 newReturnTyVarTy kind = mkTyVarTy <$> newReturnTyVar kind
@@ -652,20 +652,23 @@ newOpenReturnTyVar
        ; tv <- newReturnTyVar k
        ; return (tv, k) }
 
-tcInstTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
+newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
+newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst
+
+newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
 -- Instantiate with META type variables
 -- Note that this works for a sequence of kind, type, and coercion variables
 -- variables.  Eg    [ (k:*), (a:k->k) ]
 --             Gives [ (k7:*), (a8:k7->k7) ]
-tcInstTyVars = mapAccumLM tcInstTyVarX emptyTCvSubst
+newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
     -- emptyTCvSubst has an empty in-scope set, but that's fine here
     -- Since the tyvars are freshly made, they cannot possibly be
     -- captured by any existing for-alls.
 
-tcInstTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
+newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
 -- Make a new unification variable tyvar whose Name and Kind come from
 -- an existing TyVar. We substitute kind variables in the kind.
-tcInstTyVarX subst tyvar
+newMetaTyVarX subst tyvar
   = do  { uniq <- newUnique
                -- See Note [Levity polymorphic variables accept foralls]
         ; let info = if isLevityPolymorphic (tyVarKind tyvar)
@@ -678,6 +681,16 @@ tcInstTyVarX subst tyvar
               new_tv = mkTcTyVar name kind details
         ; return (extendTCvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
 
+newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
+-- Just like newMetaTyVarX, but make a SigTv
+newMetaSigTyVarX subst tyvar
+  = do  { uniq <- newUnique
+        ; details <- newMetaDetails SigTv
+        ; let name   = mkSystemName uniq (getOccName tyvar)
+              kind   = substTy subst (tyVarKind tyvar)
+              new_tv = mkTcTyVar name kind details
+        ; return (extendTCvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
+
 {- Note [Name of an instantiated type variable]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 At the moment we give a unification variable a System Name, which
diff --git a/compiler/typecheck/TcPat.hs b/compiler/typecheck/TcPat.hs
index 074532276e..469f2dffbb 100644
--- a/compiler/typecheck/TcPat.hs
+++ b/compiler/typecheck/TcPat.hs
@@ -705,7 +705,7 @@ tcPatSynPat :: PatEnv -> Located Name -> PatSyn
 tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
   = do  { let (univ_tvs, req_theta, ex_tvs, prov_theta, arg_tys, ty) = patSynSig pat_syn
 
-        ; (subst, univ_tvs') <- tcInstTyVars univ_tvs
+        ; (subst, univ_tvs') <- newMetaTyVars univ_tvs
 
         ; let all_arg_tys = ty : prov_theta ++ arg_tys
         ; checkExistentials ex_tvs all_arg_tys penv
@@ -775,7 +775,7 @@ matchExpectedPatTy inner_match pat_ty
          -- that is the other way round to matchExpectedPatTy
 
   | otherwise
-  = do { (subst, tvs') <- tcInstTyVars tvs
+  = do { (subst, tvs') <- newMetaTyVars tvs
        ; wrap1 <- instCall PatOrigin (mkTyVarTys tvs') (substTheta subst theta)
        ; (wrap2, arg_tys) <- matchExpectedPatTy inner_match (TcType.substTy subst tau)
        ; return (wrap2 <.> wrap1, arg_tys) }
@@ -799,7 +799,7 @@ matchExpectedConTy data_tc pat_ty
   | Just (fam_tc, fam_args, co_tc) <- tyConFamInstSig_maybe data_tc
          -- Comments refer to Note [Matching constructor patterns]
          -- co_tc :: forall a. T [a] ~ T7 a
-  = do { (subst, tvs') <- tcInstTyVars (tyConTyVars data_tc)
+  = do { (subst, tvs') <- newMetaTyVars (tyConTyVars data_tc)
              -- tys = [ty1,ty2]
 
        ; traceTc "matchExpectedConTy" (vcat [ppr data_tc,
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index e8bd5a88a2..5f9225030b 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -7,12 +7,14 @@
 
 {-# LANGUAGE CPP #-}
 
-module TcPatSyn ( tcInferPatSynDecl, tcCheckPatSynDecl
+module TcPatSyn ( tcPatSynSig, tcInferPatSynDecl, tcCheckPatSynDecl
                 , tcPatSynBuilderBind, tcPatSynBuilderOcc, nonBidirectionalErr
   ) where
 
 import HsSyn
 import TcPat
+import TcHsType( tcImplicitTKBndrs, tcHsTyVarBndrs
+               , tcHsContext, tcHsLiftedType, tcHsOpenType )
 import TcRnMonad
 import TcEnv
 import TcMType
@@ -47,10 +49,131 @@ import Data.Monoid( mconcat, mappend, mempty )
 import Bag
 import Util
 import Data.Maybe
-import Control.Monad ( zipWithM )
+import Control.Monad ( unless, zipWithM )
+import Data.List( partition )
+import Pair( Pair(..) )
 
 #include "HsVersions.h"
 
+{- *********************************************************************
+*                                                                      *
+        Type checking a pattern synonym signature
+*                                                                      *
+************************************************************************
+
+Note [Pattern synonym signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Pattern synonym signatures are surprisingly tricky (see Trac #11224 for example).
+In general they look like this:
+
+   pattern P :: forall univ_tvs. req
+             => forall ex_tvs. prov
+             => arg1 -> .. -> argn -> body_ty
+
+For parsing and renaming we treat the signature as an ordinary LHsSigType.
+
+Once we get to type checking, we decompose it into its parts, in tcPatSynSig.
+
+* Note that 'forall univ_tvs' and 'req =>'
+        and 'forall ex_tvs'   and 'prov =>'
+  are all optional.  We gather the pieces at the the top of tcPatSynSig
+
+* Initially the implicitly-bound tyvars (added by the renamer) include both
+  universal and existential vars.
+
+* After we kind-check the pieces and convert to Types, we do kind generalisation.
+
+* Note [Splitting the implicit tyvars in a pattern synonym]
+  Now the tricky bit: we must split
+     the implicitly-bound variables, and
+     the kind-generalised variables
+  into universal and existential.  We do so as follows:
+
+     Note [The pattern-synonym signature splitting rule]
+     the universals are the ones mentioned in
+          - univ_tvs (and the kinds thereof)
+          - prov
+          - body_ty
+     the existential are the rest
+
+* Moreover see Note
+-}
+
+tcPatSynSig :: Name -> LHsSigType Name -> TcM TcPatSynInfo
+tcPatSynSig name sig_ty
+  | HsIB { hsib_vars = implicit_hs_tvs
+         , hsib_body = hs_ty }  <- sig_ty
+  , (univ_hs_tvs, hs_req,  hs_ty1) <- splitLHsSigmaTy hs_ty
+  , (ex_hs_tvs,   hs_prov, hs_ty2) <- splitLHsSigmaTy hs_ty1
+  , (hs_arg_tys, hs_body_ty)       <- splitHsFunType  hs_ty2
+  = do { (implicit_tvs, (univ_tvs, req, ex_tvs, prov, arg_tys, body_ty))
+           <- solveEqualities $
+              tcImplicitTKBndrs implicit_hs_tvs $
+              tcHsTyVarBndrs univ_hs_tvs  $ \ univ_tvs ->
+              tcHsTyVarBndrs ex_hs_tvs    $ \ ex_tvs   ->
+              do { req     <- tcHsContext hs_req
+                 ; prov    <- tcHsContext hs_prov
+                 ; arg_tys <- mapM tcHsOpenType (hs_arg_tys :: [LHsType Name])
+                 ; body_ty <- tcHsLiftedType hs_body_ty
+                 ; let bound_tvs
+                         = unionVarSets [ allBoundVariabless req
+                                        , allBoundVariabless prov
+                                        , allBoundVariabless (body_ty : arg_tys)
+                                        ]
+                 ; return ( (univ_tvs, req, ex_tvs, prov, arg_tys, body_ty)
+                          , bound_tvs) }
+
+       -- These are /signatures/ so we zonk to squeeze out any kind
+       -- unification variables.
+       -- ToDo: checkValidType?
+       ; implicit_tvs <- mapM zonkTcTyCoVarBndr implicit_tvs
+       ; univ_tvs     <- mapM zonkTcTyCoVarBndr univ_tvs
+       ; ex_tvs       <- mapM zonkTcTyCoVarBndr ex_tvs
+       ; req          <- zonkTcTypes req
+       ; prov         <- zonkTcTypes prov
+       ; arg_tys      <- zonkTcTypes arg_tys
+       ; body_ty      <- zonkTcType  body_ty
+
+       -- Kind generalisation; c.f. kindGeneralise
+       ; let free_kvs = tyCoVarsOfTelescope (implicit_tvs ++ univ_tvs ++ ex_tvs) $
+                        tyCoVarsOfTypes (body_ty : req ++ prov ++ arg_tys)
+
+       ; kvs <- quantifyTyVars emptyVarSet (Pair free_kvs emptyVarSet)
+
+       -- Complain about:  pattern P :: () => forall x. x -> P x
+       -- The renamer thought it was fine, but the existential 'x'
+       -- should not appear in the result type
+       ; let bad_tvs = filter (`elemVarSet` tyCoVarsOfType body_ty) ex_tvs
+       ; unless (null bad_tvs) $ addErr $
+         hang (ptext (sLit "The result type") <+> quotes (ppr body_ty))
+            2 (ptext (sLit "mentions existential type variable") <> plural bad_tvs
+               <+> pprQuotedList bad_tvs)
+
+         -- Split [Splitting the implicit tyvars in a pattern synonym]
+       ; let univ_fvs = closeOverKinds $
+                        (tyCoVarsOfTypes (body_ty : req) `extendVarSetList` univ_tvs)
+             (extra_univ, extra_ex) = partition (`elemVarSet` univ_fvs) $
+                                      kvs ++ implicit_tvs
+       ; traceTc "tcTySig }" $
+         vcat [ text "implicit_tvs" <+> ppr implicit_tvs
+              , text "kvs" <+> ppr kvs
+              , text "extra_univ" <+> ppr extra_univ
+              , text "univ_tvs" <+> ppr univ_tvs
+              , text "req" <+> ppr req
+              , text "extra_ex" <+> ppr extra_ex
+              , text "ex_tvs_" <+> ppr ex_tvs
+              , text "prov" <+> ppr prov
+              , text "arg_tys" <+> ppr arg_tys
+              , text "body_ty" <+> ppr body_ty ]
+       ; return (TPSI { patsig_name = name
+                      , patsig_univ_tvs = extra_univ ++ univ_tvs
+                      , patsig_req      = req
+                      , patsig_ex_tvs   = extra_ex   ++ ex_tvs
+                      , patsig_prov     = prov
+                      , patsig_arg_tys  = arg_tys
+                      , patsig_body_ty  = body_ty }) }
+
+
 {-
 ************************************************************************
 *                                                                      *
@@ -117,15 +240,21 @@ tcCheckPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details
 
        ; tcCheckPatSynPat lpat
 
+       -- Right!  Let's check the pattern against the signature
+       -- See Note [Checking against a pattern signature]
        ; req_dicts <- newEvVars req_theta
-       ; (tclvl, wanted, (lpat', (ex_tys, prov_dicts, args'))) <-
+       ; (tclvl, wanted, (lpat', (ex_tvs', prov_dicts, args'))) <-
            ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys )
            pushLevelAndCaptureConstraints $
            tcPat PatSyn lpat pat_ty $
-           do { (subst, ex_tvs') <- tcInstTyVars ex_tvs
+           do { (subst, ex_tvs') <- if   isUnidirectional dir
+                                    then newMetaTyVars    ex_tvs
+                                    else newMetaSigTyVars ex_tvs
+                    -- See the "Existential type variables part of
+                    -- Note [Checking against a pattern signature]
               ; prov_dicts <- mapM (emitWanted origin) (substTheta subst prov_theta)
-              ; args' <- zipWithM (tc_arg subst) arg_names arg_tys
-              ; return (mkTyVarTys ex_tvs', prov_dicts, args') }
+              ; args'      <- zipWithM (tc_arg subst) arg_names arg_tys
+              ; return (ex_tvs', prov_dicts, args') }
 
        ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info univ_tvs req_dicts wanted
 
@@ -134,10 +263,14 @@ tcCheckPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details
        -- Since all the inputs are implications the returned bindings will be empty
        ; _ <- simplifyTop (emptyWC `addImplics` implics)
 
+       -- ToDo: in the bidirectional case, check that the ex_tvs' are all distinct
+       -- Otherwise we may get a type error when typechecking the builder,
+       -- when that should be impossible
+
        ; traceTc "tcCheckPatSynDecl }" $ ppr name
        ; tc_patsyn_finish lname dir is_infix lpat'
                           (univ_tvs, req_theta, ev_binds, req_dicts)
-                          (ex_tvs, ex_tys, prov_theta, prov_dicts)
+                          (ex_tvs, mkTyVarTys ex_tvs', prov_theta, prov_dicts)
                           (args', arg_tys)
                           pat_ty rec_fields }
   where
@@ -153,6 +286,10 @@ tcCheckPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details
 
 {- Note [Checking against a pattern signature]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When checking the actual supplied pattern against the pattern synonym
+signature, we need to be quite careful.
+
+----- Provided constraints
 Example
 
     data T a where
@@ -166,6 +303,34 @@ make available to matches against P, is derivable from the
 acutal pattern.  For example:
     f (P (x::a)) = ...here (Eq a) should be available...
 And yes, (Eq a) is derivable from the (Ord a) bound by P's rhs.
+
+----- Existential type variables
+Unusually, we instantiate the existential tyvars of the pattern with
+*meta* type variables.  For example
+
+    data S where
+      MkS :: Eq a => [a] -> S
+
+    pattern P :: () => Eq x => x -> S
+    pattern P x <- MkS x
+
+The pattern synonym conceals from its client the fact that MkS has a
+list inside it.  The client just thinks it's a type 'x'.  So we must
+unify x := [a] during type checking, and then use the instantiating type
+[a] (called ex_tys) when building the matcher.  In this case we'll get
+
+   $mP :: S -> (forall x. Ex x => x -> r) -> r -> r
+   $mP x k = case x of
+               MkS a (d:Eq a) (ys:[a]) -> let dl :: Eq [a]
+                                              dl = $dfunEqList d
+                                          in k [a] dl ys
+
+This "concealing" story works for /uni-directional/ pattern synonmys,
+but obviously not for bidirectional ones.  So in the bidirectional case
+we use SigTv, rather than a generic TauTv, meta-tyvar so that.  And
+we should really check that those SigTvs don't get unified with each
+other.
+
 -}
 
 collectPatSynArgInfo :: HsPatSynDetails (Located Name) -> ([Name], [Name], Bool)
diff --git a/compiler/typecheck/TcPatSyn.hs-boot b/compiler/typecheck/TcPatSyn.hs-boot
index 11c1bc19a2..af5aec7cbc 100644
--- a/compiler/typecheck/TcPatSyn.hs-boot
+++ b/compiler/typecheck/TcPatSyn.hs-boot
@@ -2,11 +2,14 @@ module TcPatSyn where
 
 import Name      ( Name )
 import Id        ( Id )
-import HsSyn     ( PatSynBind, LHsBinds )
+import HsSyn     ( PatSynBind, LHsBinds, LHsSigType )
 import TcRnTypes ( TcM, TcPatSynInfo )
 import TcRnMonad ( TcGblEnv)
 import Outputable ( Outputable )
 
+tcPatSynSig :: Name -> LHsSigType Name
+            -> TcM TcPatSynInfo
+
 tcInferPatSynDecl :: PatSynBind Name Name
                   -> TcM (LHsBinds Id, TcGblEnv)
 
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index c854eac851..e7833249e0 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -267,7 +267,7 @@ matchExpectedTyConApp tc orig_ty
     -- This happened in Trac #7368
     defer is_return
       = ASSERT2( classifiesTypeWithValues res_kind, ppr tc )
-        do { (k_subst, kvs') <- tcInstTyVars kvs
+        do { (k_subst, kvs') <- newMetaTyVars kvs
            ; let arg_kinds' = substTys k_subst arg_kinds
                  kappa_tys  = mkTyVarTys kvs'
            ; tau_tys <- mapM (newMaybeReturnTyVarTy is_return) arg_kinds'
@@ -482,7 +482,7 @@ tc_sub_type_ds origin ctxt ty_actual ty_expected
 
   | (tvs, theta, in_rho) <- tcSplitSigmaTy ty_actual
   , not (null tvs && null theta)
-  = do { (subst, tvs') <- tcInstTyVars tvs
+  = do { (subst, tvs') <- newMetaTyVars tvs
        ; let tys'    = mkTyVarTys tvs'
              theta'  = substTheta subst theta
              in_rho' = substTy subst in_rho
diff --git a/testsuite/tests/patsyn/should_compile/T11224b.hs b/testsuite/tests/patsyn/should_compile/T11224b.hs
index d8fcc3b884..89fb764005 100644
--- a/testsuite/tests/patsyn/should_compile/T11224b.hs
+++ b/testsuite/tests/patsyn/should_compile/T11224b.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE PatternSynonyms, GADTs #-}
+{-# LANGUAGE PatternSynonyms, GADTs, RankNTypes #-}
 
 module T11224b where
 
@@ -6,8 +6,9 @@ data T b where
   MkT :: a -> b -> T b
 
 -- Should be fine!
-pattern P :: c -> d -> T d
-pattern P x y = MkT x y
+-- pattern P :: c -> d -> T d
+pattern P :: forall d. forall c. c -> d -> T d
+pattern P x y <- MkT x y
 
 
 
diff --git a/testsuite/tests/patsyn/should_fail/T11010.stderr b/testsuite/tests/patsyn/should_fail/T11010.stderr
index 5f62b1357e..47492cde3a 100644
--- a/testsuite/tests/patsyn/should_fail/T11010.stderr
+++ b/testsuite/tests/patsyn/should_fail/T11010.stderr
@@ -1,8 +1,14 @@
 
-T11010.hs:8:1: error:
-    The 'required' context ‘a ~ Int’
-      mentions existential type variable ‘a’
-
-T11010.hs:16:1: error:
-    The 'required' context ‘a ~ Int’
-      mentions existential type variable ‘a’
+T11010.hs:9:36: error:
+    • Couldn't match type ‘a1’ with ‘Int’
+      ‘a1’ is a rigid type variable bound by
+        a pattern with constructor:
+          Fun :: forall b a. String -> (a -> b) -> Expr a -> Expr b,
+        in a pattern synonym declaration
+        at T11010.hs:9:26
+      Expected type: a -> b
+        Actual type: a1 -> b
+    • In the declaration for pattern synonym ‘IntFun’
+    • Relevant bindings include
+        x :: Expr a1 (bound at T11010.hs:9:36)
+        f :: a1 -> b (bound at T11010.hs:9:34)