Use smart constructors to eliminate Refls in zonker
This very small patch should eliminate newly-discovered Refl
s during zonking.
However, it's not as good as it could be: the about-to-be-discarded Refl
is still fully zonked. This could be a problem if we have a coercion hole that contains a Refl big_type
. We zonk the hole to reveal the Refl
, but then we zonk the type before realizing we could discard it. Laziness can't save us, because zonking is monadic. Fixing this would require, I think, propagating information to zonkCoHole
to say whether or not to stop at a Refl
.
Relates to #17223.