<div dir="ltr">I think Carter is referring to this: http://hackage.haskell.org/package/ghc-typelits-natnormalise<div><br>On Saturday, April 30, 2016 at 8:35:01 AM UTC-4, Carter Schonwald wrote:<blockquote class="gmail_quote" style="margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">Use the type lits Nat solver plugin by Christian B, or a userland peano encoding.  Sadly ghc does have any builtin equational theory so you either need to construct proofs yourself or use a plugin. <div><br></div><div>I'm personally doing the plugin approach.  If you would like to construct the proofs by hand I'll dig up some examples later today if you like. <span></span><br><br>On Saturday, April 30, 2016, Baojun Wang <<a href="javascript:" target="_blank" gdf-obfuscated-mailto="o_yzxDUEBwAJ" rel="nofollow" onmousedown="this.href='javascript:';return true;" onclick="this.href='javascript:';return true;">wan...@gmail.com</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div>Hi List,</div><div><br></div><div>When I try to build below program, the compiler complains </div><div><br></div><div>  Couldn't match type ‘n’ with ‘1 + (n - 1)’ …<br></div><div><br></div><div>Why GHC (7.10.3) cannot do type level natural number arithmetic? `` n /= 1 + (n-1)`` at type level?</div><div><br></div><div>-- | main.hs</div><div>{-# LANGUAGE ScopedTypeVariables #-}</div><div>{-# LANGUAGE FlexibleInstances #-}</div><div>{-# LANGUAGE GADTs #-}</div><div>{-# LANGUAGE PolyKinds #-}</div><div>{-# LANGUAGE KindSignatures #-}</div><div>{-# LANGUAGE TypeOperators #-}</div><div>{-# LANGUAGE DataKinds #-}</div><div>{-# LANGUAGE OverloadedStrings #-}</div><div>{-# LANGUAGE DeriveGeneric #-}</div><div><br></div><div>module Main where</div><div><br></div><div>import qualified Data.ByteString as B</div><div>import Data.ByteString(ByteString)</div><div>import Data.Serialize   -- require cereal</div><div><br></div><div>import GHC.TypeLits</div><div><br></div><div>data Scalar :: Nat -> * -> * where</div><div>  Nil :: Scalar 0 a</div><div>  Cons :: a -> Scalar m a -> Scalar (1+m) a</div><div><br></div><div>instance (Serialize a) => Serialize (Scalar 0 a)  where</div><div>  get = return Nil</div><div>  put _ = return $ mempty</div><div><br></div><div>instance (Serialize a) => Serialize (Scalar n a) where</div><div>  get = do</div><div>    x  <- get :: Get a</div><div>    xs <- get :: Get (Scalar (n-1) a)</div><div>    return $! Cons x xs</div><div>  put (Cons x xs) = do</div><div>    put (x :: a)</div><div>    put xs</div><div><br></div></div><div>--</div><div><br></div><div>/tmp/vect1/app/Main.hs:31:15: Couldn't match type ‘n’ with ‘1 + (n - 1)’ …</div><div>      ‘n’ is a rigid type variable bound by</div><div>          the instance declaration at /tmp/vect1/app/Main.hs:27:10</div><div>    Expected type: Scalar n a</div><div>      Actual type: Scalar (1 + (n - 1)) a</div><div>    Relevant bindings include</div><div>      xs :: Scalar (n - 1) a (bound at /tmp/vect1/app/Main.hs:30:5)</div><div>      get :: Get (Scalar n a) (bound at /tmp/vect1/app/Main.hs:28:3)</div><div>    In the second argument of ‘($!)’, namely ‘Cons x xs’</div><div>    In a stmt of a 'do' block: return $! Cons x xs</div><div>Compilation failed.</div><div><br></div><div>- baojun</div></div>
</blockquote></div>
</blockquote></div></div>