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_fam = fam, fi_tys = tys, fi_tycon = tycon})
92 = pprTyConSort <+> pprHead
94 pprHead = pprTypeApp fam tys
95 pprTyConSort | isDataTyCon tycon = ptext (sLit "data instance")
96 | isNewTyCon tycon = ptext (sLit "newtype instance")
97 | isSynTyCon tycon = ptext (sLit "type instance")
98 | isAbstractTyCon tycon = ptext (sLit "data instance")
99 | otherwise = panic "FamInstEnv.pprFamInstHdr"
101 pprFamInsts :: [FamInst] -> SDoc
102 pprFamInsts finsts = vcat (map pprFamInst finsts)
104 famInstHead :: FamInst -> ([TyVar], TyCon, [Type])
105 famInstHead (FamInst {fi_tycon = tycon})
106 = case tyConFamInst_maybe tycon of
107 Nothing -> panic "FamInstEnv.famInstHead"
108 Just (fam, tys) -> (tyConTyVars tycon, fam, tys)
110 -- Make a family instance representation from a tycon. This is used for local
111 -- instances, where we can safely pull on the tycon.
113 mkLocalFamInst :: TyCon -> FamInst
115 = case tyConFamInst_maybe tycon of
116 Nothing -> panic "FamInstEnv.mkLocalFamInst"
119 fi_fam = tyConName fam,
120 fi_tcs = roughMatchTcs tys,
121 fi_tvs = mkVarSet . tyConTyVars $ tycon,
126 -- Make a family instance representation from the information found in an
127 -- unterface file. In particular, we get the rough match info from the iface
128 -- (instead of computing it here).
130 mkImportedFamInst :: Name -> [Maybe Name] -> TyCon -> FamInst
131 mkImportedFamInst fam mb_tcs tycon
135 fi_tvs = mkVarSet . tyConTyVars $ tycon,
136 fi_tys = case tyConFamInst_maybe tycon of
137 Nothing -> panic "FamInstEnv.mkImportedFamInst"
138 Just (_, tys) -> tys,
144 %************************************************************************
148 %************************************************************************
150 InstEnv maps a family name to the list of known instances for that family.
153 type FamInstEnv = UniqFM FamilyInstEnv -- Maps a family to its instances
155 type FamInstEnvs = (FamInstEnv, FamInstEnv)
156 -- External package inst-env, Home-package inst-env
159 = FamIE [FamInst] -- The instances for a particular family, in any order
160 Bool -- True <=> there is an instance of form T a b c
161 -- If *not* then the common case of looking up
162 -- (T a b c) can fail immediately
165 -- * The fs_tvs are distinct in each FamInst
166 -- of a range value of the map (so we can safely unify them)
168 emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
169 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
171 emptyFamInstEnv :: FamInstEnv
172 emptyFamInstEnv = emptyUFM
174 famInstEnvElts :: FamInstEnv -> [FamInst]
175 famInstEnvElts fi = [elt | FamIE elts _ <- eltsUFM fi, elt <- elts]
177 familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
178 familyInstances (pkg_fie, home_fie) fam
179 = get home_fie ++ get pkg_fie
181 get env = case lookupUFM env fam of
182 Just (FamIE insts _) -> insts
185 extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
186 extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis
188 extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
189 extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs})
190 = addToUFM_C add inst_env cls_nm (FamIE [ins_item] ins_tyvar)
192 add (FamIE items tyvar) _ = FamIE (ins_item:items)
194 ins_tyvar = not (any isJust mb_tcs)
197 %************************************************************************
199 Looking up a family instance
201 %************************************************************************
203 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
204 Multiple matches are only possible in case of type families (not data
205 families), and then, it doesn't matter which match we choose (as the
206 instances are guaranteed confluent).
208 We return the matching family instances and the type instance at which it
209 matches. For example, if we lookup 'T [Int]' and have a family instance
211 data instance T [a] = ..
216 coe :Co:R42T a :: T [a] ~ :R42T a
218 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
221 type FamInstMatch = (FamInst, [Type]) -- Matching type instance
222 -- See Note [Over-saturated matches]
226 -> TyCon -> [Type] -- What we are looking for
227 -> [FamInstMatch] -- Successful matches
230 = lookup_fam_inst_env match True
232 match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
234 lookupFamInstEnvConflicts
236 -> FamInst -- Putative new instance
237 -> [TyVar] -- Unique tyvars, matching arity of FamInst
238 -> [FamInstMatch] -- Conflicting matches
239 -- E.g. when we are about to add
240 -- f : type instance F [a] = a->a
241 -- we do (lookupFamInstConflicts f [b])
242 -- to find conflicting matches
243 -- The skolem tyvars are needed because we don't have a
244 -- unique supply to hand
246 lookupFamInstEnvConflicts envs fam_inst skol_tvs
247 = lookup_fam_inst_env my_unify False envs fam tys'
249 inst_tycon = famInstTyCon fam_inst
250 (fam, tys) = expectJust "FamInstEnv.lookuFamInstEnvConflicts"
251 (tyConFamInst_maybe inst_tycon)
252 skol_tys = mkTyVarTys skol_tvs
253 tys' = substTys (zipTopTvSubst (tyConTyVars inst_tycon) skol_tys) tys
254 -- In example above, fam tys' = F [b]
256 my_unify old_fam_inst tpl_tvs tpl_tys match_tys
257 = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
258 (ppr fam <+> ppr tys) $$
259 (ppr tpl_tvs <+> ppr tpl_tys) )
260 -- Unification will break badly if the variables overlap
261 -- They shouldn't because we allocate separate uniques for them
262 case tcUnifyTys instanceBindFun tpl_tys match_tys of
263 Just subst | conflicting old_fam_inst subst -> Just subst
266 -- - In the case of data family instances, any overlap is fundamentally a
267 -- conflict (as these instances imply injective type mappings).
268 -- - In the case of type family instances, overlap is admitted as long as
269 -- the right-hand sides of the overlapping rules coincide under the
270 -- overlap substitution. We require that they are syntactically equal;
271 -- anything else would be difficult to test for at this stage.
272 conflicting old_fam_inst subst
273 | isAlgTyCon fam = True
274 | otherwise = not (old_rhs `tcEqType` new_rhs)
276 old_tycon = famInstTyCon old_fam_inst
277 old_tvs = tyConTyVars old_tycon
278 old_rhs = mkTyConApp old_tycon (substTyVars subst old_tvs)
279 new_rhs = mkTyConApp inst_tycon (substTyVars subst skol_tvs)
282 While @lookupFamInstEnv@ uses a one-way match, the next function
283 @lookupFamInstEnvConflicts@ uses two-way matching (ie, unification). This is
284 needed to check for overlapping instances.
286 For class instances, these two variants of lookup are combined into one
287 function (cf, @InstEnv@). We don't do that for family instances as the
288 results of matching and unification are used in two different contexts.
289 Moreover, matching is the wildly more frequently used operation in the case of
290 indexed synonyms and we don't want to slow that down by needless unification.
293 ------------------------------------------------------------
294 -- Might be a one-way match or a unifier
295 type MatchFun = FamInst -- The FamInst template
296 -> TyVarSet -> [Type] -- fi_tvs, fi_tys of that FamInst
297 -> [Type] -- Target to match against
300 type OneSidedMatch = Bool -- Are optimisations that are only valid for
301 -- one sided matches allowed?
303 lookup_fam_inst_env -- The worker, local to this module
307 -> TyCon -> [Type] -- What we are looking for
308 -> [FamInstMatch] -- Successful matches
309 lookup_fam_inst_env match_fun one_sided (pkg_ie, home_ie) fam tys
310 | not (isOpenTyCon fam)
313 = ASSERT( n_tys >= arity ) -- Family type applications must be saturated
314 home_matches ++ pkg_matches
316 home_matches = lookup home_ie
317 pkg_matches = lookup pkg_ie
319 -- See Note [Over-saturated matches]
320 arity = tyConArity fam
322 extra_tys = drop arity tys
323 (match_tys, add_extra_tys)
324 | arity > n_tys = (take arity tys, \res_tys -> res_tys ++ extra_tys)
325 | otherwise = (tys, \res_tys -> res_tys)
326 -- The second case is the common one, hence functional representation
329 rough_tcs = roughMatchTcs match_tys
330 all_tvs = all isNothing rough_tcs && one_sided
333 lookup env = case lookupUFM env fam of
334 Nothing -> [] -- No instances for this class
335 Just (FamIE insts has_tv_insts)
336 -- Short cut for common case:
337 -- The thing we are looking up is of form (C a
338 -- b c), and the FamIE has no instances of
339 -- that form, so don't bother to search
340 | all_tvs && not has_tv_insts -> []
341 | otherwise -> find insts
345 find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs,
346 fi_tys = tpl_tys, fi_tycon = tycon }) : rest)
347 -- Fast check for no match, uses the "rough match" fields
348 | instanceCantMatch rough_tcs mb_tcs
352 | Just subst <- match_fun item tpl_tvs tpl_tys match_tys
353 = (item, add_extra_tys $ substTyVars subst (tyConTyVars tycon)) : find rest
355 -- No match => try next
360 Note [Over-saturated matches]
361 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
362 It's ok to look up an over-saturated type constructor. E.g.
363 type family F a :: * -> *
364 type instance F (a,b) = Either (a->b)
366 The type instance gives rise to a newtype TyCon (at a higher kind
367 which you can't do in Haskell!):
368 newtype FPair a b = FP (Either (a->b))
370 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
371 (FPair, [Int,Bool,Char])
373 The "extra" type argument [Char] just stays on the end.
378 %************************************************************************
380 Looking up a family instance
382 %************************************************************************
385 topNormaliseType :: FamInstEnvs
387 -> Maybe (Coercion, Type)
389 -- Get rid of *outermost* (or toplevel)
392 -- using appropriate coercions.
393 -- By "outer" we mean that toplevelNormaliseType guarantees to return
394 -- a type that does not have a reducible redex (F ty1 .. tyn) as its
395 -- outermost form. It *can* return something like (Maybe (F ty)), where
396 -- (F ty) is a redex.
398 -- Its a bit like Type.repType, but handles type families too
400 topNormaliseType env ty
403 go :: [TyCon] -> Type -> Maybe (Coercion, Type)
404 go rec_nts ty | Just ty' <- coreView ty -- Expand synonyms
407 go rec_nts (TyConApp tc tys) -- Expand newtypes
408 | Just co_con <- newTyConCo_maybe tc -- See Note [Expanding newtypes]
409 = if tc `elem` rec_nts -- in Type.lhs
411 else let nt_co = mkTyConApp co_con tys
412 in add_co nt_co rec_nts' nt_rhs
414 nt_rhs = newTyConInstRhs tc tys
415 rec_nts' | isRecursiveTyCon tc = tc:rec_nts
416 | otherwise = rec_nts
418 go rec_nts (TyConApp tc tys) -- Expand open tycons
420 , (ACo co, ty) <- normaliseTcApp env tc tys
421 = -- The ACo says "something happened"
422 -- Note that normaliseType fully normalises, but it has do to so
429 = case go rec_nts ty of
430 Nothing -> Just (co, ty)
431 Just (co', ty') -> Just (mkTransCoercion co co', ty')
435 normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (CoercionI, Type)
436 normaliseTcApp env tc tys
437 = let -- First normalise the arg types so that they'll match
438 -- when we lookup in in the instance envt
439 (cois, ntys) = mapAndUnzip (normaliseType env) tys
440 tycon_coi = mkTyConAppCoI tc ntys cois
441 in -- Now try the top-level redex
442 case lookupFamInstEnv env tc ntys of
443 -- A matching family instance exists
444 [(fam_inst, tys)] -> (fix_coi, nty)
446 rep_tc = famInstTyCon fam_inst
447 co_tycon = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
448 co = mkTyConApp co_tycon tys
449 first_coi = mkTransCoI tycon_coi (ACo co)
450 (rest_coi,nty) = normaliseType env (mkTyConApp rep_tc tys)
451 fix_coi = mkTransCoI first_coi rest_coi
453 -- No unique matching family instance exists;
454 -- we do not do anything
455 _ -> (tycon_coi, TyConApp tc ntys)
457 normaliseType :: FamInstEnvs -- environment with family instances
459 -> (CoercionI, Type) -- (coercion,new type), where
460 -- co :: old-type ~ new_type
461 -- Normalise the input type, by eliminating *all* type-function redexes
462 -- Returns with IdCo if nothing happens
465 | Just ty' <- coreView ty = normaliseType env ty'
466 normaliseType env (TyConApp tc tys)
467 = normaliseTcApp env tc tys
468 normaliseType env (AppTy ty1 ty2)
469 = let (coi1,nty1) = normaliseType env ty1
470 (coi2,nty2) = normaliseType env ty2
471 in (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
472 normaliseType env (FunTy ty1 ty2)
473 = let (coi1,nty1) = normaliseType env ty1
474 (coi2,nty2) = normaliseType env ty2
475 in (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
476 normaliseType env (ForAllTy tyvar ty1)
477 = let (coi,nty1) = normaliseType env ty1
478 in (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
479 normaliseType _ ty@(TyVarTy _)
481 normaliseType env (PredTy predty)
482 = normalisePred env predty
485 normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type)
486 normalisePred env (ClassP cls tys)
487 = let (cois,tys') = mapAndUnzip (normaliseType env) tys
488 in (mkClassPPredCoI cls tys' cois, PredTy $ ClassP cls tys')
489 normalisePred env (IParam ipn ty)
490 = let (coi,ty') = normaliseType env ty
491 in (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
492 normalisePred env (EqPred ty1 ty2)
493 = let (coi1,ty1') = normaliseType env ty1
494 (coi2,ty2') = normaliseType env ty2
495 in (mkEqPredCoI ty1' coi1 ty2' coi2, PredTy $ EqPred ty1' ty2')