[project @ 2005-01-05 15:28:39 by simonpj]
[ghc-hetmet.git] / ghc / compiler / types / InstEnv.lhs
index b7a356b..5b41bf9 100644 (file)
@@ -9,7 +9,7 @@ The bits common to TcInstDcls and TcDeriv.
 module InstEnv (
        DFunId, InstEnv,
 
-       emptyInstEnv, extendInstEnv,
+       emptyInstEnv, extendInstEnv, extendInstEnvList,
        lookupInstEnv, instEnvElts,
        classInstances, simpleDFunClassTyCon, checkFunDeps
     ) where
@@ -17,13 +17,13 @@ module InstEnv (
 #include "HsVersions.h"
 
 import Class           ( Class, classTvsFds )
-import Var             ( Id, isTcTyVar )
+import Var             ( Id )
 import VarSet
-import VarEnv
+import Type            ( TvSubst )
 import TcType          ( Type, tcTyConAppTyCon, tcIsTyVarTy,
-                         tcSplitDFunTy, tyVarsOfTypes, isExistentialTyVar,
-                         matchTys, unifyTyListsX
+                         tcSplitDFunTy, tyVarsOfTypes, isExistentialTyVar
                        )
+import Unify           ( tcMatchTys, tcUnifyTys, BindFlag(..) )
 import FunDeps         ( checkClsFD )
 import TyCon           ( TyCon )
 import Outputable
@@ -41,6 +41,17 @@ import Maybe         ( isJust )
 %*                                                                     *
 %************************************************************************
 
+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
+
 \begin{code}
 type DFunId    = Id
 type InstEnv    = UniqFM ClsInstEnv    -- Maps Class to instances for that class
@@ -53,7 +64,20 @@ data ClsInstEnv
                        -- NB: use tcIsTyVarTy: don't look through newtypes!!
                                        
 type InstEnvElt = (TyVarSet, [Type], DFunId)
-       -- INVARIANTs: see notes below
+
+-- INVARIANTS:
+--  * [a,b] must be a superset of the free vars of [t1,t2,t3]
+--
+--  * The dfun must itself be quantified over [a,b]
+--
+--  * The template type variables [a,b] are distinct in each item
+--     of a ClsInstEnv (so we can safely unify them)
+
+-- 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.
+
 
 emptyInstEnv :: InstEnv
 emptyInstEnv = emptyUFM
@@ -69,6 +93,9 @@ classInstances (pkg_ie, home_ie) cls
                Just (ClsIE insts _) -> insts
                Nothing              -> []
 
+extendInstEnvList :: InstEnv -> [DFunId] -> InstEnv
+extendInstEnvList inst_env dfuns = foldl extendInstEnv inst_env dfuns
+
 extendInstEnv :: InstEnv -> DFunId -> InstEnv
 extendInstEnv inst_env dfun_id
   = addToUFM_C add inst_env clas (ClsIE [ins_item] ins_tyvar)
@@ -104,32 +131,6 @@ simpleDFunClassTyCon dfun
 %*                                                                     *
 %************************************************************************
 
-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.
-
-
 
 Notes on overlapping instances
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -270,9 +271,9 @@ thing we are looking up can have an arbitrary "flexi" part.
 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
+             -> Class -> [Type]                -- What we are looking for
+             -> ([(TvSubst, 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
@@ -300,11 +301,11 @@ lookupInstEnv dflags (pkg_ie, home_ie) cls tys
     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 :: InstEnv                     -- The envt
+               -> Class -> [Type]              -- What we are looking for
+               -> Bool                         -- All the [Type] are tyvars
+               -> ([(TvSubst, 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
@@ -314,8 +315,19 @@ lookup_inst_env env key_cls key_tys key_all_tvs
                -- 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)
+    find [] ms us = (ms, us)
+    find (item@(tpl_tyvars, tpl, dfun_id) : rest) ms us
+      = case tcMatchTys tpl_tyvars tpl key_tys of
+         Just subst -> find rest ((subst,item):ms) us
+         Nothing 
+               -- Does not match, so next check whether the things unify
+               -- [see notes about overlapping instances above]
+          -> case tcUnifyTys bind_fn tpl key_tys of
+               Just _   -> find rest ms (dfun_id:us)
+               Nothing  -> find rest ms us
+
+    bind_fn tv | isExistentialTyVar tv = Skolem
+              | otherwise             = BindMe
        -- 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:
@@ -328,24 +340,14 @@ lookup_inst_env env key_cls key_tys key_all_tvs
        -- 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 )
-                                    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)]
+       --
+       -- We do this only for pattern-bound skolems.  For example we reject
+       --      g :: forall a => [a] -> Int
+       --      g x = op x
+       -- on the grounds that the correct instance depends on the instantiation of 'a'
+
+insert_overlapping :: (TvSubst, InstEnvElt) -> [(TvSubst, InstEnvElt)] 
+                  -> [(TvSubst, InstEnvElt)]
 -- Add a new solution, knocking out strictly less specific ones
 insert_overlapping new_item [] = [new_item]
 insert_overlapping new_item (item:items)
@@ -362,7 +364,7 @@ insert_overlapping new_item (item:items)
     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       
+       = isJust (tcMatchTys 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}