[GHC] #15592: Type families without CUSKs cannot be given visible kind variable binders

[GHC]

#15592: Type families without CUSKs cannot be given visible kind variable binders
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.8.1
       Component:  Compiler          |              Version:  8.4.3
      Resolution:                    |             Keywords:
                                     |  TypeApplications, TypeFamilies,
                                     |  CUSKs
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:  14880             |             Blocking:
 Related Tickets:  #15591            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 I discovered that this bug fix has a visible effect!  Consider this in
 `GHC.Records`:
 {{{
 -- | Constraint representing the fact that the field @x@ belongs to
 -- the record type @r@ and has field type @a at .  This will be solved
 -- automatically, but manual instances may be provided as well.
 class HasField (x :: k) r a | x r -> a where
   -- | Selector function to extract the field from the record.
   getField :: r -> a
 }}}
 What is the kind of `HasField` and type of `getField`? As of today, GHC
 says
 {{{
 HasField :: forall {k}. k -> * -> * -> Constraint
 getField :: forall {k] (x::k) r a. HasField x r a => r -> a
 }}}
 But actually, because of the `(x :: k)` in the class decl, the `k` is
 `Specified`. So the correct kind and type are:
 {{{
 HasField :: forall k. k -> * -> * -> Constraint
 getField :: forall k (x::k) r a. HasField x r a => r -> a
 }}}
 So in a visible type application of `getField` you'd have to write
 `getField @Symbol @x`.

 But that is not what Adam intended.  We don't want to be forced to write
 that kind, even in a visible type application.  We want `k` to be
 `Inferred`.

 I can achieve this for now by changing the decl to
 {{{
 class HasField x r a | x r -> a where
   getField :: r -> a
 }}}
 so removing the `:: k` from the decl.  But that is rather subtle.  I'm
 looking forward to explicit kind signatures... but NB: they need to be
 able to express the `Inferred`/`Specified` distinction.

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