never executed always true always false
1 {-# LANGUAGE DeriveFunctor #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE ScopedTypeVariables #-}
4 {-# LANGUAGE TupleSections #-}
5
6 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
7 -- (c) The University of Glasgow 2006
8 --
9 -- FamInstEnv: Type checked family instance declarations
10
11 module GHC.Core.FamInstEnv (
12 FamInst(..), FamFlavor(..), famInstAxiom, famInstTyCon, famInstRHS,
13 famInstsRepTyCons, famInstRepTyCon_maybe, dataFamInstRepTyCon,
14 pprFamInst, pprFamInsts,
15 mkImportedFamInst,
16
17 FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs,
18 extendFamInstEnv, extendFamInstEnvList,
19 famInstEnvElts, famInstEnvSize, familyInstances,
20
21 -- * CoAxioms
22 mkCoAxBranch, mkBranchedCoAxiom, mkUnbranchedCoAxiom, mkSingleCoAxiom,
23 mkNewTypeCoAxiom,
24
25 FamInstMatch(..),
26 lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvByTyCon,
27
28 isDominatedBy, apartnessCheck,
29
30 -- Injectivity
31 InjectivityCheckResult(..),
32 lookupFamInstEnvInjectivityConflicts, injectiveBranches,
33
34 -- Normalisation
35 topNormaliseType, topNormaliseType_maybe,
36 normaliseType, normaliseTcApp,
37 topReduceTyFamApp_maybe, reduceTyFamApp_maybe
38 ) where
39
40 import GHC.Prelude
41
42 import GHC.Core.Unify
43 import GHC.Core.Type as Type
44 import GHC.Core.TyCo.Rep
45 import GHC.Core.TyCon
46 import GHC.Core.Coercion
47 import GHC.Core.Coercion.Axiom
48 import GHC.Core.Reduction
49 import GHC.Types.Var.Set
50 import GHC.Types.Var.Env
51 import GHC.Types.Name
52 import GHC.Types.Unique.DFM
53 import GHC.Data.Maybe
54 import GHC.Types.Var
55 import GHC.Types.SrcLoc
56 import Control.Monad
57 import Data.List( mapAccumL )
58 import Data.Array( Array, assocs )
59
60 import GHC.Utils.Misc
61 import GHC.Utils.Outputable
62 import GHC.Utils.Panic
63 import GHC.Utils.Panic.Plain
64
65 {-
66 ************************************************************************
67 * *
68 Type checked family instance heads
69 * *
70 ************************************************************************
71
72 Note [FamInsts and CoAxioms]
73 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
74 * CoAxioms and FamInsts are just like
75 DFunIds and ClsInsts
76
77 * A CoAxiom is a System-FC thing: it can relate any two types
78
79 * A FamInst is a Haskell source-language thing, corresponding
80 to a type/data family instance declaration.
81 - The FamInst contains a CoAxiom, which is the evidence
82 for the instance
83
84 - The LHS of the CoAxiom is always of form F ty1 .. tyn
85 where F is a type family
86 -}
87
88 data FamInst -- See Note [FamInsts and CoAxioms]
89 = FamInst { fi_axiom :: CoAxiom Unbranched -- The new coercion axiom
90 -- introduced by this family
91 -- instance
92 -- INVARIANT: apart from freshening (see below)
93 -- fi_tvs = cab_tvs of the (single) axiom branch
94 -- fi_cvs = cab_cvs ...ditto...
95 -- fi_tys = cab_lhs ...ditto...
96 -- fi_rhs = cab_rhs ...ditto...
97
98 , fi_flavor :: FamFlavor
99
100 -- Everything below here is a redundant,
101 -- cached version of the two things above
102 -- except that the TyVars are freshened
103 , fi_fam :: Name -- Family name
104
105 -- Used for "rough matching"; same idea as for class instances
106 -- See Note [Rough matching in class and family instances]
107 -- in GHC.Core.Unify
108 , fi_tcs :: [RoughMatchTc] -- Top of type args
109 -- INVARIANT: fi_tcs = roughMatchTcs fi_tys
110
111 -- Used for "proper matching"; ditto
112 , fi_tvs :: [TyVar] -- Template tyvars for full match
113 , fi_cvs :: [CoVar] -- Template covars for full match
114 -- Like ClsInsts, these variables are always fresh
115 -- See Note [Template tyvars are fresh] in GHC.Core.InstEnv
116
117 , fi_tys :: [Type] -- The LHS type patterns
118 -- May be eta-reduced; see Note [Eta reduction for data families]
119 -- in GHC.Core.Coercion.Axiom
120
121 , fi_rhs :: Type -- the RHS, with its freshened vars
122 }
123
124 data FamFlavor
125 = SynFamilyInst -- A synonym family
126 | DataFamilyInst TyCon -- A data family, with its representation TyCon
127
128 {-
129 Note [Arity of data families]
130 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
131 Data family instances might legitimately be over- or under-saturated.
132
133 Under-saturation has two potential causes:
134 U1) Eta reduction. See Note [Eta reduction for data families] in
135 GHC.Core.Coercion.Axiom.
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] in GHC.Core.Coercion.Axiom.
164 Accordingly, the FamInst 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 GHC.Types.TyThing.Ppr.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 GHC.IfaceToCore. 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 -> [RoughMatchTc] -- 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 GHC.Core.Opt.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] in GHC.Core.Coercion.Axiom
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 -- Internally we sometimes index by Name instead of TyCon despite
354 -- of what the type says. This is safe since
355 -- getUnique (tyCon) == getUniqe (tcName tyCon)
356 type FamInstEnv = UniqDFM TyCon FamilyInstEnv -- Maps a family to its instances
357 -- See Note [FamInstEnv]
358 -- See Note [FamInstEnv determinism]
359
360 type FamInstEnvs = (FamInstEnv, FamInstEnv)
361 -- External package inst-env, Home-package inst-env
362
363 newtype FamilyInstEnv
364 = FamIE [FamInst] -- The instances for a particular family, in any order
365
366 instance Outputable FamilyInstEnv where
367 ppr (FamIE fs) = text "FamIE" <+> vcat (map ppr fs)
368
369 -- | Index a FamInstEnv by the tyCons name.
370 toNameInstEnv :: FamInstEnv -> UniqDFM Name FamilyInstEnv
371 toNameInstEnv = unsafeCastUDFMKey
372
373 -- | Create a FamInstEnv from Name indices.
374 fromNameInstEnv :: UniqDFM Name FamilyInstEnv -> FamInstEnv
375 fromNameInstEnv = unsafeCastUDFMKey
376
377 -- INVARIANTS:
378 -- * The fs_tvs are distinct in each FamInst
379 -- of a range value of the map (so we can safely unify them)
380
381 emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
382 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
383
384 emptyFamInstEnv :: FamInstEnv
385 emptyFamInstEnv = emptyUDFM
386
387 famInstEnvElts :: FamInstEnv -> [FamInst]
388 famInstEnvElts fi = [elt | FamIE elts <- eltsUDFM fi, elt <- elts]
389 -- See Note [FamInstEnv determinism]
390
391 famInstEnvSize :: FamInstEnv -> Int
392 famInstEnvSize = nonDetStrictFoldUDFM (\(FamIE elt) sum -> sum + length elt) 0
393 -- It's OK to use nonDetStrictFoldUDFM here since we're just computing the
394 -- size.
395
396 familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
397 familyInstances (pkg_fie, home_fie) fam
398 = get home_fie ++ get pkg_fie
399 where
400 get env = case lookupUDFM env fam of
401 Just (FamIE insts) -> insts
402 Nothing -> []
403
404 extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
405 extendFamInstEnvList inst_env fis = foldl' extendFamInstEnv inst_env fis
406
407 extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
408 extendFamInstEnv inst_env
409 ins_item@(FamInst {fi_fam = cls_nm})
410 = fromNameInstEnv $ addToUDFM_C add (toNameInstEnv inst_env) cls_nm (FamIE [ins_item])
411 where
412 add (FamIE items) _ = FamIE (ins_item:items)
413
414 {-
415 ************************************************************************
416 * *
417 Compatibility
418 * *
419 ************************************************************************
420
421 Note [Apartness]
422 ~~~~~~~~~~~~~~~~
423 In dealing with closed type families, we must be able to check that one type
424 will never reduce to another. This check is called /apartness/. The check
425 is always between a target (which may be an arbitrary type) and a pattern.
426 Here is how we do it:
427
428 apart(target, pattern) = not (unify(flatten(target), pattern))
429
430 where flatten (implemented in flattenTys, below) converts all type-family
431 applications into fresh variables. (See
432 Note [Flattening type-family applications when matching instances] in GHC.Core.Unify.)
433
434 Note [Compatibility]
435 ~~~~~~~~~~~~~~~~~~~~
436 Two patterns are /compatible/ if either of the following conditions hold:
437 1) The patterns are apart.
438 2) The patterns unify with a substitution S, and their right hand sides
439 equal under that substitution.
440
441 For open type families, only compatible instances are allowed. For closed
442 type families, the story is slightly more complicated. Consider the following:
443
444 type family F a where
445 F Int = Bool
446 F a = Int
447
448 g :: Show a => a -> F a
449 g x = length (show x)
450
451 Should that type-check? No. We need to allow for the possibility that 'a'
452 might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int
453 only when we can be sure that 'a' is not Int.
454
455 To achieve this, after finding a possible match within the equations, we have to
456 go back to all previous equations and check that, under the
457 substitution induced by the match, other branches are surely apart. (See
458 Note [Apartness].) This is similar to what happens with class
459 instance selection, when we need to guarantee that there is only a match and
460 no unifiers. The exact algorithm is different here because the
461 potentially-overlapping group is closed.
462
463 As another example, consider this:
464
465 type family G x where
466 G Int = Bool
467 G a = Double
468
469 type family H y
470 -- no instances
471
472 Now, we want to simplify (G (H Char)). We can't, because (H Char) might later
473 simplify to be Int. So, (G (H Char)) is stuck, for now.
474
475 While everything above is quite sound, it isn't as expressive as we'd like.
476 Consider this:
477
478 type family J a where
479 J Int = Int
480 J a = a
481
482 Can we simplify (J b) to b? Sure we can. Yes, the first equation matches if
483 b is instantiated with Int, but the RHSs coincide there, so it's all OK.
484
485 So, the rule is this: when looking up a branch in a closed type family, we
486 find a branch that matches the target, but then we make sure that the target
487 is apart from every previous *incompatible* branch. We don't check the
488 branches that are compatible with the matching branch, because they are either
489 irrelevant (clause 1 of compatible) or benign (clause 2 of compatible).
490
491 Note [Compatibility of eta-reduced axioms]
492 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
493 In newtype instances of data families we eta-reduce the axioms,
494 See Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom. This means that
495 we sometimes need to test compatibility of two axioms that were eta-reduced to
496 different degrees, e.g.:
497
498
499 data family D a b c
500 newtype instance D a Int c = DInt (Maybe a)
501 -- D a Int ~ Maybe
502 -- lhs = [a, Int]
503 newtype instance D Bool Int Char = DIntChar Float
504 -- D Bool Int Char ~ Float
505 -- lhs = [Bool, Int, Char]
506
507 These are obviously incompatible. We could detect this by saturating
508 (eta-expanding) the shorter LHS with fresh tyvars until the lists are of
509 equal length, but instead we can just remove the tail of the longer list, as
510 those types will simply unify with the freshly introduced tyvars.
511
512 By doing this, in case the LHS are unifiable, the yielded substitution won't
513 mention the tyvars that appear in the tail we dropped off, and we might try
514 to test equality RHSes of different kinds, but that's fine since this case
515 occurs only for data families, where the RHS is a unique tycon and the equality
516 fails anyway.
517 -}
518
519 -- See Note [Compatibility]
520 compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
521 compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
522 (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
523 = let (commonlhs1, commonlhs2) = zipAndUnzip lhs1 lhs2
524 -- See Note [Compatibility of eta-reduced axioms]
525 in case tcUnifyTysFG alwaysBindFun commonlhs1 commonlhs2 of
526 SurelyApart -> True
527 Unifiable subst
528 | Type.substTyAddInScope subst rhs1 `eqType`
529 Type.substTyAddInScope subst rhs2
530 -> True
531 _ -> False
532
533 -- | Result of testing two type family equations for injectiviy.
534 data InjectivityCheckResult
535 = InjectivityAccepted
536 -- ^ Either RHSs are distinct or unification of RHSs leads to unification of
537 -- LHSs
538 | InjectivityUnified CoAxBranch CoAxBranch
539 -- ^ RHSs unify but LHSs don't unify under that substitution. Relevant for
540 -- closed type families where equation after unification might be
541 -- overlpapped (in which case it is OK if they don't unify). Constructor
542 -- stores axioms after unification.
543
544 -- | Check whether two type family axioms don't violate injectivity annotation.
545 injectiveBranches :: [Bool] -> CoAxBranch -> CoAxBranch
546 -> InjectivityCheckResult
547 injectiveBranches injectivity
548 ax1@(CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
549 ax2@(CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
550 -- See Note [Verifying injectivity annotation], case 1.
551 = let getInjArgs = filterByList injectivity
552 in case tcUnifyTyWithTFs True rhs1 rhs2 of -- True = two-way pre-unification
553 Nothing -> InjectivityAccepted
554 -- RHS are different, so equations are injective.
555 -- This is case 1A from Note [Verifying injectivity annotation]
556 Just subst -> -- RHS unify under a substitution
557 let lhs1Subst = Type.substTys subst (getInjArgs lhs1)
558 lhs2Subst = Type.substTys subst (getInjArgs lhs2)
559 -- If LHSs are equal under the substitution used for RHSs then this pair
560 -- of equations does not violate injectivity annotation. If LHSs are not
561 -- equal under that substitution then this pair of equations violates
562 -- injectivity annotation, but for closed type families it still might
563 -- be the case that one LHS after substitution is unreachable.
564 in if eqTypes lhs1Subst lhs2Subst -- check case 1B1 from Note.
565 then InjectivityAccepted
566 else InjectivityUnified ( ax1 { cab_lhs = Type.substTys subst lhs1
567 , cab_rhs = Type.substTy subst rhs1 })
568 ( ax2 { cab_lhs = Type.substTys subst lhs2
569 , cab_rhs = Type.substTy subst rhs2 })
570 -- payload of InjectivityUnified used only for check 1B2, only
571 -- for closed type families
572
573 -- takes a CoAxiom with unknown branch incompatibilities and computes
574 -- the compatibilities
575 -- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom
576 computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch]
577 computeAxiomIncomps branches
578 = snd (mapAccumL go [] branches)
579 where
580 go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
581 go prev_brs cur_br
582 = (cur_br : prev_brs, new_br)
583 where
584 new_br = cur_br { cab_incomps = mk_incomps prev_brs cur_br }
585
586 mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch]
587 mk_incomps prev_brs cur_br
588 = filter (not . compatibleBranches cur_br) prev_brs
589
590 {-
591 ************************************************************************
592 * *
593 Constructing axioms
594 These functions are here because tidyType / tcUnifyTysFG
595 are not available in GHC.Core.Coercion.Axiom
596
597 Also computeAxiomIncomps is too sophisticated for CoAxiom
598 * *
599 ************************************************************************
600
601 Note [Tidy axioms when we build them]
602 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
603 Like types and classes, we build axioms fully quantified over all
604 their variables, and tidy them when we build them. For example,
605 we print out axioms and don't want to print stuff like
606 F k k a b = ...
607 Instead we must tidy those kind variables. See #7524.
608
609 We could instead tidy when we print, but that makes it harder to get
610 things like injectivity errors to come out right. Danger of
611 Type family equation violates injectivity annotation.
612 Kind variable âkâ cannot be inferred from the right-hand side.
613 In the type family equation:
614 PolyKindVars @[k1] @[k2] ('[] @k1) = '[] @k2
615
616 Note [Always number wildcard types in CoAxBranch]
617 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
618 Consider the following example (from the DataFamilyInstanceLHS test case):
619
620 data family Sing (a :: k)
621 data instance Sing (_ :: MyKind) where
622 SingA :: Sing A
623 SingB :: Sing B
624
625 If we're not careful during tidying, then when this program is compiled with
626 -ddump-types, we'll get the following information:
627
628 COERCION AXIOMS
629 axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 ::
630 Sing _ = DataFamilyInstanceLHS.R:SingMyKind_ _
631
632 It's misleading to have a wildcard type appearing on the RHS like
633 that. To avoid this issue, when building a CoAxiom (which is what eventually
634 gets printed above), we tidy all the variables in an env that already contains
635 '_'. Thus, any variable named '_' will be renamed, giving us the nicer output
636 here:
637
638 COERCION AXIOMS
639 axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 ::
640 Sing _1 = DataFamilyInstanceLHS.R:SingMyKind_ _1
641
642 Which is at least legal syntax.
643
644 See also Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom; note that we
645 are tidying (changing OccNames only), not freshening, in accordance with
646 that Note.
647 -}
648
649 -- all axiom roles are Nominal, as this is only used with type families
650 mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
651 -> [TyVar] -- Extra eta tyvars
652 -> [CoVar] -- possibly stale covars
653 -> [Type] -- LHS patterns
654 -> Type -- RHS
655 -> [Role]
656 -> SrcSpan
657 -> CoAxBranch
658 mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc
659 = CoAxBranch { cab_tvs = tvs'
660 , cab_eta_tvs = eta_tvs'
661 , cab_cvs = cvs'
662 , cab_lhs = tidyTypes env lhs
663 , cab_roles = roles
664 , cab_rhs = tidyType env rhs
665 , cab_loc = loc
666 , cab_incomps = placeHolderIncomps }
667 where
668 (env1, tvs') = tidyVarBndrs init_tidy_env tvs
669 (env2, eta_tvs') = tidyVarBndrs env1 eta_tvs
670 (env, cvs') = tidyVarBndrs env2 cvs
671 -- See Note [Tidy axioms when we build them]
672 -- See also Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom
673
674 init_occ_env = initTidyOccEnv [mkTyVarOcc "_"]
675 init_tidy_env = mkEmptyTidyEnv init_occ_env
676 -- See Note [Always number wildcard types in CoAxBranch]
677
678 -- all of the following code is here to avoid mutual dependencies with
679 -- Coercion
680 mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
681 mkBranchedCoAxiom ax_name fam_tc branches
682 = CoAxiom { co_ax_unique = nameUnique ax_name
683 , co_ax_name = ax_name
684 , co_ax_tc = fam_tc
685 , co_ax_role = Nominal
686 , co_ax_implicit = False
687 , co_ax_branches = manyBranches (computeAxiomIncomps branches) }
688
689 mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched
690 mkUnbranchedCoAxiom ax_name fam_tc branch
691 = CoAxiom { co_ax_unique = nameUnique ax_name
692 , co_ax_name = ax_name
693 , co_ax_tc = fam_tc
694 , co_ax_role = Nominal
695 , co_ax_implicit = False
696 , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
697
698 mkSingleCoAxiom :: Role -> Name
699 -> [TyVar] -> [TyVar] -> [CoVar]
700 -> TyCon -> [Type] -> Type
701 -> CoAxiom Unbranched
702 -- Make a single-branch CoAxiom, including making the branch itself
703 -- Used for both type family (Nominal) and data family (Representational)
704 -- axioms, hence passing in the Role
705 mkSingleCoAxiom role ax_name tvs eta_tvs cvs fam_tc lhs_tys rhs_ty
706 = CoAxiom { co_ax_unique = nameUnique ax_name
707 , co_ax_name = ax_name
708 , co_ax_tc = fam_tc
709 , co_ax_role = role
710 , co_ax_implicit = False
711 , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
712 where
713 branch = mkCoAxBranch tvs eta_tvs cvs lhs_tys rhs_ty
714 (map (const Nominal) tvs)
715 (getSrcSpan ax_name)
716
717 -- | Create a coercion constructor (axiom) suitable for the given
718 -- newtype 'TyCon'. The 'Name' should be that of a new coercion
719 -- 'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and
720 -- the type the appropriate right hand side of the @newtype@, with
721 -- the free variables a subset of those 'TyVar's.
722 mkNewTypeCoAxiom :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched
723 mkNewTypeCoAxiom name tycon tvs roles rhs_ty
724 = CoAxiom { co_ax_unique = nameUnique name
725 , co_ax_name = name
726 , co_ax_implicit = True -- See Note [Implicit axioms] in GHC.Core.TyCon
727 , co_ax_role = Representational
728 , co_ax_tc = tycon
729 , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
730 where
731 branch = mkCoAxBranch tvs [] [] (mkTyVarTys tvs) rhs_ty
732 roles (getSrcSpan name)
733
734 {-
735 ************************************************************************
736 * *
737 Looking up a family instance
738 * *
739 ************************************************************************
740
741 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
742 Multiple matches are only possible in case of type families (not data
743 families), and then, it doesn't matter which match we choose (as the
744 instances are guaranteed confluent).
745
746 We return the matching family instances and the type instance at which it
747 matches. For example, if we lookup 'T [Int]' and have a family instance
748
749 data instance T [a] = ..
750
751 desugared to
752
753 data :R42T a = ..
754 coe :Co:R42T a :: T [a] ~ :R42T a
755
756 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
757 -}
758
759 -- when matching a type family application, we get a FamInst,
760 -- and the list of types the axiom should be applied to
761 data FamInstMatch = FamInstMatch { fim_instance :: FamInst
762 , fim_tys :: [Type]
763 , fim_cos :: [Coercion]
764 }
765 -- See Note [Over-saturated matches]
766
767 instance Outputable FamInstMatch where
768 ppr (FamInstMatch { fim_instance = inst
769 , fim_tys = tys
770 , fim_cos = cos })
771 = text "match with" <+> parens (ppr inst) <+> ppr tys <+> ppr cos
772
773 lookupFamInstEnvByTyCon :: FamInstEnvs -> TyCon -> [FamInst]
774 lookupFamInstEnvByTyCon (pkg_ie, home_ie) fam_tc
775 = get pkg_ie ++ get home_ie
776 where
777 get ie = case lookupUDFM ie fam_tc of
778 Nothing -> []
779 Just (FamIE fis) -> fis
780
781 lookupFamInstEnv
782 :: FamInstEnvs
783 -> TyCon -> [Type] -- What we are looking for
784 -> [FamInstMatch] -- Successful matches
785 -- Precondition: the tycon is saturated (or over-saturated)
786
787 lookupFamInstEnv
788 = lookup_fam_inst_env match
789 where
790 match _ _ tpl_tys tys = tcMatchTys tpl_tys tys
791
792 lookupFamInstEnvConflicts
793 :: FamInstEnvs
794 -> FamInst -- Putative new instance
795 -> [FamInstMatch] -- Conflicting matches (don't look at the fim_tys field)
796 -- E.g. when we are about to add
797 -- f : type instance F [a] = a->a
798 -- we do (lookupFamInstConflicts f [b])
799 -- to find conflicting matches
800 --
801 -- Precondition: the tycon is saturated (or over-saturated)
802
803 lookupFamInstEnvConflicts envs fam_inst@(FamInst { fi_axiom = new_axiom })
804 = lookup_fam_inst_env my_unify envs fam tys
805 where
806 (fam, tys) = famInstSplitLHS fam_inst
807 -- In example above, fam tys' = F [b]
808
809 my_unify (FamInst { fi_axiom = old_axiom }) tpl_tvs tpl_tys _
810 = assertPpr (tyCoVarsOfTypes tys `disjointVarSet` tpl_tvs)
811 ((ppr fam <+> ppr tys) $$
812 (ppr tpl_tvs <+> ppr tpl_tys)) $
813 -- Unification will break badly if the variables overlap
814 -- They shouldn't because we allocate separate uniques for them
815 if compatibleBranches (coAxiomSingleBranch old_axiom) new_branch
816 then Nothing
817 else Just noSubst
818 -- Note [Family instance overlap conflicts]
819
820 noSubst = panic "lookupFamInstEnvConflicts noSubst"
821 new_branch = coAxiomSingleBranch new_axiom
822
823 --------------------------------------------------------------------------------
824 -- Type family injectivity checking bits --
825 --------------------------------------------------------------------------------
826
827 {- Note [Verifying injectivity annotation]
828 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
829
830 Injectivity means that the RHS of a type family uniquely determines the LHS (see
831 Note [Type inference for type families with injectivity]). The user informs us about
832 injectivity using an injectivity annotation and it is GHC's task to verify that
833 this annotation is correct w.r.t. type family equations. Whenever we see a new
834 equation of a type family we need to make sure that adding this equation to the
835 already known equations of a type family does not violate the injectivity annotation
836 supplied by the user (see Note [Injectivity annotation]). Of course if the type
837 family has no injectivity annotation then no check is required. But if a type
838 family has injectivity annotation we need to make sure that the following
839 conditions hold:
840
841 1. For each pair of *different* equations of a type family, one of the following
842 conditions holds:
843
844 A: RHSs are different. (Check done in GHC.Core.FamInstEnv.injectiveBranches)
845
846 B1: OPEN TYPE FAMILIES: If the RHSs can be unified under some substitution
847 then it must be possible to unify the LHSs under the same substitution.
848 Example:
849
850 type family FunnyId a = r | r -> a
851 type instance FunnyId Int = Int
852 type instance FunnyId a = a
853
854 RHSs of these two equations unify under [ a |-> Int ] substitution.
855 Under this substitution LHSs are equal therefore these equations don't
856 violate injectivity annotation. (Check done in GHC.Core.FamInstEnv.injectiveBranches)
857
858 B2: CLOSED TYPE FAMILIES: If the RHSs can be unified under some
859 substitution then either the LHSs unify under the same substitution or
860 the LHS of the latter equation is overlapped by earlier equations.
861 Example 1:
862
863 type family SwapIntChar a = r | r -> a where
864 SwapIntChar Int = Char
865 SwapIntChar Char = Int
866 SwapIntChar a = a
867
868 Say we are checking the last two equations. RHSs unify under [ a |->
869 Int ] substitution but LHSs don't. So we apply the substitution to LHS
870 of last equation and check whether it is overlapped by any of previous
871 equations. Since it is overlapped by the first equation we conclude
872 that pair of last two equations does not violate injectivity
873 annotation. (Check done in GHC.Tc.Validity.checkValidCoAxiom#gather_conflicts)
874
875 A special case of B is when RHSs unify with an empty substitution ie. they
876 are identical.
877
878 If any of the above two conditions holds we conclude that the pair of
879 equations does not violate injectivity annotation. But if we find a pair
880 of equations where neither of the above holds we report that this pair
881 violates injectivity annotation because for a given RHS we don't have a
882 unique LHS. (Note that (B) actually implies (A).)
883
884 Note that we only take into account these LHS patterns that were declared
885 as injective.
886
887 2. If an RHS of a type family equation is a bare type variable then
888 all LHS variables (including implicit kind variables) also have to be bare.
889 In other words, this has to be a sole equation of that type family and it has
890 to cover all possible patterns. So for example this definition will be
891 rejected:
892
893 type family W1 a = r | r -> a
894 type instance W1 [a] = a
895
896 If it were accepted we could call `W1 [W1 Int]`, which would reduce to
897 `W1 Int` and then by injectivity we could conclude that `[W1 Int] ~ Int`,
898 which is bogus. Checked FamInst.bareTvInRHSViolated.
899
900 3. If the RHS of a type family equation is a type family application then the type
901 family is rejected as not injective. This is checked by FamInst.isTFHeaded.
902
903 4. If a LHS type variable that is declared as injective is not mentioned in an
904 injective position in the RHS then the type family is rejected as not
905 injective. "Injective position" means either an argument to a type
906 constructor or argument to a type family on injective position.
907 There are subtleties here. See Note [Coverage condition for injective type families]
908 in GHC.Tc.Instance.Family.
909
910 Check (1) must be done for all family instances (transitively) imported. Other
911 checks (2-4) should be done just for locally written equations, as they are checks
912 involving just a single equation, not about interactions. Doing the other checks for
913 imported equations led to #17405, as the behavior of check (4) depends on
914 -XUndecidableInstances (see Note [Coverage condition for injective type families] in
915 FamInst), which may vary between modules.
916
917 See also Note [Injective type families] in GHC.Core.TyCon
918 -}
919
920
921 -- | Check whether an open type family equation can be added to already existing
922 -- instance environment without causing conflicts with supplied injectivity
923 -- annotations. Returns list of conflicting axioms (type instance
924 -- declarations).
925 lookupFamInstEnvInjectivityConflicts
926 :: [Bool] -- injectivity annotation for this type family instance
927 -- INVARIANT: list contains at least one True value
928 -> FamInstEnvs -- all type instances seens so far
929 -> FamInst -- new type instance that we're checking
930 -> [CoAxBranch] -- conflicting instance declarations
931 lookupFamInstEnvInjectivityConflicts injList (pkg_ie, home_ie)
932 fam_inst@(FamInst { fi_axiom = new_axiom })
933 -- See Note [Verifying injectivity annotation]. This function implements
934 -- check (1.B1) for open type families described there.
935 = lookup_inj_fam_conflicts home_ie ++ lookup_inj_fam_conflicts pkg_ie
936 where
937 fam = famInstTyCon fam_inst
938 new_branch = coAxiomSingleBranch new_axiom
939
940 -- filtering function used by `lookup_inj_fam_conflicts` to check whether
941 -- a pair of equations conflicts with the injectivity annotation.
942 isInjConflict (FamInst { fi_axiom = old_axiom })
943 | InjectivityAccepted <-
944 injectiveBranches injList (coAxiomSingleBranch old_axiom) new_branch
945 = False -- no conflict
946 | otherwise = True
947
948 lookup_inj_fam_conflicts ie
949 | isOpenFamilyTyCon fam, Just (FamIE insts) <- lookupUDFM ie fam
950 = map (coAxiomSingleBranch . fi_axiom) $
951 filter isInjConflict insts
952 | otherwise = []
953
954
955 --------------------------------------------------------------------------------
956 -- Type family overlap checking bits --
957 --------------------------------------------------------------------------------
958
959 {-
960 Note [Family instance overlap conflicts]
961 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
962 - In the case of data family instances, any overlap is fundamentally a
963 conflict (as these instances imply injective type mappings).
964
965 - In the case of type family instances, overlap is admitted as long as
966 the right-hand sides of the overlapping rules coincide under the
967 overlap substitution. eg
968 type instance F a Int = a
969 type instance F Int b = b
970 These two overlap on (F Int Int) but then both RHSs are Int,
971 so all is well. We require that they are syntactically equal;
972 anything else would be difficult to test for at this stage.
973 -}
974
975 ------------------------------------------------------------
976 -- Might be a one-way match or a unifier
977 type MatchFun = FamInst -- The FamInst template
978 -> TyVarSet -> [Type] -- fi_tvs, fi_tys of that FamInst
979 -> [Type] -- Target to match against
980 -> Maybe TCvSubst
981
982 lookup_fam_inst_env' -- The worker, local to this module
983 :: MatchFun
984 -> FamInstEnv
985 -> TyCon -> [Type] -- What we are looking for
986 -> [FamInstMatch]
987 lookup_fam_inst_env' match_fun ie fam match_tys
988 | isOpenFamilyTyCon fam
989 , Just (FamIE insts) <- lookupUDFM ie fam
990 = find insts -- The common case
991 | otherwise = []
992 where
993
994 find [] = []
995 find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs, fi_cvs = tpl_cvs
996 , fi_tys = tpl_tys }) : rest)
997 -- Fast check for no match, uses the "rough match" fields
998 | instanceCantMatch rough_tcs mb_tcs
999 = find rest
1000
1001 -- Proper check
1002 | Just subst <- match_fun item (mkVarSet tpl_tvs) tpl_tys match_tys1
1003 = (FamInstMatch { fim_instance = item
1004 , fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2
1005 , fim_cos = assert (all (isJust . lookupCoVar subst) tpl_cvs) $
1006 substCoVars subst tpl_cvs
1007 })
1008 : find rest
1009
1010 -- No match => try next
1011 | otherwise
1012 = find rest
1013 where
1014 (rough_tcs, match_tys1, match_tys2) = split_tys tpl_tys
1015
1016 -- Precondition: the tycon is saturated (or over-saturated)
1017
1018 -- Deal with over-saturation
1019 -- See Note [Over-saturated matches]
1020 split_tys tpl_tys
1021 | isTypeFamilyTyCon fam
1022 = pre_rough_split_tys
1023
1024 | otherwise
1025 = let (match_tys1, match_tys2) = splitAtList tpl_tys match_tys
1026 rough_tcs = roughMatchTcs match_tys1
1027 in (rough_tcs, match_tys1, match_tys2)
1028
1029 (pre_match_tys1, pre_match_tys2) = splitAt (tyConArity fam) match_tys
1030 pre_rough_split_tys
1031 = (roughMatchTcs pre_match_tys1, pre_match_tys1, pre_match_tys2)
1032
1033 lookup_fam_inst_env -- The worker, local to this module
1034 :: MatchFun
1035 -> FamInstEnvs
1036 -> TyCon -> [Type] -- What we are looking for
1037 -> [FamInstMatch] -- Successful matches
1038
1039 -- Precondition: the tycon is saturated (or over-saturated)
1040
1041 lookup_fam_inst_env match_fun (pkg_ie, home_ie) fam tys
1042 = lookup_fam_inst_env' match_fun home_ie fam tys
1043 ++ lookup_fam_inst_env' match_fun pkg_ie fam tys
1044
1045 {-
1046 Note [Over-saturated matches]
1047 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1048 It's ok to look up an over-saturated type constructor. E.g.
1049 type family F a :: * -> *
1050 type instance F (a,b) = Either (a->b)
1051
1052 The type instance gives rise to a newtype TyCon (at a higher kind
1053 which you can't do in Haskell!):
1054 newtype FPair a b = FP (Either (a->b))
1055
1056 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
1057 (FPair, [Int,Bool,Char])
1058 The "extra" type argument [Char] just stays on the end.
1059
1060 We handle data families and type families separately here:
1061
1062 * For type families, all instances of a type family must have the
1063 same arity, so we can precompute the split between the match_tys
1064 and the overflow tys. This is done in pre_rough_split_tys.
1065
1066 * For data family instances, though, we need to re-split for each
1067 instance, because the breakdown might be different for each
1068 instance. Why? Because of eta reduction; see
1069 Note [Eta reduction for data families] in GHC.Core.Coercion.Axiom.
1070 -}
1071
1072 -- checks if one LHS is dominated by a list of other branches
1073 -- in other words, if an application would match the first LHS, it is guaranteed
1074 -- to match at least one of the others. The RHSs are ignored.
1075 -- This algorithm is conservative:
1076 -- True -> the LHS is definitely covered by the others
1077 -- False -> no information
1078 -- It is currently (Oct 2012) used only for generating errors for
1079 -- inaccessible branches. If these errors go unreported, no harm done.
1080 -- This is defined here to avoid a dependency from CoAxiom to Unify
1081 isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool
1082 isDominatedBy branch branches
1083 = or $ map match branches
1084 where
1085 lhs = coAxBranchLHS branch
1086 match (CoAxBranch { cab_lhs = tys })
1087 = isJust $ tcMatchTys tys lhs
1088
1089 {-
1090 ************************************************************************
1091 * *
1092 Choosing an axiom application
1093 * *
1094 ************************************************************************
1095
1096 The lookupFamInstEnv function does a nice job for *open* type families,
1097 but we also need to handle closed ones when normalising a type:
1098 -}
1099
1100 reduceTyFamApp_maybe :: FamInstEnvs
1101 -> Role -- Desired role of result coercion
1102 -> TyCon -> [Type]
1103 -> Maybe Reduction
1104 -- Attempt to do a *one-step* reduction of a type-family application
1105 -- but *not* newtypes
1106 -- Works on type-synonym families always; data-families only if
1107 -- the role we seek is representational
1108 -- It does *not* normalise the type arguments first, so this may not
1109 -- go as far as you want. If you want normalised type arguments,
1110 -- use topReduceTyFamApp_maybe
1111 --
1112 -- The TyCon can be oversaturated.
1113 -- Works on both open and closed families
1114 --
1115 -- Always returns a *homogeneous* coercion -- type family reductions are always
1116 -- homogeneous
1117 reduceTyFamApp_maybe envs role tc tys
1118 | Phantom <- role
1119 = Nothing
1120
1121 | case role of
1122 Representational -> isOpenFamilyTyCon tc
1123 _ -> isOpenTypeFamilyTyCon tc
1124 -- If we seek a representational coercion
1125 -- (e.g. the call in topNormaliseType_maybe) then we can
1126 -- unwrap data families as well as type-synonym families;
1127 -- otherwise only type-synonym families
1128 , FamInstMatch { fim_instance = FamInst { fi_axiom = ax }
1129 , fim_tys = inst_tys
1130 , fim_cos = inst_cos } : _ <- lookupFamInstEnv envs tc tys
1131 -- NB: Allow multiple matches because of compatible overlap
1132
1133 = let co = mkUnbranchedAxInstCo role ax inst_tys inst_cos
1134 in Just $ coercionRedn co
1135
1136 | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe tc
1137 , Just (ind, inst_tys, inst_cos) <- chooseBranch ax tys
1138 = let co = mkAxInstCo role ax ind inst_tys inst_cos
1139 in Just $ coercionRedn co
1140
1141 | Just ax <- isBuiltInSynFamTyCon_maybe tc
1142 , Just (coax,ts,ty) <- sfMatchFam ax tys
1143 , role == coaxrRole coax
1144 = let co = mkAxiomRuleCo coax (zipWith mkReflCo (coaxrAsmpRoles coax) ts)
1145 in Just $ mkReduction co ty
1146
1147 | otherwise
1148 = Nothing
1149
1150 -- The axiom can be oversaturated. (Closed families only.)
1151 chooseBranch :: CoAxiom Branched -> [Type]
1152 -> Maybe (BranchIndex, [Type], [Coercion]) -- found match, with args
1153 chooseBranch axiom tys
1154 = do { let num_pats = coAxiomNumPats axiom
1155 (target_tys, extra_tys) = splitAt num_pats tys
1156 branches = coAxiomBranches axiom
1157 ; (ind, inst_tys, inst_cos)
1158 <- findBranch (unMkBranches branches) target_tys
1159 ; return ( ind, inst_tys `chkAppend` extra_tys, inst_cos ) }
1160
1161 -- The axiom must *not* be oversaturated
1162 findBranch :: Array BranchIndex CoAxBranch
1163 -> [Type]
1164 -> Maybe (BranchIndex, [Type], [Coercion])
1165 -- coercions relate requested types to returned axiom LHS at role N
1166 findBranch branches target_tys
1167 = foldr go Nothing (assocs branches)
1168 where
1169 go :: (BranchIndex, CoAxBranch)
1170 -> Maybe (BranchIndex, [Type], [Coercion])
1171 -> Maybe (BranchIndex, [Type], [Coercion])
1172 go (index, branch) other
1173 = let (CoAxBranch { cab_tvs = tpl_tvs, cab_cvs = tpl_cvs
1174 , cab_lhs = tpl_lhs
1175 , cab_incomps = incomps }) = branch
1176 in_scope = mkInScopeSet (unionVarSets $
1177 map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
1178 -- See Note [Flattening type-family applications when matching instances]
1179 -- in GHC.Core.Unify
1180 flattened_target = flattenTys in_scope target_tys
1181 in case tcMatchTys tpl_lhs target_tys of
1182 Just subst -- matching worked. now, check for apartness.
1183 | apartnessCheck flattened_target branch
1184 -> -- matching worked & we're apart from all incompatible branches.
1185 -- success
1186 assert (all (isJust . lookupCoVar subst) tpl_cvs) $
1187 Just (index, substTyVars subst tpl_tvs, substCoVars subst tpl_cvs)
1188
1189 -- failure. keep looking
1190 _ -> other
1191
1192 -- | Do an apartness check, as described in the "Closed Type Families" paper
1193 -- (POPL '14). This should be used when determining if an equation
1194 -- ('CoAxBranch') of a closed type family can be used to reduce a certain target
1195 -- type family application.
1196 apartnessCheck :: [Type]
1197 -- ^ /flattened/ target arguments. Make sure they're flattened! See
1198 -- Note [Flattening type-family applications when matching instances]
1199 -- in GHC.Core.Unify.
1200 -> CoAxBranch -- ^ the candidate equation we wish to use
1201 -- Precondition: this matches the target
1202 -> Bool -- ^ True <=> equation can fire
1203 apartnessCheck flattened_target (CoAxBranch { cab_incomps = incomps })
1204 = all (isSurelyApart
1205 . tcUnifyTysFG alwaysBindFun flattened_target
1206 . coAxBranchLHS) incomps
1207 where
1208 isSurelyApart SurelyApart = True
1209 isSurelyApart _ = False
1210
1211 {-
1212 ************************************************************************
1213 * *
1214 Looking up a family instance
1215 * *
1216 ************************************************************************
1217
1218 Note [Normalising types]
1219 ~~~~~~~~~~~~~~~~~~~~~~~~
1220 The topNormaliseType function removes all occurrences of type families
1221 and newtypes from the top-level structure of a type. normaliseTcApp does
1222 the type family lookup and is fairly straightforward. normaliseType is
1223 a little more involved.
1224
1225 The complication comes from the fact that a type family might be used in the
1226 kind of a variable bound in a forall. We wish to remove this type family
1227 application, but that means coming up with a fresh variable (with the new
1228 kind). Thus, we need a substitution to be built up as we recur through the
1229 type. However, an ordinary TCvSubst just won't do: when we hit a type variable
1230 whose kind has changed during normalisation, we need both the new type
1231 variable *and* the coercion. We could conjure up a new VarEnv with just this
1232 property, but a usable substitution environment already exists:
1233 LiftingContexts from the liftCoSubst family of functions, defined in GHC.Core.Coercion.
1234 A LiftingContext maps a type variable to a coercion and a coercion variable to
1235 a pair of coercions. Let's ignore coercion variables for now. Because the
1236 coercion a type variable maps to contains the destination type (via
1237 coercionKind), we don't need to store that destination type separately. Thus,
1238 a LiftingContext has what we need: a map from type variables to (Coercion,
1239 Type) pairs.
1240
1241 We also benefit because we can piggyback on the liftCoSubstVarBndr function to
1242 deal with binders. However, I had to modify that function to work with this
1243 application. Thus, we now have liftCoSubstVarBndrUsing, which takes
1244 a function used to process the kind of the binder. We don't wish
1245 to lift the kind, but instead normalise it. So, we pass in a callback function
1246 that processes the kind of the binder.
1247
1248 After that brilliant explanation of all this, I'm sure you've forgotten the
1249 dangling reference to coercion variables. What do we do with those? Nothing at
1250 all. The point of normalising types is to remove type family applications, but
1251 there's no sense in removing these from coercions. We would just get back a
1252 new coercion witnessing the equality between the same types as the original
1253 coercion. Because coercions are irrelevant anyway, there is no point in doing
1254 this. So, whenever we encounter a coercion, we just say that it won't change.
1255 That's what the CoercionTy case is doing within normalise_type.
1256
1257 Note [Normalisation and type synonyms]
1258 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1259 We need to be a bit careful about normalising in the presence of type
1260 synonyms (#13035). Suppose S is a type synonym, and we have
1261 S t1 t2
1262 If S is family-free (on its RHS) we can just normalise t1 and t2 and
1263 reconstruct (S t1' t2'). Expanding S could not reveal any new redexes
1264 because type families are saturated.
1265
1266 But if S has a type family on its RHS we expand /before/ normalising
1267 the args t1, t2. If we normalise t1, t2 first, we'll re-normalise them
1268 after expansion, and that can lead to /exponential/ behaviour; see #13035.
1269
1270 Notice, though, that expanding first can in principle duplicate t1,t2,
1271 which might contain redexes. I'm sure you could conjure up an exponential
1272 case by that route too, but it hasn't happened in practice yet!
1273 -}
1274
1275 topNormaliseType :: FamInstEnvs -> Type -> Type
1276 topNormaliseType env ty
1277 = case topNormaliseType_maybe env ty of
1278 Just redn -> reductionReducedType redn
1279 Nothing -> ty
1280
1281 topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe Reduction
1282
1283 -- ^ Get rid of *outermost* (or toplevel)
1284 -- * type function redex
1285 -- * data family redex
1286 -- * newtypes
1287 -- returning an appropriate Representational coercion. Specifically, if
1288 -- topNormaliseType_maybe env ty = Just (co, ty')
1289 -- then
1290 -- (a) co :: ty ~R ty'
1291 -- (b) ty' is not a newtype, and is not a type-family or data-family redex
1292 --
1293 -- However, ty' can be something like (Maybe (F ty)), where
1294 -- (F ty) is a redex.
1295 --
1296 -- Always operates homogeneously: the returned type has the same kind as the
1297 -- original type, and the returned coercion is always homogeneous.
1298 topNormaliseType_maybe env ty
1299 = do { ((co, mkind_co), nty) <- topNormaliseTypeX stepper combine ty
1300 ; let hredn = mkHetReduction (mkReduction co nty) mkind_co
1301 ; return $ homogeniseHetRedn Representational hredn }
1302 where
1303 stepper = unwrapNewTypeStepper' `composeSteppers` tyFamStepper
1304
1305 combine (c1, mc1) (c2, mc2) = (c1 `mkTransCo` c2, mc1 `mkTransMCo` mc2)
1306
1307 unwrapNewTypeStepper' :: NormaliseStepper (Coercion, MCoercionN)
1308 unwrapNewTypeStepper' rec_nts tc tys
1309 = mapStepResult (, MRefl) $ unwrapNewTypeStepper rec_nts tc tys
1310
1311 -- second coercion below is the kind coercion relating the original type's kind
1312 -- to the normalised type's kind
1313 tyFamStepper :: NormaliseStepper (Coercion, MCoercionN)
1314 tyFamStepper rec_nts tc tys -- Try to step a type/data family
1315 = case topReduceTyFamApp_maybe env tc tys of
1316 Just (HetReduction (Reduction co rhs) res_co)
1317 -> NS_Step rec_nts rhs (co, res_co)
1318 _ -> NS_Done
1319
1320 ---------------
1321 normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> Reduction
1322 -- See comments on normaliseType for the arguments of this function
1323 normaliseTcApp env role tc tys
1324 = initNormM env role (tyCoVarsOfTypes tys) $
1325 normalise_tc_app tc tys
1326
1327 -- See Note [Normalising types] about the LiftingContext
1328 normalise_tc_app :: TyCon -> [Type] -> NormM Reduction
1329 normalise_tc_app tc tys
1330 | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
1331 , not (isFamFreeTyCon tc) -- Expand and try again
1332 = -- A synonym with type families in the RHS
1333 -- Expand and try again
1334 -- See Note [Normalisation and type synonyms]
1335 normalise_type (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
1336
1337 | isFamilyTyCon tc
1338 = -- A type-family application
1339 do { env <- getEnv
1340 ; role <- getRole
1341 ; ArgsReductions redns@(Reductions args_cos ntys) res_co <- normalise_tc_args tc tys
1342 ; case reduceTyFamApp_maybe env role tc ntys of
1343 Just redn1
1344 -> do { redn2 <- normalise_reduction redn1
1345 ; let redn3 = mkTyConAppCo role tc args_cos `mkTransRedn` redn2
1346 ; return $ assemble_result role redn3 res_co }
1347 _ -> -- No unique matching family instance exists;
1348 -- we do not do anything
1349 return $
1350 assemble_result role (mkTyConAppRedn role tc redns) res_co }
1351
1352 | otherwise
1353 = -- A synonym with no type families in the RHS; or data type etc
1354 -- Just normalise the arguments and rebuild
1355 do { ArgsReductions redns res_co <- normalise_tc_args tc tys
1356 ; role <- getRole
1357 ; return $
1358 assemble_result role (mkTyConAppRedn role tc redns) res_co }
1359
1360 where
1361 assemble_result :: Role -- r, ambient role in NormM monad
1362 -> Reduction -- orig_ty ~r nty, possibly heterogeneous (nty possibly of changed kind)
1363 -> MCoercionN -- typeKind(orig_ty) ~N typeKind(nty)
1364 -> Reduction -- orig_ty ~r nty_casted
1365 -- where nty_casted has same kind as orig_ty
1366 assemble_result r redn kind_co
1367 = mkCoherenceRightMRedn r redn (mkSymMCo kind_co)
1368
1369 ---------------
1370 -- | Try to simplify a type-family application, by *one* step
1371 -- If topReduceTyFamApp_maybe env r F tys = Just (HetReduction (Reduction co rhs) res_co)
1372 -- then co :: F tys ~R# rhs
1373 -- res_co :: typeKind(F tys) ~ typeKind(rhs)
1374 -- Type families and data families; always Representational role
1375 topReduceTyFamApp_maybe :: FamInstEnvs -> TyCon -> [Type]
1376 -> Maybe HetReduction
1377 topReduceTyFamApp_maybe envs fam_tc arg_tys
1378 | isFamilyTyCon fam_tc -- type families and data families
1379 , Just redn <- reduceTyFamApp_maybe envs role fam_tc ntys
1380 = Just $
1381 mkHetReduction
1382 (mkTyConAppCo role fam_tc args_cos `mkTransRedn` redn)
1383 res_co
1384 | otherwise
1385 = Nothing
1386 where
1387 role = Representational
1388 ArgsReductions (Reductions args_cos ntys) res_co
1389 = initNormM envs role (tyCoVarsOfTypes arg_tys)
1390 $ normalise_tc_args fam_tc arg_tys
1391
1392 normalise_tc_args :: TyCon -> [Type] -> NormM ArgsReductions
1393 normalise_tc_args tc tys
1394 = do { role <- getRole
1395 ; normalise_args (tyConKind tc) (tyConRolesX role tc) tys }
1396
1397 ---------------
1398 normaliseType :: FamInstEnvs
1399 -> Role -- desired role of coercion
1400 -> Type -> Reduction
1401 normaliseType env role ty
1402 = initNormM env role (tyCoVarsOfType ty) $ normalise_type ty
1403
1404 normalise_type :: Type -> NormM Reduction
1405 -- Normalise the input type, by eliminating *all* type-function redexes
1406 -- but *not* newtypes (which are visible to the programmer)
1407 -- Returns with Refl if nothing happens
1408 -- Does nothing to newtypes
1409 -- The returned coercion *must* be *homogeneous*
1410 -- See Note [Normalising types]
1411 -- Try not to disturb type synonyms if possible
1412
1413 normalise_type ty
1414 = go ty
1415 where
1416 go :: Type -> NormM Reduction
1417 go (TyConApp tc tys) = normalise_tc_app tc tys
1418 go ty@(LitTy {})
1419 = do { r <- getRole
1420 ; return $ mkReflRedn r ty }
1421 go (AppTy ty1 ty2) = go_app_tys ty1 [ty2]
1422
1423 go (FunTy { ft_af = vis, ft_mult = w, ft_arg = ty1, ft_res = ty2 })
1424 = do { arg_redn <- go ty1
1425 ; res_redn <- go ty2
1426 ; w_redn <- withRole Nominal $ go w
1427 ; r <- getRole
1428 ; return $ mkFunRedn r vis w_redn arg_redn res_redn }
1429 go (ForAllTy (Bndr tcvar vis) ty)
1430 = do { (lc', tv', k_redn) <- normalise_var_bndr tcvar
1431 ; redn <- withLC lc' $ normalise_type ty
1432 ; return $ mkForAllRedn vis tv' k_redn redn }
1433 go (TyVarTy tv) = normalise_tyvar tv
1434 go (CastTy ty co)
1435 = do { redn <- go ty
1436 ; lc <- getLC
1437 ; let co' = substRightCo lc co
1438 ; return $ mkCastRedn2 Nominal ty co redn co'
1439 -- ^^^^^^^^^^^ uses castCoercionKind2
1440 }
1441 go (CoercionTy co)
1442 = do { lc <- getLC
1443 ; r <- getRole
1444 ; let kco = liftCoSubst Nominal lc (coercionType co)
1445 co' = substRightCo lc co
1446 ; return $ mkProofIrrelRedn r kco co co' }
1447
1448 go_app_tys :: Type -- function
1449 -> [Type] -- args
1450 -> NormM Reduction
1451 -- cf. GHC.Tc.Solver.Rewrite.rewrite_app_ty_args
1452 go_app_tys (AppTy ty1 ty2) tys = go_app_tys ty1 (ty2 : tys)
1453 go_app_tys fun_ty arg_tys
1454 = do { fun_redn@(Reduction fun_co nfun) <- go fun_ty
1455 ; case tcSplitTyConApp_maybe nfun of
1456 Just (tc, xis) ->
1457 do { redn <- go (mkTyConApp tc (xis ++ arg_tys))
1458 -- rewrite_app_ty_args avoids redundantly processing the xis,
1459 -- but that's a much more performance-sensitive function.
1460 -- This type normalisation is not called in a loop.
1461 ; return $
1462 mkAppCos fun_co (map mkNomReflCo arg_tys) `mkTransRedn` redn }
1463 Nothing ->
1464 do { ArgsReductions redns res_co
1465 <- normalise_args (typeKind nfun)
1466 (repeat Nominal)
1467 arg_tys
1468 ; role <- getRole
1469 ; return $
1470 mkCoherenceRightMRedn role
1471 (mkAppRedns fun_redn redns)
1472 (mkSymMCo res_co) } }
1473
1474 normalise_args :: Kind -- of the function
1475 -> [Role] -- roles at which to normalise args
1476 -> [Type] -- args
1477 -> NormM ArgsReductions
1478 -- returns ArgsReductions (Reductions cos xis) res_co,
1479 -- where each xi is the normalised version of the corresponding type,
1480 -- each co is orig_arg ~ xi, and res_co :: kind(f orig_args) ~ kind(f xis).
1481 -- NB: The xis might *not* have the same kinds as the input types,
1482 -- but the resulting application *will* be well-kinded
1483 -- cf. GHC.Tc.Solver.Rewrite.rewrite_args_slow
1484 normalise_args fun_ki roles args
1485 = do { normed_args <- zipWithM normalise1 roles args
1486 ; return $ simplifyArgsWorker ki_binders inner_ki fvs roles normed_args }
1487 where
1488 (ki_binders, inner_ki) = splitPiTys fun_ki
1489 fvs = tyCoVarsOfTypes args
1490
1491 normalise1 role ty
1492 = withRole role $ normalise_type ty
1493
1494 normalise_tyvar :: TyVar -> NormM Reduction
1495 normalise_tyvar tv
1496 = assert (isTyVar tv) $
1497 do { lc <- getLC
1498 ; r <- getRole
1499 ; return $ case liftCoSubstTyVar lc r tv of
1500 Just co -> coercionRedn co
1501 Nothing -> mkReflRedn r (mkTyVarTy tv) }
1502
1503 normalise_reduction :: Reduction -> NormM Reduction
1504 normalise_reduction (Reduction co ty)
1505 = do { redn' <- normalise_type ty
1506 ; return $ co `mkTransRedn` redn' }
1507
1508 normalise_var_bndr :: TyCoVar -> NormM (LiftingContext, TyCoVar, Reduction)
1509 normalise_var_bndr tcvar
1510 -- works for both tvar and covar
1511 = do { lc1 <- getLC
1512 ; env <- getEnv
1513 ; let callback lc ki = runNormM (normalise_type ki) env lc Nominal
1514 ; return $ liftCoSubstVarBndrUsing reductionCoercion callback lc1 tcvar }
1515
1516 -- | a monad for the normalisation functions, reading 'FamInstEnvs',
1517 -- a 'LiftingContext', and a 'Role'.
1518 newtype NormM a = NormM { runNormM ::
1519 FamInstEnvs -> LiftingContext -> Role -> a }
1520 deriving (Functor)
1521
1522 initNormM :: FamInstEnvs -> Role
1523 -> TyCoVarSet -- the in-scope variables
1524 -> NormM a -> a
1525 initNormM env role vars (NormM thing_inside)
1526 = thing_inside env lc role
1527 where
1528 in_scope = mkInScopeSet vars
1529 lc = emptyLiftingContext in_scope
1530
1531 getRole :: NormM Role
1532 getRole = NormM (\ _ _ r -> r)
1533
1534 getLC :: NormM LiftingContext
1535 getLC = NormM (\ _ lc _ -> lc)
1536
1537 getEnv :: NormM FamInstEnvs
1538 getEnv = NormM (\ env _ _ -> env)
1539
1540 withRole :: Role -> NormM a -> NormM a
1541 withRole r thing = NormM $ \ envs lc _old_r -> runNormM thing envs lc r
1542
1543 withLC :: LiftingContext -> NormM a -> NormM a
1544 withLC lc thing = NormM $ \ envs _old_lc r -> runNormM thing envs lc r
1545
1546 instance Monad NormM where
1547 ma >>= fmb = NormM $ \env lc r ->
1548 let a = runNormM ma env lc r in
1549 runNormM (fmb a) env lc r
1550
1551 instance Applicative NormM where
1552 pure x = NormM $ \ _ _ _ -> x
1553 (<*>) = ap