Fix typechecking for pattern synonym signatures
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 22 Dec 2015 13:33:35 +0000 (14:33 +0100)
committerBen Gamari <ben@smart-cactus.org>
Tue, 22 Dec 2015 13:34:36 +0000 (14:34 +0100)
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

23 files changed:
compiler/basicTypes/PatSyn.hs
compiler/ghci/RtClosureInspect.hs
compiler/hsSyn/HsBinds.hs
compiler/parser/Parser.y
compiler/typecheck/Inst.hs
compiler/typecheck/TcBinds.hs
compiler/typecheck/TcExpr.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcPat.hs
compiler/typecheck/TcPatSyn.hs
compiler/typecheck/TcPatSyn.hs-boot
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcUnify.hs
compiler/types/TyCoRep.hs
testsuite/tests/patsyn/should_compile/MoreEx.hs [new file with mode: 0644]
testsuite/tests/patsyn/should_compile/T11224b.hs [new file with mode: 0644]
testsuite/tests/patsyn/should_compile/all.T
testsuite/tests/patsyn/should_fail/T11010.stderr
testsuite/tests/patsyn/should_fail/T9793-fail.stderr
testsuite/tests/patsyn/should_fail/as-pattern.stderr
testsuite/tests/patsyn/should_run/T11224.hs
testsuite/tests/patsyn/should_run/all.T

index b7aff18..c35bcf3 100644 (file)
@@ -159,8 +159,8 @@ so pattern P has type
 
 with the following typeclass constraints:
 
-        provides: (Show (Maybe t), Ord b)
         requires: (Eq t, Num t)
+        provides: (Show (Maybe t), Ord b)
 
 In this case, the fields of MkPatSyn will be set as follows:
 
index f71c904..502610f 100644 (file)
@@ -606,7 +606,7 @@ instTyVars :: [TyVar] -> TR (TCvSubst, [TcTyVar])
 -- Instantiate fresh mutable type variables from some TyVars
 -- This function preserves the print-name, which helps error messages
 instTyVars tvs
-  = liftTcM $ fst <$> captureConstraints (tcInstTyVars tvs)
+  = liftTcM $ fst <$> captureConstraints (newMetaTyVars tvs)
 
 type RttiInstantiation = [(TcTyVar, TyVar)]
    -- Associates the typechecker-world meta type variables
index 71d8dd2..6acac76 100644 (file)
@@ -892,13 +892,8 @@ ppr_sig (SpecInstSig _ ty)
   = pragBrackets (ptext (sLit "SPECIALIZE instance") <+> ppr ty)
 ppr_sig (MinimalSig _ bf)         = pragBrackets (pprMinimalSig bf)
 ppr_sig (PatSynSig name sig_ty)
-  = pprPatSynSig (unLoc name) False -- TODO: is_bindir
-                 (pprHsForAllTvs qtvs)
-                 (pprHsContextMaybe (unLoc req))
-                 (pprHsContextMaybe (unLoc prov))
-                 (ppr ty)
-  where
-    (qtvs, req, prov, ty) = splitLHsPatSynTy (hsSigType sig_ty)
+  = ptext (sLit "pattern") <+> pprPrefixOcc (unLoc name) <+> dcolon
+                           <+> ppr sig_ty
 
 pprPatSynSig :: (OutputableBndr name)
              => name -> Bool -> SDoc -> Maybe SDoc -> Maybe SDoc -> SDoc -> SDoc
index 2b4e779..be36b4e 100644 (file)
@@ -1191,29 +1191,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
 
index fba320c..50c28db 100644 (file)
@@ -157,7 +157,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'
@@ -248,7 +248,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)
index 56751d5..be60056 100644 (file)
@@ -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 )
@@ -63,7 +64,6 @@ import TcValidity (checkValidType)
 import qualified GHC.LanguageExtensions as LangExt
 
 import Control.Monad
-import Data.List (partition)
 
 #include "HsVersions.h"
 
@@ -1684,46 +1684,8 @@ tcTySig (L loc (TypeSig names sig_ty))
        ; return (map TcIdSig sigs) }
 
 tcTySig (L loc (PatSynSig (L _ name) sig_ty))
-  | HsIB { hsib_vars = sig_vars
-         , hsib_body = hs_ty }  <- sig_ty
-  , (tv_bndrs, req, prov, body_ty) <- splitLHsPatSynTy hs_ty
   = setSrcSpan loc $
-    do { (tvs1, (req', prov', ty', tvs2))
-           <- tcImplicitTKBndrs sig_vars $
-              tcHsTyVarBndrs tv_bndrs    $ \ tvs2 ->
-              do { req'  <- tcHsContext req
-                 ; prov' <- tcHsContext prov
-                 ; ty'   <- tcHsLiftedType body_ty
-                 ; let bound_tvs
-                         = unionVarSets [ allBoundVariabless req'
-                                        , allBoundVariabless prov'
-                                        , allBoundVariables ty' ]
-                 ; return ((req', prov', ty', tvs2), bound_tvs) }
-
-       -- These are /signatures/ so we zonk to squeeze out any kind
-       -- unification variables.  ToDo: checkValidType?
-       ; qtvs' <- mapMaybeM zonkQuantifiedTyVar (tvs1 ++ tvs2)
-       ; req'  <- zonkTcTypes req'
-       ; prov' <- zonkTcTypes prov'
-       ; ty'   <- zonkTcType  ty'
-
-       ; let (_, pat_ty) = tcSplitFunTys ty'
-             univ_set = tyCoVarsOfType pat_ty
-             (univ_tvs, ex_tvs) = partition (`elemVarSet` univ_set) qtvs'
-             bad_tvs = varSetElems (tyCoVarsOfTypes req' `minusVarSet` univ_set)
-
-       ; unless (null bad_tvs) $ addErr $
-         hang (ptext (sLit "The 'required' context") <+> quotes (pprTheta req'))
-            2 (ptext (sLit "mentions existential type variable") <> plural bad_tvs
-               <+> pprQuotedList bad_tvs)
-
-       ; traceTc "tcTySig }" $ ppr (ex_tvs, prov') $$ ppr (univ_tvs, req') $$ ppr ty'
-       ; let tpsi = TPSI{ patsig_name = name,
-                          patsig_tau  = ty',
-                          patsig_ex   = ex_tvs,
-                          patsig_univ = univ_tvs,
-                          patsig_prov = prov',
-                          patsig_req  = req' }
+    do { tpsi <- tcPatSynSig name sig_ty
        ; return [TcPatSynSig tpsi] }
 
 tcTySig _ = return []
index 008b933..f299e9d 100644 (file)
@@ -842,15 +842,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
@@ -1327,7 +1327,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
index c7b208e..5ba86e1 100644 (file)
@@ -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.
@@ -2055,7 +2055,7 @@ Here
 
  * The type signature pattern (f :: a->Int) binds "a" -> a_sig in the envt
 
- * Then unificaiton makes a_sig := a_sk
+ * Then unification makes a_sig := a_sk
 
 That's why we must make a_sig a MetaTv (albeit a SigTv),
 not a SkolemTv, so that it can unify to a_sk.
index b0776f6..9285f9a 100644 (file)
@@ -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
index f76da5b..b951ad2 100644 (file)
@@ -706,7 +706,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
@@ -776,7 +776,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) }
@@ -800,7 +800,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,
index 61b54fd..d7477ee 100644 (file)
@@ -7,19 +7,20 @@
 
 {-# 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
 import TysPrim
 import TysWiredIn  ( levityTy )
 import Name
-import Coercion    ( emptyCvSubstEnv )
 import SrcLoc
 import PatSyn
 import NameSet
@@ -38,21 +39,141 @@ import TcEvidence
 import BuildTyCl
 import VarSet
 import MkId
-import VarEnv
 import Inst
 import TcTyDecls
 import ConLike
 import FieldLabel
 #if __GLASGOW_HASKELL__ < 709
-import Data.Monoid
+import Data.Monoid( mconcat, mappend, mempty )
 #endif
 import Bag
 import Util
 import Data.Maybe
-import Control.Monad (forM)
+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 }) }
+
+
 {-
 ************************************************************************
 *                                                                      *
@@ -63,9 +184,9 @@ import Control.Monad (forM)
 
 tcInferPatSynDecl :: PatSynBind Name Name
                   -> TcM (LHsBinds Id, TcGblEnv)
-tcInferPatSynDecl PSB{ psb_id = lname@(L loc name), psb_args = details,
+tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
                        psb_def = lpat, psb_dir = dir }
-  = setSrcSpan loc $
+  = addPatSynCtxt lname $
     do { traceTc "tcInferPatSynDecl {" $ ppr name
        ; tcCheckPatSynPat lpat
 
@@ -81,93 +202,136 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L loc name), psb_args = details,
 
        ; (qtvs, req_dicts, ev_binds) <- simplifyInfer tclvl False [] named_taus wanted
 
-       ; (ex_vars, prov_dicts) <- tcCollectEx lpat'
-       ; let univ_tvs   = filter (not . (`elemVarSet` ex_vars)) qtvs
+       ; let (ex_vars, prov_dicts) = tcCollectEx lpat'
+             univ_tvs   = filter (not . (`elemVarSet` ex_vars)) qtvs
              ex_tvs     = varSetElems ex_vars
              prov_theta = map evVarPred prov_dicts
              req_theta  = map evVarPred req_dicts
 
        ; traceTc "tcInferPatSynDecl }" $ ppr name
        ; tc_patsyn_finish lname dir is_infix lpat'
-                          (univ_tvs, req_theta, ev_binds, req_dicts)
-                          (ex_tvs, mkTyVarTys ex_tvs, prov_theta, emptyTcEvBinds, map EvId prov_dicts)
-                          (zip args $ repeat idHsWrapper)
+                          (univ_tvs, req_theta,  ev_binds, req_dicts)
+                          (ex_tvs,   mkTyVarTys ex_tvs, prov_theta, map EvId prov_dicts)
+                          (map nlHsVar args, map idType args)
                           pat_ty rec_fields }
 
 
 tcCheckPatSynDecl :: PatSynBind Name Name
                   -> TcPatSynInfo
                   -> TcM (LHsBinds Id, TcGblEnv)
-tcCheckPatSynDecl PSB{ psb_id = lname@(L loc name), psb_args = details,
-                       psb_def = lpat, psb_dir = dir }
-                  TPSI{ patsig_tau = tau,
-                        patsig_ex = ex_tvs, patsig_univ = univ_tvs,
-                        patsig_prov = prov_theta, patsig_req = req_theta }
-  = setSrcSpan loc $
-    do { traceTc "tcCheckPatSynDecl" $
-         ppr (ex_tvs, prov_theta) $$
-         ppr (univ_tvs, req_theta) $$
-         ppr arg_tys $$
-         ppr tau
+tcCheckPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details
+                     , psb_def = lpat, psb_dir = dir }
+                  TPSI{ patsig_univ_tvs = univ_tvs, patsig_prov = prov_theta
+                      , patsig_ex_tvs   = ex_tvs,   patsig_req  = req_theta
+                      , patsig_arg_tys  = arg_tys,  patsig_body_ty = pat_ty }
+  = addPatSynCtxt lname $
+    do { let origin     = PatOrigin -- TODO
+             skol_info  = SigSkol (PatSynCtxt name) (mkFunTys arg_tys pat_ty)
+             decl_arity = length arg_names
+             ty_arity   = length arg_tys
+             (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
+
+       ; traceTc "tcCheckPatSynDecl" $
+         vcat [ ppr univ_tvs, ppr req_theta, ppr ex_tvs
+              , ppr prov_theta, ppr arg_tys, ppr pat_ty ]
+
+       ; checkTc (decl_arity == ty_arity)
+                 (wrongNumberOfParmsErr name decl_arity ty_arity)
+
        ; tcCheckPatSynPat lpat
 
+       -- Right!  Let's check the pattern against the signature
+       -- See Note [Checking against a pattern signature]
        ; req_dicts <- newEvVars req_theta
-
-       -- TODO: find a better SkolInfo
-       ; let skol_info = SigSkol (PatSynCtxt name) (mkFunTys arg_tys pat_ty)
-
-       ; let (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
-
-       ; let ty_arity = length arg_tys
-       ; checkTc (length arg_names == ty_arity)
-                 (wrongNumberOfParmsErr ty_arity)
-
-         -- Typecheck the pattern against pat_ty, then unify the type of args
-         -- against arg_tys, with ex_tvs changed to SigTyVars.
-         -- We get out of this:
-         --  * The evidence bindings for the requested theta: req_ev_binds
-         --  * The typechecked pattern: lpat'
-         --  * The arguments, type-coerced to the SigTyVars: wrapped_args
-         --  * The instantiation of ex_tvs to pass to the success continuation: ex_tys
-         --  * The provided theta substituted with the SigTyVars: prov_theta'
-       ; (implic1, req_ev_binds, (lpat', (ex_tys, prov_theta', wrapped_args))) <-
-           buildImplication skol_info univ_tvs req_dicts $
-           tcPat PatSyn lpat pat_ty $ do
-           { ex_sigtvs <- mapM (\tv -> newSigTyVar (getName tv) (tyVarKind tv)) ex_tvs
-           ; let subst = mkTCvSubst (mkInScopeSet (zipVarEnv ex_sigtvs ex_sigtvs)) $
-                         ( zipTyEnv ex_tvs (mkTyVarTys ex_sigtvs)
-                         , emptyCvSubstEnv )
-           ; let ex_tys = substTys subst $ mkTyVarTys ex_tvs
-                 prov_theta' = substTheta subst prov_theta
-           ; wrapped_args <- forM (zipEqual "tcCheckPatSynDecl" arg_names arg_tys) $ \(arg_name, arg_ty) -> do
-               { arg <- tcLookupId arg_name
-               ; let arg_ty' = substTy subst arg_ty
-               ; coi <- unifyType (Just arg) (varType arg) arg_ty'
-               ; return (setVarType arg arg_ty, mkWpCastN coi) }
-           ; return (ex_tys, prov_theta', wrapped_args) }
-
-       ; (ex_vars_rhs, prov_dicts_rhs) <- tcCollectEx lpat'
-       ; let ex_tvs_rhs  = varSetElems ex_vars_rhs
-
-         -- Check that prov_theta' can be satisfied with the dicts from the pattern
-       ; (implic2, prov_ev_binds, prov_dicts) <-
-           buildImplication skol_info ex_tvs_rhs prov_dicts_rhs $ do
-           { let origin = PatOrigin -- TODO
-           ; mapM (emitWanted origin) prov_theta' }
+       ; (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') <- 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 (ex_tvs', prov_dicts, args') }
+
+       ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info univ_tvs req_dicts wanted
 
        -- Solve the constraints now, because we are about to make a PatSyn,
        -- which should not contain unification variables and the like (Trac #10997)
        -- Since all the inputs are implications the returned bindings will be empty
-       ; _ <- simplifyTop (emptyWC `addImplics` (implic1 `unionBags` implic2))
+       ; _ <- 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, req_ev_binds, req_dicts)
-                          (ex_tvs, ex_tys, prov_theta, prov_ev_binds, prov_dicts)
-                          wrapped_args
+                          (univ_tvs, req_theta, ev_binds, req_dicts)
+                          (ex_tvs, mkTyVarTys ex_tvs', prov_theta, prov_dicts)
+                          (args', arg_tys)
                           pat_ty rec_fields }
   where
-    (arg_tys, pat_ty) = tcSplitFunTys tau
+    tc_arg :: TCvSubst -> Name -> Type -> TcM (LHsExpr TcId)
+    tc_arg subst arg_name arg_ty
+      = do {   -- Look up the variable actually bound by lpat
+               -- and check that it has the expected type
+             arg_id <- tcLookupId arg_name
+           ; coi <- unifyType (Just arg_id)
+                              (idType arg_id)
+                              (substTy subst arg_ty)
+           ; return (mkLHsWrapCo coi $ nlHsVar arg_id) }
+
+{- 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
+      MkT :: Ord a => a -> T a
+
+    pattern P :: () => Eq a => a -> [T a]
+    pattern P x = [MkT x]
+
+We must check that the (Eq a) that P claims to bind (and to
+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)
 collectPatSynArgInfo details =
@@ -184,10 +348,18 @@ collectPatSynArgInfo details =
                                          , recordPatSynSelectorId = L _ selId })
       = (patVar, selId)
 
-wrongNumberOfParmsErr :: Arity -> SDoc
-wrongNumberOfParmsErr ty_arity
-  = ptext (sLit "Number of pattern synonym arguments doesn't match type; expected")
-    <+> ppr ty_arity
+addPatSynCtxt :: Located Name -> TcM a -> TcM a
+addPatSynCtxt (L loc name) thing_inside
+  = setSrcSpan loc $
+    addErrCtxt (ptext (sLit "In the declaration for pattern synonym")
+                <+> quotes (ppr name)) $
+    thing_inside
+
+wrongNumberOfParmsErr :: Name -> Arity -> Arity -> SDoc
+wrongNumberOfParmsErr name decl_arity ty_arity
+  = hang (ptext (sLit "Patten synonym") <+> quotes (ppr name) <+> ptext (sLit "has")
+          <+> speakNOf decl_arity (ptext (sLit "argument")))
+       2 (ptext (sLit "but its type signature has") <+> speakN ty_arity)
 
 -------------------------
 -- Shared by both tcInferPatSyn and tcCheckPatSyn
@@ -196,16 +368,16 @@ tc_patsyn_finish :: Located Name  -- ^ PatSyn Name
                  -> Bool              -- ^ Whether infix
                  -> LPat Id           -- ^ Pattern of the PatSyn
                  -> ([TcTyVar], [PredType], TcEvBinds, [EvVar])
-                 -> ([TcTyVar], [TcType], [PredType], TcEvBinds, [EvTerm])
-                 -> [(Var, HsWrapper)]  -- ^ Pattern arguments
+                 -> ([TcTyVar], [TcType], [PredType], [EvTerm])
+                 -> ([LHsExpr TcId], [TcType])   -- ^ Pattern arguments and types
                  -> TcType              -- ^ Pattern type
                  -> [Name]              -- ^ Selector names
                  -- ^ Whether fields, empty if not record PatSyn
                  -> TcM (LHsBinds Id, TcGblEnv)
 tc_patsyn_finish lname dir is_infix lpat'
                  (univ_tvs, req_theta, req_ev_binds, req_dicts)
-                 (ex_tvs, subst, prov_theta, prov_ev_binds, prov_dicts)
-                 wrapped_args
+                 (ex_tvs, ex_tys, prov_theta, prov_dicts)
+                 (args, arg_tys)
                  pat_ty field_labels
   = do { -- Zonk everything.  We are about to build a final PatSyn
          -- so there had better be no unification variables in there
@@ -214,26 +386,26 @@ tc_patsyn_finish lname dir is_infix lpat'
        ; prov_theta   <- zonkTcTypes prov_theta
        ; req_theta    <- zonkTcTypes req_theta
        ; pat_ty       <- zonkTcType pat_ty
-       ; wrapped_args <- mapM zonk_wrapped_arg wrapped_args
+       ; arg_tys      <- zonkTcTypes arg_tys
        ; let qtvs    = univ_tvs ++ ex_tvs
              -- See Note [Record PatSyn Desugaring]
              theta   = prov_theta ++ req_theta
-             arg_tys = map (varType . fst) wrapped_args
 
        ;
 
         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 (ex_tvs, prov_theta, prov_dicts) $$
+           ppr args $$
+           ppr arg_tys $$
            ppr pat_ty
 
        -- Make the 'matcher'
        ; (matcher_id, matcher_bind) <- tcPatSynMatcher lname lpat'
                                          (univ_tvs, req_theta, req_ev_binds, req_dicts)
-                                         (ex_tvs, subst, prov_theta, prov_ev_binds, prov_dicts)
-                                         wrapped_args  -- Not necessarily zonked
+                                         (ex_tvs, ex_tys, prov_theta, prov_dicts)
+                                         (args, arg_tys)
                                          pat_ty
 
 
@@ -264,14 +436,9 @@ tc_patsyn_finish lname dir is_infix lpat'
             tcRecSelBinds
               (ValBindsOut (zip (repeat NonRecursive) selector_binds) sigs)
 
+       ; traceTc "tc_patsyn_finish }" empty
        ; return (matcher_bind, tcg_env) }
 
-  where
-    zonk_wrapped_arg :: (Var, HsWrapper) -> TcM (Var, HsWrapper)
-    -- The HsWrapper will get zonked later, as part of the LHsBinds
-    zonk_wrapped_arg (arg_id, wrap) = do { arg_id <- zonkId arg_id
-                                         ; return (arg_id, wrap) }
-
 {-
 ************************************************************************
 *                                                                      *
@@ -283,15 +450,15 @@ tc_patsyn_finish lname dir is_infix lpat'
 tcPatSynMatcher :: Located Name
                 -> LPat Id
                 -> ([TcTyVar], ThetaType, TcEvBinds, [EvVar])
-                -> ([TcTyVar], [TcType], ThetaType, TcEvBinds, [EvTerm])
-                -> [(Var, HsWrapper)]
+                -> ([TcTyVar], [TcType], ThetaType, [EvTerm])
+                -> ([LHsExpr TcId], [TcType])
                 -> TcType
                 -> TcM ((Id, Bool), LHsBinds Id)
 -- See Note [Matchers and builders for pattern synonyms] in PatSyn
 tcPatSynMatcher (L loc name) lpat
                 (univ_tvs, req_theta, req_ev_binds, req_dicts)
-                (ex_tvs, ex_tys, prov_theta, prov_ev_binds, prov_dicts)
-                wrapped_args pat_ty
+                (ex_tvs, ex_tys, prov_theta, prov_dicts)
+                (args, arg_tys) pat_ty
   = do { lev_uniq <- newUnique
        ; tv_uniq  <- newUnique
        ; let lev_name = mkInternalName lev_uniq (mkTyVarOcc "rlev") loc
@@ -299,13 +466,11 @@ tcPatSynMatcher (L loc name) lpat
              lev_tv   = mkTcTyVar lev_name levityTy   (SkolemTv False)
              lev      = mkTyVarTy lev_tv
              res_tv   = mkTcTyVar tv_name  (tYPE lev) (SkolemTv False)
-             is_unlifted = null wrapped_args && null prov_dicts
+             is_unlifted = null args && null prov_dicts
              res_ty = mkTyVarTy res_tv
-             (cont_arg_tys, cont_args)
-               | is_unlifted = ([voidPrimTy], [nlHsVar voidPrimId])
-               | otherwise   = unzip [ (varType arg, mkLHsWrap wrap $ nlHsVar arg)
-                                     | (arg, wrap) <- wrapped_args
-                                     ]
+             (cont_args, cont_arg_tys)
+               | is_unlifted = ([nlHsVar voidPrimId], [voidPrimTy])
+               | otherwise   = (args,                 arg_tys)
              cont_ty = mkInvSigmaTy ex_tvs prov_theta $
                        mkFunTys cont_arg_tys res_ty
 
@@ -321,10 +486,8 @@ tcPatSynMatcher (L loc name) lpat
              matcher_id    = mkExportedLocalId PatSynId matcher_name matcher_sigma
                              -- See Note [Exported LocalIds] in Id
 
-             cont' = mkLHsWrap (mkWpLet prov_ev_binds) $
-                     foldl nlHsApp
-                       (mkLHsWrap (mkWpEvApps prov_dicts)
-                                  (nlHsTyApp cont ex_tys)) cont_args
+             inst_wrap = mkWpEvApps prov_dicts <.> mkWpTyApps ex_tys
+             cont' = foldl nlHsApp (mkLHsWrap inst_wrap (nlHsVar cont)) cont_args
 
              fail' = nlHsApps fail [nlHsVar voidPrimId]
 
@@ -425,6 +588,7 @@ tcPatSynBuilderBind PSB{ psb_id = L loc name, psb_def = lpat
 
   | otherwise  -- Bidirectional
   = do { patsyn <- tcLookupPatSyn name
+       ; traceTc "tcPatSynBuilderBind {" $ ppr patsyn
        ; let Just (builder_id, need_dummy_arg) = patSynBuilder patsyn
                    -- Bidirectional, so patSynBuilder returns Just
 
@@ -540,7 +704,6 @@ simply discard the signature.
 
 Note [Record PatSyn Desugaring]
 -------------------------------
-
 It is important that prov_theta comes before req_theta as this ordering is used
 when desugaring record pattern synonym updates.
 
@@ -645,8 +808,8 @@ tcPatToExpr args = go
 -- These are used in computing the type of a pattern synonym and also
 -- in generating matcher functions, since success continuations need
 -- to be passed these pattern-bound evidences.
-tcCollectEx :: LPat Id -> TcM (TyVarSet, [EvVar])
-tcCollectEx = return . go
+tcCollectEx :: LPat Id -> (TyVarSet, [EvVar])
+tcCollectEx pat = go pat
   where
     go :: LPat Id -> (TyVarSet, [EvVar])
     go = go1 . unLoc
@@ -676,3 +839,4 @@ tcCollectEx = return . go
 
     goRecFd :: LHsRecField Id (LPat Id) -> (TyVarSet, [EvVar])
     goRecFd (L _ HsRecField{ hsRecFieldArg = p }) = go p
+
index 11c1bc1..af5aec7 100644 (file)
@@ -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)
 
index 9316d43..8489512 100644 (file)
@@ -1178,12 +1178,13 @@ data TcIdSigBndr   -- See Note [Complete and partial type signatures]
 
 data TcPatSynInfo
   = TPSI {
-        patsig_name  :: Name,
-        patsig_tau   :: TcSigmaType,
-        patsig_ex    :: [TcTyVar],
-        patsig_prov  :: TcThetaType,
-        patsig_univ  :: [TcTyVar],
-        patsig_req   :: TcThetaType
+        patsig_name     :: Name,
+        patsig_univ_tvs :: [TcTyVar],
+        patsig_req      :: TcThetaType,
+        patsig_ex_tvs   :: [TcTyVar],
+        patsig_prov     :: TcThetaType,
+        patsig_arg_tys  :: [TcSigmaType],
+        patsig_body_ty  :: TcSigmaType
     }
 
 findScopedTyVars  -- See Note [Binding scoped type variables]
index 1257dbf..51a1eee 100644 (file)
@@ -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
index b15ac12..c53a012 100644 (file)
@@ -57,7 +57,7 @@ module TyCoRep (
 
         -- Free variables
         tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet,
-        tyCoVarsOfTypeAcc, tyCoVarsOfTypeList,
+        tyCoVarsBndrAcc, tyCoVarsOfTypeAcc, tyCoVarsOfTypeList,
         tyCoVarsOfTypesAcc, tyCoVarsOfTypesList,
         closeOverKindsDSet, closeOverKindsAcc,
         coVarsOfType, coVarsOfTypes,
@@ -1049,19 +1049,24 @@ tyCoVarsOfTypeList ty = runFVList $ tyCoVarsOfTypeAcc ty
 -- | The worker for `tyVarsOfType` and `tyVarsOfTypeList`.
 -- The previous implementation used `unionVarSet` which is O(n+m) and can
 -- make the function quadratic.
--- It's exported, so that it can be composed with other functions that compute
--- free variables.
+-- It's exported, so that it can be composed with
+-- other functions that compute free variables.
 -- See Note [FV naming conventions] in FV.
+--
+-- Eta-expanded because that makes it run faster (apparently)
 tyCoVarsOfTypeAcc :: Type -> FV
-tyCoVarsOfTypeAcc (TyVarTy v)         fv_cand in_scope acc = (oneVar v `unionFV` tyCoVarsOfTypeAcc (tyVarKind v)) fv_cand in_scope acc
-tyCoVarsOfTypeAcc (TyConApp _ tys)    fv_cand in_scope acc = tyCoVarsOfTypesAcc tys fv_cand in_scope acc
-tyCoVarsOfTypeAcc (LitTy {})          fv_cand in_scope acc = noVars fv_cand in_scope acc
-tyCoVarsOfTypeAcc (AppTy fun arg)     fv_cand in_scope acc = (tyCoVarsOfTypeAcc fun `unionFV` tyCoVarsOfTypeAcc arg) fv_cand in_scope acc
-tyCoVarsOfTypeAcc (ForAllTy bndr ty) fv_cand in_scope acc
-  = (delBinderVarFV bndr (tyCoVarsOfTypeAcc ty)
-     `unionFV` tyCoVarsOfTypeAcc (binderType bndr)) fv_cand in_scope acc
-tyCoVarsOfTypeAcc (CastTy ty co)      fv_cand in_scope acc = (tyCoVarsOfTypeAcc ty `unionFV` tyCoVarsOfCoAcc co) fv_cand in_scope acc
-tyCoVarsOfTypeAcc (CoercionTy co)     fv_cand in_scope acc = tyCoVarsOfCoAcc co fv_cand in_scope acc
+tyCoVarsOfTypeAcc (TyVarTy v)        a b c = (oneVar v `unionFV` tyCoVarsOfTypeAcc (tyVarKind v)) a b c
+tyCoVarsOfTypeAcc (TyConApp _ tys)   a b c = tyCoVarsOfTypesAcc tys a b c
+tyCoVarsOfTypeAcc (LitTy {})         a b c = noVars a b c
+tyCoVarsOfTypeAcc (AppTy fun arg)    a b c = (tyCoVarsOfTypeAcc fun `unionFV` tyCoVarsOfTypeAcc arg) a b c
+tyCoVarsOfTypeAcc (ForAllTy bndr ty) a b c = tyCoVarsBndrAcc bndr (tyCoVarsOfTypeAcc ty)  a b c
+tyCoVarsOfTypeAcc (CastTy ty co)     a b c = (tyCoVarsOfTypeAcc ty `unionFV` tyCoVarsOfCoAcc co) a b c
+tyCoVarsOfTypeAcc (CoercionTy co)    a b c = tyCoVarsOfCoAcc co a b c
+
+tyCoVarsBndrAcc :: TyBinder -> FV -> FV
+-- Free vars of (forall b. <thing with fvs>)
+tyCoVarsBndrAcc bndr fvs = delBinderVarFV bndr fvs
+                           `unionFV` tyCoVarsOfTypeAcc (binderType bndr)
 
 -- | Returns free variables of types, including kind variables as
 -- a non-deterministic set. For type synonyms it does /not/ expand the
diff --git a/testsuite/tests/patsyn/should_compile/MoreEx.hs b/testsuite/tests/patsyn/should_compile/MoreEx.hs
new file mode 100644 (file)
index 0000000..ed5e097
--- /dev/null
@@ -0,0 +1,20 @@
+{-# LANGUAGE GADTs, PatternSynonyms #-}
+
+-- Tests that for unidirectional pattern synonyms
+-- the pattern synonym can be more existential
+-- (i.e. lose information) wrt the original
+
+module MoreEx where
+
+pattern ExCons :: a -> [a] -> [b]
+pattern ExCons x xs <- x : xs
+
+data T where
+  MkT1 :: ([a] -> Int) -> [a] -> T
+  MkT2 :: (a -> Int) -> a -> T
+
+pattern ExT1 :: b -> (b -> Int) -> T
+pattern ExT1 x f <- MkT1 f x
+
+pattern ExT2 :: b -> (c -> Int) -> T
+pattern ExT2 x f <- MkT2 f x
diff --git a/testsuite/tests/patsyn/should_compile/T11224b.hs b/testsuite/tests/patsyn/should_compile/T11224b.hs
new file mode 100644 (file)
index 0000000..89fb764
--- /dev/null
@@ -0,0 +1,17 @@
+{-# LANGUAGE PatternSynonyms, GADTs, RankNTypes #-}
+
+module T11224b where
+
+data T b where
+  MkT :: a -> b -> T b
+
+-- Should be fine!
+-- pattern P :: c -> d -> T d
+pattern P :: forall d. forall c. c -> d -> T d
+pattern P x y <- MkT x y
+
+
+
+
+
+
index 3793c0d..f3d90ac 100644 (file)
@@ -24,6 +24,7 @@ test('T9889', normal, compile, [''])
 test('T9867', normal, compile, [''])
 test('T9975a', normal, compile_fail, [''])
 test('T9975b', normal, compile, [''])
+test('T10426', [expect_broken(10426)], compile, [''])
 test('T10747', normal, compile, [''])
 test('T10997', [extra_clean(['T10997a.hi', 'T10997a.o'])], multimod_compile, ['T10997', '-v0'])
 test('T10997_1', [extra_clean(['T10997_1a.hi', 'T10997_1a.o'])], multimod_compile, ['T10997_1', '-v0'])
@@ -45,3 +46,5 @@ test('T10897', expect_broken(10897), multi_compile, ['T10897', [
                                        ('T10897a.hs','-c')
                                       ,('T10897b.hs', '-c')], ''])
 test('T9793', normal, compile, [''])
+test('T11224b', normal, compile, [''])
+test('MoreEx', normal, compile, [''])
index 5f62b13..47492cd 100644 (file)
@@ -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)
index 62713dc..23122f9 100644 (file)
@@ -1,4 +1,5 @@
 
 T9793-fail.hs:6:16: error:
-    Pattern synonym definition cannot contain as-patterns (@) which contain free variables:
-      x@(y : _)
+    • Pattern synonym definition cannot contain as-patterns (@) which contain free variables:
+        x@(y : _)
+    • In the declaration for pattern synonym ‘P’
index caabd47..00ea6c8 100644 (file)
@@ -1,4 +1,5 @@
 
 as-pattern.hs:4:18: error:
-    Pattern synonym definition cannot contain as-patterns (@) which contain free variables:
-      x@(Just y)
+    • Pattern synonym definition cannot contain as-patterns (@) which contain free variables:
+        x@(Just y)
+    • In the declaration for pattern synonym ‘P’
index f834e9b..39c744c 100644 (file)
@@ -1,10 +1,10 @@
-{-# LANGUAGE PatternSynonyms , ViewPatterns #-}
+{-# LANGUAGE  PatternSynonyms, ViewPatterns #-}
 
--- inlining a pattern synonym shouldn't change semantics
+module Main where
 
 import Text.Read
 
--- pattern PRead :: () => Read a => a -> String
+pattern PRead :: Read a => () => a -> String
 pattern PRead a <- (readMaybe -> Just a)
 
 foo :: String -> Int
@@ -26,3 +26,4 @@ main = do
   print $ bar "1"       -- 1
   print $ bar "[1,2,3]" -- 6
   print $ bar "xxx"     -- 666
+
index c12bfc6..618dd69 100644 (file)
@@ -12,4 +12,5 @@ test('match-unboxed', normal, compile_and_run, [''])
 test('unboxed-wrapper', normal, compile_and_run, [''])
 test('records-run', normal, compile_and_run, [''])
 test('ghci', just_ghci, ghci_script, ['ghci.script'])
-test('T11224', [expect_broken(11224)], compile_and_run, [''])
\ No newline at end of file
+test('T11224', [expect_broken(11224)], compile_and_run, [''])
+test('T11224', normal, compile_and_run, [''])