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