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

1 Sep 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.6.1
          Component:  Compiler       |           Version:  8.4.3
           Keywords:                 |  Operating System:  Unknown/Multiple
  TypeApplications, TypeFamilies,    |
  CUSKs                              |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider the following program and GHCi session which uses it:

 {{{
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeFamilies #-}
 module Foo where

 import Data.Kind

 type family T1 (x :: Type) (y :: a) :: Type where {}
 type family T2 x           (y :: a) :: Type where {}
 }}}
 {{{
 $ ghc2/inplace/bin/ghc-stage2 --interactive Foo.hs -fprint-explicit-
 foralls
 GHCi, version 8.7.20180831: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Foo              ( Foo.hs, interpreted )
 Ok, one module loaded.
 λ> :kind T1
 T1 :: forall a. * -> a -> *
 λ> :kind T2
 T2 :: forall {k} {a}. k -> a -> *
 }}}

 Note that `T1` quantifies `a` visibly whereas `T2` does not. I find this
 somewhat surprising, since both `T1` and `T2` explicitly mention `a` in
 their respective definitions. The only difference between the two is that
 `T1` has a CUSK while `T2` does not.

 This isn't of much importance at the moment, but it will be once visible
 kind application lands, as this will prevent anyone from instantiating the
 `a` in `T2` using a kind application.

 It's unclear to me whether this is intended behavior or not. I suppose
 there might be an unwritten rule that you can't use visible kind
 application on anything that doesn't have a CUSK, but if this really is
 the case, we should be upfront about it.

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