Refactor the treatment of predicate types
[ghc.git] / compiler / typecheck / TcInteract.hs
index 5d3a988..3914db6 100644 (file)
@@ -8,7 +8,6 @@ module TcInteract (
 #include "HsVersions.h"
 
 import GhcPrelude
-
 import BasicTypes ( SwapFlag(..), isSwapped,
                     infinity, IntWithInf, intGtLimit )
 import TcCanonical
@@ -16,38 +15,23 @@ import TcFlatten
 import TcUnify( canSolveByUnification )
 import VarSet
 import Type
-import Kind( isConstraintKind )
-import InstEnv( DFunInstType, lookupInstEnv
-              , instanceDFunId, isOverlappable )
+import InstEnv( DFunInstType )
 import CoAxiom( sfInteractTop, sfInteractInert )
 
-import TcMType (newMetaTyVars)
-
 import Var
 import TcType
-import Name
-import RdrName ( lookupGRE_FieldLabel )
-import PrelNames ( knownNatClassName, knownSymbolClassName,
-                   typeableClassName,
-                   coercibleTyConKey,
-                   hasFieldClassName,
+import PrelNames ( coercibleTyConKey,
                    heqTyConKey, eqTyConKey, ipClassKey )
-import TysWiredIn ( typeNatKind, typeSymbolKind, heqDataCon,
-                    coercibleDataCon, constraintKindTyCon )
-import TysPrim    ( eqPrimTyCon, eqReprPrimTyCon )
-import Id( idType, isNaughtyRecordSelector )
 import CoAxiom ( TypeEqn, CoAxiom(..), CoAxBranch(..), fromBranches )
 import Class
 import TyCon
-import DataCon( dataConWrapId )
-import FieldLabel
 import FunDeps
 import FamInst
+import ClsInst( ClsInstResult(..), InstanceWhat(..), safeOverlap )
 import FamInstEnv
 import Unify ( tcUnifyTyWithTFs, ruleMatchTyKiX )
 
 import TcEvidence
-import MkCore ( mkStringExprFS, mkNaturalExpr )
 import Outputable
 
 import TcRnTypes
@@ -55,6 +39,7 @@ import TcSMonad
 import Bag
 import MonadUtils ( concatMapM, foldlM )
 
+import CoreSyn
 import Data.List( partition, foldl', deleteFirstsBy )
 import SrcLoc
 import VarEnv
@@ -1098,7 +1083,7 @@ shortCutSolver dflags ev_w ev_i
  && gopt Opt_SolveConstantDicts dflags
  -- Enabled by the -fsolve-constant-dicts flag
   = do { ev_binds_var <- getTcEvBindsVar
-       ; ev_binds <- ASSERT2( not (isNoEvBindsVar ev_binds_var ), ppr ev_w )
+       ; ev_binds <- ASSERT2( not (isCoEvBindsVar ev_binds_var ), ppr ev_w )
                      getTcEvBindsMap ev_binds_var
        ; solved_dicts <- getSolvedDicts
 
@@ -1127,21 +1112,20 @@ shortCutSolver dflags ev_w ev_i
       | let pred = ctEvPred ev
             loc  = ctEvLoc  ev
       , ClassPred cls tys <- classifyPredType pred
-      = do { inst_res <- lift $ matchGlobalInst dflags True cls tys loc
+      = do { inst_res <- lift $ matchGlobalInst dflags True cls tys
            ; case inst_res of
-               OneInst { lir_new_theta = preds
-                       , lir_mk_ev = mk_ev
-                       , lir_safe_over = safeOverlap }
-                 | safeOverlap
+               OneInst { cir_new_theta = preds
+                       , cir_mk_ev     = mk_ev
+                       , cir_what      = what }
+                 | safeOverlap what
                  , all isTyFamFree preds  -- Note [Shortcut solving: type families]
                  -> do { let solved_dicts' = addDict solved_dicts cls tys ev
-                             loc'          = bumpCtLocDepth loc
                              -- solved_dicts': it is important that we add our goal
                              -- to the cache before we solve! Otherwise we may end
                              -- up in a loop while solving recursive dictionaries.
 
                        ; lift $ traceTcS "shortCutSolver: found instance" (ppr preds)
-                       ; lift $ checkReductionDepth loc pred
+                       ; loc' <- lift $ checkInstanceOK loc what pred
 
                        ; evc_vs <- mapM (new_wanted_cached loc' solved_dicts') preds
                                   -- Emit work for subgoals but use our local cache
@@ -1625,7 +1609,8 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
        ; stopWith ev "Solved from inert" }
 
   | ReprEq <- eq_rel   -- See Note [Do not unify representational equalities]
-  = continueWith workItem
+  = do { traceTcS "Not unifying representational equality" (ppr workItem)
+       ; continueWith workItem }
 
   | isGiven ev         -- See Note [Touchables and givens]
   = continueWith workItem
@@ -1836,16 +1821,58 @@ topReactionsStage work_item
 
 --------------------
 doTopReactOther :: Ct -> TcS (StopOrContinue Ct)
+-- Try local quantified constraints for
+--     CTyEqCan  e.g.  (a ~# ty)
+-- and CIrredCan e.g.  (c a)
+--
+-- Why equalities? See TcCanonical
+-- Note [Equality superclasses in quantified constraints]
 doTopReactOther work_item
-  = do { -- Try local quantified constraints
-         res <- matchLocalInst pred (ctEvLoc ev)
+  | isGiven ev
+  = continueWith work_item
+
+  | EqPred eq_rel t1 t2 <- classifyPredType pred
+  = -- See Note [Looking up primitive equalities in quantified constraints]
+    case boxEqPred eq_rel t1 t2 of
+      Nothing -> continueWith work_item
+      Just (cls, tys)
+        -> do { res <- matchLocalInst (mkClassPred cls tys) loc
+              ; case res of
+                  OneInst { cir_mk_ev = mk_ev }
+                    -> chooseInstance work_item
+                           (res { cir_mk_ev = mk_eq_ev cls tys mk_ev })
+                    where
+                  _ -> continueWith work_item }
+
+  | otherwise
+  = do { res <- matchLocalInst pred loc
        ; case res of
            OneInst {} -> chooseInstance work_item res
            _          -> continueWith work_item }
   where
     ev = ctEvidence work_item
+    loc  = ctEvLoc ev
     pred = ctEvPred ev
 
+    mk_eq_ev cls tys mk_ev evs
+      = case (mk_ev evs) of
+          EvExpr e -> EvExpr (Var sc_id `mkTyApps` tys `App` e)
+          ev       -> pprPanic "mk_eq_ev" (ppr ev)
+      where
+        [sc_id] = classSCSelIds cls
+
+{- Note [Looking up primitive equalities in quantified constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For equalities (a ~# b) look up (a ~ b), and then do a superclass
+selection. This avoids having to support quantified constraints whose
+kind is not Constraint, such as (forall a. F a ~# b)
+
+See
+ * Note [Evidence for quantified constraints] in Type
+ * Note [Equality superclasses in quantified constraints]
+   in TcCanonical
+-}
+
 --------------------
 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
 doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
@@ -2232,8 +2259,9 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
    = do { dflags <- getDynFlags
         ; lkup_res <- matchClassInst dflags inerts cls xis dict_loc
         ; case lkup_res of
-               OneInst { lir_safe_over = s }
-                  -> do { unless s $ insertSafeOverlapFailureTcS work_item
+               OneInst { cir_what = what }
+                  -> do { unless (safeOverlap what) $
+                          insertSafeOverlapFailureTcS work_item
                         ; when (isWanted ev) $ addSolvedDict ev cls xis
                         ; chooseInstance work_item lkup_res }
                _  ->  -- NoInstance or NotSure
@@ -2264,53 +2292,66 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
 
 
-chooseInstance :: Ct -> LookupInstResult -> TcS (StopOrContinue Ct)
+chooseInstance :: Ct -> ClsInstResult -> TcS (StopOrContinue Ct)
 chooseInstance work_item
-               (OneInst { lir_new_theta = theta
-                        , lir_mk_ev     = mk_ev })
+               (OneInst { cir_new_theta = theta
+                        , cir_what      = what
+                        , cir_mk_ev     = mk_ev })
   = do { traceTcS "doTopReact/found instance for" $ ppr ev
-       ; checkReductionDepth deeper_loc pred
-       ; if isDerived ev then finish_derived theta
-                         else finish_wanted  theta mk_ev }
+       ; deeper_loc <- checkInstanceOK loc what pred
+       ; if isDerived ev then finish_derived deeper_loc theta
+                         else finish_wanted  deeper_loc theta mk_ev }
   where
      ev         = ctEvidence work_item
      pred       = ctEvPred ev
      loc        = ctEvLoc ev
-     origin     = ctLocOrigin loc
-     deeper_loc = zap_origin (bumpCtLocDepth loc)
 
-     zap_origin loc  -- After applying an instance we can set ScOrigin to
-                     -- infinity, so that prohibitedSuperClassSolve never fires
-       | ScOrigin {} <- origin
-       = setCtLocOrigin loc (ScOrigin infinity)
-       | otherwise
-       = loc
-
-     finish_wanted :: [TcPredType]
+     finish_wanted :: CtLoc -> [TcPredType]
                    -> ([EvExpr] -> EvTerm) -> TcS (StopOrContinue Ct)
       -- Precondition: evidence term matches the predicate workItem
-     finish_wanted theta mk_ev
+     finish_wanted loc theta mk_ev
         = do { evb <- getTcEvBindsVar
-             ; if isNoEvBindsVar evb
+             ; if isCoEvBindsVar evb
                then -- See Note [Instances in no-evidence implications]
                     continueWith work_item
                else
-          do { evc_vars <- mapM (newWanted deeper_loc) theta
+          do { evc_vars <- mapM (newWanted loc) theta
              ; setEvBindIfWanted ev (mk_ev (map getEvExpr evc_vars))
              ; emitWorkNC (freshGoals evc_vars)
              ; stopWith ev "Dict/Top (solved wanted)" } }
 
-     finish_derived theta  -- Use type-class instances for Deriveds, in the hope
-       =                   -- of generating some improvements
-                           -- C.f. Example 3 of Note [The improvement story]
-                           -- It's easy because no evidence is involved
-         do { emitNewDeriveds deeper_loc theta
-            ; traceTcS "finish_derived" (ppr (ctl_depth deeper_loc))
+     finish_derived loc theta
+       = -- Use type-class instances for Deriveds, in the hope
+         -- of generating some improvements
+         -- C.f. Example 3 of Note [The improvement story]
+         -- It's easy because no evidence is involved
+         do { emitNewDeriveds loc theta
+            ; traceTcS "finish_derived" (ppr (ctl_depth loc))
             ; stopWith ev "Dict/Top (solved derived)" }
 
 chooseInstance work_item lookup_res
   = pprPanic "chooseInstance" (ppr work_item $$ ppr lookup_res)
 
+checkInstanceOK :: CtLoc -> InstanceWhat -> TcPredType -> TcS CtLoc
+-- Check that it's OK to use this insstance:
+--    (a) the use is well staged in the Template Haskell sense
+--    (b) we have not recursed too deep
+-- Returns the CtLoc to used for sub-goals
+checkInstanceOK loc what pred
+  = do { checkWellStagedDFun loc what pred
+       ; checkReductionDepth deeper_loc pred
+       ; return deeper_loc }
+  where
+     deeper_loc = zap_origin (bumpCtLocDepth loc)
+     origin     = ctLocOrigin loc
+
+     zap_origin loc  -- After applying an instance we can set ScOrigin to
+                     -- infinity, so that prohibitedSuperClassSolve never fires
+       | ScOrigin {} <- origin
+       = setCtLocOrigin loc (ScOrigin infinity)
+       | otherwise
+       = loc
+
 {- Note [Instances in no-evidence implications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In Trac #15290 we had
@@ -2331,40 +2372,10 @@ This test arranges to ignore the instance-based solution under these
 (rare) circumstances.   It's sad, but I  really don't see what else we can do.
 -}
 
-{- *******************************************************************
-*                                                                    *
-                       Class lookup
-*                                                                    *
-**********************************************************************-}
-
--- | Indicates if Instance met the Safe Haskell overlapping instances safety
--- check.
---
--- See Note [Safe Haskell Overlapping Instances] in TcSimplify
--- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
-type SafeOverlapping = Bool
-
-data LookupInstResult
-  = NoInstance   -- Definitely no instance
-
-  | OneInst { lir_new_theta :: [TcPredType]
-            , lir_mk_ev     :: [EvExpr] -> EvTerm
-            , lir_safe_over :: SafeOverlapping }
-
-  | NotSure      -- Multiple matches and/or one or more unifiers
-
-instance Outputable LookupInstResult where
-  ppr NoInstance = text "NoInstance"
-  ppr NotSure    = text "NotSure"
-  ppr (OneInst { lir_new_theta = ev
-               , lir_safe_over = s })
-    = text "OneInst" <+> vcat [ppr ev, ss]
-    where ss = text $ if s then "[safe]" else "[unsafe]"
-
 
 matchClassInst :: DynFlags -> InertSet
                -> Class -> [Type]
-               -> CtLoc -> TcS LookupInstResult
+               -> CtLoc -> TcS ClsInstResult
 matchClassInst dflags inerts clas tys loc
 -- First check whether there is an in-scope Given that could
 -- match this constraint.  In that case, do not use any instance
@@ -2393,28 +2404,12 @@ matchClassInst dflags inerts clas tys loc
                    ; return local_res }
 
            NoInstance  -- No local instances, so try global ones
-              -> do { global_res <- matchGlobalInst dflags False clas tys loc
+              -> do { global_res <- matchGlobalInst dflags False clas tys
                     ; traceTcS "} matchClassInst global result" $ ppr global_res
                     ; return global_res } }
   where
     pred = mkClassPred clas tys
 
-matchGlobalInst :: DynFlags
-                -> Bool      -- True <=> caller is the short-cut solver
-                             -- See Note [Shortcut solving: overlap]
-                -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
-matchGlobalInst dflags short_cut clas tys loc
-  | cls_name == knownNatClassName     = matchKnownNat        clas tys
-  | cls_name == knownSymbolClassName  = matchKnownSymbol     clas tys
-  | isCTupleClass clas                = matchCTuple          clas tys
-  | cls_name == typeableClassName     = matchTypeable        clas tys
-  | clas `hasKey` heqTyConKey         = matchLiftedEquality       tys
-  | clas `hasKey` coercibleTyConKey   = matchLiftedCoercible      tys
-  | cls_name == hasFieldClassName     = matchHasField dflags short_cut clas tys loc
-  | otherwise                         = matchInstEnv dflags short_cut clas tys loc
-  where
-    cls_name = className clas
-
 -- | If a class is "naturally coherent", then we needn't worry at all, in any
 -- way, about overlapping/incoherent instances. Just solve the thing!
 -- See Note [Naturally coherent classes]
@@ -2581,16 +2576,20 @@ those instances to build evidence to pass to f. That's just the
 nullary case of what's happening here.
 -}
 
-matchLocalInst :: TcPredType -> CtLoc -> TcS LookupInstResult
--- Try any Given quantified constraints, which are
--- effectively just local instance declarations.
+matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult
+-- Look up the predicate in Given quantified constraints,
+-- which are effectively just local instance declarations.
 matchLocalInst pred loc
   = do { ics <- getInertCans
        ; case match_local_inst (inert_insts ics) of
            ([], False) -> return NoInstance
            ([(dfun_ev, inst_tys)], unifs)
              | not unifs
-             -> match_one pred loc True (ctEvEvId dfun_ev) inst_tys
+             -> do { let dfun_id = ctEvEvId dfun_ev
+                   ; (tys, theta) <- instDFunType dfun_id inst_tys
+                   ; return $ OneInst { cir_new_theta = theta
+                                      , cir_mk_ev     = evDFunApp dfun_id tys
+                                      , cir_what      = LocalInstance } }
            _ -> return NotSure }
   where
     pred_tv_set = tyCoVarsOfType pred
@@ -2620,478 +2619,3 @@ matchLocalInst pred loc
         this_unif = mightMatchLater qpred (ctEvLoc ev) pred loc
         (matches, unif) = match_local_inst qcis
 
-matchInstEnv :: DynFlags -> Bool -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
-matchInstEnv dflags short_cut_solver clas tys loc
-   = do { instEnvs <- getInstEnvs
-        ; let safeOverlapCheck = safeHaskell dflags `elem` [Sf_Safe, Sf_Trustworthy]
-              (matches, unify, unsafeOverlaps) = lookupInstEnv True instEnvs clas tys
-              safeHaskFail = safeOverlapCheck && not (null unsafeOverlaps)
-        ; traceTcS "matchInstEnv" $
-            vcat [ text "goal:" <+> ppr clas <+> ppr tys
-                 , text "matches:" <+> ppr matches
-                 , text "unify:" <+> ppr unify ]
-        ; case (matches, unify, safeHaskFail) of
-
-            -- Nothing matches
-            ([], [], _)
-                -> do { traceTcS "matchClass not matching" (ppr pred)
-                      ; return NoInstance }
-
-            -- A single match (& no safe haskell failure)
-            ([(ispec, inst_tys)], [], False)
-                | short_cut_solver      -- Called from the short-cut solver
-                , isOverlappable ispec
-                -- If the instance has OVERLAPPABLE or OVERLAPS or INCOHERENT
-                -- then don't let the short-cut solver choose it, because a
-                -- later instance might overlap it.  Trac #14434 is an example
-                -- See Note [Shortcut solving: overlap]
-                -> do { traceTcS "matchClass: ignoring overlappable" (ppr pred)
-                      ; return NotSure }
-
-                | otherwise
-                -> do { let dfun_id = instanceDFunId ispec
-                      ; traceTcS "matchClass success" $
-                        vcat [text "dict" <+> ppr pred,
-                              text "witness" <+> ppr dfun_id
-                                             <+> ppr (idType dfun_id) ]
-                                -- Record that this dfun is needed
-                      ; match_one pred loc (null unsafeOverlaps) dfun_id inst_tys }
-
-            -- More than one matches (or Safe Haskell fail!). Defer any
-            -- reactions of a multitude until we learn more about the reagent
-            _   -> do { traceTcS "matchClass multiple matches, deferring choice" $
-                        vcat [text "dict" <+> ppr pred,
-                              text "matches" <+> ppr matches]
-                      ; return NotSure } }
-   where
-     pred = mkClassPred clas tys
-
-match_one :: TcPredType -> CtLoc -> SafeOverlapping
-          -> DFunId -> [DFunInstType] -> TcS LookupInstResult
-             -- See Note [DFunInstType: instantiating types] in InstEnv
-match_one pred loc so dfun_id mb_inst_tys
-  = do { traceTcS "match_one" (ppr dfun_id $$ ppr mb_inst_tys)
-       ; checkWellStagedDFun pred dfun_id loc
-       ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
-       ; traceTcS "match_one 2" (ppr dfun_id $$ ppr tys $$ ppr theta)
-       ; return $ OneInst { lir_new_theta = theta
-                          , lir_mk_ev     = evDFunApp dfun_id tys
-                          , lir_safe_over = so } }
-
-
-{- ********************************************************************
-*                                                                     *
-                   Class lookup for CTuples
-*                                                                     *
-***********************************************************************-}
-
-matchCTuple :: Class -> [Type] -> TcS LookupInstResult
-matchCTuple clas tys   -- (isCTupleClass clas) holds
-  = return (OneInst { lir_new_theta = tys
-                    , lir_mk_ev     = tuple_ev
-                    , lir_safe_over = True })
-            -- The dfun *is* the data constructor!
-  where
-     data_con = tyConSingleDataCon (classTyCon clas)
-     tuple_ev = evDFunApp (dataConWrapId data_con) tys
-
-{- ********************************************************************
-*                                                                     *
-                   Class lookup for Literals
-*                                                                     *
-***********************************************************************-}
-
-{-
-Note [KnownNat & KnownSymbol and EvLit]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A part of the type-level literals implementation are the classes
-"KnownNat" and "KnownSymbol", which provide a "smart" constructor for
-defining singleton values.  Here is the key stuff from GHC.TypeLits
-
-  class KnownNat (n :: Nat) where
-    natSing :: SNat n
-
-  newtype SNat (n :: Nat) = SNat Integer
-
-Conceptually, this class has infinitely many instances:
-
-  instance KnownNat 0       where natSing = SNat 0
-  instance KnownNat 1       where natSing = SNat 1
-  instance KnownNat 2       where natSing = SNat 2
-  ...
-
-In practice, we solve `KnownNat` predicates in the type-checker
-(see typecheck/TcInteract.hs) because we can't have infinitely many instances.
-The evidence (aka "dictionary") for `KnownNat` is of the form `EvLit (EvNum n)`.
-
-We make the following assumptions about dictionaries in GHC:
-  1. The "dictionary" for classes with a single method---like `KnownNat`---is
-     a newtype for the type of the method, so using a evidence amounts
-     to a coercion, and
-  2. Newtypes use the same representation as their definition types.
-
-So, the evidence for `KnownNat` is just a value of the representation type,
-wrapped in two newtype constructors: one to make it into a `SNat` value,
-and another to make it into a `KnownNat` dictionary.
-
-Also note that `natSing` and `SNat` are never actually exposed from the
-library---they are just an implementation detail.  Instead, users see
-a more convenient function, defined in terms of `natSing`:
-
-  natVal :: KnownNat n => proxy n -> Integer
-
-The reason we don't use this directly in the class is that it is simpler
-and more efficient to pass around an integer rather than an entire function,
-especially when the `KnowNat` evidence is packaged up in an existential.
-
-The story for kind `Symbol` is analogous:
-  * class KnownSymbol
-  * newtype SSymbol
-  * Evidence: a Core literal (e.g. mkNaturalExpr)
--}
-
-matchKnownNat :: Class -> [Type] -> TcS LookupInstResult
-matchKnownNat clas [ty]     -- clas = KnownNat
-  | Just n <- isNumLitTy ty = do
-        et <- mkNaturalExpr n
-        makeLitDict clas ty et
-matchKnownNat _ _           = return NoInstance
-
-matchKnownSymbol :: Class -> [Type] -> TcS LookupInstResult
-matchKnownSymbol clas [ty]  -- clas = KnownSymbol
-  | Just s <- isStrLitTy ty = do
-        et <- mkStringExprFS s
-        makeLitDict clas ty et
-matchKnownSymbol _ _       = return NoInstance
-
-makeLitDict :: Class -> Type -> EvExpr -> TcS LookupInstResult
--- makeLitDict adds a coercion that will convert the literal into a dictionary
--- of the appropriate type.  See Note [KnownNat & KnownSymbol and EvLit]
--- in TcEvidence.  The coercion happens in 2 steps:
---
---     Integer -> SNat n     -- representation of literal to singleton
---     SNat n  -> KnownNat n -- singleton to dictionary
---
---     The process is mirrored for Symbols:
---     String    -> SSymbol n
---     SSymbol n -> KnownSymbol n
-makeLitDict clas ty et
-    | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
-          -- co_dict :: KnownNat n ~ SNat n
-    , [ meth ]   <- classMethods clas
-    , Just tcRep <- tyConAppTyCon_maybe -- SNat
-                      $ funResultTy         -- SNat n
-                      $ dropForAlls         -- KnownNat n => SNat n
-                      $ idType meth         -- forall n. KnownNat n => SNat n
-    , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
-          -- SNat n ~ Integer
-    , let ev_tm = mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep))
-    = return $ OneInst { lir_new_theta = []
-                       , lir_mk_ev     = \_ -> ev_tm
-                       , lir_safe_over = True }
-
-    | otherwise
-    = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
-                     $$ vcat (map (ppr . idType) (classMethods clas)))
-
-{- ********************************************************************
-*                                                                     *
-                   Class lookup for Typeable
-*                                                                     *
-***********************************************************************-}
-
--- | Assumes that we've checked that this is the 'Typeable' class,
--- and it was applied to the correct argument.
-matchTypeable :: Class -> [Type] -> TcS LookupInstResult
-matchTypeable clas [k,t]  -- clas = Typeable
-  -- For the first two cases, See Note [No Typeable for polytypes or qualified types]
-  | isForAllTy k                      = return NoInstance   -- Polytype
-  | isJust (tcSplitPredFunTy_maybe t) = return NoInstance   -- Qualified type
-
-  -- Now cases that do work
-  | k `eqType` typeNatKind                 = doTyLit knownNatClassName         t
-  | k `eqType` typeSymbolKind              = doTyLit knownSymbolClassName      t
-  | isConstraintKind t                     = doTyConApp clas t constraintKindTyCon []
-  | Just (arg,ret) <- splitFunTy_maybe t   = doFunTy    clas t arg ret
-  | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)]
-  , onlyNamedBndrsApplied tc ks            = doTyConApp clas t tc ks
-  | Just (f,kt)   <- splitAppTy_maybe t    = doTyApp    clas t f kt
-
-matchTypeable _ _ = return NoInstance
-
--- | Representation for a type @ty@ of the form @arg -> ret@.
-doFunTy :: Class -> Type -> Type -> Type -> TcS LookupInstResult
-doFunTy clas ty arg_ty ret_ty
-  = return $ OneInst { lir_new_theta = preds
-                     , lir_mk_ev     = mk_ev
-                     , lir_safe_over = True }
-  where
-    preds = map (mk_typeable_pred clas) [arg_ty, ret_ty]
-    mk_ev [arg_ev, ret_ev] = evTypeable ty $
-                             EvTypeableTrFun (EvExpr arg_ev) (EvExpr ret_ev)
-    mk_ev _ = panic "TcInteract.doFunTy"
-
-
--- | Representation for type constructor applied to some kinds.
--- 'onlyNamedBndrsApplied' has ensured that this application results in a type
--- of monomorphic kind (e.g. all kind variables have been instantiated).
-doTyConApp :: Class -> Type -> TyCon -> [Kind] -> TcS LookupInstResult
-doTyConApp clas ty tc kind_args
-  | Just _ <- tyConRepName_maybe tc
-  = return $ OneInst { lir_new_theta = (map (mk_typeable_pred clas) kind_args)
-                     , lir_mk_ev = mk_ev
-                     , lir_safe_over = True }
-  | otherwise
-  = return NoInstance
-  where
-    mk_ev kinds = evTypeable ty $ EvTypeableTyCon tc (map EvExpr kinds)
-
--- | Representation for TyCon applications of a concrete kind. We just use the
--- kind itself, but first we must make sure that we've instantiated all kind-
--- polymorphism, but no more.
-onlyNamedBndrsApplied :: TyCon -> [KindOrType] -> Bool
-onlyNamedBndrsApplied tc ks
- = all isNamedTyConBinder used_bndrs &&
-   not (any isNamedTyConBinder leftover_bndrs)
- where
-   bndrs                        = tyConBinders tc
-   (used_bndrs, leftover_bndrs) = splitAtList ks bndrs
-
-doTyApp :: Class -> Type -> Type -> KindOrType -> TcS LookupInstResult
--- Representation for an application of a type to a type-or-kind.
---  This may happen when the type expression starts with a type variable.
---  Example (ignoring kind parameter):
---    Typeable (f Int Char)                      -->
---    (Typeable (f Int), Typeable Char)          -->
---    (Typeable f, Typeable Int, Typeable Char)  --> (after some simp. steps)
---    Typeable f
-doTyApp clas ty f tk
-  | isForAllTy (typeKind f)
-  = return NoInstance -- We can't solve until we know the ctr.
-  | otherwise
-  = return $ OneInst { lir_new_theta = map (mk_typeable_pred clas) [f, tk]
-                     , lir_mk_ev     = mk_ev
-                     , lir_safe_over = True }
-  where
-    mk_ev [t1,t2] = evTypeable ty $ EvTypeableTyApp (EvExpr t1) (EvExpr t2)
-    mk_ev _ = panic "doTyApp"
-
-
--- Emit a `Typeable` constraint for the given type.
-mk_typeable_pred :: Class -> Type -> PredType
-mk_typeable_pred clas ty = mkClassPred clas [ typeKind ty, ty ]
-
-  -- Typeable is implied by KnownNat/KnownSymbol. In the case of a type literal
-  -- we generate a sub-goal for the appropriate class.
-  -- See Note [Typeable for Nat and Symbol]
-doTyLit :: Name -> Type -> TcS LookupInstResult
-doTyLit kc t = do { kc_clas <- tcLookupClass kc
-                  ; let kc_pred    = mkClassPred kc_clas [ t ]
-                        mk_ev [ev] = evTypeable t $ EvTypeableTyLit (EvExpr ev)
-                        mk_ev _    = panic "doTyLit"
-                  ; return (OneInst { lir_new_theta = [kc_pred]
-                                    , lir_mk_ev     = mk_ev
-                                    , lir_safe_over   = True }) }
-
-{- Note [Typeable (T a b c)]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-For type applications we always decompose using binary application,
-via doTyApp, until we get to a *kind* instantiation.  Example
-   Proxy :: forall k. k -> *
-
-To solve Typeable (Proxy (* -> *) Maybe) we
-  - First decompose with doTyApp,
-    to get (Typeable (Proxy (* -> *))) and Typeable Maybe
-  - Then solve (Typeable (Proxy (* -> *))) with doTyConApp
-
-If we attempt to short-cut by solving it all at once, via
-doTyConApp
-
-(this note is sadly truncated FIXME)
-
-
-Note [No Typeable for polytypes or qualified types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We do not support impredicative typeable, such as
-   Typeable (forall a. a->a)
-   Typeable (Eq a => a -> a)
-   Typeable (() => Int)
-   Typeable (((),()) => Int)
-
-See Trac #9858.  For forall's the case is clear: we simply don't have
-a TypeRep for them.  For qualified but not polymorphic types, like
-(Eq a => a -> a), things are murkier.  But:
-
- * We don't need a TypeRep for these things.  TypeReps are for
-   monotypes only.
-
- * Perhaps we could treat `=>` as another type constructor for `Typeable`
-   purposes, and thus support things like `Eq Int => Int`, however,
-   at the current state of affairs this would be an odd exception as
-   no other class works with impredicative types.
-   For now we leave it off, until we have a better story for impredicativity.
-
-
-Note [Typeable for Nat and Symbol]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We have special Typeable instances for Nat and Symbol.  Roughly we
-have this instance, implemented here by doTyLit:
-      instance KnownNat n => Typeable (n :: Nat) where
-         typeRep = tyepNatTypeRep @n
-where
-   Data.Typeable.Internals.typeNatTypeRep :: KnownNat a => TypeRep a
-
-Ultimately typeNatTypeRep uses 'natSing' from KnownNat to get a
-runtime value 'n'; it turns it into a string with 'show' and uses
-that to whiz up a TypeRep TyCon for 'n', with mkTypeLitTyCon.
-See #10348.
-
-Because of this rule it's inadvisable (see #15322) to have a constraint
-    f :: (Typeable (n :: Nat)) => blah
-in a function signature; it gives rise to overlap problems just as
-if you'd written
-    f :: Eq [a] => blah
--}
-
-{- ********************************************************************
-*                                                                     *
-                   Class lookup for lifted equality
-*                                                                     *
-***********************************************************************-}
-
--- See also Note [The equality types story] in TysPrim
-matchLiftedEquality :: [Type] -> TcS LookupInstResult
-matchLiftedEquality args
-  = return (OneInst { lir_new_theta = [ mkTyConApp eqPrimTyCon args ]
-                    , lir_mk_ev     = evDFunApp (dataConWrapId heqDataCon) args
-                    , lir_safe_over = True })
-
--- See also Note [The equality types story] in TysPrim
-matchLiftedCoercible :: [Type] -> TcS LookupInstResult
-matchLiftedCoercible args@[k, t1, t2]
-  = return (OneInst { lir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
-                    , lir_mk_ev     = evDFunApp (dataConWrapId coercibleDataCon)
-                                                args
-                    , lir_safe_over = True })
-  where
-    args' = [k, k, t1, t2]
-matchLiftedCoercible args = pprPanic "matchLiftedCoercible" (ppr args)
-
-
-{- ********************************************************************
-*                                                                     *
-              Class lookup for overloaded record fields
-*                                                                     *
-***********************************************************************-}
-
-{-
-Note [HasField instances]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we have
-
-    data T y = MkT { foo :: [y] }
-
-and `foo` is in scope.  Then GHC will automatically solve a constraint like
-
-    HasField "foo" (T Int) b
-
-by emitting a new wanted
-
-    T alpha -> [alpha] ~# T Int -> b
-
-and building a HasField dictionary out of the selector function `foo`,
-appropriately cast.
-
-The HasField class is defined (in GHC.Records) thus:
-
-    class HasField (x :: k) r a | x r -> a where
-      getField :: r -> a
-
-Since this is a one-method class, it is represented as a newtype.
-Hence we can solve `HasField "foo" (T Int) b` by taking an expression
-of type `T Int -> b` and casting it using the newtype coercion.
-Note that
-
-    foo :: forall y . T y -> [y]
-
-so the expression we construct is
-
-    foo @alpha |> co
-
-where
-
-    co :: (T alpha -> [alpha]) ~# HasField "foo" (T Int) b
-
-is built from
-
-    co1 :: (T alpha -> [alpha]) ~# (T Int -> b)
-
-which is the new wanted, and
-
-    co2 :: (T Int -> b) ~# HasField "foo" (T Int) b
-
-which can be derived from the newtype coercion.
-
-If `foo` is not in scope, or has a higher-rank or existentially
-quantified type, then the constraint is not solved automatically, but
-may be solved by a user-supplied HasField instance.  Similarly, if we
-encounter a HasField constraint where the field is not a literal
-string, or does not belong to the type, then we fall back on the
-normal constraint solver behaviour.
--}
-
--- See Note [HasField instances]
-matchHasField :: DynFlags -> Bool -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
-matchHasField dflags short_cut clas tys loc
-  = do { fam_inst_envs <- getFamInstEnvs
-       ; rdr_env       <- getGlobalRdrEnvTcS
-       ; case tys of
-           -- We are matching HasField {k} x r a...
-           [_k_ty, x_ty, r_ty, a_ty]
-               -- x should be a literal string
-             | Just x <- isStrLitTy x_ty
-               -- r should be an applied type constructor
-             , Just (tc, args) <- tcSplitTyConApp_maybe r_ty
-               -- use representation tycon (if data family); it has the fields
-             , let r_tc = fstOf3 (tcLookupDataFamInst fam_inst_envs tc args)
-               -- x should be a field of r
-             , Just fl <- lookupTyConFieldLabel x r_tc
-               -- the field selector should be in scope
-             , Just gre <- lookupGRE_FieldLabel rdr_env fl
-
-             -> do { sel_id <- tcLookupId (flSelector fl)
-                   ; (tv_prs, preds, sel_ty) <- tcInstType newMetaTyVars sel_id
-
-                         -- The first new wanted constraint equates the actual
-                         -- type of the selector with the type (r -> a) within
-                         -- the HasField x r a dictionary.  The preds will
-                         -- typically be empty, but if the datatype has a
-                         -- "stupid theta" then we have to include it here.
-                   ; let theta = mkPrimEqPred sel_ty (mkFunTy r_ty a_ty) : preds
-
-                         -- Use the equality proof to cast the selector Id to
-                         -- type (r -> a), then use the newtype coercion to cast
-                         -- it to a HasField dictionary.
-                         mk_ev (ev1:evs) = evSelector sel_id tvs evs `evCast` co
-                           where
-                             co = mkTcSubCo (evTermCoercion (EvExpr ev1))
-                                      `mkTcTransCo` mkTcSymCo co2
-                         mk_ev [] = panic "matchHasField.mk_ev"
-
-                         Just (_, co2) = tcInstNewTyCon_maybe (classTyCon clas)
-                                                              tys
-
-                         tvs = mkTyVarTys (map snd tv_prs)
-
-                     -- The selector must not be "naughty" (i.e. the field
-                     -- cannot have an existentially quantified type), and
-                     -- it must not be higher-rank.
-                   ; if not (isNaughtyRecordSelector sel_id) && isTauTy sel_ty
-                     then do { addUsedGRE True gre
-                             ; return OneInst { lir_new_theta = theta
-                                              , lir_mk_ev     = mk_ev
-                                              , lir_safe_over = True
-                                              } }
-                     else matchInstEnv dflags short_cut clas tys loc }
-
-           _ -> matchInstEnv dflags short_cut clas tys loc }