-{-- DV: This note will go away!
-
-Note [Touchables and givens]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Touchable variables will never show up in givens which are inputs to
-the solver. However, touchables may show up in givens generated by the flattener.
-For example,
-
- axioms:
- G Int ~ Char
- F Char ~ Int
-
- wanted:
- F (G alpha) ~w Int
-
-canonicalises to
-
- G alpha ~g b
- F b ~w Int
-
-which can be put in the inert set. Suppose we also have a wanted
-
- alpha ~w Int
-
-We cannot rewrite the given G alpha ~g b using the wanted alpha ~w
-Int. Instead, after reacting alpha ~w Int with the whole inert set,
-we observe that we can solve it by unifying alpha with Int, so we mark
-it as solved and put it back in the *work list*. [We also immediately unify
-alpha := Int, without telling anyone, see trySpontaneousSolve function, to
-avoid doing this in the end.]
-
-Later, because it is solved (given, in effect), we can use it to rewrite
-G alpha ~g b to G Int ~g b, which gets put back in the work list. Eventually,
-we will dispatch the remaining wanted constraints using the top-level axioms.
-
-Finally, note that after reacting a wanted equality with the entire inert set
-we may end up with something like
-
- b ~w alpha
-
-which we should flip around to generate the solved constraint alpha ~s b.
-
--}
-
-
-