Hi List,
When I try to build below program, the compiler complains
Couldn't match type ‘n’ with ‘1 + (n - 1)’ …
Why GHC (7.10.3) cannot do type level natural number arithmetic? `` n /= 1 + (n-1)`` at type level?
-- | main.hs
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE DeriveGeneric #-}
module Main where
import qualified Data.ByteString as B
import Data.ByteString(ByteString)
import Data.Serialize -- require cereal
import GHC.TypeLits
data Scalar :: Nat -> * -> * where
Nil :: Scalar 0 a
Cons :: a -> Scalar m a -> Scalar (1+m) a
instance (Serialize a) => Serialize (Scalar 0 a) where
get = return Nil
put _ = return $ mempty
instance (Serialize a) => Serialize (Scalar n a) where
get = do
x <- get :: Get a
xs <- get :: Get (Scalar (n-1) a)
return $! Cons x xs
put (Cons x xs) = do
put (x :: a)
put xs
--
/tmp/vect1/app/Main.hs:31:15: Couldn't match type ‘n’ with ‘1 + (n - 1)’ …
‘n’ is a rigid type variable bound by
the instance declaration at /tmp/vect1/app/Main.hs:27:10
Expected type: Scalar n a
Actual type: Scalar (1 + (n - 1)) a
Relevant bindings include
xs :: Scalar (n - 1) a (bound at /tmp/vect1/app/Main.hs:30:5)
get :: Get (Scalar n a) (bound at /tmp/vect1/app/Main.hs:28:3)
In the second argument of ‘($!)’, namely ‘Cons x xs’
In a stmt of a 'do' block: return $! Cons x xs
Compilation failed.
- baojun