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