-improveOne :: (Class -> [Instance]) -- Gives instances for given class
- -> Pred_Loc -- Do improvement triggered by this
- -> [Pred_Loc] -- Current constraints
- -> [(Equation,Pred_Loc,Pred_Loc)] -- Derived equalities that must also hold
- -- (NB the above INVARIANT for type Equation)
- -- The Pred_Locs explain which two predicates were
- -- combined (for error messages)
--- Just do improvement triggered by a single, distinguised predicate
-
-improveOne inst_env pred@(IParam ip ty, _) preds
- = [ ((emptyVarSet, [(ty,ty2)]), pred, p2)
- | p2@(IParam ip2 ty2, _) <- preds
- , ip==ip2
- , not (ty `tcEqType` ty2)]
-
-improveOne inst_env pred@(ClassP cls tys, _) preds
+zipAndComputeFDEqs :: (Type -> Type -> Bool) -- Discard this FDEq if true
+ -> [Type]
+ -> [(Int,Type)]
+ -> [FDEq]
+-- Create a list of FDEqs from two lists of types, making sure
+-- that the types are not equal.
+zipAndComputeFDEqs discard (ty1:tys1) ((i2,ty2):tys2)
+ | discard ty1 ty2 = zipAndComputeFDEqs discard tys1 tys2
+ | otherwise = FDEq { fd_pos = i2
+ , fd_ty_left = ty1
+ , fd_ty_right = ty2 } : zipAndComputeFDEqs discard tys1 tys2
+zipAndComputeFDEqs _ _ _ = []
+
+-- Improve a class constraint from another class constraint
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+improveFromAnother :: Pred_Loc -- Template item (usually given, or inert)
+ -> Pred_Loc -- Workitem [that can be improved]
+ -> [Equation]
+-- Post: FDEqs always oriented from the other to the workitem
+-- Equations have empty quantified variables
+improveFromAnother pred1@(ClassP cls1 tys1, _) pred2@(ClassP cls2 tys2, _)
+ | tys1 `lengthAtLeast` 2 && cls1 == cls2
+ = [ FDEqn { fd_qtvs = emptyVarSet, fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2 }
+ | let (cls_tvs, cls_fds) = classTvsFds cls1
+ , fd <- cls_fds
+ , let (ltys1, rs1) = instFD fd cls_tvs tys1
+ (ltys2, irs2) = instFD_WithPos fd cls_tvs tys2
+ , tcEqTypes ltys1 ltys2 -- The LHSs match
+ , let eqs = zipAndComputeFDEqs tcEqType rs1 irs2
+ , not (null eqs) ]
+
+improveFromAnother _ _ = []
+
+
+-- Improve a class constraint from instance declarations
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+pprEquation :: Equation -> SDoc
+pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs })
+ = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),
+ nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (FDEq _ t1 t2) <- pairs])]
+
+improveFromInstEnv :: (InstEnv,InstEnv)
+ -> Pred_Loc
+ -> [Equation] -- Needs to be an Equation because
+ -- of quantified variables
+-- Post: Equations oriented from the template (matching instance) to the workitem!
+improveFromInstEnv _inst_env (pred,_loc)
+ | not (isClassPred pred)
+ = panic "improveFromInstEnv: not a class predicate"
+improveFromInstEnv inst_env pred@(ClassP cls tys, _)