-- Preserve type synonyms if possible
-- We can tell if ty' is function-free by
-- whether there are any floated constraints
- ; if isIdentityCoercion co then
- return (ty, ty, emptyCCan)
- ; if isEmptyCCan ccs then
++ ; if isReflCo co then
+ return (ty, mkReflCo ty, emptyCCan)
else
return (xi, co, ccs) }
-- The type function might be *over* saturated
-- in which case the remaining arguments should
-- be dealt with by AppTys
-- fam_ty = mkTyConApp tc xi_args
- fam_co = fam_ty -- identity
- fam_co = mkReflCo fam_ty -- identity
-
- ; (ret_co, rhs_var, ct) <-
- if isGiven fl then
- do { rhs_var <- newFlattenSkolemTy fam_ty
- ; cv <- newGivenCoVar fam_ty rhs_var fam_co
- ; let ct = CFunEqCan { cc_id = cv
- , cc_flavor = fl -- Given
- , cc_fun = tc
- , cc_tyargs = xi_args
- , cc_rhs = rhs_var }
- ; return $ (mkCoVarCo cv, rhs_var, ct) }
- else -- Derived or Wanted: make a new *unification* flatten variable
- do { rhs_var <- newFlexiTcSTy (typeKind fam_ty)
- ; cv <- newCoVar fam_ty rhs_var
- ; let ct = CFunEqCan { cc_id = cv
- , cc_flavor = mkWantedFlavor fl
- -- Always Wanted, not Derived
- , cc_fun = tc
- , cc_tyargs = xi_args
- , cc_rhs = rhs_var }
- ; return $ (mkCoVarCo cv, rhs_var, ct) }
-
++ fam_ty = mkTyConApp tc xi_args
+ ; (ret_co, rhs_var, ct) <-
+ do { is_cached <- lookupFlatCacheMap tc xi_args fl
+ ; case is_cached of
+ Just (rhs_var,ret_co,_fl) -> return (ret_co, rhs_var, emptyCCan)
+ Nothing
+ | isGivenOrSolved fl ->
+ do { rhs_var <- newFlattenSkolemTy fam_ty
- ; cv <- newGivenCoVar fam_ty rhs_var fam_co
++ ; cv <- newGivenCoVar fam_ty rhs_var (mkReflCo fam_ty)
+ ; let ct = CFunEqCan { cc_id = cv
+ , cc_flavor = fl -- Given
+ , cc_fun = tc
+ , cc_tyargs = xi_args
+ , cc_rhs = rhs_var }
- ; let ret_co = mkCoVarCoercion cv
++ ; let ret_co = mkCoVarCo cv
+ ; updateFlatCacheMap tc xi_args rhs_var fl ret_co
+ ; return $ (ret_co, rhs_var, singleCCan ct) }
+ | otherwise ->
+ -- Derived or Wanted: make a new *unification* flatten variable
+ do { rhs_var <- newFlexiTcSTy (typeKind fam_ty)
+ ; cv <- newCoVar fam_ty rhs_var
+ ; let ct = CFunEqCan { cc_id = cv
+ , cc_flavor = mkWantedFlavor fl
+ -- Always Wanted, not Derived
+ , cc_fun = tc
+ , cc_tyargs = xi_args
+ , cc_rhs = rhs_var }
- ; let ret_co = mkCoVarCoercion cv
++ ; let ret_co = mkCoVarCo cv
+ ; updateFlatCacheMap tc xi_args rhs_var fl ret_co
+ ; return $ (ret_co, rhs_var, singleCCan ct) } }
; return ( foldl AppTy rhs_var xi_rest
- , foldl AppTy (mkSymCoercion ret_co
- `mkTransCoercion` mkTyConCoercion tc cos_args) cos_rest
- , foldl mkAppCo
- (mkSymCo ret_co
- `mkTransCo` mkTyConAppCo tc cos_args)
- cos_rest
- , ccs `extendCCans` ct) }
-
++ , foldl AppCo (mkSymCo ret_co
++ `mkTransCo` mkTyConAppCo tc cos_args)
++ cos_rest
+ , ccs `andCCan` ct) }
-
flatten ctxt (PredTy pred)
= do { (pred', co, ccs) <- flattenPred ctxt pred
; return (PredTy pred', co, ccs) }
canClassToWorkList :: CtFlavor -> EvVar -> Class -> [TcType] -> TcS WorkList
canClassToWorkList fl v cn tys
= do { (xis,cos,ccs) <- flattenMany fl tys -- cos :: xis ~ tys
- ; let no_flattening_happened = all isIdentityCoercion cos
- dict_co = mkTyConCoercion (classTyCon cn) cos
- ; let no_flattening_happened = isEmptyCCan ccs
++ ; let no_flattening_happened = all isReflCo cos
+ dict_co = mkTyConAppCo (classTyCon cn) cos
- ; v_new <- if no_flattening_happened then return v
- else if isGiven fl then return v
+ ; v_new <- if no_flattening_happened then return v
+ else if isGivenOrSolved fl then return v
-- The cos are all identities if fl=Given,
-- hence nothing to do
else do { v' <- newDictVar cn xis -- D xis
; when (isWanted fl) $ setDictBind v (EvCast v' dict_co)
- ; when (isGivenOrSolved fl) $ setDictBind v' (EvCast v (mkSymCoercion dict_co))
- ; when (isGiven fl) $ setDictBind v' (EvCast v (mkSymCo dict_co))
++ ; when (isGivenOrSolved fl) $ setDictBind v' (EvCast v (mkSymCo dict_co))
-- NB: No more setting evidence for derived now
; return v' }
do { argv <- newCoVar s1 s2
; resv <- newCoVar t1 t2
; setCoBind cv $
- mkFunCoercion (mkCoVarCoercion argv) (mkCoVarCoercion resv)
+ mkFunCo (mkCoVarCo argv) (mkCoVarCo resv)
; return (argv,resv) }
--
- else if isGiven fl then
+ else if isGivenOrSolved fl then
- let [arg,res] = decomposeCo 2 (mkCoVarCoercion cv)
+ let [arg,res] = decomposeCo 2 (mkCoVarCo cv)
in do { argv <- newGivenCoVar s1 s2 arg
; resv <- newGivenCoVar t1 t2 res
; return (argv,resv) }
<- if isWanted fl then
do { argsv <- zipWithM newCoVar tys1 tys2
; setCoBind cv $
- mkTyConCoercion tc1 (map mkCoVarCoercion argsv)
- ; return argsv }
-
- else if isGivenOrSolved fl then
- let cos = decomposeCo (length tys1) (mkCoVarCoercion cv)
+ mkTyConAppCo tc1 (map mkCoVarCo argsv)
- ; return argsv }
-
- else if isGiven fl then
- let cos = decomposeCo (length tys1) (mkCoVarCo cv)
++ ; return argsv }
++ else if isGivenOrSolved fl then
++ let cos = decomposeCo (length tys1) (mkCoVarCo cv)
in zipWith3M newGivenCoVar tys1 tys2 cos
else -- Derived
| cls1 `re_orient` cls2
= do { cv' <- if isWanted fl
then do { cv' <- newCoVar s2 s1
- ; setCoBind cv $ mkSymCoercion (mkCoVarCoercion cv')
+ ; setCoBind cv $ mkSymCo (mkCoVarCo cv')
; return cv' }
- else if isGiven fl then
+ else if isGivenOrSolved fl then
- newGivenCoVar s2 s1 (mkSymCoercion (mkCoVarCoercion cv))
+ newGivenCoVar s2 s1 (mkSymCo (mkCoVarCo cv))
else -- Derived
newDerivedId (EqPred s2 s1)
; canEqLeafOriented fl cv' cls2 s1 }
; (xi2, co2, ccs2) <- flatten fl s2 -- Flatten entire RHS
-- co2 :: xi2 ~ s2
; let ccs = ccs1 `andCCan` ccs2
- no_flattening_happened = all isIdentityCoercion (co2:cos1)
- no_flattening_happened = isEmptyCCan ccs
- ; cv_new <- if no_flattening_happened then return cv
- else if isGiven fl then return cv
++ no_flattening_happened = all isReflCo (co2:cos1)
+ ; cv_new <- if no_flattening_happened then return cv
+ else if isGivenOrSolved fl then return cv
else if isWanted fl then
do { cv' <- newCoVar (unClassify (FunCls fn xis1)) xi2
-- cv' : F xis ~ xi2
; case mxi2' of {
Nothing -> canEqFailure fl cv ;
Just xi2' ->
- do { let no_flattening_happened = isIdentityCoercion co
- do { let no_flattening_happened = isEmptyCCan ccs2
- ; cv_new <- if no_flattening_happened then return cv
- else if isGiven fl then return cv
++ do { let no_flattening_happened = isReflCo co
+ ; cv_new <- if no_flattening_happened then return cv
+ else if isGivenOrSolved fl then return cv
else if isWanted fl then
do { cv' <- newCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2
- ; setCoBind cv (mkCoVarCoercion cv' `mkTransCoercion` co)
+ ; setCoBind cv (mkCoVarCo cv' `mkTransCo` co)
; return cv' }
else -- Derived
newDerivedId (EqPred (mkTyVarTy tv) xi2')
import TcType
import TypeRep
import Type( isTyVarTy )
+import Unify ( tcMatchTys )
-
import Inst
import InstEnv
-
import TyCon
import Name
import NameEnv
mk_overlap_msg (matches, unifiers)
= ASSERT( not (null matches) )
vcat [ addArising orig (ptext (sLit "Overlapping instances for")
- <+> pprPred pred)
+ <+> pprPredTy pred)
, sep [ptext (sLit "Matching instances") <> colon,
nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])]
+
+ , if not (null overlapping_givens) then
+ sep [ptext (sLit "Matching givens (or their superclasses)") <> colon, nest 2 (vcat overlapping_givens)]
+ else empty
+
+ , if null overlapping_givens && isSingleton matches && null unifiers then
+ -- Intuitively, some given matched the wanted in their flattened or rewritten (from given equalities)
+ -- form but the matcher can't figure that out because the constraints are non-flat and non-rewritten
+ -- so we simply report back the whole given context. Accelerate Smart.hs showed this problem.
+ sep [ptext (sLit "There exists a (perhaps superclass) match") <> colon, nest 2 (vcat (pp_givens givens))]
+ else empty
+
, if not (isSingleton matches)
then -- Two or more matches
empty
]
; setWantedTyBind tv xi
- ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi xi
+ ; let refl_xi = mkReflCo xi
+ ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi refl_xi
- ; when (isWanted wd) (setCoBind cv xi)
+ ; when (isWanted wd) (setCoBind cv refl_xi)
-- We don't want to do this for Derived, that's why we use 'when (isWanted wd)'
-
; return $ SPSolved (CTyEqCan { cc_id = cv_given
- , cc_flavor = mkGivenFlavor wd UnkSkol
+ , cc_flavor = mkSolvedFlavor wd UnkSkol
, cc_tyvar = tv, cc_rhs = xi }) }
\end{code}
doInteractWithInert
inertItem@(CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
- | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2)
+ | cls1 == cls2 && eqTypes tys1 tys2
= solveOneFromTheOther "Cls/Cls" (EvId d1,fl1) workItem
- | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2))
+ | cls1 == cls2 && (not (isGivenOrSolved fl1 && isGivenOrSolved fl2))
= -- See Note [When improvement happens]
do { let pty1 = ClassP cls1 tys1
pty2 = ClassP cls2 tys2
, cc_tyargs = args1, cc_rhs = xi1 })
workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
, cc_tyargs = args2, cc_rhs = xi2 })
- | tc1 == tc2 && and (zipWith tcEqType args1 args2)
++ | tc1 == tc2 && and (zipWith eqType args1 args2)
+ , Just GivenSolved <- isGiven_maybe fl1
+ = mkIRContinue "Funeq/Funeq" workItem DropInert emptyWorkList
- | tc1 == tc2 && and (zipWith tcEqType args1 args2)
++ | tc1 == tc2 && and (zipWith eqType args1 args2)
+ , Just GivenSolved <- isGiven_maybe fl2
+ = mkIRStopK "Funeq/Funeq" emptyWorkList
+
| fl1 `canSolve` fl2 && lhss_match
- = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCoercion cv1,xi1) (cv2,fl2,xi2)
+ = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCo cv1,xi1) (cv2,fl2,xi2)
; mkIRStopK "FunEq/FunEq" cans }
| fl2 `canSolve` fl1 && lhss_match
- = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1)
+ = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1)
; mkIRContinue "FunEq/FunEq" workItem DropInert cans }
where
- lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2)
+ lhss_match = tc1 == tc2 && eqTypes args1 args2
doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
-- RHS of a type function, so that it never
-- appears in an error message
-- See Note [Type synonym families] in TyCon
- coe = mkTyConApp coe_tc rep_tys
- coe = mkAxInstCo coe_tc rep_tys
- ; cv' <- case fl of
- Wanted {} -> do { cv' <- newCoVar rhs_ty xi
- ; setCoBind cv $
- coe `mkTransCo`
- mkCoVarCo cv'
- ; return cv' }
- Given {} -> newGivenCoVar xi rhs_ty $
- mkSymCo (mkCoVarCo cv) `mkTransCo` coe
- Derived {} -> newDerivedId (EqPred xi rhs_ty)
- ; can_cts <- mkCanonical fl cv'
- ; return $ SomeTopInt can_cts Stop }
++ coe = mkAxInstCo coe_tc rep_tys
+ ; case fl of
+ Wanted {} -> do { cv' <- newCoVar rhs_ty xi
- ; setCoBind cv $
- coe `mkTransCoercion` mkCoVarCoercion cv'
++ ; setCoBind cv $ coe `mkTransCo` mkCoVarCo cv'
+ ; can_cts <- mkCanonical fl cv'
+ ; let solved = workItem { cc_flavor = solved_fl }
+ solved_fl = mkSolvedFlavor fl UnkSkol
+ ; if isEmptyWorkList can_cts then
+ return (SomeTopInt can_cts Stop) -- No point in caching
+ else return $
+ SomeTopInt { tir_new_work = can_cts
+ , tir_new_inert = ContinueWith solved }
+ }
+ Given {} -> do { cv' <- newGivenCoVar xi rhs_ty $
- mkSymCoercion (mkCoVarCoercion cv) `mkTransCoercion` coe
++ mkSymCo (mkCoVarCo cv) `mkTransCo` coe
+ ; can_cts <- mkCanonical fl cv'
+ ; return $
+ SomeTopInt { tir_new_work = can_cts
+ , tir_new_inert = Stop }
+ }
+ Derived {} -> do { cv' <- newDerivedId (EqPred xi rhs_ty)
+ ; can_cts <- mkCanonical fl cv'
+ ; return $
+ SomeTopInt { tir_new_work = can_cts
+ , tir_new_inert = Stop }
+ }
+ }
_
-> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
}
= NoInstance
| GenInst [WantedEvVar] EvTerm
-matchClassInst :: Class -> [Type] -> WantedLoc -> TcS LookupInstResult
-matchClassInst clas tys loc
+matchClassInst :: InertSet -> Class -> [Type] -> WantedLoc -> TcS LookupInstResult
+matchClassInst inerts clas tys loc
= do { let pred = mkClassPred clas tys
; mb_result <- matchClass clas tys
+ ; untch <- getUntouchables
; case mb_result of
MatchInstNo -> return NoInstance
- MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
+ MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
-- we learn more about the reagent
- MatchInstSingle (dfun_id, mb_inst_tys) ->
+ MatchInstSingle (_,_)
+ | given_overlap untch ->
+ do { traceTcS "Delaying instance application" $
- vcat [ text "Workitem=" <+> pprPred (ClassP clas tys)
++ vcat [ text "Workitem=" <+> pprPredTy (ClassP clas tys)
+ , text "Silents and their superclasses=" <+> ppr silents_and_their_scs
+ , text "All given dictionaries=" <+> ppr all_given_dicts ]
+ ; return NoInstance -- see Note [Instance and Given overlap]
+ }
+
+ MatchInstSingle (dfun_id, mb_inst_tys) ->
do { checkWellStagedDFun pred dfun_id loc
-- It's possible that not all the tyvars are in
; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }
}
}
+ where given_overlap :: TcsUntouchables -> Bool
+ given_overlap untch
+ = foldlBag (\r d -> r || matchable untch d) False all_given_dicts
+
+ matchable untch (CDictCan { cc_class = clas', cc_tyargs = sys, cc_flavor = fl })
+ | Just GivenOrig <- isGiven_maybe fl
+ , clas' == clas
+ , does_not_originate_in_a_silent clas' sys
+ = case tcUnifyTys (\tv -> if isTouchableMetaTyVar_InRange untch 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
+ | 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)
+
+ does_not_originate_in_a_silent clas sys
+ -- UGLY: See Note [Silent parameters overlapping]
- = null $ filter (tcEqPred (ClassP clas sys)) silents_and_their_scs
++ = null $ filter (eqPred (ClassP clas sys)) silents_and_their_scs
+
+ silents_and_their_scs
+ = foldlBag (\acc rvnt -> case rvnt of
+ CDictCan { cc_id = d, cc_class = c, cc_tyargs = s }
+ | isSilentEvVar d -> (ClassP c s) : (transSuperClasses c s) ++ acc
+ _ -> acc) [] all_given_dicts
+
+ -- TODO:
+ -- When silent parameters will go away we should simply select from
+ -- the given map of the inert set.
+ all_given_dicts = Map.fold unionBags emptyCCan (cts_given $ inert_dicts inerts)
+
\end{code}
+
+Note [Silent parameters overlapping]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+DV 12/05/2011:
+The long-term goal is to completely remove silent superclass
+parameters when checking instance declarations. But until then we must
+make sure that we never prevent the application of an instance
+declaration because of a potential match from a silent parameter --
+after all we are supposed to have solved that silent parameter from
+some instance, anyway! In effect silent parameters behave more like
+Solved than like Given.
+
+A concrete example appears in typecheck/SilentParametersOverlapping.hs
+
+Note [Instance and Given overlap]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Assume that we have an inert set that looks as follows:
+ [Given] D [Int]
+And an instance declaration:
+ instance C a => D [a]
+A new wanted comes along of the form:
+ [Wanted] D [alpha]
+
+One possibility is to apply the instance declaration which will leave us
+with an unsolvable goal (C alpha). However, later on a new constraint may
+arise (for instance due to a functional dependency between two later dictionaries),
+that will add the equality (alpha ~ Int), in which case our ([Wanted] D [alpha])
+will be transformed to [Wanted] D [Int], which could have been discharged by the given.
+
+The solution is that in matchClassInst and eventually in topReact, we get back with
+a matching 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.
+
+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
+
+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.
+
+But for the Given Overlap check our goal is just related to completeness of
+constraint solving.
+
+
+
+
Implication(..),
CtLoc(..), ctLocSpan, ctLocOrigin, setCtLocOrigin,
CtOrigin(..), EqOrigin(..),
- WantedLoc, GivenLoc, pushErrCtxt,
+ WantedLoc, GivenLoc, GivenKind(..), pushErrCtxt,
- SkolemInfo(..),
+ SkolemInfo(..),
- CtFlavor(..), pprFlavorArising, isWanted, isGiven, isDerived,
+ CtFlavor(..), pprFlavorArising, isWanted,
+ isGivenOrSolved, isGiven_maybe,
+ isDerived,
FlavoredEvVar,
-- Pretty printing
tcs_untch :: TcsUntouchables,
- tcs_ic_depth :: Int, -- Implication nesting depth
- tcs_count :: IORef Int -- Global step count
+ tcs_ic_depth :: Int, -- Implication nesting depth
+ tcs_count :: IORef Int, -- Global step count
+
+ tcs_flat_map :: IORef FlatCache
}
+data FlatCache
+ = FlatCache { givenFlatCache :: Map.Map FunEqHead (TcType,Coercion,CtFlavor)
+ -- Invariant: all CtFlavors here satisfy isGiven
+ , wantedFlatCache :: Map.Map FunEqHead (TcType,Coercion,CtFlavor) }
+ -- Invariant: all CtFlavors here satisfy isWanted
+
+emptyFlatCache :: FlatCache
+emptyFlatCache
+ = FlatCache { givenFlatCache = Map.empty, wantedFlatCache = Map.empty }
+
+newtype FunEqHead = FunEqHead (TyCon,[Xi])
+
+instance Eq FunEqHead where
- FunEqHead (tc1,xis1) == FunEqHead (tc2,xis2) = tc1 == tc2 && tcEqTypes xis1 xis2
++ FunEqHead (tc1,xis1) == FunEqHead (tc2,xis2) = tc1 == tc2 && eqTypes xis1 xis2
+
+instance Ord FunEqHead where
+ FunEqHead (tc1,xis1) `compare` FunEqHead (tc2,xis2)
+ = case compare tc1 tc2 of
- EQ -> tcCmpTypes xis1 xis2
++ EQ -> cmpTypes xis1 xis2
+ other -> other
+
type TcsUntouchables = (Untouchables,TcTyVarSet)
-- Like the TcM Untouchables,
-- but records extra TcsTv variables generated during simplification
projects / ghc-hetmet.git / commitdiff