Search code examples
type-inferencedependent-typeidris

Unifying len and S len would lead to infinite value

I am trying to make a function hpure that generates an hvect by repeating the same element until it reaches the required length. Each element may have a different type. Ex: If the argument was show each element would 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 on the final v:

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

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

Solution

  • The issue is that the type of v depends on outs, and the recursive call to hpure passes the tail of outs. So v needs to be adjusted as well.

    The error is essentially saying that the lengths of outs and its tail would have to be the same in order for your version to typecheck.

    Here is a version that 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))