{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

module GHC.Tc.Instance.Class (
     matchGlobalInst,
     ClsInstResult(..),
     InstanceWhat(..), safeOverlap, instanceReturnsDictCon,
     AssocInstInfo(..), isNotAssociated,
  ) where

import GHC.Prelude

import GHC.Driver.Session

import GHC.Core.TyCo.Rep

import GHC.Tc.Utils.Env
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.TcType
import GHC.Tc.Utils.Instantiate(instDFunType, tcInstType)
import GHC.Tc.Instance.Typeable
import GHC.Tc.Utils.TcMType
import GHC.Tc.Types.Evidence
import GHC.Tc.Instance.Family( tcGetFamInstEnvs, tcInstNewTyCon_maybe, tcLookupDataFamInst )
import GHC.Rename.Env( addUsedGRE )

import GHC.Builtin.Types
import GHC.Builtin.Types.Prim
import GHC.Builtin.Names

import GHC.Types.Name.Reader( lookupGRE_FieldLabel, greMangledName )
import GHC.Types.SafeHaskell
import GHC.Types.Name   ( Name, pprDefinedAt )
import GHC.Types.Var.Env ( VarEnv )
import GHC.Types.Id
import GHC.Types.Var

import GHC.Core.Predicate
import GHC.Core.InstEnv
import GHC.Core.Type
import GHC.Core.Make ( mkCharExpr, mkNaturalExpr, mkStringExprFS, mkCoreLams )
import GHC.Core.DataCon
import GHC.Core.TyCon
import GHC.Core.Class

import GHC.Core ( Expr(Var, App, Cast, Let), Bind (NonRec) )
import GHC.Types.Basic

import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Misc( splitAtList, fstOf3 )
import GHC.Data.FastString

import Data.Maybe

{- *******************************************************************
*                                                                    *
              A helper for associated types within
              class instance declarations
*                                                                    *
**********************************************************************-}

-- | Extra information about the parent instance declaration, needed
-- when type-checking associated types. The 'Class' is the enclosing
-- class, the [TyVar] are the /scoped/ type variable of the instance decl.
-- The @VarEnv Type@ maps class variables to their instance types.
data AssocInstInfo
  = NotAssociated
  | InClsInst { AssocInstInfo -> Class
ai_class    :: Class
              , AssocInstInfo -> [DFunId]
ai_tyvars   :: [TyVar]      -- ^ The /scoped/ tyvars of the instance
                                            -- Why scoped?  See bind_me in
                                            -- 'GHC.Tc.Validity.checkConsistentFamInst'
              , AssocInstInfo -> VarEnv Type
ai_inst_env :: VarEnv Type  -- ^ Maps /class/ tyvars to their instance types
                -- See Note [Matching in the consistent-instantiation check]
    }

isNotAssociated :: AssocInstInfo -> Bool
isNotAssociated :: AssocInstInfo -> Bool
isNotAssociated (NotAssociated {}) = Bool
True
isNotAssociated (InClsInst {})     = Bool
False


{- *******************************************************************
*                                                                    *
                       Class lookup
*                                                                    *
**********************************************************************-}

-- | Indicates if Instance met the Safe Haskell overlapping instances safety
-- check.
--
-- See Note [Safe Haskell Overlapping Instances] in GHC.Tc.Solver
-- See Note [Safe Haskell Overlapping Instances Implementation] in GHC.Tc.Solver
type SafeOverlapping = Bool

data ClsInstResult
  = NoInstance   -- Definitely no instance

  | OneInst { ClsInstResult -> [Type]
cir_new_theta :: [TcPredType]
            , ClsInstResult -> [EvExpr] -> EvTerm
cir_mk_ev     :: [EvExpr] -> EvTerm
            , ClsInstResult -> InstanceWhat
cir_what      :: InstanceWhat }

  | NotSure      -- Multiple matches and/or one or more unifiers

data InstanceWhat  -- How did we solve this constraint?
  = BuiltinEqInstance    -- Built-in solver for (t1 ~ t2), (t1 ~~ t2), Coercible t1 t2
                         -- See GHC.Tc.Solver.InertSet Note [Solved dictionaries]

  | BuiltinTypeableInstance TyCon   -- Built-in solver for Typeable (T t1 .. tn)
                         -- See Note [Well-staged instance evidence]

  | BuiltinInstance      -- Built-in solver for (C t1 .. tn) where C is
                         --   KnownNat, .. etc (classes with no top-level evidence)

  | LocalInstance        -- Solved by a quantified constraint
                         -- See GHC.Tc.Solver.InertSet Note [Solved dictionaries]

  | TopLevInstance       -- Solved by a top-level instance decl
      { InstanceWhat -> DFunId
iw_dfun_id   :: DFunId
      , InstanceWhat -> Bool
iw_safe_over :: SafeOverlapping }

instance Outputable ClsInstResult where
  ppr :: ClsInstResult -> SDoc
ppr ClsInstResult
NoInstance = String -> SDoc
text String
"NoInstance"
  ppr ClsInstResult
NotSure    = String -> SDoc
text String
"NotSure"
  ppr (OneInst { cir_new_theta :: ClsInstResult -> [Type]
cir_new_theta = [Type]
ev
               , cir_what :: ClsInstResult -> InstanceWhat
cir_what = InstanceWhat
what })
    = String -> SDoc
text String
"OneInst" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat [[Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
ev, InstanceWhat -> SDoc
forall a. Outputable a => a -> SDoc
ppr InstanceWhat
what]

instance Outputable InstanceWhat where
  ppr :: InstanceWhat -> SDoc
ppr InstanceWhat
BuiltinInstance   = String -> SDoc
text String
"a built-in instance"
  ppr BuiltinTypeableInstance {} = String -> SDoc
text String
"a built-in typeable instance"
  ppr InstanceWhat
BuiltinEqInstance = String -> SDoc
text String
"a built-in equality instance"
  ppr InstanceWhat
LocalInstance     = String -> SDoc
text String
"a locally-quantified instance"
  ppr (TopLevInstance { iw_dfun_id :: InstanceWhat -> DFunId
iw_dfun_id = DFunId
dfun })
      = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"instance" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
pprSigmaType (DFunId -> Type
idType DFunId
dfun))
           Int
2 (String -> SDoc
text String
"--" SDoc -> SDoc -> SDoc
<+> Name -> SDoc
pprDefinedAt (DFunId -> Name
idName DFunId
dfun))

safeOverlap :: InstanceWhat -> Bool
safeOverlap :: InstanceWhat -> Bool
safeOverlap (TopLevInstance { iw_safe_over :: InstanceWhat -> Bool
iw_safe_over = Bool
so }) = Bool
so
safeOverlap InstanceWhat
_                                      = Bool
True

instanceReturnsDictCon :: InstanceWhat -> Bool
-- See Note [Solved dictionaries] in GHC.Tc.Solver.InertSet
instanceReturnsDictCon :: InstanceWhat -> Bool
instanceReturnsDictCon (TopLevInstance {}) = Bool
True
instanceReturnsDictCon InstanceWhat
BuiltinInstance     = Bool
True
instanceReturnsDictCon BuiltinTypeableInstance {} = Bool
True
instanceReturnsDictCon InstanceWhat
BuiltinEqInstance   = Bool
False
instanceReturnsDictCon InstanceWhat
LocalInstance       = Bool
False

matchGlobalInst :: DynFlags
                -> Bool      -- True <=> caller is the short-cut solver
                             -- See Note [Shortcut solving: overlap]
                -> Class -> [Type] -> TcM ClsInstResult
matchGlobalInst :: DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchGlobalInst DynFlags
dflags Bool
short_cut Class
clas [Type]
tys
  | Name
cls_name Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
knownNatClassName
  = DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchKnownNat    DynFlags
dflags Bool
short_cut Class
clas [Type]
tys
  | Name
cls_name Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
knownSymbolClassName
  = DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchKnownSymbol DynFlags
dflags Bool
short_cut Class
clas [Type]
tys
  | Name
cls_name Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
knownCharClassName
  = DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchKnownChar DynFlags
dflags Bool
short_cut Class
clas [Type]
tys
  | Class -> Bool
isCTupleClass Class
clas                = Class -> [Type] -> TcM ClsInstResult
matchCTuple          Class
clas [Type]
tys
  | Name
cls_name Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
typeableClassName     = Class -> [Type] -> TcM ClsInstResult
matchTypeable        Class
clas [Type]
tys
  | Name
cls_name Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
withDictClassName     = [Type] -> TcM ClsInstResult
matchWithDict             [Type]
tys
  | Class
clas Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
heqTyConKey         = [Type] -> TcM ClsInstResult
matchHeteroEquality       [Type]
tys
  | Class
clas Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqTyConKey          = [Type] -> TcM ClsInstResult
matchHomoEquality         [Type]
tys
  | Class
clas Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
coercibleTyConKey   = [Type] -> TcM ClsInstResult
matchCoercible            [Type]
tys
  | Name
cls_name Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
hasFieldClassName     = DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchHasField DynFlags
dflags Bool
short_cut Class
clas [Type]
tys
  | Bool
otherwise                         = DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchInstEnv DynFlags
dflags Bool
short_cut Class
clas [Type]
tys
  where
    cls_name :: Name
cls_name = Class -> Name
className Class
clas


{- ********************************************************************
*                                                                     *
                   Looking in the instance environment
*                                                                     *
***********************************************************************-}


matchInstEnv :: DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchInstEnv :: DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchInstEnv DynFlags
dflags Bool
short_cut_solver Class
clas [Type]
tys
   = do { InstEnvs
instEnvs <- TcM InstEnvs
tcGetInstEnvs
        ; let safeOverlapCheck :: Bool
safeOverlapCheck = DynFlags -> SafeHaskellMode
safeHaskell DynFlags
dflags SafeHaskellMode -> [SafeHaskellMode] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SafeHaskellMode
Sf_Safe, SafeHaskellMode
Sf_Trustworthy]
              ([InstMatch]
matches, PotentialUnifiers
unify, [InstMatch]
unsafeOverlaps) = Bool
-> InstEnvs
-> Class
-> [Type]
-> ([InstMatch], PotentialUnifiers, [InstMatch])
lookupInstEnv Bool
True InstEnvs
instEnvs Class
clas [Type]
tys
              safeHaskFail :: Bool
safeHaskFail = Bool
safeOverlapCheck Bool -> Bool -> Bool
&& Bool -> Bool
not ([InstMatch] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [InstMatch]
unsafeOverlaps)
        ; String -> SDoc -> TcRn ()
traceTc String
"matchInstEnv" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
            [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"goal:" SDoc -> SDoc -> SDoc
<+> Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
clas SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys
                 , String -> SDoc
text String
"matches:" SDoc -> SDoc -> SDoc
<+> [InstMatch] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [InstMatch]
matches
                 , String -> SDoc
text String
"unify:" SDoc -> SDoc -> SDoc
<+> PotentialUnifiers -> SDoc
forall a. Outputable a => a -> SDoc
ppr PotentialUnifiers
unify ]
        ; case ([InstMatch]
matches, PotentialUnifiers
unify, Bool
safeHaskFail) of

            -- Nothing matches
            ([], PotentialUnifiers
NoUnifiers, Bool
_)
                -> do { String -> SDoc -> TcRn ()
traceTc String
"matchClass not matching" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred)
                      ; ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
NoInstance }

            -- A single match (& no safe haskell failure)
            ([(ClsInst
ispec, [DFunInstType]
inst_tys)], PotentialUnifiers
NoUnifiers, Bool
False)
                | Bool
short_cut_solver      -- Called from the short-cut solver
                , ClsInst -> Bool
isOverlappable ClsInst
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.  #14434 is an example
                -- See Note [Shortcut solving: overlap]
                -> do { String -> SDoc -> TcRn ()
traceTc String
"matchClass: ignoring overlappable" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred)
                      ; ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
NotSure }

                | Bool
otherwise
                -> do { let dfun_id :: DFunId
dfun_id = ClsInst -> DFunId
instanceDFunId ClsInst
ispec
                      ; String -> SDoc -> TcRn ()
traceTc String
"matchClass success" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
                        [SDoc] -> SDoc
vcat [String -> SDoc
text String
"dict" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred,
                              String -> SDoc
text String
"witness" SDoc -> SDoc -> SDoc
<+> DFunId -> SDoc
forall a. Outputable a => a -> SDoc
ppr DFunId
dfun_id
                                             SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (DFunId -> Type
idType DFunId
dfun_id) ]
                                -- Record that this dfun is needed
                      ; Bool -> DFunId -> [DFunInstType] -> TcM ClsInstResult
match_one ([InstMatch] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [InstMatch]
unsafeOverlaps) DFunId
dfun_id [DFunInstType]
inst_tys }

            -- More than one matches (or Safe Haskell fail!). Defer any
            -- reactions of a multitude until we learn more about the reagent
            ([InstMatch], PotentialUnifiers, Bool)
_   -> do { String -> SDoc -> TcRn ()
traceTc String
"matchClass multiple matches, deferring choice" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
                        [SDoc] -> SDoc
vcat [String -> SDoc
text String
"dict" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred,
                              String -> SDoc
text String
"matches" SDoc -> SDoc -> SDoc
<+> [InstMatch] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [InstMatch]
matches]
                      ; ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
NotSure } }
   where
     pred :: Type
pred = Class -> [Type] -> Type
mkClassPred Class
clas [Type]
tys

match_one :: SafeOverlapping -> DFunId -> [DFunInstType] -> TcM ClsInstResult
             -- See Note [DFunInstType: instantiating types] in GHC.Core.InstEnv
match_one :: Bool -> DFunId -> [DFunInstType] -> TcM ClsInstResult
match_one Bool
so DFunId
dfun_id [DFunInstType]
mb_inst_tys
  = do { String -> SDoc -> TcRn ()
traceTc String
"match_one" (DFunId -> SDoc
forall a. Outputable a => a -> SDoc
ppr DFunId
dfun_id SDoc -> SDoc -> SDoc
$$ [DFunInstType] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [DFunInstType]
mb_inst_tys)
       ; ([Type]
tys, [Type]
theta) <- DFunId -> [DFunInstType] -> TcM ([Type], [Type])
instDFunType DFunId
dfun_id [DFunInstType]
mb_inst_tys
       ; String -> SDoc -> TcRn ()
traceTc String
"match_one 2" (DFunId -> SDoc
forall a. Outputable a => a -> SDoc
ppr DFunId
dfun_id SDoc -> SDoc -> SDoc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys SDoc -> SDoc -> SDoc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
theta)
       ; ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ClsInstResult -> TcM ClsInstResult)
-> ClsInstResult -> TcM ClsInstResult
forall a b. (a -> b) -> a -> b
$ OneInst { cir_new_theta :: [Type]
cir_new_theta = [Type]
theta
                          , cir_mk_ev :: [EvExpr] -> EvTerm
cir_mk_ev     = DFunId -> [Type] -> [EvExpr] -> EvTerm
evDFunApp DFunId
dfun_id [Type]
tys
                          , cir_what :: InstanceWhat
cir_what      = TopLevInstance { iw_dfun_id :: DFunId
iw_dfun_id = DFunId
dfun_id
                                                           , iw_safe_over :: Bool
iw_safe_over = Bool
so } } }


{- Note [Shortcut solving: overlap]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
  instance {-# OVERLAPPABLE #-} C a where ...
and we are typechecking
  f :: C a => a -> a
  f = e  -- Gives rise to [W] C a

We don't want to solve the wanted constraint with the overlappable
instance; rather we want to use the supplied (C a)! That was the whole
point of it being overlappable!  #14434 wwas an example.

Alas even if the instance has no overlap flag, thus
  instance C a where ...
there is nothing to stop it being overlapped. GHC provides no way to
declare an instance as "final" so it can't be overlapped.  But really
only final instances are OK for short-cut solving.  Sigh. #15135
was a puzzling example.
-}


{- ********************************************************************
*                                                                     *
                   Class lookup for CTuples
*                                                                     *
***********************************************************************-}

matchCTuple :: Class -> [Type] -> TcM ClsInstResult
matchCTuple :: Class -> [Type] -> TcM ClsInstResult
matchCTuple Class
clas [Type]
tys   -- (isCTupleClass clas) holds
  = ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (OneInst { cir_new_theta :: [Type]
cir_new_theta = [Type]
tys
                    , cir_mk_ev :: [EvExpr] -> EvTerm
cir_mk_ev     = [EvExpr] -> EvTerm
tuple_ev
                    , cir_what :: InstanceWhat
cir_what      = InstanceWhat
BuiltinInstance })
            -- The dfun *is* the data constructor!
  where
     data_con :: DataCon
data_con = TyCon -> DataCon
tyConSingleDataCon (Class -> TyCon
classTyCon Class
clas)
     tuple_ev :: [EvExpr] -> EvTerm
tuple_ev = DFunId -> [Type] -> [EvExpr] -> EvTerm
evDFunApp (DataCon -> DFunId
dataConWrapId DataCon
data_con) [Type]
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.TypeNats

  class KnownNat (n :: Nat) where
    natSing :: SNat n

  newtype SNat (n :: Nat) = SNat Natural

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 GHC.Tc.Solver.Interact) 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 -> Natural

The reason we don't use this directly in the class is that it is simpler
and more efficient to pass around a Natural rather than an entire function,
especially when the `KnownNat` 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)


Note [Fabricating Evidence for Literals in Backpack]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Let `T` be a type of kind `Nat`. When solving for a purported instance
of `KnownNat T`, ghc tries to resolve the type `T` to an integer `n`,
in which case the evidence `EvLit (EvNum n)` is generated on the
fly. It might appear that this is sufficient as users cannot define
their own instances of `KnownNat`. However, for backpack module this
would not work (see issue #15379). Consider the signature `Abstract`

> signature Abstract where
>   data T :: Nat
>   instance KnownNat T

and a module `Util` that depends on it:

> module Util where
>  import Abstract
>  printT :: IO ()
>  printT = do print $ natVal (Proxy :: Proxy T)

Clearly, we need to "use" the dictionary associated with `KnownNat T`
in the module `Util`, but it is too early for the compiler to produce
a real dictionary as we still have not fixed what `T` is. Only when we
mixin a concrete module

> module Concrete where
>   type T = 42

do we really get hold of the underlying integer. So the strategy that
we follow is the following

1. If T is indeed available as a type alias for an integer constant,
   generate the dictionary on the fly, failing which

2. Look up the type class environment for the evidence.

Finally actual code gets generate for Util only when a module like
Concrete gets "mixed-in" in place of the signature Abstract. As a
result all things, including the typeclass instances, in Concrete gets
reexported. So `KnownNat` gets resolved the normal way post-Backpack.

A similar generation works for `KnownSymbol` as well

-}

matchKnownNat :: DynFlags
              -> Bool      -- True <=> caller is the short-cut solver
                           -- See Note [Shortcut solving: overlap]
              -> Class -> [Type] -> TcM ClsInstResult
matchKnownNat :: DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchKnownNat DynFlags
dflags Bool
_ Class
clas [Type
ty]     -- clas = KnownNat
  | Just Integer
n <- Type -> Maybe Integer
isNumLitTy Type
ty  = Class -> Type -> EvExpr -> TcM ClsInstResult
makeLitDict Class
clas Type
ty (Platform -> Integer -> EvExpr
mkNaturalExpr (DynFlags -> Platform
targetPlatform DynFlags
dflags) Integer
n)
matchKnownNat DynFlags
df Bool
sc Class
clas [Type]
tys = DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchInstEnv DynFlags
df Bool
sc Class
clas [Type]
tys
 -- See Note [Fabricating Evidence for Literals in Backpack] for why
 -- this lookup into the instance environment is required.

matchKnownSymbol :: DynFlags
                 -> Bool      -- True <=> caller is the short-cut solver
                              -- See Note [Shortcut solving: overlap]
                 -> Class -> [Type] -> TcM ClsInstResult
matchKnownSymbol :: DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchKnownSymbol DynFlags
_ Bool
_ Class
clas [Type
ty]  -- clas = KnownSymbol
  | Just FastString
s <- Type -> Maybe FastString
isStrLitTy Type
ty = do
        EvExpr
et <- FastString -> IOEnv (Env TcGblEnv TcLclEnv) EvExpr
forall (m :: * -> *). MonadThings m => FastString -> m EvExpr
mkStringExprFS FastString
s
        Class -> Type -> EvExpr -> TcM ClsInstResult
makeLitDict Class
clas Type
ty EvExpr
et
matchKnownSymbol DynFlags
df Bool
sc Class
clas [Type]
tys = DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchInstEnv DynFlags
df Bool
sc Class
clas [Type]
tys
 -- See Note [Fabricating Evidence for Literals in Backpack] for why
 -- this lookup into the instance environment is required.

matchKnownChar :: DynFlags
                 -> Bool      -- True <=> caller is the short-cut solver
                              -- See Note [Shortcut solving: overlap]
                 -> Class -> [Type] -> TcM ClsInstResult
matchKnownChar :: DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchKnownChar DynFlags
_ Bool
_ Class
clas [Type
ty]  -- clas = KnownChar
  | Just Char
s <- Type -> Maybe Char
isCharLitTy Type
ty = Class -> Type -> EvExpr -> TcM ClsInstResult
makeLitDict Class
clas Type
ty (Char -> EvExpr
mkCharExpr Char
s)
matchKnownChar DynFlags
df Bool
sc Class
clas [Type]
tys = DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchInstEnv DynFlags
df Bool
sc Class
clas [Type]
tys
 -- See Note [Fabricating Evidence for Literals in Backpack] for why
 -- this lookup into the instance environment is required.

makeLitDict :: Class -> Type -> EvExpr -> TcM ClsInstResult
-- makeLitDict adds a coercion that will convert the literal into a dictionary
-- of the appropriate type.  See Note [KnownNat & KnownSymbol and EvLit]
-- in GHC.Tc.Types.Evidence.  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 :: Class -> Type -> EvExpr -> TcM ClsInstResult
makeLitDict Class
clas Type
ty EvExpr
et
    | Just (Type
_, TcCoercion
co_dict) <- TyCon -> [Type] -> Maybe (Type, TcCoercion)
tcInstNewTyCon_maybe (Class -> TyCon
classTyCon Class
clas) [Type
ty]
          -- co_dict :: KnownNat n ~ SNat n
    , [ DFunId
meth ]   <- Class -> [DFunId]
classMethods Class
clas
    , Just TyCon
tcRep <- Type -> Maybe TyCon
tyConAppTyCon_maybe (DFunId -> Type
classMethodTy DFunId
meth)
                    -- If the method type is forall n. KnownNat n => SNat n
                    -- then tcRep is SNat
    , Just (Type
_, TcCoercion
co_rep) <- TyCon -> [Type] -> Maybe (Type, TcCoercion)
tcInstNewTyCon_maybe TyCon
tcRep [Type
ty]
          -- SNat n ~ Integer
    , let ev_tm :: EvTerm
ev_tm = EvExpr -> TcCoercion -> EvTerm
mkEvCast EvExpr
et (TcCoercion -> TcCoercion
mkTcSymCo (TcCoercion -> TcCoercion -> TcCoercion
mkTcTransCo TcCoercion
co_dict TcCoercion
co_rep))
    = ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ClsInstResult -> TcM ClsInstResult)
-> ClsInstResult -> TcM ClsInstResult
forall a b. (a -> b) -> a -> b
$ OneInst { cir_new_theta :: [Type]
cir_new_theta = []
                       , cir_mk_ev :: [EvExpr] -> EvTerm
cir_mk_ev     = \[EvExpr]
_ -> EvTerm
ev_tm
                       , cir_what :: InstanceWhat
cir_what      = InstanceWhat
BuiltinInstance }

    | Bool
otherwise
    = String -> SDoc -> TcM ClsInstResult
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"makeLitDict" (SDoc -> TcM ClsInstResult) -> SDoc -> TcM ClsInstResult
forall a b. (a -> b) -> a -> b
$
      String -> SDoc
text String
"Unexpected evidence for" SDoc -> SDoc -> SDoc
<+> Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Class -> Name
className Class
clas)
      SDoc -> SDoc -> SDoc
$$ [SDoc] -> SDoc
vcat ((DFunId -> SDoc) -> [DFunId] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Type -> SDoc) -> (DFunId -> Type) -> DFunId -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DFunId -> Type
idType) (Class -> [DFunId]
classMethods Class
clas))

{- ********************************************************************
*                                                                     *
                   Class lookup for WithDict
*                                                                     *
***********************************************************************-}

-- See Note [withDict]
matchWithDict :: [Type] -> TcM ClsInstResult
matchWithDict :: [Type] -> TcM ClsInstResult
matchWithDict [Type
cls, Type
mty]
    -- Check that cls is a class constraint `C t_1 ... t_n`, where
    -- `dict_tc = C` and `dict_args = t_1 ... t_n`.
  | Just (TyCon
dict_tc, [Type]
dict_args) <- HasCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
cls
    -- Check that C is a class of the form
    -- `class C a_1 ... a_n where op :: meth_ty`
    -- and in that case let
    -- co :: C t1 ..tn ~R# inst_meth_ty
  , Just (Type
inst_meth_ty, TcCoercion
co) <- TyCon -> [Type] -> Maybe (Type, TcCoercion)
tcInstNewTyCon_maybe TyCon
dict_tc [Type]
dict_args
  = do { DFunId
sv <- FastString -> Type -> Type -> IOEnv (Env TcGblEnv TcLclEnv) DFunId
forall (m :: * -> *).
MonadUnique m =>
FastString -> Type -> Type -> m DFunId
mkSysLocalM (String -> FastString
fsLit String
"withDict_s") Type
Many Type
mty
       ; DFunId
k  <- FastString -> Type -> Type -> IOEnv (Env TcGblEnv TcLclEnv) DFunId
forall (m :: * -> *).
MonadUnique m =>
FastString -> Type -> Type -> m DFunId
mkSysLocalM (String -> FastString
fsLit String
"withDict_k") Type
Many (Type -> Type -> Type
mkInvisFunTyMany Type
cls Type
openAlphaTy)

       ; let evWithDict_type :: Type
evWithDict_type = [DFunId] -> Type -> Type
mkSpecForAllTys [DFunId
runtimeRep1TyVar, DFunId
openAlphaTyVar] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
                               [Type] -> Type -> Type
mkVisFunTysMany [Type
mty, Type -> Type -> Type
mkInvisFunTyMany Type
cls Type
openAlphaTy] Type
openAlphaTy

       ; DFunId
wd_id <- FastString -> Type -> Type -> IOEnv (Env TcGblEnv TcLclEnv) DFunId
forall (m :: * -> *).
MonadUnique m =>
FastString -> Type -> Type -> m DFunId
mkSysLocalM (String -> FastString
fsLit String
"withDict_wd") Type
Many Type
evWithDict_type
       ; let wd_id' :: DFunId
wd_id' = DFunId
wd_id DFunId -> InlinePragma -> DFunId
`setInlinePragma` InlinePragma
neverInlinePragma
               -- Inlining withDict can cause the specialiser to incorrectly common up
               -- distinct evidence terms. See (WD6) in Note [withDict].

       -- Given co2 : mty ~N# inst_meth_ty, construct the method of
       -- the WithDict dictionary:
       -- \@(r : RuntimeRep) @(a :: TYPE r) (sv : mty) (k :: cls => a) -> k (sv |> (sub co; sym co2))
       ; let evWithDict :: TcCoercion -> EvExpr
evWithDict TcCoercion
co2 =
               let wd_rhs :: EvExpr
wd_rhs = [DFunId] -> EvExpr -> EvExpr
mkCoreLams [ DFunId
runtimeRep1TyVar, DFunId
openAlphaTyVar, DFunId
sv, DFunId
k ] (EvExpr -> EvExpr) -> EvExpr -> EvExpr
forall a b. (a -> b) -> a -> b
$
                            DFunId -> EvExpr
forall b. DFunId -> Expr b
Var DFunId
k EvExpr -> EvExpr -> EvExpr
forall b. Expr b -> Expr b -> Expr b
`App` EvExpr -> TcCoercion -> EvExpr
forall b. Expr b -> TcCoercion -> Expr b
Cast (DFunId -> EvExpr
forall b. DFunId -> Expr b
Var DFunId
sv) (TcCoercion -> TcCoercion -> TcCoercion
mkTcTransCo ((() :: Constraint) => TcCoercion -> TcCoercion
TcCoercion -> TcCoercion
mkTcSubCo TcCoercion
co2) (TcCoercion -> TcCoercion
mkTcSymCo TcCoercion
co))
               in Bind DFunId -> EvExpr -> EvExpr
forall b. Bind b -> Expr b -> Expr b
Let (DFunId -> EvExpr -> Bind DFunId
forall b. b -> Expr b -> Bind b
NonRec DFunId
wd_id' EvExpr
wd_rhs) (DFunId -> EvExpr
forall b. DFunId -> Expr b
Var DFunId
wd_id')
         -- Why a Let?  See (WD6) in Note [withDict]

       ; TyCon
tc <- Name -> TcM TyCon
tcLookupTyCon Name
withDictClassName
       ; let Just DataCon
withdict_data_con
                 = TyCon -> Maybe DataCon
tyConSingleDataCon_maybe TyCon
tc    -- "Data constructor"
                                                  -- for WithDict
             mk_ev :: [EvExpr] -> EvTerm
mk_ev [EvExpr
c] = DataCon -> [Type] -> [EvExpr] -> EvTerm
evDataConApp DataCon
withdict_data_con
                            [Type
cls, Type
mty] [TcCoercion -> EvExpr
evWithDict (EvTerm -> TcCoercion
evTermCoercion (EvExpr -> EvTerm
EvExpr EvExpr
c))]
             mk_ev [EvExpr]
e   = String -> SDoc -> EvTerm
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"matchWithDict" ([EvExpr] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [EvExpr]
e)

       ; ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ClsInstResult -> TcM ClsInstResult)
-> ClsInstResult -> TcM ClsInstResult
forall a b. (a -> b) -> a -> b
$ OneInst { cir_new_theta :: [Type]
cir_new_theta = [Type -> Type -> Type
mkPrimEqPred Type
mty Type
inst_meth_ty]
                          , cir_mk_ev :: [EvExpr] -> EvTerm
cir_mk_ev     = [EvExpr] -> EvTerm
mk_ev
                          , cir_what :: InstanceWhat
cir_what      = InstanceWhat
BuiltinInstance }
       }

matchWithDict [Type]
_
  = ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
NoInstance

{-
Note [withDict]
~~~~~~~~~~~~~~~
The class `WithDict` is defined as:

    class WithDict cls meth where
        withDict :: forall {rr :: RuntimeRep} (r :: TYPE rr). meth -> (cls => r) -> r

This class is special, like `Typeable`: GHC automatically solves
for instances of `WithDict`, users cannot write their own.

It is used to implement a primitive that we cannot define in Haskell
but we can write in Core.

`WithDict` is used to create dictionaries for classes with a single method.
Consider a class like this:

   class C a where
     f :: T a

We can use `withDict` to cast values of type `T a` into dictionaries for `C a`.
To do this, we can define a function like this in the library:

  withT :: T a -> (C a => b) -> b
  withT t k = withDict @(C a) @(T a) t k

Here:

* The `cls` in `withDict` is instantiated to `C a`.

* The `meth` in `withDict` is instantiated to `T a`.
  The definition of `T` itself is irrelevant, only that `C a` is a class
  with a single method of type `T a`.

* The `r` in `withDict` is instantiated to `b`.

For any single-method class C:
   class C a1 .. an where op :: meth_ty

The solver will solve the constraint `WithDict (C t1 .. tn) mty`
as if the following instance declaration existed:

instance (mty ~# inst_meth_ty) => WithDict (C t1..tn) mty where
  withDict = \@{rr} @(r :: TYPE rr) (sv :: mty) (k :: C t1..tn => r) ->
    k (sv |> (sub co2; sym co))

That is, it matches on the first (constraint) argument of C; if C is
a single-method class, the instance "fires" and emits an equality
constraint `mty ~ inst_meth_ty`, where `inst_meth_ty` is `meth_ty[ti/ai]`.
The coercion `co2` witnesses the equality `mty ~ inst_meth_ty`.

The coercion `co` is a newtype coercion that coerces from `C t1 ... tn`
to `inst_meth_ty`.
This coercion is guaranteed to exist by virtue of the fact that
C is a class with exactly one method and no superclasses, so it
is treated like a newtype when compiled to Core.

The condition that `C` is a single-method class is implemented in the
guards of matchWithDict's definition.
If the conditions are not held, the rewriting will not fire,
and we'll report an unsolved constraint.

Some further observations about `withDict`:

(WD1) The `cls` in the type of withDict must be explicitly instantiated with
      visible type application, as invoking `withDict` would be ambiguous
      otherwise.

      For examples of how `withDict` is used in the `base` library, see `withSNat`
      in GHC.TypeNats, as well as `withSChar` and `withSSymbol` in GHC.TypeLits.

(WD2) The `r` is representation-polymorphic, to support things like
      `withTypeable` in `Data.Typeable.Internal`.

(WD3) As an alternative to `withDict`, one could define functions like `withT`
      above in terms of `unsafeCoerce`. This is more error-prone, however.

(WD4) In order to define things like `reifySymbol` below:

        reifySymbol :: forall r. String -> (forall (n :: Symbol). KnownSymbol n => r) -> r

      `withDict` needs to be instantiated with `Any`, like so:

        reifySymbol n k = withDict @(KnownSymbol Any) @String @r n (k @Any)

      The use of `Any` is explained in Note [NOINLINE someNatVal] in
      base:GHC.TypeNats.

(WD5) In earlier implementations, `withDict` was implemented as an identifier
      with special handling during either constant-folding or desugaring.
      The current approach is more robust, previously the type of `withDict`
      did not have a type-class constraint and was overly polymorphic.
      See #19915.

(WD6) In fact we desugar `withDict @(C t_1 ... t_n) @mty @{rr} @r` to

         let wd = \sv k -> k (sv |> co)
             {-# NOINLINE wd #-}
         in wd

      The local `let` and NOINLINE pragma ensure that the type-class specialiser
      doesn't wrongly common up distinct evidence terms. This is super important!
      Suppose we have calls
          withDict A k
          withDict B k
      where k1, k2 :: C T -> blah.  If we inline those withDict calls we'll get
          k (A |> co1)
          k (B |> co2)
      and the Specialiser will assume that those arguments (of type `C T`) are
      the same, will specialise `k` for that type, and will call the same,
      specialised function from both call sites.  #21575 is a concrete case in point.

      Solution: never inline `withDict`. Note that it is not sufficient to delay
      inlining until after the specialiser (that is, until Phase 2), because if
      we inline withDict in module A but import it in module B, the specialiser
      will try to common up the two distinct evidence terms.
      See test case T21575b.

      This solution is unsatisfactory, as it imposes a performance overhead
      on uses of withDict.

-}

{- ********************************************************************
*                                                                     *
                   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] -> TcM ClsInstResult
matchTypeable :: Class -> [Type] -> TcM ClsInstResult
matchTypeable Class
clas [Type
k,Type
t]  -- clas = Typeable
  -- For the first two cases, See Note [No Typeable for polytypes or qualified types]
  | Type -> Bool
isForAllTy Type
k                      = ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
NoInstance   -- Polytype
  | Maybe (Type, Type) -> Bool
forall a. Maybe a -> Bool
isJust (Type -> Maybe (Type, Type)
tcSplitPredFunTy_maybe Type
t) = ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
NoInstance   -- Qualified type

  -- Now cases that do work
  | Type
k Type -> Type -> Bool
`eqType` Type
naturalTy                   = Name -> Type -> TcM ClsInstResult
doTyLit Name
knownNatClassName         Type
t
  | Type
k Type -> Type -> Bool
`eqType` Type
typeSymbolKind              = Name -> Type -> TcM ClsInstResult
doTyLit Name
knownSymbolClassName      Type
t
  | Type
k Type -> Type -> Bool
`eqType` Type
charTy                      = Name -> Type -> TcM ClsInstResult
doTyLit Name
knownCharClassName        Type
t
  | Type -> Bool
tcIsConstraintKind Type
t                   = Class -> Type -> TyCon -> [Type] -> TcM ClsInstResult
doTyConApp Class
clas Type
t TyCon
constraintKindTyCon []
  | Just (Type
mult,Type
arg,Type
ret) <- Type -> Maybe (Type, Type, Type)
splitFunTy_maybe Type
t   = Class -> Type -> Type -> Type -> Type -> TcM ClsInstResult
doFunTy    Class
clas Type
t Type
mult Type
arg Type
ret
  | Just (TyCon
tc, [Type]
ks) <- (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
t -- See Note [Typeable (T a b c)]
  , TyCon -> [Type] -> Bool
onlyNamedBndrsApplied TyCon
tc [Type]
ks            = Class -> Type -> TyCon -> [Type] -> TcM ClsInstResult
doTyConApp Class
clas Type
t TyCon
tc [Type]
ks
  | Just (Type
f,Type
kt)   <- Type -> Maybe (Type, Type)
splitAppTy_maybe Type
t    = Class -> Type -> Type -> Type -> TcM ClsInstResult
doTyApp    Class
clas Type
t Type
f Type
kt

matchTypeable Class
_ [Type]
_ = ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
NoInstance

-- | Representation for a type @ty@ of the form @arg -> ret@.
doFunTy :: Class -> Type -> Mult -> Type -> Type -> TcM ClsInstResult
doFunTy :: Class -> Type -> Type -> Type -> Type -> TcM ClsInstResult
doFunTy Class
clas Type
ty Type
mult Type
arg_ty Type
ret_ty
  = ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ClsInstResult -> TcM ClsInstResult)
-> ClsInstResult -> TcM ClsInstResult
forall a b. (a -> b) -> a -> b
$ OneInst { cir_new_theta :: [Type]
cir_new_theta = [Type]
preds
                     , cir_mk_ev :: [EvExpr] -> EvTerm
cir_mk_ev     = [EvExpr] -> EvTerm
mk_ev
                     , cir_what :: InstanceWhat
cir_what      = InstanceWhat
BuiltinInstance }
  where
    preds :: [Type]
preds = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Class -> Type -> Type
mk_typeable_pred Class
clas) [Type
mult, Type
arg_ty, Type
ret_ty]
    mk_ev :: [EvExpr] -> EvTerm
mk_ev [EvExpr
mult_ev, EvExpr
arg_ev, EvExpr
ret_ev] = Type -> EvTypeable -> EvTerm
evTypeable Type
ty (EvTypeable -> EvTerm) -> EvTypeable -> EvTerm
forall a b. (a -> b) -> a -> b
$
                        EvTerm -> EvTerm -> EvTerm -> EvTypeable
EvTypeableTrFun (EvExpr -> EvTerm
EvExpr EvExpr
mult_ev) (EvExpr -> EvTerm
EvExpr EvExpr
arg_ev) (EvExpr -> EvTerm
EvExpr EvExpr
ret_ev)
    mk_ev [EvExpr]
_ = String -> EvTerm
forall a. String -> a
panic String
"GHC.Tc.Solver.Interact.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] -> TcM ClsInstResult
doTyConApp :: Class -> Type -> TyCon -> [Type] -> TcM ClsInstResult
doTyConApp Class
clas Type
ty TyCon
tc [Type]
kind_args
  | TyCon -> Bool
tyConIsTypeable TyCon
tc
  = do
     ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ClsInstResult -> TcM ClsInstResult)
-> ClsInstResult -> TcM ClsInstResult
forall a b. (a -> b) -> a -> b
$ OneInst { cir_new_theta :: [Type]
cir_new_theta = ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Class -> Type -> Type
mk_typeable_pred Class
clas) [Type]
kind_args)
                      , cir_mk_ev :: [EvExpr] -> EvTerm
cir_mk_ev     = [EvExpr] -> EvTerm
mk_ev
                      , cir_what :: InstanceWhat
cir_what      = TyCon -> InstanceWhat
BuiltinTypeableInstance TyCon
tc }
  | Bool
otherwise
  = ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
NoInstance
  where
    mk_ev :: [EvExpr] -> EvTerm
mk_ev [EvExpr]
kinds = Type -> EvTypeable -> EvTerm
evTypeable Type
ty (EvTypeable -> EvTerm) -> EvTypeable -> EvTerm
forall a b. (a -> b) -> a -> b
$ TyCon -> [EvTerm] -> EvTypeable
EvTypeableTyCon TyCon
tc ((EvExpr -> EvTerm) -> [EvExpr] -> [EvTerm]
forall a b. (a -> b) -> [a] -> [b]
map EvExpr -> EvTerm
EvExpr [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 :: TyCon -> [Type] -> Bool
onlyNamedBndrsApplied TyCon
tc [Type]
ks
 = (TyConBinder -> Bool) -> [TyConBinder] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TyConBinder -> Bool
isNamedTyConBinder [TyConBinder]
used_bndrs Bool -> Bool -> Bool
&&
   Bool -> Bool
not ((TyConBinder -> Bool) -> [TyConBinder] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TyConBinder -> Bool
isNamedTyConBinder [TyConBinder]
leftover_bndrs)
 where
   bndrs :: [TyConBinder]
bndrs                        = TyCon -> [TyConBinder]
tyConBinders TyCon
tc
   ([TyConBinder]
used_bndrs, [TyConBinder]
leftover_bndrs) = [Type] -> [TyConBinder] -> ([TyConBinder], [TyConBinder])
forall b a. [b] -> [a] -> ([a], [a])
splitAtList [Type]
ks [TyConBinder]
bndrs

doTyApp :: Class -> Type -> Type -> KindOrType -> TcM ClsInstResult
-- 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 :: Class -> Type -> Type -> Type -> TcM ClsInstResult
doTyApp Class
clas Type
ty Type
f Type
tk
  | Type -> Bool
isForAllTy ((() :: Constraint) => Type -> Type
Type -> Type
tcTypeKind Type
f)
  = ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
NoInstance -- We can't solve until we know the ctr.
  | Bool
otherwise
  = ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ClsInstResult -> TcM ClsInstResult)
-> ClsInstResult -> TcM ClsInstResult
forall a b. (a -> b) -> a -> b
$ OneInst { cir_new_theta :: [Type]
cir_new_theta = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Class -> Type -> Type
mk_typeable_pred Class
clas) [Type
f, Type
tk]
                     , cir_mk_ev :: [EvExpr] -> EvTerm
cir_mk_ev     = [EvExpr] -> EvTerm
mk_ev
                     , cir_what :: InstanceWhat
cir_what      = InstanceWhat
BuiltinInstance }
  where
    mk_ev :: [EvExpr] -> EvTerm
mk_ev [EvExpr
t1,EvExpr
t2] = Type -> EvTypeable -> EvTerm
evTypeable Type
ty (EvTypeable -> EvTerm) -> EvTypeable -> EvTerm
forall a b. (a -> b) -> a -> b
$ EvTerm -> EvTerm -> EvTypeable
EvTypeableTyApp (EvExpr -> EvTerm
EvExpr EvExpr
t1) (EvExpr -> EvTerm
EvExpr EvExpr
t2)
    mk_ev [EvExpr]
_ = String -> EvTerm
forall a. String -> a
panic String
"doTyApp"


-- Emit a `Typeable` constraint for the given type.
mk_typeable_pred :: Class -> Type -> PredType
mk_typeable_pred :: Class -> Type -> Type
mk_typeable_pred Class
clas Type
ty = Class -> [Type] -> Type
mkClassPred Class
clas [ (() :: Constraint) => Type -> Type
Type -> Type
tcTypeKind Type
ty, Type
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 -> TcM ClsInstResult
doTyLit :: Name -> Type -> TcM ClsInstResult
doTyLit Name
kc Type
t = do { Class
kc_clas <- Name -> TcM Class
tcLookupClass Name
kc
                  ; let kc_pred :: Type
kc_pred    = Class -> [Type] -> Type
mkClassPred Class
kc_clas [ Type
t ]
                        mk_ev :: [EvExpr] -> EvTerm
mk_ev [EvExpr
ev] = Type -> EvTypeable -> EvTerm
evTypeable Type
t (EvTypeable -> EvTerm) -> EvTypeable -> EvTerm
forall a b. (a -> b) -> a -> b
$ EvTerm -> EvTypeable
EvTypeableTyLit (EvExpr -> EvTerm
EvExpr EvExpr
ev)
                        mk_ev [EvExpr]
_    = String -> EvTerm
forall a. String -> a
panic String
"doTyLit"
                  ; ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (OneInst { cir_new_theta :: [Type]
cir_new_theta = [Type
kc_pred]
                                    , cir_mk_ev :: [EvExpr] -> EvTerm
cir_mk_ev     = [EvExpr] -> EvTerm
mk_ev
                                    , cir_what :: InstanceWhat
cir_what      = InstanceWhat
BuiltinInstance }) }

{- 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 #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 = typeNatTypeRep @n
where
   Data.Typeable.Internal.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 GHC.Builtin.Types.Prim
matchHeteroEquality :: [Type] -> TcM ClsInstResult
-- Solves (t1 ~~ t2)
matchHeteroEquality :: [Type] -> TcM ClsInstResult
matchHeteroEquality [Type]
args
  = ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (OneInst { cir_new_theta :: [Type]
cir_new_theta = [ TyCon -> [Type] -> Type
mkTyConApp TyCon
eqPrimTyCon [Type]
args ]
                    , cir_mk_ev :: [EvExpr] -> EvTerm
cir_mk_ev     = DataCon -> [Type] -> [EvExpr] -> EvTerm
evDataConApp DataCon
heqDataCon [Type]
args
                    , cir_what :: InstanceWhat
cir_what      = InstanceWhat
BuiltinEqInstance })

matchHomoEquality :: [Type] -> TcM ClsInstResult
-- Solves (t1 ~ t2)
matchHomoEquality :: [Type] -> TcM ClsInstResult
matchHomoEquality args :: [Type]
args@[Type
k,Type
t1,Type
t2]
  = ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (OneInst { cir_new_theta :: [Type]
cir_new_theta = [ TyCon -> [Type] -> Type
mkTyConApp TyCon
eqPrimTyCon [Type
k,Type
k,Type
t1,Type
t2] ]
                    , cir_mk_ev :: [EvExpr] -> EvTerm
cir_mk_ev     = DataCon -> [Type] -> [EvExpr] -> EvTerm
evDataConApp DataCon
eqDataCon [Type]
args
                    , cir_what :: InstanceWhat
cir_what      = InstanceWhat
BuiltinEqInstance })
matchHomoEquality [Type]
args = String -> SDoc -> TcM ClsInstResult
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"matchHomoEquality" ([Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
args)

-- See also Note [The equality types story] in GHC.Builtin.Types.Prim
matchCoercible :: [Type] -> TcM ClsInstResult
matchCoercible :: [Type] -> TcM ClsInstResult
matchCoercible args :: [Type]
args@[Type
k, Type
t1, Type
t2]
  = ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (OneInst { cir_new_theta :: [Type]
cir_new_theta = [ TyCon -> [Type] -> Type
mkTyConApp TyCon
eqReprPrimTyCon [Type]
args' ]
                    , cir_mk_ev :: [EvExpr] -> EvTerm
cir_mk_ev     = DataCon -> [Type] -> [EvExpr] -> EvTerm
evDataConApp DataCon
coercibleDataCon [Type]
args
                    , cir_what :: InstanceWhat
cir_what      = InstanceWhat
BuiltinEqInstance })
  where
    args' :: [Type]
args' = [Type
k, Type
k, Type
t1, Type
t2]
matchCoercible [Type]
args = String -> SDoc -> TcM ClsInstResult
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"matchLiftedCoercible" ([Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
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.


Note [Unused name reporting and HasField]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When a HasField constraint is solved by the type-checker, we must record a use
of the corresponding field name, as otherwise it might be reported as unused.
See #19213.  We need to call keepAlive to add the name to the tcg_keep set,
which accumulates names used by the constraint solver, as described by
Note [Tracking unused binding and imports] in GHC.Tc.Types.

We need to call addUsedGRE as well because there may be a deprecation warning on
the field, which will be reported by addUsedGRE.  But calling addUsedGRE without
keepAlive is not enough, because the field might be defined locally, and
addUsedGRE extends tcg_used_gres with imported GREs only.
-}

-- See Note [HasField instances]
matchHasField :: DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchHasField :: DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchHasField DynFlags
dflags Bool
short_cut Class
clas [Type]
tys
  = do { FamInstEnvs
fam_inst_envs <- TcM FamInstEnvs
tcGetFamInstEnvs
       ; GlobalRdrEnv
rdr_env       <- TcRn GlobalRdrEnv
getGlobalRdrEnv
       ; case [Type]
tys of
           -- We are matching HasField {k} x r a...
           [Type
_k_ty, Type
x_ty, Type
r_ty, Type
a_ty]
               -- x should be a literal string
             | Just FastString
x <- Type -> Maybe FastString
isStrLitTy Type
x_ty
               -- r should be an applied type constructor
             , Just (TyCon
tc, [Type]
args) <- HasCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
r_ty
               -- use representation tycon (if data family); it has the fields
             , let r_tc :: TyCon
r_tc = (TyCon, [Type], TcCoercion) -> TyCon
forall a b c. (a, b, c) -> a
fstOf3 (FamInstEnvs -> TyCon -> [Type] -> (TyCon, [Type], TcCoercion)
tcLookupDataFamInst FamInstEnvs
fam_inst_envs TyCon
tc [Type]
args)
               -- x should be a field of r
             , Just FieldLabel
fl <- FastString -> TyCon -> Maybe FieldLabel
lookupTyConFieldLabel FastString
x TyCon
r_tc
               -- the field selector should be in scope
             , Just GlobalRdrElt
gre <- GlobalRdrEnv -> FieldLabel -> Maybe GlobalRdrElt
lookupGRE_FieldLabel GlobalRdrEnv
rdr_env FieldLabel
fl

             -> do { DFunId
sel_id <- Name -> IOEnv (Env TcGblEnv TcLclEnv) DFunId
tcLookupId (FieldLabel -> Name
flSelector FieldLabel
fl)
                   ; ([(Name, DFunId)]
tv_prs, [Type]
preds, Type
sel_ty) <- ([DFunId] -> TcM (TCvSubst, [DFunId]))
-> DFunId -> TcM ([(Name, DFunId)], [Type], Type)
tcInstType [DFunId] -> TcM (TCvSubst, [DFunId])
newMetaTyVars DFunId
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 :: [Type]
theta = Type -> Type -> Type
mkPrimEqPred Type
sel_ty (Type -> Type -> Type
mkVisFunTyMany Type
r_ty Type
a_ty) Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
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 :: [EvExpr] -> EvTerm
mk_ev (EvExpr
ev1:[EvExpr]
evs) = DFunId -> [Type] -> [EvExpr] -> EvExpr
evSelector DFunId
sel_id [Type]
tvs [EvExpr]
evs EvExpr -> TcCoercion -> EvTerm
`evCast` TcCoercion
co
                           where
                             co :: TcCoercion
co = (() :: Constraint) => TcCoercion -> TcCoercion
TcCoercion -> TcCoercion
mkTcSubCo (EvTerm -> TcCoercion
evTermCoercion (EvExpr -> EvTerm
EvExpr EvExpr
ev1))
                                      TcCoercion -> TcCoercion -> TcCoercion
`mkTcTransCo` TcCoercion -> TcCoercion
mkTcSymCo TcCoercion
co2
                         mk_ev [] = String -> EvTerm
forall a. String -> a
panic String
"matchHasField.mk_ev"

                         Just (Type
_, TcCoercion
co2) = TyCon -> [Type] -> Maybe (Type, TcCoercion)
tcInstNewTyCon_maybe (Class -> TyCon
classTyCon Class
clas)
                                                              [Type]
tys

                         tvs :: [Type]
tvs = [DFunId] -> [Type]
mkTyVarTys (((Name, DFunId) -> DFunId) -> [(Name, DFunId)] -> [DFunId]
forall a b. (a -> b) -> [a] -> [b]
map (Name, DFunId) -> DFunId
forall a b. (a, b) -> b
snd [(Name, DFunId)]
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 Bool -> Bool
not (DFunId -> Bool
isNaughtyRecordSelector DFunId
sel_id) Bool -> Bool -> Bool
&& Type -> Bool
isTauTy Type
sel_ty
                     then do { -- See Note [Unused name reporting and HasField]
                               Bool -> GlobalRdrElt -> TcRn ()
addUsedGRE Bool
True GlobalRdrElt
gre
                             ; Name -> TcRn ()
keepAlive (GlobalRdrElt -> Name
greMangledName GlobalRdrElt
gre)
                             ; ClsInstResult -> TcM ClsInstResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return OneInst { cir_new_theta :: [Type]
cir_new_theta = [Type]
theta
                                              , cir_mk_ev :: [EvExpr] -> EvTerm
cir_mk_ev     = [EvExpr] -> EvTerm
mk_ev
                                              , cir_what :: InstanceWhat
cir_what      = InstanceWhat
BuiltinInstance } }
                     else DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchInstEnv DynFlags
dflags Bool
short_cut Class
clas [Type]
tys }

           [Type]
_ -> DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
matchInstEnv DynFlags
dflags Bool
short_cut Class
clas [Type]
tys }