[Haskell-cafe] cannot perform arithmetic with GHC.TypeLits?

[Baojun Wang]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160430/91c72423/attachment.html>