Inconsistent kind variable binder visibility between associated and non-associated type families

Consider the following program and GHCi session which uses it:

{-# 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 as 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.

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture