(π + 1) ≤ ν ⊢ ((π - 1) + 1) ≤ (ν - 1)

I have no idea what I’m doing with my dependent types, so bear with me if this is more of a question; the following error message seemed strange to me, even when I discount my cluelessness about the powerful magics involved.

I had good success implementing the unavoidable fixed-length Vector type, but when implementing an indexed access function, I got the error message (full message below) that ((π - 1) + 1) ≤ (ν - 1) can not be deduced from (π + 1) ≤ ν, even though it seemed to me it should be deducible. Am I running into a known limitation?

The full error message goes:

Could not deduce ((((π - 1) + 1) <=? (ν - 1)) ~ 'True) …
    from the context (KnownNat π, KnownNat (π - 1), (π + 1) <= ν)
      bound by the type signature for
                 index ∷ (KnownNat π, KnownNat (π - 1), (π + 1) <= ν) ⇒
                         Proxy π → Vector α ν → α
      at /home/seb/Dev/hs/spielwiese/dependent/dependent4.hs:53:9-79
    or from (ν ~ (ν1 + 1))
      bound by a pattern with constructor
                 :- ∷ ∀ α (ν ∷ Nat). α → Vector α ν → Vector α (ν + 1),
               in an equation for ‘index’
      at /home/seb/Dev/hs/spielwiese/dependent/dependent4.hs:54:22-49
    Relevant bindings include
      xs ∷ Vector α (ν - 1)
        (bound at /home/seb/Dev/hs/spielwiese/dependent/dependent4.hs:54:28)
      p ∷ Proxy π
        (bound at /home/seb/Dev/hs/spielwiese/dependent/dependent4.hs:54:8)
      index ∷ Proxy π → Vector α ν → α
        (bound at /home/seb/Dev/hs/spielwiese/dependent/dependent4.hs:54:1)
    In the expression: index (Proxy ∷ Proxy (π - 1)) xs
    In the expression:
      if i ≡ 0 then x else index (Proxy ∷ Proxy (π - 1)) xs
    In the expression:
      let i = natVal p
      in if i ≡ 0 then x else index (Proxy ∷ Proxy (π - 1)) xs

This is triggered by the following code (with all sorts of type annotations thrown in ~~in desperation~~ for good measure).

index ∷ (KnownNat π, KnownNat (π - 1), (π + 1 <= ν)) ⇒ Proxy π → Vector α ν → α
index (p ∷ Proxy π) (x :- (xs ∷ Vector α (ν - 1)) ∷ Vector α ν) =
    let i = natVal p
    in if i ≡ 0
       then x
       else index (Proxy ∷ Proxy (π - 1)) xs

Thanks for making this package!

This is a known limitation, one which I don't intend to tackle. This package, ghc-typelits-natnormalise, is meant to improve reasoning about equalities (=), and not inequalities (<=).

Check out https://github.com/yav/type-nat-solver for a solver that is based on an SMT solver which can handle inequalities. A short overview of the two approaches:

ghc-typelits-natnormalise:

pro: can reason about equalities of non-constant multiplication, e.g. it knows that a * (b + c) = a * b + a * c
pro: can reason about equalities of exponentiation, e.g. it knows that a^c * a^b = a^(c + b)
con: cannot reason about inequality, e.g., it doesn't know that: a <= b => (a+1) <= (b+1)

type-nat-solver:

pro: can reason about inequality, e.g., it knows that: a <= b => (a+1) <= (b+1)
con: cannot reason about equalities of non-constant multiplication, e.g. it doesn't know that a * (b + c) = a * b + a * c
con: cannot reason about equalities of exponentiation, e.g. it doesn't know that a^c * a^b = a^(c + b)

But there's nothing stopping you from using both solvers at once, seeing how they complement each other. The only problem is that type-nat-solver is not on hackage, but you can download the source from https://github.com/yav/type-nat-solver.

For your vector indexing function, check out the implementation of: http://hackage.haskell.org/package/clash-prelude-0.9/docs/src/CLaSH-Sized-Vector.html#at:

at :: SNat m -> Vec (m + (n + 1)) a -> a
at n xs = head $ snd $ splitAt n xs

head :: Vec (n + 1) a -> a
head (x :> _) = x

splitAt :: SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
splitAt n xs = splitAtU (toUNat n) xs

splitAtU :: UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
splitAtU UZero     ys        = (Nil,ys)
splitAtU (USucc s) (y :> ys) = let (as,bs) = splitAtU s ys
                               in  (y :> as, bs)

Where SNat n is sort of equivalent to your Proxy n. Of course, the devil is in the details: http://hackage.haskell.org/package/clash-prelude-0.9/docs/src/CLaSH-Promoted-Nat.html#toUNat:

toUNat :: SNat n -> UNat n
toUNat (SNat p) = fromI (natVal p)
  where
    fromI :: Integer -> UNat m
    fromI 0 = unsafeCoerce UZero
    fromI n = unsafeCoerce (USucc (fromI (n - 1)))

The reason is that you can't do indexing on SNat n is because you need an n amount of KnownNat n class constraints: KnownNat n, KnownNat (n-1), KnownNat (n-2) ... KnownNat (n-n). Anyhow, I would say that toUNat is morally safe/correct.

Thank you kindly for the helpful overview! I guess the Haskell dependent typing niche is a bit hard to overlook unless one is a researcher in the field, but hopefully the plugin system will make things more accessible to the rest of us. Also thanks for the pointer to type-nat-solver! If things won’t explode in my face when using both plugins in concert, I’ll try and see whether I can get the other one set up as well.

clash-lang / ghc-typelits-natnormalise

(π + 1) ≤ ν ⊢ ((π - 1) + 1) ≤ (ν - 1) #3