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, lookupFamInstEnvUnify,
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)'.
221 Note [Over-saturated matches]
222 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
223 It's ok to look up an over-saturated type constructor. E.g.
224 type family F a :: * -> *
225 type instance F (a,b) = Either (a->b)
227 The type instance gives rise to a newtype TyCon (at a higher kind
228 which you can't do in Haskell!):
229 newtype FPair a b = FP (Either (a->b))
231 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
232 (FPair, [Int,Bool,Char])
234 The "extra" type argument [Char] just stays on the end.
238 type FamInstMatch = (FamInst, [Type]) -- Matching type instance
239 -- See Note [Over-saturated matches]
241 lookupFamInstEnv :: FamInstEnvs
242 -> TyCon -> [Type] -- What we are looking for
243 -> [FamInstMatch] -- Successful matches
244 lookupFamInstEnv (pkg_ie, home_ie) fam tys
245 | not (isOpenTyCon fam)
248 = ASSERT( n_tys >= arity ) -- Family type applications must be saturated
249 home_matches ++ pkg_matches
251 rough_tcs = roughMatchTcs tys
252 all_tvs = all isNothing rough_tcs
253 home_matches = lookup home_ie
254 pkg_matches = lookup pkg_ie
256 -- See Note [Over-saturated matches]
257 arity = tyConArity fam
259 extra_tys = drop arity tys
260 (match_tys, add_extra_tys)
261 | arity > n_tys = (take arity tys, \res_tys -> res_tys ++ extra_tys)
262 | otherwise = (tys, \res_tys -> res_tys)
263 -- The second case is the common one, hence functional representation
266 lookup env = case lookupUFM env fam of
267 Nothing -> [] -- No instances for this class
268 Just (FamIE insts has_tv_insts)
269 -- Short cut for common case:
270 -- The thing we are looking up is of form (C a
271 -- b c), and the FamIE has no instances of
272 -- that form, so don't bother to search
273 | all_tvs && not has_tv_insts -> []
274 | otherwise -> find insts
278 find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs,
279 fi_tys = tpl_tys, fi_tycon = tycon }) : rest)
280 -- Fast check for no match, uses the "rough match" fields
281 | instanceCantMatch rough_tcs mb_tcs
285 | Just subst <- tcMatchTys tpl_tvs tpl_tys match_tys
286 = (item, add_extra_tys $ substTyVars subst (tyConTyVars tycon)) : find rest
288 -- No match => try next
293 While @lookupFamInstEnv@ uses a one-way match, the next function
294 @lookupFamInstEnvUnify@ uses two-way matching (ie, unification). This is
295 needed to check for overlapping instances.
297 For class instances, these two variants of lookup are combined into one
298 function (cf, @InstEnv@). We don't do that for family instances as the
299 results of matching and unification are used in two different contexts.
300 Moreover, matching is the wildly more frequently used operation in the case of
301 indexed synonyms and we don't want to slow that down by needless unification.
304 lookupFamInstEnvUnify :: (FamInstEnv, FamInstEnv) -> TyCon -> [Type]
305 -> [(FamInstMatch, TvSubst)]
306 lookupFamInstEnvUnify (pkg_ie, home_ie) fam tys
307 | not (isOpenTyCon fam)
310 = home_matches ++ pkg_matches
312 rough_tcs = roughMatchTcs tys
313 all_tvs = all isNothing rough_tcs
314 home_matches = lookup home_ie
315 pkg_matches = lookup pkg_ie
318 lookup env = case lookupUFM env fam of
319 Nothing -> [] -- No instances for this class
320 Just (FamIE insts has_tv_insts)
321 -- Short cut for common case:
322 -- The thing we are looking up is of form (C a
323 -- b c), and the FamIE has no instances of
324 -- that form, so don't bother to search
325 | all_tvs && not has_tv_insts -> []
326 | otherwise -> find insts
330 find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs,
331 fi_tys = tpl_tys, fi_tycon = tycon }) : rest)
332 -- Fast check for no match, uses the "rough match" fields
333 | instanceCantMatch rough_tcs mb_tcs
337 = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
338 (ppr fam <+> ppr tys <+> ppr all_tvs) $$
339 (ppr tycon <+> ppr tpl_tvs <+> ppr tpl_tys)
341 -- Unification will break badly if the variables overlap
342 -- They shouldn't because we allocate separate uniques for them
343 case tcUnifyTys instanceBindFun tpl_tys tys of
344 Just subst -> let rep_tys = substTyVars subst (tyConTyVars tycon)
346 ((item, rep_tys), subst) : find rest
350 %************************************************************************
352 Looking up a family instance
354 %************************************************************************
357 topNormaliseType :: FamInstEnvs
359 -> Maybe (Coercion, Type)
361 -- Get rid of *outermost* (or toplevel)
364 -- using appropriate coercions.
365 -- By "outer" we mean that toplevelNormaliseType guarantees to return
366 -- a type that does not have a reducible redex (F ty1 .. tyn) as its
367 -- outermost form. It *can* return something like (Maybe (F ty)), where
368 -- (F ty) is a redex.
370 -- Its a bit like Type.repType, but handles type families too
372 topNormaliseType env ty
375 go :: [TyCon] -> Type -> Maybe (Coercion, Type)
376 go rec_nts ty | Just ty' <- coreView ty -- Expand synonyms
379 go rec_nts (TyConApp tc tys) -- Expand newtypes
380 | Just co_con <- newTyConCo_maybe tc -- See Note [Expanding newtypes]
381 = if tc `elem` rec_nts -- in Type.lhs
383 else let nt_co = mkTyConApp co_con tys
384 in add_co nt_co rec_nts' nt_rhs
386 nt_rhs = newTyConInstRhs tc tys
387 rec_nts' | isRecursiveTyCon tc = tc:rec_nts
388 | otherwise = rec_nts
390 go rec_nts (TyConApp tc tys) -- Expand open tycons
392 , (ACo co, ty) <- normaliseTcApp env tc tys
393 = -- The ACo says "something happened"
394 -- Note that normaliseType fully normalises, but it has do to so
401 = case go rec_nts ty of
402 Nothing -> Just (co, ty)
403 Just (co', ty') -> Just (mkTransCoercion co co', ty')
407 normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (CoercionI, Type)
408 normaliseTcApp env tc tys
409 = let -- First normalise the arg types so that they'll match
410 -- when we lookup in in the instance envt
411 (cois, ntys) = mapAndUnzip (normaliseType env) tys
412 tycon_coi = mkTyConAppCoI tc ntys cois
413 in -- Now try the top-level redex
414 case lookupFamInstEnv env tc ntys of
415 -- A matching family instance exists
416 [(fam_inst, tys)] -> (fix_coi, nty)
418 rep_tc = famInstTyCon fam_inst
419 co_tycon = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
420 co = mkTyConApp co_tycon tys
421 first_coi = mkTransCoI tycon_coi (ACo co)
422 (rest_coi,nty) = normaliseType env (mkTyConApp rep_tc tys)
423 fix_coi = mkTransCoI first_coi rest_coi
425 -- No unique matching family instance exists;
426 -- we do not do anything
427 _ -> (tycon_coi, TyConApp tc ntys)
429 normaliseType :: FamInstEnvs -- environment with family instances
431 -> (CoercionI, Type) -- (coercion,new type), where
432 -- co :: old-type ~ new_type
433 -- Normalise the input type, by eliminating *all* type-function redexes
434 -- Returns with IdCo if nothing happens
437 | Just ty' <- coreView ty = normaliseType env ty'
438 normaliseType env (TyConApp tc tys)
439 = normaliseTcApp env tc tys
440 normaliseType env (AppTy ty1 ty2)
441 = let (coi1,nty1) = normaliseType env ty1
442 (coi2,nty2) = normaliseType env ty2
443 in (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
444 normaliseType env (FunTy ty1 ty2)
445 = let (coi1,nty1) = normaliseType env ty1
446 (coi2,nty2) = normaliseType env ty2
447 in (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
448 normaliseType env (ForAllTy tyvar ty1)
449 = let (coi,nty1) = normaliseType env ty1
450 in (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
451 normaliseType _ ty@(TyVarTy _)
453 normaliseType env (PredTy predty)
454 = normalisePred env predty
457 normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type)
458 normalisePred env (ClassP cls tys)
459 = let (cois,tys') = mapAndUnzip (normaliseType env) tys
460 in (mkClassPPredCoI cls tys' cois, PredTy $ ClassP cls tys')
461 normalisePred env (IParam ipn ty)
462 = let (coi,ty') = normaliseType env ty
463 in (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
464 normalisePred env (EqPred ty1 ty2)
465 = let (coi1,ty1') = normaliseType env ty1
466 (coi2,ty2') = normaliseType env ty2
467 in (mkEqPredCoI ty1' coi1 ty2' coi2, PredTy $ EqPred ty1' ty2')