Commit 50d02935 authored by simonpj@microsoft.com's avatar simonpj@microsoft.com

Use "on the spot" solving for fundeps

When we spot an equality arising from a functional dependency,
we now use that equality (a "wanted") to rewrite the work-item
constraint right away.  This avoids two dangers

 Danger 1: If we send the original constraint on down the pipeline
           it may react with an instance declaration, and in delicate
	   situations (when a Given overlaps with an instance) that
	   may produce new insoluble goals: see Trac #4952

 Danger 2: If we don't rewrite the constraint, it may re-react
           with the same thing later, and produce the same equality
           again --> termination worries.

To achieve this required some refactoring of FunDeps.lhs (nicer
now!).  

This patch also contains a couple of unrelated improvements

* A bad bug in TcSMonad.nestImplicTcS whereby the Tcs tyvars
  of an outer implication were not untouchable inside

* Improved logging machinery for the type constraint solver;
  use -ddump-cs-trace (probably with a wider default line width
  -dppr-cols=200 or something)
parent 53da379c
......@@ -153,6 +153,7 @@ data DynFlag
| Opt_D_dump_rn_stats
| Opt_D_dump_opt_cmm
| Opt_D_dump_simpl_stats
| Opt_D_dump_cs_trace -- Constraint solver in type checker
| Opt_D_dump_tc_trace
| Opt_D_dump_if_trace
| Opt_D_dump_splices
......@@ -1259,6 +1260,7 @@ dynamic_flags = [
, Flag "ddump-worker-wrapper" (setDumpFlag Opt_D_dump_worker_wrapper)
, Flag "ddump-rn-trace" (setDumpFlag Opt_D_dump_rn_trace)
, Flag "ddump-if-trace" (setDumpFlag Opt_D_dump_if_trace)
, Flag "ddump-cs-trace" (setDumpFlag Opt_D_dump_cs_trace)
, Flag "ddump-tc-trace" (setDumpFlag Opt_D_dump_tc_trace)
, Flag "ddump-splices" (setDumpFlag Opt_D_dump_splices)
, Flag "ddump-rn-stats" (setDumpFlag Opt_D_dump_rn_stats)
......
\begin{code}
module TcCanonical(
mkCanonical, mkCanonicals, mkCanonicalFEV, canWanteds, canGivens,
canOccursCheck, canEq
canOccursCheck, canEq,
rewriteWithFunDeps
) where
#include "HsVersions.h"
......@@ -9,7 +10,8 @@ module TcCanonical(
import BasicTypes
import Type
import TcRnTypes
import FunDeps
import qualified TcMType as TcM
import TcType
import TcErrors
import Coercion
......@@ -18,6 +20,7 @@ import TyCon
import TypeRep
import Name
import Var
import VarEnv ( TidyEnv )
import Outputable
import Control.Monad ( unless, when, zipWithM, zipWithM_ )
import MonadUtils
......@@ -28,6 +31,7 @@ import Bag
import HsBinds
import TcSMonad
import FastString
\end{code}
Note [Canonicalisation]
......@@ -991,4 +995,75 @@ a. If this turns out to be impossible, we next try expanding F
itself, and so on.
%************************************************************************
%* *
%* Functional dependencies, instantiation of equations
%* *
%************************************************************************
\begin{code}
rewriteWithFunDeps :: [Equation]
-> [Xi] -> CtFlavor
-> TcS (Maybe ([Xi], [Coercion], CanonicalCts))
rewriteWithFunDeps eqn_pred_locs xis fl
= do { fd_ev_poss <- mapM (instFunDepEqn fl) eqn_pred_locs
; let fd_ev_pos :: [(Int,FlavoredEvVar)]
fd_ev_pos = concat fd_ev_poss
(rewritten_xis, cos) = unzip (rewriteDictParams fd_ev_pos xis)
; fds <- mapM (\(_,fev) -> mkCanonicalFEV fev) fd_ev_pos
; let fd_work = unionManyBags fds
; if isEmptyBag fd_work
then return Nothing
else return (Just (rewritten_xis, cos, fd_work)) }
instFunDepEqn :: CtFlavor -- Precondition: Only Wanted or Derived
-> Equation
-> TcS [(Int, FlavoredEvVar)]
-- Post: Returns the position index as well as the corresponding FunDep equality
instFunDepEqn fl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
, fd_pred1 = d1, fd_pred2 = d2 })
= do { let tvs = varSetElems qtvs
; tvs' <- mapM instFlexiTcS tvs
; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
; mapM (do_one subst) eqs }
where
fl' = case fl of
Given _ -> panic "mkFunDepEqns"
Wanted loc -> Wanted (push_ctx loc)
Derived loc -> Derived (push_ctx loc)
push_ctx loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
do_one subst (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
= do { let sty1 = substTy subst ty1
sty2 = substTy subst ty2
; ev <- newCoVar sty1 sty2
; return (i, mkEvVarX ev fl') }
rewriteDictParams :: [(Int,FlavoredEvVar)] -- A set of coercions : (pos, ty' ~ ty)
-> [Type] -- A sequence of types: tys
-> [(Type,Coercion)] -- Returns : [(ty', co : ty' ~ ty)]
rewriteDictParams param_eqs tys
= zipWith do_one tys [0..]
where
do_one :: Type -> Int -> (Type,Coercion)
do_one ty n = case lookup n param_eqs of
Just wev -> (get_fst_ty wev, mkCoVarCoercion (evVarOf wev))
Nothing -> (ty,ty) -- Identity
get_fst_ty wev = case evVarOfPred wev of
EqPred ty1 _ -> ty1
_ -> panic "rewriteDictParams: non equality fundep"
mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
-> TcM (TidyEnv, SDoc)
mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
= do { zpred1 <- TcM.zonkTcPredType pred1
; zpred2 <- TcM.zonkTcPredType pred2
; let { tpred1 = tidyPred tidy_env zpred1
; tpred2 = tidyPred tidy_env zpred2 }
; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]),
nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
; return (tidy_env, msg) }
\end{code}
\ No newline at end of file
This diff is collapsed.
......@@ -935,10 +935,9 @@ data CtFlavor
-- superclasses.
instance Outputable CtFlavor where
ppr (Given _) = ptext (sLit "[Given]")
ppr (Wanted _) = ptext (sLit "[Wanted]")
ppr (Derived {}) = ptext (sLit "[Derived]")
ppr (Given {}) = ptext (sLit "[G]")
ppr (Wanted {}) = ptext (sLit "[W]")
ppr (Derived {}) = ptext (sLit "[D]")
pprFlavorArising :: CtFlavor -> SDoc
pprFlavorArising (Derived wl ) = pprArisingAt wl
pprFlavorArising (Wanted wl) = pprArisingAt wl
......
......@@ -10,7 +10,6 @@ module TcSMonad (
CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts,
deCanonicalise, mkFrozenError,
makeSolvedByInst,
isWanted, isGiven, isDerived,
isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
......@@ -21,7 +20,8 @@ module TcSMonad (
combineCtLoc, mkGivenFlavor, mkWantedFlavor,
getWantedLoc,
TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality
TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality
traceFireTcS, bumpStepCountTcS,
tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
......@@ -45,7 +45,7 @@ module TcSMonad (
instDFunTypes, -- Instantiation
instDFunConstraints,
newFlexiTcSTy,
newFlexiTcSTy, instFlexiTcS,
compatKind,
......@@ -58,15 +58,11 @@ module TcSMonad (
matchClass, matchFam, MatchInstResult (..),
checkWellStagedDFun,
warnTcS,
pprEq, -- Smaller utils, re-exported from TcM
pprEq -- Smaller utils, re-exported from TcM
-- TODO (DV): these are only really used in the
-- instance matcher in TcSimplify. I am wondering
-- if the whole instance matcher simply belongs
-- here
mkDerivedFunDepEqns -- Instantiation of 'Equations' from FunDeps
) where
#include "HsVersions.h"
......@@ -102,7 +98,6 @@ import FastString
import HsBinds -- for TcEvBinds stuff
import Id
import FunDeps
import TcRnTypes
......@@ -180,16 +175,6 @@ mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl }
compatKind :: Kind -> Kind -> Bool
compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1
makeSolvedByInst :: CanonicalCt -> CanonicalCt
-- Record that a constraint is now solved
-- Wanted -> Given
-- Given, Derived -> no-op
makeSolvedByInst ct
| Wanted loc <- cc_flavor ct
= ct { cc_flavor = Given (setCtLocOrigin loc UnkSkol) }
| otherwise -- Only called on wanteds
= pprPanic "makeSolvedByInst" (ppr ct)
deCanonicalise :: CanonicalCt -> FlavoredEvVar
deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
......@@ -367,7 +352,10 @@ data TcSEnv
tcs_context :: SimplContext,
tcs_untch :: TcsUntouchables
tcs_untch :: TcsUntouchables,
tcs_ic_depth :: Int, -- Implication nesting depth
tcs_count :: IORef Int -- Global step count
}
type TcsUntouchables = (Untouchables,TcTyVarSet)
......@@ -443,8 +431,21 @@ panicTcS doc = pprPanic "TcCanonical" doc
traceTcS :: String -> SDoc -> TcS ()
traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
traceTcS0 :: String -> SDoc -> TcS ()
traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
bumpStepCountTcS :: TcS ()
bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
; n <- TcM.readTcRef ref
; TcM.writeTcRef ref (n+1) }
traceFireTcS :: Int -> SDoc -> TcS ()
-- Dump a rule-firing trace
traceFireTcS depth doc
= TcS $ \env ->
TcM.ifDOptM Opt_D_dump_cs_trace $
do { n <- TcM.readTcRef (tcs_count env)
; let msg = int n
<> text (replicate (tcs_ic_depth env) '>')
<> brackets (int depth) <+> doc
; TcM.dumpTcRn msg }
runTcS :: SimplContext
-> Untouchables -- Untouchables
......@@ -453,10 +454,13 @@ runTcS :: SimplContext
runTcS context untouch tcs
= do { ty_binds_var <- TcM.newTcRef emptyVarEnv
; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
; step_count <- TcM.newTcRef 0
; let env = TcSEnv { tcs_ev_binds = ev_binds_var
, tcs_ty_binds = ty_binds_var
, tcs_context = context
, tcs_untch = (untouch, emptyVarSet) -- No Tcs untouchables yet
, tcs_count = step_count
, tcs_ic_depth = 0
}
-- Run the computation
......@@ -465,6 +469,10 @@ runTcS context untouch tcs
; ty_binds <- TcM.readTcRef ty_binds_var
; mapM_ do_unification (varEnvElts ty_binds)
#ifdef DEBUG
; count <- TcM.readTcRef step_count
; TcM.dumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count)
#endif
-- And return
; ev_binds <- TcM.readTcRef evb_ref
; return (res, evBindMapBinds ev_binds) }
......@@ -472,13 +480,23 @@ runTcS context untouch tcs
do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
nestImplicTcS ref untch (TcS thing_inside)
= TcS $ \ TcSEnv { tcs_ty_binds = ty_binds,
tcs_context = ctxt } ->
nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
= TcS $ \ TcSEnv { tcs_ty_binds = ty_binds
, tcs_untch = (_outer_range, outer_tcs)
, tcs_count = count
, tcs_ic_depth = idepth
, tcs_context = ctxt } ->
let
inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
-- The inner_range should be narrower than the outer one
-- (thus increasing the set of untouchables) but
-- the inner Tcs-untouchables must be unioned with the
-- outer ones!
nest_env = TcSEnv { tcs_ev_binds = ref
, tcs_ty_binds = ty_binds
, tcs_untch = untch
, tcs_untch = inner_untch
, tcs_count = count
, tcs_ic_depth = idepth+1
, tcs_context = ctxtUnderImplic ctxt }
in
thing_inside nest_env
......@@ -785,48 +803,4 @@ matchFam tycon args
-- DV: We never return MatchInstMany, since tcLookupFamInst never returns
-- multiple matches. Check.
}
-- Functional dependencies, instantiation of equations
-------------------------------------------------------
mkDerivedFunDepEqns :: WantedLoc
-> [(Equation, (PredType, SDoc), (PredType, SDoc))]
-> TcS [FlavoredEvVar] -- All Derived
mkDerivedFunDepEqns _ [] = return []
mkDerivedFunDepEqns loc eqns
= do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
; evvars <- mapM to_work_item eqns
; return $ concat evvars }
where
to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [FlavoredEvVar]
to_work_item ((qtvs, pairs), d1, d2)
= do { let tvs = varSetElems qtvs
; tvs' <- mapM instFlexiTcS tvs
; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
loc' = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
flav = Derived loc'
; mapM (do_one subst flav) pairs }
do_one subst flav (ty1, ty2)
= do { let sty1 = substTy subst ty1
sty2 = substTy subst ty2
; ev <- newCoVar sty1 sty2
; return (mkEvVarX ev flav) }
pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
pprEquationDoc (eqn, (p1, _), (p2, _))
= vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
-> TcM (TidyEnv, SDoc)
mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
= do { pred1' <- TcM.zonkTcPredType pred1
; pred2' <- TcM.zonkTcPredType pred2
; let { pred1'' = tidyPred tidy_env pred1'
; pred2'' = tidyPred tidy_env pred2' }
; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
; return (tidy_env, msg) }
\end{code}
......@@ -9,7 +9,8 @@ It's better to read it as: "if we know these, then we're going to know these"
\begin{code}
module FunDeps (
Equation, pprEquation,
FDEq (..),
Equation(..), pprEquation,
oclose, improveFromInstEnv, improveFromAnother,
checkInstCoverage, checkFunDeps,
pprFundeps
......@@ -140,32 +141,67 @@ oclose preds fixed_tvs
%************************************************************************
Each functional dependency with one variable in the RHS is responsible
for generating a single equality. For instance:
class C a b | a -> b
The constraints ([Wanted] C Int Bool) and [Wanted] C Int alpha
FDEq { fd_pos = 1
, fd_ty_left = Bool
, fd_ty_right = alpha }
However notice that a functional dependency may have more than one variable
in the RHS which will create more than one FDEq. Example:
class C a b c | a -> b c
[Wanted] C Int alpha alpha
[Wanted] C Int Bool beta
Will generate:
fd1 = FDEq { fd_pos = 1, fd_ty_left = alpha, fd_ty_right = Bool } and
fd2 = FDEq { fd_pos = 2, fd_ty_left = alpha, fd_ty_right = beta }
We record the paremeter position so that can immediately rewrite a constraint
using the produced FDEqs and remove it from our worklist.
INVARIANT: Corresponding types aren't already equal
That is, there exists at least one non-identity equality in FDEqs.
Assume:
class C a b c | a -> b c
instance C Int x x
And: [Wanted] C Int Bool alpha
We will /match/ the LHS of fundep equations, producing a matching substitution
and create equations for the RHS sides. In our last example we'd have generated:
({x}, [fd1,fd2])
where
fd1 = FDEq 1 Bool x
fd2 = FDEq 2 alpha x
To ``execute'' the equation, make fresh type variable for each tyvar in the set,
instantiate the two types with these fresh variables, and then unify or generate
a new constraint. In the above example we would generate a new unification
variable 'beta' for x and produce the following constraints:
[Wanted] (Bool ~ beta)
[Wanted] (alpha ~ beta)
Notice the subtle difference between the above class declaration and:
class C a b c | a -> b, a -> c
where we would generate:
({x},[fd1]),({x},[fd2])
This means that the template variable would be instantiated to different
unification variables when producing the FD constraints.
Finally, the position parameters will help us rewrite the wanted constraint ``on the spot''
\begin{code}
type Equation = (TyVarSet, [(Type, Type)])
-- These pairs of types should be equal, for some
-- substitution of the tyvars in the tyvar set
-- INVARIANT: corresponding types aren't already equal
-- It's important that we have a *list* of pairs of types. Consider
-- class C a b c | a -> b c where ...
-- instance C Int x x where ...
-- Then, given the constraint (C Int Bool v) we should improve v to Bool,
-- via the equation ({x}, [(Bool,x), (v,x)])
-- This would not happen if the class had looked like
-- class C a b c | a -> b, a -> c
-- To "execute" the equation, make fresh type variable for each tyvar in the set,
-- instantiate the two types with these fresh variables, and then unify.
--
-- For example, ({a,b}, (a,Int,b), (Int,z,Bool))
-- We unify z with Int, but since a and b are quantified we do nothing to them
-- We usually act on an equation by instantiating the quantified type varaibles
-- to fresh type variables, and then calling the standard unifier.
type Pred_Loc = (PredType, SDoc) -- SDoc says where the Pred comes from
pprEquation :: Equation -> SDoc
pprEquation (qtvs, pairs)
= vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),
nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (t1,t2) <- pairs])]
data Equation
= FDEqn { fd_qtvs :: TyVarSet -- Instantiate these to fresh unification vars
, fd_eqs :: [FDEq] -- and then make these equal
, fd_pred1, fd_pred2 :: Pred_Loc } -- The Equation arose from
-- combining these two constraints
data FDEq = FDEq { fd_pos :: Int -- We use '0' for the first position
, fd_ty_left :: Type
, fd_ty_right :: Type }
\end{code}
Given a bunch of predicates that must hold, such as
......@@ -198,93 +234,97 @@ NOTA BENE:
\begin{code}
type Pred_Loc = (PredType, SDoc) -- SDoc says where the Pred comes from
instFD_WithPos :: FunDep TyVar -> [TyVar] -> [Type] -> ([Type], [(Int,Type)])
-- Returns a FunDep between the types accompanied along with their
-- position (<=0) in the types argument list.
instFD_WithPos (ls,rs) tvs tys
= (map (snd . lookup) ls, map lookup rs)
where
ind_tys = zip [0..] tys
env = zipVarEnv tvs ind_tys
lookup tv = lookupVarEnv_NF env tv
improveFromInstEnv :: (Class -> [Instance])
-> Pred_Loc
-> [(Equation,Pred_Loc,Pred_Loc)]
-- Improvement from top-level instances
improveFromInstEnv _inst_env pred
= improveOne _inst_env pred [] -- TODO: Refactor to directly use instance_eqnd?
zipAndComputeFDEqs :: (Type -> Type -> Bool) -- Discard this FDEq if true
-> [Type]
-> [(Int,Type)]
-> [FDEq]
-- Create a list of FDEqs from two lists of types, making sure
-- that the types are not equal.
zipAndComputeFDEqs discard (ty1:tys1) ((i2,ty2):tys2)
| discard ty1 ty2 = zipAndComputeFDEqs discard tys1 tys2
| otherwise = FDEq { fd_pos = i2
, fd_ty_left = ty1
, fd_ty_right = ty2 } : zipAndComputeFDEqs discard tys1 tys2
zipAndComputeFDEqs _ _ _ = []
-- Improve a class constraint from another class constraint
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
improveFromAnother :: Pred_Loc -- Template item (usually given, or inert)
-> Pred_Loc -- Workitem [that can be improved]
-> [Equation]
-- Post: FDEqs always oriented from the other to the workitem
-- Equations have empty quantified variables
improveFromAnother pred1@(ClassP cls1 tys1, _) pred2@(ClassP cls2 tys2, _)
| tys1 `lengthAtLeast` 2 && cls1 == cls2
= [ FDEqn { fd_qtvs = emptyVarSet, fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2 }
| let (cls_tvs, cls_fds) = classTvsFds cls1
, fd <- cls_fds
, let (ltys1, rs1) = instFD fd cls_tvs tys1
(ltys2, irs2) = instFD_WithPos fd cls_tvs tys2
, tcEqTypes ltys1 ltys2 -- The LHSs match
, let eqs = zipAndComputeFDEqs tcEqType rs1 irs2
, not (null eqs) ]
improveFromAnother _ _ = []
-- Improve a class constraint from instance declarations
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
pprEquation :: Equation -> SDoc
pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs })
= vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),
nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (FDEq _ t1 t2) <- pairs])]
improveFromAnother :: Pred_Loc
improveFromInstEnv :: (InstEnv,InstEnv)
-> Pred_Loc
-> [(Equation, Pred_Loc, Pred_Loc)]
-- Improvement from another local (given or wanted) constraint
improveFromAnother pred1 pred2
= improveOne (\_ -> []) pred1 [pred2] -- TODO: Refactor to directly use pairwise_eqns?
improveOne :: (Class -> [Instance]) -- Gives instances for given class
-> Pred_Loc -- Do improvement triggered by this
-> [Pred_Loc] -- Current constraints
-> [(Equation,Pred_Loc,Pred_Loc)] -- Derived equalities that must also hold
-- (NB the above INVARIANT for type Equation)
-- The Pred_Locs explain which two predicates were
-- combined (for error messages)
-- Just do improvement triggered by a single, distinguised predicate
improveOne _inst_env pred@(IParam ip ty, _) preds
= [ ((emptyVarSet, [(ty,ty2)]), pred, p2)
| p2@(IParam ip2 ty2, _) <- preds
, ip==ip2
, not (ty `tcEqType` ty2)]
improveOne inst_env pred@(ClassP cls tys, _) preds
-> [Equation] -- Needs to be an Equation because
-- of quantified variables
-- Post: Equations oriented from the template (matching instance) to the workitem!
improveFromInstEnv _inst_env (pred,_loc)
| not (isClassPred pred)
= panic "improveFromInstEnv: not a class predicate"
improveFromInstEnv inst_env pred@(ClassP cls tys, _)
| tys `lengthAtLeast` 2
= instance_eqns ++ pairwise_eqns
-- NB: we put the instance equations first. This biases the
-- order so that we first improve individual constraints against the
-- instances (which are perhaps in a library and less likely to be
-- wrong; and THEN perform the pairwise checks.
-- The other way round, it's possible for the pairwise check to succeed
-- and cause a subsequent, misleading failure of one of the pair with an
-- instance declaration. See tcfail143.hs for an example
where
(cls_tvs, cls_fds) = classTvsFds cls
instances = inst_env cls
rough_tcs = roughMatchTcs tys
-- NOTE that we iterate over the fds first; they are typically
-- empty, which aborts the rest of the loop.
pairwise_eqns :: [(Equation,Pred_Loc,Pred_Loc)]
pairwise_eqns -- This group comes from pairwise comparison
= [ (eqn, pred, p2)
| fd <- cls_fds
, p2@(ClassP cls2 tys2, _) <- preds
, cls == cls2
, eqn <- checkClsFD emptyVarSet fd cls_tvs tys tys2
]
instance_eqns :: [(Equation,Pred_Loc,Pred_Loc)]
instance_eqns -- This group comes from comparing with instance decls
= [ (eqn, p_inst, pred)
| fd <- cls_fds -- Iterate through the fundeps first,
= [ FDEqn { fd_qtvs = qtvs, fd_eqs = eqs, fd_pred1 = p_inst, fd_pred2=pred }
| fd <- cls_fds -- Iterate through the fundeps first,
-- because there often are none!
, let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
, let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
-- Trim the rough_tcs based on the head of the fundep.
-- Remember that instanceCantMatch treats both argumnents
-- symmetrically, so it's ok to trim the rough_tcs,
-- rather than trimming each inst_tcs in turn
, ispec@(Instance { is_tvs = qtvs, is_tys = tys_inst,
is_tcs = inst_tcs }) <- instances
, not (instanceCantMatch inst_tcs trimmed_tcs)
, eqn <- checkClsFD qtvs fd cls_tvs tys_inst tys
, let p_inst = (mkClassPred cls tys_inst,
sep [ ptext (sLit "arising from the dependency") <+> quotes (pprFunDep fd)
, ptext (sLit "in the instance declaration at")
<+> ppr (getSrcLoc ispec)])
]
improveOne _ _ _
= []
, ispec@(Instance { is_tvs = qtvs, is_tys = tys_inst,
is_tcs = inst_tcs }) <- instances
, not (instanceCantMatch inst_tcs trimmed_tcs)
, let p_inst = (mkClassPred cls tys_inst,
sep [ ptext (sLit "arising from the dependency") <+> quotes (pprFunDep fd)
, ptext (sLit "in the instance declaration at")
<+> ppr (getSrcLoc ispec)])
, (qtvs, eqs) <- checkClsFD qtvs fd cls_tvs tys_inst tys -- NB: orientation
, not (null eqs)
]
where
(cls_tvs, cls_fds) = classTvsFds cls
instances = classInstances inst_env cls
rough_tcs = roughMatchTcs tys
improveFromInstEnv _ _ = []
checkClsFD :: TyVarSet -- Quantified type variables; see note below
-> FunDep TyVar -> [TyVar] -- One functional dependency from the class
-> [Type] -> [Type]
-> [Equation]
-> [(TyVarSet, [FDEq])]
checkClsFD qtvs fd clas_tvs tys1 tys2
-- 'qtvs' are the quantified type variables, the ones which an be instantiated
......@@ -313,52 +353,69 @@ checkClsFD qtvs fd clas_tvs tys1 tys2
length tys1 == length clas_tvs
, ppr tys1 <+> ppr tys2 )
case tcUnifyTys bind_fn ls1 ls2 of
case tcUnifyTys bind_fn ltys1 ltys2 of
Nothing -> []
Just subst | isJust (tcUnifyTys bind_fn rs1' rs2')
-- Don't include any equations that already hold.
Just subst | isJust (tcUnifyTys bind_fn rtys1' rtys2')
-- Don't include any equations that already hold.
-- Reason: then we know if any actual improvement has happened,
-- in which case we need to iterate the solver
-- In making this check we must taking account of the fact that any
-- qtvs that aren't already instantiated can be instantiated to anything
-- In making this check we must taking account of the fact that any
-- qtvs that aren't already instantiated can be instantiated to anything
-- at all
-> []
| otherwise -- Aha! A useful equation
-> [ (qtvs', zip rs1' rs2')]
-- NB: We can't do this 'is-useful-equation' check element-wise
-- because of:
-- class C a b c | a -> b c
-- instance C Int x x
-- [Wanted] C Int alpha Int
-- We would get that x -> alpha (isJust) and x -> Int (isJust)
-- so we would produce no FDs, which is clearly wrong.
-> []
| otherwise
-> [(qtvs', fdeqs)]
-- We could avoid this substTy stuff by producing the eqn
-- (qtvs, ls1++rs1, ls2++rs2)
-- which will re-do the ls1/ls2 unification when the equation is
-- executed. What we're doing instead is recording the partial
-- work of the ls1/ls2 unification leaving a smaller unification problem
where
rs1' = substTys subst rs1
rs2' = substTys subst rs2
where
rtys1' = map (substTy subst) rtys1
irs2' = map (\(i,x) -> (i,substTy subst x)) irs2
rtys2' = map snd irs2'
fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' irs2'
-- Don't discard anything!
-- We could discard equal types but it's an overkill to call
-- tcEqType again, since we know for sure that /at least one/
-- equation in there is useful)
qtvs' = filterVarSet (`notElemTvSubst` subst) qtvs
-- qtvs' are the quantified type variables
-- that have not been substituted out
--
-- Eg. class C a b | a -> b