Update Trac ticket URLs to point to GitLab
[ghc.git] / compiler / types / FamInstEnv.hs
1 -- (c) The University of Glasgow 2006
2 --
3 -- FamInstEnv: Type checked family instance declarations
4
5 {-# LANGUAGE CPP, GADTs, ScopedTypeVariables, BangPatterns, TupleSections #-}
6
7 module FamInstEnv (
8 FamInst(..), FamFlavor(..), famInstAxiom, famInstTyCon, famInstRHS,
9 famInstsRepTyCons, famInstRepTyCon_maybe, dataFamInstRepTyCon,
10 pprFamInst, pprFamInsts,
11 mkImportedFamInst,
12
13 FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs,
14 extendFamInstEnv, extendFamInstEnvList,
15 famInstEnvElts, famInstEnvSize, familyInstances,
16
17 -- * CoAxioms
18 mkCoAxBranch, mkBranchedCoAxiom, mkUnbranchedCoAxiom, mkSingleCoAxiom,
19 mkNewTypeCoAxiom,
20
21 FamInstMatch(..),
22 lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvByTyCon,
23
24 isDominatedBy, apartnessCheck,
25
26 -- Injectivity
27 InjectivityCheckResult(..),
28 lookupFamInstEnvInjectivityConflicts, injectiveBranches,
29
30 -- Normalisation
31 topNormaliseType, topNormaliseType_maybe,
32 normaliseType, normaliseTcApp, normaliseTcArgs,
33 reduceTyFamApp_maybe,
34
35 -- Flattening
36 flattenTys
37 ) where
38
39 #include "HsVersions.h"
40
41 import GhcPrelude
42
43 import Unify
44 import Type
45 import TyCoRep
46 import TyCon
47 import Coercion
48 import CoAxiom
49 import VarSet
50 import VarEnv
51 import Name
52 import PrelNames ( eqPrimTyConKey )
53 import UniqDFM
54 import Outputable
55 import Maybes
56 import CoreMap
57 import Unique
58 import Util
59 import Var
60 import Pair
61 import SrcLoc
62 import FastString
63 import Control.Monad
64 import Data.List( mapAccumL )
65 import Data.Array( Array, assocs )
66
67 {-
68 ************************************************************************
69 * *
70 Type checked family instance heads
71 * *
72 ************************************************************************
73
74 Note [FamInsts and CoAxioms]
75 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
76 * CoAxioms and FamInsts are just like
77 DFunIds and ClsInsts
78
79 * A CoAxiom is a System-FC thing: it can relate any two types
80
81 * A FamInst is a Haskell source-language thing, corresponding
82 to a type/data family instance declaration.
83 - The FamInst contains a CoAxiom, which is the evidence
84 for the instance
85
86 - The LHS of the CoAxiom is always of form F ty1 .. tyn
87 where F is a type family
88 -}
89
90 data FamInst -- See Note [FamInsts and CoAxioms]
91 = FamInst { fi_axiom :: CoAxiom Unbranched -- The new coercion axiom
92 -- introduced by this family
93 -- instance
94 -- INVARIANT: apart from freshening (see below)
95 -- fi_tvs = cab_tvs of the (single) axiom branch
96 -- fi_cvs = cab_cvs ...ditto...
97 -- fi_tys = cab_lhs ...ditto...
98 -- fi_rhs = cab_rhs ...ditto...
99
100 , fi_flavor :: FamFlavor
101
102 -- Everything below here is a redundant,
103 -- cached version of the two things above
104 -- except that the TyVars are freshened
105 , fi_fam :: Name -- Family name
106
107 -- Used for "rough matching"; same idea as for class instances
108 -- See Note [Rough-match field] in InstEnv
109 , fi_tcs :: [Maybe Name] -- Top of type args
110 -- INVARIANT: fi_tcs = roughMatchTcs fi_tys
111
112 -- Used for "proper matching"; ditto
113 , fi_tvs :: [TyVar] -- Template tyvars for full match
114 , fi_cvs :: [CoVar] -- Template covars for full match
115 -- Like ClsInsts, these variables are always fresh
116 -- See Note [Template tyvars are fresh] in InstEnv
117
118 , fi_tys :: [Type] -- The LHS type patterns
119 -- May be eta-reduced; see Note [Eta reduction for data families]
120
121 , fi_rhs :: Type -- the RHS, with its freshened vars
122 }
123
124 data FamFlavor
125 = SynFamilyInst -- A synonym family
126 | DataFamilyInst TyCon -- A data family, with its representation TyCon
127
128 {-
129 Note [Arity of data families]
130 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
131 Data family instances might legitimately be over- or under-saturated.
132
133 Under-saturation has two potential causes:
134 U1) Eta reduction. See Note [Eta reduction for data families].
135 U2) When the user has specified a return kind instead of written out patterns.
136 Example:
137
138 data family Sing (a :: k)
139 data instance Sing :: Bool -> Type
140
141 The data family tycon Sing has an arity of 2, the k and the a. But
142 the data instance has only one pattern, Bool (standing in for k).
143 This instance is equivalent to `data instance Sing (a :: Bool)`, but
144 without the last pattern, we have an under-saturated data family instance.
145 On its own, this example is not compelling enough to add support for
146 under-saturation, but U1 makes this feature more compelling.
147
148 Over-saturation is also possible:
149 O1) If the data family's return kind is a type variable (see also #12369),
150 an instance might legitimately have more arguments than the family.
151 Example:
152
153 data family Fix :: (Type -> k) -> k
154 data instance Fix f = MkFix1 (f (Fix f))
155 data instance Fix f x = MkFix2 (f (Fix f x) x)
156
157 In the first instance here, the k in the data family kind is chosen to
158 be Type. In the second, it's (Type -> Type).
159
160 However, we require that any over-saturation is eta-reducible. That is,
161 we require that any extra patterns be bare unrepeated type variables;
162 see Note [Eta reduction for data families]. Accordingly, the FamInst
163 is never over-saturated.
164
165 Why can we allow such flexibility for data families but not for type families?
166 Because data families can be decomposed -- that is, they are generative and
167 injective. A Type family is neither and so always must be applied to all its
168 arguments.
169 -}
170
171 -- Obtain the axiom of a family instance
172 famInstAxiom :: FamInst -> CoAxiom Unbranched
173 famInstAxiom = fi_axiom
174
175 -- Split the left-hand side of the FamInst
176 famInstSplitLHS :: FamInst -> (TyCon, [Type])
177 famInstSplitLHS (FamInst { fi_axiom = axiom, fi_tys = lhs })
178 = (coAxiomTyCon axiom, lhs)
179
180 -- Get the RHS of the FamInst
181 famInstRHS :: FamInst -> Type
182 famInstRHS = fi_rhs
183
184 -- Get the family TyCon of the FamInst
185 famInstTyCon :: FamInst -> TyCon
186 famInstTyCon = coAxiomTyCon . famInstAxiom
187
188 -- Return the representation TyCons introduced by data family instances, if any
189 famInstsRepTyCons :: [FamInst] -> [TyCon]
190 famInstsRepTyCons fis = [tc | FamInst { fi_flavor = DataFamilyInst tc } <- fis]
191
192 -- Extracts the TyCon for this *data* (or newtype) instance
193 famInstRepTyCon_maybe :: FamInst -> Maybe TyCon
194 famInstRepTyCon_maybe fi
195 = case fi_flavor fi of
196 DataFamilyInst tycon -> Just tycon
197 SynFamilyInst -> Nothing
198
199 dataFamInstRepTyCon :: FamInst -> TyCon
200 dataFamInstRepTyCon fi
201 = case fi_flavor fi of
202 DataFamilyInst tycon -> tycon
203 SynFamilyInst -> pprPanic "dataFamInstRepTyCon" (ppr fi)
204
205 {-
206 ************************************************************************
207 * *
208 Pretty printing
209 * *
210 ************************************************************************
211 -}
212
213 instance NamedThing FamInst where
214 getName = coAxiomName . fi_axiom
215
216 instance Outputable FamInst where
217 ppr = pprFamInst
218
219 pprFamInst :: FamInst -> SDoc
220 -- Prints the FamInst as a family instance declaration
221 -- NB: This function, FamInstEnv.pprFamInst, is used only for internal,
222 -- debug printing. See PprTyThing.pprFamInst for printing for the user
223 pprFamInst (FamInst { fi_flavor = flavor, fi_axiom = ax
224 , fi_tvs = tvs, fi_tys = tys, fi_rhs = rhs })
225 = hang (ppr_tc_sort <+> text "instance"
226 <+> pprCoAxBranchUser (coAxiomTyCon ax) (coAxiomSingleBranch ax))
227 2 (whenPprDebug debug_stuff)
228 where
229 ppr_tc_sort = case flavor of
230 SynFamilyInst -> text "type"
231 DataFamilyInst tycon
232 | isDataTyCon tycon -> text "data"
233 | isNewTyCon tycon -> text "newtype"
234 | isAbstractTyCon tycon -> text "data"
235 | otherwise -> text "WEIRD" <+> ppr tycon
236
237 debug_stuff = vcat [ text "Coercion axiom:" <+> ppr ax
238 , text "Tvs:" <+> ppr tvs
239 , text "LHS:" <+> ppr tys
240 , text "RHS:" <+> ppr rhs ]
241
242 pprFamInsts :: [FamInst] -> SDoc
243 pprFamInsts finsts = vcat (map pprFamInst finsts)
244
245 {-
246 Note [Lazy axiom match]
247 ~~~~~~~~~~~~~~~~~~~~~~~
248 It is Vitally Important that mkImportedFamInst is *lazy* in its axiom
249 parameter. The axiom is loaded lazily, via a forkM, in TcIface. Sometime
250 later, mkImportedFamInst is called using that axiom. However, the axiom
251 may itself depend on entities which are not yet loaded as of the time
252 of the mkImportedFamInst. Thus, if mkImportedFamInst eagerly looks at the
253 axiom, a dependency loop spontaneously appears and GHC hangs. The solution
254 is simply for mkImportedFamInst never, ever to look inside of the axiom
255 until everything else is good and ready to do so. We can assume that this
256 readiness has been achieved when some other code pulls on the axiom in the
257 FamInst. Thus, we pattern match on the axiom lazily (in the where clause,
258 not in the parameter list) and we assert the consistency of names there
259 also.
260 -}
261
262 -- Make a family instance representation from the information found in an
263 -- interface file. In particular, we get the rough match info from the iface
264 -- (instead of computing it here).
265 mkImportedFamInst :: Name -- Name of the family
266 -> [Maybe Name] -- Rough match info
267 -> CoAxiom Unbranched -- Axiom introduced
268 -> FamInst -- Resulting family instance
269 mkImportedFamInst fam mb_tcs axiom
270 = FamInst {
271 fi_fam = fam,
272 fi_tcs = mb_tcs,
273 fi_tvs = tvs,
274 fi_cvs = cvs,
275 fi_tys = tys,
276 fi_rhs = rhs,
277 fi_axiom = axiom,
278 fi_flavor = flavor }
279 where
280 -- See Note [Lazy axiom match]
281 ~(CoAxBranch { cab_lhs = tys
282 , cab_tvs = tvs
283 , cab_cvs = cvs
284 , cab_rhs = rhs }) = coAxiomSingleBranch axiom
285
286 -- Derive the flavor for an imported FamInst rather disgustingly
287 -- Maybe we should store it in the IfaceFamInst?
288 flavor = case splitTyConApp_maybe rhs of
289 Just (tc, _)
290 | Just ax' <- tyConFamilyCoercion_maybe tc
291 , ax' == axiom
292 -> DataFamilyInst tc
293 _ -> SynFamilyInst
294
295 {-
296 ************************************************************************
297 * *
298 FamInstEnv
299 * *
300 ************************************************************************
301
302 Note [FamInstEnv]
303 ~~~~~~~~~~~~~~~~~
304 A FamInstEnv maps a family name to the list of known instances for that family.
305
306 The same FamInstEnv includes both 'data family' and 'type family' instances.
307 Type families are reduced during type inference, but not data families;
308 the user explains when to use a data family instance by using constructors
309 and pattern matching.
310
311 Nevertheless it is still useful to have data families in the FamInstEnv:
312
313 - For finding overlaps and conflicts
314
315 - For finding the representation type...see FamInstEnv.topNormaliseType
316 and its call site in Simplify
317
318 - In standalone deriving instance Eq (T [Int]) we need to find the
319 representation type for T [Int]
320
321 Note [Varying number of patterns for data family axioms]
322 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
323 For data families, the number of patterns may vary between instances.
324 For example
325 data family T a b
326 data instance T Int a = T1 a | T2
327 data instance T Bool [a] = T3 a
328
329 Then we get a data type for each instance, and an axiom:
330 data TInt a = T1 a | T2
331 data TBoolList a = T3 a
332
333 axiom ax7 :: T Int ~ TInt -- Eta-reduced
334 axiom ax8 a :: T Bool [a] ~ TBoolList a
335
336 These two axioms for T, one with one pattern, one with two;
337 see Note [Eta reduction for data families]
338
339 Note [FamInstEnv determinism]
340 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
341 We turn FamInstEnvs into a list in some places that don't directly affect
342 the ABI. That happens in family consistency checks and when producing output
343 for `:info`. Unfortunately that nondeterminism is nonlocal and it's hard
344 to tell what it affects without following a chain of functions. It's also
345 easy to accidentally make that nondeterminism affect the ABI. Furthermore
346 the envs should be relatively small, so it should be free to use deterministic
347 maps here. Testing with nofib and validate detected no difference between
348 UniqFM and UniqDFM.
349 See Note [Deterministic UniqFM].
350 -}
351
352 type FamInstEnv = UniqDFM FamilyInstEnv -- Maps a family to its instances
353 -- See Note [FamInstEnv]
354 -- See Note [FamInstEnv determinism]
355
356 type FamInstEnvs = (FamInstEnv, FamInstEnv)
357 -- External package inst-env, Home-package inst-env
358
359 newtype FamilyInstEnv
360 = FamIE [FamInst] -- The instances for a particular family, in any order
361
362 instance Outputable FamilyInstEnv where
363 ppr (FamIE fs) = text "FamIE" <+> vcat (map ppr fs)
364
365 -- INVARIANTS:
366 -- * The fs_tvs are distinct in each FamInst
367 -- of a range value of the map (so we can safely unify them)
368
369 emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
370 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
371
372 emptyFamInstEnv :: FamInstEnv
373 emptyFamInstEnv = emptyUDFM
374
375 famInstEnvElts :: FamInstEnv -> [FamInst]
376 famInstEnvElts fi = [elt | FamIE elts <- eltsUDFM fi, elt <- elts]
377 -- See Note [FamInstEnv determinism]
378
379 famInstEnvSize :: FamInstEnv -> Int
380 famInstEnvSize = nonDetFoldUDFM (\(FamIE elt) sum -> sum + length elt) 0
381 -- It's OK to use nonDetFoldUDFM here since we're just computing the
382 -- size.
383
384 familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
385 familyInstances (pkg_fie, home_fie) fam
386 = get home_fie ++ get pkg_fie
387 where
388 get env = case lookupUDFM env fam of
389 Just (FamIE insts) -> insts
390 Nothing -> []
391
392 extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
393 extendFamInstEnvList inst_env fis = foldl' extendFamInstEnv inst_env fis
394
395 extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
396 extendFamInstEnv inst_env
397 ins_item@(FamInst {fi_fam = cls_nm})
398 = addToUDFM_C add inst_env cls_nm (FamIE [ins_item])
399 where
400 add (FamIE items) _ = FamIE (ins_item:items)
401
402 {-
403 ************************************************************************
404 * *
405 Compatibility
406 * *
407 ************************************************************************
408
409 Note [Apartness]
410 ~~~~~~~~~~~~~~~~
411 In dealing with closed type families, we must be able to check that one type
412 will never reduce to another. This check is called /apartness/. The check
413 is always between a target (which may be an arbitrary type) and a pattern.
414 Here is how we do it:
415
416 apart(target, pattern) = not (unify(flatten(target), pattern))
417
418 where flatten (implemented in flattenTys, below) converts all type-family
419 applications into fresh variables. (See Note [Flattening].)
420
421 Note [Compatibility]
422 ~~~~~~~~~~~~~~~~~~~~
423 Two patterns are /compatible/ if either of the following conditions hold:
424 1) The patterns are apart.
425 2) The patterns unify with a substitution S, and their right hand sides
426 equal under that substitution.
427
428 For open type families, only compatible instances are allowed. For closed
429 type families, the story is slightly more complicated. Consider the following:
430
431 type family F a where
432 F Int = Bool
433 F a = Int
434
435 g :: Show a => a -> F a
436 g x = length (show x)
437
438 Should that type-check? No. We need to allow for the possibility that 'a'
439 might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int
440 only when we can be sure that 'a' is not Int.
441
442 To achieve this, after finding a possible match within the equations, we have to
443 go back to all previous equations and check that, under the
444 substitution induced by the match, other branches are surely apart. (See
445 Note [Apartness].) This is similar to what happens with class
446 instance selection, when we need to guarantee that there is only a match and
447 no unifiers. The exact algorithm is different here because the
448 potentially-overlapping group is closed.
449
450 As another example, consider this:
451
452 type family G x where
453 G Int = Bool
454 G a = Double
455
456 type family H y
457 -- no instances
458
459 Now, we want to simplify (G (H Char)). We can't, because (H Char) might later
460 simplify to be Int. So, (G (H Char)) is stuck, for now.
461
462 While everything above is quite sound, it isn't as expressive as we'd like.
463 Consider this:
464
465 type family J a where
466 J Int = Int
467 J a = a
468
469 Can we simplify (J b) to b? Sure we can. Yes, the first equation matches if
470 b is instantiated with Int, but the RHSs coincide there, so it's all OK.
471
472 So, the rule is this: when looking up a branch in a closed type family, we
473 find a branch that matches the target, but then we make sure that the target
474 is apart from every previous *incompatible* branch. We don't check the
475 branches that are compatible with the matching branch, because they are either
476 irrelevant (clause 1 of compatible) or benign (clause 2 of compatible).
477
478 Note [Compatibility of eta-reduced axioms]
479 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
480 In newtype instances of data families we eta-reduce the axioms,
481 See Note [Eta reduction for data families] in FamInstEnv. This means that
482 we sometimes need to test compatibility of two axioms that were eta-reduced to
483 different degrees, e.g.:
484
485
486 data family D a b c
487 newtype instance D a Int c = DInt (Maybe a)
488 -- D a Int ~ Maybe
489 -- lhs = [a, Int]
490 newtype instance D Bool Int Char = DIntChar Float
491 -- D Bool Int Char ~ Float
492 -- lhs = [Bool, Int, Char]
493
494 These are obviously incompatible. We could detect this by saturating
495 (eta-expanding) the shorter LHS with fresh tyvars until the lists are of
496 equal length, but instead we can just remove the tail of the longer list, as
497 those types will simply unify with the freshly introduced tyvars.
498
499 By doing this, in case the LHS are unifiable, the yielded substitution won't
500 mention the tyvars that appear in the tail we dropped off, and we might try
501 to test equality RHSes of different kinds, but that's fine since this case
502 occurs only for data families, where the RHS is a unique tycon and the equality
503 fails anyway.
504 -}
505
506 -- See Note [Compatibility]
507 compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
508 compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
509 (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
510 = let (commonlhs1, commonlhs2) = zipAndUnzip lhs1 lhs2
511 -- See Note [Compatibility of eta-reduced axioms]
512 in case tcUnifyTysFG (const BindMe) commonlhs1 commonlhs2 of
513 SurelyApart -> True
514 Unifiable subst
515 | Type.substTyAddInScope subst rhs1 `eqType`
516 Type.substTyAddInScope subst rhs2
517 -> True
518 _ -> False
519
520 -- | Result of testing two type family equations for injectiviy.
521 data InjectivityCheckResult
522 = InjectivityAccepted
523 -- ^ Either RHSs are distinct or unification of RHSs leads to unification of
524 -- LHSs
525 | InjectivityUnified CoAxBranch CoAxBranch
526 -- ^ RHSs unify but LHSs don't unify under that substitution. Relevant for
527 -- closed type families where equation after unification might be
528 -- overlpapped (in which case it is OK if they don't unify). Constructor
529 -- stores axioms after unification.
530
531 -- | Check whether two type family axioms don't violate injectivity annotation.
532 injectiveBranches :: [Bool] -> CoAxBranch -> CoAxBranch
533 -> InjectivityCheckResult
534 injectiveBranches injectivity
535 ax1@(CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
536 ax2@(CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
537 -- See Note [Verifying injectivity annotation]. This function implements first
538 -- check described there.
539 = let getInjArgs = filterByList injectivity
540 in case tcUnifyTyWithTFs True rhs1 rhs2 of -- True = two-way pre-unification
541 Nothing -> InjectivityAccepted -- RHS are different, so equations are
542 -- injective.
543 Just subst -> -- RHS unify under a substitution
544 let lhs1Subst = Type.substTys subst (getInjArgs lhs1)
545 lhs2Subst = Type.substTys subst (getInjArgs lhs2)
546 -- If LHSs are equal under the substitution used for RHSs then this pair
547 -- of equations does not violate injectivity annotation. If LHSs are not
548 -- equal under that substitution then this pair of equations violates
549 -- injectivity annotation, but for closed type families it still might
550 -- be the case that one LHS after substitution is unreachable.
551 in if eqTypes lhs1Subst lhs2Subst
552 then InjectivityAccepted
553 else InjectivityUnified ( ax1 { cab_lhs = Type.substTys subst lhs1
554 , cab_rhs = Type.substTy subst rhs1 })
555 ( ax2 { cab_lhs = Type.substTys subst lhs2
556 , cab_rhs = Type.substTy subst rhs2 })
557
558 -- takes a CoAxiom with unknown branch incompatibilities and computes
559 -- the compatibilities
560 -- See Note [Storing compatibility] in CoAxiom
561 computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch]
562 computeAxiomIncomps branches
563 = snd (mapAccumL go [] branches)
564 where
565 go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
566 go prev_brs cur_br
567 = (cur_br : prev_brs, new_br)
568 where
569 new_br = cur_br { cab_incomps = mk_incomps prev_brs cur_br }
570
571 mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch]
572 mk_incomps prev_brs cur_br
573 = filter (not . compatibleBranches cur_br) prev_brs
574
575 {-
576 ************************************************************************
577 * *
578 Constructing axioms
579 These functions are here because tidyType / tcUnifyTysFG
580 are not available in CoAxiom
581
582 Also computeAxiomIncomps is too sophisticated for CoAxiom
583 * *
584 ************************************************************************
585
586 Note [Tidy axioms when we build them]
587 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
588 Like types and classes, we build axioms fully quantified over all
589 their variables, and tidy them when we build them. For example,
590 we print out axioms and don't want to print stuff like
591 F k k a b = ...
592 Instead we must tidy those kind variables. See #7524.
593
594 We could instead tidy when we print, but that makes it harder to get
595 things like injectivity errors to come out right. Danger of
596 Type family equation violates injectivity annotation.
597 Kind variable ‘k’ cannot be inferred from the right-hand side.
598 In the type family equation:
599 PolyKindVars @[k1] @[k2] ('[] @k1) = '[] @k2
600
601 Note [Always number wildcard types in CoAxBranch]
602 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
603 Consider the following example (from the DataFamilyInstanceLHS test case):
604
605 data family Sing (a :: k)
606 data instance Sing (_ :: MyKind) where
607 SingA :: Sing A
608 SingB :: Sing B
609
610 If we're not careful during tidying, then when this program is compiled with
611 -ddump-types, we'll get the following information:
612
613 COERCION AXIOMS
614 axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 ::
615 Sing _ = DataFamilyInstanceLHS.R:SingMyKind_ _
616
617 It's misleading to have a wildcard type appearing on the RHS like
618 that. To avoid this issue, when building a CoAxiom (which is what eventually
619 gets printed above), we tidy all the variables in an env that already contains
620 '_'. Thus, any variable named '_' will be renamed, giving us the nicer output
621 here:
622
623 COERCION AXIOMS
624 axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 ::
625 Sing _1 = DataFamilyInstanceLHS.R:SingMyKind_ _1
626
627 Which is at least legal syntax.
628
629 See also Note [CoAxBranch type variables] in CoAxiom; note that we
630 are tidying (changing OccNames only), not freshening, in accordance with
631 that Note.
632 -}
633
634 -- all axiom roles are Nominal, as this is only used with type families
635 mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
636 -> [TyVar] -- Extra eta tyvars
637 -> [CoVar] -- possibly stale covars
638 -> [Type] -- LHS patterns
639 -> Type -- RHS
640 -> [Role]
641 -> SrcSpan
642 -> CoAxBranch
643 mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc
644 = CoAxBranch { cab_tvs = tvs'
645 , cab_eta_tvs = eta_tvs'
646 , cab_cvs = cvs'
647 , cab_lhs = tidyTypes env lhs
648 , cab_roles = roles
649 , cab_rhs = tidyType env rhs
650 , cab_loc = loc
651 , cab_incomps = placeHolderIncomps }
652 where
653 (env1, tvs') = tidyVarBndrs init_tidy_env tvs
654 (env2, eta_tvs') = tidyVarBndrs env1 eta_tvs
655 (env, cvs') = tidyVarBndrs env2 cvs
656 -- See Note [Tidy axioms when we build them]
657 -- See also Note [CoAxBranch type variables] in CoAxiom
658
659 init_occ_env = initTidyOccEnv [mkTyVarOcc "_"]
660 init_tidy_env = mkEmptyTidyEnv init_occ_env
661 -- See Note [Always number wildcard types in CoAxBranch]
662
663 -- all of the following code is here to avoid mutual dependencies with
664 -- Coercion
665 mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
666 mkBranchedCoAxiom ax_name fam_tc branches
667 = CoAxiom { co_ax_unique = nameUnique ax_name
668 , co_ax_name = ax_name
669 , co_ax_tc = fam_tc
670 , co_ax_role = Nominal
671 , co_ax_implicit = False
672 , co_ax_branches = manyBranches (computeAxiomIncomps branches) }
673
674 mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched
675 mkUnbranchedCoAxiom ax_name fam_tc branch
676 = CoAxiom { co_ax_unique = nameUnique ax_name
677 , co_ax_name = ax_name
678 , co_ax_tc = fam_tc
679 , co_ax_role = Nominal
680 , co_ax_implicit = False
681 , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
682
683 mkSingleCoAxiom :: Role -> Name
684 -> [TyVar] -> [TyVar] -> [CoVar]
685 -> TyCon -> [Type] -> Type
686 -> CoAxiom Unbranched
687 -- Make a single-branch CoAxiom, incluidng making the branch itself
688 -- Used for both type family (Nominal) and data family (Representational)
689 -- axioms, hence passing in the Role
690 mkSingleCoAxiom role ax_name tvs eta_tvs cvs fam_tc lhs_tys rhs_ty
691 = CoAxiom { co_ax_unique = nameUnique ax_name
692 , co_ax_name = ax_name
693 , co_ax_tc = fam_tc
694 , co_ax_role = role
695 , co_ax_implicit = False
696 , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
697 where
698 branch = mkCoAxBranch tvs eta_tvs cvs lhs_tys rhs_ty
699 (map (const Nominal) tvs)
700 (getSrcSpan ax_name)
701
702 -- | Create a coercion constructor (axiom) suitable for the given
703 -- newtype 'TyCon'. The 'Name' should be that of a new coercion
704 -- 'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and
705 -- the type the appropriate right hand side of the @newtype@, with
706 -- the free variables a subset of those 'TyVar's.
707 mkNewTypeCoAxiom :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched
708 mkNewTypeCoAxiom name tycon tvs roles rhs_ty
709 = CoAxiom { co_ax_unique = nameUnique name
710 , co_ax_name = name
711 , co_ax_implicit = True -- See Note [Implicit axioms] in TyCon
712 , co_ax_role = Representational
713 , co_ax_tc = tycon
714 , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
715 where
716 branch = mkCoAxBranch tvs [] [] (mkTyVarTys tvs) rhs_ty
717 roles (getSrcSpan name)
718
719 {-
720 ************************************************************************
721 * *
722 Looking up a family instance
723 * *
724 ************************************************************************
725
726 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
727 Multiple matches are only possible in case of type families (not data
728 families), and then, it doesn't matter which match we choose (as the
729 instances are guaranteed confluent).
730
731 We return the matching family instances and the type instance at which it
732 matches. For example, if we lookup 'T [Int]' and have a family instance
733
734 data instance T [a] = ..
735
736 desugared to
737
738 data :R42T a = ..
739 coe :Co:R42T a :: T [a] ~ :R42T a
740
741 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
742 -}
743
744 -- when matching a type family application, we get a FamInst,
745 -- and the list of types the axiom should be applied to
746 data FamInstMatch = FamInstMatch { fim_instance :: FamInst
747 , fim_tys :: [Type]
748 , fim_cos :: [Coercion]
749 }
750 -- See Note [Over-saturated matches]
751
752 instance Outputable FamInstMatch where
753 ppr (FamInstMatch { fim_instance = inst
754 , fim_tys = tys
755 , fim_cos = cos })
756 = text "match with" <+> parens (ppr inst) <+> ppr tys <+> ppr cos
757
758 lookupFamInstEnvByTyCon :: FamInstEnvs -> TyCon -> [FamInst]
759 lookupFamInstEnvByTyCon (pkg_ie, home_ie) fam_tc
760 = get pkg_ie ++ get home_ie
761 where
762 get ie = case lookupUDFM ie fam_tc of
763 Nothing -> []
764 Just (FamIE fis) -> fis
765
766 lookupFamInstEnv
767 :: FamInstEnvs
768 -> TyCon -> [Type] -- What we are looking for
769 -> [FamInstMatch] -- Successful matches
770 -- Precondition: the tycon is saturated (or over-saturated)
771
772 lookupFamInstEnv
773 = lookup_fam_inst_env match
774 where
775 match _ _ tpl_tys tys = tcMatchTys tpl_tys tys
776
777 lookupFamInstEnvConflicts
778 :: FamInstEnvs
779 -> FamInst -- Putative new instance
780 -> [FamInstMatch] -- Conflicting matches (don't look at the fim_tys field)
781 -- E.g. when we are about to add
782 -- f : type instance F [a] = a->a
783 -- we do (lookupFamInstConflicts f [b])
784 -- to find conflicting matches
785 --
786 -- Precondition: the tycon is saturated (or over-saturated)
787
788 lookupFamInstEnvConflicts envs fam_inst@(FamInst { fi_axiom = new_axiom })
789 = lookup_fam_inst_env my_unify envs fam tys
790 where
791 (fam, tys) = famInstSplitLHS fam_inst
792 -- In example above, fam tys' = F [b]
793
794 my_unify (FamInst { fi_axiom = old_axiom }) tpl_tvs tpl_tys _
795 = ASSERT2( tyCoVarsOfTypes tys `disjointVarSet` tpl_tvs,
796 (ppr fam <+> ppr tys) $$
797 (ppr tpl_tvs <+> ppr tpl_tys) )
798 -- Unification will break badly if the variables overlap
799 -- They shouldn't because we allocate separate uniques for them
800 if compatibleBranches (coAxiomSingleBranch old_axiom) new_branch
801 then Nothing
802 else Just noSubst
803 -- Note [Family instance overlap conflicts]
804
805 noSubst = panic "lookupFamInstEnvConflicts noSubst"
806 new_branch = coAxiomSingleBranch new_axiom
807
808 --------------------------------------------------------------------------------
809 -- Type family injectivity checking bits --
810 --------------------------------------------------------------------------------
811
812 {- Note [Verifying injectivity annotation]
813 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
814
815 Injectivity means that the RHS of a type family uniquely determines the LHS (see
816 Note [Type inference for type families with injectivity]). User informs about
817 injectivity using an injectivity annotation and it is GHC's task to verify that
818 that annotation is correct wrt. to type family equations. Whenever we see a new
819 equation of a type family we need to make sure that adding this equation to
820 already known equations of a type family does not violate injectivity annotation
821 supplied by the user (see Note [Injectivity annotation]). Of course if the type
822 family has no injectivity annotation then no check is required. But if a type
823 family has injectivity annotation we need to make sure that the following
824 conditions hold:
825
826 1. For each pair of *different* equations of a type family, one of the following
827 conditions holds:
828
829 A: RHSs are different.
830
831 B1: OPEN TYPE FAMILIES: If the RHSs can be unified under some substitution
832 then it must be possible to unify the LHSs under the same substitution.
833 Example:
834
835 type family FunnyId a = r | r -> a
836 type instance FunnyId Int = Int
837 type instance FunnyId a = a
838
839 RHSs of these two equations unify under [ a |-> Int ] substitution.
840 Under this substitution LHSs are equal therefore these equations don't
841 violate injectivity annotation.
842
843 B2: CLOSED TYPE FAMILIES: If the RHSs can be unified under some
844 substitution then either the LHSs unify under the same substitution or
845 the LHS of the latter equation is overlapped by earlier equations.
846 Example 1:
847
848 type family SwapIntChar a = r | r -> a where
849 SwapIntChar Int = Char
850 SwapIntChar Char = Int
851 SwapIntChar a = a
852
853 Say we are checking the last two equations. RHSs unify under [ a |->
854 Int ] substitution but LHSs don't. So we apply the substitution to LHS
855 of last equation and check whether it is overlapped by any of previous
856 equations. Since it is overlapped by the first equation we conclude
857 that pair of last two equations does not violate injectivity
858 annotation.
859
860 A special case of B is when RHSs unify with an empty substitution ie. they
861 are identical.
862
863 If any of the above two conditions holds we conclude that the pair of
864 equations does not violate injectivity annotation. But if we find a pair
865 of equations where neither of the above holds we report that this pair
866 violates injectivity annotation because for a given RHS we don't have a
867 unique LHS. (Note that (B) actually implies (A).)
868
869 Note that we only take into account these LHS patterns that were declared
870 as injective.
871
872 2. If a RHS of a type family equation is a bare type variable then
873 all LHS variables (including implicit kind variables) also have to be bare.
874 In other words, this has to be a sole equation of that type family and it has
875 to cover all possible patterns. So for example this definition will be
876 rejected:
877
878 type family W1 a = r | r -> a
879 type instance W1 [a] = a
880
881 If it were accepted we could call `W1 [W1 Int]`, which would reduce to
882 `W1 Int` and then by injectivity we could conclude that `[W1 Int] ~ Int`,
883 which is bogus.
884
885 3. If a RHS of a type family equation is a type family application then the type
886 family is rejected as not injective.
887
888 4. If a LHS type variable that is declared as injective is not mentioned on
889 injective position in the RHS then the type family is rejected as not
890 injective. "Injective position" means either an argument to a type
891 constructor or argument to a type family on injective position.
892
893 See also Note [Injective type families] in TyCon
894 -}
895
896
897 -- | Check whether an open type family equation can be added to already existing
898 -- instance environment without causing conflicts with supplied injectivity
899 -- annotations. Returns list of conflicting axioms (type instance
900 -- declarations).
901 lookupFamInstEnvInjectivityConflicts
902 :: [Bool] -- injectivity annotation for this type family instance
903 -- INVARIANT: list contains at least one True value
904 -> FamInstEnvs -- all type instances seens so far
905 -> FamInst -- new type instance that we're checking
906 -> [CoAxBranch] -- conflicting instance declarations
907 lookupFamInstEnvInjectivityConflicts injList (pkg_ie, home_ie)
908 fam_inst@(FamInst { fi_axiom = new_axiom })
909 -- See Note [Verifying injectivity annotation]. This function implements
910 -- check (1.B1) for open type families described there.
911 = lookup_inj_fam_conflicts home_ie ++ lookup_inj_fam_conflicts pkg_ie
912 where
913 fam = famInstTyCon fam_inst
914 new_branch = coAxiomSingleBranch new_axiom
915
916 -- filtering function used by `lookup_inj_fam_conflicts` to check whether
917 -- a pair of equations conflicts with the injectivity annotation.
918 isInjConflict (FamInst { fi_axiom = old_axiom })
919 | InjectivityAccepted <-
920 injectiveBranches injList (coAxiomSingleBranch old_axiom) new_branch
921 = False -- no conflict
922 | otherwise = True
923
924 lookup_inj_fam_conflicts ie
925 | isOpenFamilyTyCon fam, Just (FamIE insts) <- lookupUDFM ie fam
926 = map (coAxiomSingleBranch . fi_axiom) $
927 filter isInjConflict insts
928 | otherwise = []
929
930
931 --------------------------------------------------------------------------------
932 -- Type family overlap checking bits --
933 --------------------------------------------------------------------------------
934
935 {-
936 Note [Family instance overlap conflicts]
937 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
938 - In the case of data family instances, any overlap is fundamentally a
939 conflict (as these instances imply injective type mappings).
940
941 - In the case of type family instances, overlap is admitted as long as
942 the right-hand sides of the overlapping rules coincide under the
943 overlap substitution. eg
944 type instance F a Int = a
945 type instance F Int b = b
946 These two overlap on (F Int Int) but then both RHSs are Int,
947 so all is well. We require that they are syntactically equal;
948 anything else would be difficult to test for at this stage.
949 -}
950
951 ------------------------------------------------------------
952 -- Might be a one-way match or a unifier
953 type MatchFun = FamInst -- The FamInst template
954 -> TyVarSet -> [Type] -- fi_tvs, fi_tys of that FamInst
955 -> [Type] -- Target to match against
956 -> Maybe TCvSubst
957
958 lookup_fam_inst_env' -- The worker, local to this module
959 :: MatchFun
960 -> FamInstEnv
961 -> TyCon -> [Type] -- What we are looking for
962 -> [FamInstMatch]
963 lookup_fam_inst_env' match_fun ie fam match_tys
964 | isOpenFamilyTyCon fam
965 , Just (FamIE insts) <- lookupUDFM ie fam
966 = find insts -- The common case
967 | otherwise = []
968 where
969
970 find [] = []
971 find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs, fi_cvs = tpl_cvs
972 , fi_tys = tpl_tys }) : rest)
973 -- Fast check for no match, uses the "rough match" fields
974 | instanceCantMatch rough_tcs mb_tcs
975 = find rest
976
977 -- Proper check
978 | Just subst <- match_fun item (mkVarSet tpl_tvs) tpl_tys match_tys1
979 = (FamInstMatch { fim_instance = item
980 , fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2
981 , fim_cos = ASSERT( all (isJust . lookupCoVar subst) tpl_cvs )
982 substCoVars subst tpl_cvs
983 })
984 : find rest
985
986 -- No match => try next
987 | otherwise
988 = find rest
989 where
990 (rough_tcs, match_tys1, match_tys2) = split_tys tpl_tys
991
992 -- Precondition: the tycon is saturated (or over-saturated)
993
994 -- Deal with over-saturation
995 -- See Note [Over-saturated matches]
996 split_tys tpl_tys
997 | isTypeFamilyTyCon fam
998 = pre_rough_split_tys
999
1000 | otherwise
1001 = let (match_tys1, match_tys2) = splitAtList tpl_tys match_tys
1002 rough_tcs = roughMatchTcs match_tys1
1003 in (rough_tcs, match_tys1, match_tys2)
1004
1005 (pre_match_tys1, pre_match_tys2) = splitAt (tyConArity fam) match_tys
1006 pre_rough_split_tys
1007 = (roughMatchTcs pre_match_tys1, pre_match_tys1, pre_match_tys2)
1008
1009 lookup_fam_inst_env -- The worker, local to this module
1010 :: MatchFun
1011 -> FamInstEnvs
1012 -> TyCon -> [Type] -- What we are looking for
1013 -> [FamInstMatch] -- Successful matches
1014
1015 -- Precondition: the tycon is saturated (or over-saturated)
1016
1017 lookup_fam_inst_env match_fun (pkg_ie, home_ie) fam tys
1018 = lookup_fam_inst_env' match_fun home_ie fam tys
1019 ++ lookup_fam_inst_env' match_fun pkg_ie fam tys
1020
1021 {-
1022 Note [Over-saturated matches]
1023 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1024 It's ok to look up an over-saturated type constructor. E.g.
1025 type family F a :: * -> *
1026 type instance F (a,b) = Either (a->b)
1027
1028 The type instance gives rise to a newtype TyCon (at a higher kind
1029 which you can't do in Haskell!):
1030 newtype FPair a b = FP (Either (a->b))
1031
1032 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
1033 (FPair, [Int,Bool,Char])
1034 The "extra" type argument [Char] just stays on the end.
1035
1036 We handle data families and type families separately here:
1037
1038 * For type families, all instances of a type family must have the
1039 same arity, so we can precompute the split between the match_tys
1040 and the overflow tys. This is done in pre_rough_split_tys.
1041
1042 * For data family instances, though, we need to re-split for each
1043 instance, because the breakdown might be different for each
1044 instance. Why? Because of eta reduction; see
1045 Note [Eta reduction for data families].
1046 -}
1047
1048 -- checks if one LHS is dominated by a list of other branches
1049 -- in other words, if an application would match the first LHS, it is guaranteed
1050 -- to match at least one of the others. The RHSs are ignored.
1051 -- This algorithm is conservative:
1052 -- True -> the LHS is definitely covered by the others
1053 -- False -> no information
1054 -- It is currently (Oct 2012) used only for generating errors for
1055 -- inaccessible branches. If these errors go unreported, no harm done.
1056 -- This is defined here to avoid a dependency from CoAxiom to Unify
1057 isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool
1058 isDominatedBy branch branches
1059 = or $ map match branches
1060 where
1061 lhs = coAxBranchLHS branch
1062 match (CoAxBranch { cab_lhs = tys })
1063 = isJust $ tcMatchTys tys lhs
1064
1065 {-
1066 ************************************************************************
1067 * *
1068 Choosing an axiom application
1069 * *
1070 ************************************************************************
1071
1072 The lookupFamInstEnv function does a nice job for *open* type families,
1073 but we also need to handle closed ones when normalising a type:
1074 -}
1075
1076 reduceTyFamApp_maybe :: FamInstEnvs
1077 -> Role -- Desired role of result coercion
1078 -> TyCon -> [Type]
1079 -> Maybe (Coercion, Type)
1080 -- Attempt to do a *one-step* reduction of a type-family application
1081 -- but *not* newtypes
1082 -- Works on type-synonym families always; data-families only if
1083 -- the role we seek is representational
1084 -- It does *not* normlise the type arguments first, so this may not
1085 -- go as far as you want. If you want normalised type arguments,
1086 -- use normaliseTcArgs first.
1087 --
1088 -- The TyCon can be oversaturated.
1089 -- Works on both open and closed families
1090 --
1091 -- Always returns a *homogeneous* coercion -- type family reductions are always
1092 -- homogeneous
1093 reduceTyFamApp_maybe envs role tc tys
1094 | Phantom <- role
1095 = Nothing
1096
1097 | case role of
1098 Representational -> isOpenFamilyTyCon tc
1099 _ -> isOpenTypeFamilyTyCon tc
1100 -- If we seek a representational coercion
1101 -- (e.g. the call in topNormaliseType_maybe) then we can
1102 -- unwrap data families as well as type-synonym families;
1103 -- otherwise only type-synonym families
1104 , FamInstMatch { fim_instance = FamInst { fi_axiom = ax }
1105 , fim_tys = inst_tys
1106 , fim_cos = inst_cos } : _ <- lookupFamInstEnv envs tc tys
1107 -- NB: Allow multiple matches because of compatible overlap
1108
1109 = let co = mkUnbranchedAxInstCo role ax inst_tys inst_cos
1110 ty = pSnd (coercionKind co)
1111 in Just (co, ty)
1112
1113 | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe tc
1114 , Just (ind, inst_tys, inst_cos) <- chooseBranch ax tys
1115 = let co = mkAxInstCo role ax ind inst_tys inst_cos
1116 ty = pSnd (coercionKind co)
1117 in Just (co, ty)
1118
1119 | Just ax <- isBuiltInSynFamTyCon_maybe tc
1120 , Just (coax,ts,ty) <- sfMatchFam ax tys
1121 = let co = mkAxiomRuleCo coax (zipWith mkReflCo (coaxrAsmpRoles coax) ts)
1122 in Just (co, ty)
1123
1124 | otherwise
1125 = Nothing
1126
1127 -- The axiom can be oversaturated. (Closed families only.)
1128 chooseBranch :: CoAxiom Branched -> [Type]
1129 -> Maybe (BranchIndex, [Type], [Coercion]) -- found match, with args
1130 chooseBranch axiom tys
1131 = do { let num_pats = coAxiomNumPats axiom
1132 (target_tys, extra_tys) = splitAt num_pats tys
1133 branches = coAxiomBranches axiom
1134 ; (ind, inst_tys, inst_cos)
1135 <- findBranch (unMkBranches branches) target_tys
1136 ; return ( ind, inst_tys `chkAppend` extra_tys, inst_cos ) }
1137
1138 -- The axiom must *not* be oversaturated
1139 findBranch :: Array BranchIndex CoAxBranch
1140 -> [Type]
1141 -> Maybe (BranchIndex, [Type], [Coercion])
1142 -- coercions relate requested types to returned axiom LHS at role N
1143 findBranch branches target_tys
1144 = foldr go Nothing (assocs branches)
1145 where
1146 go :: (BranchIndex, CoAxBranch)
1147 -> Maybe (BranchIndex, [Type], [Coercion])
1148 -> Maybe (BranchIndex, [Type], [Coercion])
1149 go (index, branch) other
1150 = let (CoAxBranch { cab_tvs = tpl_tvs, cab_cvs = tpl_cvs
1151 , cab_lhs = tpl_lhs
1152 , cab_incomps = incomps }) = branch
1153 in_scope = mkInScopeSet (unionVarSets $
1154 map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
1155 -- See Note [Flattening] below
1156 flattened_target = flattenTys in_scope target_tys
1157 in case tcMatchTys tpl_lhs target_tys of
1158 Just subst -- matching worked. now, check for apartness.
1159 | apartnessCheck flattened_target branch
1160 -> -- matching worked & we're apart from all incompatible branches.
1161 -- success
1162 ASSERT( all (isJust . lookupCoVar subst) tpl_cvs )
1163 Just (index, substTyVars subst tpl_tvs, substCoVars subst tpl_cvs)
1164
1165 -- failure. keep looking
1166 _ -> other
1167
1168 -- | Do an apartness check, as described in the "Closed Type Families" paper
1169 -- (POPL '14). This should be used when determining if an equation
1170 -- ('CoAxBranch') of a closed type family can be used to reduce a certain target
1171 -- type family application.
1172 apartnessCheck :: [Type] -- ^ /flattened/ target arguments. Make sure
1173 -- they're flattened! See Note [Flattening].
1174 -- (NB: This "flat" is a different
1175 -- "flat" than is used in TcFlatten.)
1176 -> CoAxBranch -- ^ the candidate equation we wish to use
1177 -- Precondition: this matches the target
1178 -> Bool -- ^ True <=> equation can fire
1179 apartnessCheck flattened_target (CoAxBranch { cab_incomps = incomps })
1180 = all (isSurelyApart
1181 . tcUnifyTysFG (const BindMe) flattened_target
1182 . coAxBranchLHS) incomps
1183 where
1184 isSurelyApart SurelyApart = True
1185 isSurelyApart _ = False
1186
1187 {-
1188 ************************************************************************
1189 * *
1190 Looking up a family instance
1191 * *
1192 ************************************************************************
1193
1194 Note [Normalising types]
1195 ~~~~~~~~~~~~~~~~~~~~~~~~
1196 The topNormaliseType function removes all occurrences of type families
1197 and newtypes from the top-level structure of a type. normaliseTcApp does
1198 the type family lookup and is fairly straightforward. normaliseType is
1199 a little more involved.
1200
1201 The complication comes from the fact that a type family might be used in the
1202 kind of a variable bound in a forall. We wish to remove this type family
1203 application, but that means coming up with a fresh variable (with the new
1204 kind). Thus, we need a substitution to be built up as we recur through the
1205 type. However, an ordinary TCvSubst just won't do: when we hit a type variable
1206 whose kind has changed during normalisation, we need both the new type
1207 variable *and* the coercion. We could conjure up a new VarEnv with just this
1208 property, but a usable substitution environment already exists:
1209 LiftingContexts from the liftCoSubst family of functions, defined in Coercion.
1210 A LiftingContext maps a type variable to a coercion and a coercion variable to
1211 a pair of coercions. Let's ignore coercion variables for now. Because the
1212 coercion a type variable maps to contains the destination type (via
1213 coercionKind), we don't need to store that destination type separately. Thus,
1214 a LiftingContext has what we need: a map from type variables to (Coercion,
1215 Type) pairs.
1216
1217 We also benefit because we can piggyback on the liftCoSubstVarBndr function to
1218 deal with binders. However, I had to modify that function to work with this
1219 application. Thus, we now have liftCoSubstVarBndrUsing, which takes
1220 a function used to process the kind of the binder. We don't wish
1221 to lift the kind, but instead normalise it. So, we pass in a callback function
1222 that processes the kind of the binder.
1223
1224 After that brilliant explanation of all this, I'm sure you've forgotten the
1225 dangling reference to coercion variables. What do we do with those? Nothing at
1226 all. The point of normalising types is to remove type family applications, but
1227 there's no sense in removing these from coercions. We would just get back a
1228 new coercion witnessing the equality between the same types as the original
1229 coercion. Because coercions are irrelevant anyway, there is no point in doing
1230 this. So, whenever we encounter a coercion, we just say that it won't change.
1231 That's what the CoercionTy case is doing within normalise_type.
1232
1233 Note [Normalisation and type synonyms]
1234 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1235 We need to be a bit careful about normalising in the presence of type
1236 synonyms (#13035). Suppose S is a type synonym, and we have
1237 S t1 t2
1238 If S is family-free (on its RHS) we can just normalise t1 and t2 and
1239 reconstruct (S t1' t2'). Expanding S could not reveal any new redexes
1240 because type families are saturated.
1241
1242 But if S has a type family on its RHS we expand /before/ normalising
1243 the args t1, t2. If we normalise t1, t2 first, we'll re-normalise them
1244 after expansion, and that can lead to /exponential/ behavour; see #13035.
1245
1246 Notice, though, that expanding first can in principle duplicate t1,t2,
1247 which might contain redexes. I'm sure you could conjure up an exponential
1248 case by that route too, but it hasn't happened in practice yet!
1249 -}
1250
1251 topNormaliseType :: FamInstEnvs -> Type -> Type
1252 topNormaliseType env ty = case topNormaliseType_maybe env ty of
1253 Just (_co, ty') -> ty'
1254 Nothing -> ty
1255
1256 topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Coercion, Type)
1257
1258 -- ^ Get rid of *outermost* (or toplevel)
1259 -- * type function redex
1260 -- * data family redex
1261 -- * newtypes
1262 -- returning an appropriate Representational coercion. Specifically, if
1263 -- topNormaliseType_maybe env ty = Just (co, ty')
1264 -- then
1265 -- (a) co :: ty ~R ty'
1266 -- (b) ty' is not a newtype, and is not a type-family or data-family redex
1267 --
1268 -- However, ty' can be something like (Maybe (F ty)), where
1269 -- (F ty) is a redex.
1270 --
1271 -- Always operates homogeneously: the returned type has the same kind as the
1272 -- original type, and the returned coercion is always homogeneous.
1273 topNormaliseType_maybe env ty
1274 = do { ((co, mkind_co), nty) <- topNormaliseTypeX stepper combine ty
1275 ; return $ case mkind_co of
1276 MRefl -> (co, nty)
1277 MCo kind_co -> let nty_casted = nty `mkCastTy` mkSymCo kind_co
1278 final_co = mkCoherenceRightCo Representational nty
1279 (mkSymCo kind_co) co
1280 in (final_co, nty_casted) }
1281 where
1282 stepper = unwrapNewTypeStepper' `composeSteppers` tyFamStepper
1283
1284 combine (c1, mc1) (c2, mc2) = (c1 `mkTransCo` c2, mc1 `mkTransMCo` mc2)
1285
1286 unwrapNewTypeStepper' :: NormaliseStepper (Coercion, MCoercionN)
1287 unwrapNewTypeStepper' rec_nts tc tys
1288 = mapStepResult (, MRefl) $ unwrapNewTypeStepper rec_nts tc tys
1289
1290 -- second coercion below is the kind coercion relating the original type's kind
1291 -- to the normalised type's kind
1292 tyFamStepper :: NormaliseStepper (Coercion, MCoercionN)
1293 tyFamStepper rec_nts tc tys -- Try to step a type/data family
1294 = let (args_co, ntys, res_co) = normaliseTcArgs env Representational tc tys in
1295 case reduceTyFamApp_maybe env Representational tc ntys of
1296 Just (co, rhs) -> NS_Step rec_nts rhs (args_co `mkTransCo` co, MCo res_co)
1297 _ -> NS_Done
1298
1299 ---------------
1300 normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> (Coercion, Type)
1301 -- See comments on normaliseType for the arguments of this function
1302 normaliseTcApp env role tc tys
1303 = initNormM env role (tyCoVarsOfTypes tys) $
1304 normalise_tc_app tc tys
1305
1306 -- See Note [Normalising types] about the LiftingContext
1307 normalise_tc_app :: TyCon -> [Type] -> NormM (Coercion, Type)
1308 normalise_tc_app tc tys
1309 | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
1310 , not (isFamFreeTyCon tc) -- Expand and try again
1311 = -- A synonym with type families in the RHS
1312 -- Expand and try again
1313 -- See Note [Normalisation and type synonyms]
1314 normalise_type (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
1315
1316 | isFamilyTyCon tc
1317 = -- A type-family application
1318 do { env <- getEnv
1319 ; role <- getRole
1320 ; (args_co, ntys, res_co) <- normalise_tc_args tc tys
1321 ; case reduceTyFamApp_maybe env role tc ntys of
1322 Just (first_co, ty')
1323 -> do { (rest_co,nty) <- normalise_type ty'
1324 ; return (assemble_result role nty
1325 (args_co `mkTransCo` first_co `mkTransCo` rest_co)
1326 res_co) }
1327 _ -> -- No unique matching family instance exists;
1328 -- we do not do anything
1329 return (assemble_result role (mkTyConApp tc ntys) args_co res_co) }
1330
1331 | otherwise
1332 = -- A synonym with no type families in the RHS; or data type etc
1333 -- Just normalise the arguments and rebuild
1334 do { (args_co, ntys, res_co) <- normalise_tc_args tc tys
1335 ; role <- getRole
1336 ; return (assemble_result role (mkTyConApp tc ntys) args_co res_co) }
1337
1338 where
1339 assemble_result :: Role -- r, ambient role in NormM monad
1340 -> Type -- nty, result type, possibly of changed kind
1341 -> Coercion -- orig_ty ~r nty, possibly heterogeneous
1342 -> CoercionN -- typeKind(orig_ty) ~N typeKind(nty)
1343 -> (Coercion, Type) -- (co :: orig_ty ~r nty_casted, nty_casted)
1344 -- where nty_casted has same kind as orig_ty
1345 assemble_result r nty orig_to_nty kind_co
1346 = ( final_co, nty_old_kind )
1347 where
1348 nty_old_kind = nty `mkCastTy` mkSymCo kind_co
1349 final_co = mkCoherenceRightCo r nty (mkSymCo kind_co) orig_to_nty
1350
1351 ---------------
1352 -- | Normalise arguments to a tycon
1353 normaliseTcArgs :: FamInstEnvs -- ^ env't with family instances
1354 -> Role -- ^ desired role of output coercion
1355 -> TyCon -- ^ tc
1356 -> [Type] -- ^ tys
1357 -> (Coercion, [Type], CoercionN)
1358 -- ^ co :: tc tys ~ tc new_tys
1359 -- NB: co might not be homogeneous
1360 -- last coercion :: kind(tc tys) ~ kind(tc new_tys)
1361 normaliseTcArgs env role tc tys
1362 = initNormM env role (tyCoVarsOfTypes tys) $
1363 normalise_tc_args tc tys
1364
1365 normalise_tc_args :: TyCon -> [Type] -- tc tys
1366 -> NormM (Coercion, [Type], CoercionN)
1367 -- (co, new_tys), where
1368 -- co :: tc tys ~ tc new_tys; might not be homogeneous
1369 -- res_co :: typeKind(tc tys) ~N typeKind(tc new_tys)
1370 normalise_tc_args tc tys
1371 = do { role <- getRole
1372 ; (args_cos, nargs, res_co) <- normalise_args (tyConKind tc) (tyConRolesX role tc) tys
1373 ; return (mkTyConAppCo role tc args_cos, nargs, res_co) }
1374
1375 ---------------
1376 normaliseType :: FamInstEnvs
1377 -> Role -- desired role of coercion
1378 -> Type -> (Coercion, Type)
1379 normaliseType env role ty
1380 = initNormM env role (tyCoVarsOfType ty) $ normalise_type ty
1381
1382 normalise_type :: Type -- old type
1383 -> NormM (Coercion, Type) -- (coercion, new type), where
1384 -- co :: old-type ~ new_type
1385 -- Normalise the input type, by eliminating *all* type-function redexes
1386 -- but *not* newtypes (which are visible to the programmer)
1387 -- Returns with Refl if nothing happens
1388 -- Does nothing to newtypes
1389 -- The returned coercion *must* be *homogeneous*
1390 -- See Note [Normalising types]
1391 -- Try not to disturb type synonyms if possible
1392
1393 normalise_type ty
1394 = go ty
1395 where
1396 go (TyConApp tc tys) = normalise_tc_app tc tys
1397 go ty@(LitTy {}) = do { r <- getRole
1398 ; return (mkReflCo r ty, ty) }
1399
1400 go (AppTy ty1 ty2) = go_app_tys ty1 [ty2]
1401
1402 go ty@(FunTy { ft_arg = ty1, ft_res = ty2 })
1403 = do { (co1, nty1) <- go ty1
1404 ; (co2, nty2) <- go ty2
1405 ; r <- getRole
1406 ; return (mkFunCo r co1 co2, ty { ft_arg = nty1, ft_res = nty2 }) }
1407 go (ForAllTy (Bndr tcvar vis) ty)
1408 = do { (lc', tv', h, ki') <- normalise_var_bndr tcvar
1409 ; (co, nty) <- withLC lc' $ normalise_type ty
1410 ; let tv2 = setTyVarKind tv' ki'
1411 ; return (mkForAllCo tv' h co, ForAllTy (Bndr tv2 vis) nty) }
1412 go (TyVarTy tv) = normalise_tyvar tv
1413 go (CastTy ty co)
1414 = do { (nco, nty) <- go ty
1415 ; lc <- getLC
1416 ; let co' = substRightCo lc co
1417 ; return (castCoercionKind nco Nominal ty nty co co'
1418 , mkCastTy nty co') }
1419 go (CoercionTy co)
1420 = do { lc <- getLC
1421 ; r <- getRole
1422 ; let right_co = substRightCo lc co
1423 ; return ( mkProofIrrelCo r
1424 (liftCoSubst Nominal lc (coercionType co))
1425 co right_co
1426 , mkCoercionTy right_co ) }
1427
1428 go_app_tys :: Type -- function
1429 -> [Type] -- args
1430 -> NormM (Coercion, Type)
1431 -- cf. TcFlatten.flatten_app_ty_args
1432 go_app_tys (AppTy ty1 ty2) tys = go_app_tys ty1 (ty2 : tys)
1433 go_app_tys fun_ty arg_tys
1434 = do { (fun_co, nfun) <- go fun_ty
1435 ; case tcSplitTyConApp_maybe nfun of
1436 Just (tc, xis) ->
1437 do { (second_co, nty) <- go (mkTyConApp tc (xis ++ arg_tys))
1438 -- flatten_app_ty_args avoids redundantly processing the xis,
1439 -- but that's a much more performance-sensitive function.
1440 -- This type normalisation is not called in a loop.
1441 ; return (mkAppCos fun_co (map mkNomReflCo arg_tys) `mkTransCo` second_co, nty) }
1442 Nothing ->
1443 do { (args_cos, nargs, res_co) <- normalise_args (typeKind nfun)
1444 (repeat Nominal)
1445 arg_tys
1446 ; role <- getRole
1447 ; let nty = mkAppTys nfun nargs
1448 nco = mkAppCos fun_co args_cos
1449 nty_casted = nty `mkCastTy` mkSymCo res_co
1450 final_co = mkCoherenceRightCo role nty (mkSymCo res_co) nco
1451 ; return (final_co, nty_casted) } }
1452
1453 normalise_args :: Kind -- of the function
1454 -> [Role] -- roles at which to normalise args
1455 -> [Type] -- args
1456 -> NormM ([Coercion], [Type], Coercion)
1457 -- returns (cos, xis, res_co), where each xi is the normalised
1458 -- version of the corresponding type, each co is orig_arg ~ xi,
1459 -- and the res_co :: kind(f orig_args) ~ kind(f xis)
1460 -- NB: The xis might *not* have the same kinds as the input types,
1461 -- but the resulting application *will* be well-kinded
1462 -- cf. TcFlatten.flatten_args_slow
1463 normalise_args fun_ki roles args
1464 = do { normed_args <- zipWithM normalise1 roles args
1465 ; let (xis, cos, res_co) = simplifyArgsWorker ki_binders inner_ki fvs roles normed_args
1466 ; return (map mkSymCo cos, xis, mkSymCo res_co) }
1467 where
1468 (ki_binders, inner_ki) = splitPiTys fun_ki
1469 fvs = tyCoVarsOfTypes args
1470
1471 -- flattener conventions are different from ours
1472 impedance_match :: NormM (Coercion, Type) -> NormM (Type, Coercion)
1473 impedance_match action = do { (co, ty) <- action
1474 ; return (ty, mkSymCo co) }
1475
1476 normalise1 role ty
1477 = impedance_match $ withRole role $ normalise_type ty
1478
1479 normalise_tyvar :: TyVar -> NormM (Coercion, Type)
1480 normalise_tyvar tv
1481 = ASSERT( isTyVar tv )
1482 do { lc <- getLC
1483 ; r <- getRole
1484 ; return $ case liftCoSubstTyVar lc r tv of
1485 Just co -> (co, pSnd $ coercionKind co)
1486 Nothing -> (mkReflCo r ty, ty) }
1487 where ty = mkTyVarTy tv
1488
1489 normalise_var_bndr :: TyCoVar -> NormM (LiftingContext, TyCoVar, Coercion, Kind)
1490 normalise_var_bndr tcvar
1491 -- works for both tvar and covar
1492 = do { lc1 <- getLC
1493 ; env <- getEnv
1494 ; let callback lc ki = runNormM (normalise_type ki) env lc Nominal
1495 ; return $ liftCoSubstVarBndrUsing callback lc1 tcvar }
1496
1497 -- | a monad for the normalisation functions, reading 'FamInstEnvs',
1498 -- a 'LiftingContext', and a 'Role'.
1499 newtype NormM a = NormM { runNormM ::
1500 FamInstEnvs -> LiftingContext -> Role -> a }
1501
1502 initNormM :: FamInstEnvs -> Role
1503 -> TyCoVarSet -- the in-scope variables
1504 -> NormM a -> a
1505 initNormM env role vars (NormM thing_inside)
1506 = thing_inside env lc role
1507 where
1508 in_scope = mkInScopeSet vars
1509 lc = emptyLiftingContext in_scope
1510
1511 getRole :: NormM Role
1512 getRole = NormM (\ _ _ r -> r)
1513
1514 getLC :: NormM LiftingContext
1515 getLC = NormM (\ _ lc _ -> lc)
1516
1517 getEnv :: NormM FamInstEnvs
1518 getEnv = NormM (\ env _ _ -> env)
1519
1520 withRole :: Role -> NormM a -> NormM a
1521 withRole r thing = NormM $ \ envs lc _old_r -> runNormM thing envs lc r
1522
1523 withLC :: LiftingContext -> NormM a -> NormM a
1524 withLC lc thing = NormM $ \ envs _old_lc r -> runNormM thing envs lc r
1525
1526 instance Monad NormM where
1527 ma >>= fmb = NormM $ \env lc r ->
1528 let a = runNormM ma env lc r in
1529 runNormM (fmb a) env lc r
1530
1531 instance Functor NormM where
1532 fmap = liftM
1533 instance Applicative NormM where
1534 pure x = NormM $ \ _ _ _ -> x
1535 (<*>) = ap
1536
1537 {-
1538 ************************************************************************
1539 * *
1540 Flattening
1541 * *
1542 ************************************************************************
1543
1544 Note [Flattening]
1545 ~~~~~~~~~~~~~~~~~
1546 As described in "Closed type families with overlapping equations"
1547 http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
1548 we need to flatten core types before unifying them, when checking for "surely-apart"
1549 against earlier equations of a closed type family.
1550 Flattening means replacing all top-level uses of type functions with
1551 fresh variables, *taking care to preserve sharing*. That is, the type
1552 (Either (F a b) (F a b)) should flatten to (Either c c), never (Either
1553 c d).
1554
1555 Here is a nice example of why it's all necessary:
1556
1557 type family F a b where
1558 F Int Bool = Char
1559 F a b = Double
1560 type family G a -- open, no instances
1561
1562 How do we reduce (F (G Float) (G Float))? The first equation clearly doesn't match,
1563 while the second equation does. But, before reducing, we must make sure that the
1564 target can never become (F Int Bool). Well, no matter what G Float becomes, it
1565 certainly won't become *both* Int and Bool, so indeed we're safe reducing
1566 (F (G Float) (G Float)) to Double.
1567
1568 This is necessary not only to get more reductions (which we might be
1569 willing to give up on), but for substitutivity. If we have (F x x), we
1570 can see that (F x x) can reduce to Double. So, it had better be the
1571 case that (F blah blah) can reduce to Double, no matter what (blah)
1572 is! Flattening as done below ensures this.
1573
1574 flattenTys is defined here because of module dependencies.
1575 -}
1576
1577 data FlattenEnv = FlattenEnv { fe_type_map :: TypeMap TyVar
1578 , fe_subst :: TCvSubst }
1579
1580 emptyFlattenEnv :: InScopeSet -> FlattenEnv
1581 emptyFlattenEnv in_scope
1582 = FlattenEnv { fe_type_map = emptyTypeMap
1583 , fe_subst = mkEmptyTCvSubst in_scope }
1584
1585 -- See Note [Flattening]
1586 flattenTys :: InScopeSet -> [Type] -> [Type]
1587 flattenTys in_scope tys = snd $ coreFlattenTys env tys
1588 where
1589 -- when we hit a type function, we replace it with a fresh variable
1590 -- but, we need to make sure that this fresh variable isn't mentioned
1591 -- *anywhere* in the types we're flattening, even if locally-bound in
1592 -- a forall. That way, we can ensure consistency both within and outside
1593 -- of that forall.
1594 all_in_scope = in_scope `extendInScopeSetSet` allTyCoVarsInTys tys
1595 env = emptyFlattenEnv all_in_scope
1596
1597 coreFlattenTys :: FlattenEnv -> [Type] -> (FlattenEnv, [Type])
1598 coreFlattenTys = go []
1599 where
1600 go rtys env [] = (env, reverse rtys)
1601 go rtys env (ty : tys)
1602 = let (env', ty') = coreFlattenTy env ty in
1603 go (ty' : rtys) env' tys
1604
1605 coreFlattenTy :: FlattenEnv -> Type -> (FlattenEnv, Type)
1606 coreFlattenTy = go
1607 where
1608 go env ty | Just ty' <- coreView ty = go env ty'
1609
1610 go env (TyVarTy tv) = (env, substTyVar (fe_subst env) tv)
1611 go env (AppTy ty1 ty2) = let (env1, ty1') = go env ty1
1612 (env2, ty2') = go env1 ty2 in
1613 (env2, AppTy ty1' ty2')
1614 go env (TyConApp tc tys)
1615 -- NB: Don't just check if isFamilyTyCon: this catches *data* families,
1616 -- which are generative and thus can be preserved during flattening
1617 | not (isGenerativeTyCon tc Nominal)
1618 = let (env', tv) = coreFlattenTyFamApp env tc tys in
1619 (env', mkTyVarTy tv)
1620
1621 | otherwise
1622 = let (env', tys') = coreFlattenTys env tys in
1623 (env', mkTyConApp tc tys')
1624
1625 go env ty@(FunTy { ft_arg = ty1, ft_res = ty2 })
1626 = let (env1, ty1') = go env ty1
1627 (env2, ty2') = go env1 ty2 in
1628 (env2, ty { ft_arg = ty1', ft_res = ty2' })
1629
1630 go env (ForAllTy (Bndr tv vis) ty)
1631 = let (env1, tv') = coreFlattenVarBndr env tv
1632 (env2, ty') = go env1 ty in
1633 (env2, ForAllTy (Bndr tv' vis) ty')
1634
1635 go env ty@(LitTy {}) = (env, ty)
1636
1637 go env (CastTy ty co) = let (env1, ty') = go env ty
1638 (env2, co') = coreFlattenCo env1 co in
1639 (env2, CastTy ty' co')
1640
1641 go env (CoercionTy co) = let (env', co') = coreFlattenCo env co in
1642 (env', CoercionTy co')
1643
1644 -- when flattening, we don't care about the contents of coercions.
1645 -- so, just return a fresh variable of the right (flattened) type
1646 coreFlattenCo :: FlattenEnv -> Coercion -> (FlattenEnv, Coercion)
1647 coreFlattenCo env co
1648 = (env2, mkCoVarCo covar)
1649 where
1650 (env1, kind') = coreFlattenTy env (coercionType co)
1651 fresh_name = mkFlattenFreshCoName
1652 subst1 = fe_subst env1
1653 in_scope = getTCvInScope subst1
1654 covar = uniqAway in_scope (mkCoVar fresh_name kind')
1655 env2 = env1 { fe_subst = subst1 `extendTCvInScope` covar }
1656
1657 coreFlattenVarBndr :: FlattenEnv -> TyCoVar -> (FlattenEnv, TyCoVar)
1658 coreFlattenVarBndr env tv
1659 | kind' `eqType` kind
1660 = ( env { fe_subst = extendTCvSubst old_subst tv (mkTyCoVarTy tv) }
1661 -- override any previous binding for tv
1662 , tv)
1663
1664 | otherwise
1665 = let new_tv = uniqAway (getTCvInScope old_subst) (setVarType tv kind')
1666 new_subst = extendTCvSubstWithClone old_subst tv new_tv
1667 in
1668 (env' { fe_subst = new_subst }, new_tv)
1669 where
1670 kind = varType tv
1671 (env', kind') = coreFlattenTy env kind
1672 old_subst = fe_subst env
1673
1674 coreFlattenTyFamApp :: FlattenEnv
1675 -> TyCon -- type family tycon
1676 -> [Type] -- args
1677 -> (FlattenEnv, TyVar)
1678 coreFlattenTyFamApp env fam_tc fam_args
1679 = case lookupTypeMap type_map fam_ty of
1680 Just tv -> (env, tv)
1681 -- we need fresh variables here, but this is called far from
1682 -- any good source of uniques. So, we just use the fam_tc's unique
1683 -- and trust uniqAway to avoid clashes. Recall that the in_scope set
1684 -- contains *all* tyvars, even locally bound ones elsewhere in the
1685 -- overall type, so this really is fresh.
1686 Nothing -> let tyvar_name = mkFlattenFreshTyName fam_tc
1687 tv = uniqAway (getTCvInScope subst) $
1688 mkTyVar tyvar_name (typeKind fam_ty)
1689 env' = env { fe_type_map = extendTypeMap type_map fam_ty tv
1690 , fe_subst = extendTCvInScope subst tv }
1691 in (env', tv)
1692 where fam_ty = mkTyConApp fam_tc fam_args
1693 FlattenEnv { fe_type_map = type_map
1694 , fe_subst = subst } = env
1695
1696 -- | Get the set of all type/coercion variables mentioned anywhere in the list
1697 -- of types. These variables are not necessarily free.
1698 allTyCoVarsInTys :: [Type] -> VarSet
1699 allTyCoVarsInTys [] = emptyVarSet
1700 allTyCoVarsInTys (ty:tys) = allTyCoVarsInTy ty `unionVarSet` allTyCoVarsInTys tys
1701
1702 -- | Get the set of all type/coercion variables mentioned anywhere in a type.
1703 allTyCoVarsInTy :: Type -> VarSet
1704 allTyCoVarsInTy = go
1705 where
1706 go (TyVarTy tv) = unitVarSet tv
1707 go (TyConApp _ tys) = allTyCoVarsInTys tys
1708 go (AppTy ty1 ty2) = (go ty1) `unionVarSet` (go ty2)
1709 go (FunTy _ ty1 ty2) = (go ty1) `unionVarSet` (go ty2)
1710 go (ForAllTy (Bndr tv _) ty) = unitVarSet tv `unionVarSet`
1711 go (tyVarKind tv) `unionVarSet`
1712 go ty
1713 -- Don't remove the tv from the set!
1714 go (LitTy {}) = emptyVarSet
1715 go (CastTy ty co) = go ty `unionVarSet` go_co co
1716 go (CoercionTy co) = go_co co
1717
1718 go_mco MRefl = emptyVarSet
1719 go_mco (MCo co) = go_co co
1720
1721 go_co (Refl ty) = go ty
1722 go_co (GRefl _ ty mco) = go ty `unionVarSet` go_mco mco
1723 go_co (TyConAppCo _ _ args) = go_cos args
1724 go_co (AppCo co arg) = go_co co `unionVarSet` go_co arg
1725 go_co (ForAllCo tv h co)
1726 = unionVarSets [unitVarSet tv, go_co co, go_co h]
1727 go_co (FunCo _ c1 c2) = go_co c1 `unionVarSet` go_co c2
1728 go_co (CoVarCo cv) = unitVarSet cv
1729 go_co (HoleCo h) = unitVarSet (coHoleCoVar h)
1730 go_co (AxiomInstCo _ _ cos) = go_cos cos
1731 go_co (UnivCo p _ t1 t2) = go_prov p `unionVarSet` go t1 `unionVarSet` go t2
1732 go_co (SymCo co) = go_co co
1733 go_co (TransCo c1 c2) = go_co c1 `unionVarSet` go_co c2
1734 go_co (NthCo _ _ co) = go_co co
1735 go_co (LRCo _ co) = go_co co
1736 go_co (InstCo co arg) = go_co co `unionVarSet` go_co arg
1737 go_co (KindCo co) = go_co co
1738 go_co (SubCo co) = go_co co
1739 go_co (AxiomRuleCo _ cs) = go_cos cs
1740
1741 go_cos = foldr (unionVarSet . go_co) emptyVarSet
1742
1743 go_prov UnsafeCoerceProv = emptyVarSet
1744 go_prov (PhantomProv co) = go_co co
1745 go_prov (ProofIrrelProv co) = go_co co
1746 go_prov (PluginProv _) = emptyVarSet
1747
1748 mkFlattenFreshTyName :: Uniquable a => a -> Name
1749 mkFlattenFreshTyName unq
1750 = mkSysTvName (getUnique unq) (fsLit "flt")
1751
1752 mkFlattenFreshCoName :: Name
1753 mkFlattenFreshCoName
1754 = mkSystemVarName (deriveUnique eqPrimTyConKey 71) (fsLit "flc")