Don't use deriveUnique *twice* in flattenTys.
[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 :: Name -> [TyVar] -> TyCon -> [Type] -> Type -> CoAxiom Unbranched
555 mkSingleCoAxiom ax_name tvs fam_tc lhs_tys rhs_ty
556 = CoAxiom { co_ax_unique = nameUnique ax_name
557 , co_ax_name = ax_name
558 , co_ax_tc = fam_tc
559 , co_ax_role = Nominal
560 , co_ax_implicit = False
561 , co_ax_branches = FirstBranch (branch { cab_incomps = [] }) }
562 where
563 branch = mkCoAxBranch tvs lhs_tys rhs_ty (getSrcSpan ax_name)
564
565 {-
566 ************************************************************************
567 * *
568 Looking up a family instance
569 * *
570 ************************************************************************
571
572 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
573 Multiple matches are only possible in case of type families (not data
574 families), and then, it doesn't matter which match we choose (as the
575 instances are guaranteed confluent).
576
577 We return the matching family instances and the type instance at which it
578 matches. For example, if we lookup 'T [Int]' and have a family instance
579
580 data instance T [a] = ..
581
582 desugared to
583
584 data :R42T a = ..
585 coe :Co:R42T a :: T [a] ~ :R42T a
586
587 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
588 -}
589
590 -- when matching a type family application, we get a FamInst,
591 -- and the list of types the axiom should be applied to
592 data FamInstMatch = FamInstMatch { fim_instance :: FamInst
593 , fim_tys :: [Type]
594 }
595 -- See Note [Over-saturated matches]
596
597 instance Outputable FamInstMatch where
598 ppr (FamInstMatch { fim_instance = inst
599 , fim_tys = tys })
600 = ptext (sLit "match with") <+> parens (ppr inst) <+> ppr tys
601
602 lookupFamInstEnv
603 :: FamInstEnvs
604 -> TyCon -> [Type] -- What we are looking for
605 -> [FamInstMatch] -- Successful matches
606 -- Precondition: the tycon is saturated (or over-saturated)
607
608 lookupFamInstEnv
609 = lookup_fam_inst_env match
610 where
611 match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
612
613 lookupFamInstEnvConflicts
614 :: FamInstEnvs
615 -> FamInst -- Putative new instance
616 -> [FamInstMatch] -- Conflicting matches (don't look at the fim_tys field)
617 -- E.g. when we are about to add
618 -- f : type instance F [a] = a->a
619 -- we do (lookupFamInstConflicts f [b])
620 -- to find conflicting matches
621 --
622 -- Precondition: the tycon is saturated (or over-saturated)
623
624 lookupFamInstEnvConflicts envs fam_inst@(FamInst { fi_axiom = new_axiom })
625 = lookup_fam_inst_env my_unify envs fam tys
626 where
627 (fam, tys) = famInstSplitLHS fam_inst
628 -- In example above, fam tys' = F [b]
629
630 my_unify (FamInst { fi_axiom = old_axiom }) tpl_tvs tpl_tys _
631 = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
632 (ppr fam <+> ppr tys) $$
633 (ppr tpl_tvs <+> ppr tpl_tys) )
634 -- Unification will break badly if the variables overlap
635 -- They shouldn't because we allocate separate uniques for them
636 if compatibleBranches (coAxiomSingleBranch old_axiom) new_branch
637 then Nothing
638 else Just noSubst
639 -- Note [Family instance overlap conflicts]
640
641 noSubst = panic "lookupFamInstEnvConflicts noSubst"
642 new_branch = coAxiomSingleBranch new_axiom
643
644 {-
645 Note [Family instance overlap conflicts]
646 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
647 - In the case of data family instances, any overlap is fundamentally a
648 conflict (as these instances imply injective type mappings).
649
650 - In the case of type family instances, overlap is admitted as long as
651 the right-hand sides of the overlapping rules coincide under the
652 overlap substitution. eg
653 type instance F a Int = a
654 type instance F Int b = b
655 These two overlap on (F Int Int) but then both RHSs are Int,
656 so all is well. We require that they are syntactically equal;
657 anything else would be difficult to test for at this stage.
658 -}
659
660 ------------------------------------------------------------
661 -- Might be a one-way match or a unifier
662 type MatchFun = FamInst -- The FamInst template
663 -> TyVarSet -> [Type] -- fi_tvs, fi_tys of that FamInst
664 -> [Type] -- Target to match against
665 -> Maybe TvSubst
666
667 lookup_fam_inst_env' -- The worker, local to this module
668 :: MatchFun
669 -> FamInstEnv
670 -> TyCon -> [Type] -- What we are looking for
671 -> [FamInstMatch]
672 lookup_fam_inst_env' match_fun ie fam match_tys
673 | isOpenFamilyTyCon fam
674 , Just (FamIE insts) <- lookupUFM ie fam
675 = find insts -- The common case
676 | otherwise = []
677 where
678
679 find [] = []
680 find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs,
681 fi_tys = tpl_tys }) : rest)
682 -- Fast check for no match, uses the "rough match" fields
683 | instanceCantMatch rough_tcs mb_tcs
684 = find rest
685
686 -- Proper check
687 | Just subst <- match_fun item (mkVarSet tpl_tvs) tpl_tys match_tys1
688 = (FamInstMatch { fim_instance = item
689 , fim_tys = substTyVars subst tpl_tvs `chkAppend` match_tys2 })
690 : find rest
691
692 -- No match => try next
693 | otherwise
694 = find rest
695
696 where
697 (rough_tcs, match_tys1, match_tys2) = split_tys tpl_tys
698
699 -- Precondition: the tycon is saturated (or over-saturated)
700
701 -- Deal with over-saturation
702 -- See Note [Over-saturated matches]
703 split_tys tpl_tys
704 | isTypeFamilyTyCon fam
705 = pre_rough_split_tys
706
707 | otherwise
708 = let (match_tys1, match_tys2) = splitAtList tpl_tys match_tys
709 rough_tcs = roughMatchTcs match_tys1
710 in (rough_tcs, match_tys1, match_tys2)
711
712 (pre_match_tys1, pre_match_tys2) = splitAt (tyConArity fam) match_tys
713 pre_rough_split_tys
714 = (roughMatchTcs pre_match_tys1, pre_match_tys1, pre_match_tys2)
715
716 lookup_fam_inst_env -- The worker, local to this module
717 :: MatchFun
718 -> FamInstEnvs
719 -> TyCon -> [Type] -- What we are looking for
720 -> [FamInstMatch] -- Successful matches
721
722 -- Precondition: the tycon is saturated (or over-saturated)
723
724 lookup_fam_inst_env match_fun (pkg_ie, home_ie) fam tys
725 = lookup_fam_inst_env' match_fun home_ie fam tys
726 ++ lookup_fam_inst_env' match_fun pkg_ie fam tys
727
728 {-
729 Note [Over-saturated matches]
730 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
731 It's ok to look up an over-saturated type constructor. E.g.
732 type family F a :: * -> *
733 type instance F (a,b) = Either (a->b)
734
735 The type instance gives rise to a newtype TyCon (at a higher kind
736 which you can't do in Haskell!):
737 newtype FPair a b = FP (Either (a->b))
738
739 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
740 (FPair, [Int,Bool,Char])
741 The "extra" type argument [Char] just stays on the end.
742
743 We handle data families and type families separately here:
744
745 * For type families, all instances of a type family must have the
746 same arity, so we can precompute the split between the match_tys
747 and the overflow tys. This is done in pre_rough_split_tys.
748
749 * For data family instances, though, we need to re-split for each
750 instance, because the breakdown might be different for each
751 instance. Why? Because of eta reduction; see Note [Eta reduction
752 for data family axioms] in TcInstDcls.
753 -}
754
755 -- checks if one LHS is dominated by a list of other branches
756 -- in other words, if an application would match the first LHS, it is guaranteed
757 -- to match at least one of the others. The RHSs are ignored.
758 -- This algorithm is conservative:
759 -- True -> the LHS is definitely covered by the others
760 -- False -> no information
761 -- It is currently (Oct 2012) used only for generating errors for
762 -- inaccessible branches. If these errors go unreported, no harm done.
763 -- This is defined here to avoid a dependency from CoAxiom to Unify
764 isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool
765 isDominatedBy branch branches
766 = or $ map match branches
767 where
768 lhs = coAxBranchLHS branch
769 match (CoAxBranch { cab_tvs = tvs, cab_lhs = tys })
770 = isJust $ tcMatchTys (mkVarSet tvs) tys lhs
771
772 {-
773 ************************************************************************
774 * *
775 Choosing an axiom application
776 * *
777 ************************************************************************
778
779 The lookupFamInstEnv function does a nice job for *open* type families,
780 but we also need to handle closed ones when normalising a type:
781 -}
782
783 reduceTyFamApp_maybe :: FamInstEnvs
784 -> Role -- Desired role of result coercion
785 -> TyCon -> [Type]
786 -> Maybe (Coercion, Type)
787 -- Attempt to do a *one-step* reduction of a type-family application
788 -- but *not* newtypes
789 -- Works on type-synonym families always; data-families only if
790 -- the role we seek is representational
791 -- It does *not* normlise the type arguments first, so this may not
792 -- go as far as you want. If you want normalised type arguments,
793 -- use normaliseTcArgs first.
794 --
795 -- The TyCon can be oversaturated.
796 -- Works on both open and closed families
797
798 reduceTyFamApp_maybe envs role tc tys
799 | Phantom <- role
800 = Nothing
801
802 | case role of
803 Representational -> isOpenFamilyTyCon tc
804 _ -> isOpenTypeFamilyTyCon tc
805 -- If we seek a representational coercion
806 -- (e.g. the call in topNormaliseType_maybe) then we can
807 -- unwrap data families as well as type-synonym families;
808 -- otherwise only type-synonym families
809 , FamInstMatch { fim_instance = fam_inst
810 , fim_tys = inst_tys } : _ <- lookupFamInstEnv envs tc tys
811 -- NB: Allow multiple matches because of compatible overlap
812
813 = let ax = famInstAxiom fam_inst
814 co = mkUnbranchedAxInstCo role ax inst_tys
815 ty = pSnd (coercionKind co)
816 in Just (co, ty)
817
818 | Just ax <- isClosedSynFamilyTyCon_maybe tc
819 , Just (ind, inst_tys) <- chooseBranch ax tys
820 = let co = mkAxInstCo role ax ind inst_tys
821 ty = pSnd (coercionKind co)
822 in Just (co, ty)
823
824 | Just ax <- isBuiltInSynFamTyCon_maybe tc
825 , Just (coax,ts,ty) <- sfMatchFam ax tys
826 = let co = mkAxiomRuleCo coax ts []
827 in Just (co, ty)
828
829 | otherwise
830 = Nothing
831
832 -- The axiom can be oversaturated. (Closed families only.)
833 chooseBranch :: CoAxiom Branched -> [Type] -> Maybe (BranchIndex, [Type])
834 chooseBranch axiom tys
835 = do { let num_pats = coAxiomNumPats axiom
836 (target_tys, extra_tys) = splitAt num_pats tys
837 branches = coAxiomBranches axiom
838 ; (ind, inst_tys) <- findBranch (fromBranchList branches) 0 target_tys
839 ; return (ind, inst_tys ++ extra_tys) }
840
841 -- The axiom must *not* be oversaturated
842 findBranch :: [CoAxBranch] -- branches to check
843 -> BranchIndex -- index of current branch
844 -> [Type] -- target types
845 -> Maybe (BranchIndex, [Type])
846 findBranch (CoAxBranch { cab_tvs = tpl_tvs, cab_lhs = tpl_lhs, cab_incomps = incomps }
847 : rest) ind target_tys
848 = case tcMatchTys (mkVarSet tpl_tvs) tpl_lhs target_tys of
849 Just subst -- matching worked. now, check for apartness.
850 | all (isSurelyApart
851 . tcUnifyTysFG instanceBindFun flattened_target
852 . coAxBranchLHS) incomps
853 -> -- matching worked & we're apart from all incompatible branches. success
854 Just (ind, substTyVars subst tpl_tvs)
855
856 -- failure. keep looking
857 _ -> findBranch rest (ind+1) target_tys
858
859 where isSurelyApart SurelyApart = True
860 isSurelyApart _ = False
861
862 flattened_target = flattenTys in_scope target_tys
863 in_scope = mkInScopeSet (unionVarSets $
864 map (tyVarsOfTypes . coAxBranchLHS) incomps)
865
866 -- fail if no branches left
867 findBranch [] _ _ = Nothing
868
869 {-
870 ************************************************************************
871 * *
872 Looking up a family instance
873 * *
874 ************************************************************************
875 -}
876
877 topNormaliseType :: FamInstEnvs -> Type -> Type
878 topNormaliseType env ty = case topNormaliseType_maybe env ty of
879 Just (_co, ty') -> ty'
880 Nothing -> ty
881
882 topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Coercion, Type)
883
884 -- ^ Get rid of *outermost* (or toplevel)
885 -- * type function redex
886 -- * newtypes
887 -- using appropriate coercions. Specifically, if
888 -- topNormaliseType_maybe env ty = Maybe (co, ty')
889 -- then
890 -- (a) co :: ty ~ ty'
891 -- (b) ty' is not a newtype, and is not a type-family redex
892 --
893 -- However, ty' can be something like (Maybe (F ty)), where
894 -- (F ty) is a redex.
895 --
896 -- Its a bit like Type.repType, but handles type families too
897 -- The coercion returned is always an R coercion
898
899 topNormaliseType_maybe env ty
900 = topNormaliseTypeX_maybe stepper ty
901 where
902 stepper
903 = unwrapNewTypeStepper
904 `composeSteppers`
905 \ rec_nts tc tys ->
906 let (args_co, ntys) = normaliseTcArgs env Representational tc tys in
907 case reduceTyFamApp_maybe env Representational tc ntys of
908 Just (co, rhs) -> NS_Step rec_nts rhs (args_co `mkTransCo` co)
909 Nothing -> NS_Done
910
911 ---------------
912 normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> (Coercion, Type)
913 -- See comments on normaliseType for the arguments of this function
914 normaliseTcApp env role tc tys
915 | isTypeSynonymTyCon tc
916 , Just (tenv, rhs, ntys') <- expandSynTyCon_maybe tc ntys
917 , (co2, ninst_rhs) <- normaliseType env role (Type.substTy (mkTopTvSubst tenv) rhs)
918 = if isReflCo co2 then (args_co, mkTyConApp tc ntys)
919 else (args_co `mkTransCo` co2, mkAppTys ninst_rhs ntys')
920
921 | Just (first_co, ty') <- reduceTyFamApp_maybe env role tc ntys
922 , (rest_co,nty) <- normaliseType env role ty'
923 = (args_co `mkTransCo` first_co `mkTransCo` rest_co, nty)
924
925 | otherwise -- No unique matching family instance exists;
926 -- we do not do anything
927 = (args_co, mkTyConApp tc ntys)
928
929 where
930 (args_co, ntys) = normaliseTcArgs env role tc tys
931
932
933 ---------------
934 normaliseTcArgs :: FamInstEnvs -- environment with family instances
935 -> Role -- desired role of output coercion
936 -> TyCon -> [Type] -- tc tys
937 -> (Coercion, [Type]) -- (co, new_tys), where
938 -- co :: tc tys ~ tc new_tys
939 normaliseTcArgs env role tc tys
940 = (mkTyConAppCo role tc cois, ntys)
941 where
942 (cois, ntys) = zipWithAndUnzip (normaliseType env) (tyConRolesX role tc) tys
943
944 ---------------
945 normaliseType :: FamInstEnvs -- environment with family instances
946 -> Role -- desired role of output coercion
947 -> Type -- old type
948 -> (Coercion, Type) -- (coercion,new type), where
949 -- co :: old-type ~ new_type
950 -- Normalise the input type, by eliminating *all* type-function redexes
951 -- but *not* newtypes (which are visible to the programmer)
952 -- Returns with Refl if nothing happens
953 -- Try to not to disturb type syonyms if possible
954
955 normaliseType env role (TyConApp tc tys)
956 = normaliseTcApp env role tc tys
957 normaliseType _env role ty@(LitTy {}) = (mkReflCo role ty, ty)
958 normaliseType env role (AppTy ty1 ty2)
959 = let (coi1,nty1) = normaliseType env role ty1
960 (coi2,nty2) = normaliseType env Nominal ty2
961 in (mkAppCo coi1 coi2, mkAppTy nty1 nty2)
962 normaliseType env role (FunTy ty1 ty2)
963 = let (coi1,nty1) = normaliseType env role ty1
964 (coi2,nty2) = normaliseType env role ty2
965 in (mkFunCo role coi1 coi2, mkFunTy nty1 nty2)
966 normaliseType env role (ForAllTy tyvar ty1)
967 = let (coi,nty1) = normaliseType env role ty1
968 in (mkForAllCo tyvar coi, ForAllTy tyvar nty1)
969 normaliseType _ role ty@(TyVarTy _)
970 = (mkReflCo role ty,ty)
971
972 {-
973 ************************************************************************
974 * *
975 Flattening
976 * *
977 ************************************************************************
978
979 Note [Flattening]
980 ~~~~~~~~~~~~~~~~~
981
982 As described in
983 http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
984 we sometimes need to flatten core types before unifying them. Flattening
985 means replacing all top-level uses of type functions with fresh variables,
986 taking care to preserve sharing. That is, the type (Either (F a b) (F a b)) should
987 flatten to (Either c c), never (Either c d).
988
989 Here is a nice example of why it's all necessary:
990
991 type family F a b where
992 F Int Bool = Char
993 F a b = Double
994 type family G a -- open, no instances
995
996 How do we reduce (F (G Float) (G Float))? The first equation clearly doesn't match,
997 while the second equation does. But, before reducing, we must make sure that the
998 target can never become (F Int Bool). Well, no matter what G Float becomes, it
999 certainly won't become *both* Int and Bool, so indeed we're safe reducing
1000 (F (G Float) (G Float)) to Double.
1001
1002 This is necessary not only to get more reductions, but for substitutivity. If
1003 we have (F x x), we can see that (F x x) can reduce to Double. So, it had better
1004 be the case that (F blah blah) can reduce to Double, no matter what (blah) is!
1005 Flattening as done below ensures this.
1006
1007 Defined here because of module dependencies.
1008 -}
1009
1010 type FlattenMap = TypeMap TyVar
1011
1012 -- See Note [Flattening]
1013 flattenTys :: InScopeSet -> [Type] -> [Type]
1014 flattenTys in_scope tys = snd $ coreFlattenTys all_in_scope emptyTypeMap tys
1015 where
1016 -- when we hit a type function, we replace it with a fresh variable
1017 -- but, we need to make sure that this fresh variable isn't mentioned
1018 -- *anywhere* in the types we're flattening, even if locally-bound in
1019 -- a forall. That way, we can ensure consistency both within and outside
1020 -- of that forall.
1021 all_in_scope = in_scope `extendInScopeSetSet` allTyVarsInTys tys
1022
1023 coreFlattenTys :: InScopeSet -> FlattenMap -> [Type] -> (FlattenMap, [Type])
1024 coreFlattenTys in_scope = go []
1025 where
1026 go rtys m [] = (m, reverse rtys)
1027 go rtys m (ty : tys)
1028 = let (m', ty') = coreFlattenTy in_scope m ty in
1029 go (ty' : rtys) m' tys
1030
1031 coreFlattenTy :: InScopeSet -> FlattenMap -> Type -> (FlattenMap, Type)
1032 coreFlattenTy in_scope = go
1033 where
1034 go m ty@(TyVarTy {}) = (m, ty)
1035 go m (AppTy ty1 ty2) = let (m1, ty1') = go m ty1
1036 (m2, ty2') = go m1 ty2 in
1037 (m2, AppTy ty1' ty2')
1038 go m (TyConApp tc tys)
1039 | isFamilyTyCon tc
1040 = let (m', tv) = coreFlattenTyFamApp in_scope m tc tys in
1041 (m', mkTyVarTy tv)
1042
1043 | otherwise
1044 = let (m', tys') = coreFlattenTys in_scope m tys in
1045 (m', mkTyConApp tc tys')
1046
1047 go m (FunTy ty1 ty2) = let (m1, ty1') = go m ty1
1048 (m2, ty2') = go m1 ty2 in
1049 (m2, FunTy ty1' ty2')
1050
1051 -- Note to RAE: this will have to be changed with kind families
1052 go m (ForAllTy tv ty) = let (m', ty') = go m ty in
1053 (m', ForAllTy tv ty')
1054
1055 go m ty@(LitTy {}) = (m, ty)
1056
1057 coreFlattenTyFamApp :: InScopeSet -> FlattenMap
1058 -> TyCon -- type family tycon
1059 -> [Type] -- args
1060 -> (FlattenMap, TyVar)
1061 coreFlattenTyFamApp in_scope m fam_tc fam_args
1062 = case lookupTypeMap m fam_ty of
1063 Just tv -> (m, tv)
1064 -- we need fresh variables here, but this is called far from
1065 -- any good source of uniques. So, we just use the fam_tc's unique
1066 -- and trust uniqAway to avoid clashes. Recall that the in_scope set
1067 -- contains *all* tyvars, even locally bound ones elsewhere in the
1068 -- overall type, so this really is fresh.
1069 Nothing -> let tyvar_name = mkSysTvName (getUnique fam_tc) (fsLit "fl")
1070 tv = uniqAway in_scope $ mkTyVar tyvar_name (typeKind fam_ty)
1071 m' = extendTypeMap m fam_ty tv in
1072 (m', tv)
1073 where fam_ty = TyConApp fam_tc fam_args
1074
1075 allTyVarsInTys :: [Type] -> VarSet
1076 allTyVarsInTys [] = emptyVarSet
1077 allTyVarsInTys (ty:tys) = allTyVarsInTy ty `unionVarSet` allTyVarsInTys tys
1078
1079 allTyVarsInTy :: Type -> VarSet
1080 allTyVarsInTy = go
1081 where
1082 go (TyVarTy tv) = unitVarSet tv
1083 go (AppTy ty1 ty2) = (go ty1) `unionVarSet` (go ty2)
1084 go (TyConApp _ tys) = allTyVarsInTys tys
1085 go (FunTy ty1 ty2) = (go ty1) `unionVarSet` (go ty2)
1086 go (ForAllTy tv ty) = (go (tyVarKind tv)) `unionVarSet`
1087 unitVarSet tv `unionVarSet`
1088 (go ty) -- don't remove tv
1089 go (LitTy {}) = emptyVarSet