[GHC] #15330: Error message prints invisible kind arguments in a visible matter

[GHC]

#15330: Error message prints invisible kind arguments in a visible matter
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.8.1
          Component:  Compiler       |           Version:  8.4.3
  (Type checker)                     |
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Poor/confusing
  Unknown/Multiple                   |  error message
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider the following program:

 {{{#!hs
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeInType #-}
 module Bug where

 import Data.Kind
 import Data.Proxy

 data T :: forall a. a -> Type

 f1 :: Proxy (T True)
 f1 = "foo"

 f2 :: forall (t :: forall a. a -> Type).
       Proxy (t True)
 f2 = "foo"
 }}}

 This program doesn't typecheck (for good reason). The error messages,
 however, are a bit iffy:

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

 Bug.hs:11:6: error:
     • Couldn't match expected type ‘Proxy (T 'True)’
                   with actual type ‘[Char]’
     • In the expression: "foo"
       In an equation for ‘f1’: f1 = "foo"
    |
 11 | f1 = "foo"
    |      ^^^^^

 Bug.hs:15:6: error:
     • Couldn't match expected type ‘Proxy (t Bool 'True)’
                   with actual type ‘[Char]’
     • In the expression: "foo"
       In an equation for ‘f2’: f2 = "foo"
     • Relevant bindings include
         f2 :: Proxy (t Bool 'True) (bound at Bug.hs:15:1)
    |
 15 | f2 = "foo"
    |      ^^^^^
 }}}

 Note that in the error message for `f1`, the type `T 'True` is printed
 correctly—the invisible `Bool` argument is omitted. However, in the error
 message for `f2`, this is not the case, as the type `t Bool 'True` is
 printed. That `Bool` is an invisible argument as well, and should not be
 printed without the use of, say, `-fprint-explicit-kinds`.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15330>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler