Merge branch 'master' of http://darcs.haskell.org/ghc
[ghc.git] / compiler / types / FamInstEnv.lhs
1 %
2 % (c) The University of Glasgow 2006
3 %
4
5 FamInstEnv: Type checked family instance declarations
6
7 \begin{code}
8 module FamInstEnv (
9         Branched, Unbranched,
10
11         FamInst(..), FamFlavor(..), FamInstBranch(..), 
12
13         famInstAxiom, famInstBranchRoughMatch,
14         famInstsRepTyCons, famInstNthBranch, famInstSingleBranch,
15         famInstBranchLHS, famInstBranches, 
16         toBranchedFamInst, toUnbranchedFamInst,
17         famInstTyCon, famInstRepTyCon_maybe, dataFamInstRepTyCon, 
18         pprFamInst, pprFamInsts, 
19         pprFamFlavor, 
20         mkImportedFamInst, 
21
22         FamInstEnv, FamInstEnvs,
23         emptyFamInstEnvs, emptyFamInstEnv, famInstEnvElts, familyInstances,
24         extendFamInstEnvList, extendFamInstEnv, deleteFromFamInstEnv,
25         identicalFamInst,
26
27         FamInstMatch(..),
28         lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvConflicts',
29         
30         isDominatedBy,
31
32         -- Normalisation
33         topNormaliseType, normaliseType, normaliseTcApp
34     ) where
35
36 #include "HsVersions.h"
37
38 import InstEnv
39 import Unify
40 import Type
41 import Coercion hiding ( substTy )
42 import TypeRep
43 import TyCon
44 import CoAxiom
45 import VarSet
46 import VarEnv
47 import Name
48 import UniqFM
49 import Outputable
50 import Maybes
51 import Util
52 import FastString
53 \end{code}
54
55
56 %************************************************************************
57 %*                                                                      *
58            Type checked family instance heads
59 %*                                                                      *
60 %************************************************************************
61
62 Note [FamInsts and CoAxioms]
63 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
64 * CoAxioms and FamInsts are just like
65   DFunIds  and ClsInsts
66
67 * A CoAxiom is a System-FC thing: it can relate any two types
68
69 * A FamInst is a Haskell source-language thing, corresponding
70   to a type/data family instance declaration.
71     - The FamInst contains a CoAxiom, which is the evidence
72       for the instance
73
74     - The LHSs of the CoAxiom branches are always of form
75       F ty1 .. tyn where F is a type family
76
77 * A FamInstBranch corresponds to a CoAxBranch -- it represents
78   one alternative in a family instance group. We could theoretically
79   not have FamInstBranches and just use the CoAxBranches within
80   the CoAxiom stored in the FamInst, but for one problem: we want to
81   cache the "rough match" top-level tycon names for quick matching.
82   This data is not stored in a CoAxBranch, so we use FamInstBranches
83   instead.
84
85 Note [fi_group field]
86 ~~~~~~~~~~~~~~~~~~~~~
87 A FamInst stores whether or not it was declared with "type instance where"
88 for two reasons: 
89   1. for accurate pretty-printing; and 
90   2. because confluent overlap is disallowed between branches 
91      declared in groups. 
92 Note that this "group-ness" is properly associated with the FamInst,
93 which thinks about overlap, and not in the CoAxiom, which blindly
94 assumes that it is part of a consistent axiom set.
95
96 A "group" with fi_group=True can have just one element, however.
97
98 Note [Why we need fib_rhs]
99 ~~~~~~~~~~~~~~~~~~~~~~~~~~
100 It may at first seem unnecessary to store the right-hand side of an equation
101 in a FamInstBranch. After all, FamInstBranches are used only for matching a
102 family application; the underlying CoAxiom is used to perform the actual
103 simplification.
104
105 However, we do need to know the rhs field during conflict checking to support
106 confluent overlap. When two unbranched instances have overlapping left-hand
107 sides, we check if the right-hand sides are coincident in the region of overlap.
108 This check requires fib_rhs. See lookupFamInstEnvConflicts.
109
110 \begin{code}
111 data FamInst br -- See Note [FamInsts and CoAxioms], Note [Branched axioms] in CoAxiom
112   = FamInst { fi_axiom    :: CoAxiom br      -- The new coercion axiom introduced
113                                              -- by this family instance
114             , fi_flavor   :: FamFlavor
115             , fi_group    :: Bool            -- True <=> declared with "type instance where"
116                                              -- See Note [fi_group field]
117
118             -- Everything below here is a redundant,
119             -- cached version of the two things above,
120             -- except that the TyVars are freshened in the FamInstBranches
121             , fi_branches :: BranchList FamInstBranch br
122                                              -- Haskell-source-language view of 
123                                              -- a CoAxBranch
124             , fi_fam      :: Name            -- Family name
125                 -- INVARIANT: fi_fam = name of fi_axiom.co_ax_tc
126             }
127
128 data FamInstBranch
129   = FamInstBranch
130     { fib_tvs    :: [TyVar]      -- Bound type variables
131                                  -- Like ClsInsts, these variables are always
132                                  -- fresh. See Note [Template tyvars are fresh]
133                                  -- in InstEnv
134     , fib_lhs    :: [Type]       -- type patterns
135     , fib_rhs    :: Type         -- RHS of family instance
136                                  -- See Note [Why we need fib_rhs]
137     , fib_tcs    :: [Maybe Name] -- used for "rough matching" during typechecking
138                                  -- see Note [Rough-match field] in InstEnv
139     }
140
141 data FamFlavor 
142   = SynFamilyInst         -- A synonym family
143   | DataFamilyInst TyCon  -- A data family, with its representation TyCon
144 \end{code}
145
146
147 \begin{code}
148 -- Obtain the axiom of a family instance
149 famInstAxiom :: FamInst br -> CoAxiom br
150 famInstAxiom = fi_axiom
151
152 famInstTyCon :: FamInst br -> TyCon
153 famInstTyCon = co_ax_tc . fi_axiom
154
155 famInstNthBranch :: FamInst br -> Int -> FamInstBranch
156 famInstNthBranch (FamInst { fi_branches = branches }) index
157   = ASSERT( 0 <= index && index < (length $ fromBranchList branches) )
158     brListNth branches index 
159
160 famInstSingleBranch :: FamInst Unbranched -> FamInstBranch
161 famInstSingleBranch (FamInst { fi_branches = FirstBranch branch }) = branch
162
163 toBranchedFamInst :: FamInst br -> FamInst Branched
164 toBranchedFamInst (FamInst ax flav grp branches fam)
165   = FamInst (toBranchedAxiom ax) flav grp (toBranchedList branches) fam
166
167 toUnbranchedFamInst :: FamInst br -> FamInst Unbranched
168 toUnbranchedFamInst (FamInst ax flav grp branches fam)
169   = FamInst (toUnbranchedAxiom ax) flav grp (toUnbranchedList branches) fam
170
171 famInstBranches :: FamInst br -> BranchList FamInstBranch br
172 famInstBranches = fi_branches
173
174 famInstBranchLHS :: FamInstBranch -> [Type]
175 famInstBranchLHS = fib_lhs
176
177 famInstBranchRoughMatch :: FamInstBranch -> [Maybe Name]
178 famInstBranchRoughMatch = fib_tcs
179
180 -- Return the representation TyCons introduced by data family instances, if any
181 famInstsRepTyCons :: [FamInst br] -> [TyCon]
182 famInstsRepTyCons fis = [tc | FamInst { fi_flavor = DataFamilyInst tc } <- fis]
183
184 -- Extracts the TyCon for this *data* (or newtype) instance
185 famInstRepTyCon_maybe :: FamInst br -> Maybe TyCon
186 famInstRepTyCon_maybe fi
187   = case fi_flavor fi of
188        DataFamilyInst tycon -> Just tycon
189        SynFamilyInst        -> Nothing
190
191 dataFamInstRepTyCon :: FamInst br -> TyCon
192 dataFamInstRepTyCon fi
193   = case fi_flavor fi of
194        DataFamilyInst tycon -> tycon
195        SynFamilyInst        -> pprPanic "dataFamInstRepTyCon" (ppr fi)
196 \end{code}
197
198 %************************************************************************
199 %*                                                                      *
200         Pretty printing
201 %*                                                                      *
202 %************************************************************************
203
204 \begin{code}
205 instance NamedThing (FamInst br) where
206    getName = coAxiomName . fi_axiom
207
208 instance Outputable (FamInst br) where
209    ppr = pprFamInst
210
211 -- Prints the FamInst as a family instance declaration
212 pprFamInst :: FamInst br -> SDoc
213 pprFamInst (FamInst { fi_branches = brs, fi_flavor = SynFamilyInst
214                     , fi_group = True, fi_axiom = axiom })
215   = hang (ptext (sLit "type instance where"))
216        2 (vcat [pprCoAxBranchHdr axiom i | i <- brListIndices brs])
217
218 pprFamInst fi@(FamInst { fi_flavor = flavor
219                        , fi_group = False, fi_axiom = ax })
220   = pprFamFlavor flavor <+> pp_instance
221     <+> pprCoAxBranchHdr ax 0
222   where
223     -- For *associated* types, say "type T Int = blah" 
224     -- For *top level* type instances, say "type instance T Int = blah"
225     pp_instance 
226       | isTyConAssoc (famInstTyCon fi) = empty
227       | otherwise                      = ptext (sLit "instance")
228
229 pprFamInst _ = panic "pprFamInst"
230
231 pprFamFlavor :: FamFlavor -> SDoc
232 pprFamFlavor flavor
233   = case flavor of
234       SynFamilyInst        -> ptext (sLit "type")
235       DataFamilyInst tycon
236         | isDataTyCon     tycon -> ptext (sLit "data")
237         | isNewTyCon      tycon -> ptext (sLit "newtype")
238         | isAbstractTyCon tycon -> ptext (sLit "data")
239         | otherwise             -> ptext (sLit "WEIRD") <+> ppr tycon
240
241 pprFamInsts :: [FamInst br] -> SDoc
242 pprFamInsts finsts = vcat (map pprFamInst finsts)
243 \end{code}
244
245 Note [Lazy axiom match]
246 ~~~~~~~~~~~~~~~~~~~~~~~
247 It is Vitally Important that mkImportedFamInst is *lazy* in its axiom
248 parameter. The axiom is loaded lazily, via a forkM, in TcIface. Sometime
249 later, mkImportedFamInst is called using that axiom. However, the axiom
250 may itself depend on entities which are not yet loaded as of the time
251 of the mkImportedFamInst. Thus, if mkImportedFamInst eagerly looks at the
252 axiom, a dependency loop spontaneously appears and GHC hangs. The solution
253 is simply for mkImportedFamInst never, ever to look inside of the axiom
254 until everything else is good and ready to do so. We can assume that this
255 readiness has been achieved when some other code pulls on the axiom in the
256 FamInst. Thus, we pattern match on the axiom lazily (in the where clause,
257 not in the parameter list) and we assert the consistency of names there
258 also.
259
260 \begin{code}
261
262 -- Make a family instance representation from the information found in an
263 -- interface file.  In particular, we get the rough match info from the iface
264 -- (instead of computing it here).
265 mkImportedFamInst :: Name               -- Name of the family
266                   -> Bool               -- is this a group?
267                   -> [[Maybe Name]]     -- Rough match info, per branch
268                   -> CoAxiom Branched   -- Axiom introduced
269                   -> FamInst Branched   -- Resulting family instance
270 mkImportedFamInst fam group roughs axiom
271   = FamInst {
272       fi_fam      = fam,
273       fi_axiom    = axiom,
274       fi_flavor   = flavor,
275       fi_group    = group,
276       fi_branches = branches }
277   where
278      -- Lazy match (See note [Lazy axiom match])
279      CoAxiom { co_ax_branches = axBranches }
280        = ASSERT( fam == tyConName (coAxiomTyCon axiom) )
281          axiom
282
283      branches = toBranchList $ map mk_imp_fam_inst_branch $ 
284                 (roughs `zipLazy` fromBranchList axBranches)
285                 -- Lazy zip (See note [Lazy axiom match])
286
287      mk_imp_fam_inst_branch (mb_tcs, ~(CoAxBranch { cab_tvs = tvs
288                                                   , cab_lhs = lhs
289                                                   , cab_rhs = rhs }))
290                 -- Lazy match (See note [Lazy axiom match])
291        = FamInstBranch { fib_tvs    = tvs
292                        , fib_lhs    = lhs
293                        , fib_rhs    = rhs
294                        , fib_tcs    = mb_tcs }
295
296          -- Derive the flavor for an imported FamInst rather disgustingly
297          -- Maybe we should store it in the IfaceFamInst?
298      flavor
299        | FirstBranch (CoAxBranch { cab_rhs = rhs }) <- axBranches
300        , Just (tc, _) <- splitTyConApp_maybe rhs
301        , Just ax' <- tyConFamilyCoercion_maybe tc
302        , (toBranchedAxiom ax') == axiom
303        = DataFamilyInst tc
304
305        | otherwise
306        = SynFamilyInst
307 \end{code}
308
309
310 %************************************************************************
311 %*                                                                      *
312                 FamInstEnv
313 %*                                                                      *
314 %************************************************************************
315
316 Note [FamInstEnv]
317 ~~~~~~~~~~~~~~~~~~~~~
318 A FamInstEnv maps a family name to the list of known instances for that family.
319
320 The same FamInstEnv includes both 'data family' and 'type family' instances.
321 Type families are reduced during type inference, but not data families;
322 the user explains when to use a data family instance by using contructors
323 and pattern matching.
324
325 Neverthless it is still useful to have data families in the FamInstEnv:
326
327  - For finding overlaps and conflicts
328
329  - For finding the representation type...see FamInstEnv.topNormaliseType
330    and its call site in Simplify
331
332  - In standalone deriving instance Eq (T [Int]) we need to find the
333    representation type for T [Int]
334
335 \begin{code}
336 type FamInstEnv = UniqFM FamilyInstEnv  -- Maps a family to its instances
337      -- See Note [FamInstEnv]
338
339 type FamInstEnvs = (FamInstEnv, FamInstEnv)
340      -- External package inst-env, Home-package inst-env
341
342 newtype FamilyInstEnv
343   = FamIE [FamInst Branched] -- The instances for a particular family, in any order
344
345 instance Outputable FamilyInstEnv where
346   ppr (FamIE fs) = ptext (sLit "FamIE") <+> vcat (map ppr fs)
347
348 -- INVARIANTS:
349 --  * The fs_tvs are distinct in each FamInst
350 --      of a range value of the map (so we can safely unify them)
351
352 emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
353 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
354
355 emptyFamInstEnv :: FamInstEnv
356 emptyFamInstEnv = emptyUFM
357
358 famInstEnvElts :: FamInstEnv -> [FamInst Branched]
359 famInstEnvElts fi = [elt | FamIE elts <- eltsUFM fi, elt <- elts]
360
361 familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst Branched]
362 familyInstances (pkg_fie, home_fie) fam
363   = get home_fie ++ get pkg_fie
364   where
365     get env = case lookupUFM env fam of
366                 Just (FamIE insts) -> insts
367                 Nothing            -> []
368
369 extendFamInstEnvList :: FamInstEnv -> [FamInst br] -> FamInstEnv
370 extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis
371
372 extendFamInstEnv :: FamInstEnv -> FamInst br -> FamInstEnv
373 extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm})
374   = addToUFM_C add inst_env cls_nm (FamIE [ins_item_br])
375   where
376     ins_item_br = toBranchedFamInst ins_item
377     add (FamIE items) _ = FamIE (ins_item_br:items)
378
379 deleteFromFamInstEnv :: FamInstEnv -> FamInst br -> FamInstEnv
380 deleteFromFamInstEnv inst_env fam_inst@(FamInst {fi_fam = fam_nm})
381  = adjustUFM adjust inst_env fam_nm
382  where
383    adjust :: FamilyInstEnv -> FamilyInstEnv
384    adjust (FamIE items) = FamIE (filterOut (identicalFamInst fam_inst) items)
385
386 identicalFamInst :: FamInst br1 -> FamInst br2 -> Bool
387 -- Same LHS, *and* the instance is defined in the same module
388 -- Used for overriding in GHCi
389 identicalFamInst (FamInst { fi_axiom = ax1 }) (FamInst { fi_axiom = ax2 })
390   =  nameModule (coAxiomName ax1) == nameModule (coAxiomName ax2)
391      && coAxiomTyCon ax1 == coAxiomTyCon ax2
392      && brListLength brs1 == brListLength brs2
393      && and (brListZipWith identical_ax_branch brs1 brs2)
394   where brs1 = coAxiomBranches ax1
395         brs2 = coAxiomBranches ax2
396         identical_ax_branch br1 br2
397           = length tvs1 == length tvs2
398             && length lhs1 == length lhs2
399             && and (zipWith (eqTypeX rn_env) lhs1 lhs2)
400           where
401             tvs1 = coAxBranchTyVars br1
402             tvs2 = coAxBranchTyVars br2
403             lhs1 = coAxBranchLHS br1
404             lhs2 = coAxBranchLHS br2
405             rn_env = rnBndrs2 (mkRnEnv2 emptyInScopeSet) tvs1 tvs2
406                        
407 \end{code}
408
409 %************************************************************************
410 %*                                                                      *
411                 Looking up a family instance
412 %*                                                                      *
413 %************************************************************************
414
415 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
416 Multiple matches are only possible in case of type families (not data
417 families), and then, it doesn't matter which match we choose (as the
418 instances are guaranteed confluent).
419
420 We return the matching family instances and the type instance at which it
421 matches.  For example, if we lookup 'T [Int]' and have a family instance
422
423   data instance T [a] = ..
424
425 desugared to
426
427   data :R42T a = ..
428   coe :Co:R42T a :: T [a] ~ :R42T a
429
430 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
431
432 Note [Instance checking within groups]
433 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
434
435 Consider the following:
436
437 type instance where
438   F Int = Bool
439   F a   = Int
440
441 g :: Show a => a -> F a
442 g x = length (show x)
443
444 Should that type-check? No. We need to allow for the possibility
445 that 'a' might be Int and therefore 'F a' should be Bool. We can
446 simplify 'F a' to Int only when we can be sure that 'a' is not Int.
447
448 To achieve this, after finding a possible match within an instance group, we
449 have to go back to all previous FamInstBranchess and check that, under the
450 substitution induced by the match, other matches are not possible. This is
451 similar to what happens with class instance selection, when we need to
452 guarantee that there is only a match and no unifiers. The exact algorithm is
453 different here because the the potentially-overlapping group is closed.
454
455 ALTERNATE APPROACH: As we are processing the branches, we could check if an
456 instance unifies but does not match. If this happens, there is no possible
457 match and we can fail right away. This might be more efficient.
458
459 Note [Early failure optimisation for instance groups]
460 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
461 As we're searching through the instances for a match, it is
462 possible that we find an branch within an instance that matches, but
463 a previous branch still unifies. In this case, we can abort the
464 search, because any other instance that matches will necessarily
465 overlap with the instance group we're currently searching. Because
466 overlap among instance groups is disallowed, we know that that
467 no such other instance exists.
468
469 Note [Confluence checking within groups]
470 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
471 GHC allows type family instances to have overlapping patterns as long as the
472 right-hand sides are coincident in the region of overlap. Can we extend this
473 notion of confluent overlap to branched instances? Not in any obvious way.
474
475 Consider this:
476
477 type instance where
478   F Int = Int
479   F a = a
480
481 Without confluence checking (in other words, as implemented), we cannot now
482 simplify an application of (F b) -- b might unify with Int later on, so this
483 application is stuck. However, it would seem easy to just check that, in the
484 region of overlap, (i.e. b |-> Int), the right-hand sides coincide, so we're
485 OK. The problem happens when we are simplifying an application (F (G a)),
486 where (G a) is stuck. What, now, is the region of overlap? We can't soundly
487 simplify (F (G a)) without knowing that the right-hand sides are confluent
488 in the region of overlap, but we also can't in any obvious way identify the
489 region of overlap. We don't want to do analysis on the instances of G, because
490 that is not sound in a world with open type families. (If G were known to be
491 closed, there might be a way forward here.) To find the region of overlap,
492 it is conceivable that we might convert (G a) to some fresh type variable and
493 then unify, but we must be careful to convert every (G a) to the same fresh
494 type variable. And then, what if there is an (H a) lying around? It all seems
495 rather subtle, error-prone, confusing, and probably won't help anyone. So,
496 we're not doing it.
497
498 So, why is this not a problem with non-branched confluent overlap? Because
499 we don't need to verify that an application is apart from anything. The
500 non-branched confluent overlap check happens when we add the instance to the
501 environment -- we're unifying among patterns, which cannot contain type family
502 appplications. So, we're safe there and can continue supporting that feature.
503
504 \begin{code}
505 -- when matching a type family application, we get a FamInst,
506 -- a 0-based index of the branch that matched, and the list of types
507 -- the axiom should be applied to
508 data FamInstMatch = FamInstMatch { fim_instance :: FamInst Branched
509                                  , fim_index    :: BranchIndex
510                                  , fim_tys      :: [Type]
511                                  }
512
513 instance Outputable FamInstMatch where
514   ppr (FamInstMatch { fim_instance = inst
515                     , fim_index    = ind
516                     , fim_tys      = tys })
517     = ptext (sLit "match with") <+> parens (ppr inst)
518         <> brackets (ppr ind) <+> ppr tys
519
520 lookupFamInstEnv
521     :: FamInstEnvs
522     -> TyCon -> [Type]          -- What we are looking for
523     -> [FamInstMatch]           -- Successful matches
524 -- Precondition: the tycon is saturated (or over-saturated)
525
526 lookupFamInstEnv
527   = lookup_fam_inst_env match True
528   where
529     match :: MatchFun
530     match seen (FamInstBranch { fib_tvs = tpl_tvs
531                               , fib_lhs = tpl_tys })
532           _ match_tys 
533       = ASSERT( tyVarsOfTypes match_tys `disjointVarSet` tpl_tv_set )
534                 -- Unification will break badly if the variables overlap
535                 -- They shouldn't because we allocate separate uniques for them
536         case tcMatchTys tpl_tv_set tpl_tys match_tys of
537           -- success
538           Just subst
539             | checkConflict seen match_tys
540             -> (Nothing, StopSearching) -- we found an incoherence, so stop searching
541             -- see Note [Early failure optimisation for instance groups]
542
543             | otherwise
544             -> (Just subst, KeepSearching)
545
546           -- failure; instance not relevant
547           Nothing -> (Nothing, KeepSearching) 
548       where
549         tpl_tv_set = mkVarSet tpl_tvs
550
551     -- see Note [Instance checking within groups]
552     checkConflict :: [FamInstBranch] -- the previous branches in the instance that matched
553                   -> [Type]          -- the types in the tyfam application we are matching
554                   -> Bool            -- is there a conflict?
555     checkConflict [] _ = False
556     checkConflict ((FamInstBranch { fib_lhs = tpl_tys }) : rest) match_tys
557           -- see Note [Confluence checking within groups]
558       | SurelyApart <- tcApartTys instanceBindFun tpl_tys match_tys
559       = checkConflict rest match_tys
560       | otherwise
561       = True
562
563 lookupFamInstEnvConflicts
564     :: FamInstEnvs
565     -> Bool             -- True <=> we are checking part of a group with other branches
566     -> TyCon            -- The TyCon of the family
567     -> FamInstBranch    -- the putative new instance branch
568     -> [FamInstMatch]   -- Conflicting branches
569 -- E.g. when we are about to add
570 --    f : type instance F [a] = a->a
571 -- we do (lookupFamInstConflicts f [b])
572 -- to find conflicting matches
573 --
574 -- Precondition: the tycon is saturated (or over-saturated)
575
576 lookupFamInstEnvConflicts envs grp tc
577                           (FamInstBranch { fib_lhs = tys, fib_rhs = rhs })
578   = lookup_fam_inst_env my_unify False envs tc tys
579   where
580     my_unify :: MatchFun
581     my_unify _ (FamInstBranch { fib_tvs = tpl_tvs, fib_lhs = tpl_tys
582                               , fib_rhs = tpl_rhs }) old_grp match_tys
583        = ASSERT( tyVarsOfTypes tys `disjointVarSet` mkVarSet tpl_tvs )
584                 -- Unification will break badly if the variables overlap
585                 -- They shouldn't because we allocate separate uniques for them
586          case tcUnifyTys instanceBindFun tpl_tys match_tys of
587               Just subst
588                 |  isDataFamilyTyCon tc
589                 || grp
590                 || old_grp
591                 || rhs_conflict tpl_rhs rhs subst
592                 -> (Just subst, KeepSearching)
593                 | otherwise -- confluent overlap
594                 -> (Nothing, KeepSearching)
595               -- irrelevant instance
596               Nothing -> (Nothing, KeepSearching)
597
598     -- checks whether two RHSs are distinct, under a unifying substitution
599     -- Note [Family instance overlap conflicts]
600     rhs_conflict :: Type -> Type -> TvSubst -> Bool
601     rhs_conflict rhs1 rhs2 subst 
602       = not (rhs1' `eqType` rhs2')
603         where
604           rhs1' = substTy subst rhs1
605           rhs2' = substTy subst rhs2
606
607 -- This variant is called when we want to check if the conflict is only in the
608 -- home environment (see FamInst.addLocalFamInst)
609 lookupFamInstEnvConflicts' :: FamInstEnv -> Bool -> TyCon 
610                            -> FamInstBranch -> [FamInstMatch]
611 lookupFamInstEnvConflicts' env
612   = lookupFamInstEnvConflicts (emptyFamInstEnv, env)
613 \end{code}
614
615 Note [lookup_fam_inst_env' implementation]
616 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
617 To reduce code duplication, both lookups during simplification and conflict
618 checking are routed through lookup_fam_inst_env', which looks for a
619 matching/unifying branch compared to some target. In the simplification
620 case, the search is for a match for a target application; in the conflict-
621 checking case, the search is for a unifier for a putative new instance branch.
622
623 The two uses are differentiated by different MatchFuns, which look at a given
624 branch to see if it is relevant and whether the search should continue. The
625 the branch is relevant (i.e. matches or unifies), Just subst is
626 returned; if the instance is not relevant, Nothing is returned. The MatchFun
627 also indicates what the search algorithm should do next: it could
628 KeepSearching or StopSearching.
629
630 When to StopSearching? See Note [Early failure optimisation for instance groups]
631
632 For class instances, these two variants of lookup are combined into one
633 function (cf, @InstEnv@).  We don't do that for family instances as the
634 results of matching and unification are used in two different contexts.
635 Moreover, matching is the wildly more frequently used operation in the case of
636 indexed synonyms and we don't want to slow that down by needless unification.
637
638 Note [Family instance overlap conflicts]
639 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
640 - In the case of data family instances, any overlap is fundamentally a
641   conflict (as these instances imply injective type mappings).
642
643 - In the case of type family instances, overlap is admitted as long as
644   the neither instance declares an instance group and the right-hand
645   sides of the overlapping rules coincide under the overlap substitution.
646   For example:
647        type instance F a Int = a
648        type instance F Int b = b
649   These two overlap on (F Int Int) but then both RHSs are Int,
650   so all is well. We require that they are syntactically equal;
651   anything else would be difficult to test for at this stage.
652
653 \begin{code}
654 ------------------------------------------------------------
655 data ContSearch = KeepSearching
656                 | StopSearching
657
658 -- Might be a one-way match or a unifier
659 type MatchFun =  [FamInstBranch]     -- the previous branches in the instance
660               -> FamInstBranch       -- the individual branch to check
661               -> Bool                -- is this branch a part of a group?
662               -> [Type]              -- the types to match against
663               -> (Maybe TvSubst, ContSearch)
664
665 type OneSidedMatch = Bool     -- Are optimisations that are only valid for
666                               -- one sided matches allowed?
667
668 lookup_fam_inst_env'          -- The worker, local to this module
669     :: MatchFun
670     -> OneSidedMatch
671     -> FamInstEnv
672     -> TyCon -> [Type]        -- What we are looking for
673     -> [FamInstMatch]
674 lookup_fam_inst_env' match_fun _one_sided ie fam tys
675   | isFamilyTyCon fam
676   , Just (FamIE insts) <- lookupUFM ie fam
677   = ASSERT2( n_tys >= arity, ppr fam <+> ppr tys ) 
678     if arity < n_tys then    -- Family type applications must be saturated
679                              -- See Note [Over-saturated matches]
680         map wrap_extra_tys (find match_fun (take arity tys) insts)
681     else
682         find match_fun tys insts    -- The common case
683
684   | otherwise = []
685   where
686     arity = tyConArity fam
687     n_tys = length tys
688     extra_tys = drop arity tys
689     wrap_extra_tys fim@(FamInstMatch { fim_tys = match_tys })
690       = fim { fim_tys = match_tys ++ extra_tys }
691
692
693 find :: MatchFun -> [Type] -> [FamInst Branched] -> [FamInstMatch]
694 find _         _         [] = []
695 find match_fun match_tys (inst@(FamInst { fi_branches = branches, fi_group = is_group }) : rest)
696   = case findBranch [] (fromBranchList branches) 0 of
697       (Just match, StopSearching) -> [match]
698       (Just match, KeepSearching) -> match : find match_fun match_tys rest
699       (Nothing,    StopSearching) -> []
700       (Nothing,    KeepSearching) -> find match_fun match_tys rest
701   where
702     rough_tcs = roughMatchTcs match_tys
703
704     findBranch :: [FamInstBranch]  -- the branches that have already been checked
705                -> [FamInstBranch]  -- still looking through these
706                -> BranchIndex      -- index of teh first of the "still looking" list
707                -> (Maybe FamInstMatch, ContSearch)
708     findBranch _ [] _ = (Nothing, KeepSearching)
709     findBranch seen (branch@(FamInstBranch { fib_tvs = tvs, fib_tcs = mb_tcs }) : rest) ind
710       | instanceCantMatch rough_tcs mb_tcs
711       = findBranch seen rest (ind+1) -- branch won't unify later; no need to add to 'seen'
712       | otherwise
713       = case match_fun seen branch is_group match_tys of
714           (Nothing, KeepSearching) -> findBranch (branch : seen) rest (ind+1)
715           (Nothing, StopSearching) -> (Nothing, StopSearching)
716           (Just subst, cont)       -> (Just match, cont)
717               where 
718                 match = FamInstMatch { fim_instance = inst
719                                      , fim_index    = ind
720                                      , fim_tys      = substTyVars subst tvs }
721
722 lookup_fam_inst_env           -- The worker, local to this module
723     :: MatchFun
724     -> OneSidedMatch
725     -> FamInstEnvs
726     -> TyCon -> [Type]          -- What we are looking for
727     -> [FamInstMatch]           -- What was found
728
729 -- Precondition: the tycon is saturated (or over-saturated)
730 lookup_fam_inst_env match_fun one_sided (pkg_ie, home_ie) fam tys = 
731     lookup_fam_inst_env' match_fun one_sided home_ie fam tys ++
732     lookup_fam_inst_env' match_fun one_sided pkg_ie  fam tys
733 \end{code}
734
735 Note [Over-saturated matches]
736 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
737 It's ok to look up an over-saturated type constructor.  E.g.
738      type family F a :: * -> *
739      type instance F (a,b) = Either (a->b)
740
741 The type instance gives rise to a newtype TyCon (at a higher kind
742 which you can't do in Haskell!):
743      newtype FPair a b = FP (Either (a->b))
744
745 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
746      (FPair, [Int,Bool,Char])
747
748 The "extra" type argument [Char] just stays on the end.
749
750 \begin{code}
751
752 -- checks if one LHS is dominated by a list of other branches
753 -- in other words, if an application would match the first LHS, it is guaranteed
754 -- to match at least one of the others. The RHSs are ignored.
755 -- This algorithm is conservative:
756 --   True -> the LHS is definitely covered by the others
757 --   False -> no information
758 -- It is currently (Oct 2012) used only for generating errors for
759 -- inaccessible branches. If these errors go unreported, no harm done.
760 -- This is defined here to avoid a dependency from CoAxiom to Unify
761 isDominatedBy :: [Type] -> [CoAxBranch] -> Bool
762 isDominatedBy lhs branches
763   = or $ map match branches
764     where
765       match (CoAxBranch { cab_tvs = tvs, cab_lhs = tys })
766         = isJust $ tcMatchTys (mkVarSet tvs) tys lhs
767 \end{code}
768
769
770 %************************************************************************
771 %*                                                                      *
772                 Looking up a family instance
773 %*                                                                      *
774 %************************************************************************
775
776 \begin{code}
777 topNormaliseType :: FamInstEnvs
778                  -> Type
779                  -> Maybe (Coercion, Type)
780
781 -- Get rid of *outermost* (or toplevel)
782 --      * type functions
783 --      * newtypes
784 -- using appropriate coercions.
785 -- By "outer" we mean that toplevelNormaliseType guarantees to return
786 -- a type that does not have a reducible redex (F ty1 .. tyn) as its
787 -- outermost form.  It *can* return something like (Maybe (F ty)), where
788 -- (F ty) is a redex.
789
790 -- Its a bit like Type.repType, but handles type families too
791
792 topNormaliseType env ty
793   = go [] ty
794   where
795     go :: [TyCon] -> Type -> Maybe (Coercion, Type)
796     go rec_nts ty | Just ty' <- coreView ty     -- Expand synonyms
797         = go rec_nts ty'
798
799     go rec_nts (TyConApp tc tys)
800         | isNewTyCon tc         -- Expand newtypes
801         = if tc `elem` rec_nts  -- See Note [Expanding newtypes] in Type.lhs
802           then Nothing
803           else let 
804                in add_co nt_co rec_nts' nt_rhs
805
806         | isFamilyTyCon tc              -- Expand open tycons
807         , (co, ty) <- normaliseTcApp env tc tys
808                 -- Note that normaliseType fully normalises 'tys',
809                 -- It has do to so to be sure that nested calls like
810                 --    F (G Int)
811                 -- are correctly top-normalised
812         , not (isReflCo co)
813         = add_co co rec_nts ty
814         where
815           nt_co  = mkUnbranchedAxInstCo (newTyConCo tc) tys
816           nt_rhs = newTyConInstRhs      tc              tys
817           rec_nts' | isRecursiveTyCon tc = tc:rec_nts
818                    | otherwise           = rec_nts
819
820     go _ _ = Nothing
821
822     add_co co rec_nts ty
823         = case go rec_nts ty of
824                 Nothing         -> Just (co, ty)
825                 Just (co', ty') -> Just (mkTransCo co co', ty')
826
827
828 ---------------
829 normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (Coercion, Type)
830 normaliseTcApp env tc tys
831   | isFamilyTyCon tc
832   , tyConArity tc <= length tys    -- Unsaturated data families are possible
833   , [FamInstMatch { fim_instance = fam_inst
834                   , fim_index    = fam_ind
835                   , fim_tys      = inst_tys }] <- lookupFamInstEnv env tc ntys 
836   = let    -- A matching family instance exists
837         ax              = famInstAxiom fam_inst
838         co              = mkAxInstCo  ax fam_ind inst_tys
839         rhs             = mkAxInstRHS ax fam_ind inst_tys
840         first_coi       = mkTransCo tycon_coi co
841         (rest_coi,nty)  = normaliseType env rhs
842         fix_coi         = mkTransCo first_coi rest_coi
843     in 
844     (fix_coi, nty)
845
846   | otherwise   -- No unique matching family instance exists;
847                 -- we do not do anything
848   = (tycon_coi, TyConApp tc ntys)
849
850   where
851         -- Normalise the arg types so that they'll match
852         -- when we lookup in in the instance envt
853     (cois, ntys) = mapAndUnzip (normaliseType env) tys
854     tycon_coi    = mkTyConAppCo tc cois
855
856 ---------------
857 normaliseType :: FamInstEnvs            -- environment with family instances
858               -> Type                   -- old type
859               -> (Coercion, Type)       -- (coercion,new type), where
860                                         -- co :: old-type ~ new_type
861 -- Normalise the input type, by eliminating *all* type-function redexes
862 -- Returns with Refl if nothing happens
863
864 normaliseType env ty
865   | Just ty' <- coreView ty = normaliseType env ty'
866 normaliseType env (TyConApp tc tys)
867   = normaliseTcApp env tc tys
868 normaliseType _env ty@(LitTy {}) = (Refl ty, ty)
869 normaliseType env (AppTy ty1 ty2)
870   = let (coi1,nty1) = normaliseType env ty1
871         (coi2,nty2) = normaliseType env ty2
872     in  (mkAppCo coi1 coi2, mkAppTy nty1 nty2)
873 normaliseType env (FunTy ty1 ty2)
874   = let (coi1,nty1) = normaliseType env ty1
875         (coi2,nty2) = normaliseType env ty2
876     in  (mkFunCo coi1 coi2, mkFunTy nty1 nty2)
877 normaliseType env (ForAllTy tyvar ty1)
878   = let (coi,nty1) = normaliseType env ty1
879     in  (mkForAllCo tyvar coi, ForAllTy tyvar nty1)
880 normaliseType _   ty@(TyVarTy _)
881   = (Refl ty,ty)
882 \end{code}