Idris中向量的类型检查

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 ，因此会引发该错误。）