2 % (c) The University of Glasgow 2006
5 FamInstEnv: Type checked family instance declarations
9 FamInst(..), famInstTyCon, famInstTyVars,
10 pprFamInst, pprFamInstHdr, pprFamInsts,
11 famInstHead, mkLocalFamInst, mkImportedFamInst,
13 FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs,
14 extendFamInstEnv, extendFamInstEnvList,
15 famInstEnvElts, familyInstances,
17 lookupFamInstEnv, lookupFamInstEnvConflicts,
23 #include "HsVersions.h"
42 %************************************************************************
44 \subsection{Type checked family instance heads}
46 %************************************************************************
50 = FamInst { fi_fam :: Name -- Family name
51 -- INVARIANT: fi_fam = case tyConFamInst_maybe fi_tycon of
52 -- Just (tc, tys) -> tc
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
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
65 , fi_tycon :: TyCon -- Representation tycon
68 -- Obtain the representation tycon of a family instance.
70 famInstTyCon :: FamInst -> TyCon
71 famInstTyCon = fi_tycon
73 famInstTyVars :: FamInst -> TyVarSet
74 famInstTyVars = fi_tvs
78 instance NamedThing FamInst where
79 getName = getName . fi_tycon
81 instance Outputable FamInst where
84 -- Prints the FamInst as a family instance declaration
85 pprFamInst :: FamInst -> SDoc
87 = hang (pprFamInstHdr famInst)
88 2 (ptext (sLit "--") <+> pprNameLoc (getName famInst))
90 pprFamInstHdr :: FamInst -> SDoc
91 pprFamInstHdr (FamInst {fi_tycon = rep_tc})
92 = pprTyConSort <+> pp_instance <+> pprHead
94 Just (fam_tc, tys) = tyConFamInst_maybe rep_tc
96 -- For *associated* types, say "type T Int = blah"
97 -- For *top level* type instances, say "type instance T Int = blah"
99 | isTyConAssoc fam_tc = empty
100 | otherwise = ptext (sLit "instance")
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"
109 pprFamInsts :: [FamInst] -> SDoc
110 pprFamInsts finsts = vcat (map pprFamInst finsts)
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)
118 -- Make a family instance representation from a tycon. This is used for local
119 -- instances, where we can safely pull on the tycon.
121 mkLocalFamInst :: TyCon -> FamInst
123 = case tyConFamInst_maybe tycon of
124 Nothing -> panic "FamInstEnv.mkLocalFamInst"
127 fi_fam = tyConName fam,
128 fi_tcs = roughMatchTcs tys,
129 fi_tvs = mkVarSet . tyConTyVars $ tycon,
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).
138 mkImportedFamInst :: Name -> [Maybe Name] -> TyCon -> FamInst
139 mkImportedFamInst fam mb_tcs tycon
143 fi_tvs = mkVarSet . tyConTyVars $ tycon,
144 fi_tys = case tyConFamInst_maybe tycon of
145 Nothing -> panic "FamInstEnv.mkImportedFamInst"
146 Just (_, tys) -> tys,
152 %************************************************************************
156 %************************************************************************
159 ~~~~~~~~~~~~~~~~~~~~~
160 A FamInstEnv maps a family name to the list of known instances for that family.
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.
167 Neverthless it is still useful to have data families in the FamInstEnv:
169 - For finding overlaps and conflicts
171 - For finding the representation type...see FamInstEnv.topNormaliseType
172 and its call site in Simplify
174 - In standalone deriving instance Eq (T [Int]) we need to find the
175 representation type for T [Int]
178 type FamInstEnv = UniqFM FamilyInstEnv -- Maps a family to its instances
179 -- See Note [FamInstEnv]
181 type FamInstEnvs = (FamInstEnv, FamInstEnv)
182 -- External package inst-env, Home-package inst-env
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
191 -- * The fs_tvs are distinct in each FamInst
192 -- of a range value of the map (so we can safely unify them)
194 emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
195 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
197 emptyFamInstEnv :: FamInstEnv
198 emptyFamInstEnv = emptyUFM
200 famInstEnvElts :: FamInstEnv -> [FamInst]
201 famInstEnvElts fi = [elt | FamIE elts _ <- eltsUFM fi, elt <- elts]
203 familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
204 familyInstances (pkg_fie, home_fie) fam
205 = get home_fie ++ get pkg_fie
207 get env = case lookupUFM env fam of
208 Just (FamIE insts _) -> insts
211 extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
212 extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis
214 extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
215 extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs})
216 = addToUFM_C add inst_env cls_nm (FamIE [ins_item] ins_tyvar)
218 add (FamIE items tyvar) _ = FamIE (ins_item:items)
220 ins_tyvar = not (any isJust mb_tcs)
223 %************************************************************************
225 Looking up a family instance
227 %************************************************************************
229 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
230 Multiple matches are only possible in case of type families (not data
231 families), and then, it doesn't matter which match we choose (as the
232 instances are guaranteed confluent).
234 We return the matching family instances and the type instance at which it
235 matches. For example, if we lookup 'T [Int]' and have a family instance
237 data instance T [a] = ..
242 coe :Co:R42T a :: T [a] ~ :R42T a
244 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
247 type FamInstMatch = (FamInst, [Type]) -- Matching type instance
248 -- See Note [Over-saturated matches]
252 -> TyCon -> [Type] -- What we are looking for
253 -> [FamInstMatch] -- Successful matches
254 -- Precondition: the tycon is saturated (or over-saturated)
257 = lookup_fam_inst_env match True
259 match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
261 lookupFamInstEnvConflicts
263 -> FamInst -- Putative new instance
264 -> [TyVar] -- Unique tyvars, matching arity of FamInst
265 -> [FamInstMatch] -- Conflicting matches
266 -- E.g. when we are about to add
267 -- f : type instance F [a] = a->a
268 -- we do (lookupFamInstConflicts f [b])
269 -- to find conflicting matches
270 -- The skolem tyvars are needed because we don't have a
271 -- unique supply to hand
273 -- Precondition: the tycon is saturated (or over-saturated)
275 lookupFamInstEnvConflicts envs fam_inst skol_tvs
276 = lookup_fam_inst_env my_unify False envs fam tys'
278 inst_tycon = famInstTyCon fam_inst
279 (fam, tys) = expectJust "FamInstEnv.lookuFamInstEnvConflicts"
280 (tyConFamInst_maybe inst_tycon)
281 skol_tys = mkTyVarTys skol_tvs
282 tys' = substTys (zipTopTvSubst (tyConTyVars inst_tycon) skol_tys) tys
283 -- In example above, fam tys' = F [b]
285 my_unify old_fam_inst tpl_tvs tpl_tys match_tys
286 = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
287 (ppr fam <+> ppr tys) $$
288 (ppr tpl_tvs <+> ppr tpl_tys) )
289 -- Unification will break badly if the variables overlap
290 -- They shouldn't because we allocate separate uniques for them
291 case tcUnifyTys instanceBindFun tpl_tys match_tys of
292 Just subst | conflicting old_fam_inst subst -> Just subst
295 -- - In the case of data family instances, any overlap is fundamentally a
296 -- conflict (as these instances imply injective type mappings).
297 -- - In the case of type family instances, overlap is admitted as long as
298 -- the right-hand sides of the overlapping rules coincide under the
299 -- overlap substitution. We require that they are syntactically equal;
300 -- anything else would be difficult to test for at this stage.
301 conflicting old_fam_inst subst
302 | isAlgTyCon fam = True
303 | otherwise = not (old_rhs `tcEqType` new_rhs)
305 old_tycon = famInstTyCon old_fam_inst
306 old_tvs = tyConTyVars old_tycon
307 old_rhs = mkTyConApp old_tycon (substTyVars subst old_tvs)
308 new_rhs = mkTyConApp inst_tycon (substTyVars subst skol_tvs)
311 While @lookupFamInstEnv@ uses a one-way match, the next function
312 @lookupFamInstEnvConflicts@ uses two-way matching (ie, unification). This is
313 needed to check for overlapping instances.
315 For class instances, these two variants of lookup are combined into one
316 function (cf, @InstEnv@). We don't do that for family instances as the
317 results of matching and unification are used in two different contexts.
318 Moreover, matching is the wildly more frequently used operation in the case of
319 indexed synonyms and we don't want to slow that down by needless unification.
322 ------------------------------------------------------------
323 -- Might be a one-way match or a unifier
324 type MatchFun = FamInst -- The FamInst template
325 -> TyVarSet -> [Type] -- fi_tvs, fi_tys of that FamInst
326 -> [Type] -- Target to match against
329 type OneSidedMatch = Bool -- Are optimisations that are only valid for
330 -- one sided matches allowed?
332 lookup_fam_inst_env -- The worker, local to this module
336 -> TyCon -> [Type] -- What we are looking for
337 -> [FamInstMatch] -- Successful matches
339 -- Precondition: the tycon is saturated (or over-saturated)
341 lookup_fam_inst_env match_fun one_sided (pkg_ie, home_ie) fam tys
342 | not (isFamilyTyCon fam)
345 = ASSERT2( n_tys >= arity, ppr fam <+> ppr tys ) -- Family type applications must be saturated
346 home_matches ++ pkg_matches
348 home_matches = lookup home_ie
349 pkg_matches = lookup pkg_ie
351 -- See Note [Over-saturated matches]
352 arity = tyConArity fam
354 extra_tys = drop arity tys
355 (match_tys, add_extra_tys)
356 | arity > n_tys = (take arity tys, \res_tys -> res_tys ++ extra_tys)
357 | otherwise = (tys, \res_tys -> res_tys)
358 -- The second case is the common one, hence functional representation
361 rough_tcs = roughMatchTcs match_tys
362 all_tvs = all isNothing rough_tcs && one_sided
365 lookup env = case lookupUFM env fam of
366 Nothing -> [] -- No instances for this class
367 Just (FamIE insts has_tv_insts)
368 -- Short cut for common case:
369 -- The thing we are looking up is of form (C a
370 -- b c), and the FamIE has no instances of
371 -- that form, so don't bother to search
372 | all_tvs && not has_tv_insts -> []
373 | otherwise -> find insts
377 find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs,
378 fi_tys = tpl_tys, fi_tycon = tycon }) : rest)
379 -- Fast check for no match, uses the "rough match" fields
380 | instanceCantMatch rough_tcs mb_tcs
384 | Just subst <- match_fun item tpl_tvs tpl_tys match_tys
385 = (item, add_extra_tys $ substTyVars subst (tyConTyVars tycon)) : find rest
387 -- No match => try next
392 Note [Over-saturated matches]
393 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
394 It's ok to look up an over-saturated type constructor. E.g.
395 type family F a :: * -> *
396 type instance F (a,b) = Either (a->b)
398 The type instance gives rise to a newtype TyCon (at a higher kind
399 which you can't do in Haskell!):
400 newtype FPair a b = FP (Either (a->b))
402 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
403 (FPair, [Int,Bool,Char])
405 The "extra" type argument [Char] just stays on the end.
410 %************************************************************************
412 Looking up a family instance
414 %************************************************************************
417 topNormaliseType :: FamInstEnvs
419 -> Maybe (Coercion, Type)
421 -- Get rid of *outermost* (or toplevel)
424 -- using appropriate coercions.
425 -- By "outer" we mean that toplevelNormaliseType guarantees to return
426 -- a type that does not have a reducible redex (F ty1 .. tyn) as its
427 -- outermost form. It *can* return something like (Maybe (F ty)), where
428 -- (F ty) is a redex.
430 -- Its a bit like Type.repType, but handles type families too
432 topNormaliseType env ty
435 go :: [TyCon] -> Type -> Maybe (Coercion, Type)
436 go rec_nts ty | Just ty' <- coreView ty -- Expand synonyms
439 go rec_nts (TyConApp tc tys) -- Expand newtypes
440 | Just co_con <- newTyConCo_maybe tc -- See Note [Expanding newtypes]
441 = if tc `elem` rec_nts -- in Type.lhs
443 else let nt_co = mkTyConApp co_con tys
444 in add_co nt_co rec_nts' nt_rhs
446 nt_rhs = newTyConInstRhs tc tys
447 rec_nts' | isRecursiveTyCon tc = tc:rec_nts
448 | otherwise = rec_nts
450 go rec_nts (TyConApp tc tys) -- Expand open tycons
452 , (ACo co, ty) <- normaliseTcApp env tc tys
453 = -- The ACo says "something happened"
454 -- Note that normaliseType fully normalises, but it has do to so
461 = case go rec_nts ty of
462 Nothing -> Just (co, ty)
463 Just (co', ty') -> Just (mkTransCoercion co co', ty')
467 normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (CoercionI, Type)
468 normaliseTcApp env tc tys
470 , tyConArity tc <= length tys -- Unsaturated data families are possible
471 , [(fam_inst, inst_tys)] <- lookupFamInstEnv env tc ntys
472 = let -- A matching family instance exists
473 rep_tc = famInstTyCon fam_inst
474 co_tycon = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
475 co = mkTyConApp co_tycon inst_tys
476 first_coi = mkTransCoI tycon_coi (ACo co)
477 (rest_coi, nty) = normaliseType env (mkTyConApp rep_tc inst_tys)
478 fix_coi = mkTransCoI first_coi rest_coi
483 = (tycon_coi, TyConApp tc ntys)
486 -- Normalise the arg types so that they'll match
487 -- when we lookup in in the instance envt
488 (cois, ntys) = mapAndUnzip (normaliseType env) tys
489 tycon_coi = mkTyConAppCoI tc cois
492 normaliseType :: FamInstEnvs -- environment with family instances
494 -> (CoercionI, Type) -- (coercion,new type), where
495 -- co :: old-type ~ new_type
496 -- Normalise the input type, by eliminating *all* type-function redexes
497 -- Returns with IdCo if nothing happens
500 | Just ty' <- coreView ty = normaliseType env ty'
501 normaliseType env (TyConApp tc tys)
502 = normaliseTcApp env tc tys
503 normaliseType env (AppTy ty1 ty2)
504 = let (coi1,nty1) = normaliseType env ty1
505 (coi2,nty2) = normaliseType env ty2
506 in (mkAppTyCoI coi1 coi2, mkAppTy nty1 nty2)
507 normaliseType env (FunTy ty1 ty2)
508 = let (coi1,nty1) = normaliseType env ty1
509 (coi2,nty2) = normaliseType env ty2
510 in (mkFunTyCoI coi1 coi2, mkFunTy nty1 nty2)
511 normaliseType env (ForAllTy tyvar ty1)
512 = let (coi,nty1) = normaliseType env ty1
513 in (mkForAllTyCoI tyvar coi, ForAllTy tyvar nty1)
514 normaliseType _ ty@(TyVarTy _)
516 normaliseType env (PredTy predty)
517 = normalisePred env predty
520 normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type)
521 normalisePred env (ClassP cls tys)
522 = let (cois,tys') = mapAndUnzip (normaliseType env) tys
523 in (mkClassPPredCoI cls cois, PredTy $ ClassP cls tys')
524 normalisePred env (IParam ipn ty)
525 = let (coi,ty') = normaliseType env ty
526 in (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
527 normalisePred env (EqPred ty1 ty2)
528 = let (coi1,ty1') = normaliseType env ty1
529 (coi2,ty2') = normaliseType env ty2
530 in (mkEqPredCoI coi1 coi2, PredTy $ EqPred ty1' ty2')