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