Changes between Version 2 and Version 3 of TypeFunctions/IntegratedSolver

Timestamp:

12/02/08 22:52:08 (4 years ago)

Author:

chak

Comment:

--

TypeFunctions/IntegratedSolver

@@ -21 +21 @@
 reduceList :: RedEnv -> [Inst] -> Avails -> TcM Avails
 }}}
+The `[Inst]` currently includes equalities, but they are ignored.  The `Avails` passed in are free of equalities, but the outgoing ones includes equalities (which come from the `[Inst]`).  Moreover, we have the post-processing of `Avails` by
+{{{
+extractResults :: Avails
+               -> [Inst]                -- Wanted
+               -> TcM (TcDictBinds,     -- Bindings
+                       [Inst],          -- The insts bound by the bindings
+                       [Inst])          -- Irreducible ones
+                        -- Note [Reducing implication constraints]
+}}}
+The irreducible `Inst`s will include all equalities that are passed in as wanteds.
+
+=== Integration ===
+
+Both the equality and class solver have a pre-processing and post-processing phase as well as the main solving phase.  (All three phases are structurally more complicated for equalities.)
+
+==== Pre-processing ====
+
+The two tasks:
+ * Classes: computation of the initial `Avails` value (called `init_state` in `reduceContext`).
+ * Equalities: normalisation of equalities and class constraints.
+I'd suggest to do normalisation first (basically in the same way as it done now) and then build the initial `Avails` from the normalised constraints.
+
+==== Main solver ====
+
+We can probably leave the solving of class constraints much as it is now.  How much the solving of equalities will have to change depends on how we handle `Avails` and whether we keep local equalities in `Avails`, too.  (At the moment, the code in `TcTyFuns` doesn't use the `Avails` data type.)  We need to integrate the loops of `TcSimplify.reduceList`/`TCSimplify.reduce` with those of `TcTyFuns.propagate`.
+
+==== Post-processing ====
+
+The two tasks:
+ * Classes: Extract bindings, bound insts, and irreducible insts from the final `Avails` (i.e., work of `extractResult`).
+ * Equalities: Finalisation phase.
+I'd suggest to extract results first and then finalise on the insts as usual.  That way, the code for both probably doesn't have to change much.  It's also conceptually simpler, I think.
+
+==== Open questions ====
+
+ 0. During solving we maintain the local equalities and local class constraints in rather different structures.  In particular, we don't use `Avails` for equalities.  How do we want to integrate this?
+ 0. Integration of loops of `TcSimplify.reduceList`/`TCSimplify.reduce` with those of `TcTyFuns.propagate`.
 
 === Module structure ===
@@ -31 +68 @@
 === Functional dependencies ===
 
-Currently, `tcImproveOne` generates pairs of types to be unified (on the basis of the FD improvement rules) and does unify them with `unifyType` (via `unifyEqns`).  In the integrated solver, `tcImproveOne` should generate equality constraints instead.  This will get rid of the `extra_eqs` that we currently have in `reduceContext`.
+Currently, `tcImproveOne` generates pairs of types to be unified (on the basis of the FD improvement rules) and does unify them with `unifyType` (via `unifyEqns`).  In the integrated solver, `tcImproveOne` should generate equality constraints (with identity coercions) instead.  This will get rid of the `extra_eqs` that we currently have in `reduceContext`.