How to rewrite a function body in Idris so that the type corresponds to the function signature and the whole thing compiles

Question

I would like for this to compile:

foo: Vect n String -> Vect n String
foo {n} xs = take n xs

This fails to compile because the compiler cannot unify n with n + m. I understand that this is because of the signature of take for Vect's but I cannot figure out how to go about showing the compiler that they can be unified if m = 0.

Answer 1

Just to add to the previous answer, one other possibility is to do the rewrite inline using the existing plusZeroRightNeutral lemma from the library:

foo: Vect n String -> Vect n String
foo {n} xs = let xs' : Vect (n + 0) String
                     = rewrite (plusZeroRightNeutral n) in xs in
                 take n xs'

The difficulty Idris is having in unification is because it is unwilling to infer the m in the application of take:

take : (n : Nat) -> Vect (n + m) a -> Vect n a

You've given it a Vect n String where it wanted a Vect (n + m) a - it has happily unified the a with the String, because Vect is a type constructor, but is unwilling to unify n with n + m because, in general, it can't invert functions. You and I can tell that m has to be zero, but Idris is not so clever.

Answer 2

Idris can't unify n with n + m because it does not know that n = n + 0. You need to help him by manually proving that.

First of all, why it needs this proof. The reason is that take expects Vect (n+m) a:

Idris> :t Vect.take
Prelude.Vect.take : (n : Nat) -> Vect (n + m) a -> Vect n a

So, this will typecheck

foo: Vect (n + 0) String -> Vect n String
foo {n} xs = take n xs

You need a way to convert Vect n a to Vect (n + 0) a:

addNothing : {n : Nat} -> {a : Type} -> Vect n a -> Vect (n+Z) a

It is possible with replace function:

Idris> :t replace
replace : (x = y) -> P x -> P y

But now you need a proof that n = n + 0. Here it is (with the rest of the code):

plusAddZero : (n : Nat) -> n = n + 0
plusAddZero = proof
  intros
  rewrite (plusCommutative n 0)
  trivial

addNothing : {n : Nat} -> {a : Type} -> Vect n a -> Vect (n + 0) a
addNothing {n} {a} = replace {P = \m => Vect m a} (plusAddZero n)

foo : Vect n String -> Vect n String
foo {n} xs = Vect.take n (addNothing xs)

Seems like too much for such a simple function. Hope someone will show more concise solution.