-
-
Save glaebhoerl/3844758 to your computer and use it in GitHub Desktop.
Exploring kind-indexed type constraints in GHC 7.6
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE PolyKinds, GADTs, DataKinds, TypeFamilies, TypeOperators, | |
MultiParamTypeClasses, FlexibleContexts, FlexibleInstances, | |
UndecidableInstances #-} | |
module GHC_Query where | |
data Proxy (t :: k) = Proxy | |
data KindProxy (t :: *) = KindProxy -- a type-level proxy for kinds | |
data Nat = Z | S Nat | |
-- count the number of type arguments that the kind specifies | |
type family CountArgs (kp :: KindProxy k) :: Nat | |
type instance CountArgs (kp :: KindProxy *) = Z | |
type instance CountArgs (kp :: KindProxy (kD -> kR)) | |
= S (CountArgs ('KindProxy :: KindProxy kR)) | |
class NUnits (n :: Nat) where type Ts n :: [k] | |
instance NUnits Z where type Ts Z = '[] | |
instance NUnits n => NUnits (S n) where type Ts (S n) = () ': Ts n | |
-- a handle to test the behavior of NUnits | |
demonstrate_NUnits :: (n ~ CountArgs ('KindProxy :: KindProxy k), NUnits n) => | |
Proxy (t :: k) -> Proxy (Ts n :: [*]) | |
demonstrate_NUnits _ = Proxy | |
data GADT :: [*] -> * where | |
GZ :: GADT '[] | |
GS :: GADT ts -> GADT (() ': ts) | |
class CLASS (t :: k) where | |
method :: (n ~ CountArgs ('KindProxy :: KindProxy k), NUnits n) => Proxy t -> GADT (Ts n) | |
-- this compiles now | |
instance CLASS (t :: *) where method _ = GZ | |
-- testing in GHCi | |
{- | |
*GHC_Query> :i demonstrate_NUnits | |
demonstrate_NUnits :: | |
(n ~ CountArgs k ('KindProxy k), NUnits n) => | |
Proxy k t -> Proxy [*] (Ts * n) | |
-- Defined at frisby.hs:31:1 | |
-- I think :i just regurgitates the signature from the source file? | |
*GHC_Query> :t demonstrate_NUnits | |
demonstrate_NUnits | |
:: NUnits (CountArgs * ('KindProxy *)) => | |
Proxy * t -> Proxy [*] (Ts * (CountArgs * ('KindProxy *))) | |
-- Uses * instead of k as before, substitutes in our 'n' tyvar, doesn't simplify the output type (as before) | |
*GHC_Query> :set -XPolyKinds -XDataKinds | |
*GHC_Query> :t demonstrate_NUnits | |
demonstrate_NUnits | |
:: NUnits (CountArgs k ('KindProxy k)) => | |
Proxy k t -> Proxy [*] (Ts * (CountArgs k ('KindProxy k))) | |
-- Now it's using k | |
*GHC_Query> :t demonstrate_NUnits (Proxy :: Proxy Int) | |
demonstrate_NUnits (Proxy :: Proxy Int) :: Proxy [*] (Ts * 'Z) | |
*GHC_Query> :t demonstrate_NUnits (Proxy :: Proxy Maybe) | |
demonstrate_NUnits (Proxy :: Proxy Maybe) | |
:: Proxy [*] (Ts * ('S 'Z)) | |
*GHC_Query> :t demonstrate_NUnits (Proxy :: Proxy (,)) | |
demonstrate_NUnits (Proxy :: Proxy (,)) | |
:: Proxy [*] (Ts * ('S ('S 'Z))) | |
-- It's still not simplifying the output type, but this might be just a for-display thing | |
-- Wasn't there a version of :t added at some point which simplified away type functions? :t! or :k! or something? neither of those were recognized when I tried them | |
-- anyway, using the usual workaround... | |
*GHC_Query> show $ demonstrate_NUnits (Proxy :: Proxy Int) | |
<interactive>:9:1: | |
No instance for (Show (Proxy [*] ('[] *))) | |
arising from a use of `show' | |
Possible fix: | |
add an instance declaration for (Show (Proxy [*] ('[] *))) | |
In the expression: show | |
In the expression: show $ demonstrate_NUnits (Proxy :: Proxy Int) | |
In an equation for `it': | |
it = show $ demonstrate_NUnits (Proxy :: Proxy Int) | |
-- Now we see that it does get the correct type | |
*GHC_Query> show $ demonstrate_NUnits (Proxy :: Proxy Maybe) | |
<interactive>:10:1: | |
No instance for (Show (Proxy [*] ((':) * () ('[] *)))) | |
arising from a use of `show' | |
Possible fix: | |
add an instance declaration for | |
(Show (Proxy [*] ((':) * () ('[] *)))) | |
In the expression: show | |
In the expression: show $ demonstrate_NUnits (Proxy :: Proxy Maybe) | |
In an equation for `it': | |
it = show $ demonstrate_NUnits (Proxy :: Proxy Maybe) | |
-- Also the correct type | |
*GHC_Query> show $ demonstrate_NUnits (Proxy :: Proxy (,)) | |
<interactive>:11:1: | |
No instance for (Show (Proxy [*] ((':) * () ((':) * () ('[] *))))) | |
arising from a use of `show' | |
Possible fix: | |
add an instance declaration for | |
(Show (Proxy [*] ((':) * () ((':) * () ('[] *))))) | |
In the expression: show | |
In the expression: show $ demonstrate_NUnits (Proxy :: Proxy (,)) | |
In an equation for `it': | |
it = show $ demonstrate_NUnits (Proxy :: Proxy (,)) | |
-- Also the correct type | |
-- Let's try something else | |
*GHC_Query> let foo :: Proxy '[]; foo = demonstrate_NUnits (Proxy :: Proxy Int) | |
<interactive>:12:29: | |
Couldn't match kind `k' with `*' | |
`k' is a rigid type variable bound by | |
the type signature for foo :: Proxy [k] ('[] k) | |
at <interactive>:12:12 | |
Expected type: Proxy [k] ('[] k) | |
Actual type: Proxy [*] (Ts * 'Z) | |
In the return type of a call of `demonstrate_NUnits' | |
In the expression: demonstrate_NUnits (Proxy :: Proxy Int) | |
In an equation for `foo': | |
foo = demonstrate_NUnits (Proxy :: Proxy Int) | |
-- Hmm, that's not right... but it works if we add a kind signature: | |
*GHC_Query> let foo :: Proxy ('[] :: [*]); foo = demonstrate_NUnits (Proxy :: Proxy Int) | |
-- And higher kinds also work: | |
*GHC_Query> let foo :: Proxy '[()]; foo = demonstrate_NUnits (Proxy :: Proxy Maybe) | |
*GHC_Query> let foo :: Proxy '[(), ()]; foo = demonstrate_NUnits (Proxy :: Proxy (,)) | |
-} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment