Lambda the Ultimate

I have been looking for a language that includes the following form of resolution, but have not yet come to one.

Given a function f: a -> b, and a list l: [a], I would like for the language to consider "f l" a valid expression. In particular, I would like it to automatically "lift" f to be typed as f:[a] -> [b] by rewriting "f l" as "map f l". In general, given a functor F : a -> F a, a function f : a -> b, and value v : F a, I would like for the expression "f v" to be rewritten as "F(f) v : F(b)".

In addition, a multivariable method such as + : double -> double -> double, would lift based on the types of its arguments. Examples:
x, y: Id double |- (x + y) : Id double
x, y: [double] |- (x + y) : [double]
x, y: Interval double |- (x + y) : Interval double
x, y: Dist double |- (x + y) : Dist double
x: Dist double, y: Id double |- (x + y): Dist double
etc...

I understand that all of this can be done by augmenting the code to be written in terms of do notation (almost, these are just plain functors, not monads), but I want a language that does that for me: do x < - a, y <-b, return $ x + y (is equivalent to) a + b. If such a language doesn't exist, can I get suggestions on best/easiest ways to accomplish this. I have considered using a preprocessor/modifying the type resolution process to include the additional code generation for an existing language, but I am not sure if there are other options/which is better. I wrote the above in Haskell notation just for communication purposes. OO languages would be appreciated as well.

Many thanks,
Rob