Combining len and S len will lead to infinite value

Question

I am trying to create a function hpurethat generates an hvect by repeating the same element until it reaches the required length. Each element can have a different type. Example: if an argument was shown, each element will be a specialization of the show function.

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

This is my attempt:

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

This error occurs when final v:

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

Why does an error occur and how can I fix it?

Answer 1

The problem is that the type is vdependent on outs, and the recursive call hpurepasses the tail outs. Therefore, it is valso necessary to adjust.

, outs , typecheck.

, typechecks.

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