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"
44 %************************************************************************
46 \subsection{Type checked family instance heads}
48 %************************************************************************
52 = FamInst { fi_fam :: Name -- Family name
53 -- INVARIANT: fi_fam = case tyConFamInst_maybe fi_tycon of
54 -- Just (tc, tys) -> tc
56 -- Used for "rough matching"; same idea as for class instances
57 , fi_tcs :: [Maybe Name] -- Top of type args
58 -- INVARIANT: fi_tcs = roughMatchTcs fi_tys
60 -- Used for "proper matching"; ditto
61 , fi_tvs :: TyVarSet -- Template tyvars for full match
62 , fi_tys :: [Type] -- Full arg types
63 -- INVARIANT: fi_tvs = tyConTyVars fi_tycon
64 -- fi_tys = case tyConFamInst_maybe fi_tycon of
65 -- Just (_, tys) -> tys
67 , fi_tycon :: TyCon -- Representation tycon
70 -- Obtain the representation tycon of a family instance.
72 famInstTyCon :: FamInst -> TyCon
73 famInstTyCon = fi_tycon
75 famInstTyVars :: FamInst -> TyVarSet
76 famInstTyVars = fi_tvs
80 instance NamedThing FamInst where
81 getName = getName . fi_tycon
83 instance Outputable FamInst where
86 -- Prints the FamInst as a family instance declaration
87 pprFamInst :: FamInst -> SDoc
89 = hang (pprFamInstHdr famInst)
90 2 (ptext (sLit "--") <+> pprNameLoc (getName famInst))
92 pprFamInstHdr :: FamInst -> SDoc
93 pprFamInstHdr (FamInst {fi_fam = fam, fi_tys = tys, fi_tycon = tycon})
94 = pprTyConSort <+> pprHead
96 pprHead = pprTypeApp fam tys
97 pprTyConSort | isDataTyCon tycon = ptext (sLit "data instance")
98 | isNewTyCon tycon = ptext (sLit "newtype instance")
99 | isSynTyCon tycon = ptext (sLit "type instance")
100 | otherwise = panic "FamInstEnv.pprFamInstHdr"
102 pprFamInsts :: [FamInst] -> SDoc
103 pprFamInsts finsts = vcat (map pprFamInst finsts)
105 famInstHead :: FamInst -> ([TyVar], TyCon, [Type])
106 famInstHead (FamInst {fi_tycon = tycon})
107 = case tyConFamInst_maybe tycon of
108 Nothing -> panic "FamInstEnv.famInstHead"
109 Just (fam, tys) -> (tyConTyVars tycon, fam, tys)
111 -- Make a family instance representation from a tycon. This is used for local
112 -- instances, where we can safely pull on the tycon.
114 mkLocalFamInst :: TyCon -> FamInst
116 = case tyConFamInst_maybe tycon of
117 Nothing -> panic "FamInstEnv.mkLocalFamInst"
120 fi_fam = tyConName fam,
121 fi_tcs = roughMatchTcs tys,
122 fi_tvs = mkVarSet . tyConTyVars $ tycon,
127 -- Make a family instance representation from the information found in an
128 -- unterface file. In particular, we get the rough match info from the iface
129 -- (instead of computing it here).
131 mkImportedFamInst :: Name -> [Maybe Name] -> TyCon -> FamInst
132 mkImportedFamInst fam mb_tcs tycon
136 fi_tvs = mkVarSet . tyConTyVars $ tycon,
137 fi_tys = case tyConFamInst_maybe tycon of
138 Nothing -> panic "FamInstEnv.mkImportedFamInst"
139 Just (_, tys) -> tys,
145 %************************************************************************
149 %************************************************************************
151 InstEnv maps a family name to the list of known instances for that family.
154 type FamInstEnv = UniqFM FamilyInstEnv -- Maps a family to its instances
156 type FamInstEnvs = (FamInstEnv, FamInstEnv)
157 -- External package inst-env, Home-package inst-env
160 = FamIE [FamInst] -- The instances for a particular family, in any order
161 Bool -- True <=> there is an instance of form T a b c
162 -- If *not* then the common case of looking up
163 -- (T a b c) can fail immediately
166 -- * The fs_tvs are distinct in each FamInst
167 -- of a range value of the map (so we can safely unify them)
169 emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
170 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
172 emptyFamInstEnv :: FamInstEnv
173 emptyFamInstEnv = emptyUFM
175 famInstEnvElts :: FamInstEnv -> [FamInst]
176 famInstEnvElts fi = [elt | FamIE elts _ <- eltsUFM fi, elt <- elts]
178 familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
179 familyInstances (pkg_fie, home_fie) fam
180 = get home_fie ++ get pkg_fie
182 get env = case lookupUFM env fam of
183 Just (FamIE insts _) -> insts
186 extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
187 extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis
189 extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
190 extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs})
191 = addToUFM_C add inst_env cls_nm (FamIE [ins_item] ins_tyvar)
193 add (FamIE items tyvar) _ = FamIE (ins_item:items)
195 ins_tyvar = not (any isJust mb_tcs)
198 %************************************************************************
200 Looking up a family instance
202 %************************************************************************
204 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
205 Multiple matches are only possible in case of type families (not data
206 families), and then, it doesn't matter which match we choose (as the
207 instances are guaranteed confluent).
209 We return the matching family instances and the type instance at which it
210 matches. For example, if we lookup 'T [Int]' and have a family instance
212 data instance T [a] = ..
217 coe :Co:R42T a :: T [a] ~ :R42T a
219 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
222 type FamInstMatch = (FamInst, [Type]) -- Matching type instance
223 -- See Note [Over-saturated matches]
227 -> TyCon -> [Type] -- What we are looking for
228 -> [FamInstMatch] -- Successful matches
231 = lookup_fam_inst_env match
233 match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
235 lookupFamInstEnvConflicts
237 -> FamInst -- Putative new instance
238 -> [TyVar] -- Unique tyvars, matching arity of FamInst
239 -> [FamInstMatch] -- Conflicting matches
240 -- E.g. when we are about to add
241 -- f : type instance F [a] = a->a
242 -- we do (lookupFamInstConflicts f [b])
243 -- to find conflicting matches
244 -- The skolem tyvars are needed because we don't have a
245 -- unique supply to hand
247 lookupFamInstEnvConflicts envs fam_inst skol_tvs
248 = lookup_fam_inst_env my_unify envs fam tys'
250 inst_tycon = famInstTyCon fam_inst
251 (fam, tys) = expectJust "FamInstEnv.lookuFamInstEnvConflicts"
252 (tyConFamInst_maybe inst_tycon)
253 skol_tys = mkTyVarTys skol_tvs
254 tys' = substTys (zipTopTvSubst (tyConTyVars inst_tycon) skol_tys) tys
255 -- In example above, fam tys' = F [b]
257 my_unify old_fam_inst tpl_tvs tpl_tys match_tys
258 = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
259 (ppr fam <+> ppr tys) $$
260 (ppr tpl_tvs <+> ppr tpl_tys) )
261 -- Unification will break badly if the variables overlap
262 -- They shouldn't because we allocate separate uniques for them
263 case tcUnifyTys instanceBindFun tpl_tys match_tys of
264 Just subst | conflicting old_fam_inst subst -> Just subst
267 -- - In the case of data family instances, any overlap is fundamentally a
268 -- conflict (as these instances imply injective type mappings).
269 -- - In the case of type family instances, overlap is admitted as long as
270 -- the right-hand sides of the overlapping rules coincide under the
271 -- overlap substitution. We require that they are syntactically equal;
272 -- anything else would be difficult to test for at this stage.
273 conflicting old_fam_inst subst
274 | isAlgTyCon fam = True
275 | otherwise = not (old_rhs `tcEqType` new_rhs)
277 old_tycon = famInstTyCon old_fam_inst
278 old_rhs = mkTyConApp old_tycon (substTyVars subst (tyConTyVars old_tycon))
279 new_rhs = mkTyConApp inst_tycon (substTyVars subst skol_tvs)
282 While @lookupFamInstEnv@ uses a one-way match, the next function
283 @lookupFamInstEnvUnify@ 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 lookup_fam_inst_env -- The worker, local to this module
303 -> TyCon -> [Type] -- What we are looking for
304 -> [FamInstMatch] -- Successful matches
305 lookup_fam_inst_env match_fun (pkg_ie, home_ie) fam tys
306 | not (isOpenTyCon fam)
309 = ASSERT( n_tys >= arity ) -- Family type applications must be saturated
310 home_matches ++ pkg_matches
312 home_matches = lookup home_ie
313 pkg_matches = lookup pkg_ie
315 -- See Note [Over-saturated matches]
316 arity = tyConArity fam
318 extra_tys = drop arity tys
319 (match_tys, add_extra_tys)
320 | arity > n_tys = (take arity tys, \res_tys -> res_tys ++ extra_tys)
321 | otherwise = (tys, \res_tys -> res_tys)
322 -- The second case is the common one, hence functional representation
325 rough_tcs = roughMatchTcs match_tys
326 all_tvs = all isNothing rough_tcs
329 lookup env = case lookupUFM env fam of
330 Nothing -> [] -- No instances for this class
331 Just (FamIE insts has_tv_insts)
332 -- Short cut for common case:
333 -- The thing we are looking up is of form (C a
334 -- b c), and the FamIE has no instances of
335 -- that form, so don't bother to search
336 | all_tvs && not has_tv_insts -> []
337 | otherwise -> find insts
341 find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs,
342 fi_tys = tpl_tys, fi_tycon = tycon }) : rest)
343 -- Fast check for no match, uses the "rough match" fields
344 | instanceCantMatch rough_tcs mb_tcs
348 | Just subst <- match_fun item tpl_tvs tpl_tys match_tys
349 = (item, add_extra_tys $ substTyVars subst (tyConTyVars tycon)) : find rest
351 -- No match => try next
356 Note [Over-saturated matches]
357 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
358 It's ok to look up an over-saturated type constructor. E.g.
359 type family F a :: * -> *
360 type instance F (a,b) = Either (a->b)
362 The type instance gives rise to a newtype TyCon (at a higher kind
363 which you can't do in Haskell!):
364 newtype FPair a b = FP (Either (a->b))
366 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
367 (FPair, [Int,Bool,Char])
369 The "extra" type argument [Char] just stays on the end.
374 %************************************************************************
376 Looking up a family instance
378 %************************************************************************
381 topNormaliseType :: FamInstEnvs
383 -> Maybe (Coercion, Type)
385 -- Get rid of *outermost* (or toplevel)
388 -- using appropriate coercions.
389 -- By "outer" we mean that toplevelNormaliseType guarantees to return
390 -- a type that does not have a reducible redex (F ty1 .. tyn) as its
391 -- outermost form. It *can* return something like (Maybe (F ty)), where
392 -- (F ty) is a redex.
394 -- Its a bit like Type.repType, but handles type families too
396 topNormaliseType env ty
399 go :: [TyCon] -> Type -> Maybe (Coercion, Type)
400 go rec_nts ty | Just ty' <- coreView ty -- Expand synonyms
403 go rec_nts (TyConApp tc tys) -- Expand newtypes
404 | Just co_con <- newTyConCo_maybe tc -- See Note [Expanding newtypes]
405 = if tc `elem` rec_nts -- in Type.lhs
407 else let nt_co = mkTyConApp co_con tys
408 in add_co nt_co rec_nts' nt_rhs
410 nt_rhs = newTyConInstRhs tc tys
411 rec_nts' | isRecursiveTyCon tc = tc:rec_nts
412 | otherwise = rec_nts
414 go rec_nts (TyConApp tc tys) -- Expand open tycons
416 , (ACo co, ty) <- normaliseTcApp env tc tys
417 = -- The ACo says "something happened"
418 -- Note that normaliseType fully normalises, but it has do to so
425 = case go rec_nts ty of
426 Nothing -> Just (co, ty)
427 Just (co', ty') -> Just (mkTransCoercion co co', ty')
431 normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (CoercionI, Type)
432 normaliseTcApp env tc tys
433 = let -- First normalise the arg types so that they'll match
434 -- when we lookup in in the instance envt
435 (cois, ntys) = mapAndUnzip (normaliseType env) tys
436 tycon_coi = mkTyConAppCoI tc ntys cois
437 in -- Now try the top-level redex
438 case lookupFamInstEnv env tc ntys of
439 -- A matching family instance exists
440 [(fam_inst, tys)] -> (fix_coi, nty)
442 rep_tc = famInstTyCon fam_inst
443 co_tycon = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
444 co = mkTyConApp co_tycon tys
445 first_coi = mkTransCoI tycon_coi (ACo co)
446 (rest_coi,nty) = normaliseType env (mkTyConApp rep_tc tys)
447 fix_coi = mkTransCoI first_coi rest_coi
449 -- No unique matching family instance exists;
450 -- we do not do anything
451 _ -> (tycon_coi, TyConApp tc ntys)
453 normaliseType :: FamInstEnvs -- environment with family instances
455 -> (CoercionI, Type) -- (coercion,new type), where
456 -- co :: old-type ~ new_type
457 -- Normalise the input type, by eliminating *all* type-function redexes
458 -- Returns with IdCo if nothing happens
461 | Just ty' <- coreView ty = normaliseType env ty'
462 normaliseType env (TyConApp tc tys)
463 = normaliseTcApp env tc tys
464 normaliseType env (AppTy ty1 ty2)
465 = let (coi1,nty1) = normaliseType env ty1
466 (coi2,nty2) = normaliseType env ty2
467 in (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
468 normaliseType env (FunTy ty1 ty2)
469 = let (coi1,nty1) = normaliseType env ty1
470 (coi2,nty2) = normaliseType env ty2
471 in (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
472 normaliseType env (ForAllTy tyvar ty1)
473 = let (coi,nty1) = normaliseType env ty1
474 in (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
475 normaliseType _ ty@(TyVarTy _)
477 normaliseType env (PredTy predty)
478 = normalisePred env predty
481 normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type)
482 normalisePred env (ClassP cls tys)
483 = let (cois,tys') = mapAndUnzip (normaliseType env) tys
484 in (mkClassPPredCoI cls tys' cois, PredTy $ ClassP cls tys')
485 normalisePred env (IParam ipn ty)
486 = let (coi,ty') = normaliseType env ty
487 in (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
488 normalisePred env (EqPred ty1 ty2)
489 = let (coi1,ty1') = normaliseType env ty1
490 (coi2,ty2') = normaliseType env ty2
491 in (mkEqPredCoI ty1' coi1 ty2' coi2, PredTy $ EqPred ty1' ty2')