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"
41 %************************************************************************
43 \subsection{Type checked family instance heads}
45 %************************************************************************
49 = FamInst { fi_fam :: Name -- Family name
50 -- INVARIANT: fi_fam = case tyConFamInst_maybe fi_tycon of
51 -- Just (tc, tys) -> tc
53 -- Used for "rough matching"; same idea as for class instances
54 , fi_tcs :: [Maybe Name] -- Top of type args
55 -- INVARIANT: fi_tcs = roughMatchTcs fi_tys
57 -- Used for "proper matching"; ditto
58 , fi_tvs :: TyVarSet -- Template tyvars for full match
59 , fi_tys :: [Type] -- Full arg types
60 -- INVARIANT: fi_tvs = tyConTyVars fi_tycon
61 -- fi_tys = case tyConFamInst_maybe fi_tycon of
62 -- Just (_, tys) -> tys
64 , fi_tycon :: TyCon -- Representation tycon
67 -- Obtain the representation tycon of a family instance.
69 famInstTyCon :: FamInst -> TyCon
70 famInstTyCon = fi_tycon
72 famInstTyVars :: FamInst -> TyVarSet
73 famInstTyVars = fi_tvs
77 instance NamedThing FamInst where
78 getName = getName . fi_tycon
80 instance Outputable FamInst where
83 -- Prints the FamInst as a family instance declaration
84 pprFamInst :: FamInst -> SDoc
86 = hang (pprFamInstHdr famInst)
87 2 (ptext (sLit "--") <+> pprNameLoc (getName famInst))
89 pprFamInstHdr :: FamInst -> SDoc
90 pprFamInstHdr (FamInst {fi_tycon = rep_tc})
91 = pprTyConSort <+> pp_instance <+> pprHead
93 Just (fam_tc, tys) = tyConFamInst_maybe rep_tc
95 -- For *associated* types, say "type T Int = blah"
96 -- For *top level* type instances, say "type instance T Int = blah"
98 | isTyConAssoc fam_tc = empty
99 | otherwise = ptext (sLit "instance")
101 pprHead = pprTypeApp fam_tc tys
102 pprTyConSort | isDataTyCon rep_tc = ptext (sLit "data")
103 | isNewTyCon rep_tc = ptext (sLit "newtype")
104 | isSynTyCon rep_tc = ptext (sLit "type")
105 | isAbstractTyCon rep_tc = ptext (sLit "data")
106 | otherwise = panic "FamInstEnv.pprFamInstHdr"
108 pprFamInsts :: [FamInst] -> SDoc
109 pprFamInsts finsts = vcat (map pprFamInst finsts)
111 famInstHead :: FamInst -> ([TyVar], TyCon, [Type])
112 famInstHead (FamInst {fi_tycon = tycon})
113 = case tyConFamInst_maybe tycon of
114 Nothing -> panic "FamInstEnv.famInstHead"
115 Just (fam, tys) -> (tyConTyVars tycon, fam, tys)
117 -- Make a family instance representation from a tycon. This is used for local
118 -- instances, where we can safely pull on the tycon.
120 mkLocalFamInst :: TyCon -> FamInst
122 = case tyConFamInst_maybe tycon of
123 Nothing -> panic "FamInstEnv.mkLocalFamInst"
126 fi_fam = tyConName fam,
127 fi_tcs = roughMatchTcs tys,
128 fi_tvs = mkVarSet . tyConTyVars $ tycon,
133 -- Make a family instance representation from the information found in an
134 -- unterface file. In particular, we get the rough match info from the iface
135 -- (instead of computing it here).
137 mkImportedFamInst :: Name -> [Maybe Name] -> TyCon -> FamInst
138 mkImportedFamInst fam mb_tcs tycon
142 fi_tvs = mkVarSet . tyConTyVars $ tycon,
143 fi_tys = case tyConFamInst_maybe tycon of
144 Nothing -> panic "FamInstEnv.mkImportedFamInst"
145 Just (_, tys) -> tys,
151 %************************************************************************
155 %************************************************************************
158 ~~~~~~~~~~~~~~~~~~~~~
159 A FamInstEnv maps a family name to the list of known instances for that family.
161 The same FamInstEnv includes both 'data family' and 'type family' instances.
162 Type families are reduced during type inference, but not data families;
163 the user explains when to use a data family instance by using contructors
164 and pattern matching.
166 Neverthless it is still useful to have data families in the FamInstEnv:
168 - For finding overlaps and conflicts
170 - For finding the representation type...see FamInstEnv.topNormaliseType
171 and its call site in Simplify
173 - In standalone deriving instance Eq (T [Int]) we need to find the
174 representation type for T [Int]
177 type FamInstEnv = UniqFM FamilyInstEnv -- Maps a family to its instances
178 -- See Note [FamInstEnv]
180 type FamInstEnvs = (FamInstEnv, FamInstEnv)
181 -- External package inst-env, Home-package inst-env
184 = FamIE [FamInst] -- The instances for a particular family, in any order
185 Bool -- True <=> there is an instance of form T a b c
186 -- If *not* then the common case of looking up
187 -- (T a b c) can fail immediately
189 instance Outputable FamilyInstEnv where
190 ppr (FamIE fs b) = ptext (sLit "FamIE") <+> ppr b <+> vcat (map ppr fs)
193 -- * The fs_tvs are distinct in each FamInst
194 -- of a range value of the map (so we can safely unify them)
196 emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
197 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
199 emptyFamInstEnv :: FamInstEnv
200 emptyFamInstEnv = emptyUFM
202 famInstEnvElts :: FamInstEnv -> [FamInst]
203 famInstEnvElts fi = [elt | FamIE elts _ <- eltsUFM fi, elt <- elts]
205 familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
206 familyInstances (pkg_fie, home_fie) fam
207 = get home_fie ++ get pkg_fie
209 get env = case lookupUFM env fam of
210 Just (FamIE insts _) -> insts
213 extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
214 extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis
216 extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
217 extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs})
218 = addToUFM_C add inst_env cls_nm (FamIE [ins_item] ins_tyvar)
220 add (FamIE items tyvar) _ = FamIE (ins_item:items)
222 ins_tyvar = not (any isJust mb_tcs)
225 %************************************************************************
227 Looking up a family instance
229 %************************************************************************
231 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
232 Multiple matches are only possible in case of type families (not data
233 families), and then, it doesn't matter which match we choose (as the
234 instances are guaranteed confluent).
236 We return the matching family instances and the type instance at which it
237 matches. For example, if we lookup 'T [Int]' and have a family instance
239 data instance T [a] = ..
244 coe :Co:R42T a :: T [a] ~ :R42T a
246 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
249 type FamInstMatch = (FamInst, [Type]) -- Matching type instance
250 -- See Note [Over-saturated matches]
254 -> TyCon -> [Type] -- What we are looking for
255 -> [FamInstMatch] -- Successful matches
256 -- Precondition: the tycon is saturated (or over-saturated)
259 = lookup_fam_inst_env match True
261 match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
263 lookupFamInstEnvConflicts
265 -> FamInst -- Putative new instance
266 -> [TyVar] -- Unique tyvars, matching arity of FamInst
267 -> [FamInstMatch] -- Conflicting matches
268 -- E.g. when we are about to add
269 -- f : type instance F [a] = a->a
270 -- we do (lookupFamInstConflicts f [b])
271 -- to find conflicting matches
272 -- The skolem tyvars are needed because we don't have a
273 -- unique supply to hand
275 -- Precondition: the tycon is saturated (or over-saturated)
277 lookupFamInstEnvConflicts envs fam_inst skol_tvs
278 = lookup_fam_inst_env my_unify False envs fam tys'
280 inst_tycon = famInstTyCon fam_inst
281 (fam, tys) = expectJust "FamInstEnv.lookuFamInstEnvConflicts"
282 (tyConFamInst_maybe inst_tycon)
283 skol_tys = mkTyVarTys skol_tvs
284 tys' = substTys (zipTopTvSubst (tyConTyVars inst_tycon) skol_tys) tys
285 -- In example above, fam tys' = F [b]
287 my_unify old_fam_inst tpl_tvs tpl_tys match_tys
288 = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
289 (ppr fam <+> ppr tys) $$
290 (ppr tpl_tvs <+> ppr tpl_tys) )
291 -- Unification will break badly if the variables overlap
292 -- They shouldn't because we allocate separate uniques for them
293 case tcUnifyTys instanceBindFun tpl_tys match_tys of
294 Just subst | conflicting old_fam_inst subst -> Just subst
297 -- - In the case of data family instances, any overlap is fundamentally a
298 -- conflict (as these instances imply injective type mappings).
299 -- - In the case of type family instances, overlap is admitted as long as
300 -- the right-hand sides of the overlapping rules coincide under the
301 -- overlap substitution. We require that they are syntactically equal;
302 -- anything else would be difficult to test for at this stage.
303 conflicting old_fam_inst subst
304 | isAlgTyCon fam = True
305 | otherwise = not (old_rhs `eqType` new_rhs)
307 old_tycon = famInstTyCon old_fam_inst
308 old_tvs = tyConTyVars old_tycon
309 old_rhs = mkTyConApp old_tycon (substTyVars subst old_tvs)
310 new_rhs = mkTyConApp inst_tycon (substTyVars subst skol_tvs)
313 While @lookupFamInstEnv@ uses a one-way match, the next function
314 @lookupFamInstEnvConflicts@ uses two-way matching (ie, unification). This is
315 needed to check for overlapping instances.
317 For class instances, these two variants of lookup are combined into one
318 function (cf, @InstEnv@). We don't do that for family instances as the
319 results of matching and unification are used in two different contexts.
320 Moreover, matching is the wildly more frequently used operation in the case of
321 indexed synonyms and we don't want to slow that down by needless unification.
324 ------------------------------------------------------------
325 -- Might be a one-way match or a unifier
326 type MatchFun = FamInst -- The FamInst template
327 -> TyVarSet -> [Type] -- fi_tvs, fi_tys of that FamInst
328 -> [Type] -- Target to match against
331 type OneSidedMatch = Bool -- Are optimisations that are only valid for
332 -- one sided matches allowed?
334 lookup_fam_inst_env -- The worker, local to this module
338 -> TyCon -> [Type] -- What we are looking for
339 -> [FamInstMatch] -- Successful matches
341 -- Precondition: the tycon is saturated (or over-saturated)
343 lookup_fam_inst_env match_fun one_sided (pkg_ie, home_ie) fam tys
344 | not (isFamilyTyCon fam)
347 = ASSERT2( n_tys >= arity, ppr fam <+> ppr tys ) -- Family type applications must be saturated
348 home_matches ++ pkg_matches
350 home_matches = lookup home_ie
351 pkg_matches = lookup pkg_ie
353 -- See Note [Over-saturated matches]
354 arity = tyConArity fam
356 extra_tys = drop arity tys
357 (match_tys, add_extra_tys)
358 | arity > n_tys = (take arity tys, \res_tys -> res_tys ++ extra_tys)
359 | otherwise = (tys, \res_tys -> res_tys)
360 -- The second case is the common one, hence functional representation
363 rough_tcs = roughMatchTcs match_tys
364 all_tvs = all isNothing rough_tcs && one_sided
367 lookup env = case lookupUFM env fam of
368 Nothing -> [] -- No instances for this class
369 Just (FamIE insts has_tv_insts)
370 -- Short cut for common case:
371 -- The thing we are looking up is of form (C a
372 -- b c), and the FamIE has no instances of
373 -- that form, so don't bother to search
374 | all_tvs && not has_tv_insts -> []
375 | otherwise -> find insts
379 find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs,
380 fi_tys = tpl_tys, fi_tycon = tycon }) : rest)
381 -- Fast check for no match, uses the "rough match" fields
382 | instanceCantMatch rough_tcs mb_tcs
386 | Just subst <- match_fun item tpl_tvs tpl_tys match_tys
387 = (item, add_extra_tys $ substTyVars subst (tyConTyVars tycon)) : find rest
389 -- No match => try next
394 Note [Over-saturated matches]
395 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
396 It's ok to look up an over-saturated type constructor. E.g.
397 type family F a :: * -> *
398 type instance F (a,b) = Either (a->b)
400 The type instance gives rise to a newtype TyCon (at a higher kind
401 which you can't do in Haskell!):
402 newtype FPair a b = FP (Either (a->b))
404 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
405 (FPair, [Int,Bool,Char])
407 The "extra" type argument [Char] just stays on the end.
412 %************************************************************************
414 Looking up a family instance
416 %************************************************************************
419 topNormaliseType :: FamInstEnvs
421 -> Maybe (Coercion, Type)
423 -- Get rid of *outermost* (or toplevel)
426 -- using appropriate coercions.
427 -- By "outer" we mean that toplevelNormaliseType guarantees to return
428 -- a type that does not have a reducible redex (F ty1 .. tyn) as its
429 -- outermost form. It *can* return something like (Maybe (F ty)), where
430 -- (F ty) is a redex.
432 -- Its a bit like Type.repType, but handles type families too
434 topNormaliseType env ty
437 go :: [TyCon] -> Type -> Maybe (Coercion, Type)
438 go rec_nts ty | Just ty' <- coreView ty -- Expand synonyms
441 go rec_nts (TyConApp tc tys)
442 | isNewTyCon tc -- Expand newtypes
443 = if tc `elem` rec_nts -- See Note [Expanding newtypes] in Type.lhs
445 else let nt_co = mkAxInstCo (newTyConCo tc) tys
446 in add_co nt_co rec_nts' nt_rhs
448 | isFamilyTyCon tc -- Expand open tycons
449 , (co, ty) <- normaliseTcApp env tc tys
450 -- Note that normaliseType fully normalises,
451 -- but it has do to so to be sure that
453 = add_co co rec_nts ty
455 nt_rhs = newTyConInstRhs tc tys
456 rec_nts' | isRecursiveTyCon tc = tc:rec_nts
457 | otherwise = rec_nts
462 = case go rec_nts ty of
463 Nothing -> Just (co, ty)
464 Just (co', ty') -> Just (mkTransCo co co', ty')
468 normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (Coercion, Type)
469 normaliseTcApp env tc tys
471 , tyConArity tc <= length tys -- Unsaturated data families are possible
472 , [(fam_inst, inst_tys)] <- lookupFamInstEnv env tc ntys
473 = let -- A matching family instance exists
474 rep_tc = famInstTyCon fam_inst
475 co_tycon = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
476 co = mkAxInstCo co_tycon inst_tys
477 first_coi = mkTransCo tycon_coi co
478 (rest_coi,nty) = normaliseType env (mkTyConApp rep_tc inst_tys)
479 fix_coi = mkTransCo first_coi rest_coi
483 | otherwise -- No unique matching family instance exists;
484 -- we do not do anything
485 = (tycon_coi, TyConApp tc ntys)
488 -- Normalise the arg types so that they'll match
489 -- when we lookup in in the instance envt
490 (cois, ntys) = mapAndUnzip (normaliseType env) tys
491 tycon_coi = mkTyConAppCo tc cois
494 normaliseType :: FamInstEnvs -- environment with family instances
496 -> (Coercion, Type) -- (coercion,new type), where
497 -- co :: old-type ~ new_type
498 -- Normalise the input type, by eliminating *all* type-function redexes
499 -- Returns with Refl if nothing happens
502 | Just ty' <- coreView ty = normaliseType env ty'
503 normaliseType env (TyConApp tc tys)
504 = normaliseTcApp env tc tys
505 normaliseType env (AppTy ty1 ty2)
506 = let (coi1,nty1) = normaliseType env ty1
507 (coi2,nty2) = normaliseType env ty2
508 in (mkAppCo coi1 coi2, mkAppTy nty1 nty2)
509 normaliseType env (FunTy ty1 ty2)
510 = let (coi1,nty1) = normaliseType env ty1
511 (coi2,nty2) = normaliseType env ty2
512 in (mkFunCo coi1 coi2, mkFunTy nty1 nty2)
513 normaliseType env (ForAllTy tyvar ty1)
514 = let (coi,nty1) = normaliseType env ty1
515 in (mkForAllCo tyvar coi, ForAllTy tyvar nty1)
516 normaliseType _ ty@(TyVarTy _)
518 normaliseType env (PredTy predty)
519 = normalisePred env predty
522 normalisePred :: FamInstEnvs -> PredType -> (Coercion,Type)
523 normalisePred env (ClassP cls tys)
524 = let (cos,tys') = mapAndUnzip (normaliseType env) tys
525 in (mkPredCo $ ClassP cls cos, PredTy $ ClassP cls tys')
526 normalisePred env (IParam ipn ty)
527 = let (co,ty') = normaliseType env ty
528 in (mkPredCo $ (IParam ipn co), PredTy $ IParam ipn ty')
529 normalisePred env (EqPred ty1 ty2)
530 = let (co1,ty1') = normaliseType env ty1
531 (co2,ty2') = normaliseType env ty2
532 in (mkPredCo $ (EqPred co1 co2), PredTy $ EqPred ty1' ty2')