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.