An unwritten kind variable is "specified", when it shouldn't be.

[goldfire]

This fails:

{-# LANGUAGE PolyKinds, TypeApplications, ScopedTypeVariables #-}

module Bug where

import Data.Proxy

class C a where
  foo :: Proxy a

bar :: forall a. C a => Proxy a
bar = foo @a

But it really should work, because the invisible kind variable to class C should not be available for type application. On the last line, foo @_ @a works, when you explicitly instantiate the kind variable. Also, saying :t foo in GHCi shows the specified kind variable.

Will fix. At some point.

[Richard Eisenberg <eir@…>]

In f4f315a/ghc:

Fix #11512 by getting visibility right for methods

Test case: typecheck/should_compile/T11512

[bgamari]

Merged as 4c64da079d6009f8da7877c86c12ac5212c15d3e.

[Richard Eisenberg <eir@…>]

In 35e93797/ghc:

Track specified/invisible more carefully.

In particular, this allows correct tracking of specified/invisible
for variables in Haskell98 data constructors and in pattern synonyms.
GADT-syntax constructors are harder, and are left until #11721.

This was all inspired by Simon's comments to my fix for #11512,
which this subsumes.

Test case: ghci/scripts/TypeAppData

[skip ci]  (The test case fails because of an unrelated problem
fixed in the next commit.)

[bgamari]

Merged as fefaba919f4fcfe4eb71198d91a8718b72d7b6a1.