-type Equation = (TyVarSet, Type,Type) -- These two types should be equal, for some
- -- substitution of the tyvars in the tyvar set
- -- 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, pairs)
+ = vcat [ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),
+ nest 2 (vcat [ ppr t1 <+> ptext SLIT(":=:") <+> ppr t2 | (t1,t2) <- pairs])]