You can't with type lits. The solver can only decide concrete values :"""(

You'll have to use a concrete peano Nats type instead. 

I've been toying with the idea that the type lits syntax should be just that, a type level analogue of from integer that you can give to user land types, but I'm not going to suggest that till 7.8 is fully released. 

On Sunday, March 16, 2014, Henning Thielemann <lemming@henning-thielemann.de> wrote:
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?

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users