[project @ 2004-08-16 09:53:47 by simonpj]
[ghc-hetmet.git] / ghc / compiler / types / InstEnv.lhs
index d054178..b7a356b 100644 (file)
@@ -7,106 +7,95 @@ The bits common to TcInstDcls and TcDeriv.
 
 \begin{code}
 module InstEnv (
-       InstInfo(..), pprInstInfo,
-       simpleInstInfoTy, simpleInstInfoTyCon, simpleDFunClassTyCon,
+       DFunId, InstEnv,
 
-       -- Instance environment
-       InstEnv, emptyInstEnv, extendInstEnv,
-       lookupInstEnv, InstLookupResult(..),
-       classInstEnv, classDataCon,
-
-       isLocalInst
+       emptyInstEnv, extendInstEnv,
+       lookupInstEnv, instEnvElts,
+       classInstances, simpleDFunClassTyCon, checkFunDeps
     ) where
 
 #include "HsVersions.h"
 
-import RnHsSyn         ( RenamedMonoBinds, RenamedSig )
-
-import HscTypes                ( InstEnv, ClsInstEnv, DFunId )
-import Class           ( Class )
-import Var             ( TyVar, Id )
-import VarSet          ( unionVarSet, mkVarSet )
-import VarEnv          ( TyVarSubstEnv )
-import Maybes          ( MaybeErr(..), returnMaB, failMaB, thenMaB, maybeToBool )
-import Name            ( getSrcLoc )
-import SrcLoc          ( SrcLoc )
-import Type            ( Type, ThetaType, splitTyConApp_maybe, 
-                         splitSigmaTy, splitDictTy,
-                         tyVarsOfTypes )
-import PprType         ( )
-import Class           ( classTyCon )
-import DataCon         ( DataCon )
-import TyCon           ( TyCon, tyConDataCons )
+import Class           ( Class, classTvsFds )
+import Var             ( Id, isTcTyVar )
+import VarSet
+import VarEnv
+import TcType          ( Type, tcTyConAppTyCon, tcIsTyVarTy,
+                         tcSplitDFunTy, tyVarsOfTypes, isExistentialTyVar,
+                         matchTys, unifyTyListsX
+                       )
+import FunDeps         ( checkClsFD )
+import TyCon           ( TyCon )
 import Outputable
-import Unify           ( matchTys, unifyTyListsX )
-import UniqFM          ( lookupWithDefaultUFM, addToUFM, emptyUFM )
+import UniqFM          ( UniqFM, lookupUFM, emptyUFM, addToUFM_C, eltsUFM )
 import Id              ( idType )
-import ErrUtils                ( Message )
 import CmdLineOpts
+import Util             ( notNull )
+import Maybe           ( isJust )
 \end{code}
 
 
-
 %************************************************************************
 %*                                                                     *
-\subsection{The InstInfo type}
+\subsection{The key types}
 %*                                                                     *
 %************************************************************************
 
-The InstInfo type summarises the information in an instance declaration
+\begin{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
 
-    instance c => k (t tvs) where b
+emptyInstEnv :: InstEnv
+emptyInstEnv = emptyUFM
 
-\begin{code}
-data InstInfo
-  = InstInfo {
-      iClass :: Class,         -- Class, k
-      iTyVars :: [TyVar],      -- Type variables, tvs
-      iTys    :: [Type],       -- The types at which the class is being instantiated
-      iTheta  :: ThetaType,    -- inst_decl_theta: the original context, c, from the
-                               --   instance declaration.  It constrains (some of)
-                               --   the TyVars above
-      iLocal  :: Bool,         -- True <=> it's defined in this module
-      iDFunId :: DFunId,               -- The dfun id
-      iBinds  :: RenamedMonoBinds,     -- Bindings, b
-      iLoc    :: SrcLoc,               -- Source location assoc'd with this instance's defn
-      iPrags  :: [RenamedSig]          -- User pragmas recorded for generating specialised instances
-    }
-
-pprInstInfo info = vcat [ptext SLIT("InstInfo:") <+> ppr (idType (iDFunId info)),
-                        nest 4 (ppr (iBinds info))]
-
-simpleInstInfoTy :: InstInfo -> Type
-simpleInstInfoTy (InstInfo {iTys = [ty]}) = ty
-
-simpleInstInfoTyCon :: InstInfo -> TyCon
-  -- Gets the type constructor for a simple instance declaration,
-  -- i.e. one of the form      instance (...) => C (T a b c) where ...
-simpleInstInfoTyCon inst
-   = case splitTyConApp_maybe (simpleInstInfoTy inst) of 
-       Just (tycon, _) -> tycon
-
-isLocalInst :: InstInfo -> Bool
-isLocalInst info = iLocal info
-\end{code}
+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              -> []
 
-A tiny function which doesn't belong anywhere else.
-It makes a nasty mutual-recursion knot if you put it in Class.
+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
 
-\begin{code}
 simpleDFunClassTyCon :: DFunId -> (Class, TyCon)
 simpleDFunClassTyCon dfun
   = (clas, tycon)
   where
-    (_,_,dict_ty) = splitSigmaTy (idType dfun)
-    (clas, [ty])  = splitDictTy  dict_ty
-    tycon        = case splitTyConApp_maybe ty of
-                       Just (tycon,_) -> tycon
-
-classDataCon :: Class -> DataCon
-classDataCon clas = case tyConDataCons (classTyCon clas) of
-                     (dict_constr:no_more) -> ASSERT( null no_more ) dict_constr 
+    (_,_,clas,[ty]) = tcSplitDFunTy (idType dfun)
+    tycon          = tcTyConAppTyCon ty 
 \end{code}                   
 
 %************************************************************************
@@ -115,19 +104,8 @@ classDataCon clas = case tyConDataCons (classTyCon clas) of
 %*                                                                     *
 %************************************************************************
 
-The actual type declarations are in HscTypes.
-
-\begin{code}
-emptyInstEnv :: InstEnv
-emptyInstEnv = emptyUFM
-
-classInstEnv :: InstEnv -> Class -> ClsInstEnv
-classInstEnv env cls = lookupWithDefaultUFM env [] cls
-\end{code}
-
-A @ClsInstEnv@ lives inside a class, and identifies all the instances
-of that class.  The @Id@ inside a ClsInstEnv mapping is the dfun for
-that instance.  
+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
 
@@ -142,6 +120,9 @@ 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]
@@ -262,127 +243,184 @@ exists.
 
 --Jeff
 
+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.
+
+Simple story: unify, don't match.
+
+
+%************************************************************************
+%*                                                                     *
+\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.
 
 \begin{code}
-lookupInstEnv :: InstEnv                       -- The envt
-             -> Class -> [Type]        -- Key
-             -> InstLookupResult
-
-data InstLookupResult 
-  = FoundInst                  -- There is a (template,substitution) pair 
-                               -- that makes the template match the key, 
-                               -- and no template is an instance of the key
-       TyVarSubstEnv Id
-
-  | NoMatch Bool       -- Boolean is true iff there is at least one
-                       -- template that matches the key.
-                       -- (but there are other template(s) that are
-                       --  instances of the key, so we don't report 
-                       --  FoundInst)
-       -- The NoMatch True case happens when we look up
+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 say there is no match, but identify
-       -- it as ambiguous case in the hope of giving a better error msg.
-       -- See the notes above from Jeff Lewis
-
-lookupInstEnv env key_cls key_tys
-  = find (classInstEnv env key_cls)
+       -- 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
-    key_vars = tyVarsOfTypes key_tys
-
-    find [] = NoMatch False
-    find ((tpl_tyvars, tpl, val) : rest)
+    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 = 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
-         Nothing                 ->
-           case matchTys key_vars key_tys tpl of
-             Nothing             -> find rest
-             Just (_, _)         -> NoMatch (any_match rest)
          Just (subst, leftovers) -> ASSERT( null leftovers )
-                                    FoundInst 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
 
-    any_match rest = or [ maybeToBool (matchTys tvs tpl key_tys)
-                       | (tvs,tpl,_) <- rest
-                       ]
+    (_, (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}
 
-@addToClsInstEnv@ extends a @ClsInstEnv@, 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}
-extendInstEnv :: DynFlags -> InstEnv -> [DFunId] -> (InstEnv, [Message])
-  -- Similar, but all we have is the DFuns
-extendInstEnv dflags env infos
-  = go env [] infos
+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
-    go env msgs []          = (env, msgs)
-    go env msgs (dfun:dfuns) = case addToInstEnv dflags env dfun of
-                                   Succeeded new_env -> go new_env msgs dfuns
-                                   Failed dfun'      -> go env (msg:msgs) infos
-                                                    where
-                                                        msg = dupInstErr dfun dfun'
-
-
-dupInstErr dfun1 dfun2
-       -- Overlapping/duplicate instances for given class; msg could be more glamourous
-  = hang (ptext SLIT("Duplicate or overlapping instance declarations:"))
-       2 (ppr_dfun dfun1 $$ ppr_dfun dfun2)
+    (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
-    ppr_dfun dfun = ppr (getSrcLoc dfun) <> colon <+> ppr tau
-                 where
-                   (_,_,tau) = splitSigmaTy (idType dfun)
-
-addToInstEnv :: DynFlags
-             -> InstEnv        -> DFunId
-            -> MaybeErr InstEnv        -- Success...
-                        DFunId         -- Failure: Offending overlap
-
-addToInstEnv dflags inst_env dfun_id
-  = case insert_into (classInstEnv inst_env clas) of
-       Failed stuff      -> Failed stuff
-       Succeeded new_env -> Succeeded (addToUFM inst_env clas new_env)
-       
-  where
-    (ins_tvs, _, dict_ty) = splitSigmaTy (idType dfun_id)
-    (clas, ins_tys)      = splitDictTy dict_ty
-
-    ins_tv_set = mkVarSet ins_tvs
-    ins_item = (ins_tv_set, ins_tys, dfun_id)
-
-    insert_into [] = returnMaB [ins_item]
-    insert_into 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 (dopt Opt_AllowOverlappingInstances dflags))
-      || (unifiable && not (ins_item_more_specific || cur_item_more_specific))
-      =  failMaB 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_into 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
+    (clas_tvs, fds) = classTvsFds clas
 \end{code}
-
-