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.