Type families without CUSKs cannot be given visible kind variable binders
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.
Trac metadata
Trac field | Value |
---|---|
Version | 8.4.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |