
It's _nothing_ to do with whether the kind changes!
It's everything to do with cloning the binder if it is already in scope. See "Secrets of the GHC inliner", the section called "The rapier", I think.
| Separately, I also see that substTyVar does not currently recur into a
| tyvar's kind, if the tyvar is not mapped by the substitution. This behavior
| seems wrong to me, but I guess it's worked thus far.
Well that would be deeply strange. The point is that every occurrence of a type variable should have the same kind as its binding site. So if we have
forall (a:k). ....(a:k')....
then k and k' should jolly well be the same.
Suppose the substitution S has a binding kv -> k, for some kind variable kv. Then suppose apply this substitution to
forall (a:blah). ...(a:blah)...
where blah mentions kv. Then we'll substitute k for kv in blah, and extend the substitution with (a:blah) -> (a : S(blah)). That will ensure that all occurrences of a get updated.
But it would be most odd to apply S to the body of the forall, but not to the binder. Recursing into the kind would give
forall (a:blah. ....(a:S(blah))...
which is bogus (Lint will reject it). But not recursing into the kind would also go wrong if we had, say (Proxy blah (a:blah)). The if we don’t recurse in we'd get Proxy S(blah) (a:blah), which is bogus.
So there's another invariant hiding here, but I'm not sure how to state it.
Simon
| -----Original Message-----
| From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Richard
| Eisenberg
| Sent: 11 April 2016 20:53
| To: ghc-devs@haskell.org developers