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

3 Oct 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:
      Blocked By:  14880             |             Blocking:
 Related Tickets:  #15591            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 By a series of strange coincidences, I ended up with almost exactly the
 same code as in comment:7 while working on this this morning. (Don't
 worry, I won't work on this any further until the dust has settled on
 #14880.) There's one thing I haven't worked out, though: how to make this
 work for associated types (in light of #15591). Consider:

 {{{#!hs
 class C a where
   type T (x :: f a)
 }}}

 Ideally, the kind of `T` would be:

 {{{#!hs
 T :: forall {k} (a :: k) (f :: k -> Type). f a -> Type
 }}}

 Alas, the code in comment:7 is not enough to accomplish this. It will
 instead give this as the kind for `T`:

 {{{#!hs
 T :: forall {k} {a :: k} (f :: k -> Type). f a -> Type
 }}}

 Note that `a` is now invisible. Ack.

 In order to fix this, we'd need to be aware of the fact that `a` is
 mentioned explicitly in `C` within `kcTyClGroup`. Currently, `kcTyClGroup`
 doesn't have access to this information, however.

 Another gotcha is that if you only use the code in comment:7, it'll cause
 some programs to no longer typecheck. In particular, this program:

 {{{#!hs
 class C a where
   type T (x :: (f :: k -> Type) a)
 }}}
 {{{
 Bug.hs:8:3: error:
     • These kind and type variables: (x :: (f :: k -> Type) a)
       are out of dependency order. Perhaps try this ordering:
         k (a :: k) (f :: k -> *) (x :: f a)
       NB: Implicitly declared variables come before others.
     • In the associated type family declaration for ‘T’
   |
 8 |   type T (x :: (f :: k -> Type) a)
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

 I'm unclear if this is desirable or not.

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