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