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 %************************************************************************
158 InstEnv maps a family name to the list of known instances for that family.
161 type FamInstEnv = UniqFM FamilyInstEnv -- Maps a family to its instances
163 type FamInstEnvs = (FamInstEnv, FamInstEnv)
164 -- External package inst-env, Home-package inst-env
167 = FamIE [FamInst] -- The instances for a particular family, in any order
168 Bool -- True <=> there is an instance of form T a b c
169 -- If *not* then the common case of looking up
170 -- (T a b c) can fail immediately
173 -- * The fs_tvs are distinct in each FamInst
174 -- of a range value of the map (so we can safely unify them)
176 emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
177 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
179 emptyFamInstEnv :: FamInstEnv
180 emptyFamInstEnv = emptyUFM
182 famInstEnvElts :: FamInstEnv -> [FamInst]
183 famInstEnvElts fi = [elt | FamIE elts _ <- eltsUFM fi, elt <- elts]
185 familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
186 familyInstances (pkg_fie, home_fie) fam
187 = get home_fie ++ get pkg_fie
189 get env = case lookupUFM env fam of
190 Just (FamIE insts _) -> insts
193 extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
194 extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis
196 extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
197 extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs})
198 = addToUFM_C add inst_env cls_nm (FamIE [ins_item] ins_tyvar)
200 add (FamIE items tyvar) _ = FamIE (ins_item:items)
202 ins_tyvar = not (any isJust mb_tcs)
205 %************************************************************************
207 Looking up a family instance
209 %************************************************************************
211 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
212 Multiple matches are only possible in case of type families (not data
213 families), and then, it doesn't matter which match we choose (as the
214 instances are guaranteed confluent).
216 We return the matching family instances and the type instance at which it
217 matches. For example, if we lookup 'T [Int]' and have a family instance
219 data instance T [a] = ..
224 coe :Co:R42T a :: T [a] ~ :R42T a
226 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
229 type FamInstMatch = (FamInst, [Type]) -- Matching type instance
230 -- See Note [Over-saturated matches]
234 -> TyCon -> [Type] -- What we are looking for
235 -> [FamInstMatch] -- Successful matches
238 = lookup_fam_inst_env match True
240 match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
242 lookupFamInstEnvConflicts
244 -> FamInst -- Putative new instance
245 -> [TyVar] -- Unique tyvars, matching arity of FamInst
246 -> [FamInstMatch] -- Conflicting matches
247 -- E.g. when we are about to add
248 -- f : type instance F [a] = a->a
249 -- we do (lookupFamInstConflicts f [b])
250 -- to find conflicting matches
251 -- The skolem tyvars are needed because we don't have a
252 -- unique supply to hand
254 lookupFamInstEnvConflicts envs fam_inst skol_tvs
255 = lookup_fam_inst_env my_unify False envs fam tys'
257 inst_tycon = famInstTyCon fam_inst
258 (fam, tys) = expectJust "FamInstEnv.lookuFamInstEnvConflicts"
259 (tyConFamInst_maybe inst_tycon)
260 skol_tys = mkTyVarTys skol_tvs
261 tys' = substTys (zipTopTvSubst (tyConTyVars inst_tycon) skol_tys) tys
262 -- In example above, fam tys' = F [b]
264 my_unify old_fam_inst tpl_tvs tpl_tys match_tys
265 = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
266 (ppr fam <+> ppr tys) $$
267 (ppr tpl_tvs <+> ppr tpl_tys) )
268 -- Unification will break badly if the variables overlap
269 -- They shouldn't because we allocate separate uniques for them
270 case tcUnifyTys instanceBindFun tpl_tys match_tys of
271 Just subst | conflicting old_fam_inst subst -> Just subst
274 -- - In the case of data family instances, any overlap is fundamentally a
275 -- conflict (as these instances imply injective type mappings).
276 -- - In the case of type family instances, overlap is admitted as long as
277 -- the right-hand sides of the overlapping rules coincide under the
278 -- overlap substitution. We require that they are syntactically equal;
279 -- anything else would be difficult to test for at this stage.
280 conflicting old_fam_inst subst
281 | isAlgTyCon fam = True
282 | otherwise = not (old_rhs `tcEqType` new_rhs)
284 old_tycon = famInstTyCon old_fam_inst
285 old_tvs = tyConTyVars old_tycon
286 old_rhs = mkTyConApp old_tycon (substTyVars subst old_tvs)
287 new_rhs = mkTyConApp inst_tycon (substTyVars subst skol_tvs)
290 While @lookupFamInstEnv@ uses a one-way match, the next function
291 @lookupFamInstEnvConflicts@ uses two-way matching (ie, unification). This is
292 needed to check for overlapping instances.
294 For class instances, these two variants of lookup are combined into one
295 function (cf, @InstEnv@). We don't do that for family instances as the
296 results of matching and unification are used in two different contexts.
297 Moreover, matching is the wildly more frequently used operation in the case of
298 indexed synonyms and we don't want to slow that down by needless unification.
301 ------------------------------------------------------------
302 -- Might be a one-way match or a unifier
303 type MatchFun = FamInst -- The FamInst template
304 -> TyVarSet -> [Type] -- fi_tvs, fi_tys of that FamInst
305 -> [Type] -- Target to match against
308 type OneSidedMatch = Bool -- Are optimisations that are only valid for
309 -- one sided matches allowed?
311 lookup_fam_inst_env -- The worker, local to this module
315 -> TyCon -> [Type] -- What we are looking for
316 -> [FamInstMatch] -- Successful matches
317 lookup_fam_inst_env match_fun one_sided (pkg_ie, home_ie) fam tys
318 | not (isFamilyTyCon fam)
321 = ASSERT( n_tys >= arity ) -- Family type applications must be saturated
322 home_matches ++ pkg_matches
324 home_matches = lookup home_ie
325 pkg_matches = lookup pkg_ie
327 -- See Note [Over-saturated matches]
328 arity = tyConArity fam
330 extra_tys = drop arity tys
331 (match_tys, add_extra_tys)
332 | arity > n_tys = (take arity tys, \res_tys -> res_tys ++ extra_tys)
333 | otherwise = (tys, \res_tys -> res_tys)
334 -- The second case is the common one, hence functional representation
337 rough_tcs = roughMatchTcs match_tys
338 all_tvs = all isNothing rough_tcs && one_sided
341 lookup env = case lookupUFM env fam of
342 Nothing -> [] -- No instances for this class
343 Just (FamIE insts has_tv_insts)
344 -- Short cut for common case:
345 -- The thing we are looking up is of form (C a
346 -- b c), and the FamIE has no instances of
347 -- that form, so don't bother to search
348 | all_tvs && not has_tv_insts -> []
349 | otherwise -> find insts
353 find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs,
354 fi_tys = tpl_tys, fi_tycon = tycon }) : rest)
355 -- Fast check for no match, uses the "rough match" fields
356 | instanceCantMatch rough_tcs mb_tcs
360 | Just subst <- match_fun item tpl_tvs tpl_tys match_tys
361 = (item, add_extra_tys $ substTyVars subst (tyConTyVars tycon)) : find rest
363 -- No match => try next
368 Note [Over-saturated matches]
369 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
370 It's ok to look up an over-saturated type constructor. E.g.
371 type family F a :: * -> *
372 type instance F (a,b) = Either (a->b)
374 The type instance gives rise to a newtype TyCon (at a higher kind
375 which you can't do in Haskell!):
376 newtype FPair a b = FP (Either (a->b))
378 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
379 (FPair, [Int,Bool,Char])
381 The "extra" type argument [Char] just stays on the end.
386 %************************************************************************
388 Looking up a family instance
390 %************************************************************************
393 topNormaliseType :: FamInstEnvs
395 -> Maybe (Coercion, Type)
397 -- Get rid of *outermost* (or toplevel)
400 -- using appropriate coercions.
401 -- By "outer" we mean that toplevelNormaliseType guarantees to return
402 -- a type that does not have a reducible redex (F ty1 .. tyn) as its
403 -- outermost form. It *can* return something like (Maybe (F ty)), where
404 -- (F ty) is a redex.
406 -- Its a bit like Type.repType, but handles type families too
408 topNormaliseType env ty
411 go :: [TyCon] -> Type -> Maybe (Coercion, Type)
412 go rec_nts ty | Just ty' <- coreView ty -- Expand synonyms
415 go rec_nts (TyConApp tc tys) -- Expand newtypes
416 | Just co_con <- newTyConCo_maybe tc -- See Note [Expanding newtypes]
417 = if tc `elem` rec_nts -- in Type.lhs
419 else let nt_co = mkTyConApp co_con tys
420 in add_co nt_co rec_nts' nt_rhs
422 nt_rhs = newTyConInstRhs tc tys
423 rec_nts' | isRecursiveTyCon tc = tc:rec_nts
424 | otherwise = rec_nts
426 go rec_nts (TyConApp tc tys) -- Expand open tycons
428 , (ACo co, ty) <- normaliseTcApp env tc tys
429 = -- The ACo says "something happened"
430 -- Note that normaliseType fully normalises, but it has do to so
437 = case go rec_nts ty of
438 Nothing -> Just (co, ty)
439 Just (co', ty') -> Just (mkTransCoercion co co', ty')
443 normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (CoercionI, Type)
444 normaliseTcApp env tc tys
445 = let -- First normalise the arg types so that they'll match
446 -- when we lookup in in the instance envt
447 (cois, ntys) = mapAndUnzip (normaliseType env) tys
448 tycon_coi = mkTyConAppCoI tc cois
449 in -- Now try the top-level redex
450 case lookupFamInstEnv env tc ntys of
451 -- A matching family instance exists
452 [(fam_inst, tys)] -> (fix_coi, nty)
454 rep_tc = famInstTyCon fam_inst
455 co_tycon = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
456 co = mkTyConApp co_tycon tys
457 first_coi = mkTransCoI tycon_coi (ACo co)
458 (rest_coi,nty) = normaliseType env (mkTyConApp rep_tc tys)
459 fix_coi = mkTransCoI first_coi rest_coi
461 -- No unique matching family instance exists;
462 -- we do not do anything
463 _ -> (tycon_coi, TyConApp tc ntys)
465 normaliseType :: FamInstEnvs -- environment with family instances
467 -> (CoercionI, Type) -- (coercion,new type), where
468 -- co :: old-type ~ new_type
469 -- Normalise the input type, by eliminating *all* type-function redexes
470 -- Returns with IdCo if nothing happens
473 | Just ty' <- coreView ty = normaliseType env ty'
474 normaliseType env (TyConApp tc tys)
475 = normaliseTcApp env tc tys
476 normaliseType env (AppTy ty1 ty2)
477 = let (coi1,nty1) = normaliseType env ty1
478 (coi2,nty2) = normaliseType env ty2
479 in (mkAppTyCoI coi1 coi2, mkAppTy nty1 nty2)
480 normaliseType env (FunTy ty1 ty2)
481 = let (coi1,nty1) = normaliseType env ty1
482 (coi2,nty2) = normaliseType env ty2
483 in (mkFunTyCoI coi1 coi2, mkFunTy nty1 nty2)
484 normaliseType env (ForAllTy tyvar ty1)
485 = let (coi,nty1) = normaliseType env ty1
486 in (mkForAllTyCoI tyvar coi, ForAllTy tyvar nty1)
487 normaliseType _ ty@(TyVarTy _)
489 normaliseType env (PredTy predty)
490 = normalisePred env predty
493 normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type)
494 normalisePred env (ClassP cls tys)
495 = let (cois,tys') = mapAndUnzip (normaliseType env) tys
496 in (mkClassPPredCoI cls cois, PredTy $ ClassP cls tys')
497 normalisePred env (IParam ipn ty)
498 = let (coi,ty') = normaliseType env ty
499 in (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
500 normalisePred env (EqPred ty1 ty2)
501 = let (coi1,ty1') = normaliseType env ty1
502 (coi2,ty2') = normaliseType env ty2
503 in (mkEqPredCoI coi1 coi2, PredTy $ EqPred ty1' ty2')