#16376: GHCi HEAD silently accepts ill-kinded visible type applications with :type

"GHC" <[email protected]>
Newsgroups gmane.comp.lang.haskell.glasgow.bugs
Message-ID <[email protected]>
#16376: GHCi HEAD silently accepts ill-kinded visible type applications with :type
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  highest        |         Milestone:
          Component:  GHCi           |           Version:  8.9
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC accepts
  Unknown/Multiple                   |  invalid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 If you try something nonsensical like `id @Maybe` in GHCi 8.6.3, it will
 be properly rejected:

 {{{
 $ ghci -XTypeApplications
 GHCi, version 8.6.3: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 λ> :t id @Maybe

 <interactive>:1:5: error:
     • Expecting one more argument to ‘Maybe’
       Expected a type, but ‘Maybe’ has kind ‘* -> *’
     • In the type ‘Maybe’
       In the expression: id @Maybe
 }}}

 On GHC HEAD, however, this is seemingly accepted!

 {{{
 $ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive -XTypeApplications
 GHCi, version 8.9.20190224: https://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 λ> :t id @Maybe
 λ>
 }}}

 No error message, just... a newline. Quite bizarre. Even more bizarrely,
 this phenomenon doesn't appear to happen with `:kind`:

 {{{
 λ> :set -XDataKinds -XPolyKinds
 λ> type Id (a :: k) = a
 λ> :k Id @Maybe

 <interactive>:1:5: error:
     • Expecting one more argument to ‘Maybe’
       Expected a type, but ‘Maybe’ has kind ‘* -> *’
     • In the first argument of ‘Id’, namely ‘Maybe’
       In the type ‘Id @Maybe’
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16376>
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.