Unification len et S len conduirait à une valeur infinie

Question

J'essaye de faire une fonction hpure qui génère un effet en répétant le même élément jusqu'à ce qu'il atteigne la longueur requise. Chaque élément peut avoir un type différent. Ex: Si l'argument était show, chaque élément serait une spécialisation de la fonction show.

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

Ceci est ma tentative:

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

Cette erreur se produit sur la finale v:

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

Pourquoi ne se produit l'erreur et comment puis-je résoudre ce problème?

Answer 1

La question est que le type de v dépend de outs, et l'appel récursif à hpure passe la queue de outs. Donc, v doit également être ajusté.

L'erreur est essentiellement dire que les longueurs de outs et sa queue devraient être les mêmes pour que votre version à typecheck.

Voici une version qui indique les types.

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))