diff --git a/compiler/basicTypes/PatSyn.lhs b/compiler/basicTypes/PatSyn.lhs
index 9285b3c365a7c9fd76407f50558cff9ae9ee6afd..29c1193482a03347b0c51013fe2c9b4ddacd1e11 100644
--- a/compiler/basicTypes/PatSyn.lhs
+++ b/compiler/basicTypes/PatSyn.lhs
@@ -12,7 +12,7 @@ module PatSyn (
 
         -- ** Type deconstruction
         patSynId, patSynType, patSynArity, patSynIsInfix,
-        patSynArgs, patSynArgTys, patSynTyDetails,
+        patSynArgs, patSynTyDetails,
         patSynWrapper, patSynMatcher,
         patSynExTyVars, patSynSig, patSynInstArgTys
     ) where
@@ -37,8 +37,8 @@ import Data.Function
 \end{code}
 
 
-Pattern synonym representation
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Pattern synonym representation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider the following pattern synonym declaration
 
         pattern P x = MkT [x] (Just 42)
@@ -58,15 +58,49 @@ with the following typeclass constraints:
 
 In this case, the fields of MkPatSyn will be set as follows:
 
-  psArgs       = [x :: b]
+  psArgs       = [b]
   psArity      = 1
   psInfix      = False
 
   psUnivTyVars = [t]
   psExTyVars   = [b]
-  psTheta      = ((Show (Maybe t), Ord b), (Eq t, Num t))
+  psProvTheta  = (Show (Maybe t), Ord b)
+  psReqTheta   = (Eq t, Num t)
   psOrigResTy  = T (Maybe t)
 
+Note [Matchers and wrappers for pattern synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For each pattern synonym, we generate a single matcher function which
+implements the actual matching. For the above example, the matcher
+will have type:
+
+        $mP :: forall r t. (Eq t, Num t)
+            => T (Maybe t)
+            -> (forall b. (Show (Maybe t), Ord b) => b -> r)
+            -> r
+            -> r
+
+with the following implementation:
+
+        $mP @r @t $dEq $dNum scrut cont fail = case scrut of
+            MkT @b $dShow $dOrd [x] (Just 42) -> cont @b $dShow $dOrd x
+            _                                 -> fail
+
+For *bidirectional* pattern synonyms, we also generate a single wrapper
+function which implements the pattern synonym in an expression
+context. For our running example, it will be:
+
+        $WP :: forall t b. (Show (Maybe t), Ord b, Eq t, Num t)
+            => b -> T (Maybe t)
+        $WP x = MkT [x] (Just 42)
+
+NB: the existential/universal and required/provided split does not
+apply to the wrapper since you are only putting stuff in, not getting
+stuff out.
+
+Injectivity of bidirectional pattern synonyms is checked in
+tcPatToExpr which walks the pattern and returns its corresponding
+expression when available.
 
 %************************************************************************
 %*                                                                      *
@@ -76,21 +110,36 @@ In this case, the fields of MkPatSyn will be set as follows:
 
 \begin{code}
 -- | A pattern synonym
+-- See Note [Pattern synonym representation]
 data PatSyn
   = MkPatSyn {
         psId          :: Id,
-        psUnique      :: Unique,                 -- Cached from Name
-        psMatcher     :: Id,
-        psWrapper     :: Maybe Id,
+        psUnique      :: Unique,      -- Cached from Name
+
+        psArgs        :: [Type],
+        psArity       :: Arity,       -- == length psArgs
+        psInfix       :: Bool,        -- True <=> declared infix
 
-        psArgs        :: [Var],
-        psArity       :: Arity,                  -- == length psArgs
-        psInfix       :: Bool,                   -- True <=> declared infix
+        psUnivTyVars  :: [TyVar],     -- Universially-quantified type variables
+        psExTyVars    :: [TyVar],     -- Existentially-quantified type vars
+        psProvTheta   :: ThetaType,   -- Provided dictionaries
+        psReqTheta    :: ThetaType,   -- Required dictionaries
+        psOrigResTy   :: Type,
 
-        psUnivTyVars  :: [TyVar],                -- Universially-quantified type variables
-        psExTyVars    :: [TyVar],                -- Existentially-quantified type vars
-        psTheta       :: (ThetaType, ThetaType), -- Provided and required dictionaries
-        psOrigResTy   :: Type
+        -- See Note [Matchers and wrappers for pattern synonyms]
+        psMatcher     :: Id,
+             -- Matcher function, of type
+             --   forall r univ_tvs. req_theta
+             --                   => res_ty
+             --                   -> (forall ex_tvs. prov_theta -> arg_tys -> r)
+             --                   -> r -> r
+
+        psWrapper     :: Maybe Id
+             -- Nothing  => uni-directional pattern synonym
+             -- Just wid => bi-direcitonal
+             -- Wrapper function, of type
+             --  forall univ_tvs, ex_tvs. (prov_theta, req_theta)
+             --                       =>  arg_tys -> res_ty
   }
   deriving Data.Typeable.Typeable
 \end{code}
@@ -144,7 +193,7 @@ instance Data.Data PatSyn where
 -- | Build a new pattern synonym
 mkPatSyn :: Name
          -> Bool       -- ^ Is the pattern synonym declared infix?
-         -> [Var]      -- ^ Original arguments
+         -> [Type]     -- ^ Original arguments
          -> [TyVar]    -- ^ Universially-quantified type variables
          -> [TyVar]    -- ^ Existentially-quantified type variables
          -> ThetaType  -- ^ Wanted dicts
@@ -160,7 +209,7 @@ mkPatSyn name declared_infix orig_args
          matcher wrapper
     = MkPatSyn {psId = id, psUnique = getUnique name,
                 psUnivTyVars = univ_tvs, psExTyVars = ex_tvs,
-                psTheta = (prov_theta, req_theta),
+                psProvTheta = prov_theta, psReqTheta = req_theta,
                 psInfix = declared_infix,
                 psArgs = orig_args,
                 psArity = length orig_args,
@@ -170,7 +219,7 @@ mkPatSyn name declared_infix orig_args
   where
     pat_ty = mkSigmaTy univ_tvs req_theta $
              mkSigmaTy ex_tvs prov_theta $
-             mkFunTys (map varType orig_args) orig_res_ty
+             mkFunTys orig_args orig_res_ty
     id = mkLocalId name pat_ty
 \end{code}
 
@@ -190,22 +239,21 @@ patSynIsInfix = psInfix
 patSynArity :: PatSyn -> Arity
 patSynArity = psArity
 
-patSynArgs :: PatSyn -> [Var]
+patSynArgs :: PatSyn -> [Type]
 patSynArgs = psArgs
 
-patSynArgTys :: PatSyn -> [Type]
-patSynArgTys = map varType . patSynArgs
-
 patSynTyDetails :: PatSyn -> HsPatSynDetails Type
-patSynTyDetails ps = case (patSynIsInfix ps, patSynArgTys ps) of
+patSynTyDetails ps = case (patSynIsInfix ps, patSynArgs ps) of
     (True, [left, right]) -> InfixPatSyn left right
     (_, tys) -> PrefixPatSyn tys
 
 patSynExTyVars :: PatSyn -> [TyVar]
 patSynExTyVars = psExTyVars
 
-patSynSig :: PatSyn -> ([TyVar], [TyVar], (ThetaType, ThetaType))
-patSynSig ps = (psUnivTyVars ps, psExTyVars ps, psTheta ps)
+patSynSig :: PatSyn -> ([TyVar], [TyVar], ThetaType, ThetaType)
+patSynSig (MkPatSyn { psUnivTyVars = univ_tvs, psExTyVars = ex_tvs
+                    , psProvTheta = prov, psReqTheta = req })
+  = (univ_tvs, ex_tvs, prov, req)
 
 patSynWrapper :: PatSyn -> Maybe Id
 patSynWrapper = psWrapper
@@ -217,9 +265,8 @@ patSynInstArgTys :: PatSyn -> [Type] -> [Type]
 patSynInstArgTys ps inst_tys
   = ASSERT2( length tyvars == length inst_tys
           , ptext (sLit "patSynInstArgTys") <+> ppr ps $$ ppr tyvars $$ ppr inst_tys )
-    map (substTyWith tyvars inst_tys) arg_tys
+    map (substTyWith tyvars inst_tys) (psArgs ps)
   where
-    (univ_tvs, ex_tvs, _) = patSynSig ps
-    arg_tys = map varType (psArgs ps)
+    (univ_tvs, ex_tvs, _, _) = patSynSig ps
     tyvars = univ_tvs ++ ex_tvs
 \end{code}
diff --git a/compiler/coreSyn/CorePrep.lhs b/compiler/coreSyn/CorePrep.lhs
index 5e0cd6599d27ffb80d8bbae519a171bd214754bb..d0a07ccbcb4a9c834e3bf38d6b71df9b0288fb2b 100644
--- a/compiler/coreSyn/CorePrep.lhs
+++ b/compiler/coreSyn/CorePrep.lhs
@@ -196,6 +196,7 @@ corePrepTopBinds initialCorePrepEnv binds
 
 mkDataConWorkers :: [TyCon] -> [CoreBind]
 -- See Note [Data constructor workers]
+-- c.f. Note [Injecting implicit bindings] in TidyPgm
 mkDataConWorkers data_tycons
   = [ NonRec id (Var id)        -- The ice is thin here, but it works
     | tycon <- data_tycons,     -- CorePrep will eta-expand it
diff --git a/compiler/iface/BuildTyCl.lhs b/compiler/iface/BuildTyCl.lhs
index e412d7ef301c88d43d8e38c972e5030fbad5a421..fa46a7352de7c6b9afdf41ea8f258ee2cb34af0a 100644
--- a/compiler/iface/BuildTyCl.lhs
+++ b/compiler/iface/BuildTyCl.lhs
@@ -15,7 +15,7 @@ module BuildTyCl (
         buildSynTyCon,
         buildAlgTyCon, 
         buildDataCon,
-        buildPatSyn, mkPatSynMatcherId, mkPatSynWrapperId,
+        buildPatSyn,
         TcMethInfo, buildClass,
         distinctAbstractTyConRhs, totallyAbstractTyConRhs,
         mkNewTyConRhs, mkDataTyConRhs, 
@@ -36,10 +36,9 @@ import MkId
 import Class
 import TyCon
 import Type
-import TypeRep
-import TcType
 import Id
 import Coercion
+import TcType
 
 import DynFlags
 import TcRnMonad
@@ -184,66 +183,28 @@ mkDataConStupidTheta tycon arg_tys univ_tvs
 
 
 ------------------------------------------------------
-buildPatSyn :: Name -> Bool -> Bool
-            -> [Var]
+buildPatSyn :: Name -> Bool
+            -> Id -> Maybe Id
+            -> [Type]
             -> [TyVar] -> [TyVar]     -- Univ and ext
             -> ThetaType -> ThetaType -- Prov and req
             -> Type                  -- Result type
-            -> TyVar
-            -> TcRnIf m n PatSyn
-buildPatSyn src_name declared_infix has_wrapper args univ_tvs ex_tvs prov_theta req_theta pat_ty tv
-  = do	{ (matcher, _, _) <- mkPatSynMatcherId src_name args
-                                              univ_tvs ex_tvs
-                                              prov_theta req_theta
-                                              pat_ty tv
-        ; wrapper <- case has_wrapper of
-            False -> return Nothing
-            True -> fmap Just $
-                    mkPatSynWrapperId src_name args
-                                      (univ_tvs ++ ex_tvs) (prov_theta ++ req_theta)
-                                      pat_ty
-        ; return $ mkPatSyn src_name declared_infix
-                            args
-                            univ_tvs ex_tvs
-                            prov_theta req_theta
-                            pat_ty
-                            matcher
-                            wrapper }
-
-mkPatSynMatcherId :: Name
-                  -> [Var]
-                  -> [TyVar]
-                  -> [TyVar]
-                  -> ThetaType -> ThetaType
-                  -> Type
-                  -> TyVar
-                  -> TcRnIf n m (Id, Type, Type)
-mkPatSynMatcherId name args univ_tvs ex_tvs prov_theta req_theta pat_ty res_tv
-  = do { matcher_name <- newImplicitBinder name mkMatcherOcc
-
-       ; let res_ty = TyVarTy res_tv
-             cont_ty = mkSigmaTy ex_tvs prov_theta $
-                       mkFunTys (map varType args) res_ty
-
-       ; let matcher_tau = mkFunTys [pat_ty, cont_ty, res_ty] res_ty
-             matcher_sigma = mkSigmaTy (res_tv:univ_tvs) req_theta matcher_tau
-             matcher_id = mkVanillaGlobal matcher_name matcher_sigma
-       ; return (matcher_id, res_ty, cont_ty) }
-
-mkPatSynWrapperId :: Name
-                  -> [Var]
-                  -> [TyVar]
-                  -> ThetaType
-                  -> Type
-                  -> TcRnIf n m Id
-mkPatSynWrapperId name args qtvs theta pat_ty
-  = do { wrapper_name <- newImplicitBinder name mkDataConWrapperOcc
-
-       ; let wrapper_tau = mkFunTys (map varType args) pat_ty
-             wrapper_sigma = mkSigmaTy qtvs theta wrapper_tau
-
-       ; let wrapper_id = mkVanillaGlobal wrapper_name wrapper_sigma
-       ; return wrapper_id }
+            -> PatSyn
+buildPatSyn src_name declared_infix matcher wrapper
+            args univ_tvs ex_tvs prov_theta req_theta pat_ty
+  = mkPatSyn src_name declared_infix
+             args
+             univ_tvs ex_tvs
+             prov_theta req_theta
+             pat_ty
+             matcher
+             wrapper
+  where
+    -- TODO: assert that these match the ones in the parameters
+    ((_:_univ_tvs'), _req_theta', tau) = tcSplitSigmaTy $ idType matcher
+    ([_pat_ty', cont_sigma, _], _) = tcSplitFunTys tau
+    (_ex_tvs', _prov_theta', cont_tau) = tcSplitSigmaTy cont_sigma
+    (_args', _) = tcSplitFunTys cont_tau
 
 \end{code}
 
diff --git a/compiler/iface/IfaceSyn.lhs b/compiler/iface/IfaceSyn.lhs
index 1283b095fdccf3d79b44b29b8bd5c68caec5fc88..a7f1780aacf6c4347c7cbb695106835d633e9726 100644
--- a/compiler/iface/IfaceSyn.lhs
+++ b/compiler/iface/IfaceSyn.lhs
@@ -59,6 +59,7 @@ import HsBinds
 
 import Control.Monad
 import System.IO.Unsafe
+import Data.Maybe (isJust)
 
 infixl 3 &&&
 \end{code}
@@ -120,13 +121,16 @@ data IfaceDecl
                    ifExtName :: Maybe FastString }
 
   | IfacePatSyn { ifName          :: OccName,           -- Name of the pattern synonym
-                  ifPatHasWrapper :: Bool,
                   ifPatIsInfix    :: Bool,
+                  ifPatMatcher    :: IfExtName,
+                  ifPatWrapper    :: Maybe IfExtName,
+                  -- Everything below is redundant,
+                  -- but needed to implement pprIfaceDecl
                   ifPatUnivTvs    :: [IfaceTvBndr],
                   ifPatExTvs      :: [IfaceTvBndr],
                   ifPatProvCtxt   :: IfaceContext,
                   ifPatReqCtxt    :: IfaceContext,
-                  ifPatArgs       :: [IfaceIdBndr],
+                  ifPatArgs       :: [IfaceType],
                   ifPatTy         :: IfaceType }
 
 -- A bit of magic going on here: there's no need to store the OccName
@@ -186,7 +190,7 @@ instance Binary IfaceDecl where
         put_ bh a3
         put_ bh a4
 
-    put_ bh (IfacePatSyn name a2 a3 a4 a5 a6 a7 a8 a9) = do
+    put_ bh (IfacePatSyn name a2 a3 a4 a5 a6 a7 a8 a9 a10) = do
         putByte bh 6
         put_ bh (occNameFS name)
         put_ bh a2
@@ -197,6 +201,7 @@ instance Binary IfaceDecl where
         put_ bh a7
         put_ bh a8
         put_ bh a9
+        put_ bh a10
 
     get bh = do
         h <- getByte bh
@@ -253,8 +258,9 @@ instance Binary IfaceDecl where
                     a7 <- get bh
                     a8 <- get bh
                     a9 <- get bh
+                    a10 <- get bh
                     occ <- return $! mkOccNameFS dataName a1
-                    return (IfacePatSyn occ a2 a3 a4 a5 a6 a7 a8 a9)
+                    return (IfacePatSyn occ a2 a3 a4 a5 a6 a7 a8 a9 a10)
             _ -> panic (unwords ["Unknown IfaceDecl tag:", show h])
 
 data IfaceSynTyConRhs
@@ -1015,11 +1021,6 @@ ifaceDeclImplicitBndrs (IfaceClass {ifCtxt = sc_ctxt, ifName = cls_tc_occ,
     dc_occ = mkClassDataConOcc cls_tc_occ
     is_newtype = n_sigs + n_ctxt == 1 -- Sigh
 
-ifaceDeclImplicitBndrs (IfacePatSyn{ ifName = ps_occ, ifPatHasWrapper = has_wrapper })
-  = [wrap_occ | has_wrapper]
-  where
-    wrap_occ = mkDataConWrapperOcc ps_occ  -- Id namespace
-
 ifaceDeclImplicitBndrs _ = []
 
 -- -----------------------------------------------------------------------------
@@ -1103,7 +1104,7 @@ pprIfaceDecl (IfaceAxiom {ifName = name, ifTyCon = tycon, ifAxBranches = branche
   = hang (ptext (sLit "axiom") <+> ppr name <> dcolon)
        2 (vcat $ map (pprAxBranch $ Just tycon) branches)
 
-pprIfaceDecl (IfacePatSyn { ifName = name, ifPatHasWrapper = has_wrap,
+pprIfaceDecl (IfacePatSyn { ifName = name, ifPatWrapper = wrapper,
                             ifPatIsInfix = is_infix,
                             ifPatUnivTvs = _univ_tvs, ifPatExTvs = _ex_tvs,
                             ifPatProvCtxt = prov_ctxt, ifPatReqCtxt = req_ctxt,
@@ -1111,7 +1112,8 @@ pprIfaceDecl (IfacePatSyn { ifName = name, ifPatHasWrapper = has_wrap,
                             ifPatTy = ty })
   = pprPatSynSig name has_wrap args' ty' (pprCtxt prov_ctxt) (pprCtxt req_ctxt)
   where
-    args' = case (is_infix, map snd args) of
+    has_wrap = isJust wrapper
+    args' = case (is_infix, args) of
         (True, [left_ty, right_ty]) ->
             InfixPatSyn (pprParendIfaceType left_ty) (pprParendIfaceType right_ty)
         (_, tys) ->
@@ -1392,11 +1394,13 @@ freeNamesIfDecl d@IfaceAxiom{} =
   freeNamesIfTc (ifTyCon d) &&&
   fnList freeNamesIfAxBranch (ifAxBranches d)
 freeNamesIfDecl d@IfacePatSyn{} =
+  unitNameSet (ifPatMatcher d) &&&
+  maybe emptyNameSet unitNameSet (ifPatWrapper d) &&&
   freeNamesIfTvBndrs (ifPatUnivTvs d) &&&
   freeNamesIfTvBndrs (ifPatExTvs d) &&&
   freeNamesIfContext (ifPatProvCtxt d) &&&
   freeNamesIfContext (ifPatReqCtxt d) &&&
-  fnList freeNamesIfType (map snd (ifPatArgs d)) &&&
+  fnList freeNamesIfType (ifPatArgs d) &&&
   freeNamesIfType (ifPatTy d)
 
 freeNamesIfAxBranch :: IfaceAxBranch -> NameSet
diff --git a/compiler/iface/LoadIface.lhs b/compiler/iface/LoadIface.lhs
index d7877943261e7745d79fb434ab6fb325c780aa6a..dfcad9631554d06dd75c669c7578148abe52ae77 100644
--- a/compiler/iface/LoadIface.lhs
+++ b/compiler/iface/LoadIface.lhs
@@ -416,7 +416,6 @@ loadDecl ignore_prags mod (_version, decl)
   = do  {       -- Populate the name cache with final versions of all 
                 -- the names associated with the decl
           main_name      <- lookupOrig mod (ifName decl)
---        ; traceIf (text "Loading decl for " <> ppr main_name)
 
         -- Typecheck the thing, lazily
         -- NB. Firstly, the laziness is there in case we never need the
@@ -490,6 +489,8 @@ loadDecl ignore_prags mod (_version, decl)
                              pprPanic "loadDecl" (ppr main_name <+> ppr n $$ ppr (decl))
 
         ; implicit_names <- mapM (lookupOrig mod) (ifaceDeclImplicitBndrs decl)
+
+--         ; traceIf (text "Loading decl for " <> ppr main_name $$ ppr implicit_names)
         ; return $ (main_name, thing) :
                       -- uses the invariant that implicit_names and
                       -- implictTyThings are bijective
diff --git a/compiler/iface/MkIface.lhs b/compiler/iface/MkIface.lhs
index 8b004cf6801b2be357e212e7fb0f0f6a9b7b9647..c3f9b497f2ecebb53e1537836207c651e26ce612 100644
--- a/compiler/iface/MkIface.lhs
+++ b/compiler/iface/MkIface.lhs
@@ -1488,25 +1488,26 @@ dataConToIfaceDecl dataCon
 patSynToIfaceDecl :: PatSyn -> IfaceDecl
 patSynToIfaceDecl ps
   = IfacePatSyn { ifName          = getOccName . getName $ ps
-                , ifPatHasWrapper = isJust $ patSynWrapper ps
+                , ifPatMatcher    = matcher
+                , ifPatWrapper    = wrapper
                 , ifPatIsInfix    = patSynIsInfix ps
                 , ifPatUnivTvs    = toIfaceTvBndrs univ_tvs'
                 , ifPatExTvs      = toIfaceTvBndrs ex_tvs'
                 , ifPatProvCtxt   = tidyToIfaceContext env2 prov_theta
                 , ifPatReqCtxt    = tidyToIfaceContext env2 req_theta
-                , ifPatArgs       = map toIfaceArg args
+                , ifPatArgs       = map (tidyToIfaceType env2) args
                 , ifPatTy         = tidyToIfaceType env2 rhs_ty
                 }
   where
-    toIfaceArg var = (occNameFS (getOccName var),
-                      tidyToIfaceType env2 (varType var))
-
-    (univ_tvs, ex_tvs, (prov_theta, req_theta)) = patSynSig ps
+    (univ_tvs, ex_tvs, prov_theta, req_theta) = patSynSig ps
     args = patSynArgs ps
     rhs_ty = patSynType ps
     (env1, univ_tvs') = tidyTyVarBndrs emptyTidyEnv univ_tvs
     (env2, ex_tvs')   = tidyTyVarBndrs env1 ex_tvs
 
+    matcher = idName (patSynMatcher ps)
+    wrapper = fmap idName (patSynWrapper ps)
+
 
 --------------------------
 coAxiomToIfaceDecl :: CoAxiom br -> IfaceDecl
diff --git a/compiler/iface/TcIface.lhs b/compiler/iface/TcIface.lhs
index 20adfe5896bed00e5026e5d473c6549ffac43e27..398ae4e6123bd51cfc5e20ad95b10d65f358e339 100644
--- a/compiler/iface/TcIface.lhs
+++ b/compiler/iface/TcIface.lhs
@@ -584,7 +584,8 @@ tc_iface_decl _ _ (IfaceAxiom { ifName = ax_occ, ifTyCon = tc
        ; return (ACoAxiom axiom) }
 
 tc_iface_decl _ _ (IfacePatSyn{ ifName = occ_name
-                              , ifPatHasWrapper = has_wrapper
+                              , ifPatMatcher = matcher_name
+                              , ifPatWrapper = wrapper_name
                               , ifPatIsInfix = is_infix
                               , ifPatUnivTvs = univ_tvs
                               , ifPatExTvs = ex_tvs
@@ -594,20 +595,24 @@ tc_iface_decl _ _ (IfacePatSyn{ ifName = occ_name
                               , ifPatTy = pat_ty })
   = do { name <- lookupIfaceTop occ_name
        ; traceIf (ptext (sLit "tc_iface_decl") <+> ppr name)
+       ; matcher <- tcExt "Matcher" matcher_name
+       ; wrapper <- case wrapper_name of
+                        Nothing -> return Nothing
+                        Just wn -> do { wid <- tcExt "Wrapper" wn
+                                      ; return (Just wid) }
        ; bindIfaceTyVars univ_tvs $ \univ_tvs -> do
        { bindIfaceTyVars ex_tvs $ \ex_tvs -> do
-       { bindIfaceIdVars args $ \args -> do
-       { ~(prov_theta, req_theta, pat_ty) <- forkM (mk_doc name) $
+       { patsyn <- forkM (mk_doc name) $
              do { prov_theta <- tcIfaceCtxt prov_ctxt
                 ; req_theta  <- tcIfaceCtxt req_ctxt
                 ; pat_ty     <- tcIfaceType pat_ty
-                ; return (prov_theta, req_theta, pat_ty) }
-       ; bindIfaceTyVar (fsLit "r", toIfaceKind liftedTypeKind) $ \tv -> do
-       { patsyn <- buildPatSyn name is_infix has_wrapper args univ_tvs ex_tvs prov_theta req_theta pat_ty tv
-       ; return (AConLike (PatSynCon patsyn)) }}}}}
+                ; arg_tys    <- mapM tcIfaceType args
+                ; return $ buildPatSyn name is_infix matcher wrapper
+                                       arg_tys univ_tvs ex_tvs prov_theta req_theta pat_ty }
+       ; return $ AConLike . PatSynCon $ patsyn }}}
   where
      mk_doc n = ptext (sLit "Pattern synonym") <+> ppr n
-
+     tcExt s name = forkM (ptext (sLit s) <+> ppr name) $ tcIfaceExtId name
 
 tc_ax_branches :: TyCon -> [IfaceAxBranch] -> IfL [CoAxBranch]
 tc_ax_branches tc if_branches = foldlM (tc_ax_branch (tyConKind tc)) [] if_branches
@@ -1548,20 +1553,6 @@ bindIfaceTyVars bndrs thing_inside
   where
     (occs,kinds) = unzip bndrs
 
-bindIfaceIdVar :: IfaceIdBndr -> (Id -> IfL a) -> IfL a
-bindIfaceIdVar (occ, ty) thing_inside
-  = do  { name <- newIfaceName (mkVarOccFS occ)
-        ; ty' <- tcIfaceType ty
-        ; let id = mkLocalId name ty'
-        ; extendIfaceIdEnv [id] (thing_inside id) }
-
-bindIfaceIdVars :: [IfaceIdBndr] -> ([Id] -> IfL a) -> IfL a
-bindIfaceIdVars []     thing_inside = thing_inside []
-bindIfaceIdVars (v:vs) thing_inside
-  = bindIfaceIdVar v     $ \ v' ->
-    bindIfaceIdVars vs   $ \ vs' ->
-    thing_inside (v':vs')
-
 isSuperIfaceKind :: IfaceKind -> Bool
 isSuperIfaceKind (IfaceTyConApp (IfaceTc n) []) = n == superKindTyConName
 isSuperIfaceKind _ = False
diff --git a/compiler/main/HscTypes.lhs b/compiler/main/HscTypes.lhs
index 6fcf8e24a7245e2f4adcc89e2ecc4ff876d8b6b2..58d0c584eb24b589b988c80337e700a83426a58d 100644
--- a/compiler/main/HscTypes.lhs
+++ b/compiler/main/HscTypes.lhs
@@ -1504,15 +1504,17 @@ implicitTyThings :: TyThing -> [TyThing]
 implicitTyThings (AnId _)       = []
 implicitTyThings (ACoAxiom _cc) = []
 implicitTyThings (ATyCon tc)    = implicitTyConThings tc
-implicitTyThings (AConLike cl)  = case cl of
-    RealDataCon dc ->
-        -- For data cons add the worker and (possibly) wrapper
-        map AnId (dataConImplicitIds dc)
-    PatSynCon ps ->
-        -- For bidirectional pattern synonyms, add the wrapper
-        case patSynWrapper ps of
-            Nothing -> []
-            Just id -> [AnId id]
+implicitTyThings (AConLike cl)  = implicitConLikeThings cl
+
+implicitConLikeThings :: ConLike -> [TyThing]
+implicitConLikeThings (RealDataCon dc)
+  = map AnId (dataConImplicitIds dc)
+    -- For data cons add the worker and (possibly) wrapper
+
+implicitConLikeThings (PatSynCon {})
+  = []  -- Pattern synonyms have no implicit Ids; the wrapper and matcher
+        -- are not "implicit"; they are simply new top-level bindings,
+        -- and they have their own declaration in an interface fiel
 
 implicitClassThings :: Class -> [TyThing]
 implicitClassThings cl
diff --git a/compiler/main/TidyPgm.lhs b/compiler/main/TidyPgm.lhs
index 7ab6d569bcd039daae4c4b28d215ffeaef2eb94f..858281a20b1471c459d89f88b0838ed76bc60169 100644
--- a/compiler/main/TidyPgm.lhs
+++ b/compiler/main/TidyPgm.lhs
@@ -559,7 +559,7 @@ Oh: two other reasons for injecting them late:
 There is one sort of implicit binding that is injected still later,
 namely those for data constructor workers. Reason (I think): it's
 really just a code generation trick.... binding itself makes no sense.
-See CorePrep Note [Data constructor workers].
+See Note [Data constructor workers] in CorePrep.
 
 \begin{code}
 getTyConImplicitBinds :: TyCon -> [CoreBind]
diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs
index 3c5ea84a75c7d3fd557024e3ac4c05d83bbac39f..ca2aa06e430d8d98810f5386dc2824503f605a53 100644
--- a/compiler/typecheck/TcPat.lhs
+++ b/compiler/typecheck/TcPat.lhs
@@ -789,8 +789,8 @@ tcPatSynPat :: PatEnv -> Located Name -> PatSyn
 	    -> HsConPatDetails Name -> TcM a
 	    -> TcM (Pat TcId, a)
 tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
-  = do	{ let (univ_tvs, ex_tvs, (prov_theta, req_theta)) = patSynSig pat_syn
-              arg_tys = patSynArgTys pat_syn
+  = do	{ let (univ_tvs, ex_tvs, prov_theta, req_theta) = patSynSig pat_syn
+              arg_tys = patSynArgs pat_syn
               ty = patSynType pat_syn
 
         ; (_univ_tvs', inst_tys, subst) <- tcInstTyVars univ_tvs
diff --git a/compiler/typecheck/TcPatSyn.lhs b/compiler/typecheck/TcPatSyn.lhs
index 0b3b4e4858215ea34ef12786be1d8cc07b1b3db8..e8ba56398a48d0a1ad076157413953ddbb4cdb87 100644
--- a/compiler/typecheck/TcPatSyn.lhs
+++ b/compiler/typecheck/TcPatSyn.lhs
@@ -31,31 +31,11 @@ import Data.Monoid
 import Bag
 import TcEvidence
 import BuildTyCl
+import TypeRep
 
 #include "HsVersions.h"
 \end{code}
 
-Note [Pattern synonym typechecking]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-Consider the following pattern synonym declaration
-
-        pattern P x = MkT [x] (Just 42)
-
-where
-        data T a where
-              MkT :: (Show a, Ord b) => [b] -> a -> T a
-
-The pattern synonym's type is described with five axes, given here for
-the above example:
-
-  Pattern type: T (Maybe t)
-  Arguments: [x :: b]
-  Universal type variables: [t]
-  Required theta: (Eq t, Num t)
-  Existential type variables: [b]
-  Provided theta: (Show (Maybe t), Ord b)
-
 \begin{code}
 tcPatSynDecl :: Located Name
              -> HsPatSynDetails (Located Name)
@@ -118,7 +98,7 @@ tcPatSynDecl lname@(L _ name) details lpat dir
 
        ; traceTc "tcPatSynDecl }" $ ppr name
        ; let patSyn = mkPatSyn name is_infix
-                        args
+                        (map varType args)
                         univ_tvs ex_tvs
                         prov_theta req_theta
                         pat_ty
@@ -127,40 +107,6 @@ tcPatSynDecl lname@(L _ name) details lpat dir
 
 \end{code}
 
-Note [Matchers and wrappers for pattern synonyms]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-For each pattern synonym, we generate a single matcher function which
-implements the actual matching. For the above example, the matcher
-will have type:
-
-        $mP :: forall r t. (Eq t, Num t)
-            => T (Maybe t)
-            -> (forall b. (Show (Maybe t), Ord b) => b -> r)
-            -> r
-            -> r
-
-with the following implementation:
-
-        $mP @r @t $dEq $dNum scrut cont fail = case scrut of
-            MkT @b $dShow $dOrd [x] (Just 42) -> cont @b $dShow $dOrd x
-            _                                 -> fail
-
-For bidirectional pattern synonyms, we also generate a single wrapper
-function which implements the pattern synonym in an expression
-context. For our running example, it will be:
-
-        $WP :: forall t b. (Show (Maybe t), Ord b, Eq t, Num t)
-            => b -> T (Maybe t)
-        $WP x = MkT [x] (Just 42)
-
-N.b. the existential/universal and required/provided split does not
-apply to the wrapper since you are only putting stuff in, not getting
-stuff out.
-
-Injectivity of bidirectional pattern synonyms is checked in
-tcPatToExpr which walks the pattern and returns its corresponding
-expression when available.
 
 \begin{code}
 tcPatSynMatcher :: Located Name
@@ -172,12 +118,18 @@ tcPatSynMatcher :: Located Name
                 -> ThetaType -> ThetaType
                 -> TcType
                 -> TcM (Id, LHsBinds Id)
+-- See Note [Matchers and wrappers for pattern synonyms] in PatSyn
 tcPatSynMatcher (L loc name) lpat args univ_tvs ex_tvs ev_binds prov_dicts req_dicts prov_theta req_theta pat_ty
   = do { res_tv <- zonkQuantifiedTyVar =<< newFlexiTyVar liftedTypeKind
-       ; (matcher_id, res_ty, cont_ty) <- mkPatSynMatcherId name args
-                                            univ_tvs ex_tvs
-                                            prov_theta req_theta
-                                            pat_ty res_tv
+       ; matcher_name <- newImplicitBinder name mkMatcherOcc
+       ; let res_ty = TyVarTy res_tv
+             cont_ty = mkSigmaTy ex_tvs prov_theta $
+                       mkFunTys (map varType args) res_ty
+
+       ; let matcher_tau = mkFunTys [pat_ty, cont_ty, res_ty] res_ty
+             matcher_sigma = mkSigmaTy (res_tv:univ_tvs) req_theta matcher_tau
+             matcher_id = mkVanillaGlobal matcher_name matcher_sigma
+
        ; traceTc "tcPatSynMatcher" (ppr name $$ ppr (idType matcher_id))
        ; let matcher_lid = L loc matcher_id
 
@@ -241,6 +193,7 @@ tcPatSynWrapper :: Located Name
                 -> ThetaType
                 -> TcType
                 -> TcM (Maybe (Id, LHsBinds Id))
+-- See Note [Matchers and wrappers for pattern synonyms] in PatSyn
 tcPatSynWrapper lname lpat dir args univ_tvs ex_tvs theta pat_ty
   = do { let argNames = mkNameSet (map Var.varName args)
        ; case (dir, tcPatToExpr argNames lpat) of
@@ -260,18 +213,16 @@ tc_pat_syn_wrapper_from_expr :: Located Name
                              -> TcM (Id, LHsBinds Id)
 tc_pat_syn_wrapper_from_expr (L loc name) lexpr args univ_tvs ex_tvs theta pat_ty
   = do { let qtvs = univ_tvs ++ ex_tvs
-       ; (subst, qtvs') <- tcInstSkolTyVars qtvs
-       ; let theta' = substTheta subst theta
+       ; (subst, wrapper_tvs) <- tcInstSkolTyVars qtvs
+       ; let wrapper_theta = substTheta subst theta
              pat_ty' = substTy subst pat_ty
              args' = map (\arg -> setVarType arg $ substTy subst (varType arg)) args
-
-       ; wrapper_id <- mkPatSynWrapperId name args qtvs theta pat_ty
-       ; let wrapper_name = getName wrapper_id
-             wrapper_lname = L loc wrapper_name
-             -- (wrapper_tvs, wrapper_theta, wrapper_tau) = tcSplitSigmaTy (idType wrapper_id)
-             wrapper_tvs = qtvs'
-             wrapper_theta = theta'
              wrapper_tau = mkFunTys (map varType args') pat_ty'
+             wrapper_sigma = mkSigmaTy wrapper_tvs wrapper_theta wrapper_tau
+
+       ; wrapper_name <- newImplicitBinder name mkDataConWrapperOcc
+       ; let wrapper_lname = L loc wrapper_name
+             wrapper_id = mkVanillaGlobal wrapper_name wrapper_sigma
 
        ; let wrapper_args = map (noLoc . VarPat . Var.varName) args'
              wrapper_match = mkMatch wrapper_args lexpr EmptyLocalBinds