Add nakedSubstTy and use it in TcHsType.tcInferApps
Concern Raised5067b205a8ab

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

Description

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.

goldfire raised a concern with this commit.Jul 10 2018, 9:02 AM
goldfire added a subscriber: goldfire.

The tcInferApps stuff looks good, but I think you're missing a step in nakedSubstTy.

/compiler/typecheck/TcType.hs
1407

This isn't quite the invariant. Instead, I think you mean:

INVARIANT: It is legal to call typeKind on every type even /without/ zonking

This statement of the invariant implies your EXCEPTion. And it's the one we actually need.

1493

Nice use of mapType. When I wrote that, I thought only about zonking, but substitution is a natural fit, too.

1501

I think this needs to recur into the hole's kind. Right?

This commit now has outstanding concerns.Jul 10 2018, 9:02 AM

Hmph. I'm not sure. Consider

  • substTyVar does not substitute in the kind of a tyvar occurrence
  • substCoVar does not substitute in the type of a covar occurrence
  • TyCoRep.substCo does not substitute in the type of a CoVarHole (there's even an obscure note to explain why)

So it seems inconsistent to do so here.

Here is a possible claim: based on Trac Trac #14164 comment:12, 13: there is no point in substituting in the kind because doing so is a no-op, if the invariant in Trac #14164 is satisfied.

Do you agree?

I had forgotten about that invariant. I've made a note to myself to document and check it.

Are coercion holes added to in-scope sets? I'm not sure they are consistently. If we build the in-scope set by tracking variables brought into scope as we descend from top-level, coercion holes won't be included (they're never bound anywhere). But if we build the in-scope set by looking for free vars, we're OK. I suppose we always have to do the latter in the type checker because metavars are similarly never bound.

Bottom line: yes, I agree with your assessment here. I will write a Note soon.