[GHC] #13909: Can't partially apply a data type with a visible quantifier in its kind

1 Jul 2017

      #13909: Can't partially apply a data type with a visible quantifier in its kind
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I'm not sure if this is a bug or an intended design, so I'll ask here. I
 want this program to typecheck:

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

 import Data.Kind

 data Hm (k :: Type) (a :: k) :: Type

 class HasName (a :: k) where
   getName :: proxy a -> String

 instance HasName Hm where
   getName _ = "Hm"
 }}}

 This is rejected, however:

 {{{
 $ /opt/ghc/8.2.1/bin/ghci Bug.hs
 GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/ryanglscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:11:18: error:
     • Expecting two more arguments to ‘Hm’
       Expected kind ‘k0’, but ‘Hm’ has kind ‘forall k -> k -> *’
     • In the first argument of ‘HasName’, namely ‘Hm’
       In the instance declaration for ‘HasName Hm’
    |
 11 | instance HasName Hm where
    |                  ^^
 }}}

 The culprit appears to be the fact that `Hm` has kind `forall k -> k ->
 *`, which uses a visible quantifier. Does this prevent partial
 applications of `Hm`? Or is this simply a GHC bug?

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