[GHC] #15592: Type families without CUSKs cannot be given visible kind variable binders
GHC
ghc-devs at haskell.org
Sat Sep 1 14:53:48 UTC 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
More information about the ghc-tickets
mailing list