Commit 370765b2 authored by simonpj's avatar simonpj
Browse files

[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
parent ca440e06
......@@ -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.
......
......@@ -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
......
......@@ -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
......
Supports Markdown
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