Hello,
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 """
I dislike the fact that you can produce incoherent instances with that extension. How about a restricted version that only works on fresh types? f :: Bool -> Bool f b = N id < N id where -- N is a fresh type, unique to a particular application of f. newtype N = N (a -> b) instance Ord N where _ `compare` _ = LT This is sufficient for implicit configurations, and avoids the overlap of the new instances with existing instances. I don't know how much extra burden local type definitions like these would add. Bertram