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 |