Local evidence and type class instances

[Bertram Felgenhauer]

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