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