GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order

Originally noticed in #14796 (closed). This program:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
module Bug where

import Data.Kind

data ECC ctx f a where
  ECC :: ctx => f a -> ECC ctx f a

f :: [()] -> ECC () [] ()
f = ECC @() @[] @()

Typechecks in GHC 8.2.2 and 8.4.1, but not in GHC HEAD:

$ ~/Software/ghc2/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:12:5: error:
    • Couldn't match type ‘()’ with ‘[]’
      Expected type: [()] -> ECC (() :: Constraint) [] ()
        Actual type: () [] -> ECC (() :: Constraint) () []
    • In the expression: ECC @() @[] @()
      In an equation for ‘f’: f = ECC @() @[] @()
   |
12 | f = ECC @() @[] @()
   |     ^^^^^^^^^^^^^^^

Bug.hs:12:10: error:
    • Expected kind ‘* -> *’, but ‘()’ has kind ‘*’
    • In the type ‘()’
      In the expression: ECC @() @[] @()
      In an equation for ‘f’: f = ECC @() @[] @()
   |
12 | f = ECC @() @[] @()
   |          ^^

Bug.hs:12:14: error:
    • Expecting one more argument to ‘[]’
      Expected a type, but ‘[]’ has kind ‘* -> *’
    • In the type ‘[]’
      In the expression: ECC @() @[] @()
      In an equation for ‘f’: f = ECC @() @[] @()
   |
12 | f = ECC @() @[] @()
   |              ^^

This is because the order of type variables for ECC has changed between GHC 8.4.1 and HEAD. In 8.4.1, it's

$ /opt/ghc/8.4.1/bin/ghci Bug.hs -XTypeApplications -fprint-explicit-foralls
GHCi, version 8.4.0.20180209: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
Ok, one module loaded.
λ> :type +v ECC
ECC
  :: forall (ctx :: Constraint) (f :: * -> *) a.
     ctx =>
     f a -> ECC ctx f a

In GHC HEAD, however, it's:

$ ~/Software/ghc2/inplace/bin/ghc-stage2 --interactive Bug.hs -XTypeApplications -fprint-explicit-foralls
GHCi, version 8.5.20180213: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
Ok, one module loaded.
λ> :type +v ECC
ECC
  :: forall (f :: * -> *) a (ctx :: Constraint).
     ctx =>
     f a -> ECC ctx f a

This regression was introduced in fa29df02 (Refactor ConDecl: Trac #14529 (closed)).

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	highest
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	simonpj
Operating system
Architecture