Error messages involving type famllies (and/or [Nat] kinds?) mention type variables that don't appear anywhere in the error message nor the source code

Example (with GHC 9.6.2): https://play.haskell.org/saved/9flYF7i5

The error message starts with

Could not deduce ‘sh ~ (n : (sh1 ++ sh0))’

and then has

  Expected: AstShaped r ((n : sh1) ++ sh0)
    Actual: AstShaped r sh

which are the only two places in the known universe that mention sh0 (and n and sh1 don't appear in the source code either). From this, the programmer is supposed to deduce that GHC expects the following axiom to be added

    gcastWith (unsafeCoerce Refl :: sh :~: Take p sh ++ Drop p sh) $

This, times 100, makes writing shallowly-dependently typed Haskell programs very hard currently.

Even just listing all the constraints involving n, sh1 and sh0 (perhaps behind a flag) would help. Ideally, though, expressions with variables that don't come from source code should be replaced with expressions that only mention variables that do (a pity this is not decideable, most probably). Even rewriting only the expressions that are bare variables would help in many cases (and is probably fast enough).

In this case, the error message should say Could not deduce ‘sh ~ Take p sh ++ Drop p sh’ so that I, or an IDE, can just copy-paste into gcastWith . unsafeCoerce and move on.

Note the absence of plugins, though I had trouble minimising this further, because this behaviour is fragile. But it's very common for complex enough programs.