is the type of substitute correct?

[gelisam]

It is currently:

substitute :: (Argument f n, GetArg f n ~ x)
    => Arg n -> Proof (x == x') -> f -> Proof (SetArg f n x')
substitute _ _ _ = axiom

but my understanding is that f is something like IsCons (Rev (Rev xs)), which is uninhabited. I think the third argument should be Proof f, not f:

substitute :: (Argument f n, GetArg f n ~ x)
    => Arg n -> Proof (x == x') -> Proof f -> Proof (SetArg f n x')
substitute _ _ _ = axiom

This would make it possible to use a Proof (Rev (Rev xs) == xs) to convert a Proof (IsCons (Rev (Rev xs))) into a Proof (IsCons xs).

If I am misunderstanding the purpose of substitute, is there a different way to use a Proof (Rev (Rev xs) == xs) to convert a Proof (IsCons (Rev (Rev xs))) into a Proof (IsCons xs)?

[matt-noonan]

No, I think you're exactly correct here! An earlier version of the library had both bare types and Proof types, using Proof more like a monad, but that was sort of confusing and annoying. I bet this didn't make the transition entirely intact.