Possible GHC bug with polymorphic kinds

Learn
1

I recently updated from GHC 9.6.7 to 9.12.2. However, when I did that, my custom error message failed to work with a polymorphic signature.

type MyError :: k 
type MyError = TypeError ('Text "ERROR")

This gives the error

<interactive>:35:20: error: [GHC-91028]
    • Expected kind ‘forall k. k’,
        but ‘TypeError ('Text "ERROR")’ has kind ‘b0’
      Cannot instantiate unification variable ‘b0’
      with a kind involving polytypes: forall k. k
    • In the type ‘TypeError ('Text "ERROR")’
      In the type declaration for ‘MyError’

However, when running :k MyError, I got MyError :: k and the warning gave MyError :: forall {k}. k. What is causing this? I think it worked with my old version. What should I do?
Another bug is whenever I use an infix constructor like ':| or ':<>: I get the -Woperator-whitespace warning. Again, what to do if I want to continue using the '?

2 Likes
2

I’m not sure what changed, but one thing you can do is enable the impredicative types extension: ImpredicativeTypes. That doesn’t work, I don’t know why not…

Alternatively you could also use TypeAbstractions:

{-# LANGUAGE DataKinds, TypeAbstractions #-}
import GHC.TypeError
type MyError :: forall k. k 
type MyError @k = TypeError ('Text "ERROR")

Perhaps @int-index can clarify what’s happening?

1 Like
3

That works, however another issue I am having is

Another bug is whenever I use an infix constructor like ':| or ':<>: I get the -Woperator-whitespace warning. Again, what to do if I want to continue using the '?

4

The problem is that

ghci> :k TypeError
TypeError :: forall b. ErrorMessage -> b

rather than

TypeError :: ErrorMessage -> forall b. b

so the synonym MyError needs to desugar to

type MyError :: forall k. k 
type MyError @k = TypeError @k ('Text "ERROR")

Note the @k on the RHS.

And if it’s used on the RHS, then it must be within the arity of the type synonym. Starting with GHC 9.10, arity is controlled explicitly with @-binders instead of guesswork on GHC’s part.

4 Likes
5

The -Woperator-whitespace issue is a bug, see #26471. Until it is fixed, my practical recommendation is to either avoid using the promotion tick or to disable -Woperator-whitespace.

4 Likes