never executed always true always false
    1 {-
    2 (c) The University of Glasgow 2006
    3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
    4 
    5 -}
    6 
    7 
    8 {-# LANGUAGE FlexibleContexts #-}
    9 {-# LANGUAGE TypeFamilies #-}
   10 
   11 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}
   12 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
   13 
   14 -- | Typechecking instance declarations
   15 module GHC.Tc.TyCl.Instance
   16    ( tcInstDecls1
   17    , tcInstDeclsDeriv
   18    , tcInstDecls2
   19    )
   20 where
   21 
   22 import GHC.Prelude
   23 
   24 import GHC.Hs
   25 import GHC.Tc.Errors.Types
   26 import GHC.Tc.Gen.Bind
   27 import GHC.Tc.TyCl
   28 import GHC.Tc.TyCl.Utils ( addTyConsToGblEnv )
   29 import GHC.Tc.TyCl.Class ( tcClassDecl2, ClassScopedTVEnv, tcATDefault,
   30                            HsSigFun, mkHsSigFun, badMethodErr,
   31                            findMethodBind, instantiateMethod )
   32 import GHC.Tc.Solver( pushLevelAndSolveEqualitiesX, reportUnsolvedEqualities )
   33 import GHC.Tc.Gen.Sig
   34 import GHC.Tc.Utils.Monad
   35 import GHC.Tc.Validity
   36 import GHC.Tc.Utils.Zonk
   37 import GHC.Tc.Utils.TcMType
   38 import GHC.Tc.Utils.TcType
   39 import GHC.Tc.Types.Constraint
   40 import GHC.Tc.Types.Origin
   41 import GHC.Tc.TyCl.Build
   42 import GHC.Tc.Utils.Instantiate
   43 import GHC.Tc.Instance.Class( AssocInstInfo(..), isNotAssociated )
   44 import GHC.Core.Multiplicity
   45 import GHC.Core.InstEnv
   46 import GHC.Tc.Instance.Family
   47 import GHC.Core.FamInstEnv
   48 import GHC.Tc.Deriv
   49 import GHC.Tc.Utils.Env
   50 import GHC.Tc.Gen.HsType
   51 import GHC.Tc.Utils.Unify
   52 import GHC.Core        ( Expr(..), mkApps, mkVarApps, mkLams )
   53 import GHC.Core.Make   ( nO_METHOD_BINDING_ERROR_ID )
   54 import GHC.Core.Unfold.Make ( mkInlineUnfoldingWithArity, mkDFunUnfolding )
   55 import GHC.Core.Type
   56 import GHC.Core.SimpleOpt
   57 import GHC.Core.Predicate( classMethodInstTy )
   58 import GHC.Tc.Types.Evidence
   59 import GHC.Core.TyCon
   60 import GHC.Core.Coercion.Axiom
   61 import GHC.Core.DataCon
   62 import GHC.Core.ConLike
   63 import GHC.Core.Class
   64 import GHC.Types.Error
   65 import GHC.Types.Var as Var
   66 import GHC.Types.Var.Env
   67 import GHC.Types.Var.Set
   68 import GHC.Data.Bag
   69 import GHC.Types.Basic
   70 import GHC.Types.Fixity
   71 import GHC.Driver.Session
   72 import GHC.Driver.Ppr
   73 import GHC.Utils.Logger
   74 import GHC.Data.FastString
   75 import GHC.Types.Id
   76 import GHC.Types.SourceText
   77 import GHC.Data.List.SetOps
   78 import GHC.Types.Name
   79 import GHC.Types.Name.Set
   80 import GHC.Utils.Outputable
   81 import GHC.Utils.Panic
   82 import GHC.Utils.Panic.Plain
   83 import GHC.Types.SrcLoc
   84 import GHC.Utils.Misc
   85 import GHC.Data.BooleanFormula ( isUnsatisfied, pprBooleanFormulaNice )
   86 import qualified GHC.LanguageExtensions as LangExt
   87 
   88 import Control.Monad
   89 import Data.Tuple
   90 import GHC.Data.Maybe
   91 import Data.List( mapAccumL )
   92 
   93 
   94 {-
   95 Typechecking instance declarations is done in two passes. The first
   96 pass, made by @tcInstDecls1@, collects information to be used in the
   97 second pass.
   98 
   99 This pre-processed info includes the as-yet-unprocessed bindings
  100 inside the instance declaration.  These are type-checked in the second
  101 pass, when the class-instance envs and GVE contain all the info from
  102 all the instance and value decls.  Indeed that's the reason we need
  103 two passes over the instance decls.
  104 
  105 
  106 Note [How instance declarations are translated]
  107 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  108 Here is how we translate instance declarations into Core
  109 
  110 Running example:
  111         class C a where
  112            op1, op2 :: Ix b => a -> b -> b
  113            op2 = <dm-rhs>
  114 
  115         instance C a => C [a]
  116            {-# INLINE [2] op1 #-}
  117            op1 = <rhs>
  118 ===>
  119         -- Method selectors
  120         op1,op2 :: forall a. C a => forall b. Ix b => a -> b -> b
  121         op1 = ...
  122         op2 = ...
  123 
  124         -- Default methods get the 'self' dictionary as argument
  125         -- so they can call other methods at the same type
  126         -- Default methods get the same type as their method selector
  127         $dmop2 :: forall a. C a => forall b. Ix b => a -> b -> b
  128         $dmop2 = /\a. \(d:C a). /\b. \(d2: Ix b). <dm-rhs>
  129                -- NB: type variables 'a' and 'b' are *both* in scope in <dm-rhs>
  130                -- Note [Tricky type variable scoping]
  131 
  132         -- A top-level definition for each instance method
  133         -- Here op1_i, op2_i are the "instance method Ids"
  134         -- The INLINE pragma comes from the user pragma
  135         {-# INLINE [2] op1_i #-}  -- From the instance decl bindings
  136         op1_i, op2_i :: forall a. C a => forall b. Ix b => [a] -> b -> b
  137         op1_i = /\a. \(d:C a).
  138                let this :: C [a]
  139                    this = df_i a d
  140                      -- Note [Subtle interaction of recursion and overlap]
  141 
  142                    local_op1 :: forall b. Ix b => [a] -> b -> b
  143                    local_op1 = <rhs>
  144                      -- Source code; run the type checker on this
  145                      -- NB: Type variable 'a' (but not 'b') is in scope in <rhs>
  146                      -- Note [Tricky type variable scoping]
  147 
  148                in local_op1 a d
  149 
  150         op2_i = /\a \d:C a. $dmop2 [a] (df_i a d)
  151 
  152         -- The dictionary function itself
  153         {-# NOINLINE CONLIKE df_i #-}   -- Never inline dictionary functions
  154         df_i :: forall a. C a -> C [a]
  155         df_i = /\a. \d:C a. MkC (op1_i a d) (op2_i a d)
  156                 -- But see Note [Default methods in instances]
  157                 -- We can't apply the type checker to the default-method call
  158 
  159         -- Use a RULE to short-circuit applications of the class ops
  160         {-# RULE "op1@C[a]" forall a, d:C a.
  161                             op1 [a] (df_i d) = op1_i a d #-}
  162 
  163 Note [Instances and loop breakers]
  164 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  165 * Note that df_i may be mutually recursive with both op1_i and op2_i.
  166   It's crucial that df_i is not chosen as the loop breaker, even
  167   though op1_i has a (user-specified) INLINE pragma.
  168 
  169 * Instead the idea is to inline df_i into op1_i, which may then select
  170   methods from the MkC record, and thereby break the recursion with
  171   df_i, leaving a *self*-recursive op1_i.  (If op1_i doesn't call op at
  172   the same type, it won't mention df_i, so there won't be recursion in
  173   the first place.)
  174 
  175 * If op1_i is marked INLINE by the user there's a danger that we won't
  176   inline df_i in it, and that in turn means that (since it'll be a
  177   loop-breaker because df_i isn't), op1_i will ironically never be
  178   inlined.  But this is OK: the recursion breaking happens by way of
  179   a RULE (the magic ClassOp rule above), and RULES work inside InlineRule
  180   unfoldings. See Note [RULEs enabled in InitialPhase] in GHC.Core.Opt.Simplify.Utils
  181 
  182 Note [ClassOp/DFun selection]
  183 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  184 One thing we see a lot is stuff like
  185     op2 (df d1 d2)
  186 where 'op2' is a ClassOp and 'df' is DFun.  Now, we could inline *both*
  187 'op2' and 'df' to get
  188      case (MkD ($cop1 d1 d2) ($cop2 d1 d2) ... of
  189        MkD _ op2 _ _ _ -> op2
  190 And that will reduce to ($cop2 d1 d2) which is what we wanted.
  191 
  192 But it's tricky to make this work in practice, because it requires us to
  193 inline both 'op2' and 'df'.  But neither is keen to inline without having
  194 seen the other's result; and it's very easy to get code bloat (from the
  195 big intermediate) if you inline a bit too much.
  196 
  197 Instead we use a cunning trick.
  198  * We arrange that 'df' and 'op2' NEVER inline.
  199 
  200  * We arrange that 'df' is ALWAYS defined in the sylised form
  201       df d1 d2 = MkD ($cop1 d1 d2) ($cop2 d1 d2) ...
  202 
  203  * We give 'df' a magical unfolding (DFunUnfolding [$cop1, $cop2, ..])
  204    that lists its methods.
  205 
  206  * We make GHC.Core.Unfold.exprIsConApp_maybe spot a DFunUnfolding and return
  207    a suitable constructor application -- inlining df "on the fly" as it
  208    were.
  209 
  210  * ClassOp rules: We give the ClassOp 'op2' a BuiltinRule that
  211    extracts the right piece iff its argument satisfies
  212    exprIsConApp_maybe.  This is done in GHC.Types.Id.Make.mkDictSelId
  213 
  214  * We make 'df' CONLIKE, so that shared uses still match; eg
  215       let d = df d1 d2
  216       in ...(op2 d)...(op1 d)...
  217 
  218 Note [Single-method classes]
  219 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  220 If the class has just one method (or, more accurately, just one element
  221 of {superclasses + methods}), then we use a different strategy.
  222 
  223    class C a where op :: a -> a
  224    instance C a => C [a] where op = <blah>
  225 
  226 We translate the class decl into a newtype, which just gives a
  227 top-level axiom. The "constructor" MkC expands to a cast, as does the
  228 class-op selector.
  229 
  230    axiom Co:C a :: C a ~ (a->a)
  231 
  232    op :: forall a. C a -> (a -> a)
  233    op a d = d |> (Co:C a)
  234 
  235    MkC :: forall a. (a->a) -> C a
  236    MkC = /\a.\op. op |> (sym Co:C a)
  237 
  238 The clever RULE stuff doesn't work now, because ($df a d) isn't
  239 a constructor application, so exprIsConApp_maybe won't return
  240 Just <blah>.
  241 
  242 Instead, we simply rely on the fact that casts are cheap:
  243 
  244    $df :: forall a. C a => C [a]
  245    {-# INLINE df #-}  -- NB: INLINE this
  246    $df = /\a. \d. MkC [a] ($cop_list a d)
  247        = $cop_list |> forall a. C a -> (sym (Co:C [a]))
  248 
  249    $cop_list :: forall a. C a => [a] -> [a]
  250    $cop_list = <blah>
  251 
  252 So if we see
  253    (op ($df a d))
  254 we'll inline 'op' and '$df', since both are simply casts, and
  255 good things happen.
  256 
  257 Why do we use this different strategy?  Because otherwise we
  258 end up with non-inlined dictionaries that look like
  259     $df = $cop |> blah
  260 which adds an extra indirection to every use, which seems stupid.  See
  261 #4138 for an example (although the regression reported there
  262 wasn't due to the indirection).
  263 
  264 There is an awkward wrinkle though: we want to be very
  265 careful when we have
  266     instance C a => C [a] where
  267       {-# INLINE op #-}
  268       op = ...
  269 then we'll get an INLINE pragma on $cop_list but it's important that
  270 $cop_list only inlines when it's applied to *two* arguments (the
  271 dictionary and the list argument).  So we must not eta-expand $df
  272 above.  We ensure that this doesn't happen by putting an INLINE
  273 pragma on the dfun itself; after all, it ends up being just a cast.
  274 
  275 There is one more dark corner to the INLINE story, even more deeply
  276 buried.  Consider this (#3772):
  277 
  278     class DeepSeq a => C a where
  279       gen :: Int -> a
  280 
  281     instance C a => C [a] where
  282       gen n = ...
  283 
  284     class DeepSeq a where
  285       deepSeq :: a -> b -> b
  286 
  287     instance DeepSeq a => DeepSeq [a] where
  288       {-# INLINE deepSeq #-}
  289       deepSeq xs b = foldr deepSeq b xs
  290 
  291 That gives rise to these defns:
  292 
  293     $cdeepSeq :: DeepSeq a -> [a] -> b -> b
  294     -- User INLINE( 3 args )!
  295     $cdeepSeq a (d:DS a) b (x:[a]) (y:b) = ...
  296 
  297     $fDeepSeq[] :: DeepSeq a -> DeepSeq [a]
  298     -- DFun (with auto INLINE pragma)
  299     $fDeepSeq[] a d = $cdeepSeq a d |> blah
  300 
  301     $cp1 a d :: C a => DeepSep [a]
  302     -- We don't want to eta-expand this, lest
  303     -- $cdeepSeq gets inlined in it!
  304     $cp1 a d = $fDeepSep[] a (scsel a d)
  305 
  306     $fC[] :: C a => C [a]
  307     -- Ordinary DFun
  308     $fC[] a d = MkC ($cp1 a d) ($cgen a d)
  309 
  310 Here $cp1 is the code that generates the superclass for C [a].  The
  311 issue is this: we must not eta-expand $cp1 either, or else $fDeepSeq[]
  312 and then $cdeepSeq will inline there, which is definitely wrong.  Like
  313 on the dfun, we solve this by adding an INLINE pragma to $cp1.
  314 
  315 Note [Subtle interaction of recursion and overlap]
  316 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  317 Consider this
  318   class C a where { op1,op2 :: a -> a }
  319   instance C a => C [a] where
  320     op1 x = op2 x ++ op2 x
  321     op2 x = ...
  322   instance C [Int] where
  323     ...
  324 
  325 When type-checking the C [a] instance, we need a C [a] dictionary (for
  326 the call of op2).  If we look up in the instance environment, we find
  327 an overlap.  And in *general* the right thing is to complain (see Note
  328 [Overlapping instances] in GHC.Core.InstEnv).  But in *this* case it's wrong to
  329 complain, because we just want to delegate to the op2 of this same
  330 instance.
  331 
  332 Why is this justified?  Because we generate a (C [a]) constraint in
  333 a context in which 'a' cannot be instantiated to anything that matches
  334 other overlapping instances, or else we would not be executing this
  335 version of op1 in the first place.
  336 
  337 It might even be a bit disguised:
  338 
  339   nullFail :: C [a] => [a] -> [a]
  340   nullFail x = op2 x ++ op2 x
  341 
  342   instance C a => C [a] where
  343     op1 x = nullFail x
  344 
  345 Precisely this is used in package 'regex-base', module Context.hs.
  346 See the overlapping instances for RegexContext, and the fact that they
  347 call 'nullFail' just like the example above.  The DoCon package also
  348 does the same thing; it shows up in module Fraction.hs.
  349 
  350 Conclusion: when typechecking the methods in a C [a] instance, we want to
  351 treat the 'a' as an *existential* type variable, in the sense described
  352 by Note [Binding when looking up instances].  That is why isOverlappableTyVar
  353 responds True to an InstSkol, which is the kind of skolem we use in
  354 tcInstDecl2.
  355 
  356 
  357 Note [Tricky type variable scoping]
  358 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  359 In our example
  360         class C a where
  361            op1, op2 :: Ix b => a -> b -> b
  362            op2 = <dm-rhs>
  363 
  364         instance C a => C [a]
  365            {-# INLINE [2] op1 #-}
  366            op1 = <rhs>
  367 
  368 note that 'a' and 'b' are *both* in scope in <dm-rhs>, but only 'a' is
  369 in scope in <rhs>.  In particular, we must make sure that 'b' is in
  370 scope when typechecking <dm-rhs>.  This is achieved by subFunTys,
  371 which brings appropriate tyvars into scope. This happens for both
  372 <dm-rhs> and for <rhs>, but that doesn't matter: the *renamer* will have
  373 complained if 'b' is mentioned in <rhs>.
  374 
  375 
  376 
  377 ************************************************************************
  378 *                                                                      *
  379 \subsection{Extracting instance decls}
  380 *                                                                      *
  381 ************************************************************************
  382 
  383 Gather up the instance declarations from their various sources
  384 -}
  385 
  386 tcInstDecls1    -- Deal with both source-code and imported instance decls
  387    :: [LInstDecl GhcRn]         -- Source code instance decls
  388    -> TcM (TcGblEnv,            -- The full inst env
  389            [InstInfo GhcRn],    -- Source-code instance decls to process;
  390                                 -- contains all dfuns for this module
  391            [DerivInfo],         -- From data family instances
  392            ThBindEnv)           -- TH binding levels
  393 
  394 tcInstDecls1 inst_decls
  395   = do {    -- Do class and family instance declarations
  396        ; stuff <- mapAndRecoverM tcLocalInstDecl inst_decls
  397 
  398        ; let (local_infos_s, fam_insts_s, datafam_deriv_infos) = unzip3 stuff
  399              fam_insts   = concat fam_insts_s
  400              local_infos = concat local_infos_s
  401 
  402        ; (gbl_env, th_bndrs) <-
  403            addClsInsts local_infos $
  404            addFamInsts fam_insts
  405 
  406        ; return ( gbl_env
  407                 , local_infos
  408                 , concat datafam_deriv_infos
  409                 , th_bndrs ) }
  410 
  411 -- | Use DerivInfo for data family instances (produced by tcInstDecls1),
  412 --   datatype declarations (TyClDecl), and standalone deriving declarations
  413 --   (DerivDecl) to check and process all derived class instances.
  414 tcInstDeclsDeriv
  415   :: [DerivInfo]
  416   -> [LDerivDecl GhcRn]
  417   -> TcM (TcGblEnv, [InstInfo GhcRn], HsValBinds GhcRn)
  418 tcInstDeclsDeriv deriv_infos derivds
  419   = do th_stage <- getStage -- See Note [Deriving inside TH brackets]
  420        if isBrackStage th_stage
  421        then do { gbl_env <- getGblEnv
  422                ; return (gbl_env, bagToList emptyBag, emptyValBindsOut) }
  423        else do { (tcg_env, info_bag, valbinds) <- tcDeriving deriv_infos derivds
  424                ; return (tcg_env, bagToList info_bag, valbinds) }
  425 
  426 addClsInsts :: [InstInfo GhcRn] -> TcM a -> TcM a
  427 addClsInsts infos thing_inside
  428   = tcExtendLocalInstEnv (map iSpec infos) thing_inside
  429 
  430 addFamInsts :: [FamInst] -> TcM (TcGblEnv, ThBindEnv)
  431 -- Extend (a) the family instance envt
  432 --        (b) the type envt with stuff from data type decls
  433 addFamInsts fam_insts
  434   = tcExtendLocalFamInstEnv fam_insts $
  435     tcExtendGlobalEnv axioms          $
  436     do { traceTc "addFamInsts" (pprFamInsts fam_insts)
  437        ; (gbl_env, th_bndrs) <- addTyConsToGblEnv data_rep_tycons
  438                     -- Does not add its axiom; that comes
  439                     -- from adding the 'axioms' above
  440        ; return (gbl_env, th_bndrs)
  441        }
  442   where
  443     axioms = map (ACoAxiom . toBranchedAxiom . famInstAxiom) fam_insts
  444     data_rep_tycons = famInstsRepTyCons fam_insts
  445       -- The representation tycons for 'data instances' declarations
  446 
  447 {-
  448 Note [Deriving inside TH brackets]
  449 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  450 Given a declaration bracket
  451   [d| data T = A | B deriving( Show ) |]
  452 
  453 there is really no point in generating the derived code for deriving(
  454 Show) and then type-checking it. This will happen at the call site
  455 anyway, and the type check should never fail!  Moreover (#6005)
  456 the scoping of the generated code inside the bracket does not seem to
  457 work out.
  458 
  459 The easy solution is simply not to generate the derived instances at
  460 all.  (A less brutal solution would be to generate them with no
  461 bindings.)  This will become moot when we shift to the new TH plan, so
  462 the brutal solution will do.
  463 -}
  464 
  465 tcLocalInstDecl :: LInstDecl GhcRn
  466                 -> TcM ([InstInfo GhcRn], [FamInst], [DerivInfo])
  467         -- A source-file instance declaration
  468         -- Type-check all the stuff before the "where"
  469         --
  470         -- We check for respectable instance type, and context
  471 tcLocalInstDecl (L loc (TyFamInstD { tfid_inst = decl }))
  472   = do { fam_inst <- tcTyFamInstDecl NotAssociated (L loc decl)
  473        ; return ([], [fam_inst], []) }
  474 
  475 tcLocalInstDecl (L loc (DataFamInstD { dfid_inst = decl }))
  476   = do { (fam_inst, m_deriv_info) <- tcDataFamInstDecl NotAssociated emptyVarEnv (L loc decl)
  477        ; return ([], [fam_inst], maybeToList m_deriv_info) }
  478 
  479 tcLocalInstDecl (L loc (ClsInstD { cid_inst = decl }))
  480   = do { (insts, fam_insts, deriv_infos) <- tcClsInstDecl (L loc decl)
  481        ; return (insts, fam_insts, deriv_infos) }
  482 
  483 tcClsInstDecl :: LClsInstDecl GhcRn
  484               -> TcM ([InstInfo GhcRn], [FamInst], [DerivInfo])
  485 -- The returned DerivInfos are for any associated data families
  486 tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = hs_ty, cid_binds = binds
  487                                   , cid_sigs = uprags, cid_tyfam_insts = ats
  488                                   , cid_overlap_mode = overlap_mode
  489                                   , cid_datafam_insts = adts }))
  490   = setSrcSpanA loc                      $
  491     addErrCtxt (instDeclCtxt1 hs_ty)  $
  492     do  { dfun_ty <- tcHsClsInstType (InstDeclCtxt False) hs_ty
  493         ; let (tyvars, theta, clas, inst_tys) = tcSplitDFunTy dfun_ty
  494              -- NB: tcHsClsInstType does checkValidInstance
  495 
  496         ; (subst, skol_tvs) <- tcInstSkolTyVars tyvars
  497         ; let tv_skol_prs = [ (tyVarName tv, skol_tv)
  498                             | (tv, skol_tv) <- tyvars `zip` skol_tvs ]
  499               -- Map from the skolemized Names to the original Names.
  500               -- See Note [Associated data family instances and di_scoped_tvs].
  501               tv_skol_env = mkVarEnv $ map swap tv_skol_prs
  502               n_inferred = countWhile ((== Inferred) . binderArgFlag) $
  503                            fst $ splitForAllTyCoVarBinders dfun_ty
  504               visible_skol_tvs = drop n_inferred skol_tvs
  505 
  506         ; traceTc "tcLocalInstDecl 1" (ppr dfun_ty $$ ppr (invisibleTyBndrCount dfun_ty) $$ ppr skol_tvs)
  507 
  508         -- Next, process any associated types.
  509         ; (datafam_stuff, tyfam_insts)
  510              <- tcExtendNameTyVarEnv tv_skol_prs $
  511                 do  { let mini_env   = mkVarEnv (classTyVars clas `zip` substTys subst inst_tys)
  512                           mini_subst = mkTvSubst (mkInScopeSet (mkVarSet skol_tvs)) mini_env
  513                           mb_info    = InClsInst { ai_class = clas
  514                                                  , ai_tyvars = visible_skol_tvs
  515                                                  , ai_inst_env = mini_env }
  516                     ; df_stuff  <- mapAndRecoverM (tcDataFamInstDecl mb_info tv_skol_env) adts
  517                     ; tf_insts1 <- mapAndRecoverM (tcTyFamInstDecl mb_info)   ats
  518 
  519                       -- Check for missing associated types and build them
  520                       -- from their defaults (if available)
  521                     ; is_boot <- tcIsHsBootOrSig
  522                     ; let atItems = classATItems clas
  523                     ; tf_insts2 <- mapM (tcATDefault (locA loc) mini_subst defined_ats)
  524                                         (if is_boot then [] else atItems)
  525                       -- Don't default type family instances, but rather omit, in hsig/hs-boot.
  526                       -- Since hsig/hs-boot files are essentially large binders we want omission
  527                       -- of the definition to result in no restriction, rather than for example
  528                       -- attempting to "pattern match" with the invisible defaults and generate
  529                       -- equalities. Without further handling, this would just result in a panic
  530                       -- anyway.
  531                       -- See https://github.com/ghc-proposals/ghc-proposals/pull/320 for
  532                       -- additional discussion.
  533                     ; return (df_stuff, tf_insts1 ++ concat tf_insts2) }
  534 
  535 
  536         -- Finally, construct the Core representation of the instance.
  537         -- (This no longer includes the associated types.)
  538         ; dfun_name <- newDFunName clas inst_tys (getLocA hs_ty)
  539                 -- Dfun location is that of instance *header*
  540 
  541         ; ispec <- newClsInst (fmap unLoc overlap_mode) dfun_name
  542                               tyvars theta clas inst_tys
  543 
  544         ; let inst_binds = InstBindings
  545                              { ib_binds = binds
  546                              , ib_tyvars = map Var.varName tyvars -- Scope over bindings
  547                              , ib_pragmas = uprags
  548                              , ib_extensions = []
  549                              , ib_derived = False }
  550               inst_info = InstInfo { iSpec  = ispec, iBinds = inst_binds }
  551 
  552               (datafam_insts, m_deriv_infos) = unzip datafam_stuff
  553               deriv_infos                    = catMaybes m_deriv_infos
  554               all_insts                      = tyfam_insts ++ datafam_insts
  555 
  556          -- In hs-boot files there should be no bindings
  557         ; let no_binds = isEmptyLHsBinds binds && null uprags
  558         ; is_boot <- tcIsHsBootOrSig
  559         ; failIfTc (is_boot && not no_binds) TcRnIllegalHsBootFileDecl
  560 
  561         ; return ( [inst_info], all_insts, deriv_infos ) }
  562   where
  563     defined_ats = mkNameSet (map (tyFamInstDeclName . unLoc) ats)
  564                   `unionNameSet`
  565                   mkNameSet (map (unLoc . feqn_tycon
  566                                         . dfid_eqn
  567                                         . unLoc) adts)
  568 
  569 {-
  570 ************************************************************************
  571 *                                                                      *
  572                Type family instances
  573 *                                                                      *
  574 ************************************************************************
  575 
  576 Family instances are somewhat of a hybrid.  They are processed together with
  577 class instance heads, but can contain data constructors and hence they share a
  578 lot of kinding and type checking code with ordinary algebraic data types (and
  579 GADTs).
  580 -}
  581 
  582 tcTyFamInstDecl :: AssocInstInfo
  583                 -> LTyFamInstDecl GhcRn -> TcM FamInst
  584   -- "type instance"
  585   -- See Note [Associated type instances]
  586 tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
  587   = setSrcSpanA loc           $
  588     tcAddTyFamInstCtxt decl  $
  589     do { let fam_lname = feqn_tycon eqn
  590        ; fam_tc <- tcLookupLocatedTyCon fam_lname
  591        ; tcFamInstDeclChecks mb_clsinfo fam_tc
  592 
  593          -- (0) Check it's an open type family
  594        ; checkTc (isTypeFamilyTyCon fam_tc)     (wrongKindOfFamily fam_tc)
  595        ; checkTc (isOpenTypeFamilyTyCon fam_tc) (notOpenFamily fam_tc)
  596 
  597          -- (1) do the work of verifying the synonym group
  598          -- For some reason we don't have a location for the equation
  599          -- itself, so we make do with the location of family name
  600        ; co_ax_branch <- tcTyFamInstEqn fam_tc mb_clsinfo
  601                                         (L (na2la $ getLoc fam_lname) eqn)
  602 
  603          -- (2) check for validity
  604        ; checkConsistentFamInst mb_clsinfo fam_tc co_ax_branch
  605        ; checkValidCoAxBranch fam_tc co_ax_branch
  606 
  607          -- (3) construct coercion axiom
  608        ; rep_tc_name <- newFamInstAxiomName fam_lname [coAxBranchLHS co_ax_branch]
  609        ; let axiom = mkUnbranchedCoAxiom rep_tc_name fam_tc co_ax_branch
  610        ; newFamInst SynFamilyInst axiom }
  611 
  612 
  613 ---------------------
  614 tcFamInstDeclChecks :: AssocInstInfo -> TyCon -> TcM ()
  615 -- Used for both type and data families
  616 tcFamInstDeclChecks mb_clsinfo fam_tc
  617   = do { -- Type family instances require -XTypeFamilies
  618          -- and can't (currently) be in an hs-boot file
  619        ; traceTc "tcFamInstDecl" (ppr fam_tc)
  620        ; type_families <- xoptM LangExt.TypeFamilies
  621        ; is_boot       <- tcIsHsBootOrSig   -- Are we compiling an hs-boot file?
  622        ; checkTc type_families $ badFamInstDecl fam_tc
  623        ; checkTc (not is_boot) $ badBootFamInstDeclErr
  624 
  625        -- Check that it is a family TyCon, and that
  626        -- oplevel type instances are not for associated types.
  627        ; checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
  628 
  629        ; when (isNotAssociated mb_clsinfo &&   -- Not in a class decl
  630                isTyConAssoc fam_tc)            -- but an associated type
  631               (addErr $ assocInClassErr fam_tc)
  632        }
  633 
  634 {- Note [Associated type instances]
  635 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  636 We allow this:
  637   class C a where
  638     type T x a
  639   instance C Int where
  640     type T (S y) Int = y
  641     type T Z     Int = Char
  642 
  643 Note that
  644   a) The variable 'x' is not bound by the class decl
  645   b) 'x' is instantiated to a non-type-variable in the instance
  646   c) There are several type instance decls for T in the instance
  647 
  648 All this is fine.  Of course, you can't give any *more* instances
  649 for (T ty Int) elsewhere, because it's an *associated* type.
  650 
  651 
  652 ************************************************************************
  653 *                                                                      *
  654                Data family instances
  655 *                                                                      *
  656 ************************************************************************
  657 
  658 For some reason data family instances are a lot more complicated
  659 than type family instances
  660 -}
  661 
  662 tcDataFamInstDecl ::
  663      AssocInstInfo
  664   -> TyVarEnv Name -- If this is an associated data family instance, maps the
  665                    -- parent class's skolemized type variables to their
  666                    -- original Names. If this is a non-associated instance,
  667                    -- this will be empty.
  668                    -- See Note [Associated data family instances and di_scoped_tvs].
  669   -> LDataFamInstDecl GhcRn -> TcM (FamInst, Maybe DerivInfo)
  670   -- "newtype instance" and "data instance"
  671 tcDataFamInstDecl mb_clsinfo tv_skol_env
  672     (L loc decl@(DataFamInstDecl { dfid_eqn =
  673       FamEqn { feqn_bndrs  = outer_bndrs
  674              , feqn_pats   = hs_pats
  675              , feqn_tycon  = lfam_name@(L _ fam_name)
  676              , feqn_fixity = fixity
  677              , feqn_rhs    = HsDataDefn { dd_ND      = new_or_data
  678                                         , dd_cType   = cType
  679                                         , dd_ctxt    = hs_ctxt
  680                                         , dd_cons    = hs_cons
  681                                         , dd_kindSig = m_ksig
  682                                         , dd_derivs  = derivs } }}))
  683   = setSrcSpanA loc            $
  684     tcAddDataFamInstCtxt decl  $
  685     do { fam_tc <- tcLookupLocatedTyCon lfam_name
  686 
  687        ; tcFamInstDeclChecks mb_clsinfo fam_tc
  688 
  689        -- Check that the family declaration is for the right kind
  690        ; checkTc (isDataFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
  691        ; gadt_syntax <- dataDeclChecks fam_name new_or_data hs_ctxt hs_cons
  692           -- Do /not/ check that the number of patterns = tyConArity fam_tc
  693           -- See [Arity of data families] in GHC.Core.FamInstEnv
  694        ; (qtvs, pats, res_kind, stupid_theta)
  695              <- tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity
  696                                     hs_ctxt hs_pats m_ksig new_or_data
  697 
  698        -- Eta-reduce the axiom if possible
  699        -- Quite tricky: see Note [Implementing eta reduction for data families]
  700        ; let (eta_pats, eta_tcbs) = eta_reduce fam_tc pats
  701              eta_tvs       = map binderVar eta_tcbs
  702              post_eta_qtvs = filterOut (`elem` eta_tvs) qtvs
  703 
  704              full_tcbs = mkTyConBindersPreferAnon post_eta_qtvs
  705                             (tyCoVarsOfType (mkSpecForAllTys eta_tvs res_kind))
  706                          ++ eta_tcbs
  707                  -- Put the eta-removed tyvars at the end
  708                  -- Remember, qtvs is in arbitrary order, except kind vars are
  709                  -- first, so there is no reason to suppose that the eta_tvs
  710                  -- (obtained from the pats) are at the end (#11148)
  711 
  712        -- Eta-expand the representation tycon until it has result
  713        -- kind `TYPE r`, for some `r`. If UnliftedNewtypes is not enabled, we
  714        -- go one step further and ensure that it has kind `TYPE 'LiftedRep`.
  715        --
  716        -- See also Note [Arity of data families] in GHC.Core.FamInstEnv
  717        -- NB: we can do this after eta-reducing the axiom, because if
  718        --     we did it before the "extra" tvs from etaExpandAlgTyCon
  719        --     would always be eta-reduced
  720        --
  721        ; (extra_tcbs, final_res_kind) <- etaExpandAlgTyCon full_tcbs res_kind
  722 
  723        -- Check the result kind; it may come from a user-written signature.
  724        -- See Note [Datatype return kinds] in GHC.Tc.TyCl point 4(a)
  725        ; let extra_pats  = map (mkTyVarTy . binderVar) extra_tcbs
  726              all_pats    = pats `chkAppend` extra_pats
  727              orig_res_ty = mkTyConApp fam_tc all_pats
  728              ty_binders  = full_tcbs `chkAppend` extra_tcbs
  729 
  730        ; traceTc "tcDataFamInstDecl" $
  731          vcat [ text "Fam tycon:" <+> ppr fam_tc
  732               , text "Pats:" <+> ppr pats
  733               , text "visibilities:" <+> ppr (tcbVisibilities fam_tc pats)
  734               , text "all_pats:" <+> ppr all_pats
  735               , text "ty_binders" <+> ppr ty_binders
  736               , text "fam_tc_binders:" <+> ppr (tyConBinders fam_tc)
  737               , text "res_kind:" <+> ppr res_kind
  738               , text "final_res_kind:" <+> ppr final_res_kind
  739               , text "eta_pats" <+> ppr eta_pats
  740               , text "eta_tcbs" <+> ppr eta_tcbs ]
  741 
  742        ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) ->
  743            do { data_cons <- tcExtendTyVarEnv qtvs $
  744                   -- For H98 decls, the tyvars scope
  745                   -- over the data constructors
  746                   tcConDecls new_or_data (DDataInstance orig_res_ty)
  747                              rec_rep_tc ty_binders final_res_kind
  748                              hs_cons
  749 
  750               ; rep_tc_name <- newFamInstTyConName lfam_name pats
  751               ; axiom_name  <- newFamInstAxiomName lfam_name [pats]
  752               ; tc_rhs <- case new_or_data of
  753                      DataType -> return $
  754                         mkLevPolyDataTyConRhs
  755                           (isFixedRuntimeRepKind final_res_kind)
  756                           data_cons
  757                      NewType  -> assert (not (null data_cons)) $
  758                                  mkNewTyConRhs rep_tc_name rec_rep_tc (head data_cons)
  759 
  760               ; let ax_rhs = mkTyConApp rep_tc (mkTyVarTys post_eta_qtvs)
  761                     axiom  = mkSingleCoAxiom Representational axiom_name
  762                                  post_eta_qtvs eta_tvs [] fam_tc eta_pats ax_rhs
  763                     parent = DataFamInstTyCon axiom fam_tc all_pats
  764 
  765                       -- NB: Use the full ty_binders from the pats. See bullet toward
  766                       -- the end of Note [Data type families] in GHC.Core.TyCon
  767                     rep_tc   = mkAlgTyCon rep_tc_name
  768                                           ty_binders final_res_kind
  769                                           (map (const Nominal) ty_binders)
  770                                           (fmap unLoc cType) stupid_theta
  771                                           tc_rhs parent
  772                                           gadt_syntax
  773                  -- We always assume that indexed types are recursive.  Why?
  774                  -- (1) Due to their open nature, we can never be sure that a
  775                  -- further instance might not introduce a new recursive
  776                  -- dependency.  (2) They are always valid loop breakers as
  777                  -- they involve a coercion.
  778               ; return (rep_tc, axiom) }
  779 
  780        -- Remember to check validity; no recursion to worry about here
  781        -- Check that left-hand sides are ok (mono-types, no type families,
  782        -- consistent instantiations, etc)
  783        ; let ax_branch = coAxiomSingleBranch axiom
  784        ; checkConsistentFamInst mb_clsinfo fam_tc ax_branch
  785        ; checkValidCoAxBranch fam_tc ax_branch
  786        ; checkValidTyCon rep_tc
  787 
  788        ; let scoped_tvs = map mk_deriv_info_scoped_tv_pr (tyConTyVars rep_tc)
  789              m_deriv_info = case derivs of
  790                []    -> Nothing
  791                preds ->
  792                  Just $ DerivInfo { di_rep_tc  = rep_tc
  793                                   , di_scoped_tvs = scoped_tvs
  794                                   , di_clauses = preds
  795                                   , di_ctxt    = tcMkDataFamInstCtxt decl }
  796 
  797        ; fam_inst <- newFamInst (DataFamilyInst rep_tc) axiom
  798        ; return (fam_inst, m_deriv_info) }
  799   where
  800     eta_reduce :: TyCon -> [Type] -> ([Type], [TyConBinder])
  801     -- See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom
  802     -- Splits the incoming patterns into two: the [TyVar]
  803     -- are the patterns that can be eta-reduced away.
  804     -- e.g.     T [a] Int a d c   ==>  (T [a] Int a, [d,c])
  805     --
  806     -- NB: quadratic algorithm, but types are small here
  807     eta_reduce fam_tc pats
  808         = go (reverse (zip3 pats fvs_s vis_s)) []
  809         where
  810           vis_s :: [TyConBndrVis]
  811           vis_s = tcbVisibilities fam_tc pats
  812 
  813           fvs_s :: [TyCoVarSet]  -- 1-1 correspondence with pats
  814                                  -- Each elt is the free vars of all /earlier/ pats
  815           (_, fvs_s) = mapAccumL add_fvs emptyVarSet pats
  816           add_fvs fvs pat = (fvs `unionVarSet` tyCoVarsOfType pat, fvs)
  817 
  818     go ((pat, fvs_to_the_left, tcb_vis):pats) etad_tvs
  819       | Just tv <- getTyVar_maybe pat
  820       , not (tv `elemVarSet` fvs_to_the_left)
  821       = go pats (Bndr tv tcb_vis : etad_tvs)
  822     go pats etad_tvs = (reverse (map fstOf3 pats), etad_tvs)
  823 
  824     -- Create a Name-TyVar mapping to bring into scope when typechecking any
  825     -- deriving clauses this data family instance may have.
  826     -- See Note [Associated data family instances and di_scoped_tvs].
  827     mk_deriv_info_scoped_tv_pr :: TyVar -> (Name, TyVar)
  828     mk_deriv_info_scoped_tv_pr tv =
  829       let n = lookupWithDefaultVarEnv tv_skol_env (tyVarName tv) tv
  830       in (n, tv)
  831 
  832 {-
  833 Note [Associated data family instances and di_scoped_tvs]
  834 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  835 Some care is required to implement `deriving` correctly for associated data
  836 family instances. Consider this example from #18055:
  837 
  838   class C a where
  839     data D a
  840 
  841   class X a b
  842 
  843   instance C (Maybe a) where
  844     data D (Maybe a) deriving (X a)
  845 
  846 When typechecking the `X a` in `deriving (X a)`, we must ensure that the `a`
  847 from the instance header is brought into scope. This is the role of
  848 di_scoped_tvs, which maps from the original, renamed `a` to the skolemized,
  849 typechecked `a`. When typechecking the `deriving` clause, this mapping will be
  850 consulted when looking up the `a` in `X a`.
  851 
  852 A naïve attempt at creating the di_scoped_tvs is to simply reuse the
  853 tyConTyVars of the representation TyCon for `data D (Maybe a)`. This is only
  854 half correct, however. We do want the typechecked `a`'s Name in the /range/
  855 of the mapping, but we do not want it in the /domain/ of the mapping.
  856 To ensure that the original `a`'s Name ends up in the domain, we consult a
  857 TyVarEnv (passed as an argument to tcDataFamInstDecl) that maps from the
  858 typechecked `a`'s Name to the original `a`'s Name. In the even that
  859 tcDataFamInstDecl is processing a non-associated data family instance, this
  860 TyVarEnv will simply be empty, and there is nothing to worry about.
  861 -}
  862 
  863 -----------------------
  864 tcDataFamInstHeader
  865     :: AssocInstInfo -> TyCon -> HsOuterFamEqnTyVarBndrs GhcRn
  866     -> LexicalFixity -> Maybe (LHsContext GhcRn)
  867     -> HsTyPats GhcRn -> Maybe (LHsKind GhcRn)
  868     -> NewOrData
  869     -> TcM ([TyVar], [Type], Kind, ThetaType)
  870 -- The "header" of a data family instance is the part other than
  871 -- the data constructors themselves
  872 --    e.g.  data instance D [a] :: * -> * where ...
  873 -- Here the "header" is the bit before the "where"
  874 tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity
  875                     hs_ctxt hs_pats m_ksig new_or_data
  876   = do { traceTc "tcDataFamInstHeader {" (ppr fam_tc <+> ppr hs_pats)
  877        ; (tclvl, wanted, (scoped_tvs, (stupid_theta, lhs_ty, master_res_kind, instance_res_kind)))
  878             <- pushLevelAndSolveEqualitiesX "tcDataFamInstHeader" $
  879                bindOuterFamEqnTKBndrs outer_bndrs                 $
  880                do { stupid_theta <- tcHsContext hs_ctxt
  881                   ; (lhs_ty, lhs_kind) <- tcFamTyPats fam_tc hs_pats
  882                   ; (lhs_applied_ty, lhs_applied_kind)
  883                       <- tcInstInvisibleTyBinders lhs_ty lhs_kind
  884                       -- See Note [Data family/instance return kinds]
  885                       -- in GHC.Tc.TyCl point (DF3)
  886 
  887                   -- Ensure that the instance is consistent
  888                   -- with its parent class
  889                   ; addConsistencyConstraints mb_clsinfo lhs_ty
  890 
  891                   -- Add constraints from the result signature
  892                   ; res_kind <- tc_kind_sig m_ksig
  893 
  894                   -- Do not add constraints from the data constructors
  895                   -- See Note [Kind inference for data family instances]
  896 
  897                   -- Check that the result kind of the TyCon applied to its args
  898                   -- is compatible with the explicit signature (or Type, if there
  899                   -- is none)
  900                   ; let hs_lhs = nlHsTyConApp fixity (getName fam_tc) hs_pats
  901                   ; _ <- unifyKind (Just (ppr hs_lhs)) lhs_applied_kind res_kind
  902 
  903                   ; traceTc "tcDataFamInstHeader" $
  904                     vcat [ ppr fam_tc, ppr m_ksig, ppr lhs_applied_kind, ppr res_kind ]
  905                   ; return ( stupid_theta
  906                            , lhs_applied_ty
  907                            , lhs_applied_kind
  908                            , res_kind ) }
  909 
  910        -- This code (and the stuff immediately above) is very similar
  911        -- to that in tcTyFamInstEqnGuts.  Maybe we should abstract the
  912        -- common code; but for the moment I concluded that it's
  913        -- clearer to duplicate it.  Still, if you fix a bug here,
  914        -- check there too!
  915 
  916        -- See GHC.Tc.TyCl Note [Generalising in tcFamTyPatsGuts]
  917        ; dvs  <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys scoped_tvs)
  918        ; qtvs <- quantifyTyVars noVarsOfKindDefault dvs
  919        ; reportUnsolvedEqualities FamInstSkol qtvs tclvl wanted
  920 
  921        -- Zonk the patterns etc into the Type world
  922        ; ze           <- mkEmptyZonkEnv NoFlexi
  923        ; (ze, qtvs)   <- zonkTyBndrsX           ze qtvs
  924        ; lhs_ty       <- zonkTcTypeToTypeX      ze lhs_ty
  925        ; stupid_theta <- zonkTcTypesToTypesX    ze stupid_theta
  926        ; master_res_kind   <- zonkTcTypeToTypeX ze master_res_kind
  927        ; instance_res_kind <- zonkTcTypeToTypeX ze instance_res_kind
  928 
  929        -- We check that res_kind is OK with checkDataKindSig in
  930        -- tcDataFamInstDecl, after eta-expansion.  We need to check that
  931        -- it's ok because res_kind can come from a user-written kind signature.
  932        -- See Note [Datatype return kinds], point (4a)
  933 
  934        ; checkDataKindSig (DataInstanceSort new_or_data) master_res_kind
  935        ; checkDataKindSig (DataInstanceSort new_or_data) instance_res_kind
  936 
  937        -- Check that type patterns match the class instance head
  938        -- The call to splitTyConApp_maybe here is just an inlining of
  939        -- the body of unravelFamInstPats.
  940        ; pats <- case splitTyConApp_maybe lhs_ty of
  941            Just (_, pats) -> pure pats
  942            Nothing -> pprPanic "tcDataFamInstHeader" (ppr lhs_ty)
  943 
  944        ; return (qtvs, pats, master_res_kind, stupid_theta) }
  945   where
  946     fam_name  = tyConName fam_tc
  947     data_ctxt = DataKindCtxt fam_name
  948 
  949     -- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl, families (2),
  950     -- and Note [Implementation of UnliftedDatatypes].
  951     tc_kind_sig Nothing
  952       = do { unlifted_newtypes  <- xoptM LangExt.UnliftedNewtypes
  953            ; unlifted_datatypes <- xoptM LangExt.UnliftedDatatypes
  954            ; case new_or_data of
  955                NewType  | unlifted_newtypes  -> newOpenTypeKind
  956                DataType | unlifted_datatypes -> newOpenTypeKind
  957                _                             -> pure liftedTypeKind
  958            }
  959 
  960     -- See Note [Result kind signature for a data family instance]
  961     tc_kind_sig (Just hs_kind)
  962       = do { sig_kind <- tcLHsKindSig data_ctxt hs_kind
  963            ; lvl <- getTcLevel
  964            ; let (tvs, inner_kind) = tcSplitForAllInvisTyVars sig_kind
  965            ; (subst, _tvs') <- tcInstSkolTyVarsAt lvl False emptyTCvSubst tvs
  966              -- Perhaps surprisingly, we don't need the skolemised tvs themselves
  967            ; return (substTy subst inner_kind) }
  968 
  969 {- Note [Result kind signature for a data family instance]
  970 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  971 The expected type might have a forall at the type. Normally, we
  972 can't skolemise in kinds because we don't have type-level lambda.
  973 But here, we're at the top-level of an instance declaration, so
  974 we actually have a place to put the regeneralised variables.
  975 Thus: skolemise away. cf. GHC.Tc.Utils.Unify.tcSkolemise
  976 Examples in indexed-types/should_compile/T12369
  977 
  978 Note [Implementing eta reduction for data families]
  979 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  980 Consider
  981    data D :: * -> * -> * -> * -> *
  982 
  983    data instance D [(a,b)] p q :: * -> * where
  984       D1 :: blah1
  985       D2 :: blah2
  986 
  987 Then we'll generate a representation data type
  988   data Drep a b p q z where
  989       D1 :: blah1
  990       D2 :: blah2
  991 
  992 and an axiom to connect them
  993   axiom AxDrep forall a b p q z. D [(a,b]] p q z = Drep a b p q z
  994 
  995 except that we'll eta-reduce the axiom to
  996   axiom AxDrep forall a b. D [(a,b]] = Drep a b
  997 
  998 This is described at some length in Note [Eta reduction for data families]
  999 in GHC.Core.Coercion.Axiom. There are several fiddly subtleties lurking here,
 1000 however, so this Note aims to describe these subtleties:
 1001 
 1002 * The representation tycon Drep is parameterised over the free
 1003   variables of the pattern, in no particular order. So there is no
 1004   guarantee that 'p' and 'q' will come last in Drep's parameters, and
 1005   in the right order.  So, if the /patterns/ of the family instance
 1006   are eta-reducible, we re-order Drep's parameters to put the
 1007   eta-reduced type variables last.
 1008 
 1009 * Although we eta-reduce the axiom, we eta-/expand/ the representation
 1010   tycon Drep.  The kind of D says it takes four arguments, but the
 1011   data instance header only supplies three.  But the AlgTyCon for Drep
 1012   itself must have enough TyConBinders so that its result kind is Type.
 1013   So, with etaExpandAlgTyCon we make up some extra TyConBinders.
 1014   See point (3) in Note [Datatype return kinds] in GHC.Tc.TyCl.
 1015 
 1016 * The result kind in the instance might be a polykind, like this:
 1017      data family DP a :: forall k. k -> *
 1018      data instance DP [b] :: forall k1 k2. (k1,k2) -> *
 1019 
 1020   So in type-checking the LHS (DP Int) we need to check that it is
 1021   more polymorphic than the signature.  To do that we must skolemise
 1022   the signature and instantiate the call of DP.  So we end up with
 1023      data instance DP [b] @(k1,k2) (z :: (k1,k2)) where
 1024 
 1025   Note that we must parameterise the representation tycon DPrep over
 1026   'k1' and 'k2', as well as 'b'.
 1027 
 1028   The skolemise bit is done in tc_kind_sig, while the instantiate bit
 1029   is done by tcFamTyPats.
 1030 
 1031 * Very fiddly point.  When we eta-reduce to
 1032      axiom AxDrep forall a b. D [(a,b]] = Drep a b
 1033 
 1034   we want the kind of (D [(a,b)]) to be the same as the kind of
 1035   (Drep a b).  This ensures that applying the axiom doesn't change the
 1036   kind.  Why is that hard?  Because the kind of (Drep a b) depends on
 1037   the TyConBndrVis on Drep's arguments. In particular do we have
 1038     (forall (k::*). blah) or (* -> blah)?
 1039 
 1040   We must match whatever D does!  In #15817 we had
 1041       data family X a :: forall k. * -> *   -- Note: a forall that is not used
 1042       data instance X Int b = MkX
 1043 
 1044   So the data instance is really
 1045       data istance X Int @k b = MkX
 1046 
 1047   The axiom will look like
 1048       axiom    X Int = Xrep
 1049 
 1050   and it's important that XRep :: forall k * -> *, following X.
 1051 
 1052   To achieve this we get the TyConBndrVis flags from tcbVisibilities,
 1053   and use those flags for any eta-reduced arguments.  Sigh.
 1054 
 1055 * The final turn of the knife is that tcbVisibilities is itself
 1056   tricky to sort out.  Consider
 1057       data family D k :: k
 1058   Then consider D (forall k2. k2 -> k2) Type Type
 1059   The visibility flags on an application of D may affected by the arguments
 1060   themselves.  Heavy sigh.  But not truly hard; that's what tcbVisibilities
 1061   does.
 1062 
 1063 * Happily, we don't need to worry about the possibility of
 1064   building an inhomogeneous axiom, described in GHC.Tc.TyCl.Build
 1065   Note [Newtype eta and homogeneous axioms].   For example
 1066      type F :: Type -> forall (b :: Type) -> Type
 1067      data family F a b
 1068      newtype instance F Int b = MkF (Proxy b)
 1069   we get a newtype, and a eta-reduced axiom connecting the data family
 1070   with the newtype:
 1071      type R:FIntb :: forall (b :: Type) -> Type
 1072      newtype R:FIntb b = MkF (Proxy b)
 1073      axiom Foo.D:R:FIntb0 :: F Int = Foo.R:FIntb
 1074   Now the subtleties of Note [Newtype eta and homogeneous axioms] are
 1075   dealt with by the newtype (via mkNewTyConRhs called in tcDataFamInstDecl)
 1076   while the axiom connecting F Int ~ R:FIntb is eta-reduced, but the
 1077   quantifer 'b' is derived from the original data family F, and so the
 1078   kinds will always match.
 1079 
 1080 Note [Kind inference for data family instances]
 1081 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1082 Consider this GADT-style data type declaration, where I have used
 1083 fresh variables in the data constructor's type, to stress that c,d are
 1084 quite distinct from a,b.
 1085    data T a b where
 1086      MkT :: forall c d. c d -> T c d
 1087 
 1088 Following Note [Inferring kinds for type declarations] in GHC.Tc.TyCl,
 1089 to infer T's kind, we initially give T :: kappa, a monomorpic kind,
 1090 gather constraints from the header and data constructors, and conclude
 1091    T :: (kappa1 -> type) -> kappa1 -> Type
 1092 Then we generalise, giving
 1093    T :: forall k. (k->Type) -> k -> Type
 1094 
 1095 Now what about a data /instance/ decl
 1096    data family T :: forall k. (k->Type) -> k -> Type
 1097 
 1098    data instance T p Int where ...
 1099 
 1100 No doubt here! The poly-kinded T is instantiated with k=Type, so the
 1101 header really looks like
 1102    data instance T @Type (p :: Type->Type) Int where ...
 1103 
 1104 But what about this?
 1105    data instance T p q where
 1106       MkT :: forall r. r Int -> T r Int
 1107 
 1108 So what kind do 'p' and 'q' have?  No clues from the header, but from
 1109 the data constructor we can clearly see that (r :: Type->Type).  Does
 1110 that mean that the the /entire data instance/ is instantiated at Type,
 1111 like this?
 1112    data instance T @Type (p :: Type->Type) (q :: Type) where
 1113       ...
 1114 
 1115 Not at all! This is a /GADT/-style decl, so the kind argument might
 1116 be specialised in this particular data constructor, thus:
 1117    data instance T @k (p :: k->Type) (q :: k) where
 1118      MkT :: forall (r :: Type -> Type).
 1119             r Int -> T @Type r Int
 1120 (and perhaps specialised differently in some other data
 1121 constructor MkT2).
 1122 
 1123 The key difference in this case and 'data T' at the top of this Note
 1124 is that we have no known kind for 'data T'. We thus forbid different
 1125 specialisations of T in its constructors, in an attempt to avoid
 1126 inferring polymorphic recursion. In data family T, however, there is
 1127 no problem with polymorphic recursion: we already /fully know/ T's
 1128 kind -- that came from the family declaration, and is not influenced
 1129 by the data instances -- and hence we /can/ specialise T's kind
 1130 differently in different GADT data constructors.
 1131 
 1132 SHORT SUMMARY: in a data instance decl, it's not clear whether kind
 1133 constraints arising from the data constructors should be considered
 1134 local to the (GADT) data /constructor/ or should apply to the entire
 1135 data instance.
 1136 
 1137 DESIGN CHOICE: in data/newtype family instance declarations, we ignore
 1138 the /data constructor/ declarations altogether, looking only at the
 1139 data instance /header/.
 1140 
 1141 Observations:
 1142 * This choice is simple to describe, as well as simple to implement.
 1143   For a data/newtype instance decl, the instance kinds are influenced
 1144   /only/ by the header.
 1145 
 1146 * We could treat Haskell-98 style data-instance decls differently, by
 1147   taking the data constructors into account, since there are no GADT
 1148   issues.  But we don't, for simplicity, and because it means you can
 1149   understand the data type instance by looking only at the header.
 1150 
 1151 * Newtypes can be declared in GADT syntax, but they can't do GADT-style
 1152   specialisation, so like Haskell-98 definitions we could take the
 1153   data constructors into account.  Again we don't, for the same reason.
 1154 
 1155 So for now at least, we keep the simplest choice. See #18891 and !4419
 1156 for more discussion of this issue.
 1157 
 1158 Kind inference for data types (Xie et al) https://arxiv.org/abs/1911.06153
 1159 takes a slightly different approach.
 1160 -}
 1161 
 1162 
 1163 {- *********************************************************************
 1164 *                                                                      *
 1165       Class instance declarations, pass 2
 1166 *                                                                      *
 1167 ********************************************************************* -}
 1168 
 1169 tcInstDecls2 :: [LTyClDecl GhcRn] -> [InstInfo GhcRn] -> ClassScopedTVEnv
 1170              -> TcM (LHsBinds GhcTc)
 1171 -- (a) From each class declaration,
 1172 --      generate any default-method bindings
 1173 -- (b) From each instance decl
 1174 --      generate the dfun binding
 1175 
 1176 tcInstDecls2 tycl_decls inst_decls class_scoped_tv_env
 1177   = do  { -- (a) Default methods from class decls
 1178           let class_decls = filter (isClassDecl . unLoc) tycl_decls
 1179         ; dm_binds_s <- mapM (tcClassDecl2 class_scoped_tv_env) class_decls
 1180         ; let dm_binds = unionManyBags dm_binds_s
 1181 
 1182           -- (b) instance declarations
 1183         ; let dm_ids = collectHsBindsBinders CollNoDictBinders dm_binds
 1184               -- Add the default method Ids (again)
 1185               -- (they were already added in GHC.Tc.TyCl.Utils.tcAddImplicits)
 1186               -- See Note [Default methods in the type environment]
 1187         ; inst_binds_s <- tcExtendGlobalValEnv dm_ids $
 1188                           mapM tcInstDecl2 inst_decls
 1189 
 1190           -- Done
 1191         ; return (dm_binds `unionBags` unionManyBags inst_binds_s) }
 1192 
 1193 {- Note [Default methods in the type environment]
 1194 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1195 The default method Ids are already in the type environment (see Note
 1196 [Default method Ids and Template Haskell] in TcTyDcls), BUT they
 1197 don't have their InlinePragmas yet.  Usually that would not matter,
 1198 because the simplifier propagates information from binding site to
 1199 use.  But, unusually, when compiling instance decls we *copy* the
 1200 INLINE pragma from the default method to the method for that
 1201 particular operation (see Note [INLINE and default methods] below).
 1202 
 1203 So right here in tcInstDecls2 we must re-extend the type envt with
 1204 the default method Ids replete with their INLINE pragmas.  Urk.
 1205 -}
 1206 
 1207 tcInstDecl2 :: InstInfo GhcRn -> TcM (LHsBinds GhcTc)
 1208             -- Returns a binding for the dfun
 1209 tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
 1210   = recoverM (return emptyLHsBinds)             $
 1211     setSrcSpan loc                              $
 1212     addErrCtxt (instDeclCtxt2 (idType dfun_id)) $
 1213     do {  -- Instantiate the instance decl with skolem constants
 1214        ; (inst_tyvars, dfun_theta, inst_head) <- tcSkolDFunType dfun_id
 1215        ; dfun_ev_vars <- newEvVars dfun_theta
 1216                      -- We instantiate the dfun_id with superSkolems.
 1217                      -- See Note [Subtle interaction of recursion and overlap]
 1218                      -- and Note [Binding when looking up instances]
 1219 
 1220        ; let (clas, inst_tys) = tcSplitDFunHead inst_head
 1221              (class_tyvars, sc_theta, _, op_items) = classBigSig clas
 1222              sc_theta' = substTheta (zipTvSubst class_tyvars inst_tys) sc_theta
 1223 
 1224        ; traceTc "tcInstDecl2" (vcat [ppr inst_tyvars, ppr inst_tys, ppr dfun_theta, ppr sc_theta'])
 1225 
 1226                       -- Deal with 'SPECIALISE instance' pragmas
 1227                       -- See Note [SPECIALISE instance pragmas]
 1228        ; spec_inst_info@(spec_inst_prags,_) <- tcSpecInstPrags dfun_id ibinds
 1229 
 1230          -- Typecheck superclasses and methods
 1231          -- See Note [Typechecking plan for instance declarations]
 1232        ; dfun_ev_binds_var <- newTcEvBinds
 1233        ; let dfun_ev_binds = TcEvBinds dfun_ev_binds_var
 1234        ; (tclvl, (sc_meth_ids, sc_meth_binds, sc_meth_implics))
 1235              <- pushTcLevelM $
 1236                 do { (sc_ids, sc_binds, sc_implics)
 1237                         <- tcSuperClasses dfun_id clas inst_tyvars dfun_ev_vars
 1238                                           inst_tys dfun_ev_binds
 1239                                           sc_theta'
 1240 
 1241                       -- Typecheck the methods
 1242                    ; (meth_ids, meth_binds, meth_implics)
 1243                         <- tcMethods dfun_id clas inst_tyvars dfun_ev_vars
 1244                                      inst_tys dfun_ev_binds spec_inst_info
 1245                                      op_items ibinds
 1246 
 1247                    ; return ( sc_ids     ++          meth_ids
 1248                             , sc_binds   `unionBags` meth_binds
 1249                             , sc_implics `unionBags` meth_implics ) }
 1250 
 1251        ; imp <- newImplication
 1252        ; emitImplication $
 1253          imp { ic_tclvl  = tclvl
 1254              , ic_skols  = inst_tyvars
 1255              , ic_given  = dfun_ev_vars
 1256              , ic_wanted = mkImplicWC sc_meth_implics
 1257              , ic_binds  = dfun_ev_binds_var
 1258              , ic_info   = InstSkol }
 1259 
 1260        -- Create the result bindings
 1261        ; self_dict <- newDict clas inst_tys
 1262        ; let class_tc      = classTyCon clas
 1263              loc'          = noAnnSrcSpan loc
 1264              [dict_constr] = tyConDataCons class_tc
 1265              dict_bind = mkVarBind self_dict (L loc' con_app_args)
 1266 
 1267                      -- We don't produce a binding for the dict_constr; instead we
 1268                      -- rely on the simplifier to unfold this saturated application
 1269                      -- We do this rather than generate an HsCon directly, because
 1270                      -- it means that the special cases (e.g. dictionary with only one
 1271                      -- member) are dealt with by the common MkId.mkDataConWrapId
 1272                      -- code rather than needing to be repeated here.
 1273                      --    con_app_tys  = MkD ty1 ty2
 1274                      --    con_app_scs  = MkD ty1 ty2 sc1 sc2
 1275                      --    con_app_args = MkD ty1 ty2 sc1 sc2 op1 op2
 1276              con_app_tys  = mkHsWrap (mkWpTyApps inst_tys) $
 1277                             mkConLikeTc (RealDataCon dict_constr)
 1278                        -- NB: We *can* have covars in inst_tys, in the case of
 1279                        -- promoted GADT constructors.
 1280 
 1281              con_app_args = foldl' app_to_meth con_app_tys sc_meth_ids
 1282 
 1283              app_to_meth :: HsExpr GhcTc -> Id -> HsExpr GhcTc
 1284              app_to_meth fun meth_id = HsApp noComments (L loc' fun)
 1285                                             (L loc' (wrapId arg_wrapper meth_id))
 1286 
 1287              inst_tv_tys = mkTyVarTys inst_tyvars
 1288              arg_wrapper = mkWpEvVarApps dfun_ev_vars <.> mkWpTyApps inst_tv_tys
 1289 
 1290              is_newtype = isNewTyCon class_tc
 1291              dfun_id_w_prags = addDFunPrags dfun_id sc_meth_ids
 1292              dfun_spec_prags
 1293                 | is_newtype = SpecPrags []
 1294                 | otherwise  = SpecPrags spec_inst_prags
 1295                     -- Newtype dfuns just inline unconditionally,
 1296                     -- so don't attempt to specialise them
 1297 
 1298              export = ABE { abe_ext  = noExtField
 1299                           , abe_wrap = idHsWrapper
 1300                           , abe_poly = dfun_id_w_prags
 1301                           , abe_mono = self_dict
 1302                           , abe_prags = dfun_spec_prags }
 1303                           -- NB: see Note [SPECIALISE instance pragmas]
 1304              main_bind = AbsBinds { abs_ext = noExtField
 1305                                   , abs_tvs = inst_tyvars
 1306                                   , abs_ev_vars = dfun_ev_vars
 1307                                   , abs_exports = [export]
 1308                                   , abs_ev_binds = []
 1309                                   , abs_binds = unitBag dict_bind
 1310                                   , abs_sig = True }
 1311 
 1312        ; return (unitBag (L loc' main_bind)
 1313                   `unionBags` sc_meth_binds)
 1314        }
 1315  where
 1316    dfun_id = instanceDFunId ispec
 1317    loc     = getSrcSpan dfun_id
 1318 
 1319 addDFunPrags :: DFunId -> [Id] -> DFunId
 1320 -- DFuns need a special Unfolding and InlinePrag
 1321 --    See Note [ClassOp/DFun selection]
 1322 --    and Note [Single-method classes]
 1323 -- It's easiest to create those unfoldings right here, where
 1324 -- have all the pieces in hand, even though we are messing with
 1325 -- Core at this point, which the typechecker doesn't usually do
 1326 -- However we take care to build the unfolding using the TyVars from
 1327 -- the DFunId rather than from the skolem pieces that the typechecker
 1328 -- is messing with.
 1329 addDFunPrags dfun_id sc_meth_ids
 1330  | is_newtype
 1331   = dfun_id `setIdUnfolding`  mkInlineUnfoldingWithArity 0 defaultSimpleOpts con_app
 1332             `setInlinePragma` alwaysInlinePragma { inl_sat = Just 0 }
 1333  | otherwise
 1334  = dfun_id `setIdUnfolding`  mkDFunUnfolding dfun_bndrs dict_con dict_args
 1335            `setInlinePragma` dfunInlinePragma
 1336  where
 1337    con_app    = mkLams dfun_bndrs $
 1338                 mkApps (Var (dataConWrapId dict_con)) dict_args
 1339                 -- This application will satisfy the Core invariants
 1340                 -- from Note [Representation polymorphism invariants] in GHC.Core,
 1341                 -- because typeclass method types are never unlifted.
 1342    dict_args  = map Type inst_tys ++
 1343                 [mkVarApps (Var id) dfun_bndrs | id <- sc_meth_ids]
 1344 
 1345    (dfun_tvs, dfun_theta, clas, inst_tys) = tcSplitDFunTy (idType dfun_id)
 1346    ev_ids      = mkTemplateLocalsNum 1                    dfun_theta
 1347    dfun_bndrs  = dfun_tvs ++ ev_ids
 1348    clas_tc     = classTyCon clas
 1349    [dict_con]  = tyConDataCons clas_tc
 1350    is_newtype  = isNewTyCon clas_tc
 1351 
 1352 wrapId :: HsWrapper -> Id -> HsExpr GhcTc
 1353 wrapId wrapper id = mkHsWrap wrapper (HsVar noExtField (noLocA id))
 1354 
 1355 {- Note [Typechecking plan for instance declarations]
 1356 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1357 For instance declarations we generate the following bindings and implication
 1358 constraints.  Example:
 1359 
 1360    instance Ord a => Ord [a] where compare = <compare-rhs>
 1361 
 1362 generates this:
 1363 
 1364    Bindings:
 1365       -- Method bindings
 1366       $ccompare :: forall a. Ord a => a -> a -> Ordering
 1367       $ccompare = /\a \(d:Ord a). let <meth-ev-binds> in ...
 1368 
 1369       -- Superclass bindings
 1370       $cp1Ord :: forall a. Ord a => Eq [a]
 1371       $cp1Ord = /\a \(d:Ord a). let <sc-ev-binds>
 1372                in dfEqList (dw :: Eq a)
 1373 
 1374    Constraints:
 1375       forall a. Ord a =>
 1376                 -- Method constraint
 1377              (forall. (empty) => <constraints from compare-rhs>)
 1378                 -- Superclass constraint
 1379           /\ (forall. (empty) => dw :: Eq a)
 1380 
 1381 Notice that
 1382 
 1383  * Per-meth/sc implication.  There is one inner implication per
 1384    superclass or method, with no skolem variables or givens.  The only
 1385    reason for this one is to gather the evidence bindings privately
 1386    for this superclass or method.  This implication is generated
 1387    by checkInstConstraints.
 1388 
 1389  * Overall instance implication. There is an overall enclosing
 1390    implication for the whole instance declaration, with the expected
 1391    skolems and givens.  We need this to get the correct "redundant
 1392    constraint" warnings, gathering all the uses from all the methods
 1393    and superclasses.  See GHC.Tc.Solver Note [Tracking redundant
 1394    constraints]
 1395 
 1396  * The given constraints in the outer implication may generate
 1397    evidence, notably by superclass selection.  Since the method and
 1398    superclass bindings are top-level, we want that evidence copied
 1399    into *every* method or superclass definition.  (Some of it will
 1400    be usused in some, but dead-code elimination will drop it.)
 1401 
 1402    We achieve this by putting the evidence variable for the overall
 1403    instance implication into the AbsBinds for each method/superclass.
 1404    Hence the 'dfun_ev_binds' passed into tcMethods and tcSuperClasses.
 1405    (And that in turn is why the abs_ev_binds field of AbBinds is a
 1406    [TcEvBinds] rather than simply TcEvBinds.
 1407 
 1408    This is a bit of a hack, but works very nicely in practice.
 1409 
 1410  * Note that if a method has a locally-polymorphic binding, there will
 1411    be yet another implication for that, generated by tcPolyCheck
 1412    in tcMethodBody. E.g.
 1413           class C a where
 1414             foo :: forall b. Ord b => blah
 1415 
 1416 
 1417 ************************************************************************
 1418 *                                                                      *
 1419       Type-checking superclasses
 1420 *                                                                      *
 1421 ************************************************************************
 1422 -}
 1423 
 1424 tcSuperClasses :: DFunId -> Class -> [TcTyVar] -> [EvVar] -> [TcType]
 1425                -> TcEvBinds
 1426                -> TcThetaType
 1427                -> TcM ([EvVar], LHsBinds GhcTc, Bag Implication)
 1428 -- Make a new top-level function binding for each superclass,
 1429 -- something like
 1430 --    $Ordp1 :: forall a. Ord a => Eq [a]
 1431 --    $Ordp1 = /\a \(d:Ord a). dfunEqList a (sc_sel d)
 1432 --
 1433 -- See Note [Recursive superclasses] for why this is so hard!
 1434 -- In effect, we build a special-purpose solver for the first step
 1435 -- of solving each superclass constraint
 1436 tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds sc_theta
 1437   = do { (ids, binds, implics) <- mapAndUnzip3M tc_super (zip sc_theta [fIRST_TAG..])
 1438        ; return (ids, listToBag binds, listToBag implics) }
 1439   where
 1440     loc = getSrcSpan dfun_id
 1441     size = sizeTypes inst_tys
 1442     tc_super (sc_pred, n)
 1443       = do { (sc_implic, ev_binds_var, sc_ev_tm)
 1444                 <- checkInstConstraints $ emitWanted (ScOrigin size) sc_pred
 1445 
 1446            ; sc_top_name  <- newName (mkSuperDictAuxOcc n (getOccName cls))
 1447            ; sc_ev_id     <- newEvVar sc_pred
 1448            ; addTcEvBind ev_binds_var $ mkWantedEvBind sc_ev_id sc_ev_tm
 1449            ; let sc_top_ty = mkInfForAllTys tyvars $
 1450                              mkPhiTy (map idType dfun_evs) sc_pred
 1451                  sc_top_id = mkLocalId sc_top_name Many sc_top_ty
 1452                  export = ABE { abe_ext  = noExtField
 1453                               , abe_wrap = idHsWrapper
 1454                               , abe_poly = sc_top_id
 1455                               , abe_mono = sc_ev_id
 1456                               , abe_prags = noSpecPrags }
 1457                  local_ev_binds = TcEvBinds ev_binds_var
 1458                  bind = AbsBinds { abs_ext      = noExtField
 1459                                  , abs_tvs      = tyvars
 1460                                  , abs_ev_vars  = dfun_evs
 1461                                  , abs_exports  = [export]
 1462                                  , abs_ev_binds = [dfun_ev_binds, local_ev_binds]
 1463                                  , abs_binds    = emptyBag
 1464                                  , abs_sig      = False }
 1465            ; return (sc_top_id, L (noAnnSrcSpan loc) bind, sc_implic) }
 1466 
 1467 -------------------
 1468 checkInstConstraints :: TcM result
 1469                      -> TcM (Implication, EvBindsVar, result)
 1470 -- See Note [Typechecking plan for instance declarations]
 1471 checkInstConstraints thing_inside
 1472   = do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints  $
 1473                                     thing_inside
 1474 
 1475        ; ev_binds_var <- newTcEvBinds
 1476        ; implic <- newImplication
 1477        ; let implic' = implic { ic_tclvl  = tclvl
 1478                               , ic_wanted = wanted
 1479                               , ic_binds  = ev_binds_var
 1480                               , ic_info   = InstSkol }
 1481 
 1482        ; return (implic', ev_binds_var, result) }
 1483 
 1484 {-
 1485 Note [Recursive superclasses]
 1486 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1487 See #3731, #4809, #5751, #5913, #6117, #6161, which all
 1488 describe somewhat more complicated situations, but ones
 1489 encountered in practice.
 1490 
 1491 See also tests tcrun020, tcrun021, tcrun033, and #11427.
 1492 
 1493 ----- THE PROBLEM --------
 1494 The problem is that it is all too easy to create a class whose
 1495 superclass is bottom when it should not be.
 1496 
 1497 Consider the following (extreme) situation:
 1498         class C a => D a where ...
 1499         instance D [a] => D [a] where ...   (dfunD)
 1500         instance C [a] => C [a] where ...   (dfunC)
 1501 Although this looks wrong (assume D [a] to prove D [a]), it is only a
 1502 more extreme case of what happens with recursive dictionaries, and it
 1503 can, just about, make sense because the methods do some work before
 1504 recursing.
 1505 
 1506 To implement the dfunD we must generate code for the superclass C [a],
 1507 which we had better not get by superclass selection from the supplied
 1508 argument:
 1509        dfunD :: forall a. D [a] -> D [a]
 1510        dfunD = \d::D [a] -> MkD (scsel d) ..
 1511 
 1512 Otherwise if we later encounter a situation where
 1513 we have a [Wanted] dw::D [a] we might solve it thus:
 1514      dw := dfunD dw
 1515 Which is all fine except that now ** the superclass C is bottom **!
 1516 
 1517 The instance we want is:
 1518        dfunD :: forall a. D [a] -> D [a]
 1519        dfunD = \d::D [a] -> MkD (dfunC (scsel d)) ...
 1520 
 1521 ----- THE SOLUTION --------
 1522 The basic solution is simple: be very careful about using superclass
 1523 selection to generate a superclass witness in a dictionary function
 1524 definition.  More precisely:
 1525 
 1526   Superclass Invariant: in every class dictionary,
 1527                         every superclass dictionary field
 1528                         is non-bottom
 1529 
 1530 To achieve the Superclass Invariant, in a dfun definition we can
 1531 generate a guaranteed-non-bottom superclass witness from:
 1532   (sc1) one of the dictionary arguments itself (all non-bottom)
 1533   (sc2) an immediate superclass of a smaller dictionary
 1534   (sc3) a call of a dfun (always returns a dictionary constructor)
 1535 
 1536 The tricky case is (sc2).  We proceed by induction on the size of
 1537 the (type of) the dictionary, defined by GHC.Tc.Validity.sizeTypes.
 1538 Let's suppose we are building a dictionary of size 3, and
 1539 suppose the Superclass Invariant holds of smaller dictionaries.
 1540 Then if we have a smaller dictionary, its immediate superclasses
 1541 will be non-bottom by induction.
 1542 
 1543 What does "we have a smaller dictionary" mean?  It might be
 1544 one of the arguments of the instance, or one of its superclasses.
 1545 Here is an example, taken from CmmExpr:
 1546        class Ord r => UserOfRegs r a where ...
 1547 (i1)   instance UserOfRegs r a => UserOfRegs r (Maybe a) where
 1548 (i2)   instance (Ord r, UserOfRegs r CmmReg) => UserOfRegs r CmmExpr where
 1549 
 1550 For (i1) we can get the (Ord r) superclass by selection from (UserOfRegs r a),
 1551 since it is smaller than the thing we are building (UserOfRegs r (Maybe a).
 1552 
 1553 But for (i2) that isn't the case, so we must add an explicit, and
 1554 perhaps surprising, (Ord r) argument to the instance declaration.
 1555 
 1556 Here's another example from #6161:
 1557 
 1558        class       Super a => Duper a  where ...
 1559        class Duper (Fam a) => Foo a    where ...
 1560 (i3)   instance Foo a => Duper (Fam a) where ...
 1561 (i4)   instance              Foo Float where ...
 1562 
 1563 It would be horribly wrong to define
 1564    dfDuperFam :: Foo a -> Duper (Fam a)  -- from (i3)
 1565    dfDuperFam d = MkDuper (sc_sel1 (sc_sel2 d)) ...
 1566 
 1567    dfFooFloat :: Foo Float               -- from (i4)
 1568    dfFooFloat = MkFoo (dfDuperFam dfFooFloat) ...
 1569 
 1570 Now the Super superclass of Duper is definitely bottom!
 1571 
 1572 This won't happen because when processing (i3) we can use the
 1573 superclasses of (Foo a), which is smaller, namely Duper (Fam a).  But
 1574 that is *not* smaller than the target so we can't take *its*
 1575 superclasses.  As a result the program is rightly rejected, unless you
 1576 add (Super (Fam a)) to the context of (i3).
 1577 
 1578 Note [Solving superclass constraints]
 1579 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1580 How do we ensure that every superclass witness is generated by
 1581 one of (sc1) (sc2) or (sc3) in Note [Recursive superclasses].
 1582 Answer:
 1583 
 1584   * Superclass "wanted" constraints have CtOrigin of (ScOrigin size)
 1585     where 'size' is the size of the instance declaration. e.g.
 1586           class C a => D a where...
 1587           instance blah => D [a] where ...
 1588     The wanted superclass constraint for C [a] has origin
 1589     ScOrigin size, where size = size( D [a] ).
 1590 
 1591   * (sc1) When we rewrite such a wanted constraint, it retains its
 1592     origin.  But if we apply an instance declaration, we can set the
 1593     origin to (ScOrigin infinity), thus lifting any restrictions by
 1594     making prohibitedSuperClassSolve return False.
 1595 
 1596   * (sc2) ScOrigin wanted constraints can't be solved from a
 1597     superclass selection, except at a smaller type.  This test is
 1598     implemented by GHC.Tc.Solver.Interact.prohibitedSuperClassSolve
 1599 
 1600   * The "given" constraints of an instance decl have CtOrigin
 1601     GivenOrigin InstSkol.
 1602 
 1603   * When we make a superclass selection from InstSkol we use
 1604     a SkolemInfo of (InstSC size), where 'size' is the size of
 1605     the constraint whose superclass we are taking.  A similarly
 1606     when taking the superclass of an InstSC.  This is implemented
 1607     in GHC.Tc.Solver.Canonical.newSCWorkFromFlavored
 1608 
 1609 Note [Silent superclass arguments] (historical interest only)
 1610 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1611 NB1: this note describes our *old* solution to the
 1612      recursive-superclass problem. I'm keeping the Note
 1613      for now, just as institutional memory.
 1614      However, the code for silent superclass arguments
 1615      was removed in late Dec 2014
 1616 
 1617 NB2: the silent-superclass solution introduced new problems
 1618      of its own, in the form of instance overlap.  Tests
 1619      SilentParametersOverlapping, T5051, and T7862 are examples
 1620 
 1621 NB3: the silent-superclass solution also generated tons of
 1622      extra dictionaries.  For example, in monad-transformer
 1623      code, when constructing a Monad dictionary you had to pass
 1624      an Applicative dictionary; and to construct that you need
 1625      a Functor dictionary. Yet these extra dictionaries were
 1626      often never used.  Test T3064 compiled *far* faster after
 1627      silent superclasses were eliminated.
 1628 
 1629 Our solution to this problem "silent superclass arguments".  We pass
 1630 to each dfun some ``silent superclass arguments’’, which are the
 1631 immediate superclasses of the dictionary we are trying to
 1632 construct. In our example:
 1633        dfun :: forall a. C [a] -> D [a] -> D [a]
 1634        dfun = \(dc::C [a]) (dd::D [a]) -> DOrd dc ...
 1635 Notice the extra (dc :: C [a]) argument compared to the previous version.
 1636 
 1637 This gives us:
 1638 
 1639      -----------------------------------------------------------
 1640      DFun Superclass Invariant
 1641      ~~~~~~~~~~~~~~~~~~~~~~~~
 1642      In the body of a DFun, every superclass argument to the
 1643      returned dictionary is
 1644        either   * one of the arguments of the DFun,
 1645        or       * constant, bound at top level
 1646      -----------------------------------------------------------
 1647 
 1648 This net effect is that it is safe to treat a dfun application as
 1649 wrapping a dictionary constructor around its arguments (in particular,
 1650 a dfun never picks superclasses from the arguments under the
 1651 dictionary constructor). No superclass is hidden inside a dfun
 1652 application.
 1653 
 1654 The extra arguments required to satisfy the DFun Superclass Invariant
 1655 always come first, and are called the "silent" arguments.  You can
 1656 find out how many silent arguments there are using Id.dfunNSilent;
 1657 and then you can just drop that number of arguments to see the ones
 1658 that were in the original instance declaration.
 1659 
 1660 DFun types are built (only) by MkId.mkDictFunId, so that is where we
 1661 decide what silent arguments are to be added.
 1662 -}
 1663 
 1664 {-
 1665 ************************************************************************
 1666 *                                                                      *
 1667       Type-checking an instance method
 1668 *                                                                      *
 1669 ************************************************************************
 1670 
 1671 tcMethod
 1672 - Make the method bindings, as a [(NonRec, HsBinds)], one per method
 1673 - Remembering to use fresh Name (the instance method Name) as the binder
 1674 - Bring the instance method Ids into scope, for the benefit of tcInstSig
 1675 - Use sig_fn mapping instance method Name -> instance tyvars
 1676 - Ditto prag_fn
 1677 - Use tcValBinds to do the checking
 1678 -}
 1679 
 1680 tcMethods :: DFunId -> Class
 1681           -> [TcTyVar] -> [EvVar]
 1682           -> [TcType]
 1683           -> TcEvBinds
 1684           -> ([LTcSpecPrag], TcPragEnv)
 1685           -> [ClassOpItem]
 1686           -> InstBindings GhcRn
 1687           -> TcM ([Id], LHsBinds GhcTc, Bag Implication)
 1688         -- The returned inst_meth_ids all have types starting
 1689         --      forall tvs. theta => ...
 1690 tcMethods dfun_id clas tyvars dfun_ev_vars inst_tys
 1691                   dfun_ev_binds (spec_inst_prags, prag_fn) op_items
 1692                   (InstBindings { ib_binds      = binds
 1693                                 , ib_tyvars     = lexical_tvs
 1694                                 , ib_pragmas    = sigs
 1695                                 , ib_extensions = exts
 1696                                 , ib_derived    = is_derived })
 1697   = tcExtendNameTyVarEnv (lexical_tvs `zip` tyvars) $
 1698        -- The lexical_tvs scope over the 'where' part
 1699     do { traceTc "tcInstMeth" (ppr sigs $$ ppr binds)
 1700        ; checkMinimalDefinition
 1701        ; checkMethBindMembership
 1702        ; (ids, binds, mb_implics) <- set_exts exts $
 1703                                      unset_warnings_deriving $
 1704                                      mapAndUnzip3M tc_item op_items
 1705        ; return (ids, listToBag binds, listToBag (catMaybes mb_implics)) }
 1706   where
 1707     set_exts :: [LangExt.Extension] -> TcM a -> TcM a
 1708     set_exts es thing = foldr setXOptM thing es
 1709 
 1710     -- See Note [Avoid -Winaccessible-code when deriving]
 1711     unset_warnings_deriving :: TcM a -> TcM a
 1712     unset_warnings_deriving
 1713       | is_derived = unsetWOptM Opt_WarnInaccessibleCode
 1714       | otherwise  = id
 1715 
 1716     hs_sig_fn = mkHsSigFun sigs
 1717     inst_loc  = getSrcSpan dfun_id
 1718 
 1719     ----------------------
 1720     tc_item :: ClassOpItem -> TcM (Id, LHsBind GhcTc, Maybe Implication)
 1721     tc_item (sel_id, dm_info)
 1722       | Just (user_bind, bndr_loc, prags) <- findMethodBind (idName sel_id) binds prag_fn
 1723       = tcMethodBody clas tyvars dfun_ev_vars inst_tys
 1724                               dfun_ev_binds is_derived hs_sig_fn
 1725                               spec_inst_prags prags
 1726                               sel_id user_bind bndr_loc
 1727       | otherwise
 1728       = do { traceTc "tc_def" (ppr sel_id)
 1729            ; tc_default sel_id dm_info }
 1730 
 1731     ----------------------
 1732     tc_default :: Id -> DefMethInfo
 1733                -> TcM (TcId, LHsBind GhcTc, Maybe Implication)
 1734 
 1735     tc_default sel_id (Just (dm_name, _))
 1736       = do { (meth_bind, inline_prags) <- mkDefMethBind dfun_id clas sel_id dm_name
 1737            ; tcMethodBody clas tyvars dfun_ev_vars inst_tys
 1738                           dfun_ev_binds is_derived hs_sig_fn
 1739                           spec_inst_prags inline_prags
 1740                           sel_id meth_bind inst_loc }
 1741 
 1742     tc_default sel_id Nothing     -- No default method at all
 1743       = do { traceTc "tc_def: warn" (ppr sel_id)
 1744            ; (meth_id, _) <- mkMethIds clas tyvars dfun_ev_vars
 1745                                        inst_tys sel_id
 1746            ; dflags <- getDynFlags
 1747            ; let meth_bind = mkVarBind meth_id $
 1748                              mkLHsWrap lam_wrapper (error_rhs dflags)
 1749            ; return (meth_id, meth_bind, Nothing) }
 1750       where
 1751         inst_loc' = noAnnSrcSpan inst_loc
 1752         error_rhs dflags = L inst_loc'
 1753                                  $ HsApp noComments error_fun (error_msg dflags)
 1754         error_fun    = L inst_loc' $
 1755                        wrapId (mkWpTyApps
 1756                                 [ getRuntimeRep meth_tau, meth_tau])
 1757                               nO_METHOD_BINDING_ERROR_ID
 1758         error_msg dflags = L inst_loc'
 1759                                     (HsLit noComments (HsStringPrim NoSourceText
 1760                                               (unsafeMkByteString (error_string dflags))))
 1761         meth_tau     = classMethodInstTy sel_id inst_tys
 1762         error_string dflags = showSDoc dflags
 1763                               (hcat [ppr inst_loc, vbar, ppr sel_id ])
 1764         lam_wrapper  = mkWpTyLams tyvars <.> mkWpLams dfun_ev_vars
 1765 
 1766     ----------------------
 1767     -- Check if one of the minimal complete definitions is satisfied
 1768     checkMinimalDefinition
 1769       = whenIsJust (isUnsatisfied methodExists (classMinimalDef clas)) $
 1770         warnUnsatisfiedMinimalDefinition
 1771 
 1772     methodExists meth = isJust (findMethodBind meth binds prag_fn)
 1773 
 1774     ----------------------
 1775     -- Check if any method bindings do not correspond to the class.
 1776     -- See Note [Mismatched class methods and associated type families].
 1777     checkMethBindMembership
 1778       = mapM_ (addErrTc . badMethodErr clas) mismatched_meths
 1779       where
 1780         bind_nms         = map unLoc $ collectMethodBinders binds
 1781         cls_meth_nms     = map (idName . fst) op_items
 1782         mismatched_meths = bind_nms `minusList` cls_meth_nms
 1783 
 1784 {-
 1785 Note [Mismatched class methods and associated type families]
 1786 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1787 It's entirely possible for someone to put methods or associated type family
 1788 instances inside of a class in which it doesn't belong. For instance, we'd
 1789 want to fail if someone wrote this:
 1790 
 1791   instance Eq () where
 1792     type Rep () = Maybe
 1793     compare = undefined
 1794 
 1795 Since neither the type family `Rep` nor the method `compare` belong to the
 1796 class `Eq`. Normally, this is caught in the renamer when resolving RdrNames,
 1797 since that would discover that the parent class `Eq` is incorrect.
 1798 
 1799 However, there is a scenario in which the renamer could fail to catch this:
 1800 if the instance was generated through Template Haskell, as in #12387. In that
 1801 case, Template Haskell will provide fully resolved names (e.g.,
 1802 `GHC.Classes.compare`), so the renamer won't notice the sleight-of-hand going
 1803 on. For this reason, we also put an extra validity check for this in the
 1804 typechecker as a last resort.
 1805 
 1806 Note [Avoid -Winaccessible-code when deriving]
 1807 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1808 -Winaccessible-code can be particularly noisy when deriving instances for
 1809 GADTs. Consider the following example (adapted from #8128):
 1810 
 1811   data T a where
 1812     MkT1 :: Int -> T Int
 1813     MkT2 :: T Bool
 1814     MkT3 :: T Bool
 1815   deriving instance Eq (T a)
 1816   deriving instance Ord (T a)
 1817 
 1818 In the derived Ord instance, GHC will generate the following code:
 1819 
 1820   instance Ord (T a) where
 1821     compare x y
 1822       = case x of
 1823           MkT2
 1824             -> case y of
 1825                  MkT1 {} -> GT
 1826                  MkT2    -> EQ
 1827                  _       -> LT
 1828           ...
 1829 
 1830 However, that MkT1 is unreachable, since the type indices for MkT1 and MkT2
 1831 differ, so if -Winaccessible-code is enabled, then deriving this instance will
 1832 result in unwelcome warnings.
 1833 
 1834 One conceivable approach to fixing this issue would be to change `deriving Ord`
 1835 such that it becomes smarter about not generating unreachable cases. This,
 1836 however, would be a highly nontrivial refactor, as we'd have to propagate
 1837 through typing information everywhere in the algorithm that generates Ord
 1838 instances in order to determine which cases were unreachable. This seems like
 1839 a lot of work for minimal gain, so we have opted not to go for this approach.
 1840 
 1841 Instead, we take the much simpler approach of always disabling
 1842 -Winaccessible-code for derived code. To accomplish this, we do the following:
 1843 
 1844 1. In tcMethods (which typechecks method bindings), disable
 1845    -Winaccessible-code.
 1846 2. When creating Implications during typechecking, record this flag
 1847    (in ic_warn_inaccessible) at the time of creation.
 1848 3. After typechecking comes error reporting, where GHC must decide how to
 1849    report inaccessible code to the user, on an Implication-by-Implication
 1850    basis. If an Implication's DynFlags indicate that -Winaccessible-code was
 1851    disabled, then don't bother reporting it. That's it!
 1852 -}
 1853 
 1854 ------------------------
 1855 tcMethodBody :: Class -> [TcTyVar] -> [EvVar] -> [TcType]
 1856              -> TcEvBinds -> Bool
 1857              -> HsSigFun
 1858              -> [LTcSpecPrag] -> [LSig GhcRn]
 1859              -> Id -> LHsBind GhcRn -> SrcSpan
 1860              -> TcM (TcId, LHsBind GhcTc, Maybe Implication)
 1861 tcMethodBody clas tyvars dfun_ev_vars inst_tys
 1862                      dfun_ev_binds is_derived
 1863                      sig_fn spec_inst_prags prags
 1864                      sel_id (L bind_loc meth_bind) bndr_loc
 1865   = add_meth_ctxt $
 1866     do { traceTc "tcMethodBody" (ppr sel_id <+> ppr (idType sel_id) $$ ppr bndr_loc)
 1867        ; (global_meth_id, local_meth_id) <- setSrcSpan bndr_loc $
 1868                                             mkMethIds clas tyvars dfun_ev_vars
 1869                                                       inst_tys sel_id
 1870 
 1871        ; let lm_bind = meth_bind { fun_id = L (noAnnSrcSpan bndr_loc)
 1872                                                         (idName local_meth_id) }
 1873                        -- Substitute the local_meth_name for the binder
 1874                        -- NB: the binding is always a FunBind
 1875 
 1876             -- taking instance signature into account might change the type of
 1877             -- the local_meth_id
 1878        ; (meth_implic, ev_binds_var, tc_bind)
 1879              <- checkInstConstraints $
 1880                 tcMethodBodyHelp sig_fn sel_id local_meth_id (L bind_loc lm_bind)
 1881 
 1882        ; global_meth_id <- addInlinePrags global_meth_id prags
 1883        ; spec_prags     <- tcSpecPrags global_meth_id prags
 1884 
 1885         ; let specs  = mk_meth_spec_prags global_meth_id spec_inst_prags spec_prags
 1886               export = ABE { abe_ext   = noExtField
 1887                            , abe_poly  = global_meth_id
 1888                            , abe_mono  = local_meth_id
 1889                            , abe_wrap  = idHsWrapper
 1890                            , abe_prags = specs }
 1891 
 1892               local_ev_binds = TcEvBinds ev_binds_var
 1893               full_bind = AbsBinds { abs_ext      = noExtField
 1894                                    , abs_tvs      = tyvars
 1895                                    , abs_ev_vars  = dfun_ev_vars
 1896                                    , abs_exports  = [export]
 1897                                    , abs_ev_binds = [dfun_ev_binds, local_ev_binds]
 1898                                    , abs_binds    = tc_bind
 1899                                    , abs_sig      = True }
 1900 
 1901         ; return (global_meth_id, L bind_loc full_bind, Just meth_implic) }
 1902   where
 1903         -- For instance decls that come from deriving clauses
 1904         -- we want to print out the full source code if there's an error
 1905         -- because otherwise the user won't see the code at all
 1906     add_meth_ctxt thing
 1907       | is_derived = addLandmarkErrCtxt (derivBindCtxt sel_id clas inst_tys) thing
 1908       | otherwise  = thing
 1909 
 1910 tcMethodBodyHelp :: HsSigFun -> Id -> TcId
 1911                  -> LHsBind GhcRn -> TcM (LHsBinds GhcTc)
 1912 tcMethodBodyHelp hs_sig_fn sel_id local_meth_id meth_bind
 1913   | Just hs_sig_ty <- hs_sig_fn sel_name
 1914               -- There is a signature in the instance
 1915               -- See Note [Instance method signatures]
 1916   = do { (sig_ty, hs_wrap)
 1917              <- setSrcSpan (getLocA hs_sig_ty) $
 1918                 do { inst_sigs <- xoptM LangExt.InstanceSigs
 1919                    ; checkTc inst_sigs (misplacedInstSig sel_name hs_sig_ty)
 1920                    ; let ctxt = FunSigCtxt sel_name NoRRC
 1921                    ; sig_ty  <- tcHsSigType ctxt hs_sig_ty
 1922                    ; let local_meth_ty = idType local_meth_id
 1923                                 -- False <=> do not report redundant constraints when
 1924                                 --           checking instance-sig <= class-meth-sig
 1925                                 -- The instance-sig is the focus here; the class-meth-sig
 1926                                 -- is fixed (#18036)
 1927                    ; hs_wrap <- addErrCtxtM (methSigCtxt sel_name sig_ty local_meth_ty) $
 1928                                 tcSubTypeSigma ctxt sig_ty local_meth_ty
 1929                    ; return (sig_ty, hs_wrap) }
 1930 
 1931        ; inner_meth_name <- newName (nameOccName sel_name)
 1932        ; let ctxt = FunSigCtxt sel_name (lhsSigTypeContextSpan hs_sig_ty)
 1933                     -- WantRCC <=> check for redundant constraints in the
 1934                     --          user-specified instance signature
 1935              inner_meth_id  = mkLocalId inner_meth_name Many sig_ty
 1936              inner_meth_sig = CompleteSig { sig_bndr = inner_meth_id
 1937                                           , sig_ctxt = ctxt
 1938                                           , sig_loc  = getLocA hs_sig_ty }
 1939 
 1940 
 1941        ; (tc_bind, [inner_id]) <- tcPolyCheck no_prag_fn inner_meth_sig meth_bind
 1942 
 1943        ; let export = ABE { abe_ext   = noExtField
 1944                           , abe_poly  = local_meth_id
 1945                           , abe_mono  = inner_id
 1946                           , abe_wrap  = hs_wrap
 1947                           , abe_prags = noSpecPrags }
 1948 
 1949        ; return (unitBag $ L (getLoc meth_bind) $
 1950                  AbsBinds { abs_ext = noExtField, abs_tvs = [], abs_ev_vars = []
 1951                           , abs_exports = [export]
 1952                           , abs_binds = tc_bind, abs_ev_binds = []
 1953                           , abs_sig = True }) }
 1954 
 1955   | otherwise  -- No instance signature
 1956   = do { let ctxt = FunSigCtxt sel_name NoRRC
 1957                     -- NoRRC <=> don't report redundant constraints
 1958                     -- The signature is not under the users control!
 1959              tc_sig = completeSigFromId ctxt local_meth_id
 1960               -- Absent a type sig, there are no new scoped type variables here
 1961               -- Only the ones from the instance decl itself, which are already
 1962               -- in scope.  Example:
 1963               --      class C a where { op :: forall b. Eq b => ... }
 1964               --      instance C [c] where { op = <rhs> }
 1965               -- In <rhs>, 'c' is scope but 'b' is not!
 1966 
 1967        ; (tc_bind, _) <- tcPolyCheck no_prag_fn tc_sig meth_bind
 1968        ; return tc_bind }
 1969 
 1970   where
 1971     sel_name   = idName sel_id
 1972     no_prag_fn = emptyPragEnv   -- No pragmas for local_meth_id;
 1973                                 -- they are all for meth_id
 1974 
 1975 ------------------------
 1976 mkMethIds :: Class -> [TcTyVar] -> [EvVar]
 1977           -> [TcType] -> Id -> TcM (TcId, TcId)
 1978              -- returns (poly_id, local_id), but ignoring any instance signature
 1979              -- See Note [Instance method signatures]
 1980 mkMethIds clas tyvars dfun_ev_vars inst_tys sel_id
 1981   = do  { poly_meth_name  <- newName (mkClassOpAuxOcc sel_occ)
 1982         ; local_meth_name <- newName sel_occ
 1983                   -- Base the local_meth_name on the selector name, because
 1984                   -- type errors from tcMethodBody come from here
 1985         ; let poly_meth_id  = mkLocalId poly_meth_name  Many poly_meth_ty
 1986               local_meth_id = mkLocalId local_meth_name Many local_meth_ty
 1987 
 1988         ; return (poly_meth_id, local_meth_id) }
 1989   where
 1990     sel_name      = idName sel_id
 1991     -- Force so that a thunk doesn't end up in a Name (#19619)
 1992     !sel_occ      = nameOccName sel_name
 1993     local_meth_ty = instantiateMethod clas sel_id inst_tys
 1994     poly_meth_ty  = mkSpecSigmaTy tyvars theta local_meth_ty
 1995     theta         = map idType dfun_ev_vars
 1996 
 1997 methSigCtxt :: Name -> TcType -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
 1998 methSigCtxt sel_name sig_ty meth_ty env0
 1999   = do { (env1, sig_ty)  <- zonkTidyTcType env0 sig_ty
 2000        ; (env2, meth_ty) <- zonkTidyTcType env1 meth_ty
 2001        ; let msg = hang (text "When checking that instance signature for" <+> quotes (ppr sel_name))
 2002                       2 (vcat [ text "is more general than its signature in the class"
 2003                               , text "Instance sig:" <+> ppr sig_ty
 2004                               , text "   Class sig:" <+> ppr meth_ty ])
 2005        ; return (env2, msg) }
 2006 
 2007 misplacedInstSig :: Name -> LHsSigType GhcRn -> TcRnMessage
 2008 misplacedInstSig name hs_ty
 2009   = TcRnUnknownMessage $ mkPlainError noHints $
 2010     vcat [ hang (text "Illegal type signature in instance declaration:")
 2011               2 (hang (pprPrefixName name)
 2012                     2 (dcolon <+> ppr hs_ty))
 2013          , text "(Use InstanceSigs to allow this)" ]
 2014 
 2015 {- Note [Instance method signatures]
 2016 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2017 With -XInstanceSigs we allow the user to supply a signature for the
 2018 method in an instance declaration.  Here is an artificial example:
 2019 
 2020        data T a = MkT a
 2021        instance Ord a => Ord (T a) where
 2022          (>) :: forall b. b -> b -> Bool
 2023          (>) = error "You can't compare Ts"
 2024 
 2025 The instance signature can be *more* polymorphic than the instantiated
 2026 class method (in this case: Age -> Age -> Bool), but it cannot be less
 2027 polymorphic.  Moreover, if a signature is given, the implementation
 2028 code should match the signature, and type variables bound in the
 2029 singature should scope over the method body.
 2030 
 2031 We achieve this by building a TcSigInfo for the method, whether or not
 2032 there is an instance method signature, and using that to typecheck
 2033 the declaration (in tcMethodBody).  That means, conveniently,
 2034 that the type variables bound in the signature will scope over the body.
 2035 
 2036 What about the check that the instance method signature is more
 2037 polymorphic than the instantiated class method type?  We just do a
 2038 tcSubType call in tcMethodBodyHelp, and generate a nested AbsBind, like
 2039 this (for the example above
 2040 
 2041  AbsBind { abs_tvs = [a], abs_ev_vars = [d:Ord a]
 2042          , abs_exports
 2043              = ABExport { (>) :: forall a. Ord a => T a -> T a -> Bool
 2044                         , gr_lcl :: T a -> T a -> Bool }
 2045          , abs_binds
 2046              = AbsBind { abs_tvs = [], abs_ev_vars = []
 2047                        , abs_exports = ABExport { gr_lcl :: T a -> T a -> Bool
 2048                                                 , gr_inner :: forall b. b -> b -> Bool }
 2049                        , abs_binds = AbsBind { abs_tvs = [b], abs_ev_vars = []
 2050                                              , ..etc.. }
 2051                } }
 2052 
 2053 Wow!  Three nested AbsBinds!
 2054  * The outer one abstracts over the tyvars and dicts for the instance
 2055  * The middle one is only present if there is an instance signature,
 2056    and does the impedance matching for that signature
 2057  * The inner one is for the method binding itself against either the
 2058    signature from the class, or the instance signature.
 2059 -}
 2060 
 2061 ----------------------
 2062 mk_meth_spec_prags :: Id -> [LTcSpecPrag] -> [LTcSpecPrag] -> TcSpecPrags
 2063         -- Adapt the 'SPECIALISE instance' pragmas to work for this method Id
 2064         -- There are two sources:
 2065         --   * spec_prags_for_me: {-# SPECIALISE op :: <blah> #-}
 2066         --   * spec_prags_from_inst: derived from {-# SPECIALISE instance :: <blah> #-}
 2067         --     These ones have the dfun inside, but [perhaps surprisingly]
 2068         --     the correct wrapper.
 2069         -- See Note [Handling SPECIALISE pragmas] in GHC.Tc.Gen.Bind
 2070 mk_meth_spec_prags meth_id spec_inst_prags spec_prags_for_me
 2071   = SpecPrags (spec_prags_for_me ++ spec_prags_from_inst)
 2072   where
 2073     spec_prags_from_inst
 2074        | isInlinePragma (idInlinePragma meth_id)
 2075        = []  -- Do not inherit SPECIALISE from the instance if the
 2076              -- method is marked INLINE, because then it'll be inlined
 2077              -- and the specialisation would do nothing. (Indeed it'll provoke
 2078              -- a warning from the desugarer
 2079        | otherwise
 2080        = [ L inst_loc (SpecPrag meth_id wrap inl)
 2081          | L inst_loc (SpecPrag _       wrap inl) <- spec_inst_prags]
 2082 
 2083 
 2084 mkDefMethBind :: DFunId -> Class -> Id -> Name
 2085               -> TcM (LHsBind GhcRn, [LSig GhcRn])
 2086 -- The is a default method (vanailla or generic) defined in the class
 2087 -- So make a binding   op = $dmop @t1 @t2
 2088 -- where $dmop is the name of the default method in the class,
 2089 -- and t1,t2 are the instance types.
 2090 -- See Note [Default methods in instances] for why we use
 2091 -- visible type application here
 2092 mkDefMethBind dfun_id clas sel_id dm_name
 2093   = do  { logger <- getLogger
 2094         ; dm_id <- tcLookupId dm_name
 2095         ; let inline_prag = idInlinePragma dm_id
 2096               inline_prags | isAnyInlinePragma inline_prag
 2097                            = [noLocA (InlineSig noAnn fn inline_prag)]
 2098                            | otherwise
 2099                            = []
 2100                  -- Copy the inline pragma (if any) from the default method
 2101                  -- to this version. Note [INLINE and default methods]
 2102 
 2103               fn   = noLocA (idName sel_id)
 2104               visible_inst_tys = [ ty | (tcb, ty) <- tyConBinders (classTyCon clas) `zip` inst_tys
 2105                                       , tyConBinderArgFlag tcb /= Inferred ]
 2106               rhs  = foldl' mk_vta (nlHsVar dm_name) visible_inst_tys
 2107               bind = noLocA $ mkTopFunBind Generated fn $
 2108                              [mkSimpleMatch (mkPrefixFunRhs fn) [] rhs]
 2109 
 2110         ; liftIO (putDumpFileMaybe logger Opt_D_dump_deriv "Filling in method body"
 2111                    FormatHaskell
 2112                    (vcat [ppr clas <+> ppr inst_tys,
 2113                           nest 2 (ppr sel_id <+> equals <+> ppr rhs)]))
 2114 
 2115        ; return (bind, inline_prags) }
 2116   where
 2117     (_, _, _, inst_tys) = tcSplitDFunTy (idType dfun_id)
 2118 
 2119     mk_vta :: LHsExpr GhcRn -> Type -> LHsExpr GhcRn
 2120     mk_vta fun ty = noLocA (HsAppType noExtField fun (mkEmptyWildCardBndrs $ nlHsParTy
 2121                                                 $ noLocA $ XHsType ty))
 2122        -- NB: use visible type application
 2123        -- See Note [Default methods in instances]
 2124 
 2125 ----------------------
 2126 derivBindCtxt :: Id -> Class -> [Type ] -> SDoc
 2127 derivBindCtxt sel_id clas tys
 2128    = vcat [ text "When typechecking the code for" <+> quotes (ppr sel_id)
 2129           , nest 2 (text "in a derived instance for"
 2130                     <+> quotes (pprClassPred clas tys) <> colon)
 2131           , nest 2 $ text "To see the code I am typechecking, use -ddump-deriv" ]
 2132 
 2133 warnUnsatisfiedMinimalDefinition :: ClassMinimalDef -> TcM ()
 2134 warnUnsatisfiedMinimalDefinition mindef
 2135   = do { warn <- woptM Opt_WarnMissingMethods
 2136        ; let msg = TcRnUnknownMessage $
 2137                mkPlainDiagnostic (WarningWithFlag Opt_WarnMissingMethods) noHints message
 2138        ; diagnosticTc warn msg
 2139        }
 2140   where
 2141     message = vcat [text "No explicit implementation for"
 2142                    ,nest 2 $ pprBooleanFormulaNice mindef
 2143                    ]
 2144 
 2145 {-
 2146 Note [Export helper functions]
 2147 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2148 We arrange to export the "helper functions" of an instance declaration,
 2149 so that they are not subject to preInlineUnconditionally, even if their
 2150 RHS is trivial.  Reason: they are mentioned in the DFunUnfolding of
 2151 the dict fun as Ids, not as CoreExprs, so we can't substitute a
 2152 non-variable for them.
 2153 
 2154 We could change this by making DFunUnfoldings have CoreExprs, but it
 2155 seems a bit simpler this way.
 2156 
 2157 Note [Default methods in instances]
 2158 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2159 Consider this
 2160 
 2161    class Baz v x where
 2162       foo :: x -> x
 2163       foo y = <blah>
 2164 
 2165    instance Baz Int Int
 2166 
 2167 From the class decl we get
 2168 
 2169    $dmfoo :: forall v x. Baz v x => x -> x
 2170    $dmfoo y = <blah>
 2171 
 2172 Notice that the type is ambiguous.  So we use Visible Type Application
 2173 to disambiguate:
 2174 
 2175    $dBazIntInt = MkBaz fooIntInt
 2176    fooIntInt = $dmfoo @Int @Int
 2177 
 2178 Lacking VTA we'd get ambiguity errors involving the default method.  This applies
 2179 equally to vanilla default methods (#1061) and generic default methods
 2180 (#12220).
 2181 
 2182 Historical note: before we had VTA we had to generate
 2183 post-type-checked code, which took a lot more code, and didn't work for
 2184 generic default methods.
 2185 
 2186 Note [INLINE and default methods]
 2187 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2188 Default methods need special case.  They are supposed to behave rather like
 2189 macros.  For example
 2190 
 2191   class Foo a where
 2192     op1, op2 :: Bool -> a -> a
 2193 
 2194     {-# INLINE op1 #-}
 2195     op1 b x = op2 (not b) x
 2196 
 2197   instance Foo Int where
 2198     -- op1 via default method
 2199     op2 b x = <blah>
 2200 
 2201 The instance declaration should behave
 2202 
 2203    just as if 'op1' had been defined with the
 2204    code, and INLINE pragma, from its original
 2205    definition.
 2206 
 2207 That is, just as if you'd written
 2208 
 2209   instance Foo Int where
 2210     op2 b x = <blah>
 2211 
 2212     {-# INLINE op1 #-}
 2213     op1 b x = op2 (not b) x
 2214 
 2215 So for the above example we generate:
 2216 
 2217   {-# INLINE $dmop1 #-}
 2218   -- $dmop1 has an InlineCompulsory unfolding
 2219   $dmop1 d b x = op2 d (not b) x
 2220 
 2221   $fFooInt = MkD $cop1 $cop2
 2222 
 2223   {-# INLINE $cop1 #-}
 2224   $cop1 = $dmop1 $fFooInt
 2225 
 2226   $cop2 = <blah>
 2227 
 2228 Note carefully:
 2229 
 2230 * We *copy* any INLINE pragma from the default method $dmop1 to the
 2231   instance $cop1.  Otherwise we'll just inline the former in the
 2232   latter and stop, which isn't what the user expected
 2233 
 2234 * Regardless of its pragma, we give the default method an
 2235   unfolding with an InlineCompulsory source. That means
 2236   that it'll be inlined at every use site, notably in
 2237   each instance declaration, such as $cop1.  This inlining
 2238   must happen even though
 2239     a) $dmop1 is not saturated in $cop1
 2240     b) $cop1 itself has an INLINE pragma
 2241 
 2242   It's vital that $dmop1 *is* inlined in this way, to allow the mutual
 2243   recursion between $fooInt and $cop1 to be broken
 2244 
 2245 * To communicate the need for an InlineCompulsory to the desugarer
 2246   (which makes the Unfoldings), we use the IsDefaultMethod constructor
 2247   in TcSpecPrags.
 2248 
 2249 
 2250 ************************************************************************
 2251 *                                                                      *
 2252         Specialise instance pragmas
 2253 *                                                                      *
 2254 ************************************************************************
 2255 
 2256 Note [SPECIALISE instance pragmas]
 2257 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2258 Consider
 2259 
 2260    instance (Ix a, Ix b) => Ix (a,b) where
 2261      {-# SPECIALISE instance Ix (Int,Int) #-}
 2262      range (x,y) = ...
 2263 
 2264 We make a specialised version of the dictionary function, AND
 2265 specialised versions of each *method*.  Thus we should generate
 2266 something like this:
 2267 
 2268   $dfIxPair :: (Ix a, Ix b) => Ix (a,b)
 2269   {-# DFUN [$crangePair, ...] #-}
 2270   {-# SPECIALISE $dfIxPair :: Ix (Int,Int) #-}
 2271   $dfIxPair da db = Ix ($crangePair da db) (...other methods...)
 2272 
 2273   $crange :: (Ix a, Ix b) -> ((a,b),(a,b)) -> [(a,b)]
 2274   {-# SPECIALISE $crange :: ((Int,Int),(Int,Int)) -> [(Int,Int)] #-}
 2275   $crange da db = <blah>
 2276 
 2277 The SPECIALISE pragmas are acted upon by the desugarer, which generate
 2278 
 2279   dii :: Ix Int
 2280   dii = ...
 2281 
 2282   $s$dfIxPair :: Ix ((Int,Int),(Int,Int))
 2283   {-# DFUN [$crangePair di di, ...] #-}
 2284   $s$dfIxPair = Ix ($crangePair di di) (...)
 2285 
 2286   {-# RULE forall (d1,d2:Ix Int). $dfIxPair Int Int d1 d2 = $s$dfIxPair #-}
 2287 
 2288   $s$crangePair :: ((Int,Int),(Int,Int)) -> [(Int,Int)]
 2289   $c$crangePair = ...specialised RHS of $crangePair...
 2290 
 2291   {-# RULE forall (d1,d2:Ix Int). $crangePair Int Int d1 d2 = $s$crangePair #-}
 2292 
 2293 Note that
 2294 
 2295   * The specialised dictionary $s$dfIxPair is very much needed, in case we
 2296     call a function that takes a dictionary, but in a context where the
 2297     specialised dictionary can be used.  See #7797.
 2298 
 2299   * The ClassOp rule for 'range' works equally well on $s$dfIxPair, because
 2300     it still has a DFunUnfolding.  See Note [ClassOp/DFun selection]
 2301 
 2302   * A call (range ($dfIxPair Int Int d1 d2)) might simplify two ways:
 2303        --> {ClassOp rule for range}     $crangePair Int Int d1 d2
 2304        --> {SPEC rule for $crangePair}  $s$crangePair
 2305     or thus:
 2306        --> {SPEC rule for $dfIxPair}    range $s$dfIxPair
 2307        --> {ClassOpRule for range}      $s$crangePair
 2308     It doesn't matter which way.
 2309 
 2310   * We want to specialise the RHS of both $dfIxPair and $crangePair,
 2311     but the SAME HsWrapper will do for both!  We can call tcSpecPrag
 2312     just once, and pass the result (in spec_inst_info) to tcMethods.
 2313 -}
 2314 
 2315 tcSpecInstPrags :: DFunId -> InstBindings GhcRn
 2316                 -> TcM ([LTcSpecPrag], TcPragEnv)
 2317 tcSpecInstPrags dfun_id (InstBindings { ib_binds = binds, ib_pragmas = uprags })
 2318   = do { spec_inst_prags <- mapM (wrapLocAM (tcSpecInst dfun_id)) $
 2319                             filter isSpecInstLSig uprags
 2320              -- The filter removes the pragmas for methods
 2321        ; return (spec_inst_prags, mkPragEnv uprags binds) }
 2322 
 2323 ------------------------------
 2324 tcSpecInst :: Id -> Sig GhcRn -> TcM TcSpecPrag
 2325 tcSpecInst dfun_id prag@(SpecInstSig _ _ hs_ty)
 2326   = addErrCtxt (spec_ctxt prag) $
 2327     do  { spec_dfun_ty <- tcHsClsInstType SpecInstCtxt hs_ty
 2328         ; co_fn <- tcSpecWrapper SpecInstCtxt (idType dfun_id) spec_dfun_ty
 2329         ; return (SpecPrag dfun_id co_fn defaultInlinePragma) }
 2330   where
 2331     spec_ctxt prag = hang (text "In the pragma:") 2 (ppr prag)
 2332 
 2333 tcSpecInst _  _ = panic "tcSpecInst"
 2334 
 2335 {-
 2336 ************************************************************************
 2337 *                                                                      *
 2338 \subsection{Error messages}
 2339 *                                                                      *
 2340 ************************************************************************
 2341 -}
 2342 
 2343 instDeclCtxt1 :: LHsSigType GhcRn -> SDoc
 2344 instDeclCtxt1 hs_inst_ty
 2345   = inst_decl_ctxt (ppr (getLHsInstDeclHead hs_inst_ty))
 2346 
 2347 instDeclCtxt2 :: Type -> SDoc
 2348 instDeclCtxt2 dfun_ty
 2349   = inst_decl_ctxt (ppr (mkClassPred cls tys))
 2350   where
 2351     (_,_,cls,tys) = tcSplitDFunTy dfun_ty
 2352 
 2353 inst_decl_ctxt :: SDoc -> SDoc
 2354 inst_decl_ctxt doc = hang (text "In the instance declaration for")
 2355                         2 (quotes doc)
 2356 
 2357 badBootFamInstDeclErr :: TcRnMessage
 2358 badBootFamInstDeclErr
 2359   = TcRnUnknownMessage $ mkPlainError noHints $ text "Illegal family instance in hs-boot file"
 2360 
 2361 notFamily :: TyCon -> TcRnMessage
 2362 notFamily tycon
 2363   = TcRnUnknownMessage $ mkPlainError noHints $
 2364     vcat [ text "Illegal family instance for" <+> quotes (ppr tycon)
 2365          , nest 2 $ parens (ppr tycon <+> text "is not an indexed type family")]
 2366 
 2367 assocInClassErr :: TyCon -> TcRnMessage
 2368 assocInClassErr name
 2369  = TcRnUnknownMessage $ mkPlainError noHints $
 2370    text "Associated type" <+> quotes (ppr name) <+>
 2371    text "must be inside a class instance"
 2372 
 2373 badFamInstDecl :: TyCon -> TcRnMessage
 2374 badFamInstDecl tc_name
 2375   = TcRnUnknownMessage $ mkPlainError noHints $
 2376     vcat [ text "Illegal family instance for" <+>
 2377            quotes (ppr tc_name)
 2378          , nest 2 (parens $ text "Use TypeFamilies to allow indexed type families") ]
 2379 
 2380 notOpenFamily :: TyCon -> TcRnMessage
 2381 notOpenFamily tc
 2382   = TcRnUnknownMessage $ mkPlainError noHints $
 2383   text "Illegal instance for closed family" <+> quotes (ppr tc)