GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20190707T18:04:02Zhttps://gitlab.haskell.org/ghc/ghc//issues/15579topNormaliseType is wrong20190707T18:04:02ZSimon Peyton JonestopNormaliseType is wrongI’m very puzzled about topNormaliseTYpe_maybe. Here it is:
```haskell
topNormaliseType_maybe env ty
= topNormaliseTypeX stepper mkTransCo ty
where
stepper = unwrapNewTypeStepper `composeSteppers` tyFamStepper
tyFamStepper rec_nts tc tys  Try to step a type/data family
= let (args_co, ntys) = normaliseTcArgs env Representational tc tys in
 NB: It's OK to use normaliseTcArgs here instead of
 normalise_tc_args (which takes the LiftingContext described
 in Note [Normalising types]) because the reduceTyFamApp below
 works only at top level. We'll never recur in this function
 after reducing the kind of a bound tyvar.
case reduceTyFamApp_maybe env Representational tc ntys of
Just (co, rhs) > NS_Step rec_nts rhs (args_co `mkTransCo` co)
_ > NS_Done
```
I have two puzzlements
1. First, it seems utterly wrong to normalise the arguments using Representational. Consider
```haskell
F (N Int)
where newtype N x = [x]
```
> We don’t want to reduce `(N Int)` to `[Int]`, and then try reducing `(F [Int])`!! That is totally bogus. Surely we should use (the roleaware) `normalise_tc_args` here?
1. I have literally no clue what `Note [Normalising types]` is all about. Moreover there is no Lifting Context passed to `normalise_tc_args`, so I don’t know what this stuff about `LiftingContext` is about. Is this historical baggage?
Richard and I discussed this. (1) is a bug; for (2) the comment is misleading and should be deleted.
Richard will do these things  and will add examples to the mysterious `Note [Normalising types]`I’m very puzzled about topNormaliseTYpe_maybe. Here it is:
```haskell
topNormaliseType_maybe env ty
= topNormaliseTypeX stepper mkTransCo ty
where
stepper = unwrapNewTypeStepper `composeSteppers` tyFamStepper
tyFamStepper rec_nts tc tys  Try to step a type/data family
= let (args_co, ntys) = normaliseTcArgs env Representational tc tys in
 NB: It's OK to use normaliseTcArgs here instead of
 normalise_tc_args (which takes the LiftingContext described
 in Note [Normalising types]) because the reduceTyFamApp below
 works only at top level. We'll never recur in this function
 after reducing the kind of a bound tyvar.
case reduceTyFamApp_maybe env Representational tc ntys of
Just (co, rhs) > NS_Step rec_nts rhs (args_co `mkTransCo` co)
_ > NS_Done
```
I have two puzzlements
1. First, it seems utterly wrong to normalise the arguments using Representational. Consider
```haskell
F (N Int)
where newtype N x = [x]
```
> We don’t want to reduce `(N Int)` to `[Int]`, and then try reducing `(F [Int])`!! That is totally bogus. Surely we should use (the roleaware) `normalise_tc_args` here?
1. I have literally no clue what `Note [Normalising types]` is all about. Moreover there is no Lifting Context passed to `normalise_tc_args`, so I don’t know what this stuff about `LiftingContext` is about. Is this historical baggage?
Richard and I discussed this. (1) is a bug; for (2) the comment is misleading and should be deleted.
Richard will do these things  and will add examples to the mysterious `Note [Normalising types]`8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/15419GHC 8.6.1 regression (buildKindCoercion)20190707T18:04:59ZRyan ScottGHC 8.6.1 regression (buildKindCoercion)The following program typechecks on GHC 8.4.1, but panics on GHC 8.6.1 and HEAD:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DefaultSignatures #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE TypeInType #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
data family Sing :: forall k. k > Type
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data instance Sing :: forall a b. (a, b) > Type where
STuple2 :: Sing x > Sing y > Sing '(x, y)
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t > Sing (f `Apply` t) }

newtype Par1 p = Par1 p
newtype K1 c p = K1 c
data (f :*: g) p = f p :*: g p
data instance Sing :: forall p. Par1 p > Type where
SPar1 :: Sing x > Sing ('Par1 x)
data instance Sing :: forall k c (p :: k). K1 c p > Type where
SK1 :: Sing x > Sing ('K1 x)
data instance Sing :: forall k (f :: k > Type) (g :: k > Type) (p :: k).
(f :*: g) p > Type where
(:%*:) :: Sing x > Sing y > Sing (x ':*: y)
class Generic1 (f :: k > Type) where
type Rep1 f :: k > Type
from1 :: f a > Rep1 f a
to1 :: Rep1 f a > f a
class PGeneric1 (f :: k > Type) where
type From1 (z :: f a) :: Rep1 f a
type To1 (z :: Rep1 f a) :: f a
class SGeneric1 (f :: k > Type) where
sFrom1 :: forall (a :: k) (z :: f a). Sing z > Sing (From1 z)
sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r > Sing (To1 r :: f a)
instance Generic1 ((,) a) where
type Rep1 ((,) a) = K1 a :*: Par1
from1 (x, y) = K1 x :*: Par1 y
to1 (K1 x :*: Par1 y) = (x, y)
instance PGeneric1 ((,) a) where
type From1 '(x, y) = 'K1 x ':*: 'Par1 y
type To1 ('K1 x ':*: 'Par1 y) = '(x, y)
instance SGeneric1 ((,) a) where
sFrom1 (STuple2 x y) = SK1 x :%*: SPar1 y
sTo1 (SK1 x :%*: SPar1 y) = STuple2 x y

type family GenericFmap (g :: a ~> b) (x :: f a) :: f b where
GenericFmap g x = To1 (Fmap g (From1 x))
class PFunctor (f :: Type > Type) where
type Fmap (g :: a ~> b) (x :: f a) :: f b
type Fmap g x = GenericFmap g x
class SFunctor (f :: Type > Type) where
sFmap :: forall a b (g :: a ~> b) (x :: f a).
Sing g > Sing x > Sing (Fmap g x)
default sFmap :: forall a b (g :: a ~> b) (x :: f a).
( SGeneric1 f, SFunctor (Rep1 f)
, Fmap g x ~ GenericFmap g x )
=> Sing g > Sing x > Sing (Fmap g x)
sFmap sg sx = sTo1 (sFmap sg (sFrom1 sx))

instance PFunctor Par1 where
type Fmap f ('Par1 x) = 'Par1 (f `Apply` x)
instance PFunctor (K1 c) where
type Fmap _ ('K1 x) = 'K1 x
instance PFunctor (f :*: g) where
type Fmap h (x ':*: y) = Fmap h x ':*: Fmap h y
instance SFunctor Par1 where
sFmap sf (SPar1 sx) = SPar1 (sf `applySing` sx)
instance SFunctor (K1 c) where
sFmap _ (SK1 sx) = SK1 sx
instance (SFunctor f, SFunctor g) => SFunctor (f :*: g) where
sFmap sh (sx :%*: sy) = sFmap sh sx :%*: sFmap sh sy

instance PFunctor ((,) a)
 The line below causes the panic
instance SFunctor ((,) a)
```
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.0.20180714 for x86_64unknownlinux):
buildKindCoercion
K1 a_a1Nj :*: Par1
Rep1 ((,) a_a1Nj)
*
a_a1Nj
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
pprPanic, called at compiler/types/Coercion.hs:2069:9 in ghc:Coercion
```
<details><summary>Trac metadata</summary>
 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  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC 8.6.1 regression (buildKindCoercion)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program typechecks on GHC 8.4.1, but panics on GHC 8.6.1 and HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\n{# LANGUAGE DefaultSignatures #}\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeOperators #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing :: forall k. k > Type\r\ndata TyFun :: Type > Type > Type\r\ntype a ~> b = TyFun a b > Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\n\r\ndata instance Sing :: forall a b. (a, b) > Type where\r\n STuple2 :: Sing x > Sing y > Sing '(x, y)\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t > Sing (f `Apply` t) }\r\n\r\n\r\n\r\nnewtype Par1 p = Par1 p\r\nnewtype K1 c p = K1 c\r\ndata (f :*: g) p = f p :*: g p\r\n\r\ndata instance Sing :: forall p. Par1 p > Type where\r\n SPar1 :: Sing x > Sing ('Par1 x)\r\ndata instance Sing :: forall k c (p :: k). K1 c p > Type where\r\n SK1 :: Sing x > Sing ('K1 x)\r\ndata instance Sing :: forall k (f :: k > Type) (g :: k > Type) (p :: k).\r\n (f :*: g) p > Type where\r\n (:%*:) :: Sing x > Sing y > Sing (x ':*: y)\r\n\r\nclass Generic1 (f :: k > Type) where\r\n type Rep1 f :: k > Type\r\n from1 :: f a > Rep1 f a\r\n to1 :: Rep1 f a > f a\r\n\r\nclass PGeneric1 (f :: k > Type) where\r\n type From1 (z :: f a) :: Rep1 f a\r\n type To1 (z :: Rep1 f a) :: f a\r\n\r\nclass SGeneric1 (f :: k > Type) where\r\n sFrom1 :: forall (a :: k) (z :: f a). Sing z > Sing (From1 z)\r\n sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r > Sing (To1 r :: f a)\r\n\r\ninstance Generic1 ((,) a) where\r\n type Rep1 ((,) a) = K1 a :*: Par1\r\n from1 (x, y) = K1 x :*: Par1 y\r\n to1 (K1 x :*: Par1 y) = (x, y)\r\n\r\ninstance PGeneric1 ((,) a) where\r\n type From1 '(x, y) = 'K1 x ':*: 'Par1 y\r\n type To1 ('K1 x ':*: 'Par1 y) = '(x, y)\r\n\r\ninstance SGeneric1 ((,) a) where\r\n sFrom1 (STuple2 x y) = SK1 x :%*: SPar1 y\r\n sTo1 (SK1 x :%*: SPar1 y) = STuple2 x y\r\n\r\n\r\n\r\ntype family GenericFmap (g :: a ~> b) (x :: f a) :: f b where\r\n GenericFmap g x = To1 (Fmap g (From1 x))\r\n\r\nclass PFunctor (f :: Type > Type) where\r\n type Fmap (g :: a ~> b) (x :: f a) :: f b\r\n type Fmap g x = GenericFmap g x\r\n\r\nclass SFunctor (f :: Type > Type) where\r\n sFmap :: forall a b (g :: a ~> b) (x :: f a).\r\n Sing g > Sing x > Sing (Fmap g x)\r\n default sFmap :: forall a b (g :: a ~> b) (x :: f a).\r\n ( SGeneric1 f, SFunctor (Rep1 f)\r\n , Fmap g x ~ GenericFmap g x )\r\n => Sing g > Sing x > Sing (Fmap g x)\r\n sFmap sg sx = sTo1 (sFmap sg (sFrom1 sx))\r\n\r\n\r\n\r\ninstance PFunctor Par1 where\r\n type Fmap f ('Par1 x) = 'Par1 (f `Apply` x)\r\ninstance PFunctor (K1 c) where\r\n type Fmap _ ('K1 x) = 'K1 x\r\ninstance PFunctor (f :*: g) where\r\n type Fmap h (x ':*: y) = Fmap h x ':*: Fmap h y\r\n\r\ninstance SFunctor Par1 where\r\n sFmap sf (SPar1 sx) = SPar1 (sf `applySing` sx)\r\ninstance SFunctor (K1 c) where\r\n sFmap _ (SK1 sx) = SK1 sx\r\ninstance (SFunctor f, SFunctor g) => SFunctor (f :*: g) where\r\n sFmap sh (sx :%*: sy) = sFmap sh sx :%*: sFmap sh sy\r\n\r\n\r\n\r\ninstance PFunctor ((,) a)\r\n The line below causes the panic\r\ninstance SFunctor ((,) a)\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.0.20180714 for x86_64unknownlinux):\r\n buildKindCoercion\r\n K1 a_a1Nj :*: Par1\r\n Rep1 ((,) a_a1Nj)\r\n *\r\n a_a1Nj\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Coercion.hs:2069:9 in ghc:Coercion\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >The following program typechecks on GHC 8.4.1, but panics on GHC 8.6.1 and HEAD:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DefaultSignatures #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE TypeInType #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
data family Sing :: forall k. k > Type
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data instance Sing :: forall a b. (a, b) > Type where
STuple2 :: Sing x > Sing y > Sing '(x, y)
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t > Sing (f `Apply` t) }

newtype Par1 p = Par1 p
newtype K1 c p = K1 c
data (f :*: g) p = f p :*: g p
data instance Sing :: forall p. Par1 p > Type where
SPar1 :: Sing x > Sing ('Par1 x)
data instance Sing :: forall k c (p :: k). K1 c p > Type where
SK1 :: Sing x > Sing ('K1 x)
data instance Sing :: forall k (f :: k > Type) (g :: k > Type) (p :: k).
(f :*: g) p > Type where
(:%*:) :: Sing x > Sing y > Sing (x ':*: y)
class Generic1 (f :: k > Type) where
type Rep1 f :: k > Type
from1 :: f a > Rep1 f a
to1 :: Rep1 f a > f a
class PGeneric1 (f :: k > Type) where
type From1 (z :: f a) :: Rep1 f a
type To1 (z :: Rep1 f a) :: f a
class SGeneric1 (f :: k > Type) where
sFrom1 :: forall (a :: k) (z :: f a). Sing z > Sing (From1 z)
sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r > Sing (To1 r :: f a)
instance Generic1 ((,) a) where
type Rep1 ((,) a) = K1 a :*: Par1
from1 (x, y) = K1 x :*: Par1 y
to1 (K1 x :*: Par1 y) = (x, y)
instance PGeneric1 ((,) a) where
type From1 '(x, y) = 'K1 x ':*: 'Par1 y
type To1 ('K1 x ':*: 'Par1 y) = '(x, y)
instance SGeneric1 ((,) a) where
sFrom1 (STuple2 x y) = SK1 x :%*: SPar1 y
sTo1 (SK1 x :%*: SPar1 y) = STuple2 x y

type family GenericFmap (g :: a ~> b) (x :: f a) :: f b where
GenericFmap g x = To1 (Fmap g (From1 x))
class PFunctor (f :: Type > Type) where
type Fmap (g :: a ~> b) (x :: f a) :: f b
type Fmap g x = GenericFmap g x
class SFunctor (f :: Type > Type) where
sFmap :: forall a b (g :: a ~> b) (x :: f a).
Sing g > Sing x > Sing (Fmap g x)
default sFmap :: forall a b (g :: a ~> b) (x :: f a).
( SGeneric1 f, SFunctor (Rep1 f)
, Fmap g x ~ GenericFmap g x )
=> Sing g > Sing x > Sing (Fmap g x)
sFmap sg sx = sTo1 (sFmap sg (sFrom1 sx))

instance PFunctor Par1 where
type Fmap f ('Par1 x) = 'Par1 (f `Apply` x)
instance PFunctor (K1 c) where
type Fmap _ ('K1 x) = 'K1 x
instance PFunctor (f :*: g) where
type Fmap h (x ':*: y) = Fmap h x ':*: Fmap h y
instance SFunctor Par1 where
sFmap sf (SPar1 sx) = SPar1 (sf `applySing` sx)
instance SFunctor (K1 c) where
sFmap _ (SK1 sx) = SK1 sx
instance (SFunctor f, SFunctor g) => SFunctor (f :*: g) where
sFmap sh (sx :%*: sy) = sFmap sh sx :%*: sFmap sh sy

instance PFunctor ((,) a)
 The line below causes the panic
instance SFunctor ((,) a)
```
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.0.20180714 for x86_64unknownlinux):
buildKindCoercion
K1 a_a1Nj :*: Par1
Rep1 ((,) a_a1Nj)
*
a_a1Nj
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
pprPanic, called at compiler/types/Coercion.hs:2069:9 in ghc:Coercion
```
<details><summary>Trac metadata</summary>
 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  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC 8.6.1 regression (buildKindCoercion)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program typechecks on GHC 8.4.1, but panics on GHC 8.6.1 and HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\n{# LANGUAGE DefaultSignatures #}\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeOperators #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing :: forall k. k > Type\r\ndata TyFun :: Type > Type > Type\r\ntype a ~> b = TyFun a b > Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\n\r\ndata instance Sing :: forall a b. (a, b) > Type where\r\n STuple2 :: Sing x > Sing y > Sing '(x, y)\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t > Sing (f `Apply` t) }\r\n\r\n\r\n\r\nnewtype Par1 p = Par1 p\r\nnewtype K1 c p = K1 c\r\ndata (f :*: g) p = f p :*: g p\r\n\r\ndata instance Sing :: forall p. Par1 p > Type where\r\n SPar1 :: Sing x > Sing ('Par1 x)\r\ndata instance Sing :: forall k c (p :: k). K1 c p > Type where\r\n SK1 :: Sing x > Sing ('K1 x)\r\ndata instance Sing :: forall k (f :: k > Type) (g :: k > Type) (p :: k).\r\n (f :*: g) p > Type where\r\n (:%*:) :: Sing x > Sing y > Sing (x ':*: y)\r\n\r\nclass Generic1 (f :: k > Type) where\r\n type Rep1 f :: k > Type\r\n from1 :: f a > Rep1 f a\r\n to1 :: Rep1 f a > f a\r\n\r\nclass PGeneric1 (f :: k > Type) where\r\n type From1 (z :: f a) :: Rep1 f a\r\n type To1 (z :: Rep1 f a) :: f a\r\n\r\nclass SGeneric1 (f :: k > Type) where\r\n sFrom1 :: forall (a :: k) (z :: f a). Sing z > Sing (From1 z)\r\n sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r > Sing (To1 r :: f a)\r\n\r\ninstance Generic1 ((,) a) where\r\n type Rep1 ((,) a) = K1 a :*: Par1\r\n from1 (x, y) = K1 x :*: Par1 y\r\n to1 (K1 x :*: Par1 y) = (x, y)\r\n\r\ninstance PGeneric1 ((,) a) where\r\n type From1 '(x, y) = 'K1 x ':*: 'Par1 y\r\n type To1 ('K1 x ':*: 'Par1 y) = '(x, y)\r\n\r\ninstance SGeneric1 ((,) a) where\r\n sFrom1 (STuple2 x y) = SK1 x :%*: SPar1 y\r\n sTo1 (SK1 x :%*: SPar1 y) = STuple2 x y\r\n\r\n\r\n\r\ntype family GenericFmap (g :: a ~> b) (x :: f a) :: f b where\r\n GenericFmap g x = To1 (Fmap g (From1 x))\r\n\r\nclass PFunctor (f :: Type > Type) where\r\n type Fmap (g :: a ~> b) (x :: f a) :: f b\r\n type Fmap g x = GenericFmap g x\r\n\r\nclass SFunctor (f :: Type > Type) where\r\n sFmap :: forall a b (g :: a ~> b) (x :: f a).\r\n Sing g > Sing x > Sing (Fmap g x)\r\n default sFmap :: forall a b (g :: a ~> b) (x :: f a).\r\n ( SGeneric1 f, SFunctor (Rep1 f)\r\n , Fmap g x ~ GenericFmap g x )\r\n => Sing g > Sing x > Sing (Fmap g x)\r\n sFmap sg sx = sTo1 (sFmap sg (sFrom1 sx))\r\n\r\n\r\n\r\ninstance PFunctor Par1 where\r\n type Fmap f ('Par1 x) = 'Par1 (f `Apply` x)\r\ninstance PFunctor (K1 c) where\r\n type Fmap _ ('K1 x) = 'K1 x\r\ninstance PFunctor (f :*: g) where\r\n type Fmap h (x ':*: y) = Fmap h x ':*: Fmap h y\r\n\r\ninstance SFunctor Par1 where\r\n sFmap sf (SPar1 sx) = SPar1 (sf `applySing` sx)\r\ninstance SFunctor (K1 c) where\r\n sFmap _ (SK1 sx) = SK1 sx\r\ninstance (SFunctor f, SFunctor g) => SFunctor (f :*: g) where\r\n sFmap sh (sx :%*: sy) = sFmap sh sx :%*: sFmap sh sy\r\n\r\n\r\n\r\ninstance PFunctor ((,) a)\r\n The line below causes the panic\r\ninstance SFunctor ((,) a)\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.0.20180714 for x86_64unknownlinux):\r\n buildKindCoercion\r\n K1 a_a1Nj :*: Par1\r\n Rep1 ((,) a_a1Nj)\r\n *\r\n a_a1Nj\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Coercion.hs:2069:9 in ghc:Coercion\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/15282Document how equalitybearing constructors are promoted in Core20190707T18:13:27ZRyan ScottDocument how equalitybearing constructors are promoted in CoreIn [D4728](https://phabricator.haskell.org/D4728), Simon was utterly baffled as to how one could promote the `MkT` constructor in:
```hs
data T a where
MkT :: (a ~ Int) => T a
```
Richard knows the inner machinations of how this works (including what coercions are used in the Core that `'MkT` desugars to), but not many others do. Simon requested that Richard document this knowledge in a Note somewhere. This ticket exists to keep track of this request.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  goldfire 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Document how equalitybearing constructors are promoted in Core","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"In Phab:D4728, Simon was utterly baffled as to how one could promote the `MkT` constructor in:\r\n\r\n{{{#!hs\r\ndata T a where\r\n MkT :: (a ~ Int) => T a\r\n}}}\r\n\r\nRichard knows the inner machinations of how this works (including what coercions are used in the Core that `'MkT` desugars to), but not many others do. Simon requested that Richard document this knowledge in a Note somewhere. This ticket exists to keep track of this request.","type_of_failure":"OtherFailure","blocking":[]} >In [D4728](https://phabricator.haskell.org/D4728), Simon was utterly baffled as to how one could promote the `MkT` constructor in:
```hs
data T a where
MkT :: (a ~ Int) => T a
```
Richard knows the inner machinations of how this works (including what coercions are used in the Core that `'MkT` desugars to), but not many others do. Simon requested that Richard document this knowledge in a Note somewhere. This ticket exists to keep track of this request.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  goldfire 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Document how equalitybearing constructors are promoted in Core","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"In Phab:D4728, Simon was utterly baffled as to how one could promote the `MkT` constructor in:\r\n\r\n{{{#!hs\r\ndata T a where\r\n MkT :: (a ~ Int) => T a\r\n}}}\r\n\r\nRichard knows the inner machinations of how this works (including what coercions are used in the Core that `'MkT` desugars to), but not many others do. Simon requested that Richard document this knowledge in a Note somewhere. This ticket exists to keep track of this request.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/15142GHC HEAD regression: tcTyVarDetails20190707T18:14:05ZRyan ScottGHC HEAD regression: tcTyVarDetailsThis regression prevents the `genericlens` library from building. Here is a minimized test case:
```hs
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
class ListTuple (tuple :: Type) (as :: [(k, Type)]) where
type ListToTuple as :: Type
```
On GHC 8.4.2, this compiles, but on GHC HEAD, it panics:
```
$ ~/Software/ghc/inplace/bin/ghcstage2 Bug.hs[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.5.20180511 for x86_64unknownlinux):
tcTyVarDetails
co_aWx :: (k_aWt[tau:2] :: *) ~# (* :: *)
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable
pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var
```
<details><summary>Trac metadata</summary>
 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  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC HEAD regression: tcTyVarDetails","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This regression prevents the `genericlens` library from building. Here is a minimized test case:\r\n\r\n{{{#!hs\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nclass ListTuple (tuple :: Type) (as :: [(k, Type)]) where\r\n type ListToTuple as :: Type\r\n}}}\r\n\r\nOn GHC 8.4.2, this compiles, but on GHC HEAD, it panics:\r\n\r\n{{{\r\n$ ~/Software/ghc/inplace/bin/ghcstage2 Bug.hs[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.5.20180511 for x86_64unknownlinux):\r\n tcTyVarDetails\r\n co_aWx :: (k_aWt[tau:2] :: *) ~# (* :: *)\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable\r\n pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >This regression prevents the `genericlens` library from building. Here is a minimized test case:
```hs
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
class ListTuple (tuple :: Type) (as :: [(k, Type)]) where
type ListToTuple as :: Type
```
On GHC 8.4.2, this compiles, but on GHC HEAD, it panics:
```
$ ~/Software/ghc/inplace/bin/ghcstage2 Bug.hs[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.5.20180511 for x86_64unknownlinux):
tcTyVarDetails
co_aWx :: (k_aWt[tau:2] :: *) ~# (* :: *)
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable
pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var
```
<details><summary>Trac metadata</summary>
 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  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC HEAD regression: tcTyVarDetails","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This regression prevents the `genericlens` library from building. Here is a minimized test case:\r\n\r\n{{{#!hs\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nclass ListTuple (tuple :: Type) (as :: [(k, Type)]) where\r\n type ListToTuple as :: Type\r\n}}}\r\n\r\nOn GHC 8.4.2, this compiles, but on GHC HEAD, it panics:\r\n\r\n{{{\r\n$ ~/Software/ghc/inplace/bin/ghcstage2 Bug.hs[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.5.20180511 for x86_64unknownlinux):\r\n tcTyVarDetails\r\n co_aWx :: (k_aWt[tau:2] :: *) ~# (* :: *)\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable\r\n pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/14991GHC HEAD regression involving TYPEs in type families20190707T18:14:46ZRyan ScottGHC HEAD regression involving TYPEs in type familiesThis program typechecks on GHC 8.2.2 and 8.4.1:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
type family Promote (k :: Type) :: Type
type family PromoteX (a :: k) :: Promote k
type family Demote (k :: Type) :: Type
type family DemoteX (a :: k) :: Demote k

 Type

type instance Demote Type = Type
type instance Promote Type = Type
type instance DemoteX (a :: Type) = Demote a
type instance PromoteX (a :: Type) = Promote a

 Arrows

data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type instance Demote (a ~> b) = DemoteX a > DemoteX b
type instance Promote (a > b) = PromoteX a ~> PromoteX b
```
However, it fails to typecheck on GHC HEAD:
```
$ ~/Software/ghc/inplace/bin/ghcstage2 interactive Bug.hs
GHCi, version 8.5.20180401: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:34:34: error:
• Expected a type, but ‘PromoteX a’ has kind ‘Promote (TYPE t0)’
• In the first argument of ‘(~>)’, namely ‘PromoteX a’
In the type ‘PromoteX a ~> PromoteX b’
In the type instance declaration for ‘Promote’

34  type instance Promote (a > b) = PromoteX a ~> PromoteX b
 ^^^^^^^^^^
Bug.hs:34:48: error:
• Expected a type, but ‘PromoteX b’ has kind ‘Promote (TYPE t1)’
• In the second argument of ‘(~>)’, namely ‘PromoteX b’
In the type ‘PromoteX a ~> PromoteX b’
In the type instance declaration for ‘Promote’

34  type instance Promote (a > b) = PromoteX a ~> PromoteX b
 ^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC HEAD regression involving TYPEs in type families","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program typechecks on GHC 8.2.2 and 8.4.1:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype family Promote (k :: Type) :: Type\r\ntype family PromoteX (a :: k) :: Promote k\r\n\r\ntype family Demote (k :: Type) :: Type\r\ntype family DemoteX (a :: k) :: Demote k\r\n\r\n\r\n Type\r\n\r\n\r\ntype instance Demote Type = Type\r\ntype instance Promote Type = Type\r\n\r\ntype instance DemoteX (a :: Type) = Demote a\r\ntype instance PromoteX (a :: Type) = Promote a\r\n\r\n\r\n Arrows\r\n\r\n\r\ndata TyFun :: Type > Type > Type\r\ntype a ~> b = TyFun a b > Type\r\ninfixr 0 ~>\r\n\r\ntype instance Demote (a ~> b) = DemoteX a > DemoteX b\r\ntype instance Promote (a > b) = PromoteX a ~> PromoteX b\r\n}}}\r\n\r\nHowever, it fails to typecheck on GHC HEAD:\r\n\r\n{{{\r\n$ ~/Software/ghc/inplace/bin/ghcstage2 interactive Bug.hs\r\nGHCi, version 8.5.20180401: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:34:34: error:\r\n • Expected a type, but ‘PromoteX a’ has kind ‘Promote (TYPE t0)’\r\n • In the first argument of ‘(~>)’, namely ‘PromoteX a’\r\n In the type ‘PromoteX a ~> PromoteX b’\r\n In the type instance declaration for ‘Promote’\r\n \r\n34  type instance Promote (a > b) = PromoteX a ~> PromoteX b\r\n  ^^^^^^^^^^\r\n\r\nBug.hs:34:48: error:\r\n • Expected a type, but ‘PromoteX b’ has kind ‘Promote (TYPE t1)’\r\n • In the second argument of ‘(~>)’, namely ‘PromoteX b’\r\n In the type ‘PromoteX a ~> PromoteX b’\r\n In the type instance declaration for ‘Promote’\r\n \r\n34  type instance Promote (a > b) = PromoteX a ~> PromoteX b\r\n  ^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >This program typechecks on GHC 8.2.2 and 8.4.1:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
type family Promote (k :: Type) :: Type
type family PromoteX (a :: k) :: Promote k
type family Demote (k :: Type) :: Type
type family DemoteX (a :: k) :: Demote k

 Type

type instance Demote Type = Type
type instance Promote Type = Type
type instance DemoteX (a :: Type) = Demote a
type instance PromoteX (a :: Type) = Promote a

 Arrows

data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type instance Demote (a ~> b) = DemoteX a > DemoteX b
type instance Promote (a > b) = PromoteX a ~> PromoteX b
```
However, it fails to typecheck on GHC HEAD:
```
$ ~/Software/ghc/inplace/bin/ghcstage2 interactive Bug.hs
GHCi, version 8.5.20180401: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:34:34: error:
• Expected a type, but ‘PromoteX a’ has kind ‘Promote (TYPE t0)’
• In the first argument of ‘(~>)’, namely ‘PromoteX a’
In the type ‘PromoteX a ~> PromoteX b’
In the type instance declaration for ‘Promote’

34  type instance Promote (a > b) = PromoteX a ~> PromoteX b
 ^^^^^^^^^^
Bug.hs:34:48: error:
• Expected a type, but ‘PromoteX b’ has kind ‘Promote (TYPE t1)’
• In the second argument of ‘(~>)’, namely ‘PromoteX b’
In the type ‘PromoteX a ~> PromoteX b’
In the type instance declaration for ‘Promote’

34  type instance Promote (a > b) = PromoteX a ~> PromoteX b
 ^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC HEAD regression involving TYPEs in type families","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program typechecks on GHC 8.2.2 and 8.4.1:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype family Promote (k :: Type) :: Type\r\ntype family PromoteX (a :: k) :: Promote k\r\n\r\ntype family Demote (k :: Type) :: Type\r\ntype family DemoteX (a :: k) :: Demote k\r\n\r\n\r\n Type\r\n\r\n\r\ntype instance Demote Type = Type\r\ntype instance Promote Type = Type\r\n\r\ntype instance DemoteX (a :: Type) = Demote a\r\ntype instance PromoteX (a :: Type) = Promote a\r\n\r\n\r\n Arrows\r\n\r\n\r\ndata TyFun :: Type > Type > Type\r\ntype a ~> b = TyFun a b > Type\r\ninfixr 0 ~>\r\n\r\ntype instance Demote (a ~> b) = DemoteX a > DemoteX b\r\ntype instance Promote (a > b) = PromoteX a ~> PromoteX b\r\n}}}\r\n\r\nHowever, it fails to typecheck on GHC HEAD:\r\n\r\n{{{\r\n$ ~/Software/ghc/inplace/bin/ghcstage2 interactive Bug.hs\r\nGHCi, version 8.5.20180401: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:34:34: error:\r\n • Expected a type, but ‘PromoteX a’ has kind ‘Promote (TYPE t0)’\r\n • In the first argument of ‘(~>)’, namely ‘PromoteX a’\r\n In the type ‘PromoteX a ~> PromoteX b’\r\n In the type instance declaration for ‘Promote’\r\n \r\n34  type instance Promote (a > b) = PromoteX a ~> PromoteX b\r\n  ^^^^^^^^^^\r\n\r\nBug.hs:34:48: error:\r\n • Expected a type, but ‘PromoteX b’ has kind ‘Promote (TYPE t1)’\r\n • In the second argument of ‘(~>)’, namely ‘PromoteX b’\r\n In the type ‘PromoteX a ~> PromoteX b’\r\n In the type instance declaration for ‘Promote’\r\n \r\n34  type instance Promote (a > b) = PromoteX a ~> PromoteX b\r\n  ^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/14808GHC HEAD regression: GADT constructors no longer quantify tyvars in topologic...20190707T18:15:30ZRyan ScottGHC HEAD regression: GADT constructors no longer quantify tyvars in topological orderOriginally 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/ghcstage2 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 fprintexplicitforalls
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/ghcstage2 interactive Bug.hs XTypeApplications fprintexplicitforalls
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).
<details><summary>Trac metadata</summary>
 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  
</details>
<! {"blocked_by":[],"summary":"GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["GADTs"],"differentials":[],"test_case":"","architecture":"","cc":["simonpj"],"type":"Bug","description":"Originally noticed in #14796. This program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE TypeApplications #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata ECC ctx f a where\r\n ECC :: ctx => f a > ECC ctx f a\r\n\r\nf :: [()] > ECC () [] ()\r\nf = ECC @() @[] @()\r\n}}}\r\n\r\nTypechecks in GHC 8.2.2 and 8.4.1, but not in GHC HEAD:\r\n\r\n{{{\r\n$ ~/Software/ghc2/inplace/bin/ghcstage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:12:5: error:\r\n • Couldn't match type ‘()’ with ‘[]’\r\n Expected type: [()] > ECC (() :: Constraint) [] ()\r\n Actual type: () [] > ECC (() :: Constraint) () []\r\n • In the expression: ECC @() @[] @()\r\n In an equation for ‘f’: f = ECC @() @[] @()\r\n \r\n12  f = ECC @() @[] @()\r\n  ^^^^^^^^^^^^^^^\r\n\r\nBug.hs:12:10: error:\r\n • Expected kind ‘* > *’, but ‘()’ has kind ‘*’\r\n • In the type ‘()’\r\n In the expression: ECC @() @[] @()\r\n In an equation for ‘f’: f = ECC @() @[] @()\r\n \r\n12  f = ECC @() @[] @()\r\n  ^^\r\n\r\nBug.hs:12:14: error:\r\n • Expecting one more argument to ‘[]’\r\n Expected a type, but ‘[]’ has kind ‘* > *’\r\n • In the type ‘[]’\r\n In the expression: ECC @() @[] @()\r\n In an equation for ‘f’: f = ECC @() @[] @()\r\n \r\n12  f = ECC @() @[] @()\r\n  ^^\r\n}}}\r\n\r\nThis is because the order of type variables for `ECC` has changed between GHC 8.4.1 and HEAD. In 8.4.1, it's\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghci Bug.hs XTypeApplications fprintexplicitforalls\r\nGHCi, version 8.4.0.20180209: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nOk, one module loaded.\r\nλ> :type +v ECC\r\nECC\r\n :: forall (ctx :: Constraint) (f :: * > *) a.\r\n ctx =>\r\n f a > ECC ctx f a\r\n}}}\r\n\r\nIn GHC HEAD, however, it's:\r\n\r\n{{{\r\n$ ~/Software/ghc2/inplace/bin/ghcstage2 interactive Bug.hs XTypeApplications fprintexplicitforalls\r\nGHCi, version 8.5.20180213: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nOk, one module loaded.\r\nλ> :type +v ECC\r\nECC\r\n :: forall (f :: * > *) a (ctx :: Constraint).\r\n ctx =>\r\n f a > ECC ctx f a\r\n}}}\r\n\r\nThis regression was introduced in fa29df02a1b0b926afb2525a258172dcbf0ea460 (Refactor ConDecl: Trac #14529).","type_of_failure":"OtherFailure","blocking":[]} >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/ghcstage2 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 fprintexplicitforalls
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/ghcstage2 interactive Bug.hs XTypeApplications fprintexplicitforalls
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).
<details><summary>Trac metadata</summary>
 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  
</details>
<! {"blocked_by":[],"summary":"GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["GADTs"],"differentials":[],"test_case":"","architecture":"","cc":["simonpj"],"type":"Bug","description":"Originally noticed in #14796. This program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE TypeApplications #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata ECC ctx f a where\r\n ECC :: ctx => f a > ECC ctx f a\r\n\r\nf :: [()] > ECC () [] ()\r\nf = ECC @() @[] @()\r\n}}}\r\n\r\nTypechecks in GHC 8.2.2 and 8.4.1, but not in GHC HEAD:\r\n\r\n{{{\r\n$ ~/Software/ghc2/inplace/bin/ghcstage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:12:5: error:\r\n • Couldn't match type ‘()’ with ‘[]’\r\n Expected type: [()] > ECC (() :: Constraint) [] ()\r\n Actual type: () [] > ECC (() :: Constraint) () []\r\n • In the expression: ECC @() @[] @()\r\n In an equation for ‘f’: f = ECC @() @[] @()\r\n \r\n12  f = ECC @() @[] @()\r\n  ^^^^^^^^^^^^^^^\r\n\r\nBug.hs:12:10: error:\r\n • Expected kind ‘* > *’, but ‘()’ has kind ‘*’\r\n • In the type ‘()’\r\n In the expression: ECC @() @[] @()\r\n In an equation for ‘f’: f = ECC @() @[] @()\r\n \r\n12  f = ECC @() @[] @()\r\n  ^^\r\n\r\nBug.hs:12:14: error:\r\n • Expecting one more argument to ‘[]’\r\n Expected a type, but ‘[]’ has kind ‘* > *’\r\n • In the type ‘[]’\r\n In the expression: ECC @() @[] @()\r\n In an equation for ‘f’: f = ECC @() @[] @()\r\n \r\n12  f = ECC @() @[] @()\r\n  ^^\r\n}}}\r\n\r\nThis is because the order of type variables for `ECC` has changed between GHC 8.4.1 and HEAD. In 8.4.1, it's\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghci Bug.hs XTypeApplications fprintexplicitforalls\r\nGHCi, version 8.4.0.20180209: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nOk, one module loaded.\r\nλ> :type +v ECC\r\nECC\r\n :: forall (ctx :: Constraint) (f :: * > *) a.\r\n ctx =>\r\n f a > ECC ctx f a\r\n}}}\r\n\r\nIn GHC HEAD, however, it's:\r\n\r\n{{{\r\n$ ~/Software/ghc2/inplace/bin/ghcstage2 interactive Bug.hs XTypeApplications fprintexplicitforalls\r\nGHCi, version 8.5.20180213: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nOk, one module loaded.\r\nλ> :type +v ECC\r\nECC\r\n :: forall (f :: * > *) a (ctx :: Constraint).\r\n ctx =>\r\n f a > ECC ctx f a\r\n}}}\r\n\r\nThis regression was introduced in fa29df02a1b0b926afb2525a258172dcbf0ea460 (Refactor ConDecl: Trac #14529).","type_of_failure":"OtherFailure","blocking":[]} >8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/14737Improve performance of Simplify.simplCast20190923T07:37:55ZTobias Dammerstdammers@gmail.comImprove performance of Simplify.simplCastSplitting off task 3 from #11735. When compiling [https://ghc.haskell.org/trac/ghc/attachment/ticket/14683/Grammar.hs](https://ghc.haskell.org/trac/ghc/attachment/ticket/14683/Grammar.hs), `simplCast` eats up more execution time than we think it should.
From [https://ghc.haskell.org/trac/ghc/ticket/11735\#comment:10](https://ghc.haskell.org/trac/ghc/ticket/11735#comment:10):
> Something is clearly wrong with `Simplify.simplCast`. I think I know what it is. Given
>
> ```
> (fun > co) @t1 @t2 ... @tn
> ```
>
> we will call `pushCoTyArg` `n` times, and hence does `n` singleton substitutions, via the `n` calls to `piResultTy`.
>
> Solution: gather up those type arguments (easy) and define
>
> ```
> pushCoTyArgs :: Coercion > [Type] > Maybe ([Type], Coercion)
> ```
And [https://ghc.haskell.org/trac/ghc/ticket/11735\#comment:41](https://ghc.haskell.org/trac/ghc/ticket/11735#comment:41):
> OK. I looked at `pushCoTyArg` and friends, and I have a very simple solution: just move the `isReflexiveCo` case in `addCoerce` (a local function within `Simplify.simplCast`) to the top. That should do it. Then `pushCoTyArg` is never called with a reflexive coercion, and so the `piResultTy` case won't happen.
>
> Now, `pushCoArgs` might still call `pushCoTyArg` with a reflexive coercion, but it can be taught not to as well: Have `pushCoArgs` return a `Maybe ([CoreArg], Maybe Coercion)` and `pushCoArg` return a `Maybe (CoreArg, Maybe Coercion)`. If the second return values are `Nothing`, that means that there is no cast (i.e., that the cast would have been reflexive). The only client of `pushCoArg(s)` is `exprIsConApp_maybe`, which simply omits a cast if `pushCoArgs` returns `Nothing`. Then, we never have to bother creating the reflexive coercions.
>
> This should be an easy win all around.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  goldfire, simonpj, tdammers 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Improve performance of Simplify.simplCast","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","simonpj","tdammers"],"type":"Bug","description":"Splitting off task 3 from #11735. When compiling [https://ghc.haskell.org/trac/ghc/attachment/ticket/14683/Grammar.hs], `simplCast` eats up more execution time than we think it should.\r\n\r\nFrom [https://ghc.haskell.org/trac/ghc/ticket/11735#comment:10]:\r\n\r\n> Something is clearly wrong with `Simplify.simplCast`. I think I know what it is. Given\r\n> {{{\r\n> (fun > co) @t1 @t2 ... @tn\r\n> }}}\r\n> we will call `pushCoTyArg` `n` times, and hence does `n` singleton substitutions, via the `n` calls to `piResultTy`.\r\n> \r\n> Solution: gather up those type arguments (easy) and define\r\n> {{{\r\n> pushCoTyArgs :: Coercion > [Type] > Maybe ([Type], Coercion)\r\n> }}}\r\n\r\nAnd [https://ghc.haskell.org/trac/ghc/ticket/11735#comment:41]:\r\n\r\n> OK. I looked at `pushCoTyArg` and friends, and I have a very simple solution: just move the `isReflexiveCo` case in `addCoerce` (a local function within `Simplify.simplCast`) to the top. That should do it. Then `pushCoTyArg` is never called with a reflexive coercion, and so the `piResultTy` case won't happen.\r\n> \r\n> Now, `pushCoArgs` might still call `pushCoTyArg` with a reflexive coercion, but it can be taught not to as well: Have `pushCoArgs` return a `Maybe ([CoreArg], Maybe Coercion)` and `pushCoArg` return a `Maybe (CoreArg, Maybe Coercion)`. If the second return values are `Nothing`, that means that there is no cast (i.e., that the cast would have been reflexive). The only client of `pushCoArg(s)` is `exprIsConApp_maybe`, which simply omits a cast if `pushCoArgs` returns `Nothing`. Then, we never have to bother creating the reflexive coercions.\r\n> \r\n> This should be an easy win all around.\r\n","type_of_failure":"OtherFailure","blocking":[]} >Splitting off task 3 from #11735. When compiling [https://ghc.haskell.org/trac/ghc/attachment/ticket/14683/Grammar.hs](https://ghc.haskell.org/trac/ghc/attachment/ticket/14683/Grammar.hs), `simplCast` eats up more execution time than we think it should.
From [https://ghc.haskell.org/trac/ghc/ticket/11735\#comment:10](https://ghc.haskell.org/trac/ghc/ticket/11735#comment:10):
> Something is clearly wrong with `Simplify.simplCast`. I think I know what it is. Given
>
> ```
> (fun > co) @t1 @t2 ... @tn
> ```
>
> we will call `pushCoTyArg` `n` times, and hence does `n` singleton substitutions, via the `n` calls to `piResultTy`.
>
> Solution: gather up those type arguments (easy) and define
>
> ```
> pushCoTyArgs :: Coercion > [Type] > Maybe ([Type], Coercion)
> ```
And [https://ghc.haskell.org/trac/ghc/ticket/11735\#comment:41](https://ghc.haskell.org/trac/ghc/ticket/11735#comment:41):
> OK. I looked at `pushCoTyArg` and friends, and I have a very simple solution: just move the `isReflexiveCo` case in `addCoerce` (a local function within `Simplify.simplCast`) to the top. That should do it. Then `pushCoTyArg` is never called with a reflexive coercion, and so the `piResultTy` case won't happen.
>
> Now, `pushCoArgs` might still call `pushCoTyArg` with a reflexive coercion, but it can be taught not to as well: Have `pushCoArgs` return a `Maybe ([CoreArg], Maybe Coercion)` and `pushCoArg` return a `Maybe (CoreArg, Maybe Coercion)`. If the second return values are `Nothing`, that means that there is no cast (i.e., that the cast would have been reflexive). The only client of `pushCoArg(s)` is `exprIsConApp_maybe`, which simply omits a cast if `pushCoArgs` returns `Nothing`. Then, we never have to bother creating the reflexive coercions.
>
> This should be an easy win all around.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  goldfire, simonpj, tdammers 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Improve performance of Simplify.simplCast","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","simonpj","tdammers"],"type":"Bug","description":"Splitting off task 3 from #11735. When compiling [https://ghc.haskell.org/trac/ghc/attachment/ticket/14683/Grammar.hs], `simplCast` eats up more execution time than we think it should.\r\n\r\nFrom [https://ghc.haskell.org/trac/ghc/ticket/11735#comment:10]:\r\n\r\n> Something is clearly wrong with `Simplify.simplCast`. I think I know what it is. Given\r\n> {{{\r\n> (fun > co) @t1 @t2 ... @tn\r\n> }}}\r\n> we will call `pushCoTyArg` `n` times, and hence does `n` singleton substitutions, via the `n` calls to `piResultTy`.\r\n> \r\n> Solution: gather up those type arguments (easy) and define\r\n> {{{\r\n> pushCoTyArgs :: Coercion > [Type] > Maybe ([Type], Coercion)\r\n> }}}\r\n\r\nAnd [https://ghc.haskell.org/trac/ghc/ticket/11735#comment:41]:\r\n\r\n> OK. I looked at `pushCoTyArg` and friends, and I have a very simple solution: just move the `isReflexiveCo` case in `addCoerce` (a local function within `Simplify.simplCast`) to the top. That should do it. Then `pushCoTyArg` is never called with a reflexive coercion, and so the `piResultTy` case won't happen.\r\n> \r\n> Now, `pushCoArgs` might still call `pushCoTyArg` with a reflexive coercion, but it can be taught not to as well: Have `pushCoArgs` return a `Maybe ([CoreArg], Maybe Coercion)` and `pushCoArg` return a `Maybe (CoreArg, Maybe Coercion)`. If the second return values are `Nothing`, that means that there is no cast (i.e., that the cast would have been reflexive). The only client of `pushCoArg(s)` is `exprIsConApp_maybe`, which simply omits a cast if `pushCoArgs` returns `Nothing`. Then, we never have to bother creating the reflexive coercions.\r\n> \r\n> This should be an easy win all around.\r\n","type_of_failure":"OtherFailure","blocking":[]} >8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/13650Implement KPush in types20190707T18:20:47ZRichard Eisenbergrae@richarde.devImplement KPush in typesA recent commit contributed a [Note](https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/Type.hs;a483e711da7834bc952367f554ac4e877b4e157a$1191) that explains why we need the dreaded KPush rule to be implemented in `splitTyConApp`. Without KPush there, it's possible that we can have two types t1 and t2 such that `t1 `eqType` t2` and yet they respond differently to `splitTyConApp`: t1 = `(T > co1) (a > co2)` and t2 = `T a`. Both t1 and t2 are wellkinded and can have the same kind. But one is a `TyConApp` and one is an `AppTy`. (Actually, looking at this, perhaps the magic will be in `mkAppTy`, not `splitTyConApp`.) But I have to look closer.
This ticket serves as a reminder to do so.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Implement KPush in types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"A recent commit contributed a [https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/Type.hs;a483e711da7834bc952367f554ac4e877b4e157a$1191 Note] that explains why we need the dreaded KPush rule to be implemented in `splitTyConApp`. Without KPush there, it's possible that we can have two types t1 and t2 such that {{{t1 `eqType` t2}}} and yet they respond differently to `splitTyConApp`: t1 = `(T > co1) (a > co2)` and t2 = `T a`. Both t1 and t2 are wellkinded and can have the same kind. But one is a `TyConApp` and one is an `AppTy`. (Actually, looking at this, perhaps the magic will be in `mkAppTy`, not `splitTyConApp`.) But I have to look closer.\r\n\r\nThis ticket serves as a reminder to do so.","type_of_failure":"OtherFailure","blocking":[]} >A recent commit contributed a [Note](https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/Type.hs;a483e711da7834bc952367f554ac4e877b4e157a$1191) that explains why we need the dreaded KPush rule to be implemented in `splitTyConApp`. Without KPush there, it's possible that we can have two types t1 and t2 such that `t1 `eqType` t2` and yet they respond differently to `splitTyConApp`: t1 = `(T > co1) (a > co2)` and t2 = `T a`. Both t1 and t2 are wellkinded and can have the same kind. But one is a `TyConApp` and one is an `AppTy`. (Actually, looking at this, perhaps the magic will be in `mkAppTy`, not `splitTyConApp`.) But I have to look closer.
This ticket serves as a reminder to do so.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Implement KPush in types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"A recent commit contributed a [https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/Type.hs;a483e711da7834bc952367f554ac4e877b4e157a$1191 Note] that explains why we need the dreaded KPush rule to be implemented in `splitTyConApp`. Without KPush there, it's possible that we can have two types t1 and t2 such that {{{t1 `eqType` t2}}} and yet they respond differently to `splitTyConApp`: t1 = `(T > co1) (a > co2)` and t2 = `T a`. Both t1 and t2 are wellkinded and can have the same kind. But one is a `TyConApp` and one is an `AppTy`. (Actually, looking at this, perhaps the magic will be in `mkAppTy`, not `splitTyConApp`.) But I have to look closer.\r\n\r\nThis ticket serves as a reminder to do so.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/13075Toplevel bang pattern accepted20190707T18:23:49ZRichard Eisenbergrae@richarde.devToplevel bang pattern acceptedWhen I compile/link
```hs
{# LANGUAGE BangPatterns #}
module Main where
!(Just x) = Nothing
main = putStrLn "hi there!"
```
I get
```
rae:09:50:49 ~/temp> ghc Bug.hs
[1 of 1] Compiling Main ( Bug.hs, Bug.o )
Linking Bug ...
ld: can't open output file for writing: Bug, errno=21 for architecture x86_64
clang: error: linker command failed with exit code 1 (use v to see invocation)
`gcc' failed in phase `Linker'. (Exit code: 1)
```
This bogus code should be rejected more gracefully (and earlier). It actually also loads into GHCi, but shouldn't.
Will fix while I'm in the area.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Toplevel bang pattern accepted","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I compile/link\r\n\r\n{{{#!hs\r\n{# LANGUAGE BangPatterns #}\r\n\r\nmodule Main where\r\n\r\n!(Just x) = Nothing\r\n\r\nmain = putStrLn \"hi there!\"\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nrae:09:50:49 ~/temp> ghc Bug.hs\r\n[1 of 1] Compiling Main ( Bug.hs, Bug.o )\r\nLinking Bug ...\r\nld: can't open output file for writing: Bug, errno=21 for architecture x86_64\r\nclang: error: linker command failed with exit code 1 (use v to see invocation)\r\n`gcc' failed in phase `Linker'. (Exit code: 1)\r\n}}}\r\n\r\nThis bogus code should be rejected more gracefully (and earlier). It actually also loads into GHCi, but shouldn't.\r\n\r\nWill fix while I'm in the area.","type_of_failure":"OtherFailure","blocking":[]} >When I compile/link
```hs
{# LANGUAGE BangPatterns #}
module Main where
!(Just x) = Nothing
main = putStrLn "hi there!"
```
I get
```
rae:09:50:49 ~/temp> ghc Bug.hs
[1 of 1] Compiling Main ( Bug.hs, Bug.o )
Linking Bug ...
ld: can't open output file for writing: Bug, errno=21 for architecture x86_64
clang: error: linker command failed with exit code 1 (use v to see invocation)
`gcc' failed in phase `Linker'. (Exit code: 1)
```
This bogus code should be rejected more gracefully (and earlier). It actually also loads into GHCi, but shouldn't.
Will fix while I'm in the area.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Toplevel bang pattern accepted","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I compile/link\r\n\r\n{{{#!hs\r\n{# LANGUAGE BangPatterns #}\r\n\r\nmodule Main where\r\n\r\n!(Just x) = Nothing\r\n\r\nmain = putStrLn \"hi there!\"\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nrae:09:50:49 ~/temp> ghc Bug.hs\r\n[1 of 1] Compiling Main ( Bug.hs, Bug.o )\r\nLinking Bug ...\r\nld: can't open output file for writing: Bug, errno=21 for architecture x86_64\r\nclang: error: linker command failed with exit code 1 (use v to see invocation)\r\n`gcc' failed in phase `Linker'. (Exit code: 1)\r\n}}}\r\n\r\nThis bogus code should be rejected more gracefully (and earlier). It actually also loads into GHCi, but shouldn't.\r\n\r\nWill fix while I'm in the area.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/12938Polykinded associated type family rejected on false pretenses20190707T18:24:33ZRichard Eisenbergrae@richarde.devPolykinded associated type family rejected on false pretensesIf I say
```
class HasRep a where
type Rep a :: TYPE r
```
I get
```
• Kind variable ‘r’ is implicitly bound in datatype
‘Rep’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it (with TypeInType) explicitly somewhere?
Type variables with inferred kinds: a
• In the class declaration for ‘HasRep’
```
This definition should be accepted, though, as `r` is just an invisible parameter to the associated type family. (I don't know how *useful* this is, but it's not bogus.)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Polykinded associated type family rejected on false pretenses","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I say\r\n\r\n{{{\r\nclass HasRep a where\r\n type Rep a :: TYPE r\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\n • Kind variable ‘r’ is implicitly bound in datatype\r\n ‘Rep’, but does not appear as the kind of any\r\n of its type variables. Perhaps you meant\r\n to bind it (with TypeInType) explicitly somewhere?\r\n Type variables with inferred kinds: a\r\n • In the class declaration for ‘HasRep’\r\n}}}\r\n\r\nThis definition should be accepted, though, as `r` is just an invisible parameter to the associated type family. (I don't know how ''useful'' this is, but it's not bogus.)","type_of_failure":"OtherFailure","blocking":[]} >If I say
```
class HasRep a where
type Rep a :: TYPE r
```
I get
```
• Kind variable ‘r’ is implicitly bound in datatype
‘Rep’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it (with TypeInType) explicitly somewhere?
Type variables with inferred kinds: a
• In the class declaration for ‘HasRep’
```
This definition should be accepted, though, as `r` is just an invisible parameter to the associated type family. (I don't know how *useful* this is, but it's not bogus.)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Polykinded associated type family rejected on false pretenses","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I say\r\n\r\n{{{\r\nclass HasRep a where\r\n type Rep a :: TYPE r\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\n • Kind variable ‘r’ is implicitly bound in datatype\r\n ‘Rep’, but does not appear as the kind of any\r\n of its type variables. Perhaps you meant\r\n to bind it (with TypeInType) explicitly somewhere?\r\n Type variables with inferred kinds: a\r\n • In the class declaration for ‘HasRep’\r\n}}}\r\n\r\nThis definition should be accepted, though, as `r` is just an invisible parameter to the associated type family. (I don't know how ''useful'' this is, but it's not bogus.)","type_of_failure":"OtherFailure","blocking":[]} >8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/11715Constraint vs *20200805T17:10:06ZBen GamariConstraint vs *I first noticed something was a bit odd with `Constraint` when chasing #11334. Consider this testcase (`O0` is sufficient),
```hs
import Data.Typeable
main = do
print $ typeRep (Proxy :: Proxy Eq)
print $ typeOf (Proxy :: Proxy Eq)
```
With `ghc8.0` this will produce,
```
Eq
Proxy (* > *) Eq
```
Notice the second line; GHC seems to be claiming that `Eq :: * > *`, which is clearly nonsense.
I believe this issue may be the cause of some of the testsuite failures that I'm seeing on #11011. Unfortunately I haven't the foggiest where this issue might originate.
See also
 #11621
 #12933
 #9547
 #13931
 #15918 (about `mkCastTy`)I first noticed something was a bit odd with `Constraint` when chasing #11334. Consider this testcase (`O0` is sufficient),
```hs
import Data.Typeable
main = do
print $ typeRep (Proxy :: Proxy Eq)
print $ typeOf (Proxy :: Proxy Eq)
```
With `ghc8.0` this will produce,
```
Eq
Proxy (* > *) Eq
```
Notice the second line; GHC seems to be claiming that `Eq :: * > *`, which is clearly nonsense.
I believe this issue may be the cause of some of the testsuite failures that I'm seeing on #11011. Unfortunately I haven't the foggiest where this issue might originate.
See also
 #11621
 #12933
 #9547
 #13931
 #15918 (about `mkCastTy`)8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/10141CUSK mysteries20190707T18:37:21ZRichard Eisenbergrae@richarde.devCUSK mysteriesTake the following definition:
```hs
type family G (a :: k) where
G Int = Bool
G Bool = Int
G a = a
```
It compiles in 7.8.3, but not in 7.10.1 RC2. This makes me sad. I will fix.
(Found by Jan Stolarek.)Take the following definition:
```hs
type family G (a :: k) where
G Int = Bool
G Bool = Int
G a = a
```
It compiles in 7.8.3, but not in 7.10.1 RC2. This makes me sad. I will fix.
(Found by Jan Stolarek.)8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.dev