{-# LANGUAGE MultiWayIf #-}

module GHC.Core.TyCo.FVs
  (     -- Shallow
        shallowTyCoVarsOfType, shallowTyCoVarsOfTypes,
        shallowTyCoVarsOfCo, shallowTyCoVarsOfCos,

        -- Deep
        tyCoVarsOfType, tyCoVarsOfTypes, tyCoVarsOfTypesList,
        tyCoVarsOfThings,
        tyCoVarsOfCo, tyCoVarsOfCos, tyCoVarsOfMCo,
        tyCoVarsOfTyVarEnv, tyCoVarsOfCoVarEnv, tyCoVarsOfQuant,
        deepTcvFolder, deepTypeFV, deepTypesFV, deepCoFV,

        -- Deep, deterministic
        tyCoVarsOfTypeDSet, tyCoVarsOfTypesDSet, tyCoVarsOfTypeList,
        tyCoVarsOfCoDSet, tyCoVarsOfCoList,
        tyCoVarsOfThingsDSet,
        deepDetTypeFV, deepDetTypesFV, deepDetCoFV,

        -- Selective
        someTyCoVarsOfType, someTyCoVarsOfTypes,

        -- CoVars only
        coVarsOfType, coVarsOfTypes,
        coVarsOfCo, coVarsOfCos,
        coVarsOfCoDSet, coVarsOfCosDSet,

        -- Shallow, deterministic, composable
        shallowSelTypeFV, shallowSelCoFV,

        -- Almost devoid
        almostDevoidCoVarOfCo,

        -- Injective free vars
        injectiveVarsOfType, injectiveVarsOfTypes, isInjectiveInType,
        invisibleVarsOfType, invisibleVarsOfTypes,

        -- Any and No Free vars
        anyFreeVarsOfType, anyFreeVarsOfTypes, anyFreeVarsOfCo,
        noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,

        -- * Free type constructors
        tyConsOfType, tyConsOfTypes,

        -- * Free vars with visible/invisible separate
        visVarsOfTypes, visVarsOfType,

        -- * Occurrence-check expansion
        occCheckExpand,

        -- * Closing over kinds
        closeOverKindsDSet,
        closeOverKinds,
  ) where

import GHC.Prelude

import {-# SOURCE #-} GHC.Core.Type( partitionInvisibleTypes, coreView, rewriterView )

import GHC.Builtin.Types.Prim( funTyFlagTyCon )

import Data.Monoid as DM ( Any(..) )
import GHC.Core.TyCo.Rep
import GHC.Core.TyCon
import GHC.Core.Coercion.Axiom( CoAxiomRule(..), BuiltInFamRewrite(..), coAxiomTyCon )

import GHC.Types.Var
import GHC.Types.Var.FV
import GHC.Types.Unique.FM
import GHC.Types.Unique.Set

import GHC.Types.Var.Set
import GHC.Types.Var.Env

import GHC.Utils.Misc
import GHC.Utils.EndoOS

import GHC.Data.Pair

import Data.Semigroup

{-
%************************************************************************
%*                                                                      *
                 Free variables of types and coercions
%*                                                                      *
%************************************************************************
-}

{- Note [Shallow and deep free variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Definitions

* Shallow free variables of a type: the variables
  affected by substitution. Specifically, the (TyVarTy tv)
  and (CoVar cv) that appear
    - In the type and coercions appearing in the type
    - In shallow free variables of the kind of a Forall binder
  but NOT in the kind of the /occurrences/ of a type variable.

* Deep free variables of a type: shallow free variables, plus
  the deep free variables of the kinds of those variables.
  That is,  deepFVs( t ) = closeOverKinds( shallowFVs( t ) )

Examples:

  Type                     Shallow     Deep
  ---------------------------------
  (a : (k:Type))           {a}        {a,k}
  forall (a:(k:Type)). a   {k}        {k}
  (a:k->Type) (b:k)        {a,b}      {a,b,k}


Note [Computing deep free variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
tyCoVarsOfType computes the /deep/ free variables of a type; that is, if
`a::k` is in the result, then so are the free vars of `k`.  We say that the
resulting set is "closed over kinds".

But we must take care (see #14880):

1. Efficiency. If we have Proxy (a::ki) -> Proxy (a::ki) -> Proxy (a::ki), then
   we don't want to have to traverse ki more than once.

2. Correctness. Imagine we have forall k. (b::k) -> k, where b has
   kind k, for some k bound in an /outer/ scope. If we look at b's kind inside
   the forall, we'll collect that k is free and then remove k from the set of
   free variables. This is plain wrong. We must instead compute that b is free
   and then conclude that b's kind is free.

   BUT: there is no worry here any more because of Invariant (NoTypeShadowing).
        in GHC.Core.   In the example, the `forall k` shadows the `k` in
        b's kind, which is now illegal and checked by Lint.

An obvious first approach is to compute the /shallow/ free variables of the type,
and /then/ close over kinds.   But that turns out not to be very efficient.
Fortunately, there is a simpler way, which works with the accumulating
free-var story described in (FV1) of Note [Finding free variables] in
GHC.Types.Var.FV.  At an occurrence of a variable (a::k)

* Check if `a` is a locally-bound var; if so, ignore it.

* Check if `a` is already in the accumulator; if so, ignore it because we have
  deal with its kind already. Also pre-checking set membership before inserting
  allocates less than just inserting, because the no-op case of insertion does
  allocation.

* Otherwise add `a` to the accumulator,
  AND add on the free vars of its kind `k`.
  BUT in this latter step, start with an empty BoundVars set.

The "start with an empty BoundVars set" is implemented in `deepUnitFV`.  It's
not /necessary/ to zap the BoundVars set, because of Invariant (NoTypeShadowing).
But it's a tiny bit more efficient because the BoundVars set is smaller.

Side note: the free-variable binder would still work even without (NoTypeShadowing).
Consider:
    forall k. b -> k
where b :: k->Type is free; but of course, it's a different k! When looking at
b -> k we'll have k in the bound-var set. So we'll ignore the k. But suppose
this is our first encounter with b; we want the free vars of its kind. But we
want to behave as if we took the free vars of its kind at the end; that is,
with no bound vars in scope.

And that's it. This works because a variable is either bound or free. If it is bound,
then we won't look at it at all. If it is free, then all the variables free in its
kind are free -- regardless of whether some local variable has the same Unique.
So if we're looking at a variable occurrence at all, then all variables in its
kind are free.

Note [Free vars and synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When finding free variables we generally do not expand synonyms.  So given
   type T a = Int
the type (T [b]) will return `b` as a free variable, even though expanding the
synonym would get rid of it.  Expanding synonyms might lead to types that look
ill-scoped; an alternative we have not explored.

But see `occCheckExpand` in this module for a function that does, selectively,
expand synonyms to reduce free-var occurences.

Note [CoercionHoles and coercion free variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Generally, we do not treat a CoercionHole as a free variable of a coercion;
see `tyCoVarsOfType` and friends.

But there is an exception. When finding the free /coercion/ variables of a type,
in `coVarsOfType`, we /do/ treat a CoercionHole as a free variable.  Why?
The sole reason is in Note [Emitting the residual implication in simplifyInfer]
in GHC.Tc.Solver.  Yuk.  This is not pretty.
-}


{- *********************************************************************
*                                                                      *
          Deep free variables
          See Note [Shallow and deep free variables]
*                                                                      *
********************************************************************* -}

tyCoVarsOfType :: Type -> TyCoVarSet
-- The "deep" TyCoVars of the the type
tyCoVarsOfType :: Type -> TyCoVarSet
tyCoVarsOfType Type
ty = TyCoFV -> TyCoVarSet
runTyCoVars (Type -> TyCoFV
deepTypeFV Type
ty)
-- Alternative:
--   tyCoVarsOfType ty = closeOverKinds (shallowTyCoVarsOfType ty)

tyCoVarsOfTypes :: [Type] -> TyCoVarSet
-- The "deep" TyCoVars of the the type
tyCoVarsOfTypes :: [Type] -> TyCoVarSet
tyCoVarsOfTypes [Type]
tys = TyCoFV -> TyCoVarSet
runTyCoVars ([Type] -> TyCoFV
deepTypesFV [Type]
tys)
-- Alternative:
--   tyCoVarsOfTypes tys = closeOverKinds (shallowTyCoVarsOfTypes tys)

tyCoVarsOfCo :: Coercion -> TyCoVarSet
-- The "deep" TyCoVars of the the coercion
-- See Note [Computing deep free variables]
tyCoVarsOfCo :: Coercion -> TyCoVarSet
tyCoVarsOfCo Coercion
co = TyCoFV -> TyCoVarSet
runTyCoVars (Coercion -> TyCoFV
deepCoFV Coercion
co)

tyCoVarsOfMCo :: MCoercion -> TyCoVarSet
tyCoVarsOfMCo :: MCoercion -> TyCoVarSet
tyCoVarsOfMCo MCoercion
MRefl    = TyCoVarSet
emptyVarSet
tyCoVarsOfMCo (MCo Coercion
co) = Coercion -> TyCoVarSet
tyCoVarsOfCo Coercion
co

tyCoVarsOfCos :: [Coercion] -> TyCoVarSet
tyCoVarsOfCos :: [Coercion] -> TyCoVarSet
tyCoVarsOfCos [Coercion]
cos = TyCoFV -> TyCoVarSet
runTyCoVars ([Coercion] -> TyCoFV
deepCosFV [Coercion]
cos)

tyCoVarsOfThings :: Foldable t => (a -> Type) -> t a -> TyCoVarSet
-- Works over a collection of things from which we can extract a type
-- See Note [Computing deep free variables]
tyCoVarsOfThings :: forall (t :: * -> *) a.
Foldable t =>
(a -> Type) -> t a -> TyCoVarSet
tyCoVarsOfThings a -> Type
get_ty t a
things
  = TyCoFV -> TyCoVarSet
runTyCoVars (TyCoFV -> TyCoVarSet) -> TyCoFV -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$ (a -> TyCoFV) -> t a -> TyCoFV
forall (t :: * -> *) acc a env.
(Foldable t, Monoid acc) =>
(a -> FV env acc) -> t a -> FV env acc
mapUnionFV (Type -> TyCoFV
deepTypeFV (Type -> TyCoFV) -> (a -> Type) -> a -> TyCoFV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Type
get_ty) t a
things

-- | Returns free variables of types, including kind variables as
-- a non-deterministic set. For type synonyms it does /not/ expand the
-- synonym.
tyCoVarsOfTyVarEnv :: TyVarEnv Type -> TyCoVarSet
-- See Note [Shallow and deep free variables]
tyCoVarsOfTyVarEnv :: TyVarEnv Type -> TyCoVarSet
tyCoVarsOfTyVarEnv TyVarEnv Type
tys = [Type] -> TyCoVarSet
tyCoVarsOfTypes (TyVarEnv Type -> [Type]
forall {k} (key :: k) elt. UniqFM key elt -> [elt]
nonDetEltsUFM TyVarEnv Type
tys)
  -- It's OK to use nonDetEltsUFM here because we immediately
  -- forget the ordering by returning a set

tyCoVarsOfCoVarEnv :: CoVarEnv Coercion -> TyCoVarSet
tyCoVarsOfCoVarEnv :: CoVarEnv Coercion -> TyCoVarSet
tyCoVarsOfCoVarEnv CoVarEnv Coercion
cos = [Coercion] -> TyCoVarSet
tyCoVarsOfCos (CoVarEnv Coercion -> [Coercion]
forall {k} (key :: k) elt. UniqFM key elt -> [elt]
nonDetEltsUFM CoVarEnv Coercion
cos)
  -- It's OK to use nonDetEltsUFM here because we immediately
  -- forget the ordering by returning a set

tyCoVarsOfQuant :: [TyCoVar] -> TyCoVarSet -> TyCoVarSet
-- Give the deep free vars of (forall tcvs. <set>)
tyCoVarsOfQuant :: [Var] -> TyCoVarSet -> TyCoVarSet
tyCoVarsOfQuant [] TyCoVarSet
fvs         = TyCoVarSet
fvs
tyCoVarsOfQuant (Var
tcv:[Var]
tcvs) TyCoVarSet
fvs = ([Var] -> TyCoVarSet -> TyCoVarSet
tyCoVarsOfQuant [Var]
tcvs TyCoVarSet
fvs TyCoVarSet -> Var -> TyCoVarSet
`delVarSet` Var
tcv)
                                 TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
tyCoVarsOfType (Var -> Type
varType Var
tcv)

deepTypeFV  :: Type       -> TyCoFV
deepTypesFV :: [Type]     -> TyCoFV
deepCoFV    :: Coercion   -> TyCoFV
deepCosFV   :: [Coercion] -> TyCoFV
(Type -> TyCoFV
deepTypeFV, [Type] -> TyCoFV
deepTypesFV, Coercion -> TyCoFV
deepCoFV, [Coercion] -> TyCoFV
deepCosFV) = TyCoFolder TyCoFV
-> (Type -> TyCoFV, [Type] -> TyCoFV, Coercion -> TyCoFV,
    [Coercion] -> TyCoFV)
forall a.
Monoid a =>
TyCoFolder a
-> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder TyCoFV
deepTcvFolder

deepTcvFolder :: TyCoFolder TyCoFV
-- It's important that we use a one-shot EndoOS, to ensure that all
-- the free-variable finders are eta-expanded.  Lacking the one-shot-ness
-- led to some big slow downs.  See Note [The one-shot state monad trick]
-- in GHC.Utils.Monad
deepTcvFolder :: TyCoFolder TyCoFV
deepTcvFolder = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView  -- See Note [Free vars and synonyms]
                           , tcf_tyvar :: Var -> TyCoFV
tcf_tyvar = Var -> TyCoFV
do_tcv, tcf_covar :: Var -> TyCoFV
tcf_covar = Var -> TyCoFV
do_tcv
                           , tcf_hole :: CoercionHole -> TyCoFV
tcf_hole  = CoercionHole -> TyCoFV
do_hole
                           , tcf_tycobinder :: Var -> TyCoFV -> TyCoFV
tcf_tycobinder = Var -> TyCoFV -> TyCoFV
forall a. Var -> FV TyCoVarSet a -> FV TyCoVarSet a
addBndrFV }
  where
    do_tcv :: TyVar -> TyCoFV
    do_tcv :: Var -> TyCoFV
do_tcv = (Type -> TyCoFV) -> Var -> TyCoFV
deepUnitFV Type -> TyCoFV
deepTypeFV

    do_hole :: CoercionHole -> TyCoFV
    do_hole :: CoercionHole -> TyCoFV
do_hole CoercionHole
hole = Type -> TyCoFV
deepTypeFV (Var -> Type
varType (CoercionHole -> Var
coHoleCoVar CoercionHole
hole))
                     -- We don't collect the CoercionHole itself, but we /do/
                     -- need to collect the free variables of its /kind/
                     -- See Note [CoercionHoles and coercion free variables]

deepUnitFV :: (Type -> TyCoFV) -> TyCoVar -> TyCoFV
-- Deal with a single TyCoVar
-- Takes a function to find free vars of the kind
-- See Note [Computing deep free variables]
{-# INLINE deepUnitFV #-}   -- INLINE to specialise on fvs_of_kind
deepUnitFV :: (Type -> TyCoFV) -> Var -> TyCoFV
deepUnitFV Type -> TyCoFV
fvs_of_kind
  = \Var
v -> (TyCoVarSet -> EndoOS TyCoVarSet) -> TyCoFV
forall env acc. (env -> acc) -> FV env acc
MkFV (\TyCoVarSet
bvs -> (TyCoVarSet -> TyCoVarSet) -> EndoOS TyCoVarSet
forall a. (a -> a) -> EndoOS a
EndoOS (TyCoVarSet -> Var -> TyCoVarSet -> TyCoVarSet
do_it TyCoVarSet
bvs Var
v))
  where
    do_it :: BoundVars -> TyCoVar -> TyCoVarSet -> TyCoVarSet
    do_it :: TyCoVarSet -> Var -> TyCoVarSet -> TyCoVarSet
do_it TyCoVarSet
bvs Var
v TyCoVarSet
acc | Var
v Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
bvs = TyCoVarSet
acc
                    | Var
v Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
acc = TyCoVarSet
acc
                    | Bool
otherwise          = TyCoFV -> TyCoVarSet -> TyCoVarSet
forall a. FV TyCoVarSet (EndoOS a) -> a -> a
runFVAcc (Type -> TyCoFV
fvs_of_kind (Var -> Type
varType Var
v)) TyCoVarSet
acc
                                           TyCoVarSet -> Var -> TyCoVarSet
`extendVarSet` Var
v
                  -- Left-to-right: add the kind variables to the
                  --                accumulator before v itself

{- *********************************************************************
*                                                                      *
          Shallow free variables
          See Note [Shallow and deep free variables]
*                                                                      *
********************************************************************* -}

shallowTyCoVarsOfType :: Type -> TyCoVarSet
-- See Note [Shallow and deep free variables]
shallowTyCoVarsOfType :: Type -> TyCoVarSet
shallowTyCoVarsOfType Type
ty = TyCoFV -> TyCoVarSet
runTyCoVars (Type -> TyCoFV
shallowTypeFV Type
ty)

shallowTyCoVarsOfTypes :: [Type] -> TyCoVarSet
shallowTyCoVarsOfTypes :: [Type] -> TyCoVarSet
shallowTyCoVarsOfTypes [Type]
tys = TyCoFV -> TyCoVarSet
runTyCoVars ([Type] -> TyCoFV
shallowTypesFV [Type]
tys)

shallowTyCoVarsOfCo :: Coercion -> TyCoVarSet
shallowTyCoVarsOfCo :: Coercion -> TyCoVarSet
shallowTyCoVarsOfCo Coercion
co = TyCoFV -> TyCoVarSet
runTyCoVars (Coercion -> TyCoFV
shallowCoFV Coercion
co)

shallowTyCoVarsOfCos :: [Coercion] -> TyCoVarSet
shallowTyCoVarsOfCos :: [Coercion] -> TyCoVarSet
shallowTyCoVarsOfCos [Coercion]
cos = TyCoFV -> TyCoVarSet
runTyCoVars ([Coercion] -> TyCoFV
shallowCosFV [Coercion]
cos)

shallowTypeFV  :: Type       -> TyCoFV
shallowTypesFV :: [Type]     -> TyCoFV
shallowCoFV    :: Coercion   -> TyCoFV
shallowCosFV   :: [Coercion] -> TyCoFV
(Type -> TyCoFV
shallowTypeFV, [Type] -> TyCoFV
shallowTypesFV, Coercion -> TyCoFV
shallowCoFV, [Coercion] -> TyCoFV
shallowCosFV)
   = TyCoFolder TyCoFV
-> (Type -> TyCoFV, [Type] -> TyCoFV, Coercion -> TyCoFV,
    [Coercion] -> TyCoFV)
forall a.
Monoid a =>
TyCoFolder a
-> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder TyCoFV
shallowTcvFolder

shallowTcvFolder :: TyCoFolder TyCoFV
shallowTcvFolder :: TyCoFolder TyCoFV
shallowTcvFolder = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView  -- See Note [Free vars and synonyms]
                              , tcf_tyvar :: Var -> TyCoFV
tcf_tyvar = Var -> TyCoFV
do_tcv, tcf_covar :: Var -> TyCoFV
tcf_covar = Var -> TyCoFV
do_tcv
                              , tcf_hole :: CoercionHole -> TyCoFV
tcf_hole  = CoercionHole -> TyCoFV
forall {a} {p}. Monoid a => p -> a
do_hole
                              , tcf_tycobinder :: Var -> TyCoFV -> TyCoFV
tcf_tycobinder = Var -> TyCoFV -> TyCoFV
forall a. Var -> FV TyCoVarSet a -> FV TyCoVarSet a
addBndrFV }
  where
    do_tcv :: Var -> TyCoFV
do_tcv = Var -> TyCoFV
shallowUnitFV
    do_hole :: p -> a
do_hole p
_  = a
forall a. Monoid a => a
mempty   -- Ignore coercion holes

shallowUnitFV :: TyCoVar -> TyCoFV
shallowUnitFV :: Var -> TyCoFV
shallowUnitFV Var
v
  = (TyCoVarSet -> EndoOS TyCoVarSet) -> TyCoFV
forall env acc. (env -> acc) -> FV env acc
MkFV (\TyCoVarSet
bvs -> (TyCoVarSet -> TyCoVarSet) -> EndoOS TyCoVarSet
forall a. (a -> a) -> EndoOS a
EndoOS (TyCoVarSet -> TyCoVarSet -> TyCoVarSet
do_it TyCoVarSet
bvs))
  where
    do_it :: TyCoVarSet -> TyCoVarSet -> TyCoVarSet
do_it TyCoVarSet
bvs TyCoVarSet
acc | Var
v Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
bvs = TyCoVarSet
acc
                  | Var
v Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
acc = TyCoVarSet
acc
                  | Bool
otherwise          = TyCoVarSet
acc TyCoVarSet -> Var -> TyCoVarSet
`extendVarSet` Var
v


{- *********************************************************************
*                                                                      *
          Deterministic, deep free vars
*                                                                      *
********************************************************************* -}

-- | `tyCoVarsOfTypeDSet` that returns deep free variables of a type in a
-- deterministic set. For explanation of why using `VarSet` is not deterministic
-- see Note [Deterministic FV] in "GHC.Types.Var.FV".
tyCoVarsOfTypeDSet :: Type -> DTyCoVarSet
-- See Note [Computing deep free variables]
tyCoVarsOfTypeDSet :: Type -> DVarSet
tyCoVarsOfTypeDSet Type
ty = DCoVarFV -> DVarSet
runTyCoVarsDSet (Type -> DCoVarFV
deepDetTypeFV Type
ty)

-- | Returns free variables of types, including kind variables as
-- a deterministic set. For type synonyms it does /not/ expand the
-- synonym.
tyCoVarsOfTypesDSet :: [Type] -> DTyCoVarSet
-- See Note [Computing deep free variables]
tyCoVarsOfTypesDSet :: [Type] -> DVarSet
tyCoVarsOfTypesDSet [Type]
tys = DCoVarFV -> DVarSet
runTyCoVarsDSet ([Type] -> DCoVarFV
deepDetTypesFV [Type]
tys)

tyCoVarsOfThingsDSet :: Foldable t => (a -> Type) -> t a -> DTyCoVarSet
-- Works over a collection of things from which we can extract a type
-- See Note [Computing deep free variables]
tyCoVarsOfThingsDSet :: forall (t :: * -> *) a. Foldable t => (a -> Type) -> t a -> DVarSet
tyCoVarsOfThingsDSet a -> Type
get_ty t a
things
  = DCoVarFV -> DVarSet
runTyCoVarsDSet ((a -> DCoVarFV) -> t a -> DCoVarFV
forall (t :: * -> *) acc a env.
(Foldable t, Monoid acc) =>
(a -> FV env acc) -> t a -> FV env acc
mapUnionFV (Type -> DCoVarFV
deepDetTypeFV (Type -> DCoVarFV) -> (a -> Type) -> a -> DCoVarFV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Type
get_ty) t a
things)

-- | `tyCoVarsOfTypeList` returns free variables of a type in deterministic
-- order. For explanation of why using `VarSet` is not deterministic see
-- Note [Deterministic FV] in "GHC.Types.Var.FV".
tyCoVarsOfTypeList :: Type -> [TyCoVar]
-- See Note [Computing deep free variables]
tyCoVarsOfTypeList :: Type -> [Var]
tyCoVarsOfTypeList Type
ty = DVarSet -> [Var]
dVarSetElems (DVarSet -> [Var]) -> DVarSet -> [Var]
forall a b. (a -> b) -> a -> b
$ Type -> DVarSet
tyCoVarsOfTypeDSet Type
ty

tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet
-- See Note [Computing deep free variables]
tyCoVarsOfCoDSet :: Coercion -> DVarSet
tyCoVarsOfCoDSet Coercion
ty = DCoVarFV -> DVarSet
runTyCoVarsDSet (Coercion -> DCoVarFV
deepDetCoFV Coercion
ty)

tyCoVarsOfCoList :: Coercion -> [TyCoVar]
-- See Note [Computing deep free variables]
tyCoVarsOfCoList :: Coercion -> [Var]
tyCoVarsOfCoList Coercion
ty = DVarSet -> [Var]
dVarSetElems (DVarSet -> [Var]) -> DVarSet -> [Var]
forall a b. (a -> b) -> a -> b
$ Coercion -> DVarSet
tyCoVarsOfCoDSet Coercion
ty

-- | Returns free variables of types, including kind variables as
-- a deterministically ordered list. For type synonyms it does /not/ expand the
-- synonym.
tyCoVarsOfTypesList :: [Type] -> [TyCoVar]
-- See Note [Computing deep free variables]
tyCoVarsOfTypesList :: [Type] -> [Var]
tyCoVarsOfTypesList [Type]
tys = DVarSet -> [Var]
dVarSetElems (DVarSet -> [Var]) -> DVarSet -> [Var]
forall a b. (a -> b) -> a -> b
$ [Type] -> DVarSet
tyCoVarsOfTypesDSet [Type]
tys

deepDetTypeFV  :: Type   -> DTyCoFV
deepDetTypesFV :: [Type] -> DTyCoFV
deepDetCoFV    :: Coercion -> DTyCoFV
(Type -> DCoVarFV
deepDetTypeFV, [Type] -> DCoVarFV
deepDetTypesFV, Coercion -> DCoVarFV
deepDetCoFV, [Coercion] -> DCoVarFV
_) = TyCoFolder DCoVarFV
-> (Type -> DCoVarFV, [Type] -> DCoVarFV, Coercion -> DCoVarFV,
    [Coercion] -> DCoVarFV)
forall a.
Monoid a =>
TyCoFolder a
-> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder DCoVarFV
deepDetTcvFolder

deepDetTcvFolder :: TyCoFolder DTyCoFV
-- This one returns a /deterministic/ list
-- See `deepTcvFolder` for the general pattern
deepDetTcvFolder :: TyCoFolder DCoVarFV
deepDetTcvFolder
  = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView
               , tcf_tyvar :: Var -> DCoVarFV
tcf_tyvar = Var -> DCoVarFV
do_tcv, tcf_covar :: Var -> DCoVarFV
tcf_covar = Var -> DCoVarFV
do_tcv
               , tcf_hole :: CoercionHole -> DCoVarFV
tcf_hole  = CoercionHole -> DCoVarFV
do_hole
               , tcf_tycobinder :: Var -> DCoVarFV -> DCoVarFV
tcf_tycobinder = Var -> DCoVarFV -> DCoVarFV
forall a. Var -> FV TyCoVarSet a -> FV TyCoVarSet a
addBndrFV }
  where
    do_tcv :: Var -> DCoVarFV
do_tcv = (Type -> DCoVarFV) -> Var -> DCoVarFV
deepDetUnitFV Type -> DCoVarFV
deepDetTypeFV
    do_hole :: CoercionHole -> DCoVarFV
do_hole CoercionHole
hole = Type -> DCoVarFV
deepDetTypeFV (Var -> Type
varType (CoercionHole -> Var
coHoleCoVar CoercionHole
hole))

deepDetUnitFV :: (Type -> DTyCoFV) -> TyCoVar -> DTyCoFV
-- Deal with a single TyCoVar
-- Takes a function to find free vars of the kind
-- See Note [Computing deep free variables]
deepDetUnitFV :: (Type -> DCoVarFV) -> Var -> DCoVarFV
deepDetUnitFV Type -> DCoVarFV
fvs_of_kind Var
v
  = (TyCoVarSet -> EndoOS DVarSet) -> DCoVarFV
forall env acc. (env -> acc) -> FV env acc
MkFV (\TyCoVarSet
bvs -> (DVarSet -> DVarSet) -> EndoOS DVarSet
forall a. (a -> a) -> EndoOS a
EndoOS (TyCoVarSet -> DVarSet -> DVarSet
do_it TyCoVarSet
bvs))
  where
    do_it :: BoundVars -> DTyCoVarSet -> DTyCoVarSet
    do_it :: TyCoVarSet -> DVarSet -> DVarSet
do_it TyCoVarSet
bvs DVarSet
acc | Var
v Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
bvs  = DVarSet
acc
                  | Var
v Var -> DVarSet -> Bool
`elemDVarSet` DVarSet
acc = DVarSet
acc
                  | Bool
otherwise           = DCoVarFV -> DVarSet -> DVarSet
forall a. FV TyCoVarSet (EndoOS a) -> a -> a
runFVAcc (Type -> DCoVarFV
fvs_of_kind (Var -> Type
varType Var
v)) DVarSet
acc
                                          DVarSet -> Var -> DVarSet
`extendDVarSet` Var
v
                  -- Left-to-right: add the kind variables to the
                  --                accumulator before v itself

{- *********************************************************************
*                                                                      *
          Selective, shallow, deterministic free vars
*                                                                      *
********************************************************************* -}

someTyCoVarsOfType :: (TyCoVar -> Bool) -> Type -> [TyCoVar]
someTyCoVarsOfType :: (Var -> Bool) -> Type -> [Var]
someTyCoVarsOfType Var -> Bool
interesting
  = (Var -> Bool) -> SelectiveDFV -> [Var]
runFVSelectiveList Var -> Bool
interesting (SelectiveDFV -> [Var]) -> (Type -> SelectiveDFV) -> Type -> [Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> SelectiveDFV
shallowSelTypeFV

someTyCoVarsOfTypes :: (TyCoVar -> Bool) -> [Type] -> [TyCoVar]
someTyCoVarsOfTypes :: (Var -> Bool) -> [Type] -> [Var]
someTyCoVarsOfTypes Var -> Bool
interesting
  = (Var -> Bool) -> SelectiveDFV -> [Var]
runFVSelectiveList Var -> Bool
interesting (SelectiveDFV -> [Var])
-> ([Type] -> SelectiveDFV) -> [Type] -> [Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> SelectiveDFV) -> [Type] -> SelectiveDFV
forall (t :: * -> *) acc a env.
(Foldable t, Monoid acc) =>
(a -> FV env acc) -> t a -> FV env acc
mapUnionFV Type -> SelectiveDFV
shallowSelTypeFV

shallowSelTypeFV :: Type -> SelectiveDFV
shallowSelCoFV   :: Coercion -> SelectiveDFV
-- Returns shallow free vars
-- See Note [Shallow and deep free variables]
(Type -> SelectiveDFV
shallowSelTypeFV, [Type] -> SelectiveDFV
_, Coercion -> SelectiveDFV
shallowSelCoFV, [Coercion] -> SelectiveDFV
_) = TyCoFolder SelectiveDFV
-> (Type -> SelectiveDFV, [Type] -> SelectiveDFV,
    Coercion -> SelectiveDFV, [Coercion] -> SelectiveDFV)
forall a.
Monoid a =>
TyCoFolder a
-> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder SelectiveDFV
selectiveTcvFolder

selectiveTcvFolder :: TyCoFolder SelectiveDFV
-- This one takes an `InterestingVarFun`, and returns shallow free vars
-- See `shallowTcvFolder` for the general pattern
selectiveTcvFolder :: TyCoFolder SelectiveDFV
selectiveTcvFolder
  = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view  = Type -> Maybe Type
noView  -- See Note [Free vars and synonyms]
               , tcf_tyvar :: Var -> SelectiveDFV
tcf_tyvar = Var -> SelectiveDFV
do_tcv, tcf_covar :: Var -> SelectiveDFV
tcf_covar = Var -> SelectiveDFV
do_tcv
               , tcf_hole :: CoercionHole -> SelectiveDFV
tcf_hole  = CoercionHole -> SelectiveDFV
do_hole
               , tcf_tycobinder :: Var -> SelectiveDFV -> SelectiveDFV
tcf_tycobinder = Var -> SelectiveDFV -> SelectiveDFV
forall f a. Var -> FV (TyCoVarSet, f) a -> FV (TyCoVarSet, f) a
addBndrSelectiveFV }
  where
    do_tcv :: Var -> SelectiveDFV
do_tcv Var
v = ((TyCoVarSet, Var -> Bool) -> EndoOS DVarSet) -> SelectiveDFV
forall env acc. (env -> acc) -> FV env acc
MkFV (\(TyCoVarSet, Var -> Bool)
env -> (DVarSet -> DVarSet) -> EndoOS DVarSet
forall a. (a -> a) -> EndoOS a
EndoOS ((TyCoVarSet, Var -> Bool) -> DVarSet -> DVarSet
do_it (TyCoVarSet, Var -> Bool)
env))
      where
        do_it :: (TyCoVarSet, Var -> Bool) -> DVarSet -> DVarSet
do_it (TyCoVarSet
bvs,Var -> Bool
is_interesting) DVarSet
acc
          | Var
v Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
bvs     = DVarSet
acc  -- First exclude bound variables
          | Bool -> Bool
not (Var -> Bool
is_interesting Var
v) = DVarSet
acc  -- The "selective" bit
          | Var
v Var -> DVarSet -> Bool
`elemDVarSet` DVarSet
acc    = DVarSet
acc
          | Bool
otherwise              = DVarSet
acc DVarSet -> Var -> DVarSet
`extendDVarSet` Var
v

    do_hole :: CoercionHole -> SelectiveDFV
do_hole CoercionHole
hole = Type -> SelectiveDFV
shallowSelTypeFV (Var -> Type
varType (CoercionHole -> Var
coHoleCoVar CoercionHole
hole))


{- *********************************************************************
*                                                                      *
          Free coercion variables
*                                                                      *
********************************************************************* -}

{- Note [Finding free coercion variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Here we are only interested in the free /coercion/ variables.
We can achieve this through a slightly different TyCo folder.

Notice that

* We look deeply, into kinds.

* We /include/ CoercionHoles. Why?  Specifically because of #14584,
  Note [Emitting the residual implication in simplifyInfer] in GHC.Tc.Solver

See #14880.
-}

-- See Note [Finding free coercion variables]
coVarsOfType  :: Type       -> CoVarSet
coVarsOfTypes :: [Type]     -> CoVarSet
coVarsOfCo    :: Coercion   -> CoVarSet
coVarsOfCos   :: [Coercion] -> CoVarSet

coVarsOfType :: Type -> TyCoVarSet
coVarsOfType  Type
ty  = TyCoFV -> TyCoVarSet
runTyCoVars (Type -> TyCoFV
deepCoVarTypeFV Type
ty)
coVarsOfTypes :: [Type] -> TyCoVarSet
coVarsOfTypes [Type]
tys = TyCoFV -> TyCoVarSet
runTyCoVars ([Type] -> TyCoFV
deepCoVarTypesFV [Type]
tys)
coVarsOfCo :: Coercion -> TyCoVarSet
coVarsOfCo    Coercion
co  = TyCoFV -> TyCoVarSet
runTyCoVars (Coercion -> TyCoFV
deepCoVarCoFV Coercion
co)
coVarsOfCos :: [Coercion] -> TyCoVarSet
coVarsOfCos   [Coercion]
cos = TyCoFV -> TyCoVarSet
runTyCoVars ([Coercion] -> TyCoFV
deepCoVarCosFV [Coercion]
cos)

type CoVarFV  = FV BoundVars (EndoOS CoVarSet)

deepCoVarTypeFV  :: Type       -> CoVarFV
deepCoVarTypesFV :: [Type]     -> CoVarFV
deepCoVarCoFV  :: Coercion   -> CoVarFV
deepCoVarCosFV :: [Coercion] -> CoVarFV
(Type -> TyCoFV
deepCoVarTypeFV, [Type] -> TyCoFV
deepCoVarTypesFV, Coercion -> TyCoFV
deepCoVarCoFV, [Coercion] -> TyCoFV
deepCoVarCosFV) = TyCoFolder TyCoFV
-> (Type -> TyCoFV, [Type] -> TyCoFV, Coercion -> TyCoFV,
    [Coercion] -> TyCoFV)
forall a.
Monoid a =>
TyCoFolder a
-> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder TyCoFV
deepCoVarFolder

deepCoVarFolder :: TyCoFolder CoVarFV
deepCoVarFolder :: TyCoFolder TyCoFV
deepCoVarFolder = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView
                             , tcf_tyvar :: Var -> TyCoFV
tcf_tyvar = Var -> TyCoFV
forall {a} {p}. Monoid a => p -> a
do_tyvar, tcf_covar :: Var -> TyCoFV
tcf_covar = Var -> TyCoFV
do_covar
                             , tcf_hole :: CoercionHole -> TyCoFV
tcf_hole  = CoercionHole -> TyCoFV
do_hole
                             , tcf_tycobinder :: Var -> TyCoFV -> TyCoFV
tcf_tycobinder = Var -> TyCoFV -> TyCoFV
forall a. Var -> FV TyCoVarSet a -> FV TyCoVarSet a
addBndrFV }
  where
    do_tyvar :: p -> a
do_tyvar p
_  = a
forall a. Monoid a => a
mempty
      -- This do_tyvar means we won't see any CoVars in this
      -- TyVar's kind.   This may be wrong; but it's the way it's
      -- always been.  And its awkward to change, because
      -- the tyvar won't end up in the accumulator, so
      -- we'd look repeatedly.  Blargh.

    do_covar :: Var -> TyCoFV
do_covar = (Type -> TyCoFV) -> Var -> TyCoFV
deepUnitFV Type -> TyCoFV
deepCoVarTypeFV

    do_hole :: CoercionHole -> TyCoFV
do_hole CoercionHole
hole  = Var -> TyCoFV
do_covar (CoercionHole -> Var
coHoleCoVar CoercionHole
hole)
      -- We /do/ treat a CoercionHole as a free variable
      -- See Note [CoercionHoles and coercion free variables]

-------------- Deterministic versions ------------------
type DCoVarFV  = FV BoundVars (EndoOS DCoVarSet)

coVarsOfCoDSet :: Coercion -> DCoVarSet
coVarsOfCoDSet :: Coercion -> DVarSet
coVarsOfCoDSet Coercion
co = DCoVarFV -> DVarSet
runTyCoVarsDSet (Coercion -> DCoVarFV
det_co Coercion
co)

coVarsOfCosDSet :: [Coercion] -> DCoVarSet
coVarsOfCosDSet :: [Coercion] -> DVarSet
coVarsOfCosDSet [Coercion]
cos = DCoVarFV -> DVarSet
runTyCoVarsDSet ([Coercion] -> DCoVarFV
det_cos [Coercion]
cos)

det_ty  :: Type       -> DCoVarFV
det_co  :: Coercion   -> DCoVarFV
det_cos :: [Coercion] -> DCoVarFV
(Type -> DCoVarFV
det_ty, [Type] -> DCoVarFV
_, Coercion -> DCoVarFV
det_co, [Coercion] -> DCoVarFV
det_cos) = TyCoFolder DCoVarFV
-> (Type -> DCoVarFV, [Type] -> DCoVarFV, Coercion -> DCoVarFV,
    [Coercion] -> DCoVarFV)
forall a.
Monoid a =>
TyCoFolder a
-> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder DCoVarFV
deepDetCoVarFolder

deepDetCoVarFolder :: TyCoFolder DCoVarFV
-- Follows deepCoVarFolders, but returns a /deterministic/ set
deepDetCoVarFolder :: TyCoFolder DCoVarFV
deepDetCoVarFolder = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView
                                , tcf_tyvar :: Var -> DCoVarFV
tcf_tyvar = Var -> DCoVarFV
forall {a} {p}. Monoid a => p -> a
do_tyvar
                                , tcf_covar :: Var -> DCoVarFV
tcf_covar = Var -> DCoVarFV
do_covar
                                , tcf_hole :: CoercionHole -> DCoVarFV
tcf_hole  = CoercionHole -> DCoVarFV
do_hole
                                , tcf_tycobinder :: Var -> DCoVarFV -> DCoVarFV
tcf_tycobinder = Var -> DCoVarFV -> DCoVarFV
forall a. Var -> FV TyCoVarSet a -> FV TyCoVarSet a
addBndrFV }
  where
    do_tyvar :: p -> a
do_tyvar p
_  = a
forall a. Monoid a => a
mempty

    do_covar :: CoVar -> DCoVarFV
    do_covar :: Var -> DCoVarFV
do_covar = (Type -> DCoVarFV) -> Var -> DCoVarFV
deepDetUnitFV Type -> DCoVarFV
det_ty

    do_hole :: CoercionHole -> DCoVarFV
do_hole CoercionHole
hole  = Var -> DCoVarFV
do_covar (CoercionHole -> Var
coHoleCoVar CoercionHole
hole)


{- *********************************************************************
*                                                                      *
          Closing over kinds
*                                                                      *
********************************************************************* -}

closeOverKinds :: TyCoVarSet -> TyCoVarSet
-- For each element of the input set,
-- add the deep free variables of its kind
closeOverKinds :: TyCoVarSet -> TyCoVarSet
closeOverKinds TyCoVarSet
vs = (Var -> TyCoVarSet -> TyCoVarSet)
-> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
forall a. (Var -> a -> a) -> a -> TyCoVarSet -> a
nonDetStrictFoldVarSet Var -> TyCoVarSet -> TyCoVarSet
do_one TyCoVarSet
vs TyCoVarSet
vs
  where
    do_one :: Var -> TyCoVarSet -> TyCoVarSet
do_one Var
v = TyCoFV -> TyCoVarSet -> TyCoVarSet
forall a. FV TyCoVarSet (EndoOS a) -> a -> a
runFVAcc (Type -> TyCoFV
deepTypeFV (Var -> Type
varType Var
v))

-- | Add the kind variables free in the kinds of the tyvars in the given set.
-- Returns a deterministic set.
closeOverKindsDSet :: DTyVarSet -> DTyVarSet
closeOverKindsDSet :: DVarSet -> DVarSet
closeOverKindsDSet DVarSet
vs = (Var -> DVarSet -> DVarSet) -> DVarSet -> DVarSet -> DVarSet
forall a. (Var -> a -> a) -> a -> DVarSet -> a
nonDetStrictFoldDVarSet Var -> DVarSet -> DVarSet
do_one DVarSet
vs DVarSet
vs
  where
    do_one :: Var -> DVarSet -> DVarSet
do_one Var
v = DCoVarFV -> DVarSet -> DVarSet
forall a. FV TyCoVarSet (EndoOS a) -> a -> a
runFVAcc (Type -> DCoVarFV
deepDetTypeFV (Var -> Type
varType Var
v))


{-
%************************************************************************
%*                                                                      *
        almostDevoidCoVarOfCo
%*                                                                      *
%************************************************************************
-}

----- Whether a covar is /Almost Devoid/ in a type or coercion ----

-- | Given a covar and a coercion, returns True if covar is almost devoid in
-- the coercion. That is, covar can only appear in Refl and GRefl.
-- See (FC6) in Note [ForAllCo] in "GHC.Core.TyCo.Rep"
almostDevoidCoVarOfCo :: CoVar -> Coercion -> Bool
almostDevoidCoVarOfCo :: Var -> Coercion -> Bool
almostDevoidCoVarOfCo Var
cv Coercion
co =
  Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
co Var
cv

almost_devoid_co_var_of_mco :: MCoercion -> CoVar -> Bool
almost_devoid_co_var_of_mco :: MCoercion -> Var -> Bool
almost_devoid_co_var_of_mco MCoercion
MRefl    Var
_  = Bool
True
almost_devoid_co_var_of_mco (MCo Coercion
co) Var
cv = Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
co Var
cv

almost_devoid_co_var_of_co :: Coercion -> CoVar -> Bool
almost_devoid_co_var_of_co :: Coercion -> Var -> Bool
almost_devoid_co_var_of_co (Refl {}) Var
_ = Bool
True   -- covar is allowed in Refl and
almost_devoid_co_var_of_co (GRefl {}) Var
_ = Bool
True  -- GRefl, so we don't look into
                                                -- the coercions
almost_devoid_co_var_of_co (TyConAppCo Role
_ TyCon
_ [Coercion]
cos) Var
cv
  = [Coercion] -> Var -> Bool
almost_devoid_co_var_of_cos [Coercion]
cos Var
cv
almost_devoid_co_var_of_co (AppCo Coercion
co Coercion
arg) Var
cv
  = Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
co Var
cv
  Bool -> Bool -> Bool
&& Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
arg Var
cv
almost_devoid_co_var_of_co (ForAllCo { fco_tcv :: Coercion -> Var
fco_tcv = Var
v, fco_kind :: Coercion -> MCoercion
fco_kind = MCoercion
kind_co, fco_body :: Coercion -> Coercion
fco_body = Coercion
co }) Var
cv
  = MCoercion -> Var -> Bool
almost_devoid_co_var_of_mco MCoercion
kind_co Var
cv
  Bool -> Bool -> Bool
&& (Var
v Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
cv Bool -> Bool -> Bool
|| Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
co Var
cv)
almost_devoid_co_var_of_co (FunCo { fco_mult :: Coercion -> Coercion
fco_mult = Coercion
w, fco_arg :: Coercion -> Coercion
fco_arg = Coercion
co1, fco_res :: Coercion -> Coercion
fco_res = Coercion
co2 }) Var
cv
  =  Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
w   Var
cv
  Bool -> Bool -> Bool
&& Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
co1 Var
cv
  Bool -> Bool -> Bool
&& Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
co2 Var
cv
almost_devoid_co_var_of_co (CoVarCo Var
v) Var
cv = Var
v Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
/= Var
cv
almost_devoid_co_var_of_co (HoleCo CoercionHole
h)  Var
cv = (CoercionHole -> Var
coHoleCoVar CoercionHole
h) Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
/= Var
cv
almost_devoid_co_var_of_co (AxiomCo CoAxiomRule
_ [Coercion]
cs) Var
cv
  = [Coercion] -> Var -> Bool
almost_devoid_co_var_of_cos [Coercion]
cs Var
cv
almost_devoid_co_var_of_co (UnivCo { uco_lty :: Coercion -> Type
uco_lty = Type
t1, uco_rty :: Coercion -> Type
uco_rty = Type
t2, uco_deps :: Coercion -> [Coercion]
uco_deps = [Coercion]
deps }) Var
cv
  =  [Coercion] -> Var -> Bool
almost_devoid_co_var_of_cos [Coercion]
deps Var
cv
  Bool -> Bool -> Bool
&& Type -> Var -> Bool
almost_devoid_co_var_of_type Type
t1 Var
cv
  Bool -> Bool -> Bool
&& Type -> Var -> Bool
almost_devoid_co_var_of_type Type
t2 Var
cv
almost_devoid_co_var_of_co (SymCo Coercion
co) Var
cv
  = Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
co Var
cv
almost_devoid_co_var_of_co (TransCo Coercion
co1 Coercion
co2) Var
cv
  = Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
co1 Var
cv
  Bool -> Bool -> Bool
&& Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
co2 Var
cv
almost_devoid_co_var_of_co (SelCo CoSel
_ Coercion
co) Var
cv
  = Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
co Var
cv
almost_devoid_co_var_of_co (LRCo LeftOrRight
_ Coercion
co) Var
cv
  = Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
co Var
cv
almost_devoid_co_var_of_co (InstCo Coercion
co Coercion
arg) Var
cv
  = Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
co Var
cv
  Bool -> Bool -> Bool
&& Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
arg Var
cv
almost_devoid_co_var_of_co (KindCo Coercion
co) Var
cv
  = Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
co Var
cv
almost_devoid_co_var_of_co (SubCo Coercion
co) Var
cv
  = Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
co Var
cv

almost_devoid_co_var_of_cos :: [Coercion] -> CoVar -> Bool
almost_devoid_co_var_of_cos :: [Coercion] -> Var -> Bool
almost_devoid_co_var_of_cos [] Var
_ = Bool
True
almost_devoid_co_var_of_cos (Coercion
co:[Coercion]
cos) Var
cv
  = Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
co Var
cv
  Bool -> Bool -> Bool
&& [Coercion] -> Var -> Bool
almost_devoid_co_var_of_cos [Coercion]
cos Var
cv

almost_devoid_co_var_of_type :: Type -> CoVar -> Bool
almost_devoid_co_var_of_type :: Type -> Var -> Bool
almost_devoid_co_var_of_type (TyVarTy Var
_) Var
_ = Bool
True
almost_devoid_co_var_of_type (TyConApp TyCon
_ [Type]
tys) Var
cv
  = [Type] -> Var -> Bool
almost_devoid_co_var_of_types [Type]
tys Var
cv
almost_devoid_co_var_of_type (LitTy {}) Var
_ = Bool
True
almost_devoid_co_var_of_type (AppTy Type
fun Type
arg) Var
cv
  = Type -> Var -> Bool
almost_devoid_co_var_of_type Type
fun Var
cv
  Bool -> Bool -> Bool
&& Type -> Var -> Bool
almost_devoid_co_var_of_type Type
arg Var
cv
almost_devoid_co_var_of_type (FunTy FunTyFlag
_ Type
w Type
arg Type
res) Var
cv
  = Type -> Var -> Bool
almost_devoid_co_var_of_type Type
w Var
cv
  Bool -> Bool -> Bool
&& Type -> Var -> Bool
almost_devoid_co_var_of_type Type
arg Var
cv
  Bool -> Bool -> Bool
&& Type -> Var -> Bool
almost_devoid_co_var_of_type Type
res Var
cv
almost_devoid_co_var_of_type (ForAllTy (Bndr Var
v ForAllTyFlag
_) Type
ty) Var
cv
  = Type -> Var -> Bool
almost_devoid_co_var_of_type (Var -> Type
varType Var
v) Var
cv
  Bool -> Bool -> Bool
&& (Var
v Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
cv Bool -> Bool -> Bool
|| Type -> Var -> Bool
almost_devoid_co_var_of_type Type
ty Var
cv)
almost_devoid_co_var_of_type (CastTy Type
ty Coercion
co) Var
cv
  = Type -> Var -> Bool
almost_devoid_co_var_of_type Type
ty Var
cv
  Bool -> Bool -> Bool
&& Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
co Var
cv
almost_devoid_co_var_of_type (CoercionTy Coercion
co) Var
cv
  = Coercion -> Var -> Bool
almost_devoid_co_var_of_co Coercion
co Var
cv

almost_devoid_co_var_of_types :: [Type] -> CoVar -> Bool
almost_devoid_co_var_of_types :: [Type] -> Var -> Bool
almost_devoid_co_var_of_types [] Var
_ = Bool
True
almost_devoid_co_var_of_types (Type
ty:[Type]
tys) Var
cv
  = Type -> Var -> Bool
almost_devoid_co_var_of_type Type
ty Var
cv
  Bool -> Bool -> Bool
&& [Type] -> Var -> Bool
almost_devoid_co_var_of_types [Type]
tys Var
cv



{-
%************************************************************************
%*                                                                      *
        Free tyvars, but with visible/invisible info
%*                                                                      *
%************************************************************************

-}
-- | Retrieve the free variables in this type, splitting them based
-- on whether they are used visibly or invisibly. Invisible ones come
-- first.
visVarsOfType :: Type -> Pair TyCoVarSet
visVarsOfType :: Type -> Pair TyCoVarSet
visVarsOfType Type
orig_ty = TyCoVarSet -> TyCoVarSet -> Pair TyCoVarSet
forall a. a -> a -> Pair a
Pair TyCoVarSet
invis_vars TyCoVarSet
vis_vars
  where
    Pair TyCoVarSet
invis_vars1 TyCoVarSet
vis_vars = Type -> Pair TyCoVarSet
go Type
orig_ty
    invis_vars :: TyCoVarSet
invis_vars = TyCoVarSet
invis_vars1 TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`minusVarSet` TyCoVarSet
vis_vars

    go :: Type -> Pair TyCoVarSet
go (TyVarTy Var
tv)      = TyCoVarSet -> TyCoVarSet -> Pair TyCoVarSet
forall a. a -> a -> Pair a
Pair (Type -> TyCoVarSet
tyCoVarsOfType (Type -> TyCoVarSet) -> Type -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$ Var -> Type
tyVarKind Var
tv) (Var -> TyCoVarSet
unitVarSet Var
tv)
    go (AppTy Type
t1 Type
t2)     = Type -> Pair TyCoVarSet
go Type
t1 Pair TyCoVarSet -> Pair TyCoVarSet -> Pair TyCoVarSet
forall a. Monoid a => a -> a -> a
`mappend` Type -> Pair TyCoVarSet
go Type
t2
    go (TyConApp TyCon
tc [Type]
tys) = TyCon -> [Type] -> Pair TyCoVarSet
go_tc TyCon
tc [Type]
tys
    go (FunTy FunTyFlag
_ Type
w Type
t1 Type
t2) = Type -> Pair TyCoVarSet
go Type
w Pair TyCoVarSet -> Pair TyCoVarSet -> Pair TyCoVarSet
forall a. Monoid a => a -> a -> a
`mappend` Type -> Pair TyCoVarSet
go Type
t1 Pair TyCoVarSet -> Pair TyCoVarSet -> Pair TyCoVarSet
forall a. Monoid a => a -> a -> a
`mappend` Type -> Pair TyCoVarSet
go Type
t2
    go (ForAllTy (Bndr Var
tv ForAllTyFlag
_) Type
ty)
      = ((TyCoVarSet -> Var -> TyCoVarSet
`delVarSet` Var
tv) (TyCoVarSet -> TyCoVarSet) -> Pair TyCoVarSet -> Pair TyCoVarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Pair TyCoVarSet
go Type
ty) Pair TyCoVarSet -> Pair TyCoVarSet -> Pair TyCoVarSet
forall a. Monoid a => a -> a -> a
`mappend`
        (TyCoVarSet -> Pair TyCoVarSet
invisible (Type -> TyCoVarSet
tyCoVarsOfType (Type -> TyCoVarSet) -> Type -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
tv))
    go (LitTy {}) = Pair TyCoVarSet
forall a. Monoid a => a
mempty
    go (CastTy Type
ty Coercion
co) = Type -> Pair TyCoVarSet
go Type
ty Pair TyCoVarSet -> Pair TyCoVarSet -> Pair TyCoVarSet
forall a. Monoid a => a -> a -> a
`mappend` TyCoVarSet -> Pair TyCoVarSet
invisible (Coercion -> TyCoVarSet
tyCoVarsOfCo Coercion
co)
    go (CoercionTy Coercion
co) = TyCoVarSet -> Pair TyCoVarSet
invisible (TyCoVarSet -> Pair TyCoVarSet) -> TyCoVarSet -> Pair TyCoVarSet
forall a b. (a -> b) -> a -> b
$ Coercion -> TyCoVarSet
tyCoVarsOfCo Coercion
co

    invisible :: TyCoVarSet -> Pair TyCoVarSet
invisible TyCoVarSet
vs = TyCoVarSet -> TyCoVarSet -> Pair TyCoVarSet
forall a. a -> a -> Pair a
Pair TyCoVarSet
vs TyCoVarSet
emptyVarSet

    go_tc :: TyCon -> [Type] -> Pair TyCoVarSet
go_tc TyCon
tc [Type]
tys = let ([Type]
invis, [Type]
vis) = TyCon -> [Type] -> ([Type], [Type])
partitionInvisibleTypes TyCon
tc [Type]
tys in
                   TyCoVarSet -> Pair TyCoVarSet
invisible ([Type] -> TyCoVarSet
tyCoVarsOfTypes [Type]
invis) Pair TyCoVarSet -> Pair TyCoVarSet -> Pair TyCoVarSet
forall a. Monoid a => a -> a -> a
`mappend` (Type -> Pair TyCoVarSet) -> [Type] -> Pair TyCoVarSet
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> Pair TyCoVarSet
go [Type]
vis

visVarsOfTypes :: [Type] -> Pair TyCoVarSet
visVarsOfTypes :: [Type] -> Pair TyCoVarSet
visVarsOfTypes = (Type -> Pair TyCoVarSet) -> [Type] -> Pair TyCoVarSet
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> Pair TyCoVarSet
visVarsOfType


{- *********************************************************************
*                                                                      *
                 Injective free vars
*                                                                      *
********************************************************************* -}

isInjectiveInType :: TyVar -> Type -> Bool
-- True <=> tv /definitely/ appears injectively in ty
-- A bit more efficient that (tv `elemVarSet` injectiveTyVarsOfType ty)
-- Ignore occurrence in coercions, and even in injective positions of
-- type families.
isInjectiveInType :: Var -> Type -> Bool
isInjectiveInType Var
tv Type
ty
  = Type -> Bool
go Type
ty
  where
    go :: Type -> Bool
go Type
ty | Just Type
ty' <- Type -> Maybe Type
rewriterView Type
ty = Type -> Bool
go Type
ty'
    go (TyVarTy Var
tv')                    = Var
tv' Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
tv
    go (AppTy Type
f Type
a)                      = Type -> Bool
go Type
f Bool -> Bool -> Bool
|| Type -> Bool
go Type
a
    go (FunTy FunTyFlag
_ Type
w Type
ty1 Type
ty2)              = Type -> Bool
go Type
w Bool -> Bool -> Bool
|| Type -> Bool
go Type
ty1 Bool -> Bool -> Bool
|| Type -> Bool
go Type
ty2
    go (TyConApp TyCon
tc [Type]
tys)                = TyCon -> [Type] -> Bool
go_tc TyCon
tc [Type]
tys
    go (ForAllTy (Bndr Var
tv' ForAllTyFlag
_) Type
ty)       = Type -> Bool
go (Var -> Type
tyVarKind Var
tv')
                                          Bool -> Bool -> Bool
|| (Var
tv Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
/= Var
tv' Bool -> Bool -> Bool
&& Type -> Bool
go Type
ty)
    go LitTy{}                          = Bool
False
    go (CastTy Type
ty Coercion
_)                    = Type -> Bool
go Type
ty
    go CoercionTy{}                     = Bool
False

    go_tc :: TyCon -> [Type] -> Bool
go_tc TyCon
tc [Type]
tys | TyCon -> Bool
isTypeFamilyTyCon TyCon
tc = Bool
False
                 | Bool
otherwise            = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Type -> Bool
go [Type]
tys

-- | Returns the free variables of a 'Type' that are in injective positions.
-- Specifically, it finds the free variables while:
--
-- * Expanding type synonyms
--
-- * Ignoring the coercion in @(ty |> co)@
--
-- * Ignoring the non-injective fields of a 'TyConApp'
--
--
-- For example, if @F@ is a non-injective type family, then:
--
-- @
-- injectiveTyVarsOf( Either c (Maybe (a, F b c)) ) = {a,c}
-- @
--
-- If @'injectiveVarsOfType' ty = itvs@, then knowing @ty@ fixes @itvs@.
-- More formally, if
-- @a@ is in @'injectiveVarsOfType' ty@
-- and  @S1(ty) ~ S2(ty)@,
-- then @S1(a)  ~ S2(a)@,
-- where @S1@ and @S2@ are arbitrary substitutions.
--
-- See @Note [When does a tycon application need an explicit kind signature?]@.
injectiveVarsOfType :: Bool   -- ^ Should we look under injective type families?
                              -- See Note [Coverage condition for injective type families]
                              -- in "GHC.Tc.Instance.Family".
                    -> Type -> VarSet
injectiveVarsOfType :: Bool -> Type -> TyCoVarSet
injectiveVarsOfType Bool
look_under_tfs Type
ty = TyCoFV -> TyCoVarSet
runTyCoVars (Bool -> Type -> TyCoFV
inj_vars_of_type Bool
look_under_tfs Type
ty)

-- | Returns the free variables of a 'Type' that are in injective positions.
-- Specifically, it finds the free variables while:
--
-- * Expanding type synonyms
--
-- * Ignoring the coercion in @(ty |> co)@
--
-- * Ignoring the non-injective fields of a 'TyConApp'
--
-- See @Note [When does a tycon application need an explicit kind signature?]@.
injectiveVarsOfTypes :: Bool -- ^ look under injective type families?
                             -- See Note [Coverage condition for injective type families]
                             -- in "GHC.Tc.Instance.Family".
                     -> [Type] -> VarSet
injectiveVarsOfTypes :: Bool -> [Type] -> TyCoVarSet
injectiveVarsOfTypes Bool
look_under_tfs [Type]
tys
  = TyCoFV -> TyCoVarSet
runTyCoVars (TyCoFV -> TyCoVarSet) -> TyCoFV -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$ (Type -> TyCoFV) -> [Type] -> TyCoFV
forall (t :: * -> *) acc a env.
(Foldable t, Monoid acc) =>
(a -> FV env acc) -> t a -> FV env acc
mapUnionFV (Bool -> Type -> TyCoFV
inj_vars_of_type Bool
look_under_tfs) [Type]
tys

inj_vars_of_type :: Bool -> Type -> TyCoFV
inj_vars_of_type :: Bool -> Type -> TyCoFV
inj_vars_of_type Bool
look_under_tfs = Type -> TyCoFV
go
  where
    go :: Type -> TyCoFV
go Type
ty | Just Type
ty' <- Type -> Maybe Type
rewriterView Type
ty = Type -> TyCoFV
go Type
ty'
    go (TyVarTy Var
v)                      = (Type -> TyCoFV) -> Var -> TyCoFV
deepUnitFV Type -> TyCoFV
go Var
v
    go (AppTy Type
f Type
a)                      = Type -> TyCoFV
go Type
f TyCoFV -> TyCoFV -> TyCoFV
forall a. Monoid a => a -> a -> a
`mappend` Type -> TyCoFV
go Type
a
    go (FunTy FunTyFlag
_ Type
w Type
ty1 Type
ty2)              = Type -> TyCoFV
go Type
w TyCoFV -> TyCoFV -> TyCoFV
forall a. Monoid a => a -> a -> a
`mappend` Type -> TyCoFV
go Type
ty1 TyCoFV -> TyCoFV -> TyCoFV
forall a. Monoid a => a -> a -> a
`mappend` Type -> TyCoFV
go Type
ty2
    go (TyConApp TyCon
tc [Type]
tys)                = TyCon -> [Type] -> TyCoFV
go_tc TyCon
tc [Type]
tys
    go (ForAllTy (Bndr Var
tv ForAllTyFlag
_) Type
ty)        = Type -> TyCoFV
go (Var -> Type
tyVarKind Var
tv) TyCoFV -> TyCoFV -> TyCoFV
forall a. Monoid a => a -> a -> a
`mappend`
                                          Var -> TyCoFV -> TyCoFV
forall a. Var -> FV TyCoVarSet a -> FV TyCoVarSet a
addBndrFV Var
tv (Type -> TyCoFV
go Type
ty)
    go LitTy{}                          = TyCoFV
forall a. Monoid a => a
mempty
    go (CastTy Type
ty Coercion
_)                    = Type -> TyCoFV
go Type
ty
    go CoercionTy{}                     = TyCoFV
forall a. Monoid a => a
mempty

    go_tc :: TyCon -> [Type] -> TyCoFV
go_tc TyCon
tc [Type]
tys
      | TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
      = if | Bool
look_under_tfs
           , Injective [Bool]
flags <- TyCon -> Injectivity
tyConInjectivityInfo TyCon
tc
           -> (Type -> TyCoFV) -> [Type] -> TyCoFV
forall (t :: * -> *) acc a env.
(Foldable t, Monoid acc) =>
(a -> FV env acc) -> t a -> FV env acc
mapUnionFV Type -> TyCoFV
go ([Type] -> TyCoFV) -> [Type] -> TyCoFV
forall a b. (a -> b) -> a -> b
$
              [Bool] -> [Type] -> [Type]
forall a. [Bool] -> [a] -> [a]
filterByList ([Bool]
flags [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Bool -> [Bool]
forall a. a -> [a]
repeat Bool
True) [Type]
tys
                         -- Oversaturated arguments to a tycon are
                         -- always injective, hence the repeat True
           | Bool
otherwise   -- No injectivity info for this type family
           -> TyCoFV
forall a. Monoid a => a
mempty

      | Bool
otherwise        -- Data type, injective in all positions
      = (Type -> TyCoFV) -> [Type] -> TyCoFV
forall (t :: * -> *) acc a env.
(Foldable t, Monoid acc) =>
(a -> FV env acc) -> t a -> FV env acc
mapUnionFV Type -> TyCoFV
go [Type]
tys



{- *********************************************************************
*                                                                      *
                 Invisible vars
*                                                                      *
********************************************************************* -}


-- | Returns the set of variables that are used invisibly anywhere within
-- the given type. A variable will be included even if it is used both visibly
-- and invisibly. An "invisible" use site includes:
--   * In the kind of a variable
--   * In the kind of a bound variable in a forall
--   * In a coercion
--   * In a Specified or Inferred argument to a function
-- See Note [VarBndrs, ForAllTyBinders, TyConBinders, and visibility] in "GHC.Core.TyCo.Rep"
invisibleVarsOfType :: Type -> VarSet
invisibleVarsOfType :: Type -> TyCoVarSet
invisibleVarsOfType = Type -> TyCoVarSet
go
  where
    go :: Type -> TyCoVarSet
go Type
ty                  | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty
                           = Type -> TyCoVarSet
go Type
ty'
    go (TyVarTy Var
v)         = Type -> TyCoVarSet
go (Var -> Type
tyVarKind Var
v)
    go (AppTy Type
f Type
a)         = Type -> TyCoVarSet
go Type
f TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
go Type
a
    go (FunTy FunTyFlag
_ Type
w Type
ty1 Type
ty2) = Type -> TyCoVarSet
go Type
ty1 TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
go Type
w TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
go Type
ty2
                             -- As per #23764, order is: arg, mult, res.
    go (TyConApp TyCon
tc [Type]
tys)   = [Type] -> TyCoVarSet
tyCoVarsOfTypes [Type]
invisibles TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet`
                             [Type] -> TyCoVarSet
invisibleVarsOfTypes [Type]
visibles
      where ([Type]
invisibles, [Type]
visibles) = TyCon -> [Type] -> ([Type], [Type])
partitionInvisibleTypes TyCon
tc [Type]
tys
    go (ForAllTy (Bndr Var
var ForAllTyFlag
_) Type
ty)
      = Type -> TyCoVarSet
tyCoVarsOfType (Var -> Type
varType Var
var) TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` (Type -> TyCoVarSet
go Type
ty TyCoVarSet -> Var -> TyCoVarSet
`delVarSet` Var
var)
    go LitTy{}             = TyCoVarSet
emptyVarSet
    go (CastTy Type
ty Coercion
co)      = Coercion -> TyCoVarSet
tyCoVarsOfCo Coercion
co TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
go Type
ty
    go (CoercionTy Coercion
co)     = Coercion -> TyCoVarSet
tyCoVarsOfCo Coercion
co

-- | Like 'invisibleVarsOfType', but for many types.
invisibleVarsOfTypes :: [Type] -> VarSet
invisibleVarsOfTypes :: [Type] -> TyCoVarSet
invisibleVarsOfTypes = (Type -> TyCoVarSet -> TyCoVarSet)
-> TyCoVarSet -> [Type] -> TyCoVarSet
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (TyCoVarSet -> TyCoVarSet -> TyCoVarSet
unionVarSet (TyCoVarSet -> TyCoVarSet -> TyCoVarSet)
-> (Type -> TyCoVarSet) -> Type -> TyCoVarSet -> TyCoVarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TyCoVarSet
invisibleVarsOfType) TyCoVarSet
emptyVarSet


{- *********************************************************************
*                                                                      *
                 Any free vars
*                                                                      *
********************************************************************* -}

{- Note [Any-free-var folder]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "any-free-var" folders take a `check_fv` predicate (TyCoVar -> Bool) and
check if any /deep/ free variable of the type/coercion satisfies it. So

   anyFreeVarsOfType p ty = anyVarSet p (tyCoVarsOfType ty)

Our main folders look like:

   afv_type :: Type -> FV (BoundVars, TyVar -> Bool) Any

where we cleverly pair the predicate with the forall-bound variables of the type
in the "env" field of (FV env Any).  This way we can build the /folder/ once and
for all (independent of the `check_fv` predicate), and the loop passes down
the pair.

The same idiom is used in `exprFreeVarsDSet` and friends.

However we are careful to INLINE `atvFolder` and `runAny` so that we get those
nice tight loops.
-}

{-# INLINE afvFolder #-}   -- See Note [Any-free-var folder]
afvFolder :: TyCoFolder (FV (BoundVars, TyCoVar -> Bool) DM.Any)
-- 'afvFolder' is short for "any-free-var folder", good for checking
--   if any /shallow/ free var of a type satisfies a predicate `check_fv`
-- The "env" of the (FV env Any) is a pair (bvs,pred) of
--    the bound variables (which are definitely not free), and
--    an "interesting var" predicate which the client supplies
--
-- You can get "deep" by supplying a predicate that also looks in the kind
afvFolder :: TyCoFolder (FV (TyCoVarSet, Var -> Bool) Any)
afvFolder = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView  -- See Note [Free vars and synonyms]
                       , tcf_tyvar :: Var -> FV (TyCoVarSet, Var -> Bool) Any
tcf_tyvar = Var -> FV (TyCoVarSet, Var -> Bool) Any
do_tcv
                       , tcf_covar :: Var -> FV (TyCoVarSet, Var -> Bool) Any
tcf_covar = Var -> FV (TyCoVarSet, Var -> Bool) Any
do_tcv
                       , tcf_hole :: CoercionHole -> FV (TyCoVarSet, Var -> Bool) Any
tcf_hole  = CoercionHole -> FV (TyCoVarSet, Var -> Bool) Any
do_hole
                       , tcf_tycobinder :: Var
-> FV (TyCoVarSet, Var -> Bool) Any
-> FV (TyCoVarSet, Var -> Bool) Any
tcf_tycobinder = Var
-> FV (TyCoVarSet, Var -> Bool) Any
-> FV (TyCoVarSet, Var -> Bool) Any
forall f a. Var -> FV (TyCoVarSet, f) a -> FV (TyCoVarSet, f) a
addBndrSelectiveFV }
  where
    -- Check the variable itself with check_fv,
    -- and check its kind (this is a deep folder)
    do_tcv :: Var -> FV (TyCoVarSet, Var -> Bool) Any
do_tcv Var
tcv = ((TyCoVarSet, Var -> Bool) -> Any)
-> FV (TyCoVarSet, Var -> Bool) Any
forall env acc. (env -> acc) -> FV env acc
MkFV (((TyCoVarSet, Var -> Bool) -> Any)
 -> FV (TyCoVarSet, Var -> Bool) Any)
-> ((TyCoVarSet, Var -> Bool) -> Any)
-> FV (TyCoVarSet, Var -> Bool) Any
forall a b. (a -> b) -> a -> b
$ \ (TyCoVarSet
bvs,Var -> Bool
check_fv) ->
                 Bool -> Any
Any (Bool -> Bool
not (Var
tcv Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
bvs) Bool -> Bool -> Bool
&& Var -> Bool
check_fv Var
tcv)
    do_hole :: CoercionHole -> FV (TyCoVarSet, Var -> Bool) Any
do_hole CoercionHole
hole = Var -> FV (TyCoVarSet, Var -> Bool) Any
do_tcv (CoercionHole -> Var
coHoleCoVar CoercionHole
hole)

afv_type  :: Type     -> FV (BoundVars, TyVar -> Bool) DM.Any
afv_types :: [Type]   -> FV (BoundVars, TyVar -> Bool) DM.Any
afv_co    :: Coercion -> FV (BoundVars, TyVar -> Bool) DM.Any
(Type -> FV (TyCoVarSet, Var -> Bool) Any
afv_type, [Type] -> FV (TyCoVarSet, Var -> Bool) Any
afv_types, Coercion -> FV (TyCoVarSet, Var -> Bool) Any
afv_co, [Coercion] -> FV (TyCoVarSet, Var -> Bool) Any
_) = TyCoFolder (FV (TyCoVarSet, Var -> Bool) Any)
-> (Type -> FV (TyCoVarSet, Var -> Bool) Any,
    [Type] -> FV (TyCoVarSet, Var -> Bool) Any,
    Coercion -> FV (TyCoVarSet, Var -> Bool) Any,
    [Coercion] -> FV (TyCoVarSet, Var -> Bool) Any)
forall a.
Monoid a =>
TyCoFolder a
-> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder (FV (TyCoVarSet, Var -> Bool) Any)
afvFolder

runAny :: (TyVar -> Bool) -> FV (BoundVars, TyCoVar -> Bool) DM.Any -> Bool
{-# INLINE runAny #-}
runAny :: (Var -> Bool) -> FV (TyCoVarSet, Var -> Bool) Any -> Bool
runAny Var -> Bool
check_fv FV (TyCoVarSet, Var -> Bool) Any
fvs = Any -> Bool
DM.getAny (FV (TyCoVarSet, Var -> Bool) Any
-> (TyCoVarSet, Var -> Bool) -> Any
forall env acc. FV env acc -> env -> acc
runFV FV (TyCoVarSet, Var -> Bool) Any
fvs (TyCoVarSet
emptyVarSet, Var -> Bool
check_fv))

---------------------------------------------
-- anyShallowFreeVarsOfType and friends look only for shallow free vars
--    (Currently not needed, left here in case we need it one day)
-- anyShallowFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool
-- {-# INLINE anyShallowFreeVarsOfType #-}
-- anyShallowFreeVarsOfType check_fv ty = runAny check_fv (afv_type ty)

---------------------------------------------
-- anyFreeVarsOfType and friends look for deep free vars

deep_check :: (TyCoVar -> Bool) -> TyCoVar -> Bool
-- This is inefficient because if one tyvar occurs many times
-- in a type, it'll look in its kind at each occurrence. Boo.
deep_check :: (Var -> Bool) -> Var -> Bool
deep_check Var -> Bool
check_fv Var
tcv = Var -> Bool
check_fv Var
tcv Bool -> Bool -> Bool
|| (Var -> Bool) -> Type -> Bool
anyFreeVarsOfType Var -> Bool
check_fv (Var -> Type
varType Var
tcv)

anyFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool
{-# INLINE anyFreeVarsOfType #-}
-- Looks deeply, into the kinds of the free vars
anyFreeVarsOfType :: (Var -> Bool) -> Type -> Bool
anyFreeVarsOfType Var -> Bool
check_fv Type
ty = (Var -> Bool) -> FV (TyCoVarSet, Var -> Bool) Any -> Bool
runAny ((Var -> Bool) -> Var -> Bool
deep_check Var -> Bool
check_fv) (Type -> FV (TyCoVarSet, Var -> Bool) Any
afv_type Type
ty)

anyFreeVarsOfTypes :: (TyCoVar -> Bool) -> [Type] -> Bool
{-# INLINE anyFreeVarsOfTypes #-}
anyFreeVarsOfTypes :: (Var -> Bool) -> [Type] -> Bool
anyFreeVarsOfTypes Var -> Bool
check_fv [Type]
tys = (Var -> Bool) -> FV (TyCoVarSet, Var -> Bool) Any -> Bool
runAny ((Var -> Bool) -> Var -> Bool
deep_check Var -> Bool
check_fv) ([Type] -> FV (TyCoVarSet, Var -> Bool) Any
afv_types [Type]
tys)

anyFreeVarsOfCo :: (TyCoVar -> Bool) -> Coercion -> Bool
anyFreeVarsOfCo :: (Var -> Bool) -> Coercion -> Bool
anyFreeVarsOfCo Var -> Bool
check_fv Coercion
co = (Var -> Bool) -> FV (TyCoVarSet, Var -> Bool) Any -> Bool
runAny ((Var -> Bool) -> Var -> Bool
deep_check Var -> Bool
check_fv) (Coercion -> FV (TyCoVarSet, Var -> Bool) Any
afv_co Coercion
co)

noFreeVarsOfType :: Type -> Bool
noFreeVarsOfType :: Type -> Bool
noFreeVarsOfType Type
ty = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Var -> Bool) -> FV (TyCoVarSet, Var -> Bool) Any -> Bool
runAny (Bool -> Var -> Bool
forall a b. a -> b -> a
const Bool
True) (Type -> FV (TyCoVarSet, Var -> Bool) Any
afv_type Type
ty)

noFreeVarsOfTypes :: [Type] -> Bool
noFreeVarsOfTypes :: [Type] -> Bool
noFreeVarsOfTypes [Type]
tys = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Var -> Bool) -> FV (TyCoVarSet, Var -> Bool) Any -> Bool
runAny (Bool -> Var -> Bool
forall a b. a -> b -> a
const Bool
True) ([Type] -> FV (TyCoVarSet, Var -> Bool) Any
afv_types [Type]
tys)

noFreeVarsOfCo :: Coercion -> Bool
noFreeVarsOfCo :: Coercion -> Bool
noFreeVarsOfCo Coercion
co = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Var -> Bool) -> FV (TyCoVarSet, Var -> Bool) Any -> Bool
runAny (Bool -> Var -> Bool
forall a b. a -> b -> a
const Bool
True) (Coercion -> FV (TyCoVarSet, Var -> Bool) Any
afv_co Coercion
co)


{-
************************************************************************
*                                                                      *
            Free type constructors
*                                                                      *
************************************************************************
-}

{- Note [tyConsOfType]
~~~~~~~~~~~~~~~~~~~~~~
It is slightly odd to find the TyCons of a type.  Especially since, via a type
family reduction or axiom, a type that doesn't mention T might start to mention T.

This function is used in only three places:
* In GHC.Tc.Validity.validDerivPred, when identifying "exotic" predicates.
* In GHC.Tc.Errors.Ppr.pprTcSolverReportMsg, when trying to print a helpful
  error about overlapping instances
* In utils/dump-decls/Main.hs, an ill-documented module.

None seem critical. Currently tyConsOfType looks inside coercions, but perhaps
it doesn't even need to do that.
-}

-- | All type constructors occurring in the type; looking through type
--   synonyms, but not newtypes.
--  When it finds a Class, it returns the class TyCon.
tyConsOfType :: Type -> UniqSet TyCon
tyConsOfType :: Type -> UniqSet TyCon
tyConsOfType Type
ty
  = Type -> UniqSet TyCon
go Type
ty
  where
     go :: Type -> UniqSet TyCon  -- The UniqSet does duplicate elim
     go :: Type -> UniqSet TyCon
go Type
ty | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> UniqSet TyCon
go Type
ty'
     go (TyVarTy {})                = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
     go (LitTy {})                  = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
     go (TyConApp TyCon
tc [Type]
tys)           = TyCon -> UniqSet TyCon
forall {a}. Uniquable a => a -> UniqSet a
go_tc TyCon
tc UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` [Type] -> UniqSet TyCon
tyConsOfTypes [Type]
tys
     go (AppTy Type
a Type
b)                 = Type -> UniqSet TyCon
go Type
a UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Type -> UniqSet TyCon
go Type
b
     go (FunTy FunTyFlag
af Type
w Type
a Type
b)            = Type -> UniqSet TyCon
go Type
w UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets`
                                      Type -> UniqSet TyCon
go Type
a UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Type -> UniqSet TyCon
go Type
b
                                      UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` TyCon -> UniqSet TyCon
forall {a}. Uniquable a => a -> UniqSet a
go_tc (FunTyFlag -> TyCon
funTyFlagTyCon FunTyFlag
af)
     go (ForAllTy (Bndr Var
tv ForAllTyFlag
_) Type
ty)   = Type -> UniqSet TyCon
go Type
ty UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Type -> UniqSet TyCon
go (Var -> Type
varType Var
tv)
     go (CastTy Type
ty Coercion
co)              = Type -> UniqSet TyCon
go Type
ty UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Coercion -> UniqSet TyCon
go_co Coercion
co
     go (CoercionTy Coercion
co)             = Coercion -> UniqSet TyCon
go_co Coercion
co

     go_co :: Coercion -> UniqSet TyCon
go_co (Refl Type
ty)               = Type -> UniqSet TyCon
go Type
ty
     go_co (GRefl Role
_ Type
ty MCoercion
mco)        = Type -> UniqSet TyCon
go Type
ty UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` MCoercion -> UniqSet TyCon
go_mco MCoercion
mco
     go_co (TyConAppCo Role
_ TyCon
tc [Coercion]
args)  = TyCon -> UniqSet TyCon
forall {a}. Uniquable a => a -> UniqSet a
go_tc TyCon
tc UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` [Coercion] -> UniqSet TyCon
go_cos [Coercion]
args
     go_co (AppCo Coercion
co Coercion
arg)          = Coercion -> UniqSet TyCon
go_co Coercion
co UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Coercion -> UniqSet TyCon
go_co Coercion
arg
     go_co (ForAllCo { fco_kind :: Coercion -> MCoercion
fco_kind = MCoercion
kind_co, fco_body :: Coercion -> Coercion
fco_body = Coercion
co })
                                   = MCoercion -> UniqSet TyCon
go_mco MCoercion
kind_co UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Coercion -> UniqSet TyCon
go_co Coercion
co
     go_co (FunCo { fco_mult :: Coercion -> Coercion
fco_mult = Coercion
m, fco_arg :: Coercion -> Coercion
fco_arg = Coercion
a, fco_res :: Coercion -> Coercion
fco_res = Coercion
r })
                                   = Coercion -> UniqSet TyCon
go_co Coercion
m UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Coercion -> UniqSet TyCon
go_co Coercion
a UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Coercion -> UniqSet TyCon
go_co Coercion
r
     go_co (AxiomCo CoAxiomRule
ax [Coercion]
args)       = CoAxiomRule -> UniqSet TyCon
go_ax CoAxiomRule
ax UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` [Coercion] -> UniqSet TyCon
go_cos [Coercion]
args
     go_co (UnivCo { uco_lty :: Coercion -> Type
uco_lty = Type
t1, uco_rty :: Coercion -> Type
uco_rty = Type
t2, uco_deps :: Coercion -> [Coercion]
uco_deps = [Coercion]
cos })
                                   = Type -> UniqSet TyCon
go Type
t1 UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Type -> UniqSet TyCon
go Type
t2 UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` [Coercion] -> UniqSet TyCon
go_cos [Coercion]
cos
     go_co (CoVarCo {})            = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
     go_co (HoleCo {})             = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
     go_co (SymCo Coercion
co)              = Coercion -> UniqSet TyCon
go_co Coercion
co
     go_co (TransCo Coercion
co1 Coercion
co2)       = Coercion -> UniqSet TyCon
go_co Coercion
co1 UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Coercion -> UniqSet TyCon
go_co Coercion
co2
     go_co (SelCo CoSel
_ Coercion
co)            = Coercion -> UniqSet TyCon
go_co Coercion
co
     go_co (LRCo LeftOrRight
_ Coercion
co)             = Coercion -> UniqSet TyCon
go_co Coercion
co
     go_co (InstCo Coercion
co Coercion
arg)         = Coercion -> UniqSet TyCon
go_co Coercion
co UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Coercion -> UniqSet TyCon
go_co Coercion
arg
     go_co (KindCo Coercion
co)             = Coercion -> UniqSet TyCon
go_co Coercion
co
     go_co (SubCo Coercion
co)              = Coercion -> UniqSet TyCon
go_co Coercion
co

     go_mco :: MCoercion -> UniqSet TyCon
go_mco MCoercion
MRefl    = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
     go_mco (MCo Coercion
co) = Coercion -> UniqSet TyCon
go_co Coercion
co

     go_cos :: [Coercion] -> UniqSet TyCon
go_cos [Coercion]
cos   = (Coercion -> UniqSet TyCon -> UniqSet TyCon)
-> UniqSet TyCon -> [Coercion] -> UniqSet TyCon
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
unionUniqSets (UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon)
-> (Coercion -> UniqSet TyCon)
-> Coercion
-> UniqSet TyCon
-> UniqSet TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coercion -> UniqSet TyCon
go_co)  UniqSet TyCon
forall a. UniqSet a
emptyUniqSet [Coercion]
cos

     go_tc :: a -> UniqSet a
go_tc a
tc = a -> UniqSet a
forall {a}. Uniquable a => a -> UniqSet a
unitUniqSet a
tc

     go_ax :: CoAxiomRule -> UniqSet TyCon
go_ax (UnbranchedAxiom CoAxiom Unbranched
ax) = TyCon -> UniqSet TyCon
forall {a}. Uniquable a => a -> UniqSet a
go_tc (TyCon -> UniqSet TyCon) -> TyCon -> UniqSet TyCon
forall a b. (a -> b) -> a -> b
$ CoAxiom Unbranched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Unbranched
ax
     go_ax (BranchedAxiom CoAxiom Branched
ax BranchIndex
_) = TyCon -> UniqSet TyCon
forall {a}. Uniquable a => a -> UniqSet a
go_tc (TyCon -> UniqSet TyCon) -> TyCon -> UniqSet TyCon
forall a b. (a -> b) -> a -> b
$ CoAxiom Branched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Branched
ax
     go_ax (BuiltInFamRew  BuiltInFamRewrite
bif) = TyCon -> UniqSet TyCon
forall {a}. Uniquable a => a -> UniqSet a
go_tc (TyCon -> UniqSet TyCon) -> TyCon -> UniqSet TyCon
forall a b. (a -> b) -> a -> b
$ BuiltInFamRewrite -> TyCon
bifrw_fam_tc BuiltInFamRewrite
bif
     go_ax (BuiltInFamInj {})   = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet  -- A free-floating axiom

tyConsOfTypes :: [Type] -> UniqSet TyCon
tyConsOfTypes :: [Type] -> UniqSet TyCon
tyConsOfTypes [Type]
tys = (Type -> UniqSet TyCon -> UniqSet TyCon)
-> UniqSet TyCon -> [Type] -> UniqSet TyCon
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
unionUniqSets (UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon)
-> (Type -> UniqSet TyCon)
-> Type
-> UniqSet TyCon
-> UniqSet TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> UniqSet TyCon
tyConsOfType) UniqSet TyCon
forall a. UniqSet a
emptyUniqSet [Type]
tys

{- **********************************************************************
*                                                                       *
           Occurs check expansion
%*                                                                      *
%********************************************************************* -}

{- Note [Occurs check expansion]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
of occurrences of tv outside type function arguments, if that is
possible; otherwise, it returns Nothing.

For example, suppose we have
  type F a b = [a]
Then
  occCheckExpand b (F Int b) = Just [Int]
but
  occCheckExpand a (F a Int) = Nothing

We don't promise to do the absolute minimum amount of expanding
necessary, but we try not to do expansions we don't need to.  We
prefer doing inner expansions first.  For example,
  type F a b = (a, Int, a, [a])
  type G b   = Char
We have
  occCheckExpand b (F (G b)) = Just (F Char)
even though we could also expand F to get rid of b.

Note [Occurrence checking: look inside kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we are considering unifying
   (alpha :: *)  ~  Int -> (beta :: alpha -> alpha)
This may be an error (what is that alpha doing inside beta's kind?),
but we must not make the mistake of actually unifying or we'll
build an infinite data structure.  So when looking for occurrences
of alpha in the rhs, we must look in the kinds of type variables
that occur there.

occCheckExpand tries to expand type synonyms to remove
unnecessary occurrences of a variable, and thereby get past an
occurs-check failure.  This is good; but
     we can't do it in the /kind/ of a variable /occurrence/

For example #18451 built an infinite type:
    type Const a b = a
    data SameKind :: k -> k -> Type
    type T (k :: Const Type a) = forall (b :: k). SameKind a b

We have
  b :: k
  k :: Const Type a
  a :: k   (must be same as b)

So if we aren't careful, a's kind mentions a, which is bad.
And expanding an /occurrence/ of 'a' doesn't help, because the
/binding site/ is the master copy and all the occurrences should
match it.

Here's a related example:
   f :: forall a b (c :: Const Type b). Proxy '[a, c]

The list means that 'a' gets the same kind as 'c'; but that
kind mentions 'b', so the binders are out of order.

Bottom line: in occCheckExpand, do not expand inside the kinds
of occurrences.  See bad_var_occ in occCheckExpand.  And
see #18451 for more debate.
-}

occCheckExpand :: [Var] -> Type -> Maybe Type
-- See Note [Occurs check expansion]
-- We may have needed to do some type synonym unfolding in order to
-- get rid of the variable (or forall), so we also return the unfolded
-- version of the type, which is guaranteed to be syntactically free
-- of the given type variable.  If the type is already syntactically
-- free of the variable, then the same type is returned.
occCheckExpand :: [Var] -> Type -> Maybe Type
occCheckExpand [Var]
vs_to_avoid Type
ty
  | [Var] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
vs_to_avoid  -- Efficient shortcut
  = Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty           -- Can happen, eg. GHC.Core.Utils.mkSingleAltCase

  | Bool
otherwise
  = (TyCoVarSet, VarEnv Var) -> Type -> Maybe Type
go ([Var] -> TyCoVarSet
mkVarSet [Var]
vs_to_avoid, VarEnv Var
forall a. VarEnv a
emptyVarEnv) Type
ty
  where
    go :: (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
          -- The VarSet is the set of variables we are trying to avoid
          -- The VarEnv carries mappings necessary
          -- because of kind expansion
    go :: (TyCoVarSet, VarEnv Var) -> Type -> Maybe Type
go (TyCoVarSet
as, VarEnv Var
env) ty :: Type
ty@(TyVarTy Var
tv)
      | Just Var
tv' <- VarEnv Var -> Var -> Maybe Var
forall a. VarEnv a -> Var -> Maybe a
lookupVarEnv VarEnv Var
env Var
tv = Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> Type
mkTyVarTy Var
tv')
      | TyCoVarSet -> Var -> Bool
bad_var_occ TyCoVarSet
as Var
tv               = Maybe Type
forall a. Maybe a
Nothing
      | Bool
otherwise                       = Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty

    go (TyCoVarSet, VarEnv Var)
_   ty :: Type
ty@(LitTy {}) = Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
    go (TyCoVarSet, VarEnv Var)
cxt (AppTy Type
ty1 Type
ty2) = do { ty1' <- (TyCoVarSet, VarEnv Var) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv Var)
cxt Type
ty1
                                ; ty2' <- go cxt ty2
                                ; return (AppTy ty1' ty2') }
    go (TyCoVarSet, VarEnv Var)
cxt ty :: Type
ty@(FunTy FunTyFlag
_ Type
w Type
ty1 Type
ty2)
       = do { w'   <- (TyCoVarSet, VarEnv Var) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv Var)
cxt Type
w
            ; ty1' <- go cxt ty1
            ; ty2' <- go cxt ty2
            ; return (ty { ft_mult = w', ft_arg = ty1', ft_res = ty2' }) }
    go cxt :: (TyCoVarSet, VarEnv Var)
cxt@(TyCoVarSet
as, VarEnv Var
env) (ForAllTy (Bndr Var
tv ForAllTyFlag
vis) Type
body_ty)
       = do { ki' <- (TyCoVarSet, VarEnv Var) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv Var)
cxt (Var -> Type
varType Var
tv)
            ; let tv'  = Var -> Type -> Var
setVarType Var
tv Type
ki'
                  env' = VarEnv Var -> Var -> Var -> VarEnv Var
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv VarEnv Var
env Var
tv Var
tv'
                  as'  = TyCoVarSet
as TyCoVarSet -> Var -> TyCoVarSet
`delVarSet` Var
tv
            ; body' <- go (as', env') body_ty
            ; return (ForAllTy (Bndr tv' vis) body') }

    -- For a type constructor application, first try expanding away the
    -- offending variable from the arguments.  If that doesn't work, next
    -- see if the type constructor is a type synonym, and if so, expand
    -- it and try again.
    go (TyCoVarSet, VarEnv Var)
cxt ty :: Type
ty@(TyConApp TyCon
tc [Type]
tys)
      = case (Type -> Maybe Type) -> [Type] -> Maybe [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((TyCoVarSet, VarEnv Var) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv Var)
cxt) [Type]
tys of
          Just [Type]
tys' -> Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> [Type] -> Type
TyConApp TyCon
tc [Type]
tys')
          Maybe [Type]
Nothing | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty -> (TyCoVarSet, VarEnv Var) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv Var)
cxt Type
ty'
                  | Bool
otherwise               -> Maybe Type
forall a. Maybe a
Nothing
                      -- Failing that, try to expand a synonym

    go (TyCoVarSet, VarEnv Var)
cxt (CastTy Type
ty Coercion
co) =  do { ty' <- (TyCoVarSet, VarEnv Var) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv Var)
cxt Type
ty
                                ; co' <- go_co cxt co
                                ; return (CastTy ty' co') }
    go (TyCoVarSet, VarEnv Var)
cxt (CoercionTy Coercion
co) = do { co' <- (TyCoVarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (TyCoVarSet, VarEnv Var)
cxt Coercion
co
                                ; return (CoercionTy co') }

    ------------------
    bad_var_occ :: VarSet -> Var -> Bool
    -- Works for TyVar and CoVar
    -- See Note [Occurrence checking: look inside kinds]
    bad_var_occ :: TyCoVarSet -> Var -> Bool
bad_var_occ TyCoVarSet
vs_to_avoid Var
v
       =  Var
v                          Var -> TyCoVarSet -> Bool
`elemVarSet`       TyCoVarSet
vs_to_avoid
       Bool -> Bool -> Bool
|| Type -> TyCoVarSet
tyCoVarsOfType (Var -> Type
varType Var
v) TyCoVarSet -> TyCoVarSet -> Bool
`intersectsVarSet` TyCoVarSet
vs_to_avoid

    ------------------
    go_mco :: (TyCoVarSet, VarEnv Var) -> MCoercion -> Maybe MCoercion
go_mco (TyCoVarSet, VarEnv Var)
_   MCoercion
MRefl = MCoercion -> Maybe MCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return MCoercion
MRefl
    go_mco (TyCoVarSet, VarEnv Var)
ctx (MCo Coercion
co) = Coercion -> MCoercion
Coercion -> MCoercion
MCo (Coercion -> MCoercion) -> Maybe Coercion -> Maybe MCoercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TyCoVarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (TyCoVarSet, VarEnv Var)
ctx Coercion
co

    ------------------
    go_co :: (TyCoVarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (TyCoVarSet, VarEnv Var)
cxt (Refl Type
ty)                 = do { ty' <- (TyCoVarSet, VarEnv Var) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv Var)
cxt Type
ty
                                             ; return (Refl ty') }
    go_co (TyCoVarSet, VarEnv Var)
cxt (GRefl Role
r Type
ty MCoercion
mco)          = do { mco' <- (TyCoVarSet, VarEnv Var) -> MCoercion -> Maybe MCoercion
go_mco (TyCoVarSet, VarEnv Var)
cxt MCoercion
mco
                                             ; ty' <- go cxt ty
                                             ; return (GRefl r ty' mco') }
      -- Note: Coercions do not contain type synonyms
    go_co (TyCoVarSet, VarEnv Var)
cxt (TyConAppCo Role
r TyCon
tc [Coercion]
args)    = do { args' <- (Coercion -> Maybe Coercion) -> [Coercion] -> Maybe [Coercion]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((TyCoVarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (TyCoVarSet, VarEnv Var)
cxt) [Coercion]
args
                                             ; return (TyConAppCo r tc args') }
    go_co (TyCoVarSet, VarEnv Var)
cxt (AppCo Coercion
co Coercion
arg)            = do { co' <- (TyCoVarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (TyCoVarSet, VarEnv Var)
cxt Coercion
co
                                             ; arg' <- go_co cxt arg
                                             ; return (AppCo co' arg') }
    go_co (TyCoVarSet, VarEnv Var)
cxt (SymCo Coercion
co)                = do { co' <- (TyCoVarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (TyCoVarSet, VarEnv Var)
cxt Coercion
co
                                             ; return (SymCo co') }
    go_co (TyCoVarSet, VarEnv Var)
cxt (TransCo Coercion
co1 Coercion
co2)         = do { co1' <- (TyCoVarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (TyCoVarSet, VarEnv Var)
cxt Coercion
co1
                                             ; co2' <- go_co cxt co2
                                             ; return (TransCo co1' co2') }
    go_co (TyCoVarSet, VarEnv Var)
cxt (SelCo CoSel
n Coercion
co)              = do { co' <- (TyCoVarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (TyCoVarSet, VarEnv Var)
cxt Coercion
co
                                             ; return (SelCo n co') }
    go_co (TyCoVarSet, VarEnv Var)
cxt (LRCo LeftOrRight
lr Coercion
co)              = do { co' <- (TyCoVarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (TyCoVarSet, VarEnv Var)
cxt Coercion
co
                                             ; return (LRCo lr co') }
    go_co (TyCoVarSet, VarEnv Var)
cxt (InstCo Coercion
co Coercion
arg)           = do { co' <- (TyCoVarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (TyCoVarSet, VarEnv Var)
cxt Coercion
co
                                             ; arg' <- go_co cxt arg
                                             ; return (InstCo co' arg') }
    go_co (TyCoVarSet, VarEnv Var)
cxt (KindCo Coercion
co)               = do { co' <- (TyCoVarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (TyCoVarSet, VarEnv Var)
cxt Coercion
co
                                             ; return (KindCo co') }
    go_co (TyCoVarSet, VarEnv Var)
cxt (SubCo Coercion
co)                = do { co' <- (TyCoVarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (TyCoVarSet, VarEnv Var)
cxt Coercion
co
                                             ; return (SubCo co') }

    go_co cxt :: (TyCoVarSet, VarEnv Var)
cxt@(TyCoVarSet
as, VarEnv Var
env) co :: Coercion
co@(ForAllCo { fco_tcv :: Coercion -> Var
fco_tcv = Var
tcv, fco_kind :: Coercion -> MCoercion
fco_kind = MCoercion
kind_co, fco_body :: Coercion -> Coercion
fco_body = Coercion
body_co })
      = do { ki' <- (TyCoVarSet, VarEnv Var) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv Var)
cxt (Var -> Type
varType Var
tcv)
           ; let tcv' = Var -> Type -> Var
setVarType Var
tcv Type
ki'
                 env' = VarEnv Var -> Var -> Var -> VarEnv Var
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv VarEnv Var
env Var
tcv Var
tcv'
                 as'  = TyCoVarSet
as TyCoVarSet -> Var -> TyCoVarSet
`delVarSet` Var
tcv
           ; kind_co' <- go_mco cxt kind_co
           ; body' <- go_co (as', env') body_co
           ; return (co { fco_tcv = tcv', fco_kind = kind_co', fco_body = body' }) }

    go_co (TyCoVarSet, VarEnv Var)
cxt co :: Coercion
co@(FunCo { fco_mult :: Coercion -> Coercion
fco_mult = Coercion
w, fco_arg :: Coercion -> Coercion
fco_arg = Coercion
co1 ,fco_res :: Coercion -> Coercion
fco_res = Coercion
co2 })
      = do { co1' <- (TyCoVarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (TyCoVarSet, VarEnv Var)
cxt Coercion
co1
           ; co2' <- go_co cxt co2
           ; w' <- go_co cxt w
           ; return (co { fco_mult = w', fco_arg = co1', fco_res = co2' })}

    go_co (TyCoVarSet
as,VarEnv Var
env) co :: Coercion
co@(CoVarCo Var
c)
      | Just Var
c' <- VarEnv Var -> Var -> Maybe Var
forall a. VarEnv a -> Var -> Maybe a
lookupVarEnv VarEnv Var
env Var
c   = Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> Coercion
CoVarCo Var
c')
      | TyCoVarSet -> Var -> Bool
bad_var_occ TyCoVarSet
as Var
c                = Maybe Coercion
forall a. Maybe a
Nothing
      | Bool
otherwise                       = Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Coercion
co

    go_co (TyCoVarSet
as,VarEnv Var
_) co :: Coercion
co@(HoleCo CoercionHole
h)
      | TyCoVarSet -> Var -> Bool
bad_var_occ TyCoVarSet
as (CoercionHole -> Var
ch_co_var CoercionHole
h)    = Maybe Coercion
forall a. Maybe a
Nothing
      | Bool
otherwise                       = Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Coercion
co

    go_co (TyCoVarSet, VarEnv Var)
cxt (AxiomCo CoAxiomRule
ax [Coercion]
cs)           = do { cs' <- (Coercion -> Maybe Coercion) -> [Coercion] -> Maybe [Coercion]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((TyCoVarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (TyCoVarSet, VarEnv Var)
cxt) [Coercion]
cs
                                             ; return (AxiomCo ax cs') }
    go_co (TyCoVarSet, VarEnv Var)
cxt co :: Coercion
co@(UnivCo { uco_lty :: Coercion -> Type
uco_lty = Type
ty1, uco_rty :: Coercion -> Type
uco_rty = Type
ty2, uco_deps :: Coercion -> [Coercion]
uco_deps = [Coercion]
cos })
      = do { ty1' <- (TyCoVarSet, VarEnv Var) -> Type -> Maybe Type
go (TyCoVarSet, VarEnv Var)
cxt Type
ty1
           ; ty2' <- go cxt ty2
           ; cos' <- mapM (go_co cxt) cos
           ; return (co { uco_lty = ty1', uco_rty = ty2', uco_deps = cos' }) }