[GHC] #14139: Kind signature

20 Aug 2017

      #14139: Kind signature
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
           Keywords:                 |  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 don't understand the rules for kind signatures / CUSKs but this works

 {{{#!hs
 import Data.Singletons.Prelude

 data Some (f :: u ~> v) where
   Some :: Sing (x :: u) -> f @@ x -> Some f
 }}}

 but this doesn't?

 {{{#!hs
 import Data.Kind
 import Data.Singletons.Prelude

 data Some :: (u ~> v) -> Type where
   Some :: Sing (x :: u) -> f @@ x -> Some f

 --        • Expected kind ‘u ~> v’, but ‘f’ has kind ‘u ~> *’
 --        • In the first argument of ‘Some’, namely ‘f’
 --          In the type ‘Some f’
 --          In the definition of data constructor ‘Some’
 --      |
 --    5 |   Some :: Sing (x :: u) -> f @@ x -> Some f
 --      |                                           ^
 --    Failed, modules loaded: none.
 }}}

 I have to quantify over them for it to work `forall u v. (u ~> v) ->
 Type`, if this is expected I feel like the error message ought to be
 improved.

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