Modules: type-checker (#13009)

Update Haddock submodule

7 files changed, 5396 insertions, 0 deletions

diff --git a/compiler/GHC/Tc/TyCl/Build.hs b/compiler/GHC/Tc/TyCl/Build.hs
new file mode 100644
index 0000000000..a118630fda
--- /dev/null
+++ b/compiler/GHC/Tc/TyCl/Build.hs
@@ -0,0 +1,418 @@
+{-
+(c) The University of Glasgow 2006
+(c) The GRASP/AQUA Project, Glasgow University, 1992-1998
+-}
+
+{-# LANGUAGE CPP #-}
+
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
+
+module GHC.Tc.TyCl.Build (
+        buildDataCon,
+        buildPatSyn,
+        TcMethInfo, MethInfo, buildClass,
+        mkNewTyConRhs,
+        newImplicitBinder, newTyConRepName
+    ) where
+
+#include "HsVersions.h"
+
+import GhcPrelude
+
+import GHC.Iface.Env
+import GHC.Core.FamInstEnv( FamInstEnvs, mkNewTypeCoAxiom )
+import TysWiredIn( isCTupleTyConName )
+import TysPrim ( voidPrimTy )
+import GHC.Core.DataCon
+import GHC.Core.PatSyn
+import GHC.Types.Var
+import GHC.Types.Var.Set
+import GHC.Types.Basic
+import GHC.Types.Name
+import GHC.Types.Name.Env
+import GHC.Types.Id.Make
+import GHC.Core.Class
+import GHC.Core.TyCon
+import GHC.Core.Type
+import GHC.Types.Id
+import GHC.Tc.Utils.TcType
+
+import GHC.Types.SrcLoc( SrcSpan, noSrcSpan )
+import GHC.Driver.Session
+import GHC.Tc.Utils.Monad
+import GHC.Types.Unique.Supply
+import Util
+import Outputable
+
+
+mkNewTyConRhs :: Name -> TyCon -> DataCon -> TcRnIf m n AlgTyConRhs
+-- ^ Monadic because it makes a Name for the coercion TyCon
+--   We pass the Name of the parent TyCon, as well as the TyCon itself,
+--   because the latter is part of a knot, whereas the former is not.
+mkNewTyConRhs tycon_name tycon con
+  = do  { co_tycon_name <- newImplicitBinder tycon_name mkNewTyCoOcc
+        ; let nt_ax = mkNewTypeCoAxiom co_tycon_name tycon etad_tvs etad_roles etad_rhs
+        ; traceIf (text "mkNewTyConRhs" <+> ppr nt_ax)
+        ; return (NewTyCon { data_con    = con,
+                             nt_rhs      = rhs_ty,
+                             nt_etad_rhs = (etad_tvs, etad_rhs),
+                             nt_co       = nt_ax,
+                             nt_lev_poly = isKindLevPoly res_kind } ) }
+                             -- Coreview looks through newtypes with a Nothing
+                             -- for nt_co, or uses explicit coercions otherwise
+  where
+    tvs      = tyConTyVars tycon
+    roles    = tyConRoles tycon
+    res_kind = tyConResKind tycon
+    con_arg_ty = case dataConRepArgTys con of
+                   [arg_ty] -> arg_ty
+                   tys -> pprPanic "mkNewTyConRhs" (ppr con <+> ppr tys)
+    rhs_ty = substTyWith (dataConUnivTyVars con)
+                         (mkTyVarTys tvs) con_arg_ty
+        -- Instantiate the newtype's RHS with the
+        -- type variables from the tycon
+        -- NB: a newtype DataCon has a type that must look like
+        --        forall tvs.  <arg-ty> -> T tvs
+        -- Note that we *can't* use dataConInstOrigArgTys here because
+        -- the newtype arising from   class Foo a => Bar a where {}
+        -- has a single argument (Foo a) that is a *type class*, so
+        -- dataConInstOrigArgTys returns [].
+
+    etad_tvs   :: [TyVar]  -- Matched lazily, so that mkNewTypeCo can
+    etad_roles :: [Role]   -- return a TyCon without pulling on rhs_ty
+    etad_rhs   :: Type     -- See Note [Tricky iface loop] in GHC.Iface.Load
+    (etad_tvs, etad_roles, etad_rhs) = eta_reduce (reverse tvs) (reverse roles) rhs_ty
+
+    eta_reduce :: [TyVar]       -- Reversed
+               -> [Role]        -- also reversed
+               -> Type          -- Rhs type
+               -> ([TyVar], [Role], Type)  -- Eta-reduced version
+                                           -- (tyvars in normal order)
+    eta_reduce (a:as) (_:rs) ty | Just (fun, arg) <- splitAppTy_maybe ty,
+                                  Just tv <- getTyVar_maybe arg,
+                                  tv == a,
+                                  not (a `elemVarSet` tyCoVarsOfType fun)
+                                = eta_reduce as rs fun
+    eta_reduce tvs rs ty = (reverse tvs, reverse rs, ty)
+
+------------------------------------------------------
+buildDataCon :: FamInstEnvs
+            -> Name
+            -> Bool                     -- Declared infix
+            -> TyConRepName
+            -> [HsSrcBang]
+            -> Maybe [HsImplBang]
+                -- See Note [Bangs on imported data constructors] in GHC.Types.Id.Make
+           -> [FieldLabel]             -- Field labels
+           -> [TyVar]                  -- Universals
+           -> [TyCoVar]                -- Existentials
+           -> [TyVarBinder]            -- User-written 'TyVarBinder's
+           -> [EqSpec]                 -- Equality spec
+           -> KnotTied ThetaType       -- Does not include the "stupid theta"
+                                       -- or the GADT equalities
+           -> [KnotTied Type]          -- Arguments
+           -> KnotTied Type            -- Result types
+           -> KnotTied TyCon           -- Rep tycon
+           -> NameEnv ConTag           -- Maps the Name of each DataCon to its
+                                       -- ConTag
+           -> TcRnIf m n DataCon
+-- A wrapper for DataCon.mkDataCon that
+--   a) makes the worker Id
+--   b) makes the wrapper Id if necessary, including
+--      allocating its unique (hence monadic)
+buildDataCon fam_envs src_name declared_infix prom_info src_bangs impl_bangs
+             field_lbls univ_tvs ex_tvs user_tvbs eq_spec ctxt arg_tys res_ty
+             rep_tycon tag_map
+  = do  { wrap_name <- newImplicitBinder src_name mkDataConWrapperOcc
+        ; work_name <- newImplicitBinder src_name mkDataConWorkerOcc
+        -- This last one takes the name of the data constructor in the source
+        -- code, which (for Haskell source anyway) will be in the DataName name
+        -- space, and puts it into the VarName name space
+
+        ; traceIf (text "buildDataCon 1" <+> ppr src_name)
+        ; us <- newUniqueSupply
+        ; dflags <- getDynFlags
+        ; let stupid_ctxt = mkDataConStupidTheta rep_tycon arg_tys univ_tvs
+              tag = lookupNameEnv_NF tag_map src_name
+              -- See Note [Constructor tag allocation], fixes #14657
+              data_con = mkDataCon src_name declared_infix prom_info
+                                   src_bangs field_lbls
+                                   univ_tvs ex_tvs user_tvbs eq_spec ctxt
+                                   arg_tys res_ty NoRRI rep_tycon tag
+                                   stupid_ctxt dc_wrk dc_rep
+              dc_wrk = mkDataConWorkId work_name data_con
+              dc_rep = initUs_ us (mkDataConRep dflags fam_envs wrap_name
+                                                impl_bangs data_con)
+
+        ; traceIf (text "buildDataCon 2" <+> ppr src_name)
+        ; return data_con }
+
+
+-- The stupid context for a data constructor should be limited to
+-- the type variables mentioned in the arg_tys
+-- ToDo: Or functionally dependent on?
+--       This whole stupid theta thing is, well, stupid.
+mkDataConStupidTheta :: TyCon -> [Type] -> [TyVar] -> [PredType]
+mkDataConStupidTheta tycon arg_tys univ_tvs
+  | null stupid_theta = []      -- The common case
+  | otherwise         = filter in_arg_tys stupid_theta
+  where
+    tc_subst     = zipTvSubst (tyConTyVars tycon)
+                              (mkTyVarTys univ_tvs)
+    stupid_theta = substTheta tc_subst (tyConStupidTheta tycon)
+        -- Start by instantiating the master copy of the
+        -- stupid theta, taken from the TyCon
+
+    arg_tyvars      = tyCoVarsOfTypes arg_tys
+    in_arg_tys pred = not $ isEmptyVarSet $
+                      tyCoVarsOfType pred `intersectVarSet` arg_tyvars
+
+
+------------------------------------------------------
+buildPatSyn :: Name -> Bool
+            -> (Id,Bool) -> Maybe (Id, Bool)
+            -> ([TyVarBinder], ThetaType) -- ^ Univ and req
+            -> ([TyVarBinder], ThetaType) -- ^ Ex and prov
+            -> [Type]               -- ^ Argument types
+            -> Type                 -- ^ Result type
+            -> [FieldLabel]         -- ^ Field labels for
+                                    --   a record pattern synonym
+            -> PatSyn
+buildPatSyn src_name declared_infix matcher@(matcher_id,_) builder
+            (univ_tvs, req_theta) (ex_tvs, prov_theta) arg_tys
+            pat_ty field_labels
+  = -- The assertion checks that the matcher is
+    -- compatible with the pattern synonym
+    ASSERT2((and [ univ_tvs `equalLength` univ_tvs1
+                 , ex_tvs `equalLength` ex_tvs1
+                 , pat_ty `eqType` substTy subst pat_ty1
+                 , prov_theta `eqTypes` substTys subst prov_theta1
+                 , req_theta `eqTypes` substTys subst req_theta1
+                 , compareArgTys arg_tys (substTys subst arg_tys1)
+                 ])
+            , (vcat [ ppr univ_tvs <+> twiddle <+> ppr univ_tvs1
+                    , ppr ex_tvs <+> twiddle <+> ppr ex_tvs1
+                    , ppr pat_ty <+> twiddle <+> ppr pat_ty1
+                    , ppr prov_theta <+> twiddle <+> ppr prov_theta1
+                    , ppr req_theta <+> twiddle <+> ppr req_theta1
+                    , ppr arg_tys <+> twiddle <+> ppr arg_tys1]))
+    mkPatSyn src_name declared_infix
+             (univ_tvs, req_theta) (ex_tvs, prov_theta)
+             arg_tys pat_ty
+             matcher builder field_labels
+  where
+    ((_:_:univ_tvs1), req_theta1, tau) = tcSplitSigmaTy $ idType matcher_id
+    ([pat_ty1, cont_sigma, _], _)      = tcSplitFunTys tau
+    (ex_tvs1, prov_theta1, cont_tau)   = tcSplitSigmaTy cont_sigma
+    (arg_tys1, _) = (tcSplitFunTys cont_tau)
+    twiddle = char '~'
+    subst = zipTvSubst (univ_tvs1 ++ ex_tvs1)
+                       (mkTyVarTys (binderVars (univ_tvs ++ ex_tvs)))
+
+    -- For a nullary pattern synonym we add a single void argument to the
+    -- matcher to preserve laziness in the case of unlifted types.
+    -- See #12746
+    compareArgTys :: [Type] -> [Type] -> Bool
+    compareArgTys [] [x] = x `eqType` voidPrimTy
+    compareArgTys arg_tys matcher_arg_tys = arg_tys `eqTypes` matcher_arg_tys
+
+
+------------------------------------------------------
+type TcMethInfo = MethInfo  -- this variant needs zonking
+type MethInfo       -- A temporary intermediate, to communicate
+                    -- between tcClassSigs and buildClass.
+  = ( Name   -- Name of the class op
+    , Type   -- Type of the class op
+    , Maybe (DefMethSpec (SrcSpan, Type)))
+         -- Nothing                    => no default method
+         --
+         -- Just VanillaDM             => There is an ordinary
+         --                               polymorphic default method
+         --
+         -- Just (GenericDM (loc, ty)) => There is a generic default metho
+         --                               Here is its type, and the location
+         --                               of the type signature
+         --    We need that location /only/ to attach it to the
+         --    generic default method's Name; and we need /that/
+         --    only to give the right location of an ambiguity error
+         --    for the generic default method, spat out by checkValidClass
+
+buildClass :: Name  -- Name of the class/tycon (they have the same Name)
+           -> [TyConBinder]                -- Of the tycon
+           -> [Role]
+           -> [FunDep TyVar]               -- Functional dependencies
+           -- Super classes, associated types, method info, minimal complete def.
+           -- This is Nothing if the class is abstract.
+           -> Maybe (KnotTied ThetaType, [ClassATItem], [KnotTied MethInfo], ClassMinimalDef)
+           -> TcRnIf m n Class
+
+buildClass tycon_name binders roles fds Nothing
+  = fixM  $ \ rec_clas ->       -- Only name generation inside loop
+    do  { traceIf (text "buildClass")
+
+        ; tc_rep_name  <- newTyConRepName tycon_name
+        ; let univ_tvs = binderVars binders
+              tycon = mkClassTyCon tycon_name binders roles
+                                   AbstractTyCon rec_clas tc_rep_name
+              result = mkAbstractClass tycon_name univ_tvs fds tycon
+        ; traceIf (text "buildClass" <+> ppr tycon)
+        ; return result }
+
+buildClass tycon_name binders roles fds
+           (Just (sc_theta, at_items, sig_stuff, mindef))
+  = fixM  $ \ rec_clas ->       -- Only name generation inside loop
+    do  { traceIf (text "buildClass")
+
+        ; datacon_name <- newImplicitBinder tycon_name mkClassDataConOcc
+        ; tc_rep_name  <- newTyConRepName tycon_name
+
+        ; op_items <- mapM (mk_op_item rec_clas) sig_stuff
+                        -- Build the selector id and default method id
+
+              -- Make selectors for the superclasses
+        ; sc_sel_names <- mapM  (newImplicitBinder tycon_name . mkSuperDictSelOcc)
+                                (takeList sc_theta [fIRST_TAG..])
+        ; let sc_sel_ids = [ mkDictSelId sc_name rec_clas
+                           | sc_name <- sc_sel_names]
+              -- We number off the Dict superclass selectors, 1, 2, 3 etc so that we
+              -- can construct names for the selectors. Thus
+              --      class (C a, C b) => D a b where ...
+              -- gives superclass selectors
+              --      D_sc1, D_sc2
+              -- (We used to call them D_C, but now we can have two different
+              --  superclasses both called C!)
+
+        ; let use_newtype = isSingleton arg_tys
+                -- Use a newtype if the data constructor
+                --   (a) has exactly one value field
+                --       i.e. exactly one operation or superclass taken together
+                --   (b) that value is of lifted type (which they always are, because
+                --       we box equality superclasses)
+                -- See note [Class newtypes and equality predicates]
+
+                -- We treat the dictionary superclasses as ordinary arguments.
+                -- That means that in the case of
+                --     class C a => D a
+                -- we don't get a newtype with no arguments!
+              args       = sc_sel_names ++ op_names
+              op_tys     = [ty | (_,ty,_) <- sig_stuff]
+              op_names   = [op | (op,_,_) <- sig_stuff]
+              arg_tys    = sc_theta ++ op_tys
+              rec_tycon  = classTyCon rec_clas
+              univ_bndrs = tyConTyVarBinders binders
+              univ_tvs   = binderVars univ_bndrs
+
+        ; rep_nm   <- newTyConRepName datacon_name
+        ; dict_con <- buildDataCon (panic "buildClass: FamInstEnvs")
+                                   datacon_name
+                                   False        -- Not declared infix
+                                   rep_nm
+                                   (map (const no_bang) args)
+                                   (Just (map (const HsLazy) args))
+                                   [{- No fields -}]
+                                   univ_tvs
+                                   [{- no existentials -}]
+                                   univ_bndrs
+                                   [{- No GADT equalities -}]
+                                   [{- No theta -}]
+                                   arg_tys
+                                   (mkTyConApp rec_tycon (mkTyVarTys univ_tvs))
+                                   rec_tycon
+                                   (mkTyConTagMap rec_tycon)
+
+        ; rhs <- case () of
+                  _ | use_newtype
+                    -> mkNewTyConRhs tycon_name rec_tycon dict_con
+                    | isCTupleTyConName tycon_name
+                    -> return (TupleTyCon { data_con = dict_con
+                                          , tup_sort = ConstraintTuple })
+                    | otherwise
+                    -> return (mkDataTyConRhs [dict_con])
+
+        ; let { tycon = mkClassTyCon tycon_name binders roles
+                                     rhs rec_clas tc_rep_name
+                -- A class can be recursive, and in the case of newtypes
+                -- this matters.  For example
+                --      class C a where { op :: C b => a -> b -> Int }
+                -- Because C has only one operation, it is represented by
+                -- a newtype, and it should be a *recursive* newtype.
+                -- [If we don't make it a recursive newtype, we'll expand the
+                -- newtype like a synonym, but that will lead to an infinite
+                -- type]
+
+              ; result = mkClass tycon_name univ_tvs fds
+                                 sc_theta sc_sel_ids at_items
+                                 op_items mindef tycon
+              }
+        ; traceIf (text "buildClass" <+> ppr tycon)
+        ; return result }
+  where
+    no_bang = HsSrcBang NoSourceText NoSrcUnpack NoSrcStrict
+
+    mk_op_item :: Class -> TcMethInfo -> TcRnIf n m ClassOpItem
+    mk_op_item rec_clas (op_name, _, dm_spec)
+      = do { dm_info <- mk_dm_info op_name dm_spec
+           ; return (mkDictSelId op_name rec_clas, dm_info) }
+
+    mk_dm_info :: Name -> Maybe (DefMethSpec (SrcSpan, Type))
+               -> TcRnIf n m (Maybe (Name, DefMethSpec Type))
+    mk_dm_info _ Nothing
+      = return Nothing
+    mk_dm_info op_name (Just VanillaDM)
+      = do { dm_name <- newImplicitBinder op_name mkDefaultMethodOcc
+           ; return (Just (dm_name, VanillaDM)) }
+    mk_dm_info op_name (Just (GenericDM (loc, dm_ty)))
+      = do { dm_name <- newImplicitBinderLoc op_name mkDefaultMethodOcc loc
+           ; return (Just (dm_name, GenericDM dm_ty)) }
+
+{-
+Note [Class newtypes and equality predicates]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+        class (a ~ F b) => C a b where
+          op :: a -> b
+
+We cannot represent this by a newtype, even though it's not
+existential, because there are two value fields (the equality
+predicate and op. See #2238
+
+Moreover,
+          class (a ~ F b) => C a b where {}
+Here we can't use a newtype either, even though there is only
+one field, because equality predicates are unboxed, and classes
+are boxed.
+-}
+
+newImplicitBinder :: Name                       -- Base name
+                  -> (OccName -> OccName)       -- Occurrence name modifier
+                  -> TcRnIf m n Name            -- Implicit name
+-- Called in GHC.Tc.TyCl.Build to allocate the implicit binders of type/class decls
+-- For source type/class decls, this is the first occurrence
+-- For iface ones, GHC.Iface.Load has already allocated a suitable name in the cache
+newImplicitBinder base_name mk_sys_occ
+  = newImplicitBinderLoc base_name mk_sys_occ (nameSrcSpan base_name)
+
+newImplicitBinderLoc :: Name                       -- Base name
+                     -> (OccName -> OccName)       -- Occurrence name modifier
+                     -> SrcSpan
+                     -> TcRnIf m n Name            -- Implicit name
+-- Just the same, but lets you specify the SrcSpan
+newImplicitBinderLoc base_name mk_sys_occ loc
+  | Just mod <- nameModule_maybe base_name
+  = newGlobalBinder mod occ loc
+  | otherwise           -- When typechecking a [d| decl bracket |],
+                        -- TH generates types, classes etc with Internal names,
+                        -- so we follow suit for the implicit binders
+  = do  { uniq <- newUnique
+        ; return (mkInternalName uniq occ loc) }
+  where
+    occ = mk_sys_occ (nameOccName base_name)
+
+-- | Make the 'TyConRepName' for this 'TyCon'
+newTyConRepName :: Name -> TcRnIf gbl lcl TyConRepName
+newTyConRepName tc_name
+  | Just mod <- nameModule_maybe tc_name
+  , (mod, occ) <- tyConRepModOcc mod (nameOccName tc_name)
+  = newGlobalBinder mod occ noSrcSpan
+  | otherwise
+  = newImplicitBinder tc_name mkTyConRepOcc
diff --git a/compiler/GHC/Tc/TyCl/Class.hs b/compiler/GHC/Tc/TyCl/Class.hs
new file mode 100644
index 0000000000..55105f84ff
--- /dev/null
+++ b/compiler/GHC/Tc/TyCl/Class.hs
@@ -0,0 +1,554 @@
+{-
+(c) The University of Glasgow 2006
+(c) The GRASP/AQUA Project, Glasgow University, 1992-1998
+
+-}
+
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE TypeFamilies #-}
+
+{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
+
+-- | Typechecking class declarations
+module GHC.Tc.TyCl.Class
+   ( tcClassSigs
+   , tcClassDecl2
+   , findMethodBind
+   , instantiateMethod
+   , tcClassMinimalDef
+   , HsSigFun
+   , mkHsSigFun
+   , badMethodErr
+   , instDeclCtxt1
+   , instDeclCtxt2
+   , instDeclCtxt3
+   , tcATDefault
+   )
+where
+
+#include "HsVersions.h"
+
+import GhcPrelude
+
+import GHC.Hs
+import GHC.Tc.Utils.Env
+import GHC.Tc.Gen.Sig
+import GHC.Tc.Types.Evidence ( idHsWrapper )
+import GHC.Tc.Gen.Bind
+import GHC.Tc.Utils.Unify
+import GHC.Tc.Gen.HsType
+import GHC.Tc.Utils.TcMType
+import GHC.Core.Type     ( piResultTys )
+import GHC.Core.Predicate
+import GHC.Tc.Types.Origin
+import GHC.Tc.Utils.TcType
+import GHC.Tc.Utils.Monad
+import GHC.Driver.Phases (HscSource(..))
+import GHC.Tc.TyCl.Build( TcMethInfo )
+import GHC.Core.Class
+import GHC.Core.Coercion ( pprCoAxiom )
+import GHC.Driver.Session
+import GHC.Tc.Instance.Family
+import GHC.Core.FamInstEnv
+import GHC.Types.Id
+import GHC.Types.Name
+import GHC.Types.Name.Env
+import GHC.Types.Name.Set
+import GHC.Types.Var
+import GHC.Types.Var.Env
+import Outputable
+import GHC.Types.SrcLoc
+import GHC.Core.TyCon
+import Maybes
+import GHC.Types.Basic
+import Bag
+import FastString
+import BooleanFormula
+import Util
+
+import Control.Monad
+import Data.List ( mapAccumL, partition )
+
+{-
+Dictionary handling
+~~~~~~~~~~~~~~~~~~~
+Every class implicitly declares a new data type, corresponding to dictionaries
+of that class. So, for example:
+
+        class (D a) => C a where
+          op1 :: a -> a
+          op2 :: forall b. Ord b => a -> b -> b
+
+would implicitly declare
+
+        data CDict a = CDict (D a)
+                             (a -> a)
+                             (forall b. Ord b => a -> b -> b)
+
+(We could use a record decl, but that means changing more of the existing apparatus.
+One step at a time!)
+
+For classes with just one superclass+method, we use a newtype decl instead:
+
+        class C a where
+          op :: forallb. a -> b -> b
+
+generates
+
+        newtype CDict a = CDict (forall b. a -> b -> b)
+
+Now DictTy in Type is just a form of type synomym:
+        DictTy c t = TyConTy CDict `AppTy` t
+
+Death to "ExpandingDicts".
+
+
+************************************************************************
+*                                                                      *
+                Type-checking the class op signatures
+*                                                                      *
+************************************************************************
+-}
+
+illegalHsigDefaultMethod :: Name -> SDoc
+illegalHsigDefaultMethod n =
+    text "Illegal default method(s) in class definition of" <+> ppr n <+> text "in hsig file"
+
+tcClassSigs :: Name                -- Name of the class
+            -> [LSig GhcRn]
+            -> LHsBinds GhcRn
+            -> TcM [TcMethInfo]    -- Exactly one for each method
+tcClassSigs clas sigs def_methods
+  = do { traceTc "tcClassSigs 1" (ppr clas)
+
+       ; gen_dm_prs <- concatMapM (addLocM tc_gen_sig) gen_sigs
+       ; let gen_dm_env :: NameEnv (SrcSpan, Type)
+             gen_dm_env = mkNameEnv gen_dm_prs
+
+       ; op_info <- concatMapM (addLocM (tc_sig gen_dm_env)) vanilla_sigs
+
+       ; let op_names = mkNameSet [ n | (n,_,_) <- op_info ]
+       ; sequence_ [ failWithTc (badMethodErr clas n)
+                   | n <- dm_bind_names, not (n `elemNameSet` op_names) ]
+                   -- Value binding for non class-method (ie no TypeSig)
+
+       ; tcg_env <- getGblEnv
+       ; if tcg_src tcg_env == HsigFile
+            then
+               -- Error if we have value bindings
+               -- (Generic signatures without value bindings indicate
+               -- that a default of this form is expected to be
+               -- provided.)
+               when (not (null def_methods)) $
+                failWithTc (illegalHsigDefaultMethod clas)
+            else
+               -- Error for each generic signature without value binding
+               sequence_ [ failWithTc (badGenericMethod clas n)
+                         | (n,_) <- gen_dm_prs, not (n `elem` dm_bind_names) ]
+
+       ; traceTc "tcClassSigs 2" (ppr clas)
+       ; return op_info }
+  where
+    vanilla_sigs = [L loc (nm,ty) | L loc (ClassOpSig _ False nm ty) <- sigs]
+    gen_sigs     = [L loc (nm,ty) | L loc (ClassOpSig _ True  nm ty) <- sigs]
+    dm_bind_names :: [Name] -- These ones have a value binding in the class decl
+    dm_bind_names = [op | L _ (FunBind {fun_id = L _ op}) <- bagToList def_methods]
+
+    skol_info = TyConSkol ClassFlavour clas
+
+    tc_sig :: NameEnv (SrcSpan, Type) -> ([Located Name], LHsSigType GhcRn)
+           -> TcM [TcMethInfo]
+    tc_sig gen_dm_env (op_names, op_hs_ty)
+      = do { traceTc "ClsSig 1" (ppr op_names)
+           ; op_ty <- tcClassSigType skol_info op_names op_hs_ty
+                   -- Class tyvars already in scope
+
+           ; traceTc "ClsSig 2" (ppr op_names)
+           ; return [ (op_name, op_ty, f op_name) | L _ op_name <- op_names ] }
+           where
+             f nm | Just lty <- lookupNameEnv gen_dm_env nm = Just (GenericDM lty)
+                  | nm `elem` dm_bind_names                 = Just VanillaDM
+                  | otherwise                               = Nothing
+
+    tc_gen_sig (op_names, gen_hs_ty)
+      = do { gen_op_ty <- tcClassSigType skol_info op_names gen_hs_ty
+           ; return [ (op_name, (loc, gen_op_ty)) | L loc op_name <- op_names ] }
+
+{-
+************************************************************************
+*                                                                      *
+                Class Declarations
+*                                                                      *
+************************************************************************
+-}
+
+tcClassDecl2 :: LTyClDecl GhcRn          -- The class declaration
+             -> TcM (LHsBinds GhcTcId)
+
+tcClassDecl2 (L _ (ClassDecl {tcdLName = class_name, tcdSigs = sigs,
+                                tcdMeths = default_binds}))
+  = recoverM (return emptyLHsBinds)     $
+    setSrcSpan (getLoc class_name)      $
+    do  { clas <- tcLookupLocatedClass class_name
+
+        -- We make a separate binding for each default method.
+        -- At one time I used a single AbsBinds for all of them, thus
+        -- AbsBind [d] [dm1, dm2, dm3] { dm1 = ...; dm2 = ...; dm3 = ... }
+        -- But that desugars into
+        --      ds = \d -> (..., ..., ...)
+        --      dm1 = \d -> case ds d of (a,b,c) -> a
+        -- And since ds is big, it doesn't get inlined, so we don't get good
+        -- default methods.  Better to make separate AbsBinds for each
+        ; let (tyvars, _, _, op_items) = classBigSig clas
+              prag_fn     = mkPragEnv sigs default_binds
+              sig_fn      = mkHsSigFun sigs
+              clas_tyvars = snd (tcSuperSkolTyVars tyvars)
+              pred        = mkClassPred clas (mkTyVarTys clas_tyvars)
+        ; this_dict <- newEvVar pred
+
+        ; let tc_item = tcDefMeth clas clas_tyvars this_dict
+                                  default_binds sig_fn prag_fn
+        ; dm_binds <- tcExtendTyVarEnv clas_tyvars $
+                      mapM tc_item op_items
+
+        ; return (unionManyBags dm_binds) }
+
+tcClassDecl2 d = pprPanic "tcClassDecl2" (ppr d)
+
+tcDefMeth :: Class -> [TyVar] -> EvVar -> LHsBinds GhcRn
+          -> HsSigFun -> TcPragEnv -> ClassOpItem
+          -> TcM (LHsBinds GhcTcId)
+-- Generate code for default methods
+-- This is incompatible with Hugs, which expects a polymorphic
+-- default method for every class op, regardless of whether or not
+-- the programmer supplied an explicit default decl for the class.
+-- (If necessary we can fix that, but we don't have a convenient Id to hand.)
+
+tcDefMeth _ _ _ _ _ prag_fn (sel_id, Nothing)
+  = do { -- No default method
+         mapM_ (addLocM (badDmPrag sel_id))
+               (lookupPragEnv prag_fn (idName sel_id))
+       ; return emptyBag }
+
+tcDefMeth clas tyvars this_dict binds_in hs_sig_fn prag_fn
+          (sel_id, Just (dm_name, dm_spec))
+  | Just (L bind_loc dm_bind, bndr_loc, prags) <- findMethodBind sel_name binds_in prag_fn
+  = do { -- First look up the default method; it should be there!
+         -- It can be the ordinary default method
+         -- or the generic-default method.  E.g of the latter
+         --      class C a where
+         --        op :: a -> a -> Bool
+         --        default op :: Eq a => a -> a -> Bool
+         --        op x y = x==y
+         -- The default method we generate is
+         --    $gm :: (C a, Eq a) => a -> a -> Bool
+         --    $gm x y = x==y
+
+         global_dm_id  <- tcLookupId dm_name
+       ; global_dm_id  <- addInlinePrags global_dm_id prags
+       ; local_dm_name <- newNameAt (getOccName sel_name) bndr_loc
+            -- Base the local_dm_name on the selector name, because
+            -- type errors from tcInstanceMethodBody come from here
+
+       ; spec_prags <- discardConstraints $
+                       tcSpecPrags global_dm_id prags
+       ; warnTc NoReason
+                (not (null spec_prags))
+                (text "Ignoring SPECIALISE pragmas on default method"
+                 <+> quotes (ppr sel_name))
+
+       ; let hs_ty = hs_sig_fn sel_name
+                     `orElse` pprPanic "tc_dm" (ppr sel_name)
+             -- We need the HsType so that we can bring the right
+             -- type variables into scope
+             --
+             -- Eg.   class C a where
+             --          op :: forall b. Eq b => a -> [b] -> a
+             --          gen_op :: a -> a
+             --          generic gen_op :: D a => a -> a
+             -- The "local_dm_ty" is precisely the type in the above
+             -- type signatures, ie with no "forall a. C a =>" prefix
+
+             local_dm_ty = instantiateMethod clas global_dm_id (mkTyVarTys tyvars)
+
+             lm_bind     = dm_bind { fun_id = L bind_loc local_dm_name }
+                             -- Substitute the local_meth_name for the binder
+                             -- NB: the binding is always a FunBind
+
+             warn_redundant = case dm_spec of
+                                GenericDM {} -> True
+                                VanillaDM    -> False
+                -- For GenericDM, warn if the user specifies a signature
+                -- with redundant constraints; but not for VanillaDM, where
+                -- the default method may well be 'error' or something
+
+             ctxt = FunSigCtxt sel_name warn_redundant
+
+       ; let local_dm_id = mkLocalId local_dm_name local_dm_ty
+             local_dm_sig = CompleteSig { sig_bndr = local_dm_id
+                                        , sig_ctxt  = ctxt
+                                        , sig_loc   = getLoc (hsSigType hs_ty) }
+
+       ; (ev_binds, (tc_bind, _))
+               <- checkConstraints skol_info tyvars [this_dict] $
+                  tcPolyCheck no_prag_fn local_dm_sig
+                              (L bind_loc lm_bind)
+
+       ; let export = ABE { abe_ext   = noExtField
+                          , abe_poly  = global_dm_id
+                          , abe_mono  = local_dm_id
+                          , abe_wrap  = idHsWrapper
+                          , abe_prags = IsDefaultMethod }
+             full_bind = AbsBinds { abs_ext      = noExtField
+                                  , abs_tvs      = tyvars
+                                  , abs_ev_vars  = [this_dict]
+                                  , abs_exports  = [export]
+                                  , abs_ev_binds = [ev_binds]
+                                  , abs_binds    = tc_bind
+                                  , abs_sig      = True }
+
+       ; return (unitBag (L bind_loc full_bind)) }
+
+  | otherwise = pprPanic "tcDefMeth" (ppr sel_id)
+  where
+    skol_info = TyConSkol ClassFlavour (getName clas)
+    sel_name = idName sel_id
+    no_prag_fn = emptyPragEnv   -- No pragmas for local_meth_id;
+                                -- they are all for meth_id
+
+---------------
+tcClassMinimalDef :: Name -> [LSig GhcRn] -> [TcMethInfo] -> TcM ClassMinimalDef
+tcClassMinimalDef _clas sigs op_info
+  = case findMinimalDef sigs of
+      Nothing -> return defMindef
+      Just mindef -> do
+        -- Warn if the given mindef does not imply the default one
+        -- That is, the given mindef should at least ensure that the
+        -- class ops without default methods are required, since we
+        -- have no way to fill them in otherwise
+        tcg_env <- getGblEnv
+        -- However, only do this test when it's not an hsig file,
+        -- since you can't write a default implementation.
+        when (tcg_src tcg_env /= HsigFile) $
+            whenIsJust (isUnsatisfied (mindef `impliesAtom`) defMindef) $
+                       (\bf -> addWarnTc NoReason (warningMinimalDefIncomplete bf))
+        return mindef
+  where
+    -- By default require all methods without a default implementation
+    defMindef :: ClassMinimalDef
+    defMindef = mkAnd [ noLoc (mkVar name)
+                      | (name, _, Nothing) <- op_info ]
+
+instantiateMethod :: Class -> TcId -> [TcType] -> TcType
+-- Take a class operation, say
+--      op :: forall ab. C a => forall c. Ix c => (b,c) -> a
+-- Instantiate it at [ty1,ty2]
+-- Return the "local method type":
+--      forall c. Ix x => (ty2,c) -> ty1
+instantiateMethod clas sel_id inst_tys
+  = ASSERT( ok_first_pred ) local_meth_ty
+  where
+    rho_ty = piResultTys (idType sel_id) inst_tys
+    (first_pred, local_meth_ty) = tcSplitPredFunTy_maybe rho_ty
+                `orElse` pprPanic "tcInstanceMethod" (ppr sel_id)
+
+    ok_first_pred = case getClassPredTys_maybe first_pred of
+                      Just (clas1, _tys) -> clas == clas1
+                      Nothing -> False
+              -- The first predicate should be of form (C a b)
+              -- where C is the class in question
+
+
+---------------------------
+type HsSigFun = Name -> Maybe (LHsSigType GhcRn)
+
+mkHsSigFun :: [LSig GhcRn] -> HsSigFun
+mkHsSigFun sigs = lookupNameEnv env
+  where
+    env = mkHsSigEnv get_classop_sig sigs
+
+    get_classop_sig :: LSig GhcRn -> Maybe ([Located Name], LHsSigType GhcRn)
+    get_classop_sig  (L _ (ClassOpSig _ _ ns hs_ty)) = Just (ns, hs_ty)
+    get_classop_sig  _                               = Nothing
+
+---------------------------
+findMethodBind  :: Name                 -- Selector
+                -> LHsBinds GhcRn       -- A group of bindings
+                -> TcPragEnv
+                -> Maybe (LHsBind GhcRn, SrcSpan, [LSig GhcRn])
+                -- Returns the binding, the binding
+                -- site of the method binder, and any inline or
+                -- specialisation pragmas
+findMethodBind sel_name binds prag_fn
+  = foldl' mplus Nothing (mapBag f binds)
+  where
+    prags    = lookupPragEnv prag_fn sel_name
+
+    f bind@(L _ (FunBind { fun_id = L bndr_loc op_name }))
+      | op_name == sel_name
+             = Just (bind, bndr_loc, prags)
+    f _other = Nothing
+
+---------------------------
+findMinimalDef :: [LSig GhcRn] -> Maybe ClassMinimalDef
+findMinimalDef = firstJusts . map toMinimalDef
+  where
+    toMinimalDef :: LSig GhcRn -> Maybe ClassMinimalDef
+    toMinimalDef (L _ (MinimalSig _ _ (L _ bf))) = Just (fmap unLoc bf)
+    toMinimalDef _                               = Nothing
+
+{-
+Note [Polymorphic methods]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+    class Foo a where
+        op :: forall b. Ord b => a -> b -> b -> b
+    instance Foo c => Foo [c] where
+        op = e
+
+When typechecking the binding 'op = e', we'll have a meth_id for op
+whose type is
+      op :: forall c. Foo c => forall b. Ord b => [c] -> b -> b -> b
+
+So tcPolyBinds must be capable of dealing with nested polytypes;
+and so it is. See GHC.Tc.Gen.Bind.tcMonoBinds (with type-sig case).
+
+Note [Silly default-method bind]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we pass the default method binding to the type checker, it must
+look like    op2 = e
+not          $dmop2 = e
+otherwise the "$dm" stuff comes out error messages.  But we want the
+"$dm" to come out in the interface file.  So we typecheck the former,
+and wrap it in a let, thus
+          $dmop2 = let op2 = e in op2
+This makes the error messages right.
+
+
+************************************************************************
+*                                                                      *
+                Error messages
+*                                                                      *
+************************************************************************
+-}
+
+badMethodErr :: Outputable a => a -> Name -> SDoc
+badMethodErr clas op
+  = hsep [text "Class", quotes (ppr clas),
+          text "does not have a method", quotes (ppr op)]
+
+badGenericMethod :: Outputable a => a -> Name -> SDoc
+badGenericMethod clas op
+  = hsep [text "Class", quotes (ppr clas),
+          text "has a generic-default signature without a binding", quotes (ppr op)]
+
+{-
+badGenericInstanceType :: LHsBinds Name -> SDoc
+badGenericInstanceType binds
+  = vcat [text "Illegal type pattern in the generic bindings",
+          nest 2 (ppr binds)]
+
+missingGenericInstances :: [Name] -> SDoc
+missingGenericInstances missing
+  = text "Missing type patterns for" <+> pprQuotedList missing
+
+dupGenericInsts :: [(TyCon, InstInfo a)] -> SDoc
+dupGenericInsts tc_inst_infos
+  = vcat [text "More than one type pattern for a single generic type constructor:",
+          nest 2 (vcat (map ppr_inst_ty tc_inst_infos)),
+          text "All the type patterns for a generic type constructor must be identical"
+    ]
+  where
+    ppr_inst_ty (_,inst) = ppr (simpleInstInfoTy inst)
+-}
+badDmPrag :: TcId -> Sig GhcRn -> TcM ()
+badDmPrag sel_id prag
+  = addErrTc (text "The" <+> hsSigDoc prag <+> ptext (sLit "for default method")
+              <+> quotes (ppr sel_id)
+              <+> text "lacks an accompanying binding")
+
+warningMinimalDefIncomplete :: ClassMinimalDef -> SDoc
+warningMinimalDefIncomplete mindef
+  = vcat [ text "The MINIMAL pragma does not require:"
+         , nest 2 (pprBooleanFormulaNice mindef)
+         , text "but there is no default implementation." ]
+
+instDeclCtxt1 :: LHsSigType GhcRn -> SDoc
+instDeclCtxt1 hs_inst_ty
+  = inst_decl_ctxt (ppr (getLHsInstDeclHead hs_inst_ty))
+
+instDeclCtxt2 :: Type -> SDoc
+instDeclCtxt2 dfun_ty
+  = instDeclCtxt3 cls tys
+  where
+    (_,_,cls,tys) = tcSplitDFunTy dfun_ty
+
+instDeclCtxt3 :: Class -> [Type] -> SDoc
+instDeclCtxt3 cls cls_tys
+  = inst_decl_ctxt (ppr (mkClassPred cls cls_tys))
+
+inst_decl_ctxt :: SDoc -> SDoc
+inst_decl_ctxt doc = hang (text "In the instance declaration for")
+                        2 (quotes doc)
+
+tcATDefault :: SrcSpan
+            -> TCvSubst
+            -> NameSet
+            -> ClassATItem
+            -> TcM [FamInst]
+-- ^ Construct default instances for any associated types that
+-- aren't given a user definition
+-- Returns [] or singleton
+tcATDefault loc inst_subst defined_ats (ATI fam_tc defs)
+  -- User supplied instances ==> everything is OK
+  | tyConName fam_tc `elemNameSet` defined_ats
+  = return []
+
+  -- No user instance, have defaults ==> instantiate them
+   -- Example:   class C a where { type F a b :: *; type F a b = () }
+   --            instance C [x]
+   -- Then we want to generate the decl:   type F [x] b = ()
+  | Just (rhs_ty, _loc) <- defs
+  = do { let (subst', pat_tys') = mapAccumL subst_tv inst_subst
+                                            (tyConTyVars fam_tc)
+             rhs'     = substTyUnchecked subst' rhs_ty
+             tcv' = tyCoVarsOfTypesList pat_tys'
+             (tv', cv') = partition isTyVar tcv'
+             tvs'     = scopedSort tv'
+             cvs'     = scopedSort cv'
+       ; rep_tc_name <- newFamInstTyConName (L loc (tyConName fam_tc)) pat_tys'
+       ; let axiom = mkSingleCoAxiom Nominal rep_tc_name tvs' [] cvs'
+                                     fam_tc pat_tys' rhs'
+           -- NB: no validity check. We check validity of default instances
+           -- in the class definition. Because type instance arguments cannot
+           -- be type family applications and cannot be polytypes, the
+           -- validity check is redundant.
+
+       ; traceTc "mk_deflt_at_instance" (vcat [ ppr fam_tc, ppr rhs_ty
+                                              , pprCoAxiom axiom ])
+       ; fam_inst <- newFamInst SynFamilyInst axiom
+       ; return [fam_inst] }
+
+   -- No defaults ==> generate a warning
+  | otherwise  -- defs = Nothing
+  = do { warnMissingAT (tyConName fam_tc)
+       ; return [] }
+  where
+    subst_tv subst tc_tv
+      | Just ty <- lookupVarEnv (getTvSubstEnv subst) tc_tv
+      = (subst, ty)
+      | otherwise
+      = (extendTvSubst subst tc_tv ty', ty')
+      where
+        ty' = mkTyVarTy (updateTyVarKind (substTyUnchecked subst) tc_tv)
+
+warnMissingAT :: Name -> TcM ()
+warnMissingAT name
+  = do { warn <- woptM Opt_WarnMissingMethods
+       ; traceTc "warn" (ppr name <+> ppr warn)
+       ; hsc_src <- fmap tcg_src getGblEnv
+       -- Warn only if -Wmissing-methods AND not a signature
+       ; warnTc (Reason Opt_WarnMissingMethods) (warn && hsc_src /= HsigFile)
+                (text "No explicit" <+> text "associated type"
+                    <+> text "or default declaration for"
+                    <+> quotes (ppr name)) }
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
new file mode 100644
index 0000000000..84278082e3
--- /dev/null
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -0,0 +1,2179 @@
+{-
+(c) The University of Glasgow 2006
+(c) The GRASP/AQUA Project, Glasgow University, 1992-1998
+
+-}
+
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}
+{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
+
+-- | Typechecking instance declarations
+module GHC.Tc.TyCl.Instance
+   ( tcInstDecls1
+   , tcInstDeclsDeriv
+   , tcInstDecls2
+   )
+where
+
+#include "HsVersions.h"
+
+import GhcPrelude
+
+import GHC.Hs
+import GHC.Tc.Gen.Bind
+import GHC.Tc.TyCl
+import GHC.Tc.TyCl.Utils ( addTyConsToGblEnv )
+import GHC.Tc.TyCl.Class ( tcClassDecl2, tcATDefault,
+                           HsSigFun, mkHsSigFun, badMethodErr,
+                           findMethodBind, instantiateMethod )
+import GHC.Tc.Gen.Sig
+import GHC.Tc.Utils.Monad
+import GHC.Tc.Validity
+import GHC.Tc.Utils.Zonk
+import GHC.Tc.Utils.TcMType
+import GHC.Tc.Utils.TcType
+import GHC.Tc.Types.Constraint
+import GHC.Tc.Types.Origin
+import GHC.Tc.TyCl.Build
+import GHC.Tc.Utils.Instantiate
+import GHC.Tc.Instance.Class( AssocInstInfo(..), isNotAssociated )
+import GHC.Core.InstEnv
+import GHC.Tc.Instance.Family
+import GHC.Core.FamInstEnv
+import GHC.Tc.Deriv
+import GHC.Tc.Utils.Env
+import GHC.Tc.Gen.HsType
+import GHC.Tc.Utils.Unify
+import GHC.Core        ( Expr(..), mkApps, mkVarApps, mkLams )
+import GHC.Core.Make   ( nO_METHOD_BINDING_ERROR_ID )
+import GHC.Core.Unfold ( mkInlineUnfoldingWithArity, mkDFunUnfolding )
+import GHC.Core.Type
+import GHC.Tc.Types.Evidence
+import GHC.Core.TyCon
+import GHC.Core.Coercion.Axiom
+import GHC.Core.DataCon
+import GHC.Core.ConLike
+import GHC.Core.Class
+import GHC.Types.Var as Var
+import GHC.Types.Var.Env
+import GHC.Types.Var.Set
+import Bag
+import GHC.Types.Basic
+import GHC.Driver.Session
+import ErrUtils
+import FastString
+import GHC.Types.Id
+import ListSetOps
+import GHC.Types.Name
+import GHC.Types.Name.Set
+import Outputable
+import GHC.Types.SrcLoc
+import Util
+import BooleanFormula ( isUnsatisfied, pprBooleanFormulaNice )
+import qualified GHC.LanguageExtensions as LangExt
+
+import Control.Monad
+import Maybes
+import Data.List( mapAccumL )
+
+
+{-
+Typechecking instance declarations is done in two passes. The first
+pass, made by @tcInstDecls1@, collects information to be used in the
+second pass.
+
+This pre-processed info includes the as-yet-unprocessed bindings
+inside the instance declaration.  These are type-checked in the second
+pass, when the class-instance envs and GVE contain all the info from
+all the instance and value decls.  Indeed that's the reason we need
+two passes over the instance decls.
+
+
+Note [How instance declarations are translated]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Here is how we translate instance declarations into Core
+
+Running example:
+        class C a where
+           op1, op2 :: Ix b => a -> b -> b
+           op2 = <dm-rhs>
+
+        instance C a => C [a]
+           {-# INLINE [2] op1 #-}
+           op1 = <rhs>
+===>
+        -- Method selectors
+        op1,op2 :: forall a. C a => forall b. Ix b => a -> b -> b
+        op1 = ...
+        op2 = ...
+
+        -- Default methods get the 'self' dictionary as argument
+        -- so they can call other methods at the same type
+        -- Default methods get the same type as their method selector
+        $dmop2 :: forall a. C a => forall b. Ix b => a -> b -> b
+        $dmop2 = /\a. \(d:C a). /\b. \(d2: Ix b). <dm-rhs>
+               -- NB: type variables 'a' and 'b' are *both* in scope in <dm-rhs>
+               -- Note [Tricky type variable scoping]
+
+        -- A top-level definition for each instance method
+        -- Here op1_i, op2_i are the "instance method Ids"
+        -- The INLINE pragma comes from the user pragma
+        {-# INLINE [2] op1_i #-}  -- From the instance decl bindings
+        op1_i, op2_i :: forall a. C a => forall b. Ix b => [a] -> b -> b
+        op1_i = /\a. \(d:C a).
+               let this :: C [a]
+                   this = df_i a d
+                     -- Note [Subtle interaction of recursion and overlap]
+
+                   local_op1 :: forall b. Ix b => [a] -> b -> b
+                   local_op1 = <rhs>
+                     -- Source code; run the type checker on this
+                     -- NB: Type variable 'a' (but not 'b') is in scope in <rhs>
+                     -- Note [Tricky type variable scoping]
+
+               in local_op1 a d
+
+        op2_i = /\a \d:C a. $dmop2 [a] (df_i a d)
+
+        -- The dictionary function itself
+        {-# NOINLINE CONLIKE df_i #-}   -- Never inline dictionary functions
+        df_i :: forall a. C a -> C [a]
+        df_i = /\a. \d:C a. MkC (op1_i a d) (op2_i a d)
+                -- But see Note [Default methods in instances]
+                -- We can't apply the type checker to the default-method call
+
+        -- Use a RULE to short-circuit applications of the class ops
+        {-# RULE "op1@C[a]" forall a, d:C a.
+                            op1 [a] (df_i d) = op1_i a d #-}
+
+Note [Instances and loop breakers]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+* Note that df_i may be mutually recursive with both op1_i and op2_i.
+  It's crucial that df_i is not chosen as the loop breaker, even
+  though op1_i has a (user-specified) INLINE pragma.
+
+* Instead the idea is to inline df_i into op1_i, which may then select
+  methods from the MkC record, and thereby break the recursion with
+  df_i, leaving a *self*-recursive op1_i.  (If op1_i doesn't call op at
+  the same type, it won't mention df_i, so there won't be recursion in
+  the first place.)
+
+* If op1_i is marked INLINE by the user there's a danger that we won't
+  inline df_i in it, and that in turn means that (since it'll be a
+  loop-breaker because df_i isn't), op1_i will ironically never be
+  inlined.  But this is OK: the recursion breaking happens by way of
+  a RULE (the magic ClassOp rule above), and RULES work inside InlineRule
+  unfoldings. See Note [RULEs enabled in InitialPhase] in GHC.Core.Op.Simplify.Utils
+
+Note [ClassOp/DFun selection]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+One thing we see a lot is stuff like
+    op2 (df d1 d2)
+where 'op2' is a ClassOp and 'df' is DFun.  Now, we could inline *both*
+'op2' and 'df' to get
+     case (MkD ($cop1 d1 d2) ($cop2 d1 d2) ... of
+       MkD _ op2 _ _ _ -> op2
+And that will reduce to ($cop2 d1 d2) which is what we wanted.
+
+But it's tricky to make this work in practice, because it requires us to
+inline both 'op2' and 'df'.  But neither is keen to inline without having
+seen the other's result; and it's very easy to get code bloat (from the
+big intermediate) if you inline a bit too much.
+
+Instead we use a cunning trick.
+ * We arrange that 'df' and 'op2' NEVER inline.
+
+ * We arrange that 'df' is ALWAYS defined in the sylised form
+      df d1 d2 = MkD ($cop1 d1 d2) ($cop2 d1 d2) ...
+
+ * We give 'df' a magical unfolding (DFunUnfolding [$cop1, $cop2, ..])
+   that lists its methods.
+
+ * We make GHC.Core.Unfold.exprIsConApp_maybe spot a DFunUnfolding and return
+   a suitable constructor application -- inlining df "on the fly" as it
+   were.
+
+ * ClassOp rules: We give the ClassOp 'op2' a BuiltinRule that
+   extracts the right piece iff its argument satisfies
+   exprIsConApp_maybe.  This is done in GHC.Types.Id.Make.mkDictSelId
+
+ * We make 'df' CONLIKE, so that shared uses still match; eg
+      let d = df d1 d2
+      in ...(op2 d)...(op1 d)...
+
+Note [Single-method classes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If the class has just one method (or, more accurately, just one element
+of {superclasses + methods}), then we use a different strategy.
+
+   class C a where op :: a -> a
+   instance C a => C [a] where op = <blah>
+
+We translate the class decl into a newtype, which just gives a
+top-level axiom. The "constructor" MkC expands to a cast, as does the
+class-op selector.
+
+   axiom Co:C a :: C a ~ (a->a)
+
+   op :: forall a. C a -> (a -> a)
+   op a d = d |> (Co:C a)
+
+   MkC :: forall a. (a->a) -> C a
+   MkC = /\a.\op. op |> (sym Co:C a)
+
+The clever RULE stuff doesn't work now, because ($df a d) isn't
+a constructor application, so exprIsConApp_maybe won't return
+Just <blah>.
+
+Instead, we simply rely on the fact that casts are cheap:
+
+   $df :: forall a. C a => C [a]
+   {-# INLINE df #-}  -- NB: INLINE this
+   $df = /\a. \d. MkC [a] ($cop_list a d)
+       = $cop_list |> forall a. C a -> (sym (Co:C [a]))
+
+   $cop_list :: forall a. C a => [a] -> [a]
+   $cop_list = <blah>
+
+So if we see
+   (op ($df a d))
+we'll inline 'op' and '$df', since both are simply casts, and
+good things happen.
+
+Why do we use this different strategy?  Because otherwise we
+end up with non-inlined dictionaries that look like
+    $df = $cop |> blah
+which adds an extra indirection to every use, which seems stupid.  See
+#4138 for an example (although the regression reported there
+wasn't due to the indirection).
+
+There is an awkward wrinkle though: we want to be very
+careful when we have
+    instance C a => C [a] where
+      {-# INLINE op #-}
+      op = ...
+then we'll get an INLINE pragma on $cop_list but it's important that
+$cop_list only inlines when it's applied to *two* arguments (the
+dictionary and the list argument).  So we must not eta-expand $df
+above.  We ensure that this doesn't happen by putting an INLINE
+pragma on the dfun itself; after all, it ends up being just a cast.
+
+There is one more dark corner to the INLINE story, even more deeply
+buried.  Consider this (#3772):
+
+    class DeepSeq a => C a where
+      gen :: Int -> a
+
+    instance C a => C [a] where
+      gen n = ...
+
+    class DeepSeq a where
+      deepSeq :: a -> b -> b
+
+    instance DeepSeq a => DeepSeq [a] where
+      {-# INLINE deepSeq #-}
+      deepSeq xs b = foldr deepSeq b xs
+
+That gives rise to these defns:
+
+    $cdeepSeq :: DeepSeq a -> [a] -> b -> b
+    -- User INLINE( 3 args )!
+    $cdeepSeq a (d:DS a) b (x:[a]) (y:b) = ...
+
+    $fDeepSeq[] :: DeepSeq a -> DeepSeq [a]
+    -- DFun (with auto INLINE pragma)
+    $fDeepSeq[] a d = $cdeepSeq a d |> blah
+
+    $cp1 a d :: C a => DeepSep [a]
+    -- We don't want to eta-expand this, lest
+    -- $cdeepSeq gets inlined in it!
+    $cp1 a d = $fDeepSep[] a (scsel a d)
+
+    $fC[] :: C a => C [a]
+    -- Ordinary DFun
+    $fC[] a d = MkC ($cp1 a d) ($cgen a d)
+
+Here $cp1 is the code that generates the superclass for C [a].  The
+issue is this: we must not eta-expand $cp1 either, or else $fDeepSeq[]
+and then $cdeepSeq will inline there, which is definitely wrong.  Like
+on the dfun, we solve this by adding an INLINE pragma to $cp1.
+
+Note [Subtle interaction of recursion and overlap]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this
+  class C a where { op1,op2 :: a -> a }
+  instance C a => C [a] where
+    op1 x = op2 x ++ op2 x
+    op2 x = ...
+  instance C [Int] where
+    ...
+
+When type-checking the C [a] instance, we need a C [a] dictionary (for
+the call of op2).  If we look up in the instance environment, we find
+an overlap.  And in *general* the right thing is to complain (see Note
+[Overlapping instances] in GHC.Core.InstEnv).  But in *this* case it's wrong to
+complain, because we just want to delegate to the op2 of this same
+instance.
+
+Why is this justified?  Because we generate a (C [a]) constraint in
+a context in which 'a' cannot be instantiated to anything that matches
+other overlapping instances, or else we would not be executing this
+version of op1 in the first place.
+
+It might even be a bit disguised:
+
+  nullFail :: C [a] => [a] -> [a]
+  nullFail x = op2 x ++ op2 x
+
+  instance C a => C [a] where
+    op1 x = nullFail x
+
+Precisely this is used in package 'regex-base', module Context.hs.
+See the overlapping instances for RegexContext, and the fact that they
+call 'nullFail' just like the example above.  The DoCon package also
+does the same thing; it shows up in module Fraction.hs.
+
+Conclusion: when typechecking the methods in a C [a] instance, we want to
+treat the 'a' as an *existential* type variable, in the sense described
+by Note [Binding when looking up instances].  That is why isOverlappableTyVar
+responds True to an InstSkol, which is the kind of skolem we use in
+tcInstDecl2.
+
+
+Note [Tricky type variable scoping]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In our example
+        class C a where
+           op1, op2 :: Ix b => a -> b -> b
+           op2 = <dm-rhs>
+
+        instance C a => C [a]
+           {-# INLINE [2] op1 #-}
+           op1 = <rhs>
+
+note that 'a' and 'b' are *both* in scope in <dm-rhs>, but only 'a' is
+in scope in <rhs>.  In particular, we must make sure that 'b' is in
+scope when typechecking <dm-rhs>.  This is achieved by subFunTys,
+which brings appropriate tyvars into scope. This happens for both
+<dm-rhs> and for <rhs>, but that doesn't matter: the *renamer* will have
+complained if 'b' is mentioned in <rhs>.
+
+
+
+************************************************************************
+*                                                                      *
+\subsection{Extracting instance decls}
+*                                                                      *
+************************************************************************
+
+Gather up the instance declarations from their various sources
+-}
+
+tcInstDecls1    -- Deal with both source-code and imported instance decls
+   :: [LInstDecl GhcRn]         -- Source code instance decls
+   -> TcM (TcGblEnv,            -- The full inst env
+           [InstInfo GhcRn],    -- Source-code instance decls to process;
+                                -- contains all dfuns for this module
+           [DerivInfo])         -- From data family instances
+
+tcInstDecls1 inst_decls
+  = do {    -- Do class and family instance declarations
+       ; stuff <- mapAndRecoverM tcLocalInstDecl inst_decls
+
+       ; let (local_infos_s, fam_insts_s, datafam_deriv_infos) = unzip3 stuff
+             fam_insts   = concat fam_insts_s
+             local_infos = concat local_infos_s
+
+       ; gbl_env <- addClsInsts local_infos $
+                    addFamInsts fam_insts   $
+                    getGblEnv
+
+       ; return ( gbl_env
+                , local_infos
+                , concat datafam_deriv_infos ) }
+
+-- | Use DerivInfo for data family instances (produced by tcInstDecls1),
+--   datatype declarations (TyClDecl), and standalone deriving declarations
+--   (DerivDecl) to check and process all derived class instances.
+tcInstDeclsDeriv
+  :: [DerivInfo]
+  -> [LDerivDecl GhcRn]
+  -> TcM (TcGblEnv, [InstInfo GhcRn], HsValBinds GhcRn)
+tcInstDeclsDeriv deriv_infos derivds
+  = do th_stage <- getStage -- See Note [Deriving inside TH brackets]
+       if isBrackStage th_stage
+       then do { gbl_env <- getGblEnv
+               ; return (gbl_env, bagToList emptyBag, emptyValBindsOut) }
+       else do { (tcg_env, info_bag, valbinds) <- tcDeriving deriv_infos derivds
+               ; return (tcg_env, bagToList info_bag, valbinds) }
+
+addClsInsts :: [InstInfo GhcRn] -> TcM a -> TcM a
+addClsInsts infos thing_inside
+  = tcExtendLocalInstEnv (map iSpec infos) thing_inside
+
+addFamInsts :: [FamInst] -> TcM a -> TcM a
+-- Extend (a) the family instance envt
+--        (b) the type envt with stuff from data type decls
+addFamInsts fam_insts thing_inside
+  = tcExtendLocalFamInstEnv fam_insts $
+    tcExtendGlobalEnv axioms          $
+    do { traceTc "addFamInsts" (pprFamInsts fam_insts)
+       ; gbl_env <- addTyConsToGblEnv data_rep_tycons
+                    -- Does not add its axiom; that comes
+                    -- from adding the 'axioms' above
+       ; setGblEnv gbl_env thing_inside }
+  where
+    axioms = map (ACoAxiom . toBranchedAxiom . famInstAxiom) fam_insts
+    data_rep_tycons = famInstsRepTyCons fam_insts
+      -- The representation tycons for 'data instances' declarations
+
+{-
+Note [Deriving inside TH brackets]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Given a declaration bracket
+  [d| data T = A | B deriving( Show ) |]
+
+there is really no point in generating the derived code for deriving(
+Show) and then type-checking it. This will happen at the call site
+anyway, and the type check should never fail!  Moreover (#6005)
+the scoping of the generated code inside the bracket does not seem to
+work out.
+
+The easy solution is simply not to generate the derived instances at
+all.  (A less brutal solution would be to generate them with no
+bindings.)  This will become moot when we shift to the new TH plan, so
+the brutal solution will do.
+-}
+
+tcLocalInstDecl :: LInstDecl GhcRn
+                -> TcM ([InstInfo GhcRn], [FamInst], [DerivInfo])
+        -- A source-file instance declaration
+        -- Type-check all the stuff before the "where"
+        --
+        -- We check for respectable instance type, and context
+tcLocalInstDecl (L loc (TyFamInstD { tfid_inst = decl }))
+  = do { fam_inst <- tcTyFamInstDecl NotAssociated (L loc decl)
+       ; return ([], [fam_inst], []) }
+
+tcLocalInstDecl (L loc (DataFamInstD { dfid_inst = decl }))
+  = do { (fam_inst, m_deriv_info) <- tcDataFamInstDecl NotAssociated (L loc decl)
+       ; return ([], [fam_inst], maybeToList m_deriv_info) }
+
+tcLocalInstDecl (L loc (ClsInstD { cid_inst = decl }))
+  = do { (insts, fam_insts, deriv_infos) <- tcClsInstDecl (L loc decl)
+       ; return (insts, fam_insts, deriv_infos) }
+
+tcLocalInstDecl (L _ (XInstDecl nec)) = noExtCon nec
+
+tcClsInstDecl :: LClsInstDecl GhcRn
+              -> TcM ([InstInfo GhcRn], [FamInst], [DerivInfo])
+-- The returned DerivInfos are for any associated data families
+tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = hs_ty, cid_binds = binds
+                                  , cid_sigs = uprags, cid_tyfam_insts = ats
+                                  , cid_overlap_mode = overlap_mode
+                                  , cid_datafam_insts = adts }))
+  = setSrcSpan loc                      $
+    addErrCtxt (instDeclCtxt1 hs_ty)  $
+    do  { dfun_ty <- tcHsClsInstType (InstDeclCtxt False) hs_ty
+        ; let (tyvars, theta, clas, inst_tys) = tcSplitDFunTy dfun_ty
+             -- NB: tcHsClsInstType does checkValidInstance
+
+        ; (subst, skol_tvs) <- tcInstSkolTyVars tyvars
+        ; let tv_skol_prs = [ (tyVarName tv, skol_tv)
+                            | (tv, skol_tv) <- tyvars `zip` skol_tvs ]
+              n_inferred = countWhile ((== Inferred) . binderArgFlag) $
+                           fst $ splitForAllVarBndrs dfun_ty
+              visible_skol_tvs = drop n_inferred skol_tvs
+
+        ; traceTc "tcLocalInstDecl 1" (ppr dfun_ty $$ ppr (invisibleTyBndrCount dfun_ty) $$ ppr skol_tvs)
+
+        -- Next, process any associated types.
+        ; (datafam_stuff, tyfam_insts)
+             <- tcExtendNameTyVarEnv tv_skol_prs $
+                do  { let mini_env   = mkVarEnv (classTyVars clas `zip` substTys subst inst_tys)
+                          mini_subst = mkTvSubst (mkInScopeSet (mkVarSet skol_tvs)) mini_env
+                          mb_info    = InClsInst { ai_class = clas
+                                                 , ai_tyvars = visible_skol_tvs
+                                                 , ai_inst_env = mini_env }
+                    ; df_stuff  <- mapAndRecoverM (tcDataFamInstDecl mb_info) adts
+                    ; tf_insts1 <- mapAndRecoverM (tcTyFamInstDecl mb_info)   ats
+
+                      -- Check for missing associated types and build them
+                      -- from their defaults (if available)
+                    ; tf_insts2 <- mapM (tcATDefault loc mini_subst defined_ats)
+                                        (classATItems clas)
+
+                    ; return (df_stuff, tf_insts1 ++ concat tf_insts2) }
+
+
+        -- Finally, construct the Core representation of the instance.
+        -- (This no longer includes the associated types.)
+        ; dfun_name <- newDFunName clas inst_tys (getLoc (hsSigType hs_ty))
+                -- Dfun location is that of instance *header*
+
+        ; ispec <- newClsInst (fmap unLoc overlap_mode) dfun_name
+                              tyvars theta clas inst_tys
+
+        ; let inst_binds = InstBindings
+                             { ib_binds = binds
+                             , ib_tyvars = map Var.varName tyvars -- Scope over bindings
+                             , ib_pragmas = uprags
+                             , ib_extensions = []
+                             , ib_derived = False }
+              inst_info = InstInfo { iSpec  = ispec, iBinds = inst_binds }
+
+              (datafam_insts, m_deriv_infos) = unzip datafam_stuff
+              deriv_infos                    = catMaybes m_deriv_infos
+              all_insts                      = tyfam_insts ++ datafam_insts
+
+         -- In hs-boot files there should be no bindings
+        ; is_boot <- tcIsHsBootOrSig
+        ; let no_binds = isEmptyLHsBinds binds && null uprags
+        ; failIfTc (is_boot && not no_binds) badBootDeclErr
+
+        ; return ( [inst_info], all_insts, deriv_infos ) }
+  where
+    defined_ats = mkNameSet (map (tyFamInstDeclName . unLoc) ats)
+                  `unionNameSet`
+                  mkNameSet (map (unLoc . feqn_tycon
+                                        . hsib_body
+                                        . dfid_eqn
+                                        . unLoc) adts)
+
+tcClsInstDecl (L _ (XClsInstDecl nec)) = noExtCon nec
+
+{-
+************************************************************************
+*                                                                      *
+               Type family instances
+*                                                                      *
+************************************************************************
+
+Family instances are somewhat of a hybrid.  They are processed together with
+class instance heads, but can contain data constructors and hence they share a
+lot of kinding and type checking code with ordinary algebraic data types (and
+GADTs).
+-}
+
+tcTyFamInstDecl :: AssocInstInfo
+                -> LTyFamInstDecl GhcRn -> TcM FamInst
+  -- "type instance"
+  -- See Note [Associated type instances]
+tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
+  = setSrcSpan loc           $
+    tcAddTyFamInstCtxt decl  $
+    do { let fam_lname = feqn_tycon (hsib_body eqn)
+       ; fam_tc <- tcLookupLocatedTyCon fam_lname
+       ; tcFamInstDeclChecks mb_clsinfo fam_tc
+
+         -- (0) Check it's an open type family
+       ; checkTc (isTypeFamilyTyCon fam_tc)     (wrongKindOfFamily fam_tc)
+       ; checkTc (isOpenTypeFamilyTyCon fam_tc) (notOpenFamily fam_tc)
+
+         -- (1) do the work of verifying the synonym group
+       ; co_ax_branch <- tcTyFamInstEqn fam_tc mb_clsinfo
+                                        (L (getLoc fam_lname) eqn)
+
+
+         -- (2) check for validity
+       ; checkConsistentFamInst mb_clsinfo fam_tc co_ax_branch
+       ; checkValidCoAxBranch fam_tc co_ax_branch
+
+         -- (3) construct coercion axiom
+       ; rep_tc_name <- newFamInstAxiomName fam_lname [coAxBranchLHS co_ax_branch]
+       ; let axiom = mkUnbranchedCoAxiom rep_tc_name fam_tc co_ax_branch
+       ; newFamInst SynFamilyInst axiom }
+
+
+---------------------
+tcFamInstDeclChecks :: AssocInstInfo -> TyCon -> TcM ()
+-- Used for both type and data families
+tcFamInstDeclChecks mb_clsinfo fam_tc
+  = do { -- Type family instances require -XTypeFamilies
+         -- and can't (currently) be in an hs-boot file
+       ; traceTc "tcFamInstDecl" (ppr fam_tc)
+       ; type_families <- xoptM LangExt.TypeFamilies
+       ; is_boot       <- tcIsHsBootOrSig   -- Are we compiling an hs-boot file?
+       ; checkTc type_families $ badFamInstDecl fam_tc
+       ; checkTc (not is_boot) $ badBootFamInstDeclErr
+
+       -- Check that it is a family TyCon, and that
+       -- oplevel type instances are not for associated types.
+       ; checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
+
+       ; when (isNotAssociated mb_clsinfo &&   -- Not in a class decl
+               isTyConAssoc fam_tc)            -- but an associated type
+              (addErr $ assocInClassErr fam_tc)
+       }
+
+{- Note [Associated type instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We allow this:
+  class C a where
+    type T x a
+  instance C Int where
+    type T (S y) Int = y
+    type T Z     Int = Char
+
+Note that
+  a) The variable 'x' is not bound by the class decl
+  b) 'x' is instantiated to a non-type-variable in the instance
+  c) There are several type instance decls for T in the instance
+
+All this is fine.  Of course, you can't give any *more* instances
+for (T ty Int) elsewhere, because it's an *associated* type.
+
+
+************************************************************************
+*                                                                      *
+               Data family instances
+*                                                                      *
+************************************************************************
+
+For some reason data family instances are a lot more complicated
+than type family instances
+-}
+
+tcDataFamInstDecl :: AssocInstInfo
+                  -> LDataFamInstDecl GhcRn -> TcM (FamInst, Maybe DerivInfo)
+  -- "newtype instance" and "data instance"
+tcDataFamInstDecl mb_clsinfo
+    (L loc decl@(DataFamInstDecl { dfid_eqn = HsIB { hsib_ext = imp_vars
+                                                   , hsib_body =
+      FamEqn { feqn_bndrs  = mb_bndrs
+             , feqn_pats   = hs_pats
+             , feqn_tycon  = lfam_name@(L _ fam_name)
+             , feqn_fixity = fixity
+             , feqn_rhs    = HsDataDefn { dd_ND      = new_or_data
+                                        , dd_cType   = cType
+                                        , dd_ctxt    = hs_ctxt
+                                        , dd_cons    = hs_cons
+                                        , dd_kindSig = m_ksig
+                                        , dd_derivs  = derivs } }}}))
+  = setSrcSpan loc             $
+    tcAddDataFamInstCtxt decl  $
+    do { fam_tc <- tcLookupLocatedTyCon lfam_name
+
+       ; tcFamInstDeclChecks mb_clsinfo fam_tc
+
+       -- Check that the family declaration is for the right kind
+       ; checkTc (isDataFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
+       ; gadt_syntax <- dataDeclChecks fam_name new_or_data hs_ctxt hs_cons
+          -- Do /not/ check that the number of patterns = tyConArity fam_tc
+          -- See [Arity of data families] in GHC.Core.FamInstEnv
+       ; (qtvs, pats, res_kind, stupid_theta)
+             <- tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs
+                                    fixity hs_ctxt hs_pats m_ksig hs_cons
+                                    new_or_data
+
+       -- Eta-reduce the axiom if possible
+       -- Quite tricky: see Note [Implementing eta reduction for data families]
+       ; let (eta_pats, eta_tcbs) = eta_reduce fam_tc pats
+             eta_tvs       = map binderVar eta_tcbs
+             post_eta_qtvs = filterOut (`elem` eta_tvs) qtvs
+
+             full_tcbs = mkTyConBindersPreferAnon post_eta_qtvs
+                            (tyCoVarsOfType (mkSpecForAllTys eta_tvs res_kind))
+                         ++ eta_tcbs
+                 -- Put the eta-removed tyvars at the end
+                 -- Remember, qtvs is in arbitrary order, except kind vars are
+                 -- first, so there is no reason to suppose that the eta_tvs
+                 -- (obtained from the pats) are at the end (#11148)
+
+       -- Eta-expand the representation tycon until it has result
+       -- kind `TYPE r`, for some `r`. If UnliftedNewtypes is not enabled, we
+       -- go one step further and ensure that it has kind `TYPE 'LiftedRep`.
+       --
+       -- See also Note [Arity of data families] in GHC.Core.FamInstEnv
+       -- NB: we can do this after eta-reducing the axiom, because if
+       --     we did it before the "extra" tvs from etaExpandAlgTyCon
+       --     would always be eta-reduced
+       --
+       -- See also Note [Datatype return kinds] in GHC.Tc.TyCl
+       ; (extra_tcbs, final_res_kind) <- etaExpandAlgTyCon full_tcbs res_kind
+       ; checkDataKindSig (DataInstanceSort new_or_data) final_res_kind
+       ; let extra_pats  = map (mkTyVarTy . binderVar) extra_tcbs
+             all_pats    = pats `chkAppend` extra_pats
+             orig_res_ty = mkTyConApp fam_tc all_pats
+             ty_binders  = full_tcbs `chkAppend` extra_tcbs
+
+       ; traceTc "tcDataFamInstDecl" $
+         vcat [ text "Fam tycon:" <+> ppr fam_tc
+              , text "Pats:" <+> ppr pats
+              , text "visibliities:" <+> ppr (tcbVisibilities fam_tc pats)
+              , text "all_pats:" <+> ppr all_pats
+              , text "ty_binders" <+> ppr ty_binders
+              , text "fam_tc_binders:" <+> ppr (tyConBinders fam_tc)
+              , text "eta_pats" <+> ppr eta_pats
+              , text "eta_tcbs" <+> ppr eta_tcbs ]
+
+       ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) ->
+           do { data_cons <- tcExtendTyVarEnv qtvs $
+                  -- For H98 decls, the tyvars scope
+                  -- over the data constructors
+                  tcConDecls rec_rep_tc new_or_data ty_binders final_res_kind
+                             orig_res_ty hs_cons
+
+              ; rep_tc_name <- newFamInstTyConName lfam_name pats
+              ; axiom_name  <- newFamInstAxiomName lfam_name [pats]
+              ; tc_rhs <- case new_or_data of
+                     DataType -> return (mkDataTyConRhs data_cons)
+                     NewType  -> ASSERT( not (null data_cons) )
+                                 mkNewTyConRhs rep_tc_name rec_rep_tc (head data_cons)
+
+              ; let axiom  = mkSingleCoAxiom Representational axiom_name
+                                 post_eta_qtvs eta_tvs [] fam_tc eta_pats
+                                 (mkTyConApp rep_tc (mkTyVarTys post_eta_qtvs))
+                    parent = DataFamInstTyCon axiom fam_tc all_pats
+
+                      -- NB: Use the full ty_binders from the pats. See bullet toward
+                      -- the end of Note [Data type families] in GHC.Core.TyCon
+                    rep_tc   = mkAlgTyCon rep_tc_name
+                                          ty_binders final_res_kind
+                                          (map (const Nominal) ty_binders)
+                                          (fmap unLoc cType) stupid_theta
+                                          tc_rhs parent
+                                          gadt_syntax
+                 -- We always assume that indexed types are recursive.  Why?
+                 -- (1) Due to their open nature, we can never be sure that a
+                 -- further instance might not introduce a new recursive
+                 -- dependency.  (2) They are always valid loop breakers as
+                 -- they involve a coercion.
+              ; return (rep_tc, axiom) }
+
+       -- Remember to check validity; no recursion to worry about here
+       -- Check that left-hand sides are ok (mono-types, no type families,
+       -- consistent instantiations, etc)
+       ; let ax_branch = coAxiomSingleBranch axiom
+       ; checkConsistentFamInst mb_clsinfo fam_tc ax_branch
+       ; checkValidCoAxBranch fam_tc ax_branch
+       ; checkValidTyCon rep_tc
+
+       ; let m_deriv_info = case derivs of
+               L _ []    -> Nothing
+               L _ preds ->
+                 Just $ DerivInfo { di_rep_tc  = rep_tc
+                                  , di_scoped_tvs = mkTyVarNamePairs (tyConTyVars rep_tc)
+                                  , di_clauses = preds
+                                  , di_ctxt    = tcMkDataFamInstCtxt decl }
+
+       ; fam_inst <- newFamInst (DataFamilyInst rep_tc) axiom
+       ; return (fam_inst, m_deriv_info) }
+  where
+    eta_reduce :: TyCon -> [Type] -> ([Type], [TyConBinder])
+    -- See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom
+    -- Splits the incoming patterns into two: the [TyVar]
+    -- are the patterns that can be eta-reduced away.
+    -- e.g.     T [a] Int a d c   ==>  (T [a] Int a, [d,c])
+    --
+    -- NB: quadratic algorithm, but types are small here
+    eta_reduce fam_tc pats
+        = go (reverse (zip3 pats fvs_s vis_s)) []
+        where
+          vis_s :: [TyConBndrVis]
+          vis_s = tcbVisibilities fam_tc pats
+
+          fvs_s :: [TyCoVarSet]  -- 1-1 correspondence with pats
+                                 -- Each elt is the free vars of all /earlier/ pats
+          (_, fvs_s) = mapAccumL add_fvs emptyVarSet pats
+          add_fvs fvs pat = (fvs `unionVarSet` tyCoVarsOfType pat, fvs)
+
+    go ((pat, fvs_to_the_left, tcb_vis):pats) etad_tvs
+      | Just tv <- getTyVar_maybe pat
+      , not (tv `elemVarSet` fvs_to_the_left)
+      = go pats (Bndr tv tcb_vis : etad_tvs)
+    go pats etad_tvs = (reverse (map fstOf3 pats), etad_tvs)
+
+tcDataFamInstDecl _ _ = panic "tcDataFamInstDecl"
+
+-----------------------
+tcDataFamInstHeader
+    :: AssocInstInfo -> TyCon -> [Name] -> Maybe [LHsTyVarBndr GhcRn]
+    -> LexicalFixity -> LHsContext GhcRn
+    -> HsTyPats GhcRn -> Maybe (LHsKind GhcRn) -> [LConDecl GhcRn]
+    -> NewOrData
+    -> TcM ([TyVar], [Type], Kind, ThetaType)
+-- The "header" of a data family instance is the part other than
+-- the data constructors themselves
+--    e.g.  data instance D [a] :: * -> * where ...
+-- Here the "header" is the bit before the "where"
+tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
+                    hs_ctxt hs_pats m_ksig hs_cons new_or_data
+  = do { (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, lhs_applied_kind)))
+            <- pushTcLevelM_                                $
+               solveEqualities                              $
+               bindImplicitTKBndrs_Q_Skol imp_vars          $
+               bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $
+               do { stupid_theta <- tcHsContext hs_ctxt
+                  ; (lhs_ty, lhs_kind) <- tcFamTyPats fam_tc hs_pats
+
+                  -- Ensure that the instance is consistent
+                  -- with its parent class
+                  ; addConsistencyConstraints mb_clsinfo lhs_ty
+
+                  -- Add constraints from the result signature
+                  ; res_kind <- tc_kind_sig m_ksig
+
+                  -- Add constraints from the data constructors
+                  ; kcConDecls new_or_data res_kind hs_cons
+
+                  -- See Note [Datatype return kinds] in GHC.Tc.TyCl, point (7).
+                  ; (lhs_extra_args, lhs_applied_kind)
+                      <- tcInstInvisibleTyBinders (invisibleTyBndrCount lhs_kind)
+                                                  lhs_kind
+                  ; let lhs_applied_ty = lhs_ty `mkTcAppTys` lhs_extra_args
+                        hs_lhs         = nlHsTyConApp fixity (getName fam_tc) hs_pats
+                  ; _ <- unifyKind (Just (unLoc hs_lhs)) lhs_applied_kind res_kind
+
+                  ; return ( stupid_theta
+                           , lhs_applied_ty
+                           , lhs_applied_kind ) }
+
+       -- See GHC.Tc.TyCl Note [Generalising in tcFamTyPatsGuts]
+       -- This code (and the stuff immediately above) is very similar
+       -- to that in tcTyFamInstEqnGuts.  Maybe we should abstract the
+       -- common code; but for the moment I concluded that it's
+       -- clearer to duplicate it.  Still, if you fix a bug here,
+       -- check there too!
+       ; let scoped_tvs = imp_tvs ++ exp_tvs
+       ; dvs  <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys scoped_tvs)
+       ; qtvs <- quantifyTyVars dvs
+
+       -- Zonk the patterns etc into the Type world
+       ; (ze, qtvs)       <- zonkTyBndrs qtvs
+       ; lhs_ty           <- zonkTcTypeToTypeX ze lhs_ty
+       ; stupid_theta     <- zonkTcTypesToTypesX ze stupid_theta
+       ; lhs_applied_kind <- zonkTcTypeToTypeX ze lhs_applied_kind
+
+       -- Check that type patterns match the class instance head
+       -- The call to splitTyConApp_maybe here is just an inlining of
+       -- the body of unravelFamInstPats.
+       ; pats <- case splitTyConApp_maybe lhs_ty of
+           Just (_, pats) -> pure pats
+           Nothing -> pprPanic "tcDataFamInstHeader" (ppr lhs_ty)
+       ; return (qtvs, pats, lhs_applied_kind, stupid_theta) }
+  where
+    fam_name  = tyConName fam_tc
+    data_ctxt = DataKindCtxt fam_name
+    exp_bndrs = mb_bndrs `orElse` []
+
+    -- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl, wrinkle (2).
+    tc_kind_sig Nothing
+      = do { unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
+           ; if unlifted_newtypes && new_or_data == NewType
+               then newOpenTypeKind
+               else pure liftedTypeKind
+           }
+
+    -- See Note [Result kind signature for a data family instance]
+    tc_kind_sig (Just hs_kind)
+      = do { sig_kind <- tcLHsKindSig data_ctxt hs_kind
+           ; let (tvs, inner_kind) = tcSplitForAllTys sig_kind
+           ; lvl <- getTcLevel
+           ; (subst, _tvs') <- tcInstSkolTyVarsAt lvl False emptyTCvSubst tvs
+             -- Perhaps surprisingly, we don't need the skolemised tvs themselves
+           ; let final_kind = substTy subst inner_kind
+           ; checkDataKindSig (DataInstanceSort new_or_data) $
+               snd $ tcSplitPiTys final_kind
+             -- See Note [Datatype return kinds], end of point (4)
+           ; return final_kind }
+
+{- Note [Result kind signature for a data family instance]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The expected type might have a forall at the type. Normally, we
+can't skolemise in kinds because we don't have type-level lambda.
+But here, we're at the top-level of an instance declaration, so
+we actually have a place to put the regeneralised variables.
+Thus: skolemise away. cf. Inst.deeplySkolemise and GHC.Tc.Utils.Unify.tcSkolemise
+Examples in indexed-types/should_compile/T12369
+
+Note [Implementing eta reduction for data families]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+   data D :: * -> * -> * -> * -> *
+
+   data instance D [(a,b)] p q :: * -> * where
+      D1 :: blah1
+      D2 :: blah2
+
+Then we'll generate a representation data type
+  data Drep a b p q z where
+      D1 :: blah1
+      D2 :: blah2
+
+and an axiom to connect them
+  axiom AxDrep forall a b p q z. D [(a,b]] p q z = Drep a b p q z
+
+except that we'll eta-reduce the axiom to
+  axiom AxDrep forall a b. D [(a,b]] = Drep a b
+
+This is described at some length in Note [Eta reduction for data families]
+in GHC.Core.Coercion.Axiom. There are several fiddly subtleties lurking here,
+however, so this Note aims to describe these subtleties:
+
+* The representation tycon Drep is parameterised over the free
+  variables of the pattern, in no particular order. So there is no
+  guarantee that 'p' and 'q' will come last in Drep's parameters, and
+  in the right order.  So, if the /patterns/ of the family insatance
+  are eta-reducible, we re-order Drep's parameters to put the
+  eta-reduced type variables last.
+
+* Although we eta-reduce the axiom, we eta-/expand/ the representation
+  tycon Drep.  The kind of D says it takes four arguments, but the
+  data instance header only supplies three.  But the AlgTyCon for Drep
+  itself must have enough TyConBinders so that its result kind is Type.
+  So, with etaExpandAlgTyCon we make up some extra TyConBinders.
+  See point (3) in Note [Datatype return kinds] in GHC.Tc.TyCl.
+
+* The result kind in the instance might be a polykind, like this:
+     data family DP a :: forall k. k -> *
+     data instance DP [b] :: forall k1 k2. (k1,k2) -> *
+
+  So in type-checking the LHS (DP Int) we need to check that it is
+  more polymorphic than the signature.  To do that we must skolemise
+  the signature and instantiate the call of DP.  So we end up with
+     data instance DP [b] @(k1,k2) (z :: (k1,k2)) where
+
+  Note that we must parameterise the representation tycon DPrep over
+  'k1' and 'k2', as well as 'b'.
+
+  The skolemise bit is done in tc_kind_sig, while the instantiate bit
+  is done by tcFamTyPats.
+
+* Very fiddly point.  When we eta-reduce to
+     axiom AxDrep forall a b. D [(a,b]] = Drep a b
+
+  we want the kind of (D [(a,b)]) to be the same as the kind of
+  (Drep a b).  This ensures that applying the axiom doesn't change the
+  kind.  Why is that hard?  Because the kind of (Drep a b) depends on
+  the TyConBndrVis on Drep's arguments. In particular do we have
+    (forall (k::*). blah) or (* -> blah)?
+
+  We must match whatever D does!  In #15817 we had
+      data family X a :: forall k. * -> *   -- Note: a forall that is not used
+      data instance X Int b = MkX
+
+  So the data instance is really
+      data istance X Int @k b = MkX
+
+  The axiom will look like
+      axiom    X Int = Xrep
+
+  and it's important that XRep :: forall k * -> *, following X.
+
+  To achieve this we get the TyConBndrVis flags from tcbVisibilities,
+  and use those flags for any eta-reduced arguments.  Sigh.
+
+* The final turn of the knife is that tcbVisibilities is itself
+  tricky to sort out.  Consider
+      data family D k :: k
+  Then consider D (forall k2. k2 -> k2) Type Type
+  The visibility flags on an application of D may affected by the arguments
+  themselves.  Heavy sigh.  But not truly hard; that's what tcbVisibilities
+  does.
+
+-}
+
+
+{- *********************************************************************
+*                                                                      *
+      Class instance declarations, pass 2
+*                                                                      *
+********************************************************************* -}
+
+tcInstDecls2 :: [LTyClDecl GhcRn] -> [InstInfo GhcRn]
+             -> TcM (LHsBinds GhcTc)
+-- (a) From each class declaration,
+--      generate any default-method bindings
+-- (b) From each instance decl
+--      generate the dfun binding
+
+tcInstDecls2 tycl_decls inst_decls
+  = do  { -- (a) Default methods from class decls
+          let class_decls = filter (isClassDecl . unLoc) tycl_decls
+        ; dm_binds_s <- mapM tcClassDecl2 class_decls
+        ; let dm_binds = unionManyBags dm_binds_s
+
+          -- (b) instance declarations
+        ; let dm_ids = collectHsBindsBinders dm_binds
+              -- Add the default method Ids (again)
+              -- (they were arready added in GHC.Tc.TyCl.Utils.tcAddImplicits)
+              -- See Note [Default methods in the type environment]
+        ; inst_binds_s <- tcExtendGlobalValEnv dm_ids $
+                          mapM tcInstDecl2 inst_decls
+
+          -- Done
+        ; return (dm_binds `unionBags` unionManyBags inst_binds_s) }
+
+{- Note [Default methods in the type environment]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The default method Ids are already in the type environment (see Note
+[Default method Ids and Template Haskell] in TcTyDcls), BUT they
+don't have their InlinePragmas yet.  Usually that would not matter,
+because the simplifier propagates information from binding site to
+use.  But, unusually, when compiling instance decls we *copy* the
+INLINE pragma from the default method to the method for that
+particular operation (see Note [INLINE and default methods] below).
+
+So right here in tcInstDecls2 we must re-extend the type envt with
+the default method Ids replete with their INLINE pragmas.  Urk.
+-}
+
+tcInstDecl2 :: InstInfo GhcRn -> TcM (LHsBinds GhcTc)
+            -- Returns a binding for the dfun
+tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
+  = recoverM (return emptyLHsBinds)             $
+    setSrcSpan loc                              $
+    addErrCtxt (instDeclCtxt2 (idType dfun_id)) $
+    do {  -- Instantiate the instance decl with skolem constants
+       ; (inst_tyvars, dfun_theta, inst_head) <- tcSkolDFunType dfun_id
+       ; dfun_ev_vars <- newEvVars dfun_theta
+                     -- We instantiate the dfun_id with superSkolems.
+                     -- See Note [Subtle interaction of recursion and overlap]
+                     -- and Note [Binding when looking up instances]
+
+       ; let (clas, inst_tys) = tcSplitDFunHead inst_head
+             (class_tyvars, sc_theta, _, op_items) = classBigSig clas
+             sc_theta' = substTheta (zipTvSubst class_tyvars inst_tys) sc_theta
+
+       ; traceTc "tcInstDecl2" (vcat [ppr inst_tyvars, ppr inst_tys, ppr dfun_theta, ppr sc_theta'])
+
+                      -- Deal with 'SPECIALISE instance' pragmas
+                      -- See Note [SPECIALISE instance pragmas]
+       ; spec_inst_info@(spec_inst_prags,_) <- tcSpecInstPrags dfun_id ibinds
+
+         -- Typecheck superclasses and methods
+         -- See Note [Typechecking plan for instance declarations]
+       ; dfun_ev_binds_var <- newTcEvBinds
+       ; let dfun_ev_binds = TcEvBinds dfun_ev_binds_var
+       ; (tclvl, (sc_meth_ids, sc_meth_binds, sc_meth_implics))
+             <- pushTcLevelM $
+                do { (sc_ids, sc_binds, sc_implics)
+                        <- tcSuperClasses dfun_id clas inst_tyvars dfun_ev_vars
+                                          inst_tys dfun_ev_binds
+                                          sc_theta'
+
+                      -- Typecheck the methods
+                   ; (meth_ids, meth_binds, meth_implics)
+                        <- tcMethods dfun_id clas inst_tyvars dfun_ev_vars
+                                     inst_tys dfun_ev_binds spec_inst_info
+                                     op_items ibinds
+
+                   ; return ( sc_ids     ++          meth_ids
+                            , sc_binds   `unionBags` meth_binds
+                            , sc_implics `unionBags` meth_implics ) }
+
+       ; imp <- newImplication
+       ; emitImplication $
+         imp { ic_tclvl  = tclvl
+             , ic_skols  = inst_tyvars
+             , ic_given  = dfun_ev_vars
+             , ic_wanted = mkImplicWC sc_meth_implics
+             , ic_binds  = dfun_ev_binds_var
+             , ic_info   = InstSkol }
+
+       -- Create the result bindings
+       ; self_dict <- newDict clas inst_tys
+       ; let class_tc      = classTyCon clas
+             [dict_constr] = tyConDataCons class_tc
+             dict_bind     = mkVarBind self_dict (L loc con_app_args)
+
+                     -- We don't produce a binding for the dict_constr; instead we
+                     -- rely on the simplifier to unfold this saturated application
+                     -- We do this rather than generate an HsCon directly, because
+                     -- it means that the special cases (e.g. dictionary with only one
+                     -- member) are dealt with by the common MkId.mkDataConWrapId
+                     -- code rather than needing to be repeated here.
+                     --    con_app_tys  = MkD ty1 ty2
+                     --    con_app_scs  = MkD ty1 ty2 sc1 sc2
+                     --    con_app_args = MkD ty1 ty2 sc1 sc2 op1 op2
+             con_app_tys  = mkHsWrap (mkWpTyApps inst_tys)
+                                  (HsConLikeOut noExtField (RealDataCon dict_constr))
+                       -- NB: We *can* have covars in inst_tys, in the case of
+                       -- promoted GADT constructors.
+
+             con_app_args = foldl' app_to_meth con_app_tys sc_meth_ids
+
+             app_to_meth :: HsExpr GhcTc -> Id -> HsExpr GhcTc
+             app_to_meth fun meth_id = HsApp noExtField (L loc fun)
+                                            (L loc (wrapId arg_wrapper meth_id))
+
+             inst_tv_tys = mkTyVarTys inst_tyvars
+             arg_wrapper = mkWpEvVarApps dfun_ev_vars <.> mkWpTyApps inst_tv_tys
+
+             is_newtype = isNewTyCon class_tc
+             dfun_id_w_prags = addDFunPrags dfun_id sc_meth_ids
+             dfun_spec_prags
+                | is_newtype = SpecPrags []
+                | otherwise  = SpecPrags spec_inst_prags
+                    -- Newtype dfuns just inline unconditionally,
+                    -- so don't attempt to specialise them
+
+             export = ABE { abe_ext  = noExtField
+                          , abe_wrap = idHsWrapper
+                          , abe_poly = dfun_id_w_prags
+                          , abe_mono = self_dict
+                          , abe_prags = dfun_spec_prags }
+                          -- NB: see Note [SPECIALISE instance pragmas]
+             main_bind = AbsBinds { abs_ext = noExtField
+                                  , abs_tvs = inst_tyvars
+                                  , abs_ev_vars = dfun_ev_vars
+                                  , abs_exports = [export]
+                                  , abs_ev_binds = []
+                                  , abs_binds = unitBag dict_bind
+                                  , abs_sig = True }
+
+       ; return (unitBag (L loc main_bind) `unionBags` sc_meth_binds)
+       }
+ where
+   dfun_id = instanceDFunId ispec
+   loc     = getSrcSpan dfun_id
+
+addDFunPrags :: DFunId -> [Id] -> DFunId
+-- DFuns need a special Unfolding and InlinePrag
+--    See Note [ClassOp/DFun selection]
+--    and Note [Single-method classes]
+-- It's easiest to create those unfoldings right here, where
+-- have all the pieces in hand, even though we are messing with
+-- Core at this point, which the typechecker doesn't usually do
+-- However we take care to build the unfolding using the TyVars from
+-- the DFunId rather than from the skolem pieces that the typechecker
+-- is messing with.
+addDFunPrags dfun_id sc_meth_ids
+ | is_newtype
+  = dfun_id `setIdUnfolding`  mkInlineUnfoldingWithArity 0 con_app
+            `setInlinePragma` alwaysInlinePragma { inl_sat = Just 0 }
+ | otherwise
+ = dfun_id `setIdUnfolding`  mkDFunUnfolding dfun_bndrs dict_con dict_args
+           `setInlinePragma` dfunInlinePragma
+ where
+   con_app    = mkLams dfun_bndrs $
+                mkApps (Var (dataConWrapId dict_con)) dict_args
+                 -- mkApps is OK because of the checkForLevPoly call in checkValidClass
+                 -- See Note [Levity polymorphism checking] in GHC.HsToCore.Monad
+   dict_args  = map Type inst_tys ++
+                [mkVarApps (Var id) dfun_bndrs | id <- sc_meth_ids]
+
+   (dfun_tvs, dfun_theta, clas, inst_tys) = tcSplitDFunTy (idType dfun_id)
+   ev_ids      = mkTemplateLocalsNum 1                    dfun_theta
+   dfun_bndrs  = dfun_tvs ++ ev_ids
+   clas_tc     = classTyCon clas
+   [dict_con]  = tyConDataCons clas_tc
+   is_newtype  = isNewTyCon clas_tc
+
+wrapId :: HsWrapper -> Id -> HsExpr GhcTc
+wrapId wrapper id = mkHsWrap wrapper (HsVar noExtField (noLoc id))
+
+{- Note [Typechecking plan for instance declarations]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For instance declarations we generate the following bindings and implication
+constraints.  Example:
+
+   instance Ord a => Ord [a] where compare = <compare-rhs>
+
+generates this:
+
+   Bindings:
+      -- Method bindings
+      $ccompare :: forall a. Ord a => a -> a -> Ordering
+      $ccompare = /\a \(d:Ord a). let <meth-ev-binds> in ...
+
+      -- Superclass bindings
+      $cp1Ord :: forall a. Ord a => Eq [a]
+      $cp1Ord = /\a \(d:Ord a). let <sc-ev-binds>
+               in dfEqList (dw :: Eq a)
+
+   Constraints:
+      forall a. Ord a =>
+                -- Method constraint
+             (forall. (empty) => <constraints from compare-rhs>)
+                -- Superclass constraint
+          /\ (forall. (empty) => dw :: Eq a)
+
+Notice that
+
+ * Per-meth/sc implication.  There is one inner implication per
+   superclass or method, with no skolem variables or givens.  The only
+   reason for this one is to gather the evidence bindings privately
+   for this superclass or method.  This implication is generated
+   by checkInstConstraints.
+
+ * Overall instance implication. There is an overall enclosing
+   implication for the whole instance declaration, with the expected
+   skolems and givens.  We need this to get the correct "redundant
+   constraint" warnings, gathering all the uses from all the methods
+   and superclasses.  See GHC.Tc.Solver Note [Tracking redundant
+   constraints]
+
+ * The given constraints in the outer implication may generate
+   evidence, notably by superclass selection.  Since the method and
+   superclass bindings are top-level, we want that evidence copied
+   into *every* method or superclass definition.  (Some of it will
+   be usused in some, but dead-code elimination will drop it.)
+
+   We achieve this by putting the evidence variable for the overall
+   instance implication into the AbsBinds for each method/superclass.
+   Hence the 'dfun_ev_binds' passed into tcMethods and tcSuperClasses.
+   (And that in turn is why the abs_ev_binds field of AbBinds is a
+   [TcEvBinds] rather than simply TcEvBinds.
+
+   This is a bit of a hack, but works very nicely in practice.
+
+ * Note that if a method has a locally-polymorphic binding, there will
+   be yet another implication for that, generated by tcPolyCheck
+   in tcMethodBody. E.g.
+          class C a where
+            foo :: forall b. Ord b => blah
+
+
+************************************************************************
+*                                                                      *
+      Type-checking superclasses
+*                                                                      *
+************************************************************************
+-}
+
+tcSuperClasses :: DFunId -> Class -> [TcTyVar] -> [EvVar] -> [TcType]
+               -> TcEvBinds
+               -> TcThetaType
+               -> TcM ([EvVar], LHsBinds GhcTc, Bag Implication)
+-- Make a new top-level function binding for each superclass,
+-- something like
+--    $Ordp1 :: forall a. Ord a => Eq [a]
+--    $Ordp1 = /\a \(d:Ord a). dfunEqList a (sc_sel d)
+--
+-- See Note [Recursive superclasses] for why this is so hard!
+-- In effect, we build a special-purpose solver for the first step
+-- of solving each superclass constraint
+tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds sc_theta
+  = do { (ids, binds, implics) <- mapAndUnzip3M tc_super (zip sc_theta [fIRST_TAG..])
+       ; return (ids, listToBag binds, listToBag implics) }
+  where
+    loc = getSrcSpan dfun_id
+    size = sizeTypes inst_tys
+    tc_super (sc_pred, n)
+      = do { (sc_implic, ev_binds_var, sc_ev_tm)
+                <- checkInstConstraints $ emitWanted (ScOrigin size) sc_pred
+
+           ; sc_top_name  <- newName (mkSuperDictAuxOcc n (getOccName cls))
+           ; sc_ev_id     <- newEvVar sc_pred
+           ; addTcEvBind ev_binds_var $ mkWantedEvBind sc_ev_id sc_ev_tm
+           ; let sc_top_ty = mkInvForAllTys tyvars $
+                             mkPhiTy (map idType dfun_evs) sc_pred
+                 sc_top_id = mkLocalId sc_top_name sc_top_ty
+                 export = ABE { abe_ext  = noExtField
+                              , abe_wrap = idHsWrapper
+                              , abe_poly = sc_top_id
+                              , abe_mono = sc_ev_id
+                              , abe_prags = noSpecPrags }
+                 local_ev_binds = TcEvBinds ev_binds_var
+                 bind = AbsBinds { abs_ext      = noExtField
+                                 , abs_tvs      = tyvars
+                                 , abs_ev_vars  = dfun_evs
+                                 , abs_exports  = [export]
+                                 , abs_ev_binds = [dfun_ev_binds, local_ev_binds]
+                                 , abs_binds    = emptyBag
+                                 , abs_sig      = False }
+           ; return (sc_top_id, L loc bind, sc_implic) }
+
+-------------------
+checkInstConstraints :: TcM result
+                     -> TcM (Implication, EvBindsVar, result)
+-- See Note [Typechecking plan for instance declarations]
+checkInstConstraints thing_inside
+  = do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints  $
+                                    thing_inside
+
+       ; ev_binds_var <- newTcEvBinds
+       ; implic <- newImplication
+       ; let implic' = implic { ic_tclvl  = tclvl
+                              , ic_wanted = wanted
+                              , ic_binds  = ev_binds_var
+                              , ic_info   = InstSkol }
+
+       ; return (implic', ev_binds_var, result) }
+
+{-
+Note [Recursive superclasses]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See #3731, #4809, #5751, #5913, #6117, #6161, which all
+describe somewhat more complicated situations, but ones
+encountered in practice.
+
+See also tests tcrun020, tcrun021, tcrun033, and #11427.
+
+----- THE PROBLEM --------
+The problem is that it is all too easy to create a class whose
+superclass is bottom when it should not be.
+
+Consider the following (extreme) situation:
+        class C a => D a where ...
+        instance D [a] => D [a] where ...   (dfunD)
+        instance C [a] => C [a] where ...   (dfunC)
+Although this looks wrong (assume D [a] to prove D [a]), it is only a
+more extreme case of what happens with recursive dictionaries, and it
+can, just about, make sense because the methods do some work before
+recursing.
+
+To implement the dfunD we must generate code for the superclass C [a],
+which we had better not get by superclass selection from the supplied
+argument:
+       dfunD :: forall a. D [a] -> D [a]
+       dfunD = \d::D [a] -> MkD (scsel d) ..
+
+Otherwise if we later encounter a situation where
+we have a [Wanted] dw::D [a] we might solve it thus:
+     dw := dfunD dw
+Which is all fine except that now ** the superclass C is bottom **!
+
+The instance we want is:
+       dfunD :: forall a. D [a] -> D [a]
+       dfunD = \d::D [a] -> MkD (dfunC (scsel d)) ...
+
+----- THE SOLUTION --------
+The basic solution is simple: be very careful about using superclass
+selection to generate a superclass witness in a dictionary function
+definition.  More precisely:
+
+  Superclass Invariant: in every class dictionary,
+                        every superclass dictionary field
+                        is non-bottom
+
+To achieve the Superclass Invariant, in a dfun definition we can
+generate a guaranteed-non-bottom superclass witness from:
+  (sc1) one of the dictionary arguments itself (all non-bottom)
+  (sc2) an immediate superclass of a smaller dictionary
+  (sc3) a call of a dfun (always returns a dictionary constructor)
+
+The tricky case is (sc2).  We proceed by induction on the size of
+the (type of) the dictionary, defined by GHC.Tc.Validity.sizeTypes.
+Let's suppose we are building a dictionary of size 3, and
+suppose the Superclass Invariant holds of smaller dictionaries.
+Then if we have a smaller dictionary, its immediate superclasses
+will be non-bottom by induction.
+
+What does "we have a smaller dictionary" mean?  It might be
+one of the arguments of the instance, or one of its superclasses.
+Here is an example, taken from CmmExpr:
+       class Ord r => UserOfRegs r a where ...
+(i1)   instance UserOfRegs r a => UserOfRegs r (Maybe a) where
+(i2)   instance (Ord r, UserOfRegs r CmmReg) => UserOfRegs r CmmExpr where
+
+For (i1) we can get the (Ord r) superclass by selection from (UserOfRegs r a),
+since it is smaller than the thing we are building (UserOfRegs r (Maybe a).
+
+But for (i2) that isn't the case, so we must add an explicit, and
+perhaps surprising, (Ord r) argument to the instance declaration.
+
+Here's another example from #6161:
+
+       class       Super a => Duper a  where ...
+       class Duper (Fam a) => Foo a    where ...
+(i3)   instance Foo a => Duper (Fam a) where ...
+(i4)   instance              Foo Float where ...
+
+It would be horribly wrong to define
+   dfDuperFam :: Foo a -> Duper (Fam a)  -- from (i3)
+   dfDuperFam d = MkDuper (sc_sel1 (sc_sel2 d)) ...
+
+   dfFooFloat :: Foo Float               -- from (i4)
+   dfFooFloat = MkFoo (dfDuperFam dfFooFloat) ...
+
+Now the Super superclass of Duper is definitely bottom!
+
+This won't happen because when processing (i3) we can use the
+superclasses of (Foo a), which is smaller, namely Duper (Fam a).  But
+that is *not* smaller than the target so we can't take *its*
+superclasses.  As a result the program is rightly rejected, unless you
+add (Super (Fam a)) to the context of (i3).
+
+Note [Solving superclass constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+How do we ensure that every superclass witness is generated by
+one of (sc1) (sc2) or (sc3) in Note [Recursive superclasses].
+Answer:
+
+  * Superclass "wanted" constraints have CtOrigin of (ScOrigin size)
+    where 'size' is the size of the instance declaration. e.g.
+          class C a => D a where...
+          instance blah => D [a] where ...
+    The wanted superclass constraint for C [a] has origin
+    ScOrigin size, where size = size( D [a] ).
+
+  * (sc1) When we rewrite such a wanted constraint, it retains its
+    origin.  But if we apply an instance declaration, we can set the
+    origin to (ScOrigin infinity), thus lifting any restrictions by
+    making prohibitedSuperClassSolve return False.
+
+  * (sc2) ScOrigin wanted constraints can't be solved from a
+    superclass selection, except at a smaller type.  This test is
+    implemented by GHC.Tc.Solver.Interact.prohibitedSuperClassSolve
+
+  * The "given" constraints of an instance decl have CtOrigin
+    GivenOrigin InstSkol.
+
+  * When we make a superclass selection from InstSkol we use
+    a SkolemInfo of (InstSC size), where 'size' is the size of
+    the constraint whose superclass we are taking.  A similarly
+    when taking the superclass of an InstSC.  This is implemented
+    in GHC.Tc.Solver.Canonical.newSCWorkFromFlavored
+
+Note [Silent superclass arguments] (historical interest only)
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+NB1: this note describes our *old* solution to the
+     recursive-superclass problem. I'm keeping the Note
+     for now, just as institutional memory.
+     However, the code for silent superclass arguments
+     was removed in late Dec 2014
+
+NB2: the silent-superclass solution introduced new problems
+     of its own, in the form of instance overlap.  Tests
+     SilentParametersOverlapping, T5051, and T7862 are examples
+
+NB3: the silent-superclass solution also generated tons of
+     extra dictionaries.  For example, in monad-transformer
+     code, when constructing a Monad dictionary you had to pass
+     an Applicative dictionary; and to construct that you need
+     a Functor dictionary. Yet these extra dictionaries were
+     often never used.  Test T3064 compiled *far* faster after
+     silent superclasses were eliminated.
+
+Our solution to this problem "silent superclass arguments".  We pass
+to each dfun some ``silent superclass arguments’’, which are the
+immediate superclasses of the dictionary we are trying to
+construct. In our example:
+       dfun :: forall a. C [a] -> D [a] -> D [a]
+       dfun = \(dc::C [a]) (dd::D [a]) -> DOrd dc ...
+Notice the extra (dc :: C [a]) argument compared to the previous version.
+
+This gives us:
+
+     -----------------------------------------------------------
+     DFun Superclass Invariant
+     ~~~~~~~~~~~~~~~~~~~~~~~~
+     In the body of a DFun, every superclass argument to the
+     returned dictionary is
+       either   * one of the arguments of the DFun,
+       or       * constant, bound at top level
+     -----------------------------------------------------------
+
+This net effect is that it is safe to treat a dfun application as
+wrapping a dictionary constructor around its arguments (in particular,
+a dfun never picks superclasses from the arguments under the
+dictionary constructor). No superclass is hidden inside a dfun
+application.
+
+The extra arguments required to satisfy the DFun Superclass Invariant
+always come first, and are called the "silent" arguments.  You can
+find out how many silent arguments there are using Id.dfunNSilent;
+and then you can just drop that number of arguments to see the ones
+that were in the original instance declaration.
+
+DFun types are built (only) by MkId.mkDictFunId, so that is where we
+decide what silent arguments are to be added.
+-}
+
+{-
+************************************************************************
+*                                                                      *
+      Type-checking an instance method
+*                                                                      *
+************************************************************************
+
+tcMethod
+- Make the method bindings, as a [(NonRec, HsBinds)], one per method
+- Remembering to use fresh Name (the instance method Name) as the binder
+- Bring the instance method Ids into scope, for the benefit of tcInstSig
+- Use sig_fn mapping instance method Name -> instance tyvars
+- Ditto prag_fn
+- Use tcValBinds to do the checking
+-}
+
+tcMethods :: DFunId -> Class
+          -> [TcTyVar] -> [EvVar]
+          -> [TcType]
+          -> TcEvBinds
+          -> ([Located TcSpecPrag], TcPragEnv)
+          -> [ClassOpItem]
+          -> InstBindings GhcRn
+          -> TcM ([Id], LHsBinds GhcTc, Bag Implication)
+        -- The returned inst_meth_ids all have types starting
+        --      forall tvs. theta => ...
+tcMethods dfun_id clas tyvars dfun_ev_vars inst_tys
+                  dfun_ev_binds (spec_inst_prags, prag_fn) op_items
+                  (InstBindings { ib_binds      = binds
+                                , ib_tyvars     = lexical_tvs
+                                , ib_pragmas    = sigs
+                                , ib_extensions = exts
+                                , ib_derived    = is_derived })
+  = tcExtendNameTyVarEnv (lexical_tvs `zip` tyvars) $
+       -- The lexical_tvs scope over the 'where' part
+    do { traceTc "tcInstMeth" (ppr sigs $$ ppr binds)
+       ; checkMinimalDefinition
+       ; checkMethBindMembership
+       ; (ids, binds, mb_implics) <- set_exts exts $
+                                     unset_warnings_deriving $
+                                     mapAndUnzip3M tc_item op_items
+       ; return (ids, listToBag binds, listToBag (catMaybes mb_implics)) }
+  where
+    set_exts :: [LangExt.Extension] -> TcM a -> TcM a
+    set_exts es thing = foldr setXOptM thing es
+
+    -- See Note [Avoid -Winaccessible-code when deriving]
+    unset_warnings_deriving :: TcM a -> TcM a
+    unset_warnings_deriving
+      | is_derived = unsetWOptM Opt_WarnInaccessibleCode
+      | otherwise  = id
+
+    hs_sig_fn = mkHsSigFun sigs
+    inst_loc  = getSrcSpan dfun_id
+
+    ----------------------
+    tc_item :: ClassOpItem -> TcM (Id, LHsBind GhcTc, Maybe Implication)
+    tc_item (sel_id, dm_info)
+      | Just (user_bind, bndr_loc, prags) <- findMethodBind (idName sel_id) binds prag_fn
+      = tcMethodBody clas tyvars dfun_ev_vars inst_tys
+                              dfun_ev_binds is_derived hs_sig_fn
+                              spec_inst_prags prags
+                              sel_id user_bind bndr_loc
+      | otherwise
+      = do { traceTc "tc_def" (ppr sel_id)
+           ; tc_default sel_id dm_info }
+
+    ----------------------
+    tc_default :: Id -> DefMethInfo
+               -> TcM (TcId, LHsBind GhcTc, Maybe Implication)
+
+    tc_default sel_id (Just (dm_name, _))
+      = do { (meth_bind, inline_prags) <- mkDefMethBind clas inst_tys sel_id dm_name
+           ; tcMethodBody clas tyvars dfun_ev_vars inst_tys
+                          dfun_ev_binds is_derived hs_sig_fn
+                          spec_inst_prags inline_prags
+                          sel_id meth_bind inst_loc }
+
+    tc_default sel_id Nothing     -- No default method at all
+      = do { traceTc "tc_def: warn" (ppr sel_id)
+           ; (meth_id, _) <- mkMethIds clas tyvars dfun_ev_vars
+                                       inst_tys sel_id
+           ; dflags <- getDynFlags
+           ; let meth_bind = mkVarBind meth_id $
+                             mkLHsWrap lam_wrapper (error_rhs dflags)
+           ; return (meth_id, meth_bind, Nothing) }
+      where
+        error_rhs dflags = L inst_loc $ HsApp noExtField error_fun (error_msg dflags)
+        error_fun    = L inst_loc $
+                       wrapId (mkWpTyApps
+                                [ getRuntimeRep meth_tau, meth_tau])
+                              nO_METHOD_BINDING_ERROR_ID
+        error_msg dflags = L inst_loc (HsLit noExtField (HsStringPrim NoSourceText
+                                              (unsafeMkByteString (error_string dflags))))
+        meth_tau     = funResultTy (piResultTys (idType sel_id) inst_tys)
+        error_string dflags = showSDoc dflags
+                              (hcat [ppr inst_loc, vbar, ppr sel_id ])
+        lam_wrapper  = mkWpTyLams tyvars <.> mkWpLams dfun_ev_vars
+
+    ----------------------
+    -- Check if one of the minimal complete definitions is satisfied
+    checkMinimalDefinition
+      = whenIsJust (isUnsatisfied methodExists (classMinimalDef clas)) $
+        warnUnsatisfiedMinimalDefinition
+
+    methodExists meth = isJust (findMethodBind meth binds prag_fn)
+
+    ----------------------
+    -- Check if any method bindings do not correspond to the class.
+    -- See Note [Mismatched class methods and associated type families].
+    checkMethBindMembership
+      = mapM_ (addErrTc . badMethodErr clas) mismatched_meths
+      where
+        bind_nms         = map unLoc $ collectMethodBinders binds
+        cls_meth_nms     = map (idName . fst) op_items
+        mismatched_meths = bind_nms `minusList` cls_meth_nms
+
+{-
+Note [Mismatched class methods and associated type families]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's entirely possible for someone to put methods or associated type family
+instances inside of a class in which it doesn't belong. For instance, we'd
+want to fail if someone wrote this:
+
+  instance Eq () where
+    type Rep () = Maybe
+    compare = undefined
+
+Since neither the type family `Rep` nor the method `compare` belong to the
+class `Eq`. Normally, this is caught in the renamer when resolving RdrNames,
+since that would discover that the parent class `Eq` is incorrect.
+
+However, there is a scenario in which the renamer could fail to catch this:
+if the instance was generated through Template Haskell, as in #12387. In that
+case, Template Haskell will provide fully resolved names (e.g.,
+`GHC.Classes.compare`), so the renamer won't notice the sleight-of-hand going
+on. For this reason, we also put an extra validity check for this in the
+typechecker as a last resort.
+
+Note [Avoid -Winaccessible-code when deriving]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-Winaccessible-code can be particularly noisy when deriving instances for
+GADTs. Consider the following example (adapted from #8128):
+
+  data T a where
+    MkT1 :: Int -> T Int
+    MkT2 :: T Bool
+    MkT3 :: T Bool
+  deriving instance Eq (T a)
+  deriving instance Ord (T a)
+
+In the derived Ord instance, GHC will generate the following code:
+
+  instance Ord (T a) where
+    compare x y
+      = case x of
+          MkT2
+            -> case y of
+                 MkT1 {} -> GT
+                 MkT2    -> EQ
+                 _       -> LT
+          ...
+
+However, that MkT1 is unreachable, since the type indices for MkT1 and MkT2
+differ, so if -Winaccessible-code is enabled, then deriving this instance will
+result in unwelcome warnings.
+
+One conceivable approach to fixing this issue would be to change `deriving Ord`
+such that it becomes smarter about not generating unreachable cases. This,
+however, would be a highly nontrivial refactor, as we'd have to propagate
+through typing information everywhere in the algorithm that generates Ord
+instances in order to determine which cases were unreachable. This seems like
+a lot of work for minimal gain, so we have opted not to go for this approach.
+
+Instead, we take the much simpler approach of always disabling
+-Winaccessible-code for derived code. To accomplish this, we do the following:
+
+1. In tcMethods (which typechecks method bindings), disable
+   -Winaccessible-code.
+2. When creating Implications during typechecking, record this flag
+   (in ic_warn_inaccessible) at the time of creation.
+3. After typechecking comes error reporting, where GHC must decide how to
+   report inaccessible code to the user, on an Implication-by-Implication
+   basis. If an Implication's DynFlags indicate that -Winaccessible-code was
+   disabled, then don't bother reporting it. That's it!
+-}
+
+------------------------
+tcMethodBody :: Class -> [TcTyVar] -> [EvVar] -> [TcType]
+             -> TcEvBinds -> Bool
+             -> HsSigFun
+             -> [LTcSpecPrag] -> [LSig GhcRn]
+             -> Id -> LHsBind GhcRn -> SrcSpan
+             -> TcM (TcId, LHsBind GhcTc, Maybe Implication)
+tcMethodBody clas tyvars dfun_ev_vars inst_tys
+                     dfun_ev_binds is_derived
+                     sig_fn spec_inst_prags prags
+                     sel_id (L bind_loc meth_bind) bndr_loc
+  = add_meth_ctxt $
+    do { traceTc "tcMethodBody" (ppr sel_id <+> ppr (idType sel_id) $$ ppr bndr_loc)
+       ; (global_meth_id, local_meth_id) <- setSrcSpan bndr_loc $
+                                            mkMethIds clas tyvars dfun_ev_vars
+                                                      inst_tys sel_id
+
+       ; let lm_bind = meth_bind { fun_id = L bndr_loc (idName local_meth_id) }
+                       -- Substitute the local_meth_name for the binder
+                       -- NB: the binding is always a FunBind
+
+            -- taking instance signature into account might change the type of
+            -- the local_meth_id
+       ; (meth_implic, ev_binds_var, tc_bind)
+             <- checkInstConstraints $
+                tcMethodBodyHelp sig_fn sel_id local_meth_id (L bind_loc lm_bind)
+
+       ; global_meth_id <- addInlinePrags global_meth_id prags
+       ; spec_prags     <- tcSpecPrags global_meth_id prags
+
+        ; let specs  = mk_meth_spec_prags global_meth_id spec_inst_prags spec_prags
+              export = ABE { abe_ext   = noExtField
+                           , abe_poly  = global_meth_id
+                           , abe_mono  = local_meth_id
+                           , abe_wrap  = idHsWrapper
+                           , abe_prags = specs }
+
+              local_ev_binds = TcEvBinds ev_binds_var
+              full_bind = AbsBinds { abs_ext      = noExtField
+                                   , abs_tvs      = tyvars
+                                   , abs_ev_vars  = dfun_ev_vars
+                                   , abs_exports  = [export]
+                                   , abs_ev_binds = [dfun_ev_binds, local_ev_binds]
+                                   , abs_binds    = tc_bind
+                                   , abs_sig      = True }
+
+        ; return (global_meth_id, L bind_loc full_bind, Just meth_implic) }
+  where
+        -- For instance decls that come from deriving clauses
+        -- we want to print out the full source code if there's an error
+        -- because otherwise the user won't see the code at all
+    add_meth_ctxt thing
+      | is_derived = addLandmarkErrCtxt (derivBindCtxt sel_id clas inst_tys) thing
+      | otherwise  = thing
+
+tcMethodBodyHelp :: HsSigFun -> Id -> TcId
+                 -> LHsBind GhcRn -> TcM (LHsBinds GhcTcId)
+tcMethodBodyHelp hs_sig_fn sel_id local_meth_id meth_bind
+  | Just hs_sig_ty <- hs_sig_fn sel_name
+              -- There is a signature in the instance
+              -- See Note [Instance method signatures]
+  = do { let ctxt = FunSigCtxt sel_name True
+       ; (sig_ty, hs_wrap)
+             <- setSrcSpan (getLoc (hsSigType hs_sig_ty)) $
+                do { inst_sigs <- xoptM LangExt.InstanceSigs
+                   ; checkTc inst_sigs (misplacedInstSig sel_name hs_sig_ty)
+                   ; sig_ty  <- tcHsSigType (FunSigCtxt sel_name False) hs_sig_ty
+                   ; let local_meth_ty = idType local_meth_id
+                   ; hs_wrap <- addErrCtxtM (methSigCtxt sel_name sig_ty local_meth_ty) $
+                                tcSubType_NC ctxt sig_ty local_meth_ty
+                   ; return (sig_ty, hs_wrap) }
+
+       ; inner_meth_name <- newName (nameOccName sel_name)
+       ; let inner_meth_id  = mkLocalId inner_meth_name sig_ty
+             inner_meth_sig = CompleteSig { sig_bndr = inner_meth_id
+                                          , sig_ctxt = ctxt
+                                          , sig_loc  = getLoc (hsSigType hs_sig_ty) }
+
+
+       ; (tc_bind, [inner_id]) <- tcPolyCheck no_prag_fn inner_meth_sig meth_bind
+
+       ; let export = ABE { abe_ext   = noExtField
+                          , abe_poly  = local_meth_id
+                          , abe_mono  = inner_id
+                          , abe_wrap  = hs_wrap
+                          , abe_prags = noSpecPrags }
+
+       ; return (unitBag $ L (getLoc meth_bind) $
+                 AbsBinds { abs_ext = noExtField, abs_tvs = [], abs_ev_vars = []
+                          , abs_exports = [export]
+                          , abs_binds = tc_bind, abs_ev_binds = []
+                          , abs_sig = True }) }
+
+  | otherwise  -- No instance signature
+  = do { let ctxt = FunSigCtxt sel_name False
+                    -- False <=> don't report redundant constraints
+                    -- The signature is not under the users control!
+             tc_sig = completeSigFromId ctxt local_meth_id
+              -- Absent a type sig, there are no new scoped type variables here
+              -- Only the ones from the instance decl itself, which are already
+              -- in scope.  Example:
+              --      class C a where { op :: forall b. Eq b => ... }
+              --      instance C [c] where { op = <rhs> }
+              -- In <rhs>, 'c' is scope but 'b' is not!
+
+       ; (tc_bind, _) <- tcPolyCheck no_prag_fn tc_sig meth_bind
+       ; return tc_bind }
+
+  where
+    sel_name   = idName sel_id
+    no_prag_fn = emptyPragEnv   -- No pragmas for local_meth_id;
+                                -- they are all for meth_id
+
+
+------------------------
+mkMethIds :: Class -> [TcTyVar] -> [EvVar]
+          -> [TcType] -> Id -> TcM (TcId, TcId)
+             -- returns (poly_id, local_id), but ignoring any instance signature
+             -- See Note [Instance method signatures]
+mkMethIds clas tyvars dfun_ev_vars inst_tys sel_id
+  = do  { poly_meth_name  <- newName (mkClassOpAuxOcc sel_occ)
+        ; local_meth_name <- newName sel_occ
+                  -- Base the local_meth_name on the selector name, because
+                  -- type errors from tcMethodBody come from here
+        ; let poly_meth_id  = mkLocalId poly_meth_name  poly_meth_ty
+              local_meth_id = mkLocalId local_meth_name local_meth_ty
+
+        ; return (poly_meth_id, local_meth_id) }
+  where
+    sel_name      = idName sel_id
+    sel_occ       = nameOccName sel_name
+    local_meth_ty = instantiateMethod clas sel_id inst_tys
+    poly_meth_ty  = mkSpecSigmaTy tyvars theta local_meth_ty
+    theta         = map idType dfun_ev_vars
+
+methSigCtxt :: Name -> TcType -> TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc)
+methSigCtxt sel_name sig_ty meth_ty env0
+  = do { (env1, sig_ty)  <- zonkTidyTcType env0 sig_ty
+       ; (env2, meth_ty) <- zonkTidyTcType env1 meth_ty
+       ; let msg = hang (text "When checking that instance signature for" <+> quotes (ppr sel_name))
+                      2 (vcat [ text "is more general than its signature in the class"
+                              , text "Instance sig:" <+> ppr sig_ty
+                              , text "   Class sig:" <+> ppr meth_ty ])
+       ; return (env2, msg) }
+
+misplacedInstSig :: Name -> LHsSigType GhcRn -> SDoc
+misplacedInstSig name hs_ty
+  = vcat [ hang (text "Illegal type signature in instance declaration:")
+              2 (hang (pprPrefixName name)
+                    2 (dcolon <+> ppr hs_ty))
+         , text "(Use InstanceSigs to allow this)" ]
+
+{- Note [Instance method signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+With -XInstanceSigs we allow the user to supply a signature for the
+method in an instance declaration.  Here is an artificial example:
+
+       data T a = MkT a
+       instance Ord a => Ord (T a) where
+         (>) :: forall b. b -> b -> Bool
+         (>) = error "You can't compare Ts"
+
+The instance signature can be *more* polymorphic than the instantiated
+class method (in this case: Age -> Age -> Bool), but it cannot be less
+polymorphic.  Moreover, if a signature is given, the implementation
+code should match the signature, and type variables bound in the
+singature should scope over the method body.
+
+We achieve this by building a TcSigInfo for the method, whether or not
+there is an instance method signature, and using that to typecheck
+the declaration (in tcMethodBody).  That means, conveniently,
+that the type variables bound in the signature will scope over the body.
+
+What about the check that the instance method signature is more
+polymorphic than the instantiated class method type?  We just do a
+tcSubType call in tcMethodBodyHelp, and generate a nested AbsBind, like
+this (for the example above
+
+ AbsBind { abs_tvs = [a], abs_ev_vars = [d:Ord a]
+         , abs_exports
+             = ABExport { (>) :: forall a. Ord a => T a -> T a -> Bool
+                        , gr_lcl :: T a -> T a -> Bool }
+         , abs_binds
+             = AbsBind { abs_tvs = [], abs_ev_vars = []
+                       , abs_exports = ABExport { gr_lcl :: T a -> T a -> Bool
+                                                , gr_inner :: forall b. b -> b -> Bool }
+                       , abs_binds = AbsBind { abs_tvs = [b], abs_ev_vars = []
+                                             , ..etc.. }
+               } }
+
+Wow!  Three nested AbsBinds!
+ * The outer one abstracts over the tyvars and dicts for the instance
+ * The middle one is only present if there is an instance signature,
+   and does the impedance matching for that signature
+ * The inner one is for the method binding itself against either the
+   signature from the class, or the instance signature.
+-}
+
+----------------------
+mk_meth_spec_prags :: Id -> [LTcSpecPrag] -> [LTcSpecPrag] -> TcSpecPrags
+        -- Adapt the 'SPECIALISE instance' pragmas to work for this method Id
+        -- There are two sources:
+        --   * spec_prags_for_me: {-# SPECIALISE op :: <blah> #-}
+        --   * spec_prags_from_inst: derived from {-# SPECIALISE instance :: <blah> #-}
+        --     These ones have the dfun inside, but [perhaps surprisingly]
+        --     the correct wrapper.
+        -- See Note [Handling SPECIALISE pragmas] in GHC.Tc.Gen.Bind
+mk_meth_spec_prags meth_id spec_inst_prags spec_prags_for_me
+  = SpecPrags (spec_prags_for_me ++ spec_prags_from_inst)
+  where
+    spec_prags_from_inst
+       | isInlinePragma (idInlinePragma meth_id)
+       = []  -- Do not inherit SPECIALISE from the instance if the
+             -- method is marked INLINE, because then it'll be inlined
+             -- and the specialisation would do nothing. (Indeed it'll provoke
+             -- a warning from the desugarer
+       | otherwise
+       = [ L inst_loc (SpecPrag meth_id wrap inl)
+         | L inst_loc (SpecPrag _       wrap inl) <- spec_inst_prags]
+
+
+mkDefMethBind :: Class -> [Type] -> Id -> Name
+              -> TcM (LHsBind GhcRn, [LSig GhcRn])
+-- The is a default method (vanailla or generic) defined in the class
+-- So make a binding   op = $dmop @t1 @t2
+-- where $dmop is the name of the default method in the class,
+-- and t1,t2 are the instance types.
+-- See Note [Default methods in instances] for why we use
+-- visible type application here
+mkDefMethBind clas inst_tys sel_id dm_name
+  = do  { dflags <- getDynFlags
+        ; dm_id <- tcLookupId dm_name
+        ; let inline_prag = idInlinePragma dm_id
+              inline_prags | isAnyInlinePragma inline_prag
+                           = [noLoc (InlineSig noExtField fn inline_prag)]
+                           | otherwise
+                           = []
+                 -- Copy the inline pragma (if any) from the default method
+                 -- to this version. Note [INLINE and default methods]
+
+              fn   = noLoc (idName sel_id)
+              visible_inst_tys = [ ty | (tcb, ty) <- tyConBinders (classTyCon clas) `zip` inst_tys
+                                      , tyConBinderArgFlag tcb /= Inferred ]
+              rhs  = foldl' mk_vta (nlHsVar dm_name) visible_inst_tys
+              bind = noLoc $ mkTopFunBind Generated fn $
+                             [mkSimpleMatch (mkPrefixFunRhs fn) [] rhs]
+
+        ; liftIO (dumpIfSet_dyn dflags Opt_D_dump_deriv "Filling in method body"
+                   FormatHaskell
+                   (vcat [ppr clas <+> ppr inst_tys,
+                          nest 2 (ppr sel_id <+> equals <+> ppr rhs)]))
+
+       ; return (bind, inline_prags) }
+  where
+    mk_vta :: LHsExpr GhcRn -> Type -> LHsExpr GhcRn
+    mk_vta fun ty = noLoc (HsAppType noExtField fun (mkEmptyWildCardBndrs $ nlHsParTy
+                                                $ noLoc $ XHsType $ NHsCoreTy ty))
+       -- NB: use visible type application
+       -- See Note [Default methods in instances]
+
+----------------------
+derivBindCtxt :: Id -> Class -> [Type ] -> SDoc
+derivBindCtxt sel_id clas tys
+   = vcat [ text "When typechecking the code for" <+> quotes (ppr sel_id)
+          , nest 2 (text "in a derived instance for"
+                    <+> quotes (pprClassPred clas tys) <> colon)
+          , nest 2 $ text "To see the code I am typechecking, use -ddump-deriv" ]
+
+warnUnsatisfiedMinimalDefinition :: ClassMinimalDef -> TcM ()
+warnUnsatisfiedMinimalDefinition mindef
+  = do { warn <- woptM Opt_WarnMissingMethods
+       ; warnTc (Reason Opt_WarnMissingMethods) warn message
+       }
+  where
+    message = vcat [text "No explicit implementation for"
+                   ,nest 2 $ pprBooleanFormulaNice mindef
+                   ]
+
+{-
+Note [Export helper functions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We arrange to export the "helper functions" of an instance declaration,
+so that they are not subject to preInlineUnconditionally, even if their
+RHS is trivial.  Reason: they are mentioned in the DFunUnfolding of
+the dict fun as Ids, not as CoreExprs, so we can't substitute a
+non-variable for them.
+
+We could change this by making DFunUnfoldings have CoreExprs, but it
+seems a bit simpler this way.
+
+Note [Default methods in instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this
+
+   class Baz v x where
+      foo :: x -> x
+      foo y = <blah>
+
+   instance Baz Int Int
+
+From the class decl we get
+
+   $dmfoo :: forall v x. Baz v x => x -> x
+   $dmfoo y = <blah>
+
+Notice that the type is ambiguous.  So we use Visible Type Application
+to disambiguate:
+
+   $dBazIntInt = MkBaz fooIntInt
+   fooIntInt = $dmfoo @Int @Int
+
+Lacking VTA we'd get ambiguity errors involving the default method.  This applies
+equally to vanilla default methods (#1061) and generic default methods
+(#12220).
+
+Historical note: before we had VTA we had to generate
+post-type-checked code, which took a lot more code, and didn't work for
+generic default methods.
+
+Note [INLINE and default methods]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Default methods need special case.  They are supposed to behave rather like
+macros.  For example
+
+  class Foo a where
+    op1, op2 :: Bool -> a -> a
+
+    {-# INLINE op1 #-}
+    op1 b x = op2 (not b) x
+
+  instance Foo Int where
+    -- op1 via default method
+    op2 b x = <blah>
+
+The instance declaration should behave
+
+   just as if 'op1' had been defined with the
+   code, and INLINE pragma, from its original
+   definition.
+
+That is, just as if you'd written
+
+  instance Foo Int where
+    op2 b x = <blah>
+
+    {-# INLINE op1 #-}
+    op1 b x = op2 (not b) x
+
+So for the above example we generate:
+
+  {-# INLINE $dmop1 #-}
+  -- $dmop1 has an InlineCompulsory unfolding
+  $dmop1 d b x = op2 d (not b) x
+
+  $fFooInt = MkD $cop1 $cop2
+
+  {-# INLINE $cop1 #-}
+  $cop1 = $dmop1 $fFooInt
+
+  $cop2 = <blah>
+
+Note carefully:
+
+* We *copy* any INLINE pragma from the default method $dmop1 to the
+  instance $cop1.  Otherwise we'll just inline the former in the
+  latter and stop, which isn't what the user expected
+
+* Regardless of its pragma, we give the default method an
+  unfolding with an InlineCompulsory source. That means
+  that it'll be inlined at every use site, notably in
+  each instance declaration, such as $cop1.  This inlining
+  must happen even though
+    a) $dmop1 is not saturated in $cop1
+    b) $cop1 itself has an INLINE pragma
+
+  It's vital that $dmop1 *is* inlined in this way, to allow the mutual
+  recursion between $fooInt and $cop1 to be broken
+
+* To communicate the need for an InlineCompulsory to the desugarer
+  (which makes the Unfoldings), we use the IsDefaultMethod constructor
+  in TcSpecPrags.
+
+
+************************************************************************
+*                                                                      *
+        Specialise instance pragmas
+*                                                                      *
+************************************************************************
+
+Note [SPECIALISE instance pragmas]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+
+   instance (Ix a, Ix b) => Ix (a,b) where
+     {-# SPECIALISE instance Ix (Int,Int) #-}
+     range (x,y) = ...
+
+We make a specialised version of the dictionary function, AND
+specialised versions of each *method*.  Thus we should generate
+something like this:
+
+  $dfIxPair :: (Ix a, Ix b) => Ix (a,b)
+  {-# DFUN [$crangePair, ...] #-}
+  {-# SPECIALISE $dfIxPair :: Ix (Int,Int) #-}
+  $dfIxPair da db = Ix ($crangePair da db) (...other methods...)
+
+  $crange :: (Ix a, Ix b) -> ((a,b),(a,b)) -> [(a,b)]
+  {-# SPECIALISE $crange :: ((Int,Int),(Int,Int)) -> [(Int,Int)] #-}
+  $crange da db = <blah>
+
+The SPECIALISE pragmas are acted upon by the desugarer, which generate
+
+  dii :: Ix Int
+  dii = ...
+
+  $s$dfIxPair :: Ix ((Int,Int),(Int,Int))
+  {-# DFUN [$crangePair di di, ...] #-}
+  $s$dfIxPair = Ix ($crangePair di di) (...)
+
+  {-# RULE forall (d1,d2:Ix Int). $dfIxPair Int Int d1 d2 = $s$dfIxPair #-}
+
+  $s$crangePair :: ((Int,Int),(Int,Int)) -> [(Int,Int)]
+  $c$crangePair = ...specialised RHS of $crangePair...
+
+  {-# RULE forall (d1,d2:Ix Int). $crangePair Int Int d1 d2 = $s$crangePair #-}
+
+Note that
+
+  * The specialised dictionary $s$dfIxPair is very much needed, in case we
+    call a function that takes a dictionary, but in a context where the
+    specialised dictionary can be used.  See #7797.
+
+  * The ClassOp rule for 'range' works equally well on $s$dfIxPair, because
+    it still has a DFunUnfolding.  See Note [ClassOp/DFun selection]
+
+  * A call (range ($dfIxPair Int Int d1 d2)) might simplify two ways:
+       --> {ClassOp rule for range}     $crangePair Int Int d1 d2
+       --> {SPEC rule for $crangePair}  $s$crangePair
+    or thus:
+       --> {SPEC rule for $dfIxPair}    range $s$dfIxPair
+       --> {ClassOpRule for range}      $s$crangePair
+    It doesn't matter which way.
+
+  * We want to specialise the RHS of both $dfIxPair and $crangePair,
+    but the SAME HsWrapper will do for both!  We can call tcSpecPrag
+    just once, and pass the result (in spec_inst_info) to tcMethods.
+-}
+
+tcSpecInstPrags :: DFunId -> InstBindings GhcRn
+                -> TcM ([Located TcSpecPrag], TcPragEnv)
+tcSpecInstPrags dfun_id (InstBindings { ib_binds = binds, ib_pragmas = uprags })
+  = do { spec_inst_prags <- mapM (wrapLocM (tcSpecInst dfun_id)) $
+                            filter isSpecInstLSig uprags
+             -- The filter removes the pragmas for methods
+       ; return (spec_inst_prags, mkPragEnv uprags binds) }
+
+------------------------------
+tcSpecInst :: Id -> Sig GhcRn -> TcM TcSpecPrag
+tcSpecInst dfun_id prag@(SpecInstSig _ _ hs_ty)
+  = addErrCtxt (spec_ctxt prag) $
+    do  { spec_dfun_ty <- tcHsClsInstType SpecInstCtxt hs_ty
+        ; co_fn <- tcSpecWrapper SpecInstCtxt (idType dfun_id) spec_dfun_ty
+        ; return (SpecPrag dfun_id co_fn defaultInlinePragma) }
+  where
+    spec_ctxt prag = hang (text "In the pragma:") 2 (ppr prag)
+
+tcSpecInst _  _ = panic "tcSpecInst"
+
+{-
+************************************************************************
+*                                                                      *
+\subsection{Error messages}
+*                                                                      *
+************************************************************************
+-}
+
+instDeclCtxt1 :: LHsSigType GhcRn -> SDoc
+instDeclCtxt1 hs_inst_ty
+  = inst_decl_ctxt (ppr (getLHsInstDeclHead hs_inst_ty))
+
+instDeclCtxt2 :: Type -> SDoc
+instDeclCtxt2 dfun_ty
+  = inst_decl_ctxt (ppr (mkClassPred cls tys))
+  where
+    (_,_,cls,tys) = tcSplitDFunTy dfun_ty
+
+inst_decl_ctxt :: SDoc -> SDoc
+inst_decl_ctxt doc = hang (text "In the instance declaration for")
+                        2 (quotes doc)
+
+badBootFamInstDeclErr :: SDoc
+badBootFamInstDeclErr
+  = text "Illegal family instance in hs-boot file"
+
+notFamily :: TyCon -> SDoc
+notFamily tycon
+  = vcat [ text "Illegal family instance for" <+> quotes (ppr tycon)
+         , nest 2 $ parens (ppr tycon <+> text "is not an indexed type family")]
+
+assocInClassErr :: TyCon -> SDoc
+assocInClassErr name
+ = text "Associated type" <+> quotes (ppr name) <+>
+   text "must be inside a class instance"
+
+badFamInstDecl :: TyCon -> SDoc
+badFamInstDecl tc_name
+  = vcat [ text "Illegal family instance for" <+>
+           quotes (ppr tc_name)
+         , nest 2 (parens $ text "Use TypeFamilies to allow indexed type families") ]
+
+notOpenFamily :: TyCon -> SDoc
+notOpenFamily tc
+  = text "Illegal instance for closed family" <+> quotes (ppr tc)
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs-boot b/compiler/GHC/Tc/TyCl/Instance.hs-boot
new file mode 100644
index 0000000000..1e47211460
--- /dev/null
+++ b/compiler/GHC/Tc/TyCl/Instance.hs-boot
@@ -0,0 +1,16 @@
+{-
+(c) The University of Glasgow 2006
+(c) The GRASP/AQUA Project, Glasgow University, 1992-1998
+-}
+
+module GHC.Tc.TyCl.Instance ( tcInstDecls1 ) where
+
+import GHC.Hs
+import GHC.Tc.Types
+import GHC.Tc.Utils.Env( InstInfo )
+import GHC.Tc.Deriv
+
+-- We need this because of the mutual recursion
+-- between GHC.Tc.TyCl and GHC.Tc.TyCl.Instance
+tcInstDecls1 :: [LInstDecl GhcRn]
+             -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo])
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs
new file mode 100644
index 0000000000..01b446c88b
--- /dev/null
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs
@@ -0,0 +1,1154 @@
+{-
+(c) The University of Glasgow 2006
+(c) The GRASP/AQUA Project, Glasgow University, 1992-1998
+
+-}
+
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ViewPatterns #-}
+
+{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
+
+-- | Typechecking pattern synonym declarations
+module GHC.Tc.TyCl.PatSyn
+   ( tcPatSynDecl
+   , tcPatSynBuilderBind
+   , tcPatSynBuilderOcc
+   , nonBidirectionalErr
+   )
+where
+
+import GhcPrelude
+
+import GHC.Hs
+import GHC.Tc.Gen.Pat
+import GHC.Core.Type ( tidyTyCoVarBinders, tidyTypes, tidyType )
+import GHC.Tc.Utils.Monad
+import GHC.Tc.Gen.Sig( emptyPragEnv, completeSigFromId )
+import GHC.Tc.Utils.Env
+import GHC.Tc.Utils.TcMType
+import GHC.Tc.Utils.Zonk
+import TysPrim
+import GHC.Types.Name
+import GHC.Types.SrcLoc
+import GHC.Core.PatSyn
+import GHC.Types.Name.Set
+import Panic
+import Outputable
+import FastString
+import GHC.Types.Var
+import GHC.Types.Var.Env( emptyTidyEnv, mkInScopeSet )
+import GHC.Types.Id
+import GHC.Types.Id.Info( RecSelParent(..), setLevityInfoWithType )
+import GHC.Tc.Gen.Bind
+import GHC.Types.Basic
+import GHC.Tc.Solver
+import GHC.Tc.Utils.Unify
+import GHC.Core.Predicate
+import TysWiredIn
+import GHC.Tc.Utils.TcType
+import GHC.Tc.Types.Evidence
+import GHC.Tc.Types.Origin
+import GHC.Tc.TyCl.Build
+import GHC.Types.Var.Set
+import GHC.Types.Id.Make
+import GHC.Tc.TyCl.Utils
+import GHC.Core.ConLike
+import GHC.Types.FieldLabel
+import Bag
+import Util
+import ErrUtils
+import Data.Maybe( mapMaybe )
+import Control.Monad ( zipWithM )
+import Data.List( partition )
+
+#include "HsVersions.h"
+
+{-
+************************************************************************
+*                                                                      *
+                    Type checking a pattern synonym
+*                                                                      *
+************************************************************************
+-}
+
+tcPatSynDecl :: PatSynBind GhcRn GhcRn
+             -> Maybe TcSigInfo
+             -> TcM (LHsBinds GhcTc, TcGblEnv)
+tcPatSynDecl psb mb_sig
+  = recoverM (recoverPSB psb) $
+    case mb_sig of
+      Nothing                 -> tcInferPatSynDecl psb
+      Just (TcPatSynSig tpsi) -> tcCheckPatSynDecl psb tpsi
+      _                       -> panic "tcPatSynDecl"
+
+recoverPSB :: PatSynBind GhcRn GhcRn
+           -> TcM (LHsBinds GhcTc, TcGblEnv)
+-- See Note [Pattern synonym error recovery]
+recoverPSB (PSB { psb_id = L _ name
+                , psb_args = details })
+ = do { matcher_name <- newImplicitBinder name mkMatcherOcc
+      ; let placeholder = AConLike $ PatSynCon $
+                          mk_placeholder matcher_name
+      ; gbl_env <- tcExtendGlobalEnv [placeholder] getGblEnv
+      ; return (emptyBag, gbl_env) }
+  where
+    (_arg_names, _rec_fields, is_infix) = collectPatSynArgInfo details
+    mk_placeholder matcher_name
+      = mkPatSyn name is_infix
+                        ([mkTyVarBinder Specified alphaTyVar], []) ([], [])
+                        [] -- Arg tys
+                        alphaTy
+                        (matcher_id, True) Nothing
+                        []  -- Field labels
+       where
+         -- The matcher_id is used only by the desugarer, so actually
+         -- and error-thunk would probably do just as well here.
+         matcher_id = mkLocalId matcher_name $
+                      mkSpecForAllTys [alphaTyVar] alphaTy
+
+recoverPSB (XPatSynBind nec) = noExtCon nec
+
+{- Note [Pattern synonym error recovery]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If type inference for a pattern synonym fails, we can't continue with
+the rest of tc_patsyn_finish, because we may get knock-on errors, or
+even a crash.  E.g. from
+   pattern What = True :: Maybe
+we get a kind error; and we must stop right away (#15289).
+
+We stop if there are /any/ unsolved constraints, not just insoluble
+ones; because pattern synonyms are top-level things, we will never
+solve them later if we can't solve them now.  And if we were to carry
+on, tc_patsyn_finish does zonkTcTypeToType, which defaults any
+unsolved unificatdion variables to Any, which confuses the error
+reporting no end (#15685).
+
+So we use simplifyTop to completely solve the constraint, report
+any errors, throw an exception.
+
+Even in the event of such an error we can recover and carry on, just
+as we do for value bindings, provided we plug in placeholder for the
+pattern synonym: see recoverPSB.  The goal of the placeholder is not
+to cause a raft of follow-on errors.  I've used the simplest thing for
+now, but we might need to elaborate it a bit later.  (e.g.  I've given
+it zero args, which may cause knock-on errors if it is used in a
+pattern.) But it'll do for now.
+
+-}
+
+tcInferPatSynDecl :: PatSynBind GhcRn GhcRn
+                  -> TcM (LHsBinds GhcTc, TcGblEnv)
+tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details
+                       , psb_def = lpat, psb_dir = dir })
+  = addPatSynCtxt lname $
+    do { traceTc "tcInferPatSynDecl {" $ ppr name
+
+       ; let (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
+       ; (tclvl, wanted, ((lpat', args), pat_ty))
+            <- pushLevelAndCaptureConstraints  $
+               tcInferNoInst                   $ \ exp_ty ->
+               tcPat PatSyn lpat exp_ty        $
+               mapM tcLookupId arg_names
+
+       ; let (ex_tvs, prov_dicts) = tcCollectEx lpat'
+
+             named_taus = (name, pat_ty) : map mk_named_tau args
+             mk_named_tau arg
+               = (getName arg, mkSpecForAllTys ex_tvs (varType arg))
+               -- The mkSpecForAllTys is important (#14552), albeit
+               -- slightly artificial (there is no variable with this funny type).
+               -- We do not want to quantify over variable (alpha::k)
+               -- that mention the existentially-bound type variables
+               -- ex_tvs in its kind k.
+               -- See Note [Type variables whose kind is captured]
+
+       ; (univ_tvs, req_dicts, ev_binds, residual, _)
+               <- simplifyInfer tclvl NoRestrictions [] named_taus wanted
+       ; top_ev_binds <- checkNoErrs (simplifyTop residual)
+       ; addTopEvBinds top_ev_binds $
+
+    do { prov_dicts <- mapM zonkId prov_dicts
+       ; let filtered_prov_dicts = mkMinimalBySCs evVarPred prov_dicts
+             -- Filtering: see Note [Remove redundant provided dicts]
+             (prov_theta, prov_evs)
+                 = unzip (mapMaybe mkProvEvidence filtered_prov_dicts)
+             req_theta = map evVarPred req_dicts
+
+       -- Report coercions that escape
+       -- See Note [Coercions that escape]
+       ; args <- mapM zonkId args
+       ; let bad_args = [ (arg, bad_cos) | arg <- args ++ prov_dicts
+                              , let bad_cos = filterDVarSet isId $
+                                              (tyCoVarsOfTypeDSet (idType arg))
+                              , not (isEmptyDVarSet bad_cos) ]
+       ; mapM_ dependentArgErr bad_args
+
+       ; traceTc "tcInferPatSynDecl }" $ (ppr name $$ ppr ex_tvs)
+       ; tc_patsyn_finish lname dir is_infix lpat'
+                          (mkTyVarBinders Inferred univ_tvs
+                            , req_theta,  ev_binds, req_dicts)
+                          (mkTyVarBinders Inferred ex_tvs
+                            , mkTyVarTys ex_tvs, prov_theta, prov_evs)
+                          (map nlHsVar args, map idType args)
+                          pat_ty rec_fields } }
+tcInferPatSynDecl (XPatSynBind nec) = noExtCon nec
+
+mkProvEvidence :: EvId -> Maybe (PredType, EvTerm)
+-- See Note [Equality evidence in pattern synonyms]
+mkProvEvidence ev_id
+  | EqPred r ty1 ty2 <- classifyPredType pred
+  , let k1 = tcTypeKind ty1
+        k2 = tcTypeKind ty2
+        is_homo = k1 `tcEqType` k2
+        homo_tys   = [k1, ty1, ty2]
+        hetero_tys = [k1, k2, ty1, ty2]
+  = case r of
+      ReprEq | is_homo
+             -> Just ( mkClassPred coercibleClass    homo_tys
+                     , evDataConApp coercibleDataCon homo_tys eq_con_args )
+             | otherwise -> Nothing
+      NomEq  | is_homo
+             -> Just ( mkClassPred eqClass    homo_tys
+                     , evDataConApp eqDataCon homo_tys eq_con_args )
+             | otherwise
+             -> Just ( mkClassPred heqClass    hetero_tys
+                     , evDataConApp heqDataCon hetero_tys eq_con_args )
+
+  | otherwise
+  = Just (pred, EvExpr (evId ev_id))
+  where
+    pred = evVarPred ev_id
+    eq_con_args = [evId ev_id]
+
+dependentArgErr :: (Id, DTyCoVarSet) -> TcM ()
+-- See Note [Coercions that escape]
+dependentArgErr (arg, bad_cos)
+  = addErrTc $
+    vcat [ text "Iceland Jack!  Iceland Jack! Stop torturing me!"
+         , hang (text "Pattern-bound variable")
+              2 (ppr arg <+> dcolon <+> ppr (idType arg))
+         , nest 2 $
+           hang (text "has a type that mentions pattern-bound coercion"
+                 <> plural bad_co_list <> colon)
+              2 (pprWithCommas ppr bad_co_list)
+         , text "Hint: use -fprint-explicit-coercions to see the coercions"
+         , text "Probable fix: add a pattern signature" ]
+  where
+    bad_co_list = dVarSetElems bad_cos
+
+{- Note [Type variables whose kind is captured]
+~~-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  data AST a = Sym [a]
+  class Prj s where { prj :: [a] -> Maybe (s a) }
+  pattern P x <= Sym (prj -> Just x)
+
+Here we get a matcher with this type
+  $mP :: forall s a. Prj s => AST a -> (s a -> r) -> r -> r
+
+No problem.  But note that 's' is not fixed by the type of the
+pattern (AST a), nor is it existentially bound.  It's really only
+fixed by the type of the continuation.
+
+#14552 showed that this can go wrong if the kind of 's' mentions
+existentially bound variables.  We obviously can't make a type like
+  $mP :: forall (s::k->*) a. Prj s => AST a -> (forall k. s a -> r)
+                                   -> r -> r
+But neither is 's' itself existentially bound, so the forall (s::k->*)
+can't go in the inner forall either.  (What would the matcher apply
+the continuation to?)
+
+Solution: do not quantiify over any unification variable whose kind
+mentions the existentials.  We can conveniently do that by making the
+"taus" passed to simplifyInfer look like
+   forall ex_tvs. arg_ty
+
+After that, Note [Naughty quantification candidates] in GHC.Tc.Utils.TcMType takes
+over and errors.
+
+Note [Remove redundant provided dicts]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Recall that
+   HRefl :: forall k1 k2 (a1:k1) (a2:k2). (k1 ~ k2, a1 ~ a2)
+                                       => a1 :~~: a2
+(NB: technically the (k1~k2) existential dictionary is not necessary,
+but it's there at the moment.)
+
+Now consider (#14394):
+   pattern Foo = HRefl
+in a non-poly-kinded module.  We don't want to get
+    pattern Foo :: () => (* ~ *, b ~ a) => a :~~: b
+with that redundant (* ~ *).  We'd like to remove it; hence the call to
+mkMinimalWithSCs.
+
+Similarly consider
+  data S a where { MkS :: Ord a => a -> S a }
+  pattern Bam x y <- (MkS (x::a), MkS (y::a)))
+
+The pattern (Bam x y) binds two (Ord a) dictionaries, but we only
+need one.  Again mkMimimalWithSCs removes the redundant one.
+
+Note [Equality evidence in pattern synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  data X a where
+     MkX :: Eq a => [a] -> X (Maybe a)
+  pattern P x = MkG x
+
+Then there is a danger that GHC will infer
+  P :: forall a.  () =>
+       forall b. (a ~# Maybe b, Eq b) => [b] -> X a
+
+The 'builder' for P, which is called in user-code, will then
+have type
+  $bP :: forall a b. (a ~# Maybe b, Eq b) => [b] -> X a
+
+and that is bad because (a ~# Maybe b) is not a predicate type
+(see Note [Types for coercions, predicates, and evidence] in GHC.Core.TyCo.Rep
+and is not implicitly instantiated.
+
+So in mkProvEvidence we lift (a ~# b) to (a ~ b).  Tiresome, and
+marginally less efficient, if the builder/martcher are not inlined.
+
+See also Note [Lift equality constraints when quantifying] in GHC.Tc.Utils.TcType
+
+Note [Coercions that escape]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+#14507 showed an example where the inferred type of the matcher
+for the pattern synonym was something like
+   $mSO :: forall (r :: TYPE rep) kk (a :: k).
+           TypeRep k a
+           -> ((Bool ~ k) => TypeRep Bool (a |> co_a2sv) -> r)
+           -> (Void# -> r)
+           -> r
+
+What is that co_a2sv :: Bool ~# *??  It was bound (via a superclass
+selection) by the pattern being matched; and indeed it is implicit in
+the context (Bool ~ k).  You could imagine trying to extract it like
+this:
+   $mSO :: forall (r :: TYPE rep) kk (a :: k).
+           TypeRep k a
+           -> ( co :: ((Bool :: *) ~ (k :: *)) =>
+                  let co_a2sv = sc_sel co
+                  in TypeRep Bool (a |> co_a2sv) -> r)
+           -> (Void# -> r)
+           -> r
+
+But we simply don't allow that in types.  Maybe one day but not now.
+
+How to detect this situation?  We just look for free coercion variables
+in the types of any of the arguments to the matcher.  The error message
+is not very helpful, but at least we don't get a Lint error.
+-}
+
+tcCheckPatSynDecl :: PatSynBind GhcRn GhcRn
+                  -> TcPatSynInfo
+                  -> TcM (LHsBinds GhcTc, TcGblEnv)
+tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
+                         , psb_def = lpat, psb_dir = dir }
+                  TPSI{ patsig_implicit_bndrs = implicit_tvs
+                      , patsig_univ_bndrs = explicit_univ_tvs, patsig_prov = prov_theta
+                      , patsig_ex_bndrs   = explicit_ex_tvs,   patsig_req  = req_theta
+                      , patsig_body_ty    = sig_body_ty }
+  = addPatSynCtxt lname $
+    do { let decl_arity = length arg_names
+             (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
+
+       ; traceTc "tcCheckPatSynDecl" $
+         vcat [ ppr implicit_tvs, ppr explicit_univ_tvs, ppr req_theta
+              , ppr explicit_ex_tvs, ppr prov_theta, ppr sig_body_ty ]
+
+       ; (arg_tys, pat_ty) <- case tcSplitFunTysN decl_arity sig_body_ty of
+                                 Right stuff  -> return stuff
+                                 Left missing -> wrongNumberOfParmsErr name decl_arity missing
+
+       -- Complain about:  pattern P :: () => forall x. x -> P x
+       -- The existential 'x' should not appear in the result type
+       -- Can't check this until we know P's arity
+       ; let bad_tvs = filter (`elemVarSet` tyCoVarsOfType pat_ty) explicit_ex_tvs
+       ; checkTc (null bad_tvs) $
+         hang (sep [ text "The result type of the signature for" <+> quotes (ppr name) <> comma
+                   , text "namely" <+> quotes (ppr pat_ty) ])
+            2 (text "mentions existential type variable" <> plural bad_tvs
+               <+> pprQuotedList bad_tvs)
+
+         -- See Note [The pattern-synonym signature splitting rule] in GHC.Tc.Gen.Sig
+       ; let univ_fvs = closeOverKinds $
+                        (tyCoVarsOfTypes (pat_ty : req_theta) `extendVarSetList` explicit_univ_tvs)
+             (extra_univ, extra_ex) = partition ((`elemVarSet` univ_fvs) . binderVar) implicit_tvs
+             univ_bndrs = extra_univ ++ mkTyVarBinders Specified explicit_univ_tvs
+             ex_bndrs   = extra_ex   ++ mkTyVarBinders Specified explicit_ex_tvs
+             univ_tvs   = binderVars univ_bndrs
+             ex_tvs     = binderVars ex_bndrs
+
+       -- 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_tvs', prov_dicts, args'))) <-
+           ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys )
+           pushLevelAndCaptureConstraints            $
+           tcExtendTyVarEnv univ_tvs                 $
+           tcPat PatSyn lpat (mkCheckExpType pat_ty) $
+           do { let in_scope    = mkInScopeSet (mkVarSet univ_tvs)
+                    empty_subst = mkEmptyTCvSubst in_scope
+              ; (subst, ex_tvs') <- mapAccumLM newMetaTyVarX empty_subst ex_tvs
+                    -- newMetaTyVarX: see the "Existential type variables"
+                    -- part of Note [Checking against a pattern signature]
+              ; traceTc "tcpatsyn1" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs])
+              ; traceTc "tcpatsyn2" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs'])
+              ; let prov_theta' = substTheta subst prov_theta
+                  -- Add univ_tvs to the in_scope set to
+                  -- satisfy the substitution invariant. There's no need to
+                  -- add 'ex_tvs' as they are already in the domain of the
+                  -- substitution.
+                  -- See also Note [The substitution invariant] in GHC.Core.TyCo.Subst.
+              ; prov_dicts <- mapM (emitWanted (ProvCtxtOrigin psb)) prov_theta'
+              ; args'      <- zipWithM (tc_arg subst) arg_names arg_tys
+              ; return (ex_tvs', prov_dicts, args') }
+
+       ; let skol_info = SigSkol (PatSynCtxt name) pat_ty []
+                         -- The type here is a bit bogus, but we do not print
+                         -- the type for PatSynCtxt, so it doesn't matter
+                         -- See Note [Skolem info for pattern synonyms] in Origin
+       ; (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 (#10997)
+       ; simplifyTopImplic 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_bndrs, req_theta, ev_binds, req_dicts)
+                          (ex_bndrs, mkTyVarTys ex_tvs', prov_theta, prov_dicts)
+                          (args', arg_tys)
+                          pat_ty rec_fields }
+  where
+    tc_arg :: TCvSubst -> Name -> Type -> TcM (LHsExpr GhcTcId)
+    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
+           ; wrap <- tcSubType_NC GenSigCtxt
+                                 (idType arg_id)
+                                 (substTyUnchecked subst arg_ty)
+                -- Why do we need tcSubType here?
+                -- See Note [Pattern synonyms and higher rank types]
+           ; return (mkLHsWrap wrap $ nlHsVar arg_id) }
+tcCheckPatSynDecl (XPatSynBind nec) _ = noExtCon nec
+
+{- [Pattern synonyms and higher rank types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  data T = MkT (forall a. a->a)
+
+  pattern P :: (Int -> Int) -> T
+  pattern P x <- MkT x
+
+This should work.  But in the matcher we must match against MkT, and then
+instantiate its argument 'x', to get a function of type (Int -> Int).
+Equality is not enough!  #13752 was an example.
+
+
+Note [The pattern-synonym signature splitting rule]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Given a pattern signature, we must split
+     the kind-generalised variables, and
+     the implicitly-bound variables
+into universal and existential.  The rule is this
+(see discussion on #11224):
+
+     The universal tyvars are the ones mentioned in
+          - univ_tvs: the user-specified (forall'd) universals
+          - req_theta
+          - res_ty
+     The existential tyvars are all the rest
+
+For example
+
+   pattern P :: () => b -> T a
+   pattern P x = ...
+
+Here 'a' is universal, and 'b' is existential.  But there is a wrinkle:
+how do we split the arg_tys from req_ty?  Consider
+
+   pattern Q :: () => b -> S c -> T a
+   pattern Q x = ...
+
+This is an odd example because Q has only one syntactic argument, and
+so presumably is defined by a view pattern matching a function.  But
+it can happen (#11977, #12108).
+
+We don't know Q's arity from the pattern signature, so we have to wait
+until we see the pattern declaration itself before deciding res_ty is,
+and hence which variables are existential and which are universal.
+
+And that in turn is why TcPatSynInfo has a separate field,
+patsig_implicit_bndrs, to capture the implicitly bound type variables,
+because we don't yet know how to split them up.
+
+It's a slight compromise, because it means we don't really know the
+pattern synonym's real signature until we see its declaration.  So,
+for example, in hs-boot file, we may need to think what to do...
+(eg don't have any implicitly-bound variables).
+
+
+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
+actual 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
+
+All this applies when type-checking the /matching/ side of
+a pattern synonym.  What about the /building/ side?
+
+* For Unidirectional, there is no builder
+
+* For ExplicitBidirectional, the builder is completely separate
+  code, typechecked in tcPatSynBuilderBind
+
+* For ImplicitBidirectional, the builder is still typechecked in
+  tcPatSynBuilderBind, by converting the pattern to an expression and
+  typechecking it.
+
+  At one point, for ImplicitBidirectional I used TyVarTvs (instead of
+  TauTvs) in tcCheckPatSynDecl.  But (a) strengthening the check here
+  is redundant since tcPatSynBuilderBind does the job, (b) it was
+  still incomplete (TyVarTvs can unify with each other), and (c) it
+  didn't even work (#13441 was accepted with
+  ExplicitBidirectional, but rejected if expressed in
+  ImplicitBidirectional form.  Conclusion: trying to be too clever is
+  a bad idea.
+-}
+
+collectPatSynArgInfo :: HsPatSynDetails (Located Name)
+                     -> ([Name], [Name], Bool)
+collectPatSynArgInfo details =
+  case details of
+    PrefixCon names      -> (map unLoc names, [], False)
+    InfixCon name1 name2 -> (map unLoc [name1, name2], [], True)
+    RecCon names         -> (vars, sels, False)
+                         where
+                            (vars, sels) = unzip (map splitRecordPatSyn names)
+  where
+    splitRecordPatSyn :: RecordPatSynField (Located Name)
+                      -> (Name, Name)
+    splitRecordPatSyn (RecordPatSynField
+                       { recordPatSynPatVar     = L _ patVar
+                       , recordPatSynSelectorId = L _ selId })
+      = (patVar, selId)
+
+addPatSynCtxt :: Located Name -> TcM a -> TcM a
+addPatSynCtxt (L loc name) thing_inside
+  = setSrcSpan loc $
+    addErrCtxt (text "In the declaration for pattern synonym"
+                <+> quotes (ppr name)) $
+    thing_inside
+
+wrongNumberOfParmsErr :: Name -> Arity -> Arity -> TcM a
+wrongNumberOfParmsErr name decl_arity missing
+  = failWithTc $
+    hang (text "Pattern synonym" <+> quotes (ppr name) <+> ptext (sLit "has")
+          <+> speakNOf decl_arity (text "argument"))
+       2 (text "but its type signature has" <+> int missing <+> text "fewer arrows")
+
+-------------------------
+-- Shared by both tcInferPatSyn and tcCheckPatSyn
+tc_patsyn_finish :: Located Name      -- ^ PatSyn Name
+                 -> HsPatSynDir GhcRn -- ^ PatSyn type (Uni/Bidir/ExplicitBidir)
+                 -> Bool              -- ^ Whether infix
+                 -> LPat GhcTc        -- ^ Pattern of the PatSyn
+                 -> ([TcTyVarBinder], [PredType], TcEvBinds, [EvVar])
+                 -> ([TcTyVarBinder], [TcType], [PredType], [EvTerm])
+                 -> ([LHsExpr GhcTcId], [TcType])   -- ^ Pattern arguments and
+                                                    -- types
+                 -> TcType            -- ^ Pattern type
+                 -> [Name]            -- ^ Selector names
+                 -- ^ Whether fields, empty if not record PatSyn
+                 -> TcM (LHsBinds GhcTc, TcGblEnv)
+tc_patsyn_finish lname dir is_infix lpat'
+                 (univ_tvs, req_theta, req_ev_binds, req_dicts)
+                 (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
+
+         (ze, univ_tvs') <- zonkTyVarBinders univ_tvs
+       ; req_theta'      <- zonkTcTypesToTypesX ze req_theta
+       ; (ze, ex_tvs')   <- zonkTyVarBindersX ze ex_tvs
+       ; prov_theta'     <- zonkTcTypesToTypesX ze prov_theta
+       ; pat_ty'         <- zonkTcTypeToTypeX ze pat_ty
+       ; arg_tys'        <- zonkTcTypesToTypesX ze arg_tys
+
+       ; let (env1, univ_tvs) = tidyTyCoVarBinders emptyTidyEnv univ_tvs'
+             (env2, ex_tvs)   = tidyTyCoVarBinders env1 ex_tvs'
+             req_theta  = tidyTypes env2 req_theta'
+             prov_theta = tidyTypes env2 prov_theta'
+             arg_tys    = tidyTypes env2 arg_tys'
+             pat_ty     = tidyType  env2 pat_ty'
+
+       ; traceTc "tc_patsyn_finish {" $
+           ppr (unLoc lname) $$ ppr (unLoc lpat') $$
+           ppr (univ_tvs, req_theta, req_ev_binds, req_dicts) $$
+           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'
+                                         (binderVars univ_tvs, req_theta, req_ev_binds, req_dicts)
+                                         (binderVars ex_tvs, ex_tys, prov_theta, prov_dicts)
+                                         (args, arg_tys)
+                                         pat_ty
+
+       -- Make the 'builder'
+       ; builder_id <- mkPatSynBuilderId dir lname
+                                         univ_tvs req_theta
+                                         ex_tvs   prov_theta
+                                         arg_tys pat_ty
+
+         -- TODO: Make this have the proper information
+       ; let mkFieldLabel name = FieldLabel { flLabel = occNameFS (nameOccName name)
+                                            , flIsOverloaded = False
+                                            , flSelector = name }
+             field_labels' = map mkFieldLabel field_labels
+
+
+       -- Make the PatSyn itself
+       ; let patSyn = mkPatSyn (unLoc lname) is_infix
+                        (univ_tvs, req_theta)
+                        (ex_tvs, prov_theta)
+                        arg_tys
+                        pat_ty
+                        matcher_id builder_id
+                        field_labels'
+
+       -- Selectors
+       ; let rn_rec_sel_binds = mkPatSynRecSelBinds patSyn (patSynFieldLabels patSyn)
+             tything = AConLike (PatSynCon patSyn)
+       ; tcg_env <- tcExtendGlobalEnv [tything] $
+                    tcRecSelBinds rn_rec_sel_binds
+
+       ; traceTc "tc_patsyn_finish }" empty
+       ; return (matcher_bind, tcg_env) }
+
+{-
+************************************************************************
+*                                                                      *
+         Constructing the "matcher" Id and its binding
+*                                                                      *
+************************************************************************
+-}
+
+tcPatSynMatcher :: Located Name
+                -> LPat GhcTc
+                -> ([TcTyVar], ThetaType, TcEvBinds, [EvVar])
+                -> ([TcTyVar], [TcType], ThetaType, [EvTerm])
+                -> ([LHsExpr GhcTcId], [TcType])
+                -> TcType
+                -> TcM ((Id, Bool), LHsBinds GhcTc)
+-- See Note [Matchers and builders for pattern synonyms] in GHC.Core.PatSyn
+tcPatSynMatcher (L loc name) lpat
+                (univ_tvs, req_theta, req_ev_binds, req_dicts)
+                (ex_tvs, ex_tys, prov_theta, prov_dicts)
+                (args, arg_tys) pat_ty
+  = do { rr_name <- newNameAt (mkTyVarOcc "rep") loc
+       ; tv_name <- newNameAt (mkTyVarOcc "r")   loc
+       ; let rr_tv  = mkTyVar rr_name runtimeRepTy
+             rr     = mkTyVarTy rr_tv
+             res_tv = mkTyVar tv_name (tYPE rr)
+             res_ty = mkTyVarTy res_tv
+             is_unlifted = null args && null prov_dicts
+             (cont_args, cont_arg_tys)
+               | is_unlifted = ([nlHsVar voidPrimId], [voidPrimTy])
+               | otherwise   = (args,                 arg_tys)
+             cont_ty = mkInfSigmaTy ex_tvs prov_theta $
+                       mkVisFunTys cont_arg_tys res_ty
+
+             fail_ty  = mkVisFunTy voidPrimTy res_ty
+
+       ; matcher_name <- newImplicitBinder name mkMatcherOcc
+       ; scrutinee    <- newSysLocalId (fsLit "scrut") pat_ty
+       ; cont         <- newSysLocalId (fsLit "cont")  cont_ty
+       ; fail         <- newSysLocalId (fsLit "fail")  fail_ty
+
+       ; let matcher_tau   = mkVisFunTys [pat_ty, cont_ty, fail_ty] res_ty
+             matcher_sigma = mkInfSigmaTy (rr_tv:res_tv:univ_tvs) req_theta matcher_tau
+             matcher_id    = mkExportedVanillaId matcher_name matcher_sigma
+                             -- See Note [Exported LocalIds] in GHC.Types.Id
+
+             inst_wrap = mkWpEvApps prov_dicts <.> mkWpTyApps ex_tys
+             cont' = foldl' nlHsApp (mkLHsWrap inst_wrap (nlHsVar cont)) cont_args
+
+             fail' = nlHsApps fail [nlHsVar voidPrimId]
+
+             args = map nlVarPat [scrutinee, cont, fail]
+             lwpat = noLoc $ WildPat pat_ty
+             cases = if isIrrefutableHsPat lpat
+                     then [mkHsCaseAlt lpat  cont']
+                     else [mkHsCaseAlt lpat  cont',
+                           mkHsCaseAlt lwpat fail']
+             body = mkLHsWrap (mkWpLet req_ev_binds) $
+                    L (getLoc lpat) $
+                    HsCase noExtField (nlHsVar scrutinee) $
+                    MG{ mg_alts = L (getLoc lpat) cases
+                      , mg_ext = MatchGroupTc [pat_ty] res_ty
+                      , mg_origin = Generated
+                      }
+             body' = noLoc $
+                     HsLam noExtField $
+                     MG{ mg_alts = noLoc [mkSimpleMatch LambdaExpr
+                                                        args body]
+                       , mg_ext = MatchGroupTc [pat_ty, cont_ty, fail_ty] res_ty
+                       , mg_origin = Generated
+                       }
+             match = mkMatch (mkPrefixFunRhs (L loc name)) []
+                             (mkHsLams (rr_tv:res_tv:univ_tvs)
+                                       req_dicts body')
+                             (noLoc (EmptyLocalBinds noExtField))
+             mg :: MatchGroup GhcTc (LHsExpr GhcTc)
+             mg = MG{ mg_alts = L (getLoc match) [match]
+                    , mg_ext = MatchGroupTc [] res_ty
+                    , mg_origin = Generated
+                    }
+
+       ; let bind = FunBind{ fun_id = L loc matcher_id
+                           , fun_matches = mg
+                           , fun_ext = idHsWrapper
+                           , fun_tick = [] }
+             matcher_bind = unitBag (noLoc bind)
+
+       ; traceTc "tcPatSynMatcher" (ppr name $$ ppr (idType matcher_id))
+       ; traceTc "tcPatSynMatcher" (ppr matcher_bind)
+
+       ; return ((matcher_id, is_unlifted), matcher_bind) }
+
+mkPatSynRecSelBinds :: PatSyn
+                    -> [FieldLabel]  -- ^ Visible field labels
+                    -> [(Id, LHsBind GhcRn)]
+mkPatSynRecSelBinds ps fields
+  = [ mkOneRecordSelector [PatSynCon ps] (RecSelPatSyn ps) fld_lbl
+    | fld_lbl <- fields ]
+
+isUnidirectional :: HsPatSynDir a -> Bool
+isUnidirectional Unidirectional          = True
+isUnidirectional ImplicitBidirectional   = False
+isUnidirectional ExplicitBidirectional{} = False
+
+{-
+************************************************************************
+*                                                                      *
+         Constructing the "builder" Id
+*                                                                      *
+************************************************************************
+-}
+
+mkPatSynBuilderId :: HsPatSynDir a -> Located Name
+                  -> [TyVarBinder] -> ThetaType
+                  -> [TyVarBinder] -> ThetaType
+                  -> [Type] -> Type
+                  -> TcM (Maybe (Id, Bool))
+mkPatSynBuilderId dir (L _ name)
+                  univ_bndrs req_theta ex_bndrs prov_theta
+                  arg_tys pat_ty
+  | isUnidirectional dir
+  = return Nothing
+  | otherwise
+  = do { builder_name <- newImplicitBinder name mkBuilderOcc
+       ; let theta          = req_theta ++ prov_theta
+             need_dummy_arg = isUnliftedType pat_ty && null arg_tys && null theta
+             builder_sigma  = add_void need_dummy_arg $
+                              mkForAllTys univ_bndrs $
+                              mkForAllTys ex_bndrs $
+                              mkPhiTy theta $
+                              mkVisFunTys arg_tys $
+                              pat_ty
+             builder_id     = mkExportedVanillaId builder_name builder_sigma
+              -- See Note [Exported LocalIds] in GHC.Types.Id
+
+             builder_id'    = modifyIdInfo (`setLevityInfoWithType` pat_ty) builder_id
+
+       ; return (Just (builder_id', need_dummy_arg)) }
+  where
+
+tcPatSynBuilderBind :: PatSynBind GhcRn GhcRn
+                    -> TcM (LHsBinds GhcTc)
+-- See Note [Matchers and builders for pattern synonyms] in GHC.Core.PatSyn
+tcPatSynBuilderBind (PSB { psb_id = L loc name
+                         , psb_def = lpat
+                         , psb_dir = dir
+                         , psb_args = details })
+  | isUnidirectional dir
+  = return emptyBag
+
+  | Left why <- mb_match_group       -- Can't invert the pattern
+  = setSrcSpan (getLoc lpat) $ failWithTc $
+    vcat [ hang (text "Invalid right-hand side of bidirectional pattern synonym"
+                 <+> quotes (ppr name) <> colon)
+              2 why
+         , text "RHS pattern:" <+> ppr lpat ]
+
+  | Right match_group <- mb_match_group  -- Bidirectional
+  = do { patsyn <- tcLookupPatSyn name
+       ; case patSynBuilder patsyn of {
+           Nothing -> return emptyBag ;
+             -- This case happens if we found a type error in the
+             -- pattern synonym, recovered, and put a placeholder
+             -- with patSynBuilder=Nothing in the environment
+
+           Just (builder_id, need_dummy_arg) ->  -- Normal case
+    do { -- Bidirectional, so patSynBuilder returns Just
+         let match_group' | need_dummy_arg = add_dummy_arg match_group
+                          | otherwise      = match_group
+
+             bind = FunBind { fun_id      = L loc (idName builder_id)
+                            , fun_matches = match_group'
+                            , fun_ext     = emptyNameSet
+                            , fun_tick    = [] }
+
+             sig = completeSigFromId (PatSynCtxt name) builder_id
+
+       ; traceTc "tcPatSynBuilderBind {" $
+         ppr patsyn $$ ppr builder_id <+> dcolon <+> ppr (idType builder_id)
+       ; (builder_binds, _) <- tcPolyCheck emptyPragEnv sig (noLoc bind)
+       ; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds
+       ; return builder_binds } } }
+
+#if __GLASGOW_HASKELL__ <= 810
+  | otherwise = panic "tcPatSynBuilderBind"  -- Both cases dealt with
+#endif
+  where
+    mb_match_group
+       = case dir of
+           ExplicitBidirectional explicit_mg -> Right explicit_mg
+           ImplicitBidirectional -> fmap mk_mg (tcPatToExpr name args lpat)
+           Unidirectional -> panic "tcPatSynBuilderBind"
+
+    mk_mg :: LHsExpr GhcRn -> MatchGroup GhcRn (LHsExpr GhcRn)
+    mk_mg body = mkMatchGroup Generated [builder_match]
+          where
+            builder_args  = [L loc (VarPat noExtField (L loc n))
+                            | L loc n <- args]
+            builder_match = mkMatch (mkPrefixFunRhs (L loc name))
+                                    builder_args body
+                                    (noLoc (EmptyLocalBinds noExtField))
+
+    args = case details of
+              PrefixCon args     -> args
+              InfixCon arg1 arg2 -> [arg1, arg2]
+              RecCon args        -> map recordPatSynPatVar args
+
+    add_dummy_arg :: MatchGroup GhcRn (LHsExpr GhcRn)
+                  -> MatchGroup GhcRn (LHsExpr GhcRn)
+    add_dummy_arg mg@(MG { mg_alts =
+                           (L l [L loc match@(Match { m_pats = pats })]) })
+      = mg { mg_alts = L l [L loc (match { m_pats = nlWildPatName : pats })] }
+    add_dummy_arg other_mg = pprPanic "add_dummy_arg" $
+                             pprMatches other_mg
+tcPatSynBuilderBind (XPatSynBind nec) = noExtCon nec
+
+tcPatSynBuilderOcc :: PatSyn -> TcM (HsExpr GhcTcId, TcSigmaType)
+-- monadic only for failure
+tcPatSynBuilderOcc ps
+  | Just (builder_id, add_void_arg) <- builder
+  , let builder_expr = HsConLikeOut noExtField (PatSynCon ps)
+        builder_ty   = idType builder_id
+  = return $
+    if add_void_arg
+    then ( builder_expr   -- still just return builder_expr; the void# arg is added
+                          -- by dsConLike in the desugarer
+         , tcFunResultTy builder_ty )
+    else (builder_expr, builder_ty)
+
+  | otherwise  -- Unidirectional
+  = nonBidirectionalErr name
+  where
+    name    = patSynName ps
+    builder = patSynBuilder ps
+
+add_void :: Bool -> Type -> Type
+add_void need_dummy_arg ty
+  | need_dummy_arg = mkVisFunTy voidPrimTy ty
+  | otherwise      = ty
+
+tcPatToExpr :: Name -> [Located Name] -> LPat GhcRn
+            -> Either MsgDoc (LHsExpr GhcRn)
+-- Given a /pattern/, return an /expression/ that builds a value
+-- that matches the pattern.  E.g. if the pattern is (Just [x]),
+-- the expression is (Just [x]).  They look the same, but the
+-- input uses constructors from HsPat and the output uses constructors
+-- from HsExpr.
+--
+-- Returns (Left r) if the pattern is not invertible, for reason r.
+-- See Note [Builder for a bidirectional pattern synonym]
+tcPatToExpr name args pat = go pat
+  where
+    lhsVars = mkNameSet (map unLoc args)
+
+    -- Make a prefix con for prefix and infix patterns for simplicity
+    mkPrefixConExpr :: Located Name -> [LPat GhcRn]
+                    -> Either MsgDoc (HsExpr GhcRn)
+    mkPrefixConExpr lcon@(L loc _) pats
+      = do { exprs <- mapM go pats
+           ; return (foldl' (\x y -> HsApp noExtField (L loc x) y)
+                            (HsVar noExtField lcon) exprs) }
+
+    mkRecordConExpr :: Located Name -> HsRecFields GhcRn (LPat GhcRn)
+                    -> Either MsgDoc (HsExpr GhcRn)
+    mkRecordConExpr con fields
+      = do { exprFields <- mapM go fields
+           ; return (RecordCon noExtField con exprFields) }
+
+    go :: LPat GhcRn -> Either MsgDoc (LHsExpr GhcRn)
+    go (L loc p) = L loc <$> go1 p
+
+    go1 :: Pat GhcRn -> Either MsgDoc (HsExpr GhcRn)
+    go1 (ConPatIn con info)
+      = case info of
+          PrefixCon ps  -> mkPrefixConExpr con ps
+          InfixCon l r  -> mkPrefixConExpr con [l,r]
+          RecCon fields -> mkRecordConExpr con fields
+
+    go1 (SigPat _ pat _) = go1 (unLoc pat)
+        -- See Note [Type signatures and the builder expression]
+
+    go1 (VarPat _ (L l var))
+        | var `elemNameSet` lhsVars
+        = return $ HsVar noExtField (L l var)
+        | otherwise
+        = Left (quotes (ppr var) <+> text "is not bound by the LHS of the pattern synonym")
+    go1 (ParPat _ pat)          = fmap (HsPar noExtField) $ go pat
+    go1 p@(ListPat reb pats)
+      | Nothing <- reb = do { exprs <- mapM go pats
+                            ; return $ ExplicitList noExtField Nothing exprs }
+      | otherwise                   = notInvertibleListPat p
+    go1 (TuplePat _ pats box)       = do { exprs <- mapM go pats
+                                         ; return $ ExplicitTuple noExtField
+                                           (map (noLoc . (Present noExtField)) exprs)
+                                                                           box }
+    go1 (SumPat _ pat alt arity)    = do { expr <- go1 (unLoc pat)
+                                         ; return $ ExplicitSum noExtField alt arity
+                                                                   (noLoc expr)
+                                         }
+    go1 (LitPat _ lit)              = return $ HsLit noExtField lit
+    go1 (NPat _ (L _ n) mb_neg _)
+        | Just (SyntaxExprRn neg) <- mb_neg
+                                    = return $ unLoc $ foldl' nlHsApp (noLoc neg)
+                                                       [noLoc (HsOverLit noExtField n)]
+        | otherwise                 = return $ HsOverLit noExtField n
+    go1 (ConPatOut{})               = panic "ConPatOut in output of renamer"
+    go1 (CoPat{})                   = panic "CoPat in output of renamer"
+    go1 (SplicePat _ (HsSpliced _ _ (HsSplicedPat pat)))
+                                    = go1 pat
+    go1 (SplicePat _ (HsSpliced{})) = panic "Invalid splice variety"
+
+    -- The following patterns are not invertible.
+    go1 p@(BangPat {})                       = notInvertible p -- #14112
+    go1 p@(LazyPat {})                       = notInvertible p
+    go1 p@(WildPat {})                       = notInvertible p
+    go1 p@(AsPat {})                         = notInvertible p
+    go1 p@(ViewPat {})                       = notInvertible p
+    go1 p@(NPlusKPat {})                     = notInvertible p
+    go1   (XPat nec)                         = noExtCon nec
+    go1 p@(SplicePat _ (HsTypedSplice {}))   = notInvertible p
+    go1 p@(SplicePat _ (HsUntypedSplice {})) = notInvertible p
+    go1 p@(SplicePat _ (HsQuasiQuote {}))    = notInvertible p
+    go1   (SplicePat _ (XSplice nec))        = noExtCon nec
+
+    notInvertible p = Left (not_invertible_msg p)
+
+    not_invertible_msg p
+      =   text "Pattern" <+> quotes (ppr p) <+> text "is not invertible"
+      $+$ hang (text "Suggestion: instead use an explicitly bidirectional"
+                <+> text "pattern synonym, e.g.")
+             2 (hang (text "pattern" <+> pp_name <+> pp_args <+> larrow
+                      <+> ppr pat <+> text "where")
+                   2 (pp_name <+> pp_args <+> equals <+> text "..."))
+      where
+        pp_name = ppr name
+        pp_args = hsep (map ppr args)
+
+    -- We should really be able to invert list patterns, even when
+    -- rebindable syntax is on, but doing so involves a bit of
+    -- refactoring; see #14380.  Until then we reject with a
+    -- helpful error message.
+    notInvertibleListPat p
+      = Left (vcat [ not_invertible_msg p
+                   , text "Reason: rebindable syntax is on."
+                   , text "This is fixable: add use-case to #14380" ])
+
+{- Note [Builder for a bidirectional pattern synonym]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For a bidirectional pattern synonym we need to produce an /expression/
+that matches the supplied /pattern/, given values for the arguments
+of the pattern synonym.  For example
+  pattern F x y = (Just x, [y])
+The 'builder' for F looks like
+  $builderF x y = (Just x, [y])
+
+We can't always do this:
+ * Some patterns aren't invertible; e.g. view patterns
+      pattern F x = (reverse -> x:_)
+
+ * The RHS pattern might bind more variables than the pattern
+   synonym, so again we can't invert it
+      pattern F x = (x,y)
+
+ * Ditto wildcards
+      pattern F x = (x,_)
+
+
+Note [Redundant constraints for builder]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The builder can have redundant constraints, which are awkward to eliminate.
+Consider
+   pattern P = Just 34
+To match against this pattern we need (Eq a, Num a).  But to build
+(Just 34) we need only (Num a).  Fortunately instTcSigFromId sets
+sig_warn_redundant to False.
+
+************************************************************************
+*                                                                      *
+         Helper functions
+*                                                                      *
+************************************************************************
+
+Note [As-patterns in pattern synonym definitions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The rationale for rejecting as-patterns in pattern synonym definitions
+is that an as-pattern would introduce nonindependent pattern synonym
+arguments, e.g. given a pattern synonym like:
+
+        pattern K x y = x@(Just y)
+
+one could write a nonsensical function like
+
+        f (K Nothing x) = ...
+
+or
+        g (K (Just True) False) = ...
+
+Note [Type signatures and the builder expression]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+   pattern L x = Left x :: Either [a] [b]
+
+In tc{Infer/Check}PatSynDecl we will check that the pattern has the
+specified type.  We check the pattern *as a pattern*, so the type
+signature is a pattern signature, and so brings 'a' and 'b' into
+scope.  But we don't have a way to bind 'a, b' in the LHS, as we do
+'x', say.  Nevertheless, the signature may be useful to constrain
+the type.
+
+When making the binding for the *builder*, though, we don't want
+  $buildL x = Left x :: Either [a] [b]
+because that wil either mean (forall a b. Either [a] [b]), or we'll
+get a complaint that 'a' and 'b' are out of scope. (Actually the
+latter; #9867.)  No, the job of the signature is done, so when
+converting the pattern to an expression (for the builder RHS) we
+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.
+
+Any change to this ordering should make sure to change GHC.HsToCore.Expr if you
+want to avoid difficult to decipher core lint errors!
+ -}
+
+
+nonBidirectionalErr :: Outputable name => name -> TcM a
+nonBidirectionalErr name = failWithTc $
+    text "non-bidirectional pattern synonym"
+    <+> quotes (ppr name) <+> text "used in an expression"
+
+-- Walk the whole pattern and for all ConPatOuts, collect the
+-- existentially-bound type variables and evidence binding variables.
+--
+-- 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 GhcTc
+  -> ( [TyVar]        -- Existentially-bound type variables
+                      -- in correctly-scoped order; e.g. [ k:*, x:k ]
+     , [EvVar] )      -- and evidence variables
+
+tcCollectEx pat = go pat
+  where
+    go :: LPat GhcTc -> ([TyVar], [EvVar])
+    go = go1 . unLoc
+
+    go1 :: Pat GhcTc -> ([TyVar], [EvVar])
+    go1 (LazyPat _ p)      = go p
+    go1 (AsPat _ _ p)      = go p
+    go1 (ParPat _ p)       = go p
+    go1 (BangPat _ p)      = go p
+    go1 (ListPat _ ps)     = mergeMany . map go $ ps
+    go1 (TuplePat _ ps _)  = mergeMany . map go $ ps
+    go1 (SumPat _ p _ _)   = go p
+    go1 (ViewPat _ _ p)    = go p
+    go1 con@ConPatOut{}    = merge (pat_tvs con, pat_dicts con) $
+                              goConDetails $ pat_args con
+    go1 (SigPat _ p _)     = go p
+    go1 (CoPat _ _ p _)    = go1 p
+    go1 (NPlusKPat _ n k _ geq subtract)
+      = pprPanic "TODO: NPlusKPat" $ ppr n $$ ppr k $$ ppr geq $$ ppr subtract
+    go1 _                   = empty
+
+    goConDetails :: HsConPatDetails GhcTc -> ([TyVar], [EvVar])
+    goConDetails (PrefixCon ps) = mergeMany . map go $ ps
+    goConDetails (InfixCon p1 p2) = go p1 `merge` go p2
+    goConDetails (RecCon HsRecFields{ rec_flds = flds })
+      = mergeMany . map goRecFd $ flds
+
+    goRecFd :: LHsRecField GhcTc (LPat GhcTc) -> ([TyVar], [EvVar])
+    goRecFd (L _ HsRecField{ hsRecFieldArg = p }) = go p
+
+    merge (vs1, evs1) (vs2, evs2) = (vs1 ++ vs2, evs1 ++ evs2)
+    mergeMany = foldr merge empty
+    empty     = ([], [])
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs-boot b/compiler/GHC/Tc/TyCl/PatSyn.hs-boot
new file mode 100644
index 0000000000..44be72781d
--- /dev/null
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs-boot
@@ -0,0 +1,16 @@
+module GHC.Tc.TyCl.PatSyn where
+
+import GHC.Hs    ( PatSynBind, LHsBinds )
+import GHC.Tc.Types ( TcM, TcSigInfo )
+import GHC.Tc.Utils.Monad ( TcGblEnv)
+import Outputable ( Outputable )
+import GHC.Hs.Extension ( GhcRn, GhcTc )
+import Data.Maybe  ( Maybe )
+
+tcPatSynDecl :: PatSynBind GhcRn GhcRn
+             -> Maybe TcSigInfo
+             -> TcM (LHsBinds GhcTc, TcGblEnv)
+
+tcPatSynBuilderBind :: PatSynBind GhcRn GhcRn -> TcM (LHsBinds GhcTc)
+
+nonBidirectionalErr :: Outputable name => name -> TcM a
diff --git a/compiler/GHC/Tc/TyCl/Utils.hs b/compiler/GHC/Tc/TyCl/Utils.hs
new file mode 100644
index 0000000000..80157caa0d
--- /dev/null
+++ b/compiler/GHC/Tc/TyCl/Utils.hs
@@ -0,0 +1,1059 @@
+{-
+(c) The University of Glasgow 2006
+(c) The GRASP/AQUA Project, Glasgow University, 1992-1999
+
+-}
+
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ViewPatterns #-}
+
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
+
+-- | Analysis functions over data types. Specifically, detecting recursive types.
+--
+-- This stuff is only used for source-code decls; it's recorded in interface
+-- files for imported data types.
+module GHC.Tc.TyCl.Utils(
+        RolesInfo,
+        inferRoles,
+        checkSynCycles,
+        checkClassCycles,
+
+        -- * Implicits
+        addTyConsToGblEnv, mkDefaultMethodType,
+
+        -- * Record selectors
+        tcRecSelBinds, mkRecSelBinds, mkOneRecordSelector
+    ) where
+
+#include "HsVersions.h"
+
+import GhcPrelude
+
+import GHC.Tc.Utils.Monad
+import GHC.Tc.Utils.Env
+import GHC.Tc.Gen.Bind( tcValBinds )
+import GHC.Core.TyCo.Rep( Type(..), Coercion(..), MCoercion(..), UnivCoProvenance(..) )
+import GHC.Tc.Utils.TcType
+import GHC.Core.Predicate
+import TysWiredIn( unitTy )
+import GHC.Core.Make( rEC_SEL_ERROR_ID )
+import GHC.Hs
+import GHC.Core.Class
+import GHC.Core.Type
+import GHC.Driver.Types
+import GHC.Core.TyCon
+import GHC.Core.ConLike
+import GHC.Core.DataCon
+import GHC.Types.Name
+import GHC.Types.Name.Env
+import GHC.Types.Name.Set hiding (unitFV)
+import GHC.Types.Name.Reader ( mkVarUnqual )
+import GHC.Types.Id
+import GHC.Types.Id.Info
+import GHC.Types.Var.Env
+import GHC.Types.Var.Set
+import GHC.Core.Coercion ( ltRole )
+import GHC.Types.Basic
+import GHC.Types.SrcLoc
+import GHC.Types.Unique ( mkBuiltinUnique )
+import Outputable
+import Util
+import Maybes
+import Bag
+import FastString
+import FV
+import GHC.Types.Module
+import qualified GHC.LanguageExtensions as LangExt
+
+import Control.Monad
+
+{-
+************************************************************************
+*                                                                      *
+        Cycles in type synonym declarations
+*                                                                      *
+************************************************************************
+-}
+
+synonymTyConsOfType :: Type -> [TyCon]
+-- Does not look through type synonyms at all
+-- Return a list of synonym tycons
+-- Keep this synchronized with 'expandTypeSynonyms'
+synonymTyConsOfType ty
+  = nameEnvElts (go ty)
+  where
+     go :: Type -> NameEnv TyCon  -- The NameEnv does duplicate elim
+     go (TyConApp tc tys) = go_tc tc `plusNameEnv` go_s tys
+     go (LitTy _)         = emptyNameEnv
+     go (TyVarTy _)       = emptyNameEnv
+     go (AppTy a b)       = go a `plusNameEnv` go b
+     go (FunTy _ a b)     = go a `plusNameEnv` go b
+     go (ForAllTy _ ty)   = go ty
+     go (CastTy ty co)    = go ty `plusNameEnv` go_co co
+     go (CoercionTy co)   = go_co co
+
+     -- Note [TyCon cycles through coercions?!]
+     -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+     -- Although, in principle, it's possible for a type synonym loop
+     -- could go through a coercion (since a coercion can refer to
+     -- a TyCon or Type), it doesn't seem possible to actually construct
+     -- a Haskell program which tickles this case.  Here is an example
+     -- program which causes a coercion:
+     --
+     --   type family Star where
+     --       Star = Type
+     --
+     --   data T :: Star -> Type
+     --   data S :: forall (a :: Type). T a -> Type
+     --
+     -- Here, the application 'T a' must first coerce a :: Type to a :: Star,
+     -- witnessed by the type family.  But if we now try to make Type refer
+     -- to a type synonym which in turn refers to Star, we'll run into
+     -- trouble: we're trying to define and use the type constructor
+     -- in the same recursive group.  Possibly this restriction will be
+     -- lifted in the future but for now, this code is "just for completeness
+     -- sake".
+     go_mco MRefl    = emptyNameEnv
+     go_mco (MCo co) = go_co co
+
+     go_co (Refl ty)              = go ty
+     go_co (GRefl _ ty mco)       = go ty `plusNameEnv` go_mco mco
+     go_co (TyConAppCo _ tc cs)   = go_tc tc `plusNameEnv` go_co_s cs
+     go_co (AppCo co co')         = go_co co `plusNameEnv` go_co co'
+     go_co (ForAllCo _ co co')    = go_co co `plusNameEnv` go_co co'
+     go_co (FunCo _ co co')       = go_co co `plusNameEnv` go_co co'
+     go_co (CoVarCo _)            = emptyNameEnv
+     go_co (HoleCo {})            = emptyNameEnv
+     go_co (AxiomInstCo _ _ cs)   = go_co_s cs
+     go_co (UnivCo p _ ty ty')    = go_prov p `plusNameEnv` go ty `plusNameEnv` go ty'
+     go_co (SymCo co)             = go_co co
+     go_co (TransCo co co')       = go_co co `plusNameEnv` go_co co'
+     go_co (NthCo _ _ co)         = go_co co
+     go_co (LRCo _ co)            = go_co co
+     go_co (InstCo co co')        = go_co co `plusNameEnv` go_co co'
+     go_co (KindCo co)            = go_co co
+     go_co (SubCo co)             = go_co co
+     go_co (AxiomRuleCo _ cs)     = go_co_s cs
+
+     go_prov (PhantomProv co)     = go_co co
+     go_prov (ProofIrrelProv co)  = go_co co
+     go_prov (PluginProv _)       = emptyNameEnv
+
+     go_tc tc | isTypeSynonymTyCon tc = unitNameEnv (tyConName tc) tc
+              | otherwise             = emptyNameEnv
+     go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
+     go_co_s cos = foldr (plusNameEnv . go_co) emptyNameEnv cos
+
+-- | A monad for type synonym cycle checking, which keeps
+-- track of the TyCons which are known to be acyclic, or
+-- a failure message reporting that a cycle was found.
+newtype SynCycleM a = SynCycleM {
+    runSynCycleM :: SynCycleState -> Either (SrcSpan, SDoc) (a, SynCycleState) }
+    deriving (Functor)
+
+type SynCycleState = NameSet
+
+instance Applicative SynCycleM where
+    pure x = SynCycleM $ \state -> Right (x, state)
+    (<*>) = ap
+
+instance Monad SynCycleM where
+    m >>= f = SynCycleM $ \state ->
+        case runSynCycleM m state of
+            Right (x, state') ->
+                runSynCycleM (f x) state'
+            Left err -> Left err
+
+failSynCycleM :: SrcSpan -> SDoc -> SynCycleM ()
+failSynCycleM loc err = SynCycleM $ \_ -> Left (loc, err)
+
+-- | Test if a 'Name' is acyclic, short-circuiting if we've
+-- seen it already.
+checkNameIsAcyclic :: Name -> SynCycleM () -> SynCycleM ()
+checkNameIsAcyclic n m = SynCycleM $ \s ->
+    if n `elemNameSet` s
+        then Right ((), s) -- short circuit
+        else case runSynCycleM m s of
+                Right ((), s') -> Right ((), extendNameSet s' n)
+                Left err -> Left err
+
+-- | Checks if any of the passed in 'TyCon's have cycles.
+-- Takes the 'UnitId' of the home package (as we can avoid
+-- checking those TyCons: cycles never go through foreign packages) and
+-- the corresponding @LTyClDecl Name@ for each 'TyCon', so we
+-- can give better error messages.
+checkSynCycles :: UnitId -> [TyCon] -> [LTyClDecl GhcRn] -> TcM ()
+checkSynCycles this_uid tcs tyclds = do
+    case runSynCycleM (mapM_ (go emptyNameSet []) tcs) emptyNameSet of
+        Left (loc, err) -> setSrcSpan loc $ failWithTc err
+        Right _  -> return ()
+  where
+    -- Try our best to print the LTyClDecl for locally defined things
+    lcl_decls = mkNameEnv (zip (map tyConName tcs) tyclds)
+
+    -- Short circuit if we've already seen this Name and concluded
+    -- it was acyclic.
+    go :: NameSet -> [TyCon] -> TyCon -> SynCycleM ()
+    go so_far seen_tcs tc =
+        checkNameIsAcyclic (tyConName tc) $ go' so_far seen_tcs tc
+
+    -- Expand type synonyms, complaining if you find the same
+    -- type synonym a second time.
+    go' :: NameSet -> [TyCon] -> TyCon -> SynCycleM ()
+    go' so_far seen_tcs tc
+        | n `elemNameSet` so_far
+            = failSynCycleM (getSrcSpan (head seen_tcs)) $
+                  sep [ text "Cycle in type synonym declarations:"
+                      , nest 2 (vcat (map ppr_decl seen_tcs)) ]
+        -- Optimization: we don't allow cycles through external packages,
+        -- so once we find a non-local name we are guaranteed to not
+        -- have a cycle.
+        --
+        -- This won't hold once we get recursive packages with Backpack,
+        -- but for now it's fine.
+        | not (isHoleModule mod ||
+               moduleUnitId mod == this_uid ||
+               isInteractiveModule mod)
+            = return ()
+        | Just ty <- synTyConRhs_maybe tc =
+            go_ty (extendNameSet so_far (tyConName tc)) (tc:seen_tcs) ty
+        | otherwise = return ()
+      where
+        n = tyConName tc
+        mod = nameModule n
+        ppr_decl tc =
+          case lookupNameEnv lcl_decls n of
+            Just (L loc decl) -> ppr loc <> colon <+> ppr decl
+            Nothing -> ppr (getSrcSpan n) <> colon <+> ppr n
+                       <+> text "from external module"
+         where
+          n = tyConName tc
+
+    go_ty :: NameSet -> [TyCon] -> Type -> SynCycleM ()
+    go_ty so_far seen_tcs ty =
+        mapM_ (go so_far seen_tcs) (synonymTyConsOfType ty)
+
+{- Note [Superclass cycle check]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The superclass cycle check for C decides if we can statically
+guarantee that expanding C's superclass cycles transitively is
+guaranteed to terminate.  This is a Haskell98 requirement,
+but one that we lift with -XUndecidableSuperClasses.
+
+The worry is that a superclass cycle could make the type checker loop.
+More precisely, with a constraint (Given or Wanted)
+    C ty1 .. tyn
+one approach is to instantiate all of C's superclasses, transitively.
+We can only do so if that set is finite.
+
+This potential loop occurs only through superclasses.  This, for
+example, is fine
+  class C a where
+    op :: C b => a -> b -> b
+even though C's full definition uses C.
+
+Making the check static also makes it conservative.  Eg
+  type family F a
+  class F a => C a
+Here an instance of (F a) might mention C:
+  type instance F [a] = C a
+and now we'd have a loop.
+
+The static check works like this, starting with C
+  * Look at C's superclass predicates
+  * If any is a type-function application,
+    or is headed by a type variable, fail
+  * If any has C at the head, fail
+  * If any has a type class D at the head,
+    make the same test with D
+
+A tricky point is: what if there is a type variable at the head?
+Consider this:
+   class f (C f) => C f
+   class c       => Id c
+and now expand superclasses for constraint (C Id):
+     C Id
+ --> Id (C Id)
+ --> C Id
+ --> ....
+Each step expands superclasses one layer, and clearly does not terminate.
+-}
+
+checkClassCycles :: Class -> Maybe SDoc
+-- Nothing  <=> ok
+-- Just err <=> possible cycle error
+checkClassCycles cls
+  = do { (definite_cycle, err) <- go (unitNameSet (getName cls))
+                                     cls (mkTyVarTys (classTyVars cls))
+       ; let herald | definite_cycle = text "Superclass cycle for"
+                    | otherwise      = text "Potential superclass cycle for"
+       ; return (vcat [ herald <+> quotes (ppr cls)
+                      , nest 2 err, hint]) }
+  where
+    hint = text "Use UndecidableSuperClasses to accept this"
+
+    -- Expand superclasses starting with (C a b), complaining
+    -- if you find the same class a second time, or a type function
+    -- or predicate headed by a type variable
+    --
+    -- NB: this code duplicates TcType.transSuperClasses, but
+    --     with more error message generation clobber
+    -- Make sure the two stay in sync.
+    go :: NameSet -> Class -> [Type] -> Maybe (Bool, SDoc)
+    go so_far cls tys = firstJusts $
+                        map (go_pred so_far) $
+                        immSuperClasses cls tys
+
+    go_pred :: NameSet -> PredType -> Maybe (Bool, SDoc)
+       -- Nothing <=> ok
+       -- Just (True, err)  <=> definite cycle
+       -- Just (False, err) <=> possible cycle
+    go_pred so_far pred  -- NB: tcSplitTyConApp looks through synonyms
+       | Just (tc, tys) <- tcSplitTyConApp_maybe pred
+       = go_tc so_far pred tc tys
+       | hasTyVarHead pred
+       = Just (False, hang (text "one of whose superclass constraints is headed by a type variable:")
+                         2 (quotes (ppr pred)))
+       | otherwise
+       = Nothing
+
+    go_tc :: NameSet -> PredType -> TyCon -> [Type] -> Maybe (Bool, SDoc)
+    go_tc so_far pred tc tys
+      | isFamilyTyCon tc
+      = Just (False, hang (text "one of whose superclass constraints is headed by a type family:")
+                        2 (quotes (ppr pred)))
+      | Just cls <- tyConClass_maybe tc
+      = go_cls so_far cls tys
+      | otherwise   -- Equality predicate, for example
+      = Nothing
+
+    go_cls :: NameSet -> Class -> [Type] -> Maybe (Bool, SDoc)
+    go_cls so_far cls tys
+       | cls_nm `elemNameSet` so_far
+       = Just (True, text "one of whose superclasses is" <+> quotes (ppr cls))
+       | isCTupleClass cls
+       = go so_far cls tys
+       | otherwise
+       = do { (b,err) <- go  (so_far `extendNameSet` cls_nm) cls tys
+          ; return (b, text "one of whose superclasses is" <+> quotes (ppr cls)
+                       $$ err) }
+       where
+         cls_nm = getName cls
+
+{-
+************************************************************************
+*                                                                      *
+        Role inference
+*                                                                      *
+************************************************************************
+
+Note [Role inference]
+~~~~~~~~~~~~~~~~~~~~~
+The role inference algorithm datatype definitions to infer the roles on the
+parameters. Although these roles are stored in the tycons, we can perform this
+algorithm on the built tycons, as long as we don't peek at an as-yet-unknown
+roles field! Ah, the magic of laziness.
+
+First, we choose appropriate initial roles. For families and classes, roles
+(including initial roles) are N. For datatypes, we start with the role in the
+role annotation (if any), or otherwise use Phantom. This is done in
+initialRoleEnv1.
+
+The function irGroup then propagates role information until it reaches a
+fixpoint, preferring N over (R or P) and R over P. To aid in this, we have a
+monad RoleM, which is a combination reader and state monad. In its state are
+the current RoleEnv, which gets updated by role propagation, and an update
+bit, which we use to know whether or not we've reached the fixpoint. The
+environment of RoleM contains the tycon whose parameters we are inferring, and
+a VarEnv from parameters to their positions, so we can update the RoleEnv.
+Between tycons, this reader information is missing; it is added by
+addRoleInferenceInfo.
+
+There are two kinds of tycons to consider: algebraic ones (excluding classes)
+and type synonyms. (Remember, families don't participate -- all their parameters
+are N.) An algebraic tycon processes each of its datacons, in turn. Note that
+a datacon's universally quantified parameters might be different from the parent
+tycon's parameters, so we use the datacon's univ parameters in the mapping from
+vars to positions. Note also that we don't want to infer roles for existentials
+(they're all at N, too), so we put them in the set of local variables. As an
+optimisation, we skip any tycons whose roles are already all Nominal, as there
+nowhere else for them to go. For synonyms, we just analyse their right-hand sides.
+
+irType walks through a type, looking for uses of a variable of interest and
+propagating role information. Because anything used under a phantom position
+is at phantom and anything used under a nominal position is at nominal, the
+irType function can assume that anything it sees is at representational. (The
+other possibilities are pruned when they're encountered.)
+
+The rest of the code is just plumbing.
+
+How do we know that this algorithm is correct? It should meet the following
+specification:
+
+Let Z be a role context -- a mapping from variables to roles. The following
+rules define the property (Z |- t : r), where t is a type and r is a role:
+
+Z(a) = r'        r' <= r
+------------------------- RCVar
+Z |- a : r
+
+---------- RCConst
+Z |- T : r               -- T is a type constructor
+
+Z |- t1 : r
+Z |- t2 : N
+-------------- RCApp
+Z |- t1 t2 : r
+
+forall i<=n. (r_i is R or N) implies Z |- t_i : r_i
+roles(T) = r_1 .. r_n
+---------------------------------------------------- RCDApp
+Z |- T t_1 .. t_n : R
+
+Z, a:N |- t : r
+---------------------- RCAll
+Z |- forall a:k.t : r
+
+
+We also have the following rules:
+
+For all datacon_i in type T, where a_1 .. a_n are universally quantified
+and b_1 .. b_m are existentially quantified, and the arguments are t_1 .. t_p,
+then if forall j<=p, a_1 : r_1 .. a_n : r_n, b_1 : N .. b_m : N |- t_j : R,
+then roles(T) = r_1 .. r_n
+
+roles(->) = R, R
+roles(~#) = N, N
+
+With -dcore-lint on, the output of this algorithm is checked in checkValidRoles,
+called from checkValidTycon.
+
+Note [Role-checking data constructor arguments]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  data T a where
+    MkT :: Eq b => F a -> (a->a) -> T (G a)
+
+Then we want to check the roles at which 'a' is used
+in MkT's type.  We want to work on the user-written type,
+so we need to take into account
+  * the arguments:   (F a) and (a->a)
+  * the context:     C a b
+  * the result type: (G a)   -- this is in the eq_spec
+
+
+Note [Coercions in role inference]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Is (t |> co1) representationally equal to (t |> co2)? Of course they are! Changing
+the kind of a type is totally irrelevant to the representation of that type. So,
+we want to totally ignore coercions when doing role inference. This includes omitting
+any type variables that appear in nominal positions but only within coercions.
+-}
+
+type RolesInfo = Name -> [Role]
+
+type RoleEnv = NameEnv [Role]        -- from tycon names to roles
+
+-- This, and any of the functions it calls, must *not* look at the roles
+-- field of a tycon we are inferring roles about!
+-- See Note [Role inference]
+inferRoles :: HscSource -> RoleAnnotEnv -> [TyCon] -> Name -> [Role]
+inferRoles hsc_src annots tycons
+  = let role_env  = initialRoleEnv hsc_src annots tycons
+        role_env' = irGroup role_env tycons in
+    \name -> case lookupNameEnv role_env' name of
+      Just roles -> roles
+      Nothing    -> pprPanic "inferRoles" (ppr name)
+
+initialRoleEnv :: HscSource -> RoleAnnotEnv -> [TyCon] -> RoleEnv
+initialRoleEnv hsc_src annots = extendNameEnvList emptyNameEnv .
+                                map (initialRoleEnv1 hsc_src annots)
+
+initialRoleEnv1 :: HscSource -> RoleAnnotEnv -> TyCon -> (Name, [Role])
+initialRoleEnv1 hsc_src annots_env tc
+  | isFamilyTyCon tc      = (name, map (const Nominal) bndrs)
+  | isAlgTyCon tc         = (name, default_roles)
+  | isTypeSynonymTyCon tc = (name, default_roles)
+  | otherwise             = pprPanic "initialRoleEnv1" (ppr tc)
+  where name         = tyConName tc
+        bndrs        = tyConBinders tc
+        argflags     = map tyConBinderArgFlag bndrs
+        num_exps     = count isVisibleArgFlag argflags
+
+          -- if the number of annotations in the role annotation decl
+          -- is wrong, just ignore it. We check this in the validity check.
+        role_annots
+          = case lookupRoleAnnot annots_env name of
+              Just (L _ (RoleAnnotDecl _ _ annots))
+                | annots `lengthIs` num_exps -> map unLoc annots
+              _                              -> replicate num_exps Nothing
+        default_roles = build_default_roles argflags role_annots
+
+        build_default_roles (argf : argfs) (m_annot : ras)
+          | isVisibleArgFlag argf
+          = (m_annot `orElse` default_role) : build_default_roles argfs ras
+        build_default_roles (_argf : argfs) ras
+          = Nominal : build_default_roles argfs ras
+        build_default_roles [] [] = []
+        build_default_roles _ _ = pprPanic "initialRoleEnv1 (2)"
+                                           (vcat [ppr tc, ppr role_annots])
+
+        default_role
+          | isClassTyCon tc               = Nominal
+          -- Note [Default roles for abstract TyCons in hs-boot/hsig]
+          | HsBootFile <- hsc_src
+          , isAbstractTyCon tc            = Representational
+          | HsigFile   <- hsc_src
+          , isAbstractTyCon tc            = Nominal
+          | otherwise                     = Phantom
+
+-- Note [Default roles for abstract TyCons in hs-boot/hsig]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- What should the default role for an abstract TyCon be?
+--
+-- Originally, we inferred phantom role for abstract TyCons
+-- in hs-boot files, because the type variables were never used.
+--
+-- This was silly, because the role of the abstract TyCon
+-- was required to match the implementation, and the roles of
+-- data types are almost never phantom.  Thus, in ticket #9204,
+-- the default was changed so be representational (the most common case).  If
+-- the implementing data type was actually nominal, you'd get an easy
+-- to understand error, and add the role annotation yourself.
+--
+-- Then Backpack was added, and with it we added role *subtyping*
+-- the matching judgment: if an abstract TyCon has a nominal
+-- parameter, it's OK to implement it with a representational
+-- parameter.  But now, the representational default is not a good
+-- one, because you should *only* request representational if
+-- you're planning to do coercions. To be maximally flexible
+-- with what data types you will accept, you want the default
+-- for hsig files is nominal.  We don't allow role subtyping
+-- with hs-boot files (it's good practice to give an exactly
+-- accurate role here, because any types that use the abstract
+-- type will propagate the role information.)
+
+irGroup :: RoleEnv -> [TyCon] -> RoleEnv
+irGroup env tcs
+  = let (env', update) = runRoleM env $ mapM_ irTyCon tcs in
+    if update
+    then irGroup env' tcs
+    else env'
+
+irTyCon :: TyCon -> RoleM ()
+irTyCon tc
+  | isAlgTyCon tc
+  = do { old_roles <- lookupRoles tc
+       ; unless (all (== Nominal) old_roles) $  -- also catches data families,
+                                                -- which don't want or need role inference
+         irTcTyVars tc $
+         do { mapM_ (irType emptyVarSet) (tyConStupidTheta tc)  -- See #8958
+            ; whenIsJust (tyConClass_maybe tc) irClass
+            ; mapM_ irDataCon (visibleDataCons $ algTyConRhs tc) }}
+
+  | Just ty <- synTyConRhs_maybe tc
+  = irTcTyVars tc $
+    irType emptyVarSet ty
+
+  | otherwise
+  = return ()
+
+-- any type variable used in an associated type must be Nominal
+irClass :: Class -> RoleM ()
+irClass cls
+  = mapM_ ir_at (classATs cls)
+  where
+    cls_tvs    = classTyVars cls
+    cls_tv_set = mkVarSet cls_tvs
+
+    ir_at at_tc
+      = mapM_ (updateRole Nominal) nvars
+      where nvars = filter (`elemVarSet` cls_tv_set) $ tyConTyVars at_tc
+
+-- See Note [Role inference]
+irDataCon :: DataCon -> RoleM ()
+irDataCon datacon
+  = setRoleInferenceVars univ_tvs $
+    irExTyVars ex_tvs $ \ ex_var_set ->
+    mapM_ (irType ex_var_set)
+          (map tyVarKind ex_tvs ++ eqSpecPreds eq_spec ++ theta ++ arg_tys)
+      -- See Note [Role-checking data constructor arguments]
+  where
+    (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty)
+      = dataConFullSig datacon
+
+irType :: VarSet -> Type -> RoleM ()
+irType = go
+  where
+    go lcls ty                 | Just ty' <- coreView ty -- #14101
+                               = go lcls ty'
+    go lcls (TyVarTy tv)       = unless (tv `elemVarSet` lcls) $
+                                 updateRole Representational tv
+    go lcls (AppTy t1 t2)      = go lcls t1 >> markNominal lcls t2
+    go lcls (TyConApp tc tys)  = do { roles <- lookupRolesX tc
+                                    ; zipWithM_ (go_app lcls) roles tys }
+    go lcls (ForAllTy tvb ty)  = do { let tv = binderVar tvb
+                                          lcls' = extendVarSet lcls tv
+                                    ; markNominal lcls (tyVarKind tv)
+                                    ; go lcls' ty }
+    go lcls (FunTy _ arg res)  = go lcls arg >> go lcls res
+    go _    (LitTy {})         = return ()
+      -- See Note [Coercions in role inference]
+    go lcls (CastTy ty _)      = go lcls ty
+    go _    (CoercionTy _)     = return ()
+
+    go_app _ Phantom _ = return ()                 -- nothing to do here
+    go_app lcls Nominal ty = markNominal lcls ty  -- all vars below here are N
+    go_app lcls Representational ty = go lcls ty
+
+irTcTyVars :: TyCon -> RoleM a -> RoleM a
+irTcTyVars tc thing
+  = setRoleInferenceTc (tyConName tc) $ go (tyConTyVars tc)
+  where
+    go []       = thing
+    go (tv:tvs) = do { markNominal emptyVarSet (tyVarKind tv)
+                     ; addRoleInferenceVar tv $ go tvs }
+
+irExTyVars :: [TyVar] -> (TyVarSet -> RoleM a) -> RoleM a
+irExTyVars orig_tvs thing = go emptyVarSet orig_tvs
+  where
+    go lcls []       = thing lcls
+    go lcls (tv:tvs) = do { markNominal lcls (tyVarKind tv)
+                          ; go (extendVarSet lcls tv) tvs }
+
+markNominal :: TyVarSet   -- local variables
+            -> Type -> RoleM ()
+markNominal lcls ty = let nvars = fvVarList (FV.delFVs lcls $ get_ty_vars ty) in
+                      mapM_ (updateRole Nominal) nvars
+  where
+     -- get_ty_vars gets all the tyvars (no covars!) from a type *without*
+     -- recurring into coercions. Recall: coercions are totally ignored during
+     -- role inference. See [Coercions in role inference]
+    get_ty_vars :: Type -> FV
+    get_ty_vars (TyVarTy tv)      = unitFV tv
+    get_ty_vars (AppTy t1 t2)     = get_ty_vars t1 `unionFV` get_ty_vars t2
+    get_ty_vars (FunTy _ t1 t2)   = get_ty_vars t1 `unionFV` get_ty_vars t2
+    get_ty_vars (TyConApp _ tys)  = mapUnionFV get_ty_vars tys
+    get_ty_vars (ForAllTy tvb ty) = tyCoFVsBndr tvb (get_ty_vars ty)
+    get_ty_vars (LitTy {})        = emptyFV
+    get_ty_vars (CastTy ty _)     = get_ty_vars ty
+    get_ty_vars (CoercionTy _)    = emptyFV
+
+-- like lookupRoles, but with Nominal tags at the end for oversaturated TyConApps
+lookupRolesX :: TyCon -> RoleM [Role]
+lookupRolesX tc
+  = do { roles <- lookupRoles tc
+       ; return $ roles ++ repeat Nominal }
+
+-- gets the roles either from the environment or the tycon
+lookupRoles :: TyCon -> RoleM [Role]
+lookupRoles tc
+  = do { env <- getRoleEnv
+       ; case lookupNameEnv env (tyConName tc) of
+           Just roles -> return roles
+           Nothing    -> return $ tyConRoles tc }
+
+-- tries to update a role; won't ever update a role "downwards"
+updateRole :: Role -> TyVar -> RoleM ()
+updateRole role tv
+  = do { var_ns <- getVarNs
+       ; name <- getTyConName
+       ; case lookupVarEnv var_ns tv of
+           Nothing -> pprPanic "updateRole" (ppr name $$ ppr tv $$ ppr var_ns)
+           Just n  -> updateRoleEnv name n role }
+
+-- the state in the RoleM monad
+data RoleInferenceState = RIS { role_env  :: RoleEnv
+                              , update    :: Bool }
+
+-- the environment in the RoleM monad
+type VarPositions = VarEnv Int
+
+-- See [Role inference]
+newtype RoleM a = RM { unRM :: Maybe Name -- of the tycon
+                            -> VarPositions
+                            -> Int          -- size of VarPositions
+                            -> RoleInferenceState
+                            -> (a, RoleInferenceState) }
+    deriving (Functor)
+
+instance Applicative RoleM where
+    pure x = RM $ \_ _ _ state -> (x, state)
+    (<*>) = ap
+
+instance Monad RoleM where
+  a >>= f  = RM $ \m_info vps nvps state ->
+                  let (a', state') = unRM a m_info vps nvps state in
+                  unRM (f a') m_info vps nvps state'
+
+runRoleM :: RoleEnv -> RoleM () -> (RoleEnv, Bool)
+runRoleM env thing = (env', update)
+  where RIS { role_env = env', update = update }
+          = snd $ unRM thing Nothing emptyVarEnv 0 state
+        state = RIS { role_env  = env
+                    , update    = False }
+
+setRoleInferenceTc :: Name -> RoleM a -> RoleM a
+setRoleInferenceTc name thing = RM $ \m_name vps nvps state ->
+                                ASSERT( isNothing m_name )
+                                ASSERT( isEmptyVarEnv vps )
+                                ASSERT( nvps == 0 )
+                                unRM thing (Just name) vps nvps state
+
+addRoleInferenceVar :: TyVar -> RoleM a -> RoleM a
+addRoleInferenceVar tv thing
+  = RM $ \m_name vps nvps state ->
+    ASSERT( isJust m_name )
+    unRM thing m_name (extendVarEnv vps tv nvps) (nvps+1) state
+
+setRoleInferenceVars :: [TyVar] -> RoleM a -> RoleM a
+setRoleInferenceVars tvs thing
+  = RM $ \m_name _vps _nvps state ->
+    ASSERT( isJust m_name )
+    unRM thing m_name (mkVarEnv (zip tvs [0..])) (panic "setRoleInferenceVars")
+         state
+
+getRoleEnv :: RoleM RoleEnv
+getRoleEnv = RM $ \_ _ _ state@(RIS { role_env = env }) -> (env, state)
+
+getVarNs :: RoleM VarPositions
+getVarNs = RM $ \_ vps _ state -> (vps, state)
+
+getTyConName :: RoleM Name
+getTyConName = RM $ \m_name _ _ state ->
+                    case m_name of
+                      Nothing   -> panic "getTyConName"
+                      Just name -> (name, state)
+
+updateRoleEnv :: Name -> Int -> Role -> RoleM ()
+updateRoleEnv name n role
+  = RM $ \_ _ _ state@(RIS { role_env = role_env }) -> ((),
+         case lookupNameEnv role_env name of
+           Nothing -> pprPanic "updateRoleEnv" (ppr name)
+           Just roles -> let (before, old_role : after) = splitAt n roles in
+                         if role `ltRole` old_role
+                         then let roles' = before ++ role : after
+                                  role_env' = extendNameEnv role_env name roles' in
+                              RIS { role_env = role_env', update = True }
+                         else state )
+
+
+{- *********************************************************************
+*                                                                      *
+                Building implicits
+*                                                                      *
+********************************************************************* -}
+
+addTyConsToGblEnv :: [TyCon] -> TcM TcGblEnv
+-- Given a [TyCon], add to the TcGblEnv
+--   * extend the TypeEnv with the tycons
+--   * extend the TypeEnv with their implicitTyThings
+--   * extend the TypeEnv with any default method Ids
+--   * add bindings for record selectors
+addTyConsToGblEnv tyclss
+  = tcExtendTyConEnv tyclss                    $
+    tcExtendGlobalEnvImplicit implicit_things  $
+    tcExtendGlobalValEnv def_meth_ids          $
+    do { traceTc "tcAddTyCons" $ vcat
+            [ text "tycons" <+> ppr tyclss
+            , text "implicits" <+> ppr implicit_things ]
+       ; gbl_env <- tcRecSelBinds (mkRecSelBinds tyclss)
+       ; return gbl_env }
+ where
+   implicit_things = concatMap implicitTyConThings tyclss
+   def_meth_ids    = mkDefaultMethodIds tyclss
+
+mkDefaultMethodIds :: [TyCon] -> [Id]
+-- We want to put the default-method Ids (both vanilla and generic)
+-- into the type environment so that they are found when we typecheck
+-- the filled-in default methods of each instance declaration
+-- See Note [Default method Ids and Template Haskell]
+mkDefaultMethodIds tycons
+  = [ mkExportedVanillaId dm_name (mkDefaultMethodType cls sel_id dm_spec)
+    | tc <- tycons
+    , Just cls <- [tyConClass_maybe tc]
+    , (sel_id, Just (dm_name, dm_spec)) <- classOpItems cls ]
+
+mkDefaultMethodType :: Class -> Id -> DefMethSpec Type -> Type
+-- Returns the top-level type of the default method
+mkDefaultMethodType _ sel_id VanillaDM        = idType sel_id
+mkDefaultMethodType cls _   (GenericDM dm_ty) = mkSigmaTy tv_bndrs [pred] dm_ty
+   where
+     pred      = mkClassPred cls (mkTyVarTys (binderVars cls_bndrs))
+     cls_bndrs = tyConBinders (classTyCon cls)
+     tv_bndrs  = tyConTyVarBinders cls_bndrs
+     -- NB: the Class doesn't have TyConBinders; we reach into its
+     --     TyCon to get those.  We /do/ need the TyConBinders because
+     --     we need the correct visibility: these default methods are
+     --     used in code generated by the fill-in for missing
+     --     methods in instances (GHC.Tc.TyCl.Instance.mkDefMethBind), and
+     --     then typechecked.  So we need the right visibility info
+     --     (#13998)
+
+{-
+************************************************************************
+*                                                                      *
+                Building record selectors
+*                                                                      *
+************************************************************************
+-}
+
+{-
+Note [Default method Ids and Template Haskell]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this (#4169):
+   class Numeric a where
+     fromIntegerNum :: a
+     fromIntegerNum = ...
+
+   ast :: Q [Dec]
+   ast = [d| instance Numeric Int |]
+
+When we typecheck 'ast' we have done the first pass over the class decl
+(in tcTyClDecls), but we have not yet typechecked the default-method
+declarations (because they can mention value declarations).  So we
+must bring the default method Ids into scope first (so they can be seen
+when typechecking the [d| .. |] quote, and typecheck them later.
+-}
+
+{-
+************************************************************************
+*                                                                      *
+                Building record selectors
+*                                                                      *
+************************************************************************
+-}
+
+tcRecSelBinds :: [(Id, LHsBind GhcRn)] -> TcM TcGblEnv
+tcRecSelBinds sel_bind_prs
+  = tcExtendGlobalValEnv [sel_id | (L _ (IdSig _ sel_id)) <- sigs] $
+    do { (rec_sel_binds, tcg_env) <- discardWarnings $
+                                     -- See Note [Impredicative record selectors]
+                                     setXOptM LangExt.ImpredicativeTypes $
+                                     tcValBinds TopLevel binds sigs getGblEnv
+       ; return (tcg_env `addTypecheckedBinds` map snd rec_sel_binds) }
+  where
+    sigs = [ L loc (IdSig noExtField sel_id) | (sel_id, _) <- sel_bind_prs
+                                             , let loc = getSrcSpan sel_id ]
+    binds = [(NonRecursive, unitBag bind) | (_, bind) <- sel_bind_prs]
+
+mkRecSelBinds :: [TyCon] -> [(Id, LHsBind GhcRn)]
+-- NB We produce *un-typechecked* bindings, rather like 'deriving'
+--    This makes life easier, because the later type checking will add
+--    all necessary type abstractions and applications
+mkRecSelBinds tycons
+  = map mkRecSelBind [ (tc,fld) | tc <- tycons
+                                , fld <- tyConFieldLabels tc ]
+
+mkRecSelBind :: (TyCon, FieldLabel) -> (Id, LHsBind GhcRn)
+mkRecSelBind (tycon, fl)
+  = mkOneRecordSelector all_cons (RecSelData tycon) fl
+  where
+    all_cons = map RealDataCon (tyConDataCons tycon)
+
+mkOneRecordSelector :: [ConLike] -> RecSelParent -> FieldLabel
+                    -> (Id, LHsBind GhcRn)
+mkOneRecordSelector all_cons idDetails fl
+  = (sel_id, L loc sel_bind)
+  where
+    loc      = getSrcSpan sel_name
+    lbl      = flLabel fl
+    sel_name = flSelector fl
+
+    sel_id = mkExportedLocalId rec_details sel_name sel_ty
+    rec_details = RecSelId { sel_tycon = idDetails, sel_naughty = is_naughty }
+
+    -- Find a representative constructor, con1
+    cons_w_field = conLikesWithFields all_cons [lbl]
+    con1 = ASSERT( not (null cons_w_field) ) head cons_w_field
+
+    -- Selector type; Note [Polymorphic selectors]
+    field_ty   = conLikeFieldType con1 lbl
+    data_tvs   = tyCoVarsOfTypesWellScoped inst_tys
+    data_tv_set= mkVarSet data_tvs
+    is_naughty = not (tyCoVarsOfType field_ty `subVarSet` data_tv_set)
+    (field_tvs, field_theta, field_tau) = tcSplitSigmaTy field_ty
+    sel_ty | is_naughty = unitTy  -- See Note [Naughty record selectors]
+           | otherwise  = mkSpecForAllTys data_tvs          $
+                          mkPhiTy (conLikeStupidTheta con1) $   -- Urgh!
+                          mkVisFunTy data_ty                $
+                          mkSpecForAllTys field_tvs         $
+                          mkPhiTy field_theta               $
+                          -- req_theta is empty for normal DataCon
+                          mkPhiTy req_theta                 $
+                          field_tau
+
+    -- Make the binding: sel (C2 { fld = x }) = x
+    --                   sel (C7 { fld = x }) = x
+    --    where cons_w_field = [C2,C7]
+    sel_bind = mkTopFunBind Generated sel_lname alts
+      where
+        alts | is_naughty = [mkSimpleMatch (mkPrefixFunRhs sel_lname)
+                                           [] unit_rhs]
+             | otherwise =  map mk_match cons_w_field ++ deflt
+    mk_match con = mkSimpleMatch (mkPrefixFunRhs sel_lname)
+                                 [L loc (mk_sel_pat con)]
+                                 (L loc (HsVar noExtField (L loc field_var)))
+    mk_sel_pat con = ConPatIn (L loc (getName con)) (RecCon rec_fields)
+    rec_fields = HsRecFields { rec_flds = [rec_field], rec_dotdot = Nothing }
+    rec_field  = noLoc (HsRecField
+                        { hsRecFieldLbl
+                           = L loc (FieldOcc sel_name
+                                     (L loc $ mkVarUnqual lbl))
+                        , hsRecFieldArg
+                           = L loc (VarPat noExtField (L loc field_var))
+                        , hsRecPun = False })
+    sel_lname = L loc sel_name
+    field_var = mkInternalName (mkBuiltinUnique 1) (getOccName sel_name) loc
+
+    -- Add catch-all default case unless the case is exhaustive
+    -- We do this explicitly so that we get a nice error message that
+    -- mentions this particular record selector
+    deflt | all dealt_with all_cons = []
+          | otherwise = [mkSimpleMatch CaseAlt
+                            [L loc (WildPat noExtField)]
+                            (mkHsApp (L loc (HsVar noExtField
+                                         (L loc (getName rEC_SEL_ERROR_ID))))
+                                     (L loc (HsLit noExtField msg_lit)))]
+
+        -- Do not add a default case unless there are unmatched
+        -- constructors.  We must take account of GADTs, else we
+        -- get overlap warning messages from the pattern-match checker
+        -- NB: we need to pass type args for the *representation* TyCon
+        --     to dataConCannotMatch, hence the calculation of inst_tys
+        --     This matters in data families
+        --              data instance T Int a where
+        --                 A :: { fld :: Int } -> T Int Bool
+        --                 B :: { fld :: Int } -> T Int Char
+    dealt_with :: ConLike -> Bool
+    dealt_with (PatSynCon _) = False -- We can't predict overlap
+    dealt_with con@(RealDataCon dc) =
+      con `elem` cons_w_field || dataConCannotMatch inst_tys dc
+
+    (univ_tvs, _, eq_spec, _, req_theta, _, data_ty) = conLikeFullSig con1
+
+    eq_subst = mkTvSubstPrs (map eqSpecPair eq_spec)
+    inst_tys = substTyVars eq_subst univ_tvs
+
+    unit_rhs = mkLHsTupleExpr []
+    msg_lit = HsStringPrim NoSourceText (bytesFS lbl)
+
+{-
+Note [Polymorphic selectors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We take care to build the type of a polymorphic selector in the right
+order, so that visible type application works.
+
+  data Ord a => T a = MkT { field :: forall b. (Num a, Show b) => (a, b) }
+
+We want
+
+  field :: forall a. Ord a => T a -> forall b. (Num a, Show b) => (a, b)
+
+Note [Naughty record selectors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A "naughty" field is one for which we can't define a record
+selector, because an existential type variable would escape.  For example:
+        data T = forall a. MkT { x,y::a }
+We obviously can't define
+        x (MkT v _) = v
+Nevertheless we *do* put a RecSelId into the type environment
+so that if the user tries to use 'x' as a selector we can bleat
+helpfully, rather than saying unhelpfully that 'x' is not in scope.
+Hence the sel_naughty flag, to identify record selectors that don't really exist.
+
+In general, a field is "naughty" if its type mentions a type variable that
+isn't in the result type of the constructor.  Note that this *allows*
+GADT record selectors (Note [GADT record selectors]) whose types may look
+like     sel :: T [a] -> a
+
+For naughty selectors we make a dummy binding
+   sel = ()
+so that the later type-check will add them to the environment, and they'll be
+exported.  The function is never called, because the typechecker spots the
+sel_naughty field.
+
+Note [GADT record selectors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For GADTs, we require that all constructors with a common field 'f' have the same
+result type (modulo alpha conversion).  [Checked in GHC.Tc.TyCl.checkValidTyCon]
+E.g.
+        data T where
+          T1 { f :: Maybe a } :: T [a]
+          T2 { f :: Maybe a, y :: b  } :: T [a]
+          T3 :: T Int
+
+and now the selector takes that result type as its argument:
+   f :: forall a. T [a] -> Maybe a
+
+Details: the "real" types of T1,T2 are:
+   T1 :: forall r a.   (r~[a]) => a -> T r
+   T2 :: forall r a b. (r~[a]) => a -> b -> T r
+
+So the selector loooks like this:
+   f :: forall a. T [a] -> Maybe a
+   f (a:*) (t:T [a])
+     = case t of
+         T1 c   (g:[a]~[c]) (v:Maybe c)       -> v `cast` Maybe (right (sym g))
+         T2 c d (g:[a]~[c]) (v:Maybe c) (w:d) -> v `cast` Maybe (right (sym g))
+         T3 -> error "T3 does not have field f"
+
+Note the forall'd tyvars of the selector are just the free tyvars
+of the result type; there may be other tyvars in the constructor's
+type (e.g. 'b' in T2).
+
+Note the need for casts in the result!
+
+Note [Selector running example]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's OK to combine GADTs and type families.  Here's a running example:
+
+        data instance T [a] where
+          T1 { fld :: b } :: T [Maybe b]
+
+The representation type looks like this
+        data :R7T a where
+          T1 { fld :: b } :: :R7T (Maybe b)
+
+and there's coercion from the family type to the representation type
+        :CoR7T a :: T [a] ~ :R7T a
+
+The selector we want for fld looks like this:
+
+        fld :: forall b. T [Maybe b] -> b
+        fld = /\b. \(d::T [Maybe b]).
+              case d `cast` :CoR7T (Maybe b) of
+                T1 (x::b) -> x
+
+The scrutinee of the case has type :R7T (Maybe b), which can be
+gotten by applying the eq_spec to the univ_tvs of the data con.
+
+Note [Impredicative record selectors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+There are situations where generating code for record selectors requires the
+use of ImpredicativeTypes. Here is one example (adapted from #18005):
+
+  type S = (forall b. b -> b) -> Int
+  data T = MkT {unT :: S}
+         | Dummy
+
+We want to generate HsBinds for unT that look something like this:
+
+  unT :: S
+  unT (MkT x) = x
+  unT _       = recSelError "unT"#
+
+Note that the type of recSelError is `forall r (a :: TYPE r). Addr# -> a`.
+Therefore, when used in the right-hand side of `unT`, GHC attempts to
+instantiate `a` with `(forall b. b -> b) -> Int`, which is impredicative.
+To make sure that GHC is OK with this, we enable ImpredicativeTypes interally
+when typechecking these HsBinds so that the user does not have to.
+
+Although ImpredicativeTypes is somewhat fragile and unpredictable in GHC right
+now, it will become robust when Quick Look impredicativity is implemented. In
+the meantime, using ImpredicativeTypes to instantiate the `a` type variable in
+recSelError's type does actually work, so its use here is benign.
+-}