never executed always true always false
    1 
    2 
    3 module GHC.Core.TyCo.FVs
    4   (     shallowTyCoVarsOfType, shallowTyCoVarsOfTypes,
    5         tyCoVarsOfType,        tyCoVarsOfTypes,
    6         tyCoVarsOfTypeDSet, tyCoVarsOfTypesDSet,
    7 
    8         tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs,
    9         tyCoFVsOfType, tyCoVarsOfTypeList,
   10         tyCoFVsOfTypes, tyCoVarsOfTypesList,
   11         deepTcvFolder,
   12 
   13         shallowTyCoVarsOfTyVarEnv, shallowTyCoVarsOfCoVarEnv,
   14 
   15         shallowTyCoVarsOfCo, shallowTyCoVarsOfCos,
   16         tyCoVarsOfCo, tyCoVarsOfCos, tyCoVarsOfMCo,
   17         coVarsOfType, coVarsOfTypes,
   18         coVarsOfCo, coVarsOfCos,
   19         tyCoVarsOfCoDSet,
   20         tyCoFVsOfCo, tyCoFVsOfCos,
   21         tyCoVarsOfCoList,
   22 
   23         almostDevoidCoVarOfCo,
   24 
   25         -- Injective free vars
   26         injectiveVarsOfType, injectiveVarsOfTypes,
   27         invisibleVarsOfType, invisibleVarsOfTypes,
   28 
   29         -- Any and No Free vars
   30         anyFreeVarsOfType, anyFreeVarsOfTypes, anyFreeVarsOfCo,
   31         noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,
   32 
   33         -- * Well-scoped free variables
   34         scopedSort, tyCoVarsOfTypeWellScoped,
   35         tyCoVarsOfTypesWellScoped,
   36 
   37         -- * Closing over kinds
   38         closeOverKindsDSet, closeOverKindsList,
   39         closeOverKinds,
   40 
   41         -- * Raw materials
   42         Endo(..), runTyCoVars
   43   ) where
   44 
   45 import GHC.Prelude
   46 
   47 import {-# SOURCE #-} GHC.Core.Type (coreView, partitionInvisibleTypes)
   48 
   49 import Data.Monoid as DM ( Endo(..), Any(..) )
   50 import GHC.Core.TyCo.Rep
   51 import GHC.Core.TyCon
   52 import GHC.Types.Var
   53 import GHC.Utils.FV
   54 
   55 import GHC.Types.Unique.FM
   56 import GHC.Types.Var.Set
   57 import GHC.Types.Var.Env
   58 import GHC.Utils.Misc
   59 import GHC.Utils.Panic
   60 
   61 {-
   62 %************************************************************************
   63 %*                                                                      *
   64                  Free variables of types and coercions
   65 %*                                                                      *
   66 %************************************************************************
   67 -}
   68 
   69 {- Note [Shallow and deep free variables]
   70 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   71 Definitions
   72 
   73 * Shallow free variables of a type: the variables
   74   affected by substitution. Specifically, the (TyVarTy tv)
   75   and (CoVar cv) that appear
   76     - In the type and coercions appearing in the type
   77     - In shallow free variables of the kind of a Forall binder
   78   but NOT in the kind of the /occurrences/ of a type variable.
   79 
   80 * Deep free variables of a type: shallow free variables, plus
   81   the deep free variables of the kinds of those variables.
   82   That is,  deepFVs( t ) = closeOverKinds( shallowFVs( t ) )
   83 
   84 Examples:
   85 
   86   Type                     Shallow     Deep
   87   ---------------------------------
   88   (a : (k:Type))           {a}        {a,k}
   89   forall (a:(k:Type)). a   {k}        {k}
   90   (a:k->Type) (b:k)        {a,b}      {a,b,k}
   91 -}
   92 
   93 
   94 {- Note [Free variables of types]
   95 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   96 The family of functions tyCoVarsOfType, tyCoVarsOfTypes etc, returns
   97 a VarSet that is closed over the types of its variables.  More precisely,
   98   if    S = tyCoVarsOfType( t )
   99   and   (a:k) is in S
  100   then  tyCoVarsOftype( k ) is a subset of S
  101 
  102 Example: The tyCoVars of this ((a:* -> k) Int) is {a, k}.
  103 
  104 We could /not/ close over the kinds of the variable occurrences, and
  105 instead do so at call sites, but it seems that we always want to do
  106 so, so it's easiest to do it here.
  107 
  108 It turns out that getting the free variables of types is performance critical,
  109 so we profiled several versions, exploring different implementation strategies.
  110 
  111 1. Baseline version: uses FV naively. Essentially:
  112 
  113    tyCoVarsOfType ty = fvVarSet $ tyCoFVsOfType ty
  114 
  115    This is not nice, because FV introduces some overhead to implement
  116    determinism, and through its "interesting var" function, neither of which
  117    we need here, so they are a complete waste.
  118 
  119 2. UnionVarSet version: instead of reusing the FV-based code, we simply used
  120    VarSets directly, trying to avoid the overhead of FV. E.g.:
  121 
  122    -- FV version:
  123    tyCoFVsOfType (AppTy fun arg)    a b c = (tyCoFVsOfType fun `unionFV` tyCoFVsOfType arg) a b c
  124 
  125    -- UnionVarSet version:
  126    tyCoVarsOfType (AppTy fun arg)    = (tyCoVarsOfType fun `unionVarSet` tyCoVarsOfType arg)
  127 
  128    This looks deceptively similar, but while FV internally builds a list- and
  129    set-generating function, the VarSet functions manipulate sets directly, and
  130    the latter performs a lot worse than the naive FV version.
  131 
  132 3. Accumulator-style VarSet version: this is what we use now. We do use VarSet
  133    as our data structure, but delegate the actual work to a new
  134    ty_co_vars_of_...  family of functions, which use accumulator style and the
  135    "in-scope set" filter found in the internals of FV, but without the
  136    determinism overhead.
  137 
  138 See #14880.
  139 
  140 Note [Closing over free variable kinds]
  141 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  142 tyCoVarsOfType and tyCoFVsOfType, while traversing a type, will also close over
  143 free variable kinds. In previous GHC versions, this happened naively: whenever
  144 we would encounter an occurrence of a free type variable, we would close over
  145 its kind. This, however is wrong for two reasons (see #14880):
  146 
  147 1. Efficiency. If we have Proxy (a::k) -> Proxy (a::k) -> Proxy (a::k), then
  148    we don't want to have to traverse k more than once.
  149 
  150 2. Correctness. Imagine we have forall k. b -> k, where b has
  151    kind k, for some k bound in an outer scope. If we look at b's kind inside
  152    the forall, we'll collect that k is free and then remove k from the set of
  153    free variables. This is plain wrong. We must instead compute that b is free
  154    and then conclude that b's kind is free.
  155 
  156 An obvious first approach is to move the closing-over-kinds from the
  157 occurrences of a type variable to after finding the free vars - however, this
  158 turns out to introduce performance regressions, and isn't even entirely
  159 correct.
  160 
  161 In fact, it isn't even important *when* we close over kinds; what matters is
  162 that we handle each type var exactly once, and that we do it in the right
  163 context.
  164 
  165 So the next approach we tried was to use the "in-scope set" part of FV or the
  166 equivalent argument in the accumulator-style `ty_co_vars_of_type` function, to
  167 say "don't bother with variables we have already closed over". This should work
  168 fine in theory, but the code is complicated and doesn't perform well.
  169 
  170 But there is a simpler way, which is implemented here. Consider the two points
  171 above:
  172 
  173 1. Efficiency: we now have an accumulator, so the second time we encounter 'a',
  174    we'll ignore it, certainly not looking at its kind - this is why
  175    pre-checking set membership before inserting ends up not only being faster,
  176    but also being correct.
  177 
  178 2. Correctness: we have an "in-scope set" (I think we should call it it a
  179   "bound-var set"), specifying variables that are bound by a forall in the type
  180   we are traversing; we simply ignore these variables, certainly not looking at
  181   their kind.
  182 
  183 So now consider:
  184 
  185     forall k. b -> k
  186 
  187 where b :: k->Type is free; but of course, it's a different k! When looking at
  188 b -> k we'll have k in the bound-var set. So we'll ignore the k. But suppose
  189 this is our first encounter with b; we want the free vars of its kind. But we
  190 want to behave as if we took the free vars of its kind at the end; that is,
  191 with no bound vars in scope.
  192 
  193 So the solution is easy. The old code was this:
  194 
  195   ty_co_vars_of_type (TyVarTy v) is acc
  196     | v `elemVarSet` is  = acc
  197     | v `elemVarSet` acc = acc
  198     | otherwise          = ty_co_vars_of_type (tyVarKind v) is (extendVarSet acc v)
  199 
  200 Now all we need to do is take the free vars of tyVarKind v *with an empty
  201 bound-var set*, thus:
  202 
  203 ty_co_vars_of_type (TyVarTy v) is acc
  204   | v `elemVarSet` is  = acc
  205   | v `elemVarSet` acc = acc
  206   | otherwise          = ty_co_vars_of_type (tyVarKind v) emptyVarSet (extendVarSet acc v)
  207                                                           ^^^^^^^^^^^
  208 
  209 And that's it. This works because a variable is either bound or free. If it is bound,
  210 then we won't look at it at all. If it is free, then all the variables free in its
  211 kind are free -- regardless of whether some local variable has the same Unique.
  212 So if we're looking at a variable occurrence at all, then all variables in its
  213 kind are free.
  214 -}
  215 
  216 {- *********************************************************************
  217 *                                                                      *
  218           Endo for free variables
  219 *                                                                      *
  220 ********************************************************************* -}
  221 
  222 {- Note [Acumulating parameter free variables]
  223 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  224 We can use foldType to build an accumulating-parameter version of a
  225 free-var finder, thus:
  226 
  227     fvs :: Type -> TyCoVarSet
  228     fvs ty = appEndo (foldType folder ty) emptyVarSet
  229 
  230 Recall that
  231     foldType :: TyCoFolder env a -> env -> Type -> a
  232 
  233     newtype Endo a = Endo (a -> a)   -- In Data.Monoid
  234     instance Monoid a => Monoid (Endo a) where
  235        (Endo f) `mappend` (Endo g) = Endo (f.g)
  236 
  237     appEndo :: Endo a -> a -> a
  238     appEndo (Endo f) x = f x
  239 
  240 So `mappend` for Endos is just function composition.
  241 
  242 It's very important that, after optimisation, we end up with
  243 * an arity-three function
  244 * that is strict in the accumulator
  245 
  246    fvs env (TyVarTy v) acc
  247       | v `elemVarSet` env = acc
  248       | v `elemVarSet` acc = acc
  249       | otherwise          = acc `extendVarSet` v
  250    fvs env (AppTy t1 t2)   = fvs env t1 (fvs env t2 acc)
  251    ...
  252 
  253 The "strict in the accumulator" part is to ensure that in the
  254 AppTy equation we don't build a thunk for (fvs env t2 acc).
  255 
  256 The optimiser does do all this, but not very robustly. It depends
  257 critially on the basic arity-2 function not being exported, so that
  258 all its calls are visibly to three arguments. This analysis is
  259 done by the Call Arity pass.
  260 
  261 TL;DR: check this regularly!
  262 -}
  263 
  264 runTyCoVars :: Endo TyCoVarSet -> TyCoVarSet
  265 {-# INLINE runTyCoVars #-}
  266 runTyCoVars f = appEndo f emptyVarSet
  267 
  268 noView :: Type -> Maybe Type
  269 noView _ = Nothing
  270 
  271 {- *********************************************************************
  272 *                                                                      *
  273           Deep free variables
  274           See Note [Shallow and deep free variables]
  275 *                                                                      *
  276 ********************************************************************* -}
  277 
  278 tyCoVarsOfType :: Type -> TyCoVarSet
  279 tyCoVarsOfType ty = runTyCoVars (deep_ty ty)
  280 -- Alternative:
  281 --   tyCoVarsOfType ty = closeOverKinds (shallowTyCoVarsOfType ty)
  282 
  283 tyCoVarsOfTypes :: [Type] -> TyCoVarSet
  284 tyCoVarsOfTypes tys = runTyCoVars (deep_tys tys)
  285 -- Alternative:
  286 --   tyCoVarsOfTypes tys = closeOverKinds (shallowTyCoVarsOfTypes tys)
  287 
  288 tyCoVarsOfCo :: Coercion -> TyCoVarSet
  289 -- See Note [Free variables of Coercions]
  290 tyCoVarsOfCo co = runTyCoVars (deep_co co)
  291 
  292 tyCoVarsOfMCo :: MCoercion -> TyCoVarSet
  293 tyCoVarsOfMCo MRefl    = emptyVarSet
  294 tyCoVarsOfMCo (MCo co) = tyCoVarsOfCo co
  295 
  296 tyCoVarsOfCos :: [Coercion] -> TyCoVarSet
  297 tyCoVarsOfCos cos = runTyCoVars (deep_cos cos)
  298 
  299 deep_ty  :: Type       -> Endo TyCoVarSet
  300 deep_tys :: [Type]     -> Endo TyCoVarSet
  301 deep_co  :: Coercion   -> Endo TyCoVarSet
  302 deep_cos :: [Coercion] -> Endo TyCoVarSet
  303 (deep_ty, deep_tys, deep_co, deep_cos) = foldTyCo deepTcvFolder emptyVarSet
  304 
  305 deepTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
  306 deepTcvFolder = TyCoFolder { tcf_view = noView
  307                            , tcf_tyvar = do_tcv, tcf_covar = do_tcv
  308                            , tcf_hole  = do_hole, tcf_tycobinder = do_bndr }
  309   where
  310     do_tcv is v = Endo do_it
  311       where
  312         do_it acc | v `elemVarSet` is  = acc
  313                   | v `elemVarSet` acc = acc
  314                   | otherwise          = appEndo (deep_ty (varType v)) $
  315                                          acc `extendVarSet` v
  316 
  317     do_bndr is tcv _ = extendVarSet is tcv
  318     do_hole is hole  = do_tcv is (coHoleCoVar hole)
  319                        -- See Note [CoercionHoles and coercion free variables]
  320                        -- in GHC.Core.TyCo.Rep
  321 
  322 {- *********************************************************************
  323 *                                                                      *
  324           Shallow free variables
  325           See Note [Shallow and deep free variables]
  326 *                                                                      *
  327 ********************************************************************* -}
  328 
  329 
  330 shallowTyCoVarsOfType :: Type -> TyCoVarSet
  331 -- See Note [Free variables of types]
  332 shallowTyCoVarsOfType ty = runTyCoVars (shallow_ty ty)
  333 
  334 shallowTyCoVarsOfTypes :: [Type] -> TyCoVarSet
  335 shallowTyCoVarsOfTypes tys = runTyCoVars (shallow_tys tys)
  336 
  337 shallowTyCoVarsOfCo :: Coercion -> TyCoVarSet
  338 shallowTyCoVarsOfCo co = runTyCoVars (shallow_co co)
  339 
  340 shallowTyCoVarsOfCos :: [Coercion] -> TyCoVarSet
  341 shallowTyCoVarsOfCos cos = runTyCoVars (shallow_cos cos)
  342 
  343 -- | Returns free variables of types, including kind variables as
  344 -- a non-deterministic set. For type synonyms it does /not/ expand the
  345 -- synonym.
  346 shallowTyCoVarsOfTyVarEnv :: TyVarEnv Type -> TyCoVarSet
  347 -- See Note [Free variables of types]
  348 shallowTyCoVarsOfTyVarEnv tys = shallowTyCoVarsOfTypes (nonDetEltsUFM tys)
  349   -- It's OK to use nonDetEltsUFM here because we immediately
  350   -- forget the ordering by returning a set
  351 
  352 shallowTyCoVarsOfCoVarEnv :: CoVarEnv Coercion -> TyCoVarSet
  353 shallowTyCoVarsOfCoVarEnv cos = shallowTyCoVarsOfCos (nonDetEltsUFM cos)
  354   -- It's OK to use nonDetEltsUFM here because we immediately
  355   -- forget the ordering by returning a set
  356 
  357 shallow_ty  :: Type       -> Endo TyCoVarSet
  358 shallow_tys :: [Type]     -> Endo TyCoVarSet
  359 shallow_co  :: Coercion   -> Endo TyCoVarSet
  360 shallow_cos :: [Coercion] -> Endo TyCoVarSet
  361 (shallow_ty, shallow_tys, shallow_co, shallow_cos) = foldTyCo shallowTcvFolder emptyVarSet
  362 
  363 shallowTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
  364 shallowTcvFolder = TyCoFolder { tcf_view = noView
  365                               , tcf_tyvar = do_tcv, tcf_covar = do_tcv
  366                               , tcf_hole  = do_hole, tcf_tycobinder = do_bndr }
  367   where
  368     do_tcv is v = Endo do_it
  369       where
  370         do_it acc | v `elemVarSet` is  = acc
  371                   | v `elemVarSet` acc = acc
  372                   | otherwise          = acc `extendVarSet` v
  373 
  374     do_bndr is tcv _ = extendVarSet is tcv
  375     do_hole _ _  = mempty   -- Ignore coercion holes
  376 
  377 
  378 {- *********************************************************************
  379 *                                                                      *
  380           Free coercion variables
  381 *                                                                      *
  382 ********************************************************************* -}
  383 
  384 
  385 {- Note [Finding free coercion varibles]
  386 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  387 Here we are only interested in the free /coercion/ variables.
  388 We can achieve this through a slightly different TyCo folder.
  389 
  390 Notice that we look deeply, into kinds.
  391 
  392 See #14880.
  393 -}
  394 
  395 coVarsOfType  :: Type       -> CoVarSet
  396 coVarsOfTypes :: [Type]     -> CoVarSet
  397 coVarsOfCo    :: Coercion   -> CoVarSet
  398 coVarsOfCos   :: [Coercion] -> CoVarSet
  399 
  400 coVarsOfType  ty  = runTyCoVars (deep_cv_ty ty)
  401 coVarsOfTypes tys = runTyCoVars (deep_cv_tys tys)
  402 coVarsOfCo    co  = runTyCoVars (deep_cv_co co)
  403 coVarsOfCos   cos = runTyCoVars (deep_cv_cos cos)
  404 
  405 deep_cv_ty  :: Type       -> Endo CoVarSet
  406 deep_cv_tys :: [Type]     -> Endo CoVarSet
  407 deep_cv_co  :: Coercion   -> Endo CoVarSet
  408 deep_cv_cos :: [Coercion] -> Endo CoVarSet
  409 (deep_cv_ty, deep_cv_tys, deep_cv_co, deep_cv_cos) = foldTyCo deepCoVarFolder emptyVarSet
  410 
  411 deepCoVarFolder :: TyCoFolder TyCoVarSet (Endo CoVarSet)
  412 deepCoVarFolder = TyCoFolder { tcf_view = noView
  413                              , tcf_tyvar = do_tyvar, tcf_covar = do_covar
  414                              , tcf_hole  = do_hole, tcf_tycobinder = do_bndr }
  415   where
  416     do_tyvar _ _  = mempty
  417       -- This do_tyvar means we won't see any CoVars in this
  418       -- TyVar's kind.   This may be wrong; but it's the way it's
  419       -- always been.  And its awkward to change, because
  420       -- the tyvar won't end up in the accumulator, so
  421       -- we'd look repeatedly.  Blargh.
  422 
  423     do_covar is v = Endo do_it
  424       where
  425         do_it acc | v `elemVarSet` is  = acc
  426                   | v `elemVarSet` acc = acc
  427                   | otherwise          = appEndo (deep_cv_ty (varType v)) $
  428                                          acc `extendVarSet` v
  429 
  430     do_bndr is tcv _ = extendVarSet is tcv
  431     do_hole is hole  = do_covar is (coHoleCoVar hole)
  432                        -- See Note [CoercionHoles and coercion free variables]
  433                        -- in GHC.Core.TyCo.Rep
  434 
  435 
  436 {- *********************************************************************
  437 *                                                                      *
  438           Closing over kinds
  439 *                                                                      *
  440 ********************************************************************* -}
  441 
  442 ------------- Closing over kinds -----------------
  443 
  444 closeOverKinds :: TyCoVarSet -> TyCoVarSet
  445 -- For each element of the input set,
  446 -- add the deep free variables of its kind
  447 closeOverKinds vs = nonDetStrictFoldVarSet do_one vs vs
  448   where
  449     do_one v acc = appEndo (deep_ty (varType v)) acc
  450 
  451 {- --------------- Alternative version 1 (using FV) ------------
  452 closeOverKinds = fvVarSet . closeOverKindsFV . nonDetEltsUniqSet
  453 -}
  454 
  455 {- ---------------- Alternative version 2 -------------
  456 
  457 -- | Add the kind variables free in the kinds of the tyvars in the given set.
  458 -- Returns a non-deterministic set.
  459 closeOverKinds :: TyCoVarSet -> TyCoVarSet
  460 closeOverKinds vs
  461    = go vs vs
  462   where
  463     go :: VarSet   -- Work list
  464        -> VarSet   -- Accumulator, always a superset of wl
  465        -> VarSet
  466     go wl acc
  467       | isEmptyVarSet wl = acc
  468       | otherwise        = go wl_kvs (acc `unionVarSet` wl_kvs)
  469       where
  470         k v inner_acc = ty_co_vars_of_type (varType v) acc inner_acc
  471         wl_kvs = nonDetFoldVarSet k emptyVarSet wl
  472         -- wl_kvs = union of shallow free vars of the kinds of wl
  473         --          but don't bother to collect vars in acc
  474 
  475 -}
  476 
  477 {- ---------------- Alternative version 3 -------------
  478 -- | Add the kind variables free in the kinds of the tyvars in the given set.
  479 -- Returns a non-deterministic set.
  480 closeOverKinds :: TyVarSet -> TyVarSet
  481 closeOverKinds vs = close_over_kinds vs emptyVarSet
  482 
  483 
  484 close_over_kinds :: TyVarSet  -- Work list
  485                  -> TyVarSet  -- Accumulator
  486                  -> TyVarSet
  487 -- Precondition: in any call (close_over_kinds wl acc)
  488 --  for every tv in acc, the shallow kind-vars of tv
  489 --  are either in the work list wl, or in acc
  490 -- Postcondition: result is the deep free vars of (wl `union` acc)
  491 close_over_kinds wl acc
  492   = nonDetFoldVarSet do_one acc wl
  493   where
  494     do_one :: Var -> TyVarSet -> TyVarSet
  495     -- (do_one v acc) adds v and its deep free-vars to acc
  496     do_one v acc | v `elemVarSet` acc
  497                  = acc
  498                  | otherwise
  499                  = close_over_kinds (shallowTyCoVarsOfType (varType v)) $
  500                    acc `extendVarSet` v
  501 -}
  502 
  503 
  504 {- *********************************************************************
  505 *                                                                      *
  506           The FV versions return deterministic results
  507 *                                                                      *
  508 ********************************************************************* -}
  509 
  510 -- | Given a list of tyvars returns a deterministic FV computation that
  511 -- returns the given tyvars with the kind variables free in the kinds of the
  512 -- given tyvars.
  513 closeOverKindsFV :: [TyVar] -> FV
  514 closeOverKindsFV tvs =
  515   mapUnionFV (tyCoFVsOfType . tyVarKind) tvs `unionFV` mkFVs tvs
  516 
  517 -- | Add the kind variables free in the kinds of the tyvars in the given set.
  518 -- Returns a deterministically ordered list.
  519 closeOverKindsList :: [TyVar] -> [TyVar]
  520 closeOverKindsList tvs = fvVarList $ closeOverKindsFV tvs
  521 
  522 -- | Add the kind variables free in the kinds of the tyvars in the given set.
  523 -- Returns a deterministic set.
  524 closeOverKindsDSet :: DTyVarSet -> DTyVarSet
  525 closeOverKindsDSet = fvDVarSet . closeOverKindsFV . dVarSetElems
  526 
  527 -- | `tyCoFVsOfType` that returns free variables of a type in a deterministic
  528 -- set. For explanation of why using `VarSet` is not deterministic see
  529 -- Note [Deterministic FV] in "GHC.Utils.FV".
  530 tyCoVarsOfTypeDSet :: Type -> DTyCoVarSet
  531 -- See Note [Free variables of types]
  532 tyCoVarsOfTypeDSet ty = fvDVarSet $ tyCoFVsOfType ty
  533 
  534 -- | `tyCoFVsOfType` that returns free variables of a type in deterministic
  535 -- order. For explanation of why using `VarSet` is not deterministic see
  536 -- Note [Deterministic FV] in "GHC.Utils.FV".
  537 tyCoVarsOfTypeList :: Type -> [TyCoVar]
  538 -- See Note [Free variables of types]
  539 tyCoVarsOfTypeList ty = fvVarList $ tyCoFVsOfType ty
  540 
  541 -- | Returns free variables of types, including kind variables as
  542 -- a deterministic set. For type synonyms it does /not/ expand the
  543 -- synonym.
  544 tyCoVarsOfTypesDSet :: [Type] -> DTyCoVarSet
  545 -- See Note [Free variables of types]
  546 tyCoVarsOfTypesDSet tys = fvDVarSet $ tyCoFVsOfTypes tys
  547 
  548 -- | Returns free variables of types, including kind variables as
  549 -- a deterministically ordered list. For type synonyms it does /not/ expand the
  550 -- synonym.
  551 tyCoVarsOfTypesList :: [Type] -> [TyCoVar]
  552 -- See Note [Free variables of types]
  553 tyCoVarsOfTypesList tys = fvVarList $ tyCoFVsOfTypes tys
  554 
  555 -- | The worker for `tyCoFVsOfType` and `tyCoFVsOfTypeList`.
  556 -- The previous implementation used `unionVarSet` which is O(n+m) and can
  557 -- make the function quadratic.
  558 -- It's exported, so that it can be composed with
  559 -- other functions that compute free variables.
  560 -- See Note [FV naming conventions] in "GHC.Utils.FV".
  561 --
  562 -- Eta-expanded because that makes it run faster (apparently)
  563 -- See Note [FV eta expansion] in "GHC.Utils.FV" for explanation.
  564 tyCoFVsOfType :: Type -> FV
  565 -- See Note [Free variables of types]
  566 tyCoFVsOfType (TyVarTy v)        f bound_vars (acc_list, acc_set)
  567   | not (f v) = (acc_list, acc_set)
  568   | v `elemVarSet` bound_vars = (acc_list, acc_set)
  569   | v `elemVarSet` acc_set = (acc_list, acc_set)
  570   | otherwise = tyCoFVsOfType (tyVarKind v) f
  571                                emptyVarSet   -- See Note [Closing over free variable kinds]
  572                                (v:acc_list, extendVarSet acc_set v)
  573 tyCoFVsOfType (TyConApp _ tys)   f bound_vars acc = tyCoFVsOfTypes tys f bound_vars acc
  574 tyCoFVsOfType (LitTy {})         f bound_vars acc = emptyFV f bound_vars acc
  575 tyCoFVsOfType (AppTy fun arg)    f bound_vars acc = (tyCoFVsOfType fun `unionFV` tyCoFVsOfType arg) f bound_vars acc
  576 tyCoFVsOfType (FunTy _ w arg res)  f bound_vars acc = (tyCoFVsOfType w `unionFV` tyCoFVsOfType arg `unionFV` tyCoFVsOfType res) f bound_vars acc
  577 tyCoFVsOfType (ForAllTy bndr ty) f bound_vars acc = tyCoFVsBndr bndr (tyCoFVsOfType ty)  f bound_vars acc
  578 tyCoFVsOfType (CastTy ty co)     f bound_vars acc = (tyCoFVsOfType ty `unionFV` tyCoFVsOfCo co) f bound_vars acc
  579 tyCoFVsOfType (CoercionTy co)    f bound_vars acc = tyCoFVsOfCo co f bound_vars acc
  580 
  581 tyCoFVsBndr :: TyCoVarBinder -> FV -> FV
  582 -- Free vars of (forall b. <thing with fvs>)
  583 tyCoFVsBndr (Bndr tv _) fvs = tyCoFVsVarBndr tv fvs
  584 
  585 tyCoFVsVarBndrs :: [Var] -> FV -> FV
  586 tyCoFVsVarBndrs vars fvs = foldr tyCoFVsVarBndr fvs vars
  587 
  588 tyCoFVsVarBndr :: Var -> FV -> FV
  589 tyCoFVsVarBndr var fvs
  590   = tyCoFVsOfType (varType var)   -- Free vars of its type/kind
  591     `unionFV` delFV var fvs       -- Delete it from the thing-inside
  592 
  593 tyCoFVsOfTypes :: [Type] -> FV
  594 -- See Note [Free variables of types]
  595 tyCoFVsOfTypes (ty:tys) fv_cand in_scope acc = (tyCoFVsOfType ty `unionFV` tyCoFVsOfTypes tys) fv_cand in_scope acc
  596 tyCoFVsOfTypes []       fv_cand in_scope acc = emptyFV fv_cand in_scope acc
  597 
  598 -- | Get a deterministic set of the vars free in a coercion
  599 tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet
  600 -- See Note [Free variables of types]
  601 tyCoVarsOfCoDSet co = fvDVarSet $ tyCoFVsOfCo co
  602 
  603 tyCoVarsOfCoList :: Coercion -> [TyCoVar]
  604 -- See Note [Free variables of types]
  605 tyCoVarsOfCoList co = fvVarList $ tyCoFVsOfCo co
  606 
  607 tyCoFVsOfMCo :: MCoercion -> FV
  608 tyCoFVsOfMCo MRefl    = emptyFV
  609 tyCoFVsOfMCo (MCo co) = tyCoFVsOfCo co
  610 
  611 tyCoFVsOfCo :: Coercion -> FV
  612 -- Extracts type and coercion variables from a coercion
  613 -- See Note [Free variables of types]
  614 tyCoFVsOfCo (Refl ty) fv_cand in_scope acc
  615   = tyCoFVsOfType ty fv_cand in_scope acc
  616 tyCoFVsOfCo (GRefl _ ty mco) fv_cand in_scope acc
  617   = (tyCoFVsOfType ty `unionFV` tyCoFVsOfMCo mco) fv_cand in_scope acc
  618 tyCoFVsOfCo (TyConAppCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc
  619 tyCoFVsOfCo (AppCo co arg) fv_cand in_scope acc
  620   = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc
  621 tyCoFVsOfCo (ForAllCo tv kind_co co) fv_cand in_scope acc
  622   = (tyCoFVsVarBndr tv (tyCoFVsOfCo co) `unionFV` tyCoFVsOfCo kind_co) fv_cand in_scope acc
  623 tyCoFVsOfCo (FunCo _ w co1 co2)    fv_cand in_scope acc
  624   = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2 `unionFV` tyCoFVsOfCo w) fv_cand in_scope acc
  625 tyCoFVsOfCo (CoVarCo v) fv_cand in_scope acc
  626   = tyCoFVsOfCoVar v fv_cand in_scope acc
  627 tyCoFVsOfCo (HoleCo h) fv_cand in_scope acc
  628   = tyCoFVsOfCoVar (coHoleCoVar h) fv_cand in_scope acc
  629     -- See Note [CoercionHoles and coercion free variables]
  630 tyCoFVsOfCo (AxiomInstCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc
  631 tyCoFVsOfCo (UnivCo p _ t1 t2) fv_cand in_scope acc
  632   = (tyCoFVsOfProv p `unionFV` tyCoFVsOfType t1
  633                      `unionFV` tyCoFVsOfType t2) fv_cand in_scope acc
  634 tyCoFVsOfCo (SymCo co)          fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
  635 tyCoFVsOfCo (TransCo co1 co2)   fv_cand in_scope acc = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2) fv_cand in_scope acc
  636 tyCoFVsOfCo (NthCo _ _ co)      fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
  637 tyCoFVsOfCo (LRCo _ co)         fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
  638 tyCoFVsOfCo (InstCo co arg)     fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc
  639 tyCoFVsOfCo (KindCo co)         fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
  640 tyCoFVsOfCo (SubCo co)          fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
  641 tyCoFVsOfCo (AxiomRuleCo _ cs)  fv_cand in_scope acc = tyCoFVsOfCos cs fv_cand in_scope acc
  642 
  643 tyCoFVsOfCoVar :: CoVar -> FV
  644 tyCoFVsOfCoVar v fv_cand in_scope acc
  645   = (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc
  646 
  647 tyCoFVsOfProv :: UnivCoProvenance -> FV
  648 tyCoFVsOfProv (PhantomProv co)    fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
  649 tyCoFVsOfProv (ProofIrrelProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
  650 tyCoFVsOfProv (PluginProv _)      fv_cand in_scope acc = emptyFV fv_cand in_scope acc
  651 tyCoFVsOfProv (CorePrepProv _)    fv_cand in_scope acc = emptyFV fv_cand in_scope acc
  652 
  653 tyCoFVsOfCos :: [Coercion] -> FV
  654 tyCoFVsOfCos []       fv_cand in_scope acc = emptyFV fv_cand in_scope acc
  655 tyCoFVsOfCos (co:cos) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCos cos) fv_cand in_scope acc
  656 
  657 
  658 ----- Whether a covar is /Almost Devoid/ in a type or coercion ----
  659 
  660 -- | Given a covar and a coercion, returns True if covar is almost devoid in
  661 -- the coercion. That is, covar can only appear in Refl and GRefl.
  662 -- See last wrinkle in Note [Unused coercion variable in ForAllCo] in "GHC.Core.Coercion"
  663 almostDevoidCoVarOfCo :: CoVar -> Coercion -> Bool
  664 almostDevoidCoVarOfCo cv co =
  665   almost_devoid_co_var_of_co co cv
  666 
  667 almost_devoid_co_var_of_co :: Coercion -> CoVar -> Bool
  668 almost_devoid_co_var_of_co (Refl {}) _ = True   -- covar is allowed in Refl and
  669 almost_devoid_co_var_of_co (GRefl {}) _ = True  -- GRefl, so we don't look into
  670                                                 -- the coercions
  671 almost_devoid_co_var_of_co (TyConAppCo _ _ cos) cv
  672   = almost_devoid_co_var_of_cos cos cv
  673 almost_devoid_co_var_of_co (AppCo co arg) cv
  674   = almost_devoid_co_var_of_co co cv
  675   && almost_devoid_co_var_of_co arg cv
  676 almost_devoid_co_var_of_co (ForAllCo v kind_co co) cv
  677   = almost_devoid_co_var_of_co kind_co cv
  678   && (v == cv || almost_devoid_co_var_of_co co cv)
  679 almost_devoid_co_var_of_co (FunCo _ w co1 co2) cv
  680   = almost_devoid_co_var_of_co w cv
  681   && almost_devoid_co_var_of_co co1 cv
  682   && almost_devoid_co_var_of_co co2 cv
  683 almost_devoid_co_var_of_co (CoVarCo v) cv = v /= cv
  684 almost_devoid_co_var_of_co (HoleCo h)  cv = (coHoleCoVar h) /= cv
  685 almost_devoid_co_var_of_co (AxiomInstCo _ _ cos) cv
  686   = almost_devoid_co_var_of_cos cos cv
  687 almost_devoid_co_var_of_co (UnivCo p _ t1 t2) cv
  688   = almost_devoid_co_var_of_prov p cv
  689   && almost_devoid_co_var_of_type t1 cv
  690   && almost_devoid_co_var_of_type t2 cv
  691 almost_devoid_co_var_of_co (SymCo co) cv
  692   = almost_devoid_co_var_of_co co cv
  693 almost_devoid_co_var_of_co (TransCo co1 co2) cv
  694   = almost_devoid_co_var_of_co co1 cv
  695   && almost_devoid_co_var_of_co co2 cv
  696 almost_devoid_co_var_of_co (NthCo _ _ co) cv
  697   = almost_devoid_co_var_of_co co cv
  698 almost_devoid_co_var_of_co (LRCo _ co) cv
  699   = almost_devoid_co_var_of_co co cv
  700 almost_devoid_co_var_of_co (InstCo co arg) cv
  701   = almost_devoid_co_var_of_co co cv
  702   && almost_devoid_co_var_of_co arg cv
  703 almost_devoid_co_var_of_co (KindCo co) cv
  704   = almost_devoid_co_var_of_co co cv
  705 almost_devoid_co_var_of_co (SubCo co) cv
  706   = almost_devoid_co_var_of_co co cv
  707 almost_devoid_co_var_of_co (AxiomRuleCo _ cs) cv
  708   = almost_devoid_co_var_of_cos cs cv
  709 
  710 almost_devoid_co_var_of_cos :: [Coercion] -> CoVar -> Bool
  711 almost_devoid_co_var_of_cos [] _ = True
  712 almost_devoid_co_var_of_cos (co:cos) cv
  713   = almost_devoid_co_var_of_co co cv
  714   && almost_devoid_co_var_of_cos cos cv
  715 
  716 almost_devoid_co_var_of_prov :: UnivCoProvenance -> CoVar -> Bool
  717 almost_devoid_co_var_of_prov (PhantomProv co) cv
  718   = almost_devoid_co_var_of_co co cv
  719 almost_devoid_co_var_of_prov (ProofIrrelProv co) cv
  720   = almost_devoid_co_var_of_co co cv
  721 almost_devoid_co_var_of_prov (PluginProv _)   _ = True
  722 almost_devoid_co_var_of_prov (CorePrepProv _) _ = True
  723 
  724 almost_devoid_co_var_of_type :: Type -> CoVar -> Bool
  725 almost_devoid_co_var_of_type (TyVarTy _) _ = True
  726 almost_devoid_co_var_of_type (TyConApp _ tys) cv
  727   = almost_devoid_co_var_of_types tys cv
  728 almost_devoid_co_var_of_type (LitTy {}) _ = True
  729 almost_devoid_co_var_of_type (AppTy fun arg) cv
  730   = almost_devoid_co_var_of_type fun cv
  731   && almost_devoid_co_var_of_type arg cv
  732 almost_devoid_co_var_of_type (FunTy _ w arg res) cv
  733   = almost_devoid_co_var_of_type w cv
  734   && almost_devoid_co_var_of_type arg cv
  735   && almost_devoid_co_var_of_type res cv
  736 almost_devoid_co_var_of_type (ForAllTy (Bndr v _) ty) cv
  737   = almost_devoid_co_var_of_type (varType v) cv
  738   && (v == cv || almost_devoid_co_var_of_type ty cv)
  739 almost_devoid_co_var_of_type (CastTy ty co) cv
  740   = almost_devoid_co_var_of_type ty cv
  741   && almost_devoid_co_var_of_co co cv
  742 almost_devoid_co_var_of_type (CoercionTy co) cv
  743   = almost_devoid_co_var_of_co co cv
  744 
  745 almost_devoid_co_var_of_types :: [Type] -> CoVar -> Bool
  746 almost_devoid_co_var_of_types [] _ = True
  747 almost_devoid_co_var_of_types (ty:tys) cv
  748   = almost_devoid_co_var_of_type ty cv
  749   && almost_devoid_co_var_of_types tys cv
  750 
  751 
  752 
  753 {- *********************************************************************
  754 *                                                                      *
  755                  Injective free vars
  756 *                                                                      *
  757 ********************************************************************* -}
  758 
  759 -- | Returns the free variables of a 'Type' that are in injective positions.
  760 -- Specifically, it finds the free variables while:
  761 --
  762 -- * Expanding type synonyms
  763 --
  764 -- * Ignoring the coercion in @(ty |> co)@
  765 --
  766 -- * Ignoring the non-injective fields of a 'TyConApp'
  767 --
  768 --
  769 -- For example, if @F@ is a non-injective type family, then:
  770 --
  771 -- @
  772 -- injectiveTyVarsOf( Either c (Maybe (a, F b c)) ) = {a,c}
  773 -- @
  774 --
  775 -- If @'injectiveVarsOfType' ty = itvs@, then knowing @ty@ fixes @itvs@.
  776 -- More formally, if
  777 -- @a@ is in @'injectiveVarsOfType' ty@
  778 -- and  @S1(ty) ~ S2(ty)@,
  779 -- then @S1(a)  ~ S2(a)@,
  780 -- where @S1@ and @S2@ are arbitrary substitutions.
  781 --
  782 -- See @Note [When does a tycon application need an explicit kind signature?]@.
  783 injectiveVarsOfType :: Bool   -- ^ Should we look under injective type families?
  784                               -- See Note [Coverage condition for injective type families]
  785                               -- in "GHC.Tc.Instance.Family".
  786                     -> Type -> FV
  787 injectiveVarsOfType look_under_tfs = go
  788   where
  789     go ty                  | Just ty' <- coreView ty
  790                            = go ty'
  791     go (TyVarTy v)         = unitFV v `unionFV` go (tyVarKind v)
  792     go (AppTy f a)         = go f `unionFV` go a
  793     go (FunTy _ w ty1 ty2) = go w `unionFV` go ty1 `unionFV` go ty2
  794     go (TyConApp tc tys)   =
  795       case tyConInjectivityInfo tc of
  796         Injective inj
  797           |  look_under_tfs || not (isTypeFamilyTyCon tc)
  798           -> mapUnionFV go $
  799              filterByList (inj ++ repeat True) tys
  800                          -- Oversaturated arguments to a tycon are
  801                          -- always injective, hence the repeat True
  802         _ -> emptyFV
  803     go (ForAllTy (Bndr tv _) ty) = go (tyVarKind tv) `unionFV` delFV tv (go ty)
  804     go LitTy{}                   = emptyFV
  805     go (CastTy ty _)             = go ty
  806     go CoercionTy{}              = emptyFV
  807 
  808 -- | Returns the free variables of a 'Type' that are in injective positions.
  809 -- Specifically, it finds the free variables while:
  810 --
  811 -- * Expanding type synonyms
  812 --
  813 -- * Ignoring the coercion in @(ty |> co)@
  814 --
  815 -- * Ignoring the non-injective fields of a 'TyConApp'
  816 --
  817 -- See @Note [When does a tycon application need an explicit kind signature?]@.
  818 injectiveVarsOfTypes :: Bool -- ^ look under injective type families?
  819                              -- See Note [Coverage condition for injective type families]
  820                              -- in "GHC.Tc.Instance.Family".
  821                      -> [Type] -> FV
  822 injectiveVarsOfTypes look_under_tfs = mapUnionFV (injectiveVarsOfType look_under_tfs)
  823 
  824 
  825 {- *********************************************************************
  826 *                                                                      *
  827                  Invisible vars
  828 *                                                                      *
  829 ********************************************************************* -}
  830 
  831 
  832 -- | Returns the set of variables that are used invisibly anywhere within
  833 -- the given type. A variable will be included even if it is used both visibly
  834 -- and invisibly. An invisible use site includes:
  835 --   * In the kind of a variable
  836 --   * In the kind of a bound variable in a forall
  837 --   * In a coercion
  838 --   * In a Specified or Inferred argument to a function
  839 -- See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in "GHC.Core.TyCo.Rep"
  840 invisibleVarsOfType :: Type -> FV
  841 invisibleVarsOfType = go
  842   where
  843     go ty                 | Just ty' <- coreView ty
  844                           = go ty'
  845     go (TyVarTy v)        = go (tyVarKind v)
  846     go (AppTy f a)        = go f `unionFV` go a
  847     go (FunTy _ w ty1 ty2) = go w `unionFV` go ty1 `unionFV` go ty2
  848     go (TyConApp tc tys)  = tyCoFVsOfTypes invisibles `unionFV`
  849                             invisibleVarsOfTypes visibles
  850       where (invisibles, visibles) = partitionInvisibleTypes tc tys
  851     go (ForAllTy tvb ty)  = tyCoFVsBndr tvb $ go ty
  852     go LitTy{}            = emptyFV
  853     go (CastTy ty co)     = tyCoFVsOfCo co `unionFV` go ty
  854     go (CoercionTy co)    = tyCoFVsOfCo co
  855 
  856 -- | Like 'invisibleVarsOfType', but for many types.
  857 invisibleVarsOfTypes :: [Type] -> FV
  858 invisibleVarsOfTypes = mapUnionFV invisibleVarsOfType
  859 
  860 
  861 {- *********************************************************************
  862 *                                                                      *
  863                  Any free vars
  864 *                                                                      *
  865 ********************************************************************* -}
  866 
  867 {-# INLINE afvFolder #-}   -- so that specialization to (const True) works
  868 afvFolder :: (TyCoVar -> Bool) -> TyCoFolder TyCoVarSet DM.Any
  869 afvFolder check_fv = TyCoFolder { tcf_view = noView
  870                                 , tcf_tyvar = do_tcv, tcf_covar = do_tcv
  871                                 , tcf_hole = do_hole, tcf_tycobinder = do_bndr }
  872   where
  873     do_tcv is tv = Any (not (tv `elemVarSet` is) && check_fv tv)
  874     do_hole _ _  = Any False    -- I'm unsure; probably never happens
  875     do_bndr is tv _ = is `extendVarSet` tv
  876 
  877 anyFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool
  878 anyFreeVarsOfType check_fv ty = DM.getAny (f ty)
  879   where (f, _, _, _) = foldTyCo (afvFolder check_fv) emptyVarSet
  880 
  881 anyFreeVarsOfTypes :: (TyCoVar -> Bool) -> [Type] -> Bool
  882 anyFreeVarsOfTypes check_fv tys = DM.getAny (f tys)
  883   where (_, f, _, _) = foldTyCo (afvFolder check_fv) emptyVarSet
  884 
  885 anyFreeVarsOfCo :: (TyCoVar -> Bool) -> Coercion -> Bool
  886 anyFreeVarsOfCo check_fv co = DM.getAny (f co)
  887   where (_, _, f, _) = foldTyCo (afvFolder check_fv) emptyVarSet
  888 
  889 noFreeVarsOfType :: Type -> Bool
  890 noFreeVarsOfType ty = not $ DM.getAny (f ty)
  891   where (f, _, _, _) = foldTyCo (afvFolder (const True)) emptyVarSet
  892 
  893 noFreeVarsOfTypes :: [Type] -> Bool
  894 noFreeVarsOfTypes tys = not $ DM.getAny (f tys)
  895   where (_, f, _, _) = foldTyCo (afvFolder (const True)) emptyVarSet
  896 
  897 noFreeVarsOfCo :: Coercion -> Bool
  898 noFreeVarsOfCo co = not $ DM.getAny (f co)
  899   where (_, _, f, _) = foldTyCo (afvFolder (const True)) emptyVarSet
  900 
  901 
  902 {- *********************************************************************
  903 *                                                                      *
  904                  scopedSort
  905 *                                                                      *
  906 ********************************************************************* -}
  907 
  908 {- Note [ScopedSort]
  909 ~~~~~~~~~~~~~~~~~~~~
  910 Consider
  911 
  912   foo :: Proxy a -> Proxy (b :: k) -> Proxy (a :: k2) -> ()
  913 
  914 This function type is implicitly generalised over [a, b, k, k2]. These
  915 variables will be Specified; that is, they will be available for visible
  916 type application. This is because they are written in the type signature
  917 by the user.
  918 
  919 However, we must ask: what order will they appear in? In cases without
  920 dependency, this is easy: we just use the lexical left-to-right ordering
  921 of first occurrence. With dependency, we cannot get off the hook so
  922 easily.
  923 
  924 We thus state:
  925 
  926  * These variables appear in the order as given by ScopedSort, where
  927    the input to ScopedSort is the left-to-right order of first occurrence.
  928 
  929 Note that this applies only to *implicit* quantification, without a
  930 `forall`. If the user writes a `forall`, then we just use the order given.
  931 
  932 ScopedSort is defined thusly (as proposed in #15743):
  933   * Work left-to-right through the input list, with a cursor.
  934   * If variable v at the cursor is depended on by any earlier variable w,
  935     move v immediately before the leftmost such w.
  936 
  937 INVARIANT: The prefix of variables before the cursor form a valid telescope.
  938 
  939 Note that ScopedSort makes sense only after type inference is done and all
  940 types/kinds are fully settled and zonked.
  941 
  942 -}
  943 
  944 -- | Do a topological sort on a list of tyvars,
  945 --   so that binders occur before occurrences
  946 -- E.g. given  [ a::k, k::*, b::k ]
  947 -- it'll return a well-scoped list [ k::*, a::k, b::k ]
  948 --
  949 -- This is a deterministic sorting operation
  950 -- (that is, doesn't depend on Uniques).
  951 --
  952 -- It is also meant to be stable: that is, variables should not
  953 -- be reordered unnecessarily. This is specified in Note [ScopedSort]
  954 -- See also Note [Ordering of implicit variables] in "GHC.Rename.HsType"
  955 
  956 scopedSort :: [TyCoVar] -> [TyCoVar]
  957 scopedSort = go [] []
  958   where
  959     go :: [TyCoVar] -- already sorted, in reverse order
  960        -> [TyCoVarSet] -- each set contains all the variables which must be placed
  961                        -- before the tv corresponding to the set; they are accumulations
  962                        -- of the fvs in the sorted tvs' kinds
  963 
  964                        -- This list is in 1-to-1 correspondence with the sorted tyvars
  965                        -- INVARIANT:
  966                        --   all (\tl -> all (`subVarSet` head tl) (tail tl)) (tails fv_list)
  967                        -- That is, each set in the list is a superset of all later sets.
  968 
  969        -> [TyCoVar] -- yet to be sorted
  970        -> [TyCoVar]
  971     go acc _fv_list [] = reverse acc
  972     go acc  fv_list (tv:tvs)
  973       = go acc' fv_list' tvs
  974       where
  975         (acc', fv_list') = insert tv acc fv_list
  976 
  977     insert :: TyCoVar       -- var to insert
  978            -> [TyCoVar]     -- sorted list, in reverse order
  979            -> [TyCoVarSet]  -- list of fvs, as above
  980            -> ([TyCoVar], [TyCoVarSet])   -- augmented lists
  981     insert tv []     []         = ([tv], [tyCoVarsOfType (tyVarKind tv)])
  982     insert tv (a:as) (fvs:fvss)
  983       | tv `elemVarSet` fvs
  984       , (as', fvss') <- insert tv as fvss
  985       = (a:as', fvs `unionVarSet` fv_tv : fvss')
  986 
  987       | otherwise
  988       = (tv:a:as, fvs `unionVarSet` fv_tv : fvs : fvss)
  989       where
  990         fv_tv = tyCoVarsOfType (tyVarKind tv)
  991 
  992        -- lists not in correspondence
  993     insert _ _ _ = panic "scopedSort"
  994 
  995 -- | Get the free vars of a type in scoped order
  996 tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
  997 tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList
  998 
  999 -- | Get the free vars of types in scoped order
 1000 tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
 1001 tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList