[GHC] #14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order

[GHC]

#14808: GHC HEAD regression: GADT constructors no longer quantify tyvars in
topological order
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  highest        |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.5
  (Type checker)                     |
           Keywords:  GADTs          |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #14529, #14796
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Originally noticed in #14796. This program:

 {{{#!hs
 {-# 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 fa29df02a1b0b926afb2525a258172dcbf0ea460
 (Refactor ConDecl: Trac #14529).

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14808>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler