Local evidence and type class instances

[Max Bolingbroke]

Hi GHC users,

Now that the Glorious New type checker can handle local evidence
seamlessly, is it a big implementation burden to extend it to deal
with local *type class instances* in addition to local *equality
constraints*?

For example, you could write this:

"""
f :: Bool
f = id < id
 where
   instance Ord (a -> b) where
     _ `compare` _ = LT
"""

Not only would this prevent instances from "leaking" into all
importing modules, but you could refer to *lexically scoped variables*
in the type class instance. This would let programmers implement e.g.
implicit configurations in the style of Kieslyov and Shan
(http://okmij.org/ftp/Haskell/types.html#Prepose) without any mad
hackery to tunnel pointers through the type system.

Of course, it could lead to problems. For example:

"""
newtype MyInt = MyInt { unMyInt :: Int }

f :: [Int] -> S.Set Int
f xs = S.map unMyInt $ S.toList (map MyInt xs)
 where
   instance Ord MyInt where
     x `compare` y = unMyInt x `compare` unMyInt y

g :: [Int] -> S.Set Int
g xs = S.map unMyInt $ S.toList (map MyInt xs)
 where
   instance Ord MyInt where
     x `compare` y = unMyInt y `compare` unMyInt x

main = do
 let s1 = f [1, 2]
     s2 = g [1, 2]
 print $ s1 == s2  -- prints False!
 print $ S.toList s1 == s2  -- prints True!
"""

I don't think this is a big problem. It would be up to the users of
this extension to do the Right Thing.

As Kieslyov and Shan point out, this extension also kills the
principal types property - but so do GADTs. Just add more type
signatures!

Are there big theoretical problems with this extension, or is it just
a lack of engineering effort that has prevented its implementation?

Max