{-# 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 -> VarSet
tyCoVarsOfType Type
ty = TyCoFV -> VarSet
runTyCoVars (Type -> TyCoFV
deepTypeFV Type
ty)
-- Alternative:
--   tyCoVarsOfType ty = closeOverKinds (shallowTyCoVarsOfType ty)

tyCoVarsOfTypes :: [Type] -> TyCoVarSet
-- The "deep" TyCoVars of the the type
tyCoVarsOfTypes :: [Type] -> VarSet
tyCoVarsOfTypes [Type]
tys = TyCoFV -> VarSet
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 -> VarSet
tyCoVarsOfCo Coercion
co = TyCoFV -> VarSet
runTyCoVars (Coercion -> TyCoFV
deepCoFV Coercion
co)

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

tyCoVarsOfCos :: [Coercion] -> TyCoVarSet
tyCoVarsOfCos :: [Coercion] -> VarSet
tyCoVarsOfCos [Coercion]
cos = TyCoFV -> VarSet
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 -> VarSet
tyCoVarsOfThings a -> Type
get_ty t a
things
  = TyCoFV -> VarSet
runTyCoVars (TyCoFV -> VarSet) -> TyCoFV -> VarSet
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 -> VarSet
tyCoVarsOfTyVarEnv TyVarEnv Type
tys = [Type] -> VarSet
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 -> VarSet
tyCoVarsOfCoVarEnv CoVarEnv Coercion
cos = [Coercion] -> VarSet
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] -> VarSet -> VarSet
tyCoVarsOfQuant [] VarSet
fvs         = VarSet
fvs
tyCoVarsOfQuant (Var
tcv:[Var]
tcvs) VarSet
fvs = ([Var] -> VarSet -> VarSet
tyCoVarsOfQuant [Var]
tcvs VarSet
fvs VarSet -> Var -> VarSet
`delVarSet` Var
tcv)
                                 VarSet -> VarSet -> VarSet
`unionVarSet` Type -> VarSet
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 VarSet a -> FV VarSet 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]
deepUnitFV :: (Type -> TyCoFV) -> Var -> TyCoFV
deepUnitFV Type -> TyCoFV
fvs_of_kind Var
v
  = (VarSet -> EndoOS VarSet) -> TyCoFV
forall env acc. (env -> acc) -> FV env acc
MkFV (\VarSet
bvs -> (VarSet -> VarSet) -> EndoOS VarSet
forall a. (a -> a) -> EndoOS a
EndoOS (VarSet -> VarSet -> VarSet
do_it VarSet
bvs))
  where
    do_it :: BoundVars -> TyCoVarSet -> TyCoVarSet
    do_it :: VarSet -> VarSet -> VarSet
do_it VarSet
bvs VarSet
acc | Var
v Var -> VarSet -> Bool
`elemVarSet` VarSet
bvs = VarSet
acc
                  | Var
v Var -> VarSet -> Bool
`elemVarSet` VarSet
acc = VarSet
acc
                  | Bool
otherwise          = TyCoFV -> VarSet -> VarSet
forall a. FV VarSet (EndoOS a) -> a -> a
runFVAcc (Type -> TyCoFV
fvs_of_kind (Var -> Type
varType Var
v)) VarSet
acc
                                         VarSet -> Var -> VarSet
`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 -> VarSet
shallowTyCoVarsOfType Type
ty = TyCoFV -> VarSet
runTyCoVars (Type -> TyCoFV
shallowTypeFV Type
ty)

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

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

shallowTyCoVarsOfCos :: [Coercion] -> TyCoVarSet
shallowTyCoVarsOfCos :: [Coercion] -> VarSet
shallowTyCoVarsOfCos [Coercion]
cos = TyCoFV -> VarSet
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 VarSet a -> FV VarSet 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
  = (VarSet -> EndoOS VarSet) -> TyCoFV
forall env acc. (env -> acc) -> FV env acc
MkFV (\VarSet
bvs -> (VarSet -> VarSet) -> EndoOS VarSet
forall a. (a -> a) -> EndoOS a
EndoOS (VarSet -> VarSet -> VarSet
do_it VarSet
bvs))
  where
    do_it :: VarSet -> VarSet -> VarSet
do_it VarSet
bvs VarSet
acc | Var
v Var -> VarSet -> Bool
`elemVarSet` VarSet
bvs = VarSet
acc
                  | Var
v Var -> VarSet -> Bool
`elemVarSet` VarSet
acc = VarSet
acc
                  | Bool
otherwise          = VarSet
acc VarSet -> Var -> VarSet
`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 VarSet a -> FV VarSet 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
  = (VarSet -> EndoOS DVarSet) -> DCoVarFV
forall env acc. (env -> acc) -> FV env acc
MkFV (\VarSet
bvs -> (DVarSet -> DVarSet) -> EndoOS DVarSet
forall a. (a -> a) -> EndoOS a
EndoOS (VarSet -> DVarSet -> DVarSet
do_it VarSet
bvs))
  where
    do_it :: BoundVars -> DTyCoVarSet -> DTyCoVarSet
    do_it :: VarSet -> DVarSet -> DVarSet
do_it VarSet
bvs DVarSet
acc | Var
v Var -> VarSet -> Bool
`elemVarSet` VarSet
bvs  = DVarSet
acc
                  | Var
v Var -> DVarSet -> Bool
`elemDVarSet` DVarSet
acc = DVarSet
acc
                  | Bool
otherwise           = DCoVarFV -> DVarSet -> DVarSet
forall a. FV VarSet (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 (f, VarSet) a -> FV (f, VarSet) a
addBndrSelectiveFV }
  where
    do_tcv :: Var -> SelectiveDFV
do_tcv Var
v = ((Var -> Bool, VarSet) -> EndoOS DVarSet) -> SelectiveDFV
forall env acc. (env -> acc) -> FV env acc
MkFV (\(Var -> Bool, VarSet)
bvs -> (DVarSet -> DVarSet) -> EndoOS DVarSet
forall a. (a -> a) -> EndoOS a
EndoOS ((Var -> Bool, VarSet) -> DVarSet -> DVarSet
do_it (Var -> Bool, VarSet)
bvs))
      where
        do_it :: (Var -> Bool, VarSet) -> DVarSet -> DVarSet
do_it (Var -> Bool
is_interesting,VarSet
bvs) DVarSet
acc
          | Bool -> Bool
not (Var -> Bool
is_interesting Var
v) = DVarSet
acc  -- The "selective" bit
          | Var
v Var -> VarSet -> Bool
`elemVarSet` VarSet
bvs     = DVarSet
acc
          | 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 -> VarSet
coVarsOfType  Type
ty  = TyCoFV -> VarSet
runTyCoVars (Type -> TyCoFV
deepCoVarTypeFV Type
ty)
coVarsOfTypes :: [Type] -> VarSet
coVarsOfTypes [Type]
tys = TyCoFV -> VarSet
runTyCoVars ([Type] -> TyCoFV
deepCoVarTypesFV [Type]
tys)
coVarsOfCo :: Coercion -> VarSet
coVarsOfCo    Coercion
co  = TyCoFV -> VarSet
runTyCoVars (Coercion -> TyCoFV
deepCoVarCoFV Coercion
co)
coVarsOfCos :: [Coercion] -> VarSet
coVarsOfCos   [Coercion]
cos = TyCoFV -> VarSet
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 VarSet a -> FV VarSet 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 VarSet a -> FV VarSet 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 :: VarSet -> VarSet
closeOverKinds VarSet
vs = (Var -> VarSet -> VarSet) -> VarSet -> VarSet -> VarSet
forall a. (Var -> a -> a) -> a -> VarSet -> a
nonDetStrictFoldVarSet Var -> VarSet -> VarSet
do_one VarSet
vs VarSet
vs
  where
    do_one :: Var -> VarSet -> VarSet
do_one Var
v = TyCoFV -> VarSet -> VarSet
forall a. FV VarSet (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 VarSet (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 VarSet
visVarsOfType Type
orig_ty = VarSet -> VarSet -> Pair VarSet
forall a. a -> a -> Pair a
Pair VarSet
invis_vars VarSet
vis_vars
  where
    Pair VarSet
invis_vars1 VarSet
vis_vars = Type -> Pair VarSet
go Type
orig_ty
    invis_vars :: VarSet
invis_vars = VarSet
invis_vars1 VarSet -> VarSet -> VarSet
`minusVarSet` VarSet
vis_vars

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

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

    go_tc :: TyCon -> [Type] -> Pair VarSet
go_tc TyCon
tc [Type]
tys = let ([Type]
invis, [Type]
vis) = TyCon -> [Type] -> ([Type], [Type])
partitionInvisibleTypes TyCon
tc [Type]
tys in
                   VarSet -> Pair VarSet
invisible ([Type] -> VarSet
tyCoVarsOfTypes [Type]
invis) Pair VarSet -> Pair VarSet -> Pair VarSet
forall a. Monoid a => a -> a -> a
`mappend` (Type -> Pair VarSet) -> [Type] -> Pair VarSet
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 VarSet
go [Type]
vis

visVarsOfTypes :: [Type] -> Pair TyCoVarSet
visVarsOfTypes :: [Type] -> Pair VarSet
visVarsOfTypes = (Type -> Pair VarSet) -> [Type] -> Pair VarSet
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 VarSet
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 -> VarSet
injectiveVarsOfType Bool
look_under_tfs Type
ty = TyCoFV -> VarSet
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] -> VarSet
injectiveVarsOfTypes Bool
look_under_tfs [Type]
tys
  = TyCoFV -> VarSet
runTyCoVars (TyCoFV -> VarSet) -> TyCoFV -> VarSet
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 VarSet a -> FV VarSet 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 -> VarSet
invisibleVarsOfType = Type -> VarSet
go
  where
    go :: Type -> VarSet
go Type
ty                  | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty
                           = Type -> VarSet
go Type
ty'
    go (TyVarTy Var
v)         = Type -> VarSet
go (Var -> Type
tyVarKind Var
v)
    go (AppTy Type
f Type
a)         = Type -> VarSet
go Type
f VarSet -> VarSet -> VarSet
`unionVarSet` Type -> VarSet
go Type
a
    go (FunTy FunTyFlag
_ Type
w Type
ty1 Type
ty2) = Type -> VarSet
go Type
ty1 VarSet -> VarSet -> VarSet
`unionVarSet` Type -> VarSet
go Type
w VarSet -> VarSet -> VarSet
`unionVarSet` Type -> VarSet
go Type
ty2
                             -- As per #23764, order is: arg, mult, res.
    go (TyConApp TyCon
tc [Type]
tys)   = [Type] -> VarSet
tyCoVarsOfTypes [Type]
invisibles VarSet -> VarSet -> VarSet
`unionVarSet`
                             [Type] -> VarSet
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 -> VarSet
tyCoVarsOfType (Var -> Type
varType Var
var) VarSet -> VarSet -> VarSet
`unionVarSet` (Type -> VarSet
go Type
ty VarSet -> Var -> VarSet
`delVarSet` Var
var)
    go LitTy{}             = VarSet
emptyVarSet
    go (CastTy Type
ty Coercion
co)      = Coercion -> VarSet
tyCoVarsOfCo Coercion
co VarSet -> VarSet -> VarSet
`unionVarSet` Type -> VarSet
go Type
ty
    go (CoercionTy Coercion
co)     = Coercion -> VarSet
tyCoVarsOfCo Coercion
co

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


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

{-# INLINE afvFolder #-}   -- so that specialization to (const True) works
afvFolder :: (TyCoVar -> Bool) -> TyCoFolder (FV TyCoVarSet DM.Any)
-- 'afvFolder' is short for "any-free-var folder", good for checking
-- if any free var of a type satisfies a predicate `check_fv`
afvFolder :: (Var -> Bool) -> TyCoFolder (FV VarSet Any)
afvFolder Var -> Bool
check_fv = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView  -- See Note [Free vars and synonyms]
                                , tcf_tyvar :: Var -> FV VarSet Any
tcf_tyvar = Var -> FV VarSet Any
do_tcv, tcf_covar :: Var -> FV VarSet Any
tcf_covar = Var -> FV VarSet Any
do_tcv
                                , tcf_hole :: CoercionHole -> FV VarSet Any
tcf_hole = CoercionHole -> FV VarSet Any
forall {a} {p}. Monoid a => p -> a
do_hole
                                , tcf_tycobinder :: Var -> FV VarSet Any -> FV VarSet Any
tcf_tycobinder = Var -> FV VarSet Any -> FV VarSet Any
forall a. Var -> FV VarSet a -> FV VarSet a
addBndrFV }
  where
    do_tcv :: Var -> FV VarSet Any
do_tcv Var
tv = (VarSet -> Any) -> FV VarSet Any
forall env acc. (env -> acc) -> FV env acc
MkFV ((VarSet -> Any) -> FV VarSet Any)
-> (VarSet -> Any) -> FV VarSet Any
forall a b. (a -> b) -> a -> b
$ \ VarSet
bvs ->
                Bool -> Any
Any (Bool -> Bool
not (Var
tv Var -> VarSet -> Bool
`elemVarSet` VarSet
bvs) Bool -> Bool -> Bool
&& Var -> Bool
check_fv Var
tv)
    do_hole :: p -> a
do_hole p
_ = a
forall a. Monoid a => a
mempty    -- I'm unsure; probably never happens

anyFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool
anyFreeVarsOfType :: (Var -> Bool) -> Type -> Bool
anyFreeVarsOfType Var -> Bool
check_fv Type
ty = Any -> Bool
DM.getAny (FV VarSet Any -> Any
forall a. FV VarSet a -> a
runFVTop (Type -> FV VarSet Any
f Type
ty))
  where (Type -> FV VarSet Any
f, [Type] -> FV VarSet Any
_, Coercion -> FV VarSet Any
_, [Coercion] -> FV VarSet Any
_) = TyCoFolder (FV VarSet Any)
-> (Type -> FV VarSet Any, [Type] -> FV VarSet Any,
    Coercion -> FV VarSet Any, [Coercion] -> FV VarSet Any)
forall a.
Monoid a =>
TyCoFolder a
-> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo ((Var -> Bool) -> TyCoFolder (FV VarSet Any)
afvFolder Var -> Bool
check_fv)

anyFreeVarsOfTypes :: (TyCoVar -> Bool) -> [Type] -> Bool
anyFreeVarsOfTypes :: (Var -> Bool) -> [Type] -> Bool
anyFreeVarsOfTypes Var -> Bool
check_fv [Type]
tys = Any -> Bool
DM.getAny (FV VarSet Any -> Any
forall a. FV VarSet a -> a
runFVTop ([Type] -> FV VarSet Any
f [Type]
tys))
  where (Type -> FV VarSet Any
_, [Type] -> FV VarSet Any
f, Coercion -> FV VarSet Any
_, [Coercion] -> FV VarSet Any
_) = TyCoFolder (FV VarSet Any)
-> (Type -> FV VarSet Any, [Type] -> FV VarSet Any,
    Coercion -> FV VarSet Any, [Coercion] -> FV VarSet Any)
forall a.
Monoid a =>
TyCoFolder a
-> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo ((Var -> Bool) -> TyCoFolder (FV VarSet Any)
afvFolder Var -> Bool
check_fv)

anyFreeVarsOfCo :: (TyCoVar -> Bool) -> Coercion -> Bool
anyFreeVarsOfCo :: (Var -> Bool) -> Coercion -> Bool
anyFreeVarsOfCo Var -> Bool
check_fv Coercion
co = Any -> Bool
DM.getAny (FV VarSet Any -> Any
forall a. FV VarSet a -> a
runFVTop (Coercion -> FV VarSet Any
f Coercion
co))
  where (Type -> FV VarSet Any
_, [Type] -> FV VarSet Any
_, Coercion -> FV VarSet Any
f, [Coercion] -> FV VarSet Any
_) = TyCoFolder (FV VarSet Any)
-> (Type -> FV VarSet Any, [Type] -> FV VarSet Any,
    Coercion -> FV VarSet Any, [Coercion] -> FV VarSet Any)
forall a.
Monoid a =>
TyCoFolder a
-> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo ((Var -> Bool) -> TyCoFolder (FV VarSet Any)
afvFolder Var -> Bool
check_fv)

noFreeVarsOfType :: Type -> Bool
noFreeVarsOfType :: Type -> Bool
noFreeVarsOfType Type
ty = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Any -> Bool
DM.getAny (FV VarSet Any -> Any
forall a. FV VarSet a -> a
runFVTop (Type -> FV VarSet Any
f Type
ty))
  where (Type -> FV VarSet Any
f, [Type] -> FV VarSet Any
_, Coercion -> FV VarSet Any
_, [Coercion] -> FV VarSet Any
_) = TyCoFolder (FV VarSet Any)
-> (Type -> FV VarSet Any, [Type] -> FV VarSet Any,
    Coercion -> FV VarSet Any, [Coercion] -> FV VarSet Any)
forall a.
Monoid a =>
TyCoFolder a
-> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo ((Var -> Bool) -> TyCoFolder (FV VarSet Any)
afvFolder (Bool -> Var -> Bool
forall a b. a -> b -> a
const Bool
True))

noFreeVarsOfTypes :: [Type] -> Bool
noFreeVarsOfTypes :: [Type] -> Bool
noFreeVarsOfTypes [Type]
tys = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Any -> Bool
DM.getAny (FV VarSet Any -> Any
forall a. FV VarSet a -> a
runFVTop ([Type] -> FV VarSet Any
f [Type]
tys))
  where (Type -> FV VarSet Any
_, [Type] -> FV VarSet Any
f, Coercion -> FV VarSet Any
_, [Coercion] -> FV VarSet Any
_) = TyCoFolder (FV VarSet Any)
-> (Type -> FV VarSet Any, [Type] -> FV VarSet Any,
    Coercion -> FV VarSet Any, [Coercion] -> FV VarSet Any)
forall a.
Monoid a =>
TyCoFolder a
-> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo ((Var -> Bool) -> TyCoFolder (FV VarSet Any)
afvFolder (Bool -> Var -> Bool
forall a b. a -> b -> a
const Bool
True))

noFreeVarsOfCo :: Coercion -> Bool
noFreeVarsOfCo :: Coercion -> Bool
noFreeVarsOfCo Coercion
co = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Any -> Bool
DM.getAny (FV VarSet Any -> Any
forall a. FV VarSet a -> a
runFVTop (Coercion -> FV VarSet Any
f Coercion
co))
  where (Type -> FV VarSet Any
_, [Type] -> FV VarSet Any
_, Coercion -> FV VarSet Any
f, [Coercion] -> FV VarSet Any
_) = TyCoFolder (FV VarSet Any)
-> (Type -> FV VarSet Any, [Type] -> FV VarSet Any,
    Coercion -> FV VarSet Any, [Coercion] -> FV VarSet Any)
forall a.
Monoid a =>
TyCoFolder a
-> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo ((Var -> Bool) -> TyCoFolder (FV VarSet Any)
afvFolder (Bool -> Var -> Bool
forall a b. a -> b -> a
const Bool
True))


{-
************************************************************************
*                                                                      *
            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
  = (VarSet, VarEnv Var) -> Type -> Maybe Type
go ([Var] -> VarSet
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 :: (VarSet, VarEnv Var) -> Type -> Maybe Type
go (VarSet
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')
      | VarSet -> Var -> Bool
bad_var_occ VarSet
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 (VarSet, 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 (VarSet, VarEnv Var)
cxt (AppTy Type
ty1 Type
ty2) = do { ty1' <- (VarSet, VarEnv Var) -> Type -> Maybe Type
go (VarSet, VarEnv Var)
cxt Type
ty1
                                ; ty2' <- go cxt ty2
                                ; return (AppTy ty1' ty2') }
    go (VarSet, VarEnv Var)
cxt ty :: Type
ty@(FunTy FunTyFlag
_ Type
w Type
ty1 Type
ty2)
       = do { w'   <- (VarSet, VarEnv Var) -> Type -> Maybe Type
go (VarSet, 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 :: (VarSet, VarEnv Var)
cxt@(VarSet
as, VarEnv Var
env) (ForAllTy (Bndr Var
tv ForAllTyFlag
vis) Type
body_ty)
       = do { ki' <- (VarSet, VarEnv Var) -> Type -> Maybe Type
go (VarSet, 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'  = VarSet
as VarSet -> Var -> VarSet
`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 (VarSet, 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 ((VarSet, VarEnv Var) -> Type -> Maybe Type
go (VarSet, 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 -> (VarSet, VarEnv Var) -> Type -> Maybe Type
go (VarSet, VarEnv Var)
cxt Type
ty'
                  | Bool
otherwise               -> Maybe Type
forall a. Maybe a
Nothing
                      -- Failing that, try to expand a synonym

    go (VarSet, VarEnv Var)
cxt (CastTy Type
ty Coercion
co) =  do { ty' <- (VarSet, VarEnv Var) -> Type -> Maybe Type
go (VarSet, VarEnv Var)
cxt Type
ty
                                ; co' <- go_co cxt co
                                ; return (CastTy ty' co') }
    go (VarSet, VarEnv Var)
cxt (CoercionTy Coercion
co) = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, 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 :: VarSet -> Var -> Bool
bad_var_occ VarSet
vs_to_avoid Var
v
       =  Var
v                          Var -> VarSet -> Bool
`elemVarSet`       VarSet
vs_to_avoid
       Bool -> Bool -> Bool
|| Type -> VarSet
tyCoVarsOfType (Var -> Type
varType Var
v) VarSet -> VarSet -> Bool
`intersectsVarSet` VarSet
vs_to_avoid

    ------------------
    go_mco :: (VarSet, VarEnv Var) -> MCoercion -> Maybe MCoercion
go_mco (VarSet, 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 (VarSet, 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
<$> (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
ctx Coercion
co

    ------------------
    go_co :: (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt (Refl Type
ty)                 = do { ty' <- (VarSet, VarEnv Var) -> Type -> Maybe Type
go (VarSet, VarEnv Var)
cxt Type
ty
                                             ; return (Refl ty') }
    go_co (VarSet, VarEnv Var)
cxt (GRefl Role
r Type
ty MCoercion
mco)          = do { mco' <- (VarSet, VarEnv Var) -> MCoercion -> Maybe MCoercion
go_mco (VarSet, VarEnv Var)
cxt MCoercion
mco
                                             ; ty' <- go cxt ty
                                             ; return (GRefl r ty' mco') }
      -- Note: Coercions do not contain type synonyms
    go_co (VarSet, 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 ((VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt) [Coercion]
args
                                             ; return (TyConAppCo r tc args') }
    go_co (VarSet, VarEnv Var)
cxt (AppCo Coercion
co Coercion
arg)            = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt Coercion
co
                                             ; arg' <- go_co cxt arg
                                             ; return (AppCo co' arg') }
    go_co (VarSet, VarEnv Var)
cxt (SymCo Coercion
co)                = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt Coercion
co
                                             ; return (SymCo co') }
    go_co (VarSet, VarEnv Var)
cxt (TransCo Coercion
co1 Coercion
co2)         = do { co1' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt Coercion
co1
                                             ; co2' <- go_co cxt co2
                                             ; return (TransCo co1' co2') }
    go_co (VarSet, VarEnv Var)
cxt (SelCo CoSel
n Coercion
co)              = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt Coercion
co
                                             ; return (SelCo n co') }
    go_co (VarSet, VarEnv Var)
cxt (LRCo LeftOrRight
lr Coercion
co)              = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt Coercion
co
                                             ; return (LRCo lr co') }
    go_co (VarSet, VarEnv Var)
cxt (InstCo Coercion
co Coercion
arg)           = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt Coercion
co
                                             ; arg' <- go_co cxt arg
                                             ; return (InstCo co' arg') }
    go_co (VarSet, VarEnv Var)
cxt (KindCo Coercion
co)               = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt Coercion
co
                                             ; return (KindCo co') }
    go_co (VarSet, VarEnv Var)
cxt (SubCo Coercion
co)                = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt Coercion
co
                                             ; return (SubCo co') }

    go_co cxt :: (VarSet, VarEnv Var)
cxt@(VarSet
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' <- (VarSet, VarEnv Var) -> Type -> Maybe Type
go (VarSet, 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'  = VarSet
as VarSet -> Var -> VarSet
`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 (VarSet, 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' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, 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 (VarSet
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')
      | VarSet -> Var -> Bool
bad_var_occ VarSet
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 (VarSet
as,VarEnv Var
_) co :: Coercion
co@(HoleCo CoercionHole
h)
      | VarSet -> Var -> Bool
bad_var_occ VarSet
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 (VarSet, 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 ((VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt) [Coercion]
cs
                                             ; return (AxiomCo ax cs') }
    go_co (VarSet, 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' <- (VarSet, VarEnv Var) -> Type -> Maybe Type
go (VarSet, 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' }) }