Infelicities in pure unifier
During code review on !852 (closed), Simon and I discovered a few infelicities in the pure unifier.
-
Many functions (ex:
unify_ty
,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
S
containing a mappinga :: k
tot
, then it is always the case thatt :: S(k)
. This can be checked. -
There is no
FunTy
case forunify_ty
because it is handled by the tycon case. This should be commented. Specifically, we must make sure to unify theRuntimeRep
s in theFunTy
. This is indeed OK, but it should be made more clear. -
ty_co_match
is rather involved and may not be paying its way. Experiment what happens if it is removed. -
The
ty_co_match
function is missing a case forFunCo
. This is not actually a bug, becausety_co_match
is a "best effort" function. -
The
FunTy
case forty_co_match
incorrectly drops theRuntimeRep
s. -
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 RuntimeRep
s in functions. I'm not going to try to find a test case.