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

2 Nov 2018

      #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:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Richard and I talked more about this. We worreid abou
 {{{
 class C a b whre
   type T (x :: b a)
 }}}
 In what order do T's Specified variables show up?

 We got as far as a detailed proposal for associated types:

 * Which vars are Specified and which Inferred is determined by type decl
 alone (Specified = explicitly mentioned in the type decl)
 • For the Specified variables:
      * Start with lexical order from type decl
      * Do a stable partition, moving the ones from the class decl to the
 front
      * Use ScopedSort to put them in dependency order.

 But it all seemed terribly complicated.  We ended up thinking that it'd be
 better to ''ingnore'' the class header, and just do the normal thing:

 * Start with the lexical order from the type decl
 * Use ScopedSort

 This simplifies the spec, and simplifies the code.

 It is a bit unlike what happens for class methods (where the class
 variables all show up at the front, but
 we have no idea how to do make associated types really behave like class
 methods.  Eg
 {{{
 class C a where
  type F a
 }}}
 Then perhaps `F :: forall a -> C a => Type`, which is not ery nice. And it
 gets worse
 {{{
 class C a b where
   type F a
 }}}
 then perhaps `F :: forall {b}. forall a -> C a b => Type`. Ugh.  But if
 `b` depends on `a` we'd have to put
 it later in the telescope.

 So we decided to keep it simple!  (This is a small change from the commit
 in comment:15).

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