never executed always true always false
    1 
    2 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
    3 
    4 module GHC.Tc.Instance.Class (
    5      matchGlobalInst,
    6      ClsInstResult(..),
    7      InstanceWhat(..), safeOverlap, instanceReturnsDictCon,
    8      AssocInstInfo(..), isNotAssociated,
    9   ) where
   10 
   11 import GHC.Prelude
   12 
   13 import GHC.Driver.Session
   14 
   15 import GHC.Core.TyCo.Rep
   16 
   17 import GHC.Tc.Utils.Env
   18 import GHC.Tc.Utils.Monad
   19 import GHC.Tc.Utils.TcType
   20 import GHC.Tc.Utils.Instantiate(instDFunType, tcInstType)
   21 import GHC.Tc.Instance.Typeable
   22 import GHC.Tc.Utils.TcMType
   23 import GHC.Tc.Types.Evidence
   24 import GHC.Tc.Instance.Family( tcGetFamInstEnvs, tcInstNewTyCon_maybe, tcLookupDataFamInst )
   25 import GHC.Rename.Env( addUsedGRE )
   26 
   27 import GHC.Builtin.Types
   28 import GHC.Builtin.Types.Prim
   29 import GHC.Builtin.Names
   30 
   31 import GHC.Types.Name.Reader( lookupGRE_FieldLabel, greMangledName )
   32 import GHC.Types.SafeHaskell
   33 import GHC.Types.Name   ( Name, pprDefinedAt )
   34 import GHC.Types.Var.Env ( VarEnv )
   35 import GHC.Types.Id
   36 
   37 import GHC.Core.Predicate
   38 import GHC.Core.InstEnv
   39 import GHC.Core.Type
   40 import GHC.Core.Make ( mkCharExpr, mkNaturalExpr, mkStringExprFS )
   41 import GHC.Core.DataCon
   42 import GHC.Core.TyCon
   43 import GHC.Core.Class
   44 
   45 import GHC.Utils.Outputable
   46 import GHC.Utils.Panic
   47 import GHC.Utils.Misc( splitAtList, fstOf3 )
   48 
   49 import Data.Maybe
   50 
   51 {- *******************************************************************
   52 *                                                                    *
   53               A helper for associated types within
   54               class instance declarations
   55 *                                                                    *
   56 **********************************************************************-}
   57 
   58 -- | Extra information about the parent instance declaration, needed
   59 -- when type-checking associated types. The 'Class' is the enclosing
   60 -- class, the [TyVar] are the /scoped/ type variable of the instance decl.
   61 -- The @VarEnv Type@ maps class variables to their instance types.
   62 data AssocInstInfo
   63   = NotAssociated
   64   | InClsInst { ai_class    :: Class
   65               , ai_tyvars   :: [TyVar]      -- ^ The /scoped/ tyvars of the instance
   66                                             -- Why scoped?  See bind_me in
   67                                             -- 'GHC.Tc.Validity.checkConsistentFamInst'
   68               , ai_inst_env :: VarEnv Type  -- ^ Maps /class/ tyvars to their instance types
   69                 -- See Note [Matching in the consistent-instantiation check]
   70     }
   71 
   72 isNotAssociated :: AssocInstInfo -> Bool
   73 isNotAssociated (NotAssociated {}) = True
   74 isNotAssociated (InClsInst {})     = False
   75 
   76 
   77 {- *******************************************************************
   78 *                                                                    *
   79                        Class lookup
   80 *                                                                    *
   81 **********************************************************************-}
   82 
   83 -- | Indicates if Instance met the Safe Haskell overlapping instances safety
   84 -- check.
   85 --
   86 -- See Note [Safe Haskell Overlapping Instances] in GHC.Tc.Solver
   87 -- See Note [Safe Haskell Overlapping Instances Implementation] in GHC.Tc.Solver
   88 type SafeOverlapping = Bool
   89 
   90 data ClsInstResult
   91   = NoInstance   -- Definitely no instance
   92 
   93   | OneInst { cir_new_theta :: [TcPredType]
   94             , cir_mk_ev     :: [EvExpr] -> EvTerm
   95             , cir_what      :: InstanceWhat }
   96 
   97   | NotSure      -- Multiple matches and/or one or more unifiers
   98 
   99 data InstanceWhat
  100   = BuiltinInstance
  101   | BuiltinEqInstance   -- A built-in "equality instance"; see the
  102                         -- GHC.Tc.Solver.InertSet Note [Solved dictionaries]
  103   | LocalInstance
  104   | TopLevInstance { iw_dfun_id   :: DFunId
  105                    , iw_safe_over :: SafeOverlapping }
  106 
  107 instance Outputable ClsInstResult where
  108   ppr NoInstance = text "NoInstance"
  109   ppr NotSure    = text "NotSure"
  110   ppr (OneInst { cir_new_theta = ev
  111                , cir_what = what })
  112     = text "OneInst" <+> vcat [ppr ev, ppr what]
  113 
  114 instance Outputable InstanceWhat where
  115   ppr BuiltinInstance   = text "a built-in instance"
  116   ppr BuiltinEqInstance = text "a built-in equality instance"
  117   ppr LocalInstance     = text "a locally-quantified instance"
  118   ppr (TopLevInstance { iw_dfun_id = dfun })
  119       = hang (text "instance" <+> pprSigmaType (idType dfun))
  120            2 (text "--" <+> pprDefinedAt (idName dfun))
  121 
  122 safeOverlap :: InstanceWhat -> Bool
  123 safeOverlap (TopLevInstance { iw_safe_over = so }) = so
  124 safeOverlap _                                      = True
  125 
  126 instanceReturnsDictCon :: InstanceWhat -> Bool
  127 -- See Note [Solved dictionaries] in GHC.Tc.Solver.InertSet
  128 instanceReturnsDictCon (TopLevInstance {}) = True
  129 instanceReturnsDictCon BuiltinInstance     = True
  130 instanceReturnsDictCon BuiltinEqInstance   = False
  131 instanceReturnsDictCon LocalInstance       = False
  132 
  133 matchGlobalInst :: DynFlags
  134                 -> Bool      -- True <=> caller is the short-cut solver
  135                              -- See Note [Shortcut solving: overlap]
  136                 -> Class -> [Type] -> TcM ClsInstResult
  137 matchGlobalInst dflags short_cut clas tys
  138   | cls_name == knownNatClassName
  139   = matchKnownNat    dflags short_cut clas tys
  140   | cls_name == knownSymbolClassName
  141   = matchKnownSymbol dflags short_cut clas tys
  142   | cls_name == knownCharClassName
  143   = matchKnownChar dflags short_cut clas tys
  144   | isCTupleClass clas                = matchCTuple          clas tys
  145   | cls_name == typeableClassName     = matchTypeable        clas tys
  146   | clas `hasKey` heqTyConKey         = matchHeteroEquality       tys
  147   | clas `hasKey` eqTyConKey          = matchHomoEquality         tys
  148   | clas `hasKey` coercibleTyConKey   = matchCoercible            tys
  149   | cls_name == hasFieldClassName     = matchHasField dflags short_cut clas tys
  150   | otherwise                         = matchInstEnv dflags short_cut clas tys
  151   where
  152     cls_name = className clas
  153 
  154 
  155 {- ********************************************************************
  156 *                                                                     *
  157                    Looking in the instance environment
  158 *                                                                     *
  159 ***********************************************************************-}
  160 
  161 
  162 matchInstEnv :: DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
  163 matchInstEnv dflags short_cut_solver clas tys
  164    = do { instEnvs <- tcGetInstEnvs
  165         ; let safeOverlapCheck = safeHaskell dflags `elem` [Sf_Safe, Sf_Trustworthy]
  166               (matches, unify, unsafeOverlaps) = lookupInstEnv True instEnvs clas tys
  167               safeHaskFail = safeOverlapCheck && not (null unsafeOverlaps)
  168         ; traceTc "matchInstEnv" $
  169             vcat [ text "goal:" <+> ppr clas <+> ppr tys
  170                  , text "matches:" <+> ppr matches
  171                  , text "unify:" <+> ppr unify ]
  172         ; case (matches, unify, safeHaskFail) of
  173 
  174             -- Nothing matches
  175             ([], [], _)
  176                 -> do { traceTc "matchClass not matching" (ppr pred)
  177                       ; return NoInstance }
  178 
  179             -- A single match (& no safe haskell failure)
  180             ([(ispec, inst_tys)], [], False)
  181                 | short_cut_solver      -- Called from the short-cut solver
  182                 , isOverlappable ispec
  183                 -- If the instance has OVERLAPPABLE or OVERLAPS or INCOHERENT
  184                 -- then don't let the short-cut solver choose it, because a
  185                 -- later instance might overlap it.  #14434 is an example
  186                 -- See Note [Shortcut solving: overlap]
  187                 -> do { traceTc "matchClass: ignoring overlappable" (ppr pred)
  188                       ; return NotSure }
  189 
  190                 | otherwise
  191                 -> do { let dfun_id = instanceDFunId ispec
  192                       ; traceTc "matchClass success" $
  193                         vcat [text "dict" <+> ppr pred,
  194                               text "witness" <+> ppr dfun_id
  195                                              <+> ppr (idType dfun_id) ]
  196                                 -- Record that this dfun is needed
  197                       ; match_one (null unsafeOverlaps) dfun_id inst_tys }
  198 
  199             -- More than one matches (or Safe Haskell fail!). Defer any
  200             -- reactions of a multitude until we learn more about the reagent
  201             _   -> do { traceTc "matchClass multiple matches, deferring choice" $
  202                         vcat [text "dict" <+> ppr pred,
  203                               text "matches" <+> ppr matches]
  204                       ; return NotSure } }
  205    where
  206      pred = mkClassPred clas tys
  207 
  208 match_one :: SafeOverlapping -> DFunId -> [DFunInstType] -> TcM ClsInstResult
  209              -- See Note [DFunInstType: instantiating types] in GHC.Core.InstEnv
  210 match_one so dfun_id mb_inst_tys
  211   = do { traceTc "match_one" (ppr dfun_id $$ ppr mb_inst_tys)
  212        ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
  213        ; traceTc "match_one 2" (ppr dfun_id $$ ppr tys $$ ppr theta)
  214        ; return $ OneInst { cir_new_theta = theta
  215                           , cir_mk_ev     = evDFunApp dfun_id tys
  216                           , cir_what      = TopLevInstance { iw_dfun_id = dfun_id
  217                                                            , iw_safe_over = so } } }
  218 
  219 
  220 {- Note [Shortcut solving: overlap]
  221 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  222 Suppose we have
  223   instance {-# OVERLAPPABLE #-} C a where ...
  224 and we are typechecking
  225   f :: C a => a -> a
  226   f = e  -- Gives rise to [W] C a
  227 
  228 We don't want to solve the wanted constraint with the overlappable
  229 instance; rather we want to use the supplied (C a)! That was the whole
  230 point of it being overlappable!  #14434 wwas an example.
  231 
  232 Alas even if the instance has no overlap flag, thus
  233   instance C a where ...
  234 there is nothing to stop it being overlapped. GHC provides no way to
  235 declare an instance as "final" so it can't be overlapped.  But really
  236 only final instances are OK for short-cut solving.  Sigh. #15135
  237 was a puzzling example.
  238 -}
  239 
  240 
  241 {- ********************************************************************
  242 *                                                                     *
  243                    Class lookup for CTuples
  244 *                                                                     *
  245 ***********************************************************************-}
  246 
  247 matchCTuple :: Class -> [Type] -> TcM ClsInstResult
  248 matchCTuple clas tys   -- (isCTupleClass clas) holds
  249   = return (OneInst { cir_new_theta = tys
  250                     , cir_mk_ev     = tuple_ev
  251                     , cir_what      = BuiltinInstance })
  252             -- The dfun *is* the data constructor!
  253   where
  254      data_con = tyConSingleDataCon (classTyCon clas)
  255      tuple_ev = evDFunApp (dataConWrapId data_con) tys
  256 
  257 {- ********************************************************************
  258 *                                                                     *
  259                    Class lookup for Literals
  260 *                                                                     *
  261 ***********************************************************************-}
  262 
  263 {-
  264 Note [KnownNat & KnownSymbol and EvLit]
  265 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  266 A part of the type-level literals implementation are the classes
  267 "KnownNat" and "KnownSymbol", which provide a "smart" constructor for
  268 defining singleton values.  Here is the key stuff from GHC.TypeNats
  269 
  270   class KnownNat (n :: Nat) where
  271     natSing :: SNat n
  272 
  273   newtype SNat (n :: Nat) = SNat Natural
  274 
  275 Conceptually, this class has infinitely many instances:
  276 
  277   instance KnownNat 0       where natSing = SNat 0
  278   instance KnownNat 1       where natSing = SNat 1
  279   instance KnownNat 2       where natSing = SNat 2
  280   ...
  281 
  282 In practice, we solve `KnownNat` predicates in the type-checker
  283 (see GHC.Tc.Solver.Interact) because we can't have infinitely many instances.
  284 The evidence (aka "dictionary") for `KnownNat` is of the form `EvLit (EvNum n)`.
  285 
  286 We make the following assumptions about dictionaries in GHC:
  287   1. The "dictionary" for classes with a single method---like `KnownNat`---is
  288      a newtype for the type of the method, so using a evidence amounts
  289      to a coercion, and
  290   2. Newtypes use the same representation as their definition types.
  291 
  292 So, the evidence for `KnownNat` is just a value of the representation type,
  293 wrapped in two newtype constructors: one to make it into a `SNat` value,
  294 and another to make it into a `KnownNat` dictionary.
  295 
  296 Also note that `natSing` and `SNat` are never actually exposed from the
  297 library---they are just an implementation detail.  Instead, users see
  298 a more convenient function, defined in terms of `natSing`:
  299 
  300   natVal :: KnownNat n => proxy n -> Natural
  301 
  302 The reason we don't use this directly in the class is that it is simpler
  303 and more efficient to pass around a Natural rather than an entire function,
  304 especially when the `KnownNat` evidence is packaged up in an existential.
  305 
  306 The story for kind `Symbol` is analogous:
  307   * class KnownSymbol
  308   * newtype SSymbol
  309   * Evidence: a Core literal (e.g. mkNaturalExpr)
  310 
  311 
  312 Note [Fabricating Evidence for Literals in Backpack]
  313 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  314 
  315 Let `T` be a type of kind `Nat`. When solving for a purported instance
  316 of `KnownNat T`, ghc tries to resolve the type `T` to an integer `n`,
  317 in which case the evidence `EvLit (EvNum n)` is generated on the
  318 fly. It might appear that this is sufficient as users cannot define
  319 their own instances of `KnownNat`. However, for backpack module this
  320 would not work (see issue #15379). Consider the signature `Abstract`
  321 
  322 > signature Abstract where
  323 >   data T :: Nat
  324 >   instance KnownNat T
  325 
  326 and a module `Util` that depends on it:
  327 
  328 > module Util where
  329 >  import Abstract
  330 >  printT :: IO ()
  331 >  printT = do print $ natVal (Proxy :: Proxy T)
  332 
  333 Clearly, we need to "use" the dictionary associated with `KnownNat T`
  334 in the module `Util`, but it is too early for the compiler to produce
  335 a real dictionary as we still have not fixed what `T` is. Only when we
  336 mixin a concrete module
  337 
  338 > module Concrete where
  339 >   type T = 42
  340 
  341 do we really get hold of the underlying integer. So the strategy that
  342 we follow is the following
  343 
  344 1. If T is indeed available as a type alias for an integer constant,
  345    generate the dictionary on the fly, failing which
  346 
  347 2. Look up the type class environment for the evidence.
  348 
  349 Finally actual code gets generate for Util only when a module like
  350 Concrete gets "mixed-in" in place of the signature Abstract. As a
  351 result all things, including the typeclass instances, in Concrete gets
  352 reexported. So `KnownNat` gets resolved the normal way post-Backpack.
  353 
  354 A similar generation works for `KnownSymbol` as well
  355 
  356 -}
  357 
  358 matchKnownNat :: DynFlags
  359               -> Bool      -- True <=> caller is the short-cut solver
  360                            -- See Note [Shortcut solving: overlap]
  361               -> Class -> [Type] -> TcM ClsInstResult
  362 matchKnownNat dflags _ clas [ty]     -- clas = KnownNat
  363   | Just n <- isNumLitTy ty  = makeLitDict clas ty (mkNaturalExpr (targetPlatform dflags) n)
  364 matchKnownNat df sc clas tys = matchInstEnv df sc clas tys
  365  -- See Note [Fabricating Evidence for Literals in Backpack] for why
  366  -- this lookup into the instance environment is required.
  367 
  368 matchKnownSymbol :: DynFlags
  369                  -> Bool      -- True <=> caller is the short-cut solver
  370                               -- See Note [Shortcut solving: overlap]
  371                  -> Class -> [Type] -> TcM ClsInstResult
  372 matchKnownSymbol _ _ clas [ty]  -- clas = KnownSymbol
  373   | Just s <- isStrLitTy ty = do
  374         et <- mkStringExprFS s
  375         makeLitDict clas ty et
  376 matchKnownSymbol df sc clas tys = matchInstEnv df sc clas tys
  377  -- See Note [Fabricating Evidence for Literals in Backpack] for why
  378  -- this lookup into the instance environment is required.
  379 
  380 matchKnownChar :: DynFlags
  381                  -> Bool      -- True <=> caller is the short-cut solver
  382                               -- See Note [Shortcut solving: overlap]
  383                  -> Class -> [Type] -> TcM ClsInstResult
  384 matchKnownChar _ _ clas [ty]  -- clas = KnownChar
  385   | Just s <- isCharLitTy ty = makeLitDict clas ty (mkCharExpr s)
  386 matchKnownChar df sc clas tys = matchInstEnv df sc clas tys
  387  -- See Note [Fabricating Evidence for Literals in Backpack] for why
  388  -- this lookup into the instance environment is required.
  389 
  390 makeLitDict :: Class -> Type -> EvExpr -> TcM ClsInstResult
  391 -- makeLitDict adds a coercion that will convert the literal into a dictionary
  392 -- of the appropriate type.  See Note [KnownNat & KnownSymbol and EvLit]
  393 -- in GHC.Tc.Types.Evidence.  The coercion happens in 2 steps:
  394 --
  395 --     Integer -> SNat n     -- representation of literal to singleton
  396 --     SNat n  -> KnownNat n -- singleton to dictionary
  397 --
  398 --     The process is mirrored for Symbols:
  399 --     String    -> SSymbol n
  400 --     SSymbol n -> KnownSymbol n
  401 makeLitDict clas ty et
  402     | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
  403           -- co_dict :: KnownNat n ~ SNat n
  404     , [ meth ]   <- classMethods clas
  405     , Just tcRep <- tyConAppTyCon_maybe (classMethodTy meth)
  406                     -- If the method type is forall n. KnownNat n => SNat n
  407                     -- then tcRep is SNat
  408     , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
  409           -- SNat n ~ Integer
  410     , let ev_tm = mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep))
  411     = return $ OneInst { cir_new_theta = []
  412                        , cir_mk_ev     = \_ -> ev_tm
  413                        , cir_what      = BuiltinInstance }
  414 
  415     | otherwise
  416     = pprPanic "makeLitDict" $
  417       text "Unexpected evidence for" <+> ppr (className clas)
  418       $$ vcat (map (ppr . idType) (classMethods clas))
  419 
  420 {- ********************************************************************
  421 *                                                                     *
  422                    Class lookup for Typeable
  423 *                                                                     *
  424 ***********************************************************************-}
  425 
  426 -- | Assumes that we've checked that this is the 'Typeable' class,
  427 -- and it was applied to the correct argument.
  428 matchTypeable :: Class -> [Type] -> TcM ClsInstResult
  429 matchTypeable clas [k,t]  -- clas = Typeable
  430   -- For the first two cases, See Note [No Typeable for polytypes or qualified types]
  431   | isForAllTy k                      = return NoInstance   -- Polytype
  432   | isJust (tcSplitPredFunTy_maybe t) = return NoInstance   -- Qualified type
  433 
  434   -- Now cases that do work
  435   | k `eqType` naturalTy                   = doTyLit knownNatClassName         t
  436   | k `eqType` typeSymbolKind              = doTyLit knownSymbolClassName      t
  437   | k `eqType` charTy                      = doTyLit knownCharClassName        t
  438   | tcIsConstraintKind t                   = doTyConApp clas t constraintKindTyCon []
  439   | Just (mult,arg,ret) <- splitFunTy_maybe t   = doFunTy    clas t mult arg ret
  440   | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)]
  441   , onlyNamedBndrsApplied tc ks            = doTyConApp clas t tc ks
  442   | Just (f,kt)   <- splitAppTy_maybe t    = doTyApp    clas t f kt
  443 
  444 matchTypeable _ _ = return NoInstance
  445 
  446 -- | Representation for a type @ty@ of the form @arg -> ret@.
  447 doFunTy :: Class -> Type -> Mult -> Type -> Type -> TcM ClsInstResult
  448 doFunTy clas ty mult arg_ty ret_ty
  449   = return $ OneInst { cir_new_theta = preds
  450                      , cir_mk_ev     = mk_ev
  451                      , cir_what      = BuiltinInstance }
  452   where
  453     preds = map (mk_typeable_pred clas) [mult, arg_ty, ret_ty]
  454     mk_ev [mult_ev, arg_ev, ret_ev] = evTypeable ty $
  455                         EvTypeableTrFun (EvExpr mult_ev) (EvExpr arg_ev) (EvExpr ret_ev)
  456     mk_ev _ = panic "GHC.Tc.Solver.Interact.doFunTy"
  457 
  458 
  459 -- | Representation for type constructor applied to some kinds.
  460 -- 'onlyNamedBndrsApplied' has ensured that this application results in a type
  461 -- of monomorphic kind (e.g. all kind variables have been instantiated).
  462 doTyConApp :: Class -> Type -> TyCon -> [Kind] -> TcM ClsInstResult
  463 doTyConApp clas ty tc kind_args
  464   | tyConIsTypeable tc
  465   = return $ OneInst { cir_new_theta = (map (mk_typeable_pred clas) kind_args)
  466                      , cir_mk_ev     = mk_ev
  467                      , cir_what      = BuiltinInstance }
  468   | otherwise
  469   = return NoInstance
  470   where
  471     mk_ev kinds = evTypeable ty $ EvTypeableTyCon tc (map EvExpr kinds)
  472 
  473 -- | Representation for TyCon applications of a concrete kind. We just use the
  474 -- kind itself, but first we must make sure that we've instantiated all kind-
  475 -- polymorphism, but no more.
  476 onlyNamedBndrsApplied :: TyCon -> [KindOrType] -> Bool
  477 onlyNamedBndrsApplied tc ks
  478  = all isNamedTyConBinder used_bndrs &&
  479    not (any isNamedTyConBinder leftover_bndrs)
  480  where
  481    bndrs                        = tyConBinders tc
  482    (used_bndrs, leftover_bndrs) = splitAtList ks bndrs
  483 
  484 doTyApp :: Class -> Type -> Type -> KindOrType -> TcM ClsInstResult
  485 -- Representation for an application of a type to a type-or-kind.
  486 --  This may happen when the type expression starts with a type variable.
  487 --  Example (ignoring kind parameter):
  488 --    Typeable (f Int Char)                      -->
  489 --    (Typeable (f Int), Typeable Char)          -->
  490 --    (Typeable f, Typeable Int, Typeable Char)  --> (after some simp. steps)
  491 --    Typeable f
  492 doTyApp clas ty f tk
  493   | isForAllTy (tcTypeKind f)
  494   = return NoInstance -- We can't solve until we know the ctr.
  495   | otherwise
  496   = return $ OneInst { cir_new_theta = map (mk_typeable_pred clas) [f, tk]
  497                      , cir_mk_ev     = mk_ev
  498                      , cir_what      = BuiltinInstance }
  499   where
  500     mk_ev [t1,t2] = evTypeable ty $ EvTypeableTyApp (EvExpr t1) (EvExpr t2)
  501     mk_ev _ = panic "doTyApp"
  502 
  503 
  504 -- Emit a `Typeable` constraint for the given type.
  505 mk_typeable_pred :: Class -> Type -> PredType
  506 mk_typeable_pred clas ty = mkClassPred clas [ tcTypeKind ty, ty ]
  507 
  508   -- Typeable is implied by KnownNat/KnownSymbol. In the case of a type literal
  509   -- we generate a sub-goal for the appropriate class.
  510   -- See Note [Typeable for Nat and Symbol]
  511 doTyLit :: Name -> Type -> TcM ClsInstResult
  512 doTyLit kc t = do { kc_clas <- tcLookupClass kc
  513                   ; let kc_pred    = mkClassPred kc_clas [ t ]
  514                         mk_ev [ev] = evTypeable t $ EvTypeableTyLit (EvExpr ev)
  515                         mk_ev _    = panic "doTyLit"
  516                   ; return (OneInst { cir_new_theta = [kc_pred]
  517                                     , cir_mk_ev     = mk_ev
  518                                     , cir_what      = BuiltinInstance }) }
  519 
  520 {- Note [Typeable (T a b c)]
  521 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  522 For type applications we always decompose using binary application,
  523 via doTyApp, until we get to a *kind* instantiation.  Example
  524    Proxy :: forall k. k -> *
  525 
  526 To solve Typeable (Proxy (* -> *) Maybe) we
  527   - First decompose with doTyApp,
  528     to get (Typeable (Proxy (* -> *))) and Typeable Maybe
  529   - Then solve (Typeable (Proxy (* -> *))) with doTyConApp
  530 
  531 If we attempt to short-cut by solving it all at once, via
  532 doTyConApp
  533 
  534 (this note is sadly truncated FIXME)
  535 
  536 
  537 Note [No Typeable for polytypes or qualified types]
  538 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  539 We do not support impredicative typeable, such as
  540    Typeable (forall a. a->a)
  541    Typeable (Eq a => a -> a)
  542    Typeable (() => Int)
  543    Typeable (((),()) => Int)
  544 
  545 See #9858.  For forall's the case is clear: we simply don't have
  546 a TypeRep for them.  For qualified but not polymorphic types, like
  547 (Eq a => a -> a), things are murkier.  But:
  548 
  549  * We don't need a TypeRep for these things.  TypeReps are for
  550    monotypes only.
  551 
  552  * Perhaps we could treat `=>` as another type constructor for `Typeable`
  553    purposes, and thus support things like `Eq Int => Int`, however,
  554    at the current state of affairs this would be an odd exception as
  555    no other class works with impredicative types.
  556    For now we leave it off, until we have a better story for impredicativity.
  557 
  558 
  559 Note [Typeable for Nat and Symbol]
  560 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  561 We have special Typeable instances for Nat and Symbol.  Roughly we
  562 have this instance, implemented here by doTyLit:
  563       instance KnownNat n => Typeable (n :: Nat) where
  564          typeRep = typeNatTypeRep @n
  565 where
  566    Data.Typeable.Internal.typeNatTypeRep :: KnownNat a => TypeRep a
  567 
  568 Ultimately typeNatTypeRep uses 'natSing' from KnownNat to get a
  569 runtime value 'n'; it turns it into a string with 'show' and uses
  570 that to whiz up a TypeRep TyCon for 'n', with mkTypeLitTyCon.
  571 See #10348.
  572 
  573 Because of this rule it's inadvisable (see #15322) to have a constraint
  574     f :: (Typeable (n :: Nat)) => blah
  575 in a function signature; it gives rise to overlap problems just as
  576 if you'd written
  577     f :: Eq [a] => blah
  578 -}
  579 
  580 {- ********************************************************************
  581 *                                                                     *
  582                    Class lookup for lifted equality
  583 *                                                                     *
  584 ***********************************************************************-}
  585 
  586 -- See also Note [The equality types story] in GHC.Builtin.Types.Prim
  587 matchHeteroEquality :: [Type] -> TcM ClsInstResult
  588 -- Solves (t1 ~~ t2)
  589 matchHeteroEquality args
  590   = return (OneInst { cir_new_theta = [ mkTyConApp eqPrimTyCon args ]
  591                     , cir_mk_ev     = evDataConApp heqDataCon args
  592                     , cir_what      = BuiltinEqInstance })
  593 
  594 matchHomoEquality :: [Type] -> TcM ClsInstResult
  595 -- Solves (t1 ~ t2)
  596 matchHomoEquality args@[k,t1,t2]
  597   = return (OneInst { cir_new_theta = [ mkTyConApp eqPrimTyCon [k,k,t1,t2] ]
  598                     , cir_mk_ev     = evDataConApp eqDataCon args
  599                     , cir_what      = BuiltinEqInstance })
  600 matchHomoEquality args = pprPanic "matchHomoEquality" (ppr args)
  601 
  602 -- See also Note [The equality types story] in GHC.Builtin.Types.Prim
  603 matchCoercible :: [Type] -> TcM ClsInstResult
  604 matchCoercible args@[k, t1, t2]
  605   = return (OneInst { cir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
  606                     , cir_mk_ev     = evDataConApp coercibleDataCon args
  607                     , cir_what      = BuiltinEqInstance })
  608   where
  609     args' = [k, k, t1, t2]
  610 matchCoercible args = pprPanic "matchLiftedCoercible" (ppr args)
  611 
  612 {- ********************************************************************
  613 *                                                                     *
  614               Class lookup for overloaded record fields
  615 *                                                                     *
  616 ***********************************************************************-}
  617 
  618 {-
  619 Note [HasField instances]
  620 ~~~~~~~~~~~~~~~~~~~~~~~~~
  621 Suppose we have
  622 
  623     data T y = MkT { foo :: [y] }
  624 
  625 and `foo` is in scope.  Then GHC will automatically solve a constraint like
  626 
  627     HasField "foo" (T Int) b
  628 
  629 by emitting a new wanted
  630 
  631     T alpha -> [alpha] ~# T Int -> b
  632 
  633 and building a HasField dictionary out of the selector function `foo`,
  634 appropriately cast.
  635 
  636 The HasField class is defined (in GHC.Records) thus:
  637 
  638     class HasField (x :: k) r a | x r -> a where
  639       getField :: r -> a
  640 
  641 Since this is a one-method class, it is represented as a newtype.
  642 Hence we can solve `HasField "foo" (T Int) b` by taking an expression
  643 of type `T Int -> b` and casting it using the newtype coercion.
  644 Note that
  645 
  646     foo :: forall y . T y -> [y]
  647 
  648 so the expression we construct is
  649 
  650     foo @alpha |> co
  651 
  652 where
  653 
  654     co :: (T alpha -> [alpha]) ~# HasField "foo" (T Int) b
  655 
  656 is built from
  657 
  658     co1 :: (T alpha -> [alpha]) ~# (T Int -> b)
  659 
  660 which is the new wanted, and
  661 
  662     co2 :: (T Int -> b) ~# HasField "foo" (T Int) b
  663 
  664 which can be derived from the newtype coercion.
  665 
  666 If `foo` is not in scope, or has a higher-rank or existentially
  667 quantified type, then the constraint is not solved automatically, but
  668 may be solved by a user-supplied HasField instance.  Similarly, if we
  669 encounter a HasField constraint where the field is not a literal
  670 string, or does not belong to the type, then we fall back on the
  671 normal constraint solver behaviour.
  672 
  673 
  674 Note [Unused name reporting and HasField]
  675 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  676 When a HasField constraint is solved by the type-checker, we must record a use
  677 of the corresponding field name, as otherwise it might be reported as unused.
  678 See #19213.  We need to call keepAlive to add the name to the tcg_keep set,
  679 which accumulates names used by the constraint solver, as described by
  680 Note [Tracking unused binding and imports] in GHC.Tc.Types.
  681 
  682 We need to call addUsedGRE as well because there may be a deprecation warning on
  683 the field, which will be reported by addUsedGRE.  But calling addUsedGRE without
  684 keepAlive is not enough, because the field might be defined locally, and
  685 addUsedGRE extends tcg_used_gres with imported GREs only.
  686 -}
  687 
  688 -- See Note [HasField instances]
  689 matchHasField :: DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
  690 matchHasField dflags short_cut clas tys
  691   = do { fam_inst_envs <- tcGetFamInstEnvs
  692        ; rdr_env       <- getGlobalRdrEnv
  693        ; case tys of
  694            -- We are matching HasField {k} x r a...
  695            [_k_ty, x_ty, r_ty, a_ty]
  696                -- x should be a literal string
  697              | Just x <- isStrLitTy x_ty
  698                -- r should be an applied type constructor
  699              , Just (tc, args) <- tcSplitTyConApp_maybe r_ty
  700                -- use representation tycon (if data family); it has the fields
  701              , let r_tc = fstOf3 (tcLookupDataFamInst fam_inst_envs tc args)
  702                -- x should be a field of r
  703              , Just fl <- lookupTyConFieldLabel x r_tc
  704                -- the field selector should be in scope
  705              , Just gre <- lookupGRE_FieldLabel rdr_env fl
  706 
  707              -> do { sel_id <- tcLookupId (flSelector fl)
  708                    ; (tv_prs, preds, sel_ty) <- tcInstType newMetaTyVars sel_id
  709 
  710                          -- The first new wanted constraint equates the actual
  711                          -- type of the selector with the type (r -> a) within
  712                          -- the HasField x r a dictionary.  The preds will
  713                          -- typically be empty, but if the datatype has a
  714                          -- "stupid theta" then we have to include it here.
  715                    ; let theta = mkPrimEqPred sel_ty (mkVisFunTyMany r_ty a_ty) : preds
  716 
  717                          -- Use the equality proof to cast the selector Id to
  718                          -- type (r -> a), then use the newtype coercion to cast
  719                          -- it to a HasField dictionary.
  720                          mk_ev (ev1:evs) = evSelector sel_id tvs evs `evCast` co
  721                            where
  722                              co = mkTcSubCo (evTermCoercion (EvExpr ev1))
  723                                       `mkTcTransCo` mkTcSymCo co2
  724                          mk_ev [] = panic "matchHasField.mk_ev"
  725 
  726                          Just (_, co2) = tcInstNewTyCon_maybe (classTyCon clas)
  727                                                               tys
  728 
  729                          tvs = mkTyVarTys (map snd tv_prs)
  730 
  731                      -- The selector must not be "naughty" (i.e. the field
  732                      -- cannot have an existentially quantified type), and
  733                      -- it must not be higher-rank.
  734                    ; if not (isNaughtyRecordSelector sel_id) && isTauTy sel_ty
  735                      then do { -- See Note [Unused name reporting and HasField]
  736                                addUsedGRE True gre
  737                              ; keepAlive (greMangledName gre)
  738                              ; return OneInst { cir_new_theta = theta
  739                                               , cir_mk_ev     = mk_ev
  740                                               , cir_what      = BuiltinInstance } }
  741                      else matchInstEnv dflags short_cut clas tys }
  742 
  743            _ -> matchInstEnv dflags short_cut clas tys }