Kind variables in type family aren't quantified in toposorted order
Recently, I noticed that an error message I was experiencing differs between GHC 8.4.3 and GHC 8.6.1+. Take this program:
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
import Data.Proxy
import GHC.Exts (Any)
type family F (a :: j) :: k
f :: Proxy a -> Proxy (F (a :: j) :: k)
f _ = Proxy :: Proxy (Any :: k)
On 8.4.3, you'll get:
$ /opt/ghc/8.4.3/bin/ghc Bug.hs -fprint-explicit-kinds
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:7: error:
• Couldn't match type ‘Any k’ with ‘F j k a’
Expected type: Proxy k (F j k a)
Actual type: Proxy k (Any k)
• In the expression: Proxy :: Proxy (Any :: k)
In an equation for ‘f’: f _ = Proxy :: Proxy (Any :: k)
• Relevant bindings include
f :: Proxy j a -> Proxy k (F j k a) (bound at Bug.hs:11:1)
|
11 | f _ = Proxy :: Proxy (Any :: k)
| ^^^^^^^^^^^^^^^^^^^^^^^^^
But on 8.6.1 and HEAD, you'll instead get:
$ /opt/ghc/8.6.1/bin/ghc Bug.hs -fprint-explicit-kinds
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:7: error:
• Couldn't match type ‘Any k’ with ‘F k j a’
Expected type: Proxy k (F k j a)
Actual type: Proxy k (Any k)
• In the expression: Proxy :: Proxy (Any :: k)
In an equation for ‘f’: f _ = Proxy :: Proxy (Any :: k)
• Relevant bindings include
f :: Proxy j a -> Proxy k (F k j a) (bound at Bug.hs:11:1)
|
11 | f _ = Proxy :: Proxy (Any :: k)
| ^^^^^^^^^^^^^^^^^^^^^^^^^
Notice that on 8.4.3, it displays F j k a
, but on 8.6.1, it displays F k j a
! After some digging, it turns out that this is because on 8.6.1, the order of F
's kind variables are quantified completely differently! On 8.4.3, we have:
λ> :kind F
F :: forall j k. j -> k
But on 8.6.1, we have:
λ> :kind F
F :: forall k j. j -> k
I would prefer the old behavior of 8.4.3, since j k
is what you get after performing a left-to-right, reverse topological sort on the kind variables of F
, which is consistent with how type signatures quantify their type variables. Currently, this quirk doesn't matter that much (except for error messages, as shown above), but if/when visible kind application is implemented, it'll be more noticeable.
Trac metadata
Trac field | Value |
---|---|
Version | 8.5 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |