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 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.
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 |