positive type-level naturals

[Henning Thielemann]

Am 16.03.2014 09:40, schrieb Christiaan Baaij:

> To answer the second question (under the assumption that you want
> phantom-type style Vectors and not GADT-style):

Now I like to define non-empty vectors. The phantom parameter for the 
length shall refer to the actual vector length, not to length-1, for 
consistency between possibly empty and non-empty vectors.

I have modified your code as follows:

{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
module PositiveNat where

import Data.Proxy (Proxy(Proxy))
import GHC.TypeLits
           (Nat, SomeNat(SomeNat), KnownNat, someNatVal, natVal,
            type (<=), type (+))

data Vector (n :: Nat) a = Vector a [a]

withVector ::
    forall a b.
    a -> [a] ->
    (forall n . (KnownNat n, 1<=n) => Vector n a -> b) -> b
withVector x xs f =
    case someNatVal $ toInteger $ length xs of
       Nothing -> error "static/dynamic mismatch"
       Just (SomeNat (_ :: Proxy m)) -> f (Vector x xs :: Vector (m+1) a)

vecLen :: forall n . KnownNat n => Vector n Integer -> Integer
vecLen _ = natVal (Proxy :: Proxy n)

-- > withVector vecLen [1,2,3,4]
-- 4


GHC-7.8 complains with:

PositiveNat.hs:23:40:
     Could not deduce ((1 GHC.TypeLits.<=? (n + 1)) ~ 'True)
     from the context (KnownNat n)
       bound by a pattern with constructor
                  SomeNat :: forall (n :: Nat). KnownNat n => Proxy n -> 
SomeNat,
                in a case alternative
       at PositiveNat.hs:23:13-34
     In the expression: f (Vector x xs :: Vector (m + 1) a)
     In a case alternative:
         Just (SomeNat (_ :: Proxy m))
           -> f (Vector x xs :: Vector (m + 1) a)
     In the expression:
       case someNatVal $ toInteger $ length xs of {
         Nothing -> error "static/dynamic mismatch"
         Just (SomeNat (_ :: Proxy m))
           -> f (Vector x xs :: Vector (m + 1) a) }


How can I convince GHC that n+1 is always at least 1?


When I remove the (1<=n) constraint, I still get:

PositiveNat.hs:23:40:
     Could not deduce (KnownNat (n + 1)) arising from a use of ‘f’
     from the context (KnownNat n)
       bound by a pattern with constructor
                  SomeNat :: forall (n :: Nat). KnownNat n => Proxy n -> 
SomeNat,
                in a case alternative
       at PositiveNat.hs:23:13-34
     In the expression: f (Vector x xs :: Vector (m + 1) a)
     In a case alternative:
         Just (SomeNat (_ :: Proxy m))
           -> f (Vector x xs :: Vector (m + 1) a)
     In the expression:
       case someNatVal (toInteger (length xs)) of {
         Nothing -> error "static/dynamic mismatch"
         Just (SomeNat (_ :: Proxy m))
           -> f (Vector x xs :: Vector (m + 1) a) }

That is, I also have to convince GHC, that if (KnownNat n) then (n+1) is 
also KnownNat. How to do that?