5b4374afa2e834cad5c9f283e805baf5d82a4462
[ghc.git] / compiler / types / FamInstEnv.lhs
1 %
2 % (c) The University of Glasgow 2006
3 %
4
5 FamInstEnv: Type checked family instance declarations
6
7 \begin{code}
8 module FamInstEnv (
9         FamInst(..), famInstTyCon, famInstTyVars, 
10         pprFamInst, pprFamInstHdr, pprFamInsts, 
11         famInstHead, mkLocalFamInst, mkImportedFamInst,
12
13         FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs, 
14         extendFamInstEnv, extendFamInstEnvList, 
15         famInstEnvElts, familyInstances,
16
17         lookupFamInstEnv, lookupFamInstEnvConflicts,
18         
19         -- Normalisation
20         topNormaliseType
21     ) where
22
23 #include "HsVersions.h"
24
25 import InstEnv
26 import Unify
27 import Type
28 import TypeRep
29 import TyCon
30 import Coercion
31 import VarSet
32 import Name
33 import UniqFM
34 import Outputable
35 import Maybes
36 import Util
37 import FastString
38 \end{code}
39
40
41 %************************************************************************
42 %*                                                                      *
43 \subsection{Type checked family instance heads}
44 %*                                                                      *
45 %************************************************************************
46
47 \begin{code}
48 data FamInst 
49   = FamInst { fi_fam   :: Name          -- Family name
50                 -- INVARIANT: fi_fam = case tyConFamInst_maybe fi_tycon of
51                 --                         Just (tc, tys) -> tc
52
53                 -- Used for "rough matching"; same idea as for class instances
54             , fi_tcs   :: [Maybe Name]  -- Top of type args
55                 -- INVARIANT: fi_tcs = roughMatchTcs fi_tys
56
57                 -- Used for "proper matching"; ditto
58             , fi_tvs   :: TyVarSet      -- Template tyvars for full match
59             , fi_tys   :: [Type]        -- Full arg types
60                 -- INVARIANT: fi_tvs = tyConTyVars fi_tycon
61                 --            fi_tys = case tyConFamInst_maybe fi_tycon of
62                 --                         Just (_, tys) -> tys
63
64             , fi_tycon :: TyCon         -- Representation tycon
65             }
66
67 -- Obtain the representation tycon of a family instance.
68 --
69 famInstTyCon :: FamInst -> TyCon
70 famInstTyCon = fi_tycon
71
72 famInstTyVars :: FamInst -> TyVarSet
73 famInstTyVars = fi_tvs
74 \end{code}
75
76 \begin{code}
77 instance NamedThing FamInst where
78    getName = getName . fi_tycon
79
80 instance Outputable FamInst where
81    ppr = pprFamInst
82
83 -- Prints the FamInst as a family instance declaration
84 pprFamInst :: FamInst -> SDoc
85 pprFamInst famInst
86   = hang (pprFamInstHdr famInst)
87        2 (vcat [ ifPprDebug (ptext (sLit "Coercion axiom:") <+> pp_ax)
88                , ptext (sLit "--") <+> pprNameLoc (getName famInst)])
89   where
90     pp_ax = case tyConFamilyCoercion_maybe (fi_tycon famInst) of
91               Just ax -> ppr ax
92               Nothing -> ptext (sLit "<not there!>")
93
94 pprFamInstHdr :: FamInst -> SDoc
95 pprFamInstHdr (FamInst {fi_tycon = rep_tc})
96   = pprTyConSort <+> pp_instance <+> pprHead
97   where
98     Just (fam_tc, tys) = tyConFamInst_maybe rep_tc 
99     
100     -- For *associated* types, say "type T Int = blah" 
101     -- For *top level* type instances, say "type instance T Int = blah"
102     pp_instance 
103       | isTyConAssoc fam_tc = empty
104       | otherwise           = ptext (sLit "instance")
105
106     pprHead = pprTypeApp fam_tc tys
107     pprTyConSort | isDataTyCon     rep_tc = ptext (sLit "data")
108                  | isNewTyCon      rep_tc = ptext (sLit "newtype")
109                  | isSynTyCon      rep_tc = ptext (sLit "type")
110                  | isAbstractTyCon rep_tc = ptext (sLit "data")
111                  | otherwise              = panic "FamInstEnv.pprFamInstHdr"
112
113 pprFamInsts :: [FamInst] -> SDoc
114 pprFamInsts finsts = vcat (map pprFamInst finsts)
115
116 famInstHead :: FamInst -> ([TyVar], TyCon, [Type])
117 famInstHead (FamInst {fi_tycon = tycon})
118   = case tyConFamInst_maybe tycon of
119       Nothing         -> panic "FamInstEnv.famInstHead"
120       Just (fam, tys) -> (tyConTyVars tycon, fam, tys)
121
122 -- Make a family instance representation from a tycon.  This is used for local
123 -- instances, where we can safely pull on the tycon.
124 --
125 mkLocalFamInst :: TyCon -> FamInst
126 mkLocalFamInst tycon
127   = case tyConFamInst_maybe tycon of
128            Nothing         -> panic "FamInstEnv.mkLocalFamInst"
129            Just (fam, tys) -> 
130              FamInst {
131                fi_fam   = tyConName fam,
132                fi_tcs   = roughMatchTcs tys,
133                fi_tvs   = mkVarSet . tyConTyVars $ tycon,
134                fi_tys   = tys,
135                fi_tycon = tycon
136              }
137
138 -- Make a family instance representation from the information found in an
139 -- unterface file.  In particular, we get the rough match info from the iface
140 -- (instead of computing it here).
141 --
142 mkImportedFamInst :: Name -> [Maybe Name] -> TyCon -> FamInst
143 mkImportedFamInst fam mb_tcs tycon
144   = FamInst {
145       fi_fam   = fam,
146       fi_tcs   = mb_tcs,
147       fi_tvs   = mkVarSet . tyConTyVars $ tycon,
148       fi_tys   = case tyConFamInst_maybe tycon of
149                    Nothing       -> panic "FamInstEnv.mkImportedFamInst"
150                    Just (_, tys) -> tys,
151       fi_tycon = tycon
152     }
153 \end{code}
154
155
156 %************************************************************************
157 %*                                                                      *
158                 FamInstEnv
159 %*                                                                      *
160 %************************************************************************
161
162 Note [FamInstEnv]
163 ~~~~~~~~~~~~~~~~~~~~~
164 A FamInstEnv maps a family name to the list of known instances for that family.
165
166 The same FamInstEnv includes both 'data family' and 'type family' instances.
167 Type families are reduced during type inference, but not data families;
168 the user explains when to use a data family instance by using contructors
169 and pattern matching.
170
171 Neverthless it is still useful to have data families in the FamInstEnv:
172
173  - For finding overlaps and conflicts
174
175  - For finding the representation type...see FamInstEnv.topNormaliseType
176    and its call site in Simplify
177
178  - In standalone deriving instance Eq (T [Int]) we need to find the 
179    representation type for T [Int]
180
181 \begin{code}
182 type FamInstEnv = UniqFM FamilyInstEnv  -- Maps a family to its instances
183      -- See Note [FamInstEnv]
184
185 type FamInstEnvs = (FamInstEnv, FamInstEnv)
186      -- External package inst-env, Home-package inst-env
187
188 data FamilyInstEnv
189   = FamIE [FamInst]     -- The instances for a particular family, in any order
190           Bool          -- True <=> there is an instance of form T a b c
191                         --      If *not* then the common case of looking up
192                         --      (T a b c) can fail immediately
193
194 instance Outputable FamilyInstEnv where
195   ppr (FamIE fs b) = ptext (sLit "FamIE") <+> ppr b <+> vcat (map ppr fs)
196
197 -- INVARIANTS:
198 --  * The fs_tvs are distinct in each FamInst
199 --      of a range value of the map (so we can safely unify them)
200
201 emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
202 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
203
204 emptyFamInstEnv :: FamInstEnv
205 emptyFamInstEnv = emptyUFM
206
207 famInstEnvElts :: FamInstEnv -> [FamInst]
208 famInstEnvElts fi = [elt | FamIE elts _ <- eltsUFM fi, elt <- elts]
209
210 familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
211 familyInstances (pkg_fie, home_fie) fam
212   = get home_fie ++ get pkg_fie
213   where
214     get env = case lookupUFM env fam of
215                 Just (FamIE insts _) -> insts
216                 Nothing              -> []
217
218 extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
219 extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis
220
221 extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
222 extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs})
223   = addToUFM_C add inst_env cls_nm (FamIE [ins_item] ins_tyvar)
224   where
225     add (FamIE items tyvar) _ = FamIE (ins_item:items)
226                                       (ins_tyvar || tyvar)
227     ins_tyvar = not (any isJust mb_tcs)
228 \end{code}
229
230 %************************************************************************
231 %*                                                                      *
232                 Looking up a family instance
233 %*                                                                      *
234 %************************************************************************
235
236 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
237 Multiple matches are only possible in case of type families (not data
238 families), and then, it doesn't matter which match we choose (as the
239 instances are guaranteed confluent).
240
241 We return the matching family instances and the type instance at which it
242 matches.  For example, if we lookup 'T [Int]' and have a family instance
243
244   data instance T [a] = ..
245
246 desugared to
247
248   data :R42T a = ..
249   coe :Co:R42T a :: T [a] ~ :R42T a
250
251 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
252
253 \begin{code}
254 type FamInstMatch = (FamInst, [Type])           -- Matching type instance
255   -- See Note [Over-saturated matches]
256
257 lookupFamInstEnv
258     :: FamInstEnvs
259     -> TyCon -> [Type]          -- What we are looking for
260     -> [FamInstMatch]           -- Successful matches
261 -- Precondition: the tycon is saturated (or over-saturated)
262
263 lookupFamInstEnv
264    = lookup_fam_inst_env match True
265    where
266      match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
267
268 lookupFamInstEnvConflicts
269     :: FamInstEnvs
270     -> FamInst          -- Putative new instance
271     -> [TyVar]          -- Unique tyvars, matching arity of FamInst
272     -> [FamInstMatch]   -- Conflicting matches
273 -- E.g. when we are about to add
274 --    f : type instance F [a] = a->a
275 -- we do (lookupFamInstConflicts f [b])
276 -- to find conflicting matches
277 -- The skolem tyvars are needed because we don't have a 
278 -- unique supply to hand
279 --
280 -- Precondition: the tycon is saturated (or over-saturated)
281
282 lookupFamInstEnvConflicts envs fam_inst skol_tvs
283   = lookup_fam_inst_env my_unify False envs fam tys'
284   where
285     inst_tycon = famInstTyCon fam_inst
286     (fam, tys) = expectJust "FamInstEnv.lookuFamInstEnvConflicts"
287                             (tyConFamInst_maybe inst_tycon)
288     skol_tys = mkTyVarTys skol_tvs
289     tys'     = substTys (zipTopTvSubst (tyConTyVars inst_tycon) skol_tys) tys
290         -- In example above,   fam tys' = F [b]   
291
292     my_unify old_fam_inst tpl_tvs tpl_tys match_tys
293        = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
294                   (ppr fam <+> ppr tys) $$
295                   (ppr tpl_tvs <+> ppr tpl_tys) )
296                 -- Unification will break badly if the variables overlap
297                 -- They shouldn't because we allocate separate uniques for them
298          case tcUnifyTys instanceBindFun tpl_tys match_tys of
299               Just subst | conflicting old_fam_inst subst -> Just subst
300               _other                                      -> Nothing
301
302       -- - In the case of data family instances, any overlap is fundamentally a
303       --   conflict (as these instances imply injective type mappings).
304       -- - In the case of type family instances, overlap is admitted as long as
305       --   the right-hand sides of the overlapping rules coincide under the
306       --   overlap substitution.  We require that they are syntactically equal;
307       --   anything else would be difficult to test for at this stage.
308     conflicting old_fam_inst subst 
309       | isAlgTyCon fam = True
310       | otherwise      = not (old_rhs `eqType` new_rhs)
311       where
312         old_tycon = famInstTyCon old_fam_inst
313         old_tvs   = tyConTyVars old_tycon
314         old_rhs   = mkTyConApp old_tycon  (substTyVars subst old_tvs)
315         new_rhs   = mkTyConApp inst_tycon (substTyVars subst skol_tvs)
316 \end{code}
317
318 While @lookupFamInstEnv@ uses a one-way match, the next function
319 @lookupFamInstEnvConflicts@ uses two-way matching (ie, unification).  This is
320 needed to check for overlapping instances.
321
322 For class instances, these two variants of lookup are combined into one
323 function (cf, @InstEnv@).  We don't do that for family instances as the
324 results of matching and unification are used in two different contexts.
325 Moreover, matching is the wildly more frequently used operation in the case of
326 indexed synonyms and we don't want to slow that down by needless unification.
327
328 \begin{code}
329 ------------------------------------------------------------
330 -- Might be a one-way match or a unifier
331 type MatchFun =  FamInst                -- The FamInst template
332               -> TyVarSet -> [Type]     --   fi_tvs, fi_tys of that FamInst
333               -> [Type]                 -- Target to match against
334               -> Maybe TvSubst
335
336 type OneSidedMatch = Bool     -- Are optimisations that are only valid for
337                               -- one sided matches allowed?
338
339 lookup_fam_inst_env           -- The worker, local to this module
340     :: MatchFun
341     -> OneSidedMatch
342     -> FamInstEnvs
343     -> TyCon -> [Type]          -- What we are looking for
344     -> [FamInstMatch]           -- Successful matches
345
346 -- Precondition: the tycon is saturated (or over-saturated)
347
348 lookup_fam_inst_env match_fun one_sided (pkg_ie, home_ie) fam tys
349   | not (isFamilyTyCon fam) 
350   = []
351   | otherwise
352   = ASSERT2( n_tys >= arity, ppr fam <+> ppr tys )      -- Family type applications must be saturated
353     home_matches ++ pkg_matches
354   where
355     home_matches = lookup home_ie 
356     pkg_matches  = lookup pkg_ie  
357
358     -- See Note [Over-saturated matches]
359     arity = tyConArity fam
360     n_tys = length tys
361     extra_tys = drop arity tys
362     (match_tys, add_extra_tys) 
363        | arity > n_tys = (take arity tys, \res_tys -> res_tys ++ extra_tys)
364        | otherwise     = (tys,            \res_tys -> res_tys)
365          -- The second case is the common one, hence functional representation
366
367     --------------
368     rough_tcs = roughMatchTcs match_tys
369     all_tvs   = all isNothing rough_tcs && one_sided
370
371     --------------
372     lookup env = case lookupUFM env fam of
373                    Nothing -> []        -- No instances for this class
374                    Just (FamIE insts has_tv_insts)
375                        -- Short cut for common case:
376                        --   The thing we are looking up is of form (C a
377                        --   b c), and the FamIE has no instances of
378                        --   that form, so don't bother to search 
379                      | all_tvs && not has_tv_insts -> []
380                      | otherwise                   -> find insts
381
382     --------------
383     find [] = []
384     find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs, 
385                           fi_tys = tpl_tys, fi_tycon = tycon }) : rest)
386         -- Fast check for no match, uses the "rough match" fields
387       | instanceCantMatch rough_tcs mb_tcs
388       = find rest
389
390         -- Proper check
391       | Just subst <- match_fun item tpl_tvs tpl_tys match_tys
392       = (item, add_extra_tys $ substTyVars subst (tyConTyVars tycon)) : find rest
393
394         -- No match => try next
395       | otherwise
396       = find rest
397 \end{code}
398
399 Note [Over-saturated matches]
400 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
401 It's ok to look up an over-saturated type constructor.  E.g.
402      type family F a :: * -> *
403      type instance F (a,b) = Either (a->b)
404
405 The type instance gives rise to a newtype TyCon (at a higher kind
406 which you can't do in Haskell!):
407      newtype FPair a b = FP (Either (a->b))
408
409 Then looking up (F (Int,Bool) Char) will return a FamInstMatch 
410      (FPair, [Int,Bool,Char])
411
412 The "extra" type argument [Char] just stays on the end.
413
414
415
416
417 %************************************************************************
418 %*                                                                      *
419                 Looking up a family instance
420 %*                                                                      *
421 %************************************************************************
422
423 \begin{code}
424 topNormaliseType :: FamInstEnvs
425                  -> Type
426                  -> Maybe (Coercion, Type)
427
428 -- Get rid of *outermost* (or toplevel) 
429 --      * type functions 
430 --      * newtypes
431 -- using appropriate coercions.
432 -- By "outer" we mean that toplevelNormaliseType guarantees to return
433 -- a type that does not have a reducible redex (F ty1 .. tyn) as its
434 -- outermost form.  It *can* return something like (Maybe (F ty)), where
435 -- (F ty) is a redex.
436
437 -- Its a bit like Type.repType, but handles type families too
438
439 topNormaliseType env ty
440   = go [] ty
441   where
442     go :: [TyCon] -> Type -> Maybe (Coercion, Type)
443     go rec_nts ty | Just ty' <- coreView ty     -- Expand synonyms
444         = go rec_nts ty'        
445
446     go rec_nts (TyConApp tc tys)
447         | isNewTyCon tc         -- Expand newtypes
448         = if tc `elem` rec_nts  -- See Note [Expanding newtypes] in Type.lhs
449           then Nothing
450           else let nt_co = mkAxInstCo (newTyConCo tc) tys
451                in add_co nt_co rec_nts' nt_rhs
452
453         | isFamilyTyCon tc              -- Expand open tycons
454         , (co, ty) <- normaliseTcApp env tc tys
455                 -- Note that normaliseType fully normalises, 
456                 -- but it has do to so to be sure that 
457         , not (isReflCo co)
458         = add_co co rec_nts ty
459         where
460           nt_rhs = newTyConInstRhs tc tys
461           rec_nts' | isRecursiveTyCon tc = tc:rec_nts
462                    | otherwise           = rec_nts
463
464     go _ _ = Nothing
465
466     add_co co rec_nts ty 
467         = case go rec_nts ty of
468                 Nothing         -> Just (co, ty)
469                 Just (co', ty') -> Just (mkTransCo co co', ty')
470          
471
472 ---------------
473 normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (Coercion, Type)
474 normaliseTcApp env tc tys
475   | isFamilyTyCon tc
476   , tyConArity tc <= length tys    -- Unsaturated data families are possible
477   , [(fam_inst, inst_tys)] <- lookupFamInstEnv env tc ntys 
478   = let    -- A matching family instance exists
479         rep_tc          = famInstTyCon fam_inst
480         co_tycon        = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
481         co              = mkAxInstCo co_tycon inst_tys
482         first_coi       = mkTransCo tycon_coi co
483         (rest_coi,nty)  = normaliseType env (mkTyConApp rep_tc inst_tys)
484         fix_coi         = mkTransCo first_coi rest_coi
485     in 
486     (fix_coi, nty)
487
488   | otherwise   -- No unique matching family instance exists;
489                 -- we do not do anything
490   = (tycon_coi, TyConApp tc ntys)
491
492   where
493         -- Normalise the arg types so that they'll match 
494         -- when we lookup in in the instance envt
495     (cois, ntys) = mapAndUnzip (normaliseType env) tys
496     tycon_coi    = mkTyConAppCo tc cois
497
498 ---------------
499 normaliseType :: FamInstEnvs            -- environment with family instances
500               -> Type                   -- old type
501               -> (Coercion, Type)       -- (coercion,new type), where
502                                         -- co :: old-type ~ new_type
503 -- Normalise the input type, by eliminating *all* type-function redexes
504 -- Returns with Refl if nothing happens
505
506 normaliseType env ty 
507   | Just ty' <- coreView ty = normaliseType env ty' 
508 normaliseType env (TyConApp tc tys)
509   = normaliseTcApp env tc tys
510 normaliseType env (AppTy ty1 ty2)
511   = let (coi1,nty1) = normaliseType env ty1
512         (coi2,nty2) = normaliseType env ty2
513     in  (mkAppCo coi1 coi2, mkAppTy nty1 nty2)
514 normaliseType env (FunTy ty1 ty2)
515   = let (coi1,nty1) = normaliseType env ty1
516         (coi2,nty2) = normaliseType env ty2
517     in  (mkFunCo coi1 coi2, mkFunTy nty1 nty2)
518 normaliseType env (ForAllTy tyvar ty1)
519   = let (coi,nty1) = normaliseType env ty1
520     in  (mkForAllCo tyvar coi, ForAllTy tyvar nty1)
521 normaliseType _   ty@(TyVarTy _)
522   = (Refl ty,ty)
523 normaliseType env (PredTy predty)
524   = normalisePred env predty
525
526 ---------------
527 normalisePred :: FamInstEnvs -> PredType -> (Coercion,Type)
528 normalisePred env (ClassP cls tys)
529   = let (cos,tys') = mapAndUnzip (normaliseType env) tys
530     in  (mkPredCo $ ClassP cls cos, PredTy $ ClassP cls tys')
531 normalisePred env (IParam ipn ty)
532   = let (co,ty') = normaliseType env ty
533     in  (mkPredCo $ (IParam ipn co), PredTy $ IParam ipn ty')
534 normalisePred env (EqPred ty1 ty2)
535   = let (co1,ty1') = normaliseType env ty1
536         (co2,ty2') = normaliseType env ty2
537     in  (mkPredCo $ (EqPred co1 co2), PredTy $ EqPred ty1' ty2')
538 \end{code}