[project @ 2001-06-25 08:01:16 by simonpj]
authorsimonpj <unknown>
Mon, 25 Jun 2001 08:01:16 +0000 (08:01 +0000)
committersimonpj <unknown>
Mon, 25 Jun 2001 08:01:16 +0000 (08:01 +0000)
----------------------------------
Fix a predicate-simplification bug
----------------------------------

Fixes a bug pointed out by Marcin

    data R = R {f :: Int}
    foo:: (?x :: Int) => R -> R
    foo r = r {f = ?x}

    Test.hs:4:
Could not deduce `?x :: Int' from the context ()
arising from use of implicit parameter `?x' at Test.hs:4
In the record update: r {f = ?x}
In the definition of `foo': r {f = ?x}

The predicate simplifier was declining to 'inherit' an
implicit parameter.  This is right for a let-binding, but
wrong for an expression binding.  For example, a simple
expression type signature:

(?x + 1) :: Int

This was rejected because the ?x constraint could not be
floated out -- but that's wrong for expressions.

ghc/compiler/typecheck/TcSimplify.lhs

index 1cb0ca4..33a5c6a 100644 (file)
@@ -7,8 +7,8 @@
 
 \begin{code}
 module TcSimplify (
-       tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyCheck,
-       tcSimplifyRestricted,
+       tcSimplifyInfer, tcSimplifyInferCheck, 
+       tcSimplifyCheck, tcSimplifyRestricted,
        tcSimplifyToDicts, tcSimplifyIPs, tcSimplifyTop, 
 
        tcSimplifyThetas, tcSimplifyCheckThetas,
@@ -38,20 +38,17 @@ import Inst         ( lookupInst, lookupSimpleInst, LookupInstResult(..),
 import TcEnv           ( tcGetGlobalTyVars, tcGetInstEnv )
 import InstEnv         ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
 
-import TcType          ( zonkTcTyVarsAndFV, tcInstTyVars )
-import TcUnify         ( unifyTauTy )
+import TcMType         ( zonkTcTyVarsAndFV, tcInstTyVars, unifyTauTy )
+import TcType          ( ThetaType, PredType, mkClassPred, isOverloadedTy,
+                         mkTyVarTy, tcGetTyVar, isTyVarClassPred,
+                         tyVarsOfPred, getClassPredTys_maybe, isClassPred, isIPPred,
+                         inheritablePred, predHasFDs )
 import Id              ( idType )
 import NameSet         ( mkNameSet )
 import Class           ( classBigSig )
 import FunDeps         ( oclose, grow, improve )
 import PrelInfo                ( isNumericClass, isCreturnableClass, isCcallishClass )
 
-import Type            ( ThetaType, PredType, mkClassPred,
-                         mkTyVarTy, getTyVar, isTyVarClassPred,
-                         splitSigmaTy, tyVarsOfPred,
-                         getClassPredTys_maybe, isClassPred, isIPPred,
-                         inheritablePred, predHasFDs
-                       )
 import Subst           ( mkTopTyVarSubst, substTheta, substTy )
 import TysWiredIn      ( unitTy )
 import VarSet
@@ -325,7 +322,21 @@ having to be passed at each call site.  But of course, the WHOLE
 IDEA is that ?y should be passed at each call site (that's what
 dynamic binding means) so we'd better infer the second.
 
-BOTTOM LINE: you *must* quantify over implicit parameters.
+BOTTOM LINE: you *must* quantify over implicit parameters. See
+isFreeAndInheritable.
+
+BUT WATCH OUT: for *expressions*, this isn't right.  Consider:
+
+       (?x + 1) :: Int
+
+This is perfectly reasonable.  We do not want to insist on
+
+       (?x + 1) :: (?x::Int => Int)
+
+That would be silly.  Here, the definition site *is* the occurrence site,
+so the above strictures don't apply.  Hence the difference between
+tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
+and tcSimplifyCheckBind (which does not).
 
 
 Question 2: type signatures
@@ -488,7 +499,7 @@ again.
 \begin{code}
 tcSimplifyInfer
        :: SDoc 
-       -> [TcTyVar]            -- fv(T); type vars 
+       -> TcTyVarSet           -- fv(T); type vars 
        -> LIE                  -- Wanted
        -> TcM ([TcTyVar],      -- Tyvars to quantify (zonked)
                LIE,            -- Free
@@ -499,7 +510,8 @@ tcSimplifyInfer
 
 \begin{code}
 tcSimplifyInfer doc tau_tvs wanted_lie
-  = inferLoop doc tau_tvs (lieToList wanted_lie)       `thenTc` \ (qtvs, frees, binds, irreds) ->
+  = inferLoop doc (varSetElems tau_tvs) 
+             (lieToList wanted_lie)    `thenTc` \ (qtvs, frees, binds, irreds) ->
 
        -- Check for non-generalisable insts
     mapTc_ addCantGenErr (filter (not . instCanBeGeneralised) irreds)  `thenTc_`
@@ -566,7 +578,8 @@ isFreeAndInheritable qtvs inst
   && all inheritablePred (predsOfInst inst)            -- And no implicit parameter involved
                                                        -- (see "Notes on implicit parameters")
 
-isFree qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
+isFree qtvs inst 
+  = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
 \end{code}
 
 
@@ -588,36 +601,90 @@ tcSimplifyCheck
         -> TcM (LIE,           -- Free
                 TcDictBinds)   -- Bindings
 
+-- tcSimplifyCheck is used when checking exprssion type signatures, 
+-- class decls, instance decls etc.
+-- Note that we psss isFree (not isFreeAndInheritable) to tcSimplCheck
+-- It's important that we can float out non-inheritable predicates
+-- Example:            (?x :: Int) is ok!
 tcSimplifyCheck doc qtvs givens wanted_lie
-  = checkLoop doc qtvs givens (lieToList wanted_lie)   `thenTc` \ (frees, binds, irreds) ->
+  = tcSimplCheck doc isFree get_qtvs
+                givens wanted_lie      `thenTc` \ (qtvs', frees, binds) ->
+    returnTc (frees, binds)
+  where
+    get_qtvs = zonkTcTyVarsAndFV qtvs
+
+
+-- tcSimplifyInferCheck is used when we know the constraints we are to simplify
+-- against, but we don't know the type variables over which we are going to quantify.
+-- This happens when we have a type signature for a mutually recursive group
+tcSimplifyInferCheck
+        :: SDoc 
+        -> TcTyVarSet          -- fv(T)
+        -> [Inst]              -- Given
+        -> LIE                 -- Wanted
+        -> TcM ([TcTyVar],     -- Variables over which to quantify
+                LIE,           -- Free
+                TcDictBinds)   -- Bindings
+
+tcSimplifyInferCheck doc tau_tvs givens wanted_lie
+  = tcSimplCheck doc isFreeAndInheritable get_qtvs givens wanted_lie
+  where
+       -- Figure out which type variables to quantify over
+       -- You might think it should just be the signature tyvars,
+       -- but in bizarre cases you can get extra ones
+       --      f :: forall a. Num a => a -> a
+       --      f x = fst (g (x, head [])) + 1
+       --      g a b = (b,a)
+       -- Here we infer g :: forall a b. a -> b -> (b,a)
+       -- We don't want g to be monomorphic in b just because
+       -- f isn't quantified over b.
+    all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
+
+    get_qtvs = zonkTcTyVarsAndFV all_tvs       `thenNF_Tc` \ all_tvs' ->
+              tcGetGlobalTyVars                `thenNF_Tc` \ gbl_tvs ->
+              let
+                 qtvs = all_tvs' `minusVarSet` gbl_tvs
+                       -- We could close gbl_tvs, but its not necessary for
+                       -- soundness, and it'll only affect which tyvars, not which 
+                       -- dictionaries, we quantify over
+              in
+              returnNF_Tc qtvs
+\end{code}
+
+Here is the workhorse function for all three wrappers.
+
+\begin{code}            
+tcSimplCheck doc is_free get_qtvs givens wanted_lie
+  = check_loop givens (lieToList wanted_lie)   `thenTc` \ (qtvs, frees, binds, irreds) ->
 
        -- Complain about any irreducible ones
     complainCheck doc givens irreds            `thenNF_Tc_`
 
        -- Done
-    returnTc (mkLIE frees, binds)
-
-checkLoop doc qtvs givens wanteds
-  =            -- Step 1
-    zonkTcTyVarsAndFV qtvs             `thenNF_Tc` \ qtvs' ->
-    mapNF_Tc zonkInst givens           `thenNF_Tc` \ givens' ->
-    mapNF_Tc zonkInst wanteds          `thenNF_Tc` \ wanteds' ->
+    returnTc (qtvs, mkLIE frees, binds)
 
-               -- Step 2
-    let
-       -- When checking against a given signature we always reduce
-       -- until we find a match against something given, or can't reduce
-       try_me inst | isFreeAndInheritable qtvs' inst = Free
-                   | otherwise                       = ReduceMe 
-    in
-    reduceContext doc try_me givens' wanteds'  `thenTc` \ (no_improvement, frees, binds, irreds) ->
-       
-               -- Step 3
-    if no_improvement then
-       returnTc (frees, binds, irreds)
-    else
-       checkLoop doc qtvs givens' (irreds ++ frees)    `thenTc` \ (frees1, binds1, irreds1) ->
-       returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
+  where
+    check_loop givens wanteds
+      =                -- Step 1
+       mapNF_Tc zonkInst givens        `thenNF_Tc` \ givens' ->
+       mapNF_Tc zonkInst wanteds       `thenNF_Tc` \ wanteds' ->
+       get_qtvs                        `thenNF_Tc` \ qtvs' ->   
+    
+                   -- Step 2
+       let
+           -- When checking against a given signature we always reduce
+           -- until we find a match against something given, or can't reduce
+           try_me inst | is_free qtvs' inst = Free
+                       | otherwise          = ReduceMe 
+       in
+       reduceContext doc try_me givens' wanteds'       `thenTc` \ (no_improvement, frees, binds, irreds) ->
+           
+                   -- Step 3
+       if no_improvement then
+           returnTc (varSetElems qtvs', frees, binds, irreds)
+       else
+           check_loop givens' (irreds ++ frees)        `thenTc` \ (qtvs', frees1, binds1, irreds1) ->
+           returnTc (qtvs', frees1, binds `AndMonoBinds` binds1, irreds1)
 
 complainCheck doc givens irreds
   = mapNF_Tc zonkInst given_dicts                      `thenNF_Tc` \ givens' ->
@@ -638,8 +705,9 @@ complainCheck doc givens irreds
 
 \begin{code}
 tcSimplifyRestricted   -- Used for restricted binding groups
+                       -- i.e. ones subject to the monomorphism restriction
        :: SDoc 
-       -> [TcTyVar]            -- Free in the type of the RHSs
+       -> TcTyVarSet           -- Free in the type of the RHSs
        -> LIE                  -- Free in the RHSs
        -> TcM ([TcTyVar],      -- Tyvars to quantify (zonked)
                LIE,            -- Free
@@ -660,8 +728,8 @@ tcSimplifyRestricted doc tau_tvs wanted_lie
     in
 
        -- Next, figure out the tyvars we will quantify over
-    zonkTcTyVarsAndFV tau_tvs          `thenNF_Tc` \ tau_tvs' ->
-    tcGetGlobalTyVars                  `thenNF_Tc` \ gbl_tvs ->
+    zonkTcTyVarsAndFV (varSetElems tau_tvs)    `thenNF_Tc` \ tau_tvs' ->
+    tcGetGlobalTyVars                          `thenNF_Tc` \ gbl_tvs ->
     let
        qtvs = (tau_tvs' `minusVarSet` oclose (predsOfInsts dicts) gbl_tvs)
                         `minusVarSet` constrained_tvs
@@ -693,75 +761,6 @@ tcSimplifyRestricted doc tau_tvs wanted_lie
 
 %************************************************************************
 %*                                                                     *
-\subsection{tcSimplifyAndCheck}
-%*                                                                     *
-%************************************************************************
-
-@tcSimplifyInferCheck@ is used when we know the constraints we are to simplify
-against, but we don't know the type variables over which we are going to quantify.
-This happens when we have a type signature for a mutually recursive
-group.
-
-\begin{code}
-tcSimplifyInferCheck
-        :: SDoc 
-        -> [TcTyVar]           -- fv(T)
-        -> [Inst]              -- Given
-        -> LIE                 -- Wanted
-        -> TcM ([TcTyVar],     -- Variables over which to quantify
-                LIE,           -- Free
-                TcDictBinds)   -- Bindings
-
-tcSimplifyInferCheck doc tau_tvs givens wanted
-  = inferCheckLoop doc tau_tvs givens (lieToList wanted)       `thenTc` \ (qtvs, frees, binds, irreds) ->
-
-       -- Complain about any irreducible ones
-    complainCheck doc givens irreds            `thenNF_Tc_`
-
-       -- Done
-    returnTc (qtvs, mkLIE frees, binds)
-
-inferCheckLoop doc tau_tvs givens wanteds
-  =    -- Step 1
-    zonkTcTyVarsAndFV tau_tvs          `thenNF_Tc` \ tau_tvs' ->
-    mapNF_Tc zonkInst givens           `thenNF_Tc` \ givens' ->
-    mapNF_Tc zonkInst wanteds          `thenNF_Tc` \ wanteds' ->
-    tcGetGlobalTyVars                  `thenNF_Tc` \ gbl_tvs ->
-
-    let
-       -- Figure out what we are going to generalise over
-       -- You might think it should just be the signature tyvars,
-       -- but in bizarre cases you can get extra ones
-       --      f :: forall a. Num a => a -> a
-       --      f x = fst (g (x, head [])) + 1
-       --      g a b = (b,a)
-       -- Here we infer g :: forall a b. a -> b -> (b,a)
-       -- We don't want g to be monomorphic in b just because
-       -- f isn't quantified over b.
-       qtvs    = (tau_tvs' `unionVarSet` tyVarsOfInsts givens') `minusVarSet` gbl_tvs
-                       -- We could close gbl_tvs, but its not necessary for
-                       -- soundness, and it'll only affect which tyvars, not which 
-                       -- dictionaries, we quantify over
-
-             -- When checking against a given signature we always reduce
-             -- until we find a match against something given, or can't reduce
-       try_me inst | isFreeAndInheritable qtvs inst  = Free
-                   | otherwise                       = ReduceMe 
-    in
-               -- Step 2
-    reduceContext doc try_me givens' wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
-       
-               -- Step 3
-    if no_improvement then
-       returnTc (varSetElems qtvs, frees, binds, irreds)
-    else
-       inferCheckLoop doc tau_tvs givens' (irreds ++ frees)    `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
-       returnTc (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
-\end{code}
-
-
-%************************************************************************
-%*                                                                     *
 \subsection{tcSimplifyToDicts}
 %*                                                                     *
 %************************************************************************
@@ -917,8 +916,7 @@ bindInstsOfLocalFuns init_lie local_ids
     doc                     = text "bindInsts" <+> ppr local_ids
     wanteds         = lieToList init_lie
     overloaded_ids   = filter is_overloaded local_ids
-    is_overloaded id = case splitSigmaTy (idType id) of
-                         (_, theta, _) -> not (null theta)
+    is_overloaded id = isOverloadedTy (idType id)
 
     overloaded_set = mkVarSet overloaded_ids   -- There can occasionally be a lot of them
                                                -- so it's worth building a set, so that 
@@ -1435,7 +1433,7 @@ tcSimplifyTop wanted_lie
     d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
 
 get_tv d   = case getDictClassTys d of
-                  (clas, [ty]) -> getTyVar "tcSimplifyTop" ty
+                  (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
 get_clas d = case getDictClassTys d of
                   (clas, [ty]) -> clas
 \end{code}
@@ -1543,7 +1541,7 @@ To try to minimise the potential for surprises here, the
 defaulting mechanism is turned off in the presence of
 CCallable and CReturnable.
 
-]
+End of aside]
 
 
 %************************************************************************