{-

Describes predicates as they are considered by the solver.

-}

module GHC.Core.Predicate (
  Pred(..), classifyPredType,
  isPredTy, isEvVarType,

  -- Equality predicates
  EqRel(..), eqRelRole,
  isEqPrimPred, isEqPred,
  getEqPredTys, getEqPredTys_maybe, getEqPredRole,
  predTypeEqRel,
  mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
  mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,

  -- Class predicates
  mkClassPred, isDictTy,
  isClassPred, isEqPredClass, isCTupleClass,
  getClassPredTys, getClassPredTys_maybe,
  classMethodTy, classMethodInstTy,

  -- Implicit parameters
  isIPLikePred, hasIPSuperClasses, isIPTyCon, isIPClass,

  -- Evidence variables
  DictId, isEvVar, isDictId
  ) where

import GHC.Prelude

import GHC.Core.Type
import GHC.Core.Class
import GHC.Core.TyCon
import GHC.Core.TyCon.RecWalk
import GHC.Types.Var
import GHC.Core.Coercion
import GHC.Core.Multiplicity ( scaledThing )

import GHC.Builtin.Names

import GHC.Utils.Outputable
import GHC.Utils.Misc
import GHC.Utils.Panic


-- | A predicate in the solver. The solver tries to prove Wanted predicates
-- from Given ones.
data Pred
  = ClassPred Class [Type]
  | EqPred EqRel Type Type
  | IrredPred PredType
  | ForAllPred [TyVar] [PredType] PredType
     -- ForAllPred: see Note [Quantified constraints] in GHC.Tc.Solver.Canonical
  -- NB: There is no TuplePred case
  --     Tuple predicates like (Eq a, Ord b) are just treated
  --     as ClassPred, as if we had a tuple class with two superclasses
  --        class (c1, c2) => (%,%) c1 c2

classifyPredType :: PredType -> Pred
classifyPredType :: PredType -> Pred
classifyPredType PredType
ev_ty = case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ev_ty of
    Just (TyCon
tc, [PredType
_, PredType
_, PredType
ty1, PredType
ty2])
      | TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqReprPrimTyConKey -> EqRel -> PredType -> PredType -> Pred
EqPred EqRel
ReprEq PredType
ty1 PredType
ty2
      | TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqPrimTyConKey     -> EqRel -> PredType -> PredType -> Pred
EqPred EqRel
NomEq PredType
ty1 PredType
ty2

    Just (TyCon
tc, [PredType]
tys)
      | Just Class
clas <- TyCon -> Maybe Class
tyConClass_maybe TyCon
tc
      -> Class -> [PredType] -> Pred
ClassPred Class
clas [PredType]
tys

    Maybe (TyCon, [PredType])
_ | ([TyCoVar]
tvs, PredType
rho) <- PredType -> ([TyCoVar], PredType)
splitForAllTyCoVars PredType
ev_ty
      , ([Scaled PredType]
theta, PredType
pred) <- PredType -> ([Scaled PredType], PredType)
splitFunTys PredType
rho
      , Bool -> Bool
not ([TyCoVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyCoVar]
tvs Bool -> Bool -> Bool
&& [Scaled PredType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Scaled PredType]
theta)
      -> [TyCoVar] -> [PredType] -> PredType -> Pred
ForAllPred [TyCoVar]
tvs ((Scaled PredType -> PredType) -> [Scaled PredType] -> [PredType]
forall a b. (a -> b) -> [a] -> [b]
map Scaled PredType -> PredType
forall a. Scaled a -> a
scaledThing [Scaled PredType]
theta) PredType
pred

      | Bool
otherwise
      -> PredType -> Pred
IrredPred PredType
ev_ty

-- --------------------- Dictionary types ---------------------------------

mkClassPred :: Class -> [Type] -> PredType
mkClassPred :: Class -> [PredType] -> PredType
mkClassPred Class
clas [PredType]
tys = TyCon -> [PredType] -> PredType
mkTyConApp (Class -> TyCon
classTyCon Class
clas) [PredType]
tys

isDictTy :: Type -> Bool
isDictTy :: PredType -> Bool
isDictTy = PredType -> Bool
isClassPred

getClassPredTys :: HasDebugCallStack => PredType -> (Class, [Type])
getClassPredTys :: HasDebugCallStack => PredType -> (Class, [PredType])
getClassPredTys PredType
ty = case PredType -> Maybe (Class, [PredType])
getClassPredTys_maybe PredType
ty of
        Just (Class
clas, [PredType]
tys) -> (Class
clas, [PredType]
tys)
        Maybe (Class, [PredType])
Nothing          -> String -> SDoc -> (Class, [PredType])
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"getClassPredTys" (PredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr PredType
ty)

getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
getClassPredTys_maybe :: PredType -> Maybe (Class, [PredType])
getClassPredTys_maybe PredType
ty = case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty of
        Just (TyCon
tc, [PredType]
tys) | Just Class
clas <- TyCon -> Maybe Class
tyConClass_maybe TyCon
tc -> (Class, [PredType]) -> Maybe (Class, [PredType])
forall a. a -> Maybe a
Just (Class
clas, [PredType]
tys)
        Maybe (TyCon, [PredType])
_ -> Maybe (Class, [PredType])
forall a. Maybe a
Nothing

classMethodTy :: Id -> Type
-- Takes a class selector op :: forall a. C a => meth_ty
-- and returns the type of its method, meth_ty
-- The selector can be a superclass selector, in which case
-- you get back a superclass
classMethodTy :: TyCoVar -> PredType
classMethodTy TyCoVar
sel_id
  = PredType -> PredType
funResultTy (PredType -> PredType) -> PredType -> PredType
forall a b. (a -> b) -> a -> b
$        -- meth_ty
    PredType -> PredType
dropForAlls (PredType -> PredType) -> PredType -> PredType
forall a b. (a -> b) -> a -> b
$        -- C a => meth_ty
    TyCoVar -> PredType
varType TyCoVar
sel_id        -- forall a. C n => meth_ty

classMethodInstTy :: Id -> [Type] -> Type
-- Takes a class selector op :: forall a b. C a b => meth_ty
-- and the types [ty1, ty2] at which it is instantiated,
-- returns the instantiated type of its method, meth_ty[t1/a,t2/b]
-- The selector can be a superclass selector, in which case
-- you get back a superclass
classMethodInstTy :: TyCoVar -> [PredType] -> PredType
classMethodInstTy TyCoVar
sel_id [PredType]
arg_tys
  = PredType -> PredType
funResultTy (PredType -> PredType) -> PredType -> PredType
forall a b. (a -> b) -> a -> b
$
    HasDebugCallStack => PredType -> [PredType] -> PredType
PredType -> [PredType] -> PredType
piResultTys (TyCoVar -> PredType
varType TyCoVar
sel_id) [PredType]
arg_tys

-- --------------------- Equality predicates ---------------------------------

-- | A choice of equality relation. This is separate from the type 'Role'
-- because 'Phantom' does not define a (non-trivial) equality relation.
data EqRel = NomEq | ReprEq
  deriving (EqRel -> EqRel -> Bool
(EqRel -> EqRel -> Bool) -> (EqRel -> EqRel -> Bool) -> Eq EqRel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EqRel -> EqRel -> Bool
$c/= :: EqRel -> EqRel -> Bool
== :: EqRel -> EqRel -> Bool
$c== :: EqRel -> EqRel -> Bool
Eq, Eq EqRel
Eq EqRel
-> (EqRel -> EqRel -> Ordering)
-> (EqRel -> EqRel -> Bool)
-> (EqRel -> EqRel -> Bool)
-> (EqRel -> EqRel -> Bool)
-> (EqRel -> EqRel -> Bool)
-> (EqRel -> EqRel -> EqRel)
-> (EqRel -> EqRel -> EqRel)
-> Ord EqRel
EqRel -> EqRel -> Bool
EqRel -> EqRel -> Ordering
EqRel -> EqRel -> EqRel
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: EqRel -> EqRel -> EqRel
$cmin :: EqRel -> EqRel -> EqRel
max :: EqRel -> EqRel -> EqRel
$cmax :: EqRel -> EqRel -> EqRel
>= :: EqRel -> EqRel -> Bool
$c>= :: EqRel -> EqRel -> Bool
> :: EqRel -> EqRel -> Bool
$c> :: EqRel -> EqRel -> Bool
<= :: EqRel -> EqRel -> Bool
$c<= :: EqRel -> EqRel -> Bool
< :: EqRel -> EqRel -> Bool
$c< :: EqRel -> EqRel -> Bool
compare :: EqRel -> EqRel -> Ordering
$ccompare :: EqRel -> EqRel -> Ordering
Ord)

instance Outputable EqRel where
  ppr :: EqRel -> SDoc
ppr EqRel
NomEq  = String -> SDoc
text String
"nominal equality"
  ppr EqRel
ReprEq = String -> SDoc
text String
"representational equality"

eqRelRole :: EqRel -> Role
eqRelRole :: EqRel -> Role
eqRelRole EqRel
NomEq  = Role
Nominal
eqRelRole EqRel
ReprEq = Role
Representational

getEqPredTys :: PredType -> (Type, Type)
getEqPredTys :: PredType -> (PredType, PredType)
getEqPredTys PredType
ty
  = case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty of
      Just (TyCon
tc, [PredType
_, PredType
_, PredType
ty1, PredType
ty2])
        |  TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqPrimTyConKey
        Bool -> Bool -> Bool
|| TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqReprPrimTyConKey
        -> (PredType
ty1, PredType
ty2)
      Maybe (TyCon, [PredType])
_ -> String -> SDoc -> (PredType, PredType)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"getEqPredTys" (PredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr PredType
ty)

getEqPredTys_maybe :: PredType -> Maybe (Role, Type, Type)
getEqPredTys_maybe :: PredType -> Maybe (Role, PredType, PredType)
getEqPredTys_maybe PredType
ty
  = case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty of
      Just (TyCon
tc, [PredType
_, PredType
_, PredType
ty1, PredType
ty2])
        | TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqPrimTyConKey     -> (Role, PredType, PredType) -> Maybe (Role, PredType, PredType)
forall a. a -> Maybe a
Just (Role
Nominal, PredType
ty1, PredType
ty2)
        | TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqReprPrimTyConKey -> (Role, PredType, PredType) -> Maybe (Role, PredType, PredType)
forall a. a -> Maybe a
Just (Role
Representational, PredType
ty1, PredType
ty2)
      Maybe (TyCon, [PredType])
_ -> Maybe (Role, PredType, PredType)
forall a. Maybe a
Nothing

getEqPredRole :: PredType -> Role
getEqPredRole :: PredType -> Role
getEqPredRole PredType
ty = EqRel -> Role
eqRelRole (PredType -> EqRel
predTypeEqRel PredType
ty)

-- | Get the equality relation relevant for a pred type.
predTypeEqRel :: PredType -> EqRel
predTypeEqRel :: PredType -> EqRel
predTypeEqRel PredType
ty
  | Just (TyCon
tc, [PredType]
_) <- HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty
  , TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqReprPrimTyConKey
  = EqRel
ReprEq
  | Bool
otherwise
  = EqRel
NomEq

{-------------------------------------------
Predicates on PredType
--------------------------------------------}

{-
Note [Evidence for quantified constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The superclass mechanism in GHC.Tc.Solver.Canonical.makeSuperClasses risks
taking a quantified constraint like
   (forall a. C a => a ~ b)
and generate superclass evidence
   (forall a. C a => a ~# b)

This is a funny thing: neither isPredTy nor isCoVarType are true
of it.  So we are careful not to generate it in the first place:
see Note [Equality superclasses in quantified constraints]
in GHC.Tc.Solver.Canonical.
-}

isEvVarType :: Type -> Bool
-- True of (a) predicates, of kind Constraint, such as (Eq a), and (a ~ b)
--         (b) coercion types, such as (t1 ~# t2) or (t1 ~R# t2)
-- See Note [Types for coercions, predicates, and evidence] in GHC.Core.TyCo.Rep
-- See Note [Evidence for quantified constraints]
isEvVarType :: PredType -> Bool
isEvVarType PredType
ty = PredType -> Bool
isCoVarType PredType
ty Bool -> Bool -> Bool
|| HasDebugCallStack => PredType -> Bool
PredType -> Bool
isPredTy PredType
ty

isEqPredClass :: Class -> Bool
-- True of (~) and (~~)
isEqPredClass :: Class -> Bool
isEqPredClass Class
cls =  Class
cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqTyConKey
                  Bool -> Bool -> Bool
|| Class
cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
heqTyConKey

isClassPred, isEqPred, isEqPrimPred :: PredType -> Bool
isClassPred :: PredType -> Bool
isClassPred PredType
ty = case PredType -> Maybe TyCon
tyConAppTyCon_maybe PredType
ty of
    Just TyCon
tyCon | TyCon -> Bool
isClassTyCon TyCon
tyCon -> Bool
True
    Maybe TyCon
_                               -> Bool
False

isEqPred :: PredType -> Bool
isEqPred PredType
ty  -- True of (a ~ b) and (a ~~ b)
             -- ToDo: should we check saturation?
  | Just TyCon
tc <- PredType -> Maybe TyCon
tyConAppTyCon_maybe PredType
ty
  , Just Class
cls <- TyCon -> Maybe Class
tyConClass_maybe TyCon
tc
  = Class -> Bool
isEqPredClass Class
cls
  | Bool
otherwise
  = Bool
False

isEqPrimPred :: PredType -> Bool
isEqPrimPred PredType
ty = PredType -> Bool
isCoVarType PredType
ty
  -- True of (a ~# b) (a ~R# b)

isCTupleClass :: Class -> Bool
isCTupleClass :: Class -> Bool
isCTupleClass Class
cls = TyCon -> Bool
isTupleTyCon (Class -> TyCon
classTyCon Class
cls)


{- *********************************************************************
*                                                                      *
              Implicit parameters
*                                                                      *
********************************************************************* -}

isIPTyCon :: TyCon -> Bool
isIPTyCon :: TyCon -> Bool
isIPTyCon TyCon
tc = TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
ipClassKey
  -- Class and its corresponding TyCon have the same Unique

isIPClass :: Class -> Bool
isIPClass :: Class -> Bool
isIPClass Class
cls = Class
cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
ipClassKey

isIPLikePred :: Type -> Bool
-- See Note [Local implicit parameters]
isIPLikePred :: PredType -> Bool
isIPLikePred = RecTcChecker -> PredType -> Bool
is_ip_like_pred RecTcChecker
initIPRecTc


is_ip_like_pred :: RecTcChecker -> Type -> Bool
is_ip_like_pred :: RecTcChecker -> PredType -> Bool
is_ip_like_pred RecTcChecker
rec_clss PredType
ty
  | Just (TyCon
tc, [PredType]
tys) <- HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty
  , Just RecTcChecker
rec_clss' <- if TyCon -> Bool
isTupleTyCon TyCon
tc  -- Tuples never cause recursion
                      then RecTcChecker -> Maybe RecTcChecker
forall a. a -> Maybe a
Just RecTcChecker
rec_clss
                      else RecTcChecker -> TyCon -> Maybe RecTcChecker
checkRecTc RecTcChecker
rec_clss TyCon
tc
  , Just Class
cls       <- TyCon -> Maybe Class
tyConClass_maybe TyCon
tc
  = Class -> Bool
isIPClass Class
cls Bool -> Bool -> Bool
|| RecTcChecker -> Class -> [PredType] -> Bool
has_ip_super_classes RecTcChecker
rec_clss' Class
cls [PredType]
tys

  | Bool
otherwise
  = Bool
False -- Includes things like (D []) where D is
          -- a Constraint-ranged family; #7785

hasIPSuperClasses :: Class -> [Type] -> Bool
-- See Note [Local implicit parameters]
hasIPSuperClasses :: Class -> [PredType] -> Bool
hasIPSuperClasses = RecTcChecker -> Class -> [PredType] -> Bool
has_ip_super_classes RecTcChecker
initIPRecTc

has_ip_super_classes :: RecTcChecker -> Class -> [Type] -> Bool
has_ip_super_classes :: RecTcChecker -> Class -> [PredType] -> Bool
has_ip_super_classes RecTcChecker
rec_clss Class
cls [PredType]
tys
  = (TyCoVar -> Bool) -> [TyCoVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TyCoVar -> Bool
ip_ish (Class -> [TyCoVar]
classSCSelIds Class
cls)
  where
    -- Check that the type of a superclass determines its value
    -- sc_sel_id :: forall a b. C a b -> <superclass type>
    ip_ish :: TyCoVar -> Bool
ip_ish TyCoVar
sc_sel_id = RecTcChecker -> PredType -> Bool
is_ip_like_pred RecTcChecker
rec_clss (PredType -> Bool) -> PredType -> Bool
forall a b. (a -> b) -> a -> b
$
                       TyCoVar -> [PredType] -> PredType
classMethodInstTy TyCoVar
sc_sel_id [PredType]
tys

initIPRecTc :: RecTcChecker
initIPRecTc :: RecTcChecker
initIPRecTc = Int -> RecTcChecker -> RecTcChecker
setRecTcMaxBound Int
1 RecTcChecker
initRecTc

{- Note [Local implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The function isIPLikePred tells if this predicate, or any of its
superclasses, is an implicit parameter.

Why are implicit parameters special?  Unlike normal classes, we can
have local instances for implicit parameters, in the form of
   let ?x = True in ...
So in various places we must be careful not to assume that any value
of the right type will do; we must carefully look for the innermost binding.
So isIPLikePred checks whether this is an implicit parameter, or has
a superclass that is an implicit parameter.

Several wrinkles

* We must be careful with superclasses, as #18649 showed.  Haskell
  doesn't allow an implicit parameter as a superclass
    class (?x::a) => C a where ...
  but with a constraint tuple we might have
     (% Eq a, ?x::Int %)
  and /its/ superclasses, namely (Eq a) and (?x::Int), /do/ include an
  implicit parameter.

  With ConstraintKinds this can apply to /any/ class, e.g.
     class sc => C sc where ...
  Then (C (?x::Int)) has (?x::Int) as a superclass.  So we must
  instantiate and check each superclass, one by one, in
  hasIPSuperClasses.

* With -XRecursiveSuperClasses, the superclass hunt can go on forever,
  so we need a RecTcChecker to cut it off.

* Another apparent additional complexity involves type families. For
  example, consider
         type family D (v::*->*) :: Constraint
         type instance D [] = ()
         f :: D v => v Char -> Int
  If we see a call (f "foo"), we'll pass a "dictionary"
    () |> (g :: () ~ D [])
  and it's good to specialise f at this dictionary.

So the question is: can an implicit parameter "hide inside" a
type-family constraint like (D a).  Well, no.  We don't allow
        type instance D Maybe = ?x:Int
Hence the umbrella 'otherwise' case in is_ip_like_pred.  See #7785.

Small worries (Sept 20):
* I don't see what stops us having that 'type instance'. Indeed I
  think nothing does.
* I'm a little concerned about type variables; such a variable might
  be instantiated to an implicit parameter.  I don't think this
  matters in the cases for which isIPLikePred is used, and it's pretty
  obscure anyway.
* The superclass hunt stops when it encounters the same class again,
  but in principle we could have the same class, differently instantiated,
  and the second time it could have an implicit parameter
I'm going to treat these as problems for another day. They are all exotic.  -}

{- *********************************************************************
*                                                                      *
              Evidence variables
*                                                                      *
********************************************************************* -}

isEvVar :: Var -> Bool
isEvVar :: TyCoVar -> Bool
isEvVar TyCoVar
var = PredType -> Bool
isEvVarType (TyCoVar -> PredType
varType TyCoVar
var)

isDictId :: Id -> Bool
isDictId :: TyCoVar -> Bool
isDictId TyCoVar
id = PredType -> Bool
isDictTy (TyCoVar -> PredType
varType TyCoVar
id)