More aggressive Given/Wanted overlap check
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 7 Apr 2015 13:29:10 +0000 (14:29 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 7 Apr 2015 14:10:45 +0000 (15:10 +0100)
This fixes Trac #10195

For some reason we considered untouchability before, but Trac #10195
shows that this is positively worng.

See Note [Instance and Given overlap] in TcInteract.

Looking at the Git log, it seems that this bug was introduced at the
same time that we introduced the Given/Wanted overlap check in the first
place.

compiler/typecheck/TcInteract.hs
compiler/typecheck/TcType.hs
testsuite/tests/typecheck/should_compile/T10195.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/all.T

index ce34d1f..d36bcff 100644 (file)
@@ -1697,10 +1697,8 @@ matchClassInst _ clas [k,t] loc
 
 matchClassInst inerts clas tys loc
    = do { dflags <- getDynFlags
-        ; tclvl <- getTcLevel
         ; traceTcS "matchClassInst" $ vcat [ text "pred =" <+> ppr pred
-                                           , text "inerts=" <+> ppr inerts
-                                           , text "untouchables=" <+> ppr tclvl ]
+                                           , text "inerts=" <+> ppr inerts ]
         ; instEnvs <- getInstEnvs
         ; case lookupInstEnv instEnvs clas tys of
             ([], _, _)               -- Nothing matches
@@ -1710,11 +1708,11 @@ matchClassInst inerts clas tys loc
 
             ([(ispec, inst_tys)], [], _) -- A single match
                 | not (xopt Opt_IncoherentInstances dflags)
-                , given_overlap tclvl
+                , not (isEmptyBag unifiable_givens)
                 -> -- See Note [Instance and Given overlap]
                    do { traceTcS "Delaying instance application" $
-                          vcat [ text "Workitem=" <+> pprType (mkClassPred clas tys)
-                               , text "Relevant given dictionaries=" <+> ppr givens_for_this_clas ]
+                          vcat [ text "Work item=" <+> pprType (mkClassPred clas tys)
+                               , text "Relevant given dictionaries=" <+> ppr unifiable_givens ]
                       ; return NoInstance  }
 
                 | otherwise
@@ -1747,33 +1745,29 @@ matchClassInst inerts clas tys loc
                   dfun_app = EvDFunApp dfun_id tys (map (ctEvTerm . fst) evc_vars)
             ; return $ GenInst new_ev_vars dfun_app }
 
-     givens_for_this_clas :: Cts
-     givens_for_this_clas
-         = filterBag isGivenCt (findDictsByClass (inert_dicts $ inert_cans inerts) clas)
+     unifiable_givens :: Cts
+     unifiable_givens = filterBag matchable $
+                        findDictsByClass (inert_dicts $ inert_cans inerts) clas
 
-     given_overlap :: TcLevel -> Bool
-     given_overlap tclvl = anyBag (matchable tclvl) givens_for_this_clas
-
-     matchable tclvl (CDictCan { cc_class = clas_g, cc_tyargs = sys
-                               , cc_ev = fl })
+     matchable (CDictCan { cc_class = clas_g, cc_tyargs = sys, cc_ev = fl })
        | isGiven fl
-       = ASSERT( clas_g == clas )
-         case tcUnifyTys (\tv -> if isTouchableMetaTyVar tclvl tv &&
-                                    tv `elemVarSet` tyVarsOfTypes tys
-                                 then BindMe else Skolem) tys sys of
-       -- We can't learn anything more about any variable at this point, so the only
-       -- cause of overlap can be by an instantiation of a touchable unification
-       -- variable. Hence we only bind touchable unification variables. In addition,
-       -- we use tcUnifyTys instead of tcMatchTys to rule out cyclic substitutions.
-            Nothing -> False
-            Just _  -> True
+       , Just {} <- tcUnifyTys bind_meta_tv tys sys
+       = ASSERT( clas_g == clas ) True
        | otherwise = False -- No overlap with a solved, already been taken care of
                            -- by the overlap check with the instance environment.
-     matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct)
-
-{-
-Note [Instance and Given overlap]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+     matchable ct = pprPanic "Expecting dictionary!" (ppr ct)
+
+     bind_meta_tv :: TcTyVar -> BindFlag
+     -- Any meta tyvar may be unified later, so we treat it as
+     -- bindable when unifying with givens. That ensures that we
+     -- conservatively assume that a meta tyvar might get unified with
+     -- something that matches the 'given', until demonstrated
+     -- otherwise.
+     bind_meta_tv tv | isMetaTyVar tv = BindMe
+                     | otherwise      = Skolem
+
+{- Note [Instance and Given overlap]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Example, from the OutsideIn(X) paper:
        instance P x => Q [x]
        instance (x ~ y) => R y [x]
@@ -1796,26 +1790,37 @@ The solution is that:
   instance only when there is no Given in the inerts which is
   unifiable to this particular dictionary.
 
-The end effect is that, much as we do for overlapping instances, we delay choosing a
-class instance if there is a possibility of another instance OR a given to match our
-constraint later on. This fixes bugs #4981 and #5002.
+  We treat any meta-tyvar as "unifiable" for this purpose,
+  *including* untouchable ones
+
+The end effect is that, much as we do for overlapping instances, we
+delay choosing a class instance if there is a possibility of another
+instance OR a given to match our constraint later on. This fixes
+Trac #4981 and #5002.
+
+Other notes:
+
+* This is arguably not easy to appear in practice due to our
+  aggressive prioritization of equality solving over other
+  constraints, but it is possible. I've added a test case in
+  typecheck/should-compile/GivenOverlapping.hs
 
-This is arguably not easy to appear in practice due to our aggressive prioritization
-of equality solving over other constraints, but it is possible. I've added a test case
-in typecheck/should-compile/GivenOverlapping.hs
+* Another "live" example is Trac #10195
 
-We ignore the overlap problem if -XIncoherentInstances is in force: see
-Trac #6002 for a worked-out example where this makes a difference.
+* We ignore the overlap problem if -XIncoherentInstances is in force:
+  see Trac #6002 for a worked-out example where this makes a
+  difference.
 
-Moreover notice that our goals here are different than the goals of the top-level
-overlapping checks. There we are interested in validating the following principle:
+* Moreover notice that our goals here are different than the goals of
+  the top-level overlapping checks. There we are interested in
+  validating the following principle:
 
-    If we inline a function f at a site where the same global instance environment
-    is available as the instance environment at the definition site of f then we
-    should get the same behaviour.
+      If we inline a function f at a site where the same global
+      instance environment is available as the instance environment at
+      the definition site of f then we should get the same behaviour.
 
-But for the Given Overlap check our goal is just related to completeness of
-constraint solving.
+  But for the Given Overlap check our goal is just related to completeness of
+  constraint solving.
 -}
 
 -- | Is the constraint for an implicit CallStack parameter?
index cf6836b..42c9af3 100644 (file)
@@ -451,8 +451,8 @@ Note [TcLevel and untouchable type variables]
 Note [Skolem escape prevention]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We only unify touchable unification variables.  Because of
-(MetaTvInv), there can be no occurrences of he variable further out,
-so the unification can't cause the kolems to escape. Example:
+(MetaTvInv), there can be no occurrences of the variable further out,
+so the unification can't cause the skolems to escape. Example:
      data T = forall a. MkT a (a->Int)
      f x (MkT v f) = length [v,x]
 We decide (x::alpha), and generate an implication like
diff --git a/testsuite/tests/typecheck/should_compile/T10195.hs b/testsuite/tests/typecheck/should_compile/T10195.hs
new file mode 100644 (file)
index 0000000..7ec4e9e
--- /dev/null
@@ -0,0 +1,31 @@
+{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, GADTs,
+             ConstraintKinds, DataKinds, KindSignatures,
+             FlexibleInstances #-}
+{-# OPTIONS -fno-warn-redundant-constraints #-}
+
+module T10195 where
+
+import GHC.Exts
+
+data Foo m zp r'q = Foo zp
+data Dict :: Constraint -> * where
+  Dict :: a => Dict a
+
+type family BarFamily a b :: Bool
+class Bar m m'
+instance (BarFamily m m' ~ 'True) => Bar m m'
+
+magic :: (Bar m m') => c m zp -> Foo m zp (c m' zq)
+magic = undefined
+
+getDict :: a -> Dict (Num a)
+getDict _ = undefined
+fromScalar :: r -> c m r
+fromScalar = undefined
+
+foo :: (Bar m m')
+  => c m zp -> Foo m zp (c m' zq) -> Foo m zp (c m' zq)
+foo b (Foo sc) =
+  let scinv = fromScalar sc
+  in case getDict scinv of
+    Dict -> magic $ scinv * b
index f01e720..ab0a3fe 100644 (file)
@@ -447,3 +447,4 @@ test('T10100', normal, compile, [''])
 test('T10156', normal, compile, [''])
 test('T10177', normal, compile, [''])
 test('T10185', expect_broken(10185), compile, [''])
+test('T10195', normal, compile, [''])