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