Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Exploring kind-indexed type constraints in GHC 7.6
{-# 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