Commit 8b7ceece authored by Simon Peyton Jones's avatar Simon Peyton Jones

More aggressive Given/Wanted overlap check

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.
parent 6ca7b847
......@@ -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?
......
......@@ -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
......
{-# 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
......@@ -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, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment