@kl0tl @natefaubion I've gotten myself into a bit of a pickle here, and it's at the intersection of Coercible and polykinds.

There's one golden test that fails to match as a consequence of adding a skolem's kind to the type traversals. In that test, a NoInstanceFound error is raised due to a Coercible constraint not being solved. The constraint contains an unknown kind in a skolem, but otherwise doesn't contain unknowns. So the test output is now changed in two ways: first, it reports that there are unknown types in the instance head, and second, it lists a new unknown type. But, at least with the invisible kind applications that are the default in error messages, the unknown type never appears in the rest of the message, which is clearly not good. And I'm also not sure that it's good that an unknown in the kind of a skolem should trigger the ‘unknown type in instance head’ hint—can kinds have an effect on Coercible solving?

Is it true, then, that the original error message is the correct one to show? If so, how should we go about ignoring the kind unknowns? (If all kind information is irrelevant in Coercible solving, maybe we should suppress unknowns in KindApps as well? Or was there actually intent behind leaving skolem kinds untraversed?) And how should ignoring those unknowns interact with whether --verbose-errors is in use?

can kinds have an effect on Coercible solving?

The interaction solver only unifies kinds in order to emit KindsDoNotUnify errors instead of NoInstanceFound errors when solving heterogeneously kinded Coercible contraints, so annotating kinds to instantiate unknowns in Coercible constraints should never resolve NoInstanceFound errors.

Is it true, then, that the original error message is the correct one to show? If so, how should we go about ignoring the kind unknowns? (If all kind information is irrelevant in Coercible solving, maybe we should suppress unknowns in KindApps as well? Or was there actually intent behind leaving skolem kinds untraversed?)

I don’t know if skolem kinds were purposefuly ignored, but I think we can erase skolems kinds and kinds applications when computing whether insoluble Coercible constraints contain unknowns. That would get rid of the “The instance head contains unknown type variables. Consider adding a type annotation.” part of the error message.

And how should ignoring those unknowns interact with whether --verbose-errors is in use?

We could avoid listing “invisible” unknowns by erasing skolem kinds in insoluble Coercible constraints arguments and in ErrorSolvingConstraint hints, while stripping redundants hints, and since we erase kind applications when pretty printing types unless --verbose-errors is enabled I think we should erase them when simplifying error messages.

Also, do we hide kinds arguments of constraints on purpose?

Taking the failing CoercibleRepresentational test as example, should we display

 No type class instance was found for

-    Prim.Coerce.Coercible a2
+    Prim.Coerce.Coercible @t4 a2
                               b3

with --verbose-errors, and

 while solving type class constraint

-  Prim.Coerce.Coercible (Phantom @t0 a1)
+  Prim.Coerce.Coercible @Type (Phantom @t0 a1)
                               (Phantom @t2 b3)

in hints, regardless of the flag?

Also, do we hide kinds arguments of constraints on purpose?

The first behavior I think we have already (Edit: nope, see below); the second is due to not doing anything with the second wildcard in

Edit: The first behavior is similarly connected to the second wildcard in

@rhendric I just made an attempt at #1647 and the approach I am taking appears to work, although I have stumbled due to missing cases in onTypesInErrorMessage, in a similar vein to this. The subterms trick won't work here unfortunately; do you have any other suggestions? I'm tempted to pull in a syb dependency in the tests and just compare against everywhere.

Mind sharing your branch? subterms is just the shrinking strategy here, so even if that doesn't work (I imagine recursivelyShrink would be better) you could still have a functional test with forAll instead of forAllShrink.

👍 I'll make a PR

See #4337. Come to think of it, maybe everywhere isn't really what I'm after, I think I might just want gmapT, because I don't want to visit every Type node in this case, I just want to visit the Type values that are immediate children of the ErrorMessageHint and SimpleErrorMessage constructors.

I didn't see any new property-based tests in #4337, so I'm still not 100% sure I'm following you, but I think gmapQ is actually the thing to use here, assuming a test that does roughly this:

• create a Gen ErrorMessage by using genericArbitraryUG with an environment that includes a trivial SourceType generator—pure $ srcTypeLevelInt 0, perhaps
• use a function with onTypesInErrorMessage that increments each TypeLevelInt by 1
• use gmapQ on the result to collect all the types, and then assert that they're all TypeLevelInt _ 1 (to verify that none of them are unvisited or visited multiple times)

Oh, sorry, I don't yet have anything that tries to verify that onTypesInErrorMessage is hitting all of the cases it should be hitting. Thanks, I'll give that a try!