type-inference - 统一 len 和 S len 会带来无限的值(value)

Question

我正在尝试创建一个函数 hpure通过重复相同的元素直到达到所需的长度来生成 hvect。每个元素可能有不同的类型。例如:如果参数是 show 每个元素将是 show 函数的特化。

hpure show : HVect [Int -> String, String -> String, SomeRandomShowableType ->  String]

这是我的尝试:

hpure : {outs : Vect k Type} -> ({a : _} -> {auto p : Elem a outs} -> a) -> HVect outs
hpure {outs = []} _ = []
hpure {outs = _ :: _ } v = v :: hpure v

此错误发生在最后的 v 上:

When checking an application of Main.hpure:
        Unifying len and S len would lead to infinite value

为什么会发生错误，我该如何解决？

Answer 1

问题在于 v 的类型取决于 outs ，以及对 hpure 的递归调用通过outs的尾部.所以v也需要调整。

该错误本质上是说 outs 的长度并且它的尾部必须相同才能让您的版本进行类型检查。

这是一个类型检查的版本。

hpure : {outs : Vect k Type} -> ({a : Type} -> {auto p : Elem a outs} -> a) -> HVect outs
hpure {outs = []} _ = []
hpure {outs = _ :: _} v = v Here :: hpure (\p => v (There p))