Metavariables in have's type should not leak into body

[Kha]

As a side effect of #4308, the tactic have : $ty := by $tacs* now requires all mvars in ty to be solved before elaborating tacs, which is not the case for other have forms but is the case for e.g. theorem. Everyone seems to agree that have should consistently behave like theorem in this respect, which should also help with parallelism.

Reported on Zulip.