<div dir="ltr">Iavor is working on a branch that allows the constraint solver to call an external solver: <a href="https://github.com/ghc/ghc/tree/decision-procedure">https://github.com/ghc/ghc/tree/decision-procedure</a><div>
Currently, it: a) only supports CVC4 (an SMT solver), and b) is slightly out of of line with HEAD.</div><div>I think the above branch will be able to solve things like: 1 <= n + 1 ~ True</div><div><br></div><div>I myself worked on a patch that can only work with equalities: <a href="https://gist.github.com/christiaanb/8396614">https://gist.github.com/christiaanb/8396614</a></div>
<div>It allows you to solve both more and less constraints than Iavor's CVC4 approach:</div><div>More: It can deal with non-constant multiplications, and also with exponentials</div><div>Less: It cannot deal with inequalities</div>
<div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Mar 16, 2014 at 1:44 PM, Henning Thielemann <span dir="ltr"><<a href="mailto:lemming@henning-thielemann.de" target="_blank">lemming@henning-thielemann.de</a>></span> 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>
</blockquote></div><br></div>