{-

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 ev_ty :: PredType
ev_ty = case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ev_ty of
    Just (tc :: TyCon
tc, [_, _, ty1 :: PredType
ty1, ty2 :: 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 (tc :: TyCon
tc, tys :: [PredType]
tys)
      | Just clas :: Class
clas <- TyCon -> Maybe Class
tyConClass_maybe TyCon
tc
      -> Class -> [PredType] -> Pred
ClassPred Class
clas [PredType]
tys

    _ | (tvs :: [TyCoVarBinder]
tvs, rho :: PredType
rho) <- PredType -> ([TyCoVarBinder], PredType)
splitForAllVarBndrs PredType
ev_ty
      , (theta :: [PredType]
theta, pred :: 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 clas :: Class
clas tys :: [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 ty :: PredType
ty = case PredType -> Maybe (Class, [PredType])
getClassPredTys_maybe PredType
ty of
        Just (clas :: Class
clas, tys :: [PredType]
tys) -> (Class
clas, [PredType]
tys)
        Nothing          -> String -> SDoc -> (Class, [PredType])
forall a. HasCallStack => String -> SDoc -> a
pprPanic "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 ty :: PredType
ty = case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty of
        Just (tc :: TyCon
tc, tys :: [PredType]
tys) | Just clas :: 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 (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 NomEq  = String -> SDoc
text "nominal equality"
  ppr ReprEq = String -> SDoc
text "representational equality"

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

getEqPredTys :: PredType -> (Type, Type)
getEqPredTys :: PredType -> (PredType, PredType)
getEqPredTys ty :: PredType
ty
  = case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty of
      Just (tc :: TyCon
tc, [_, _, ty1 :: PredType
ty1, ty2 :: 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)
      _ -> String -> SDoc -> (PredType, PredType)
forall a. HasCallStack => String -> SDoc -> a
pprPanic "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 ty :: PredType
ty
  = case HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty of
      Just (tc :: TyCon
tc, [_, _, ty1 :: PredType
ty1, ty2 :: 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 (Role, PredType, PredType)
forall a. Maybe a
Nothing

getEqPredRole :: PredType -> Role
getEqPredRole :: PredType -> Role
getEqPredRole ty :: 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 ty :: PredType
ty
  | Just (tc :: TyCon
tc, _) <- 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 ty :: 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 cls :: 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 ty :: PredType
ty = case PredType -> Maybe TyCon
tyConAppTyCon_maybe PredType
ty of
    Just tyCon :: TyCon
tyCon | TyCon -> Bool
isClassTyCon TyCon
tyCon -> Bool
True
    _                               -> Bool
False

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

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

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

isIPTyCon :: TyCon -> Bool
isIPTyCon :: TyCon -> Bool
isIPTyCon tc :: 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 cls :: Class
cls = Class
cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
ipClassKey

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

isIPPred_maybe :: Type -> Maybe (FastString, Type)
isIPPred_maybe :: PredType -> Maybe (FastString, PredType)
isIPPred_maybe ty :: PredType
ty =
  do (tc :: TyCon
tc,[t1 :: PredType
t1,t2 :: 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 pred :: PredType
pred
  = case PredType -> Pred
classifyPredType PredType
pred of
      ClassPred cls :: Class
cls tys :: [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
      _other :: Pred
_other -> Bool
False

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

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

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