module TyCoFVs
  (
        tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet,
        exactTyCoVarsOfType, exactTyCoVarsOfTypes,
        tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs,
        tyCoFVsOfType, tyCoVarsOfTypeList,
        tyCoFVsOfTypes, tyCoVarsOfTypesList,
        tyCoVarsOfTypesSet, tyCoVarsOfCosSet,
        coVarsOfType, coVarsOfTypes,
        coVarsOfCo, coVarsOfCos,
        tyCoVarsOfCo, tyCoVarsOfCos,
        tyCoVarsOfCoDSet,
        tyCoFVsOfCo, tyCoFVsOfCos,
        tyCoVarsOfCoList, tyCoVarsOfProv,
        almostDevoidCoVarOfCo,
        injectiveVarsOfType, injectiveVarsOfTypes,
        invisibleVarsOfType, invisibleVarsOfTypes,

        noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,

        mkTyCoInScopeSet,

        -- * Welll-scoped free variables
        scopedSort, tyCoVarsOfTypeWellScoped,
        tyCoVarsOfTypesWellScoped,
  ) where

import GhcPrelude

import {-# SOURCE #-} Type (coreView, tcView, partitionInvisibleTypes)

import TyCoRep
import TyCon
import Var
import FV

import UniqFM
import VarSet
import VarEnv
import Util
import Panic

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

{- Note [Free variables of types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The family of functions tyCoVarsOfType, tyCoVarsOfTypes etc, returns
a VarSet that is closed over the types of its variables.  More precisely,
  if    S = tyCoVarsOfType( t )
  and   (a:k) is in S
  then  tyCoVarsOftype( k ) is a subset of S

Example: The tyCoVars of this ((a:* -> k) Int) is {a, k}.

We could /not/ close over the kinds of the variable occurrences, and
instead do so at call sites, but it seems that we always want to do
so, so it's easiest to do it here.

It turns out that getting the free variables of types is performance critical,
so we profiled several versions, exploring different implementation strategies.

1. Baseline version: uses FV naively. Essentially:

   tyCoVarsOfType ty = fvVarSet $ tyCoFVsOfType ty

   This is not nice, because FV introduces some overhead to implement
   determinism, and throught its "interesting var" function, neither of which
   we need here, so they are a complete waste.

2. UnionVarSet version: instead of reusing the FV-based code, we simply used
   VarSets directly, trying to avoid the overhead of FV. E.g.:

   -- FV version:
   tyCoFVsOfType (AppTy fun arg)    a b c = (tyCoFVsOfType fun `unionFV` tyCoFVsOfType arg) a b c

   -- UnionVarSet version:
   tyCoVarsOfType (AppTy fun arg)    = (tyCoVarsOfType fun `unionVarSet` tyCoVarsOfType arg)

   This looks deceptively similar, but while FV internally builds a list- and
   set-generating function, the VarSet functions manipulate sets directly, and
   the latter peforms a lot worse than the naive FV version.

3. Accumulator-style VarSet version: this is what we use now. We do use VarSet
   as our data structure, but delegate the actual work to a new
   ty_co_vars_of_...  family of functions, which use accumulator style and the
   "in-scope set" filter found in the internals of FV, but without the
   determinism overhead.

See #14880.

Note [Closing over free variable kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
tyCoVarsOfType and tyCoFVsOfType, while traversing a type, will also close over
free variable kinds. In previous GHC versions, this happened naively: whenever
we would encounter an occurrence of a free type variable, we would close over
its kind. This, however is wrong for two reasons (see #14880):

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

2. Correctness. Imagine we have forall k. b -> 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.

An obvious first approach is to move the closing-over-kinds from the
occurrences of a type variable to after finding the free vars - however, this
turns out to introduce performance regressions, and isn't even entirely
correct.

In fact, it isn't even important *when* we close over kinds; what matters is
that we handle each type var exactly once, and that we do it in the right
context.

So the next approach we tried was to use the "in-scope set" part of FV or the
equivalent argument in the accumulator-style `ty_co_vars_of_type` function, to
say "don't bother with variables we have already closed over". This should work
fine in theory, but the code is complicated and doesn't perform well.

But there is a simpler way, which is implemented here. Consider the two points
above:

1. Efficiency: we now have an accumulator, so the second time we encounter 'a',
   we'll ignore it, certainly not looking at its kind - this is why
   pre-checking set membership before inserting ends up not only being faster,
   but also being correct.

2. Correctness: we have an "in-scope set" (I think we should call it it a
  "bound-var set"), specifying variables that are bound by a forall in the type
  we are traversing; we simply ignore these variables, certainly not looking at
  their kind.

So now 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.

So the solution is easy. The old code was this:

  ty_co_vars_of_type (TyVarTy v) is acc
    | v `elemVarSet` is  = acc
    | v `elemVarSet` acc = acc
    | otherwise          = ty_co_vars_of_type (tyVarKind v) is (extendVarSet acc v)

Now all we need to do is take the free vars of tyVarKind v *with an empty
bound-var set*, thus:

ty_co_vars_of_type (TyVarTy v) is acc
  | v `elemVarSet` is  = acc
  | v `elemVarSet` acc = acc
  | otherwise          = ty_co_vars_of_type (tyVarKind v) emptyVarSet (extendVarSet acc v)
                                                          ^^^^^^^^^^^

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.
-}

tyCoVarsOfType :: Type -> TyCoVarSet
-- See Note [Free variables of types]
tyCoVarsOfType :: Type -> TyCoVarSet
tyCoVarsOfType Type
ty = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
ty TyCoVarSet
emptyVarSet TyCoVarSet
emptyVarSet

tyCoVarsOfTypes :: [Type] -> TyCoVarSet
tyCoVarsOfTypes :: [Type] -> TyCoVarSet
tyCoVarsOfTypes [Type]
tys = [Type] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_types [Type]
tys TyCoVarSet
emptyVarSet TyCoVarSet
emptyVarSet

ty_co_vars_of_type :: Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type :: Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type (TyVarTy Var
v) TyCoVarSet
is TyCoVarSet
acc
  | Var
v Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
is  = TyCoVarSet
acc
  | Var
v Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
acc = TyCoVarSet
acc
  | Bool
otherwise          = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type (Var -> Type
tyVarKind Var
v)
                            TyCoVarSet
emptyVarSet  -- See Note [Closing over free variable kinds]
                            (TyCoVarSet -> Var -> TyCoVarSet
extendVarSet TyCoVarSet
acc Var
v)

ty_co_vars_of_type (TyConApp TyCon
_ [Type]
tys)   TyCoVarSet
is TyCoVarSet
acc = [Type] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_types [Type]
tys TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_type (LitTy {})         TyCoVarSet
_  TyCoVarSet
acc = TyCoVarSet
acc
ty_co_vars_of_type (AppTy Type
fun Type
arg)    TyCoVarSet
is TyCoVarSet
acc = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
fun TyCoVarSet
is (Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
arg TyCoVarSet
is TyCoVarSet
acc)
ty_co_vars_of_type (FunTy AnonArgFlag
_ Type
arg Type
res)  TyCoVarSet
is TyCoVarSet
acc = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
arg TyCoVarSet
is (Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
res TyCoVarSet
is TyCoVarSet
acc)
ty_co_vars_of_type (ForAllTy (Bndr Var
tv ArgFlag
_) Type
ty) TyCoVarSet
is TyCoVarSet
acc = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type (Var -> Type
varType Var
tv) TyCoVarSet
is (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
                                                      Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
ty (TyCoVarSet -> Var -> TyCoVarSet
extendVarSet TyCoVarSet
is Var
tv) TyCoVarSet
acc
ty_co_vars_of_type (CastTy Type
ty KindCoercion
co)     TyCoVarSet
is TyCoVarSet
acc = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
ty TyCoVarSet
is (KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc)
ty_co_vars_of_type (CoercionTy KindCoercion
co)    TyCoVarSet
is TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc

ty_co_vars_of_types :: [Type] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_types :: [Type] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_types []       TyCoVarSet
_  TyCoVarSet
acc = TyCoVarSet
acc
ty_co_vars_of_types (Type
ty:[Type]
tys) TyCoVarSet
is TyCoVarSet
acc = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
ty TyCoVarSet
is ([Type] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_types [Type]
tys TyCoVarSet
is TyCoVarSet
acc)

tyCoVarsOfCo :: Coercion -> TyCoVarSet
-- See Note [Free variables of types]
tyCoVarsOfCo :: KindCoercion -> TyCoVarSet
tyCoVarsOfCo KindCoercion
co = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
emptyVarSet TyCoVarSet
emptyVarSet

tyCoVarsOfCos :: [Coercion] -> TyCoVarSet
tyCoVarsOfCos :: [KindCoercion] -> TyCoVarSet
tyCoVarsOfCos [KindCoercion]
cos = [KindCoercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_cos [KindCoercion]
cos TyCoVarSet
emptyVarSet TyCoVarSet
emptyVarSet


ty_co_vars_of_co :: Coercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co :: KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co (Refl Type
ty)            TyCoVarSet
is TyCoVarSet
acc = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
ty TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (GRefl Role
_ Type
ty MCoercionN
mco)     TyCoVarSet
is TyCoVarSet
acc = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
ty TyCoVarSet
is (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
                                               MCoercionN -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_mco MCoercionN
mco TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (TyConAppCo Role
_ TyCon
_ [KindCoercion]
cos) TyCoVarSet
is TyCoVarSet
acc = [KindCoercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_cos [KindCoercion]
cos TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (AppCo KindCoercion
co KindCoercion
arg)       TyCoVarSet
is TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
                                               KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
arg TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (ForAllCo Var
tv KindCoercion
kind_co KindCoercion
co) TyCoVarSet
is TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
kind_co TyCoVarSet
is (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
                                                   KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co (TyCoVarSet -> Var -> TyCoVarSet
extendVarSet TyCoVarSet
is Var
tv) TyCoVarSet
acc
ty_co_vars_of_co (FunCo Role
_ KindCoercion
co1 KindCoercion
co2)    TyCoVarSet
is TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co1 TyCoVarSet
is (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
                                               KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co2 TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (CoVarCo Var
v)          TyCoVarSet
is TyCoVarSet
acc = Var -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co_var Var
v TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (HoleCo CoercionHole
h)           TyCoVarSet
is TyCoVarSet
acc = Var -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co_var (CoercionHole -> Var
coHoleCoVar CoercionHole
h) TyCoVarSet
is TyCoVarSet
acc
    -- See Note [CoercionHoles and coercion free variables]
ty_co_vars_of_co (AxiomInstCo CoAxiom Branched
_ BranchIndex
_ [KindCoercion]
cos) TyCoVarSet
is TyCoVarSet
acc = [KindCoercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_cos [KindCoercion]
cos TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (UnivCo UnivCoProvenance
p Role
_ Type
t1 Type
t2)    TyCoVarSet
is TyCoVarSet
acc = UnivCoProvenance -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_prov UnivCoProvenance
p TyCoVarSet
is (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
                                                Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
t1 TyCoVarSet
is (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
                                                Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
t2 TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (SymCo KindCoercion
co)          TyCoVarSet
is TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (TransCo KindCoercion
co1 KindCoercion
co2)   TyCoVarSet
is TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co1 TyCoVarSet
is (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
                                              KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co2 TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (NthCo Role
_ BranchIndex
_ KindCoercion
co)      TyCoVarSet
is TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (LRCo LeftOrRight
_ KindCoercion
co)         TyCoVarSet
is TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (InstCo KindCoercion
co KindCoercion
arg)     TyCoVarSet
is TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
                                              KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
arg TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (KindCo KindCoercion
co)         TyCoVarSet
is TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (SubCo KindCoercion
co)          TyCoVarSet
is TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (AxiomRuleCo CoAxiomRule
_ [KindCoercion]
cs)  TyCoVarSet
is TyCoVarSet
acc = [KindCoercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_cos [KindCoercion]
cs TyCoVarSet
is TyCoVarSet
acc

ty_co_vars_of_mco :: MCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_mco :: MCoercionN -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_mco MCoercionN
MRefl    TyCoVarSet
_is TyCoVarSet
acc = TyCoVarSet
acc
ty_co_vars_of_mco (MCo KindCoercion
co) TyCoVarSet
is  TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc

ty_co_vars_of_co_var :: CoVar -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co_var :: Var -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co_var Var
v TyCoVarSet
is TyCoVarSet
acc
  | Var
v Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
is  = TyCoVarSet
acc
  | Var
v Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
acc = TyCoVarSet
acc
  | Bool
otherwise          = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type (Var -> Type
varType Var
v)
                            TyCoVarSet
emptyVarSet  -- See Note [Closing over free variable kinds]
                            (TyCoVarSet -> Var -> TyCoVarSet
extendVarSet TyCoVarSet
acc Var
v)

ty_co_vars_of_cos :: [Coercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_cos :: [KindCoercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_cos []       TyCoVarSet
_  TyCoVarSet
acc = TyCoVarSet
acc
ty_co_vars_of_cos (KindCoercion
co:[KindCoercion]
cos) TyCoVarSet
is TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is ([KindCoercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_cos [KindCoercion]
cos TyCoVarSet
is TyCoVarSet
acc)

tyCoVarsOfProv :: UnivCoProvenance -> TyCoVarSet
tyCoVarsOfProv :: UnivCoProvenance -> TyCoVarSet
tyCoVarsOfProv UnivCoProvenance
prov = UnivCoProvenance -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_prov UnivCoProvenance
prov TyCoVarSet
emptyVarSet TyCoVarSet
emptyVarSet

ty_co_vars_of_prov :: UnivCoProvenance -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_prov :: UnivCoProvenance -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_prov (PhantomProv KindCoercion
co)    TyCoVarSet
is TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_prov (ProofIrrelProv KindCoercion
co) TyCoVarSet
is TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_prov UnivCoProvenance
UnsafeCoerceProv    TyCoVarSet
_  TyCoVarSet
acc = TyCoVarSet
acc
ty_co_vars_of_prov (PluginProv String
_)      TyCoVarSet
_  TyCoVarSet
acc = TyCoVarSet
acc

-- | Generates an in-scope set from the free variables in a list of types
-- and a list of coercions
mkTyCoInScopeSet :: [Type] -> [Coercion] -> InScopeSet
mkTyCoInScopeSet :: [Type] -> [KindCoercion] -> InScopeSet
mkTyCoInScopeSet [Type]
tys [KindCoercion]
cos
  = TyCoVarSet -> InScopeSet
mkInScopeSet ([Type] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_types [Type]
tys TyCoVarSet
emptyVarSet (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
                  [KindCoercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_cos   [KindCoercion]
cos TyCoVarSet
emptyVarSet TyCoVarSet
emptyVarSet)

-- | `tyCoFVsOfType` that returns free variables of a type in a deterministic
-- set. For explanation of why using `VarSet` is not deterministic see
-- Note [Deterministic FV] in FV.
tyCoVarsOfTypeDSet :: Type -> DTyCoVarSet
-- See Note [Free variables of types]
tyCoVarsOfTypeDSet :: Type -> DTyCoVarSet
tyCoVarsOfTypeDSet Type
ty = FV -> DTyCoVarSet
fvDVarSet (FV -> DTyCoVarSet) -> FV -> DTyCoVarSet
forall a b. (a -> b) -> a -> b
$ Type -> FV
tyCoFVsOfType Type
ty

-- | `tyCoFVsOfType` that returns free variables of a type in deterministic
-- order. For explanation of why using `VarSet` is not deterministic see
-- Note [Deterministic FV] in FV.
tyCoVarsOfTypeList :: Type -> [TyCoVar]
-- See Note [Free variables of types]
tyCoVarsOfTypeList :: Type -> [Var]
tyCoVarsOfTypeList Type
ty = FV -> [Var]
fvVarList (FV -> [Var]) -> FV -> [Var]
forall a b. (a -> b) -> a -> b
$ Type -> FV
tyCoFVsOfType Type
ty

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

-- | 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 [Free variables of types]
tyCoVarsOfTypesDSet :: [Type] -> DTyCoVarSet
tyCoVarsOfTypesDSet [Type]
tys = FV -> DTyCoVarSet
fvDVarSet (FV -> DTyCoVarSet) -> FV -> DTyCoVarSet
forall a b. (a -> b) -> a -> b
$ [Type] -> FV
tyCoFVsOfTypes [Type]
tys

-- | 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 [Free variables of types]
tyCoVarsOfTypesList :: [Type] -> [Var]
tyCoVarsOfTypesList [Type]
tys = FV -> [Var]
fvVarList (FV -> [Var]) -> FV -> [Var]
forall a b. (a -> b) -> a -> b
$ [Type] -> FV
tyCoFVsOfTypes [Type]
tys

{-
************************************************************************
*                                                                      *
          The "exact" free variables of a type
*                                                                      *
************************************************************************

Note [Silly type synonym]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
  type T a = Int
What are the free tyvars of (T x)?  Empty, of course!

exactTyCoVarsOfType is used by the type checker to figure out exactly
which type variables are mentioned in a type.  It only matters
occasionally -- see the calls to exactTyCoVarsOfType.
-}

exactTyCoVarsOfType :: Type -> TyCoVarSet
-- Find the free type variables (of any kind)
-- but *expand* type synonyms.  See Note [Silly type synonym] above.
exactTyCoVarsOfType :: Type -> TyCoVarSet
exactTyCoVarsOfType Type
ty
  = Type -> TyCoVarSet
go Type
ty
  where
    go :: Type -> TyCoVarSet
go Type
ty | Just Type
ty' <- Type -> Maybe Type
tcView Type
ty = Type -> TyCoVarSet
go Type
ty'  -- This is the key line
    go (TyVarTy Var
tv)         = Var -> TyCoVarSet
goVar Var
tv
    go (TyConApp TyCon
_ [Type]
tys)     = [Type] -> TyCoVarSet
exactTyCoVarsOfTypes [Type]
tys
    go (LitTy {})           = TyCoVarSet
emptyVarSet
    go (AppTy Type
fun Type
arg)      = Type -> TyCoVarSet
go Type
fun TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
go Type
arg
    go (FunTy AnonArgFlag
_ Type
arg Type
res)    = Type -> TyCoVarSet
go Type
arg TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
go Type
res
    go (ForAllTy VarBndr Var ArgFlag
bndr Type
ty)   = TyCoVarSet -> VarBndr Var ArgFlag -> TyCoVarSet
delBinderVar (Type -> TyCoVarSet
go Type
ty) VarBndr Var ArgFlag
bndr TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
go (VarBndr Var ArgFlag -> Type
forall argf. VarBndr Var argf -> Type
binderType VarBndr Var ArgFlag
bndr)
    go (CastTy Type
ty KindCoercion
co)       = Type -> TyCoVarSet
go Type
ty TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` KindCoercion -> TyCoVarSet
goCo KindCoercion
co
    go (CoercionTy KindCoercion
co)      = KindCoercion -> TyCoVarSet
goCo KindCoercion
co

    goMCo :: MCoercionN -> TyCoVarSet
goMCo MCoercionN
MRefl    = TyCoVarSet
emptyVarSet
    goMCo (MCo KindCoercion
co) = KindCoercion -> TyCoVarSet
goCo KindCoercion
co

    goCo :: KindCoercion -> TyCoVarSet
goCo (Refl Type
ty)            = Type -> TyCoVarSet
go Type
ty
    goCo (GRefl Role
_ Type
ty MCoercionN
mco)     = Type -> TyCoVarSet
go Type
ty TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` MCoercionN -> TyCoVarSet
goMCo MCoercionN
mco
    goCo (TyConAppCo Role
_ TyCon
_ [KindCoercion]
args)= [KindCoercion] -> TyCoVarSet
goCos [KindCoercion]
args
    goCo (AppCo KindCoercion
co KindCoercion
arg)     = KindCoercion -> TyCoVarSet
goCo KindCoercion
co TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` KindCoercion -> TyCoVarSet
goCo KindCoercion
arg
    goCo (ForAllCo Var
tv KindCoercion
k_co KindCoercion
co)
      = KindCoercion -> TyCoVarSet
goCo KindCoercion
co TyCoVarSet -> Var -> TyCoVarSet
`delVarSet` Var
tv TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` KindCoercion -> TyCoVarSet
goCo KindCoercion
k_co
    goCo (FunCo Role
_ KindCoercion
co1 KindCoercion
co2)   = KindCoercion -> TyCoVarSet
goCo KindCoercion
co1 TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` KindCoercion -> TyCoVarSet
goCo KindCoercion
co2
    goCo (CoVarCo Var
v)         = Var -> TyCoVarSet
goVar Var
v
    goCo (HoleCo CoercionHole
h)          = Var -> TyCoVarSet
goVar (CoercionHole -> Var
coHoleCoVar CoercionHole
h)
    goCo (AxiomInstCo CoAxiom Branched
_ BranchIndex
_ [KindCoercion]
args) = [KindCoercion] -> TyCoVarSet
goCos [KindCoercion]
args
    goCo (UnivCo UnivCoProvenance
p Role
_ Type
t1 Type
t2)  = UnivCoProvenance -> TyCoVarSet
goProv UnivCoProvenance
p TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
go Type
t1 TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
go Type
t2
    goCo (SymCo KindCoercion
co)          = KindCoercion -> TyCoVarSet
goCo KindCoercion
co
    goCo (TransCo KindCoercion
co1 KindCoercion
co2)   = KindCoercion -> TyCoVarSet
goCo KindCoercion
co1 TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` KindCoercion -> TyCoVarSet
goCo KindCoercion
co2
    goCo (NthCo Role
_ BranchIndex
_ KindCoercion
co)      = KindCoercion -> TyCoVarSet
goCo KindCoercion
co
    goCo (LRCo LeftOrRight
_ KindCoercion
co)         = KindCoercion -> TyCoVarSet
goCo KindCoercion
co
    goCo (InstCo KindCoercion
co KindCoercion
arg)     = KindCoercion -> TyCoVarSet
goCo KindCoercion
co TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` KindCoercion -> TyCoVarSet
goCo KindCoercion
arg
    goCo (KindCo KindCoercion
co)         = KindCoercion -> TyCoVarSet
goCo KindCoercion
co
    goCo (SubCo KindCoercion
co)          = KindCoercion -> TyCoVarSet
goCo KindCoercion
co
    goCo (AxiomRuleCo CoAxiomRule
_ [KindCoercion]
c)   = [KindCoercion] -> TyCoVarSet
goCos [KindCoercion]
c

    goCos :: [KindCoercion] -> TyCoVarSet
goCos [KindCoercion]
cos = (KindCoercion -> TyCoVarSet -> TyCoVarSet)
-> TyCoVarSet -> [KindCoercion] -> TyCoVarSet
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (TyCoVarSet -> TyCoVarSet -> TyCoVarSet
unionVarSet (TyCoVarSet -> TyCoVarSet -> TyCoVarSet)
-> (KindCoercion -> TyCoVarSet)
-> KindCoercion
-> TyCoVarSet
-> TyCoVarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KindCoercion -> TyCoVarSet
goCo) TyCoVarSet
emptyVarSet [KindCoercion]
cos

    goProv :: UnivCoProvenance -> TyCoVarSet
goProv UnivCoProvenance
UnsafeCoerceProv     = TyCoVarSet
emptyVarSet
    goProv (PhantomProv KindCoercion
kco)    = KindCoercion -> TyCoVarSet
goCo KindCoercion
kco
    goProv (ProofIrrelProv KindCoercion
kco) = KindCoercion -> TyCoVarSet
goCo KindCoercion
kco
    goProv (PluginProv String
_)       = TyCoVarSet
emptyVarSet

    goVar :: Var -> TyCoVarSet
goVar Var
v = Var -> TyCoVarSet
unitVarSet Var
v TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
go (Var -> Type
varType Var
v)

exactTyCoVarsOfTypes :: [Type] -> TyVarSet
exactTyCoVarsOfTypes :: [Type] -> TyCoVarSet
exactTyCoVarsOfTypes [Type]
tys = (Type -> TyCoVarSet) -> [Type] -> TyCoVarSet
forall a. (a -> TyCoVarSet) -> [a] -> TyCoVarSet
mapUnionVarSet Type -> TyCoVarSet
exactTyCoVarsOfType [Type]
tys

-- | The worker for `tyCoFVsOfType` and `tyCoFVsOfTypeList`.
-- The previous implementation used `unionVarSet` which is O(n+m) and can
-- make the function quadratic.
-- It's exported, so that it can be composed with
-- other functions that compute free variables.
-- See Note [FV naming conventions] in FV.
--
-- Eta-expanded because that makes it run faster (apparently)
-- See Note [FV eta expansion] in FV for explanation.
tyCoFVsOfType :: Type -> FV
-- See Note [Free variables of types]
tyCoFVsOfType :: Type -> FV
tyCoFVsOfType (TyVarTy Var
v)        InterestingVarFun
f TyCoVarSet
bound_vars ([Var]
acc_list, TyCoVarSet
acc_set)
  | Bool -> Bool
not (InterestingVarFun
f Var
v) = ([Var]
acc_list, TyCoVarSet
acc_set)
  | Var
v Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
bound_vars = ([Var]
acc_list, TyCoVarSet
acc_set)
  | Var
v Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
acc_set = ([Var]
acc_list, TyCoVarSet
acc_set)
  | Bool
otherwise = Type -> FV
tyCoFVsOfType (Var -> Type
tyVarKind Var
v) InterestingVarFun
f
                               TyCoVarSet
emptyVarSet   -- See Note [Closing over free variable kinds]
                               (Var
vVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
acc_list, TyCoVarSet -> Var -> TyCoVarSet
extendVarSet TyCoVarSet
acc_set Var
v)
tyCoFVsOfType (TyConApp TyCon
_ [Type]
tys)   InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc = [Type] -> FV
tyCoFVsOfTypes [Type]
tys InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc
tyCoFVsOfType (LitTy {})         InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc = FV
emptyFV InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc
tyCoFVsOfType (AppTy Type
fun Type
arg)    InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc = (Type -> FV
tyCoFVsOfType Type
fun FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
arg) InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc
tyCoFVsOfType (FunTy AnonArgFlag
_ Type
arg Type
res)  InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc = (Type -> FV
tyCoFVsOfType Type
arg FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
res) InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc
tyCoFVsOfType (ForAllTy VarBndr Var ArgFlag
bndr Type
ty) InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc = VarBndr Var ArgFlag -> FV -> FV
tyCoFVsBndr VarBndr Var ArgFlag
bndr (Type -> FV
tyCoFVsOfType Type
ty)  InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc
tyCoFVsOfType (CastTy Type
ty KindCoercion
co)     InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc = (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co) InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc
tyCoFVsOfType (CoercionTy KindCoercion
co)    InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc

tyCoFVsBndr :: TyCoVarBinder -> FV -> FV
-- Free vars of (forall b. <thing with fvs>)
tyCoFVsBndr :: VarBndr Var ArgFlag -> FV -> FV
tyCoFVsBndr (Bndr Var
tv ArgFlag
_) FV
fvs = Var -> FV -> FV
tyCoFVsVarBndr Var
tv FV
fvs

tyCoFVsVarBndrs :: [Var] -> FV -> FV
tyCoFVsVarBndrs :: [Var] -> FV -> FV
tyCoFVsVarBndrs [Var]
vars FV
fvs = (Var -> FV -> FV) -> FV -> [Var] -> FV
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Var -> FV -> FV
tyCoFVsVarBndr FV
fvs [Var]
vars

tyCoFVsVarBndr :: Var -> FV -> FV
tyCoFVsVarBndr :: Var -> FV -> FV
tyCoFVsVarBndr Var
var FV
fvs
  = Type -> FV
tyCoFVsOfType (Var -> Type
varType Var
var)   -- Free vars of its type/kind
    FV -> FV -> FV
`unionFV` Var -> FV -> FV
delFV Var
var FV
fvs       -- Delete it from the thing-inside

tyCoFVsOfTypes :: [Type] -> FV
-- See Note [Free variables of types]
tyCoFVsOfTypes :: [Type] -> FV
tyCoFVsOfTypes (Type
ty:[Type]
tys) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc = (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` [Type] -> FV
tyCoFVsOfTypes [Type]
tys) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfTypes []       InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc

-- | Get a deterministic set of the vars free in a coercion
tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet
-- See Note [Free variables of types]
tyCoVarsOfCoDSet :: KindCoercion -> DTyCoVarSet
tyCoVarsOfCoDSet KindCoercion
co = FV -> DTyCoVarSet
fvDVarSet (FV -> DTyCoVarSet) -> FV -> DTyCoVarSet
forall a b. (a -> b) -> a -> b
$ KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co

tyCoVarsOfCoList :: Coercion -> [TyCoVar]
-- See Note [Free variables of types]
tyCoVarsOfCoList :: KindCoercion -> [Var]
tyCoVarsOfCoList KindCoercion
co = FV -> [Var]
fvVarList (FV -> [Var]) -> FV -> [Var]
forall a b. (a -> b) -> a -> b
$ KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co

tyCoFVsOfMCo :: MCoercion -> FV
tyCoFVsOfMCo :: MCoercionN -> FV
tyCoFVsOfMCo MCoercionN
MRefl    = FV
emptyFV
tyCoFVsOfMCo (MCo KindCoercion
co) = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co

tyCoVarsOfCosSet :: CoVarEnv Coercion -> TyCoVarSet
tyCoVarsOfCosSet :: CoVarEnv KindCoercion -> TyCoVarSet
tyCoVarsOfCosSet CoVarEnv KindCoercion
cos = [KindCoercion] -> TyCoVarSet
tyCoVarsOfCos ([KindCoercion] -> TyCoVarSet) -> [KindCoercion] -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$ CoVarEnv KindCoercion -> [KindCoercion]
forall elt. UniqFM elt -> [elt]
nonDetEltsUFM CoVarEnv KindCoercion
cos
  -- It's OK to use nonDetEltsUFM here because we immediately forget the
  -- ordering by returning a set

tyCoFVsOfCo :: Coercion -> FV
-- Extracts type and coercion variables from a coercion
-- See Note [Free variables of types]
tyCoFVsOfCo :: KindCoercion -> FV
tyCoFVsOfCo (Refl Type
ty) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
  = Type -> FV
tyCoFVsOfType Type
ty InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (GRefl Role
_ Type
ty MCoercionN
mco) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
  = (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` MCoercionN -> FV
tyCoFVsOfMCo MCoercionN
mco) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (TyConAppCo Role
_ TyCon
_ [KindCoercion]
cos) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc = [KindCoercion] -> FV
tyCoFVsOfCos [KindCoercion]
cos InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (AppCo KindCoercion
co KindCoercion
arg) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
  = (KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co FV -> FV -> FV
`unionFV` KindCoercion -> FV
tyCoFVsOfCo KindCoercion
arg) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (ForAllCo Var
tv KindCoercion
kind_co KindCoercion
co) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
  = (Var -> FV -> FV
tyCoFVsVarBndr Var
tv (KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co) FV -> FV -> FV
`unionFV` KindCoercion -> FV
tyCoFVsOfCo KindCoercion
kind_co) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (FunCo Role
_ KindCoercion
co1 KindCoercion
co2)    InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
  = (KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co1 FV -> FV -> FV
`unionFV` KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co2) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (CoVarCo Var
v) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
  = Var -> FV
tyCoFVsOfCoVar Var
v InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (HoleCo CoercionHole
h) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
  = Var -> FV
tyCoFVsOfCoVar (CoercionHole -> Var
coHoleCoVar CoercionHole
h) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
    -- See Note [CoercionHoles and coercion free variables]
tyCoFVsOfCo (AxiomInstCo CoAxiom Branched
_ BranchIndex
_ [KindCoercion]
cos) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc = [KindCoercion] -> FV
tyCoFVsOfCos [KindCoercion]
cos InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (UnivCo UnivCoProvenance
p Role
_ Type
t1 Type
t2) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
  = (UnivCoProvenance -> FV
tyCoFVsOfProv UnivCoProvenance
p FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
t1
                     FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
t2) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (SymCo KindCoercion
co)          InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (TransCo KindCoercion
co1 KindCoercion
co2)   InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc = (KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co1 FV -> FV -> FV
`unionFV` KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co2) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (NthCo Role
_ BranchIndex
_ KindCoercion
co)      InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (LRCo LeftOrRight
_ KindCoercion
co)         InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (InstCo KindCoercion
co KindCoercion
arg)     InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc = (KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co FV -> FV -> FV
`unionFV` KindCoercion -> FV
tyCoFVsOfCo KindCoercion
arg) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (KindCo KindCoercion
co)         InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (SubCo KindCoercion
co)          InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (AxiomRuleCo CoAxiomRule
_ [KindCoercion]
cs)  InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc = [KindCoercion] -> FV
tyCoFVsOfCos [KindCoercion]
cs InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc

tyCoFVsOfCoVar :: CoVar -> FV
tyCoFVsOfCoVar :: Var -> FV
tyCoFVsOfCoVar Var
v InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
  = (Var -> FV
unitFV Var
v FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType (Var -> Type
varType Var
v)) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc

tyCoFVsOfProv :: UnivCoProvenance -> FV
tyCoFVsOfProv :: UnivCoProvenance -> FV
tyCoFVsOfProv UnivCoProvenance
UnsafeCoerceProv    InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfProv (PhantomProv KindCoercion
co)    InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfProv (ProofIrrelProv KindCoercion
co) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfProv (PluginProv String
_)      InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc

tyCoFVsOfCos :: [Coercion] -> FV
tyCoFVsOfCos :: [KindCoercion] -> FV
tyCoFVsOfCos []       InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCos (KindCoercion
co:[KindCoercion]
cos) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc = (KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co FV -> FV -> FV
`unionFV` [KindCoercion] -> FV
tyCoFVsOfCos [KindCoercion]
cos) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc


------------- Extracting the CoVars of a type or coercion -----------

{-

Note [CoVarsOfX and the InterestingVarFun]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

The coVarsOfType, coVarsOfTypes, coVarsOfCo, and coVarsOfCos functions are
implemented in terms of the respective FV equivalents (tyCoFVsOf...), rather
than the VarSet-based flavors (tyCoVarsOf...), despite the performance
considerations outlined in Note [Free variables of types].

This is because FV includes the InterestingVarFun, which is useful here,
because we can cleverly use it to restrict our calculations to CoVars - this
is what getCoVarSet achieves.

See #14880.

-}

getCoVarSet :: FV -> CoVarSet
getCoVarSet :: FV -> TyCoVarSet
getCoVarSet FV
fv = ([Var], TyCoVarSet) -> TyCoVarSet
forall a b. (a, b) -> b
snd (FV
fv InterestingVarFun
isCoVar TyCoVarSet
emptyVarSet ([], TyCoVarSet
emptyVarSet))

coVarsOfType :: Type -> CoVarSet
coVarsOfType :: Type -> TyCoVarSet
coVarsOfType Type
ty = FV -> TyCoVarSet
getCoVarSet (Type -> FV
tyCoFVsOfType Type
ty)

coVarsOfTypes :: [Type] -> TyCoVarSet
coVarsOfTypes :: [Type] -> TyCoVarSet
coVarsOfTypes [Type]
tys = FV -> TyCoVarSet
getCoVarSet ([Type] -> FV
tyCoFVsOfTypes [Type]
tys)

coVarsOfCo :: Coercion -> CoVarSet
coVarsOfCo :: KindCoercion -> TyCoVarSet
coVarsOfCo KindCoercion
co = FV -> TyCoVarSet
getCoVarSet (KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co)

coVarsOfCos :: [Coercion] -> CoVarSet
coVarsOfCos :: [KindCoercion] -> TyCoVarSet
coVarsOfCos [KindCoercion]
cos = FV -> TyCoVarSet
getCoVarSet ([KindCoercion] -> FV
tyCoFVsOfCos [KindCoercion]
cos)

----- 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 last wrinkle in Note [Unused coercion variable in ForAllCo] in Coercion
almostDevoidCoVarOfCo :: CoVar -> Coercion -> Bool
almostDevoidCoVarOfCo :: Var -> KindCoercion -> Bool
almostDevoidCoVarOfCo Var
cv KindCoercion
co =
  KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv

almost_devoid_co_var_of_co :: Coercion -> CoVar -> Bool
almost_devoid_co_var_of_co :: KindCoercion -> InterestingVarFun
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
_ [KindCoercion]
cos) Var
cv
  = [KindCoercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [KindCoercion]
cos Var
cv
almost_devoid_co_var_of_co (AppCo KindCoercion
co KindCoercion
arg) Var
cv
  = KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
  Bool -> Bool -> Bool
&& KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
arg Var
cv
almost_devoid_co_var_of_co (ForAllCo Var
v KindCoercion
kind_co KindCoercion
co) Var
cv
  = KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
kind_co Var
cv
  Bool -> Bool -> Bool
&& (Var
v Var -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
== Var
cv Bool -> Bool -> Bool
|| KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv)
almost_devoid_co_var_of_co (FunCo Role
_ KindCoercion
co1 KindCoercion
co2) Var
cv
  = KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co1 Var
cv
  Bool -> Bool -> Bool
&& KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co2 Var
cv
almost_devoid_co_var_of_co (CoVarCo Var
v) Var
cv = Var
v Var -> InterestingVarFun
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 -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
/= Var
cv
almost_devoid_co_var_of_co (AxiomInstCo CoAxiom Branched
_ BranchIndex
_ [KindCoercion]
cos) Var
cv
  = [KindCoercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [KindCoercion]
cos Var
cv
almost_devoid_co_var_of_co (UnivCo UnivCoProvenance
p Role
_ Type
t1 Type
t2) Var
cv
  = UnivCoProvenance -> InterestingVarFun
almost_devoid_co_var_of_prov UnivCoProvenance
p Var
cv
  Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
t1 Var
cv
  Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
t2 Var
cv
almost_devoid_co_var_of_co (SymCo KindCoercion
co) Var
cv
  = KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
almost_devoid_co_var_of_co (TransCo KindCoercion
co1 KindCoercion
co2) Var
cv
  = KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co1 Var
cv
  Bool -> Bool -> Bool
&& KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co2 Var
cv
almost_devoid_co_var_of_co (NthCo Role
_ BranchIndex
_ KindCoercion
co) Var
cv
  = KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
almost_devoid_co_var_of_co (LRCo LeftOrRight
_ KindCoercion
co) Var
cv
  = KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
almost_devoid_co_var_of_co (InstCo KindCoercion
co KindCoercion
arg) Var
cv
  = KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
  Bool -> Bool -> Bool
&& KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
arg Var
cv
almost_devoid_co_var_of_co (KindCo KindCoercion
co) Var
cv
  = KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
almost_devoid_co_var_of_co (SubCo KindCoercion
co) Var
cv
  = KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
almost_devoid_co_var_of_co (AxiomRuleCo CoAxiomRule
_ [KindCoercion]
cs) Var
cv
  = [KindCoercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [KindCoercion]
cs Var
cv

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

almost_devoid_co_var_of_prov :: UnivCoProvenance -> CoVar -> Bool
almost_devoid_co_var_of_prov :: UnivCoProvenance -> InterestingVarFun
almost_devoid_co_var_of_prov (PhantomProv KindCoercion
co) Var
cv
  = KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
almost_devoid_co_var_of_prov (ProofIrrelProv KindCoercion
co) Var
cv
  = KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
almost_devoid_co_var_of_prov UnivCoProvenance
UnsafeCoerceProv Var
_ = Bool
True
almost_devoid_co_var_of_prov (PluginProv String
_) Var
_ = Bool
True

almost_devoid_co_var_of_type :: Type -> CoVar -> Bool
almost_devoid_co_var_of_type :: Type -> InterestingVarFun
almost_devoid_co_var_of_type (TyVarTy Var
_) Var
_ = Bool
True
almost_devoid_co_var_of_type (TyConApp TyCon
_ [Type]
tys) Var
cv
  = [Type] -> InterestingVarFun
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 -> InterestingVarFun
almost_devoid_co_var_of_type Type
fun Var
cv
  Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
arg Var
cv
almost_devoid_co_var_of_type (FunTy AnonArgFlag
_ Type
arg Type
res) Var
cv
  = Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
arg Var
cv
  Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
res Var
cv
almost_devoid_co_var_of_type (ForAllTy (Bndr Var
v ArgFlag
_) Type
ty) Var
cv
  = Type -> InterestingVarFun
almost_devoid_co_var_of_type (Var -> Type
varType Var
v) Var
cv
  Bool -> Bool -> Bool
&& (Var
v Var -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
== Var
cv Bool -> Bool -> Bool
|| Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
ty Var
cv)
almost_devoid_co_var_of_type (CastTy Type
ty KindCoercion
co) Var
cv
  = Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
ty Var
cv
  Bool -> Bool -> Bool
&& KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
almost_devoid_co_var_of_type (CoercionTy KindCoercion
co) Var
cv
  = KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv

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

------------- Injective free vars -----------------

-- | 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 FamInst.
                    -> Type -> FV
injectiveVarsOfType :: Bool -> Type -> FV
injectiveVarsOfType Bool
look_under_tfs = Type -> FV
go
  where
    go :: Type -> FV
go Type
ty                 | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty
                          = Type -> FV
go Type
ty'
    go (TyVarTy Var
v)        = Var -> FV
unitFV Var
v FV -> FV -> FV
`unionFV` Type -> FV
go (Var -> Type
tyVarKind Var
v)
    go (AppTy Type
f Type
a)        = Type -> FV
go Type
f FV -> FV -> FV
`unionFV` Type -> FV
go Type
a
    go (FunTy AnonArgFlag
_ Type
ty1 Type
ty2)  = Type -> FV
go Type
ty1 FV -> FV -> FV
`unionFV` Type -> FV
go Type
ty2
    go (TyConApp TyCon
tc [Type]
tys)  =
      case TyCon -> Injectivity
tyConInjectivityInfo TyCon
tc of
        Injective [Bool]
inj
          |  Bool
look_under_tfs Bool -> Bool -> Bool
|| Bool -> Bool
not (TyCon -> Bool
isTypeFamilyTyCon TyCon
tc)
          -> (Type -> FV) -> [Type] -> FV
forall a. (a -> FV) -> [a] -> FV
mapUnionFV Type -> FV
go ([Type] -> FV) -> [Type] -> FV
forall a b. (a -> b) -> a -> b
$
             [Bool] -> [Type] -> [Type]
forall a. [Bool] -> [a] -> [a]
filterByList ([Bool]
inj [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
        Injectivity
_ -> FV
emptyFV
    go (ForAllTy (Bndr Var
tv ArgFlag
_) Type
ty) = Type -> FV
go (Var -> Type
tyVarKind Var
tv) FV -> FV -> FV
`unionFV` Var -> FV -> FV
delFV Var
tv (Type -> FV
go Type
ty)
    go LitTy{}                   = FV
emptyFV
    go (CastTy Type
ty KindCoercion
_)             = Type -> FV
go Type
ty
    go CoercionTy{}              = FV
emptyFV

-- | 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 FamInst.
                     -> [Type] -> FV
injectiveVarsOfTypes :: Bool -> [Type] -> FV
injectiveVarsOfTypes Bool
look_under_tfs = (Type -> FV) -> [Type] -> FV
forall a. (a -> FV) -> [a] -> FV
mapUnionFV (Bool -> Type -> FV
injectiveVarsOfType Bool
look_under_tfs)


------------- 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, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep
invisibleVarsOfType :: Type -> FV
invisibleVarsOfType :: Type -> FV
invisibleVarsOfType = Type -> FV
go
  where
    go :: Type -> FV
go Type
ty                 | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty
                          = Type -> FV
go Type
ty'
    go (TyVarTy Var
v)        = Type -> FV
go (Var -> Type
tyVarKind Var
v)
    go (AppTy Type
f Type
a)        = Type -> FV
go Type
f FV -> FV -> FV
`unionFV` Type -> FV
go Type
a
    go (FunTy AnonArgFlag
_ Type
ty1 Type
ty2)  = Type -> FV
go Type
ty1 FV -> FV -> FV
`unionFV` Type -> FV
go Type
ty2
    go (TyConApp TyCon
tc [Type]
tys)  = [Type] -> FV
tyCoFVsOfTypes [Type]
invisibles FV -> FV -> FV
`unionFV`
                            [Type] -> FV
invisibleVarsOfTypes [Type]
visibles
      where ([Type]
invisibles, [Type]
visibles) = TyCon -> [Type] -> ([Type], [Type])
partitionInvisibleTypes TyCon
tc [Type]
tys
    go (ForAllTy VarBndr Var ArgFlag
tvb Type
ty)  = VarBndr Var ArgFlag -> FV -> FV
tyCoFVsBndr VarBndr Var ArgFlag
tvb (FV -> FV) -> FV -> FV
forall a b. (a -> b) -> a -> b
$ Type -> FV
go Type
ty
    go LitTy{}            = FV
emptyFV
    go (CastTy Type
ty KindCoercion
co)     = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co FV -> FV -> FV
`unionFV` Type -> FV
go Type
ty
    go (CoercionTy KindCoercion
co)    = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co

-- | Like 'invisibleVarsOfType', but for many types.
invisibleVarsOfTypes :: [Type] -> FV
invisibleVarsOfTypes :: [Type] -> FV
invisibleVarsOfTypes = (Type -> FV) -> [Type] -> FV
forall a. (a -> FV) -> [a] -> FV
mapUnionFV Type -> FV
invisibleVarsOfType


------------- No free vars -----------------

-- | Returns True if this type has no free variables. Should be the same as
-- isEmptyVarSet . tyCoVarsOfType, but faster in the non-forall case.
noFreeVarsOfType :: Type -> Bool
noFreeVarsOfType :: Type -> Bool
noFreeVarsOfType (TyVarTy Var
_)      = Bool
False
noFreeVarsOfType (AppTy Type
t1 Type
t2)    = Type -> Bool
noFreeVarsOfType Type
t1 Bool -> Bool -> Bool
&& Type -> Bool
noFreeVarsOfType Type
t2
noFreeVarsOfType (TyConApp TyCon
_ [Type]
tys) = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
noFreeVarsOfType [Type]
tys
noFreeVarsOfType ty :: Type
ty@(ForAllTy {}) = TyCoVarSet -> Bool
isEmptyVarSet (Type -> TyCoVarSet
tyCoVarsOfType Type
ty)
noFreeVarsOfType (FunTy AnonArgFlag
_ Type
t1 Type
t2)  = Type -> Bool
noFreeVarsOfType Type
t1 Bool -> Bool -> Bool
&& Type -> Bool
noFreeVarsOfType Type
t2
noFreeVarsOfType (LitTy TyLit
_)        = Bool
True
noFreeVarsOfType (CastTy Type
ty KindCoercion
co)   = Type -> Bool
noFreeVarsOfType Type
ty Bool -> Bool -> Bool
&& KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co
noFreeVarsOfType (CoercionTy KindCoercion
co)  = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co

noFreeVarsOfMCo :: MCoercion -> Bool
noFreeVarsOfMCo :: MCoercionN -> Bool
noFreeVarsOfMCo MCoercionN
MRefl    = Bool
True
noFreeVarsOfMCo (MCo KindCoercion
co) = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co

noFreeVarsOfTypes :: [Type] -> Bool
noFreeVarsOfTypes :: [Type] -> Bool
noFreeVarsOfTypes = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
noFreeVarsOfType

-- | Returns True if this coercion has no free variables. Should be the same as
-- isEmptyVarSet . tyCoVarsOfCo, but faster in the non-forall case.
noFreeVarsOfCo :: Coercion -> Bool
noFreeVarsOfCo :: KindCoercion -> Bool
noFreeVarsOfCo (Refl Type
ty)              = Type -> Bool
noFreeVarsOfType Type
ty
noFreeVarsOfCo (GRefl Role
_ Type
ty MCoercionN
co)        = Type -> Bool
noFreeVarsOfType Type
ty Bool -> Bool -> Bool
&& MCoercionN -> Bool
noFreeVarsOfMCo MCoercionN
co
noFreeVarsOfCo (TyConAppCo Role
_ TyCon
_ [KindCoercion]
args)  = (KindCoercion -> Bool) -> [KindCoercion] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all KindCoercion -> Bool
noFreeVarsOfCo [KindCoercion]
args
noFreeVarsOfCo (AppCo KindCoercion
c1 KindCoercion
c2)          = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
c1 Bool -> Bool -> Bool
&& KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
c2
noFreeVarsOfCo co :: KindCoercion
co@(ForAllCo {})       = TyCoVarSet -> Bool
isEmptyVarSet (KindCoercion -> TyCoVarSet
tyCoVarsOfCo KindCoercion
co)
noFreeVarsOfCo (FunCo Role
_ KindCoercion
c1 KindCoercion
c2)        = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
c1 Bool -> Bool -> Bool
&& KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
c2
noFreeVarsOfCo (CoVarCo Var
_)            = Bool
False
noFreeVarsOfCo (HoleCo {})            = Bool
True    -- I'm unsure; probably never happens
noFreeVarsOfCo (AxiomInstCo CoAxiom Branched
_ BranchIndex
_ [KindCoercion]
args) = (KindCoercion -> Bool) -> [KindCoercion] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all KindCoercion -> Bool
noFreeVarsOfCo [KindCoercion]
args
noFreeVarsOfCo (UnivCo UnivCoProvenance
p Role
_ Type
t1 Type
t2)     = UnivCoProvenance -> Bool
noFreeVarsOfProv UnivCoProvenance
p Bool -> Bool -> Bool
&&
                                        Type -> Bool
noFreeVarsOfType Type
t1 Bool -> Bool -> Bool
&&
                                        Type -> Bool
noFreeVarsOfType Type
t2
noFreeVarsOfCo (SymCo KindCoercion
co)             = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co
noFreeVarsOfCo (TransCo KindCoercion
co1 KindCoercion
co2)      = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co1 Bool -> Bool -> Bool
&& KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co2
noFreeVarsOfCo (NthCo Role
_ BranchIndex
_ KindCoercion
co)         = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co
noFreeVarsOfCo (LRCo LeftOrRight
_ KindCoercion
co)            = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co
noFreeVarsOfCo (InstCo KindCoercion
co1 KindCoercion
co2)       = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co1 Bool -> Bool -> Bool
&& KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co2
noFreeVarsOfCo (KindCo KindCoercion
co)            = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co
noFreeVarsOfCo (SubCo KindCoercion
co)             = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co
noFreeVarsOfCo (AxiomRuleCo CoAxiomRule
_ [KindCoercion]
cs)     = (KindCoercion -> Bool) -> [KindCoercion] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all KindCoercion -> Bool
noFreeVarsOfCo [KindCoercion]
cs

-- | Returns True if this UnivCoProv has no free variables. Should be the same as
-- isEmptyVarSet . tyCoVarsOfProv, but faster in the non-forall case.
noFreeVarsOfProv :: UnivCoProvenance -> Bool
noFreeVarsOfProv :: UnivCoProvenance -> Bool
noFreeVarsOfProv UnivCoProvenance
UnsafeCoerceProv    = Bool
True
noFreeVarsOfProv (PhantomProv KindCoercion
co)    = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co
noFreeVarsOfProv (ProofIrrelProv KindCoercion
co) = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co
noFreeVarsOfProv (PluginProv {})     = Bool
True

{-
%************************************************************************
%*                                                                      *
         Well-scoped tyvars
*                                                                      *
************************************************************************

Note [ScopedSort]
~~~~~~~~~~~~~~~~~
Consider

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

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

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

We thus state:

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

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

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

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

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

-}

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

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

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

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

    insert :: TyCoVar       -- var to insert
           -> [TyCoVar]     -- sorted list, in reverse order
           -> [TyCoVarSet]  -- list of fvs, as above
           -> ([TyCoVar], [TyCoVarSet])   -- augmented lists
    insert :: Var -> [Var] -> [TyCoVarSet] -> ([Var], [TyCoVarSet])
insert Var
tv []     []         = ([Var
tv], [Type -> TyCoVarSet
tyCoVarsOfType (Var -> Type
tyVarKind Var
tv)])
    insert Var
tv (Var
a:[Var]
as) (TyCoVarSet
fvs:[TyCoVarSet]
fvss)
      | Var
tv Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
fvs
      , ([Var]
as', [TyCoVarSet]
fvss') <- Var -> [Var] -> [TyCoVarSet] -> ([Var], [TyCoVarSet])
insert Var
tv [Var]
as [TyCoVarSet]
fvss
      = (Var
aVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
as', TyCoVarSet
fvs TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` TyCoVarSet
fv_tv TyCoVarSet -> [TyCoVarSet] -> [TyCoVarSet]
forall a. a -> [a] -> [a]
: [TyCoVarSet]
fvss')

      | Bool
otherwise
      = (Var
tvVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:Var
aVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
as, TyCoVarSet
fvs TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` TyCoVarSet
fv_tv TyCoVarSet -> [TyCoVarSet] -> [TyCoVarSet]
forall a. a -> [a] -> [a]
: TyCoVarSet
fvs TyCoVarSet -> [TyCoVarSet] -> [TyCoVarSet]
forall a. a -> [a] -> [a]
: [TyCoVarSet]
fvss)
      where
        fv_tv :: TyCoVarSet
fv_tv = Type -> TyCoVarSet
tyCoVarsOfType (Var -> Type
tyVarKind Var
tv)

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

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

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