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 (vcat [ ifPprDebug (ptext (sLit "Coercion axiom:") <+> pp_ax)
88 , ptext (sLit "--") <+> pprNameLoc (getName famInst)])
90 pp_ax = case tyConFamilyCoercion_maybe (fi_tycon famInst) of
92 Nothing -> ptext (sLit "<not there!>")
94 pprFamInstHdr :: FamInst -> SDoc
95 pprFamInstHdr (FamInst {fi_tycon = rep_tc})
96 = pprTyConSort <+> pp_instance <+> pprHead
98 Just (fam_tc, tys) = tyConFamInst_maybe rep_tc
100 -- For *associated* types, say "type T Int = blah"
101 -- For *top level* type instances, say "type instance T Int = blah"
103 | isTyConAssoc fam_tc = empty
104 | otherwise = ptext (sLit "instance")
106 pprHead = pprTypeApp fam_tc tys
107 pprTyConSort | isDataTyCon rep_tc = ptext (sLit "data")
108 | isNewTyCon rep_tc = ptext (sLit "newtype")
109 | isSynTyCon rep_tc = ptext (sLit "type")
110 | isAbstractTyCon rep_tc = ptext (sLit "data")
111 | otherwise = panic "FamInstEnv.pprFamInstHdr"
113 pprFamInsts :: [FamInst] -> SDoc
114 pprFamInsts finsts = vcat (map pprFamInst finsts)
116 famInstHead :: FamInst -> ([TyVar], TyCon, [Type])
117 famInstHead (FamInst {fi_tycon = tycon})
118 = case tyConFamInst_maybe tycon of
119 Nothing -> panic "FamInstEnv.famInstHead"
120 Just (fam, tys) -> (tyConTyVars tycon, fam, tys)
122 -- Make a family instance representation from a tycon. This is used for local
123 -- instances, where we can safely pull on the tycon.
125 mkLocalFamInst :: TyCon -> FamInst
127 = case tyConFamInst_maybe tycon of
128 Nothing -> panic "FamInstEnv.mkLocalFamInst"
131 fi_fam = tyConName fam,
132 fi_tcs = roughMatchTcs tys,
133 fi_tvs = mkVarSet . tyConTyVars $ tycon,
138 -- Make a family instance representation from the information found in an
139 -- unterface file. In particular, we get the rough match info from the iface
140 -- (instead of computing it here).
142 mkImportedFamInst :: Name -> [Maybe Name] -> TyCon -> FamInst
143 mkImportedFamInst fam mb_tcs tycon
147 fi_tvs = mkVarSet . tyConTyVars $ tycon,
148 fi_tys = case tyConFamInst_maybe tycon of
149 Nothing -> panic "FamInstEnv.mkImportedFamInst"
150 Just (_, tys) -> tys,
156 %************************************************************************
160 %************************************************************************
163 ~~~~~~~~~~~~~~~~~~~~~
164 A FamInstEnv maps a family name to the list of known instances for that family.
166 The same FamInstEnv includes both 'data family' and 'type family' instances.
167 Type families are reduced during type inference, but not data families;
168 the user explains when to use a data family instance by using contructors
169 and pattern matching.
171 Neverthless it is still useful to have data families in the FamInstEnv:
173 - For finding overlaps and conflicts
175 - For finding the representation type...see FamInstEnv.topNormaliseType
176 and its call site in Simplify
178 - In standalone deriving instance Eq (T [Int]) we need to find the
179 representation type for T [Int]
182 type FamInstEnv = UniqFM FamilyInstEnv -- Maps a family to its instances
183 -- See Note [FamInstEnv]
185 type FamInstEnvs = (FamInstEnv, FamInstEnv)
186 -- External package inst-env, Home-package inst-env
189 = FamIE [FamInst] -- The instances for a particular family, in any order
190 Bool -- True <=> there is an instance of form T a b c
191 -- If *not* then the common case of looking up
192 -- (T a b c) can fail immediately
194 instance Outputable FamilyInstEnv where
195 ppr (FamIE fs b) = ptext (sLit "FamIE") <+> ppr b <+> vcat (map ppr fs)
198 -- * The fs_tvs are distinct in each FamInst
199 -- of a range value of the map (so we can safely unify them)
201 emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
202 emptyFamInstEnvs = (emptyFamInstEnv, emptyFamInstEnv)
204 emptyFamInstEnv :: FamInstEnv
205 emptyFamInstEnv = emptyUFM
207 famInstEnvElts :: FamInstEnv -> [FamInst]
208 famInstEnvElts fi = [elt | FamIE elts _ <- eltsUFM fi, elt <- elts]
210 familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
211 familyInstances (pkg_fie, home_fie) fam
212 = get home_fie ++ get pkg_fie
214 get env = case lookupUFM env fam of
215 Just (FamIE insts _) -> insts
218 extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
219 extendFamInstEnvList inst_env fis = foldl extendFamInstEnv inst_env fis
221 extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
222 extendFamInstEnv inst_env ins_item@(FamInst {fi_fam = cls_nm, fi_tcs = mb_tcs})
223 = addToUFM_C add inst_env cls_nm (FamIE [ins_item] ins_tyvar)
225 add (FamIE items tyvar) _ = FamIE (ins_item:items)
227 ins_tyvar = not (any isJust mb_tcs)
230 %************************************************************************
232 Looking up a family instance
234 %************************************************************************
236 @lookupFamInstEnv@ looks up in a @FamInstEnv@, using a one-way match.
237 Multiple matches are only possible in case of type families (not data
238 families), and then, it doesn't matter which match we choose (as the
239 instances are guaranteed confluent).
241 We return the matching family instances and the type instance at which it
242 matches. For example, if we lookup 'T [Int]' and have a family instance
244 data instance T [a] = ..
249 coe :Co:R42T a :: T [a] ~ :R42T a
251 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
254 type FamInstMatch = (FamInst, [Type]) -- Matching type instance
255 -- See Note [Over-saturated matches]
259 -> TyCon -> [Type] -- What we are looking for
260 -> [FamInstMatch] -- Successful matches
261 -- Precondition: the tycon is saturated (or over-saturated)
264 = lookup_fam_inst_env match True
266 match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
268 lookupFamInstEnvConflicts
270 -> FamInst -- Putative new instance
271 -> [TyVar] -- Unique tyvars, matching arity of FamInst
272 -> [FamInstMatch] -- Conflicting matches
273 -- E.g. when we are about to add
274 -- f : type instance F [a] = a->a
275 -- we do (lookupFamInstConflicts f [b])
276 -- to find conflicting matches
277 -- The skolem tyvars are needed because we don't have a
278 -- unique supply to hand
280 -- Precondition: the tycon is saturated (or over-saturated)
282 lookupFamInstEnvConflicts envs fam_inst skol_tvs
283 = lookup_fam_inst_env my_unify False envs fam tys'
285 inst_tycon = famInstTyCon fam_inst
286 (fam, tys) = expectJust "FamInstEnv.lookuFamInstEnvConflicts"
287 (tyConFamInst_maybe inst_tycon)
288 skol_tys = mkTyVarTys skol_tvs
289 tys' = substTys (zipTopTvSubst (tyConTyVars inst_tycon) skol_tys) tys
290 -- In example above, fam tys' = F [b]
292 my_unify old_fam_inst tpl_tvs tpl_tys match_tys
293 = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
294 (ppr fam <+> ppr tys) $$
295 (ppr tpl_tvs <+> ppr tpl_tys) )
296 -- Unification will break badly if the variables overlap
297 -- They shouldn't because we allocate separate uniques for them
298 case tcUnifyTys instanceBindFun tpl_tys match_tys of
299 Just subst | conflicting old_fam_inst subst -> Just subst
302 -- - In the case of data family instances, any overlap is fundamentally a
303 -- conflict (as these instances imply injective type mappings).
304 -- - In the case of type family instances, overlap is admitted as long as
305 -- the right-hand sides of the overlapping rules coincide under the
306 -- overlap substitution. We require that they are syntactically equal;
307 -- anything else would be difficult to test for at this stage.
308 conflicting old_fam_inst subst
309 | isAlgTyCon fam = True
310 | otherwise = not (old_rhs `eqType` new_rhs)
312 old_tycon = famInstTyCon old_fam_inst
313 old_tvs = tyConTyVars old_tycon
314 old_rhs = mkTyConApp old_tycon (substTyVars subst old_tvs)
315 new_rhs = mkTyConApp inst_tycon (substTyVars subst skol_tvs)
318 While @lookupFamInstEnv@ uses a one-way match, the next function
319 @lookupFamInstEnvConflicts@ uses two-way matching (ie, unification). This is
320 needed to check for overlapping instances.
322 For class instances, these two variants of lookup are combined into one
323 function (cf, @InstEnv@). We don't do that for family instances as the
324 results of matching and unification are used in two different contexts.
325 Moreover, matching is the wildly more frequently used operation in the case of
326 indexed synonyms and we don't want to slow that down by needless unification.
329 ------------------------------------------------------------
330 -- Might be a one-way match or a unifier
331 type MatchFun = FamInst -- The FamInst template
332 -> TyVarSet -> [Type] -- fi_tvs, fi_tys of that FamInst
333 -> [Type] -- Target to match against
336 type OneSidedMatch = Bool -- Are optimisations that are only valid for
337 -- one sided matches allowed?
339 lookup_fam_inst_env -- The worker, local to this module
343 -> TyCon -> [Type] -- What we are looking for
344 -> [FamInstMatch] -- Successful matches
346 -- Precondition: the tycon is saturated (or over-saturated)
348 lookup_fam_inst_env match_fun one_sided (pkg_ie, home_ie) fam tys
349 | not (isFamilyTyCon fam)
352 = ASSERT2( n_tys >= arity, ppr fam <+> ppr tys ) -- Family type applications must be saturated
353 home_matches ++ pkg_matches
355 home_matches = lookup home_ie
356 pkg_matches = lookup pkg_ie
358 -- See Note [Over-saturated matches]
359 arity = tyConArity fam
361 extra_tys = drop arity tys
362 (match_tys, add_extra_tys)
363 | arity > n_tys = (take arity tys, \res_tys -> res_tys ++ extra_tys)
364 | otherwise = (tys, \res_tys -> res_tys)
365 -- The second case is the common one, hence functional representation
368 rough_tcs = roughMatchTcs match_tys
369 all_tvs = all isNothing rough_tcs && one_sided
372 lookup env = case lookupUFM env fam of
373 Nothing -> [] -- No instances for this class
374 Just (FamIE insts has_tv_insts)
375 -- Short cut for common case:
376 -- The thing we are looking up is of form (C a
377 -- b c), and the FamIE has no instances of
378 -- that form, so don't bother to search
379 | all_tvs && not has_tv_insts -> []
380 | otherwise -> find insts
384 find (item@(FamInst { fi_tcs = mb_tcs, fi_tvs = tpl_tvs,
385 fi_tys = tpl_tys, fi_tycon = tycon }) : rest)
386 -- Fast check for no match, uses the "rough match" fields
387 | instanceCantMatch rough_tcs mb_tcs
391 | Just subst <- match_fun item tpl_tvs tpl_tys match_tys
392 = (item, add_extra_tys $ substTyVars subst (tyConTyVars tycon)) : find rest
394 -- No match => try next
399 Note [Over-saturated matches]
400 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
401 It's ok to look up an over-saturated type constructor. E.g.
402 type family F a :: * -> *
403 type instance F (a,b) = Either (a->b)
405 The type instance gives rise to a newtype TyCon (at a higher kind
406 which you can't do in Haskell!):
407 newtype FPair a b = FP (Either (a->b))
409 Then looking up (F (Int,Bool) Char) will return a FamInstMatch
410 (FPair, [Int,Bool,Char])
412 The "extra" type argument [Char] just stays on the end.
417 %************************************************************************
419 Looking up a family instance
421 %************************************************************************
424 topNormaliseType :: FamInstEnvs
426 -> Maybe (Coercion, Type)
428 -- Get rid of *outermost* (or toplevel)
431 -- using appropriate coercions.
432 -- By "outer" we mean that toplevelNormaliseType guarantees to return
433 -- a type that does not have a reducible redex (F ty1 .. tyn) as its
434 -- outermost form. It *can* return something like (Maybe (F ty)), where
435 -- (F ty) is a redex.
437 -- Its a bit like Type.repType, but handles type families too
439 topNormaliseType env ty
442 go :: [TyCon] -> Type -> Maybe (Coercion, Type)
443 go rec_nts ty | Just ty' <- coreView ty -- Expand synonyms
446 go rec_nts (TyConApp tc tys)
447 | isNewTyCon tc -- Expand newtypes
448 = if tc `elem` rec_nts -- See Note [Expanding newtypes] in Type.lhs
450 else let nt_co = mkAxInstCo (newTyConCo tc) tys
451 in add_co nt_co rec_nts' nt_rhs
453 | isFamilyTyCon tc -- Expand open tycons
454 , (co, ty) <- normaliseTcApp env tc tys
455 -- Note that normaliseType fully normalises,
456 -- but it has do to so to be sure that
458 = add_co co rec_nts ty
460 nt_rhs = newTyConInstRhs tc tys
461 rec_nts' | isRecursiveTyCon tc = tc:rec_nts
462 | otherwise = rec_nts
467 = case go rec_nts ty of
468 Nothing -> Just (co, ty)
469 Just (co', ty') -> Just (mkTransCo co co', ty')
473 normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (Coercion, Type)
474 normaliseTcApp env tc tys
476 , tyConArity tc <= length tys -- Unsaturated data families are possible
477 , [(fam_inst, inst_tys)] <- lookupFamInstEnv env tc ntys
478 = let -- A matching family instance exists
479 rep_tc = famInstTyCon fam_inst
480 co_tycon = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
481 co = mkAxInstCo co_tycon inst_tys
482 first_coi = mkTransCo tycon_coi co
483 (rest_coi,nty) = normaliseType env (mkTyConApp rep_tc inst_tys)
484 fix_coi = mkTransCo first_coi rest_coi
488 | otherwise -- No unique matching family instance exists;
489 -- we do not do anything
490 = (tycon_coi, TyConApp tc ntys)
493 -- Normalise the arg types so that they'll match
494 -- when we lookup in in the instance envt
495 (cois, ntys) = mapAndUnzip (normaliseType env) tys
496 tycon_coi = mkTyConAppCo tc cois
499 normaliseType :: FamInstEnvs -- environment with family instances
501 -> (Coercion, Type) -- (coercion,new type), where
502 -- co :: old-type ~ new_type
503 -- Normalise the input type, by eliminating *all* type-function redexes
504 -- Returns with Refl if nothing happens
507 | Just ty' <- coreView ty = normaliseType env ty'
508 normaliseType env (TyConApp tc tys)
509 = normaliseTcApp env tc tys
510 normaliseType env (AppTy ty1 ty2)
511 = let (coi1,nty1) = normaliseType env ty1
512 (coi2,nty2) = normaliseType env ty2
513 in (mkAppCo coi1 coi2, mkAppTy nty1 nty2)
514 normaliseType env (FunTy ty1 ty2)
515 = let (coi1,nty1) = normaliseType env ty1
516 (coi2,nty2) = normaliseType env ty2
517 in (mkFunCo coi1 coi2, mkFunTy nty1 nty2)
518 normaliseType env (ForAllTy tyvar ty1)
519 = let (coi,nty1) = normaliseType env ty1
520 in (mkForAllCo tyvar coi, ForAllTy tyvar nty1)
521 normaliseType _ ty@(TyVarTy _)
523 normaliseType env (PredTy predty)
524 = normalisePred env predty
527 normalisePred :: FamInstEnvs -> PredType -> (Coercion,Type)
528 normalisePred env (ClassP cls tys)
529 = let (cos,tys') = mapAndUnzip (normaliseType env) tys
530 in (mkPredCo $ ClassP cls cos, PredTy $ ClassP cls tys')
531 normalisePred env (IParam ipn ty)
532 = let (co,ty') = normaliseType env ty
533 in (mkPredCo $ (IParam ipn co), PredTy $ IParam ipn ty')
534 normalisePred env (EqPred ty1 ty2)
535 = let (co1,ty1') = normaliseType env ty1
536 (co2,ty2') = normaliseType env ty2
537 in (mkPredCo $ (EqPred co1 co2), PredTy $ EqPred ty1' ty2')