From: simonpj Date: Wed, 18 Aug 2004 09:33:11 +0000 (+0000) Subject: [project @ 2004-08-18 09:33:03 by simonpj] X-Git-Tag: Initial_conversion_from_CVS_complete~1720 X-Git-Url: http://git.megacz.com/?a=commitdiff_plain;ds=sidebyside;h=370765b2f80105d7ca6e6080bab24c76970fdc4e;p=ghc-hetmet.git [project @ 2004-08-18 09:33:03 by simonpj] ------------------------------- Fix a fundep bug ------------------------------- MERGE TO STABLE Big thank-you to Martin Sulzmann for finding this functional dependency bug. The new defn of FunDeps.Equation is: type Equation = (TyVarSet, [(Type, Type)]) Before it was (TyVarSet, Type, Type), so each pair of types was separately quantified (wrong). 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 Test in typecheck/should_compile/tc180 --- diff --git a/ghc/compiler/typecheck/TcSimplify.lhs b/ghc/compiler/typecheck/TcSimplify.lhs index 8dba75c..b7002f8 100644 --- a/ghc/compiler/typecheck/TcSimplify.lhs +++ b/ghc/compiler/typecheck/TcSimplify.lhs @@ -26,7 +26,7 @@ import TcHsSyn ( TcId, TcDictBinds, mkHsApp, mkHsTyApp, mkHsDictApp ) import TcRnMonad import Inst ( lookupInst, LookupInstResult(..), - tyVarsOfInst, fdPredsOfInsts, fdPredsOfInst, newDicts, + tyVarsOfInst, fdPredsOfInsts, newDicts, isDict, isClassDict, isLinearInst, linearInstType, isStdClassTyVarDict, isMethodFor, isMethod, instToId, tyVarsOfInsts, cloneDict, @@ -1532,16 +1532,19 @@ tcImprove :: Avails -> TcM Bool -- False <=> no change tcImprove avails = tcGetInstEnvs `thenM` \ inst_envs -> let - preds = [ (pred, pp_loc) + preds = [ (dictPred inst, pp_loc) | inst <- keysFM avails, - let pp_loc = pprInstLoc (instLoc inst), - pred <- fdPredsOfInst inst + isDict inst, + let pp_loc = pprInstLoc (instLoc inst) ] -- Avails has all the superclasses etc (good) -- It also has all the intermediates of the deduction (good) -- It does not have duplicates (good) -- NB that (?x::t1) and (?x::t2) will be held separately in avails -- so that improve will see them separate + -- + -- Notice that we only look at dicts; LitInsts and Methods will have + -- been squished, so their dicts will be in Avails too eqns = improve get_insts preds get_insts clas = classInstances inst_envs clas in @@ -1552,10 +1555,11 @@ tcImprove avails mappM_ unify eqns `thenM_` returnM False where - unify ((qtvs, t1, t2), doc) + unify ((qtvs, pairs), doc) = addErrCtxt doc $ tcInstTyVars VanillaTv (varSetElems qtvs) `thenM` \ (_, _, tenv) -> - unifyTauTy (substTy tenv t1) (substTy tenv t2) + mapM_ (unif_pr tenv) pairs + unif_pr tenv (ty1,ty2) = unifyTauTy (substTy tenv ty1) (substTy tenv ty2) \end{code} The main context-reduction function is @reduce@. Here's its game plan. diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs index af03b7a..eaade6d 100644 --- a/ghc/compiler/typecheck/TcType.lhs +++ b/ghc/compiler/typecheck/TcType.lhs @@ -79,7 +79,7 @@ module TcType ( --------------------------------- -- Unifier and matcher - unifyTysX, unifyTyListsX, unifyExtendTysX, + unifyTysX, unifyTyListsX, unifyExtendTyListsX, matchTy, matchTys, match, -------------------------------- @@ -966,7 +966,6 @@ isByteArrayLikeTyCon tc = %************************************************************************ Unify types with an explicit substitution and no monad. -Ignore usage annotations. \begin{code} type MySubst @@ -980,13 +979,14 @@ unifyTysX :: TyVarSet -- Template tyvars unifyTysX tmpl_tyvars ty1 ty2 = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv) -unifyExtendTysX :: TyVarSet -- Template tyvars - -> TyVarSubstEnv -- Substitution to start with - -> Type - -> Type - -> Maybe TyVarSubstEnv -- Extended substitution -unifyExtendTysX tmpl_tyvars subst ty1 ty2 - = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst) +unifyExtendTyListsX + :: TyVarSet -- Template tyvars + -> TyVarSubstEnv -- Substitution to start with + -> [Type] + -> [Type] + -> Maybe TyVarSubstEnv -- Extended substitution +unifyExtendTyListsX tmpl_tyvars subst tys1 tys2 + = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, subst) unifyTyListsX :: TyVarSet -> [Type] -> [Type] -> Maybe TyVarSubstEnv diff --git a/ghc/compiler/types/FunDeps.lhs b/ghc/compiler/types/FunDeps.lhs index 743a34c..9102b68 100644 --- a/ghc/compiler/types/FunDeps.lhs +++ b/ghc/compiler/types/FunDeps.lhs @@ -19,7 +19,7 @@ import Class ( Class, FunDep, classTvsFds ) import Subst ( mkSubst, emptyInScopeSet, substTy ) import TcType ( Type, ThetaType, PredType(..), predTyUnique, mkClassPred, tyVarsOfTypes, tyVarsOfPred, - unifyTyListsX, unifyExtendTysX, tcEqType + unifyTyListsX, unifyExtendTyListsX, tcEqType ) import VarSet import VarEnv @@ -147,24 +147,32 @@ grow preds fixed_tvs \begin{code} ---------- -type Equation = (TyVarSet, Type, Type) -- These two types should be equal, for some - -- substitution of the tyvars in the tyvar set - -- 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. - -- - -- INVARIANT: they aren't already equal - -- - +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. pprEquationDoc (eqn, doc) = vcat [pprEquation eqn, nest 2 doc] -pprEquation (qtvs, t1, t2) = ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)) - <+> ppr t1 <+> ptext SLIT(":=:") <+> ppr t2 +pprEquation (qtvs, pairs) + = vcat [ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)), + nest 2 (vcat [ ppr t1 <+> ptext SLIT(":=:") <+> ppr t2 | (t1,t2) <- pairs])] ---------- improve :: InstEnv Id -- Gives instances for given class @@ -221,7 +229,7 @@ checkGroup :: InstEnv Id -> [(PredType,SDoc)] -> [(Equation, SDoc)] checkGroup inst_env (p1@(IParam _ ty, _) : ips) = -- For implicit parameters, all the types must match - [ ((emptyVarSet, ty, ty'), mkEqnMsg p1 p2) + [ ((emptyVarSet, [(ty,ty')]), mkEqnMsg p1 p2) | p2@(IParam _ ty', _) <- ips, not (ty `tcEqType` ty')] checkGroup inst_env clss@((ClassP cls _, _) : _) @@ -296,17 +304,24 @@ checkClsFD qtvs fd clas_tvs tys1 tys2 -- unifyTyListsX will only bind variables in qtvs, so it's OK! = case unifyTyListsX qtvs ls1 ls2 of Nothing -> [] - Just unif -> -- pprTrace "checkFD" (vcat [ppr_fd fd, - -- ppr (varSetElems qtvs) <+> (ppr ls1 $$ ppr ls2), - -- ppr unif]) $ - [ (qtvs', substTy full_unif r1, substTy full_unif r2) - | (r1,r2) <- rs1 `zip` rs2, - not (maybeToBool (unifyExtendTysX qtvs unif r1 r2))] - -- Don't include any equations that already hold - -- taking account of the fact that any qtvs that aren't - -- already instantiated can be instantiated to anything at all - -- NB: qtvs, not qtvs' because unifyExtendTysX only tries to + Just unif | maybeToBool (unifyExtendTyListsX qtvs unif rs1 rs2) + -- 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 + -- at all + -- NB: qtvs, not qtvs' because unifyExtendTyListsX only tries to -- look template tyvars up in the substitution + -> [] + + | otherwise -- Aha! A useful equation + -> [ (qtvs', map (substTy full_unif) rs1 `zip` map (substTy full_unif) rs2)] + -- 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 full_unif = mkSubst emptyInScopeSet unif -- No for-alls in sight; hmm