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 | otherwise = panic "FamInstEnv.pprFamInstHdr"
100 pprFamInsts :: [FamInst] -> SDoc
101 pprFamInsts finsts = vcat (map pprFamInst finsts)
103 famInstHead :: FamInst -> ([TyVar], TyCon, [Type])
104 famInstHead (FamInst {fi_tycon = tycon})
105 = case tyConFamInst_maybe tycon of
106 Nothing -> panic "FamInstEnv.famInstHead"
107 Just (fam, tys) -> (tyConTyVars tycon, fam, tys)
109 -- Make a family instance representation from a tycon. This is used for local
110 -- instances, where we can safely pull on the tycon.
112 mkLocalFamInst :: TyCon -> FamInst
114 = case tyConFamInst_maybe tycon of
115 Nothing -> panic "FamInstEnv.mkLocalFamInst"
118 fi_fam = tyConName fam,
119 fi_tcs = roughMatchTcs tys,
120 fi_tvs = mkVarSet . tyConTyVars $ tycon,
125 -- Make a family instance representation from the information found in an
126 -- unterface file. In particular, we get the rough match info from the iface
127 -- (instead of computing it here).
129 mkImportedFamInst :: Name -> [Maybe Name] -> TyCon -> FamInst
130 mkImportedFamInst fam mb_tcs tycon
134 fi_tvs = mkVarSet . tyConTyVars $ tycon,
135 fi_tys = case tyConFamInst_maybe tycon of
136 Nothing -> panic "FamInstEnv.mkImportedFamInst"
137 Just (_, tys) -> tys,
143 %************************************************************************
147 %************************************************************************
149 InstEnv maps a family name to the list of known instances for that family.
152 type FamInstEnv = UniqFM FamilyInstEnv -- Maps a family to its instances
154 type FamInstEnvs = (FamInstEnv, FamInstEnv)
155 -- External package inst-env, Home-package inst-env
158 = FamIE [FamInst] -- The instances for a particular family, in any order
159 Bool -- True <=> there is an instance of form T a b c
160 -- If *not* then the common case of looking up
161 -- (T a b c) can fail immediately
164 -- * The fs_tvs are distinct in each FamInst
165 -- of a range value of the map (so we can safely unify them)
167 emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
168 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
170 emptyFamInstEnv :: FamInstEnv
171 emptyFamInstEnv = emptyUFM
173 famInstEnvElts :: FamInstEnv -> [FamInst]
174 famInstEnvElts fi = [elt | FamIE elts _ <- eltsUFM fi, elt <- elts]
176 familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
177 familyInstances (pkg_fie, home_fie) fam
178 = get home_fie ++ get pkg_fie
180 get env = case lookupUFM env fam of
181 Just (FamIE insts _) -> insts
184 extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
185 extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis
187 extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
188 extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs})
189 = addToUFM_C add inst_env cls_nm (FamIE [ins_item] ins_tyvar)
191 add (FamIE items tyvar) _ = FamIE (ins_item:items)
193 ins_tyvar = not (any isJust mb_tcs)
196 %************************************************************************
198 Looking up a family instance
200 %************************************************************************
202 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
203 Multiple matches are only possible in case of type families (not data
204 families), and then, it doesn't matter which match we choose (as the
205 instances are guaranteed confluent).
207 We return the matching family instances and the type instance at which it
208 matches. For example, if we lookup 'T [Int]' and have a family instance
210 data instance T [a] = ..
215 coe :Co:R42T a :: T [a] ~ :R42T a
217 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
220 type FamInstMatch = (FamInst, [Type]) -- Matching type instance
221 -- See Note [Over-saturated matches]
225 -> TyCon -> [Type] -- What we are looking for
226 -> [FamInstMatch] -- Successful matches
229 = lookup_fam_inst_env match True
231 match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
233 lookupFamInstEnvConflicts
235 -> FamInst -- Putative new instance
236 -> [TyVar] -- Unique tyvars, matching arity of FamInst
237 -> [FamInstMatch] -- Conflicting matches
238 -- E.g. when we are about to add
239 -- f : type instance F [a] = a->a
240 -- we do (lookupFamInstConflicts f [b])
241 -- to find conflicting matches
242 -- The skolem tyvars are needed because we don't have a
243 -- unique supply to hand
245 lookupFamInstEnvConflicts envs fam_inst skol_tvs
246 = lookup_fam_inst_env my_unify False envs fam tys'
248 inst_tycon = famInstTyCon fam_inst
249 (fam, tys) = expectJust "FamInstEnv.lookuFamInstEnvConflicts"
250 (tyConFamInst_maybe inst_tycon)
251 skol_tys = mkTyVarTys skol_tvs
252 tys' = substTys (zipTopTvSubst (tyConTyVars inst_tycon) skol_tys) tys
253 -- In example above, fam tys' = F [b]
255 my_unify old_fam_inst tpl_tvs tpl_tys match_tys
256 = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
257 (ppr fam <+> ppr tys) $$
258 (ppr tpl_tvs <+> ppr tpl_tys) )
259 -- Unification will break badly if the variables overlap
260 -- They shouldn't because we allocate separate uniques for them
261 case tcUnifyTys instanceBindFun tpl_tys match_tys of
262 Just subst | conflicting old_fam_inst subst -> Just subst
265 -- - In the case of data family instances, any overlap is fundamentally a
266 -- conflict (as these instances imply injective type mappings).
267 -- - In the case of type family instances, overlap is admitted as long as
268 -- the right-hand sides of the overlapping rules coincide under the
269 -- overlap substitution. We require that they are syntactically equal;
270 -- anything else would be difficult to test for at this stage.
271 conflicting old_fam_inst subst
272 | isAlgTyCon fam = True
273 | otherwise = not (old_rhs `tcEqType` new_rhs)
275 old_tycon = famInstTyCon old_fam_inst
276 old_tvs = tyConTyVars old_tycon
277 old_rhs = mkTyConApp old_tycon (substTyVars subst old_tvs)
278 new_rhs = mkTyConApp inst_tycon (substTyVars subst skol_tvs)
281 While @lookupFamInstEnv@ uses a one-way match, the next function
282 @lookupFamInstEnvConflicts@ uses two-way matching (ie, unification). This is
283 needed to check for overlapping instances.
285 For class instances, these two variants of lookup are combined into one
286 function (cf, @InstEnv@). We don't do that for family instances as the
287 results of matching and unification are used in two different contexts.
288 Moreover, matching is the wildly more frequently used operation in the case of
289 indexed synonyms and we don't want to slow that down by needless unification.
292 ------------------------------------------------------------
293 -- Might be a one-way match or a unifier
294 type MatchFun = FamInst -- The FamInst template
295 -> TyVarSet -> [Type] -- fi_tvs, fi_tys of that FamInst
296 -> [Type] -- Target to match against
299 type OneSidedMatch = Bool -- Are optimisations that are only valid for
300 -- one sided matches allowed?
302 lookup_fam_inst_env -- The worker, local to this module
306 -> TyCon -> [Type] -- What we are looking for
307 -> [FamInstMatch] -- Successful matches
308 lookup_fam_inst_env match_fun one_sided (pkg_ie, home_ie) fam tys
309 | not (isOpenTyCon fam)
312 = ASSERT( n_tys >= arity ) -- Family type applications must be saturated
313 home_matches ++ pkg_matches
315 home_matches = lookup home_ie
316 pkg_matches = lookup pkg_ie
318 -- See Note [Over-saturated matches]
319 arity = tyConArity fam
321 extra_tys = drop arity tys
322 (match_tys, add_extra_tys)
323 | arity > n_tys = (take arity tys, \res_tys -> res_tys ++ extra_tys)
324 | otherwise = (tys, \res_tys -> res_tys)
325 -- The second case is the common one, hence functional representation
328 rough_tcs = roughMatchTcs match_tys
329 all_tvs = all isNothing rough_tcs && one_sided
332 lookup env = case lookupUFM env fam of
333 Nothing -> [] -- No instances for this class
334 Just (FamIE insts has_tv_insts)
335 -- Short cut for common case:
336 -- The thing we are looking up is of form (C a
337 -- b c), and the FamIE has no instances of
338 -- that form, so don't bother to search
339 | all_tvs && not has_tv_insts -> []
340 | otherwise -> find insts
344 find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs,
345 fi_tys = tpl_tys, fi_tycon = tycon }) : rest)
346 -- Fast check for no match, uses the "rough match" fields
347 | instanceCantMatch rough_tcs mb_tcs
351 | Just subst <- match_fun item tpl_tvs tpl_tys match_tys
352 = (item, add_extra_tys $ substTyVars subst (tyConTyVars tycon)) : find rest
354 -- No match => try next
359 Note [Over-saturated matches]
360 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
361 It's ok to look up an over-saturated type constructor. E.g.
362 type family F a :: * -> *
363 type instance F (a,b) = Either (a->b)
365 The type instance gives rise to a newtype TyCon (at a higher kind
366 which you can't do in Haskell!):
367 newtype FPair a b = FP (Either (a->b))
369 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
370 (FPair, [Int,Bool,Char])
372 The "extra" type argument [Char] just stays on the end.
377 %************************************************************************
379 Looking up a family instance
381 %************************************************************************
384 topNormaliseType :: FamInstEnvs
386 -> Maybe (Coercion, Type)
388 -- Get rid of *outermost* (or toplevel)
391 -- using appropriate coercions.
392 -- By "outer" we mean that toplevelNormaliseType guarantees to return
393 -- a type that does not have a reducible redex (F ty1 .. tyn) as its
394 -- outermost form. It *can* return something like (Maybe (F ty)), where
395 -- (F ty) is a redex.
397 -- Its a bit like Type.repType, but handles type families too
399 topNormaliseType env ty
402 go :: [TyCon] -> Type -> Maybe (Coercion, Type)
403 go rec_nts ty | Just ty' <- coreView ty -- Expand synonyms
406 go rec_nts (TyConApp tc tys) -- Expand newtypes
407 | Just co_con <- newTyConCo_maybe tc -- See Note [Expanding newtypes]
408 = if tc `elem` rec_nts -- in Type.lhs
410 else let nt_co = mkTyConApp co_con tys
411 in add_co nt_co rec_nts' nt_rhs
413 nt_rhs = newTyConInstRhs tc tys
414 rec_nts' | isRecursiveTyCon tc = tc:rec_nts
415 | otherwise = rec_nts
417 go rec_nts (TyConApp tc tys) -- Expand open tycons
419 , (ACo co, ty) <- normaliseTcApp env tc tys
420 = -- The ACo says "something happened"
421 -- Note that normaliseType fully normalises, but it has do to so
428 = case go rec_nts ty of
429 Nothing -> Just (co, ty)
430 Just (co', ty') -> Just (mkTransCoercion co co', ty')
434 normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (CoercionI, Type)
435 normaliseTcApp env tc tys
436 = let -- First normalise the arg types so that they'll match
437 -- when we lookup in in the instance envt
438 (cois, ntys) = mapAndUnzip (normaliseType env) tys
439 tycon_coi = mkTyConAppCoI tc ntys cois
440 in -- Now try the top-level redex
441 case lookupFamInstEnv env tc ntys of
442 -- A matching family instance exists
443 [(fam_inst, tys)] -> (fix_coi, nty)
445 rep_tc = famInstTyCon fam_inst
446 co_tycon = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
447 co = mkTyConApp co_tycon tys
448 first_coi = mkTransCoI tycon_coi (ACo co)
449 (rest_coi,nty) = normaliseType env (mkTyConApp rep_tc tys)
450 fix_coi = mkTransCoI first_coi rest_coi
452 -- No unique matching family instance exists;
453 -- we do not do anything
454 _ -> (tycon_coi, TyConApp tc ntys)
456 normaliseType :: FamInstEnvs -- environment with family instances
458 -> (CoercionI, Type) -- (coercion,new type), where
459 -- co :: old-type ~ new_type
460 -- Normalise the input type, by eliminating *all* type-function redexes
461 -- Returns with IdCo if nothing happens
464 | Just ty' <- coreView ty = normaliseType env ty'
465 normaliseType env (TyConApp tc tys)
466 = normaliseTcApp env tc tys
467 normaliseType env (AppTy ty1 ty2)
468 = let (coi1,nty1) = normaliseType env ty1
469 (coi2,nty2) = normaliseType env ty2
470 in (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
471 normaliseType env (FunTy ty1 ty2)
472 = let (coi1,nty1) = normaliseType env ty1
473 (coi2,nty2) = normaliseType env ty2
474 in (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
475 normaliseType env (ForAllTy tyvar ty1)
476 = let (coi,nty1) = normaliseType env ty1
477 in (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
478 normaliseType _ ty@(TyVarTy _)
480 normaliseType env (PredTy predty)
481 = normalisePred env predty
484 normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type)
485 normalisePred env (ClassP cls tys)
486 = let (cois,tys') = mapAndUnzip (normaliseType env) tys
487 in (mkClassPPredCoI cls tys' cois, PredTy $ ClassP cls tys')
488 normalisePred env (IParam ipn ty)
489 = let (coi,ty') = normaliseType env ty
490 in (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
491 normalisePred env (EqPred ty1 ty2)
492 = let (coi1,ty1') = normaliseType env ty1
493 (coi2,ty2') = normaliseType env ty2
494 in (mkEqPredCoI ty1' coi1 ty2' coi2, PredTy $ EqPred ty1' ty2')