{-# LANGUAGE DerivingStrategies #-}

{-

Describes predicates as they are considered by the solver.

-}

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

  -- Equality predicates
  EqRel(..), eqRelRole,
  isEqPred, isReprEqPred, isEqClassPred, isCoVarType,
  getEqPredTys, getEqPredTys_maybe, getEqPredRole,
  predTypeEqRel,
  mkNomEqPred, mkReprEqPred, mkEqPred, mkEqPredRole,

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

  -- Implicit parameters
  isIPLikePred, mentionsIP, isIPTyCon, isIPClass,
  isCallStackTy, isCallStackPred, isCallStackPredTy,
  isExceptionContextPred, isExceptionContextTy,
  isIPPred_maybe,

  -- Evidence variables
  DictId, isEvVar, isDictId,

  -- * Well-scoped free variables
  scopedSort, tyCoVarsOfTypeWellScoped,
  tyCoVarsOfTypesWellScoped,

  -- Equality left-hand sides
  CanEqLHS(..), canEqLHS_maybe, canTyFamEqLHS_maybe,
  canEqLHSKind, canEqLHSType, eqCanEqLHS

  ) where

import GHC.Prelude

import GHC.Core.Type
import GHC.Core.Class
import GHC.Core.TyCo.Compare( tcEqTyConApps )
import GHC.Core.TyCo.FVs( tyCoVarsOfTypeList, tyCoVarsOfTypesList )
import GHC.Core.TyCon
import GHC.Core.TyCon.RecWalk
import GHC.Types.Var
import GHC.Types.Var.Set
import GHC.Core.Multiplicity ( scaledThing )

import GHC.Builtin.Names
import GHC.Builtin.Types.Prim( eqPrimTyCon, eqReprPrimTyCon )

import GHC.Utils.Outputable
import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Data.FastString


{- *********************************************************************
*                                                                      *
*                   Pred and PredType                                  *
*                                                                      *
********************************************************************* -}

-- | A predicate in the solver. The solver tries to prove Wanted predicates
-- from Given ones.
data Pred

  -- | A typeclass predicate.
  = ClassPred Class [Type]

  -- | A type equality predicate, (t1 ~#N t2) or (t1 ~#R t2)
  | EqPred EqRel Type Type

  -- | An irreducible predicate.
  | IrredPred PredType

  -- | A quantified predicate.
  --
  -- See Note [Quantified constraints] in GHC.Tc.Solver.Solve
  | ForAllPred [TyVar] [PredType] PredType

  -- 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) => CTuple2 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])
_ | ([TyVar]
tvs, PredType
rho) <- PredType -> ([TyVar], PredType)
splitForAllTyCoVars PredType
ev_ty
      , ([Scaled PredType]
theta, PredType
pred) <- PredType -> ([Scaled PredType], PredType)
splitFunTys PredType
rho
      , Bool -> Bool
not ([TyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVar]
tvs Bool -> Bool -> Bool
&& [Scaled PredType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Scaled PredType]
theta)
      -> [TyVar] -> [PredType] -> PredType -> Pred
ForAllPred [TyVar]
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
-- True of dictionaries (Eq a) and
--         dictionary functions (forall a. Eq a => Eq [a])
-- See Note [Type determines value]
-- See #24370 (and the isDictId call in GHC.HsToCore.Binds.decomposeRuleLhs)
--     for why it's important to catch dictionary bindings
isDictTy :: PredType -> Bool
isDictTy PredType
ty = PredType -> Bool
isClassPred PredType
pred
  where
    ([PiTyBinder]
_, PredType
pred) = PredType -> ([PiTyBinder], PredType)
splitInvisPiTys PredType
ty

typeDeterminesValue :: Type -> Bool
-- See Note [Type determines value]
typeDeterminesValue :: PredType -> Bool
typeDeterminesValue PredType
ty = PredType -> Bool
isDictTy PredType
ty Bool -> Bool -> Bool
&& Bool -> Bool
not (PredType -> Bool
isIPLikePred PredType
ty)

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 :: TyVar -> PredType
classMethodTy TyVar
sel_id
  = HasDebugCallStack => PredType -> PredType
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
    TyVar -> PredType
varType TyVar
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 :: TyVar -> [PredType] -> PredType
classMethodInstTy TyVar
sel_id [PredType]
arg_tys
  = HasDebugCallStack => PredType -> PredType
PredType -> PredType
funResultTy (PredType -> PredType) -> PredType -> PredType
forall a b. (a -> b) -> a -> b
$
    HasDebugCallStack => PredType -> [PredType] -> PredType
PredType -> [PredType] -> PredType
piResultTys (TyVar -> PredType
varType TyVar
sel_id) [PredType]
arg_tys

{- Note [Type determines value]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Only specialise on non-impicit-parameter predicates, because these
are the ones whose *type* determines their *value*.  In particular,
with implicit params, the type args *don't* say what the value of the
implicit param is!  See #7101.

So we treat implicit params just like ordinary arguments for the
purposes of specialisation.  Note that we still want to specialise
functions with implicit params if they have *other* dicts which are
class params; see #17930.
-}

-- --------------------- 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
$c== :: EqRel -> EqRel -> Bool
== :: EqRel -> EqRel -> Bool
$c/= :: EqRel -> EqRel -> Bool
/= :: 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
$ccompare :: EqRel -> EqRel -> Ordering
compare :: EqRel -> EqRel -> Ordering
$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
>= :: EqRel -> EqRel -> Bool
$cmax :: EqRel -> EqRel -> EqRel
max :: EqRel -> EqRel -> EqRel
$cmin :: EqRel -> EqRel -> EqRel
min :: EqRel -> EqRel -> EqRel
Ord)

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

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

-- | Creates a primitive nominal type equality predicate.
--      t1 ~# t2
-- Invariant: the types are not Coercions
mkNomEqPred :: Type -> Type -> Type
mkNomEqPred :: PredType -> PredType -> PredType
mkNomEqPred PredType
ty1 PredType
ty2
  = TyCon -> [PredType] -> PredType
mkTyConApp TyCon
eqPrimTyCon [PredType
k1, PredType
k2, PredType
ty1, PredType
ty2]
  where
    k1 :: PredType
k1 = HasDebugCallStack => PredType -> PredType
PredType -> PredType
typeKind PredType
ty1
    k2 :: PredType
k2 = HasDebugCallStack => PredType -> PredType
PredType -> PredType
typeKind PredType
ty2

-- | Creates a primitive representational type equality predicate.
--      t1 ~R# t2
-- Invariant: the types are not Coercions
mkReprEqPred :: Type -> Type -> Type
mkReprEqPred :: PredType -> PredType -> PredType
mkReprEqPred PredType
ty1  PredType
ty2
  = TyCon -> [PredType] -> PredType
mkTyConApp TyCon
eqReprPrimTyCon [PredType
k1, PredType
k2, PredType
ty1, PredType
ty2]
  where
    k1 :: PredType
k1 = HasDebugCallStack => PredType -> PredType
PredType -> PredType
typeKind PredType
ty1
    k2 :: PredType
k2 = HasDebugCallStack => PredType -> PredType
PredType -> PredType
typeKind PredType
ty2

-- | Makes a lifted equality predicate at the given role
mkEqPred :: EqRel -> Type -> Type -> PredType
mkEqPred :: EqRel -> PredType -> PredType -> PredType
mkEqPred EqRel
NomEq  = PredType -> PredType -> PredType
mkNomEqPred
mkEqPred EqRel
ReprEq = PredType -> PredType -> PredType
mkReprEqPred

-- | Makes a lifted equality predicate at the given role
mkEqPredRole :: Role -> Type -> Type -> PredType
mkEqPredRole :: Role -> PredType -> PredType -> PredType
mkEqPredRole Role
Nominal          = PredType -> PredType -> PredType
mkNomEqPred
mkEqPredRole Role
Representational = PredType -> PredType -> PredType
mkReprEqPred
mkEqPredRole Role
Phantom          = String -> PredType -> PredType -> PredType
forall a. HasCallStack => String -> a
panic String
"mkEqPred phantom"

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
-- Precondition: the PredType is (s ~#N t) or (s ~#R t)
getEqPredRole :: PredType -> Role
getEqPredRole PredType
ty = EqRel -> Role
eqRelRole (PredType -> EqRel
predTypeEqRel PredType
ty)

-- | Get the equality relation relevant for a pred type
-- Returns NomEq for dictionary predicates, etc
predTypeEqRel :: PredType -> EqRel
predTypeEqRel :: PredType -> EqRel
predTypeEqRel PredType
ty
  | PredType -> Bool
isReprEqPred PredType
ty = EqRel
ReprEq
  | Bool
otherwise       = EqRel
NomEq


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

{-
Note [Evidence for quantified constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The superclass mechanism in GHC.Tc.Solver.Dict.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.Dict.
-}

isPredTy :: HasDebugCallStack => Type -> Bool
-- Precondition: expects a type that classifies values
-- See Note [Types for coercions, predicates, and evidence] in GHC.Core.TyCo.Rep
-- Returns True for types of kind (CONSTRAINT _), False for ones of kind (TYPE _)
isPredTy :: HasDebugCallStack => PredType -> Bool
isPredTy PredType
ty = case HasDebugCallStack => PredType -> TypeOrConstraint
PredType -> TypeOrConstraint
typeTypeOrConstraint PredType
ty of
                  TypeOrConstraint
TypeLike       -> Bool
False
                  TypeOrConstraint
ConstraintLike -> Bool
True

-- | Does this type classify a core (unlifted) Coercion?
-- At either role nominal or representational
--    (t1 ~# t2) or (t1 ~R# t2)
-- See Note [Types for coercions, predicates, and evidence] in "GHC.Core.TyCo.Rep"
isCoVarType :: Type -> Bool
  -- ToDo: should we check saturation?
isCoVarType :: PredType -> Bool
isCoVarType PredType
ty = PredType -> Bool
isEqPred PredType
ty

isEvVarType :: Type -> Bool
-- True of (a) predicates, of kind Constraint, such as (Eq t), and (s ~ t)
--         (b) coercion types, such as (s ~# t) or (s ~R# t)
-- 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

isEqPred :: PredType -> Bool
-- True of (s ~# t) (s ~R# t)
-- NB: but NOT true of (s ~ t) or (s ~~ t) or (Coecible s t)
isEqPred :: PredType -> Bool
isEqPred PredType
ty
  | Just TyCon
tc <- PredType -> Maybe TyCon
tyConAppTyCon_maybe PredType
ty
  = 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
  | Bool
otherwise
  = Bool
False

isReprEqPred :: PredType -> Bool
-- True of (s ~R# t)
isReprEqPred :: PredType -> Bool
isReprEqPred PredType
ty
  | Just TyCon
tc <- PredType -> Maybe TyCon
tyConAppTyCon_maybe PredType
ty
  = TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqReprPrimTyConKey
  | Bool
otherwise
  = Bool
False

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

isEqClassPred :: PredType -> Bool
isEqClassPred :: PredType -> Bool
isEqClassPred PredType
ty  -- True of (s ~ t) and (s ~~ t)
                  -- 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
isEqualityClass Class
cls
  | Bool
otherwise
  = Bool
False

isEqualityClass :: Class -> Bool
-- True of (~), (~~), and Coercible
-- These all have a single primitive-equality superclass, either (~N# or ~R#)
isEqualityClass :: Class -> Bool
isEqualityClass Class
cls
  = Class
cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
heqTyConKey
    Bool -> Bool -> Bool
|| 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
coercibleTyConKey

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

-- | Decomposes a predicate if it is an implicit parameter. Does not look in
-- superclasses. See also [Local implicit parameters].
isIPPred_maybe :: Class -> [Type] -> Maybe (Type, Type)
isIPPred_maybe :: Class -> [PredType] -> Maybe (PredType, PredType)
isIPPred_maybe Class
cls [PredType]
tys
  | Class -> Bool
isIPClass Class
cls
  , [PredType
t1,PredType
t2] <- [PredType]
tys
  = (PredType, PredType) -> Maybe (PredType, PredType)
forall a. a -> Maybe a
Just (PredType
t1,PredType
t2)
  | Bool
otherwise
  = Maybe (PredType, PredType)
forall a. Maybe a
Nothing

-- --------------------- ExceptionContext predicates --------------------------

-- | Is a 'PredType' an @ExceptionContext@ implicit parameter?
--
-- If so, return the name of the parameter.
isExceptionContextPred :: Class -> [Type] -> Maybe FastString
isExceptionContextPred :: Class -> [PredType] -> Maybe FastString
isExceptionContextPred Class
cls [PredType]
tys
  | [PredType
ty1, PredType
ty2] <- [PredType]
tys
  , Class -> Bool
isIPClass Class
cls
  , PredType -> Bool
isExceptionContextTy PredType
ty2
  = PredType -> Maybe FastString
isStrLitTy PredType
ty1
  | Bool
otherwise
  = Maybe FastString
forall a. Maybe a
Nothing

-- | Is a type an 'ExceptionContext'?
isExceptionContextTy :: Type -> Bool
isExceptionContextTy :: PredType -> Bool
isExceptionContextTy PredType
ty
  | Just TyCon
tc <- PredType -> Maybe TyCon
tyConAppTyCon_maybe PredType
ty
  = TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
exceptionContextTyConKey
  | Bool
otherwise
  = Bool
False

-- --------------------- CallStack predicates ---------------------------------

isCallStackPredTy :: Type -> Bool
-- True of HasCallStack, or IP "blah" CallStack
isCallStackPredTy :: PredType -> Bool
isCallStackPredTy PredType
ty
  | Just (TyCon
tc, [PredType]
tys) <- HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
ty
  , Just Class
cls <- TyCon -> Maybe Class
tyConClass_maybe TyCon
tc
  , Just {} <- Class -> [PredType] -> Maybe FastString
isCallStackPred Class
cls [PredType]
tys
  = Bool
True
  | Bool
otherwise
  = Bool
False

-- | Is a 'PredType' a 'CallStack' implicit parameter?
--
-- If so, return the name of the parameter.
isCallStackPred :: Class -> [Type] -> Maybe FastString
isCallStackPred :: Class -> [PredType] -> Maybe FastString
isCallStackPred Class
cls [PredType]
tys
  | [PredType
ty1, PredType
ty2] <- [PredType]
tys
  , Class -> Bool
isIPClass Class
cls
  , PredType -> Bool
isCallStackTy PredType
ty2
  = PredType -> Maybe FastString
isStrLitTy PredType
ty1
  | Bool
otherwise
  = Maybe FastString
forall a. Maybe a
Nothing

-- | Is a type a 'CallStack'?
isCallStackTy :: Type -> Bool
isCallStackTy :: PredType -> Bool
isCallStackTy PredType
ty
  | Just TyCon
tc <- PredType -> Maybe TyCon
tyConAppTyCon_maybe PredType
ty
  = TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
callStackTyConKey
  | Bool
otherwise
  = Bool
False

-- --------------------- isIPLike and mentionsIP  --------------------------
--                 See Note [Local implicit parameters]

isIPLikePred :: Type -> Bool
-- Is `pred`, or any of its superclasses, an implicit parameter?
-- See Note [Local implicit parameters]
isIPLikePred :: PredType -> Bool
isIPLikePred PredType
pred =
  RecTcChecker
-> (PredType -> Bool) -> (PredType -> Bool) -> PredType -> Bool
mentions_ip_pred RecTcChecker
initIPRecTc (Bool -> PredType -> Bool
forall a b. a -> b -> a
const Bool
True) (Bool -> PredType -> Bool
forall a b. a -> b -> a
const Bool
True) PredType
pred

mentionsIP :: (Type -> Bool) -- ^ predicate on the string
           -> (Type -> Bool) -- ^ predicate on the type
           -> Class
           -> [Type] -> Bool
-- ^ @'mentionsIP' str_cond ty_cond cls tys@ returns @True@ if:
--
--    - @cls tys@ is of the form @IP str ty@, where @str_cond str@ and @ty_cond ty@
--      are both @True@,
--    - or any superclass of @cls tys@ has this property.
--
-- See Note [Local implicit parameters]
mentionsIP :: (PredType -> Bool)
-> (PredType -> Bool) -> Class -> [PredType] -> Bool
mentionsIP = RecTcChecker
-> (PredType -> Bool)
-> (PredType -> Bool)
-> Class
-> [PredType]
-> Bool
mentions_ip RecTcChecker
initIPRecTc

mentions_ip :: RecTcChecker -> (Type -> Bool) -> (Type -> Bool) -> Class -> [Type] -> Bool
mentions_ip :: RecTcChecker
-> (PredType -> Bool)
-> (PredType -> Bool)
-> Class
-> [PredType]
-> Bool
mentions_ip RecTcChecker
rec_clss PredType -> Bool
str_cond PredType -> Bool
ty_cond Class
cls [PredType]
tys
  | Just (PredType
str_ty, PredType
ty) <- Class -> [PredType] -> Maybe (PredType, PredType)
isIPPred_maybe Class
cls [PredType]
tys
  = PredType -> Bool
str_cond PredType
str_ty Bool -> Bool -> Bool
&& PredType -> Bool
ty_cond PredType
ty
  | Bool
otherwise
  = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ RecTcChecker
-> (PredType -> Bool) -> (PredType -> Bool) -> PredType -> Bool
mentions_ip_pred RecTcChecker
rec_clss PredType -> Bool
str_cond PredType -> Bool
ty_cond (TyVar -> [PredType] -> PredType
classMethodInstTy TyVar
sc_sel_id [PredType]
tys)
       | TyVar
sc_sel_id <- Class -> [TyVar]
classSCSelIds Class
cls ]


mentions_ip_pred :: RecTcChecker -> (Type -> Bool) -> (Type -> Bool) -> Type -> Bool
mentions_ip_pred :: RecTcChecker
-> (PredType -> Bool) -> (PredType -> Bool) -> PredType -> Bool
mentions_ip_pred RecTcChecker
rec_clss PredType -> Bool
str_cond PredType -> Bool
ty_cond PredType
ty
  | Just (Class
cls, [PredType]
tys) <- PredType -> Maybe (Class, [PredType])
getClassPredTys_maybe PredType
ty
  , let tc :: TyCon
tc = Class -> TyCon
classTyCon Class
cls
  , Just RecTcChecker
rec_clss' <- if TyCon -> Bool
isTupleTyCon TyCon
tc then RecTcChecker -> Maybe RecTcChecker
forall a. a -> Maybe a
Just RecTcChecker
rec_clss
                      else RecTcChecker -> TyCon -> Maybe RecTcChecker
checkRecTc RecTcChecker
rec_clss TyCon
tc
  = RecTcChecker
-> (PredType -> Bool)
-> (PredType -> Bool)
-> Class
-> [PredType]
-> Bool
mentions_ip RecTcChecker
rec_clss' PredType -> Bool
str_cond PredType -> Bool
ty_cond Class
cls [PredType]
tys
  | Bool
otherwise
  = Bool
False -- Includes things like (D []) where D is
          -- a Constraint-ranged family; #7785

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

{- Note [Local implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
See also wrinkle (SIP1) in Note [Shadowing of implicit parameters] in
GHC.Tc.Solver.Dict.

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 -XUndecidableSuperClasses, 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.

Note [Using typesAreApart when calling mentionsIP]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We call 'mentionsIP' in two situations:

  (1) to check that a predicate does not contain any implicit parameters
      IP str ty, for a fixed literal str and any type ty,
  (2) to check that a predicate does not contain any HasCallStack or
      HasExceptionContext constraints.

In both of these cases, we want to be sure, so we should be conservative:

  For (1), the predicate might contain an implicit parameter IP Str a, where
  Str is a type family such as:

    type family MyStr where MyStr = "abc"

  To safeguard against this (niche) situation, instead of doing a simple
  type equality check, we use 'typesAreApart'. This allows us to recognise
  that 'IP MyStr a' contains an implicit parameter of the form 'IP "abc" ty'.

  For (2), we similarly might have

    type family MyCallStack where MyCallStack = CallStack

  Again, here we use 'typesAreApart'. This allows us to see that

    (?foo :: MyCallStack)

  is indeed a CallStack constraint, hidden under a type family.
-}

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

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

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


{- *********************************************************************
*                                                                      *
                 scopedSort

       This function lives here becuase it uses isEvVar
*                                                                      *
********************************************************************* -}

{- Note [ScopedSort]
~~~~~~~~~~~~~~~~~~~~
Consider

  foo :: Proxy a -> Proxy (b :: k) -> Proxy (a :: k2) -> ()

This function type is implicitly generalised over [a, b, k, k2]. These
variables will be Specified; that is, they will be available for visible
type application. This is because they are written in the type signature
by the user.

However, we must ask: what order will they appear in? In cases without
dependency, this is easy: we just use the lexical left-to-right ordering
of first occurrence. With dependency, we cannot get off the hook so
easily.

We thus state:

 * These variables appear in the order as given by ScopedSort, where
   the input to ScopedSort is the left-to-right order of first occurrence.

Note that this applies only to *implicit* quantification, without a
`forall`. If the user writes a `forall`, then we just use the order given.

ScopedSort is defined thusly (as proposed in #15743):
  * Work left-to-right through the input list, with a cursor.
  * If variable v at the cursor is depended on by any earlier variable w,
    move v immediately before the leftmost such w.

INVARIANT: The prefix of variables before the cursor form a valid telescope.

Note that ScopedSort makes sense only after type inference is done and all
types/kinds are fully settled and zonked.

-}

-- | Do a topological sort on a list of tyvars,
--   so that binders occur before occurrences
-- E.g. given  @[ a::k, k::Type, b::k ]@
-- it'll return a well-scoped list @[ k::Type, a::k, b::k ]@.
--
-- This is a deterministic sorting operation
-- (that is, doesn't depend on Uniques).
--
-- It is also meant to be stable: that is, variables should not
-- be reordered unnecessarily. This is specified in Note [ScopedSort]
-- See also Note [Ordering of implicit variables] in "GHC.Rename.HsType"

scopedSort :: [Var] -> [Var]
scopedSort :: [TyVar] -> [TyVar]
scopedSort = [TyVar] -> [TyCoVarSet] -> [TyVar] -> [TyVar]
go [] []
  where
    go :: [Var] -- already sorted, in reverse order
       -> [TyCoVarSet] -- each set contains all the variables which must be placed
                       -- before the tv corresponding to the set; they are accumulations
                       -- of the fvs in the sorted Var's types

                       -- This list is in 1-to-1 correspondence with the sorted Vars
                       -- INVARIANT:
                       --   all (\tl -> all (`subVarSet` head tl) (tail tl)) (tails fv_list)
                       -- That is, each set in the list is a superset of all later sets.

       -> [Var] -- yet to be sorted
       -> [Var]
    go :: [TyVar] -> [TyCoVarSet] -> [TyVar] -> [TyVar]
go [TyVar]
acc [TyCoVarSet]
_fv_list [] = [TyVar] -> [TyVar]
forall a. [a] -> [a]
reverse [TyVar]
acc
    go [TyVar]
acc  [TyCoVarSet]
fv_list (TyVar
tv:[TyVar]
tvs)
      = [TyVar] -> [TyCoVarSet] -> [TyVar] -> [TyVar]
go [TyVar]
acc' [TyCoVarSet]
fv_list' [TyVar]
tvs
      where
        ([TyVar]
acc', [TyCoVarSet]
fv_list') = TyVar -> [TyVar] -> [TyCoVarSet] -> ([TyVar], [TyCoVarSet])
insert TyVar
tv [TyVar]
acc [TyCoVarSet]
fv_list

    insert :: Var           -- var to insert
           -> [Var]         -- sorted list, in reverse order
           -> [TyCoVarSet]  -- list of fvs, as above
           -> ([Var], [TyCoVarSet])   -- augmented lists
    -- Generally we put the new Var at the front of the accumulating list
    -- (leading to a stable sort) unless there is are reason to put it later.
    insert :: TyVar -> [TyVar] -> [TyCoVarSet] -> ([TyVar], [TyCoVarSet])
insert TyVar
v []     []         = ([TyVar
v], [PredType -> TyCoVarSet
tyCoVarsOfType (TyVar -> PredType
varType TyVar
v)])
    insert TyVar
v (TyVar
a:[TyVar]
as) (TyCoVarSet
fvs:[TyCoVarSet]
fvss)
      | (TyVar -> Bool
isTyVar TyVar
v Bool -> Bool -> Bool
&& TyVar -> Bool
isId TyVar
a) Bool -> Bool -> Bool
||          -- TyVars precede Ids
        (TyVar -> Bool
isEvVar TyVar
v Bool -> Bool -> Bool
&& TyVar -> Bool
isId TyVar
a Bool -> Bool -> Bool
&& Bool -> Bool
not (TyVar -> Bool
isEvVar TyVar
a)) Bool -> Bool -> Bool
|| -- DictIds precede non-DictIds
        (TyVar
v TyVar -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
fvs)
          -- (a) put Ids after TyVars, and (b) respect dependencies
      , ([TyVar]
as', [TyCoVarSet]
fvss') <- TyVar -> [TyVar] -> [TyCoVarSet] -> ([TyVar], [TyCoVarSet])
insert TyVar
v [TyVar]
as [TyCoVarSet]
fvss
      = (TyVar
aTyVar -> [TyVar] -> [TyVar]
forall a. a -> [a] -> [a]
:[TyVar]
as', TyCoVarSet
fvs TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` TyCoVarSet
fv_v TyCoVarSet -> [TyCoVarSet] -> [TyCoVarSet]
forall a. a -> [a] -> [a]
: [TyCoVarSet]
fvss')

      | Bool
otherwise  -- Put `v` at the front
      = (TyVar
vTyVar -> [TyVar] -> [TyVar]
forall a. a -> [a] -> [a]
:TyVar
aTyVar -> [TyVar] -> [TyVar]
forall a. a -> [a] -> [a]
:[TyVar]
as, TyCoVarSet
fvs TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` TyCoVarSet
fv_v TyCoVarSet -> [TyCoVarSet] -> [TyCoVarSet]
forall a. a -> [a] -> [a]
: TyCoVarSet
fvs TyCoVarSet -> [TyCoVarSet] -> [TyCoVarSet]
forall a. a -> [a] -> [a]
: [TyCoVarSet]
fvss)
      where
        fv_v :: TyCoVarSet
fv_v = PredType -> TyCoVarSet
tyCoVarsOfType (TyVar -> PredType
varType TyVar
v)

       -- lists not in correspondence
    insert TyVar
_ [TyVar]
_ [TyCoVarSet]
_ = String -> ([TyVar], [TyCoVarSet])
forall a. HasCallStack => String -> a
panic String
"scopedSort"

-- | Get the free vars of a type in scoped order
tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
tyCoVarsOfTypeWellScoped :: PredType -> [TyVar]
tyCoVarsOfTypeWellScoped = [TyVar] -> [TyVar]
scopedSort ([TyVar] -> [TyVar])
-> (PredType -> [TyVar]) -> PredType -> [TyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> [TyVar]
tyCoVarsOfTypeList

-- | Get the free vars of types in scoped order
tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
tyCoVarsOfTypesWellScoped :: [PredType] -> [TyVar]
tyCoVarsOfTypesWellScoped = [TyVar] -> [TyVar]
scopedSort ([TyVar] -> [TyVar])
-> ([PredType] -> [TyVar]) -> [PredType] -> [TyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [PredType] -> [TyVar]
tyCoVarsOfTypesList


{- *********************************************************************
*                                                                      *
*                   Equality left-hand sides
*                                                                      *
********************************************************************* -}

-- | A 'CanEqLHS' is a type that can appear on the left of a canonical
-- equality: a type variable or /exactly-saturated/ type family application.
data CanEqLHS
  = TyVarLHS TyVar
  | TyFamLHS TyCon  -- ^ TyCon of the family
             [Type]   -- ^ Arguments, /exactly saturating/ the family

instance Outputable CanEqLHS where
  ppr :: CanEqLHS -> SDoc
ppr (TyVarLHS TyVar
tv)              = TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tv
  ppr (TyFamLHS TyCon
fam_tc [PredType]
fam_args) = PredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCon -> [PredType] -> PredType
mkTyConApp TyCon
fam_tc [PredType]
fam_args)

-----------------------------------
-- | Is a type a canonical LHS? That is, is it a tyvar or an exactly-saturated
-- type family application?
-- Does not look through type synonyms.
canEqLHS_maybe :: Type -> Maybe CanEqLHS
canEqLHS_maybe :: PredType -> Maybe CanEqLHS
canEqLHS_maybe PredType
xi
  | Just TyVar
tv <- PredType -> Maybe TyVar
getTyVar_maybe PredType
xi
  = CanEqLHS -> Maybe CanEqLHS
forall a. a -> Maybe a
Just (CanEqLHS -> Maybe CanEqLHS) -> CanEqLHS -> Maybe CanEqLHS
forall a b. (a -> b) -> a -> b
$ TyVar -> CanEqLHS
TyVarLHS TyVar
tv

  | Bool
otherwise
  = PredType -> Maybe CanEqLHS
canTyFamEqLHS_maybe PredType
xi

canTyFamEqLHS_maybe :: Type -> Maybe CanEqLHS
canTyFamEqLHS_maybe :: PredType -> Maybe CanEqLHS
canTyFamEqLHS_maybe PredType
xi
  | Just (TyCon
tc, [PredType]
args) <- HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
tcSplitTyConApp_maybe PredType
xi
  , TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
  , [PredType]
args [PredType] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthIs` TyCon -> Int
tyConArity TyCon
tc
  = CanEqLHS -> Maybe CanEqLHS
forall a. a -> Maybe a
Just (CanEqLHS -> Maybe CanEqLHS) -> CanEqLHS -> Maybe CanEqLHS
forall a b. (a -> b) -> a -> b
$ TyCon -> [PredType] -> CanEqLHS
TyFamLHS TyCon
tc [PredType]
args

  | Bool
otherwise
  = Maybe CanEqLHS
forall a. Maybe a
Nothing

-- | Convert a 'CanEqLHS' back into a 'Type'
canEqLHSType :: CanEqLHS -> Type
canEqLHSType :: CanEqLHS -> PredType
canEqLHSType (TyVarLHS TyVar
tv) = TyVar -> PredType
mkTyVarTy TyVar
tv
canEqLHSType (TyFamLHS TyCon
fam_tc [PredType]
fam_args) = TyCon -> [PredType] -> PredType
mkTyConApp TyCon
fam_tc [PredType]
fam_args

-- | Retrieve the kind of a 'CanEqLHS'
canEqLHSKind :: CanEqLHS -> Kind
canEqLHSKind :: CanEqLHS -> PredType
canEqLHSKind (TyVarLHS TyVar
tv) = TyVar -> PredType
tyVarKind TyVar
tv
canEqLHSKind (TyFamLHS TyCon
fam_tc [PredType]
fam_args) = HasDebugCallStack => PredType -> [PredType] -> PredType
PredType -> [PredType] -> PredType
piResultTys (TyCon -> PredType
tyConKind TyCon
fam_tc) [PredType]
fam_args

-- | Are two 'CanEqLHS's equal?
eqCanEqLHS :: CanEqLHS -> CanEqLHS -> Bool
eqCanEqLHS :: CanEqLHS -> CanEqLHS -> Bool
eqCanEqLHS (TyVarLHS TyVar
tv1) (TyVarLHS TyVar
tv2) = TyVar
tv1 TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar
tv2
eqCanEqLHS (TyFamLHS TyCon
fam_tc1 [PredType]
fam_args1) (TyFamLHS TyCon
fam_tc2 [PredType]
fam_args2)
  = TyCon -> [PredType] -> TyCon -> [PredType] -> Bool
tcEqTyConApps TyCon
fam_tc1 [PredType]
fam_args1 TyCon
fam_tc2 [PredType]
fam_args2
eqCanEqLHS CanEqLHS
_ CanEqLHS
_ = Bool
False