Unification and Assignments

Is unification an appropriate tool in assignment generation? I imagine a user specifying some
partially filled in template (possibly a type like (a->b) or (((Int->Int)->[Int]->Int)+) where we are saying that we want a problem where + is folded over a list. A problem is generated and the very general test case of folds is specialized to use some addition operation. The story is one of probably many possible for that type and the things in the list are things with a property that can be summed. This is discovered by a database of knowledge that backs the whole system. Hopefully there is some way to allow composition to occur between function types, and we can get application of assignments to assignments, composition of assignments, and still instantiate because some invariants are satisfied and ensure or at least guide the composition to semantically valid templates from which assignments and test cases can be created.

Will this ever exist? Does it make any sense? I don't know.