%
-% (c) The GRASP/AQUA Project, Glasgow University, 1993-1998
+% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
-\section{Class Instance environments}
+\section[InstEnv]{Utilities for typechecking instance declarations}
+
+The bits common to TcInstDcls and TcDeriv.
\begin{code}
module InstEnv (
- InstEnv, emptyInstEnv, addToInstEnv, lookupInstEnv
+ DFunId, InstEnv,
+
+ emptyInstEnv, extendInstEnv,
+ lookupInstEnv, instEnvElts,
+ classInstances, simpleDFunClassTyCon, checkFunDeps
) where
#include "HsVersions.h"
-import Var ( TyVar, Id )
+import Class ( Class, classTvsFds )
+import Var ( Id, isTcTyVar )
import VarSet
-import VarEnv ( TyVarSubstEnv )
-import Type ( Type, tyVarsOfTypes )
-import Unify ( unifyTyListsX, matchTys )
+import VarEnv
+import TcType ( Type, tcTyConAppTyCon, tcIsTyVarTy,
+ tcSplitDFunTy, tyVarsOfTypes, isExistentialTyVar,
+ matchTys, unifyTyListsX
+ )
+import FunDeps ( checkClsFD )
+import TyCon ( TyCon )
import Outputable
-import Maybes
+import UniqFM ( UniqFM, lookupUFM, emptyUFM, addToUFM_C, eltsUFM )
+import Id ( idType )
+import CmdLineOpts
+import Util ( notNull )
+import Maybe ( isJust )
\end{code}
%************************************************************************
%* *
-\section{InstEnv}
+\subsection{The key types}
%* *
%************************************************************************
\begin{code}
-type InstEnv = [(TyVarSet, [Type], Id)]
-\end{code}
+type DFunId = Id
+type InstEnv = UniqFM ClsInstEnv -- Maps Class to instances for that class
+
+data ClsInstEnv
+ = ClsIE [InstEnvElt] -- The instances for a particular class, in any order
+ Bool -- True <=> there is an instance of form C a b c
+ -- If *not* then the common case of looking up
+ -- (C a b c) can fail immediately
+ -- NB: use tcIsTyVarTy: don't look through newtypes!!
+
+type InstEnvElt = (TyVarSet, [Type], DFunId)
+ -- INVARIANTs: see notes below
+
+emptyInstEnv :: InstEnv
+emptyInstEnv = emptyUFM
+
+instEnvElts :: InstEnv -> [InstEnvElt]
+instEnvElts ie = [elt | ClsIE elts _ <- eltsUFM ie, elt <- elts]
+
+classInstances :: (InstEnv,InstEnv) -> Class -> [InstEnvElt]
+classInstances (pkg_ie, home_ie) cls
+ = get home_ie ++ get pkg_ie
+ where
+ get env = case lookupUFM env cls of
+ Just (ClsIE insts _) -> insts
+ Nothing -> []
+
+extendInstEnv :: InstEnv -> DFunId -> InstEnv
+extendInstEnv inst_env dfun_id
+ = addToUFM_C add inst_env clas (ClsIE [ins_item] ins_tyvar)
+ where
+ add (ClsIE cur_insts cur_tyvar) _ = ClsIE (ins_item : cur_insts)
+ (ins_tyvar || cur_tyvar)
+ (ins_tvs, _, clas, ins_tys) = tcSplitDFunTy (idType dfun_id)
+ ins_tv_set = mkVarSet ins_tvs
+ ins_item = (ins_tv_set, ins_tys, dfun_id)
+ ins_tyvar = all tcIsTyVarTy ins_tys
+
+#ifdef UNUSED
+pprInstEnv :: InstEnv -> SDoc
+pprInstEnv env
+ = vcat [ brackets (pprWithCommas ppr (varSetElems tyvars)) <+>
+ brackets (pprWithCommas ppr tys) <+> ppr dfun
+ | ClsIE cls_inst_env _ <- eltsUFM env
+ , (tyvars, tys, dfun) <- cls_inst_env
+ ]
+#endif
+
+simpleDFunClassTyCon :: DFunId -> (Class, TyCon)
+simpleDFunClassTyCon dfun
+ = (clas, tycon)
+ where
+ (_,_,clas,[ty]) = tcSplitDFunTy (idType dfun)
+ tycon = tcTyConAppTyCon ty
+\end{code}
+
+%************************************************************************
+%* *
+\subsection{Instance environments: InstEnv and ClsInstEnv}
+%* *
+%************************************************************************
+
+A @ClsInstEnv@ all the instances of that class. The @Id@ inside a
+ClsInstEnv mapping is the dfun for that instance.
+
+If class C maps to a list containing the item ([a,b], [t1,t2,t3], dfun), then
+
+ forall a b, C t1 t2 t3 can be constructed by dfun
+
+or, to put it another way, we have
+
+ instance (...) => C t1 t2 t3, witnessed by dfun
+
+There is an important consistency constraint in the elements of a ClsInstEnv:
+
+ * [a,b] must be a superset of the free vars of [t1,t2,t3]
+
+ * The dfun must itself be quantified over [a,b]
+
+ * More specific instances come before less specific ones,
+ where they overlap
+
+Thus, the @ClassInstEnv@ for @Eq@ might contain the following entry:
+ [a] ===> dfun_Eq_List :: forall a. Eq a => Eq [a]
+The "a" in the pattern must be one of the forall'd variables in
+the dfun type.
+
+
-In some InstEnvs overlap is prohibited; that is, no pair of templates unify.
+Notes on overlapping instances
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In some ClsInstEnvs, overlap is prohibited; that is, no pair of templates unify.
In others, overlap is permitted, but only in such a way that one can make
a unique choice when looking up. That is, overlap is only permitted if
--Jeff
-\begin{code}
-emptyInstEnv :: InstEnv
-emptyInstEnv = []
+BUT NOTE [Nov 2001]: we must actually *unify* not reverse-match in
+this test. Suppose the instance envt had
+ ..., forall a b. C a a b, ..., forall a b c. C a b c, ...
+(still most specific first)
+Now suppose we are looking for (C x y Int), where x and y are unconstrained.
+ C x y Int doesn't match the template {a,b} C a a b
+but neither does
+ C a a b match the template {x,y} C x y Int
+But still x and y might subsequently be unified so they *do* match.
-isEmptyInstEnv env = null env
-\end{code}
+Simple story: unify, don't match.
-@lookupInstEnv@ looks up in a @InstEnv@, using a one-way match. Since the env is kept
-ordered, the first match must be the only one.
-The thing we are looking up can have an
-arbitrary "flexi" part.
-\begin{code}
-lookupInstEnv :: SDoc -- For error report
- -> InstEnv -- The envt
- -> [Type] -- Key
- -> Maybe (TyVarSubstEnv, Id)
+%************************************************************************
+%* *
+\subsection{Looking up an instance}
+%* *
+%************************************************************************
+
+@lookupInstEnv@ looks up in a @InstEnv@, using a one-way match. Since
+the env is kept ordered, the first match must be the only one. The
+thing we are looking up can have an arbitrary "flexi" part.
-lookupInstEnv doc env key
- = find env
+\begin{code}
+lookupInstEnv :: DynFlags
+ -> (InstEnv -- External package inst-env
+ ,InstEnv) -- Home-package inst-env
+ -> Class -> [Type] -- What we are looking for
+ -> ([(TyVarSubstEnv, InstEnvElt)], -- Successful matches
+ [Id]) -- These don't match but do unify
+ -- The second component of the tuple happens when we look up
+ -- Foo [a]
+ -- in an InstEnv that has entries for
+ -- Foo [Int]
+ -- Foo [b]
+ -- Then which we choose would depend on the way in which 'a'
+ -- is instantiated. So we report that Foo [b] is a match (mapping b->a)
+ -- but Foo [Int] is a unifier. This gives the caller a better chance of
+ -- giving a suitable error messagen
+
+lookupInstEnv dflags (pkg_ie, home_ie) cls tys
+ | not (null all_unifs) = (all_matches, all_unifs) -- This is always an error situation,
+ -- so don't attempt to pune the matches
+ | otherwise = (pruned_matches, [])
+ where
+ all_tvs = all tcIsTyVarTy tys
+ incoherent_ok = dopt Opt_AllowIncoherentInstances dflags
+ overlap_ok = dopt Opt_AllowOverlappingInstances dflags
+ (home_matches, home_unifs) = lookup_inst_env home_ie cls tys all_tvs
+ (pkg_matches, pkg_unifs) = lookup_inst_env pkg_ie cls tys all_tvs
+ all_matches = home_matches ++ pkg_matches
+ all_unifs | incoherent_ok = [] -- Don't worry about these if incoherent is ok!
+ | otherwise = home_unifs ++ pkg_unifs
+
+ pruned_matches | overlap_ok = foldr insert_overlapping [] all_matches
+ | otherwise = all_matches
+
+lookup_inst_env :: InstEnv -- The envt
+ -> Class -> [Type] -- What we are looking for
+ -> Bool -- All the [Type] are tyvars
+ -> ([(TyVarSubstEnv, InstEnvElt)], -- Successful matches
+ [Id]) -- These don't match but do unify
+lookup_inst_env env key_cls key_tys key_all_tvs
+ = case lookupUFM env key_cls of
+ Nothing -> ([],[]) -- No instances for this class
+ Just (ClsIE insts has_tv_insts)
+ | key_all_tvs && not has_tv_insts -> ([],[]) -- Short cut for common case
+ -- The thing we are looking up is of form (C a b c), and
+ -- the ClsIE has no instances of that form, so don't bother to search
+ | otherwise -> find insts [] []
where
- key_vars = tyVarsOfTypes key
- find [] = Nothing
- find ((tpl_tyvars, tpl, val) : rest)
- = case matchTys tpl_tyvars tpl key of
- Nothing ->
- case matchTys key_vars key tpl of
- Nothing -> find rest
- Just (_, _) -> Nothing
+ key_vars = filterVarSet not_existential (tyVarsOfTypes key_tys)
+ not_existential tv = not (isTcTyVar tv && isExistentialTyVar tv)
+ -- The key_tys can contain skolem constants, and we can guarantee that those
+ -- are never going to be instantiated to anything, so we should not involve
+ -- them in the unification test. Example:
+ -- class Foo a where { op :: a -> Int }
+ -- instance Foo a => Foo [a] -- NB overlap
+ -- instance Foo [Int] -- NB overlap
+ -- data T = forall a. Foo a => MkT a
+ -- f :: T -> Int
+ -- f (MkT x) = op [x,x]
+ -- The op [x,x] means we need (Foo [a]). Without the filterVarSet we'd
+ -- complain, saying that the choice of instance depended on the instantiation
+ -- of 'a'; but of course it isn't *going* to be instantiated.
+
+ find [] ms us = (ms, us)
+ find (item@(tpl_tyvars, tpl, dfun_id) : rest) ms us
+ = case matchTys tpl_tyvars tpl key_tys of
Just (subst, leftovers) -> ASSERT( null leftovers )
- Just (subst, val)
+ find rest ((subst,item):ms) us
+ Nothing
+ -- Does not match, so next check whether the things unify
+ -- [see notes about overlapping instances above]
+ -> ASSERT( not (key_vars `intersectsVarSet` tpl_tyvars) )
+ -- Unification will break badly if the variables overlap
+ -- They shouldn't because we allocate separate uniques for them
+ case unifyTyListsX (key_vars `unionVarSet` tpl_tyvars) key_tys tpl of
+ Just _ -> find rest ms (dfun_id:us)
+ Nothing -> find rest ms us
+
+insert_overlapping :: (TyVarSubstEnv, InstEnvElt) -> [(TyVarSubstEnv, InstEnvElt)]
+ -> [(TyVarSubstEnv, InstEnvElt)]
+-- Add a new solution, knocking out strictly less specific ones
+insert_overlapping new_item [] = [new_item]
+insert_overlapping new_item (item:items)
+ | new_beats_old && old_beats_new = item : insert_overlapping new_item items
+ -- Duplicate => keep both for error report
+ | new_beats_old = insert_overlapping new_item items
+ -- Keep new one
+ | old_beats_new = item : items
+ -- Keep old one
+ | otherwise = item : insert_overlapping new_item items
+ -- Keep both
+ where
+ new_beats_old = new_item `beats` item
+ old_beats_new = item `beats` new_item
+
+ (_, (tvs1, tys1, _)) `beats` (_, (tvs2, tys2, _))
+ = isJust (matchTys tvs2 tys2 tys1) -- A beats B if A is more specific than B
+ -- I.e. if B can be instantiated to match A
\end{code}
-@addToInstEnv@ extends a @InstEnv@, checking for overlaps.
-A boolean flag controls overlap reporting.
+%************************************************************************
+%* *
+ Functional dependencies
+%* *
+%************************************************************************
+
+Here is the bad case:
+ class C a b | a->b where ...
+ instance C Int Bool where ...
+ instance C Int Char where ...
+
+The point is that a->b, so Int in the first parameter must uniquely
+determine the second. In general, given the same class decl, and given
+
+ instance C s1 s2 where ...
+ instance C t1 t2 where ...
+
+Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
+
+Matters are a little more complicated if there are free variables in
+the s2/t2.
+
+ class D a b c | a -> b
+ instance D a b => D [(a,a)] [b] Int
+ instance D a b => D [a] [b] Bool
+
+The instance decls don't overlap, because the third parameter keeps
+them separate. But we want to make sure that given any constraint
+ D s1 s2 s3
+if s1 matches
-True => overlap is permitted, but only if one template matches the other;
- not if they unify but neither is
\begin{code}
-addToInstEnv :: Bool -- True <=> overlap permitted
- -> InstEnv -- Envt
- -> [TyVar] -> [Type] -> Id -- New item
- -> MaybeErr InstEnv -- Success...
- ([Type], Id) -- Failure: Offending overlap
-
-addToInstEnv overlap_ok env ins_tvs ins_tys value
- = insert env
+checkFunDeps :: (InstEnv, InstEnv) -> DFunId
+ -> Maybe [DFunId] -- Nothing <=> ok
+ -- Just dfs <=> conflict with dfs
+-- Check wheher adding DFunId would break functional-dependency constraints
+checkFunDeps inst_envs dfun
+ | null bad_fundeps = Nothing
+ | otherwise = Just bad_fundeps
where
- ins_tv_set = mkVarSet ins_tvs
- ins_item = (ins_tv_set, ins_tys, value)
-
- insert [] = returnMaB [ins_item]
- insert env@(cur_item@(tpl_tvs, tpl_tys, val) : rest)
-
- -- FAIL if:
- -- (a) they are the same, or
- -- (b) they unify, and any sort of overlap is prohibited,
- -- (c) they unify but neither is more specific than t'other
- | identical
- || (unifiable && not overlap_ok)
- || (unifiable && not (ins_item_more_specific || cur_item_more_specific))
- = failMaB (tpl_tys, val)
-
- -- New item is an instance of current item, so drop it here
- | ins_item_more_specific = returnMaB (ins_item : env)
-
- -- Otherwise carry on
- | otherwise = insert rest `thenMaB` \ rest' ->
- returnMaB (cur_item : rest')
- where
- unifiable = maybeToBool (unifyTyListsX (ins_tv_set `unionVarSet` tpl_tvs) tpl_tys ins_tys)
- ins_item_more_specific = maybeToBool (matchTys tpl_tvs tpl_tys ins_tys)
- cur_item_more_specific = maybeToBool (matchTys ins_tv_set ins_tys tpl_tys)
- identical = ins_item_more_specific && cur_item_more_specific
+ (ins_tvs, _, clas, ins_tys) = tcSplitDFunTy (idType dfun)
+ ins_tv_set = mkVarSet ins_tvs
+ cls_inst_env = classInstances inst_envs clas
+ bad_fundeps = badFunDeps cls_inst_env clas ins_tv_set ins_tys
+
+badFunDeps :: [InstEnvElt] -> Class
+ -> TyVarSet -> [Type] -- Proposed new instance type
+ -> [DFunId]
+badFunDeps cls_inst_env clas ins_tv_set ins_tys
+ = [ dfun_id | fd <- fds,
+ (tvs, tys, dfun_id) <- cls_inst_env,
+ notNull (checkClsFD (tvs `unionVarSet` ins_tv_set) fd clas_tvs tys ins_tys)
+ ]
+ where
+ (clas_tvs, fds) = classTvsFds clas
\end{code}
-