Let me understand if you understand what you are doing here. You have type AV a , which describes a computation that produces something like a , where the structure of this computation can be saved in such a way as to allow validation. You need a way to raise arbitrary functions in operations on AV , preserving the structure, without creating special cases for each operation.
Usually, Functor and Applicative can be used to raise functions into a structure. However, a simple way to do this involves transforming the structure and directly applying the raised function, rather than saving the application of the function as part of the structure.
What you want is much more inconvenient, and here's why:
Let's say we have some function that we want to raise, and two abstract values of the corresponding type, to apply them to:
x :: AV A x = ... y :: AV B y = ... f :: A -> B -> C f = ...
Suppose that there is a liftAV2 function that does what you want. We expect the type lift2 f be AV A -> AV B -> AV C , just like liftA for Applicative .
Later we want to check the calculations obtained with lift2 f , restoring the values of f , x and y . Let's say that at the moment we just want to extract the first argument. Suppose that there exists a function extractArg1 such that extractArg1 (liftAV2 fxy) = x . What is the type of extractArg1 ? Here, in the context, we know that it must be of type AV C -> AV A But what would he be? Something like AV C -> AV A ? This is wrong, because the result is not only a type a , it is irrespective of what type was used to construct the value of AV c . Assuming that the value we are working on was built using the result of liftAV2 f , we know that the type in question exists, but we cannot find it at all.
Here we enter a country that is sufficiently suitable, of existential types . Honestly use them, however, and not just misuse them with class types, as is often the case.
You can, perhaps, accomplish what you need with some effort, but this happens in a fairly advanced area. You want to use GADTs for beginners, although I think you can already do this. It also tends to be extremely awkward when working with existential types, because you are limited only by the fact that they are in limited contexts.
In your particular case, it would be easier to give AV two types of parameters: one of which represents the final type of calculation, and the other represents the structure of the calculation, for example:
data f :$ x = ... data AV structure result where ... AVApply :: AV f (a -> b) -> AV xa -> AV (f :$ x) b
Then, to check the calculations, you can look at the first type to find out what you have; to build the calculations, you can look at the second one to ensure type matching. The evaluation function will be of type AV ta -> a , discarding the structure. You can also “unzip” the calculations using the structure type, throwing out the result type if you need to split the structure so that, say, it is enough to print it.