Proof of concept of explanations for instance resolution

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

On Wed, Oct 26, 2016 at 05:53:31PM -0700, Michael Sloan wrote:
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. [...] Thanks for reading! I hope we can address this UI concern in the future. I hope I've contributed something by demonstrating the possibility!
I think a "stack trace" of what GHC was thinking would be a great idea! I brought this idea here: https://mail.haskell.org/pipermail/haskell-cafe/2016-August/124622.html Tom
participants (2)
-
Michael Sloan
-
Tom Ellis