The "non-local error" problem in Trac #14185 was due to the
interaction of constraints from different function definitions.

This patch makes a start towards fixing it.  It adds
TcUnify.alwaysBuildImplication to unconditionally build an
implication in some cases, to keep the constraints from different
functions separate.

See the new Note [When to build an implication] in TcUnify.

But a lot of error messages change, so for now I have set
   alwaysBuildImplication = False

Result: no operational change at all.  I'll get back to it!