x = y now tries homogeneous equality first

People often assume that the type of x is enough to give the type of y,
but because = is heterogeneous this isn't always the case. So now the
elaborator will assume homogeneous equality is intended, and revert to
heterogeneous when necessary.

Fixes #1386