如何返回正确的依赖类型？咨询fnc2定义报错原因

在研究依赖类型应用时，我定义了如下依赖向量类型：

Inductive vector(A: Type): nat -> Type :=
  empty_vector: vector A 0
  | nonempty_vector: forall (n: nat), A -> vector A n -> vector A (S n).

我想编写返回与输入向量同类型的函数，下面是几个尝试的情况：

正常运行的函数fnc1 #

Definition fnc1(n: nat) (v: vector bool n): Type :=
vector bool n.

这个函数没问题，因为它的返回类型是Type——也就是说，它返回的是类型本身，而vector bool n确实是属于Set（Coq类型层级分支）的一个类型，完全符合要求。

报错的函数fnc2 #

Definition fnc2(n: nat) (v: vector bool n): vector bool n :=
vector bool n.

报错信息如下：

In environment
n : nat
v : vector bool n
The term "vector bool n" has type "Set"
while it is expected to have type "vector bool n".

fnc2的问题所在 #

这里函数的返回类型被指定为vector bool n，这要求函数必须返回该类型下的一个具体实例（比如空向量empty_vector bool，或者用nonempty_vector构造的非空向量）。但你写的返回表达式vector bool n是一个类型，不是该类型的具体值——就像你定义一个返回bool的函数，却返回bool这个类型本身，而非true或false，类型完全不匹配。

正常运行的函数fnc3 #

Definition fnc3(n: nat) (v: vector bool n): vector bool n :=
v.

这个函数没问题，因为输入的v本身就是vector bool n类型的实例，直接返回它完全符合返回类型的要求。

内容的提问来源于stack exchange，提问作者Attila Károly