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