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
190 instance Outputable FamilyInstEnv where
191 ppr (FamIE fs b) = ptext (sLit "FamIE") <+> ppr b <+> vcat (map ppr fs)
194 -- * The fs_tvs are distinct in each FamInst
195 -- of a range value of the map (so we can safely unify them)
197 emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
198 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
200 emptyFamInstEnv :: FamInstEnv
201 emptyFamInstEnv = emptyUFM
203 famInstEnvElts :: FamInstEnv -> [FamInst]
204 famInstEnvElts fi = [elt | FamIE elts _ <- eltsUFM fi, elt <- elts]
206 familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
207 familyInstances (pkg_fie, home_fie) fam
208 = get home_fie ++ get pkg_fie
210 get env = case lookupUFM env fam of
211 Just (FamIE insts _) -> insts
214 extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
215 extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis
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)
221 add (FamIE items tyvar) _ = FamIE (ins_item:items)
223 ins_tyvar = not (any isJust mb_tcs)
226 %************************************************************************
228 Looking up a family instance
230 %************************************************************************
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).
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
240 data instance T [a] = ..
245 coe :Co:R42T a :: T [a] ~ :R42T a
247 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
250 type FamInstMatch = (FamInst, [Type]) -- Matching type instance
251 -- See Note [Over-saturated matches]
255 -> TyCon -> [Type] -- What we are looking for
256 -> [FamInstMatch] -- Successful matches
257 -- Precondition: the tycon is saturated (or over-saturated)
260 = lookup_fam_inst_env match True
262 match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
264 lookupFamInstEnvConflicts
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
276 -- Precondition: the tycon is saturated (or over-saturated)
278 lookupFamInstEnvConflicts envs fam_inst skol_tvs
279 = lookup_fam_inst_env my_unify False envs fam tys'
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]
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
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)
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)
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.
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.
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
332 type OneSidedMatch = Bool -- Are optimisations that are only valid for
333 -- one sided matches allowed?
335 lookup_fam_inst_env -- The worker, local to this module
339 -> TyCon -> [Type] -- What we are looking for
340 -> [FamInstMatch] -- Successful matches
342 -- Precondition: the tycon is saturated (or over-saturated)
344 lookup_fam_inst_env match_fun one_sided (pkg_ie, home_ie) fam tys
345 | not (isFamilyTyCon fam)
348 = ASSERT2( n_tys >= arity, ppr fam <+> ppr tys ) -- Family type applications must be saturated
349 home_matches ++ pkg_matches
351 home_matches = lookup home_ie
352 pkg_matches = lookup pkg_ie
354 -- See Note [Over-saturated matches]
355 arity = tyConArity fam
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
364 rough_tcs = roughMatchTcs match_tys
365 all_tvs = all isNothing rough_tcs && one_sided
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
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
387 | Just subst <- match_fun item tpl_tvs tpl_tys match_tys
388 = (item, add_extra_tys $ substTyVars subst (tyConTyVars tycon)) : find rest
390 -- No match => try next
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)
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))
405 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
406 (FPair, [Int,Bool,Char])
408 The "extra" type argument [Char] just stays on the end.
413 %************************************************************************
415 Looking up a family instance
417 %************************************************************************
420 topNormaliseType :: FamInstEnvs
422 -> Maybe (Coercion, Type)
424 -- Get rid of *outermost* (or toplevel)
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.
433 -- Its a bit like Type.repType, but handles type families too
435 topNormaliseType env ty
438 go :: [TyCon] -> Type -> Maybe (Coercion, Type)
439 go rec_nts ty | Just ty' <- coreView ty -- Expand synonyms
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
446 else let nt_co = mkTyConApp co_con tys
447 in add_co nt_co rec_nts' nt_rhs
449 nt_rhs = newTyConInstRhs tc tys
450 rec_nts' | isRecursiveTyCon tc = tc:rec_nts
451 | otherwise = rec_nts
453 go rec_nts (TyConApp tc tys) -- Expand open tycons
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
464 = case go rec_nts ty of
465 Nothing -> Just (co, ty)
466 Just (co', ty') -> Just (mkTransCoercion co co', ty')
470 normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (CoercionI, Type)
471 normaliseTcApp env tc tys
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
486 = (tycon_coi, TyConApp tc ntys)
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
495 normaliseType :: FamInstEnvs -- environment with family instances
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
503 | Just ty' <- coreView ty = normaliseType env ty'
504 normaliseType env (TyConApp tc tys)
505 = normaliseTcApp env tc tys
506 normaliseType env (AppTy ty1 ty2)
507 = let (coi1,nty1) = normaliseType env ty1
508 (coi2,nty2) = normaliseType env ty2
509 in (mkAppTyCoI coi1 coi2, mkAppTy nty1 nty2)
510 normaliseType env (FunTy ty1 ty2)
511 = let (coi1,nty1) = normaliseType env ty1
512 (coi2,nty2) = normaliseType env ty2
513 in (mkFunTyCoI coi1 coi2, mkFunTy nty1 nty2)
514 normaliseType env (ForAllTy tyvar ty1)
515 = let (coi,nty1) = normaliseType env ty1
516 in (mkForAllTyCoI tyvar coi, ForAllTy tyvar nty1)
517 normaliseType _ ty@(TyVarTy _)
519 normaliseType env (PredTy predty)
520 = normalisePred env predty
523 normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type)
524 normalisePred env (ClassP cls tys)
525 = let (cois,tys') = mapAndUnzip (normaliseType env) tys
526 in (mkClassPPredCoI cls cois, PredTy $ ClassP cls tys')
527 normalisePred env (IParam ipn ty)
528 = let (coi,ty') = normaliseType env ty
529 in (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
530 normalisePred env (EqPred ty1 ty2)
531 = let (coi1,ty1') = normaliseType env ty1
532 (coi2,ty2') = normaliseType env ty2
533 in (mkEqPredCoI coi1 coi2, PredTy $ EqPred ty1' ty2')