[GHC] #15591: Inconsistent kind variable binder visibility between associated and non-associated type families

1 Sep 2018

      #15591: Inconsistent kind variable binder visibility between associated and non-
associated type families
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.5
           Keywords:                 |  Operating System:  Unknown/Multiple
  TypeApplications, TypeFamilies     |
       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:

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

 import Data.Kind

 type family T1 (x :: f (a :: Type))

 class C (a :: Type) where
   type T2 (x :: f a)
 }}}
 {{{
 $ 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 (f :: * -> *) a. f a -> *
 λ> :kind T2
 T2 :: forall {a} (f :: * -> *). f a -> *
 }}}

 Something is strange about the visibility of `a` in the kinds of `T1` and
 `T2`. In `T1`, it's visible, but in `T2`, it's not! I would expect them to
 both be visible, since they were both mentioned by name in each type
 family's definition.

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

 I indicated 8.5 as the version for this ticket since this behavior has
 changed since GHC 8.4, where you'd get the following:

 {{{
 $ /opt/ghc/8.4.3/bin/ghci Foo.hs -fprint-explicit-foralls
 GHCi, version 8.4.3: 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 (f :: * -> *) a. f a -> *
 λ> :kind T2
 T2 :: forall (f :: * -> *) a. f a -> *
 }}}

 Here, both `a`s are visible. However, it's still wrong in that `a` should
 be listed before `f` in `T2`'s telescope, since `a` was bound first (in
 `C`'s class head), before `f`. In that sense, the current behavior is a
 slight improvement, although we're not fully correct yet.

 The only difference between `T1` and `T2` is that `T2` is associated with
 a class, which suggests that there is some difference in code paths
 between the two that is accounting for this.

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