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