#15568 closed bug (fixed)

Kind variables in type family aren't quantified in toposorted order

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler Version: 8.5
Keywords: TypeApplications, TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D5108
Wiki Page:

Description

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.

Change History (4)

comment:1 Changed 13 months ago by RyanGlScott

I figured out what caused this regression. The primary culprit is commit fa29df02a1b0b926afb2525a258172dcbf0ea460 (Refactor ConDecl: Trac #14529). In particular, this commit made a rather suspicious-looking change to bindHsQTyVars:

  • compiler/rename/RnTypes.hs

    diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs
    index dd66cd3..727744d 100644
    a b bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside 
    898905
    899906       ; let -- See Note [bindHsQTyVars examples] for what
    900907             -- all these various things are doing
    901              bndrs, kv_occs, implicit_bndr_kvs,
    902                     implicit_body_kvs, implicit_kvs :: [Located RdrName]
    903              bndrs             = map hsLTyVarLocName hs_tv_bndrs
    904              kv_occs           = body_kv_occs ++ bndr_kv_occs
    905              implicit_bndr_kvs = filter_occs rdr_env bndrs bndr_kv_occs
    906              implicit_body_kvs = filter_occs rdr_env (implicit_bndr_kvs ++ bndrs) body_kv_occs
     908             bndrs, kv_occs, implicit_kvs :: [Located RdrName]
     909             bndrs        = map hsLTyVarLocName hs_tv_bndrs
     910             kv_occs      = nubL (body_kv_occs ++ bndr_kv_occs)
     911             implicit_kvs = filter_occs rdr_env bndrs kv_occs
    907912                                 -- Deleting bndrs: See Note [Kind-variable ordering]
    908              implicit_kvs      = implicit_bndr_kvs ++ implicit_body_kvs
    909 

The value of implicit_kvs is what's important here, since it determines the order in which kind variables appear in type family kind signatures. In the commit before, we had:

implicit_kvs      = implicit_bndr_kvs ++ implicit_body_kvs

Which makes sense, as you'd expect the binder kind variables to appear before any kind variables from the body. But after that commit, we now have:

kv_occs      = nubL (body_kv_occs ++ bndr_kv_occs)
implicit_kvs = filter_occs rdr_env bndrs kv_occs

Now, we're putting all of the body kind variables before the binder ones!

(Note that the first commit in which you can actually see the forall k j. order instead of the old forall j k. order is actually 12794287174146f982257cdeffd491e3e23838dc (Quantify unfixed kind variables in CUSKs), but that's only because that commit changed the way kind variables were quantified to use quantifyTyVars instead of tyCoVarsOfTypeWellScoped, causing GHC to be more sensitive to the order of the kind variables in implicit_kvs.)

I think fixing this is a simple matter of defining kv_occs = nubL (bndr_kv_occs ++ body_kv_occs) instead. Patch incoming.

comment:2 Changed 13 months ago by RyanGlScott

Differential Rev(s): Phab:D5108
Status: newpatch

comment:3 Changed 13 months ago by Krzysztof Gogolewski <krz.gogolewski@…>

In 102284e/ghc:

Rename kind vars in left-to-right order in bindHsQTyVars

Summary:
When renaming kind variables in an `LHsQTyVars`, we were
erroneously putting all of the kind variables in the binders
//after// the kind variables in the body, resulting in #15568. The
fix is simple: just swap the order of these two around.

Test Plan: make test TEST=T15568

Reviewers: simonpj, bgamari, goldfire

Reviewed By: goldfire

Subscribers: goldfire, rwbarton, carter

GHC Trac Issues: #15568

Differential Revision: https://phabricator.haskell.org/D5108

comment:4 Changed 13 months ago by monoidal

Resolution: fixed
Status: patchclosed
Note: See TracTickets for help on using tickets.