Add nakedSubstTy and use it in TcHsType.tcInferApps

Authored by simonpj on Mon, Jul 9, 11:29 AM.


Add nakedSubstTy and use it in TcHsType.tcInferApps

This was a tricky one.

During type checking we maintain TcType:

Note [The well-kinded type invariant]

That is, types are well-kinded /without/ zonking.

But in tcInferApps we were destroying that invariant by calling
substTy, which in turn uses smart constructors, which eliminate
apparently-redundant Refl casts.

This is horribly hard to debug beause they really are Refls and
so it "ought" to be OK to discard them. But it isn't, as the
above Note describes in some detail.

Maybe we should review the invariant? But for now I just followed
it, tricky thought it is.

This popped up because (for some reason) when I fixed Trac Trac #15343,
that exposed this bug by making test polykinds/T14174a fail (in
Trac Trac #14174 which indeed has the same origin).

So this patch fixes a long standing and very subtle bug.

One interesting point: I defined nakedSubstTy in a few lines by
using the generic mapType stuff. I note that the "normal"
TyCoRep.substTy does /not/ use mapType. But perhaps it should:
substTy has lots of $! strict applications in it, and they could
all be eliminated just by useing the StrictIdentity monad. And
that'd make it much easier to experiment with switching between
strict and lazy versions.

(cherry picked from commit 5067b205a8abb5a9f98335d3a929f647c88c0aa2)