Techniques for Tracing Constraints

by

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:

  1. It does not emphasize understanding the code.
  2. You can end up with 5 constraints where one would have sufficed (for example, if the 5 are implied by one more specific constraint)
  3. 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:

  1. Why did GHC propose that constraint? Nowhere in syntactic is there a constraint Internal a ~ Internal b, so where did GHC pull that from?
  2. 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.

2 Answers
2

Leave a Comment