+\end{code}
+Note [Rewriting wanteds with wanteds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We will currently never use a wanted to rewrite any other
+constraint (function @canRewrite@). If a rewriting was possible at all,
+we simply wait until the wanted equality becomes given or derived and
+then use it. This way we avoid rewriting by eventually insoluble wanteds,
+such as in the following situation:
+ w1 : a ~ Int
+ w2 : F a ~ a
+ w3 : F Int ~ G Bool
+where 'a' is a skolem variable. If we rewrite using w1 inside w2 we will
+get the perhaps mystifying error at the end that we could not solve
+(a ~ Int) and (G Bool ~ Int). But there is no point in rewriting with
+a ~ Int as long as it is still wanted.
+
+Notice that on the other hand we often do solve one wanted from another,
+(function @canSolve@) for instance in dictionary interactions, which is
+a reaction that enables sharing both in the solver and in the final evidence
+produced.
+
+\begin{code}
+