Created
October 5, 2012 21:39
-
-
Save nfrisby/3842579 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 #-} | |
-- this gist demonstrates some GHC 7.6 behaviors that I'm seeing as some type errors (example at the bottom). | |
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)) | |
-- constrains @ts@ to be a list of @()s@ that is @n@ long | |
class NUnits (n :: Nat) (ts :: [k]) | |
instance ('[] ~ ps) => NUnits Z ps | |
instance ((() ': pstail) ~ ps, NUnits n pstail) => NUnits (S n) ps | |
-- a handle to test the behavior of NUnits | |
-- (I get the same behaviors if I fold CountArgs into the declaration | |
-- and instances of NUnits) | |
demonstrate_NUnits :: NUnits (CountArgs ('KindProxy :: KindProxy k)) ts => | |
Proxy (t :: k) -> Proxy (ts :: [*]) | |
demonstrate_NUnits _ = Proxy | |
{- some NUnit behaviors | |
*GHC_Query> :i demonstrate_NUnits | |
demonstrate_NUnits :: | |
NUnits * (CountArgs k ('KindProxy k)) ts => | |
Proxy k t -> Proxy [*] ts | |
-- the above looks correct; k is unconstrained, so nothing is known about ts | |
*GHC_Query> :t demonstrate_NUnits | |
demonstrate_NUnits | |
:: NUnits * (CountArgs * ('KindProxy *)) ts => | |
Proxy * t -> Proxy [*] ts | |
-- apparently k defaults to *; but now shouldn't NUnits accordingly constrain ts to be '[]? | |
-- note that @NUnits * (CountArgs * ('KindProxy *)) ts@, if simplified, matches an instance head, | |
-- but remains unsimplified | |
*GHC_Query> :t demonstrate_NUnits (Proxy :: Proxy Int) | |
demonstrate_NUnits (Proxy :: Proxy Int) :: Proxy [*] ('[] *) | |
-- if we provide Int, that forces k to * and then ts _is_ subsequently forced to be '[]: the | |
-- NUnit constraint has been reduced and ts expanded accordingly | |
*GHC_Query> :t demonstrate_NUnits (Proxy :: Proxy (,,)) | |
demonstrate_NUnits (Proxy :: Proxy (,,)) | |
:: Proxy [*] ((':) * () ((':) * () ((':) * () ('[] *)))) | |
-- it also works the same way at higher kinds; that last type is just '[(), (), ()] | |
-} | |
{- | |
As in the case where NUnit is unexpectedly not simplified, I get this error from the instance of CLASS below. | |
Could not deduce (ts ~ '[] *) | |
from the context (NUnits * ('KindProxy *) ts) | |
I believe GHC can deduce that--it _does_ deduce that in the Proxy Int example behavior above, but not in the ":t demonstrate_NUnits" case and not in the following instance. | |
-} | |
data GADT :: [*] -> * where | |
GZ :: GADT '[] | |
GS :: GADT ts -> GADT (() ': ts) | |
class CLASS (t :: k) where | |
method :: NUnits (CountArgs ('KindProxy :: KindProxy k)) ts => Proxy t -> GADT ts | |
-- this instance causes the error | |
instance CLASS (t :: *) where method _ = GZ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment