Add -fcross-module-specialise flag
[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 #-}
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, deleteFromFamInstEnv, extendFamInstEnvList,
15 identicalFamInstHead, famInstEnvElts, familyInstances, orphNamesOfFamInst,
16
17 -- * CoAxioms
18 mkCoAxBranch, mkBranchedCoAxiom, mkUnbranchedCoAxiom, mkSingleCoAxiom,
19 computeAxiomIncomps,
20
21 FamInstMatch(..),
22 lookupFamInstEnv, lookupFamInstEnvConflicts,
23 isDominatedBy,
24
25 -- Normalisation
26 topNormaliseType, topNormaliseType_maybe,
27 normaliseType, normaliseTcApp,
28 reduceTyFamApp_maybe, chooseBranch,
29
30 -- Flattening
31 flattenTys
32 ) where
33
34 #include "HsVersions.h"
35
36 import InstEnv
37 import Unify
38 import Type
39 import TcType ( orphNamesOfTypes )
40 import TypeRep
41 import TyCon
42 import Coercion
43 import CoAxiom
44 import VarSet
45 import VarEnv
46 import Name
47 import UniqFM
48 import Outputable
49 import Maybes
50 import TrieMap
51 import Unique
52 import Util
53 import Var
54 import Pair
55 import SrcLoc
56 import NameSet
57 import FastString
58
59 {-
60 ************************************************************************
61 * *
62 Type checked family instance heads
63 * *
64 ************************************************************************
65
66 Note [FamInsts and CoAxioms]
67 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
68 * CoAxioms and FamInsts are just like
69 DFunIds and ClsInsts
70
71 * A CoAxiom is a System-FC thing: it can relate any two types
72
73 * A FamInst is a Haskell source-language thing, corresponding
74 to a type/data family instance declaration.
75 - The FamInst contains a CoAxiom, which is the evidence
76 for the instance
77
78 - The LHS of the CoAxiom is always of form F ty1 .. tyn
79 where F is a type family
80 -}
81
82 data FamInst -- See Note [FamInsts and CoAxioms]
83 = FamInst { fi_axiom :: CoAxiom Unbranched -- The new coercion axiom introduced
84 -- by this family instance
85 , fi_flavor :: FamFlavor
86
87 -- Everything below here is a redundant,
88 -- cached version of the two things above
89 -- except that the TyVars are freshened
90 , fi_fam :: Name -- Family name
91
92 -- Used for "rough matching"; same idea as for class instances
93 -- See Note [Rough-match field] in InstEnv
94 , fi_tcs :: [Maybe Name] -- Top of type args
95 -- INVARIANT: fi_tcs = roughMatchTcs fi_tys
96
97 -- Used for "proper matching"; ditto
98 , fi_tvs :: [TyVar] -- Template tyvars for full match
99 -- Like ClsInsts, these variables are always
100 -- fresh. See Note [Template tyvars are fresh]
101 -- in InstEnv
102
103 , fi_tys :: [Type] -- and its arg types
104 -- INVARIANT: fi_tvs = coAxiomTyVars fi_axiom
105
106 , fi_rhs :: Type -- the RHS, with its freshened vars
107 }
108
109 data FamFlavor
110 = SynFamilyInst -- A synonym family
111 | DataFamilyInst TyCon -- A data family, with its representation TyCon
112
113 -- Obtain the axiom of a family instance
114 famInstAxiom :: FamInst -> CoAxiom Unbranched
115 famInstAxiom = fi_axiom
116
117 -- Split the left-hand side of the FamInst
118 famInstSplitLHS :: FamInst -> (TyCon, [Type])
119 famInstSplitLHS (FamInst { fi_axiom = axiom, fi_tys = lhs })
120 = (coAxiomTyCon axiom, lhs)
121
122 -- Get the RHS of the FamInst
123 famInstRHS :: FamInst -> Type
124 famInstRHS = fi_rhs
125
126 -- Get the family TyCon of the FamInst
127 famInstTyCon :: FamInst -> TyCon
128 famInstTyCon = coAxiomTyCon . famInstAxiom
129
130 -- Return the representation TyCons introduced by data family instances, if any
131 famInstsRepTyCons :: [FamInst] -> [TyCon]
132 famInstsRepTyCons fis = [tc | FamInst { fi_flavor = DataFamilyInst tc } <- fis]
133
134 -- Extracts the TyCon for this *data* (or newtype) instance
135 famInstRepTyCon_maybe :: FamInst -> Maybe TyCon
136 famInstRepTyCon_maybe fi
137 = case fi_flavor fi of
138 DataFamilyInst tycon -> Just tycon
139 SynFamilyInst -> Nothing
140
141 dataFamInstRepTyCon :: FamInst -> TyCon
142 dataFamInstRepTyCon fi
143 = case fi_flavor fi of
144 DataFamilyInst tycon -> tycon
145 SynFamilyInst -> pprPanic "dataFamInstRepTyCon" (ppr fi)
146
147 {-
148 ************************************************************************
149 * *
150 Pretty printing
151 * *
152 ************************************************************************
153 -}
154
155 instance NamedThing FamInst where
156 getName = coAxiomName . fi_axiom
157
158 instance Outputable FamInst where
159 ppr = pprFamInst
160
161 -- Prints the FamInst as a family instance declaration
162 -- NB: FamInstEnv.pprFamInst is used only for internal, debug printing
163 -- See pprTyThing.pprFamInst for printing for the user
164 pprFamInst :: FamInst -> SDoc
165 pprFamInst famInst
166 = hang (pprFamInstHdr famInst)
167 2 (vcat [ ifPprDebug (ptext (sLit "Coercion axiom:") <+> ppr ax)
168 , ifPprDebug (ptext (sLit "RHS:") <+> ppr (famInstRHS famInst)) ])
169 where
170 ax = fi_axiom famInst
171
172 pprFamInstHdr :: FamInst -> SDoc
173 pprFamInstHdr fi@(FamInst {fi_flavor = flavor})
174 = pprTyConSort <+> pp_instance <+> pp_head
175 where
176 -- For *associated* types, say "type T Int = blah"
177 -- For *top level* type instances, say "type instance T Int = blah"
178 pp_instance
179 | isTyConAssoc fam_tc = empty
180 | otherwise = ptext (sLit "instance")
181
182 (fam_tc, etad_lhs_tys) = famInstSplitLHS fi
183 vanilla_pp_head = pprTypeApp fam_tc etad_lhs_tys
184
185 pp_head | DataFamilyInst rep_tc <- flavor
186 , isAlgTyCon rep_tc
187 , let extra_tvs = dropList etad_lhs_tys (tyConTyVars rep_tc)
188 , not (null extra_tvs)
189 = getPprStyle $ \ sty ->
190 if debugStyle sty
191 then vanilla_pp_head -- With -dppr-debug just show it as-is
192 else pprTypeApp fam_tc (etad_lhs_tys ++ mkTyVarTys extra_tvs)
193 -- Without -dppr-debug, eta-expand
194 -- See Trac #8674
195 -- (This is probably over the top now that we use this
196 -- only for internal debug printing; PprTyThing.pprFamInst
197 -- is used for user-level printing.)
198 | otherwise
199 = vanilla_pp_head
200
201 pprTyConSort = case flavor of
202 SynFamilyInst -> ptext (sLit "type")
203 DataFamilyInst tycon
204 | isDataTyCon tycon -> ptext (sLit "data")
205 | isNewTyCon tycon -> ptext (sLit "newtype")
206 | isAbstractTyCon tycon -> ptext (sLit "data")
207 | otherwise -> ptext (sLit "WEIRD") <+> ppr tycon
208
209 pprFamInsts :: [FamInst] -> SDoc
210 pprFamInsts finsts = vcat (map pprFamInst finsts)
211
212 {-
213 Note [Lazy axiom match]
214 ~~~~~~~~~~~~~~~~~~~~~~~
215 It is Vitally Important that mkImportedFamInst is *lazy* in its axiom
216 parameter. The axiom is loaded lazily, via a forkM, in TcIface. Sometime
217 later, mkImportedFamInst is called using that axiom. However, the axiom
218 may itself depend on entities which are not yet loaded as of the time
219 of the mkImportedFamInst. Thus, if mkImportedFamInst eagerly looks at the
220 axiom, a dependency loop spontaneously appears and GHC hangs. The solution
221 is simply for mkImportedFamInst never, ever to look inside of the axiom
222 until everything else is good and ready to do so. We can assume that this
223 readiness has been achieved when some other code pulls on the axiom in the
224 FamInst. Thus, we pattern match on the axiom lazily (in the where clause,
225 not in the parameter list) and we assert the consistency of names there
226 also.
227 -}
228
229 -- Make a family instance representation from the information found in an
230 -- interface file. In particular, we get the rough match info from the iface
231 -- (instead of computing it here).
232 mkImportedFamInst :: Name -- Name of the family
233 -> [Maybe Name] -- Rough match info
234 -> CoAxiom Unbranched -- Axiom introduced
235 -> FamInst -- Resulting family instance
236 mkImportedFamInst fam mb_tcs axiom
237 = FamInst {
238 fi_fam = fam,
239 fi_tcs = mb_tcs,
240 fi_tvs = tvs,
241 fi_tys = tys,
242 fi_rhs = rhs,
243 fi_axiom = axiom,
244 fi_flavor = flavor }
245 where
246 -- See Note [Lazy axiom match]
247 ~(CoAxiom { co_ax_branches =
248 ~(FirstBranch ~(CoAxBranch { cab_lhs = tys
249 , cab_tvs = tvs
250 , cab_rhs = rhs })) }) = axiom
251
252 -- Derive the flavor for an imported FamInst rather disgustingly
253 -- Maybe we should store it in the IfaceFamInst?
254 flavor = case splitTyConApp_maybe rhs of
255 Just (tc, _)
256 | Just ax' <- tyConFamilyCoercion_maybe tc
257 , ax' == axiom
258 -> DataFamilyInst tc
259 _ -> SynFamilyInst
260
261 {-
262 ************************************************************************
263 * *
264 FamInstEnv
265 * *
266 ************************************************************************
267
268 Note [FamInstEnv]
269 ~~~~~~~~~~~~~~~~~
270 A FamInstEnv maps a family name to the list of known instances for that family.
271
272 The same FamInstEnv includes both 'data family' and 'type family' instances.
273 Type families are reduced during type inference, but not data families;
274 the user explains when to use a data family instance by using contructors
275 and pattern matching.
276
277 Neverthless it is still useful to have data families in the FamInstEnv:
278
279 - For finding overlaps and conflicts
280
281 - For finding the representation type...see FamInstEnv.topNormaliseType
282 and its call site in Simplify
283
284 - In standalone deriving instance Eq (T [Int]) we need to find the
285 representation type for T [Int]
286
287 Note [Varying number of patterns for data family axioms]
288 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
289 For data families, the number of patterns may vary between instances.
290 For example
291 data family T a b
292 data instance T Int a = T1 a | T2
293 data instance T Bool [a] = T3 a
294
295 Then we get a data type for each instance, and an axiom:
296 data TInt a = T1 a | T2
297 data TBoolList a = T3 a
298
299 axiom ax7 :: T Int ~ TInt -- Eta-reduced
300 axiom ax8 a :: T Bool [a] ~ TBoolList a
301
302 These two axioms for T, one with one pattern, one with two. The reason
303 for this eta-reduction is decribed in TcInstDcls
304 Note [Eta reduction for data family axioms]
305 -}
306
307 type FamInstEnv = UniqFM FamilyInstEnv -- Maps a family to its instances
308 -- See Note [FamInstEnv]
309
310 type FamInstEnvs = (FamInstEnv, FamInstEnv)
311 -- External package inst-env, Home-package inst-env
312
313 newtype FamilyInstEnv
314 = FamIE [FamInst] -- The instances for a particular family, in any order
315
316 instance Outputable FamilyInstEnv where
317 ppr (FamIE fs) = ptext (sLit "FamIE") <+> vcat (map ppr fs)
318
319 -- INVARIANTS:
320 -- * The fs_tvs are distinct in each FamInst
321 -- of a range value of the map (so we can safely unify them)
322
323 emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
324 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
325
326 emptyFamInstEnv :: FamInstEnv
327 emptyFamInstEnv = emptyUFM
328
329 famInstEnvElts :: FamInstEnv -> [FamInst]
330 famInstEnvElts fi = [elt | FamIE elts <- eltsUFM fi, elt <- elts]
331
332 familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
333 familyInstances (pkg_fie, home_fie) fam
334 = get home_fie ++ get pkg_fie
335 where
336 get env = case lookupUFM env fam of
337 Just (FamIE insts) -> insts
338 Nothing -> []
339
340 -- | Collects the names of the concrete types and type constructors that
341 -- make up the LHS of a type family instance, including the family
342 -- name itself.
343 --
344 -- For instance, given `type family Foo a b`:
345 -- `type instance Foo (F (G (H a))) b = ...` would yield [Foo,F,G,H]
346 --
347 -- Used in the implementation of ":info" in GHCi.
348 orphNamesOfFamInst :: FamInst -> NameSet
349 orphNamesOfFamInst fam_inst
350 = orphNamesOfTypes (concat (brListMap cab_lhs (coAxiomBranches axiom)))
351 `extendNameSet` getName (coAxiomTyCon axiom)
352 where
353 axiom = fi_axiom fam_inst
354
355 extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
356 extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis
357
358 extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
359 extendFamInstEnv inst_env
360 ins_item@(FamInst {fi_fam = cls_nm})
361 = addToUFM_C add inst_env cls_nm (FamIE [ins_item])
362 where
363 add (FamIE items) _ = FamIE (ins_item:items)
364
365 deleteFromFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
366 -- Used only for overriding in GHCi
367 deleteFromFamInstEnv inst_env fam_inst@(FamInst {fi_fam = fam_nm})
368 = adjustUFM adjust inst_env fam_nm
369 where
370 adjust :: FamilyInstEnv -> FamilyInstEnv
371 adjust (FamIE items)
372 = FamIE (filterOut (identicalFamInstHead fam_inst) items)
373
374 identicalFamInstHead :: FamInst -> FamInst -> Bool
375 -- ^ True when the LHSs are identical
376 -- Used for overriding in GHCi
377 identicalFamInstHead (FamInst { fi_axiom = ax1 }) (FamInst { fi_axiom = ax2 })
378 = coAxiomTyCon ax1 == coAxiomTyCon ax2
379 && brListLength brs1 == brListLength brs2
380 && and (brListZipWith identical_branch brs1 brs2)
381 where
382 brs1 = coAxiomBranches ax1
383 brs2 = coAxiomBranches ax2
384
385 identical_branch br1 br2
386 = isJust (tcMatchTys tvs1 lhs1 lhs2)
387 && isJust (tcMatchTys tvs2 lhs2 lhs1)
388 where
389 tvs1 = mkVarSet (coAxBranchTyVars br1)
390 tvs2 = mkVarSet (coAxBranchTyVars br2)
391 lhs1 = coAxBranchLHS br1
392 lhs2 = coAxBranchLHS br2
393
394 {-
395 ************************************************************************
396 * *
397 Compatibility
398 * *
399 ************************************************************************
400
401 Note [Apartness]
402 ~~~~~~~~~~~~~~~~
403 In dealing with closed type families, we must be able to check that one type
404 will never reduce to another. This check is called /apartness/. The check
405 is always between a target (which may be an arbitrary type) and a pattern.
406 Here is how we do it:
407
408 apart(target, pattern) = not (unify(flatten(target), pattern))
409
410 where flatten (implemented in flattenTys, below) converts all type-family
411 applications into fresh variables. (See Note [Flattening].)
412
413 Note [Compatibility]
414 ~~~~~~~~~~~~~~~~~~~~
415 Two patterns are /compatible/ if either of the following conditions hold:
416 1) The patterns are apart.
417 2) The patterns unify with a substitution S, and their right hand sides
418 equal under that substitution.
419
420 For open type families, only compatible instances are allowed. For closed
421 type families, the story is slightly more complicated. Consider the following:
422
423 type family F a where
424 F Int = Bool
425 F a = Int
426
427 g :: Show a => a -> F a
428 g x = length (show x)
429
430 Should that type-check? No. We need to allow for the possibility that 'a'
431 might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int
432 only when we can be sure that 'a' is not Int.
433
434 To achieve this, after finding a possible match within the equations, we have to
435 go back to all previous equations and check that, under the
436 substitution induced by the match, other branches are surely apart. (See
437 Note [Apartness].) This is similar to what happens with class
438 instance selection, when we need to guarantee that there is only a match and
439 no unifiers. The exact algorithm is different here because the the
440 potentially-overlapping group is closed.
441
442 As another example, consider this:
443
444 type family G x
445 type instance where
446 G Int = Bool
447 G a = Double
448
449 type family H y
450 -- no instances
451
452 Now, we want to simplify (G (H Char)). We can't, because (H Char) might later
453 simplify to be Int. So, (G (H Char)) is stuck, for now.
454
455 While everything above is quite sound, it isn't as expressive as we'd like.
456 Consider this:
457
458 type family J a where
459 J Int = Int
460 J a = a
461
462 Can we simplify (J b) to b? Sure we can. Yes, the first equation matches if
463 b is instantiated with Int, but the RHSs coincide there, so it's all OK.
464
465 So, the rule is this: when looking up a branch in a closed type family, we
466 find a branch that matches the target, but then we make sure that the target
467 is apart from every previous *incompatible* branch. We don't check the
468 branches that are compatible with the matching branch, because they are either
469 irrelevant (clause 1 of compatible) or benign (clause 2 of compatible).
470 -}
471
472 -- See Note [Compatibility]
473 compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
474 compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
475 (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
476 = case tcUnifyTysFG instanceBindFun lhs1 lhs2 of
477 SurelyApart -> True
478 Unifiable subst
479 | Type.substTy subst rhs1 `eqType` Type.substTy subst rhs2
480 -> True
481 _ -> False
482
483 -- takes a CoAxiom with unknown branch incompatibilities and computes
484 -- the compatibilities
485 -- See Note [Storing compatibility] in CoAxiom
486 computeAxiomIncomps :: CoAxiom br -> CoAxiom br
487 computeAxiomIncomps ax@(CoAxiom { co_ax_branches = branches })
488 = ax { co_ax_branches = go [] branches }
489 where
490 go :: [CoAxBranch] -> BranchList CoAxBranch br -> BranchList CoAxBranch br
491 go prev_branches (FirstBranch br)
492 = FirstBranch (br { cab_incomps = mk_incomps br prev_branches })
493 go prev_branches (NextBranch br tail)
494 = let br' = br { cab_incomps = mk_incomps br prev_branches } in
495 NextBranch br' (go (br' : prev_branches) tail)
496
497 mk_incomps :: CoAxBranch -> [CoAxBranch] -> [CoAxBranch]
498 mk_incomps br = filter (not . compatibleBranches br)
499
500 {-
501 ************************************************************************
502 * *
503 Constructing axioms
504 These functions are here because tidyType / tcUnifyTysFG
505 are not available in CoAxiom
506 * *
507 ************************************************************************
508
509 Note [Tidy axioms when we build them]
510 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
511 We print out axioms and don't want to print stuff like
512 F k k a b = ...
513 Instead we must tidy those kind variables. See Trac #7524.
514 -}
515
516 -- all axiom roles are Nominal, as this is only used with type families
517 mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
518 -> [Type] -- LHS patterns
519 -> Type -- RHS
520 -> SrcSpan
521 -> CoAxBranch
522 mkCoAxBranch tvs lhs rhs loc
523 = CoAxBranch { cab_tvs = tvs1
524 , cab_lhs = tidyTypes env lhs
525 , cab_roles = map (const Nominal) tvs1
526 , cab_rhs = tidyType env rhs
527 , cab_loc = loc
528 , cab_incomps = placeHolderIncomps }
529 where
530 (env, tvs1) = tidyTyVarBndrs emptyTidyEnv tvs
531 -- See Note [Tidy axioms when we build them]
532
533 -- all of the following code is here to avoid mutual dependencies with
534 -- Coercion
535 mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
536 mkBranchedCoAxiom ax_name fam_tc branches
537 = computeAxiomIncomps $
538 CoAxiom { co_ax_unique = nameUnique ax_name
539 , co_ax_name = ax_name
540 , co_ax_tc = fam_tc
541 , co_ax_role = Nominal
542 , co_ax_implicit = False
543 , co_ax_branches = toBranchList branches }
544
545 mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched
546 mkUnbranchedCoAxiom ax_name fam_tc branch
547 = CoAxiom { co_ax_unique = nameUnique ax_name
548 , co_ax_name = ax_name
549 , co_ax_tc = fam_tc
550 , co_ax_role = Nominal
551 , co_ax_implicit = False
552 , co_ax_branches = FirstBranch (branch { cab_incomps = [] }) }
553
554 mkSingleCoAxiom :: Role -> Name
555 -> [TyVar] -> TyCon -> [Type] -> Type
556 -> CoAxiom Unbranched
557 -- Make a single-branch CoAxiom, incluidng making the branch itself
558 -- Used for both type family (Nominal) and data family (Representational)
559 -- axioms, hence passing in the Role
560 mkSingleCoAxiom role ax_name tvs fam_tc lhs_tys rhs_ty
561 = CoAxiom { co_ax_unique = nameUnique ax_name
562 , co_ax_name = ax_name
563 , co_ax_tc = fam_tc
564 , co_ax_role = role
565 , co_ax_implicit = False
566 , co_ax_branches = FirstBranch (branch { cab_incomps = [] }) }
567 where
568 branch = mkCoAxBranch tvs lhs_tys rhs_ty (getSrcSpan ax_name)
569
570 {-
571 ************************************************************************
572 * *
573 Looking up a family instance
574 * *
575 ************************************************************************
576
577 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
578 Multiple matches are only possible in case of type families (not data
579 families), and then, it doesn't matter which match we choose (as the
580 instances are guaranteed confluent).
581
582 We return the matching family instances and the type instance at which it
583 matches. For example, if we lookup 'T [Int]' and have a family instance
584
585 data instance T [a] = ..
586
587 desugared to
588
589 data :R42T a = ..
590 coe :Co:R42T a :: T [a] ~ :R42T a
591
592 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
593 -}
594
595 -- when matching a type family application, we get a FamInst,
596 -- and the list of types the axiom should be applied to
597 data FamInstMatch = FamInstMatch { fim_instance :: FamInst
598 , fim_tys :: [Type]
599 }
600 -- See Note [Over-saturated matches]
601
602 instance Outputable FamInstMatch where
603 ppr (FamInstMatch { fim_instance = inst
604 , fim_tys = tys })
605 = ptext (sLit "match with") <+> parens (ppr inst) <+> ppr tys
606
607 lookupFamInstEnv
608 :: FamInstEnvs
609 -> TyCon -> [Type] -- What we are looking for
610 -> [FamInstMatch] -- Successful matches
611 -- Precondition: the tycon is saturated (or over-saturated)
612
613 lookupFamInstEnv
614 = lookup_fam_inst_env match
615 where
616 match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
617
618 lookupFamInstEnvConflicts
619 :: FamInstEnvs
620 -> FamInst -- Putative new instance
621 -> [FamInstMatch] -- Conflicting matches (don't look at the fim_tys field)
622 -- E.g. when we are about to add
623 -- f : type instance F [a] = a->a
624 -- we do (lookupFamInstConflicts f [b])
625 -- to find conflicting matches
626 --
627 -- Precondition: the tycon is saturated (or over-saturated)
628
629 lookupFamInstEnvConflicts envs fam_inst@(FamInst { fi_axiom = new_axiom })
630 = lookup_fam_inst_env my_unify envs fam tys
631 where
632 (fam, tys) = famInstSplitLHS fam_inst
633 -- In example above, fam tys' = F [b]
634
635 my_unify (FamInst { fi_axiom = old_axiom }) tpl_tvs tpl_tys _
636 = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
637 (ppr fam <+> ppr tys) $$
638 (ppr tpl_tvs <+> ppr tpl_tys) )
639 -- Unification will break badly if the variables overlap
640 -- They shouldn't because we allocate separate uniques for them
641 if compatibleBranches (coAxiomSingleBranch old_axiom) new_branch
642 then Nothing
643 else Just noSubst
644 -- Note [Family instance overlap conflicts]
645
646 noSubst = panic "lookupFamInstEnvConflicts noSubst"
647 new_branch = coAxiomSingleBranch new_axiom
648
649 {-
650 Note [Family instance overlap conflicts]
651 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
652 - In the case of data family instances, any overlap is fundamentally a
653 conflict (as these instances imply injective type mappings).
654
655 - In the case of type family instances, overlap is admitted as long as
656 the right-hand sides of the overlapping rules coincide under the
657 overlap substitution. eg
658 type instance F a Int = a
659 type instance F Int b = b
660 These two overlap on (F Int Int) but then both RHSs are Int,
661 so all is well. We require that they are syntactically equal;
662 anything else would be difficult to test for at this stage.
663 -}
664
665 ------------------------------------------------------------
666 -- Might be a one-way match or a unifier
667 type MatchFun = FamInst -- The FamInst template
668 -> TyVarSet -> [Type] -- fi_tvs, fi_tys of that FamInst
669 -> [Type] -- Target to match against
670 -> Maybe TvSubst
671
672 lookup_fam_inst_env' -- The worker, local to this module
673 :: MatchFun
674 -> FamInstEnv
675 -> TyCon -> [Type] -- What we are looking for
676 -> [FamInstMatch]
677 lookup_fam_inst_env' match_fun ie fam match_tys
678 | isOpenFamilyTyCon fam
679 , Just (FamIE insts) <- lookupUFM ie fam
680 = find insts -- The common case
681 | otherwise = []
682 where
683
684 find [] = []
685 find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs,
686 fi_tys = tpl_tys }) : rest)
687 -- Fast check for no match, uses the "rough match" fields
688 | instanceCantMatch rough_tcs mb_tcs
689 = find rest
690
691 -- Proper check
692 | Just subst <- match_fun item (mkVarSet tpl_tvs) tpl_tys match_tys1
693 = (FamInstMatch { fim_instance = item
694 , fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2 })
695 : find rest
696
697 -- No match => try next
698 | otherwise
699 = find rest
700
701 where
702 (rough_tcs, match_tys1, match_tys2) = split_tys tpl_tys
703
704 -- Precondition: the tycon is saturated (or over-saturated)
705
706 -- Deal with over-saturation
707 -- See Note [Over-saturated matches]
708 split_tys tpl_tys
709 | isTypeFamilyTyCon fam
710 = pre_rough_split_tys
711
712 | otherwise
713 = let (match_tys1, match_tys2) = splitAtList tpl_tys match_tys
714 rough_tcs = roughMatchTcs match_tys1
715 in (rough_tcs, match_tys1, match_tys2)
716
717 (pre_match_tys1, pre_match_tys2) = splitAt (tyConArity fam) match_tys
718 pre_rough_split_tys
719 = (roughMatchTcs pre_match_tys1, pre_match_tys1, pre_match_tys2)
720
721 lookup_fam_inst_env -- The worker, local to this module
722 :: MatchFun
723 -> FamInstEnvs
724 -> TyCon -> [Type] -- What we are looking for
725 -> [FamInstMatch] -- Successful matches
726
727 -- Precondition: the tycon is saturated (or over-saturated)
728
729 lookup_fam_inst_env match_fun (pkg_ie, home_ie) fam tys
730 = lookup_fam_inst_env' match_fun home_ie fam tys
731 ++ lookup_fam_inst_env' match_fun pkg_ie fam tys
732
733 {-
734 Note [Over-saturated matches]
735 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
736 It's ok to look up an over-saturated type constructor. E.g.
737 type family F a :: * -> *
738 type instance F (a,b) = Either (a->b)
739
740 The type instance gives rise to a newtype TyCon (at a higher kind
741 which you can't do in Haskell!):
742 newtype FPair a b = FP (Either (a->b))
743
744 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
745 (FPair, [Int,Bool,Char])
746 The "extra" type argument [Char] just stays on the end.
747
748 We handle data families and type families separately here:
749
750 * For type families, all instances of a type family must have the
751 same arity, so we can precompute the split between the match_tys
752 and the overflow tys. This is done in pre_rough_split_tys.
753
754 * For data family instances, though, we need to re-split for each
755 instance, because the breakdown might be different for each
756 instance. Why? Because of eta reduction; see Note [Eta reduction
757 for data family axioms] in TcInstDcls.
758 -}
759
760 -- checks if one LHS is dominated by a list of other branches
761 -- in other words, if an application would match the first LHS, it is guaranteed
762 -- to match at least one of the others. The RHSs are ignored.
763 -- This algorithm is conservative:
764 -- True -> the LHS is definitely covered by the others
765 -- False -> no information
766 -- It is currently (Oct 2012) used only for generating errors for
767 -- inaccessible branches. If these errors go unreported, no harm done.
768 -- This is defined here to avoid a dependency from CoAxiom to Unify
769 isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool
770 isDominatedBy branch branches
771 = or $ map match branches
772 where
773 lhs = coAxBranchLHS branch
774 match (CoAxBranch { cab_tvs = tvs, cab_lhs = tys })
775 = isJust $ tcMatchTys (mkVarSet tvs) tys lhs
776
777 {-
778 ************************************************************************
779 * *
780 Choosing an axiom application
781 * *
782 ************************************************************************
783
784 The lookupFamInstEnv function does a nice job for *open* type families,
785 but we also need to handle closed ones when normalising a type:
786 -}
787
788 reduceTyFamApp_maybe :: FamInstEnvs
789 -> Role -- Desired role of result coercion
790 -> TyCon -> [Type]
791 -> Maybe (Coercion, Type)
792 -- Attempt to do a *one-step* reduction of a type-family application
793 -- but *not* newtypes
794 -- Works on type-synonym families always; data-families only if
795 -- the role we seek is representational
796 -- It does *not* normlise the type arguments first, so this may not
797 -- go as far as you want. If you want normalised type arguments,
798 -- use normaliseTcArgs first.
799 --
800 -- The TyCon can be oversaturated.
801 -- Works on both open and closed families
802
803 reduceTyFamApp_maybe envs role tc tys
804 | Phantom <- role
805 = Nothing
806
807 | case role of
808 Representational -> isOpenFamilyTyCon tc
809 _ -> isOpenTypeFamilyTyCon tc
810 -- If we seek a representational coercion
811 -- (e.g. the call in topNormaliseType_maybe) then we can
812 -- unwrap data families as well as type-synonym families;
813 -- otherwise only type-synonym families
814 , FamInstMatch { fim_instance = fam_inst
815 , fim_tys = inst_tys } : _ <- lookupFamInstEnv envs tc tys
816 -- NB: Allow multiple matches because of compatible overlap
817
818 = let ax = famInstAxiom fam_inst
819 co = mkUnbranchedAxInstCo role ax inst_tys
820 ty = pSnd (coercionKind co)
821 in Just (co, ty)
822
823 | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe tc
824 , Just (ind, inst_tys) <- chooseBranch ax tys
825 = let co = mkAxInstCo role ax ind inst_tys
826 ty = pSnd (coercionKind co)
827 in Just (co, ty)
828
829 | Just ax <- isBuiltInSynFamTyCon_maybe tc
830 , Just (coax,ts,ty) <- sfMatchFam ax tys
831 = let co = mkAxiomRuleCo coax ts []
832 in Just (co, ty)
833
834 | otherwise
835 = Nothing
836
837 -- The axiom can be oversaturated. (Closed families only.)
838 chooseBranch :: CoAxiom Branched -> [Type] -> Maybe (BranchIndex, [Type])
839 chooseBranch axiom tys
840 = do { let num_pats = coAxiomNumPats axiom
841 (target_tys, extra_tys) = splitAt num_pats tys
842 branches = coAxiomBranches axiom
843 ; (ind, inst_tys) <- findBranch (fromBranchList branches) 0 target_tys
844 ; return (ind, inst_tys ++ extra_tys) }
845
846 -- The axiom must *not* be oversaturated
847 findBranch :: [CoAxBranch] -- branches to check
848 -> BranchIndex -- index of current branch
849 -> [Type] -- target types
850 -> Maybe (BranchIndex, [Type])
851 findBranch (CoAxBranch { cab_tvs = tpl_tvs, cab_lhs = tpl_lhs, cab_incomps = incomps }
852 : rest) ind target_tys
853 = case tcMatchTys (mkVarSet tpl_tvs) tpl_lhs target_tys of
854 Just subst -- matching worked. now, check for apartness.
855 | all (isSurelyApart
856 . tcUnifyTysFG instanceBindFun flattened_target
857 . coAxBranchLHS) incomps
858 -> -- matching worked & we're apart from all incompatible branches. success
859 Just (ind, substTyVars subst tpl_tvs)
860
861 -- failure. keep looking
862 _ -> findBranch rest (ind+1) target_tys
863
864 where isSurelyApart SurelyApart = True
865 isSurelyApart _ = False
866
867 -- See Note [Flattening] below
868 flattened_target = flattenTys in_scope target_tys
869 in_scope = mkInScopeSet (unionVarSets $
870 map (tyVarsOfTypes . coAxBranchLHS) incomps)
871
872 -- fail if no branches left
873 findBranch [] _ _ = Nothing
874
875 {-
876 ************************************************************************
877 * *
878 Looking up a family instance
879 * *
880 ************************************************************************
881 -}
882
883 topNormaliseType :: FamInstEnvs -> Type -> Type
884 topNormaliseType env ty = case topNormaliseType_maybe env ty of
885 Just (_co, ty') -> ty'
886 Nothing -> ty
887
888 topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Coercion, Type)
889
890 -- ^ Get rid of *outermost* (or toplevel)
891 -- * type function redex
892 -- * data family redex
893 -- * newtypes
894 -- returning an appropriate Representaitonal coercion. Specifically, if
895 -- topNormaliseType_maybe env ty = Maybe (co, ty')
896 -- then
897 -- (a) co :: ty ~R ty'
898 -- (b) ty' is not a newtype, and is not a type-family or data-family redex
899 --
900 -- However, ty' can be something like (Maybe (F ty)), where
901 -- (F ty) is a redex.
902 --
903 -- Its a bit like Type.repType, but handles type families too
904
905 topNormaliseType_maybe env ty
906 = topNormaliseTypeX_maybe stepper ty
907 where
908 stepper = unwrapNewTypeStepper `composeSteppers` tyFamStepper
909
910 tyFamStepper rec_nts tc tys -- Try to step a type/data familiy
911 = let (args_co, ntys) = normaliseTcArgs env Representational tc tys in
912 case reduceTyFamApp_maybe env Representational tc ntys of
913 Just (co, rhs) -> NS_Step rec_nts rhs (args_co `mkTransCo` co)
914 Nothing -> NS_Done
915
916 ---------------
917 normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> (Coercion, Type)
918 -- See comments on normaliseType for the arguments of this function
919 normaliseTcApp env role tc tys
920 | isTypeSynonymTyCon tc
921 , Just (tenv, rhs, ntys') <- expandSynTyCon_maybe tc ntys
922 , (co2, ninst_rhs) <- normaliseType env role (Type.substTy (mkTopTvSubst tenv) rhs)
923 = if isReflCo co2 then (args_co, mkTyConApp tc ntys)
924 else (args_co `mkTransCo` co2, mkAppTys ninst_rhs ntys')
925
926 | Just (first_co, ty') <- reduceTyFamApp_maybe env role tc ntys
927 , (rest_co,nty) <- normaliseType env role ty'
928 = (args_co `mkTransCo` first_co `mkTransCo` rest_co, nty)
929
930 | otherwise -- No unique matching family instance exists;
931 -- we do not do anything
932 = (args_co, mkTyConApp tc ntys)
933
934 where
935 (args_co, ntys) = normaliseTcArgs env role tc tys
936
937
938 ---------------
939 normaliseTcArgs :: FamInstEnvs -- environment with family instances
940 -> Role -- desired role of output coercion
941 -> TyCon -> [Type] -- tc tys
942 -> (Coercion, [Type]) -- (co, new_tys), where
943 -- co :: tc tys ~ tc new_tys
944 normaliseTcArgs env role tc tys
945 = (mkTyConAppCo role tc cois, ntys)
946 where
947 (cois, ntys) = zipWithAndUnzip (normaliseType env) (tyConRolesX role tc) tys
948
949 ---------------
950 normaliseType :: FamInstEnvs -- environment with family instances
951 -> Role -- desired role of output coercion
952 -> Type -- old type
953 -> (Coercion, Type) -- (coercion,new type), where
954 -- co :: old-type ~ new_type
955 -- Normalise the input type, by eliminating *all* type-function redexes
956 -- but *not* newtypes (which are visible to the programmer)
957 -- Returns with Refl if nothing happens
958 -- Try to not to disturb type synonyms if possible
959
960 normaliseType env role (TyConApp tc tys)
961 = normaliseTcApp env role tc tys
962 normaliseType _env role ty@(LitTy {}) = (mkReflCo role ty, ty)
963 normaliseType env role (AppTy ty1 ty2)
964 = let (coi1,nty1) = normaliseType env role ty1
965 (coi2,nty2) = normaliseType env Nominal ty2
966 in (mkAppCo coi1 coi2, mkAppTy nty1 nty2)
967 normaliseType env role (FunTy ty1 ty2)
968 = let (coi1,nty1) = normaliseType env role ty1
969 (coi2,nty2) = normaliseType env role ty2
970 in (mkFunCo role coi1 coi2, mkFunTy nty1 nty2)
971 normaliseType env role (ForAllTy tyvar ty1)
972 = let (coi,nty1) = normaliseType env role ty1
973 in (mkForAllCo tyvar coi, ForAllTy tyvar nty1)
974 normaliseType _ role ty@(TyVarTy _)
975 = (mkReflCo role ty,ty)
976
977 {-
978 ************************************************************************
979 * *
980 Flattening
981 * *
982 ************************************************************************
983
984 Note [Flattening]
985 ~~~~~~~~~~~~~~~~~
986 As described in "Closed type families with overlapping equations"
987 http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
988 we need to flatten core types before unifying them, when checking for "surely-apart"
989 against earlier equations of a closed type family.
990 Flattening means replacing all top-level uses of type functions with
991 fresh variables, *taking care to preserve sharing*. That is, the type
992 (Either (F a b) (F a b)) should flatten to (Either c c), never (Either
993 c d).
994
995 Here is a nice example of why it's all necessary:
996
997 type family F a b where
998 F Int Bool = Char
999 F a b = Double
1000 type family G a -- open, no instances
1001
1002 How do we reduce (F (G Float) (G Float))? The first equation clearly doesn't match,
1003 while the second equation does. But, before reducing, we must make sure that the
1004 target can never become (F Int Bool). Well, no matter what G Float becomes, it
1005 certainly won't become *both* Int and Bool, so indeed we're safe reducing
1006 (F (G Float) (G Float)) to Double.
1007
1008 This is necessary not only to get more reductions (which we might be
1009 willing to give up on), but for substitutivity. If we have (F x x), we
1010 can see that (F x x) can reduce to Double. So, it had better be the
1011 case that (F blah blah) can reduce to Double, no matter what (blah)
1012 is! Flattening as done below ensures this.
1013
1014 flattenTys is defined here because of module dependencies.
1015 -}
1016
1017 type FlattenMap = TypeMap TyVar
1018
1019 -- See Note [Flattening]
1020 flattenTys :: InScopeSet -> [Type] -> [Type]
1021 flattenTys in_scope tys = snd $ coreFlattenTys all_in_scope emptyTypeMap tys
1022 where
1023 -- when we hit a type function, we replace it with a fresh variable
1024 -- but, we need to make sure that this fresh variable isn't mentioned
1025 -- *anywhere* in the types we're flattening, even if locally-bound in
1026 -- a forall. That way, we can ensure consistency both within and outside
1027 -- of that forall.
1028 all_in_scope = in_scope `extendInScopeSetSet` allTyVarsInTys tys
1029
1030 coreFlattenTys :: InScopeSet -> FlattenMap -> [Type] -> (FlattenMap, [Type])
1031 coreFlattenTys in_scope = go []
1032 where
1033 go rtys m [] = (m, reverse rtys)
1034 go rtys m (ty : tys)
1035 = let (m', ty') = coreFlattenTy in_scope m ty in
1036 go (ty' : rtys) m' tys
1037
1038 coreFlattenTy :: InScopeSet -> FlattenMap -> Type -> (FlattenMap, Type)
1039 coreFlattenTy in_scope = go
1040 where
1041 go m ty | Just ty' <- coreView ty = go m ty'
1042
1043 go m ty@(TyVarTy {}) = (m, ty)
1044 go m (AppTy ty1 ty2) = let (m1, ty1') = go m ty1
1045 (m2, ty2') = go m1 ty2 in
1046 (m2, AppTy ty1' ty2')
1047 go m (TyConApp tc tys)
1048 | isFamilyTyCon tc
1049 = let (m', tv) = coreFlattenTyFamApp in_scope m tc tys in
1050 (m', mkTyVarTy tv)
1051
1052 | otherwise
1053 = let (m', tys') = coreFlattenTys in_scope m tys in
1054 (m', mkTyConApp tc tys')
1055
1056 go m (FunTy ty1 ty2) = let (m1, ty1') = go m ty1
1057 (m2, ty2') = go m1 ty2 in
1058 (m2, FunTy ty1' ty2')
1059
1060 -- Note to RAE: this will have to be changed with kind families
1061 go m (ForAllTy tv ty) = let (m', ty') = go m ty in
1062 (m', ForAllTy tv ty')
1063
1064 go m ty@(LitTy {}) = (m, ty)
1065
1066 coreFlattenTyFamApp :: InScopeSet -> FlattenMap
1067 -> TyCon -- type family tycon
1068 -> [Type] -- args
1069 -> (FlattenMap, TyVar)
1070 coreFlattenTyFamApp in_scope m fam_tc fam_args
1071 = case lookupTypeMap m fam_ty of
1072 Just tv -> (m, tv)
1073 -- we need fresh variables here, but this is called far from
1074 -- any good source of uniques. So, we just use the fam_tc's unique
1075 -- and trust uniqAway to avoid clashes. Recall that the in_scope set
1076 -- contains *all* tyvars, even locally bound ones elsewhere in the
1077 -- overall type, so this really is fresh.
1078 Nothing -> let tyvar_name = mkSysTvName (getUnique fam_tc) (fsLit "fl")
1079 tv = uniqAway in_scope $ mkTyVar tyvar_name (typeKind fam_ty)
1080 m' = extendTypeMap m fam_ty tv in
1081 (m', tv)
1082 where fam_ty = TyConApp fam_tc fam_args
1083
1084 allTyVarsInTys :: [Type] -> VarSet
1085 allTyVarsInTys [] = emptyVarSet
1086 allTyVarsInTys (ty:tys) = allTyVarsInTy ty `unionVarSet` allTyVarsInTys tys
1087
1088 allTyVarsInTy :: Type -> VarSet
1089 allTyVarsInTy = go
1090 where
1091 go (TyVarTy tv) = unitVarSet tv
1092 go (AppTy ty1 ty2) = (go ty1) `unionVarSet` (go ty2)
1093 go (TyConApp _ tys) = allTyVarsInTys tys
1094 go (FunTy ty1 ty2) = (go ty1) `unionVarSet` (go ty2)
1095 go (ForAllTy tv ty) = (go (tyVarKind tv)) `unionVarSet`
1096 unitVarSet tv `unionVarSet`
1097 (go ty) -- don't remove tv
1098 go (LitTy {}) = emptyVarSet