Playing around with DataKinds in Haskell, I produced the following code, which implements and abuses some type-level unary nats:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Demo where
import Data.Proxy
import Data.Semigroup
import Numeric.Natural
import Data.Constraint
data Nat = Zero | Succ Nat
type family Pred (n :: Nat) where Pred ('Succ n) = n
class IsNat (n :: Nat) where
nat :: proxy n -> Natural
unNat :: proxy n -> (n ~ 'Zero => x) -> ((n ~ 'Succ (Pred n), IsNat (Pred n)) => x) -> x
instance IsNat 'Zero where
nat _ = 0
unNat _ z _ = z
instance IsNat n => IsNat ('Succ n) where
nat _ = succ (nat (Proxy @n))
unNat _ _ s = s
noneIsNotSuccd :: (n ~ 'Zero, n ~ 'Succ (Pred n)) => proxy n -> a
noneIsNotSuccd _ = error "GHC proved ('Zero ~ 'Succ (Pred 'Zero))!" -- don't worry, this won't happen
predSuccIsNat :: forall n proxy r. (n ~ 'Succ (Pred n)) => proxy n -> (IsNat (Pred n) => r) -> r
predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r
data Indexed (n :: Nat) where
Z :: Indexed 'Zero
S :: Indexed n -> Indexed ('Succ n)
instance Show (Indexed n) where
show Z = "0"
show (S n) = "S" <> show n
recr :: forall n x. (IsNat n, Semigroup x) => (forall k. IsNat k => Indexed k -> x) -> Indexed n -> x
recr f Z = f Z
recr f (S predn) = predSuccIsNat (Proxy @n) (f predn) <> f (S predn)
main :: IO ()
main = print $ getSum $ recr (Sum . nat) (S Z)
When I attempt to compile it in GHC 8.2.2, I get the following type error:
Demo.hs:35:25: error:
• Could not deduce (IsNat (Pred n)) arising from a use of ‘unNat’
from the context: n ~ 'Succ (Pred n)
bound by the type signature for:
predSuccIsNat :: forall (n :: Nat) (proxy :: Nat -> *) r.
n ~ 'Succ (Pred n) =>
proxy n -> (IsNat (Pred n) => r) -> r
at Demo.hs:34:1-96
• In the expression: unNat proxy (noneIsNotSuccd proxy) r
In an equation for ‘predSuccIsNat’:
predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r
|
35 | predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
This is admittedly an improvement over what happens in GHC 8.0.1, where it compiles fine and then fails at runtime:
*** Exception: Demo.hs:34:23: error:
• Could not deduce (IsNat (Pred n)) arising from a use of ‘unNat’
from the context: n ~ 'Succ (Pred n)
bound by the type signature for:
predSuccIsNat :: n ~ 'Succ (Pred n) =>
proxy n -> (IsNat (Pred n) => r) -> r
at Demo.hs:33:1-78
• In the expression: unNat proxy (noneIsNotSuccd proxy)
In an equation for ‘predSuccIsNat’:
predSuccIsNat proxy = unNat proxy (noneIsNotSuccd proxy)
(deferred type error)
It appears that in GHC 8.2.2, unNat is adopting an implicit (IsNat (Pred n)) constraint that does not appear in the type signature:
λ» :t unNat
unNat
:: IsNat n =>
proxy n
-> (n ~ 'Zero => x)
-> ((n ~ 'Succ (Pred n), IsNat (Pred n)) => x)
-> x
Is there any way for me to call unNat to implement something like predSuccIsNat?
predSuccIsNat :: forall n proxy r. (n ~ 'Succ (Pred n)) => proxy n -> (IsNat (Pred n) => r) -> r
predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r
^^^^^
I don't know where you expect to get the IsNat dictionary that you need in order to use unNat. If I add it to the type signature
predSuccIsNat :: forall n proxy r. IsNat n => (n ~ 'Succ (Pred n)) => proxy n -> (IsNat (Pred n) => r) -> r
predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r
everything works fine (on ghc 8.2.1, which has the same deferred problem as 8.0.1).
Without it, it seems like you want to infer that if n ~ 'Succ (Pred n) then IsNat n -- presumably from the fact that Pred n is only defined on Succs. But even if that inference could be made, it would not be enough. For example n ~ Succ m is not enough to infer IsNat either, you would also need IsNat m.