Lambda the Ultimate

reading up on the ADT vs. OO debate, i came across an old comment that "function equality is actually decidable" if only some programming language would actually implement that particular approach. anybody understand that or know of any languages which might support it?

In a Haskell-like language, could we unify map :: (a -> b) -> [a] -> [b] and mapM :: (Monad m) => (a -> b) -> [a] -> m [b] (and all the similar pairs like filter/filterM, fold/foldM, ...) by adopting the monadic definitions with the "normal" (suffix-free) names and extending the type system to allow implicit conversion into and out of the Identity monad?

It seems that such conversions aren't as problematic as a general subtyping system, since proving confluence isn't a problem. We'd have to do something to prevent the typechecker from looping indefinitely trying to unify a with Identity a by way of Identity (Identity (Identity (Identity (... a ...)))), but I'm not sure that this would be a problem in practice. (Perhaps by avoiding an explicit transitivity-of-subtyping deduction rule, keeping the Identity-introduction, Identity-elimination, and reflexivity rules as the only deduction rules, and proving that transitivity follows from this?)

Are there other difficulties that this approach might cause? What sort of trickery might be needed to convince an optimizer over a typed intermediate language that the Identity introduction and elimination functions should have no operational effect? (Furthermore, is it true that they should have no effect, or is there a useful distinction between _|_ :: Identity a and Identity _|_ :: Identity a?)