GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20190707T18:03:54Zhttps://gitlab.haskell.org/ghc/ghc//issues/15597GHC shouting: panic!20190707T18:03:54ZtstrGHC shouting: panic!This program makes the impossible happen:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
import GHC.Types
data Bug :: (f x > Type) > Type where
Bug :: forall
(r::h > forall x. f x > Type)
(a::f x)
. (r::((f x > Type) > Type) > forall x. f x > Type) Bug a
> Bug (r::f x > Type)
```
And asked for reporting the error:
```
ghc: panic! (the 'impossible' happened)
(GHC version 8.4.1 for x86_64unknownlinux):
piResultTy
k_aozeA[tau:1]
(x_aozeN[sk:2] > {co_aozeO})
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:950:35 in ghc:Type
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC shouting: panic!","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program makes the impossible happen:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeInType #}\r\n\r\nimport GHC.Types\r\n\r\ndata Bug :: (f x > Type) > Type where\r\n Bug :: forall\r\n (r::h > forall x. f x > Type)\r\n (a::f x)\r\n . (r::((f x > Type) > Type) > forall x. f x > Type) Bug a\r\n > Bug (r::f x > Type)\r\n}}}\r\n\r\n\r\nAnd asked for reporting the error:\r\n\r\n{{{\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.4.1 for x86_64unknownlinux):\r\n\tpiResultTy\r\n k_aozeA[tau:1]\r\n (x_aozeN[sk:2] > {co_aozeO})\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:950:35 in ghc:Type\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >This program makes the impossible happen:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
import GHC.Types
data Bug :: (f x > Type) > Type where
Bug :: forall
(r::h > forall x. f x > Type)
(a::f x)
. (r::((f x > Type) > Type) > forall x. f x > Type) Bug a
> Bug (r::f x > Type)
```
And asked for reporting the error:
```
ghc: panic! (the 'impossible' happened)
(GHC version 8.4.1 for x86_64unknownlinux):
piResultTy
k_aozeA[tau:1]
(x_aozeN[sk:2] > {co_aozeO})
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:950:35 in ghc:Type
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC shouting: panic!","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program makes the impossible happen:\r\n\r\n{{{#!hs\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeInType #}\r\n\r\nimport GHC.Types\r\n\r\ndata Bug :: (f x > Type) > Type where\r\n Bug :: forall\r\n (r::h > forall x. f x > Type)\r\n (a::f x)\r\n . (r::((f x > Type) > Type) > forall x. f x > Type) Bug a\r\n > Bug (r::f x > Type)\r\n}}}\r\n\r\n\r\nAnd asked for reporting the error:\r\n\r\n{{{\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.4.1 for x86_64unknownlinux):\r\n\tpiResultTy\r\n k_aozeA[tau:1]\r\n (x_aozeN[sk:2] > {co_aozeO})\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:950:35 in ghc:Type\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://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/15577TypeApplicationsrelated infinite loop (GHC 8.6+ only)20190830T12:55:21ZRyan ScottTypeApplicationsrelated infinite loop (GHC 8.6+ only)The following program will loop infinitely when compiled on GHC 8.6 or HEAD:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# 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
class Generic1 (f :: k > Type) where
type Rep1 f :: k > Type
class PGeneric1 (f :: k > Type) where
type From1 (z :: f a) :: Rep1 f a
type To1 (z :: Rep1 f a) :: f a
class SGeneric1 (f :: k > Type) where
sFrom1 :: forall (a :: k) (z :: f a). Sing z > Sing (From1 z)
sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r > Sing (To1 r :: f a)
class (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k > Type) where
sTof1 :: forall (a :: k) (z :: f a). Sing z > To1 (From1 z) :~: z
sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r > From1 (To1 r :: f a) :~: r
foo :: forall (f :: Type > Type) (a :: Type) (r :: Rep1 f a).
VGeneric1 f
=> Sing r > From1 (To1 r :: f a) :~: r
foo x
 Refl < sFot1  Uncommenting the line below makes it work again:
 @Type
@f @a @r x
= Refl
```
This is a regression from GHC 8.4, since compiling this program with 8.4 simply errors:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:35:20: error:
• Expecting one more argument to ‘f’
Expected a type, but ‘f’ has kind ‘* > *’
• In the type ‘f’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl

35  @f @a @r x
 ^
Bug.hs:35:23: error:
• Expected kind ‘f1 > *’, but ‘a’ has kind ‘*’
• In the type ‘a’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

35  @f @a @r x
 ^
Bug.hs:35:26: error:
• Couldn't match kind ‘* > *’ with ‘*’
When matching kinds
f1 :: * > *
Rep1 f1 a1 :: *
Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’
• In the type ‘r’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

35  @f @a @r x
 ^
Bug.hs:35:28: error:
• Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’
When matching kinds
a1 :: *
'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep
• In the fourth argument of ‘sFot1’, namely ‘x’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

35  @f @a @r x
 ^
Bug.hs:36:5: error:
• Could not deduce: From1 (To1 r1) ~ r1
from the context: r0 ~ From1 (To1 r0)
bound by a pattern with constructor:
Refl :: forall k (a :: k). a :~: a,
in a pattern binding in
pattern guard for
an equation for ‘foo’
at Bug.hs:33:58
‘r1’ is a rigid type variable bound by
the type signature for:
foo :: forall (f1 :: * > *) a1 (r1 :: Rep1 f1 a1).
VGeneric1 f1 =>
Sing r1 > From1 (To1 r1) :~: r1
at Bug.hs:(29,1)(31,43)
Expected type: From1 (To1 r1) :~: r1
Actual type: r1 :~: r1
• In the expression: Refl
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

36  = Refl
 ^^^^
```
<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":"TypeApplicationsrelated infinite loop (GHC 8.6+ only)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeApplications,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program will loop infinitely when compiled on GHC 8.6 or HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\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\n\r\nclass Generic1 (f :: k > Type) where\r\n type Rep1 f :: k > Type\r\n\r\nclass PGeneric1 (f :: k > Type) where\r\n type From1 (z :: f a) :: Rep1 f a\r\n type To1 (z :: Rep1 f a) :: f a\r\n\r\nclass SGeneric1 (f :: k > Type) where\r\n sFrom1 :: forall (a :: k) (z :: f a). Sing z > Sing (From1 z)\r\n sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r > Sing (To1 r :: f a)\r\n\r\nclass (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k > Type) where\r\n sTof1 :: forall (a :: k) (z :: f a). Sing z > To1 (From1 z) :~: z\r\n sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r > From1 (To1 r :: f a) :~: r\r\n\r\nfoo :: forall (f :: Type > Type) (a :: Type) (r :: Rep1 f a).\r\n VGeneric1 f\r\n => Sing r > From1 (To1 r :: f a) :~: r\r\nfoo x\r\n  Refl < sFot1  Uncommenting the line below makes it work again:\r\n  @Type\r\n @f @a @r x\r\n = Refl\r\n}}}\r\n\r\nThis is a regression from GHC 8.4, since compiling this program with 8.4 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:35:20: error:\r\n • Expecting one more argument to ‘f’\r\n Expected a type, but ‘f’ has kind ‘* > *’\r\n • In the type ‘f’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:35:23: error:\r\n • Expected kind ‘f1 > *’, but ‘a’ has kind ‘*’\r\n • In the type ‘a’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:35:26: error:\r\n • Couldn't match kind ‘* > *’ with ‘*’\r\n When matching kinds\r\n f1 :: * > *\r\n Rep1 f1 a1 :: *\r\n Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’\r\n • In the type ‘r’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:35:28: error:\r\n • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’\r\n When matching kinds\r\n a1 :: *\r\n 'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep\r\n • In the fourth argument of ‘sFot1’, namely ‘x’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:36:5: error:\r\n • Could not deduce: From1 (To1 r1) ~ r1\r\n from the context: r0 ~ From1 (To1 r0)\r\n bound by a pattern with constructor:\r\n Refl :: forall k (a :: k). a :~: a,\r\n in a pattern binding in\r\n pattern guard for\r\n an equation for ‘foo’\r\n at Bug.hs:33:58\r\n ‘r1’ is a rigid type variable bound by\r\n the type signature for:\r\n foo :: forall (f1 :: * > *) a1 (r1 :: Rep1 f1 a1).\r\n VGeneric1 f1 =>\r\n Sing r1 > From1 (To1 r1) :~: r1\r\n at Bug.hs:(29,1)(31,43)\r\n Expected type: From1 (To1 r1) :~: r1\r\n Actual type: r1 :~: r1\r\n • In the expression: Refl\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n36  = Refl\r\n  ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >The following program will loop infinitely when compiled on GHC 8.6 or HEAD:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# 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
class Generic1 (f :: k > Type) where
type Rep1 f :: k > Type
class PGeneric1 (f :: k > Type) where
type From1 (z :: f a) :: Rep1 f a
type To1 (z :: Rep1 f a) :: f a
class SGeneric1 (f :: k > Type) where
sFrom1 :: forall (a :: k) (z :: f a). Sing z > Sing (From1 z)
sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r > Sing (To1 r :: f a)
class (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k > Type) where
sTof1 :: forall (a :: k) (z :: f a). Sing z > To1 (From1 z) :~: z
sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r > From1 (To1 r :: f a) :~: r
foo :: forall (f :: Type > Type) (a :: Type) (r :: Rep1 f a).
VGeneric1 f
=> Sing r > From1 (To1 r :: f a) :~: r
foo x
 Refl < sFot1  Uncommenting the line below makes it work again:
 @Type
@f @a @r x
= Refl
```
This is a regression from GHC 8.4, since compiling this program with 8.4 simply errors:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:35:20: error:
• Expecting one more argument to ‘f’
Expected a type, but ‘f’ has kind ‘* > *’
• In the type ‘f’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl

35  @f @a @r x
 ^
Bug.hs:35:23: error:
• Expected kind ‘f1 > *’, but ‘a’ has kind ‘*’
• In the type ‘a’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

35  @f @a @r x
 ^
Bug.hs:35:26: error:
• Couldn't match kind ‘* > *’ with ‘*’
When matching kinds
f1 :: * > *
Rep1 f1 a1 :: *
Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’
• In the type ‘r’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

35  @f @a @r x
 ^
Bug.hs:35:28: error:
• Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’
When matching kinds
a1 :: *
'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep
• In the fourth argument of ‘sFot1’, namely ‘x’
In a stmt of a pattern guard for
an equation for ‘foo’:
Refl < sFot1 @f @a @r x
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

35  @f @a @r x
 ^
Bug.hs:36:5: error:
• Could not deduce: From1 (To1 r1) ~ r1
from the context: r0 ~ From1 (To1 r0)
bound by a pattern with constructor:
Refl :: forall k (a :: k). a :~: a,
in a pattern binding in
pattern guard for
an equation for ‘foo’
at Bug.hs:33:58
‘r1’ is a rigid type variable bound by
the type signature for:
foo :: forall (f1 :: * > *) a1 (r1 :: Rep1 f1 a1).
VGeneric1 f1 =>
Sing r1 > From1 (To1 r1) :~: r1
at Bug.hs:(29,1)(31,43)
Expected type: From1 (To1 r1) :~: r1
Actual type: r1 :~: r1
• In the expression: Refl
In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl
• Relevant bindings include
x :: Sing r1 (bound at Bug.hs:32:5)
foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)

36  = Refl
 ^^^^
```
<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":"TypeApplicationsrelated infinite loop (GHC 8.6+ only)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeApplications,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program will loop infinitely when compiled on GHC 8.6 or HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\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\n\r\nclass Generic1 (f :: k > Type) where\r\n type Rep1 f :: k > Type\r\n\r\nclass PGeneric1 (f :: k > Type) where\r\n type From1 (z :: f a) :: Rep1 f a\r\n type To1 (z :: Rep1 f a) :: f a\r\n\r\nclass SGeneric1 (f :: k > Type) where\r\n sFrom1 :: forall (a :: k) (z :: f a). Sing z > Sing (From1 z)\r\n sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r > Sing (To1 r :: f a)\r\n\r\nclass (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k > Type) where\r\n sTof1 :: forall (a :: k) (z :: f a). Sing z > To1 (From1 z) :~: z\r\n sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r > From1 (To1 r :: f a) :~: r\r\n\r\nfoo :: forall (f :: Type > Type) (a :: Type) (r :: Rep1 f a).\r\n VGeneric1 f\r\n => Sing r > From1 (To1 r :: f a) :~: r\r\nfoo x\r\n  Refl < sFot1  Uncommenting the line below makes it work again:\r\n  @Type\r\n @f @a @r x\r\n = Refl\r\n}}}\r\n\r\nThis is a regression from GHC 8.4, since compiling this program with 8.4 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:35:20: error:\r\n • Expecting one more argument to ‘f’\r\n Expected a type, but ‘f’ has kind ‘* > *’\r\n • In the type ‘f’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:35:23: error:\r\n • Expected kind ‘f1 > *’, but ‘a’ has kind ‘*’\r\n • In the type ‘a’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:35:26: error:\r\n • Couldn't match kind ‘* > *’ with ‘*’\r\n When matching kinds\r\n f1 :: * > *\r\n Rep1 f1 a1 :: *\r\n Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’\r\n • In the type ‘r’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:35:28: error:\r\n • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’\r\n When matching kinds\r\n a1 :: *\r\n 'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep\r\n • In the fourth argument of ‘sFot1’, namely ‘x’\r\n In a stmt of a pattern guard for\r\n an equation for ‘foo’:\r\n Refl < sFot1 @f @a @r x\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n35  @f @a @r x\r\n  ^\r\n\r\nBug.hs:36:5: error:\r\n • Could not deduce: From1 (To1 r1) ~ r1\r\n from the context: r0 ~ From1 (To1 r0)\r\n bound by a pattern with constructor:\r\n Refl :: forall k (a :: k). a :~: a,\r\n in a pattern binding in\r\n pattern guard for\r\n an equation for ‘foo’\r\n at Bug.hs:33:58\r\n ‘r1’ is a rigid type variable bound by\r\n the type signature for:\r\n foo :: forall (f1 :: * > *) a1 (r1 :: Rep1 f1 a1).\r\n VGeneric1 f1 =>\r\n Sing r1 > From1 (To1 r1) :~: r1\r\n at Bug.hs:(29,1)(31,43)\r\n Expected type: From1 (To1 r1) :~: r1\r\n Actual type: r1 :~: r1\r\n • In the expression: Refl\r\n In an equation for ‘foo’: foo x  Refl < sFot1 @f @a @r x = Refl\r\n • Relevant bindings include\r\n x :: Sing r1 (bound at Bug.hs:32:5)\r\n foo :: Sing r1 > From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1)\r\n \r\n36  = Refl\r\n  ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.8.2Alp MestanogullariBen GamariAlp Mestanogullarihttps://gitlab.haskell.org/ghc/ghc//issues/15549Core Lint error with EmptyCase20190707T18:04:11ZRyan ScottCore Lint error with EmptyCaseThe following program gives a Core Lint error on GHC 8.2.2 and later:
```hs
{# LANGUAGE EmptyCase #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
import Data.Void
data family Sing (a :: k)
data V1 :: Type > Type
data instance Sing (z :: V1 p)
class Generic a where
type Rep a :: Type > Type
to :: Rep a x > a
class PGeneric a where
type To (z :: Rep a x) :: a
class SGeneric a where
sTo :: forall x (r :: Rep a x). Sing r > Sing (To r :: a)

instance Generic Void where
type Rep Void = V1
to x = case x of {}
type family EmptyCase (a :: j) :: k where
instance PGeneric Void where
type To x = EmptyCase x
instance SGeneric Void where
sTo x = case x of
```
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs dcorelint fforcerecomp
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
Bug.hs:38:7: warning:
[in body of lambda with binder x_aZ8 :: Sing r_a12q]
Kind application error in
coercion ‘(Sing (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R’
Function kind = forall k. k > *
Arg kinds = [(V1 x_a12p, *), (r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
Bug.hs:38:7: warning:
[in body of lambda with binder x_aZ8 :: Sing r_a12q]
Kind application error in
coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’
Function kind = V1 x_a12p > *
Arg kinds = [(r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
Bug.hs:38:7: warning:
[in body of lambda with binder x_aZ8 :: Sing r_a12q]
Kind application error in
coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’
Function kind = V1 x_a12p > *
Arg kinds = [(r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
<no location info>: warning:
In the type ‘R:SingV1z x_a12p r_a12q’
Kind application error in type ‘R:SingV1z x_a12p r_a12q’
Function kind = forall p > V1 p > *
Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
<no location info>: warning:
In the type ‘R:SingV1z x_a12p r_a12q’
Kind application error in type ‘R:SingV1z x_a12p r_a12q’
Function kind = forall p > V1 p > *
Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
*** Offending Program ***
<elided>
$csTo_a12n :: forall x (r :: Rep Void x). Sing r > Sing (To r)
[LclId,
Arity=1,
Str=<L,U>x,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]
$csTo_a12n
= \ (@ x_a12p)
(@ (r_a12q :: Rep Void x_a12p))
(x_aZ8 :: Sing r_a12q) >
case x_aZ8
`cast` ((Sing
(D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R ; D:R:SingV1z0[0]
<x_a12p>_N <r_a12q>_N
:: (Sing r_a12q :: *) ~R# (R:SingV1z x_a12p r_a12q :: *))
of nt_s13T {
}
```
GHC 8.0.2 does not appear to suffer from this Core Lint error.
<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":"Core Lint error with empty closed type family","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 gives a Core Lint error on GHC 8.2.2 and later:\r\n\r\n{{{#!hs\r\n{# LANGUAGE EmptyCase #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Void\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata V1 :: Type > Type\r\ndata instance Sing (z :: V1 p)\r\n\r\nclass Generic a where\r\n type Rep a :: Type > Type\r\n to :: Rep a x > a\r\n\r\nclass PGeneric a where\r\n type To (z :: Rep a x) :: a\r\n\r\nclass SGeneric a where\r\n sTo :: forall x (r :: Rep a x). Sing r > Sing (To r :: a)\r\n\r\n\r\n\r\ninstance Generic Void where\r\n type Rep Void = V1\r\n to x = case x of {}\r\n\r\ntype family EmptyCase (a :: j) :: k where\r\n\r\ninstance PGeneric Void where\r\n type To x = EmptyCase x\r\n\r\ninstance SGeneric Void where\r\n sTo x = case x of\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs dcorelint fforcerecomp \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n*** Core Lint errors : in result of Simplifier ***\r\nBug.hs:38:7: warning:\r\n [in body of lambda with binder x_aZ8 :: Sing r_a12q]\r\n Kind application error in\r\n coercion ‘(Sing (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R’\r\n Function kind = forall k. k > *\r\n Arg kinds = [(V1 x_a12p, *), (r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\nBug.hs:38:7: warning:\r\n [in body of lambda with binder x_aZ8 :: Sing r_a12q]\r\n Kind application error in\r\n coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’\r\n Function kind = V1 x_a12p > *\r\n Arg kinds = [(r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\nBug.hs:38:7: warning:\r\n [in body of lambda with binder x_aZ8 :: Sing r_a12q]\r\n Kind application error in\r\n coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’\r\n Function kind = V1 x_a12p > *\r\n Arg kinds = [(r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\n<no location info>: warning:\r\n In the type ‘R:SingV1z x_a12p r_a12q’\r\n Kind application error in type ‘R:SingV1z x_a12p r_a12q’\r\n Function kind = forall p > V1 p > *\r\n Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\n<no location info>: warning:\r\n In the type ‘R:SingV1z x_a12p r_a12q’\r\n Kind application error in type ‘R:SingV1z x_a12p r_a12q’\r\n Function kind = forall p > V1 p > *\r\n Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\n*** Offending Program ***\r\n\r\n<elided>\r\n\r\n$csTo_a12n :: forall x (r :: Rep Void x). Sing r > Sing (To r)\r\n[LclId,\r\n Arity=1,\r\n Str=<L,U>x,\r\n Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,\r\n WorkFree=True, Expandable=True,\r\n Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]\r\n$csTo_a12n\r\n = \\ (@ x_a12p)\r\n (@ (r_a12q :: Rep Void x_a12p))\r\n (x_aZ8 :: Sing r_a12q) >\r\n case x_aZ8\r\n `cast` ((Sing\r\n (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R ; D:R:SingV1z0[0]\r\n <x_a12p>_N <r_a12q>_N\r\n :: (Sing r_a12q :: *) ~R# (R:SingV1z x_a12p r_a12q :: *))\r\n of nt_s13T {\r\n }\r\n}}}\r\n\r\nGHC 8.0.2 does not appear to suffer from this Core Lint error.","type_of_failure":"OtherFailure","blocking":[]} >The following program gives a Core Lint error on GHC 8.2.2 and later:
```hs
{# LANGUAGE EmptyCase #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
import Data.Void
data family Sing (a :: k)
data V1 :: Type > Type
data instance Sing (z :: V1 p)
class Generic a where
type Rep a :: Type > Type
to :: Rep a x > a
class PGeneric a where
type To (z :: Rep a x) :: a
class SGeneric a where
sTo :: forall x (r :: Rep a x). Sing r > Sing (To r :: a)

instance Generic Void where
type Rep Void = V1
to x = case x of {}
type family EmptyCase (a :: j) :: k where
instance PGeneric Void where
type To x = EmptyCase x
instance SGeneric Void where
sTo x = case x of
```
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs dcorelint fforcerecomp
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
Bug.hs:38:7: warning:
[in body of lambda with binder x_aZ8 :: Sing r_a12q]
Kind application error in
coercion ‘(Sing (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R’
Function kind = forall k. k > *
Arg kinds = [(V1 x_a12p, *), (r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
Bug.hs:38:7: warning:
[in body of lambda with binder x_aZ8 :: Sing r_a12q]
Kind application error in
coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’
Function kind = V1 x_a12p > *
Arg kinds = [(r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
Bug.hs:38:7: warning:
[in body of lambda with binder x_aZ8 :: Sing r_a12q]
Kind application error in
coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’
Function kind = V1 x_a12p > *
Arg kinds = [(r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
<no location info>: warning:
In the type ‘R:SingV1z x_a12p r_a12q’
Kind application error in type ‘R:SingV1z x_a12p r_a12q’
Function kind = forall p > V1 p > *
Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
<no location info>: warning:
In the type ‘R:SingV1z x_a12p r_a12q’
Kind application error in type ‘R:SingV1z x_a12p r_a12q’
Function kind = forall p > V1 p > *
Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]
Fun: V1 x_a12p
(r_a12q, Rep Void x_a12p)
*** Offending Program ***
<elided>
$csTo_a12n :: forall x (r :: Rep Void x). Sing r > Sing (To r)
[LclId,
Arity=1,
Str=<L,U>x,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]
$csTo_a12n
= \ (@ x_a12p)
(@ (r_a12q :: Rep Void x_a12p))
(x_aZ8 :: Sing r_a12q) >
case x_aZ8
`cast` ((Sing
(D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R ; D:R:SingV1z0[0]
<x_a12p>_N <r_a12q>_N
:: (Sing r_a12q :: *) ~R# (R:SingV1z x_a12p r_a12q :: *))
of nt_s13T {
}
```
GHC 8.0.2 does not appear to suffer from this Core Lint error.
<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":"Core Lint error with empty closed type family","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 gives a Core Lint error on GHC 8.2.2 and later:\r\n\r\n{{{#!hs\r\n{# LANGUAGE EmptyCase #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Void\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata V1 :: Type > Type\r\ndata instance Sing (z :: V1 p)\r\n\r\nclass Generic a where\r\n type Rep a :: Type > Type\r\n to :: Rep a x > a\r\n\r\nclass PGeneric a where\r\n type To (z :: Rep a x) :: a\r\n\r\nclass SGeneric a where\r\n sTo :: forall x (r :: Rep a x). Sing r > Sing (To r :: a)\r\n\r\n\r\n\r\ninstance Generic Void where\r\n type Rep Void = V1\r\n to x = case x of {}\r\n\r\ntype family EmptyCase (a :: j) :: k where\r\n\r\ninstance PGeneric Void where\r\n type To x = EmptyCase x\r\n\r\ninstance SGeneric Void where\r\n sTo x = case x of\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs dcorelint fforcerecomp \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n*** Core Lint errors : in result of Simplifier ***\r\nBug.hs:38:7: warning:\r\n [in body of lambda with binder x_aZ8 :: Sing r_a12q]\r\n Kind application error in\r\n coercion ‘(Sing (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R’\r\n Function kind = forall k. k > *\r\n Arg kinds = [(V1 x_a12p, *), (r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\nBug.hs:38:7: warning:\r\n [in body of lambda with binder x_aZ8 :: Sing r_a12q]\r\n Kind application error in\r\n coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’\r\n Function kind = V1 x_a12p > *\r\n Arg kinds = [(r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\nBug.hs:38:7: warning:\r\n [in body of lambda with binder x_aZ8 :: Sing r_a12q]\r\n Kind application error in\r\n coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’\r\n Function kind = V1 x_a12p > *\r\n Arg kinds = [(r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\n<no location info>: warning:\r\n In the type ‘R:SingV1z x_a12p r_a12q’\r\n Kind application error in type ‘R:SingV1z x_a12p r_a12q’\r\n Function kind = forall p > V1 p > *\r\n Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\n<no location info>: warning:\r\n In the type ‘R:SingV1z x_a12p r_a12q’\r\n Kind application error in type ‘R:SingV1z x_a12p r_a12q’\r\n Function kind = forall p > V1 p > *\r\n Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)]\r\n Fun: V1 x_a12p\r\n (r_a12q, Rep Void x_a12p)\r\n*** Offending Program ***\r\n\r\n<elided>\r\n\r\n$csTo_a12n :: forall x (r :: Rep Void x). Sing r > Sing (To r)\r\n[LclId,\r\n Arity=1,\r\n Str=<L,U>x,\r\n Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,\r\n WorkFree=True, Expandable=True,\r\n Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]\r\n$csTo_a12n\r\n = \\ (@ x_a12p)\r\n (@ (r_a12q :: Rep Void x_a12p))\r\n (x_aZ8 :: Sing r_a12q) >\r\n case x_aZ8\r\n `cast` ((Sing\r\n (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R ; D:R:SingV1z0[0]\r\n <x_a12p>_N <r_a12q>_N\r\n :: (Sing r_a12q :: *) ~R# (R:SingV1z x_a12p r_a12q :: *))\r\n of nt_s13T {\r\n }\r\n}}}\r\n\r\nGHC 8.0.2 does not appear to suffer from this Core Lint error.","type_of_failure":"OtherFailure","blocking":[]} >8.8.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/15515Bogus "No instance" error when type families appear in kinds20190707T18:04:23ZRyan ScottBogus "No instance" error when type families appear in kindsThe following code typechecks:
```hs
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
import Data.Proxy
class C a where
c :: Proxy a
type family F
data D :: F > Type
instance C (D :: F > Type) where
c = undefined
```
However, if we try to actually //use// that `C D` instance, like so:
```hs
c' :: Proxy (D :: F > Type)
c' = c @(D :: F > Type)
```
Then GHC gives a rather flummoxing error message:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:20:6: error:
• No instance for (C D) arising from a use of ‘c’
• In the expression: c @(D :: F > Type)
In an equation for ‘c'’: c' = c @(D :: F > Type)

20  c' = c @(D :: F > Type)
 ^^^^^^^^^^^^^^^^^^^
```
But that error is clearly misleading, as we defined such a `C D` instance directly above it!
The use of the type family `F` in the kind of `D` appears to play an important role in this bug. If I change `F` to be a data type (e.g., `data F`), then `c'` is accepted.
<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":"Bogus \"No instance\" error when type families appear in kinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code typechecks:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\nclass C a where\r\n c :: Proxy a\r\n\r\ntype family F\r\n\r\ndata D :: F > Type\r\n\r\ninstance C (D :: F > Type) where\r\n c = undefined\r\n}}}\r\n\r\nHowever, if we try to actually //use// that `C D` instance, like so:\r\n\r\n{{{#!hs\r\nc' :: Proxy (D :: F > Type)\r\nc' = c @(D :: F > Type)\r\n}}}\r\n\r\nThen GHC gives a rather flummoxing 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:20:6: error:\r\n • No instance for (C D) arising from a use of ‘c’\r\n • In the expression: c @(D :: F > Type)\r\n In an equation for ‘c'’: c' = c @(D :: F > Type)\r\n \r\n20  c' = c @(D :: F > Type)\r\n  ^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nBut that error is clearly misleading, as we defined such a `C D` instance directly above it!\r\n\r\nThe use of the type family `F` in the kind of `D` appears to play an important role in this bug. If I change `F` to be a data type (e.g., `data F`), then `c'` is accepted.","type_of_failure":"OtherFailure","blocking":[]} >The following code typechecks:
```hs
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
import Data.Proxy
class C a where
c :: Proxy a
type family F
data D :: F > Type
instance C (D :: F > Type) where
c = undefined
```
However, if we try to actually //use// that `C D` instance, like so:
```hs
c' :: Proxy (D :: F > Type)
c' = c @(D :: F > Type)
```
Then GHC gives a rather flummoxing error message:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:20:6: error:
• No instance for (C D) arising from a use of ‘c’
• In the expression: c @(D :: F > Type)
In an equation for ‘c'’: c' = c @(D :: F > Type)

20  c' = c @(D :: F > Type)
 ^^^^^^^^^^^^^^^^^^^
```
But that error is clearly misleading, as we defined such a `C D` instance directly above it!
The use of the type family `F` in the kind of `D` appears to play an important role in this bug. If I change `F` to be a data type (e.g., `data F`), then `c'` is accepted.
<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":"Bogus \"No instance\" error when type families appear in kinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code typechecks:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\nclass C a where\r\n c :: Proxy a\r\n\r\ntype family F\r\n\r\ndata D :: F > Type\r\n\r\ninstance C (D :: F > Type) where\r\n c = undefined\r\n}}}\r\n\r\nHowever, if we try to actually //use// that `C D` instance, like so:\r\n\r\n{{{#!hs\r\nc' :: Proxy (D :: F > Type)\r\nc' = c @(D :: F > Type)\r\n}}}\r\n\r\nThen GHC gives a rather flummoxing 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:20:6: error:\r\n • No instance for (C D) arising from a use of ‘c’\r\n • In the expression: c @(D :: F > Type)\r\n In an equation for ‘c'’: c' = c @(D :: F > Type)\r\n \r\n20  c' = c @(D :: F > Type)\r\n  ^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nBut that error is clearly misleading, as we defined such a `C D` instance directly above it!\r\n\r\nThe use of the type family `F` in the kind of `D` appears to play an important role in this bug. If I change `F` to be a data type (e.g., `data F`), then `c'` is accepted.","type_of_failure":"OtherFailure","blocking":[]} >8.8.1https://gitlab.haskell.org/ghc/ghc//issues/15497Coercion Quantification20190707T18:04:29ZNingning XieCoercion QuantificationAs described in [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2](https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2).
We would like to have coercion quantifications back in Haskell Core language.
This means in Core we can define types like
```hs
\/ (a: k1) .
\/ (co : k1 ~ k2)  an explicit quantification for the coercion
> (a > co)  use the name for an explicit cast
> ...
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Coercion Quantification","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"As described in [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2].\r\n\r\nWe would like to have coercion quantifications back in Haskell Core language.\r\n\r\nThis means in Core we can define types like\r\n\r\n{{{#!hs\r\n\\/ (a: k1) . \r\n \\/ (co : k1 ~ k2)  an explicit quantification for the coercion\r\n > (a > co)  use the name for an explicit cast\r\n > ...\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >As described in [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2](https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2).
We would like to have coercion quantifications back in Haskell Core language.
This means in Core we can define types like
```hs
\/ (a: k1) .
\/ (co : k1 ~ k2)  an explicit quantification for the coercion
> (a > co)  use the name for an explicit cast
> ...
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Coercion Quantification","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"As described in [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2].\r\n\r\nWe would like to have coercion quantifications back in Haskell Core language.\r\n\r\nThis means in Core we can define types like\r\n\r\n{{{#!hs\r\n\\/ (a: k1) . \r\n \\/ (co : k1 ~ k2)  an explicit quantification for the coercion\r\n > (a > co)  use the name for an explicit cast\r\n > ...\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >Ningning XieNingning Xiehttps://gitlab.haskell.org/ghc/ghc//issues/15474Error message mentions Any20210111T13:19:08ZKrzysztof GogolewskiError message mentions AnyI'm not sure if this is a bug. File:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
module T15474 where
import Data.Kind (Type)
data Proxy a
type Forall = forall t. Proxy t
f1 :: forall (t :: Type). Proxy t
f1 = f1
f2 :: Forall
f2 = f1
```
gives an error message mentioning Any:
```
• Couldn't match type ‘GHC.Types.Any’ with ‘*’
Expected type: Proxy t
Actual type: Proxy t0
```
The appearance of Any is suspicious to me  I thought it's an implementation detail?I'm not sure if this is a bug. File:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
module T15474 where
import Data.Kind (Type)
data Proxy a
type Forall = forall t. Proxy t
f1 :: forall (t :: Type). Proxy t
f1 = f1
f2 :: Forall
f2 = f1
```
gives an error message mentioning Any:
```
• Couldn't match type ‘GHC.Types.Any’ with ‘*’
Expected type: Proxy t
Actual type: Proxy t0
```
The appearance of Any is suspicious to me  I thought it's an implementation detail?9.0.1https://gitlab.haskell.org/ghc/ghc//issues/15472GHC HEAD type inference regression post"Remove decideKindGeneralisationPlan"20190707T18:04:35ZRyan ScottGHC HEAD type inference regression post"Remove decideKindGeneralisationPlan"Commit c955a514f033a12f6d0ab0fbacec3e18a5757ab5 (`Remove decideKindGeneralisationPlan`) causes the `singletons` library to no longer compile. Here is as minimal of an example as I can muster:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
module Bug (sPermutations) where
import Data.Kind
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing :: forall k. k > Type
data instance Sing :: forall a. [a] > Type where
SNil :: Sing '[]
SCons :: Sing x > Sing xs > Sing (x:xs)
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }
type SingFunction1 f = forall t. Sing t > Sing (Apply f t)
singFun1 :: forall f. SingFunction1 f > Sing f
singFun1 f = SLambda f
type SingFunction2 f = forall t. Sing t > SingFunction1 (Apply f t)
singFun2 :: forall f. SingFunction2 f > Sing f
singFun2 f = SLambda (\x > singFun1 (f x))
type family Undefined :: k where {}
sUndefined :: a
sUndefined = undefined
type family LetGo k z x ys where
LetGo k z x '[] = z
LetGo k z x (y ': ys) = Apply (Apply k y) (LetGo k z x ys)
type family Foldr (k :: a ~> b ~> b) (x :: b) (xs :: [a]) :: b where
Foldr k z x = LetGo k z x x
sFoldr :: forall (t1 :: a ~> b ~> b) (t2 :: b) (t3 :: [a]).
Sing t1 > Sing t2 > Sing t3
> Sing (Foldr t1 t2 t3 :: b)
sFoldr (sK :: Sing k) (sZ :: Sing z) (sX :: Sing x)
= let sGo :: forall arg. Sing arg > Sing (LetGo k z x arg)
sGo SNil = sZ
sGo (SCons (sY :: Sing y) (sYs :: Sing ys))
= sK `applySing` sY `applySing` sGo sYs
in sGo sX
type family LetInterleave xs0 t ts is (a1 :: [a]) (a2 :: [[a]]) :: [[a]] where
LetInterleave xs0 t ts is a1 a2 = Undefined a1 a2
data LetInterleaveSym5 l_ahko l_ahkp l_ahkq l_ahkr (l_ahks :: [a]) :: [[a]] ~> [[a]]
type instance Apply (LetInterleaveSym5 l_ahko l_ahkp l_ahkq l_ahkr l_ahks) l_ahkn = LetInterleave l_ahko l_ahkp l_ahkq l_ahkr l_ahks l_ahkn
data LetInterleaveSym4 l_ahkv l_ahkw l_ahkx l_ahky :: forall a. [a] ~> [[a]] ~> [[a]]
type instance Apply (LetInterleaveSym4 l_ahkv l_ahkw l_ahkx l_ahky) l_ahku = LetInterleaveSym5 l_ahkv l_ahkw l_ahkx l_ahky l_ahku
data LetInterleaveSym3 l_ahkB l_ahkC l_ahkD l_ahkA
type instance Apply (LetInterleaveSym3 l_ahkB l_ahkC l_ahkD) l_ahkA = LetInterleaveSym4 l_ahkB l_ahkC l_ahkD l_ahkA
data LetInterleaveSym2 l_ahkG l_ahkH l_ahkF
type instance Apply (LetInterleaveSym2 l_ahkG l_ahkH) l_ahkF = LetInterleaveSym3 l_ahkG l_ahkH l_ahkF
data LetInterleaveSym1 l_ahkK l_ahkJ
type instance Apply (LetInterleaveSym1 l_ahkK) l_ahkJ = LetInterleaveSym2 l_ahkK l_ahkJ
data LetInterleaveSym0 l_ahkM
type instance Apply LetInterleaveSym0 l_ahkM = LetInterleaveSym1 l_ahkM
type family LetPerms xs0 a1 a2 where
LetPerms xs0 '[] _ = '[]
LetPerms xs0 (t ': ts) is =
Foldr (LetInterleaveSym4 xs0 t ts is) (LetPerms xs0 ts (t ': is)) (Permutations is)
{
$(singletons [d
permutations :: forall a. [a] > [[a]]
permutations xs0 = xs0 : perms xs0 []
where
perms [] _ = []
perms (t:ts) is = foldr interleave (perms ts (t:is)) (permutations is)
where
interleave :: [a] > [[a]] > [[a]]
interleave = undefined
])
}
type family Permutations (xs0 :: [a]) :: [[a]] where
Permutations xs0 = xs0 ': LetPerms xs0 xs0 '[]
sPermutations :: forall (t1 :: [a]).
Sing t1 > Sing (Permutations t1 :: [[a]])
sPermutations (sXs0 :: Sing xs0)
= let sPerms :: forall arg1 arg2.
Sing arg1 > Sing arg2
> Sing (LetPerms xs0 arg1 arg2)
sPerms SNil _ = SNil
sPerms (SCons (sT :: Sing t) (sTs :: Sing ts)) (sIs :: Sing is)
= let sInterleave :: forall (t2 :: [a]) (t3 :: [[a]]).
Sing t2 > Sing t3
> Sing (LetInterleave xs0 t ts is t2 t3 :: [[a]])
sInterleave (sA1 :: Sing a1) (sA2 :: Sing a2)
= sUndefined sA1 sA2
in sFoldr (singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)
(sPerms sTs (sT `SCons` sIs))
(sPermutations sIs)
in sXs0 `SCons` sPerms sXs0 SNil
```
After that commit, this program (which previously typechecked) now errors with:
```
$ ~/Software/ghc4/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:105:66: error:
• Could not deduce: t2 ~~ t30
from the context: arg1 ~ (x : xs)
bound by a pattern with constructor:
SCons :: forall a (x :: a) (xs :: [a]).
Sing x > Sing xs > Sing (x : xs),
in an equation for ‘sPerms’
at Bug.hs:99:1753
‘t2’ is a rigid type variable bound by
a type expected by the context:
SingFunction2 (LetInterleaveSym4 t1 x xs arg2)
at Bug.hs:105:2476
Expected type: Sing t
> Sing t2
> Sing (Apply (Apply (LetInterleaveSym4 t1 x xs arg2) t) t2)
Actual type: Sing t20
> Sing t30 > Sing (LetInterleave t1 x xs arg2 t20 t30)
• In the second argument of ‘singFun2’, namely ‘sInterleave’
In the first argument of ‘sFoldr’, namely
‘(singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)’
In the expression:
sFoldr
(singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)
(sPerms sTs (sT `SCons` sIs))
(sPermutations sIs)
• Relevant bindings include
sInterleave :: forall (t2 :: [a1]) (t3 :: [[a1]]).
Sing t2 > Sing t3 > Sing (LetInterleave t1 x xs arg2 t2 t3)
(bound at Bug.hs:103:17)
sIs :: Sing arg2 (bound at Bug.hs:99:57)
sTs :: Sing xs (bound at Bug.hs:99:39)
sT :: Sing x (bound at Bug.hs:99:24)
sPerms :: Sing arg1 > Sing arg2 > Sing (LetPerms t1 arg1 arg2)
(bound at Bug.hs:98:9)
sXs0 :: Sing t1 (bound at Bug.hs:94:16)
(Some bindings suppressed; use fmaxrelevantbinds=N or fnomaxrelevantbinds)

105  in sFoldr (singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)
 ^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  highest 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  goldfire 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC HEAD type inference regression post\"Remove decideKindGeneralisationPlan\"","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"Commit c955a514f033a12f6d0ab0fbacec3e18a5757ab5 (`Remove decideKindGeneralisationPlan`) causes the `singletons` library to no longer compile. Here is as minimal of an example as I can muster:\r\n\r\n{{{#!hs\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\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug (sPermutations) where\r\n\r\nimport Data.Kind\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\ndata family Sing :: forall k. k > Type\r\ndata instance Sing :: forall a. [a] > Type where\r\n SNil :: Sing '[]\r\n SCons :: Sing x > Sing xs > Sing (x:xs)\r\n\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }\r\n\r\ntype SingFunction1 f = forall t. Sing t > Sing (Apply f t)\r\nsingFun1 :: forall f. SingFunction1 f > Sing f\r\nsingFun1 f = SLambda f\r\n\r\ntype SingFunction2 f = forall t. Sing t > SingFunction1 (Apply f t)\r\nsingFun2 :: forall f. SingFunction2 f > Sing f\r\nsingFun2 f = SLambda (\\x > singFun1 (f x))\r\n\r\ntype family Undefined :: k where {}\r\n\r\nsUndefined :: a\r\nsUndefined = undefined\r\n\r\ntype family LetGo k z x ys where\r\n LetGo k z x '[] = z\r\n LetGo k z x (y ': ys) = Apply (Apply k y) (LetGo k z x ys)\r\n\r\ntype family Foldr (k :: a ~> b ~> b) (x :: b) (xs :: [a]) :: b where\r\n Foldr k z x = LetGo k z x x\r\n\r\nsFoldr :: forall (t1 :: a ~> b ~> b) (t2 :: b) (t3 :: [a]).\r\n Sing t1 > Sing t2 > Sing t3\r\n > Sing (Foldr t1 t2 t3 :: b)\r\nsFoldr (sK :: Sing k) (sZ :: Sing z) (sX :: Sing x)\r\n = let sGo :: forall arg. Sing arg > Sing (LetGo k z x arg)\r\n sGo SNil = sZ\r\n sGo (SCons (sY :: Sing y) (sYs :: Sing ys))\r\n = sK `applySing` sY `applySing` sGo sYs\r\n in sGo sX\r\n\r\ntype family LetInterleave xs0 t ts is (a1 :: [a]) (a2 :: [[a]]) :: [[a]] where\r\n LetInterleave xs0 t ts is a1 a2 = Undefined a1 a2\r\ndata LetInterleaveSym5 l_ahko l_ahkp l_ahkq l_ahkr (l_ahks :: [a]) :: [[a]] ~> [[a]]\r\ntype instance Apply (LetInterleaveSym5 l_ahko l_ahkp l_ahkq l_ahkr l_ahks) l_ahkn = LetInterleave l_ahko l_ahkp l_ahkq l_ahkr l_ahks l_ahkn\r\ndata LetInterleaveSym4 l_ahkv l_ahkw l_ahkx l_ahky :: forall a. [a] ~> [[a]] ~> [[a]]\r\ntype instance Apply (LetInterleaveSym4 l_ahkv l_ahkw l_ahkx l_ahky) l_ahku = LetInterleaveSym5 l_ahkv l_ahkw l_ahkx l_ahky l_ahku\r\ndata LetInterleaveSym3 l_ahkB l_ahkC l_ahkD l_ahkA\r\ntype instance Apply (LetInterleaveSym3 l_ahkB l_ahkC l_ahkD) l_ahkA = LetInterleaveSym4 l_ahkB l_ahkC l_ahkD l_ahkA\r\ndata LetInterleaveSym2 l_ahkG l_ahkH l_ahkF\r\ntype instance Apply (LetInterleaveSym2 l_ahkG l_ahkH) l_ahkF = LetInterleaveSym3 l_ahkG l_ahkH l_ahkF\r\ndata LetInterleaveSym1 l_ahkK l_ahkJ\r\ntype instance Apply (LetInterleaveSym1 l_ahkK) l_ahkJ = LetInterleaveSym2 l_ahkK l_ahkJ\r\ndata LetInterleaveSym0 l_ahkM\r\ntype instance Apply LetInterleaveSym0 l_ahkM = LetInterleaveSym1 l_ahkM\r\n\r\ntype family LetPerms xs0 a1 a2 where\r\n LetPerms xs0 '[] _ = '[]\r\n LetPerms xs0 (t ': ts) is =\r\n Foldr (LetInterleaveSym4 xs0 t ts is) (LetPerms xs0 ts (t ': is)) (Permutations is)\r\n\r\n{\r\n$(singletons [d\r\n permutations :: forall a. [a] > [[a]]\r\n permutations xs0 = xs0 : perms xs0 []\r\n where\r\n perms [] _ = []\r\n perms (t:ts) is = foldr interleave (perms ts (t:is)) (permutations is)\r\n where\r\n interleave :: [a] > [[a]] > [[a]]\r\n interleave = undefined\r\n ])\r\n}\r\n\r\ntype family Permutations (xs0 :: [a]) :: [[a]] where\r\n Permutations xs0 = xs0 ': LetPerms xs0 xs0 '[]\r\n\r\nsPermutations :: forall (t1 :: [a]).\r\n Sing t1 > Sing (Permutations t1 :: [[a]])\r\nsPermutations (sXs0 :: Sing xs0)\r\n = let sPerms :: forall arg1 arg2.\r\n Sing arg1 > Sing arg2\r\n > Sing (LetPerms xs0 arg1 arg2)\r\n sPerms SNil _ = SNil\r\n sPerms (SCons (sT :: Sing t) (sTs :: Sing ts)) (sIs :: Sing is)\r\n = let sInterleave :: forall (t2 :: [a]) (t3 :: [[a]]).\r\n Sing t2 > Sing t3\r\n > Sing (LetInterleave xs0 t ts is t2 t3 :: [[a]])\r\n sInterleave (sA1 :: Sing a1) (sA2 :: Sing a2)\r\n = sUndefined sA1 sA2\r\n in sFoldr (singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)\r\n (sPerms sTs (sT `SCons` sIs))\r\n (sPermutations sIs)\r\n in sXs0 `SCons` sPerms sXs0 SNil\r\n}}}\r\n\r\nAfter that commit, this program (which previously typechecked) now errors with:\r\n\r\n{{{\r\n$ ~/Software/ghc4/inplace/bin/ghcstage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:105:66: error:\r\n • Could not deduce: t2 ~~ t30\r\n from the context: arg1 ~ (x : xs)\r\n bound by a pattern with constructor:\r\n SCons :: forall a (x :: a) (xs :: [a]).\r\n Sing x > Sing xs > Sing (x : xs),\r\n in an equation for ‘sPerms’\r\n at Bug.hs:99:1753\r\n ‘t2’ is a rigid type variable bound by\r\n a type expected by the context:\r\n SingFunction2 (LetInterleaveSym4 t1 x xs arg2)\r\n at Bug.hs:105:2476\r\n Expected type: Sing t\r\n > Sing t2\r\n > Sing (Apply (Apply (LetInterleaveSym4 t1 x xs arg2) t) t2)\r\n Actual type: Sing t20\r\n > Sing t30 > Sing (LetInterleave t1 x xs arg2 t20 t30)\r\n • In the second argument of ‘singFun2’, namely ‘sInterleave’\r\n In the first argument of ‘sFoldr’, namely\r\n ‘(singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)’\r\n In the expression:\r\n sFoldr\r\n (singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)\r\n (sPerms sTs (sT `SCons` sIs))\r\n (sPermutations sIs)\r\n • Relevant bindings include\r\n sInterleave :: forall (t2 :: [a1]) (t3 :: [[a1]]).\r\n Sing t2 > Sing t3 > Sing (LetInterleave t1 x xs arg2 t2 t3)\r\n (bound at Bug.hs:103:17)\r\n sIs :: Sing arg2 (bound at Bug.hs:99:57)\r\n sTs :: Sing xs (bound at Bug.hs:99:39)\r\n sT :: Sing x (bound at Bug.hs:99:24)\r\n sPerms :: Sing arg1 > Sing arg2 > Sing (LetPerms t1 arg1 arg2)\r\n (bound at Bug.hs:98:9)\r\n sXs0 :: Sing t1 (bound at Bug.hs:94:16)\r\n (Some bindings suppressed; use fmaxrelevantbinds=N or fnomaxrelevantbinds)\r\n \r\n105  in sFoldr (singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)\r\n  ^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >Commit c955a514f033a12f6d0ab0fbacec3e18a5757ab5 (`Remove decideKindGeneralisationPlan`) causes the `singletons` library to no longer compile. Here is as minimal of an example as I can muster:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
module Bug (sPermutations) where
import Data.Kind
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing :: forall k. k > Type
data instance Sing :: forall a. [a] > Type where
SNil :: Sing '[]
SCons :: Sing x > Sing xs > Sing (x:xs)
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }
type SingFunction1 f = forall t. Sing t > Sing (Apply f t)
singFun1 :: forall f. SingFunction1 f > Sing f
singFun1 f = SLambda f
type SingFunction2 f = forall t. Sing t > SingFunction1 (Apply f t)
singFun2 :: forall f. SingFunction2 f > Sing f
singFun2 f = SLambda (\x > singFun1 (f x))
type family Undefined :: k where {}
sUndefined :: a
sUndefined = undefined
type family LetGo k z x ys where
LetGo k z x '[] = z
LetGo k z x (y ': ys) = Apply (Apply k y) (LetGo k z x ys)
type family Foldr (k :: a ~> b ~> b) (x :: b) (xs :: [a]) :: b where
Foldr k z x = LetGo k z x x
sFoldr :: forall (t1 :: a ~> b ~> b) (t2 :: b) (t3 :: [a]).
Sing t1 > Sing t2 > Sing t3
> Sing (Foldr t1 t2 t3 :: b)
sFoldr (sK :: Sing k) (sZ :: Sing z) (sX :: Sing x)
= let sGo :: forall arg. Sing arg > Sing (LetGo k z x arg)
sGo SNil = sZ
sGo (SCons (sY :: Sing y) (sYs :: Sing ys))
= sK `applySing` sY `applySing` sGo sYs
in sGo sX
type family LetInterleave xs0 t ts is (a1 :: [a]) (a2 :: [[a]]) :: [[a]] where
LetInterleave xs0 t ts is a1 a2 = Undefined a1 a2
data LetInterleaveSym5 l_ahko l_ahkp l_ahkq l_ahkr (l_ahks :: [a]) :: [[a]] ~> [[a]]
type instance Apply (LetInterleaveSym5 l_ahko l_ahkp l_ahkq l_ahkr l_ahks) l_ahkn = LetInterleave l_ahko l_ahkp l_ahkq l_ahkr l_ahks l_ahkn
data LetInterleaveSym4 l_ahkv l_ahkw l_ahkx l_ahky :: forall a. [a] ~> [[a]] ~> [[a]]
type instance Apply (LetInterleaveSym4 l_ahkv l_ahkw l_ahkx l_ahky) l_ahku = LetInterleaveSym5 l_ahkv l_ahkw l_ahkx l_ahky l_ahku
data LetInterleaveSym3 l_ahkB l_ahkC l_ahkD l_ahkA
type instance Apply (LetInterleaveSym3 l_ahkB l_ahkC l_ahkD) l_ahkA = LetInterleaveSym4 l_ahkB l_ahkC l_ahkD l_ahkA
data LetInterleaveSym2 l_ahkG l_ahkH l_ahkF
type instance Apply (LetInterleaveSym2 l_ahkG l_ahkH) l_ahkF = LetInterleaveSym3 l_ahkG l_ahkH l_ahkF
data LetInterleaveSym1 l_ahkK l_ahkJ
type instance Apply (LetInterleaveSym1 l_ahkK) l_ahkJ = LetInterleaveSym2 l_ahkK l_ahkJ
data LetInterleaveSym0 l_ahkM
type instance Apply LetInterleaveSym0 l_ahkM = LetInterleaveSym1 l_ahkM
type family LetPerms xs0 a1 a2 where
LetPerms xs0 '[] _ = '[]
LetPerms xs0 (t ': ts) is =
Foldr (LetInterleaveSym4 xs0 t ts is) (LetPerms xs0 ts (t ': is)) (Permutations is)
{
$(singletons [d
permutations :: forall a. [a] > [[a]]
permutations xs0 = xs0 : perms xs0 []
where
perms [] _ = []
perms (t:ts) is = foldr interleave (perms ts (t:is)) (permutations is)
where
interleave :: [a] > [[a]] > [[a]]
interleave = undefined
])
}
type family Permutations (xs0 :: [a]) :: [[a]] where
Permutations xs0 = xs0 ': LetPerms xs0 xs0 '[]
sPermutations :: forall (t1 :: [a]).
Sing t1 > Sing (Permutations t1 :: [[a]])
sPermutations (sXs0 :: Sing xs0)
= let sPerms :: forall arg1 arg2.
Sing arg1 > Sing arg2
> Sing (LetPerms xs0 arg1 arg2)
sPerms SNil _ = SNil
sPerms (SCons (sT :: Sing t) (sTs :: Sing ts)) (sIs :: Sing is)
= let sInterleave :: forall (t2 :: [a]) (t3 :: [[a]]).
Sing t2 > Sing t3
> Sing (LetInterleave xs0 t ts is t2 t3 :: [[a]])
sInterleave (sA1 :: Sing a1) (sA2 :: Sing a2)
= sUndefined sA1 sA2
in sFoldr (singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)
(sPerms sTs (sT `SCons` sIs))
(sPermutations sIs)
in sXs0 `SCons` sPerms sXs0 SNil
```
After that commit, this program (which previously typechecked) now errors with:
```
$ ~/Software/ghc4/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:105:66: error:
• Could not deduce: t2 ~~ t30
from the context: arg1 ~ (x : xs)
bound by a pattern with constructor:
SCons :: forall a (x :: a) (xs :: [a]).
Sing x > Sing xs > Sing (x : xs),
in an equation for ‘sPerms’
at Bug.hs:99:1753
‘t2’ is a rigid type variable bound by
a type expected by the context:
SingFunction2 (LetInterleaveSym4 t1 x xs arg2)
at Bug.hs:105:2476
Expected type: Sing t
> Sing t2
> Sing (Apply (Apply (LetInterleaveSym4 t1 x xs arg2) t) t2)
Actual type: Sing t20
> Sing t30 > Sing (LetInterleave t1 x xs arg2 t20 t30)
• In the second argument of ‘singFun2’, namely ‘sInterleave’
In the first argument of ‘sFoldr’, namely
‘(singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)’
In the expression:
sFoldr
(singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)
(sPerms sTs (sT `SCons` sIs))
(sPermutations sIs)
• Relevant bindings include
sInterleave :: forall (t2 :: [a1]) (t3 :: [[a1]]).
Sing t2 > Sing t3 > Sing (LetInterleave t1 x xs arg2 t2 t3)
(bound at Bug.hs:103:17)
sIs :: Sing arg2 (bound at Bug.hs:99:57)
sTs :: Sing xs (bound at Bug.hs:99:39)
sT :: Sing x (bound at Bug.hs:99:24)
sPerms :: Sing arg1 > Sing arg2 > Sing (LetPerms t1 arg1 arg2)
(bound at Bug.hs:98:9)
sXs0 :: Sing t1 (bound at Bug.hs:94:16)
(Some bindings suppressed; use fmaxrelevantbinds=N or fnomaxrelevantbinds)

105  in sFoldr (singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)
 ^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  highest 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  goldfire 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC HEAD type inference regression post\"Remove decideKindGeneralisationPlan\"","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"Commit c955a514f033a12f6d0ab0fbacec3e18a5757ab5 (`Remove decideKindGeneralisationPlan`) causes the `singletons` library to no longer compile. Here is as minimal of an example as I can muster:\r\n\r\n{{{#!hs\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\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug (sPermutations) where\r\n\r\nimport Data.Kind\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\ndata family Sing :: forall k. k > Type\r\ndata instance Sing :: forall a. [a] > Type where\r\n SNil :: Sing '[]\r\n SCons :: Sing x > Sing xs > Sing (x:xs)\r\n\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }\r\n\r\ntype SingFunction1 f = forall t. Sing t > Sing (Apply f t)\r\nsingFun1 :: forall f. SingFunction1 f > Sing f\r\nsingFun1 f = SLambda f\r\n\r\ntype SingFunction2 f = forall t. Sing t > SingFunction1 (Apply f t)\r\nsingFun2 :: forall f. SingFunction2 f > Sing f\r\nsingFun2 f = SLambda (\\x > singFun1 (f x))\r\n\r\ntype family Undefined :: k where {}\r\n\r\nsUndefined :: a\r\nsUndefined = undefined\r\n\r\ntype family LetGo k z x ys where\r\n LetGo k z x '[] = z\r\n LetGo k z x (y ': ys) = Apply (Apply k y) (LetGo k z x ys)\r\n\r\ntype family Foldr (k :: a ~> b ~> b) (x :: b) (xs :: [a]) :: b where\r\n Foldr k z x = LetGo k z x x\r\n\r\nsFoldr :: forall (t1 :: a ~> b ~> b) (t2 :: b) (t3 :: [a]).\r\n Sing t1 > Sing t2 > Sing t3\r\n > Sing (Foldr t1 t2 t3 :: b)\r\nsFoldr (sK :: Sing k) (sZ :: Sing z) (sX :: Sing x)\r\n = let sGo :: forall arg. Sing arg > Sing (LetGo k z x arg)\r\n sGo SNil = sZ\r\n sGo (SCons (sY :: Sing y) (sYs :: Sing ys))\r\n = sK `applySing` sY `applySing` sGo sYs\r\n in sGo sX\r\n\r\ntype family LetInterleave xs0 t ts is (a1 :: [a]) (a2 :: [[a]]) :: [[a]] where\r\n LetInterleave xs0 t ts is a1 a2 = Undefined a1 a2\r\ndata LetInterleaveSym5 l_ahko l_ahkp l_ahkq l_ahkr (l_ahks :: [a]) :: [[a]] ~> [[a]]\r\ntype instance Apply (LetInterleaveSym5 l_ahko l_ahkp l_ahkq l_ahkr l_ahks) l_ahkn = LetInterleave l_ahko l_ahkp l_ahkq l_ahkr l_ahks l_ahkn\r\ndata LetInterleaveSym4 l_ahkv l_ahkw l_ahkx l_ahky :: forall a. [a] ~> [[a]] ~> [[a]]\r\ntype instance Apply (LetInterleaveSym4 l_ahkv l_ahkw l_ahkx l_ahky) l_ahku = LetInterleaveSym5 l_ahkv l_ahkw l_ahkx l_ahky l_ahku\r\ndata LetInterleaveSym3 l_ahkB l_ahkC l_ahkD l_ahkA\r\ntype instance Apply (LetInterleaveSym3 l_ahkB l_ahkC l_ahkD) l_ahkA = LetInterleaveSym4 l_ahkB l_ahkC l_ahkD l_ahkA\r\ndata LetInterleaveSym2 l_ahkG l_ahkH l_ahkF\r\ntype instance Apply (LetInterleaveSym2 l_ahkG l_ahkH) l_ahkF = LetInterleaveSym3 l_ahkG l_ahkH l_ahkF\r\ndata LetInterleaveSym1 l_ahkK l_ahkJ\r\ntype instance Apply (LetInterleaveSym1 l_ahkK) l_ahkJ = LetInterleaveSym2 l_ahkK l_ahkJ\r\ndata LetInterleaveSym0 l_ahkM\r\ntype instance Apply LetInterleaveSym0 l_ahkM = LetInterleaveSym1 l_ahkM\r\n\r\ntype family LetPerms xs0 a1 a2 where\r\n LetPerms xs0 '[] _ = '[]\r\n LetPerms xs0 (t ': ts) is =\r\n Foldr (LetInterleaveSym4 xs0 t ts is) (LetPerms xs0 ts (t ': is)) (Permutations is)\r\n\r\n{\r\n$(singletons [d\r\n permutations :: forall a. [a] > [[a]]\r\n permutations xs0 = xs0 : perms xs0 []\r\n where\r\n perms [] _ = []\r\n perms (t:ts) is = foldr interleave (perms ts (t:is)) (permutations is)\r\n where\r\n interleave :: [a] > [[a]] > [[a]]\r\n interleave = undefined\r\n ])\r\n}\r\n\r\ntype family Permutations (xs0 :: [a]) :: [[a]] where\r\n Permutations xs0 = xs0 ': LetPerms xs0 xs0 '[]\r\n\r\nsPermutations :: forall (t1 :: [a]).\r\n Sing t1 > Sing (Permutations t1 :: [[a]])\r\nsPermutations (sXs0 :: Sing xs0)\r\n = let sPerms :: forall arg1 arg2.\r\n Sing arg1 > Sing arg2\r\n > Sing (LetPerms xs0 arg1 arg2)\r\n sPerms SNil _ = SNil\r\n sPerms (SCons (sT :: Sing t) (sTs :: Sing ts)) (sIs :: Sing is)\r\n = let sInterleave :: forall (t2 :: [a]) (t3 :: [[a]]).\r\n Sing t2 > Sing t3\r\n > Sing (LetInterleave xs0 t ts is t2 t3 :: [[a]])\r\n sInterleave (sA1 :: Sing a1) (sA2 :: Sing a2)\r\n = sUndefined sA1 sA2\r\n in sFoldr (singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)\r\n (sPerms sTs (sT `SCons` sIs))\r\n (sPermutations sIs)\r\n in sXs0 `SCons` sPerms sXs0 SNil\r\n}}}\r\n\r\nAfter that commit, this program (which previously typechecked) now errors with:\r\n\r\n{{{\r\n$ ~/Software/ghc4/inplace/bin/ghcstage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:105:66: error:\r\n • Could not deduce: t2 ~~ t30\r\n from the context: arg1 ~ (x : xs)\r\n bound by a pattern with constructor:\r\n SCons :: forall a (x :: a) (xs :: [a]).\r\n Sing x > Sing xs > Sing (x : xs),\r\n in an equation for ‘sPerms’\r\n at Bug.hs:99:1753\r\n ‘t2’ is a rigid type variable bound by\r\n a type expected by the context:\r\n SingFunction2 (LetInterleaveSym4 t1 x xs arg2)\r\n at Bug.hs:105:2476\r\n Expected type: Sing t\r\n > Sing t2\r\n > Sing (Apply (Apply (LetInterleaveSym4 t1 x xs arg2) t) t2)\r\n Actual type: Sing t20\r\n > Sing t30 > Sing (LetInterleave t1 x xs arg2 t20 t30)\r\n • In the second argument of ‘singFun2’, namely ‘sInterleave’\r\n In the first argument of ‘sFoldr’, namely\r\n ‘(singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)’\r\n In the expression:\r\n sFoldr\r\n (singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)\r\n (sPerms sTs (sT `SCons` sIs))\r\n (sPermutations sIs)\r\n • Relevant bindings include\r\n sInterleave :: forall (t2 :: [a1]) (t3 :: [[a1]]).\r\n Sing t2 > Sing t3 > Sing (LetInterleave t1 x xs arg2 t2 t3)\r\n (bound at Bug.hs:103:17)\r\n sIs :: Sing arg2 (bound at Bug.hs:99:57)\r\n sTs :: Sing xs (bound at Bug.hs:99:39)\r\n sT :: Sing x (bound at Bug.hs:99:24)\r\n sPerms :: Sing arg1 > Sing arg2 > Sing (LetPerms t1 arg1 arg2)\r\n (bound at Bug.hs:98:9)\r\n sXs0 :: Sing t1 (bound at Bug.hs:94:16)\r\n (Some bindings suppressed; use fmaxrelevantbinds=N or fnomaxrelevantbinds)\r\n \r\n105  in sFoldr (singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)\r\n  ^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.8.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/15419GHC 8.6.1 regression (buildKindCoercion)20190707T18:04:59ZRyan ScottGHC 8.6.1 regression (buildKindCoercion)The following program typechecks on GHC 8.4.1, but panics on GHC 8.6.1 and HEAD:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE DefaultSignatures #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE TypeInType #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
data family Sing :: forall k. k > Type
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data instance Sing :: forall a b. (a, b) > Type where
STuple2 :: Sing x > Sing y > Sing '(x, y)
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t > Sing (f `Apply` t) }

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

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

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

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

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

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

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

instance PFunctor ((,) a)
 The line below causes the panic
instance SFunctor ((,) a)
```
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.0.20180714 for x86_64unknownlinux):
buildKindCoercion
K1 a_a1Nj :*: Par1
Rep1 ((,) a_a1Nj)
*
a_a1Nj
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
pprPanic, called at compiler/types/Coercion.hs:2069:9 in ghc:Coercion
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  highest 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC 8.6.1 regression (buildKindCoercion)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program typechecks on GHC 8.4.1, but panics on GHC 8.6.1 and HEAD:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ConstraintKinds #}\r\n{# LANGUAGE DefaultSignatures #}\r\n{# LANGUAGE FlexibleContexts #}\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeOperators #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE UndecidableInstances #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing :: forall k. k > Type\r\ndata TyFun :: Type > Type > Type\r\ntype a ~> b = TyFun a b > Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\n\r\ndata instance Sing :: forall a b. (a, b) > Type where\r\n STuple2 :: Sing x > Sing y > Sing '(x, y)\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t > Sing (f `Apply` t) }\r\n\r\n\r\n\r\nnewtype Par1 p = Par1 p\r\nnewtype K1 c p = K1 c\r\ndata (f :*: g) p = f p :*: g p\r\n\r\ndata instance Sing :: forall p. Par1 p > Type where\r\n SPar1 :: Sing x > Sing ('Par1 x)\r\ndata instance Sing :: forall k c (p :: k). K1 c p > Type where\r\n SK1 :: Sing x > Sing ('K1 x)\r\ndata instance Sing :: forall k (f :: k > Type) (g :: k > Type) (p :: k).\r\n (f :*: g) p > Type where\r\n (:%*:) :: Sing x > Sing y > Sing (x ':*: y)\r\n\r\nclass Generic1 (f :: k > Type) where\r\n type Rep1 f :: k > Type\r\n from1 :: f a > Rep1 f a\r\n to1 :: Rep1 f a > f a\r\n\r\nclass PGeneric1 (f :: k > Type) where\r\n type From1 (z :: f a) :: Rep1 f a\r\n type To1 (z :: Rep1 f a) :: f a\r\n\r\nclass SGeneric1 (f :: k > Type) where\r\n sFrom1 :: forall (a :: k) (z :: f a). Sing z > Sing (From1 z)\r\n sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r > Sing (To1 r :: f a)\r\n\r\ninstance Generic1 ((,) a) where\r\n type Rep1 ((,) a) = K1 a :*: Par1\r\n from1 (x, y) = K1 x :*: Par1 y\r\n to1 (K1 x :*: Par1 y) = (x, y)\r\n\r\ninstance PGeneric1 ((,) a) where\r\n type From1 '(x, y) = 'K1 x ':*: 'Par1 y\r\n type To1 ('K1 x ':*: 'Par1 y) = '(x, y)\r\n\r\ninstance SGeneric1 ((,) a) where\r\n sFrom1 (STuple2 x y) = SK1 x :%*: SPar1 y\r\n sTo1 (SK1 x :%*: SPar1 y) = STuple2 x y\r\n\r\n\r\n\r\ntype family GenericFmap (g :: a ~> b) (x :: f a) :: f b where\r\n GenericFmap g x = To1 (Fmap g (From1 x))\r\n\r\nclass PFunctor (f :: Type > Type) where\r\n type Fmap (g :: a ~> b) (x :: f a) :: f b\r\n type Fmap g x = GenericFmap g x\r\n\r\nclass SFunctor (f :: Type > Type) where\r\n sFmap :: forall a b (g :: a ~> b) (x :: f a).\r\n Sing g > Sing x > Sing (Fmap g x)\r\n default sFmap :: forall a b (g :: a ~> b) (x :: f a).\r\n ( SGeneric1 f, SFunctor (Rep1 f)\r\n , Fmap g x ~ GenericFmap g x )\r\n => Sing g > Sing x > Sing (Fmap g x)\r\n sFmap sg sx = sTo1 (sFmap sg (sFrom1 sx))\r\n\r\n\r\n\r\ninstance PFunctor Par1 where\r\n type Fmap f ('Par1 x) = 'Par1 (f `Apply` x)\r\ninstance PFunctor (K1 c) where\r\n type Fmap _ ('K1 x) = 'K1 x\r\ninstance PFunctor (f :*: g) where\r\n type Fmap h (x ':*: y) = Fmap h x ':*: Fmap h y\r\n\r\ninstance SFunctor Par1 where\r\n sFmap sf (SPar1 sx) = SPar1 (sf `applySing` sx)\r\ninstance SFunctor (K1 c) where\r\n sFmap _ (SK1 sx) = SK1 sx\r\ninstance (SFunctor f, SFunctor g) => SFunctor (f :*: g) where\r\n sFmap sh (sx :%*: sy) = sFmap sh sx :%*: sFmap sh sy\r\n\r\n\r\n\r\ninstance PFunctor ((,) a)\r\n The line below causes the panic\r\ninstance SFunctor ((,) a)\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.0.20180714 for x86_64unknownlinux):\r\n buildKindCoercion\r\n K1 a_a1Nj :*: Par1\r\n Rep1 ((,) a_a1Nj)\r\n *\r\n a_a1Nj\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Coercion.hs:2069:9 in ghc:Coercion\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/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/15330Error message prints invisible kind arguments in a visible matter20190707T18:13:08ZRyan ScottError message prints invisible kind arguments in a visible matterConsider the following program:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
import Data.Proxy
data T :: forall a. a > Type
f1 :: Proxy (T True)
f1 = "foo"
f2 :: forall (t :: forall a. a > Type).
Proxy (t True)
f2 = "foo"
```
This program doesn't typecheck (for good reason). The error messages, however, are a bit iffy:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:6: error:
• Couldn't match expected type ‘Proxy (T 'True)’
with actual type ‘[Char]’
• In the expression: "foo"
In an equation for ‘f1’: f1 = "foo"

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

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

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

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

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

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

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

13  f = show
 ^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Error message prints explicit kinds when it shouldn't","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When compiled, this program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeInType #}\r\n{# OPTIONS_GHC fnoprintexplicitkinds #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata Foo (a :: Type) :: forall b. (a > b > Type) > Type where\r\n MkFoo :: Foo a f\r\n\r\nf :: Foo a f > String\r\nf = show\r\n}}}\r\n\r\nGives the following error:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:13:5: error:\r\n • No instance for (Show (Foo a b f)) arising from a use of ‘show’\r\n • In the expression: show\r\n In an equation for ‘f’: f = show\r\n \r\n13  f = show\r\n  ^^^^\r\n}}}\r\n\r\nThis error message is slightly incorrect, however. In \"`No instance for (Show (Foo a b f))`\", it claims that `Foo` has three visible type parameters, but it only has two. (I've even made sure to enable `fnoprintexplicitkinds` at the type to ensure that the invisible `b` kind shouldn't get printed, but it was anyway.)\r\n\r\nThis is a regression that was apparently introduced between GHC 8.0 and 8.2, since in GHC 8.0.2, it prints the correct thing:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:13:5: error:\r\n • No instance for (Show (Foo a f)) arising from a use of ‘show’\r\n • In the expression: show\r\n In an equation for ‘f’: f = show\r\n}}}\r\n\r\nBut it does not in GHC 8.2.1:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:13:5: error:\r\n • No instance for (Show (Foo a b f)) arising from a use of ‘show’\r\n • In the expression: show\r\n In an equation for ‘f’: f = show\r\n \r\n13  f = show\r\n  ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/15282Document how equalitybearing constructors are promoted in Core20190707T18:13:27ZRyan ScottDocument how equalitybearing constructors are promoted in CoreIn [D4728](https://phabricator.haskell.org/D4728), Simon was utterly baffled as to how one could promote the `MkT` constructor in:
```hs
data T a where
MkT :: (a ~ Int) => T a
```
Richard knows the inner machinations of how this works (including what coercions are used in the Core that `'MkT` desugars to), but not many others do. Simon requested that Richard document this knowledge in a Note somewhere. This ticket exists to keep track of this request.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  goldfire 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Document how equalitybearing constructors are promoted in Core","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"In Phab:D4728, Simon was utterly baffled as to how one could promote the `MkT` constructor in:\r\n\r\n{{{#!hs\r\ndata T a where\r\n MkT :: (a ~ Int) => T a\r\n}}}\r\n\r\nRichard knows the inner machinations of how this works (including what coercions are used in the Core that `'MkT` desugars to), but not many others do. Simon requested that Richard document this knowledge in a Note somewhere. This ticket exists to keep track of this request.","type_of_failure":"OtherFailure","blocking":[]} >In [D4728](https://phabricator.haskell.org/D4728), Simon was utterly baffled as to how one could promote the `MkT` constructor in:
```hs
data T a where
MkT :: (a ~ Int) => T a
```
Richard knows the inner machinations of how this works (including what coercions are used in the Core that `'MkT` desugars to), but not many others do. Simon requested that Richard document this knowledge in a Note somewhere. This ticket exists to keep track of this request.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  goldfire 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Document how equalitybearing constructors are promoted in Core","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"In Phab:D4728, Simon was utterly baffled as to how one could promote the `MkT` constructor in:\r\n\r\n{{{#!hs\r\ndata T a where\r\n MkT :: (a ~ Int) => T a\r\n}}}\r\n\r\nRichard knows the inner machinations of how this works (including what coercions are used in the Core that `'MkT` desugars to), but not many others do. Simon requested that Richard document this knowledge in a Note somewhere. This ticket exists to keep track of this request.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/15245Data family promotion is possible20190707T18:13:38ZVladislav ZavialovData family promotion is possibleThe User's Guide states that data families cannot be promoted, even with `XTypeInType`:
> We promote data types and newtypes; type synonyms and type/data families are not promoted.
>
> The flag TypeInType (which implies DataKinds) relaxes some of these restrictions, allowing:
>
> Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types.
And yet the following code typechecks and runs:
```hs
{# LANGUAGE TypeFamilies, TypeInType, TypeApplications #}
import Type.Reflection
data family K
data instance K = MkK
main = print (typeRep @'MkK)
```
Is this a GHC bug or a documentation bug? I asked in IRC but I'm still confused:
```
<intindex> The user guide states that data families aren't promoted even when XTypeInType is enabled. Where's the logic that ensures this? I checked with `data family K; data instance K = MkK` and I can use `'MkK` with no errors/warnings.
<intindex> https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#overview "Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types."
<intindex> Is this info outdated?
<RyanGlScott> intindex: Is this in GHCi?
<RyanGlScott> It certainly fails in GHC
<RyanGlScott> But I think I understand why the former works
<intindex> RyanGlScott, yes, I'm checking this in GHCi
<RyanGlScott> intindex: So here's my understanding of how this works
<RyanGlScott> GHC kindchecks toplevel declarations using a rather primitive SCC analysis
<RyanGlScott> In particular, it's primitive in the sense that data family instances give it a lot of trouble
<RyanGlScott> If you tried taking your code and putting it into a standalone .hs file and compiling that, then it would definitely complain about a promoted use of MkT
<RyanGlScott> As luck would have it, though, you were trying things out in GHCi
<RyanGlScott> Which essentially checks each line of input as its own strongly connected group of declarations
<RyanGlScott> So you can define MkT on one line and promote it in subsequent lines, since they're separate in the sense
<RyanGlScott> *that sense
<intindex> this sounds related to Trac #12088, and then I could work around it in GHC by using `$(return [])`, so data families are actually promoted anyway and this has nothing to do with GHC needing more powerful type theory
<RyanGlScott> Well, it does need more powerful type theory in the sense that that's a prerequisite for making the SCC analysis for kindchecking sophisticated enough to handle this
<RyanGlScott> But yes, it's quite simple to work around by using Template Haskell to explicitly split up groups.
<intindex> https://gist.github.com/intindex/c6cc1e20c4b9b5c99af40ee4e23ecb61 this works and no template haskell involved
<intindex> The reason I'm asking is that I'm touching this part of the User's Guide and I don't know what to write there.
<RyanGlScott> Huh, now that's interesting
<intindex> RyanGlScott, the only check I could find that controls what's promoted and what's not is 'isLegacyPromotableDataCon'  and enabling XTypeInType disables this check.
<RyanGlScott> intindex: Right, that's baffling me
<RyanGlScott> Since that's supposed to be checked every time you promote a data constructor (I think)
<RyanGlScott> intindex: File a bug about that, I suppose
<RyanGlScott> Richard (who's sitting next to me right now) seems to think that that shouldn't be possible
<intindex> RyanGlScott, the thing is, I happily removed this check completely in D4748. Does this mean I have to restore a weaker version of it that only checks for data families? Why?
<intindex> Is it bad that XDataKinds promotes data family constructors? Looks like I can just remove the "restrictions" part of the user guide and be done with it
<RyanGlScott> intindex: In theory, that shouldn't be possible
<intindex> OK, then what the check should be? No data families, any other restrictions?
<RyanGlScott> I might qualify that with "no data family instances defined in the same module"
<RyanGlScott> (Or to be precise, in the same SCC, but that's probably too technical for the users' guide)
<intindex> Well, this sounds hard to check. I was thinking along the lines of keeping the 'not (isFamInstTyCon (dataConTyCon dc))' part of the check...
<RyanGlScott> Oh, I thought you were only changing the users' guide :)
<intindex> Well, at this point I'm confused if I should change only the user guide or the check as well. If data families shouldn't be promoted ever, then I'll change GHC. If the limitation is about the current SCC group, I can just mention Trac #12088 as a known infelicity in the User's Guide
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Documentation 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  RyanGlScott, goldfire 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Data family promotion is possible","status":"New","operating_system":"","component":"Documentation","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["RyanGlScott","goldfire"],"type":"Bug","description":"The User's Guide states that data families cannot be promoted, even with `XTypeInType`:\r\n\r\n> We promote data types and newtypes; type synonyms and type/data families are not promoted.\r\n>\r\n> The flag TypeInType (which implies DataKinds) relaxes some of these restrictions, allowing:\r\n>\r\n> Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types.\r\n\r\nAnd yet the following code typechecks and runs:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies, TypeInType, TypeApplications #}\r\n\r\nimport Type.Reflection\r\n\r\ndata family K\r\ndata instance K = MkK\r\n\r\nmain = print (typeRep @'MkK)\r\n}}}\r\n\r\nIs this a GHC bug or a documentation bug? I asked in IRC but I'm still confused:\r\n\r\n{{{\r\n<intindex> The user guide states that data families aren't promoted even when XTypeInType is enabled. Where's the logic that ensures this? I checked with `data family K; data instance K = MkK` and I can use `'MkK` with no errors/warnings.\r\n<intindex> https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#overview \"Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types.\"\r\n<intindex> Is this info outdated?\r\n<RyanGlScott> intindex: Is this in GHCi?\r\n<RyanGlScott> It certainly fails in GHC\r\n<RyanGlScott> But I think I understand why the former works\r\n<intindex> RyanGlScott, yes, I'm checking this in GHCi\r\n<RyanGlScott> intindex: So here's my understanding of how this works\r\n<RyanGlScott> GHC kindchecks toplevel declarations using a rather primitive SCC analysis\r\n<RyanGlScott> In particular, it's primitive in the sense that data family instances give it a lot of trouble\r\n<RyanGlScott> If you tried taking your code and putting it into a standalone .hs file and compiling that, then it would definitely complain about a promoted use of MkT\r\n<RyanGlScott> As luck would have it, though, you were trying things out in GHCi\r\n<RyanGlScott> Which essentially checks each line of input as its own strongly connected group of declarations\r\n<RyanGlScott> So you can define MkT on one line and promote it in subsequent lines, since they're separate in the sense\r\n<RyanGlScott> *that sense\r\n<intindex> this sounds related to Trac #12088, and then I could work around it in GHC by using `$(return [])`, so data families are actually promoted anyway and this has nothing to do with GHC needing more powerful type theory\r\n<RyanGlScott> Well, it does need more powerful type theory in the sense that that's a prerequisite for making the SCC analysis for kindchecking sophisticated enough to handle this\r\n<RyanGlScott> But yes, it's quite simple to work around by using Template Haskell to explicitly split up groups.\r\n<intindex> https://gist.github.com/intindex/c6cc1e20c4b9b5c99af40ee4e23ecb61 this works and no template haskell involved\r\n<intindex> The reason I'm asking is that I'm touching this part of the User's Guide and I don't know what to write there.\r\n<RyanGlScott> Huh, now that's interesting\r\n<intindex> RyanGlScott, the only check I could find that controls what's promoted and what's not is 'isLegacyPromotableDataCon'  and enabling XTypeInType disables this check.\r\n<RyanGlScott> intindex: Right, that's baffling me\r\n<RyanGlScott> Since that's supposed to be checked every time you promote a data constructor (I think)\r\n<RyanGlScott> intindex: File a bug about that, I suppose\r\n<RyanGlScott> Richard (who's sitting next to me right now) seems to think that that shouldn't be possible\r\n<intindex> RyanGlScott, the thing is, I happily removed this check completely in D4748. Does this mean I have to restore a weaker version of it that only checks for data families? Why?\r\n<intindex> Is it bad that XDataKinds promotes data family constructors? Looks like I can just remove the \"restrictions\" part of the user guide and be done with it\r\n<RyanGlScott> intindex: In theory, that shouldn't be possible\r\n<intindex> OK, then what the check should be? No data families, any other restrictions?\r\n<RyanGlScott> I might qualify that with \"no data family instances defined in the same module\"\r\n<RyanGlScott> (Or to be precise, in the same SCC, but that's probably too technical for the users' guide)\r\n<intindex> Well, this sounds hard to check. I was thinking along the lines of keeping the 'not (isFamInstTyCon (dataConTyCon dc))' part of the check...\r\n<RyanGlScott> Oh, I thought you were only changing the users' guide :)\r\n<intindex> Well, at this point I'm confused if I should change only the user guide or the check as well. If data families shouldn't be promoted ever, then I'll change GHC. If the limitation is about the current SCC group, I can just mention Trac #12088 as a known infelicity in the User's Guide\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >The User's Guide states that data families cannot be promoted, even with `XTypeInType`:
> We promote data types and newtypes; type synonyms and type/data families are not promoted.
>
> The flag TypeInType (which implies DataKinds) relaxes some of these restrictions, allowing:
>
> Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types.
And yet the following code typechecks and runs:
```hs
{# LANGUAGE TypeFamilies, TypeInType, TypeApplications #}
import Type.Reflection
data family K
data instance K = MkK
main = print (typeRep @'MkK)
```
Is this a GHC bug or a documentation bug? I asked in IRC but I'm still confused:
```
<intindex> The user guide states that data families aren't promoted even when XTypeInType is enabled. Where's the logic that ensures this? I checked with `data family K; data instance K = MkK` and I can use `'MkK` with no errors/warnings.
<intindex> https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#overview "Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types."
<intindex> Is this info outdated?
<RyanGlScott> intindex: Is this in GHCi?
<RyanGlScott> It certainly fails in GHC
<RyanGlScott> But I think I understand why the former works
<intindex> RyanGlScott, yes, I'm checking this in GHCi
<RyanGlScott> intindex: So here's my understanding of how this works
<RyanGlScott> GHC kindchecks toplevel declarations using a rather primitive SCC analysis
<RyanGlScott> In particular, it's primitive in the sense that data family instances give it a lot of trouble
<RyanGlScott> If you tried taking your code and putting it into a standalone .hs file and compiling that, then it would definitely complain about a promoted use of MkT
<RyanGlScott> As luck would have it, though, you were trying things out in GHCi
<RyanGlScott> Which essentially checks each line of input as its own strongly connected group of declarations
<RyanGlScott> So you can define MkT on one line and promote it in subsequent lines, since they're separate in the sense
<RyanGlScott> *that sense
<intindex> this sounds related to Trac #12088, and then I could work around it in GHC by using `$(return [])`, so data families are actually promoted anyway and this has nothing to do with GHC needing more powerful type theory
<RyanGlScott> Well, it does need more powerful type theory in the sense that that's a prerequisite for making the SCC analysis for kindchecking sophisticated enough to handle this
<RyanGlScott> But yes, it's quite simple to work around by using Template Haskell to explicitly split up groups.
<intindex> https://gist.github.com/intindex/c6cc1e20c4b9b5c99af40ee4e23ecb61 this works and no template haskell involved
<intindex> The reason I'm asking is that I'm touching this part of the User's Guide and I don't know what to write there.
<RyanGlScott> Huh, now that's interesting
<intindex> RyanGlScott, the only check I could find that controls what's promoted and what's not is 'isLegacyPromotableDataCon'  and enabling XTypeInType disables this check.
<RyanGlScott> intindex: Right, that's baffling me
<RyanGlScott> Since that's supposed to be checked every time you promote a data constructor (I think)
<RyanGlScott> intindex: File a bug about that, I suppose
<RyanGlScott> Richard (who's sitting next to me right now) seems to think that that shouldn't be possible
<intindex> RyanGlScott, the thing is, I happily removed this check completely in D4748. Does this mean I have to restore a weaker version of it that only checks for data families? Why?
<intindex> Is it bad that XDataKinds promotes data family constructors? Looks like I can just remove the "restrictions" part of the user guide and be done with it
<RyanGlScott> intindex: In theory, that shouldn't be possible
<intindex> OK, then what the check should be? No data families, any other restrictions?
<RyanGlScott> I might qualify that with "no data family instances defined in the same module"
<RyanGlScott> (Or to be precise, in the same SCC, but that's probably too technical for the users' guide)
<intindex> Well, this sounds hard to check. I was thinking along the lines of keeping the 'not (isFamInstTyCon (dataConTyCon dc))' part of the check...
<RyanGlScott> Oh, I thought you were only changing the users' guide :)
<intindex> Well, at this point I'm confused if I should change only the user guide or the check as well. If data families shouldn't be promoted ever, then I'll change GHC. If the limitation is about the current SCC group, I can just mention Trac #12088 as a known infelicity in the User's Guide
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Documentation 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  RyanGlScott, goldfire 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Data family promotion is possible","status":"New","operating_system":"","component":"Documentation","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["RyanGlScott","goldfire"],"type":"Bug","description":"The User's Guide states that data families cannot be promoted, even with `XTypeInType`:\r\n\r\n> We promote data types and newtypes; type synonyms and type/data families are not promoted.\r\n>\r\n> The flag TypeInType (which implies DataKinds) relaxes some of these restrictions, allowing:\r\n>\r\n> Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types.\r\n\r\nAnd yet the following code typechecks and runs:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies, TypeInType, TypeApplications #}\r\n\r\nimport Type.Reflection\r\n\r\ndata family K\r\ndata instance K = MkK\r\n\r\nmain = print (typeRep @'MkK)\r\n}}}\r\n\r\nIs this a GHC bug or a documentation bug? I asked in IRC but I'm still confused:\r\n\r\n{{{\r\n<intindex> The user guide states that data families aren't promoted even when XTypeInType is enabled. Where's the logic that ensures this? I checked with `data family K; data instance K = MkK` and I can use `'MkK` with no errors/warnings.\r\n<intindex> https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#overview \"Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types.\"\r\n<intindex> Is this info outdated?\r\n<RyanGlScott> intindex: Is this in GHCi?\r\n<RyanGlScott> It certainly fails in GHC\r\n<RyanGlScott> But I think I understand why the former works\r\n<intindex> RyanGlScott, yes, I'm checking this in GHCi\r\n<RyanGlScott> intindex: So here's my understanding of how this works\r\n<RyanGlScott> GHC kindchecks toplevel declarations using a rather primitive SCC analysis\r\n<RyanGlScott> In particular, it's primitive in the sense that data family instances give it a lot of trouble\r\n<RyanGlScott> If you tried taking your code and putting it into a standalone .hs file and compiling that, then it would definitely complain about a promoted use of MkT\r\n<RyanGlScott> As luck would have it, though, you were trying things out in GHCi\r\n<RyanGlScott> Which essentially checks each line of input as its own strongly connected group of declarations\r\n<RyanGlScott> So you can define MkT on one line and promote it in subsequent lines, since they're separate in the sense\r\n<RyanGlScott> *that sense\r\n<intindex> this sounds related to Trac #12088, and then I could work around it in GHC by using `$(return [])`, so data families are actually promoted anyway and this has nothing to do with GHC needing more powerful type theory\r\n<RyanGlScott> Well, it does need more powerful type theory in the sense that that's a prerequisite for making the SCC analysis for kindchecking sophisticated enough to handle this\r\n<RyanGlScott> But yes, it's quite simple to work around by using Template Haskell to explicitly split up groups.\r\n<intindex> https://gist.github.com/intindex/c6cc1e20c4b9b5c99af40ee4e23ecb61 this works and no template haskell involved\r\n<intindex> The reason I'm asking is that I'm touching this part of the User's Guide and I don't know what to write there.\r\n<RyanGlScott> Huh, now that's interesting\r\n<intindex> RyanGlScott, the only check I could find that controls what's promoted and what's not is 'isLegacyPromotableDataCon'  and enabling XTypeInType disables this check.\r\n<RyanGlScott> intindex: Right, that's baffling me\r\n<RyanGlScott> Since that's supposed to be checked every time you promote a data constructor (I think)\r\n<RyanGlScott> intindex: File a bug about that, I suppose\r\n<RyanGlScott> Richard (who's sitting next to me right now) seems to think that that shouldn't be possible\r\n<intindex> RyanGlScott, the thing is, I happily removed this check completely in D4748. Does this mean I have to restore a weaker version of it that only checks for data families? Why?\r\n<intindex> Is it bad that XDataKinds promotes data family constructors? Looks like I can just remove the \"restrictions\" part of the user guide and be done with it\r\n<RyanGlScott> intindex: In theory, that shouldn't be possible\r\n<intindex> OK, then what the check should be? No data families, any other restrictions?\r\n<RyanGlScott> I might qualify that with \"no data family instances defined in the same module\"\r\n<RyanGlScott> (Or to be precise, in the same SCC, but that's probably too technical for the users' guide)\r\n<intindex> Well, this sounds hard to check. I was thinking along the lines of keeping the 'not (isFamInstTyCon (dataConTyCon dc))' part of the check...\r\n<RyanGlScott> Oh, I thought you were only changing the users' guide :)\r\n<intindex> Well, at this point I'm confused if I should change only the user guide or the check as well. If data families shouldn't be promoted ever, then I'll change GHC. If the limitation is about the current SCC group, I can just mention Trac #12088 as a known infelicity in the User's Guide\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} >8.6.1