[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:
                                     |  polykinds/T15592{,b}
      Blocked By:  14880             |             Blocking:
 Related Tickets:  #15591            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * status:  closed => new
 * resolution:  fixed =>


Comment:

 Concerning comment:16 we need to be careful

 We certainly have `C :: forall {k}. k -> Constraint`.  So `k` is
 `Inferred` and `a` is `Required`.

 Now look at `T`.  I think we want
 {{{
 T :: forall k (a::k) (f :: k->Type). f a -> Type
 }}}
 That is: `k` must be `Specified` (because the user wrote it); but it must
 precede the `a` which comes from the class. On the other hand, if `T`
 didn't mention `k` it'd be `Inferred`.

 What about this?
 {{{
 class D (a::k) where
   type S a
 }}}
 Here `k` is `Specified` for `D`, but is it `Specified` or `Inferred` for
 `S`?  The notes in `Note [Required, Specified, and Inferred for types]` do
 not really answer this question.

 This business of thinking about how the class header affects the
 Inferred/Specified/Required spec for the associated type is desperately
 tricky. I still wonder if we should instead look at the type declaration
 alone.

 An improvement would be this:

 * Whether the tyvar is Inferred or Specified is determined by looking at
 the associated type (alone)

 * But the order in which the Specified variables appear is affected by the
 class header.

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