Hi all, Vlad has proposed https://github.com/ghc-proposals/ghc-proposals/pull/556, an amendment to recently accepted proposal #448 on scoped type variables. It adds a nuance saying that f (MkT @(a :: <<here>>)) = ... should have the same scoping behavior as f (MkT (x :: <<here>>)) = ... Note that the first is a kind signature of a visible-type-application-in-a-pattern, while the second is a pattern signature. The intended scoping rule says that the use of an in-scope type variable in these positions is an occurrence, while the use of an out-of-scope type variable brings that variable into scope. Vlad's proposal corrects the phrasing in the original proposal that aligns the treatment of the kind signature with the type it is describing, forbidding e.g. the use of a repeated variable in the kind signature. Vlad's amendment makes the proposal what I had intended when I wrote #448; I strongly recommend acceptance. I think this is a small tweak of a technical detail buried in #448 and hope this does not cause widespread debate. I will accept this proposal in a week if I don't hear objections. Thanks! Richard