Error message prints explicit kinds when it shouldn't

When compiled, this program:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -fno-print-explicit-kinds #-}
module Bug where

import Data.Kind

data Foo (a :: Type) :: forall b. (a -> b -> Type) -> Type where
  MkFoo :: Foo a f

f :: Foo a f -> String
f = show

Gives the following error:

$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:13:5: error:
    • No instance for (Show (Foo a b f)) arising from a use of ‘show’
    • In the expression: show
      In an equation for ‘f’: f = show
   |
13 | f = show
   |     ^^^^

This error message is slightly incorrect, however. In "No instance for (Show (Foo a b f))", it claims that Foo has three visible type parameters, but it only has two. (I've even made sure to enable -fno-print-explicit-kinds at the type to ensure that the invisible b kind shouldn't get printed, but it was anyway.)

This is a regression that was apparently introduced between GHC 8.0 and 8.2, since in GHC 8.0.2, it prints the correct thing:

$ /opt/ghc/8.0.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:13:5: error:
    • No instance for (Show (Foo a f)) arising from a use of ‘show’
    • In the expression: show
      In an equation for ‘f’: f = show

But it does not in GHC 8.2.1:

$ /opt/ghc/8.2.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:13:5: error:
    • No instance for (Show (Foo a b f)) arising from a use of ‘show’
    • In the expression: show
      In an equation for ‘f’: f = show
   |
13 | f = show
   |     ^^^^

Trac metadata

Trac field	Value
Version	8.4.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed milestone to %8.6.1

changed weight to 5

added Tbug Trac import TypeInType typechecker labels

Trac metadata

Trac field	Value
Differential revisions	- → D4891

mentioned in commit 3d002087

mentioned in issue #15330 (closed)

mentioned in commit 93b7ac8d

Trac metadata

Trac field	Value
Test case	- → dependent/should_fail/T15308

added 1 deleted label

closed

#15308 (closed) merged with 42396113.

#15308 (closed) merged with 9bcbb222.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

removed 1 deleted label

added error messages label

added Pnormal label