import Name ( getSrcLoc )
import Var ( Id, TyVar )
import Class ( Class, FunDep, classTvsFds )
-import Subst ( mkSubst, emptyInScopeSet, substTy )
-import TcType ( Type, ThetaType, SourceType(..), PredType,
- predTyUnique, mkClassPred, tyVarsOfTypes, tyVarsOfPred,
- unifyTyListsX, unifyExtendTysX, tcEqType
- )
-import PprType ( )
+import Unify ( tcUnifyTys, BindFlag(..) )
+import Type ( substTys, notElemTvSubst )
+import TcType ( Type, ThetaType, PredType(..), tcEqType,
+ predTyUnique, mkClassPred, tyVarsOfTypes, tyVarsOfPred )
import VarSet
import VarEnv
import Outputable
import List ( tails )
-import Maybes ( maybeToBool )
+import Maybe ( isJust )
import ListSetOps ( equivClassesByUniq )
\end{code}
\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
type InstEnv a = Class -> [(TyVarSet, [Type], a)]
-- This is a bit clumsy, because InstEnv is really
-- defined in module InstEnv. However, we don't want
--- to define it (and ClsInstEnv) here because InstEnv
+-- to define it here because InstEnv
-- is their home. Nor do we want to make a recursive
-- module group (InstEnv imports stuff from FunDeps).
\end{code}
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 _, _) : _)
--
-- We can instantiate x to t1, and then we want to force
-- (Tree x) [t1/x] :=: t2
-
--- We use 'unify' even though we are often only matching
--- 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
- -- look template tyvars up in the substitution
+--
+-- This function is also used when matching two Insts (rather than an Inst
+-- against an instance decl. In that case, qtvs is empty, and we are doing
+-- an equality check
+--
+-- This function is also used by InstEnv.badFunDeps, which needs to *unify*
+-- For the one-sided matching case, the qtvs are just from the template,
+-- so we get matching
+--
+ = ASSERT2( length tys1 == length tys2 &&
+ length tys1 == length clas_tvs
+ , ppr tys1 <+> ppr tys2 )
+
+ case tcUnifyTys bind_fn ls1 ls2 of
+ Nothing -> []
+ Just subst | isJust (tcUnifyTys bind_fn 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
+ -> []
+
+ | otherwise -- Aha! A useful equation
+ -> [ (qtvs', zip rs1' 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
-
- qtvs' = filterVarSet (\v -> not (v `elemSubstEnv` unif)) qtvs
+ rs1' = substTys subst rs1
+ rs2' = substTys subst rs2
+ qtvs' = filterVarSet (`notElemTvSubst` subst) qtvs
-- qtvs' are the quantified type variables
-- that have not been substituted out
--
-- we generate the equation
-- ({y}, [y], z)
where
+ bind_fn tv | tv `elemVarSet` qtvs = BindMe
+ | otherwise = Skolem
+
(ls1, rs1) = instFD fd clas_tvs tys1
(ls2, rs2) = instFD fd clas_tvs tys2
projects / ghc-hetmet.git / blobdiff