module GHC.Core.TyCo.FVs
  (     shallowTyCoVarsOfType, shallowTyCoVarsOfTypes,
        tyCoVarsOfType,        tyCoVarsOfTypes,
        tyCoVarsOfTypeDSet, tyCoVarsOfTypesDSet,

        tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs,
        tyCoFVsOfType, tyCoVarsOfTypeList,
        tyCoFVsOfTypes, tyCoVarsOfTypesList,
        deepTcvFolder,

        shallowTyCoVarsOfTyVarEnv, shallowTyCoVarsOfCoVarEnv,

        shallowTyCoVarsOfCo, shallowTyCoVarsOfCos,
        tyCoVarsOfCo, tyCoVarsOfCos, tyCoVarsOfMCo,
        coVarsOfType, coVarsOfTypes,
        coVarsOfCo, coVarsOfCos,
        tyCoVarsOfCoDSet,
        tyCoFVsOfCo, tyCoFVsOfCos,
        tyCoVarsOfCoList,

        almostDevoidCoVarOfCo,

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

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

        -- * Free type constructors
        tyConsOfType,

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

        -- * Occurrence-check expansion
        occCheckExpand,

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

        -- * Closing over kinds
        closeOverKindsDSet, closeOverKindsList,
        closeOverKinds,

        -- * Raw materials
        Endo(..), runTyCoVars
  ) where

import GHC.Prelude

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

import GHC.Builtin.Types.Prim( funTyFlagTyCon )

import Data.Monoid as DM ( Endo(..), Any(..) )
import GHC.Core.TyCo.Rep
import GHC.Core.TyCon
import GHC.Core.Coercion.Axiom( coAxiomTyCon )
import GHC.Utils.FV

import GHC.Types.Var
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.Panic
import GHC.Data.Pair

{-
%************************************************************************
%*                                                                      *
                 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 [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 through 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 performs 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.
-}

{- *********************************************************************
*                                                                      *
          Endo for free variables
*                                                                      *
********************************************************************* -}

{- Note [Accumulating parameter free variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We can use foldType to build an accumulating-parameter version of a
free-var finder, thus:

    fvs :: Type -> TyCoVarSet
    fvs ty = appEndo (foldType folder ty) emptyVarSet

Recall that
    foldType :: TyCoFolder env a -> env -> Type -> a

    newtype Endo a = Endo (a -> a)   -- In Data.Monoid
    instance Monoid a => Monoid (Endo a) where
       (Endo f) `mappend` (Endo g) = Endo (f.g)

    appEndo :: Endo a -> a -> a
    appEndo (Endo f) x = f x

So `mappend` for Endos is just function composition.

It's very important that, after optimisation, we end up with
* an arity-three function
* that is strict in the accumulator

   fvs env (TyVarTy v) acc
      | v `elemVarSet` env = acc
      | v `elemVarSet` acc = acc
      | otherwise          = acc `extendVarSet` v
   fvs env (AppTy t1 t2)   = fvs env t1 (fvs env t2 acc)
   ...

The "strict in the accumulator" part is to ensure that in the
AppTy equation we don't build a thunk for (fvs env t2 acc).

The optimiser does do all this, but not very robustly. It depends
critically on the basic arity-2 function not being exported, so that
all its calls are visibly to three arguments. This analysis is
done by the Call Arity pass.

TL;DR: check this regularly!
-}

runTyCoVars :: Endo TyCoVarSet -> TyCoVarSet
{-# INLINE runTyCoVars #-}
runTyCoVars :: Endo VarSet -> VarSet
runTyCoVars Endo VarSet
f = Endo VarSet -> VarSet -> VarSet
forall a. Endo a -> a -> a
appEndo Endo VarSet
f VarSet
emptyVarSet

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

tyCoVarsOfType :: Type -> TyCoVarSet
tyCoVarsOfType :: Type -> VarSet
tyCoVarsOfType Type
ty = Endo VarSet -> VarSet
runTyCoVars (Type -> Endo VarSet
deep_ty Type
ty)
-- Alternative:
--   tyCoVarsOfType ty = closeOverKinds (shallowTyCoVarsOfType ty)

tyCoVarsOfTypes :: [Type] -> TyCoVarSet
tyCoVarsOfTypes :: [Type] -> VarSet
tyCoVarsOfTypes [Type]
tys = Endo VarSet -> VarSet
runTyCoVars ([Type] -> Endo VarSet
deep_tys [Type]
tys)
-- Alternative:
--   tyCoVarsOfTypes tys = closeOverKinds (shallowTyCoVarsOfTypes tys)

tyCoVarsOfCo :: Coercion -> TyCoVarSet
-- See Note [Free variables of types]
tyCoVarsOfCo :: Coercion -> VarSet
tyCoVarsOfCo Coercion
co = Endo VarSet -> VarSet
runTyCoVars (Coercion -> Endo VarSet
deep_co 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 = Endo VarSet -> VarSet
runTyCoVars ([Coercion] -> Endo VarSet
deep_cos [Coercion]
cos)

deep_ty  :: Type       -> Endo TyCoVarSet
deep_tys :: [Type]     -> Endo TyCoVarSet
deep_co  :: Coercion   -> Endo TyCoVarSet
deep_cos :: [Coercion] -> Endo TyCoVarSet
(Type -> Endo VarSet
deep_ty, [Type] -> Endo VarSet
deep_tys, Coercion -> Endo VarSet
deep_co, [Coercion] -> Endo VarSet
deep_cos) = TyCoFolder VarSet (Endo VarSet)
-> VarSet
-> (Type -> Endo VarSet, [Type] -> Endo VarSet,
    Coercion -> Endo VarSet, [Coercion] -> Endo VarSet)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder VarSet (Endo VarSet)
deepTcvFolder VarSet
emptyVarSet

deepTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
deepTcvFolder :: TyCoFolder VarSet (Endo VarSet)
deepTcvFolder = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView
                           , tcf_tyvar :: VarSet -> TyCoVar -> Endo VarSet
tcf_tyvar = VarSet -> TyCoVar -> Endo VarSet
do_tcv, tcf_covar :: VarSet -> TyCoVar -> Endo VarSet
tcf_covar = VarSet -> TyCoVar -> Endo VarSet
do_tcv
                           , tcf_hole :: VarSet -> CoercionHole -> Endo VarSet
tcf_hole  = VarSet -> CoercionHole -> Endo VarSet
do_hole, tcf_tycobinder :: VarSet -> TyCoVar -> ForAllTyFlag -> VarSet
tcf_tycobinder = VarSet -> TyCoVar -> ForAllTyFlag -> VarSet
forall {p}. VarSet -> TyCoVar -> p -> VarSet
do_bndr }
  where
    do_tcv :: VarSet -> TyCoVar -> Endo VarSet
do_tcv VarSet
is TyCoVar
v = (VarSet -> VarSet) -> Endo VarSet
forall a. (a -> a) -> Endo a
Endo VarSet -> VarSet
do_it
      where
        do_it :: VarSet -> VarSet
do_it VarSet
acc | TyCoVar
v TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
is  = VarSet
acc
                  | TyCoVar
v TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
acc = VarSet
acc
                  | Bool
otherwise          = Endo VarSet -> VarSet -> VarSet
forall a. Endo a -> a -> a
appEndo (Type -> Endo VarSet
deep_ty (TyCoVar -> Type
varType TyCoVar
v)) (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$
                                         VarSet
acc VarSet -> TyCoVar -> VarSet
`extendVarSet` TyCoVar
v

    do_bndr :: VarSet -> TyCoVar -> p -> VarSet
do_bndr VarSet
is TyCoVar
tcv p
_ = VarSet -> TyCoVar -> VarSet
extendVarSet VarSet
is TyCoVar
tcv
    do_hole :: VarSet -> CoercionHole -> Endo VarSet
do_hole VarSet
is CoercionHole
hole  = VarSet -> TyCoVar -> Endo VarSet
do_tcv VarSet
is (CoercionHole -> TyCoVar
coHoleCoVar CoercionHole
hole)
                       -- See Note [CoercionHoles and coercion free variables]
                       -- in GHC.Core.TyCo.Rep

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


shallowTyCoVarsOfType :: Type -> TyCoVarSet
-- See Note [Free variables of types]
shallowTyCoVarsOfType :: Type -> VarSet
shallowTyCoVarsOfType Type
ty = Endo VarSet -> VarSet
runTyCoVars (Type -> Endo VarSet
shallow_ty Type
ty)

shallowTyCoVarsOfTypes :: [Type] -> TyCoVarSet
shallowTyCoVarsOfTypes :: [Type] -> VarSet
shallowTyCoVarsOfTypes [Type]
tys = Endo VarSet -> VarSet
runTyCoVars ([Type] -> Endo VarSet
shallow_tys [Type]
tys)

shallowTyCoVarsOfCo :: Coercion -> TyCoVarSet
shallowTyCoVarsOfCo :: Coercion -> VarSet
shallowTyCoVarsOfCo Coercion
co = Endo VarSet -> VarSet
runTyCoVars (Coercion -> Endo VarSet
shallow_co Coercion
co)

shallowTyCoVarsOfCos :: [Coercion] -> TyCoVarSet
shallowTyCoVarsOfCos :: [Coercion] -> VarSet
shallowTyCoVarsOfCos [Coercion]
cos = Endo VarSet -> VarSet
runTyCoVars ([Coercion] -> Endo VarSet
shallow_cos [Coercion]
cos)

-- | Returns free variables of types, including kind variables as
-- a non-deterministic set. For type synonyms it does /not/ expand the
-- synonym.
shallowTyCoVarsOfTyVarEnv :: TyVarEnv Type -> TyCoVarSet
-- See Note [Free variables of types]
shallowTyCoVarsOfTyVarEnv :: TyVarEnv Type -> VarSet
shallowTyCoVarsOfTyVarEnv TyVarEnv Type
tys = [Type] -> VarSet
shallowTyCoVarsOfTypes (TyVarEnv Type -> [Type]
forall key 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

shallowTyCoVarsOfCoVarEnv :: CoVarEnv Coercion -> TyCoVarSet
shallowTyCoVarsOfCoVarEnv :: CoVarEnv Coercion -> VarSet
shallowTyCoVarsOfCoVarEnv CoVarEnv Coercion
cos = [Coercion] -> VarSet
shallowTyCoVarsOfCos (CoVarEnv Coercion -> [Coercion]
forall key 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

shallow_ty  :: Type       -> Endo TyCoVarSet
shallow_tys :: [Type]     -> Endo TyCoVarSet
shallow_co  :: Coercion   -> Endo TyCoVarSet
shallow_cos :: [Coercion] -> Endo TyCoVarSet
(Type -> Endo VarSet
shallow_ty, [Type] -> Endo VarSet
shallow_tys, Coercion -> Endo VarSet
shallow_co, [Coercion] -> Endo VarSet
shallow_cos) = TyCoFolder VarSet (Endo VarSet)
-> VarSet
-> (Type -> Endo VarSet, [Type] -> Endo VarSet,
    Coercion -> Endo VarSet, [Coercion] -> Endo VarSet)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder VarSet (Endo VarSet)
shallowTcvFolder VarSet
emptyVarSet

shallowTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
shallowTcvFolder :: TyCoFolder VarSet (Endo VarSet)
shallowTcvFolder = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView
                              , tcf_tyvar :: VarSet -> TyCoVar -> Endo VarSet
tcf_tyvar = VarSet -> TyCoVar -> Endo VarSet
do_tcv, tcf_covar :: VarSet -> TyCoVar -> Endo VarSet
tcf_covar = VarSet -> TyCoVar -> Endo VarSet
do_tcv
                              , tcf_hole :: VarSet -> CoercionHole -> Endo VarSet
tcf_hole  = VarSet -> CoercionHole -> Endo VarSet
forall {a} {p} {p}. Monoid a => p -> p -> a
do_hole, tcf_tycobinder :: VarSet -> TyCoVar -> ForAllTyFlag -> VarSet
tcf_tycobinder = VarSet -> TyCoVar -> ForAllTyFlag -> VarSet
forall {p}. VarSet -> TyCoVar -> p -> VarSet
do_bndr }
  where
    do_tcv :: VarSet -> TyCoVar -> Endo VarSet
do_tcv VarSet
is TyCoVar
v = (VarSet -> VarSet) -> Endo VarSet
forall a. (a -> a) -> Endo a
Endo VarSet -> VarSet
do_it
      where
        do_it :: VarSet -> VarSet
do_it VarSet
acc | TyCoVar
v TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
is  = VarSet
acc
                  | TyCoVar
v TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
acc = VarSet
acc
                  | Bool
otherwise          = VarSet
acc VarSet -> TyCoVar -> VarSet
`extendVarSet` TyCoVar
v

    do_bndr :: VarSet -> TyCoVar -> p -> VarSet
do_bndr VarSet
is TyCoVar
tcv p
_ = VarSet -> TyCoVar -> VarSet
extendVarSet VarSet
is TyCoVar
tcv
    do_hole :: p -> p -> a
do_hole p
_ p
_  = a
forall a. Monoid a => a
mempty   -- Ignore coercion holes


{- *********************************************************************
*                                                                      *
          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.

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  = Endo VarSet -> VarSet
runTyCoVars (Type -> Endo VarSet
deep_cv_ty Type
ty)
coVarsOfTypes :: [Type] -> VarSet
coVarsOfTypes [Type]
tys = Endo VarSet -> VarSet
runTyCoVars ([Type] -> Endo VarSet
deep_cv_tys [Type]
tys)
coVarsOfCo :: Coercion -> VarSet
coVarsOfCo    Coercion
co  = Endo VarSet -> VarSet
runTyCoVars (Coercion -> Endo VarSet
deep_cv_co Coercion
co)
coVarsOfCos :: [Coercion] -> VarSet
coVarsOfCos   [Coercion]
cos = Endo VarSet -> VarSet
runTyCoVars ([Coercion] -> Endo VarSet
deep_cv_cos [Coercion]
cos)

deep_cv_ty  :: Type       -> Endo CoVarSet
deep_cv_tys :: [Type]     -> Endo CoVarSet
deep_cv_co  :: Coercion   -> Endo CoVarSet
deep_cv_cos :: [Coercion] -> Endo CoVarSet
(Type -> Endo VarSet
deep_cv_ty, [Type] -> Endo VarSet
deep_cv_tys, Coercion -> Endo VarSet
deep_cv_co, [Coercion] -> Endo VarSet
deep_cv_cos) = TyCoFolder VarSet (Endo VarSet)
-> VarSet
-> (Type -> Endo VarSet, [Type] -> Endo VarSet,
    Coercion -> Endo VarSet, [Coercion] -> Endo VarSet)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder VarSet (Endo VarSet)
deepCoVarFolder VarSet
emptyVarSet

deepCoVarFolder :: TyCoFolder TyCoVarSet (Endo CoVarSet)
deepCoVarFolder :: TyCoFolder VarSet (Endo VarSet)
deepCoVarFolder = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView
                             , tcf_tyvar :: VarSet -> TyCoVar -> Endo VarSet
tcf_tyvar = VarSet -> TyCoVar -> Endo VarSet
forall {a} {p} {p}. Monoid a => p -> p -> a
do_tyvar, tcf_covar :: VarSet -> TyCoVar -> Endo VarSet
tcf_covar = VarSet -> TyCoVar -> Endo VarSet
do_covar
                             , tcf_hole :: VarSet -> CoercionHole -> Endo VarSet
tcf_hole  = VarSet -> CoercionHole -> Endo VarSet
do_hole, tcf_tycobinder :: VarSet -> TyCoVar -> ForAllTyFlag -> VarSet
tcf_tycobinder = VarSet -> TyCoVar -> ForAllTyFlag -> VarSet
forall {p}. VarSet -> TyCoVar -> p -> VarSet
do_bndr }
  where
    do_tyvar :: p -> p -> a
do_tyvar p
_ 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 :: VarSet -> TyCoVar -> Endo VarSet
do_covar VarSet
is TyCoVar
v = (VarSet -> VarSet) -> Endo VarSet
forall a. (a -> a) -> Endo a
Endo VarSet -> VarSet
do_it
      where
        do_it :: VarSet -> VarSet
do_it VarSet
acc | TyCoVar
v TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
is  = VarSet
acc
                  | TyCoVar
v TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
acc = VarSet
acc
                  | Bool
otherwise          = Endo VarSet -> VarSet -> VarSet
forall a. Endo a -> a -> a
appEndo (Type -> Endo VarSet
deep_cv_ty (TyCoVar -> Type
varType TyCoVar
v)) (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$
                                         VarSet
acc VarSet -> TyCoVar -> VarSet
`extendVarSet` TyCoVar
v

    do_bndr :: VarSet -> TyCoVar -> p -> VarSet
do_bndr VarSet
is TyCoVar
tcv p
_ = VarSet -> TyCoVar -> VarSet
extendVarSet VarSet
is TyCoVar
tcv
    do_hole :: VarSet -> CoercionHole -> Endo VarSet
do_hole VarSet
is CoercionHole
hole  = VarSet -> TyCoVar -> Endo VarSet
do_covar VarSet
is (CoercionHole -> TyCoVar
coHoleCoVar CoercionHole
hole)
                       -- See Note [CoercionHoles and coercion free variables]
                       -- in GHC.Core.TyCo.Rep

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

------------- 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 = (TyCoVar -> VarSet -> VarSet) -> VarSet -> VarSet -> VarSet
forall a. (TyCoVar -> a -> a) -> a -> VarSet -> a
nonDetStrictFoldVarSet TyCoVar -> VarSet -> VarSet
do_one VarSet
vs VarSet
vs
  where
    do_one :: TyCoVar -> VarSet -> VarSet
do_one TyCoVar
v VarSet
acc = Endo VarSet -> VarSet -> VarSet
forall a. Endo a -> a -> a
appEndo (Type -> Endo VarSet
deep_ty (TyCoVar -> Type
varType TyCoVar
v)) VarSet
acc

{- --------------- Alternative version 1 (using FV) ------------
closeOverKinds = fvVarSet . closeOverKindsFV . nonDetEltsUniqSet
-}

{- ---------------- Alternative version 2 -------------

-- | Add the kind variables free in the kinds of the tyvars in the given set.
-- Returns a non-deterministic set.
closeOverKinds :: TyCoVarSet -> TyCoVarSet
closeOverKinds vs
   = go vs vs
  where
    go :: VarSet   -- Work list
       -> VarSet   -- Accumulator, always a superset of wl
       -> VarSet
    go wl acc
      | isEmptyVarSet wl = acc
      | otherwise        = go wl_kvs (acc `unionVarSet` wl_kvs)
      where
        k v inner_acc = ty_co_vars_of_type (varType v) acc inner_acc
        wl_kvs = nonDetFoldVarSet k emptyVarSet wl
        -- wl_kvs = union of shallow free vars of the kinds of wl
        --          but don't bother to collect vars in acc

-}

{- ---------------- Alternative version 3 -------------
-- | Add the kind variables free in the kinds of the tyvars in the given set.
-- Returns a non-deterministic set.
closeOverKinds :: TyVarSet -> TyVarSet
closeOverKinds vs = close_over_kinds vs emptyVarSet


close_over_kinds :: TyVarSet  -- Work list
                 -> TyVarSet  -- Accumulator
                 -> TyVarSet
-- Precondition: in any call (close_over_kinds wl acc)
--  for every tv in acc, the shallow kind-vars of tv
--  are either in the work list wl, or in acc
-- Postcondition: result is the deep free vars of (wl `union` acc)
close_over_kinds wl acc
  = nonDetFoldVarSet do_one acc wl
  where
    do_one :: Var -> TyVarSet -> TyVarSet
    -- (do_one v acc) adds v and its deep free-vars to acc
    do_one v acc | v `elemVarSet` acc
                 = acc
                 | otherwise
                 = close_over_kinds (shallowTyCoVarsOfType (varType v)) $
                   acc `extendVarSet` v
-}


{- *********************************************************************
*                                                                      *
          The FV versions return deterministic results
*                                                                      *
********************************************************************* -}

-- | Given a list of tyvars returns a deterministic FV computation that
-- returns the given tyvars with the kind variables free in the kinds of the
-- given tyvars.
closeOverKindsFV :: [TyVar] -> FV
closeOverKindsFV :: [TyCoVar] -> FV
closeOverKindsFV [TyCoVar]
tvs =
  (TyCoVar -> FV) -> [TyCoVar] -> FV
forall a. (a -> FV) -> [a] -> FV
mapUnionFV (Type -> FV
tyCoFVsOfType (Type -> FV) -> (TyCoVar -> Type) -> TyCoVar -> FV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCoVar -> Type
tyVarKind) [TyCoVar]
tvs FV -> FV -> FV
`unionFV` [TyCoVar] -> FV
mkFVs [TyCoVar]
tvs

-- | Add the kind variables free in the kinds of the tyvars in the given set.
-- Returns a deterministically ordered list.
closeOverKindsList :: [TyVar] -> [TyVar]
closeOverKindsList :: [TyCoVar] -> [TyCoVar]
closeOverKindsList [TyCoVar]
tvs = FV -> [TyCoVar]
fvVarList (FV -> [TyCoVar]) -> FV -> [TyCoVar]
forall a b. (a -> b) -> a -> b
$ [TyCoVar] -> FV
closeOverKindsFV [TyCoVar]
tvs

-- | Add the kind variables free in the kinds of the tyvars in the given set.
-- Returns a deterministic set.
closeOverKindsDSet :: DTyVarSet -> DTyVarSet
closeOverKindsDSet :: DTyVarSet -> DTyVarSet
closeOverKindsDSet = FV -> DTyVarSet
fvDVarSet (FV -> DTyVarSet) -> (DTyVarSet -> FV) -> DTyVarSet -> DTyVarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TyCoVar] -> FV
closeOverKindsFV ([TyCoVar] -> FV) -> (DTyVarSet -> [TyCoVar]) -> DTyVarSet -> FV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DTyVarSet -> [TyCoVar]
dVarSetElems

-- | `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 "GHC.Utils.FV".
tyCoVarsOfTypeDSet :: Type -> DTyCoVarSet
-- See Note [Free variables of types]
tyCoVarsOfTypeDSet :: Type -> DTyVarSet
tyCoVarsOfTypeDSet Type
ty = FV -> DTyVarSet
fvDVarSet (FV -> DTyVarSet) -> FV -> DTyVarSet
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 "GHC.Utils.FV".
tyCoVarsOfTypeList :: Type -> [TyCoVar]
-- See Note [Free variables of types]
tyCoVarsOfTypeList :: Type -> [TyCoVar]
tyCoVarsOfTypeList Type
ty = FV -> [TyCoVar]
fvVarList (FV -> [TyCoVar]) -> FV -> [TyCoVar]
forall a b. (a -> b) -> a -> b
$ Type -> FV
tyCoFVsOfType 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 [Free variables of types]
tyCoVarsOfTypesDSet :: [Type] -> DTyVarSet
tyCoVarsOfTypesDSet [Type]
tys = FV -> DTyVarSet
fvDVarSet (FV -> DTyVarSet) -> FV -> DTyVarSet
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] -> [TyCoVar]
tyCoVarsOfTypesList [Type]
tys = FV -> [TyCoVar]
fvVarList (FV -> [TyCoVar]) -> FV -> [TyCoVar]
forall a b. (a -> b) -> a -> b
$ [Type] -> FV
tyCoFVsOfTypes [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 "GHC.Utils.FV".
--
-- Eta-expanded because that makes it run faster (apparently)
-- See Note [FV eta expansion] in "GHC.Utils.FV" for explanation.
tyCoFVsOfType :: Type -> FV
-- See Note [Free variables of types]
tyCoFVsOfType :: Type -> FV
tyCoFVsOfType (TyVarTy TyCoVar
v)        InterestingVarFun
f VarSet
bound_vars ([TyCoVar]
acc_list, VarSet
acc_set)
  | Bool -> Bool
not (InterestingVarFun
f TyCoVar
v) = ([TyCoVar]
acc_list, VarSet
acc_set)
  | TyCoVar
v TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
bound_vars = ([TyCoVar]
acc_list, VarSet
acc_set)
  | TyCoVar
v TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
acc_set = ([TyCoVar]
acc_list, VarSet
acc_set)
  | Bool
otherwise = Type -> FV
tyCoFVsOfType (TyCoVar -> Type
tyVarKind TyCoVar
v) InterestingVarFun
f
                               VarSet
emptyVarSet   -- See Note [Closing over free variable kinds]
                               (TyCoVar
vTyCoVar -> [TyCoVar] -> [TyCoVar]
forall a. a -> [a] -> [a]
:[TyCoVar]
acc_list, VarSet -> TyCoVar -> VarSet
extendVarSet VarSet
acc_set TyCoVar
v)
tyCoFVsOfType (TyConApp TyCon
_ [Type]
tys)   InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc = [Type] -> FV
tyCoFVsOfTypes [Type]
tys InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc
tyCoFVsOfType (LitTy {})         InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc = FV
emptyFV InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc
tyCoFVsOfType (AppTy Type
fun Type
arg)    InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc = (Type -> FV
tyCoFVsOfType Type
fun FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
arg) InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc
tyCoFVsOfType (FunTy FunTyFlag
_ Type
w Type
arg Type
res)  InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc = (Type -> FV
tyCoFVsOfType Type
w FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
arg FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
res) InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc
tyCoFVsOfType (ForAllTy ForAllTyBinder
bndr Type
ty) InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc = ForAllTyBinder -> FV -> FV
tyCoFVsBndr ForAllTyBinder
bndr (Type -> FV
tyCoFVsOfType Type
ty)  InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc
tyCoFVsOfType (CastTy Type
ty Coercion
co)     InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc = (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
co) InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc
tyCoFVsOfType (CoercionTy Coercion
co)    InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc

tyCoFVsBndr :: ForAllTyBinder -> FV -> FV
-- Free vars of (forall b. <thing with fvs>)
tyCoFVsBndr :: ForAllTyBinder -> FV -> FV
tyCoFVsBndr (Bndr TyCoVar
tv ForAllTyFlag
_) FV
fvs = TyCoVar -> FV -> FV
tyCoFVsVarBndr TyCoVar
tv FV
fvs

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

tyCoFVsVarBndr :: Var -> FV -> FV
tyCoFVsVarBndr :: TyCoVar -> FV -> FV
tyCoFVsVarBndr TyCoVar
var FV
fvs
  = Type -> FV
tyCoFVsOfType (TyCoVar -> Type
varType TyCoVar
var)   -- Free vars of its type/kind
    FV -> FV -> FV
`unionFV` TyCoVar -> FV -> FV
delFV TyCoVar
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 VarSet
in_scope ([TyCoVar], VarSet)
acc = (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` [Type] -> FV
tyCoFVsOfTypes [Type]
tys) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfTypes []       InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc

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

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

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

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

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

tyCoFVsOfProv :: UnivCoProvenance -> FV
tyCoFVsOfProv :: UnivCoProvenance -> FV
tyCoFVsOfProv (PhantomProv Coercion
co)    InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfProv (ProofIrrelProv Coercion
co) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfProv (PluginProv String
_)      InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfProv (CorePrepProv Bool
_)    InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc

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


----- 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 "GHC.Core.Coercion"
almostDevoidCoVarOfCo :: CoVar -> Coercion -> Bool
almostDevoidCoVarOfCo :: TyCoVar -> Coercion -> Bool
almostDevoidCoVarOfCo TyCoVar
cv Coercion
co =
  Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv

almost_devoid_co_var_of_co :: Coercion -> CoVar -> Bool
almost_devoid_co_var_of_co :: Coercion -> InterestingVarFun
almost_devoid_co_var_of_co (Refl {}) TyCoVar
_ = Bool
True   -- covar is allowed in Refl and
almost_devoid_co_var_of_co (GRefl {}) TyCoVar
_ = Bool
True  -- GRefl, so we don't look into
                                                -- the coercions
almost_devoid_co_var_of_co (TyConAppCo Role
_ TyCon
_ [Coercion]
cos) TyCoVar
cv
  = [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [Coercion]
cos TyCoVar
cv
almost_devoid_co_var_of_co (AppCo Coercion
co Coercion
arg) TyCoVar
cv
  = Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
  Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
arg TyCoVar
cv
almost_devoid_co_var_of_co (ForAllCo TyCoVar
v Coercion
kind_co Coercion
co) TyCoVar
cv
  = Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
kind_co TyCoVar
cv
  Bool -> Bool -> Bool
&& (TyCoVar
v TyCoVar -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
== TyCoVar
cv Bool -> Bool -> Bool
|| Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
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 }) TyCoVar
cv
  =  Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
w   TyCoVar
cv
  Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co1 TyCoVar
cv
  Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co2 TyCoVar
cv
almost_devoid_co_var_of_co (CoVarCo TyCoVar
v) TyCoVar
cv = TyCoVar
v TyCoVar -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
/= TyCoVar
cv
almost_devoid_co_var_of_co (HoleCo CoercionHole
h)  TyCoVar
cv = (CoercionHole -> TyCoVar
coHoleCoVar CoercionHole
h) TyCoVar -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
/= TyCoVar
cv
almost_devoid_co_var_of_co (AxiomInstCo CoAxiom Branched
_ BranchIndex
_ [Coercion]
cos) TyCoVar
cv
  = [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [Coercion]
cos TyCoVar
cv
almost_devoid_co_var_of_co (UnivCo UnivCoProvenance
p Role
_ Type
t1 Type
t2) TyCoVar
cv
  = UnivCoProvenance -> InterestingVarFun
almost_devoid_co_var_of_prov UnivCoProvenance
p TyCoVar
cv
  Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
t1 TyCoVar
cv
  Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
t2 TyCoVar
cv
almost_devoid_co_var_of_co (SymCo Coercion
co) TyCoVar
cv
  = Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
almost_devoid_co_var_of_co (TransCo Coercion
co1 Coercion
co2) TyCoVar
cv
  = Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co1 TyCoVar
cv
  Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co2 TyCoVar
cv
almost_devoid_co_var_of_co (SelCo CoSel
_ Coercion
co) TyCoVar
cv
  = Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
almost_devoid_co_var_of_co (LRCo LeftOrRight
_ Coercion
co) TyCoVar
cv
  = Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
almost_devoid_co_var_of_co (InstCo Coercion
co Coercion
arg) TyCoVar
cv
  = Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
  Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
arg TyCoVar
cv
almost_devoid_co_var_of_co (KindCo Coercion
co) TyCoVar
cv
  = Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
almost_devoid_co_var_of_co (SubCo Coercion
co) TyCoVar
cv
  = Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
almost_devoid_co_var_of_co (AxiomRuleCo CoAxiomRule
_ [Coercion]
cs) TyCoVar
cv
  = [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [Coercion]
cs TyCoVar
cv

almost_devoid_co_var_of_cos :: [Coercion] -> CoVar -> Bool
almost_devoid_co_var_of_cos :: [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [] TyCoVar
_ = Bool
True
almost_devoid_co_var_of_cos (Coercion
co:[Coercion]
cos) TyCoVar
cv
  = Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
  Bool -> Bool -> Bool
&& [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [Coercion]
cos TyCoVar
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 Coercion
co) TyCoVar
cv
  = Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
almost_devoid_co_var_of_prov (ProofIrrelProv Coercion
co) TyCoVar
cv
  = Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
almost_devoid_co_var_of_prov (PluginProv String
_)   TyCoVar
_ = Bool
True
almost_devoid_co_var_of_prov (CorePrepProv Bool
_) TyCoVar
_ = 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 TyCoVar
_) TyCoVar
_ = Bool
True
almost_devoid_co_var_of_type (TyConApp TyCon
_ [Type]
tys) TyCoVar
cv
  = [Type] -> InterestingVarFun
almost_devoid_co_var_of_types [Type]
tys TyCoVar
cv
almost_devoid_co_var_of_type (LitTy {}) TyCoVar
_ = Bool
True
almost_devoid_co_var_of_type (AppTy Type
fun Type
arg) TyCoVar
cv
  = Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
fun TyCoVar
cv
  Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
arg TyCoVar
cv
almost_devoid_co_var_of_type (FunTy FunTyFlag
_ Type
w Type
arg Type
res) TyCoVar
cv
  = Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
w TyCoVar
cv
  Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
arg TyCoVar
cv
  Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
res TyCoVar
cv
almost_devoid_co_var_of_type (ForAllTy (Bndr TyCoVar
v ForAllTyFlag
_) Type
ty) TyCoVar
cv
  = Type -> InterestingVarFun
almost_devoid_co_var_of_type (TyCoVar -> Type
varType TyCoVar
v) TyCoVar
cv
  Bool -> Bool -> Bool
&& (TyCoVar
v TyCoVar -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
== TyCoVar
cv Bool -> Bool -> Bool
|| Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
ty TyCoVar
cv)
almost_devoid_co_var_of_type (CastTy Type
ty Coercion
co) TyCoVar
cv
  = Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
ty TyCoVar
cv
  Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
almost_devoid_co_var_of_type (CoercionTy Coercion
co) TyCoVar
cv
  = Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv

almost_devoid_co_var_of_types :: [Type] -> CoVar -> Bool
almost_devoid_co_var_of_types :: [Type] -> InterestingVarFun
almost_devoid_co_var_of_types [] TyCoVar
_ = Bool
True
almost_devoid_co_var_of_types (Type
ty:[Type]
tys) TyCoVar
cv
  = Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
ty TyCoVar
cv
  Bool -> Bool -> Bool
&& [Type] -> InterestingVarFun
almost_devoid_co_var_of_types [Type]
tys TyCoVar
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 TyCoVar
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
$ TyCoVar -> Type
tyVarKind TyCoVar
tv) (TyCoVar -> VarSet
unitVarSet TyCoVar
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 TyCoVar
tv ForAllTyFlag
_) Type
ty)
      = ((VarSet -> TyCoVar -> VarSet
`delVarSet` TyCoVar
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
$ TyCoVar -> Type
varType TyCoVar
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
*                                                                      *
********************************************************************* -}

-- | 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 -> 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 TyCoVar
v)         = TyCoVar -> FV
unitFV TyCoVar
v FV -> FV -> FV
`unionFV` Type -> FV
go (TyCoVar -> Type
tyVarKind TyCoVar
v)
    go (AppTy Type
f Type
a)         = Type -> FV
go Type
f FV -> FV -> FV
`unionFV` Type -> FV
go Type
a
    go (FunTy FunTyFlag
_ Type
w Type
ty1 Type
ty2) = Type -> FV
go Type
w FV -> FV -> FV
`unionFV` 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 TyCoVar
tv ForAllTyFlag
_) Type
ty) = Type -> FV
go (TyCoVar -> Type
tyVarKind TyCoVar
tv) FV -> FV -> FV
`unionFV` TyCoVar -> FV -> FV
delFV TyCoVar
tv (Type -> FV
go Type
ty)
    go LitTy{}                   = FV
emptyFV
    go (CastTy Type
ty Coercion
_)             = 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 "GHC.Tc.Instance.Family".
                     -> [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, ForAllTyBinders, TyConBinders, and visibility] in "GHC.Core.TyCo.Rep"
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 TyCoVar
v)        = Type -> FV
go (TyCoVar -> Type
tyVarKind TyCoVar
v)
    go (AppTy Type
f Type
a)        = Type -> FV
go Type
f FV -> FV -> FV
`unionFV` Type -> FV
go Type
a
    go (FunTy FunTyFlag
_ Type
w Type
ty1 Type
ty2) = Type -> FV
go Type
w FV -> FV -> FV
`unionFV` 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 ForAllTyBinder
tvb Type
ty)  = ForAllTyBinder -> FV -> FV
tyCoFVsBndr ForAllTyBinder
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 Coercion
co)     = Coercion -> FV
tyCoFVsOfCo Coercion
co FV -> FV -> FV
`unionFV` Type -> FV
go Type
ty
    go (CoercionTy Coercion
co)    = Coercion -> FV
tyCoFVsOfCo Coercion
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


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

{-# INLINE afvFolder #-}   -- so that specialization to (const True) works
afvFolder :: (TyCoVar -> Bool) -> TyCoFolder TyCoVarSet DM.Any
afvFolder :: InterestingVarFun -> TyCoFolder VarSet Any
afvFolder InterestingVarFun
check_fv = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView
                                , tcf_tyvar :: VarSet -> TyCoVar -> Any
tcf_tyvar = VarSet -> TyCoVar -> Any
do_tcv, tcf_covar :: VarSet -> TyCoVar -> Any
tcf_covar = VarSet -> TyCoVar -> Any
do_tcv
                                , tcf_hole :: VarSet -> CoercionHole -> Any
tcf_hole = VarSet -> CoercionHole -> Any
forall {p} {p}. p -> p -> Any
do_hole, tcf_tycobinder :: VarSet -> TyCoVar -> ForAllTyFlag -> VarSet
tcf_tycobinder = VarSet -> TyCoVar -> ForAllTyFlag -> VarSet
forall {p}. VarSet -> TyCoVar -> p -> VarSet
do_bndr }
  where
    do_tcv :: VarSet -> TyCoVar -> Any
do_tcv VarSet
is TyCoVar
tv = Bool -> Any
Any (Bool -> Bool
not (TyCoVar
tv TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
is) Bool -> Bool -> Bool
&& InterestingVarFun
check_fv TyCoVar
tv)
    do_hole :: p -> p -> Any
do_hole p
_ p
_  = Bool -> Any
Any Bool
False    -- I'm unsure; probably never happens
    do_bndr :: VarSet -> TyCoVar -> p -> VarSet
do_bndr VarSet
is TyCoVar
tv p
_ = VarSet
is VarSet -> TyCoVar -> VarSet
`extendVarSet` TyCoVar
tv

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

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

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

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 (Type -> Any
f Type
ty)
  where (Type -> Any
f, [Type] -> Any
_, Coercion -> Any
_, [Coercion] -> Any
_) = TyCoFolder VarSet Any
-> VarSet
-> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
afvFolder (Bool -> InterestingVarFun
forall a b. a -> b -> a
const Bool
True)) VarSet
emptyVarSet

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 ([Type] -> Any
f [Type]
tys)
  where (Type -> Any
_, [Type] -> Any
f, Coercion -> Any
_, [Coercion] -> Any
_) = TyCoFolder VarSet Any
-> VarSet
-> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
afvFolder (Bool -> InterestingVarFun
forall a b. a -> b -> a
const Bool
True)) VarSet
emptyVarSet

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 (Coercion -> Any
f Coercion
co)
  where (Type -> Any
_, [Type] -> Any
_, Coercion -> Any
f, [Coercion] -> Any
_) = TyCoFolder VarSet Any
-> VarSet
-> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
afvFolder (Bool -> InterestingVarFun
forall a b. a -> b -> a
const Bool
True)) VarSet
emptyVarSet


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

{- 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 "GHC.Rename.HsType"

scopedSort :: [TyCoVar] -> [TyCoVar]
scopedSort :: [TyCoVar] -> [TyCoVar]
scopedSort = [TyCoVar] -> [VarSet] -> [TyCoVar] -> [TyCoVar]
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 :: [TyCoVar] -> [VarSet] -> [TyCoVar] -> [TyCoVar]
go [TyCoVar]
acc [VarSet]
_fv_list [] = [TyCoVar] -> [TyCoVar]
forall a. [a] -> [a]
reverse [TyCoVar]
acc
    go [TyCoVar]
acc  [VarSet]
fv_list (TyCoVar
tv:[TyCoVar]
tvs)
      = [TyCoVar] -> [VarSet] -> [TyCoVar] -> [TyCoVar]
go [TyCoVar]
acc' [VarSet]
fv_list' [TyCoVar]
tvs
      where
        ([TyCoVar]
acc', [VarSet]
fv_list') = TyCoVar -> [TyCoVar] -> [VarSet] -> ([TyCoVar], [VarSet])
insert TyCoVar
tv [TyCoVar]
acc [VarSet]
fv_list

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

      | Bool
otherwise
      = (TyCoVar
tvTyCoVar -> [TyCoVar] -> [TyCoVar]
forall a. a -> [a] -> [a]
:TyCoVar
aTyCoVar -> [TyCoVar] -> [TyCoVar]
forall a. a -> [a] -> [a]
:[TyCoVar]
as, VarSet
fvs VarSet -> VarSet -> VarSet
`unionVarSet` VarSet
fv_tv VarSet -> [VarSet] -> [VarSet]
forall a. a -> [a] -> [a]
: VarSet
fvs VarSet -> [VarSet] -> [VarSet]
forall a. a -> [a] -> [a]
: [VarSet]
fvss)
      where
        fv_tv :: VarSet
fv_tv = Type -> VarSet
tyCoVarsOfType (TyCoVar -> Type
tyVarKind TyCoVar
tv)

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

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

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

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

-- | 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
forall {t :: * -> *}. Foldable t => t Type -> UniqSet TyCon
go_s [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 TyCoVar
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 (TyCoVar -> Type
varType TyCoVar
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 TyCoVar
_ Coercion
kind_co Coercion
co) = Coercion -> UniqSet TyCon
go_co Coercion
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 (AxiomInstCo CoAxiom Branched
ax BranchIndex
_ [Coercion]
args) = CoAxiom Branched -> UniqSet TyCon
forall {br :: BranchFlag}. CoAxiom br -> UniqSet TyCon
go_ax CoAxiom Branched
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 UnivCoProvenance
p Role
_ Type
t1 Type
t2)      = UnivCoProvenance -> UniqSet TyCon
go_prov UnivCoProvenance
p UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` 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
     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_co (AxiomRuleCo CoAxiomRule
_ [Coercion]
cs)      = [Coercion] -> UniqSet TyCon
go_cos [Coercion]
cs

     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_prov :: UnivCoProvenance -> UniqSet TyCon
go_prov (PhantomProv Coercion
co)    = Coercion -> UniqSet TyCon
go_co Coercion
co
     go_prov (ProofIrrelProv Coercion
co) = Coercion -> UniqSet TyCon
go_co Coercion
co
     go_prov (PluginProv String
_)      = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
     go_prov (CorePrepProv Bool
_)    = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
        -- this last case can happen from the tyConsOfType used from
        -- checkTauTvUpdate

     go_s :: t Type -> UniqSet TyCon
go_s t Type
tys     = (Type -> UniqSet TyCon -> UniqSet TyCon)
-> UniqSet TyCon -> t Type -> UniqSet TyCon
forall a b. (a -> b -> b) -> b -> t 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
go)     UniqSet TyCon
forall a. UniqSet a
emptyUniqSet t Type
tys
     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 :: CoAxiom br -> UniqSet TyCon
go_ax CoAxiom br
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 br -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom br
ax


{- **********************************************************************
*                                                                       *
           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 :: [TyCoVar] -> Type -> Maybe Type
occCheckExpand [TyCoVar]
vs_to_avoid Type
ty
  | [TyCoVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyCoVar]
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 TyCoVar) -> Type -> Maybe Type
go ([TyCoVar] -> VarSet
mkVarSet [TyCoVar]
vs_to_avoid, VarEnv TyCoVar
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 TyCoVar) -> Type -> Maybe Type
go (VarSet
as, VarEnv TyCoVar
env) ty :: Type
ty@(TyVarTy TyCoVar
tv)
      | Just TyCoVar
tv' <- VarEnv TyCoVar -> TyCoVar -> Maybe TyCoVar
forall a. VarEnv a -> TyCoVar -> Maybe a
lookupVarEnv VarEnv TyCoVar
env TyCoVar
tv = Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCoVar -> Type
mkTyVarTy TyCoVar
tv')
      | VarSet -> InterestingVarFun
bad_var_occ VarSet
as TyCoVar
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 TyCoVar)
_   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 TyCoVar)
cxt (AppTy Type
ty1 Type
ty2) = do { Type
ty1' <- (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
go (VarSet, VarEnv TyCoVar)
cxt Type
ty1
                                ; Type
ty2' <- (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
go (VarSet, VarEnv TyCoVar)
cxt Type
ty2
                                ; Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
AppTy Type
ty1' Type
ty2') }
    go (VarSet, VarEnv TyCoVar)
cxt ty :: Type
ty@(FunTy FunTyFlag
_ Type
w Type
ty1 Type
ty2)
       = do { Type
w'   <- (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
go (VarSet, VarEnv TyCoVar)
cxt Type
w
            ; Type
ty1' <- (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
go (VarSet, VarEnv TyCoVar)
cxt Type
ty1
            ; Type
ty2' <- (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
go (VarSet, VarEnv TyCoVar)
cxt Type
ty2
            ; Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty { ft_mult = w', ft_arg = ty1', ft_res = ty2' }) }
    go cxt :: (VarSet, VarEnv TyCoVar)
cxt@(VarSet
as, VarEnv TyCoVar
env) (ForAllTy (Bndr TyCoVar
tv ForAllTyFlag
vis) Type
body_ty)
       = do { Type
ki' <- (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
go (VarSet, VarEnv TyCoVar)
cxt (TyCoVar -> Type
varType TyCoVar
tv)
            ; let tv' :: TyCoVar
tv'  = TyCoVar -> Type -> TyCoVar
setVarType TyCoVar
tv Type
ki'
                  env' :: VarEnv TyCoVar
env' = VarEnv TyCoVar -> TyCoVar -> TyCoVar -> VarEnv TyCoVar
forall a. VarEnv a -> TyCoVar -> a -> VarEnv a
extendVarEnv VarEnv TyCoVar
env TyCoVar
tv TyCoVar
tv'
                  as' :: VarSet
as'  = VarSet
as VarSet -> TyCoVar -> VarSet
`delVarSet` TyCoVar
tv
            ; Type
body' <- (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
go (VarSet
as', VarEnv TyCoVar
env') Type
body_ty
            ; Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (ForAllTyBinder -> Type -> Type
ForAllTy (TyCoVar -> ForAllTyFlag -> ForAllTyBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr TyCoVar
tv' ForAllTyFlag
vis) Type
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 TyCoVar)
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 TyCoVar) -> Type -> Maybe Type
go (VarSet, VarEnv TyCoVar)
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 TyCoVar) -> Type -> Maybe Type
go (VarSet, VarEnv TyCoVar)
cxt Type
ty'
                  | Bool
otherwise               -> Maybe Type
forall a. Maybe a
Nothing
                      -- Failing that, try to expand a synonym

    go (VarSet, VarEnv TyCoVar)
cxt (CastTy Type
ty Coercion
co) =  do { Type
ty' <- (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
go (VarSet, VarEnv TyCoVar)
cxt Type
ty
                                ; Coercion
co' <- (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt Coercion
co
                                ; Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Coercion -> Type
CastTy Type
ty' Coercion
co') }
    go (VarSet, VarEnv TyCoVar)
cxt (CoercionTy Coercion
co) = do { Coercion
co' <- (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt Coercion
co
                                ; Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> Type
CoercionTy Coercion
co') }

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

    ------------------
    go_mco :: (VarSet, VarEnv TyCoVar) -> MCoercion -> Maybe MCoercion
go_mco (VarSet, VarEnv TyCoVar)
_   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 TyCoVar)
ctx (MCo Coercion
co) = Coercion -> MCoercion
MCo (Coercion -> MCoercion) -> Maybe Coercion -> Maybe MCoercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
ctx Coercion
co

    ------------------
    go_co :: (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt (Refl Type
ty)                 = do { Type
ty' <- (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
go (VarSet, VarEnv TyCoVar)
cxt Type
ty
                                             ; Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Coercion
Refl Type
ty') }
    go_co (VarSet, VarEnv TyCoVar)
cxt (GRefl Role
r Type
ty MCoercion
mco)          = do { MCoercion
mco' <- (VarSet, VarEnv TyCoVar) -> MCoercion -> Maybe MCoercion
go_mco (VarSet, VarEnv TyCoVar)
cxt MCoercion
mco
                                             ; Type
ty' <- (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
go (VarSet, VarEnv TyCoVar)
cxt Type
ty
                                             ; Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> Type -> MCoercion -> Coercion
GRefl Role
r Type
ty' MCoercion
mco') }
      -- Note: Coercions do not contain type synonyms
    go_co (VarSet, VarEnv TyCoVar)
cxt (TyConAppCo Role
r TyCon
tc [Coercion]
args)    = do { [Coercion]
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 TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt) [Coercion]
args
                                             ; Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> TyCon -> [Coercion] -> Coercion
TyConAppCo Role
r TyCon
tc [Coercion]
args') }
    go_co (VarSet, VarEnv TyCoVar)
cxt (AppCo Coercion
co Coercion
arg)            = do { Coercion
co' <- (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt Coercion
co
                                             ; Coercion
arg' <- (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt Coercion
arg
                                             ; Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> Coercion -> Coercion
AppCo Coercion
co' Coercion
arg') }
    go_co cxt :: (VarSet, VarEnv TyCoVar)
cxt@(VarSet
as, VarEnv TyCoVar
env) (ForAllCo TyCoVar
tv Coercion
kind_co Coercion
body_co)
      = do { Coercion
kind_co' <- (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt Coercion
kind_co
           ; let tv' :: TyCoVar
tv' = TyCoVar -> Type -> TyCoVar
setVarType TyCoVar
tv (Type -> TyCoVar) -> Type -> TyCoVar
forall a b. (a -> b) -> a -> b
$
                       Coercion -> Type
coercionLKind Coercion
kind_co'
                 env' :: VarEnv TyCoVar
env' = VarEnv TyCoVar -> TyCoVar -> TyCoVar -> VarEnv TyCoVar
forall a. VarEnv a -> TyCoVar -> a -> VarEnv a
extendVarEnv VarEnv TyCoVar
env TyCoVar
tv TyCoVar
tv'
                 as' :: VarSet
as'  = VarSet
as VarSet -> TyCoVar -> VarSet
`delVarSet` TyCoVar
tv
           ; Coercion
body' <- (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet
as', VarEnv TyCoVar
env') Coercion
body_co
           ; Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCoVar -> Coercion -> Coercion -> Coercion
ForAllCo TyCoVar
tv' Coercion
kind_co' Coercion
body') }
    go_co (VarSet, VarEnv TyCoVar)
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 { Coercion
co1' <- (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt Coercion
co1
           ; Coercion
co2' <- (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt Coercion
co2
           ; Coercion
w' <- (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt Coercion
w
           ; Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion
co { fco_mult = w', fco_arg = co1', fco_res = co2' })}

    go_co (VarSet
as,VarEnv TyCoVar
env) co :: Coercion
co@(CoVarCo TyCoVar
c)
      | Just TyCoVar
c' <- VarEnv TyCoVar -> TyCoVar -> Maybe TyCoVar
forall a. VarEnv a -> TyCoVar -> Maybe a
lookupVarEnv VarEnv TyCoVar
env TyCoVar
c   = Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCoVar -> Coercion
CoVarCo TyCoVar
c')
      | VarSet -> InterestingVarFun
bad_var_occ VarSet
as TyCoVar
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 TyCoVar
_) co :: Coercion
co@(HoleCo CoercionHole
h)
      | VarSet -> InterestingVarFun
bad_var_occ VarSet
as (CoercionHole -> TyCoVar
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 TyCoVar)
cxt (AxiomInstCo CoAxiom Branched
ax BranchIndex
ind [Coercion]
args) = do { [Coercion]
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 TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt) [Coercion]
args
                                             ; Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
AxiomInstCo CoAxiom Branched
ax BranchIndex
ind [Coercion]
args') }
    go_co (VarSet, VarEnv TyCoVar)
cxt (UnivCo UnivCoProvenance
p Role
r Type
ty1 Type
ty2)      = do { UnivCoProvenance
p' <- (VarSet, VarEnv TyCoVar)
-> UnivCoProvenance -> Maybe UnivCoProvenance
go_prov (VarSet, VarEnv TyCoVar)
cxt UnivCoProvenance
p
                                             ; Type
ty1' <- (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
go (VarSet, VarEnv TyCoVar)
cxt Type
ty1
                                             ; Type
ty2' <- (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
go (VarSet, VarEnv TyCoVar)
cxt Type
ty2
                                             ; Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (UnivCoProvenance -> Role -> Type -> Type -> Coercion
UnivCo UnivCoProvenance
p' Role
r Type
ty1' Type
ty2') }
    go_co (VarSet, VarEnv TyCoVar)
cxt (SymCo Coercion
co)                = do { Coercion
co' <- (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt Coercion
co
                                             ; Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> Coercion
SymCo Coercion
co') }
    go_co (VarSet, VarEnv TyCoVar)
cxt (TransCo Coercion
co1 Coercion
co2)         = do { Coercion
co1' <- (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt Coercion
co1
                                             ; Coercion
co2' <- (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt Coercion
co2
                                             ; Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> Coercion -> Coercion
TransCo Coercion
co1' Coercion
co2') }
    go_co (VarSet, VarEnv TyCoVar)
cxt (SelCo CoSel
n Coercion
co)              = do { Coercion
co' <- (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt Coercion
co
                                             ; Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (CoSel -> Coercion -> Coercion
SelCo CoSel
n Coercion
co') }
    go_co (VarSet, VarEnv TyCoVar)
cxt (LRCo LeftOrRight
lr Coercion
co)              = do { Coercion
co' <- (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt Coercion
co
                                             ; Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (LeftOrRight -> Coercion -> Coercion
LRCo LeftOrRight
lr Coercion
co') }
    go_co (VarSet, VarEnv TyCoVar)
cxt (InstCo Coercion
co Coercion
arg)           = do { Coercion
co' <- (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt Coercion
co
                                             ; Coercion
arg' <- (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt Coercion
arg
                                             ; Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> Coercion -> Coercion
InstCo Coercion
co' Coercion
arg') }
    go_co (VarSet, VarEnv TyCoVar)
cxt (KindCo Coercion
co)               = do { Coercion
co' <- (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt Coercion
co
                                             ; Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> Coercion
KindCo Coercion
co') }
    go_co (VarSet, VarEnv TyCoVar)
cxt (SubCo Coercion
co)                = do { Coercion
co' <- (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt Coercion
co
                                             ; Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> Coercion
SubCo Coercion
co') }
    go_co (VarSet, VarEnv TyCoVar)
cxt (AxiomRuleCo CoAxiomRule
ax [Coercion]
cs)       = do { [Coercion]
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 TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt) [Coercion]
cs
                                             ; Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (CoAxiomRule -> [Coercion] -> Coercion
AxiomRuleCo CoAxiomRule
ax [Coercion]
cs') }

    ------------------
    go_prov :: (VarSet, VarEnv TyCoVar)
-> UnivCoProvenance -> Maybe UnivCoProvenance
go_prov (VarSet, VarEnv TyCoVar)
cxt (PhantomProv Coercion
co)    = Coercion -> UnivCoProvenance
PhantomProv (Coercion -> UnivCoProvenance)
-> Maybe Coercion -> Maybe UnivCoProvenance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt Coercion
co
    go_prov (VarSet, VarEnv TyCoVar)
cxt (ProofIrrelProv Coercion
co) = Coercion -> UnivCoProvenance
ProofIrrelProv (Coercion -> UnivCoProvenance)
-> Maybe Coercion -> Maybe UnivCoProvenance
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (VarSet, VarEnv TyCoVar) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv TyCoVar)
cxt Coercion
co
    go_prov (VarSet, VarEnv TyCoVar)
_   p :: UnivCoProvenance
p@(PluginProv String
_)    = UnivCoProvenance -> Maybe UnivCoProvenance
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return UnivCoProvenance
p
    go_prov (VarSet, VarEnv TyCoVar)
_   p :: UnivCoProvenance
p@(CorePrepProv Bool
_)  = UnivCoProvenance -> Maybe UnivCoProvenance
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return UnivCoProvenance
p