GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20190707T18:14:57Zhttps://gitlab.haskell.org/ghc/ghc//issues/14938Pattern matching on GADT does not refine type family parameters20190707T18:14:57ZCsongor KissPattern matching on GADT does not refine type family parametersCompiling the following code
```hs
type family R (x :: k) (y :: k) (prf :: x :~: y) :: x :~: y where
R x y Refl = Refl
```
fails with the error
```txt
Temp.hs:49:9: error:
• Expected kind ‘x :~: y’, but ‘Refl’ has kind ‘x :~: x’
• In the third argument of ‘R’, namely ‘Refl’
In the type family declaration for ‘R’

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

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

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

13  Foo2 k (e :: a :~: a) = a :~: a
 ^^^^^^^^^^^^^^
```
(Moreover, there seems to be a tidying bug, since GHC claims that `(:~:) k a a` is not the same kind as `(:~:) k a a`.)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Explicitly quantifying a kind variable causes a type family to fail to typecheck","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["TypeFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeOperators #}\r\n{# OPTIONS_GHC fprintexplicitkinds #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ntype family Foo1 (e :: (a :: k) :~: (a :: k)) :: Type where\r\n Foo1 (e :: a :~: a) = a :~: a\r\n\r\ntype family Foo2 (k :: Type) (e :: (a :: k) :~: (a :: k)) :: Type where\r\n Foo2 k (e :: a :~: a) = a :~: a\r\n}}}\r\n\r\n`Foo2` is wholly equivalent to `Foo1`, except that in `Foo2`, the `k` kind variable is explicitly quantified. However, `Foo1` typechecks, but `Foo2` does not!\r\n\r\n{{{\r\n$ /opt/ghc/8.2.2/bin/ghci Bug.hs fprintexplicitkinds\r\nGHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/ryanglscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:13:10: error:\r\n • Couldn't match kind ‘k’ with ‘k1’\r\n When matching the kind of ‘a’\r\n Expected kind ‘(:~:) k a a’, but ‘e’ has kind ‘(:~:) k a a’\r\n • In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’\r\n In the type family declaration for ‘Foo2’\r\n \r\n13  Foo2 k (e :: a :~: a) = a :~: a\r\n  ^^^^^^^^^^^^^^\r\n}}}\r\n\r\n(Moreover, there seems to be a tidying bug, since GHC claims that `(:~:) k a a` is not the same kind as `(:~:) k a a`.)","type_of_failure":"OtherFailure","blocking":[]} >8.8.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/14880GHC panic: updateRole20190707T18:15:13ZRyan ScottGHC panic: updateRoleThe following program panics on GHC 8.0.2, 8.2.2, 8.4.1, and HEAD:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Type.Equality ((:~:))
type SameKind (a :: k) (b :: k) = (() :: Constraint)
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data WhyCongSym1 (x :: Type) :: forall (a :: x)
(y :: Type)
(z :: x).
Type ~> (x ~> y) ~> x ~> x ~> (a :~: z) ~> Type
data WhyCongSym0 :: forall (x :: Type)
(a :: x)
(y :: Type)
(z :: x).
Type ~> Type ~> (x ~> y) ~> x ~> x ~> (a :~: z) ~> Type
where
WhyCongSym0KindInference :: forall x arg.
SameKind (Apply WhyCongSym0 arg) (WhyCongSym1 arg) =>
WhyCongSym0 x
```
```
$ /opt/ghc/8.2.2/bin/ghci Bug.hs
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.2 for x86_64unknownlinux):
updateRole
WhyCongSym0
arg_a1A6[sk:1]
[a1A5 :> 4, a2Cy :> 0, a2Cz :> 1, a2CA :> 2, a2CB :> 3]
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcTyDecls.hs:656:23 in ghc:TcTyDecls
```The following program panics on GHC 8.0.2, 8.2.2, 8.4.1, and HEAD:
```hs
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind
import Data.Type.Equality ((:~:))
type SameKind (a :: k) (b :: k) = (() :: Constraint)
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data WhyCongSym1 (x :: Type) :: forall (a :: x)
(y :: Type)
(z :: x).
Type ~> (x ~> y) ~> x ~> x ~> (a :~: z) ~> Type
data WhyCongSym0 :: forall (x :: Type)
(a :: x)
(y :: Type)
(z :: x).
Type ~> Type ~> (x ~> y) ~> x ~> x ~> (a :~: z) ~> Type
where
WhyCongSym0KindInference :: forall x arg.
SameKind (Apply WhyCongSym0 arg) (WhyCongSym1 arg) =>
WhyCongSym0 x
```
```
$ /opt/ghc/8.2.2/bin/ghci Bug.hs
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.2 for x86_64unknownlinux):
updateRole
WhyCongSym0
arg_a1A6[sk:1]
[a1A5 :> 4, a2Cy :> 0, a2Cz :> 1, a2CA :> 2, a2CB :> 3]
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcTyDecls.hs:656:23 in ghc:TcTyDecls
```8.6.2Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/14873The wellkinded type invariant (in TcType)20200124T11:45:58ZRyan ScottThe wellkinded type invariant (in TcType)(Originally noticed [here](https://travisci.org/goldfirere/singletons/jobs/347945148#L1179).)
The following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC HEAD:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind (Type)
data family Sing (a :: k)
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
class SingI (a :: k) where
sing :: Sing a
data ColSym1 :: f a > a ~> Bool
type instance Apply (ColSym1 x) y = Col x y
class PColumn (f :: Type > Type) where
type Col (x :: f a) (y :: a) :: Bool
class SColumn (f :: Type > Type) where
sCol :: forall (x :: f a) (y :: a).
Sing x > Sing y > Sing (Col x y :: Bool)
instance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where
sing = SLambda (sCol (sing @_ @x))
```
```
$ /opt/ghc/head/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.5.20180201 for x86_64unknownlinux):
piResultTy
k_aZU[tau:1]
(a_aW8[sk:1] > <*>_N)
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:947:35 in ghc:Type
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  highest 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC HEAD regression (piResultTy)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"(Originally noticed [https://travisci.org/goldfirere/singletons/jobs/347945148#L1179 here].)\r\n\r\nThe following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC 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 (Type)\r\n\r\ndata family Sing (a :: k)\r\n\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }\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\nclass SingI (a :: k) where\r\n sing :: Sing a\r\n\r\ndata ColSym1 :: f a > a ~> Bool\r\ntype instance Apply (ColSym1 x) y = Col x y\r\n\r\nclass PColumn (f :: Type > Type) where\r\n type Col (x :: f a) (y :: a) :: Bool\r\n\r\nclass SColumn (f :: Type > Type) where\r\n sCol :: forall (x :: f a) (y :: a).\r\n Sing x > Sing y > Sing (Col x y :: Bool)\r\n\r\ninstance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where\r\n sing = SLambda (sCol (sing @_ @x))\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/head/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.5.20180201 for x86_64unknownlinux):\r\n piResultTy\r\n k_aZU[tau:1]\r\n (a_aW8[sk:1] > <*>_N)\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:947:35 in ghc:Type\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >(Originally noticed [here](https://travisci.org/goldfirere/singletons/jobs/347945148#L1179).)
The following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC HEAD:
```hs
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module Bug where
import Data.Kind (Type)
data family Sing (a :: k)
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
class SingI (a :: k) where
sing :: Sing a
data ColSym1 :: f a > a ~> Bool
type instance Apply (ColSym1 x) y = Col x y
class PColumn (f :: Type > Type) where
type Col (x :: f a) (y :: a) :: Bool
class SColumn (f :: Type > Type) where
sCol :: forall (x :: f a) (y :: a).
Sing x > Sing y > Sing (Col x y :: Bool)
instance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where
sing = SLambda (sCol (sing @_ @x))
```
```
$ /opt/ghc/head/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.5.20180201 for x86_64unknownlinux):
piResultTy
k_aZU[tau:1]
(a_aW8[sk:1] > <*>_N)
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:947:35 in ghc:Type
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  highest 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC HEAD regression (piResultTy)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"(Originally noticed [https://travisci.org/goldfirere/singletons/jobs/347945148#L1179 here].)\r\n\r\nThe following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC 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 (Type)\r\n\r\ndata family Sing (a :: k)\r\n\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t > Sing (Apply f t) }\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\nclass SingI (a :: k) where\r\n sing :: Sing a\r\n\r\ndata ColSym1 :: f a > a ~> Bool\r\ntype instance Apply (ColSym1 x) y = Col x y\r\n\r\nclass PColumn (f :: Type > Type) where\r\n type Col (x :: f a) (y :: a) :: Bool\r\n\r\nclass SColumn (f :: Type > Type) where\r\n sCol :: forall (x :: f a) (y :: a).\r\n Sing x > Sing y > Sing (Col x y :: Bool)\r\n\r\ninstance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where\r\n sing = SLambda (sCol (sing @_ @x))\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/head/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.5.20180201 for x86_64unknownlinux):\r\n piResultTy\r\n k_aZU[tau:1]\r\n (a_aW8[sk:1] > <*>_N)\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:947:35 in ghc:Type\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >9.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/14847Inferring dependent kinds for nonrecursive types20190707T18:15:20ZSimon Peyton JonesInferring dependent kinds for nonrecursive typesConsider this
```
data Proxy k (a :: k) = MkProxy
data Proxy2 k a = MkP (Proxy k a)
```
which is discussed in [a corner of the user manual](http://downloads.haskell.org/~ghc/master/usersguide/glasgow_exts.html#inferringdependencyindatatypedeclarations).
Surprisingly, we reject `Proxy2`  but there is nothing difficult about inferring its kind. There would be if it was recursive  but it isn't.
Simple solution: for nonrecursive type declarations (we do SCC analysis so we know which these are) do not call `getInitialKinds`; instead, just infer the kind of the definition! Simple.
Warning: is this recursive?
```
data Proxy2 k a where
MkP :: Proxy k a > Proxy2 k a
```
Presumably no more than the other definition. But currently we need `Proxy2` in the environment during kind inference, because we kindcheck the result type. That seems jolly odd and inconsistent. Needs more thought.
Similar questions for
```
data T a where
T :: Int > T Bool
type family F a where
F Int = True
F _ = False
```
See also:
 #14451
 #12088
 #9427Consider this
```
data Proxy k (a :: k) = MkProxy
data Proxy2 k a = MkP (Proxy k a)
```
which is discussed in [a corner of the user manual](http://downloads.haskell.org/~ghc/master/usersguide/glasgow_exts.html#inferringdependencyindatatypedeclarations).
Surprisingly, we reject `Proxy2`  but there is nothing difficult about inferring its kind. There would be if it was recursive  but it isn't.
Simple solution: for nonrecursive type declarations (we do SCC analysis so we know which these are) do not call `getInitialKinds`; instead, just infer the kind of the definition! Simple.
Warning: is this recursive?
```
data Proxy2 k a where
MkP :: Proxy k a > Proxy2 k a
```
Presumably no more than the other definition. But currently we need `Proxy2` in the environment during kind inference, because we kindcheck the result type. That seems jolly odd and inconsistent. Needs more thought.
Similar questions for
```
data T a where
T :: Int > T Bool
type family F a where
F Int = True
F _ = False
```
See also:
 #14451
 #12088
 #9427https://gitlab.haskell.org/ghc/ghc//issues/14846Renamer hangs (because of XInstanceSigs?)20190707T18:15:20ZIcelandjackRenamer hangs (because of XInstanceSigs?)```hs
{# Language RankNTypes, TypeInType, EmptyCase, GADTs, FlexibleInstances, ConstraintKinds, UndecidableInstances, AllowAmbiguousTypes, InstanceSigs, ScopedTypeVariables #}
import Data.Kind
import Data.Proxy
type Cat ob = ob > ob > Type
data Struct :: (k > Constraint) > Type where
S :: Proxy (a::k) > Struct (cls::k > Constraint)
type Structured a cls = (S ('Proxy :: Proxy a)::Struct cls)
data AStruct :: Struct cls > Type where
AStruct :: cls a => AStruct (Structured a cls)
class StructI (structured::Struct (cls :: k > Constraint)) where
struct :: AStruct structured
instance (Structured xx cls ~ structured, cls xx) => StructI structured where
struct :: AStruct (Structured xx cls)
struct = AStruct
data Hom :: Cat k > Cat (Struct cls) where
class Category (cat::Cat ob) where
i :: StructI a => ríki a a
instance Category ríki => Category (Hom ríki :: Cat (Struct cls)) where
 Commenting out this instance signature makes the issue go away
i :: forall a. StructI a => Hom ríki a a
i = case struct :: AStruct (Structured a cls) of
```
Running on 8.2.1 and 8.5.20180105 both loop until interrupted
```
$ ghci ignoredotghci 199.hs
GHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 199.hs, interpreted )
^CInterrupted.
>
>
``````hs
{# Language RankNTypes, TypeInType, EmptyCase, GADTs, FlexibleInstances, ConstraintKinds, UndecidableInstances, AllowAmbiguousTypes, InstanceSigs, ScopedTypeVariables #}
import Data.Kind
import Data.Proxy
type Cat ob = ob > ob > Type
data Struct :: (k > Constraint) > Type where
S :: Proxy (a::k) > Struct (cls::k > Constraint)
type Structured a cls = (S ('Proxy :: Proxy a)::Struct cls)
data AStruct :: Struct cls > Type where
AStruct :: cls a => AStruct (Structured a cls)
class StructI (structured::Struct (cls :: k > Constraint)) where
struct :: AStruct structured
instance (Structured xx cls ~ structured, cls xx) => StructI structured where
struct :: AStruct (Structured xx cls)
struct = AStruct
data Hom :: Cat k > Cat (Struct cls) where
class Category (cat::Cat ob) where
i :: StructI a => ríki a a
instance Category ríki => Category (Hom ríki :: Cat (Struct cls)) where
 Commenting out this instance signature makes the issue go away
i :: forall a. StructI a => Hom ríki a a
i = case struct :: AStruct (Structured a cls) of
```
Running on 8.2.1 and 8.5.20180105 both loop until interrupted
```
$ ghci ignoredotghci 199.hs
GHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 199.hs, interpreted )
^CInterrupted.
>
>
```8.4.2Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/14845TypeInType, index GADT by constraint witness20190707T18:15:21ZIcelandjackTypeInType, index GADT by constraint witnessJust wondering if it would ever make sense to allow or use constraints like this
```hs
{# Language PolyKinds, DataKinds, KindSignatures, GADTs, TypeInType, ConstraintKinds #}
import Data.Kind
data Struct :: (k > Constraint) > (k > Type) where
S :: cls a => Struct cls a
data Foo a where
F :: Foo (S::Struct Eq a)
```
```
$ ghci ignoredotghci /tmp/test.hs
GHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/test.hs, interpreted )
/tmp/test.hs:9:13: error:
• Illegal constraint in a type: cls0 a0
• In the first argument of ‘Foo’, namely ‘(S :: Struct Eq a)’
In the type ‘Foo (S :: Struct Eq a)’
In the definition of data constructor ‘F’

9  F :: Foo (S::Struct Eq a)
 ^
Failed, no modules loaded.
Prelude>
```
Please close the ticket if it doesn't
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"TypeInType, index by GADT witnessing constraint","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Just wondering if it would ever make sense to allow or use constraints like this\r\n\r\n{{{#!hs\r\n{# Language PolyKinds, DataKinds, KindSignatures, GADTs, TypeInType, ConstraintKinds #}\r\n\r\nimport Data.Kind\r\n\r\ndata Struct :: (k > Constraint) > (k > Type) where\r\n S :: cls a => Struct cls a\r\n\r\ndata Foo a where\r\n F :: Foo (S::Struct Eq a)\r\n}}}\r\n\r\n{{{\r\n$ ghci ignoredotghci /tmp/test.hs\r\nGHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/test.hs, interpreted )\r\n\r\n/tmp/test.hs:9:13: error:\r\n • Illegal constraint in a type: cls0 a0\r\n • In the first argument of ‘Foo’, namely ‘(S :: Struct Eq a)’\r\n In the type ‘Foo (S :: Struct Eq a)’\r\n In the definition of data constructor ‘F’\r\n \r\n9  F :: Foo (S::Struct Eq a)\r\n  ^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}\r\n\r\nPlease close the ticket if it doesn't","type_of_failure":"OtherFailure","blocking":[]} >Just wondering if it would ever make sense to allow or use constraints like this
```hs
{# Language PolyKinds, DataKinds, KindSignatures, GADTs, TypeInType, ConstraintKinds #}
import Data.Kind
data Struct :: (k > Constraint) > (k > Type) where
S :: cls a => Struct cls a
data Foo a where
F :: Foo (S::Struct Eq a)
```
```
$ ghci ignoredotghci /tmp/test.hs
GHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/test.hs, interpreted )
/tmp/test.hs:9:13: error:
• Illegal constraint in a type: cls0 a0
• In the first argument of ‘Foo’, namely ‘(S :: Struct Eq a)’
In the type ‘Foo (S :: Struct Eq a)’
In the definition of data constructor ‘F’

9  F :: Foo (S::Struct Eq a)
 ^
Failed, no modules loaded.
Prelude>
```
Please close the ticket if it doesn't
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.5 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"TypeInType, index by GADT witnessing constraint","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Just wondering if it would ever make sense to allow or use constraints like this\r\n\r\n{{{#!hs\r\n{# Language PolyKinds, DataKinds, KindSignatures, GADTs, TypeInType, ConstraintKinds #}\r\n\r\nimport Data.Kind\r\n\r\ndata Struct :: (k > Constraint) > (k > Type) where\r\n S :: cls a => Struct cls a\r\n\r\ndata Foo a where\r\n F :: Foo (S::Struct Eq a)\r\n}}}\r\n\r\n{{{\r\n$ ghci ignoredotghci /tmp/test.hs\r\nGHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/test.hs, interpreted )\r\n\r\n/tmp/test.hs:9:13: error:\r\n • Illegal constraint in a type: cls0 a0\r\n • In the first argument of ‘Foo’, namely ‘(S :: Struct Eq a)’\r\n In the type ‘Foo (S :: Struct Eq a)’\r\n In the definition of data constructor ‘F’\r\n \r\n9  F :: Foo (S::Struct Eq a)\r\n  ^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}\r\n\r\nPlease close the ticket if it doesn't","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/14795Data type return kinds don't obey the forallornothing rule20190707T18:15:32ZRyan ScottData type return kinds don't obey the forallornothing ruleOriginally noticed [here](https://github.com/ghcproposals/ghcproposals/pull/103#issuecomment364562974). GHC accepts this:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
import Data.Kind
data Foo :: forall a. a > b > Type where
MkFoo :: a > Foo a b
```
Despite the fact that `Foo`'s return kind is headed by an explicit `forall` which does not quantify `b`.
The users' guide doesn't explicitly indicate that the `forall`ornothing rule should apply to data type return kinds, but goldfirere believes that not doing so is an [inconsistent design](https://github.com/ghcproposals/ghcproposals/pull/103#issuecomment364670215), so I'm opening this ticket to track this.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Data type return kinds don't obey the forallornothing rule","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Originally noticed [https://github.com/ghcproposals/ghcproposals/pull/103#issuecomment364562974 here]. GHC accepts this:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeInType #}\r\n\r\nimport Data.Kind\r\n\r\ndata Foo :: forall a. a > b > Type where\r\n MkFoo :: a > Foo a b\r\n}}}\r\n\r\nDespite the fact that `Foo`'s return kind is headed by an explicit `forall` which does not quantify `b`.\r\n\r\nThe users' guide doesn't explicitly indicate that the `forall`ornothing rule should apply to data type return kinds, but goldfirere believes that not doing so is an [https://github.com/ghcproposals/ghcproposals/pull/103#issuecomment364670215 inconsistent design], so I'm opening this ticket to track this.","type_of_failure":"OtherFailure","blocking":[]} >Originally noticed [here](https://github.com/ghcproposals/ghcproposals/pull/103#issuecomment364562974). GHC accepts this:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeInType #}
import Data.Kind
data Foo :: forall a. a > b > Type where
MkFoo :: a > Foo a b
```
Despite the fact that `Foo`'s return kind is headed by an explicit `forall` which does not quantify `b`.
The users' guide doesn't explicitly indicate that the `forall`ornothing rule should apply to data type return kinds, but goldfirere believes that not doing so is an [inconsistent design](https://github.com/ghcproposals/ghcproposals/pull/103#issuecomment364670215), so I'm opening this ticket to track this.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Data type return kinds don't obey the forallornothing rule","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Originally noticed [https://github.com/ghcproposals/ghcproposals/pull/103#issuecomment364562974 here]. GHC accepts this:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeInType #}\r\n\r\nimport Data.Kind\r\n\r\ndata Foo :: forall a. a > b > Type where\r\n MkFoo :: a > Foo a b\r\n}}}\r\n\r\nDespite the fact that `Foo`'s return kind is headed by an explicit `forall` which does not quantify `b`.\r\n\r\nThe users' guide doesn't explicitly indicate that the `forall`ornothing rule should apply to data type return kinds, but goldfirere believes that not doing so is an [https://github.com/ghcproposals/ghcproposals/pull/103#issuecomment364670215 inconsistent design], so I'm opening this ticket to track this.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14764Make $! representationpolymorphic20190707T18:15:43ZDavid FeuerMake $! representationpolymorphicCurrently,
```hs
($) :: forall r a (b :: TYPE r). (a > b) > a > b
```
but
```hs
($!) :: (a > b) > a > b
```
It seems fairly obvious that we should generalize `($!)`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Core Libraries 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Make $! representationpolymorphic","status":"New","operating_system":"","component":"Core Libraries","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"Currently,\r\n\r\n{{{#!hs\r\n($) :: forall r a (b :: TYPE r). (a > b) > a > b\r\n}}}\r\n\r\nbut\r\n\r\n{{{#!hs\r\n($!) :: (a > b) > a > b\r\n}}}\r\n\r\nIt seems fairly obvious that we should generalize `($!)`.","type_of_failure":"OtherFailure","blocking":[]} >Currently,
```hs
($) :: forall r a (b :: TYPE r). (a > b) > a > b
```
but
```hs
($!) :: (a > b) > a > b
```
It seems fairly obvious that we should generalize `($!)`.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Core Libraries 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Make $! representationpolymorphic","status":"New","operating_system":"","component":"Core Libraries","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"Currently,\r\n\r\n{{{#!hs\r\n($) :: forall r a (b :: TYPE r). (a > b) > a > b\r\n}}}\r\n\r\nbut\r\n\r\n{{{#!hs\r\n($!) :: (a > b) > a > b\r\n}}}\r\n\r\nIt seems fairly obvious that we should generalize `($!)`.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/14749T13822 fails20190707T18:15:46ZSimon Peyton JonesT13822 failsConsider this cutdown T13822
```
{# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, TypeInType #}
module T13822 where
import Data.Kind
data KIND = STAR  KIND :> KIND
data Ty :: KIND > Type where
TMaybe :: Ty (STAR :> STAR)
TApp :: Ty (a :> b) > (Ty a > Ty b)
type family IK (k :: KIND) = (res :: Type) where
IK STAR = Type
IK (a:>b) = IK a > IK b
type family I (t :: Ty k) = (res :: IK k) where
I TMaybe = Maybe
I (TApp f a) = (I f) (I a)
data TyRep (k :: KIND) (t :: Ty k) where
TyMaybe :: TyRep (STAR:>STAR) TMaybe
TyApp :: TyRep (a:>b) f > TyRep a x > TyRep b (TApp f x)
zero :: TyRep STAR a > I a
zero x = case x of
TyApp TyMaybe _ > Nothing
```
With a stage1 compiler with DEBUG enabled, this program yields a Lint error in all recent versions of GHC. (NB: Lint, not an assertion failure.)
With stage2 it succeeds, and passes Lint. Reason: without DEBUG the output of the typechecker is not Linted until after a run of the `CoreOpt`; and that simplifies the coercions; which somehow eliminates the Lint error.
I added`ddumpdspreopt` to made the precoreopt dump optional  it is sometimes useful in a nonDEBUG compiler. But that makes Lint run on the precoreopt code, and that shows up the bug always.
But an apparently unrelated patch makes it fail Lint even in stage 2. So it's kind of harmless; but a clear bug that we should fix.
I'll mark T13822 as expectbroken; you can reenable it when this ticket is fixed.
The Lint error is pretty obscure
```
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
[in body of letrec with binders co_a10u :: (f_a10g :: Ty
(a_a10f ':> 'STAR))
~# (('TMaybe > (Ty
(Sym co_a10r
':> <'STAR>_N)_N)_N) :: Ty
(a_a10f
':> 'STAR))]
Kind application error in
coercion ‘(Maybe
(Sym (Coh <I (x_a10h > Sym (Ty (Sym co_a10r))_N)>_N
(D:R:IK[0]) ; Coh <(I (x_a10h > Sym (Ty
(Sym co_a10r))_N) > D:R:IK[0])>_N
(Sym (D:R:IK[0]))) ; Coh <I (x_a10h > Sym (Ty
(Sym co_a10r))_N)>_N
(D:R:IK[0])))_N’
Function kind = * > *
Arg kinds = [(I (x_a10h > Sym (Ty (Sym co_a10r))_N), IK 'STAR)]
Fun: *
(I (x_a10h > Sym (Ty (Sym co_a10r))_N), IK 'STAR)
```Consider this cutdown T13822
```
{# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, TypeInType #}
module T13822 where
import Data.Kind
data KIND = STAR  KIND :> KIND
data Ty :: KIND > Type where
TMaybe :: Ty (STAR :> STAR)
TApp :: Ty (a :> b) > (Ty a > Ty b)
type family IK (k :: KIND) = (res :: Type) where
IK STAR = Type
IK (a:>b) = IK a > IK b
type family I (t :: Ty k) = (res :: IK k) where
I TMaybe = Maybe
I (TApp f a) = (I f) (I a)
data TyRep (k :: KIND) (t :: Ty k) where
TyMaybe :: TyRep (STAR:>STAR) TMaybe
TyApp :: TyRep (a:>b) f > TyRep a x > TyRep b (TApp f x)
zero :: TyRep STAR a > I a
zero x = case x of
TyApp TyMaybe _ > Nothing
```
With a stage1 compiler with DEBUG enabled, this program yields a Lint error in all recent versions of GHC. (NB: Lint, not an assertion failure.)
With stage2 it succeeds, and passes Lint. Reason: without DEBUG the output of the typechecker is not Linted until after a run of the `CoreOpt`; and that simplifies the coercions; which somehow eliminates the Lint error.
I added`ddumpdspreopt` to made the precoreopt dump optional  it is sometimes useful in a nonDEBUG compiler. But that makes Lint run on the precoreopt code, and that shows up the bug always.
But an apparently unrelated patch makes it fail Lint even in stage 2. So it's kind of harmless; but a clear bug that we should fix.
I'll mark T13822 as expectbroken; you can reenable it when this ticket is fixed.
The Lint error is pretty obscure
```
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
[in body of letrec with binders co_a10u :: (f_a10g :: Ty
(a_a10f ':> 'STAR))
~# (('TMaybe > (Ty
(Sym co_a10r
':> <'STAR>_N)_N)_N) :: Ty
(a_a10f
':> 'STAR))]
Kind application error in
coercion ‘(Maybe
(Sym (Coh <I (x_a10h > Sym (Ty (Sym co_a10r))_N)>_N
(D:R:IK[0]) ; Coh <(I (x_a10h > Sym (Ty
(Sym co_a10r))_N) > D:R:IK[0])>_N
(Sym (D:R:IK[0]))) ; Coh <I (x_a10h > Sym (Ty
(Sym co_a10r))_N)>_N
(D:R:IK[0])))_N’
Function kind = * > *
Arg kinds = [(I (x_a10h > Sym (Ty (Sym co_a10r))_N), IK 'STAR)]
Fun: *
(I (x_a10h > Sym (Ty (Sym co_a10r))_N), IK 'STAR)
```Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/14720GHC 8.4.1alpha regression with TypeInType20190707T18:15:53ZRyan ScottGHC 8.4.1alpha regression with TypeInTypeGHC 8.2.2 is able to typecheck this code:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE DefaultSignatures #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module SGenerics where
import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..), sym, trans)
import Data.Void
data family Sing (z :: k)
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)
class (PGeneric k, SGeneric k) => VGeneric k where
sTof :: forall (a :: k). Sing a > PTo (PFrom a) :~: a
sFot :: forall (a :: Rep k). Sing a > PFrom (PTo a :: k) :~: a
data Decision a = Proved a
 Disproved (a > Void)
class SDecide k where
(%~) :: forall (a :: k) (b :: k). Sing a > Sing b > Decision (a :~: b)
default (%~) :: forall (a :: k) (b :: k). (VGeneric 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) >
case (sTof s1, sTof s2) of
(Refl, Refl) > Proved Refl
Disproved contra > Disproved (\Refl > contra Refl)
```
But GHC 8.4.1alpha2 cannot:
```
$ /opt/ghc/8.4.1/bin/ghc Bug.hs
[1 of 1] Compiling SGenerics ( Bug.hs, Bug.o )
Bug.hs:44:52: error:
• Could not deduce: PFrom a ~ PFrom a
from the context: b ~ a
bound by a pattern with constructor:
Refl :: forall k (a :: k). a :~: a,
in a lambda abstraction
at Bug.hs:44:3740
Expected type: PFrom a :~: PFrom b
Actual type: PFrom a :~: PFrom a
NB: ‘PFrom’ is a noninjective type family
• In the first argument of ‘contra’, namely ‘Refl’
In the expression: contra Refl
In the first argument of ‘Disproved’, namely
‘(\ Refl > contra Refl)’
• Relevant bindings include
contra :: (PFrom a :~: PFrom b) > Void (bound at Bug.hs:44:15)
s2 :: Sing b (bound at Bug.hs:40:9)
s1 :: Sing a (bound at Bug.hs:40:3)
(%~) :: Sing a > Sing b > Decision (a :~: b)
(bound at Bug.hs:40:3)

44  Disproved contra > Disproved (\Refl > contra Refl)
 ^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1alpha1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC 8.4.1alpha regression with TypeInType","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1alpha1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC 8.2.2 is able to typecheck this code:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE DefaultSignatures #}\r\n{# LANGUAGE FlexibleContexts #}\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 (Type)\r\nimport Data.Type.Equality ((:~:)(..), sym, trans)\r\nimport Data.Void\r\n\r\ndata family Sing (z :: k)\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\r\nclass (PGeneric k, SGeneric k) => VGeneric k where\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\ndata Decision a = Proved a\r\n  Disproved (a > Void)\r\n\r\nclass SDecide k where\r\n (%~) :: forall (a :: k) (b :: k). Sing a > Sing b > Decision (a :~: b)\r\n default (%~) :: forall (a :: k) (b :: k). (VGeneric 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 case (sTof s1, sTof s2) of\r\n (Refl, Refl) > Proved Refl\r\n Disproved contra > Disproved (\\Refl > contra Refl)\r\n}}}\r\n\r\nBut GHC 8.4.1alpha2 cannot:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling SGenerics ( Bug.hs, Bug.o )\r\n\r\nBug.hs:44:52: error:\r\n • Could not deduce: PFrom a ~ PFrom a\r\n from the context: b ~ a\r\n bound by a pattern with constructor:\r\n Refl :: forall k (a :: k). a :~: a,\r\n in a lambda abstraction\r\n at Bug.hs:44:3740\r\n Expected type: PFrom a :~: PFrom b\r\n Actual type: PFrom a :~: PFrom a\r\n NB: ‘PFrom’ is a noninjective type family\r\n • In the first argument of ‘contra’, namely ‘Refl’\r\n In the expression: contra Refl\r\n In the first argument of ‘Disproved’, namely\r\n ‘(\\ Refl > contra Refl)’\r\n • Relevant bindings include\r\n contra :: (PFrom a :~: PFrom b) > Void (bound at Bug.hs:44:15)\r\n s2 :: Sing b (bound at Bug.hs:40:9)\r\n s1 :: Sing a (bound at Bug.hs:40:3)\r\n (%~) :: Sing a > Sing b > Decision (a :~: b)\r\n (bound at Bug.hs:40:3)\r\n \r\n44  Disproved contra > Disproved (\\Refl > contra Refl)\r\n  ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >GHC 8.2.2 is able to typecheck this code:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE DefaultSignatures #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module SGenerics where
import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..), sym, trans)
import Data.Void
data family Sing (z :: k)
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)
class (PGeneric k, SGeneric k) => VGeneric k where
sTof :: forall (a :: k). Sing a > PTo (PFrom a) :~: a
sFot :: forall (a :: Rep k). Sing a > PFrom (PTo a :: k) :~: a
data Decision a = Proved a
 Disproved (a > Void)
class SDecide k where
(%~) :: forall (a :: k) (b :: k). Sing a > Sing b > Decision (a :~: b)
default (%~) :: forall (a :: k) (b :: k). (VGeneric 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) >
case (sTof s1, sTof s2) of
(Refl, Refl) > Proved Refl
Disproved contra > Disproved (\Refl > contra Refl)
```
But GHC 8.4.1alpha2 cannot:
```
$ /opt/ghc/8.4.1/bin/ghc Bug.hs
[1 of 1] Compiling SGenerics ( Bug.hs, Bug.o )
Bug.hs:44:52: error:
• Could not deduce: PFrom a ~ PFrom a
from the context: b ~ a
bound by a pattern with constructor:
Refl :: forall k (a :: k). a :~: a,
in a lambda abstraction
at Bug.hs:44:3740
Expected type: PFrom a :~: PFrom b
Actual type: PFrom a :~: PFrom a
NB: ‘PFrom’ is a noninjective type family
• In the first argument of ‘contra’, namely ‘Refl’
In the expression: contra Refl
In the first argument of ‘Disproved’, namely
‘(\ Refl > contra Refl)’
• Relevant bindings include
contra :: (PFrom a :~: PFrom b) > Void (bound at Bug.hs:44:15)
s2 :: Sing b (bound at Bug.hs:40:9)
s1 :: Sing a (bound at Bug.hs:40:3)
(%~) :: Sing a > Sing b > Decision (a :~: b)
(bound at Bug.hs:40:3)

44  Disproved contra > Disproved (\Refl > contra Refl)
 ^^^^
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1alpha1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC 8.4.1alpha regression with TypeInType","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1alpha1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC 8.2.2 is able to typecheck this code:\r\n\r\n{{{#!hs\r\n{# LANGUAGE AllowAmbiguousTypes #}\r\n{# LANGUAGE DefaultSignatures #}\r\n{# LANGUAGE FlexibleContexts #}\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 (Type)\r\nimport Data.Type.Equality ((:~:)(..), sym, trans)\r\nimport Data.Void\r\n\r\ndata family Sing (z :: k)\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\r\nclass (PGeneric k, SGeneric k) => VGeneric k where\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\ndata Decision a = Proved a\r\n  Disproved (a > Void)\r\n\r\nclass SDecide k where\r\n (%~) :: forall (a :: k) (b :: k). Sing a > Sing b > Decision (a :~: b)\r\n default (%~) :: forall (a :: k) (b :: k). (VGeneric 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 case (sTof s1, sTof s2) of\r\n (Refl, Refl) > Proved Refl\r\n Disproved contra > Disproved (\\Refl > contra Refl)\r\n}}}\r\n\r\nBut GHC 8.4.1alpha2 cannot:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling SGenerics ( Bug.hs, Bug.o )\r\n\r\nBug.hs:44:52: error:\r\n • Could not deduce: PFrom a ~ PFrom a\r\n from the context: b ~ a\r\n bound by a pattern with constructor:\r\n Refl :: forall k (a :: k). a :~: a,\r\n in a lambda abstraction\r\n at Bug.hs:44:3740\r\n Expected type: PFrom a :~: PFrom b\r\n Actual type: PFrom a :~: PFrom a\r\n NB: ‘PFrom’ is a noninjective type family\r\n • In the first argument of ‘contra’, namely ‘Refl’\r\n In the expression: contra Refl\r\n In the first argument of ‘Disproved’, namely\r\n ‘(\\ Refl > contra Refl)’\r\n • Relevant bindings include\r\n contra :: (PFrom a :~: PFrom b) > Void (bound at Bug.hs:44:15)\r\n s2 :: Sing b (bound at Bug.hs:40:9)\r\n s1 :: Sing a (bound at Bug.hs:40:3)\r\n (%~) :: Sing a > Sing b > Decision (a :~: b)\r\n (bound at Bug.hs:40:3)\r\n \r\n44  Disproved contra > Disproved (\\Refl > contra Refl)\r\n  ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.4.1https://gitlab.haskell.org/ghc/ghc//issues/14668Ordering of declarations can cause typechecking to fail20190707T18:16:05ZheptahedronOrdering of declarations can cause typechecking to failThe following will successfully typecheck:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeFamilies #}
data CInst
data G (b :: ()) = G
class C a where
type family F a
class (C a) => C' a where
type family F' a (b :: F a)
 data CInst
instance C CInst where
type F CInst = ()
instance C' CInst where
type F' CInst (b :: F CInst) = G b
```
But if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error:
```
Test.hs:23:18: error:
• Expected kind ‘F CInst’, but ‘b’ has kind ‘()’
• In the second argument of ‘F'’, namely ‘(b :: F CInst)’
In the type instance declaration for ‘F'’
In the instance declaration for ‘C' CInst’

23  type F' CInst (b :: F CInst) = G b

```
However, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as `data G (b :: F CInst) = G`.
This behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).
I was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Ordering of declarations can cause typechecking to fail","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following will successfully typecheck:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeFamilies #}\r\n\r\ndata CInst\r\n\r\ndata G (b :: ()) = G \r\n\r\nclass C a where\r\n type family F a\r\n \r\nclass (C a) => C' a where\r\n type family F' a (b :: F a)\r\n\r\n data CInst\r\n\r\ninstance C CInst where\r\n type F CInst = ()\r\n\r\ninstance C' CInst where\r\ntype F' CInst (b :: F CInst) = G b\r\n}}}\r\n\r\nBut if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error: \r\n\r\n{{{\r\nTest.hs:23:18: error:\r\n • Expected kind ‘F CInst’, but ‘b’ has kind ‘()’\r\n • In the second argument of ‘F'’, namely ‘(b :: F CInst)’\r\n In the type instance declaration for ‘F'’\r\n In the instance declaration for ‘C' CInst’\r\n \r\n23  type F' CInst (b :: F CInst) = G b\r\n  \r\n}}}\r\n\r\nHowever, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as `data G (b :: F CInst) = G`.\r\n\r\nThis behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).\r\n\r\nI was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well.","type_of_failure":"OtherFailure","blocking":[]} >The following will successfully typecheck:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeFamilies #}
data CInst
data G (b :: ()) = G
class C a where
type family F a
class (C a) => C' a where
type family F' a (b :: F a)
 data CInst
instance C CInst where
type F CInst = ()
instance C' CInst where
type F' CInst (b :: F CInst) = G b
```
But if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error:
```
Test.hs:23:18: error:
• Expected kind ‘F CInst’, but ‘b’ has kind ‘()’
• In the second argument of ‘F'’, namely ‘(b :: F CInst)’
In the type instance declaration for ‘F'’
In the instance declaration for ‘C' CInst’

23  type F' CInst (b :: F CInst) = G b

```
However, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as `data G (b :: F CInst) = G`.
This behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).
I was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Ordering of declarations can cause typechecking to fail","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following will successfully typecheck:\r\n\r\n{{{#!hs\r\n{# LANGUAGE DataKinds #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE TypeInType #}\r\n{# LANGUAGE TypeFamilies #}\r\n\r\ndata CInst\r\n\r\ndata G (b :: ()) = G \r\n\r\nclass C a where\r\n type family F a\r\n \r\nclass (C a) => C' a where\r\n type family F' a (b :: F a)\r\n\r\n data CInst\r\n\r\ninstance C CInst where\r\n type F CInst = ()\r\n\r\ninstance C' CInst where\r\ntype F' CInst (b :: F CInst) = G b\r\n}}}\r\n\r\nBut if the `data CInst` declaration is moved to where it is currently commented out, typechecking fails with this error: \r\n\r\n{{{\r\nTest.hs:23:18: error:\r\n • Expected kind ‘F CInst’, but ‘b’ has kind ‘()’\r\n • In the second argument of ‘F'’, namely ‘(b :: F CInst)’\r\n In the type instance declaration for ‘F'’\r\n In the instance declaration for ‘C' CInst’\r\n \r\n23  type F' CInst (b :: F CInst) = G b\r\n  \r\n}}}\r\n\r\nHowever, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as `data G (b :: F CInst) = G`.\r\n\r\nThis behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).\r\n\r\nI was using GHC 8.2.2 when I discovered this, but user `erisco` on `#haskell` confirmed for 8.2.1 as well.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14645Allow type family in data family return kind20190707T18:16:10ZRichard Eisenbergrae@richarde.devAllow type family in data family return kindGHC currently allows
```hs
data family DF1 :: k1 > k2
```
where it's expected (and checked) that all data *instances* have a return kind of `Type`. (Perhaps `k2` expands to `Type > Type`, for example.)
However, it rejects
```hs
type family TF (x :: Type) :: Type
data family DF2 :: x > TF x
```
when that's clearly just as sensible as the first definition.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1alpha1 
 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":"Allow type family in data family return kind","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1alpha1","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC currently allows\r\n\r\n{{{#!hs\r\ndata family DF1 :: k1 > k2\r\n}}}\r\n\r\nwhere it's expected (and checked) that all data ''instances'' have a return kind of `Type`. (Perhaps `k2` expands to `Type > Type`, for example.)\r\n\r\nHowever, it rejects\r\n\r\n{{{#!hs\r\ntype family TF (x :: Type) :: Type\r\ndata family DF2 :: x > TF x\r\n}}}\r\n\r\nwhen that's clearly just as sensible as the first definition.","type_of_failure":"OtherFailure","blocking":[]} >GHC currently allows
```hs
data family DF1 :: k1 > k2
```
where it's expected (and checked) that all data *instances* have a return kind of `Type`. (Perhaps `k2` expands to `Type > Type`, for example.)
However, it rejects
```hs
type family TF (x :: Type) :: Type
data family DF2 :: x > TF x
```
when that's clearly just as sensible as the first definition.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.4.1alpha1 
 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":"Allow type family in data family return kind","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1alpha1","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC currently allows\r\n\r\n{{{#!hs\r\ndata family DF1 :: k1 > k2\r\n}}}\r\n\r\nwhere it's expected (and checked) that all data ''instances'' have a return kind of `Type`. (Perhaps `k2` expands to `Type > Type`, for example.)\r\n\r\nHowever, it rejects\r\n\r\n{{{#!hs\r\ntype family TF (x :: Type) :: Type\r\ndata family DF2 :: x > TF x\r\n}}}\r\n\r\nwhen that's clearly just as sensible as the first definition.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14607Core Lint error20190707T18:16:18ZIcelandjackCore Lint errorThis produces a long Core lint error:
```hs
{# Language DerivingStrategies #}
{# Language GADTs #}
{# Language GeneralizedNewtypeDeriving #}
{# Language InstanceSigs #}
{# Language KindSignatures #}
{# Language TypeFamilies #}
{# Language TypeInType #}
{# Language TypeOperators #}
import Data.Kind
data DEFUNC :: Type > Type > Type where
(:~>) :: a > b > DEFUNC a b
type a ~> b = DEFUNC a b > Type
data LamCons a :: Type ~> Type where
LamCons :: a > LamCons a ([a] :~> [a])
class Mk (app :: Type ~> Type) where
type Arg app :: Type
mk :: Arg app > app (a :~> b)
instance Mk (LamCons a :: Type ~> Type) where
type Arg (LamCons a) = a
mk :: a > LamCons (a :~> b)
mk = LamCons
```
with `ghci ignoredotghci fdefertypeerrors dcorelint bug.hs` on GHC 8.2.1 and 8.3.20171208.This produces a long Core lint error:
```hs
{# Language DerivingStrategies #}
{# Language GADTs #}
{# Language GeneralizedNewtypeDeriving #}
{# Language InstanceSigs #}
{# Language KindSignatures #}
{# Language TypeFamilies #}
{# Language TypeInType #}
{# Language TypeOperators #}
import Data.Kind
data DEFUNC :: Type > Type > Type where
(:~>) :: a > b > DEFUNC a b
type a ~> b = DEFUNC a b > Type
data LamCons a :: Type ~> Type where
LamCons :: a > LamCons a ([a] :~> [a])
class Mk (app :: Type ~> Type) where
type Arg app :: Type
mk :: Arg app > app (a :~> b)
instance Mk (LamCons a :: Type ~> Type) where
type Arg (LamCons a) = a
mk :: a > LamCons (a :~> b)
mk = LamCons
```
with `ghci ignoredotghci fdefertypeerrors dcorelint bug.hs` on GHC 8.2.1 and 8.3.20171208.https://gitlab.haskell.org/ghc/ghc//issues/14605Core Lint error20190707T18:16:19ZIcelandjackCore Lint errorThis piece of code fails when run with `ghci ignoredotghci fdefertypeerrors dcorelint bug.hs`, maybe same as my previous #14584.
```hs
{# Language DerivingStrategies #}
{# Language GeneralizedNewtypeDeriving #}
{# Language InstanceSigs #}
{# Language KindSignatures #}
{# Language PolyKinds #}
{# Language ScopedTypeVariables #}
{# Language TypeApplications #}
{# Language TypeFamilies #}
{# Language TypeInType #}
{# Language TypeOperators #}
{# Language UndecidableInstances #}
import Data.Kind
import Data.Functor.Identity
import Data.Functor.Product
type a <> b = a > b > Type
class Iso (iso :: a <> b) where
iso :: a > b
osi :: b > a
data Iso_Bool :: Either () () <> Bool
instance Iso Iso_Bool where
class Representable f where
type Rep f :: Type
index :: f a > (Rep f > a)
tabulate :: (Rep f > a) > f a
class Comonad w where
extract :: w a > a
duplicate :: w a > w (w a)
newtype Co f a = Co (f a) deriving newtype (Functor, Representable)
instance (Representable f, Monoid (Rep f)) => Comonad (Co f) where
extract = (`index` mempty)
newtype WRAP (iso::old <> new) f a = WRAP (f a)
instance (Representable f, Rep f ~ old, Iso iso) => Representable (WRAP (iso :: old <> new) f) where
type Rep (WRAP (iso :: old <> new) f) = new
index :: WRAP iso f a > (new > a)
index (WRAP fa) = index fa . osi @old @new @iso
tabulate :: (new > a) > WRAP iso f a
tabulate gen = WRAP $
tabulate (gen . iso @old @new @iso)
newtype PAIR a = PAIR (Co (WRAP Iso_Bool (Product Identity Identity)) a)
deriving newtype
Comonad
```
I unfortunately don't have time to find a more minimal example. Core linter vomits a lot of errors on 8.2.1 & 8.3.20171208.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Core Lint error","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["DeferredTypeErrors","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This piece of code fails when run with `ghci ignoredotghci fdefertypeerrors dcorelint bug.hs`, maybe same as my previous #14584.\r\n\r\n{{{#!hs\r\n{# Language DerivingStrategies #}\r\n{# Language GeneralizedNewtypeDeriving #}\r\n{# Language InstanceSigs #}\r\n{# Language KindSignatures #}\r\n{# Language PolyKinds #}\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\n\r\nimport Data.Kind\r\nimport Data.Functor.Identity\r\nimport Data.Functor.Product\r\n\r\ntype a <> b = a > b > Type\r\n\r\nclass Iso (iso :: a <> b) where\r\n iso :: a > b\r\n osi :: b > a\r\n\r\ndata Iso_Bool :: Either () () <> Bool\r\n\r\ninstance Iso Iso_Bool where\r\n\r\nclass Representable f where\r\n type Rep f :: Type\r\n\r\n index :: f a > (Rep f > a)\r\n tabulate :: (Rep f > a) > f a\r\n\r\nclass Comonad w where\r\n extract :: w a > a\r\n duplicate :: w a > w (w a)\r\n\r\nnewtype Co f a = Co (f a) deriving newtype (Functor, Representable)\r\n\r\ninstance (Representable f, Monoid (Rep f)) => Comonad (Co f) where\r\n extract = (`index` mempty)\r\n\r\nnewtype WRAP (iso::old <> new) f a = WRAP (f a)\r\n\r\ninstance (Representable f, Rep f ~ old, Iso iso) => Representable (WRAP (iso :: old <> new) f) where\r\n type Rep (WRAP (iso :: old <> new) f) = new\r\n\r\n index :: WRAP iso f a > (new > a)\r\n index (WRAP fa) = index fa . osi @old @new @iso\r\n\r\n tabulate :: (new > a) > WRAP iso f a\r\n tabulate gen = WRAP $ \r\n tabulate (gen . iso @old @new @iso)\r\n\r\nnewtype PAIR a = PAIR (Co (WRAP Iso_Bool (Product Identity Identity)) a)\r\n deriving newtype\r\n Comonad \r\n}}}\r\n\r\nI unfortunately don't have time to find a more minimal example. Core linter vomits a lot of errors on 8.2.1 & 8.3.20171208. ","type_of_failure":"OtherFailure","blocking":[]} >This piece of code fails when run with `ghci ignoredotghci fdefertypeerrors dcorelint bug.hs`, maybe same as my previous #14584.
```hs
{# Language DerivingStrategies #}
{# Language GeneralizedNewtypeDeriving #}
{# Language InstanceSigs #}
{# Language KindSignatures #}
{# Language PolyKinds #}
{# Language ScopedTypeVariables #}
{# Language TypeApplications #}
{# Language TypeFamilies #}
{# Language TypeInType #}
{# Language TypeOperators #}
{# Language UndecidableInstances #}
import Data.Kind
import Data.Functor.Identity
import Data.Functor.Product
type a <> b = a > b > Type
class Iso (iso :: a <> b) where
iso :: a > b
osi :: b > a
data Iso_Bool :: Either () () <> Bool
instance Iso Iso_Bool where
class Representable f where
type Rep f :: Type
index :: f a > (Rep f > a)
tabulate :: (Rep f > a) > f a
class Comonad w where
extract :: w a > a
duplicate :: w a > w (w a)
newtype Co f a = Co (f a) deriving newtype (Functor, Representable)
instance (Representable f, Monoid (Rep f)) => Comonad (Co f) where
extract = (`index` mempty)
newtype WRAP (iso::old <> new) f a = WRAP (f a)
instance (Representable f, Rep f ~ old, Iso iso) => Representable (WRAP (iso :: old <> new) f) where
type Rep (WRAP (iso :: old <> new) f) = new
index :: WRAP iso f a > (new > a)
index (WRAP fa) = index fa . osi @old @new @iso
tabulate :: (new > a) > WRAP iso f a
tabulate gen = WRAP $
tabulate (gen . iso @old @new @iso)
newtype PAIR a = PAIR (Co (WRAP Iso_Bool (Product Identity Identity)) a)
deriving newtype
Comonad
```
I unfortunately don't have time to find a more minimal example. Core linter vomits a lot of errors on 8.2.1 & 8.3.20171208.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Core Lint error","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["DeferredTypeErrors","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This piece of code fails when run with `ghci ignoredotghci fdefertypeerrors dcorelint bug.hs`, maybe same as my previous #14584.\r\n\r\n{{{#!hs\r\n{# Language DerivingStrategies #}\r\n{# Language GeneralizedNewtypeDeriving #}\r\n{# Language InstanceSigs #}\r\n{# Language KindSignatures #}\r\n{# Language PolyKinds #}\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\n\r\nimport Data.Kind\r\nimport Data.Functor.Identity\r\nimport Data.Functor.Product\r\n\r\ntype a <> b = a > b > Type\r\n\r\nclass Iso (iso :: a <> b) where\r\n iso :: a > b\r\n osi :: b > a\r\n\r\ndata Iso_Bool :: Either () () <> Bool\r\n\r\ninstance Iso Iso_Bool where\r\n\r\nclass Representable f where\r\n type Rep f :: Type\r\n\r\n index :: f a > (Rep f > a)\r\n tabulate :: (Rep f > a) > f a\r\n\r\nclass Comonad w where\r\n extract :: w a > a\r\n duplicate :: w a > w (w a)\r\n\r\nnewtype Co f a = Co (f a) deriving newtype (Functor, Representable)\r\n\r\ninstance (Representable f, Monoid (Rep f)) => Comonad (Co f) where\r\n extract = (`index` mempty)\r\n\r\nnewtype WRAP (iso::old <> new) f a = WRAP (f a)\r\n\r\ninstance (Representable f, Rep f ~ old, Iso iso) => Representable (WRAP (iso :: old <> new) f) where\r\n type Rep (WRAP (iso :: old <> new) f) = new\r\n\r\n index :: WRAP iso f a > (new > a)\r\n index (WRAP fa) = index fa . osi @old @new @iso\r\n\r\n tabulate :: (new > a) > WRAP iso f a\r\n tabulate gen = WRAP $ \r\n tabulate (gen . iso @old @new @iso)\r\n\r\nnewtype PAIR a = PAIR (Co (WRAP Iso_Bool (Product Identity Identity)) a)\r\n deriving newtype\r\n Comonad \r\n}}}\r\n\r\nI unfortunately don't have time to find a more minimal example. Core linter vomits a lot of errors on 8.2.1 & 8.3.20171208. ","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14580GHC panic (TypeInType) (the 'impossible' happened)20190707T18:16:25ZIcelandjackGHC panic (TypeInType) (the 'impossible' happened)```
$ ghci ignoredotghci
GHCi, version 8.3.20171208: http://www.haskell.org/ghc/ :? for help
Prelude> import Data.Kind
Prelude Data.Kind> :set XPolyKinds XDataKinds XTypeInType XTypeOperators
Prelude Data.Kind> type Cat ob = ob > ob > Type
Prelude Data.Kind> data ISO' :: Cat i > i > i > Type
Prelude Data.Kind> type ISO cat a b = ISO' cat a b > Type
Prelude Data.Kind> type (a <> b) iso cat = ISO (iso :: cat a b)
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171208 for x86_64unknownlinux):
piResultTy
k_a1x1[tau:1]
a_a1wU[sk:1]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1144:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:951:35 in ghc:Type
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
Prelude Data.Kind>
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC panic (TypeInType) (the 'impossible' happened)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\n$ ghci ignoredotghci\r\nGHCi, version 8.3.20171208: http://www.haskell.org/ghc/ :? for help\r\nPrelude> import Data.Kind\r\nPrelude Data.Kind> :set XPolyKinds XDataKinds XTypeInType XTypeOperators \r\nPrelude Data.Kind> type Cat ob = ob > ob > Type\r\nPrelude Data.Kind> data ISO' :: Cat i > i > i > Type\r\nPrelude Data.Kind> type ISO cat a b = ISO' cat a b > Type\r\nPrelude Data.Kind> type (a <> b) iso cat = ISO (iso :: cat a b)\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171208 for x86_64unknownlinux):\r\n\tpiResultTy\r\n k_a1x1[tau:1]\r\n a_a1wU[sk:1]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1144:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:951:35 in ghc:Type\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\nPrelude Data.Kind> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >```
$ ghci ignoredotghci
GHCi, version 8.3.20171208: http://www.haskell.org/ghc/ :? for help
Prelude> import Data.Kind
Prelude Data.Kind> :set XPolyKinds XDataKinds XTypeInType XTypeOperators
Prelude Data.Kind> type Cat ob = ob > ob > Type
Prelude Data.Kind> data ISO' :: Cat i > i > i > Type
Prelude Data.Kind> type ISO cat a b = ISO' cat a b > Type
Prelude Data.Kind> type (a <> b) iso cat = ISO (iso :: cat a b)
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171208 for x86_64unknownlinux):
piResultTy
k_a1x1[tau:1]
a_a1wU[sk:1]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1144:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:951:35 in ghc:Type
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
Prelude Data.Kind>
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC panic (TypeInType) (the 'impossible' happened)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\n$ ghci ignoredotghci\r\nGHCi, version 8.3.20171208: http://www.haskell.org/ghc/ :? for help\r\nPrelude> import Data.Kind\r\nPrelude Data.Kind> :set XPolyKinds XDataKinds XTypeInType XTypeOperators \r\nPrelude Data.Kind> type Cat ob = ob > ob > Type\r\nPrelude Data.Kind> data ISO' :: Cat i > i > i > Type\r\nPrelude Data.Kind> type ISO cat a b = ISO' cat a b > Type\r\nPrelude Data.Kind> type (a <> b) iso cat = ISO (iso :: cat a b)\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171208 for x86_64unknownlinux):\r\n\tpiResultTy\r\n k_a1x1[tau:1]\r\n a_a1wU[sk:1]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1144:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:951:35 in ghc:Type\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\nPrelude Data.Kind> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14563GHC Panic with TypeInType / levity polymorphism20190707T18:16:30ZIcelandjackGHC Panic with TypeInType / levity polymorphismThis code is rightfully rejected.
```hs
 {# Language TypeInType #}
{# Language RankNTypes, KindSignatures, PolyKinds #}
import GHC.Types (TYPE)
import Data.Kind
data Lan (g::TYPE rep > TYPE rep') (h::TYPE rep > TYPE rep'') a where Lan :: forall xx (g::TYPE rep > TYPE rep') (h::TYPE rep > Type) a. (g xx > a) > h xx > Lan g h a
```
But uncomment first line and it panics
```
$ ghci2 ~/hs/132bug.hs
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /home/baldur/hs/132bug.hs, interpreted )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171122 for x86_64unknownlinux):
zonkTcTyVarToVar
'LiftedRep
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcType.hs:1640:17 in ghc:TcType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
Maybe the same as #14555.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.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 Panic with TypeInType / levity polymorphism","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["LevityPolymorphism,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code is rightfully rejected.\r\n\r\n{{{#!hs\r\n {# Language TypeInType #}\r\n{# Language RankNTypes, KindSignatures, PolyKinds #}\r\n\r\nimport GHC.Types (TYPE)\r\nimport Data.Kind\r\n\r\ndata Lan (g::TYPE rep > TYPE rep') (h::TYPE rep > TYPE rep'') a where Lan :: forall xx (g::TYPE rep > TYPE rep') (h::TYPE rep > Type) a. (g xx > a) > h xx > Lan g h a\r\n}}}\r\n\r\nBut uncomment first line and it panics\r\n\r\n{{{\r\n$ ghci2 ~/hs/132bug.hs\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /home/baldur/hs/132bug.hs, interpreted )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171122 for x86_64unknownlinux):\r\n\tzonkTcTyVarToVar\r\n 'LiftedRep\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcType.hs:1640:17 in ghc:TcType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n> \r\n}}}\r\n\r\nMaybe the same as #14555.","type_of_failure":"OtherFailure","blocking":[]} >This code is rightfully rejected.
```hs
 {# Language TypeInType #}
{# Language RankNTypes, KindSignatures, PolyKinds #}
import GHC.Types (TYPE)
import Data.Kind
data Lan (g::TYPE rep > TYPE rep') (h::TYPE rep > TYPE rep'') a where Lan :: forall xx (g::TYPE rep > TYPE rep') (h::TYPE rep > Type) a. (g xx > a) > h xx > Lan g h a
```
But uncomment first line and it panics
```
$ ghci2 ~/hs/132bug.hs
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /home/baldur/hs/132bug.hs, interpreted )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171122 for x86_64unknownlinux):
zonkTcTyVarToVar
'LiftedRep
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcType.hs:1640:17 in ghc:TcType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
Maybe the same as #14555.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.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 Panic with TypeInType / levity polymorphism","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["LevityPolymorphism,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code is rightfully rejected.\r\n\r\n{{{#!hs\r\n {# Language TypeInType #}\r\n{# Language RankNTypes, KindSignatures, PolyKinds #}\r\n\r\nimport GHC.Types (TYPE)\r\nimport Data.Kind\r\n\r\ndata Lan (g::TYPE rep > TYPE rep') (h::TYPE rep > TYPE rep'') a where Lan :: forall xx (g::TYPE rep > TYPE rep') (h::TYPE rep > Type) a. (g xx > a) > h xx > Lan g h a\r\n}}}\r\n\r\nBut uncomment first line and it panics\r\n\r\n{{{\r\n$ ghci2 ~/hs/132bug.hs\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /home/baldur/hs/132bug.hs, interpreted )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171122 for x86_64unknownlinux):\r\n\tzonkTcTyVarToVar\r\n 'LiftedRep\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcType.hs:1640:17 in ghc:TcType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n> \r\n}}}\r\n\r\nMaybe the same as #14555.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14556Core Lint error: Illkinded result in coercion20190707T18:16:31ZIcelandjackCore Lint error: Illkinded result in coercion```hs
{# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #}
import Data.Kind
import Data.Proxy
data Fn a b where
IdSym :: Fn Type Type
type family
(@@) (f::Fn k k') (a::k)::k' where
IdSym @@ a = a
data KIND = X  FNARR KIND KIND
data TY :: KIND > Type where
ID :: TY (FNARR X X)
FNAPP :: TY (FNARR k k') > TY k > TY k'
data TyRep (kind::KIND) :: TY kind > Type where
TID :: TyRep (FNARR X X) ID
TFnApp :: TyRep (FNARR k k') f
> TyRep k a
> TyRep k' (FNAPP f a)
type family
IK (kind::KIND) :: Type where
IK X = Type
IK (FNARR k k') = Fn (IK k) (IK k')
type family
IT (ty::TY kind) :: IK kind where
IT ID = IdSym
IT (FNAPP f x) = IT f @@ IT x
zero :: TyRep X a > IT a
zero = undefined
```
which gives Core lint error when run with `ghci ignoredotghci dcorelint` (8.3.20171122) attached.
It compiles fine with
```hs
zero :: TyRep X a > IT a
zero = zero
```
but fails with `zero = let x = x in x`. See #14554.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Core Lint error: Illkinded result in coercion","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #}\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\ndata Fn a b where\r\n IdSym :: Fn Type Type\r\n\r\ntype family\r\n (@@) (f::Fn k k') (a::k)::k' where\r\n IdSym @@ a = a\r\n\r\ndata KIND = X  FNARR KIND KIND\r\n\r\ndata TY :: KIND > Type where\r\n ID :: TY (FNARR X X)\r\n FNAPP :: TY (FNARR k k') > TY k > TY k'\r\n\r\ndata TyRep (kind::KIND) :: TY kind > Type where\r\n TID :: TyRep (FNARR X X) ID\r\n TFnApp :: TyRep (FNARR k k') f\r\n > TyRep k a\r\n > TyRep k' (FNAPP f a)\r\n\r\ntype family\r\n IK (kind::KIND) :: Type where\r\n IK X = Type\r\n IK (FNARR k k') = Fn (IK k) (IK k')\r\n\r\ntype family\r\n IT (ty::TY kind) :: IK kind where\r\n IT ID = IdSym\r\n IT (FNAPP f x) = IT f @@ IT x\r\n\r\nzero :: TyRep X a > IT a\r\nzero = undefined \r\n}}}\r\n\r\nwhich gives Core lint error when run with `ghci ignoredotghci dcorelint` (8.3.20171122) attached. \r\n\r\nIt compiles fine with\r\n\r\n{{{#!hs\r\nzero :: TyRep X a > IT a\r\nzero = zero\r\n}}}\r\n\r\nbut fails with `zero = let x = x in x`. See #14554.","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #}
import Data.Kind
import Data.Proxy
data Fn a b where
IdSym :: Fn Type Type
type family
(@@) (f::Fn k k') (a::k)::k' where
IdSym @@ a = a
data KIND = X  FNARR KIND KIND
data TY :: KIND > Type where
ID :: TY (FNARR X X)
FNAPP :: TY (FNARR k k') > TY k > TY k'
data TyRep (kind::KIND) :: TY kind > Type where
TID :: TyRep (FNARR X X) ID
TFnApp :: TyRep (FNARR k k') f
> TyRep k a
> TyRep k' (FNAPP f a)
type family
IK (kind::KIND) :: Type where
IK X = Type
IK (FNARR k k') = Fn (IK k) (IK k')
type family
IT (ty::TY kind) :: IK kind where
IT ID = IdSym
IT (FNAPP f x) = IT f @@ IT x
zero :: TyRep X a > IT a
zero = undefined
```
which gives Core lint error when run with `ghci ignoredotghci dcorelint` (8.3.20171122) attached.
It compiles fine with
```hs
zero :: TyRep X a > IT a
zero = zero
```
but fails with `zero = let x = x in x`. See #14554.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Core Lint error: Illkinded result in coercion","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #}\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\ndata Fn a b where\r\n IdSym :: Fn Type Type\r\n\r\ntype family\r\n (@@) (f::Fn k k') (a::k)::k' where\r\n IdSym @@ a = a\r\n\r\ndata KIND = X  FNARR KIND KIND\r\n\r\ndata TY :: KIND > Type where\r\n ID :: TY (FNARR X X)\r\n FNAPP :: TY (FNARR k k') > TY k > TY k'\r\n\r\ndata TyRep (kind::KIND) :: TY kind > Type where\r\n TID :: TyRep (FNARR X X) ID\r\n TFnApp :: TyRep (FNARR k k') f\r\n > TyRep k a\r\n > TyRep k' (FNAPP f a)\r\n\r\ntype family\r\n IK (kind::KIND) :: Type where\r\n IK X = Type\r\n IK (FNARR k k') = Fn (IK k) (IK k')\r\n\r\ntype family\r\n IT (ty::TY kind) :: IK kind where\r\n IT ID = IdSym\r\n IT (FNAPP f x) = IT f @@ IT x\r\n\r\nzero :: TyRep X a > IT a\r\nzero = undefined \r\n}}}\r\n\r\nwhich gives Core lint error when run with `ghci ignoredotghci dcorelint` (8.3.20171122) attached. \r\n\r\nIt compiles fine with\r\n\r\n{{{#!hs\r\nzero :: TyRep X a > IT a\r\nzero = zero\r\n}}}\r\n\r\nbut fails with `zero = let x = x in x`. See #14554.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14555GHC Panic with TypeInType / levity polymorphism20190707T18:16:32ZIcelandjackGHC Panic with TypeInType / levity polymorphism```hs
{# Language TypeInType #}
{# Language TypeOperators, DataKinds, PolyKinds #}
import Data.Kind
import GHC.Types (TYPE)
data Exp :: [TYPE rep] > TYPE rep > Type where
Lam :: Exp (a:xs) b > Exp xs (a > b)
```
gives
```
$ ghci ignoredotghci hs/126bug.hs
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( hs/126bug.hs, interpreted )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171122 for x86_64unknownlinux):
zonkTcTyVarToVar
'LiftedRep
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcType.hs:1640:17 in ghc:TcType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
caused by `TypeInType`. Removing the first line, we get an error
```
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( hs/126bug.hs, interpreted )
hs/126bug.hs:7:19: error:
• Expected kind ‘GHC.Types.RuntimeRep’, but ‘rep’ has kind ‘*’
• In the first argument of ‘TYPE’, namely ‘rep’
In the kind ‘[TYPE rep] > TYPE rep > Type’

7  data Exp :: [TYPE rep] > TYPE rep > Type where
 ^^^
hs/126bug.hs:7:32: error:
• Expected kind ‘GHC.Types.RuntimeRep’, but ‘rep’ has kind ‘*’
• In the first argument of ‘TYPE’, namely ‘rep’
In the kind ‘[TYPE rep] > TYPE rep > Type’

7  data Exp :: [TYPE rep] > TYPE rep > Type where
 ^^^
Failed, no modules loaded.
Prelude>
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC Panic with TypeInType / levity polymorphism","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["LevityPolymorphism,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# Language TypeInType #}\r\n{# Language TypeOperators, DataKinds, PolyKinds #}\r\n\r\nimport Data.Kind\r\nimport GHC.Types (TYPE)\r\n\r\ndata Exp :: [TYPE rep] > TYPE rep > Type where\r\n Lam :: Exp (a:xs) b > Exp xs (a > b)\r\n}}}\r\n\r\ngives\r\n\r\n{{{\r\n$ ghci ignoredotghci hs/126bug.hs\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( hs/126bug.hs, interpreted )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171122 for x86_64unknownlinux):\r\n\tzonkTcTyVarToVar\r\n 'LiftedRep\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcType.hs:1640:17 in ghc:TcType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\ncaused by `TypeInType`. Removing the first line, we get an error\r\n\r\n{{{\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( hs/126bug.hs, interpreted )\r\n\r\nhs/126bug.hs:7:19: error:\r\n • Expected kind ‘GHC.Types.RuntimeRep’, but ‘rep’ has kind ‘*’\r\n • In the first argument of ‘TYPE’, namely ‘rep’\r\n In the kind ‘[TYPE rep] > TYPE rep > Type’\r\n \r\n7  data Exp :: [TYPE rep] > TYPE rep > Type where\r\n  ^^^\r\n\r\nhs/126bug.hs:7:32: error:\r\n • Expected kind ‘GHC.Types.RuntimeRep’, but ‘rep’ has kind ‘*’\r\n • In the first argument of ‘TYPE’, namely ‘rep’\r\n In the kind ‘[TYPE rep] > TYPE rep > Type’\r\n \r\n7  data Exp :: [TYPE rep] > TYPE rep > Type where\r\n  ^^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >```hs
{# Language TypeInType #}
{# Language TypeOperators, DataKinds, PolyKinds #}
import Data.Kind
import GHC.Types (TYPE)
data Exp :: [TYPE rep] > TYPE rep > Type where
Lam :: Exp (a:xs) b > Exp xs (a > b)
```
gives
```
$ ghci ignoredotghci hs/126bug.hs
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( hs/126bug.hs, interpreted )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171122 for x86_64unknownlinux):
zonkTcTyVarToVar
'LiftedRep
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcType.hs:1640:17 in ghc:TcType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
caused by `TypeInType`. Removing the first line, we get an error
```
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( hs/126bug.hs, interpreted )
hs/126bug.hs:7:19: error:
• Expected kind ‘GHC.Types.RuntimeRep’, but ‘rep’ has kind ‘*’
• In the first argument of ‘TYPE’, namely ‘rep’
In the kind ‘[TYPE rep] > TYPE rep > Type’

7  data Exp :: [TYPE rep] > TYPE rep > Type where
 ^^^
hs/126bug.hs:7:32: error:
• Expected kind ‘GHC.Types.RuntimeRep’, but ‘rep’ has kind ‘*’
• In the first argument of ‘TYPE’, namely ‘rep’
In the kind ‘[TYPE rep] > TYPE rep > Type’

7  data Exp :: [TYPE rep] > TYPE rep > Type where
 ^^^
Failed, no modules loaded.
Prelude>
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC Panic with TypeInType / levity polymorphism","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["LevityPolymorphism,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{# Language TypeInType #}\r\n{# Language TypeOperators, DataKinds, PolyKinds #}\r\n\r\nimport Data.Kind\r\nimport GHC.Types (TYPE)\r\n\r\ndata Exp :: [TYPE rep] > TYPE rep > Type where\r\n Lam :: Exp (a:xs) b > Exp xs (a > b)\r\n}}}\r\n\r\ngives\r\n\r\n{{{\r\n$ ghci ignoredotghci hs/126bug.hs\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( hs/126bug.hs, interpreted )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171122 for x86_64unknownlinux):\r\n\tzonkTcTyVarToVar\r\n 'LiftedRep\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcType.hs:1640:17 in ghc:TcType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\ncaused by `TypeInType`. Removing the first line, we get an error\r\n\r\n{{{\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( hs/126bug.hs, interpreted )\r\n\r\nhs/126bug.hs:7:19: error:\r\n • Expected kind ‘GHC.Types.RuntimeRep’, but ‘rep’ has kind ‘*’\r\n • In the first argument of ‘TYPE’, namely ‘rep’\r\n In the kind ‘[TYPE rep] > TYPE rep > Type’\r\n \r\n7  data Exp :: [TYPE rep] > TYPE rep > Type where\r\n  ^^^\r\n\r\nhs/126bug.hs:7:32: error:\r\n • Expected kind ‘GHC.Types.RuntimeRep’, but ‘rep’ has kind ‘*’\r\n • In the first argument of ‘TYPE’, namely ‘rep’\r\n In the kind ‘[TYPE rep] > TYPE rep > Type’\r\n \r\n7  data Exp :: [TYPE rep] > TYPE rep > Type where\r\n  ^^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >