GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20190707T18:12:57Zhttps://gitlab.haskell.org/ghc/ghc//issues/15370Typed hole panic on GHC 8.6 (tcTyVarDetails)20190707T18:12:57ZRyan ScottTyped hole panic on GHC 8.6 (tcTyVarDetails)The following program panics on GHC 8.6 and HEAD:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Type.Equality
import Data.Void
data family Sing :: forall k. k > Type
data (~>) :: Type > Type > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }
mkRefl :: n :~: j
mkRefl = Refl
right :: forall (r :: (x :~: y) ~> z).
Sing r > ()
right no =
case mkRefl @x @y of
Refl > applySing no _
```
```
$ /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.20180627 for x86_64unknownlinux):
tcTyVarDetails
co_a1BG :: y_a1Bz[sk:1] ~# x_a1By[sk:1]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var
```
On GHC 8.4, this simply errors:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:23:10: error:
• Couldn't match type ‘n’ with ‘j’
‘n’ is a rigid type variable bound by
the type signature for:
mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j
at Bug.hs:22:117
‘j’ is a rigid type variable bound by
the type signature for:
mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j
at Bug.hs:22:117
Expected type: n :~: j
Actual type: n :~: n
• In the expression: Refl
In an equation for ‘mkRefl’: mkRefl = Refl
• Relevant bindings include
mkRefl :: n :~: j (bound at Bug.hs:23:1)

23  mkRefl = Refl
 ^^^^
Bug.hs:29:13: error:
• Couldn't match type ‘Sing (Apply r t0)’ with ‘()’
Expected type: ()
Actual type: Sing (Apply r t0)
• In the expression: applySing no _
In a case alternative: Refl > applySing no _
In the expression: case mkRefl @x @y of { Refl > applySing no _ }
• Relevant bindings include
no :: Sing r (bound at Bug.hs:27:7)
right :: Sing r > () (bound at Bug.hs:27:1)

29  Refl > applySing no _
 ^^^^^^^^^^^^^^
Bug.hs:29:26: error:
• Found hole: _ :: Sing t0
Where: ‘t0’ is an ambiguous type variable
‘y’, ‘x’, ‘k’ are rigid type variables bound by
the type signature for:
right :: forall k1 (x1 :: k1) (y1 :: k1) z (r :: (x1 :~: y1) ~> z).
Sing r > ()
at Bug.hs:(25,1)(26,21)
• In the second argument of ‘applySing’, namely ‘_’
In the expression: applySing no _
In a case alternative: Refl > applySing no _
• Relevant bindings include
no :: Sing r (bound at Bug.hs:27:7)
right :: Sing r > () (bound at Bug.hs:27:1)
Valid substitutions include
undefined :: forall (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
(imported from ‘Prelude’ at Bug.hs:7:810
(and originally defined in ‘GHC.Err’))

29  Refl > applySing no _
 ^
```
Note that this is distinct from #15142, as this is still reproducible on HEAD, even after commit 030211d21207dabb7a4bf21cc9af6fa5eb066db1.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Typed hole panic on GHC 8.6 (tcTyVarDetails)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType,","TypedHoles"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics on GHC 8.6 and HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\nimport Data.Void\r\n\r\ndata family Sing :: forall k. k > Type\r\n\r\ndata (~>) :: Type > Type > Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\n\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }\r\n\r\nmkRefl :: n :~: j\r\nmkRefl = Refl\r\n\r\nright :: forall (r :: (x :~: y) ~> z).\r\n Sing r > ()\r\nright no =\r\n case mkRefl @x @y of\r\n Refl > applySing no _\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.20180627 for x86_64unknownlinux):\r\n tcTyVarDetails\r\n co_a1BG :: y_a1Bz[sk:1] ~# x_a1By[sk:1]\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/basicTypes/Var.hs:497:22 in ghc:Var\r\n}}}\r\n\r\nOn GHC 8.4, this simply errors:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:23:10: error:\r\n • Couldn't match type ‘n’ with ‘j’\r\n ‘n’ is a rigid type variable bound by\r\n the type signature for:\r\n mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j\r\n at Bug.hs:22:117\r\n ‘j’ is a rigid type variable bound by\r\n the type signature for:\r\n mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j\r\n at Bug.hs:22:117\r\n Expected type: n :~: j\r\n Actual type: n :~: n\r\n • In the expression: Refl\r\n In an equation for ‘mkRefl’: mkRefl = Refl\r\n • Relevant bindings include\r\n mkRefl :: n :~: j (bound at Bug.hs:23:1)\r\n \r\n23  mkRefl = Refl\r\n  ^^^^\r\n\r\nBug.hs:29:13: error:\r\n • Couldn't match type ‘Sing (Apply r t0)’ with ‘()’\r\n Expected type: ()\r\n Actual type: Sing (Apply r t0)\r\n • In the expression: applySing no _\r\n In a case alternative: Refl > applySing no _\r\n In the expression: case mkRefl @x @y of { Refl > applySing no _ }\r\n • Relevant bindings include\r\n no :: Sing r (bound at Bug.hs:27:7)\r\n right :: Sing r > () (bound at Bug.hs:27:1)\r\n \r\n29  Refl > applySing no _\r\n  ^^^^^^^^^^^^^^\r\n\r\nBug.hs:29:26: error:\r\n • Found hole: _ :: Sing t0\r\n Where: ‘t0’ is an ambiguous type variable\r\n ‘y’, ‘x’, ‘k’ are rigid type variables bound by\r\n the type signature for:\r\n right :: forall k1 (x1 :: k1) (y1 :: k1) z (r :: (x1 :~: y1) ~> z).\r\n Sing r > ()\r\n at Bug.hs:(25,1)(26,21)\r\n • In the second argument of ‘applySing’, namely ‘_’\r\n In the expression: applySing no _\r\n In a case alternative: Refl > applySing no _\r\n • Relevant bindings include\r\n no :: Sing r (bound at Bug.hs:27:7)\r\n right :: Sing r > () (bound at Bug.hs:27:1)\r\n Valid substitutions include\r\n undefined :: forall (a :: TYPE r).\r\n GHC.Stack.Types.HasCallStack =>\r\n a\r\n (imported from ‘Prelude’ at Bug.hs:7:810\r\n (and originally defined in ‘GHC.Err’))\r\n \r\n29  Refl > applySing no _\r\n  ^\r\n}}}\r\n\r\nNote that this is distinct from #15142, as this is still reproducible on HEAD, even after commit 030211d21207dabb7a4bf21cc9af6fa5eb066db1.","type_of_failure":"OtherFailure","blocking":[]} >The following program panics on GHC 8.6 and HEAD:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Type.Equality
import Data.Void
data family Sing :: forall k. k > Type
data (~>) :: Type > Type > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }
mkRefl :: n :~: j
mkRefl = Refl
right :: forall (r :: (x :~: y) ~> z).
Sing r > ()
right no =
case mkRefl @x @y of
Refl > applySing no _
```
```
$ /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.20180627 for x86_64unknownlinux):
tcTyVarDetails
co_a1BG :: y_a1Bz[sk:1] ~# x_a1By[sk:1]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var
```
On GHC 8.4, this simply errors:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:23:10: error:
• Couldn't match type ‘n’ with ‘j’
‘n’ is a rigid type variable bound by
the type signature for:
mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j
at Bug.hs:22:117
‘j’ is a rigid type variable bound by
the type signature for:
mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j
at Bug.hs:22:117
Expected type: n :~: j
Actual type: n :~: n
• In the expression: Refl
In an equation for ‘mkRefl’: mkRefl = Refl
• Relevant bindings include
mkRefl :: n :~: j (bound at Bug.hs:23:1)

23  mkRefl = Refl
 ^^^^
Bug.hs:29:13: error:
• Couldn't match type ‘Sing (Apply r t0)’ with ‘()’
Expected type: ()
Actual type: Sing (Apply r t0)
• In the expression: applySing no _
In a case alternative: Refl > applySing no _
In the expression: case mkRefl @x @y of { Refl > applySing no _ }
• Relevant bindings include
no :: Sing r (bound at Bug.hs:27:7)
right :: Sing r > () (bound at Bug.hs:27:1)

29  Refl > applySing no _
 ^^^^^^^^^^^^^^
Bug.hs:29:26: error:
• Found hole: _ :: Sing t0
Where: ‘t0’ is an ambiguous type variable
‘y’, ‘x’, ‘k’ are rigid type variables bound by
the type signature for:
right :: forall k1 (x1 :: k1) (y1 :: k1) z (r :: (x1 :~: y1) ~> z).
Sing r > ()
at Bug.hs:(25,1)(26,21)
• In the second argument of ‘applySing’, namely ‘_’
In the expression: applySing no _
In a case alternative: Refl > applySing no _
• Relevant bindings include
no :: Sing r (bound at Bug.hs:27:7)
right :: Sing r > () (bound at Bug.hs:27:1)
Valid substitutions include
undefined :: forall (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
(imported from ‘Prelude’ at Bug.hs:7:810
(and originally defined in ‘GHC.Err’))

29  Refl > applySing no _
 ^
```
Note that this is distinct from #15142, as this is still reproducible on HEAD, even after commit 030211d21207dabb7a4bf21cc9af6fa5eb066db1.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Typed hole panic on GHC 8.6 (tcTyVarDetails)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType,","TypedHoles"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics on GHC 8.6 and HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\nimport Data.Void\r\n\r\ndata family Sing :: forall k. k > Type\r\n\r\ndata (~>) :: Type > Type > Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\n\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }\r\n\r\nmkRefl :: n :~: j\r\nmkRefl = Refl\r\n\r\nright :: forall (r :: (x :~: y) ~> z).\r\n Sing r > ()\r\nright no =\r\n case mkRefl @x @y of\r\n Refl > applySing no _\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.20180627 for x86_64unknownlinux):\r\n tcTyVarDetails\r\n co_a1BG :: y_a1Bz[sk:1] ~# x_a1By[sk:1]\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/basicTypes/Var.hs:497:22 in ghc:Var\r\n}}}\r\n\r\nOn GHC 8.4, this simply errors:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:23:10: error:\r\n • Couldn't match type ‘n’ with ‘j’\r\n ‘n’ is a rigid type variable bound by\r\n the type signature for:\r\n mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j\r\n at Bug.hs:22:117\r\n ‘j’ is a rigid type variable bound by\r\n the type signature for:\r\n mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j\r\n at Bug.hs:22:117\r\n Expected type: n :~: j\r\n Actual type: n :~: n\r\n • In the expression: Refl\r\n In an equation for ‘mkRefl’: mkRefl = Refl\r\n • Relevant bindings include\r\n mkRefl :: n :~: j (bound at Bug.hs:23:1)\r\n \r\n23  mkRefl = Refl\r\n  ^^^^\r\n\r\nBug.hs:29:13: error:\r\n • Couldn't match type ‘Sing (Apply r t0)’ with ‘()’\r\n Expected type: ()\r\n Actual type: Sing (Apply r t0)\r\n • In the expression: applySing no _\r\n In a case alternative: Refl > applySing no _\r\n In the expression: case mkRefl @x @y of { Refl > applySing no _ }\r\n • Relevant bindings include\r\n no :: Sing r (bound at Bug.hs:27:7)\r\n right :: Sing r > () (bound at Bug.hs:27:1)\r\n \r\n29  Refl > applySing no _\r\n  ^^^^^^^^^^^^^^\r\n\r\nBug.hs:29:26: error:\r\n • Found hole: _ :: Sing t0\r\n Where: ‘t0’ is an ambiguous type variable\r\n ‘y’, ‘x’, ‘k’ are rigid type variables bound by\r\n the type signature for:\r\n right :: forall k1 (x1 :: k1) (y1 :: k1) z (r :: (x1 :~: y1) ~> z).\r\n Sing r > ()\r\n at Bug.hs:(25,1)(26,21)\r\n • In the second argument of ‘applySing’, namely ‘_’\r\n In the expression: applySing no _\r\n In a case alternative: Refl > applySing no _\r\n • Relevant bindings include\r\n no :: Sing r (bound at Bug.hs:27:7)\r\n right :: Sing r > () (bound at Bug.hs:27:1)\r\n Valid substitutions include\r\n undefined :: forall (a :: TYPE r).\r\n GHC.Stack.Types.HasCallStack =>\r\n a\r\n (imported from ‘Prelude’ at Bug.hs:7:810\r\n (and originally defined in ‘GHC.Err’))\r\n \r\n29  Refl > applySing no _\r\n  ^\r\n}}}\r\n\r\nNote that this is distinct from #15142, as this is still reproducible on HEAD, even after commit 030211d21207dabb7a4bf21cc9af6fa5eb066db1.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1Matthías Páll GissurarsonMatthías Páll Gissurarsonhttps://gitlab.haskell.org/ghc/ghc//issues/15361Error message displays redundant equality constraint20190707T18:13:00ZRyan ScottError message displays redundant equality constraintWhen compiling this program:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Type.Equality
foo :: forall (a :: Type) (b :: Type) (c :: Type).
a :~~: b > a :~~: c
foo HRefl = HRefl
```
GHC complains thus:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:13: error:
• Could not deduce: a ~ c
from the context: (* ~ *, b ~ a)
bound by a pattern with constructor:
HRefl :: forall k1 (a :: k1). a :~~: a,
in an equation for ‘foo’
at Bug.hs:12:59
‘a’ is a rigid type variable bound by
the type signature for:
foo :: forall a b c. (a :~~: b) > a :~~: c
at Bug.hs:(10,1)(11,27)
‘c’ is a rigid type variable bound by
the type signature for:
foo :: forall a b c. (a :~~: b) > a :~~: c
at Bug.hs:(10,1)(11,27)
Expected type: a :~~: c
Actual type: a :~~: a
• In the expression: HRefl
In an equation for ‘foo’: foo HRefl = HRefl
• Relevant bindings include
foo :: (a :~~: b) > a :~~: c (bound at Bug.hs:12:1)

12  foo HRefl = HRefl
 ^^^^^
```
That `* ~ *` constraint is entirely redundant.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 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":"Error message displays redundant equality constraint","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When compiling this program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\nfoo :: forall (a :: Type) (b :: Type) (c :: Type).\r\n a :~~: b > a :~~: c\r\nfoo HRefl = HRefl\r\n}}}\r\n\r\nGHC complains thus:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:12:13: error:\r\n • Could not deduce: a ~ c\r\n from the context: (* ~ *, b ~ a)\r\n bound by a pattern with constructor:\r\n HRefl :: forall k1 (a :: k1). a :~~: a,\r\n in an equation for ‘foo’\r\n at Bug.hs:12:59\r\n ‘a’ is a rigid type variable bound by\r\n the type signature for:\r\n foo :: forall a b c. (a :~~: b) > a :~~: c\r\n at Bug.hs:(10,1)(11,27)\r\n ‘c’ is a rigid type variable bound by\r\n the type signature for:\r\n foo :: forall a b c. (a :~~: b) > a :~~: c\r\n at Bug.hs:(10,1)(11,27)\r\n Expected type: a :~~: c\r\n Actual type: a :~~: a\r\n • In the expression: HRefl\r\n In an equation for ‘foo’: foo HRefl = HRefl\r\n • Relevant bindings include\r\n foo :: (a :~~: b) > a :~~: c (bound at Bug.hs:12:1)\r\n \r\n12  foo HRefl = HRefl\r\n  ^^^^^\r\n}}}\r\n\r\nThat `* ~ *` constraint is entirely redundant.","type_of_failure":"OtherFailure","blocking":[]} >When compiling this program:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Type.Equality
foo :: forall (a :: Type) (b :: Type) (c :: Type).
a :~~: b > a :~~: c
foo HRefl = HRefl
```
GHC complains thus:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:13: error:
• Could not deduce: a ~ c
from the context: (* ~ *, b ~ a)
bound by a pattern with constructor:
HRefl :: forall k1 (a :: k1). a :~~: a,
in an equation for ‘foo’
at Bug.hs:12:59
‘a’ is a rigid type variable bound by
the type signature for:
foo :: forall a b c. (a :~~: b) > a :~~: c
at Bug.hs:(10,1)(11,27)
‘c’ is a rigid type variable bound by
the type signature for:
foo :: forall a b c. (a :~~: b) > a :~~: c
at Bug.hs:(10,1)(11,27)
Expected type: a :~~: c
Actual type: a :~~: a
• In the expression: HRefl
In an equation for ‘foo’: foo HRefl = HRefl
• Relevant bindings include
foo :: (a :~~: b) > a :~~: c (bound at Bug.hs:12:1)

12  foo HRefl = HRefl
 ^^^^^
```
That `* ~ *` constraint is entirely redundant.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 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":"Error message displays redundant equality constraint","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When compiling this program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\nfoo :: forall (a :: Type) (b :: Type) (c :: Type).\r\n a :~~: b > a :~~: c\r\nfoo HRefl = HRefl\r\n}}}\r\n\r\nGHC complains thus:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:12:13: error:\r\n • Could not deduce: a ~ c\r\n from the context: (* ~ *, b ~ a)\r\n bound by a pattern with constructor:\r\n HRefl :: forall k1 (a :: k1). a :~~: a,\r\n in an equation for ‘foo’\r\n at Bug.hs:12:59\r\n ‘a’ is a rigid type variable bound by\r\n the type signature for:\r\n foo :: forall a b c. (a :~~: b) > a :~~: c\r\n at Bug.hs:(10,1)(11,27)\r\n ‘c’ is a rigid type variable bound by\r\n the type signature for:\r\n foo :: forall a b c. (a :~~: b) > a :~~: c\r\n at Bug.hs:(10,1)(11,27)\r\n Expected type: a :~~: c\r\n Actual type: a :~~: a\r\n • In the expression: HRefl\r\n In an equation for ‘foo’: foo HRefl = HRefl\r\n • Relevant bindings include\r\n foo :: (a :~~: b) > a :~~: c (bound at Bug.hs:12:1)\r\n \r\n12  foo HRefl = HRefl\r\n  ^^^^^\r\n}}}\r\n\r\nThat `* ~ *` constraint is entirely redundant.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15346Core Lint error in GHC 8.6.1: Fromtype of Cast differs from type of enclosed...20190707T18:13:04ZRyan ScottCore Lint error in GHC 8.6.1: Fromtype of Cast differs from type of enclosed expressionThe following program typechecks on GHC 8.6.1alpha1:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE DefaultSignatures #}
{# LANGUAGE EmptyCase #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE GADTs #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module SGenerics where
import Data.Kind
import Data.Type.Equality
import Data.Void

 singletons machinery

data family Sing :: forall k. k > Type
data instance Sing :: () > Type where
STuple0 :: Sing '()
type Refuted a = a > Void
data Decision a = Proved a  Disproved (Refuted a)

 A stripped down version of GHC.Generics

data U1 = MkU1
data instance Sing (z :: U1) where
SMkU1 :: Sing MkU1

class Generic (a :: Type) where
type Rep a :: Type
from :: a > Rep a
to :: Rep a > a
class PGeneric (a :: Type) where
type PFrom (x :: a) :: Rep a
type PTo (x :: Rep a) :: a
class SGeneric k where
sFrom :: forall (a :: k). Sing a > Sing (PFrom a)
sTo :: forall (a :: Rep k). Sing a > Sing (PTo a :: k)
sTof :: forall (a :: k). Sing a > PTo (PFrom a) :~: a
sFot :: forall (a :: Rep k). Sing a > PFrom (PTo a :: k) :~: a

instance Generic () where
type Rep () = U1
from () = MkU1
to MkU1 = ()
instance PGeneric () where
type PFrom '() = MkU1
type PTo 'MkU1 = '()
instance SGeneric () where
sFrom STuple0 = SMkU1
sTo SMkU1 = STuple0
sTof STuple0 = Refl
sFot SMkU1 = Refl

class SDecide k where
  Compute a proof or disproof of equality, given two singletons.
(%~) :: forall (a :: k) (b :: k). Sing a > Sing b > Decision (a :~: b)
default (%~) :: forall (a :: k) (b :: k). (SGeneric k, SDecide (Rep k))
=> Sing a > Sing b > Decision (a :~: b)
s1 %~ s2 = case sFrom s1 %~ sFrom s2 of
Proved (Refl :: PFrom a :~: PFrom b) >
let r :: PTo (PFrom a) :~: PTo (PFrom b)
r = Refl
sTof1 :: PTo (PFrom a) :~: a
sTof1 = sTof s1
sTof2 :: PTo (PFrom b) :~: b
sTof2 = sTof s2
in Proved (sym sTof1 `trans` r `trans` sTof2)
Disproved contra > Disproved (\Refl > contra Refl)
instance SDecide U1 where
SMkU1 %~ SMkU1 = Proved Refl
instance SDecide ()
```
However, it throws a Core Lint error with `dcorelint`. The full error is absolutely massive, so I'll attach it separately. Here is the toplevel bit:
```
*** Core Lint errors : in result of Simplifier ***
<no location info>: warning:
In the expression: <elided>
Fromtype of Cast differs from type of enclosed expression
Fromtype: U1
Type of enclosed expr: Rep ()
Actual enclosed expr: PFrom a_a1Fm
Coercion used in cast: Sym (D:R:Rep()[0])
```
<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":"Core Lint error in GHC 8.6.1: Fromtype of Cast differs from type of enclosed expression","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.6.1alpha1:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE DefaultSignatures #}\r\n{# LANGUAGE EmptyCase #}\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule SGenerics where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\nimport Data.Void\r\n\r\n\r\n singletons machinery\r\n\r\n\r\ndata family Sing :: forall k. k > Type\r\n\r\ndata instance Sing :: () > Type where\r\n STuple0 :: Sing '()\r\n\r\ntype Refuted a = a > Void\r\ndata Decision a = Proved a  Disproved (Refuted a)\r\n\r\n\r\n A stripped down version of GHC.Generics\r\n\r\n\r\ndata U1 = MkU1\r\ndata instance Sing (z :: U1) where\r\n SMkU1 :: Sing MkU1\r\n\r\n\r\n\r\nclass Generic (a :: Type) where\r\n type Rep a :: Type\r\n from :: a > Rep a\r\n to :: Rep a > a\r\n\r\nclass PGeneric (a :: Type) where\r\n type PFrom (x :: a) :: Rep a\r\n type PTo (x :: Rep a) :: a\r\n\r\nclass SGeneric k where\r\n sFrom :: forall (a :: k). Sing a > Sing (PFrom a)\r\n sTo :: forall (a :: Rep k). Sing a > Sing (PTo a :: k)\r\n sTof :: forall (a :: k). Sing a > PTo (PFrom a) :~: a\r\n sFot :: forall (a :: Rep k). Sing a > PFrom (PTo a :: k) :~: a\r\n\r\n\r\n\r\ninstance Generic () where\r\n type Rep () = U1\r\n from () = MkU1\r\n to MkU1 = ()\r\n\r\ninstance PGeneric () where\r\n type PFrom '() = MkU1\r\n type PTo 'MkU1 = '()\r\n\r\ninstance SGeneric () where\r\n sFrom STuple0 = SMkU1\r\n sTo SMkU1 = STuple0\r\n sTof STuple0 = Refl\r\n sFot SMkU1 = Refl\r\n\r\n\r\n\r\nclass SDecide k where\r\n   Compute a proof or disproof of equality, given two singletons.\r\n (%~) :: forall (a :: k) (b :: k). Sing a > Sing b > Decision (a :~: b)\r\n default (%~) :: forall (a :: k) (b :: k). (SGeneric k, SDecide (Rep k))\r\n => Sing a > Sing b > Decision (a :~: b)\r\n s1 %~ s2 = case sFrom s1 %~ sFrom s2 of\r\n Proved (Refl :: PFrom a :~: PFrom b) >\r\n let r :: PTo (PFrom a) :~: PTo (PFrom b)\r\n r = Refl\r\n\r\n sTof1 :: PTo (PFrom a) :~: a\r\n sTof1 = sTof s1\r\n\r\n sTof2 :: PTo (PFrom b) :~: b\r\n sTof2 = sTof s2\r\n in Proved (sym sTof1 `trans` r `trans` sTof2)\r\n Disproved contra > Disproved (\\Refl > contra Refl)\r\n\r\ninstance SDecide U1 where\r\n SMkU1 %~ SMkU1 = Proved Refl\r\n\r\ninstance SDecide ()\r\n}}}\r\n\r\nHowever, it throws a Core Lint error with `dcorelint`. The full error is absolutely massive, so I'll attach it separately. Here is the toplevel bit:\r\n\r\n{{{\r\n*** Core Lint errors : in result of Simplifier ***\r\n<no location info>: warning:\r\n In the expression: <elided>\r\n Fromtype of Cast differs from type of enclosed expression\r\n Fromtype: U1\r\n Type of enclosed expr: Rep ()\r\n Actual enclosed expr: PFrom a_a1Fm\r\n Coercion used in cast: Sym (D:R:Rep()[0])\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >The following program typechecks on GHC 8.6.1alpha1:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE DefaultSignatures #}
{# LANGUAGE EmptyCase #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE GADTs #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module SGenerics where
import Data.Kind
import Data.Type.Equality
import Data.Void

 singletons machinery

data family Sing :: forall k. k > Type
data instance Sing :: () > Type where
STuple0 :: Sing '()
type Refuted a = a > Void
data Decision a = Proved a  Disproved (Refuted a)

 A stripped down version of GHC.Generics

data U1 = MkU1
data instance Sing (z :: U1) where
SMkU1 :: Sing MkU1

class Generic (a :: Type) where
type Rep a :: Type
from :: a > Rep a
to :: Rep a > a
class PGeneric (a :: Type) where
type PFrom (x :: a) :: Rep a
type PTo (x :: Rep a) :: a
class SGeneric k where
sFrom :: forall (a :: k). Sing a > Sing (PFrom a)
sTo :: forall (a :: Rep k). Sing a > Sing (PTo a :: k)
sTof :: forall (a :: k). Sing a > PTo (PFrom a) :~: a
sFot :: forall (a :: Rep k). Sing a > PFrom (PTo a :: k) :~: a

instance Generic () where
type Rep () = U1
from () = MkU1
to MkU1 = ()
instance PGeneric () where
type PFrom '() = MkU1
type PTo 'MkU1 = '()
instance SGeneric () where
sFrom STuple0 = SMkU1
sTo SMkU1 = STuple0
sTof STuple0 = Refl
sFot SMkU1 = Refl

class SDecide k where
  Compute a proof or disproof of equality, given two singletons.
(%~) :: forall (a :: k) (b :: k). Sing a > Sing b > Decision (a :~: b)
default (%~) :: forall (a :: k) (b :: k). (SGeneric k, SDecide (Rep k))
=> Sing a > Sing b > Decision (a :~: b)
s1 %~ s2 = case sFrom s1 %~ sFrom s2 of
Proved (Refl :: PFrom a :~: PFrom b) >
let r :: PTo (PFrom a) :~: PTo (PFrom b)
r = Refl
sTof1 :: PTo (PFrom a) :~: a
sTof1 = sTof s1
sTof2 :: PTo (PFrom b) :~: b
sTof2 = sTof s2
in Proved (sym sTof1 `trans` r `trans` sTof2)
Disproved contra > Disproved (\Refl > contra Refl)
instance SDecide U1 where
SMkU1 %~ SMkU1 = Proved Refl
instance SDecide ()
```
However, it throws a Core Lint error with `dcorelint`. The full error is absolutely massive, so I'll attach it separately. Here is the toplevel bit:
```
*** Core Lint errors : in result of Simplifier ***
<no location info>: warning:
In the expression: <elided>
Fromtype of Cast differs from type of enclosed expression
Fromtype: U1
Type of enclosed expr: Rep ()
Actual enclosed expr: PFrom a_a1Fm
Coercion used in cast: Sym (D:R:Rep()[0])
```
<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":"Core Lint error in GHC 8.6.1: Fromtype of Cast differs from type of enclosed expression","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.6.1alpha1:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE DefaultSignatures #}\r\n{# LANGUAGE EmptyCase #}\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule SGenerics where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\nimport Data.Void\r\n\r\n\r\n singletons machinery\r\n\r\n\r\ndata family Sing :: forall k. k > Type\r\n\r\ndata instance Sing :: () > Type where\r\n STuple0 :: Sing '()\r\n\r\ntype Refuted a = a > Void\r\ndata Decision a = Proved a  Disproved (Refuted a)\r\n\r\n\r\n A stripped down version of GHC.Generics\r\n\r\n\r\ndata U1 = MkU1\r\ndata instance Sing (z :: U1) where\r\n SMkU1 :: Sing MkU1\r\n\r\n\r\n\r\nclass Generic (a :: Type) where\r\n type Rep a :: Type\r\n from :: a > Rep a\r\n to :: Rep a > a\r\n\r\nclass PGeneric (a :: Type) where\r\n type PFrom (x :: a) :: Rep a\r\n type PTo (x :: Rep a) :: a\r\n\r\nclass SGeneric k where\r\n sFrom :: forall (a :: k). Sing a > Sing (PFrom a)\r\n sTo :: forall (a :: Rep k). Sing a > Sing (PTo a :: k)\r\n sTof :: forall (a :: k). Sing a > PTo (PFrom a) :~: a\r\n sFot :: forall (a :: Rep k). Sing a > PFrom (PTo a :: k) :~: a\r\n\r\n\r\n\r\ninstance Generic () where\r\n type Rep () = U1\r\n from () = MkU1\r\n to MkU1 = ()\r\n\r\ninstance PGeneric () where\r\n type PFrom '() = MkU1\r\n type PTo 'MkU1 = '()\r\n\r\ninstance SGeneric () where\r\n sFrom STuple0 = SMkU1\r\n sTo SMkU1 = STuple0\r\n sTof STuple0 = Refl\r\n sFot SMkU1 = Refl\r\n\r\n\r\n\r\nclass SDecide k where\r\n   Compute a proof or disproof of equality, given two singletons.\r\n (%~) :: forall (a :: k) (b :: k). Sing a > Sing b > Decision (a :~: b)\r\n default (%~) :: forall (a :: k) (b :: k). (SGeneric k, SDecide (Rep k))\r\n => Sing a > Sing b > Decision (a :~: b)\r\n s1 %~ s2 = case sFrom s1 %~ sFrom s2 of\r\n Proved (Refl :: PFrom a :~: PFrom b) >\r\n let r :: PTo (PFrom a) :~: PTo (PFrom b)\r\n r = Refl\r\n\r\n sTof1 :: PTo (PFrom a) :~: a\r\n sTof1 = sTof s1\r\n\r\n sTof2 :: PTo (PFrom b) :~: b\r\n sTof2 = sTof s2\r\n in Proved (sym sTof1 `trans` r `trans` sTof2)\r\n Disproved contra > Disproved (\\Refl > contra Refl)\r\n\r\ninstance SDecide U1 where\r\n SMkU1 %~ SMkU1 = Proved Refl\r\n\r\ninstance SDecide ()\r\n}}}\r\n\r\nHowever, it throws a Core Lint error with `dcorelint`. The full error is absolutely massive, so I'll attach it separately. Here is the toplevel bit:\r\n\r\n{{{\r\n*** Core Lint errors : in result of Simplifier ***\r\n<no location info>: warning:\r\n In the expression: <elided>\r\n Fromtype of Cast differs from type of enclosed expression\r\n Fromtype: U1\r\n Type of enclosed expr: Rep ()\r\n Actual enclosed expr: PFrom a_a1Fm\r\n Coercion used in cast: Sym (D:R:Rep()[0])\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15343Implicitly quantifying a kind variable causes GHC 8.6 to panic (coercionKind)20190707T18:13:05ZRyan ScottImplicitly quantifying a kind variable causes GHC 8.6 to panic (coercionKind)The following program panics on GHC 8.6 and later:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Type.Equality
data family Sing :: forall k. k > Type
data SomeSing :: Type > Type where
SomeSing :: Sing (a :: k) > SomeSing k
class SingKind k where
type Demote k :: Type
fromSing :: Sing (a :: k) > Demote k
toSing :: Demote k > SomeSing k
data instance Sing (z :: a :~~: b) where
SHRefl :: Sing HRefl
instance SingKind (a :~~: b) where
type Demote (a :~~: b) = a :~~: b
fromSing SHRefl = HRefl
toSing HRefl = SomeSing SHRefl
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
(~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)
(p :: forall (z :: Type) (y :: z). (a :~~: y) ~> Type)
(r :: a :~~: b).
Sing r
> Apply p HRefl
> Apply p r
(~>:~~:) SHRefl pHRefl = pHRefl
type family Why (a :: j) (e :: a :~~: (y :: z)) :: Type where
Why a (_ :: a :~~: y) = y :~~: a
data WhySym (a :: j) :: forall (y :: z). (a :~~: y) ~> Type
 data WhySym (a :: j) :: forall z (y :: z). (a :~~: y) ~> Type
 The version above does NOT panic
type instance Apply (WhySym a) e = Why a e
hsym :: forall (j :: Type) (k :: Type) (a :: j) (b :: k).
a :~~: b > b :~~: a
hsym eq = case toSing eq of
SomeSing (singEq :: Sing r) >
(~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
```
```
$ /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.20180627 for x86_64unknownlinux):
coercionKind
Nth:3
(Inst {co_a1jI} (Coh <k_a1js[sk:1]>_N (Nth:0 (Sym {co_a1jI}))))
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
pprPanic, called at compiler/types/Coercion.hs:1887:9 in ghc:Coercion
```
As noted in the comments, replacing `WhySym` with a version that explicitly quantifies `z` avoids the panic.
This is a regression from GHC 8.4.3, in which the program simply errored:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:56:38: error:
• Expected kind ‘forall z (y :: z). (a1 :~~: y) ~> *’,
but ‘WhySym a’ has kind ‘forall (y :: z0).
TyFun (a1 :~~: y) * > *’
• In the type ‘(WhySym a)’
In the expression: (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
In a case alternative:
SomeSing (singEq :: Sing r)
> (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
• Relevant bindings include
singEq :: Sing a2 (bound at Bug.hs:55:23)
eq :: a1 :~~: b (bound at Bug.hs:54:6)
hsym :: (a1 :~~: b) > b :~~: a1 (bound at Bug.hs:54:1)

56  (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
 ^^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Implicitly quantifying a kind variable causes GHC 8.6 to panic (coercionKind)","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 panics on GHC 8.6 and later:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ndata family Sing :: forall k. k > Type\r\ndata SomeSing :: Type > Type where\r\n SomeSing :: Sing (a :: k) > SomeSing k\r\n\r\nclass SingKind k where\r\n type Demote k :: Type\r\n fromSing :: Sing (a :: k) > Demote k\r\n toSing :: Demote k > SomeSing k\r\n\r\ndata instance Sing (z :: a :~~: b) where\r\n SHRefl :: Sing HRefl\r\n\r\ninstance SingKind (a :~~: b) where\r\n type Demote (a :~~: b) = a :~~: b\r\n fromSing SHRefl = HRefl\r\n toSing HRefl = SomeSing SHRefl\r\n\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\n(~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)\r\n (p :: forall (z :: Type) (y :: z). (a :~~: y) ~> Type)\r\n (r :: a :~~: b).\r\n Sing r\r\n > Apply p HRefl\r\n > Apply p r\r\n(~>:~~:) SHRefl pHRefl = pHRefl\r\n\r\ntype family Why (a :: j) (e :: a :~~: (y :: z)) :: Type where\r\n Why a (_ :: a :~~: y) = y :~~: a\r\n\r\ndata WhySym (a :: j) :: forall (y :: z). (a :~~: y) ~> Type\r\n data WhySym (a :: j) :: forall z (y :: z). (a :~~: y) ~> Type\r\n The version above does NOT panic\r\ntype instance Apply (WhySym a) e = Why a e\r\n\r\nhsym :: forall (j :: Type) (k :: Type) (a :: j) (b :: k).\r\n a :~~: b > b :~~: a\r\nhsym eq = case toSing eq of\r\n SomeSing (singEq :: Sing r) >\r\n (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl\r\n}}}\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.20180627 for x86_64unknownlinux):\r\n coercionKind\r\n Nth:3\r\n (Inst {co_a1jI} (Coh <k_a1js[sk:1]>_N (Nth:0 (Sym {co_a1jI}))))\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:1887:9 in ghc:Coercion\r\n}}}\r\n\r\nAs noted in the comments, replacing `WhySym` with a version that explicitly quantifies `z` avoids the panic.\r\n\r\nThis is a regression from GHC 8.4.3, in which the program simply errored:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:56:38: error:\r\n • Expected kind ‘forall z (y :: z). (a1 :~~: y) ~> *’,\r\n but ‘WhySym a’ has kind ‘forall (y :: z0).\r\n TyFun (a1 :~~: y) * > *’\r\n • In the type ‘(WhySym a)’\r\n In the expression: (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl\r\n In a case alternative:\r\n SomeSing (singEq :: Sing r)\r\n > (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl\r\n • Relevant bindings include\r\n singEq :: Sing a2 (bound at Bug.hs:55:23)\r\n eq :: a1 :~~: b (bound at Bug.hs:54:6)\r\n hsym :: (a1 :~~: b) > b :~~: a1 (bound at Bug.hs:54:1)\r\n \r\n56  (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl\r\n  ^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >The following program panics on GHC 8.6 and later:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Type.Equality
data family Sing :: forall k. k > Type
data SomeSing :: Type > Type where
SomeSing :: Sing (a :: k) > SomeSing k
class SingKind k where
type Demote k :: Type
fromSing :: Sing (a :: k) > Demote k
toSing :: Demote k > SomeSing k
data instance Sing (z :: a :~~: b) where
SHRefl :: Sing HRefl
instance SingKind (a :~~: b) where
type Demote (a :~~: b) = a :~~: b
fromSing SHRefl = HRefl
toSing HRefl = SomeSing SHRefl
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
(~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)
(p :: forall (z :: Type) (y :: z). (a :~~: y) ~> Type)
(r :: a :~~: b).
Sing r
> Apply p HRefl
> Apply p r
(~>:~~:) SHRefl pHRefl = pHRefl
type family Why (a :: j) (e :: a :~~: (y :: z)) :: Type where
Why a (_ :: a :~~: y) = y :~~: a
data WhySym (a :: j) :: forall (y :: z). (a :~~: y) ~> Type
 data WhySym (a :: j) :: forall z (y :: z). (a :~~: y) ~> Type
 The version above does NOT panic
type instance Apply (WhySym a) e = Why a e
hsym :: forall (j :: Type) (k :: Type) (a :: j) (b :: k).
a :~~: b > b :~~: a
hsym eq = case toSing eq of
SomeSing (singEq :: Sing r) >
(~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
```
```
$ /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.20180627 for x86_64unknownlinux):
coercionKind
Nth:3
(Inst {co_a1jI} (Coh <k_a1js[sk:1]>_N (Nth:0 (Sym {co_a1jI}))))
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
pprPanic, called at compiler/types/Coercion.hs:1887:9 in ghc:Coercion
```
As noted in the comments, replacing `WhySym` with a version that explicitly quantifies `z` avoids the panic.
This is a regression from GHC 8.4.3, in which the program simply errored:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:56:38: error:
• Expected kind ‘forall z (y :: z). (a1 :~~: y) ~> *’,
but ‘WhySym a’ has kind ‘forall (y :: z0).
TyFun (a1 :~~: y) * > *’
• In the type ‘(WhySym a)’
In the expression: (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
In a case alternative:
SomeSing (singEq :: Sing r)
> (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
• Relevant bindings include
singEq :: Sing a2 (bound at Bug.hs:55:23)
eq :: a1 :~~: b (bound at Bug.hs:54:6)
hsym :: (a1 :~~: b) > b :~~: a1 (bound at Bug.hs:54:1)

56  (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
 ^^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Implicitly quantifying a kind variable causes GHC 8.6 to panic (coercionKind)","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 panics on GHC 8.6 and later:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ndata family Sing :: forall k. k > Type\r\ndata SomeSing :: Type > Type where\r\n SomeSing :: Sing (a :: k) > SomeSing k\r\n\r\nclass SingKind k where\r\n type Demote k :: Type\r\n fromSing :: Sing (a :: k) > Demote k\r\n toSing :: Demote k > SomeSing k\r\n\r\ndata instance Sing (z :: a :~~: b) where\r\n SHRefl :: Sing HRefl\r\n\r\ninstance SingKind (a :~~: b) where\r\n type Demote (a :~~: b) = a :~~: b\r\n fromSing SHRefl = HRefl\r\n toSing HRefl = SomeSing SHRefl\r\n\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\n(~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)\r\n (p :: forall (z :: Type) (y :: z). (a :~~: y) ~> Type)\r\n (r :: a :~~: b).\r\n Sing r\r\n > Apply p HRefl\r\n > Apply p r\r\n(~>:~~:) SHRefl pHRefl = pHRefl\r\n\r\ntype family Why (a :: j) (e :: a :~~: (y :: z)) :: Type where\r\n Why a (_ :: a :~~: y) = y :~~: a\r\n\r\ndata WhySym (a :: j) :: forall (y :: z). (a :~~: y) ~> Type\r\n data WhySym (a :: j) :: forall z (y :: z). (a :~~: y) ~> Type\r\n The version above does NOT panic\r\ntype instance Apply (WhySym a) e = Why a e\r\n\r\nhsym :: forall (j :: Type) (k :: Type) (a :: j) (b :: k).\r\n a :~~: b > b :~~: a\r\nhsym eq = case toSing eq of\r\n SomeSing (singEq :: Sing r) >\r\n (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl\r\n}}}\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.20180627 for x86_64unknownlinux):\r\n coercionKind\r\n Nth:3\r\n (Inst {co_a1jI} (Coh <k_a1js[sk:1]>_N (Nth:0 (Sym {co_a1jI}))))\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:1887:9 in ghc:Coercion\r\n}}}\r\n\r\nAs noted in the comments, replacing `WhySym` with a version that explicitly quantifies `z` avoids the panic.\r\n\r\nThis is a regression from GHC 8.4.3, in which the program simply errored:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:56:38: error:\r\n • Expected kind ‘forall z (y :: z). (a1 :~~: y) ~> *’,\r\n but ‘WhySym a’ has kind ‘forall (y :: z0).\r\n TyFun (a1 :~~: y) * > *’\r\n • In the type ‘(WhySym a)’\r\n In the expression: (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl\r\n In a case alternative:\r\n SomeSing (singEq :: Sing r)\r\n > (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl\r\n • Relevant bindings include\r\n singEq :: Sing a2 (bound at Bug.hs:55:23)\r\n eq :: a1 :~~: b (bound at Bug.hs:54:6)\r\n hsym :: (a1 :~~: b) > b :~~: a1 (bound at Bug.hs:54:1)\r\n \r\n56  (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl\r\n  ^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15330Error message prints invisible kind arguments in a visible matter20190707T18:13:08ZRyan ScottError message prints invisible kind arguments in a visible matterConsider the following program:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
import Data.Proxy
data T :: forall a. a > Type
f1 :: Proxy (T True)
f1 = "foo"
f2 :: forall (t :: forall a. a > Type).
Proxy (t True)
f2 = "foo"
```
This program doesn't typecheck (for good reason). The error messages, however, are a bit iffy:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:6: error:
• Couldn't match expected type ‘Proxy (T 'True)’
with actual type ‘[Char]’
• In the expression: "foo"
In an equation for ‘f1’: f1 = "foo"

11  f1 = "foo"
 ^^^^^
Bug.hs:15:6: error:
• Couldn't match expected type ‘Proxy (t Bool 'True)’
with actual type ‘[Char]’
• In the expression: "foo"
In an equation for ‘f2’: f2 = "foo"
• Relevant bindings include
f2 :: Proxy (t Bool 'True) (bound at Bug.hs:15:1)

15  f2 = "foo"
 ^^^^^
```
Note that in the error message for `f1`, the type `T 'True` is printed correctly—the invisible `Bool` argument is omitted. However, in the error message for `f2`, this is not the case, as the type `t Bool 'True` is printed. That `Bool` is an invisible argument as well, and should not be printed without the use of, say, `fprintexplicitkinds`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 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":"Error message prints invisible kind arguments in a visible matter","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #} \r\n{# LANGUAGE TypeInType #} \r\nmodule Bug where \r\n \r\nimport Data.Kind \r\nimport Data.Proxy \r\n \r\ndata T :: forall a. a > Type \r\n \r\nf1 :: Proxy (T True)\r\nf1 = \"foo\"\r\n\r\nf2 :: forall (t :: forall a. a > Type).\r\n Proxy (t True)\r\nf2 = \"foo\"\r\n}}}\r\n\r\nThis program doesn't typecheck (for good reason). The error messages, however, are a bit iffy:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:11:6: error:\r\n • Couldn't match expected type ‘Proxy (T 'True)’\r\n with actual type ‘[Char]’\r\n • In the expression: \"foo\"\r\n In an equation for ‘f1’: f1 = \"foo\"\r\n \r\n11  f1 = \"foo\"\r\n  ^^^^^\r\n\r\nBug.hs:15:6: error:\r\n • Couldn't match expected type ‘Proxy (t Bool 'True)’\r\n with actual type ‘[Char]’\r\n • In the expression: \"foo\"\r\n In an equation for ‘f2’: f2 = \"foo\"\r\n • Relevant bindings include\r\n f2 :: Proxy (t Bool 'True) (bound at Bug.hs:15:1)\r\n \r\n15  f2 = \"foo\"\r\n  ^^^^^\r\n}}}\r\n\r\nNote that in the error message for `f1`, the type `T 'True` is printed correctly—the invisible `Bool` argument is omitted. However, in the error message for `f2`, this is not the case, as the type `t Bool 'True` is printed. That `Bool` is an invisible argument as well, and should not be printed without the use of, say, `fprintexplicitkinds`.","type_of_failure":"OtherFailure","blocking":[]} >Consider the following program:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
import Data.Proxy
data T :: forall a. a > Type
f1 :: Proxy (T True)
f1 = "foo"
f2 :: forall (t :: forall a. a > Type).
Proxy (t True)
f2 = "foo"
```
This program doesn't typecheck (for good reason). The error messages, however, are a bit iffy:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:6: error:
• Couldn't match expected type ‘Proxy (T 'True)’
with actual type ‘[Char]’
• In the expression: "foo"
In an equation for ‘f1’: f1 = "foo"

11  f1 = "foo"
 ^^^^^
Bug.hs:15:6: error:
• Couldn't match expected type ‘Proxy (t Bool 'True)’
with actual type ‘[Char]’
• In the expression: "foo"
In an equation for ‘f2’: f2 = "foo"
• Relevant bindings include
f2 :: Proxy (t Bool 'True) (bound at Bug.hs:15:1)

15  f2 = "foo"
 ^^^^^
```
Note that in the error message for `f1`, the type `T 'True` is printed correctly—the invisible `Bool` argument is omitted. However, in the error message for `f2`, this is not the case, as the type `t Bool 'True` is printed. That `Bool` is an invisible argument as well, and should not be printed without the use of, say, `fprintexplicitkinds`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 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":"Error message prints invisible kind arguments in a visible matter","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #} \r\n{# LANGUAGE TypeInType #} \r\nmodule Bug where \r\n \r\nimport Data.Kind \r\nimport Data.Proxy \r\n \r\ndata T :: forall a. a > Type \r\n \r\nf1 :: Proxy (T True)\r\nf1 = \"foo\"\r\n\r\nf2 :: forall (t :: forall a. a > Type).\r\n Proxy (t True)\r\nf2 = \"foo\"\r\n}}}\r\n\r\nThis program doesn't typecheck (for good reason). The error messages, however, are a bit iffy:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:11:6: error:\r\n • Couldn't match expected type ‘Proxy (T 'True)’\r\n with actual type ‘[Char]’\r\n • In the expression: \"foo\"\r\n In an equation for ‘f1’: f1 = \"foo\"\r\n \r\n11  f1 = \"foo\"\r\n  ^^^^^\r\n\r\nBug.hs:15:6: error:\r\n • Couldn't match expected type ‘Proxy (t Bool 'True)’\r\n with actual type ‘[Char]’\r\n • In the expression: \"foo\"\r\n In an equation for ‘f2’: f2 = \"foo\"\r\n • Relevant bindings include\r\n f2 :: Proxy (t Bool 'True) (bound at Bug.hs:15:1)\r\n \r\n15  f2 = \"foo\"\r\n  ^^^^^\r\n}}}\r\n\r\nNote that in the error message for `f1`, the type `T 'True` is printed correctly—the invisible `Bool` argument is omitted. However, in the error message for `f2`, this is not the case, as the type `t Bool 'True` is printed. That `Bool` is an invisible argument as well, and should not be printed without the use of, say, `fprintexplicitkinds`.","type_of_failure":"OtherFailure","blocking":[]} >8.8.1https://gitlab.haskell.org/ghc/ghc//issues/15308Error message prints explicit kinds when it shouldn't20190707T18:13:20ZRyan ScottError message prints explicit kinds when it shouldn'tWhen compiled, this program:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeInType #}
{# OPTIONS_GHC fnoprintexplicitkinds #}
module Bug where
import Data.Kind
data Foo (a :: Type) :: forall b. (a > b > Type) > Type where
MkFoo :: Foo a f
f :: Foo a f > String
f = show
```
Gives the following error:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:13:5: error:
• No instance for (Show (Foo a b f)) arising from a use of ‘show’
• In the expression: show
In an equation for ‘f’: f = show

13  f = show
 ^^^^
```
This error message is slightly incorrect, however. In "`No instance for (Show (Foo a b f))`", it claims that `Foo` has three visible type parameters, but it only has two. (I've even made sure to enable `fnoprintexplicitkinds` at the type to ensure that the invisible `b` kind shouldn't get printed, but it was anyway.)
This is a regression that was apparently introduced between GHC 8.0 and 8.2, since in GHC 8.0.2, it prints the correct thing:
```
$ /opt/ghc/8.0.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:13:5: error:
• No instance for (Show (Foo a f)) arising from a use of ‘show’
• In the expression: show
In an equation for ‘f’: f = show
```
But it does not in GHC 8.2.1:
```
$ /opt/ghc/8.2.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:13:5: error:
• No instance for (Show (Foo a b f)) arising from a use of ‘show’
• In the expression: show
In an equation for ‘f’: f = show

13  f = show
 ^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 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":"Error message prints explicit kinds when it shouldn't","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When compiled, this program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeInType #}\r\n{# OPTIONS_GHC fnoprintexplicitkinds #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata Foo (a :: Type) :: forall b. (a > b > Type) > Type where\r\n MkFoo :: Foo a f\r\n\r\nf :: Foo a f > String\r\nf = show\r\n}}}\r\n\r\nGives the following error:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:13:5: error:\r\n • No instance for (Show (Foo a b f)) arising from a use of ‘show’\r\n • In the expression: show\r\n In an equation for ‘f’: f = show\r\n \r\n13  f = show\r\n  ^^^^\r\n}}}\r\n\r\nThis error message is slightly incorrect, however. In \"`No instance for (Show (Foo a b f))`\", it claims that `Foo` has three visible type parameters, but it only has two. (I've even made sure to enable `fnoprintexplicitkinds` at the type to ensure that the invisible `b` kind shouldn't get printed, but it was anyway.)\r\n\r\nThis is a regression that was apparently introduced between GHC 8.0 and 8.2, since in GHC 8.0.2, it prints the correct thing:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:13:5: error:\r\n • No instance for (Show (Foo a f)) arising from a use of ‘show’\r\n • In the expression: show\r\n In an equation for ‘f’: f = show\r\n}}}\r\n\r\nBut it does not in GHC 8.2.1:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:13:5: error:\r\n • No instance for (Show (Foo a b f)) arising from a use of ‘show’\r\n • In the expression: show\r\n In an equation for ‘f’: f = show\r\n \r\n13  f = show\r\n  ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >When compiled, this program:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeInType #}
{# OPTIONS_GHC fnoprintexplicitkinds #}
module Bug where
import Data.Kind
data Foo (a :: Type) :: forall b. (a > b > Type) > Type where
MkFoo :: Foo a f
f :: Foo a f > String
f = show
```
Gives the following error:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:13:5: error:
• No instance for (Show (Foo a b f)) arising from a use of ‘show’
• In the expression: show
In an equation for ‘f’: f = show

13  f = show
 ^^^^
```
This error message is slightly incorrect, however. In "`No instance for (Show (Foo a b f))`", it claims that `Foo` has three visible type parameters, but it only has two. (I've even made sure to enable `fnoprintexplicitkinds` at the type to ensure that the invisible `b` kind shouldn't get printed, but it was anyway.)
This is a regression that was apparently introduced between GHC 8.0 and 8.2, since in GHC 8.0.2, it prints the correct thing:
```
$ /opt/ghc/8.0.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:13:5: error:
• No instance for (Show (Foo a f)) arising from a use of ‘show’
• In the expression: show
In an equation for ‘f’: f = show
```
But it does not in GHC 8.2.1:
```
$ /opt/ghc/8.2.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:13:5: error:
• No instance for (Show (Foo a b f)) arising from a use of ‘show’
• In the expression: show
In an equation for ‘f’: f = show

13  f = show
 ^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 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":"Error message prints explicit kinds when it shouldn't","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When compiled, this program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeInType #}\r\n{# OPTIONS_GHC fnoprintexplicitkinds #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata Foo (a :: Type) :: forall b. (a > b > Type) > Type where\r\n MkFoo :: Foo a f\r\n\r\nf :: Foo a f > String\r\nf = show\r\n}}}\r\n\r\nGives the following error:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:13:5: error:\r\n • No instance for (Show (Foo a b f)) arising from a use of ‘show’\r\n • In the expression: show\r\n In an equation for ‘f’: f = show\r\n \r\n13  f = show\r\n  ^^^^\r\n}}}\r\n\r\nThis error message is slightly incorrect, however. In \"`No instance for (Show (Foo a b f))`\", it claims that `Foo` has three visible type parameters, but it only has two. (I've even made sure to enable `fnoprintexplicitkinds` at the type to ensure that the invisible `b` kind shouldn't get printed, but it was anyway.)\r\n\r\nThis is a regression that was apparently introduced between GHC 8.0 and 8.2, since in GHC 8.0.2, it prints the correct thing:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:13:5: error:\r\n • No instance for (Show (Foo a f)) arising from a use of ‘show’\r\n • In the expression: show\r\n In an equation for ‘f’: f = show\r\n}}}\r\n\r\nBut it does not in GHC 8.2.1:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:13:5: error:\r\n • No instance for (Show (Foo a b f)) arising from a use of ‘show’\r\n • In the expression: show\r\n In an equation for ‘f’: f = show\r\n \r\n13  f = show\r\n  ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://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/15245Data family promotion is possible20190707T18:13:38ZVladislav ZavialovData family promotion is possibleThe User's Guide states that data families cannot be promoted, even with `XTypeInType`:
> We promote data types and newtypes; type synonyms and type/data families are not promoted.
>
> The flag TypeInType (which implies DataKinds) relaxes some of these restrictions, allowing:
>
> Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types.
And yet the following code typechecks and runs:
```hs
{# LANGUAGE TypeFamilies, TypeInType, TypeApplications #}
import Type.Reflection
data family K
data instance K = MkK
main = print (typeRep @'MkK)
```
Is this a GHC bug or a documentation bug? I asked in IRC but I'm still confused:
```
<intindex> The user guide states that data families aren't promoted even when XTypeInType is enabled. Where's the logic that ensures this? I checked with `data family K; data instance K = MkK` and I can use `'MkK` with no errors/warnings.
<intindex> https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#overview "Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types."
<intindex> Is this info outdated?
<RyanGlScott> intindex: Is this in GHCi?
<RyanGlScott> It certainly fails in GHC
<RyanGlScott> But I think I understand why the former works
<intindex> RyanGlScott, yes, I'm checking this in GHCi
<RyanGlScott> intindex: So here's my understanding of how this works
<RyanGlScott> GHC kindchecks toplevel declarations using a rather primitive SCC analysis
<RyanGlScott> In particular, it's primitive in the sense that data family instances give it a lot of trouble
<RyanGlScott> If you tried taking your code and putting it into a standalone .hs file and compiling that, then it would definitely complain about a promoted use of MkT
<RyanGlScott> As luck would have it, though, you were trying things out in GHCi
<RyanGlScott> Which essentially checks each line of input as its own strongly connected group of declarations
<RyanGlScott> So you can define MkT on one line and promote it in subsequent lines, since they're separate in the sense
<RyanGlScott> *that sense
<intindex> this sounds related to Trac #12088, and then I could work around it in GHC by using `$(return [])`, so data families are actually promoted anyway and this has nothing to do with GHC needing more powerful type theory
<RyanGlScott> Well, it does need more powerful type theory in the sense that that's a prerequisite for making the SCC analysis for kindchecking sophisticated enough to handle this
<RyanGlScott> But yes, it's quite simple to work around by using Template Haskell to explicitly split up groups.
<intindex> https://gist.github.com/intindex/c6cc1e20c4b9b5c99af40ee4e23ecb61 this works and no template haskell involved
<intindex> The reason I'm asking is that I'm touching this part of the User's Guide and I don't know what to write there.
<RyanGlScott> Huh, now that's interesting
<intindex> RyanGlScott, the only check I could find that controls what's promoted and what's not is 'isLegacyPromotableDataCon'  and enabling XTypeInType disables this check.
<RyanGlScott> intindex: Right, that's baffling me
<RyanGlScott> Since that's supposed to be checked every time you promote a data constructor (I think)
<RyanGlScott> intindex: File a bug about that, I suppose
<RyanGlScott> Richard (who's sitting next to me right now) seems to think that that shouldn't be possible
<intindex> RyanGlScott, the thing is, I happily removed this check completely in D4748. Does this mean I have to restore a weaker version of it that only checks for data families? Why?
<intindex> Is it bad that XDataKinds promotes data family constructors? Looks like I can just remove the "restrictions" part of the user guide and be done with it
<RyanGlScott> intindex: In theory, that shouldn't be possible
<intindex> OK, then what the check should be? No data families, any other restrictions?
<RyanGlScott> I might qualify that with "no data family instances defined in the same module"
<RyanGlScott> (Or to be precise, in the same SCC, but that's probably too technical for the users' guide)
<intindex> Well, this sounds hard to check. I was thinking along the lines of keeping the 'not (isFamInstTyCon (dataConTyCon dc))' part of the check...
<RyanGlScott> Oh, I thought you were only changing the users' guide :)
<intindex> Well, at this point I'm confused if I should change only the user guide or the check as well. If data families shouldn't be promoted ever, then I'll change GHC. If the limitation is about the current SCC group, I can just mention Trac #12088 as a known infelicity in the User's Guide
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Documentation 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  RyanGlScott, goldfire 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Data family promotion is possible","status":"New","operating_system":"","component":"Documentation","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["RyanGlScott","goldfire"],"type":"Bug","description":"The User's Guide states that data families cannot be promoted, even with `XTypeInType`:\r\n\r\n> We promote data types and newtypes; type synonyms and type/data families are not promoted.\r\n>\r\n> The flag TypeInType (which implies DataKinds) relaxes some of these restrictions, allowing:\r\n>\r\n> Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types.\r\n\r\nAnd yet the following code typechecks and runs:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies, TypeInType, TypeApplications #}\r\n\r\nimport Type.Reflection\r\n\r\ndata family K\r\ndata instance K = MkK\r\n\r\nmain = print (typeRep @'MkK)\r\n}}}\r\n\r\nIs this a GHC bug or a documentation bug? I asked in IRC but I'm still confused:\r\n\r\n{{{\r\n<intindex> The user guide states that data families aren't promoted even when XTypeInType is enabled. Where's the logic that ensures this? I checked with `data family K; data instance K = MkK` and I can use `'MkK` with no errors/warnings.\r\n<intindex> https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#overview \"Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types.\"\r\n<intindex> Is this info outdated?\r\n<RyanGlScott> intindex: Is this in GHCi?\r\n<RyanGlScott> It certainly fails in GHC\r\n<RyanGlScott> But I think I understand why the former works\r\n<intindex> RyanGlScott, yes, I'm checking this in GHCi\r\n<RyanGlScott> intindex: So here's my understanding of how this works\r\n<RyanGlScott> GHC kindchecks toplevel declarations using a rather primitive SCC analysis\r\n<RyanGlScott> In particular, it's primitive in the sense that data family instances give it a lot of trouble\r\n<RyanGlScott> If you tried taking your code and putting it into a standalone .hs file and compiling that, then it would definitely complain about a promoted use of MkT\r\n<RyanGlScott> As luck would have it, though, you were trying things out in GHCi\r\n<RyanGlScott> Which essentially checks each line of input as its own strongly connected group of declarations\r\n<RyanGlScott> So you can define MkT on one line and promote it in subsequent lines, since they're separate in the sense\r\n<RyanGlScott> *that sense\r\n<intindex> this sounds related to Trac #12088, and then I could work around it in GHC by using `$(return [])`, so data families are actually promoted anyway and this has nothing to do with GHC needing more powerful type theory\r\n<RyanGlScott> Well, it does need more powerful type theory in the sense that that's a prerequisite for making the SCC analysis for kindchecking sophisticated enough to handle this\r\n<RyanGlScott> But yes, it's quite simple to work around by using Template Haskell to explicitly split up groups.\r\n<intindex> https://gist.github.com/intindex/c6cc1e20c4b9b5c99af40ee4e23ecb61 this works and no template haskell involved\r\n<intindex> The reason I'm asking is that I'm touching this part of the User's Guide and I don't know what to write there.\r\n<RyanGlScott> Huh, now that's interesting\r\n<intindex> RyanGlScott, the only check I could find that controls what's promoted and what's not is 'isLegacyPromotableDataCon'  and enabling XTypeInType disables this check.\r\n<RyanGlScott> intindex: Right, that's baffling me\r\n<RyanGlScott> Since that's supposed to be checked every time you promote a data constructor (I think)\r\n<RyanGlScott> intindex: File a bug about that, I suppose\r\n<RyanGlScott> Richard (who's sitting next to me right now) seems to think that that shouldn't be possible\r\n<intindex> RyanGlScott, the thing is, I happily removed this check completely in D4748. Does this mean I have to restore a weaker version of it that only checks for data families? Why?\r\n<intindex> Is it bad that XDataKinds promotes data family constructors? Looks like I can just remove the \"restrictions\" part of the user guide and be done with it\r\n<RyanGlScott> intindex: In theory, that shouldn't be possible\r\n<intindex> OK, then what the check should be? No data families, any other restrictions?\r\n<RyanGlScott> I might qualify that with \"no data family instances defined in the same module\"\r\n<RyanGlScott> (Or to be precise, in the same SCC, but that's probably too technical for the users' guide)\r\n<intindex> Well, this sounds hard to check. I was thinking along the lines of keeping the 'not (isFamInstTyCon (dataConTyCon dc))' part of the check...\r\n<RyanGlScott> Oh, I thought you were only changing the users' guide :)\r\n<intindex> Well, at this point I'm confused if I should change only the user guide or the check as well. If data families shouldn't be promoted ever, then I'll change GHC. If the limitation is about the current SCC group, I can just mention Trac #12088 as a known infelicity in the User's Guide\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >The User's Guide states that data families cannot be promoted, even with `XTypeInType`:
> We promote data types and newtypes; type synonyms and type/data families are not promoted.
>
> The flag TypeInType (which implies DataKinds) relaxes some of these restrictions, allowing:
>
> Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types.
And yet the following code typechecks and runs:
```hs
{# LANGUAGE TypeFamilies, TypeInType, TypeApplications #}
import Type.Reflection
data family K
data instance K = MkK
main = print (typeRep @'MkK)
```
Is this a GHC bug or a documentation bug? I asked in IRC but I'm still confused:
```
<intindex> The user guide states that data families aren't promoted even when XTypeInType is enabled. Where's the logic that ensures this? I checked with `data family K; data instance K = MkK` and I can use `'MkK` with no errors/warnings.
<intindex> https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#overview "Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types."
<intindex> Is this info outdated?
<RyanGlScott> intindex: Is this in GHCi?
<RyanGlScott> It certainly fails in GHC
<RyanGlScott> But I think I understand why the former works
<intindex> RyanGlScott, yes, I'm checking this in GHCi
<RyanGlScott> intindex: So here's my understanding of how this works
<RyanGlScott> GHC kindchecks toplevel declarations using a rather primitive SCC analysis
<RyanGlScott> In particular, it's primitive in the sense that data family instances give it a lot of trouble
<RyanGlScott> If you tried taking your code and putting it into a standalone .hs file and compiling that, then it would definitely complain about a promoted use of MkT
<RyanGlScott> As luck would have it, though, you were trying things out in GHCi
<RyanGlScott> Which essentially checks each line of input as its own strongly connected group of declarations
<RyanGlScott> So you can define MkT on one line and promote it in subsequent lines, since they're separate in the sense
<RyanGlScott> *that sense
<intindex> this sounds related to Trac #12088, and then I could work around it in GHC by using `$(return [])`, so data families are actually promoted anyway and this has nothing to do with GHC needing more powerful type theory
<RyanGlScott> Well, it does need more powerful type theory in the sense that that's a prerequisite for making the SCC analysis for kindchecking sophisticated enough to handle this
<RyanGlScott> But yes, it's quite simple to work around by using Template Haskell to explicitly split up groups.
<intindex> https://gist.github.com/intindex/c6cc1e20c4b9b5c99af40ee4e23ecb61 this works and no template haskell involved
<intindex> The reason I'm asking is that I'm touching this part of the User's Guide and I don't know what to write there.
<RyanGlScott> Huh, now that's interesting
<intindex> RyanGlScott, the only check I could find that controls what's promoted and what's not is 'isLegacyPromotableDataCon'  and enabling XTypeInType disables this check.
<RyanGlScott> intindex: Right, that's baffling me
<RyanGlScott> Since that's supposed to be checked every time you promote a data constructor (I think)
<RyanGlScott> intindex: File a bug about that, I suppose
<RyanGlScott> Richard (who's sitting next to me right now) seems to think that that shouldn't be possible
<intindex> RyanGlScott, the thing is, I happily removed this check completely in D4748. Does this mean I have to restore a weaker version of it that only checks for data families? Why?
<intindex> Is it bad that XDataKinds promotes data family constructors? Looks like I can just remove the "restrictions" part of the user guide and be done with it
<RyanGlScott> intindex: In theory, that shouldn't be possible
<intindex> OK, then what the check should be? No data families, any other restrictions?
<RyanGlScott> I might qualify that with "no data family instances defined in the same module"
<RyanGlScott> (Or to be precise, in the same SCC, but that's probably too technical for the users' guide)
<intindex> Well, this sounds hard to check. I was thinking along the lines of keeping the 'not (isFamInstTyCon (dataConTyCon dc))' part of the check...
<RyanGlScott> Oh, I thought you were only changing the users' guide :)
<intindex> Well, at this point I'm confused if I should change only the user guide or the check as well. If data families shouldn't be promoted ever, then I'll change GHC. If the limitation is about the current SCC group, I can just mention Trac #12088 as a known infelicity in the User's Guide
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Documentation 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  RyanGlScott, goldfire 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Data family promotion is possible","status":"New","operating_system":"","component":"Documentation","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["RyanGlScott","goldfire"],"type":"Bug","description":"The User's Guide states that data families cannot be promoted, even with `XTypeInType`:\r\n\r\n> We promote data types and newtypes; type synonyms and type/data families are not promoted.\r\n>\r\n> The flag TypeInType (which implies DataKinds) relaxes some of these restrictions, allowing:\r\n>\r\n> Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types.\r\n\r\nAnd yet the following code typechecks and runs:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies, TypeInType, TypeApplications #}\r\n\r\nimport Type.Reflection\r\n\r\ndata family K\r\ndata instance K = MkK\r\n\r\nmain = print (typeRep @'MkK)\r\n}}}\r\n\r\nIs this a GHC bug or a documentation bug? I asked in IRC but I'm still confused:\r\n\r\n{{{\r\n<intindex> The user guide states that data families aren't promoted even when XTypeInType is enabled. Where's the logic that ensures this? I checked with `data family K; data instance K = MkK` and I can use `'MkK` with no errors/warnings.\r\n<intindex> https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#overview \"Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types.\"\r\n<intindex> Is this info outdated?\r\n<RyanGlScott> intindex: Is this in GHCi?\r\n<RyanGlScott> It certainly fails in GHC\r\n<RyanGlScott> But I think I understand why the former works\r\n<intindex> RyanGlScott, yes, I'm checking this in GHCi\r\n<RyanGlScott> intindex: So here's my understanding of how this works\r\n<RyanGlScott> GHC kindchecks toplevel declarations using a rather primitive SCC analysis\r\n<RyanGlScott> In particular, it's primitive in the sense that data family instances give it a lot of trouble\r\n<RyanGlScott> If you tried taking your code and putting it into a standalone .hs file and compiling that, then it would definitely complain about a promoted use of MkT\r\n<RyanGlScott> As luck would have it, though, you were trying things out in GHCi\r\n<RyanGlScott> Which essentially checks each line of input as its own strongly connected group of declarations\r\n<RyanGlScott> So you can define MkT on one line and promote it in subsequent lines, since they're separate in the sense\r\n<RyanGlScott> *that sense\r\n<intindex> this sounds related to Trac #12088, and then I could work around it in GHC by using `$(return [])`, so data families are actually promoted anyway and this has nothing to do with GHC needing more powerful type theory\r\n<RyanGlScott> Well, it does need more powerful type theory in the sense that that's a prerequisite for making the SCC analysis for kindchecking sophisticated enough to handle this\r\n<RyanGlScott> But yes, it's quite simple to work around by using Template Haskell to explicitly split up groups.\r\n<intindex> https://gist.github.com/intindex/c6cc1e20c4b9b5c99af40ee4e23ecb61 this works and no template haskell involved\r\n<intindex> The reason I'm asking is that I'm touching this part of the User's Guide and I don't know what to write there.\r\n<RyanGlScott> Huh, now that's interesting\r\n<intindex> RyanGlScott, the only check I could find that controls what's promoted and what's not is 'isLegacyPromotableDataCon'  and enabling XTypeInType disables this check.\r\n<RyanGlScott> intindex: Right, that's baffling me\r\n<RyanGlScott> Since that's supposed to be checked every time you promote a data constructor (I think)\r\n<RyanGlScott> intindex: File a bug about that, I suppose\r\n<RyanGlScott> Richard (who's sitting next to me right now) seems to think that that shouldn't be possible\r\n<intindex> RyanGlScott, the thing is, I happily removed this check completely in D4748. Does this mean I have to restore a weaker version of it that only checks for data families? Why?\r\n<intindex> Is it bad that XDataKinds promotes data family constructors? Looks like I can just remove the \"restrictions\" part of the user guide and be done with it\r\n<RyanGlScott> intindex: In theory, that shouldn't be possible\r\n<intindex> OK, then what the check should be? No data families, any other restrictions?\r\n<RyanGlScott> I might qualify that with \"no data family instances defined in the same module\"\r\n<RyanGlScott> (Or to be precise, in the same SCC, but that's probably too technical for the users' guide)\r\n<intindex> Well, this sounds hard to check. I was thinking along the lines of keeping the 'not (isFamInstTyCon (dataConTyCon dc))' part of the check...\r\n<RyanGlScott> Oh, I thought you were only changing the users' guide :)\r\n<intindex> Well, at this point I'm confused if I should change only the user guide or the check as well. If data families shouldn't be promoted ever, then I'll change GHC. If the limitation is about the current SCC group, I can just mention Trac #12088 as a known infelicity in the User's Guide\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15195Merge XPolyKinds with XTypeInType20190707T18:13:50ZRichard Eisenbergrae@richarde.devMerge XPolyKinds with XTypeInTypeAs described in [this accepted proposal](https://github.com/ghcproposals/ghcproposals/blob/master/proposals/0020notypeintype.rst).
<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  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Merge XPolyKinds with XTypeInType","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"As described in [https://github.com/ghcproposals/ghcproposals/blob/master/proposals/0020notypeintype.rst this accepted proposal].","type_of_failure":"OtherFailure","blocking":[]} >As described in [this accepted proposal](https://github.com/ghcproposals/ghcproposals/blob/master/proposals/0020notypeintype.rst).
<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  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Merge XPolyKinds with XTypeInType","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"As described in [https://github.com/ghcproposals/ghcproposals/blob/master/proposals/0020notypeintype.rst this accepted proposal].","type_of_failure":"OtherFailure","blocking":[]} >8.6.1Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc//issues/15170GHC HEAD panic (dischargeFmv)20190707T18:13:56ZRyan ScottGHC HEAD panic (dischargeFmv)The following program panics on GHC HEAD:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilyDependencies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Proxy
data family Sing (a :: k)
data SomeSing :: Type > Type where
SomeSing :: Sing (a :: k) > SomeSing k
class SingKind k where
type Demote k = (r :: Type)  r > k
fromSing :: Sing (a :: k) > Demote k
toSing :: Demote k > SomeSing k
withSomeSing :: forall k r
. SingKind k
=> Demote k
> (forall (a :: k). Sing a > r)
> r
withSomeSing x f =
case toSing x of
SomeSing x' > f x'
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t > Sing (f @@ t) }
instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where
type Demote (k1 ~> k2) = Demote k1 > Demote k2
fromSing sFun x = withSomeSing x (fromSing . applySing sFun)
toSing = undefined
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type f @@ x = Apply f x
infixl 9 @@
dcomp :: forall (a :: Type)
(b :: a ~> Type)
(c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
(f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
(g :: forall (x :: a). Proxy x ~> b @@ x)
(x :: a).
SingKind (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))
=> (forall (xx :: a) (yy :: b @@ xx). Sing (f @@ ('Proxy :: Proxy xx) @@ ('Proxy :: Proxy yy)))
> Sing g
> Sing a
> Demote (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))
dcomp _sf _ _ = undefined
```
```
$ /opt/ghc/head/bin/ghc Bug2.hs
[1 of 1] Compiling Bug ( Bug2.hs, Bug2.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.5.20180501 for x86_64unknownlinux):
dischargeFmv
[D] _ {0}:: (Apply
(f_a1ih[sk:2] xx_a1iA[tau:3] yy_a1iB[tau:3] > Sym ((TyFun
<Proxy xx_a1iA[tau:3]>_N
((TyFun
(Proxy
(Sym {co_a1jm})
(Coh <yy_a1iB[tau:3]>_N
{co_a1jm}))_N
(Sym {co_a1jB} ; (Apply
(Sym {co_a1jm})
<*>_N
(Coh ((Coh <s_a1jn[fmv:0]>_N
((TyFun
(Sym {co_a1jm})
<*>_N)_N
>_N <*>_N) ; Sym {co_a1jA}) ; (Apply
<Proxy
xx_a1iA[tau:3]>_N
((TyFun
(Sym {co_a1jm})
<*>_N)_N
>_N <*>_N)
(Coh <c_a1ig[sk:2] xx_a1iA[tau:3]>_N
(Sym ((TyFun
<Proxy
xx_a1iA[tau:3]>_N
((TyFun
(Sym {co_a1jm})
<*>_N)_N
>_N <*>_N))_N
>_N <*>_N)))
<'Proxy>_N)_N)
(Sym ((TyFun
(Sym {co_a1jm})
<*>_N)_N
>_N <*>_N)))
(Coh <yy_a1iB[tau:3]>_N
{co_a1jm}))_N))_N
>_N <*>_N))_N
>_N <*>_N))
'Proxy :: (Proxy (yy_a1iB[tau:3] > {co_a1jm}) ~> s_a1jp[fmv:0]))
~# (s_a1jQ[fmv:0] :: (Proxy (yy_a1iB[tau:3] > {co_a1jm})
~> s_a1jp[fmv:0]))
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcSMonad.hs:3047:25 in ghc:TcSMonad
```
On GHC 8.4.2, it simply throws an error:
```
$ /opt/ghc/8.4.2/bin/ghci Bug2.hs
GHCi, version 8.4.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug2.hs, interpreted )
Bug2.hs:53:71: error:
• Expected kind ‘Apply b xx’, but ‘y’ has kind ‘b @@ x’
• In the first argument of ‘Proxy’, namely ‘y’
In the first argument of ‘(~>)’, namely ‘Proxy y’
In the second argument of ‘(~>)’, namely
‘Proxy y ~> c @@ ( 'Proxy :: Proxy x) @@ y’

53  (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
 ^
```
<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 panic (dischargeFmv)","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 panics on GHC HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilyDependencies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\ndata family Sing (a :: k)\r\ndata SomeSing :: Type > Type where\r\n SomeSing :: Sing (a :: k) > SomeSing k\r\n\r\nclass SingKind k where\r\n type Demote k = (r :: Type)  r > k\r\n fromSing :: Sing (a :: k) > Demote k\r\n toSing :: Demote k > SomeSing k\r\n\r\nwithSomeSing :: forall k r\r\n . SingKind k\r\n => Demote k\r\n > (forall (a :: k). Sing a > r)\r\n > r\r\nwithSomeSing x f =\r\n case toSing x of\r\n SomeSing x' > f x'\r\n\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t > Sing (f @@ t) }\r\n\r\ninstance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where\r\n type Demote (k1 ~> k2) = Demote k1 > Demote k2\r\n fromSing sFun x = withSomeSing x (fromSing . applySing sFun)\r\n toSing = undefined\r\n\r\ndata TyFun :: Type > Type > Type\r\ntype a ~> b = TyFun a b > Type\r\ninfixr 0 ~>\r\n\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\ntype f @@ x = Apply f x\r\ninfixl 9 @@\r\n\r\ndcomp :: forall (a :: Type)\r\n (b :: a ~> Type)\r\n (c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)\r\n (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)\r\n (g :: forall (x :: a). Proxy x ~> b @@ x)\r\n (x :: a).\r\n SingKind (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))\r\n => (forall (xx :: a) (yy :: b @@ xx). Sing (f @@ ('Proxy :: Proxy xx) @@ ('Proxy :: Proxy yy)))\r\n > Sing g\r\n > Sing a\r\n > Demote (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))\r\ndcomp _sf _ _ = undefined\r\n}}}\r\n{{{\r\n$ /opt/ghc/head/bin/ghc Bug2.hs\r\n[1 of 1] Compiling Bug ( Bug2.hs, Bug2.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.5.20180501 for x86_64unknownlinux):\r\n dischargeFmv\r\n [D] _ {0}:: (Apply\r\n (f_a1ih[sk:2] xx_a1iA[tau:3] yy_a1iB[tau:3] > Sym ((TyFun\r\n <Proxy xx_a1iA[tau:3]>_N\r\n ((TyFun\r\n (Proxy\r\n (Sym {co_a1jm})\r\n (Coh <yy_a1iB[tau:3]>_N\r\n {co_a1jm}))_N\r\n (Sym {co_a1jB} ; (Apply\r\n (Sym {co_a1jm})\r\n <*>_N\r\n (Coh ((Coh <s_a1jn[fmv:0]>_N\r\n ((TyFun\r\n (Sym {co_a1jm})\r\n <*>_N)_N\r\n >_N <*>_N) ; Sym {co_a1jA}) ; (Apply\r\n <Proxy\r\n xx_a1iA[tau:3]>_N\r\n ((TyFun\r\n (Sym {co_a1jm})\r\n <*>_N)_N\r\n >_N <*>_N)\r\n (Coh <c_a1ig[sk:2] xx_a1iA[tau:3]>_N\r\n (Sym ((TyFun\r\n <Proxy\r\n xx_a1iA[tau:3]>_N\r\n ((TyFun\r\n (Sym {co_a1jm})\r\n <*>_N)_N\r\n >_N <*>_N))_N\r\n >_N <*>_N)))\r\n <'Proxy>_N)_N)\r\n (Sym ((TyFun\r\n (Sym {co_a1jm})\r\n <*>_N)_N\r\n >_N <*>_N)))\r\n (Coh <yy_a1iB[tau:3]>_N\r\n {co_a1jm}))_N))_N\r\n >_N <*>_N))_N\r\n >_N <*>_N))\r\n 'Proxy :: (Proxy (yy_a1iB[tau:3] > {co_a1jm}) ~> s_a1jp[fmv:0]))\r\n ~# (s_a1jQ[fmv:0] :: (Proxy (yy_a1iB[tau:3] > {co_a1jm})\r\n ~> s_a1jp[fmv:0]))\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/typecheck/TcSMonad.hs:3047:25 in ghc:TcSMonad\r\n}}}\r\n\r\nOn GHC 8.4.2, it simply throws an error:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.2/bin/ghci Bug2.hs\r\nGHCi, version 8.4.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug2.hs, interpreted )\r\n\r\nBug2.hs:53:71: error:\r\n • Expected kind ‘Apply b xx’, but ‘y’ has kind ‘b @@ x’\r\n • In the first argument of ‘Proxy’, namely ‘y’\r\n In the first argument of ‘(~>)’, namely ‘Proxy y’\r\n In the second argument of ‘(~>)’, namely\r\n ‘Proxy y ~> c @@ ( 'Proxy :: Proxy x) @@ y’\r\n \r\n53  (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)\r\n  ^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >The following program panics on GHC HEAD:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilyDependencies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Proxy
data family Sing (a :: k)
data SomeSing :: Type > Type where
SomeSing :: Sing (a :: k) > SomeSing k
class SingKind k where
type Demote k = (r :: Type)  r > k
fromSing :: Sing (a :: k) > Demote k
toSing :: Demote k > SomeSing k
withSomeSing :: forall k r
. SingKind k
=> Demote k
> (forall (a :: k). Sing a > r)
> r
withSomeSing x f =
case toSing x of
SomeSing x' > f x'
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t > Sing (f @@ t) }
instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where
type Demote (k1 ~> k2) = Demote k1 > Demote k2
fromSing sFun x = withSomeSing x (fromSing . applySing sFun)
toSing = undefined
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type f @@ x = Apply f x
infixl 9 @@
dcomp :: forall (a :: Type)
(b :: a ~> Type)
(c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
(f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
(g :: forall (x :: a). Proxy x ~> b @@ x)
(x :: a).
SingKind (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))
=> (forall (xx :: a) (yy :: b @@ xx). Sing (f @@ ('Proxy :: Proxy xx) @@ ('Proxy :: Proxy yy)))
> Sing g
> Sing a
> Demote (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))
dcomp _sf _ _ = undefined
```
```
$ /opt/ghc/head/bin/ghc Bug2.hs
[1 of 1] Compiling Bug ( Bug2.hs, Bug2.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.5.20180501 for x86_64unknownlinux):
dischargeFmv
[D] _ {0}:: (Apply
(f_a1ih[sk:2] xx_a1iA[tau:3] yy_a1iB[tau:3] > Sym ((TyFun
<Proxy xx_a1iA[tau:3]>_N
((TyFun
(Proxy
(Sym {co_a1jm})
(Coh <yy_a1iB[tau:3]>_N
{co_a1jm}))_N
(Sym {co_a1jB} ; (Apply
(Sym {co_a1jm})
<*>_N
(Coh ((Coh <s_a1jn[fmv:0]>_N
((TyFun
(Sym {co_a1jm})
<*>_N)_N
>_N <*>_N) ; Sym {co_a1jA}) ; (Apply
<Proxy
xx_a1iA[tau:3]>_N
((TyFun
(Sym {co_a1jm})
<*>_N)_N
>_N <*>_N)
(Coh <c_a1ig[sk:2] xx_a1iA[tau:3]>_N
(Sym ((TyFun
<Proxy
xx_a1iA[tau:3]>_N
((TyFun
(Sym {co_a1jm})
<*>_N)_N
>_N <*>_N))_N
>_N <*>_N)))
<'Proxy>_N)_N)
(Sym ((TyFun
(Sym {co_a1jm})
<*>_N)_N
>_N <*>_N)))
(Coh <yy_a1iB[tau:3]>_N
{co_a1jm}))_N))_N
>_N <*>_N))_N
>_N <*>_N))
'Proxy :: (Proxy (yy_a1iB[tau:3] > {co_a1jm}) ~> s_a1jp[fmv:0]))
~# (s_a1jQ[fmv:0] :: (Proxy (yy_a1iB[tau:3] > {co_a1jm})
~> s_a1jp[fmv:0]))
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcSMonad.hs:3047:25 in ghc:TcSMonad
```
On GHC 8.4.2, it simply throws an error:
```
$ /opt/ghc/8.4.2/bin/ghci Bug2.hs
GHCi, version 8.4.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug2.hs, interpreted )
Bug2.hs:53:71: error:
• Expected kind ‘Apply b xx’, but ‘y’ has kind ‘b @@ x’
• In the first argument of ‘Proxy’, namely ‘y’
In the first argument of ‘(~>)’, namely ‘Proxy y’
In the second argument of ‘(~>)’, namely
‘Proxy y ~> c @@ ( 'Proxy :: Proxy x) @@ y’

53  (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
 ^
```
<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 panic (dischargeFmv)","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 panics on GHC HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilyDependencies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\ndata family Sing (a :: k)\r\ndata SomeSing :: Type > Type where\r\n SomeSing :: Sing (a :: k) > SomeSing k\r\n\r\nclass SingKind k where\r\n type Demote k = (r :: Type)  r > k\r\n fromSing :: Sing (a :: k) > Demote k\r\n toSing :: Demote k > SomeSing k\r\n\r\nwithSomeSing :: forall k r\r\n . SingKind k\r\n => Demote k\r\n > (forall (a :: k). Sing a > r)\r\n > r\r\nwithSomeSing x f =\r\n case toSing x of\r\n SomeSing x' > f x'\r\n\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t > Sing (f @@ t) }\r\n\r\ninstance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where\r\n type Demote (k1 ~> k2) = Demote k1 > Demote k2\r\n fromSing sFun x = withSomeSing x (fromSing . applySing sFun)\r\n toSing = undefined\r\n\r\ndata TyFun :: Type > Type > Type\r\ntype a ~> b = TyFun a b > Type\r\ninfixr 0 ~>\r\n\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\ntype f @@ x = Apply f x\r\ninfixl 9 @@\r\n\r\ndcomp :: forall (a :: Type)\r\n (b :: a ~> Type)\r\n (c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)\r\n (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)\r\n (g :: forall (x :: a). Proxy x ~> b @@ x)\r\n (x :: a).\r\n SingKind (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))\r\n => (forall (xx :: a) (yy :: b @@ xx). Sing (f @@ ('Proxy :: Proxy xx) @@ ('Proxy :: Proxy yy)))\r\n > Sing g\r\n > Sing a\r\n > Demote (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))\r\ndcomp _sf _ _ = undefined\r\n}}}\r\n{{{\r\n$ /opt/ghc/head/bin/ghc Bug2.hs\r\n[1 of 1] Compiling Bug ( Bug2.hs, Bug2.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.5.20180501 for x86_64unknownlinux):\r\n dischargeFmv\r\n [D] _ {0}:: (Apply\r\n (f_a1ih[sk:2] xx_a1iA[tau:3] yy_a1iB[tau:3] > Sym ((TyFun\r\n <Proxy xx_a1iA[tau:3]>_N\r\n ((TyFun\r\n (Proxy\r\n (Sym {co_a1jm})\r\n (Coh <yy_a1iB[tau:3]>_N\r\n {co_a1jm}))_N\r\n (Sym {co_a1jB} ; (Apply\r\n (Sym {co_a1jm})\r\n <*>_N\r\n (Coh ((Coh <s_a1jn[fmv:0]>_N\r\n ((TyFun\r\n (Sym {co_a1jm})\r\n <*>_N)_N\r\n >_N <*>_N) ; Sym {co_a1jA}) ; (Apply\r\n <Proxy\r\n xx_a1iA[tau:3]>_N\r\n ((TyFun\r\n (Sym {co_a1jm})\r\n <*>_N)_N\r\n >_N <*>_N)\r\n (Coh <c_a1ig[sk:2] xx_a1iA[tau:3]>_N\r\n (Sym ((TyFun\r\n <Proxy\r\n xx_a1iA[tau:3]>_N\r\n ((TyFun\r\n (Sym {co_a1jm})\r\n <*>_N)_N\r\n >_N <*>_N))_N\r\n >_N <*>_N)))\r\n <'Proxy>_N)_N)\r\n (Sym ((TyFun\r\n (Sym {co_a1jm})\r\n <*>_N)_N\r\n >_N <*>_N)))\r\n (Coh <yy_a1iB[tau:3]>_N\r\n {co_a1jm}))_N))_N\r\n >_N <*>_N))_N\r\n >_N <*>_N))\r\n 'Proxy :: (Proxy (yy_a1iB[tau:3] > {co_a1jm}) ~> s_a1jp[fmv:0]))\r\n ~# (s_a1jQ[fmv:0] :: (Proxy (yy_a1iB[tau:3] > {co_a1jm})\r\n ~> s_a1jp[fmv:0]))\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/typecheck/TcSMonad.hs:3047:25 in ghc:TcSMonad\r\n}}}\r\n\r\nOn GHC 8.4.2, it simply throws an error:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.2/bin/ghci Bug2.hs\r\nGHCi, version 8.4.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug2.hs, interpreted )\r\n\r\nBug2.hs:53:71: error:\r\n • Expected kind ‘Apply b xx’, but ‘y’ has kind ‘b @@ x’\r\n • In the first argument of ‘Proxy’, namely ‘y’\r\n In the first argument of ‘(~>)’, namely ‘Proxy y’\r\n In the second argument of ‘(~>)’, namely\r\n ‘Proxy y ~> c @@ ( 'Proxy :: Proxy x) @@ y’\r\n \r\n53  (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)\r\n  ^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15116GHC internal error when GADT return type mentions its own constructor name20190707T18:14:11ZRyan ScottGHC internal error when GADT return type mentions its own constructor nameTake the following program:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE TypeInType #}
module Bug where
data A (a :: k) where
MkA :: A MkA
```
On GHC 8.4.2, this is rejected with a sensible error message:
```
$ /opt/ghc/8.4.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:6:12: error:
• Data constructor ‘MkA’ cannot be used here
(it is defined and used in the same recursive group)
• In the first argument of ‘A’, namely ‘MkA’
In the type ‘A MkA’
In the definition of data constructor ‘MkA’

6  MkA :: A MkA
 ^^^
```
On GHC HEAD, however, this causes a GHC internal error:
```
$ ghc2/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:6:12: error:
• GHC internal error: ‘MkA’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [asv :> Type variable ‘k’ = k :: *,
asw :> Type variable ‘a’ = a :: k,
rqs :> ATcTyCon A :: forall k. k > *]
• In the first argument of ‘A’, namely ‘MkA’
In the type ‘A MkA’
In the definition of data constructor ‘MkA’

6  MkA :: A MkA
 ^^^
```
<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 internal error when GADT return type mentions its own constructor name","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["GADTs,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Take the following program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\ndata A (a :: k) where\r\n MkA :: A MkA\r\n}}}\r\n\r\nOn GHC 8.4.2, this is rejected with a sensible error message:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:6:12: error:\r\n • Data constructor ‘MkA’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the first argument of ‘A’, namely ‘MkA’\r\n In the type ‘A MkA’\r\n In the definition of data constructor ‘MkA’\r\n \r\n6  MkA :: A MkA\r\n  ^^^\r\n}}}\r\n\r\nOn GHC HEAD, however, this causes a GHC internal error:\r\n\r\n{{{\r\n$ ghc2/inplace/bin/ghcstage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:6:12: error:\r\n • GHC internal error: ‘MkA’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [asv :> Type variable ‘k’ = k :: *,\r\n asw :> Type variable ‘a’ = a :: k,\r\n rqs :> ATcTyCon A :: forall k. k > *]\r\n • In the first argument of ‘A’, namely ‘MkA’\r\n In the type ‘A MkA’\r\n In the definition of data constructor ‘MkA’\r\n \r\n6  MkA :: A MkA\r\n  ^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >Take the following program:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE TypeInType #}
module Bug where
data A (a :: k) where
MkA :: A MkA
```
On GHC 8.4.2, this is rejected with a sensible error message:
```
$ /opt/ghc/8.4.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:6:12: error:
• Data constructor ‘MkA’ cannot be used here
(it is defined and used in the same recursive group)
• In the first argument of ‘A’, namely ‘MkA’
In the type ‘A MkA’
In the definition of data constructor ‘MkA’

6  MkA :: A MkA
 ^^^
```
On GHC HEAD, however, this causes a GHC internal error:
```
$ ghc2/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:6:12: error:
• GHC internal error: ‘MkA’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [asv :> Type variable ‘k’ = k :: *,
asw :> Type variable ‘a’ = a :: k,
rqs :> ATcTyCon A :: forall k. k > *]
• In the first argument of ‘A’, namely ‘MkA’
In the type ‘A MkA’
In the definition of data constructor ‘MkA’

6  MkA :: A MkA
 ^^^
```
<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 internal error when GADT return type mentions its own constructor name","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["GADTs,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Take the following program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\ndata A (a :: k) where\r\n MkA :: A MkA\r\n}}}\r\n\r\nOn GHC 8.4.2, this is rejected with a sensible error message:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:6:12: error:\r\n • Data constructor ‘MkA’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the first argument of ‘A’, namely ‘MkA’\r\n In the type ‘A MkA’\r\n In the definition of data constructor ‘MkA’\r\n \r\n6  MkA :: A MkA\r\n  ^^^\r\n}}}\r\n\r\nOn GHC HEAD, however, this causes a GHC internal error:\r\n\r\n{{{\r\n$ ghc2/inplace/bin/ghcstage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:6:12: error:\r\n • GHC internal error: ‘MkA’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [asv :> Type variable ‘k’ = k :: *,\r\n asw :> Type variable ‘a’ = a :: k,\r\n rqs :> ATcTyCon A :: forall k. k > *]\r\n • In the first argument of ‘A’, namely ‘MkA’\r\n In the type ‘A MkA’\r\n In the definition of data constructor ‘MkA’\r\n \r\n6  MkA :: A MkA\r\n  ^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15079GHC HEAD regression: cannot instantiate higherrank kind20201031T11:08:22ZRyan ScottGHC HEAD regression: cannot instantiate higherrank kindThe following program typechecks on GHC 8.2.2 and 8.4.2:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Void
infixl 4 :==
  Heterogeneous Leibnizian equality.
newtype (a :: j) :== (b :: k)
= HRefl { hsubst :: forall (c :: forall (i :: Type). i > Type). c a > c b }
newtype Coerce a = Coerce { uncoerce :: Starify a }
type family Starify (a :: k) :: Type where
Starify (a :: Type) = a
Starify _ = Void
coerce :: a :== b > a > b
coerce f = uncoerce . hsubst f . Coerce
```
But GHC HEAD rejects it:
```
$ ~/Software/ghc/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:21:34: error:
• Kind mismatch: cannot unify (c0 :: forall i. i > *) with:
Coerce :: forall k. k > *
Their kinds differ.
Expected type: a > c0 * a
Actual type: Starify a > Coerce a
• In the second argument of ‘(.)’, namely ‘Coerce’
In the second argument of ‘(.)’, namely ‘hsubst f . Coerce’
In the expression: uncoerce . hsubst f . Coerce

21  coerce f = uncoerce . hsubst f . Coerce
 ^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC HEAD regression: cannot instantiate higherrank kind","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.2.2 and 8.4.2:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Void\r\n\r\ninfixl 4 :==\r\n  Heterogeneous Leibnizian equality.\r\nnewtype (a :: j) :== (b :: k)\r\n = HRefl { hsubst :: forall (c :: forall (i :: Type). i > Type). c a > c b }\r\n\r\nnewtype Coerce a = Coerce { uncoerce :: Starify a }\r\ntype family Starify (a :: k) :: Type where\r\n Starify (a :: Type) = a\r\n Starify _ = Void\r\n\r\ncoerce :: a :== b > a > b\r\ncoerce f = uncoerce . hsubst f . Coerce\r\n}}}\r\n\r\nBut GHC HEAD rejects it:\r\n\r\n{{{\r\n$ ~/Software/ghc/inplace/bin/ghcstage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:21:34: error:\r\n • Kind mismatch: cannot unify (c0 :: forall i. i > *) with:\r\n Coerce :: forall k. k > *\r\n Their kinds differ.\r\n Expected type: a > c0 * a\r\n Actual type: Starify a > Coerce a\r\n • In the second argument of ‘(.)’, namely ‘Coerce’\r\n In the second argument of ‘(.)’, namely ‘hsubst f . Coerce’\r\n In the expression: uncoerce . hsubst f . Coerce\r\n \r\n21  coerce f = uncoerce . hsubst f . Coerce\r\n  ^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >The following program typechecks on GHC 8.2.2 and 8.4.2:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Void
infixl 4 :==
  Heterogeneous Leibnizian equality.
newtype (a :: j) :== (b :: k)
= HRefl { hsubst :: forall (c :: forall (i :: Type). i > Type). c a > c b }
newtype Coerce a = Coerce { uncoerce :: Starify a }
type family Starify (a :: k) :: Type where
Starify (a :: Type) = a
Starify _ = Void
coerce :: a :== b > a > b
coerce f = uncoerce . hsubst f . Coerce
```
But GHC HEAD rejects it:
```
$ ~/Software/ghc/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:21:34: error:
• Kind mismatch: cannot unify (c0 :: forall i. i > *) with:
Coerce :: forall k. k > *
Their kinds differ.
Expected type: a > c0 * a
Actual type: Starify a > Coerce a
• In the second argument of ‘(.)’, namely ‘Coerce’
In the second argument of ‘(.)’, namely ‘hsubst f . Coerce’
In the expression: uncoerce . hsubst f . Coerce

21  coerce f = uncoerce . hsubst f . Coerce
 ^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC HEAD regression: cannot instantiate higherrank kind","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.2.2 and 8.4.2:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Void\r\n\r\ninfixl 4 :==\r\n  Heterogeneous Leibnizian equality.\r\nnewtype (a :: j) :== (b :: k)\r\n = HRefl { hsubst :: forall (c :: forall (i :: Type). i > Type). c a > c b }\r\n\r\nnewtype Coerce a = Coerce { uncoerce :: Starify a }\r\ntype family Starify (a :: k) :: Type where\r\n Starify (a :: Type) = a\r\n Starify _ = Void\r\n\r\ncoerce :: a :== b > a > b\r\ncoerce f = uncoerce . hsubst f . Coerce\r\n}}}\r\n\r\nBut GHC HEAD rejects it:\r\n\r\n{{{\r\n$ ~/Software/ghc/inplace/bin/ghcstage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:21:34: error:\r\n • Kind mismatch: cannot unify (c0 :: forall i. i > *) with:\r\n Coerce :: forall k. k > *\r\n Their kinds differ.\r\n Expected type: a > c0 * a\r\n Actual type: Starify a > Coerce a\r\n • In the second argument of ‘(.)’, namely ‘Coerce’\r\n In the second argument of ‘(.)’, namely ‘hsubst f . Coerce’\r\n In the expression: uncoerce . hsubst f . Coerce\r\n \r\n21  coerce f = uncoerce . hsubst f . Coerce\r\n  ^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15076Typed hole with higherrank kind causes GHC to panic (No skolem info)20190707T18:14:23ZRyan ScottTyped hole with higherrank kind causes GHC to panic (No skolem info)Spun out from #14040\#[ticket:15076\#comment:152359](https://gitlab.haskell.org//ghc/ghc/issues/15076#note_152359), which was different enough from the original program in #14040 to warrant its own ticket. The following program panics on every version of GHC from 8.0.2 onward:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
import Data.Proxy
foo :: forall (a :: Type)
(f :: forall (x :: a). Proxy x > Type).
Proxy f > ()
foo (_ :: _) = ()
```
```
$ ~/Software/ghc/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:11: error:ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.5.20180420 for x86_64unknownlinux):
No skolem info:
[a_aZo[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:3224:5 in ghc:TcErrors
```Spun out from #14040\#[ticket:15076\#comment:152359](https://gitlab.haskell.org//ghc/ghc/issues/15076#note_152359), which was different enough from the original program in #14040 to warrant its own ticket. The following program panics on every version of GHC from 8.0.2 onward:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
import Data.Proxy
foo :: forall (a :: Type)
(f :: forall (x :: a). Proxy x > Type).
Proxy f > ()
foo (_ :: _) = ()
```
```
$ ~/Software/ghc/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:11: error:ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.5.20180420 for x86_64unknownlinux):
No skolem info:
[a_aZo[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:3224:5 in ghc:TcErrors
```8.8.1https://gitlab.haskell.org/ghc/ghc//issues/15039Bizarre prettyprinting of inferred Coercible constraint in partial type sign...20190707T18:14:36ZRyan ScottBizarre prettyprinting of inferred Coercible constraint in partial type signatureConsider the following GHCi session:
```
$ ghci
GHCi, version 8.4.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> import Data.Type.Coercion
λ> foo :: _ => Coercion a b; foo = Coercion
<interactive>:2:8: error:
• Found type wildcard ‘_’
standing for ‘Coercible a b :: TYPE ('GHC.Types.TupleRep '[])’
Where: ‘a’, ‘b’ are rigid type variables bound by
the inferred type of foo :: Coercible a b => Coercion a b
at <interactive>:2:2740
To use the inferred type, enable PartialTypeSignatures
• In the type signature: foo :: _ => Coercion a b
λ> :set fprintexplicitkinds
λ> foo :: _ => Coercion a b; foo = Coercion
<interactive>:4:8: error:
• Found type wildcard ‘_’
standing for ‘(a :: *) ~~ (b :: *) :: TYPE
('GHC.Types.TupleRep ('[] GHC.Types.RuntimeRep))’
Where: ‘a’, ‘b’ are rigid type variables bound by
the inferred type of
foo :: ((a :: *) ~~ (b :: *)) => Coercion * a b
at <interactive>:4:2740
To use the inferred type, enable PartialTypeSignatures
• In the type signature: foo :: _ => Coercion a b
```
There are two things quite strange about this:
1. In both error messages, GHC claims that `Coercible a b`/`a ~~ b` has kind `TYPE (TupleRep '[])`. This is wrong, and should be `Coercible`.
1. For some reason, enabling `fprintexplicitkinds` causes the inferred constraint to be `(~~)` instead of `Coercible`, which is just plain wrong.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1 
 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":"Bizarre prettyprinting of inferred Coercible constraint in partial type signature","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1","keywords":["PartialTypeSignatures"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following GHCi session:\r\n\r\n{{{\r\n$ ghci\r\nGHCi, version 8.4.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\nλ> import Data.Type.Coercion\r\nλ> foo :: _ => Coercion a b; foo = Coercion\r\n\r\n<interactive>:2:8: error:\r\n • Found type wildcard ‘_’\r\n standing for ‘Coercible a b :: TYPE ('GHC.Types.TupleRep '[])’\r\n Where: ‘a’, ‘b’ are rigid type variables bound by\r\n the inferred type of foo :: Coercible a b => Coercion a b\r\n at <interactive>:2:2740\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature: foo :: _ => Coercion a b\r\nλ> :set fprintexplicitkinds \r\nλ> foo :: _ => Coercion a b; foo = Coercion\r\n\r\n<interactive>:4:8: error:\r\n • Found type wildcard ‘_’\r\n standing for ‘(a :: *) ~~ (b :: *) :: TYPE\r\n ('GHC.Types.TupleRep ('[] GHC.Types.RuntimeRep))’\r\n Where: ‘a’, ‘b’ are rigid type variables bound by\r\n the inferred type of\r\n foo :: ((a :: *) ~~ (b :: *)) => Coercion * a b\r\n at <interactive>:4:2740\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature: foo :: _ => Coercion a b\r\n}}}\r\n\r\nThere are two things quite strange about this:\r\n\r\n1. In both error messages, GHC claims that `Coercible a b`/`a ~~ b` has kind `TYPE (TupleRep '[])`. This is wrong, and should be `Coercible`.\r\n2. For some reason, enabling `fprintexplicitkinds` causes the inferred constraint to be `(~~)` instead of `Coercible`, which is just plain wrong.","type_of_failure":"OtherFailure","blocking":[]} >Consider the following GHCi session:
```
$ ghci
GHCi, version 8.4.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> import Data.Type.Coercion
λ> foo :: _ => Coercion a b; foo = Coercion
<interactive>:2:8: error:
• Found type wildcard ‘_’
standing for ‘Coercible a b :: TYPE ('GHC.Types.TupleRep '[])’
Where: ‘a’, ‘b’ are rigid type variables bound by
the inferred type of foo :: Coercible a b => Coercion a b
at <interactive>:2:2740
To use the inferred type, enable PartialTypeSignatures
• In the type signature: foo :: _ => Coercion a b
λ> :set fprintexplicitkinds
λ> foo :: _ => Coercion a b; foo = Coercion
<interactive>:4:8: error:
• Found type wildcard ‘_’
standing for ‘(a :: *) ~~ (b :: *) :: TYPE
('GHC.Types.TupleRep ('[] GHC.Types.RuntimeRep))’
Where: ‘a’, ‘b’ are rigid type variables bound by
the inferred type of
foo :: ((a :: *) ~~ (b :: *)) => Coercion * a b
at <interactive>:4:2740
To use the inferred type, enable PartialTypeSignatures
• In the type signature: foo :: _ => Coercion a b
```
There are two things quite strange about this:
1. In both error messages, GHC claims that `Coercible a b`/`a ~~ b` has kind `TYPE (TupleRep '[])`. This is wrong, and should be `Coercible`.
1. For some reason, enabling `fprintexplicitkinds` causes the inferred constraint to be `(~~)` instead of `Coercible`, which is just plain wrong.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1 
 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":"Bizarre prettyprinting of inferred Coercible constraint in partial type signature","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1","keywords":["PartialTypeSignatures"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following GHCi session:\r\n\r\n{{{\r\n$ ghci\r\nGHCi, version 8.4.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\nλ> import Data.Type.Coercion\r\nλ> foo :: _ => Coercion a b; foo = Coercion\r\n\r\n<interactive>:2:8: error:\r\n • Found type wildcard ‘_’\r\n standing for ‘Coercible a b :: TYPE ('GHC.Types.TupleRep '[])’\r\n Where: ‘a’, ‘b’ are rigid type variables bound by\r\n the inferred type of foo :: Coercible a b => Coercion a b\r\n at <interactive>:2:2740\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature: foo :: _ => Coercion a b\r\nλ> :set fprintexplicitkinds \r\nλ> foo :: _ => Coercion a b; foo = Coercion\r\n\r\n<interactive>:4:8: error:\r\n • Found type wildcard ‘_’\r\n standing for ‘(a :: *) ~~ (b :: *) :: TYPE\r\n ('GHC.Types.TupleRep ('[] GHC.Types.RuntimeRep))’\r\n Where: ‘a’, ‘b’ are rigid type variables bound by\r\n the inferred type of\r\n foo :: ((a :: *) ~~ (b :: *)) => Coercion * a b\r\n at <interactive>:4:2740\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature: foo :: _ => Coercion a b\r\n}}}\r\n\r\nThere are two things quite strange about this:\r\n\r\n1. In both error messages, GHC claims that `Coercible a b`/`a ~~ b` has kind `TYPE (TupleRep '[])`. This is wrong, and should be `Coercible`.\r\n2. For some reason, enabling `fprintexplicitkinds` causes the inferred constraint to be `(~~)` instead of `Coercible`, which is just plain wrong.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://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/14938Pattern matching on GADT does not refine type family parameters20190707T18:14:57ZCsongor KissPattern matching on GADT does not refine type family parametersCompiling the following code
```hs
type family R (x :: k) (y :: k) (prf :: x :~: y) :: x :~: y where
R x y Refl = Refl
```
fails with the error
```txt
Temp.hs:49:9: error:
• Expected kind ‘x :~: y’, but ‘Refl’ has kind ‘x :~: x’
• In the third argument of ‘R’, namely ‘Refl’
In the type family declaration for ‘R’

49  R x y Refl = Refl
 ^^^^
```
where `Refl` is defined as
```hs
data a :~: b where
Refl :: a :~: a
```
I would expect patternmatching on `Refl` to bring the equality `x ~ y` into scope. It seems like it not only doesn't do that, but the pattern match itself is rejected.
(both 8.2.2 and HEAD)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 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":"Pattern matching on GADT does not refine type family parameters","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["GADTs,","TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Compiling the following code\r\n\r\n{{{#!hs\r\ntype family R (x :: k) (y :: k) (prf :: x :~: y) :: x :~: y where\r\n R x y Refl = Refl\r\n}}}\r\n\r\nfails with the error\r\n\r\n\r\n{{{#!txt\r\nTemp.hs:49:9: error:\r\n • Expected kind ‘x :~: y’, but ‘Refl’ has kind ‘x :~: x’\r\n • In the third argument of ‘R’, namely ‘Refl’\r\n In the type family declaration for ‘R’\r\n \r\n49  R x y Refl = Refl\r\n  ^^^^\r\n}}}\r\n\r\nwhere `Refl` is defined as\r\n{{{#!hs\r\ndata a :~: b where\r\n Refl :: a :~: a\r\n}}}\r\n\r\nI would expect patternmatching on `Refl` to bring the equality `x ~ y` into scope. It seems like it not only doesn't do that, but the pattern match itself is rejected.\r\n\r\n(both 8.2.2 and HEAD)\r\n","type_of_failure":"OtherFailure","blocking":[]} >Compiling the following code
```hs
type family R (x :: k) (y :: k) (prf :: x :~: y) :: x :~: y where
R x y Refl = Refl
```
fails with the error
```txt
Temp.hs:49:9: error:
• Expected kind ‘x :~: y’, but ‘Refl’ has kind ‘x :~: x’
• In the third argument of ‘R’, namely ‘Refl’
In the type family declaration for ‘R’

49  R x y Refl = Refl
 ^^^^
```
where `Refl` is defined as
```hs
data a :~: b where
Refl :: a :~: a
```
I would expect patternmatching on `Refl` to bring the equality `x ~ y` into scope. It seems like it not only doesn't do that, but the pattern match itself is rejected.
(both 8.2.2 and HEAD)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 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":"Pattern matching on GADT does not refine type family parameters","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["GADTs,","TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Compiling the following code\r\n\r\n{{{#!hs\r\ntype family R (x :: k) (y :: k) (prf :: x :~: y) :: x :~: y where\r\n R x y Refl = Refl\r\n}}}\r\n\r\nfails with the error\r\n\r\n\r\n{{{#!txt\r\nTemp.hs:49:9: error:\r\n • Expected kind ‘x :~: y’, but ‘Refl’ has kind ‘x :~: x’\r\n • In the third argument of ‘R’, namely ‘Refl’\r\n In the type family declaration for ‘R’\r\n \r\n49  R x y Refl = Refl\r\n  ^^^^\r\n}}}\r\n\r\nwhere `Refl` is defined as\r\n{{{#!hs\r\ndata a :~: b where\r\n Refl :: a :~: a\r\n}}}\r\n\r\nI would expect patternmatching on `Refl` to bring the equality `x ~ y` into scope. It seems like it not only doesn't do that, but the pattern match itself is rejected.\r\n\r\n(both 8.2.2 and HEAD)\r\n","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14904Compiler panic (piResultTy)20190707T18:15:06ZCsongor KissCompiler panic (piResultTy)Typechecking the following type family
```hs
type family F (f :: forall a. g a) :: Type where
F (f :: forall a. g a) = Int
```
panics with the message:
```txt
ghc: panic! (the 'impossible' happened)
(GHC version 8.4.0.20180118 for x86_64appledarwin):
piResultTy
k_aVM[tau:1]
a_aVF[sk:1]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:950:35 in ghc:Type
```
The panic happens with HEAD, 8.4 and 8.2. 8.0 rejects the program with an error message, but even it panics on the following version:
```hs
type family F f :: Type where
F ((f :: forall a. g a) :: forall a. g a) = Int
```
#14873 seemed somewhat related, so I tried with the patch implemented in 3d252037234ce48f9bdada7d5c9b1d8eba470829, but that fails with the same panic too.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  #14873 
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Compiler panic (piResultTy)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[14873],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Typechecking the following type family\r\n\r\n{{{#!hs\r\ntype family F (f :: forall a. g a) :: Type where\r\n F (f :: forall a. g a) = Int\r\n}}}\r\n\r\npanics with the message:\r\n\r\n{{{#!txt\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.4.0.20180118 for x86_64appledarwin):\r\n piResultTy\r\n k_aVM[tau:1]\r\n a_aVF[sk:1]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:950:35 in ghc:Type\r\n\r\n}}}\r\n\r\nThe panic happens with HEAD, 8.4 and 8.2. 8.0 rejects the program with an error message, but even it panics on the following version:\r\n\r\n{{{#!hs\r\ntype family F f :: Type where\r\n F ((f :: forall a. g a) :: forall a. g a) = Int\r\n}}}\r\n\r\n#14873 seemed somewhat related, so I tried with the patch implemented in 3d252037234ce48f9bdada7d5c9b1d8eba470829, but that fails with the same panic too.","type_of_failure":"OtherFailure","blocking":[]} >Typechecking the following type family
```hs
type family F (f :: forall a. g a) :: Type where
F (f :: forall a. g a) = Int
```
panics with the message:
```txt
ghc: panic! (the 'impossible' happened)
(GHC version 8.4.0.20180118 for x86_64appledarwin):
piResultTy
k_aVM[tau:1]
a_aVF[sk:1]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:950:35 in ghc:Type
```
The panic happens with HEAD, 8.4 and 8.2. 8.0 rejects the program with an error message, but even it panics on the following version:
```hs
type family F f :: Type where
F ((f :: forall a. g a) :: forall a. g a) = Int
```
#14873 seemed somewhat related, so I tried with the patch implemented in 3d252037234ce48f9bdada7d5c9b1d8eba470829, but that fails with the same panic too.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  #14873 
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Compiler panic (piResultTy)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[14873],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Typechecking the following type family\r\n\r\n{{{#!hs\r\ntype family F (f :: forall a. g a) :: Type where\r\n F (f :: forall a. g a) = Int\r\n}}}\r\n\r\npanics with the message:\r\n\r\n{{{#!txt\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.4.0.20180118 for x86_64appledarwin):\r\n piResultTy\r\n k_aVM[tau:1]\r\n a_aVF[sk:1]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:950:35 in ghc:Type\r\n\r\n}}}\r\n\r\nThe panic happens with HEAD, 8.4 and 8.2. 8.0 rejects the program with an error message, but even it panics on the following version:\r\n\r\n{{{#!hs\r\ntype family F f :: Type where\r\n F ((f :: forall a. g a) :: forall a. g a) = Int\r\n}}}\r\n\r\n#14873 seemed somewhat related, so I tried with the patch implemented in 3d252037234ce48f9bdada7d5c9b1d8eba470829, but that fails with the same panic too.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/14887Explicitly quantifying a kind variable causes a telescope to fail to kindcheck20190707T18:15:11ZRyan ScottExplicitly quantifying a kind variable causes a telescope to fail to kindcheckConsider the following program:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
{# OPTIONS_GHC fprintexplicitkinds #}
module Bug where
import Data.Kind
import Data.Type.Equality
type family Foo1 (e :: (a :: k) :~: (a :: k)) :: Type where
Foo1 (e :: a :~: a) = a :~: a
type family Foo2 (k :: Type) (e :: (a :: k) :~: (a :: k)) :: Type where
Foo2 k (e :: a :~: a) = a :~: a
```
`Foo2` is wholly equivalent to `Foo1`, except that in `Foo2`, the `k` kind variable is explicitly quantified. However, `Foo1` typechecks, but `Foo2` does not!
```
$ /opt/ghc/8.2.2/bin/ghci Bug.hs fprintexplicitkinds
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:13:10: error:
• Couldn't match kind ‘k’ with ‘k1’
When matching the kind of ‘a’
Expected kind ‘(:~:) k a a’, but ‘e’ has kind ‘(:~:) k a a’
• In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’
In the type family declaration for ‘Foo2’

13  Foo2 k (e :: a :~: a) = a :~: a
 ^^^^^^^^^^^^^^
```
(Moreover, there seems to be a tidying bug, since GHC claims that `(:~:) k a a` is not the same kind as `(:~:) k a a`.)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 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":"Explicitly quantifying a kind variable causes a type family to fail to typecheck","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["TypeFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n{# OPTIONS_GHC fprintexplicitkinds #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ntype family Foo1 (e :: (a :: k) :~: (a :: k)) :: Type where\r\n Foo1 (e :: a :~: a) = a :~: a\r\n\r\ntype family Foo2 (k :: Type) (e :: (a :: k) :~: (a :: k)) :: Type where\r\n Foo2 k (e :: a :~: a) = a :~: a\r\n}}}\r\n\r\n`Foo2` is wholly equivalent to `Foo1`, except that in `Foo2`, the `k` kind variable is explicitly quantified. However, `Foo1` typechecks, but `Foo2` does not!\r\n\r\n{{{\r\n$ /opt/ghc/8.2.2/bin/ghci Bug.hs fprintexplicitkinds\r\nGHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/ryanglscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:13:10: error:\r\n • Couldn't match kind ‘k’ with ‘k1’\r\n When matching the kind of ‘a’\r\n Expected kind ‘(:~:) k a a’, but ‘e’ has kind ‘(:~:) k a a’\r\n • In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’\r\n In the type family declaration for ‘Foo2’\r\n \r\n13  Foo2 k (e :: a :~: a) = a :~: a\r\n  ^^^^^^^^^^^^^^\r\n}}}\r\n\r\n(Moreover, there seems to be a tidying bug, since GHC claims that `(:~:) k a a` is not the same kind as `(:~:) k a a`.)","type_of_failure":"OtherFailure","blocking":[]} >Consider the following program:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
{# OPTIONS_GHC fprintexplicitkinds #}
module Bug where
import Data.Kind
import Data.Type.Equality
type family Foo1 (e :: (a :: k) :~: (a :: k)) :: Type where
Foo1 (e :: a :~: a) = a :~: a
type family Foo2 (k :: Type) (e :: (a :: k) :~: (a :: k)) :: Type where
Foo2 k (e :: a :~: a) = a :~: a
```
`Foo2` is wholly equivalent to `Foo1`, except that in `Foo2`, the `k` kind variable is explicitly quantified. However, `Foo1` typechecks, but `Foo2` does not!
```
$ /opt/ghc/8.2.2/bin/ghci Bug.hs fprintexplicitkinds
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:13:10: error:
• Couldn't match kind ‘k’ with ‘k1’
When matching the kind of ‘a’
Expected kind ‘(:~:) k a a’, but ‘e’ has kind ‘(:~:) k a a’
• In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’
In the type family declaration for ‘Foo2’

13  Foo2 k (e :: a :~: a) = a :~: a
 ^^^^^^^^^^^^^^
```
(Moreover, there seems to be a tidying bug, since GHC claims that `(:~:) k a a` is not the same kind as `(:~:) k a a`.)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 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":"Explicitly quantifying a kind variable causes a type family to fail to typecheck","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["TypeFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n{# OPTIONS_GHC fprintexplicitkinds #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ntype family Foo1 (e :: (a :: k) :~: (a :: k)) :: Type where\r\n Foo1 (e :: a :~: a) = a :~: a\r\n\r\ntype family Foo2 (k :: Type) (e :: (a :: k) :~: (a :: k)) :: Type where\r\n Foo2 k (e :: a :~: a) = a :~: a\r\n}}}\r\n\r\n`Foo2` is wholly equivalent to `Foo1`, except that in `Foo2`, the `k` kind variable is explicitly quantified. However, `Foo1` typechecks, but `Foo2` does not!\r\n\r\n{{{\r\n$ /opt/ghc/8.2.2/bin/ghci Bug.hs fprintexplicitkinds\r\nGHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/ryanglscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:13:10: error:\r\n • Couldn't match kind ‘k’ with ‘k1’\r\n When matching the kind of ‘a’\r\n Expected kind ‘(:~:) k a a’, but ‘e’ has kind ‘(:~:) k a a’\r\n • In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’\r\n In the type family declaration for ‘Foo2’\r\n \r\n13  Foo2 k (e :: a :~: a) = a :~: a\r\n  ^^^^^^^^^^^^^^\r\n}}}\r\n\r\n(Moreover, there seems to be a tidying bug, since GHC claims that `(:~:) k a a` is not the same kind as `(:~:) k a a`.)","type_of_failure":"OtherFailure","blocking":[]} >8.8.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/14880GHC panic: updateRole20190707T18:15:13ZRyan ScottGHC panic: updateRoleThe following program panics on GHC 8.0.2, 8.2.2, 8.4.1, and HEAD:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Type.Equality ((:~:))
type SameKind (a :: k) (b :: k) = (() :: Constraint)
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data WhyCongSym1 (x :: Type) :: forall (a :: x)
(y :: Type)
(z :: x).
Type ~> (x ~> y) ~> x ~> x ~> (a :~: z) ~> Type
data WhyCongSym0 :: forall (x :: Type)
(a :: x)
(y :: Type)
(z :: x).
Type ~> Type ~> (x ~> y) ~> x ~> x ~> (a :~: z) ~> Type
where
WhyCongSym0KindInference :: forall x arg.
SameKind (Apply WhyCongSym0 arg) (WhyCongSym1 arg) =>
WhyCongSym0 x
```
```
$ /opt/ghc/8.2.2/bin/ghci Bug.hs
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.2 for x86_64unknownlinux):
updateRole
WhyCongSym0
arg_a1A6[sk:1]
[a1A5 :> 4, a2Cy :> 0, a2Cz :> 1, a2CA :> 2, a2CB :> 3]
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcTyDecls.hs:656:23 in ghc:TcTyDecls
```The following program panics on GHC 8.0.2, 8.2.2, 8.4.1, and HEAD:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Type.Equality ((:~:))
type SameKind (a :: k) (b :: k) = (() :: Constraint)
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data WhyCongSym1 (x :: Type) :: forall (a :: x)
(y :: Type)
(z :: x).
Type ~> (x ~> y) ~> x ~> x ~> (a :~: z) ~> Type
data WhyCongSym0 :: forall (x :: Type)
(a :: x)
(y :: Type)
(z :: x).
Type ~> Type ~> (x ~> y) ~> x ~> x ~> (a :~: z) ~> Type
where
WhyCongSym0KindInference :: forall x arg.
SameKind (Apply WhyCongSym0 arg) (WhyCongSym1 arg) =>
WhyCongSym0 x
```
```
$ /opt/ghc/8.2.2/bin/ghci Bug.hs
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.2 for x86_64unknownlinux):
updateRole
WhyCongSym0
arg_a1A6[sk:1]
[a1A5 :> 4, a2Cy :> 0, a2Cz :> 1, a2CA :> 2, a2CB :> 3]
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcTyDecls.hs:656:23 in ghc:TcTyDecls
```8.6.2Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/14847Inferring dependent kinds for nonrecursive types20190707T18:15:20ZSimon Peyton JonesInferring dependent kinds for nonrecursive typesConsider this
```
data Proxy k (a :: k) = MkProxy
data Proxy2 k a = MkP (Proxy k a)
```
which is discussed in [a corner of the user manual](http://downloads.haskell.org/~ghc/master/usersguide/glasgow_exts.html#inferringdependencyindatatypedeclarations).
Surprisingly, we reject `Proxy2`  but there is nothing difficult about inferring its kind. There would be if it was recursive  but it isn't.
Simple solution: for nonrecursive type declarations (we do SCC analysis so we know which these are) do not call `getInitialKinds`; instead, just infer the kind of the definition! Simple.
Warning: is this recursive?
```
data Proxy2 k a where
MkP :: Proxy k a > Proxy2 k a
```
Presumably no more than the other definition. But currently we need `Proxy2` in the environment during kind inference, because we kindcheck the result type. That seems jolly odd and inconsistent. Needs more thought.
Similar questions for
```
data T a where
T :: Int > T Bool
type family F a where
F Int = True
F _ = False
```
See also:
 #14451
 #12088
 #9427Consider this
```
data Proxy k (a :: k) = MkProxy
data Proxy2 k a = MkP (Proxy k a)
```
which is discussed in [a corner of the user manual](http://downloads.haskell.org/~ghc/master/usersguide/glasgow_exts.html#inferringdependencyindatatypedeclarations).
Surprisingly, we reject `Proxy2`  but there is nothing difficult about inferring its kind. There would be if it was recursive  but it isn't.
Simple solution: for nonrecursive type declarations (we do SCC analysis so we know which these are) do not call `getInitialKinds`; instead, just infer the kind of the definition! Simple.
Warning: is this recursive?
```
data Proxy2 k a where
MkP :: Proxy k a > Proxy2 k a
```
Presumably no more than the other definition. But currently we need `Proxy2` in the environment during kind inference, because we kindcheck the result type. That seems jolly odd and inconsistent. Needs more thought.
Similar questions for
```
data T a where
T :: Int > T Bool
type family F a where
F Int = True
F _ = False
```
See also:
 #14451
 #12088
 #9427