-type Equation = (Type,Type) -- These two types should be equal
- -- INVARIANT: they aren't already equal
+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
+ --
+
+
+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