{-

Describes predicates as they are considered by the solver.

-}

module 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,

  -- Implicit parameters
  isIPPred, isIPPred_maybe, isIPTyCon, isIPClass, hasIPPred,

  -- Evidence variables
  DictId, isEvVar, isDictId
  ) where

import GhcPrelude

import Type
import Class
import TyCon
import Var
import Coercion

import PrelNames

import FastString
import Outputable
import Util

import Control.Monad ( guard )

-- | 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 [TyCoVarBinder] [PredType] PredType
     -- ForAllPred: see Note [Quantified constraints] in TcCanonical
  -- 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])
_ | ([TyCoVarBinder]
tvs, PredType
rho) <- PredType -> ([TyCoVarBinder], PredType)
splitForAllVarBndrs PredType
ev_ty
      , ([PredType]
theta, PredType
pred) <- PredType -> ([PredType], PredType)
splitFunTys PredType
rho
      , Bool -> Bool
not ([TyCoVarBinder] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyCoVarBinder]
tvs Bool -> Bool -> Bool
&& [PredType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PredType]
theta)
      -> [TyCoVarBinder] -> [PredType] -> PredType -> Pred
ForAllPred [TyCoVarBinder]
tvs [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 :: 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

-- --------------------- 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
$cp1Ord :: Eq EqRel
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 TcCanonical.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 TcCanonical.
-}

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 TyCoRep
-- 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, isIPPred :: 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)

isIPPred :: PredType -> Bool
isIPPred PredType
ty = case PredType -> Maybe TyCon
tyConAppTyCon_maybe PredType
ty of
    Just TyCon
tc -> TyCon -> Bool
isIPTyCon TyCon
tc
    Maybe TyCon
_       -> Bool
False

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

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

isIPPred_maybe :: Type -> Maybe (FastString, Type)
isIPPred_maybe :: PredType -> Maybe (FastString, PredType)
isIPPred_maybe PredType
ty =
  do (TyCon
tc,[PredType
t1,PredType
t2]) <- HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty
     Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (TyCon -> Bool
isIPTyCon TyCon
tc)
     FastString
x <- PredType -> Maybe FastString
isStrLitTy PredType
t1
     (FastString, PredType) -> Maybe (FastString, PredType)
forall (m :: * -> *) a. Monad m => a -> m a
return (FastString
x,PredType
t2)

hasIPPred :: PredType -> Bool
hasIPPred :: PredType -> Bool
hasIPPred PredType
pred
  = case PredType -> Pred
classifyPredType PredType
pred of
      ClassPred Class
cls [PredType]
tys
        | Class -> Bool
isIPClass     Class
cls -> Bool
True
        | Class -> Bool
isCTupleClass Class
cls -> (PredType -> Bool) -> [PredType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any PredType -> Bool
hasIPPred [PredType]
tys
      Pred
_other -> Bool
False

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

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

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