Ian Childs wrote:

I have a function that returns a witness to 's :: Term a' and 't :: Term b' having the same type, if they do, but I am wondering how to extend this to the first argument of an arrow type.

Basically you have to write the deconstruct that takes (TRepr a), the witness for type a, and returns either Nothing or Just (exists b1 b2. (EQ a (b1->b2), TRepr b1, TRepr b2)) That is, if the type a is indeed an arrow type, you return the triple: the witnesses for the argument and the result types and the witness for the equality of a and b1->b2. Problems like these often occur in type-checking (or in de-serialization of a typed term from an untyped representations). The following page discusses two (GADT and GADT-less) solutions: http://okmij.org/ftp/tagless-final/course/course.html#type-checking Specifically, http://okmij.org/ftp/tagless-final/course/Typ.hs defines such an arrow witness, names `AsArrow'. Both approaches are essentially equivalent -- and both are quite complex. It really takes a couple of hours to explain either of them. I don't believe a simple solution exists.