d721ad287363514b1316ebdabe5dffcc0f054b7b
[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 #-}
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 MonadUtils
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]. This function implements first
539 -- check described there.
540 = let getInjArgs = filterByList injectivity
541 in case tcUnifyTyWithTFs True rhs1 rhs2 of -- True = two-way pre-unification
542 Nothing -> InjectivityAccepted -- RHS are different, so equations are
543 -- injective.
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
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
559 -- takes a CoAxiom with unknown branch incompatibilities and computes
560 -- the compatibilities
561 -- See Note [Storing compatibility] in CoAxiom
562 computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch]
563 computeAxiomIncomps branches
564 = snd (mapAccumL go [] branches)
565 where
566 go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
567 go prev_brs cur_br
568 = (cur_br : prev_brs, new_br)
569 where
570 new_br = cur_br { cab_incomps = mk_incomps prev_brs cur_br }
571
572 mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch]
573 mk_incomps prev_brs cur_br
574 = filter (not . compatibleBranches cur_br) prev_brs
575
576 {-
577 ************************************************************************
578 * *
579 Constructing axioms
580 These functions are here because tidyType / tcUnifyTysFG
581 are not available in CoAxiom
582
583 Also computeAxiomIncomps is too sophisticated for CoAxiom
584 * *
585 ************************************************************************
586
587 Note [Tidy axioms when we build them]
588 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
589 Like types and classes, we build axioms fully quantified over all
590 their variables, and tidy them when we build them. For example,
591 we print out axioms and don't want to print stuff like
592 F k k a b = ...
593 Instead we must tidy those kind variables. See Trac #7524.
594
595 We could instead tidy when we print, but that makes it harder to get
596 things like injectivity errors to come out right. Danger of
597 Type family equation violates injectivity annotation.
598 Kind variable ‘k’ cannot be inferred from the right-hand side.
599 In the type family equation:
600 PolyKindVars @[k1] @[k2] ('[] @k1) = '[] @k2
601
602 Note [Always number wildcard types in CoAxBranch]
603 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
604 Consider the following example (from the DataFamilyInstanceLHS test case):
605
606 data family Sing (a :: k)
607 data instance Sing (_ :: MyKind) where
608 SingA :: Sing A
609 SingB :: Sing B
610
611 If we're not careful during tidying, then when this program is compiled with
612 -ddump-types, we'll get the following information:
613
614 COERCION AXIOMS
615 axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 ::
616 Sing _ = DataFamilyInstanceLHS.R:SingMyKind_ _
617
618 It's misleading to have a wildcard type appearing on the RHS like
619 that. To avoid this issue, when building a CoAxiom (which is what eventually
620 gets printed above), we tidy all the variables in an env that already contains
621 '_'. Thus, any variable named '_' will be renamed, giving us the nicer output
622 here:
623
624 COERCION AXIOMS
625 axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 ::
626 Sing _1 = DataFamilyInstanceLHS.R:SingMyKind_ _1
627
628 Which is at least legal syntax.
629
630 See also Note [CoAxBranch type variables] in CoAxiom; note that we
631 are tidying (changing OccNames only), not freshening, in accordance with
632 that Note.
633 -}
634
635 -- all axiom roles are Nominal, as this is only used with type families
636 mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
637 -> [TyVar] -- Extra eta tyvars
638 -> [CoVar] -- possibly stale covars
639 -> [Type] -- LHS patterns
640 -> Type -- RHS
641 -> [Role]
642 -> SrcSpan
643 -> CoAxBranch
644 mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc
645 = CoAxBranch { cab_tvs = tvs'
646 , cab_eta_tvs = eta_tvs'
647 , cab_cvs = cvs'
648 , cab_lhs = tidyTypes env lhs
649 , cab_roles = roles
650 , cab_rhs = tidyType env rhs
651 , cab_loc = loc
652 , cab_incomps = placeHolderIncomps }
653 where
654 (env1, tvs') = tidyVarBndrs init_tidy_env tvs
655 (env2, eta_tvs') = tidyVarBndrs env1 eta_tvs
656 (env, cvs') = tidyVarBndrs env2 cvs
657 -- See Note [Tidy axioms when we build them]
658 -- See also Note [CoAxBranch type variables] in CoAxiom
659
660 init_occ_env = initTidyOccEnv [mkTyVarOcc "_"]
661 init_tidy_env = mkEmptyTidyEnv init_occ_env
662 -- See Note [Always number wildcard types in CoAxBranch]
663
664 -- all of the following code is here to avoid mutual dependencies with
665 -- Coercion
666 mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
667 mkBranchedCoAxiom ax_name fam_tc branches
668 = CoAxiom { co_ax_unique = nameUnique ax_name
669 , co_ax_name = ax_name
670 , co_ax_tc = fam_tc
671 , co_ax_role = Nominal
672 , co_ax_implicit = False
673 , co_ax_branches = manyBranches (computeAxiomIncomps branches) }
674
675 mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched
676 mkUnbranchedCoAxiom ax_name fam_tc branch
677 = CoAxiom { co_ax_unique = nameUnique ax_name
678 , co_ax_name = ax_name
679 , co_ax_tc = fam_tc
680 , co_ax_role = Nominal
681 , co_ax_implicit = False
682 , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
683
684 mkSingleCoAxiom :: Role -> Name
685 -> [TyVar] -> [TyVar] -> [CoVar]
686 -> TyCon -> [Type] -> Type
687 -> CoAxiom Unbranched
688 -- Make a single-branch CoAxiom, incluidng making the branch itself
689 -- Used for both type family (Nominal) and data family (Representational)
690 -- axioms, hence passing in the Role
691 mkSingleCoAxiom role ax_name tvs eta_tvs cvs fam_tc lhs_tys rhs_ty
692 = CoAxiom { co_ax_unique = nameUnique ax_name
693 , co_ax_name = ax_name
694 , co_ax_tc = fam_tc
695 , co_ax_role = role
696 , co_ax_implicit = False
697 , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
698 where
699 branch = mkCoAxBranch tvs eta_tvs cvs lhs_tys rhs_ty
700 (map (const Nominal) tvs)
701 (getSrcSpan ax_name)
702
703 -- | Create a coercion constructor (axiom) suitable for the given
704 -- newtype 'TyCon'. The 'Name' should be that of a new coercion
705 -- 'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and
706 -- the type the appropriate right hand side of the @newtype@, with
707 -- the free variables a subset of those 'TyVar's.
708 mkNewTypeCoAxiom :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched
709 mkNewTypeCoAxiom name tycon tvs roles rhs_ty
710 = CoAxiom { co_ax_unique = nameUnique name
711 , co_ax_name = name
712 , co_ax_implicit = True -- See Note [Implicit axioms] in TyCon
713 , co_ax_role = Representational
714 , co_ax_tc = tycon
715 , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
716 where
717 branch = mkCoAxBranch tvs [] [] (mkTyVarTys tvs) rhs_ty
718 roles (getSrcSpan name)
719
720 {-
721 ************************************************************************
722 * *
723 Looking up a family instance
724 * *
725 ************************************************************************
726
727 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
728 Multiple matches are only possible in case of type families (not data
729 families), and then, it doesn't matter which match we choose (as the
730 instances are guaranteed confluent).
731
732 We return the matching family instances and the type instance at which it
733 matches. For example, if we lookup 'T [Int]' and have a family instance
734
735 data instance T [a] = ..
736
737 desugared to
738
739 data :R42T a = ..
740 coe :Co:R42T a :: T [a] ~ :R42T a
741
742 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
743 -}
744
745 -- when matching a type family application, we get a FamInst,
746 -- and the list of types the axiom should be applied to
747 data FamInstMatch = FamInstMatch { fim_instance :: FamInst
748 , fim_tys :: [Type]
749 , fim_cos :: [Coercion]
750 }
751 -- See Note [Over-saturated matches]
752
753 instance Outputable FamInstMatch where
754 ppr (FamInstMatch { fim_instance = inst
755 , fim_tys = tys
756 , fim_cos = cos })
757 = text "match with" <+> parens (ppr inst) <+> ppr tys <+> ppr cos
758
759 lookupFamInstEnvByTyCon :: FamInstEnvs -> TyCon -> [FamInst]
760 lookupFamInstEnvByTyCon (pkg_ie, home_ie) fam_tc
761 = get pkg_ie ++ get home_ie
762 where
763 get ie = case lookupUDFM ie fam_tc of
764 Nothing -> []
765 Just (FamIE fis) -> fis
766
767 lookupFamInstEnv
768 :: FamInstEnvs
769 -> TyCon -> [Type] -- What we are looking for
770 -> [FamInstMatch] -- Successful matches
771 -- Precondition: the tycon is saturated (or over-saturated)
772
773 lookupFamInstEnv
774 = lookup_fam_inst_env match
775 where
776 match _ _ tpl_tys tys = tcMatchTys tpl_tys tys
777
778 lookupFamInstEnvConflicts
779 :: FamInstEnvs
780 -> FamInst -- Putative new instance
781 -> [FamInstMatch] -- Conflicting matches (don't look at the fim_tys field)
782 -- E.g. when we are about to add
783 -- f : type instance F [a] = a->a
784 -- we do (lookupFamInstConflicts f [b])
785 -- to find conflicting matches
786 --
787 -- Precondition: the tycon is saturated (or over-saturated)
788
789 lookupFamInstEnvConflicts envs fam_inst@(FamInst { fi_axiom = new_axiom })
790 = lookup_fam_inst_env my_unify envs fam tys
791 where
792 (fam, tys) = famInstSplitLHS fam_inst
793 -- In example above, fam tys' = F [b]
794
795 my_unify (FamInst { fi_axiom = old_axiom }) tpl_tvs tpl_tys _
796 = ASSERT2( tyCoVarsOfTypes tys `disjointVarSet` tpl_tvs,
797 (ppr fam <+> ppr tys) $$
798 (ppr tpl_tvs <+> ppr tpl_tys) )
799 -- Unification will break badly if the variables overlap
800 -- They shouldn't because we allocate separate uniques for them
801 if compatibleBranches (coAxiomSingleBranch old_axiom) new_branch
802 then Nothing
803 else Just noSubst
804 -- Note [Family instance overlap conflicts]
805
806 noSubst = panic "lookupFamInstEnvConflicts noSubst"
807 new_branch = coAxiomSingleBranch new_axiom
808
809 --------------------------------------------------------------------------------
810 -- Type family injectivity checking bits --
811 --------------------------------------------------------------------------------
812
813 {- Note [Verifying injectivity annotation]
814 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
815
816 Injectivity means that the RHS of a type family uniquely determines the LHS (see
817 Note [Type inference for type families with injectivity]). User informs about
818 injectivity using an injectivity annotation and it is GHC's task to verify that
819 that annotation is correct wrt. to type family equations. Whenever we see a new
820 equation of a type family we need to make sure that adding this equation to
821 already known equations of a type family does not violate injectivity annotation
822 supplied by the user (see Note [Injectivity annotation]). Of course if the type
823 family has no injectivity annotation then no check is required. But if a type
824 family has injectivity annotation we need to make sure that the following
825 conditions hold:
826
827 1. For each pair of *different* equations of a type family, one of the following
828 conditions holds:
829
830 A: RHSs are different.
831
832 B1: OPEN TYPE FAMILIES: If the RHSs can be unified under some substitution
833 then it must be possible to unify the LHSs under the same substitution.
834 Example:
835
836 type family FunnyId a = r | r -> a
837 type instance FunnyId Int = Int
838 type instance FunnyId a = a
839
840 RHSs of these two equations unify under [ a |-> Int ] substitution.
841 Under this substitution LHSs are equal therefore these equations don't
842 violate injectivity annotation.
843
844 B2: CLOSED TYPE FAMILIES: If the RHSs can be unified under some
845 substitution then either the LHSs unify under the same substitution or
846 the LHS of the latter equation is overlapped by earlier equations.
847 Example 1:
848
849 type family SwapIntChar a = r | r -> a where
850 SwapIntChar Int = Char
851 SwapIntChar Char = Int
852 SwapIntChar a = a
853
854 Say we are checking the last two equations. RHSs unify under [ a |->
855 Int ] substitution but LHSs don't. So we apply the substitution to LHS
856 of last equation and check whether it is overlapped by any of previous
857 equations. Since it is overlapped by the first equation we conclude
858 that pair of last two equations does not violate injectivity
859 annotation.
860
861 A special case of B is when RHSs unify with an empty substitution ie. they
862 are identical.
863
864 If any of the above two conditions holds we conclude that the pair of
865 equations does not violate injectivity annotation. But if we find a pair
866 of equations where neither of the above holds we report that this pair
867 violates injectivity annotation because for a given RHS we don't have a
868 unique LHS. (Note that (B) actually implies (A).)
869
870 Note that we only take into account these LHS patterns that were declared
871 as injective.
872
873 2. If a RHS of a type family equation is a bare type variable then
874 all LHS variables (including implicit kind variables) also have to be bare.
875 In other words, this has to be a sole equation of that type family and it has
876 to cover all possible patterns. So for example this definition will be
877 rejected:
878
879 type family W1 a = r | r -> a
880 type instance W1 [a] = a
881
882 If it were accepted we could call `W1 [W1 Int]`, which would reduce to
883 `W1 Int` and then by injectivity we could conclude that `[W1 Int] ~ Int`,
884 which is bogus.
885
886 3. If a RHS of a type family equation is a type family application then the type
887 family is rejected as not injective.
888
889 4. If a LHS type variable that is declared as injective is not mentioned on
890 injective position in the RHS then the type family is rejected as not
891 injective. "Injective position" means either an argument to a type
892 constructor or argument to a type family on injective position.
893
894 See also Note [Injective type families] in TyCon
895 -}
896
897
898 -- | Check whether an open type family equation can be added to already existing
899 -- instance environment without causing conflicts with supplied injectivity
900 -- annotations. Returns list of conflicting axioms (type instance
901 -- declarations).
902 lookupFamInstEnvInjectivityConflicts
903 :: [Bool] -- injectivity annotation for this type family instance
904 -- INVARIANT: list contains at least one True value
905 -> FamInstEnvs -- all type instances seens so far
906 -> FamInst -- new type instance that we're checking
907 -> [CoAxBranch] -- conflicting instance declarations
908 lookupFamInstEnvInjectivityConflicts injList (pkg_ie, home_ie)
909 fam_inst@(FamInst { fi_axiom = new_axiom })
910 -- See Note [Verifying injectivity annotation]. This function implements
911 -- check (1.B1) for open type families described there.
912 = lookup_inj_fam_conflicts home_ie ++ lookup_inj_fam_conflicts pkg_ie
913 where
914 fam = famInstTyCon fam_inst
915 new_branch = coAxiomSingleBranch new_axiom
916
917 -- filtering function used by `lookup_inj_fam_conflicts` to check whether
918 -- a pair of equations conflicts with the injectivity annotation.
919 isInjConflict (FamInst { fi_axiom = old_axiom })
920 | InjectivityAccepted <-
921 injectiveBranches injList (coAxiomSingleBranch old_axiom) new_branch
922 = False -- no conflict
923 | otherwise = True
924
925 lookup_inj_fam_conflicts ie
926 | isOpenFamilyTyCon fam, Just (FamIE insts) <- lookupUDFM ie fam
927 = map (coAxiomSingleBranch . fi_axiom) $
928 filter isInjConflict insts
929 | otherwise = []
930
931
932 --------------------------------------------------------------------------------
933 -- Type family overlap checking bits --
934 --------------------------------------------------------------------------------
935
936 {-
937 Note [Family instance overlap conflicts]
938 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
939 - In the case of data family instances, any overlap is fundamentally a
940 conflict (as these instances imply injective type mappings).
941
942 - In the case of type family instances, overlap is admitted as long as
943 the right-hand sides of the overlapping rules coincide under the
944 overlap substitution. eg
945 type instance F a Int = a
946 type instance F Int b = b
947 These two overlap on (F Int Int) but then both RHSs are Int,
948 so all is well. We require that they are syntactically equal;
949 anything else would be difficult to test for at this stage.
950 -}
951
952 ------------------------------------------------------------
953 -- Might be a one-way match or a unifier
954 type MatchFun = FamInst -- The FamInst template
955 -> TyVarSet -> [Type] -- fi_tvs, fi_tys of that FamInst
956 -> [Type] -- Target to match against
957 -> Maybe TCvSubst
958
959 lookup_fam_inst_env' -- The worker, local to this module
960 :: MatchFun
961 -> FamInstEnv
962 -> TyCon -> [Type] -- What we are looking for
963 -> [FamInstMatch]
964 lookup_fam_inst_env' match_fun ie fam match_tys
965 | isOpenFamilyTyCon fam
966 , Just (FamIE insts) <- lookupUDFM ie fam
967 = find insts -- The common case
968 | otherwise = []
969 where
970
971 find [] = []
972 find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs, fi_cvs = tpl_cvs
973 , fi_tys = tpl_tys }) : rest)
974 -- Fast check for no match, uses the "rough match" fields
975 | instanceCantMatch rough_tcs mb_tcs
976 = find rest
977
978 -- Proper check
979 | Just subst <- match_fun item (mkVarSet tpl_tvs) tpl_tys match_tys1
980 = (FamInstMatch { fim_instance = item
981 , fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2
982 , fim_cos = ASSERT( all (isJust . lookupCoVar subst) tpl_cvs )
983 substCoVars subst tpl_cvs
984 })
985 : find rest
986
987 -- No match => try next
988 | otherwise
989 = find rest
990 where
991 (rough_tcs, match_tys1, match_tys2) = split_tys tpl_tys
992
993 -- Precondition: the tycon is saturated (or over-saturated)
994
995 -- Deal with over-saturation
996 -- See Note [Over-saturated matches]
997 split_tys tpl_tys
998 | isTypeFamilyTyCon fam
999 = pre_rough_split_tys
1000
1001 | otherwise
1002 = let (match_tys1, match_tys2) = splitAtList tpl_tys match_tys
1003 rough_tcs = roughMatchTcs match_tys1
1004 in (rough_tcs, match_tys1, match_tys2)
1005
1006 (pre_match_tys1, pre_match_tys2) = splitAt (tyConArity fam) match_tys
1007 pre_rough_split_tys
1008 = (roughMatchTcs pre_match_tys1, pre_match_tys1, pre_match_tys2)
1009
1010 lookup_fam_inst_env -- The worker, local to this module
1011 :: MatchFun
1012 -> FamInstEnvs
1013 -> TyCon -> [Type] -- What we are looking for
1014 -> [FamInstMatch] -- Successful matches
1015
1016 -- Precondition: the tycon is saturated (or over-saturated)
1017
1018 lookup_fam_inst_env match_fun (pkg_ie, home_ie) fam tys
1019 = lookup_fam_inst_env' match_fun home_ie fam tys
1020 ++ lookup_fam_inst_env' match_fun pkg_ie fam tys
1021
1022 {-
1023 Note [Over-saturated matches]
1024 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1025 It's ok to look up an over-saturated type constructor. E.g.
1026 type family F a :: * -> *
1027 type instance F (a,b) = Either (a->b)
1028
1029 The type instance gives rise to a newtype TyCon (at a higher kind
1030 which you can't do in Haskell!):
1031 newtype FPair a b = FP (Either (a->b))
1032
1033 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
1034 (FPair, [Int,Bool,Char])
1035 The "extra" type argument [Char] just stays on the end.
1036
1037 We handle data families and type families separately here:
1038
1039 * For type families, all instances of a type family must have the
1040 same arity, so we can precompute the split between the match_tys
1041 and the overflow tys. This is done in pre_rough_split_tys.
1042
1043 * For data family instances, though, we need to re-split for each
1044 instance, because the breakdown might be different for each
1045 instance. Why? Because of eta reduction; see
1046 Note [Eta reduction for data families].
1047 -}
1048
1049 -- checks if one LHS is dominated by a list of other branches
1050 -- in other words, if an application would match the first LHS, it is guaranteed
1051 -- to match at least one of the others. The RHSs are ignored.
1052 -- This algorithm is conservative:
1053 -- True -> the LHS is definitely covered by the others
1054 -- False -> no information
1055 -- It is currently (Oct 2012) used only for generating errors for
1056 -- inaccessible branches. If these errors go unreported, no harm done.
1057 -- This is defined here to avoid a dependency from CoAxiom to Unify
1058 isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool
1059 isDominatedBy branch branches
1060 = or $ map match branches
1061 where
1062 lhs = coAxBranchLHS branch
1063 match (CoAxBranch { cab_lhs = tys })
1064 = isJust $ tcMatchTys tys lhs
1065
1066 {-
1067 ************************************************************************
1068 * *
1069 Choosing an axiom application
1070 * *
1071 ************************************************************************
1072
1073 The lookupFamInstEnv function does a nice job for *open* type families,
1074 but we also need to handle closed ones when normalising a type:
1075 -}
1076
1077 reduceTyFamApp_maybe :: FamInstEnvs
1078 -> Role -- Desired role of result coercion
1079 -> TyCon -> [Type]
1080 -> Maybe (Coercion, Type)
1081 -- Attempt to do a *one-step* reduction of a type-family application
1082 -- but *not* newtypes
1083 -- Works on type-synonym families always; data-families only if
1084 -- the role we seek is representational
1085 -- It does *not* normlise the type arguments first, so this may not
1086 -- go as far as you want. If you want normalised type arguments,
1087 -- use normaliseTcArgs first.
1088 --
1089 -- The TyCon can be oversaturated.
1090 -- Works on both open and closed families
1091 --
1092 -- Always returns a *homogeneous* coercion -- type family reductions are always
1093 -- homogeneous
1094 reduceTyFamApp_maybe envs role tc tys
1095 | Phantom <- role
1096 = Nothing
1097
1098 | case role of
1099 Representational -> isOpenFamilyTyCon tc
1100 _ -> isOpenTypeFamilyTyCon tc
1101 -- If we seek a representational coercion
1102 -- (e.g. the call in topNormaliseType_maybe) then we can
1103 -- unwrap data families as well as type-synonym families;
1104 -- otherwise only type-synonym families
1105 , FamInstMatch { fim_instance = FamInst { fi_axiom = ax }
1106 , fim_tys = inst_tys
1107 , fim_cos = inst_cos } : _ <- lookupFamInstEnv envs tc tys
1108 -- NB: Allow multiple matches because of compatible overlap
1109
1110 = let co = mkUnbranchedAxInstCo role ax inst_tys inst_cos
1111 ty = pSnd (coercionKind co)
1112 in Just (co, ty)
1113
1114 | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe tc
1115 , Just (ind, inst_tys, inst_cos) <- chooseBranch ax tys
1116 = let co = mkAxInstCo role ax ind inst_tys inst_cos
1117 ty = pSnd (coercionKind co)
1118 in Just (co, ty)
1119
1120 | Just ax <- isBuiltInSynFamTyCon_maybe tc
1121 , Just (coax,ts,ty) <- sfMatchFam ax tys
1122 = let co = mkAxiomRuleCo coax (zipWith mkReflCo (coaxrAsmpRoles coax) ts)
1123 in Just (co, ty)
1124
1125 | otherwise
1126 = Nothing
1127
1128 -- The axiom can be oversaturated. (Closed families only.)
1129 chooseBranch :: CoAxiom Branched -> [Type]
1130 -> Maybe (BranchIndex, [Type], [Coercion]) -- found match, with args
1131 chooseBranch axiom tys
1132 = do { let num_pats = coAxiomNumPats axiom
1133 (target_tys, extra_tys) = splitAt num_pats tys
1134 branches = coAxiomBranches axiom
1135 ; (ind, inst_tys, inst_cos)
1136 <- findBranch (unMkBranches branches) target_tys
1137 ; return ( ind, inst_tys `chkAppend` extra_tys, inst_cos ) }
1138
1139 -- The axiom must *not* be oversaturated
1140 findBranch :: Array BranchIndex CoAxBranch
1141 -> [Type]
1142 -> Maybe (BranchIndex, [Type], [Coercion])
1143 -- coercions relate requested types to returned axiom LHS at role N
1144 findBranch branches target_tys
1145 = foldr go Nothing (assocs branches)
1146 where
1147 go :: (BranchIndex, CoAxBranch)
1148 -> Maybe (BranchIndex, [Type], [Coercion])
1149 -> Maybe (BranchIndex, [Type], [Coercion])
1150 go (index, branch) other
1151 = let (CoAxBranch { cab_tvs = tpl_tvs, cab_cvs = tpl_cvs
1152 , cab_lhs = tpl_lhs
1153 , cab_incomps = incomps }) = branch
1154 in_scope = mkInScopeSet (unionVarSets $
1155 map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
1156 -- See Note [Flattening] below
1157 flattened_target = flattenTys in_scope target_tys
1158 in case tcMatchTys tpl_lhs target_tys of
1159 Just subst -- matching worked. now, check for apartness.
1160 | apartnessCheck flattened_target branch
1161 -> -- matching worked & we're apart from all incompatible branches.
1162 -- success
1163 ASSERT( all (isJust . lookupCoVar subst) tpl_cvs )
1164 Just (index, substTyVars subst tpl_tvs, substCoVars subst tpl_cvs)
1165
1166 -- failure. keep looking
1167 _ -> other
1168
1169 -- | Do an apartness check, as described in the "Closed Type Families" paper
1170 -- (POPL '14). This should be used when determining if an equation
1171 -- ('CoAxBranch') of a closed type family can be used to reduce a certain target
1172 -- type family application.
1173 apartnessCheck :: [Type] -- ^ /flattened/ target arguments. Make sure
1174 -- they're flattened! See Note [Flattening].
1175 -- (NB: This "flat" is a different
1176 -- "flat" than is used in TcFlatten.)
1177 -> CoAxBranch -- ^ the candidate equation we wish to use
1178 -- Precondition: this matches the target
1179 -> Bool -- ^ True <=> equation can fire
1180 apartnessCheck flattened_target (CoAxBranch { cab_incomps = incomps })
1181 = all (isSurelyApart
1182 . tcUnifyTysFG (const BindMe) flattened_target
1183 . coAxBranchLHS) incomps
1184 where
1185 isSurelyApart SurelyApart = True
1186 isSurelyApart _ = False
1187
1188 {-
1189 ************************************************************************
1190 * *
1191 Looking up a family instance
1192 * *
1193 ************************************************************************
1194
1195 Note [Normalising types]
1196 ~~~~~~~~~~~~~~~~~~~~~~~~
1197 The topNormaliseType function removes all occurrences of type families
1198 and newtypes from the top-level structure of a type. normaliseTcApp does
1199 the type family lookup and is fairly straightforward. normaliseType is
1200 a little more involved.
1201
1202 The complication comes from the fact that a type family might be used in the
1203 kind of a variable bound in a forall. We wish to remove this type family
1204 application, but that means coming up with a fresh variable (with the new
1205 kind). Thus, we need a substitution to be built up as we recur through the
1206 type. However, an ordinary TCvSubst just won't do: when we hit a type variable
1207 whose kind has changed during normalisation, we need both the new type
1208 variable *and* the coercion. We could conjure up a new VarEnv with just this
1209 property, but a usable substitution environment already exists:
1210 LiftingContexts from the liftCoSubst family of functions, defined in Coercion.
1211 A LiftingContext maps a type variable to a coercion and a coercion variable to
1212 a pair of coercions. Let's ignore coercion variables for now. Because the
1213 coercion a type variable maps to contains the destination type (via
1214 coercionKind), we don't need to store that destination type separately. Thus,
1215 a LiftingContext has what we need: a map from type variables to (Coercion,
1216 Type) pairs.
1217
1218 We also benefit because we can piggyback on the liftCoSubstVarBndr function to
1219 deal with binders. However, I had to modify that function to work with this
1220 application. Thus, we now have liftCoSubstVarBndrUsing, which takes
1221 a function used to process the kind of the binder. We don't wish
1222 to lift the kind, but instead normalise it. So, we pass in a callback function
1223 that processes the kind of the binder.
1224
1225 After that brilliant explanation of all this, I'm sure you've forgotten the
1226 dangling reference to coercion variables. What do we do with those? Nothing at
1227 all. The point of normalising types is to remove type family applications, but
1228 there's no sense in removing these from coercions. We would just get back a
1229 new coercion witnessing the equality between the same types as the original
1230 coercion. Because coercions are irrelevant anyway, there is no point in doing
1231 this. So, whenever we encounter a coercion, we just say that it won't change.
1232 That's what the CoercionTy case is doing within normalise_type.
1233
1234 Note [Normalisation and type synonyms]
1235 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1236 We need to be a bit careful about normalising in the presence of type
1237 synonyms (Trac #13035). Suppose S is a type synonym, and we have
1238 S t1 t2
1239 If S is family-free (on its RHS) we can just normalise t1 and t2 and
1240 reconstruct (S t1' t2'). Expanding S could not reveal any new redexes
1241 because type families are saturated.
1242
1243 But if S has a type family on its RHS we expand /before/ normalising
1244 the args t1, t2. If we normalise t1, t2 first, we'll re-normalise them
1245 after expansion, and that can lead to /exponential/ behavour; see Trac #13035.
1246
1247 Notice, though, that expanding first can in principle duplicate t1,t2,
1248 which might contain redexes. I'm sure you could conjure up an exponential
1249 case by that route too, but it hasn't happened in practice yet!
1250 -}
1251
1252 topNormaliseType :: FamInstEnvs -> Type -> Type
1253 topNormaliseType env ty = case topNormaliseType_maybe env ty of
1254 Just (_co, ty') -> ty'
1255 Nothing -> ty
1256
1257 topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Coercion, Type)
1258
1259 -- ^ Get rid of *outermost* (or toplevel)
1260 -- * type function redex
1261 -- * data family redex
1262 -- * newtypes
1263 -- returning an appropriate Representational coercion. Specifically, if
1264 -- topNormaliseType_maybe env ty = Just (co, ty')
1265 -- then
1266 -- (a) co :: ty ~R ty'
1267 -- (b) ty' is not a newtype, and is not a type-family or data-family redex
1268 --
1269 -- However, ty' can be something like (Maybe (F ty)), where
1270 -- (F ty) is a redex.
1271
1272 topNormaliseType_maybe env ty
1273 = topNormaliseTypeX stepper mkTransCo ty
1274 where
1275 stepper = unwrapNewTypeStepper `composeSteppers` tyFamStepper
1276
1277 tyFamStepper rec_nts tc tys -- Try to step a type/data family
1278 = let (args_co, ntys) = normaliseTcArgs env Representational tc tys in
1279 case reduceTyFamApp_maybe env Representational tc ntys of
1280 Just (co, rhs) -> NS_Step rec_nts rhs (args_co `mkTransCo` co)
1281 _ -> NS_Done
1282
1283 ---------------
1284 normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> (Coercion, Type)
1285 -- See comments on normaliseType for the arguments of this function
1286 normaliseTcApp env role tc tys
1287 = initNormM env role (tyCoVarsOfTypes tys) $
1288 normalise_tc_app tc tys
1289
1290 -- See Note [Normalising types] about the LiftingContext
1291 normalise_tc_app :: TyCon -> [Type] -> NormM (Coercion, Type)
1292 normalise_tc_app tc tys
1293 | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
1294 , not (isFamFreeTyCon tc) -- Expand and try again
1295 = -- A synonym with type families in the RHS
1296 -- Expand and try again
1297 -- See Note [Normalisation and type synonyms]
1298 normalise_type (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
1299
1300 | isFamilyTyCon tc
1301 = -- A type-family application
1302 do { env <- getEnv
1303 ; role <- getRole
1304 ; (args_co, ntys) <- normalise_tc_args tc tys
1305 ; case reduceTyFamApp_maybe env role tc ntys of
1306 Just (first_co, ty')
1307 -> do { (rest_co,nty) <- normalise_type ty'
1308 ; return ( args_co `mkTransCo` first_co `mkTransCo` rest_co
1309 , nty ) }
1310 _ -> -- No unique matching family instance exists;
1311 -- we do not do anything
1312 return (args_co, mkTyConApp tc ntys) }
1313
1314 | otherwise
1315 = -- A synonym with no type families in the RHS; or data type etc
1316 -- Just normalise the arguments and rebuild
1317 do { (args_co, ntys) <- normalise_tc_args tc tys
1318 ; return (args_co, mkTyConApp tc ntys) }
1319
1320 ---------------
1321 -- | Normalise arguments to a tycon
1322 normaliseTcArgs :: FamInstEnvs -- ^ env't with family instances
1323 -> Role -- ^ desired role of output coercion
1324 -> TyCon -- ^ tc
1325 -> [Type] -- ^ tys
1326 -> (Coercion, [Type]) -- ^ co :: tc tys ~ tc new_tys
1327 normaliseTcArgs env role tc tys
1328 = initNormM env role (tyCoVarsOfTypes tys) $
1329 normalise_tc_args tc tys
1330
1331 normalise_tc_args :: TyCon -> [Type] -- tc tys
1332 -> NormM (Coercion, [Type]) -- (co, new_tys), where
1333 -- co :: tc tys ~ tc new_tys
1334 normalise_tc_args tc tys
1335 = do { role <- getRole
1336 ; (cois, ntys) <- zipWithAndUnzipM normalise_type_role
1337 tys (tyConRolesX role tc)
1338 ; return (mkTyConAppCo role tc cois, ntys) }
1339 where
1340 normalise_type_role ty r = withRole r $ normalise_type ty
1341
1342 ---------------
1343 normaliseType :: FamInstEnvs
1344 -> Role -- desired role of coercion
1345 -> Type -> (Coercion, Type)
1346 normaliseType env role ty
1347 = initNormM env role (tyCoVarsOfType ty) $ normalise_type ty
1348
1349 normalise_type :: Type -- old type
1350 -> NormM (Coercion, Type) -- (coercion, new type), where
1351 -- co :: old-type ~ new_type
1352 -- Normalise the input type, by eliminating *all* type-function redexes
1353 -- but *not* newtypes (which are visible to the programmer)
1354 -- Returns with Refl if nothing happens
1355 -- Does nothing to newtypes
1356 -- The returned coercion *must* be *homogeneous*
1357 -- See Note [Normalising types]
1358 -- Try not to disturb type synonyms if possible
1359
1360 normalise_type ty
1361 = go ty
1362 where
1363 go (TyConApp tc tys) = normalise_tc_app tc tys
1364 go ty@(LitTy {}) = do { r <- getRole
1365 ; return (mkReflCo r ty, ty) }
1366 go (AppTy ty1 ty2)
1367 = do { (co, nty1) <- go ty1
1368 ; (arg, nty2) <- withRole Nominal $ go ty2
1369 ; return (mkAppCo co arg, mkAppTy nty1 nty2) }
1370 go (FunTy ty1 ty2)
1371 = do { (co1, nty1) <- go ty1
1372 ; (co2, nty2) <- go ty2
1373 ; r <- getRole
1374 ; return (mkFunCo r co1 co2, mkFunTy nty1 nty2) }
1375 go (ForAllTy (Bndr tcvar vis) ty)
1376 = do { (lc', tv', h, ki') <- normalise_var_bndr tcvar
1377 ; (co, nty) <- withLC lc' $ normalise_type ty
1378 ; let tv2 = setTyVarKind tv' ki'
1379 ; return (mkForAllCo tv' h co, ForAllTy (Bndr tv2 vis) nty) }
1380 go (TyVarTy tv) = normalise_tyvar tv
1381 go (CastTy ty co)
1382 = do { (nco, nty) <- go ty
1383 ; lc <- getLC
1384 ; let co' = substRightCo lc co
1385 ; return (castCoercionKind nco Nominal ty nty co co'
1386 , mkCastTy nty co') }
1387 go (CoercionTy co)
1388 = do { lc <- getLC
1389 ; r <- getRole
1390 ; let right_co = substRightCo lc co
1391 ; return ( mkProofIrrelCo r
1392 (liftCoSubst Nominal lc (coercionType co))
1393 co right_co
1394 , mkCoercionTy right_co ) }
1395
1396 normalise_tyvar :: TyVar -> NormM (Coercion, Type)
1397 normalise_tyvar tv
1398 = ASSERT( isTyVar tv )
1399 do { lc <- getLC
1400 ; r <- getRole
1401 ; return $ case liftCoSubstTyVar lc r tv of
1402 Just co -> (co, pSnd $ coercionKind co)
1403 Nothing -> (mkReflCo r ty, ty) }
1404 where ty = mkTyVarTy tv
1405
1406 normalise_var_bndr :: TyCoVar -> NormM (LiftingContext, TyCoVar, Coercion, Kind)
1407 normalise_var_bndr tcvar
1408 -- works for both tvar and covar
1409 = do { lc1 <- getLC
1410 ; env <- getEnv
1411 ; let callback lc ki = runNormM (normalise_type ki) env lc Nominal
1412 ; return $ liftCoSubstVarBndrUsing callback lc1 tcvar }
1413
1414 -- | a monad for the normalisation functions, reading 'FamInstEnvs',
1415 -- a 'LiftingContext', and a 'Role'.
1416 newtype NormM a = NormM { runNormM ::
1417 FamInstEnvs -> LiftingContext -> Role -> a }
1418
1419 initNormM :: FamInstEnvs -> Role
1420 -> TyCoVarSet -- the in-scope variables
1421 -> NormM a -> a
1422 initNormM env role vars (NormM thing_inside)
1423 = thing_inside env lc role
1424 where
1425 in_scope = mkInScopeSet vars
1426 lc = emptyLiftingContext in_scope
1427
1428 getRole :: NormM Role
1429 getRole = NormM (\ _ _ r -> r)
1430
1431 getLC :: NormM LiftingContext
1432 getLC = NormM (\ _ lc _ -> lc)
1433
1434 getEnv :: NormM FamInstEnvs
1435 getEnv = NormM (\ env _ _ -> env)
1436
1437 withRole :: Role -> NormM a -> NormM a
1438 withRole r thing = NormM $ \ envs lc _old_r -> runNormM thing envs lc r
1439
1440 withLC :: LiftingContext -> NormM a -> NormM a
1441 withLC lc thing = NormM $ \ envs _old_lc r -> runNormM thing envs lc r
1442
1443 instance Monad NormM where
1444 ma >>= fmb = NormM $ \env lc r ->
1445 let a = runNormM ma env lc r in
1446 runNormM (fmb a) env lc r
1447
1448 instance Functor NormM where
1449 fmap = liftM
1450 instance Applicative NormM where
1451 pure x = NormM $ \ _ _ _ -> x
1452 (<*>) = ap
1453
1454 {-
1455 ************************************************************************
1456 * *
1457 Flattening
1458 * *
1459 ************************************************************************
1460
1461 Note [Flattening]
1462 ~~~~~~~~~~~~~~~~~
1463 As described in "Closed type families with overlapping equations"
1464 http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
1465 we need to flatten core types before unifying them, when checking for "surely-apart"
1466 against earlier equations of a closed type family.
1467 Flattening means replacing all top-level uses of type functions with
1468 fresh variables, *taking care to preserve sharing*. That is, the type
1469 (Either (F a b) (F a b)) should flatten to (Either c c), never (Either
1470 c d).
1471
1472 Here is a nice example of why it's all necessary:
1473
1474 type family F a b where
1475 F Int Bool = Char
1476 F a b = Double
1477 type family G a -- open, no instances
1478
1479 How do we reduce (F (G Float) (G Float))? The first equation clearly doesn't match,
1480 while the second equation does. But, before reducing, we must make sure that the
1481 target can never become (F Int Bool). Well, no matter what G Float becomes, it
1482 certainly won't become *both* Int and Bool, so indeed we're safe reducing
1483 (F (G Float) (G Float)) to Double.
1484
1485 This is necessary not only to get more reductions (which we might be
1486 willing to give up on), but for substitutivity. If we have (F x x), we
1487 can see that (F x x) can reduce to Double. So, it had better be the
1488 case that (F blah blah) can reduce to Double, no matter what (blah)
1489 is! Flattening as done below ensures this.
1490
1491 flattenTys is defined here because of module dependencies.
1492 -}
1493
1494 data FlattenEnv = FlattenEnv { fe_type_map :: TypeMap TyVar
1495 , fe_subst :: TCvSubst }
1496
1497 emptyFlattenEnv :: InScopeSet -> FlattenEnv
1498 emptyFlattenEnv in_scope
1499 = FlattenEnv { fe_type_map = emptyTypeMap
1500 , fe_subst = mkEmptyTCvSubst in_scope }
1501
1502 -- See Note [Flattening]
1503 flattenTys :: InScopeSet -> [Type] -> [Type]
1504 flattenTys in_scope tys = snd $ coreFlattenTys env tys
1505 where
1506 -- when we hit a type function, we replace it with a fresh variable
1507 -- but, we need to make sure that this fresh variable isn't mentioned
1508 -- *anywhere* in the types we're flattening, even if locally-bound in
1509 -- a forall. That way, we can ensure consistency both within and outside
1510 -- of that forall.
1511 all_in_scope = in_scope `extendInScopeSetSet` allTyCoVarsInTys tys
1512 env = emptyFlattenEnv all_in_scope
1513
1514 coreFlattenTys :: FlattenEnv -> [Type] -> (FlattenEnv, [Type])
1515 coreFlattenTys = go []
1516 where
1517 go rtys env [] = (env, reverse rtys)
1518 go rtys env (ty : tys)
1519 = let (env', ty') = coreFlattenTy env ty in
1520 go (ty' : rtys) env' tys
1521
1522 coreFlattenTy :: FlattenEnv -> Type -> (FlattenEnv, Type)
1523 coreFlattenTy = go
1524 where
1525 go env ty | Just ty' <- coreView ty = go env ty'
1526
1527 go env (TyVarTy tv) = (env, substTyVar (fe_subst env) tv)
1528 go env (AppTy ty1 ty2) = let (env1, ty1') = go env ty1
1529 (env2, ty2') = go env1 ty2 in
1530 (env2, AppTy ty1' ty2')
1531 go env (TyConApp tc tys)
1532 -- NB: Don't just check if isFamilyTyCon: this catches *data* families,
1533 -- which are generative and thus can be preserved during flattening
1534 | not (isGenerativeTyCon tc Nominal)
1535 = let (env', tv) = coreFlattenTyFamApp env tc tys in
1536 (env', mkTyVarTy tv)
1537
1538 | otherwise
1539 = let (env', tys') = coreFlattenTys env tys in
1540 (env', mkTyConApp tc tys')
1541
1542 go env (FunTy ty1 ty2) = let (env1, ty1') = go env ty1
1543 (env2, ty2') = go env1 ty2 in
1544 (env2, mkFunTy ty1' ty2')
1545
1546 go env (ForAllTy (Bndr tv vis) ty)
1547 = let (env1, tv') = coreFlattenVarBndr env tv
1548 (env2, ty') = go env1 ty in
1549 (env2, ForAllTy (Bndr tv' vis) ty')
1550
1551 go env ty@(LitTy {}) = (env, ty)
1552
1553 go env (CastTy ty co) = let (env1, ty') = go env ty
1554 (env2, co') = coreFlattenCo env1 co in
1555 (env2, CastTy ty' co')
1556
1557 go env (CoercionTy co) = let (env', co') = coreFlattenCo env co in
1558 (env', CoercionTy co')
1559
1560 -- when flattening, we don't care about the contents of coercions.
1561 -- so, just return a fresh variable of the right (flattened) type
1562 coreFlattenCo :: FlattenEnv -> Coercion -> (FlattenEnv, Coercion)
1563 coreFlattenCo env co
1564 = (env2, mkCoVarCo covar)
1565 where
1566 (env1, kind') = coreFlattenTy env (coercionType co)
1567 fresh_name = mkFlattenFreshCoName
1568 subst1 = fe_subst env1
1569 in_scope = getTCvInScope subst1
1570 covar = uniqAway in_scope (mkCoVar fresh_name kind')
1571 env2 = env1 { fe_subst = subst1 `extendTCvInScope` covar }
1572
1573 coreFlattenVarBndr :: FlattenEnv -> TyCoVar -> (FlattenEnv, TyCoVar)
1574 coreFlattenVarBndr env tv
1575 | kind' `eqType` kind
1576 = ( env { fe_subst = extendTCvSubst old_subst tv (mkTyCoVarTy tv) }
1577 -- override any previous binding for tv
1578 , tv)
1579
1580 | otherwise
1581 = let new_tv = uniqAway (getTCvInScope old_subst) (setVarType tv kind')
1582 new_subst = extendTCvSubstWithClone old_subst tv new_tv
1583 in
1584 (env' { fe_subst = new_subst }, new_tv)
1585 where
1586 kind = varType tv
1587 (env', kind') = coreFlattenTy env kind
1588 old_subst = fe_subst env
1589
1590 coreFlattenTyFamApp :: FlattenEnv
1591 -> TyCon -- type family tycon
1592 -> [Type] -- args
1593 -> (FlattenEnv, TyVar)
1594 coreFlattenTyFamApp env fam_tc fam_args
1595 = case lookupTypeMap type_map fam_ty of
1596 Just tv -> (env, tv)
1597 -- we need fresh variables here, but this is called far from
1598 -- any good source of uniques. So, we just use the fam_tc's unique
1599 -- and trust uniqAway to avoid clashes. Recall that the in_scope set
1600 -- contains *all* tyvars, even locally bound ones elsewhere in the
1601 -- overall type, so this really is fresh.
1602 Nothing -> let tyvar_name = mkFlattenFreshTyName fam_tc
1603 tv = uniqAway (getTCvInScope subst) $
1604 mkTyVar tyvar_name (typeKind fam_ty)
1605 env' = env { fe_type_map = extendTypeMap type_map fam_ty tv
1606 , fe_subst = extendTCvInScope subst tv }
1607 in (env', tv)
1608 where fam_ty = mkTyConApp fam_tc fam_args
1609 FlattenEnv { fe_type_map = type_map
1610 , fe_subst = subst } = env
1611
1612 -- | Get the set of all type/coercion variables mentioned anywhere in the list
1613 -- of types. These variables are not necessarily free.
1614 allTyCoVarsInTys :: [Type] -> VarSet
1615 allTyCoVarsInTys [] = emptyVarSet
1616 allTyCoVarsInTys (ty:tys) = allTyCoVarsInTy ty `unionVarSet` allTyCoVarsInTys tys
1617
1618 -- | Get the set of all type/coercion variables mentioned anywhere in a type.
1619 allTyCoVarsInTy :: Type -> VarSet
1620 allTyCoVarsInTy = go
1621 where
1622 go (TyVarTy tv) = unitVarSet tv
1623 go (TyConApp _ tys) = allTyCoVarsInTys tys
1624 go (AppTy ty1 ty2) = (go ty1) `unionVarSet` (go ty2)
1625 go (FunTy ty1 ty2) = (go ty1) `unionVarSet` (go ty2)
1626 go (ForAllTy (Bndr tv _) ty) = unitVarSet tv `unionVarSet`
1627 go (tyVarKind tv) `unionVarSet`
1628 go ty
1629 -- Don't remove the tv from the set!
1630 go (LitTy {}) = emptyVarSet
1631 go (CastTy ty co) = go ty `unionVarSet` go_co co
1632 go (CoercionTy co) = go_co co
1633
1634 go_mco MRefl = emptyVarSet
1635 go_mco (MCo co) = go_co co
1636
1637 go_co (Refl ty) = go ty
1638 go_co (GRefl _ ty mco) = go ty `unionVarSet` go_mco mco
1639 go_co (TyConAppCo _ _ args) = go_cos args
1640 go_co (AppCo co arg) = go_co co `unionVarSet` go_co arg
1641 go_co (ForAllCo tv h co)
1642 = unionVarSets [unitVarSet tv, go_co co, go_co h]
1643 go_co (FunCo _ c1 c2) = go_co c1 `unionVarSet` go_co c2
1644 go_co (CoVarCo cv) = unitVarSet cv
1645 go_co (HoleCo h) = unitVarSet (coHoleCoVar h)
1646 go_co (AxiomInstCo _ _ cos) = go_cos cos
1647 go_co (UnivCo p _ t1 t2) = go_prov p `unionVarSet` go t1 `unionVarSet` go t2
1648 go_co (SymCo co) = go_co co
1649 go_co (TransCo c1 c2) = go_co c1 `unionVarSet` go_co c2
1650 go_co (NthCo _ _ co) = go_co co
1651 go_co (LRCo _ co) = go_co co
1652 go_co (InstCo co arg) = go_co co `unionVarSet` go_co arg
1653 go_co (KindCo co) = go_co co
1654 go_co (SubCo co) = go_co co
1655 go_co (AxiomRuleCo _ cs) = go_cos cs
1656
1657 go_cos = foldr (unionVarSet . go_co) emptyVarSet
1658
1659 go_prov UnsafeCoerceProv = emptyVarSet
1660 go_prov (PhantomProv co) = go_co co
1661 go_prov (ProofIrrelProv co) = go_co co
1662 go_prov (PluginProv _) = emptyVarSet
1663
1664 mkFlattenFreshTyName :: Uniquable a => a -> Name
1665 mkFlattenFreshTyName unq
1666 = mkSysTvName (getUnique unq) (fsLit "flt")
1667
1668 mkFlattenFreshCoName :: Name
1669 mkFlattenFreshCoName
1670 = mkSystemVarName (deriveUnique eqPrimTyConKey 71) (fsLit "flc")