You can't with type lits. The solver can only decide concrete values :"""(<div><br></div><div>You'll have to use a concrete peano Nats type instead. </div><div><br></div><div>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. <span></span><br>
<div><br>On Sunday, March 16, 2014, Henning Thielemann <<a href="mailto:lemming@henning-thielemann.de">lemming@henning-thielemann.de</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Am 16.03.2014 09:40, schrieb Christiaan Baaij:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
To answer the second question (under the assumption that you want<br>
phantom-type style Vectors and not GADT-style):<br>
</blockquote>
<br>
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.<br>
<br>
I have modified your code as follows:<br>
<br>
{-# LANGUAGE Rank2Types #-}<br>
{-# LANGUAGE DataKinds #-}<br>
{-# LANGUAGE KindSignatures #-}<br>
{-# LANGUAGE ScopedTypeVariables #-}<br>
{-# LANGUAGE TypeOperators #-}<br>
{-# LANGUAGE TypeFamilies #-}<br>
module PositiveNat where<br>
<br>
import Data.Proxy (Proxy(Proxy))<br>
import GHC.TypeLits<br>
          (Nat, SomeNat(SomeNat), KnownNat, someNatVal, natVal,<br>
           type (<=), type (+))<br>
<br>
data Vector (n :: Nat) a = Vector a [a]<br>
<br>
withVector ::<br>
   forall a b.<br>
   a -> [a] -><br>
   (forall n . (KnownNat n, 1<=n) => Vector n a -> b) -> b<br>
withVector x xs f =<br>
   case someNatVal $ toInteger $ length xs of<br>
      Nothing -> error "static/dynamic mismatch"<br>
      Just (SomeNat (_ :: Proxy m)) -> f (Vector x xs :: Vector (m+1) a)<br>
<br>
vecLen :: forall n . KnownNat n => Vector n Integer -> Integer<br>
vecLen _ = natVal (Proxy :: Proxy n)<br>
<br>
-- > withVector vecLen [1,2,3,4]<br>
-- 4<br>
<br>
<br>
GHC-7.8 complains with:<br>
<br>
PositiveNat.hs:23:40:<br>
    Could not deduce ((1 GHC.TypeLits.<=? (n + 1)) ~ 'True)<br>
    from the context (KnownNat n)<br>
      bound by a pattern with constructor<br>
                 SomeNat :: forall (n :: Nat). KnownNat n => Proxy n -> SomeNat,<br>
               in a case alternative<br>
      at PositiveNat.hs:23:13-34<br>
    In the expression: f (Vector x xs :: Vector (m + 1) a)<br>
    In a case alternative:<br>
        Just (SomeNat (_ :: Proxy m))<br>
          -> f (Vector x xs :: Vector (m + 1) a)<br>
    In the expression:<br>
      case someNatVal $ toInteger $ length xs of {<br>
        Nothing -> error "static/dynamic mismatch"<br>
        Just (SomeNat (_ :: Proxy m))<br>
          -> f (Vector x xs :: Vector (m + 1) a) }<br>
<br>
<br>
How can I convince GHC that n+1 is always at least 1?<br>
<br>
<br>
When I remove the (1<=n) constraint, I still get:<br>
<br>
PositiveNat.hs:23:40:<br>
    Could not deduce (KnownNat (n + 1)) arising from a use of ‘f’<br>
    from the context (KnownNat n)<br>
      bound by a pattern with constructor<br>
                 SomeNat :: forall (n :: Nat). KnownNat n => Proxy n -> SomeNat,<br>
               in a case alternative<br>
      at PositiveNat.hs:23:13-34<br>
    In the expression: f (Vector x xs :: Vector (m + 1) a)<br>
    In a case alternative:<br>
        Just (SomeNat (_ :: Proxy m))<br>
          -> f (Vector x xs :: Vector (m + 1) a)<br>
    In the expression:<br>
      case someNatVal (toInteger (length xs)) of {<br>
        Nothing -> error "static/dynamic mismatch"<br>
        Just (SomeNat (_ :: Proxy m))<br>
          -> f (Vector x xs :: Vector (m + 1) a) }<br>
<br>
That is, I also have to convince GHC, that if (KnownNat n) then (n+1) is also KnownNat. How to do that?<br>
<br>
______________________________<u></u>_________________<br>
Glasgow-haskell-users mailing list<br>
<a>Glasgow-haskell-users@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/<u></u>mailman/listinfo/glasgow-<u></u>haskell-users</a><br>
</blockquote></div></div>