Not sure I understand, can you give an example?

(map identity xs) is a classic example, identity doesn't have type any -> any, but a -> a, there's a clear relation between input and output

Thanks I see what you mean now, but isn’t that orthogonal to that particular issue?

Partially. How will you write the schema for the higher order function map?

Right, I think I see what you mean now. The instrumentation fn would unify the type variables with the actual values at runtime