История изменений

> {-# LANGUAGE DataKinds, TypeOperators, GADTs, TypeFamilies, UndecidableInstances #-}
> import Control.Applicative
> import Control.Monad
> import GHC.TypeLits
> import Data.Proxy
> data Proof2D :: (Nat -> *) -> * where Proof2D :: KnownNat n => (Proxy n -> Integer) -> c n -> Proxy n -> Proof2D c
> instance Show (Proof2D c) where show (Proof2D _ _ k) = show $ natVal k
> data LessThen255D (n::Nat) where LessThen255D :: (n <= 255) => LessThen255D n
> oned :: KnownNat n => (Proxy n -> Integer) -> LessThen255D n -> Proxy n -> Proof2D LessThen255D
> oned = Proof2D
> c2dk :: KnownNat n => Proxy n -> (Proxy n -> Integer) -- Dict (KnownNat n)
> c2dk _ = natVal 
> guessProof :: (KnownNat n, n <= 255) => SomeNat -> Proxy n -> Maybe (Proof2D LessThen255D)
> guessProof (SomeNat p) n = Proof2D (c2dk n) LessThen255D n <$ sameNat p n
> data N = Z | S N
> type family Guesses (n::Nat) :: [Nat] where
>    Guesses 0 = '[0]
>    Guesses n = n ': Guesses (n-1)
> g :: Proxy n -> Proxy (Guesses n)
> g _ = Proxy
> class GuessProof (n :: [Nat]) where proof :: SomeNat -> Proxy n -> Maybe (Proof2D LessThen255D)
> instance GuessProof '[] where proof _ _ = Nothing
> instance (KnownNat n, n <= 255, GuessProof ns) => GuessProof (n ': ns) where
>   proof s p = guessProof s (inner p) `mplus` proof s (next p)
>    where inner :: Proxy (n ': ns) -> Proxy (n::Nat)
>          inner _ = Proxy
>          next :: Proxy (n ': ns) -> Proxy (ns::[Nat])
>          next _ = Proxy
> main :: IO()
> main = return ()
> type family C2N (n::N) :: Nat where
>   C2N 'Z = 0
>   C2N ('S x) = 1 + C2N x