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.

## Best Solution

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

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.