Techniques for Tracing Constraints

Question

Here's the scenario: I've written some code with a type signature and GHC complains could not deduce x ~ y for some x and y. You can usually throw GHC a bone and simply add the isomorphism to the function constraints, but this is a bad idea for several reasons:

It does not emphasize understanding the code.
You can end up with 5 constraints where one would have sufficed (for example, if the 5 are implied by one more specific constraint)
You can end up with bogus constraints if you've done something wrong or if GHC is being unhelpful

I just spent several hours battling case 3. I'm playing with syntactic-2.0, and I was trying to define a domain-independent version of share, similar to the version defined in NanoFeldspar.hs.

I had this:

{-# LANGUAGE GADTs, FlexibleContexts, TypeOperators #-}
import Data.Syntactic

-- Based on NanoFeldspar.hs
data Let a where
    Let :: Let (a :-> (a -> b) :-> Full b)

share :: (Let :<: sup,
          Domain a ~ sup,
          Domain b ~ sup,
          SyntacticN (a -> (a -> b) -> b) fi) 
      => a -> (a -> b) -> a
share = sugarSym Let

and GHC could not deduce (Internal a) ~ (Internal b), which is certainly not what I was going for. So either I had written some code I didn't intend to (which required the constraint), or GHC wanted that constraint due to some other constraints I had written.

It turns out I needed to add (Syntactic a, Syntactic b, Syntactic (a->b)) to the constraint list, none of which imply (Internal a) ~ (Internal b). I basically stumbled upon the correct constraints; I still don't have a systematic way to find them.

My questions are:

Why did GHC propose that constraint? Nowhere in syntactic is there a constraint Internal a ~ Internal b, so where did GHC pull that from?
In general, what techniques can be used to trace the origin of a constraint which GHC believes it needs? Even for constraints that I can discover myself, my approach is essentially brute forcing the offending path by physically writing down recursive constraints. This approach is basically going down an infinite rabbit hole of constraints and is about the least efficient method I can imagine.

There's been some discussions on a type level debugger, but the general consensus seems to be showing the internal logic of the typechecker isn't going to help :/ As of right now Haskell's constraint solver is a crappy opaque logic language :) — Daniel Gratzer
Often it helps to just remove the type signature completely and let ghci tell you what it thinks the signature should be. — Tobias Brandt
Somehow a and b are bound - look at the type signature outside of your context - a -> (a -> b) -> a, not a -> (a -> b) -> b. Maybe that's it? With constraint solvers, they can influence the transitive equality anywhere, but the errors usually show a location "close" to where the constraint was induced. That would be cool though @jozefg - maybe annotating constraints with tags or something, to show where they came from? :s — Athan Clark

Cactus Cactus · Accepted Answer · 2016-01-15T06:11:29

First of all, your function has the wrong type; I am pretty sure it should be (without the context) a -> (a -> b) -> b. GHC 7.10 is somewhat more helpful in pointing that out, because with your original code, it complains about a missing constraint Internal (a -> b) ~ (Internal a -> Internal a). After fixing share's type, GHC 7.10 remains helpful in guiding us:

Could not deduce (Internal (a -> b) ~ (Internal a -> Internal b))
After adding the above, we get Could not deduce (sup ~ Domain (a -> b))
After adding that, we get Could not deduce (Syntactic a), Could not deduce (Syntactic b) and Could not deduce (Syntactic (a -> b))

After adding these three, it finally typechecks; so we end up with

share :: (Let :<: sup,
          Domain a ~ sup,
          Domain b ~ sup,
          Domain (a -> b) ~ sup,
          Internal (a -> b) ~ (Internal a -> Internal b),
          Syntactic a, Syntactic b, Syntactic (a -> b),
          SyntacticN (a -> (a -> b) -> b) fi)
      => a -> (a -> b) -> b
share = sugarSym Let

So I'd say GHC hasn't been useless in leading us.

As for your question about tracing where GHC gets its constraint requirements from, you could try GHC's debugging flags, in particular, -ddump-tc-trace, and then read through the resulting log to see where Internal (a -> b) ~ t and (Internal a -> Internal a) ~ t are added to the Wanted set, but that will be quite a long read.

Techniques for Tracing Constraints

2 Answers