Проверка типов для Векторов в Идрисе

Question

Как из REPL не гарантирует, что список действительно интерпретируется как вектор?

Например, если я наберу:

:t Vect

Я получу Vect : Nat -> Type -> Type, что делает абсолютным смысл, если я наберу

:t Vect 2

, я получу Vect : Type -> Type, что снова имеет абсолютный смысл. Но я сейчас пытаюсь:

:t Vect 2 [1,2]

и получаю ошибку

Can't disambiguate since no name has a suitable type: 
         Prelude.List.::, Prelude.Stream.::, Data.Vect.::

Я надеялся вместо этого увидеть [1,2] : Vect 2 Int. Что я делаю не так? У меня также возникают проблемы при использовании функции the при попытке интерпретировать список как вектор.

Есть предложения?

Answer 1

the : (a : Type) -> a -> a принимает тип и значение этого типа и возвращает это значение. Поэтому, если целевой тип не может быть выведен из контекста, как в REPL, вы можете использовать the (Vect 2 Int) [1,2], чтобы указать, что вы подразумеваете под [1,2].

(Vect 2 [1,2] пытается использовать List, Stream или Vect [1,2] в качестве аргумента в Vect 2 : Type -> Type. Но, в отличие, например, Int, список [1,2] не является Type, поэтому выдает эту ошибку.)