Re: [GHC] #11252: :kind command hides the explicit kind

18 Dec 2015

      #11252: :kind command hides the explicit kind
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  GHCi              |              Version:  7.11
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Linux             |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  Other             |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Iceland_jack):

 Example from [https://www.cis.upenn.edu/~eir/papers/2013/fckinds/fckinds-
 extended.pdf System FC with Explicit Kind Equality (Extended Version)]:

 {{{#!hs
 data Kind = Star | Arr Kind Kind

 data Ty :: Kind -> * where
   TInt :: Ty Star
   ...

 data TypeRep (k :: Kind) (t :: Ty k) where
   TyInt :: TyRep Star TInt
   ...
 }}}

 gives

 {{{#!hs
...
...
...
:kind TyRep
 TyRep :: Ty k -> *
 }}}
making the user think they should provide a `Ty k`

 {{{#!hs
...
...
...
:kind TyRep TInt
 <error>
 }}}
when they should really provide a `Kind` and ''then'' some `Ty k`:

 {{{#!hs
...
...
...
:kind TyRep Star
 TyRep Star :: Ty 'Star -> *
:kind TyRep Star TInt
 TyRep Star TInt :: *
 }}}
--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11252#comment:3
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler