# Changes between Version 23 and Version 24 of TypeFunctionsSolving

Show
Ignore:
Timestamp:
08/02/08 23:37:05 (5 years ago)
Comment:

--

Unmodified
Removed
Modified
• ## TypeFunctionsSolving

v23 v24
11= Normalising and Solving Type Equalities =
22
3 The following is based on ideas for the new, post-ICFP'08 solving algorithm.  Technical details are in CVS `papers/type-synonym/new-single.tex`.  Most of the code is in the module `TcTyFuns`.
3The following is based on ideas for the new, post-ICFP'08 solving algorithm described in CVS `papers/type-synonym/new-single.tex`.  Most of the code is in the module `TcTyFuns`.
4
5== Terminology ==
6
7 ''Wanted equality''::
8  An equality constraint that we need to derive during type checking.  Failure to derive it leads to rejection of the checked program.
9 ''Local equality'', ''given equality''::
10  An equality constraint that -in a certain scope- may be used to derive wanted equalities.
11 ''Flexible type variable'',  ''unification variable'', ''HM variable''::
12  Type variables that may be '''globally''' instantiated by unification.
13 ''Rigid type variable'', ''skolem type variable''::
14  Type variable that cannot be globally instantiated, but it may be '''locally''' refined by a local equality constraint.
15
16
417
518== Overall algorithm ==
619
720The overall algorithm is as in `new-single.tex`, namely
8  * Normalise all constraints (both locals and wanteds)
9  * Solve the wanteds
10  * Finalise
21 1. normalise all constraints (both locals and wanteds),
22 2. solve the wanteds, and
23 3. finalise.
1124
1225== Normal equalities ==

1932
2033The types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families.  Moreover, in Forms (2) & (3), the left- and right-hand side need to be different, and the left-hand side may not occur in the right-hand side.
21
22 '''SLPJ''': Terminology: I think "flexible type variable" = "unification variable" = "HM variable".
2334
2435'''SLPJ''': I think that you intend a "normal equality" to embody the Orientation Invariant and the Flattening Invariant from new-single.tex.  But they don't line up exactly.  For example, what about `F [x] ~ G x`?  That satisfies both invariants.