<wagnerdm <at> seas.upenn.edu> writes: > > Quoting AntC <anthony_clayden <at> clear.net.nz>: > > > {-# OPTIONS_GHC -XDataKinds -XPolyKinds -XKindSignatures #-} > > > > data MyNat = Z | S MyNat > > > > class NatToIntN (n :: MyNat) > > where natToIntN :: (n :: MyNat) -> Int > > instance NatToIntN Z > > where natToIntN _ = 0 > > instance (NatToIntN n) => NatToIntN (S n) > > where natToIntN _ = 1 + natToInt (undefined :: n) > > > > But GHC rejects the class declaration (method's type): > > "Kind mis-match > > Expected kind `ArgKind', but `n' has kind `MyNat'" > > (Taking the Kind signature out of the method's type gives same message.) > > At a guess, (->) :: * -> * -> *, but n :: MyNat, not n :: *, so (->) n > is badly kinded. In comparison: > > > data Proxy a = Proxy > > > > class NatToInt (n :: MyNat) > > where natToInt :: Proxy (n :: MyNat) -> Int > > instance NatToInt Z > > where natToInt _ = 0 > > instance (NatToInt n) => NatToInt (S n) > > where natToInt _ = 1 + natToInt (Proxy :: Proxy n) > > Here Proxy n :: *, even if n :: MyNat, so Proxy n is a fine argument > to hand to (->). > > ~d >
Thanks for the prompt response, and yes, you're right, so says GHCi: :k (->) :: * -> * -> * -- so `ArgKind` in the message means `*' :k Proxy :: AnyK -> * -- which answers what is `AnyKind' So Proxy is a kind-level wormhole: forall k. k -> * Singleton types are a wormhole from types to values. For the natToInt method, it's a shame having to insert Proxy's everywhere -- it takes away from the parallel to value-level equations. Perhaps I need promoted GADT's? Or perhaps PolyKinded (->) :: k1 -> k2 -> k3? AntC _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users