Can Idris deduce indices into top-level constant types?

Question

For example, Agda lets me write this:

open import Data.Vec open import Data.Nat myVec : Vec ℕ _ myVec = 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] 

and myVec will be of type Vec ℕ 4 , as expected.

But if I try the same in Idris:

 import Data.Vect myVec : Vect _ Nat myVec = [0, 1, 2, 3] 

I get an error from typechecker:

  When checking right hand side of myVec with expected type Vect len Nat Type mismatch between Vect 4 Nat (Type of [0, 1, 2, 3]) and Vect len Nat (Expected type) Specifically: Type mismatch between 4 and len 

Is there a way to define myVec in Idris without specifying a Vect index pointer?

Answer 1

In the comments, the top-level holes in Idris were universally counted, not filled with the term.

I believe (but ultimately someone from the development team would have to confirm / deny) that this was done in part to encourage explicit types and, therefore, to develop using the type, and in part to have good syntax for not care values ​​in interface implementations, for example:

 Uninhabited v => Uninhabited (_, v) where uninhabited (_, void) = uninhabited void 

This misuse of underscores is taken from its use in templates, not expressions.

---

For something like this (this is not exactly what you want, but it is resistant to constant changes), you can use an explicit existential one:

 fst : DPair t _ -> t fst (x ** _) = x snd : (s : DPair _ p) -> p (fst s) snd (_ ** prf) = prf myVecEx : (n ** Vect n Nat) myVecEx = (_ ** [0, 1, 2, 3]) myVec : Vect (fst myVecEx) Nat myVec = snd myVecEx 

fst and snd may be in the standard library under different names, but as a result of a quick search, I did not find it.