[Haskell-cafe] Proof of concept of explanations for instance resolution

[Michael Sloan]

When typeclass machinery gets complicated, it can be hard to figure interpret
the meaning behind GHC's messages. In particular "Could not deduce ..." messages
often reference constraints that are deep in a tree of resolving typeclasses. I
think it would be great if GHC provided additional information for this
circumstance. In a way what we need is a "stack trace" of what GHC was thinking
about when yielding these type errors.

A couple years ago, I wrote an extremely hacky approach to yielding this
information through TH. It is quite imperfect, and only works with GHC 7.8. I've
realized that it's highly unlikely that this project will reach the level of
polish for it to be very usable in practice:
https://github.com/mgsloan/explain-instance

However, rather than allow that work to be wasted, I'd like to bring people's
attention to the problem in general, and how we might solve it in GHC. Along
with providing more information in type errors, this could also look like having
a ":explain" command in ghci.

Lets take Text.Printf as an example. The expression (printf "%d %d" (1 :: Int)
(2 :: A) :: String) has quite a bit of machinery behind it:

    printf :: (PrintfType r) => String -> r

    class PrintfType t
    instance (IsChar c) => PrintfType [c]
    instance (a ~ ()) => PrintfType (IO a)
    instance (PrintfArg a, PrintfType r) => PrintfType (a -> r)

    class PrintfArg a where
    instance PrintfArg Int where

With explain-instance, all we have to do is create a module with the following
in it:

    import ExplainInstance
    import Text.Printf
    $(explainInstance [t| PrintfType (Int -> Int -> String) |])

Then, upon running the generated main function, we get the following
explanation:

    instance (PrintfArg a, PrintfType r) => PrintfType (a -> r)
      with a ~ Int
           r ~ (Int -> [Char])

      instance PrintfArg Int

      instance (PrintfArg a, PrintfType r) => PrintfType (a -> r)
        with a ~ Int
             r ~ [Char]

        instance PrintfArg Int

        instance IsChar c => PrintfType ([c])
          with c ~ Char

          instance IsChar Char

This is the recursive tree of instance instantiation! It shows the instance
head, the particular types that it has been instantiated at in a made up "with"
clause.  Most importantly, it shows how the instance's constraints are also
satisfied, giving a tree for an explanation.

The implementation of this is irrelevant, but for the curious: it involves
recursively reifying all of the typeclasses, and then generating a whole new set
of typeclasses. These modified versions have the same heads (renamed) as the
original typeclasses, but just have one method, which yields a description of
the the types it has been instantiated with, via Typeable.

Well that's quite convenient!  I think it can really aid in understanding
typeclass machinery to be able to get this variety of trace through what GHC is
thinking when satisfying a constraint.  However, this is just half the problem -
what about type errors?  I played around with a solution to this via
UndecidableInstances, where it would create a base-case instance that represents
the error case.

Lets say I wanted to use (printf :: String -> A -> Int -> Maybe String) where A
is a type that is not an instance of PrintfArg. Another issue with this is that
the result type (Maybe String) is not allowed by PrintfType.

The output of

    $(explainInstanceError [t| PrintfType (A -> Int -> Maybe String) |])

is

    instance (PrintfArg a, PrintfType r) => PrintfType (a -> r)
      with a ~ A
           r ~ (Int -> Maybe [Char])

      ERROR instance PrintfArg a
        with a ~ A

      instance (PrintfArg a, PrintfType r) => PrintfType (a -> r)
        with a ~ Int
             r ~ Maybe [Char]

        instance PrintfArg Int

        ERROR instance PrintfType t
          with t ~ Maybe [Char]

This explains exactly where the problem is coming from in the typeclass
machinery.  If you're just looking at the type of printf, and see a `PrintfType`
constraint, it can be a total mystery as to why GHC is complaining about some
class we may or may not know about:

    No instance for (PrintfArg A) arising from a use of ‘printf’

Thanks for reading!  I hope we can address this UI concern in the future.  I
hope I've contributed something by demonstrating the possibility!

-Michael