Remove shadowed IP parameters, when nesting implications.imp-param-class

Assumed implicit parameters in a nested implication "shadow" outer
implicit parameters with the same name.  There are more details
in Note [Shadowing of Implicit Parameters] in module TcSimplify.

2 files changed, 64 insertions, 14 deletions

diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 8fa7fd58cb..adff5ea182 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -24,7 +24,7 @@ import Coercion( mkAxInstRHS )
 
 import Var
 import TcType
-import PrelNames (singIClassName,ipClassName)
+import PrelNames (singIClassName)
 
 import Class
 import TyCon
@@ -275,9 +275,6 @@ Case 1: In Rewriting Equalities (function rewriteEqLHS)
 Case 2: Functional Dependencies 
     Again, we should prefer, if possible, the inert variables on the RHS
 
-Case 3: IP improvement work
-    We must always rewrite so that the inert type is on the right. 
-
 \begin{code}
 spontaneousSolveStage :: SimplifierStage 
 spontaneousSolveStage workItem
@@ -721,13 +718,6 @@ doInteractWithInert
   inertItem@(CDictCan { cc_ev = fl1, cc_class = cls1, cc_tyargs = tys1 })
    workItem@(CDictCan { cc_ev = fl2, cc_class = cls2, cc_tyargs = tys2 })
 
-  -- see Note [Shadowing of Implicit Parameters]
-  | isGiven fl1 && isGiven fl2 &&
-    tyConName (classTyCon cls1) == ipClassName &&
-    tyConName (classTyCon cls2) == ipClassName &&
-    eqType (head tys1) (head tys2) -- The IP class has arity 2, so this should be fine.
-  = irInertConsumed "IP Shadow"
-
   | cls1 == cls2  
   = do { let pty1 = mkClassPred cls1 tys1
              pty2 = mkClassPred cls2 tys2
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 34c40f2a63..c93b3b1fd4 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -22,7 +22,7 @@ import TcSMonad
 import TcInteract 
 import Inst
 import Unify	( niFixTvSubst, niSubstTvSet )
-import Type     ( classifyPredType, PredTree(..) )
+import Type     ( classifyPredType, PredTree(..), isIPPred_maybe )
 import Var
 import Unique
 import VarSet
@@ -42,7 +42,7 @@ import Outputable
 import FastString
 import TrieMap () -- DV: for now
 import DynFlags
-
+import Data.Maybe ( mapMaybe )
 \end{code}
 
 
@@ -965,7 +965,8 @@ solveImplication tcs_untouchables
                  , ic_given  = givens
                  , ic_wanted = wanteds
                  , ic_loc    = loc })
-  = nestImplicTcS ev_binds (untch, tcs_untouchables) $
+  = shadowIPs givens $    -- See Note [Shadowing of Implicit Parameters]
+    nestImplicTcS ev_binds (untch, tcs_untouchables) $
     recoverTcS (return (emptyBag, emptyBag)) $
        -- Recover from nested failures.  Even the top level is
        -- just a bunch of implications, so failing at the first one is bad
@@ -1039,6 +1040,31 @@ floatEqualities skols can_given wantders
                                         inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
           where
             inner_tvs = tvs_under_fsks ty
+
+shadowIPs :: [EvVar] -> TcS a -> TcS a
+shadowIPs gs m
+  | null shadowed = m
+  | otherwise     = do is <- getTcSInerts
+                       doWithInert (purgeShadowed is) m
+  where
+  shadowed  = mapMaybe isIP gs
+
+  isIP g    = do p <- evVarPred_maybe g
+                 (x,_) <- isIPPred_maybe p
+                 return x
+
+  isShadowedCt ct = isShadowedEv (ctEvidence ct)
+  isShadowedEv ev = case isIPPred_maybe (ctEvPred ev) of
+                      Just (x,_) -> x `elem` shadowed
+                      _          -> False
+
+  purgeShadowed is = is { inert_cans = purgeCans (inert_cans is)
+                        , inert_solved = purgeSolved (inert_solved is)
+                        }
+
+  purgeDicts    = snd . partitionCCanMap isShadowedCt
+  purgeCans ics = ics { inert_dicts = purgeDicts (inert_dicts ics) }
+  purgeSolved   = filterSolved (not . isShadowedEv)
 \end{code}
 
 Note [Preparing inert set for implications]
@@ -1241,6 +1267,40 @@ f (x::beta) =
         g2 z = case z of TEx y -> (h [[undefined]], op x [y])
     in (g1 '3', g2 undefined)
 
+
+Note [Shadowing of Implicit Parameters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Consider the following example:
+
+f :: (?x :: Char) => Char
+f = let ?x = 'a' in ?x
+
+The "let ?x = ..." generates an implication constraint of the form:
+
+?x :: Char => ?x :: Char
+
+Furthermore, the signature for `f` also generates an implication
+constraint, so we end up with the following nested implication:
+
+?x :: Char => (?x :: Char => ?x :: Char)
+
+Note that the wanted (?x :: Char) constraint may be solved in
+two incompatible ways:  either by using the parameter from the
+signature, or by using the local definition.  Our intention is
+that the local definition should "shadow" the parameter of the
+signature, and we implement this as follows: when we nest implications,
+we remove any implicit parameters in the outer implication, that
+have the same name as givens of the inner implication.
+
+Here is another variation of the example:
+
+f :: (?x :: Int) => Char
+f = let ?x = 'x' in ?x
+
+This program should also be accepted: the two constraints `?x :: Int`
+and `?x :: Char` never exist in the same context, so they don't get to
+interact to cause failure.
 \begin{code}
 
 solveCTyFunEqs :: Cts -> TcS (TvSubst, Cts)