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