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