Infelicities in pure unifier
During code review on !852 (closed), Simon and I discovered a few infelicities in the pure unifier.
Many functions (ex:
uVar) take a coercion between the kinds of the types being unified. It should be clarified what we are trying to say. To wit:
A. If matching:
kco :: subst(typeKind ty1) ~N typeKind ty2
B. If unifying:
subst(kco) :: subst(ty1) ~N subst(typeKind ty2)
All substitutions throughout GHC are kind preserving. Specifically, if we have a subst
Scontaining a mapping
a :: kto
t, then it is always the case that
t :: S(k). This can be checked.
There is no
unify_tybecause it is handled by the tycon case. This should be commented. Specifically, we must make sure to unify the
RuntimeReps in the
FunTy. This is indeed OK, but it should be made more clear.
ty_co_matchis rather involved and may not be paying its way. Experiment what happens if it is removed.
ty_co_matchfunction is missing a case for
FunCo. This is not actually a bug, because
ty_co_matchis a "best effort" function.
ty_co_matchincorrectly drops the
We do not unify the kinds of type variables because the relationship between the kinds is passed in. See point (1).
We appear to be making fix-points of substitutions even when doing one-way matching. As originally reported in #16512 (comment 221617).
The only real bug here is (6), but it can only happen when performing coercion optimization on programs involving type families that twiddle
RuntimeReps in functions. I'm not going to try to find a test case.