lenとS lenを統一すると無限の値になる

Question

同じ要素を必要な長さに達するまで繰り返すことによってhvectを生成する関数hpureを作成しようとしています。各要素は異なる型を持つことができます。例：引数が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))