GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20190707T18:14:10Zhttps://gitlab.haskell.org/ghc/ghc//issues/15122GHC HEAD typechecker regression20190707T18:14:10ZfmixingGHC HEAD typechecker regressionThis code, distilled from the `typelevelsets` library:
```hs
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE GADTs #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
data Proxy (p :: k) = Proxy
data Set (n :: [k]) where
Empty :: Set '[]
Ext :: e > Set s > Set (e ': s)
type family (m :: [k]) :\ (x :: k) :: [k] where
'[] :\ x = '[]
(x ': xs) :\ x = xs
(y ': xs) :\ x = y ': (xs :\ x)
class Remove s t where
remove :: Set s > Proxy t > Set (s :\ t)
instance Remove '[] t where
remove Empty Proxy = Empty
instance {# OVERLAPS #} Remove (x ': xs) x where
remove (Ext _ xs) Proxy = xs
instance {# OVERLAPPABLE #} (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
=> Remove (y ': xs) x where
remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
```
Typechecks in GHC 8.4.2, but not in GHC HEAD:
```
$ /opt/ghc/head/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:31:33: error:
• Could not deduce: ((e : s) :\ x) ~ (e : (s :\ x))
from the context: (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
bound by the instance declaration at Bug.hs:(29,31)(30,27)
or from: (k ~ *, (y : xs :: [k]) ~~ (e : s :: [*]))
bound by a pattern with constructor:
Ext :: forall e (s :: [*]). e > Set s > Set (e : s),
in an equation for ‘remove’
at Bug.hs:31:1118
Expected type: Set ((y : xs) :\ x)
Actual type: Set (e : (s :\ x))
• In the expression: Ext y (remove xs x)
In an equation for ‘remove’:
remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
In the instance declaration for ‘Remove (y : xs) x’
• Relevant bindings include
x :: Proxy x (bound at Bug.hs:31:22)
xs :: Set s (bound at Bug.hs:31:17)
y :: e (bound at Bug.hs:31:15)
remove :: Set (y : xs) > Proxy x > Set ((y : xs) :\ x)
(bound at Bug.hs:31:3)

31  remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
 ^^^^^^^^^^^^^^^^^^^
```
This regression was introduced in commit e3dbb44f53b2f9403d20d84e27f187062755a089 (Fix #12919 by making the flattener homegeneous.).This code, distilled from the `typelevelsets` library:
```hs
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE GADTs #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
data Proxy (p :: k) = Proxy
data Set (n :: [k]) where
Empty :: Set '[]
Ext :: e > Set s > Set (e ': s)
type family (m :: [k]) :\ (x :: k) :: [k] where
'[] :\ x = '[]
(x ': xs) :\ x = xs
(y ': xs) :\ x = y ': (xs :\ x)
class Remove s t where
remove :: Set s > Proxy t > Set (s :\ t)
instance Remove '[] t where
remove Empty Proxy = Empty
instance {# OVERLAPS #} Remove (x ': xs) x where
remove (Ext _ xs) Proxy = xs
instance {# OVERLAPPABLE #} (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
=> Remove (y ': xs) x where
remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
```
Typechecks in GHC 8.4.2, but not in GHC HEAD:
```
$ /opt/ghc/head/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:31:33: error:
• Could not deduce: ((e : s) :\ x) ~ (e : (s :\ x))
from the context: (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
bound by the instance declaration at Bug.hs:(29,31)(30,27)
or from: (k ~ *, (y : xs :: [k]) ~~ (e : s :: [*]))
bound by a pattern with constructor:
Ext :: forall e (s :: [*]). e > Set s > Set (e : s),
in an equation for ‘remove’
at Bug.hs:31:1118
Expected type: Set ((y : xs) :\ x)
Actual type: Set (e : (s :\ x))
• In the expression: Ext y (remove xs x)
In an equation for ‘remove’:
remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
In the instance declaration for ‘Remove (y : xs) x’
• Relevant bindings include
x :: Proxy x (bound at Bug.hs:31:22)
xs :: Set s (bound at Bug.hs:31:17)
y :: e (bound at Bug.hs:31:15)
remove :: Set (y : xs) > Proxy x > Set ((y : xs) :\ x)
(bound at Bug.hs:31:3)

31  remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
 ^^^^^^^^^^^^^^^^^^^
```
This regression was introduced in commit e3dbb44f53b2f9403d20d84e27f187062755a089 (Fix #12919 by making the flattener homegeneous.).8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15664Core Lint error20190707T18:03:32ZIcelandjackCore Lint errorFrom [Generic Programming of All Kinds](https://dl.acm.org/citation.cfm?id=3242745),
```hs
{# Language RankNTypes, TypeOperators, DataKinds, PolyKinds, GADTs, TypeInType, TypeFamilies #}
{# Options_GHC dcorelint #}
import Data.Kind
import GHC.Exts
import Data.Function
data Ctx :: Type > Type where
E :: Ctx(Type)
(:&:) :: a > Ctx(as) > Ctx(a > as)
type family
Apply(kind) (f :: kind) (ctx :: Ctx kind) :: Type where
Apply(Type) a E = a
Apply(k > ks) f (a:&:as) = Apply(ks) (f a) as
data ApplyT kind :: kind > Ctx(kind) > Type where
A0 :: a
> ApplyT(Type) a E
AS :: ApplyT(ks) (f a) as
> ApplyT(k > ks) f (a:&:as)
type f ~> g = (forall xx. f xx > g xx)
unravel :: ApplyT(k) f ~> Apply(k) f
unravel (A0 a) = a
unravel (AS fa) = unravel fa
```
gives a core lint error
```
$ ghci ignoredotghci hs/443.hs > /tmp/bug.log
```From [Generic Programming of All Kinds](https://dl.acm.org/citation.cfm?id=3242745),
```hs
{# Language RankNTypes, TypeOperators, DataKinds, PolyKinds, GADTs, TypeInType, TypeFamilies #}
{# Options_GHC dcorelint #}
import Data.Kind
import GHC.Exts
import Data.Function
data Ctx :: Type > Type where
E :: Ctx(Type)
(:&:) :: a > Ctx(as) > Ctx(a > as)
type family
Apply(kind) (f :: kind) (ctx :: Ctx kind) :: Type where
Apply(Type) a E = a
Apply(k > ks) f (a:&:as) = Apply(ks) (f a) as
data ApplyT kind :: kind > Ctx(kind) > Type where
A0 :: a
> ApplyT(Type) a E
AS :: ApplyT(ks) (f a) as
> ApplyT(k > ks) f (a:&:as)
type f ~> g = (forall xx. f xx > g xx)
unravel :: ApplyT(k) f ~> Apply(k) f
unravel (A0 a) = a
unravel (AS fa) = unravel fa
```
gives a core lint error
```
$ ghci ignoredotghci hs/443.hs > /tmp/bug.log
```8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15589Always promoting metavariables during type inference may be wrong20190707T18:04:00ZRichard Eisenbergrae@richarde.devAlways promoting metavariables during type inference may be wrongCurrently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.
Consider
```hs
{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: forall k. k > k > Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
IfK (_ :: Proxy True) f _ = f
IfK (_ :: Proxy False) _ g = g
y :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True > ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
x = undefined
in ()
```
This panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.
 We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j > m > n > If j m n`, where `If :: forall k. Bool > k > k > k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator.
 In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2.
 If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem.
 Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`.
 Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late.
Yet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these "ambient givens" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed.
An alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case  promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [my thesis](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs)  section 6.5 to be specific.)
<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  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Always promoting metavariables during type inference may be wrong","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Currently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.\r\n\r\nConsider\r\n\r\n{{{#!hs\r\n{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,\r\n AllowAmbiguousTypes #}\r\n\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\nimport Data.Type.Bool\r\nimport Data.Kind\r\n\r\ndata SameKind :: forall k. k > k > Type\r\ntype family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where\r\n IfK (_ :: Proxy True) f _ = f\r\n IfK (_ :: Proxy False) _ g = g\r\n\r\ny :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True > ()\r\ny Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d\r\n x = undefined\r\n in ()\r\n}}}\r\n\r\nThis panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.\r\n\r\n* We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j > m > n > If j m n`, where `If :: forall k. Bool > k > k > k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator.\r\n\r\n* In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2.\r\n\r\n* If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem.\r\n\r\n* Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`.\r\n\r\n* Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late.\r\n\r\nYet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these \"ambient givens\" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed.\r\n\r\nAn alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case  promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs my thesis]  section 6.5 to be specific.)","type_of_failure":"OtherFailure","blocking":[]} >Currently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.
Consider
```hs
{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: forall k. k > k > Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
IfK (_ :: Proxy True) f _ = f
IfK (_ :: Proxy False) _ g = g
y :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True > ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
x = undefined
in ()
```
This panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.
 We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j > m > n > If j m n`, where `If :: forall k. Bool > k > k > k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator.
 In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2.
 If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem.
 Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`.
 Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late.
Yet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these "ambient givens" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed.
An alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case  promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [my thesis](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs)  section 6.5 to be specific.)
<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  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Always promoting metavariables during type inference may be wrong","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Currently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.\r\n\r\nConsider\r\n\r\n{{{#!hs\r\n{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,\r\n AllowAmbiguousTypes #}\r\n\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\nimport Data.Type.Bool\r\nimport Data.Kind\r\n\r\ndata SameKind :: forall k. k > k > Type\r\ntype family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where\r\n IfK (_ :: Proxy True) f _ = f\r\n IfK (_ :: Proxy False) _ g = g\r\n\r\ny :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True > ()\r\ny Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d\r\n x = undefined\r\n in ()\r\n}}}\r\n\r\nThis panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.\r\n\r\n* We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j > m > n > If j m n`, where `If :: forall k. Bool > k > k > k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator.\r\n\r\n* In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2.\r\n\r\n* If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem.\r\n\r\n* Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`.\r\n\r\n* Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late.\r\n\r\nYet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these \"ambient givens\" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed.\r\n\r\nAn alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case  promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs my thesis]  section 6.5 to be specific.)","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15588Panic when abusing kind inference20190707T18:04:01ZRichard Eisenbergrae@richarde.devPanic when abusing kind inferenceWhen I say
```hs
{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: forall k. k > k > Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
IfK (_ :: Proxy True) f _ = f
IfK (_ :: Proxy False) _ g = g
y :: forall ck (c :: ck). ck :~: Proxy True > ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
x = undefined
in ()
```
HEAD says
```
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.7.20180827 for x86_64appledarwin):
ASSERT failed!
Bad coercion hole co_a3iZ: If
j_a3j0[tau:2] m_a3j1[tau:2] a_a3gV[sk:3]
a_a3gV[sk:3]
nominal
If j_a3j0[tau:2] m_a3j1[tau:2] a_a3jj[sk:3] ~# a_a3jj[sk:3]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcMType.hs:316:25 in ghc:TcMType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
It's as yet unclear whether the program should be accepted. My best guess is that it should, but that (even with this panic fixed) GHC isn't up to the task.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"Panic when abusing kind inference","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I say\r\n\r\n{{{#!hs\r\n{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,\r\n AllowAmbiguousTypes #}\r\n\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\nimport Data.Type.Bool\r\nimport Data.Kind\r\n\r\ndata SameKind :: forall k. k > k > Type\r\ntype family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where\r\n IfK (_ :: Proxy True) f _ = f\r\n IfK (_ :: Proxy False) _ g = g\r\n\r\ny :: forall ck (c :: ck). ck :~: Proxy True > ()\r\ny Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d\r\n x = undefined\r\n in ()\r\n}}}\r\n\r\nHEAD says\r\n\r\n{{{\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20180827 for x86_64appledarwin):\r\n\tASSERT failed!\r\n Bad coercion hole co_a3iZ: If\r\n j_a3j0[tau:2] m_a3j1[tau:2] a_a3gV[sk:3]\r\n a_a3gV[sk:3]\r\n nominal\r\n If j_a3j0[tau:2] m_a3j1[tau:2] a_a3jj[sk:3] ~# a_a3jj[sk:3]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcMType.hs:316:25 in ghc:TcMType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nIt's as yet unclear whether the program should be accepted. My best guess is that it should, but that (even with this panic fixed) GHC isn't up to the task.","type_of_failure":"OtherFailure","blocking":[]} >When I say
```hs
{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: forall k. k > k > Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
IfK (_ :: Proxy True) f _ = f
IfK (_ :: Proxy False) _ g = g
y :: forall ck (c :: ck). ck :~: Proxy True > ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
x = undefined
in ()
```
HEAD says
```
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.7.20180827 for x86_64appledarwin):
ASSERT failed!
Bad coercion hole co_a3iZ: If
j_a3j0[tau:2] m_a3j1[tau:2] a_a3gV[sk:3]
a_a3gV[sk:3]
nominal
If j_a3j0[tau:2] m_a3j1[tau:2] a_a3jj[sk:3] ~# a_a3jj[sk:3]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcMType.hs:316:25 in ghc:TcMType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
It's as yet unclear whether the program should be accepted. My best guess is that it should, but that (even with this panic fixed) GHC isn't up to the task.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"Panic when abusing kind inference","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I say\r\n\r\n{{{#!hs\r\n{# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,\r\n AllowAmbiguousTypes #}\r\n\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\nimport Data.Type.Bool\r\nimport Data.Kind\r\n\r\ndata SameKind :: forall k. k > k > Type\r\ntype family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where\r\n IfK (_ :: Proxy True) f _ = f\r\n IfK (_ :: Proxy False) _ g = g\r\n\r\ny :: forall ck (c :: ck). ck :~: Proxy True > ()\r\ny Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d\r\n x = undefined\r\n in ()\r\n}}}\r\n\r\nHEAD says\r\n\r\n{{{\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20180827 for x86_64appledarwin):\r\n\tASSERT failed!\r\n Bad coercion hole co_a3iZ: If\r\n j_a3j0[tau:2] m_a3j1[tau:2] a_a3gV[sk:3]\r\n a_a3gV[sk:3]\r\n nominal\r\n If j_a3j0[tau:2] m_a3j1[tau:2] a_a3jj[sk:3] ~# a_a3jj[sk:3]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcMType.hs:316:25 in ghc:TcMType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nIt's as yet unclear whether the program should be accepted. My best guess is that it should, but that (even with this panic fixed) GHC isn't up to the task.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15583Treating Constraint as Type when using (type C = Constraint)20190707T18:04:02ZIcelandjackTreating Constraint as Type when using (type C = Constraint)This may be similar/same as #15412? I can't get to the latest GHC right now. Again the "culprit" is using `type C = Constraint`.
The code example should not compile, but the error it gives is unexpected. If we define the associated type family `Ob_ (cat :: Cat ob) :: ob > C` using `C`
```hs
{# Language KindSignatures, PolyKinds, DataKinds, TypeInType, TypeFamilies, FlexibleInstances #}
import Data.Kind
type T = Type
type C = Constraint
type Cat ob = ob > ob > T
class Category_ (cat :: Cat ob) where
type Ob_ (cat :: Cat ob) :: ob > C
id_ :: Ob_ cat a => cat a a
class NoCls (a::k)
instance NoCls (a::k)
instance Category_ (>) where
type Ob_ (>) = NoCls
 id_ :: NoCls a => (a > a) XInstanceSigs
id_ = ()
```
the definition of `id_` fails (as we expect), but the expected type (`Ob_ (>) a > a > a`) is wrong:
```
$ ghci ignoredotghci 348.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 348.hs, interpreted )
348.hs:22:9: error:
• Couldn't match expected type ‘Ob_ (>) a > a > a’
with actual type ‘()’
• In the expression: ()
In an equation for ‘id_’: id_ = ()
In the instance declaration for ‘Category_ (>)’
• Relevant bindings include
id_ :: Ob_ (>) a > a > a (bound at 348.hs:22:3)

22  id_ = ()
 ^^
Failed, no modules loaded.
Prelude>
```
If we simply replace `Ob_` with `type Ob_ (cat :: Cat ob) :: ob > Constraint`, the expected type (`a > a`) matches my intuition:
```
348.hs:22:9: error:
• Couldn't match expected type ‘a > a’ with actual type ‘()’
• In the expression: ()
In an equation for ‘id_’: id_ = ()
In the instance declaration for ‘Category_ (>)’
• Relevant bindings include id_ :: a > a (bound at 348.hs:22:3)

22  id_ = ()
 ^^
```This may be similar/same as #15412? I can't get to the latest GHC right now. Again the "culprit" is using `type C = Constraint`.
The code example should not compile, but the error it gives is unexpected. If we define the associated type family `Ob_ (cat :: Cat ob) :: ob > C` using `C`
```hs
{# Language KindSignatures, PolyKinds, DataKinds, TypeInType, TypeFamilies, FlexibleInstances #}
import Data.Kind
type T = Type
type C = Constraint
type Cat ob = ob > ob > T
class Category_ (cat :: Cat ob) where
type Ob_ (cat :: Cat ob) :: ob > C
id_ :: Ob_ cat a => cat a a
class NoCls (a::k)
instance NoCls (a::k)
instance Category_ (>) where
type Ob_ (>) = NoCls
 id_ :: NoCls a => (a > a) XInstanceSigs
id_ = ()
```
the definition of `id_` fails (as we expect), but the expected type (`Ob_ (>) a > a > a`) is wrong:
```
$ ghci ignoredotghci 348.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 348.hs, interpreted )
348.hs:22:9: error:
• Couldn't match expected type ‘Ob_ (>) a > a > a’
with actual type ‘()’
• In the expression: ()
In an equation for ‘id_’: id_ = ()
In the instance declaration for ‘Category_ (>)’
• Relevant bindings include
id_ :: Ob_ (>) a > a > a (bound at 348.hs:22:3)

22  id_ = ()
 ^^
Failed, no modules loaded.
Prelude>
```
If we simply replace `Ob_` with `type Ob_ (cat :: Cat ob) :: ob > Constraint`, the expected type (`a > a`) matches my intuition:
```
348.hs:22:9: error:
• Couldn't match expected type ‘a > a’ with actual type ‘()’
• In the expression: ()
In an equation for ‘id_’: id_ = ()
In the instance declaration for ‘Category_ (>)’
• Relevant bindings include id_ :: a > a (bound at 348.hs:22:3)

22  id_ = ()
 ^^
```8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15561TypeInType: Type error conditioned on ordering of GADT and type family defini...20190707T18:04:07ZBj0rnTypeInType: Type error conditioned on ordering of GADT and type family definitionsConsider this code which successfully compiles:
```hs
{# LANGUAGE TypeInType, TypeFamilies, GADTs #}
module Bug where
class HasIndex a where
type Index a
emptyIndex :: IndexWrapper a
instance HasIndex [a] where
type Index [a] = Int
emptyIndex = Wrap 0
data IndexWrapper a where
Wrap :: Index a > IndexWrapper a
type family UnwrapAnyWrapperLikeThing (a :: t) :: k
type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a
```
The mere act of moving the definition of `IndexWrapper` anywhere below the definition of `UnwrapAnyWrapperLikeThing` makes the type family instance at the bottom of the example fail compilation, with this error:
```
Bug.hs:17:15: error:
• Illegal type synonym family application in instance: Index [b]
• In the type instance declaration for ‘UnwrapAnyWrapperLikeThing’

17  type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is the smallest example that I could come up with; my real scenario of course has more things going on, but I can share if it would help.
The problem for me (other than that I'm pretty sure reordering definitions in Haskell should never affect anything) is that I would like just the definition of the type family (`UnwrapAnyWrapperLikeThing` in this example) in module `A` and all of the other definitions in module `B` that imports `A`.
Ideally, I would have liked to add a `HasIndex a` constraint to the `Wrap` constructor, but that disqualifies use of `'Wrap` on the type level. This does make me feel like I'm on shaky ground to begin with.
I have reproduced this bug on 8.2.2, 8.4.3 and 8.6.0.20180810 (NixOS). I should note that 8.0.2 rejects even the code that I pasted here.
<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  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"TypeInType: Type error conditioned on ordering of GADT and type family definitions","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["GADTs","TypeFamilies,","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this code which successfully compiles:\r\n{{{#!hs\r\n{# LANGUAGE TypeInType, TypeFamilies, GADTs #}\r\n\r\nmodule Bug where\r\n\r\nclass HasIndex a where\r\n type Index a\r\n emptyIndex :: IndexWrapper a\r\ninstance HasIndex [a] where\r\n type Index [a] = Int\r\n emptyIndex = Wrap 0\r\n\r\ndata IndexWrapper a where\r\n Wrap :: Index a > IndexWrapper a\r\n\r\ntype family UnwrapAnyWrapperLikeThing (a :: t) :: k\r\n\r\ntype instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a\r\n}}}\r\n\r\nThe mere act of moving the definition of `IndexWrapper` anywhere below the definition of `UnwrapAnyWrapperLikeThing` makes the type family instance at the bottom of the example fail compilation, with this error:\r\n{{{\r\nBug.hs:17:15: error:\r\n • Illegal type synonym family application in instance: Index [b]\r\n • In the type instance declaration for ‘UnwrapAnyWrapperLikeThing’\r\n \r\n17  type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nThis is the smallest example that I could come up with; my real scenario of course has more things going on, but I can share if it would help.\r\n\r\nThe problem for me (other than that I'm pretty sure reordering definitions in Haskell should never affect anything) is that I would like just the definition of the type family (`UnwrapAnyWrapperLikeThing` in this example) in module `A` and all of the other definitions in module `B` that imports `A`.\r\n\r\nIdeally, I would have liked to add a `HasIndex a` constraint to the `Wrap` constructor, but that disqualifies use of `'Wrap` on the type level. This does make me feel like I'm on shaky ground to begin with.\r\n\r\nI have reproduced this bug on 8.2.2, 8.4.3 and 8.6.0.20180810 (NixOS). I should note that 8.0.2 rejects even the code that I pasted here.","type_of_failure":"OtherFailure","blocking":[]} >Consider this code which successfully compiles:
```hs
{# LANGUAGE TypeInType, TypeFamilies, GADTs #}
module Bug where
class HasIndex a where
type Index a
emptyIndex :: IndexWrapper a
instance HasIndex [a] where
type Index [a] = Int
emptyIndex = Wrap 0
data IndexWrapper a where
Wrap :: Index a > IndexWrapper a
type family UnwrapAnyWrapperLikeThing (a :: t) :: k
type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a
```
The mere act of moving the definition of `IndexWrapper` anywhere below the definition of `UnwrapAnyWrapperLikeThing` makes the type family instance at the bottom of the example fail compilation, with this error:
```
Bug.hs:17:15: error:
• Illegal type synonym family application in instance: Index [b]
• In the type instance declaration for ‘UnwrapAnyWrapperLikeThing’

17  type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is the smallest example that I could come up with; my real scenario of course has more things going on, but I can share if it would help.
The problem for me (other than that I'm pretty sure reordering definitions in Haskell should never affect anything) is that I would like just the definition of the type family (`UnwrapAnyWrapperLikeThing` in this example) in module `A` and all of the other definitions in module `B` that imports `A`.
Ideally, I would have liked to add a `HasIndex a` constraint to the `Wrap` constructor, but that disqualifies use of `'Wrap` on the type level. This does make me feel like I'm on shaky ground to begin with.
I have reproduced this bug on 8.2.2, 8.4.3 and 8.6.0.20180810 (NixOS). I should note that 8.0.2 rejects even the code that I pasted here.
<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  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"TypeInType: Type error conditioned on ordering of GADT and type family definitions","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["GADTs","TypeFamilies,","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this code which successfully compiles:\r\n{{{#!hs\r\n{# LANGUAGE TypeInType, TypeFamilies, GADTs #}\r\n\r\nmodule Bug where\r\n\r\nclass HasIndex a where\r\n type Index a\r\n emptyIndex :: IndexWrapper a\r\ninstance HasIndex [a] where\r\n type Index [a] = Int\r\n emptyIndex = Wrap 0\r\n\r\ndata IndexWrapper a where\r\n Wrap :: Index a > IndexWrapper a\r\n\r\ntype family UnwrapAnyWrapperLikeThing (a :: t) :: k\r\n\r\ntype instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a\r\n}}}\r\n\r\nThe mere act of moving the definition of `IndexWrapper` anywhere below the definition of `UnwrapAnyWrapperLikeThing` makes the type family instance at the bottom of the example fail compilation, with this error:\r\n{{{\r\nBug.hs:17:15: error:\r\n • Illegal type synonym family application in instance: Index [b]\r\n • In the type instance declaration for ‘UnwrapAnyWrapperLikeThing’\r\n \r\n17  type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nThis is the smallest example that I could come up with; my real scenario of course has more things going on, but I can share if it would help.\r\n\r\nThe problem for me (other than that I'm pretty sure reordering definitions in Haskell should never affect anything) is that I would like just the definition of the type family (`UnwrapAnyWrapperLikeThing` in this example) in module `A` and all of the other definitions in module `B` that imports `A`.\r\n\r\nIdeally, I would have liked to add a `HasIndex a` constraint to the `Wrap` constructor, but that disqualifies use of `'Wrap` on the type level. This does make me feel like I'm on shaky ground to begin with.\r\n\r\nI have reproduced this bug on 8.2.2, 8.4.3 and 8.6.0.20180810 (NixOS). I should note that 8.0.2 rejects even the code that I pasted here.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15545Forced to enable TypeInType because of (i ~ i)20190707T18:04:13ZIcelandjackForced to enable TypeInType because of (i ~ i)I don't know if this is a bug but `i ~ i` holds by reflexivity so I would not have expected it to require `TypeInType`
```
$ ghci ignoredotghci
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
Prelude> :set XPolyKinds XGADTs
Prelude> import Data.Kind
Prelude Data.Kind> data NP :: (k > Type) > (i > Type) where NP :: f a > NP f a
<interactive>:3:45: error:
• Data constructor ‘NP’ constrains the choice of kind parameter:
i ~ i
Use TypeInType to allow this
• In the definition of data constructor ‘NP’
In the data type declaration for ‘NP’
Prelude Data.Kind>
```
I would rather expect the warning I get after enabling `TypeInType`
```
Prelude Data.Kind> :set XTypeInType
Prelude Data.Kind> data NP :: (k > Type) > (i > Type) where NP :: f a > NP f a
<interactive>:8:28: error:
• Couldn't match ‘k’ with ‘i’
• In the data declaration for ‘NP’
```

**ps** making sure this is OK as well; it works after enabling `XTypeInType` and quantifying with `XRankNTypes` (is this using polymorphic recursion?)
```
Prelude Data.Kind> :set XTypeInType XRankNTypes
Prelude Data.Kind> data NP :: forall i k. (k > Type) > (i > Type) where NP :: f a > NP f a
Prelude Data.Kind> :t NP
NP :: forall i (f :: i > *) (a :: i). f a > NP f a
```
it also works for
```hs
data NP :: forall k. (k > Type) > (i > Type) where NP :: f a > NP f a
data NP :: forall i. (k > Type) > (i > Type) where NP :: f a > NP f a
data NP :: (k > Type) > forall i. (i > Type) where NP :: f a > NP f a
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"Forced to enable TypeInType because of (i ~ i)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I don't know if this is a bug but `i ~ i` holds by reflexivity so I would not have expected it to require `TypeInType`\r\n\r\n{{{\r\n$ ghci ignoredotghci\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\nPrelude> :set XPolyKinds XGADTs\r\nPrelude> import Data.Kind\r\nPrelude Data.Kind> data NP :: (k > Type) > (i > Type) where NP :: f a > NP f a\r\n\r\n<interactive>:3:45: error:\r\n • Data constructor ‘NP’ constrains the choice of kind parameter:\r\n i ~ i\r\n Use TypeInType to allow this\r\n • In the definition of data constructor ‘NP’\r\n In the data type declaration for ‘NP’\r\nPrelude Data.Kind> \r\n}}}\r\n\r\nI would rather expect the warning I get after enabling `TypeInType`\r\n\r\n{{{\r\nPrelude Data.Kind> :set XTypeInType\r\nPrelude Data.Kind> data NP :: (k > Type) > (i > Type) where NP :: f a > NP f a\r\n\r\n<interactive>:8:28: error:\r\n • Couldn't match ‘k’ with ‘i’\r\n • In the data declaration for ‘NP’\r\n}}}\r\n\r\n\r\n\r\n'''ps''' making sure this is OK as well; it works after enabling `XTypeInType` and quantifying with `XRankNTypes` (is this using polymorphic recursion?)\r\n\r\n{{{\r\nPrelude Data.Kind> :set XTypeInType XRankNTypes\r\nPrelude Data.Kind> data NP :: forall i k. (k > Type) > (i > Type) where NP :: f a > NP f a\r\nPrelude Data.Kind> :t NP\r\nNP :: forall i (f :: i > *) (a :: i). f a > NP f a\r\n}}}\r\n\r\nit also works for\r\n\r\n{{{#!hs\r\ndata NP :: forall k. (k > Type) > (i > Type) where NP :: f a > NP f a\r\ndata NP :: forall i. (k > Type) > (i > Type) where NP :: f a > NP f a\r\ndata NP :: (k > Type) > forall i. (i > Type) where NP :: f a > NP f a\r\n}}}\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} >I don't know if this is a bug but `i ~ i` holds by reflexivity so I would not have expected it to require `TypeInType`
```
$ ghci ignoredotghci
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
Prelude> :set XPolyKinds XGADTs
Prelude> import Data.Kind
Prelude Data.Kind> data NP :: (k > Type) > (i > Type) where NP :: f a > NP f a
<interactive>:3:45: error:
• Data constructor ‘NP’ constrains the choice of kind parameter:
i ~ i
Use TypeInType to allow this
• In the definition of data constructor ‘NP’
In the data type declaration for ‘NP’
Prelude Data.Kind>
```
I would rather expect the warning I get after enabling `TypeInType`
```
Prelude Data.Kind> :set XTypeInType
Prelude Data.Kind> data NP :: (k > Type) > (i > Type) where NP :: f a > NP f a
<interactive>:8:28: error:
• Couldn't match ‘k’ with ‘i’
• In the data declaration for ‘NP’
```

**ps** making sure this is OK as well; it works after enabling `XTypeInType` and quantifying with `XRankNTypes` (is this using polymorphic recursion?)
```
Prelude Data.Kind> :set XTypeInType XRankNTypes
Prelude Data.Kind> data NP :: forall i k. (k > Type) > (i > Type) where NP :: f a > NP f a
Prelude Data.Kind> :t NP
NP :: forall i (f :: i > *) (a :: i). f a > NP f a
```
it also works for
```hs
data NP :: forall k. (k > Type) > (i > Type) where NP :: f a > NP f a
data NP :: forall i. (k > Type) > (i > Type) where NP :: f a > NP f a
data NP :: (k > Type) > forall i. (i > Type) where NP :: f a > NP f a
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 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":"Forced to enable TypeInType because of (i ~ i)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I don't know if this is a bug but `i ~ i` holds by reflexivity so I would not have expected it to require `TypeInType`\r\n\r\n{{{\r\n$ ghci ignoredotghci\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\nPrelude> :set XPolyKinds XGADTs\r\nPrelude> import Data.Kind\r\nPrelude Data.Kind> data NP :: (k > Type) > (i > Type) where NP :: f a > NP f a\r\n\r\n<interactive>:3:45: error:\r\n • Data constructor ‘NP’ constrains the choice of kind parameter:\r\n i ~ i\r\n Use TypeInType to allow this\r\n • In the definition of data constructor ‘NP’\r\n In the data type declaration for ‘NP’\r\nPrelude Data.Kind> \r\n}}}\r\n\r\nI would rather expect the warning I get after enabling `TypeInType`\r\n\r\n{{{\r\nPrelude Data.Kind> :set XTypeInType\r\nPrelude Data.Kind> data NP :: (k > Type) > (i > Type) where NP :: f a > NP f a\r\n\r\n<interactive>:8:28: error:\r\n • Couldn't match ‘k’ with ‘i’\r\n • In the data declaration for ‘NP’\r\n}}}\r\n\r\n\r\n\r\n'''ps''' making sure this is OK as well; it works after enabling `XTypeInType` and quantifying with `XRankNTypes` (is this using polymorphic recursion?)\r\n\r\n{{{\r\nPrelude Data.Kind> :set XTypeInType XRankNTypes\r\nPrelude Data.Kind> data NP :: forall i k. (k > Type) > (i > Type) where NP :: f a > NP f a\r\nPrelude Data.Kind> :t NP\r\nNP :: forall i (f :: i > *) (a :: i). f a > NP f a\r\n}}}\r\n\r\nit also works for\r\n\r\n{{{#!hs\r\ndata NP :: forall k. (k > Type) > (i > Type) where NP :: f a > NP f a\r\ndata NP :: forall i. (k > Type) > (i > Type) where NP :: f a > NP f a\r\ndata NP :: (k > Type) > forall i. (i > Type) where NP :: f a > NP f a\r\n}}}\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15428Oversaturated type family application panicks GHC (piResultTys2)20190707T18:04:56ZRyan ScottOversaturated type family application panicks GHC (piResultTys2)The following program panics when compiled with GHC 8.6.1 or HEAD:
```hs
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Proxy
import Data.Type.Equality
type family Flurmp :: k
type family Pure (x :: a) :: f a
wat :: forall (f :: Type > Type) (p :: Type).
Proxy (f p) > ()
wat _ =
let s :: (Flurmp :: f p)
:~: Pure (Flurmp :: p > p) (Flurmp :: p)
s = undefined
in ()
```
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.0.20180714 for x86_64unknownlinux):
piResultTys2
f_aAT a_aAU
[(>) p_a1uI[sk:1], p_a1uI[sk:1] > p_a1uI[sk:1], Flurmp, Flurmp]
[Flurmp]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1041:9 in ghc:Type
```
On GHC 8.4 and earlier, this simply gives an error message:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:18:16: error:
• Expecting one more argument to ‘Pure (Flurmp :: p > p)’
Expected kind ‘p > f p’,
but ‘Pure (Flurmp :: p > p)’ has kind ‘p > p > p’
• In the second argument of ‘(:~:)’, namely
‘Pure (Flurmp :: p > p) (Flurmp :: p)’
In the type signature:
s :: (Flurmp :: f p) :~: Pure (Flurmp :: p > p) (Flurmp :: p)
In the expression:
let
s :: (Flurmp :: f p) :~: Pure (Flurmp :: p > p) (Flurmp :: p)
s = undefined
in ()
• Relevant bindings include
wat :: Proxy (f p) > () (bound at Bug.hs:16:1)

18  :~: Pure (Flurmp :: p > p) (Flurmp :: p)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC 8.6+ panics (piResultTys2), older GHCs don't","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics when compiled with GHC 8.6.1 or HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ScopedTypeVariables #}\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.Proxy\r\nimport Data.Type.Equality\r\n\r\ntype family Flurmp :: k\r\ntype family Pure (x :: a) :: f a\r\n\r\nwat :: forall (f :: Type > Type) (p :: Type).\r\n Proxy (f p) > ()\r\nwat _ =\r\n let s :: (Flurmp :: f p)\r\n :~: Pure (Flurmp :: p > p) (Flurmp :: p)\r\n s = undefined\r\n in ()\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.0.20180714 for x86_64unknownlinux):\r\n piResultTys2\r\n f_aAT a_aAU\r\n [(>) p_a1uI[sk:1], p_a1uI[sk:1] > p_a1uI[sk:1], Flurmp, Flurmp]\r\n [Flurmp]\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/Type.hs:1041:9 in ghc:Type\r\n}}}\r\n\r\nOn GHC 8.4 and earlier, this simply gives an error message:\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:18:16: error:\r\n • Expecting one more argument to ‘Pure (Flurmp :: p > p)’\r\n Expected kind ‘p > f p’,\r\n but ‘Pure (Flurmp :: p > p)’ has kind ‘p > p > p’\r\n • In the second argument of ‘(:~:)’, namely\r\n ‘Pure (Flurmp :: p > p) (Flurmp :: p)’\r\n In the type signature:\r\n s :: (Flurmp :: f p) :~: Pure (Flurmp :: p > p) (Flurmp :: p)\r\n In the expression:\r\n let\r\n s :: (Flurmp :: f p) :~: Pure (Flurmp :: p > p) (Flurmp :: p)\r\n s = undefined\r\n in ()\r\n • Relevant bindings include\r\n wat :: Proxy (f p) > () (bound at Bug.hs:16:1)\r\n \r\n18  :~: Pure (Flurmp :: p > p) (Flurmp :: p)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >The following program panics when compiled with GHC 8.6.1 or HEAD:
```hs
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Proxy
import Data.Type.Equality
type family Flurmp :: k
type family Pure (x :: a) :: f a
wat :: forall (f :: Type > Type) (p :: Type).
Proxy (f p) > ()
wat _ =
let s :: (Flurmp :: f p)
:~: Pure (Flurmp :: p > p) (Flurmp :: p)
s = undefined
in ()
```
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.0.20180714 for x86_64unknownlinux):
piResultTys2
f_aAT a_aAU
[(>) p_a1uI[sk:1], p_a1uI[sk:1] > p_a1uI[sk:1], Flurmp, Flurmp]
[Flurmp]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1041:9 in ghc:Type
```
On GHC 8.4 and earlier, this simply gives an error message:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:18:16: error:
• Expecting one more argument to ‘Pure (Flurmp :: p > p)’
Expected kind ‘p > f p’,
but ‘Pure (Flurmp :: p > p)’ has kind ‘p > p > p’
• In the second argument of ‘(:~:)’, namely
‘Pure (Flurmp :: p > p) (Flurmp :: p)’
In the type signature:
s :: (Flurmp :: f p) :~: Pure (Flurmp :: p > p) (Flurmp :: p)
In the expression:
let
s :: (Flurmp :: f p) :~: Pure (Flurmp :: p > p) (Flurmp :: p)
s = undefined
in ()
• Relevant bindings include
wat :: Proxy (f p) > () (bound at Bug.hs:16:1)

18  :~: Pure (Flurmp :: p > p) (Flurmp :: p)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC 8.6+ panics (piResultTys2), older GHCs don't","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics when compiled with GHC 8.6.1 or HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ScopedTypeVariables #}\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.Proxy\r\nimport Data.Type.Equality\r\n\r\ntype family Flurmp :: k\r\ntype family Pure (x :: a) :: f a\r\n\r\nwat :: forall (f :: Type > Type) (p :: Type).\r\n Proxy (f p) > ()\r\nwat _ =\r\n let s :: (Flurmp :: f p)\r\n :~: Pure (Flurmp :: p > p) (Flurmp :: p)\r\n s = undefined\r\n in ()\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.0.20180714 for x86_64unknownlinux):\r\n piResultTys2\r\n f_aAT a_aAU\r\n [(>) p_a1uI[sk:1], p_a1uI[sk:1] > p_a1uI[sk:1], Flurmp, Flurmp]\r\n [Flurmp]\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/Type.hs:1041:9 in ghc:Type\r\n}}}\r\n\r\nOn GHC 8.4 and earlier, this simply gives an error message:\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:18:16: error:\r\n • Expecting one more argument to ‘Pure (Flurmp :: p > p)’\r\n Expected kind ‘p > f p’,\r\n but ‘Pure (Flurmp :: p > p)’ has kind ‘p > p > p’\r\n • In the second argument of ‘(:~:)’, namely\r\n ‘Pure (Flurmp :: p > p) (Flurmp :: p)’\r\n In the type signature:\r\n s :: (Flurmp :: f p) :~: Pure (Flurmp :: p > p) (Flurmp :: p)\r\n In the expression:\r\n let\r\n s :: (Flurmp :: f p) :~: Pure (Flurmp :: p > p) (Flurmp :: p)\r\n s = undefined\r\n in ()\r\n • Relevant bindings include\r\n wat :: Proxy (f p) > () (bound at Bug.hs:16:1)\r\n \r\n18  :~: Pure (Flurmp :: p > p) (Flurmp :: p)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15380Infinite typechecker loop in GHC 8.620190707T18:12:54ZRyan ScottInfinite typechecker loop in GHC 8.6The following program loops infinitely during typechecking with GHC 8.6.1 and HEAD:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
class Generic a where
type Rep a :: Type
class PGeneric a where
type To a (x :: Rep a) :: a
type family MDefault (x :: a) :: a where
MDefault x = To (M x)
class C a where
type M (x :: a) :: a
type M (x :: a) = MDefault x
```
In GHC 8.4.3, however this fails with a proper error:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:16: error:
• Occurs check: cannot construct the infinite kind:
a ~ Rep (M x) > M x
• In the type ‘To (M x)’
In the type family declaration for ‘MDefault’
• Type variable kinds: x :: a

15  MDefault x = To (M x)
 ^^^^^^^^
```
<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":"Infinite typechecker loop in GHC 8.6","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program loops infinitely during typechecking with GHC 8.6.1 and HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nclass Generic a where\r\n type Rep a :: Type\r\n\r\nclass PGeneric a where\r\n type To a (x :: Rep a) :: a\r\n\r\ntype family MDefault (x :: a) :: a where\r\n MDefault x = To (M x)\r\n\r\nclass C a where\r\n type M (x :: a) :: a\r\n type M (x :: a) = MDefault x\r\n}}}\r\n\r\nIn GHC 8.4.3, however this fails with a proper 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:15:16: error:\r\n • Occurs check: cannot construct the infinite kind:\r\n a ~ Rep (M x) > M x\r\n • In the type ‘To (M x)’\r\n In the type family declaration for ‘MDefault’\r\n • Type variable kinds: x :: a\r\n \r\n15  MDefault x = To (M x)\r\n  ^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >The following program loops infinitely during typechecking with GHC 8.6.1 and HEAD:
```hs
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
class Generic a where
type Rep a :: Type
class PGeneric a where
type To a (x :: Rep a) :: a
type family MDefault (x :: a) :: a where
MDefault x = To (M x)
class C a where
type M (x :: a) :: a
type M (x :: a) = MDefault x
```
In GHC 8.4.3, however this fails with a proper error:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:16: error:
• Occurs check: cannot construct the infinite kind:
a ~ Rep (M x) > M x
• In the type ‘To (M x)’
In the type family declaration for ‘MDefault’
• Type variable kinds: x :: a

15  MDefault x = To (M x)
 ^^^^^^^^
```
<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":"Infinite typechecker loop in GHC 8.6","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program loops infinitely during typechecking with GHC 8.6.1 and HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nclass Generic a where\r\n type Rep a :: Type\r\n\r\nclass PGeneric a where\r\n type To a (x :: Rep a) :: a\r\n\r\ntype family MDefault (x :: a) :: a where\r\n MDefault x = To (M x)\r\n\r\nclass C a where\r\n type M (x :: a) :: a\r\n type M (x :: a) = MDefault x\r\n}}}\r\n\r\nIn GHC 8.4.3, however this fails with a proper 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:15:16: error:\r\n • Occurs check: cannot construct the infinite kind:\r\n a ~ Rep (M x) > M x\r\n • In the type ‘To (M x)’\r\n In the type family declaration for ‘MDefault’\r\n • Type variable kinds: x :: a\r\n \r\n15  MDefault x = To (M x)\r\n  ^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://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/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 kind20190707T18:14:21ZRyan 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.1