GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20190707T18:42:55Zhttps://gitlab.haskell.org/ghc/ghc//issues/8893XPolyKinds causes "*** Exception: Prelude.(!!): index too large"20190707T18:42:55ZghornXPolyKinds causes "*** Exception: Prelude.(!!): index too large"The following program will compile fine:
```
{# OPTIONS_GHC Wall #}
{# Language DeriveFunctor #}
{# Language PolyKinds #}
module Bug where
data V a = V [a] deriving Functor
data C x a = C (V (P x a)) deriving Functor
data P x a = P (x a) deriving Functor
```
But when PolyKinds is enabled, GHC crashes with
```
$ ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:9:37:ghc: panic! (the 'impossible' happened)
(GHC version 7.8.0.20140228 for x86_64unknownlinux):
Prelude.(!!): index too large
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.8.1rc2 
 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":"XPolyKinds causes \"*** Exception: Prelude.(!!): index too large\"","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.1rc2","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program will compile fine:\r\n{{{\r\n{# OPTIONS_GHC Wall #}\r\n{# Language DeriveFunctor #}\r\n{# Language PolyKinds #}\r\n\r\nmodule Bug where\r\n\r\ndata V a = V [a] deriving Functor\r\n\r\ndata C x a = C (V (P x a)) deriving Functor\r\n\r\ndata P x a = P (x a) deriving Functor\r\n}}}\r\n\r\nBut when PolyKinds is enabled, GHC crashes with\r\n\r\n{{{\r\n$ ghc Bug.hs \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:9:37:ghc: panic! (the 'impossible' happened)\r\n (GHC version 7.8.0.20140228 for x86_64unknownlinux):\r\n\tPrelude.(!!): index too large\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >The following program will compile fine:
```
{# OPTIONS_GHC Wall #}
{# Language DeriveFunctor #}
{# Language PolyKinds #}
module Bug where
data V a = V [a] deriving Functor
data C x a = C (V (P x a)) deriving Functor
data P x a = P (x a) deriving Functor
```
But when PolyKinds is enabled, GHC crashes with
```
$ ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:9:37:ghc: panic! (the 'impossible' happened)
(GHC version 7.8.0.20140228 for x86_64unknownlinux):
Prelude.(!!): index too large
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.8.1rc2 
 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":"XPolyKinds causes \"*** Exception: Prelude.(!!): index too large\"","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.1rc2","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program will compile fine:\r\n{{{\r\n{# OPTIONS_GHC Wall #}\r\n{# Language DeriveFunctor #}\r\n{# Language PolyKinds #}\r\n\r\nmodule Bug where\r\n\r\ndata V a = V [a] deriving Functor\r\n\r\ndata C x a = C (V (P x a)) deriving Functor\r\n\r\ndata P x a = P (x a) deriving Functor\r\n}}}\r\n\r\nBut when PolyKinds is enabled, GHC crashes with\r\n\r\n{{{\r\n$ ghc Bug.hs \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:9:37:ghc: panic! (the 'impossible' happened)\r\n (GHC version 7.8.0.20140228 for x86_64unknownlinux):\r\n\tPrelude.(!!): index too large\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >7.8.1https://gitlab.haskell.org/ghc/ghc//issues/7477reifyInstances can't deal with polykinded type families20190707T18:49:34ZRichard Eisenbergrae@richarde.devreifyInstances can't deal with polykinded type familiesWhen I run the following code
```
{# LANGUAGE DataKinds, KindSignatures, PolyKinds, TypeFamilies, TemplateHaskell #}
import Language.Haskell.TH
type family F (a :: k)
type instance F Int = Bool
$( do { info < reifyInstances ''F [ConT ''Int]
; reportWarning (pprint info)
; return [] })
```
I get this error:
```
Wrong number of types (expected 2)
In the argument of reifyInstances: Main.F GHC.Types.Int
```
I assumed that TH wanted me to supply the kind parameter, so I tried this:
```
...
$( do { info < reifyInstances ''F [StarT, ConT ''Int]
...
```
I got this response:
```
`F' is applied to too many type arguments
In the argument of reifyInstances: Main.F * GHC.Types.Int
```
I poked around in the code to see what might be causing it. I found a couple of interesting things:
 `reifyInstances` uses `tyConArity` to get the arity of a type family. For my `F`, `tyConArity` reported 3. So, I wrote some code to go through the kind and count only nonsuperkind arguments. This didn't fix the problem, because ...
 `reifyInstances` passes control off, through a handful of other functions, to `matchExpectedFunKind`, which works only with `FunTy`, not `ForAllTy`. So, my `F`, whose kind is headed by `ForAllTy`, looks like it takes no arguments at all.
I could try to fix this, but I'm worried about upsetting the apple cart here. If a knowledgeable individual could give some pointers about what's safe and what's not safe to change in this code, I'm happy to write the fix.
This was all tested on 7.7.20121130.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.7 
 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":"reifyInstances can't deal with polykinded type families","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.7","keywords":["PolyKinds","TemplateHaskell","TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I run the following code\r\n\r\n{{{\r\n{# LANGUAGE DataKinds, KindSignatures, PolyKinds, TypeFamilies, TemplateHaskell #}\r\n\r\nimport Language.Haskell.TH\r\n\r\ntype family F (a :: k)\r\ntype instance F Int = Bool\r\n\r\n$( do { info < reifyInstances ''F [ConT ''Int]\r\n ; reportWarning (pprint info)\r\n ; return [] })\r\n}}}\r\n\r\nI get this error:\r\n\r\n{{{\r\n Wrong number of types (expected 2)\r\n In the argument of reifyInstances: Main.F GHC.Types.Int\r\n}}}\r\n\r\nI assumed that TH wanted me to supply the kind parameter, so I tried this:\r\n\r\n{{{\r\n...\r\n$( do { info < reifyInstances ''F [StarT, ConT ''Int]\r\n...\r\n}}}\r\n\r\nI got this response:\r\n\r\n{{{\r\n `F' is applied to too many type arguments\r\n In the argument of reifyInstances: Main.F * GHC.Types.Int\r\n}}}\r\n\r\nI poked around in the code to see what might be causing it. I found a couple of interesting things:\r\n\r\n * {{{reifyInstances}}} uses {{{tyConArity}}} to get the arity of a type family. For my {{{F}}}, {{{tyConArity}}} reported 3. So, I wrote some code to go through the kind and count only nonsuperkind arguments. This didn't fix the problem, because ...\r\n * {{{reifyInstances}}} passes control off, through a handful of other functions, to {{{matchExpectedFunKind}}}, which works only with {{{FunTy}}}, not {{{ForAllTy}}}. So, my {{{F}}}, whose kind is headed by {{{ForAllTy}}}, looks like it takes no arguments at all.\r\n\r\nI could try to fix this, but I'm worried about upsetting the apple cart here. If a knowledgeable individual could give some pointers about what's safe and what's not safe to change in this code, I'm happy to write the fix.\r\n\r\nThis was all tested on 7.7.20121130.\r\n","type_of_failure":"OtherFailure","blocking":[]} >When I run the following code
```
{# LANGUAGE DataKinds, KindSignatures, PolyKinds, TypeFamilies, TemplateHaskell #}
import Language.Haskell.TH
type family F (a :: k)
type instance F Int = Bool
$( do { info < reifyInstances ''F [ConT ''Int]
; reportWarning (pprint info)
; return [] })
```
I get this error:
```
Wrong number of types (expected 2)
In the argument of reifyInstances: Main.F GHC.Types.Int
```
I assumed that TH wanted me to supply the kind parameter, so I tried this:
```
...
$( do { info < reifyInstances ''F [StarT, ConT ''Int]
...
```
I got this response:
```
`F' is applied to too many type arguments
In the argument of reifyInstances: Main.F * GHC.Types.Int
```
I poked around in the code to see what might be causing it. I found a couple of interesting things:
 `reifyInstances` uses `tyConArity` to get the arity of a type family. For my `F`, `tyConArity` reported 3. So, I wrote some code to go through the kind and count only nonsuperkind arguments. This didn't fix the problem, because ...
 `reifyInstances` passes control off, through a handful of other functions, to `matchExpectedFunKind`, which works only with `FunTy`, not `ForAllTy`. So, my `F`, whose kind is headed by `ForAllTy`, looks like it takes no arguments at all.
I could try to fix this, but I'm worried about upsetting the apple cart here. If a knowledgeable individual could give some pointers about what's safe and what's not safe to change in this code, I'm happy to write the fix.
This was all tested on 7.7.20121130.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.7 
 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":"reifyInstances can't deal with polykinded type families","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.7","keywords":["PolyKinds","TemplateHaskell","TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I run the following code\r\n\r\n{{{\r\n{# LANGUAGE DataKinds, KindSignatures, PolyKinds, TypeFamilies, TemplateHaskell #}\r\n\r\nimport Language.Haskell.TH\r\n\r\ntype family F (a :: k)\r\ntype instance F Int = Bool\r\n\r\n$( do { info < reifyInstances ''F [ConT ''Int]\r\n ; reportWarning (pprint info)\r\n ; return [] })\r\n}}}\r\n\r\nI get this error:\r\n\r\n{{{\r\n Wrong number of types (expected 2)\r\n In the argument of reifyInstances: Main.F GHC.Types.Int\r\n}}}\r\n\r\nI assumed that TH wanted me to supply the kind parameter, so I tried this:\r\n\r\n{{{\r\n...\r\n$( do { info < reifyInstances ''F [StarT, ConT ''Int]\r\n...\r\n}}}\r\n\r\nI got this response:\r\n\r\n{{{\r\n `F' is applied to too many type arguments\r\n In the argument of reifyInstances: Main.F * GHC.Types.Int\r\n}}}\r\n\r\nI poked around in the code to see what might be causing it. I found a couple of interesting things:\r\n\r\n * {{{reifyInstances}}} uses {{{tyConArity}}} to get the arity of a type family. For my {{{F}}}, {{{tyConArity}}} reported 3. So, I wrote some code to go through the kind and count only nonsuperkind arguments. This didn't fix the problem, because ...\r\n * {{{reifyInstances}}} passes control off, through a handful of other functions, to {{{matchExpectedFunKind}}}, which works only with {{{FunTy}}}, not {{{ForAllTy}}}. So, my {{{F}}}, whose kind is headed by {{{ForAllTy}}}, looks like it takes no arguments at all.\r\n\r\nI could try to fix this, but I'm worried about upsetting the apple cart here. If a knowledgeable individual could give some pointers about what's safe and what's not safe to change in this code, I'm happy to write the fix.\r\n\r\nThis was all tested on 7.7.20121130.\r\n","type_of_failure":"OtherFailure","blocking":[]} >7.8.1https://gitlab.haskell.org/ghc/ghc//issues/5682Properly parse promoted data constructor operators20190707T18:54:04ZlunarisProperly parse promoted data constructor operators```
% ghci XPolyKinds XTypeOperators
GHCi, version 7.3.20111204: http://www.haskell.org/ghc/ :? for help
Loading package ghcprim ... linking ... done.
Loading package integergmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :k (:)
<interactive>:1:2: parse error on input `:'
Prelude> :k '(:)
<interactive>:1:3: parse error on input `:'
Prelude> :k (':)
<interactive>:1:3: parse error on input `:'
Prelude> :k (Int ': '[Bool])
(Int ': '[Bool]) :: [*]
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.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":"Cannot parse (:) in a KindSignature with XPolyKinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"dreixel"},"version":"7.3","keywords":["PolyKinds,","ghckinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\n% ghci XPolyKinds XTypeOperators\r\nGHCi, version 7.3.20111204: http://www.haskell.org/ghc/ :? for help\r\nLoading package ghcprim ... linking ... done.\r\nLoading package integergmp ... linking ... done.\r\nLoading package base ... linking ... done.\r\nPrelude> :k (:)\r\n\r\n<interactive>:1:2: parse error on input `:'\r\nPrelude> :k '(:)\r\n\r\n<interactive>:1:3: parse error on input `:'\r\nPrelude> :k (':)\r\n\r\n<interactive>:1:3: parse error on input `:'\r\nPrelude> :k (Int ': '[Bool])\r\n(Int ': '[Bool]) :: [*]\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >```
% ghci XPolyKinds XTypeOperators
GHCi, version 7.3.20111204: http://www.haskell.org/ghc/ :? for help
Loading package ghcprim ... linking ... done.
Loading package integergmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :k (:)
<interactive>:1:2: parse error on input `:'
Prelude> :k '(:)
<interactive>:1:3: parse error on input `:'
Prelude> :k (':)
<interactive>:1:3: parse error on input `:'
Prelude> :k (Int ': '[Bool])
(Int ': '[Bool]) :: [*]
```
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.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":"Cannot parse (:) in a KindSignature with XPolyKinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"dreixel"},"version":"7.3","keywords":["PolyKinds,","ghckinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\n% ghci XPolyKinds XTypeOperators\r\nGHCi, version 7.3.20111204: http://www.haskell.org/ghc/ :? for help\r\nLoading package ghcprim ... linking ... done.\r\nLoading package integergmp ... linking ... done.\r\nLoading package base ... linking ... done.\r\nPrelude> :k (:)\r\n\r\n<interactive>:1:2: parse error on input `:'\r\nPrelude> :k '(:)\r\n\r\n<interactive>:1:3: parse error on input `:'\r\nPrelude> :k (':)\r\n\r\n<interactive>:1:3: parse error on input `:'\r\nPrelude> :k (Int ': '[Bool])\r\n(Int ': '[Bool]) :: [*]\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >7.8.1https://gitlab.haskell.org/ghc/ghc//issues/9633PolyKinds in 7.8.2 vs 7.8.320190707T18:39:44ZEric CrockettPolyKinds in 7.8.2 vs 7.8.3The following code **compiles** with GHC 7.8.2.
This code has been distilled down from a larger example where I needed `XPolyKinds` in Bar.hs but not in Foo.hs. In addition, the `modify` function is supposed to modify a mutable `Data.Vector`, hence the inner `go` function has the intended type of `Int > m ()`, though strictly speaking it could return any value since everything is discarded by the `forM_`.
```
 {# LANGUAGE PolyKinds #}
module Foo where
import Control.Monad (forM_)
import Bar
 Vector signatures
unsafeRead :: (Monad m) => v (PrimState m) a > Int > m a
unsafeRead = error "type only"
unsafeWrite :: (Monad m) => v (PrimState m) a > Int > a > m ()
unsafeWrite = error "type only"
modify :: Int > Bar v r
modify p = Bar (p1) $ \y > do
let go i = do
a < unsafeRead y i
unsafeWrite y i a
return a
forM_ [0..(p1)] go
```
```
{# LANGUAGE RankNTypes, KindSignatures, TypeFamilies, PolyKinds #}
module Bar where
type family PrimState (m :: * > *) :: *
data Bar v r = Bar Int (forall s . (Monad s) => v (PrimState s) r > s ())
```
In 7.8.3, this above code results in the error (with `fprintexplicitkinds`)
```
Foo.hs:19:23:
Couldn't match type ‘a0’ with ‘r’
‘a0’ is untouchable
inside the constraints (Monad m,
(~) * (PrimState m) (PrimState s))
bound by the inferred type of
go :: (Monad m, (~) * (PrimState m) (PrimState s)) =>
Int > m ()
at Foo.hs:(18,7)(20,23)
‘r’ is a rigid type variable bound by
the type signature for modify :: Int > Bar * v r at Foo.hs:16:11
Expected type: v0 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeRead’, namely ‘y’
In a stmt of a 'do' block: a < unsafeRead y i
Foo.hs:20:19:
Couldn't match type ‘v1’ with ‘v’
‘v1’ is untouchable
inside the constraints (Monad m,
(~) * (PrimState m) (PrimState s))
bound by the inferred type of
go :: (Monad m, (~) * (PrimState m) (PrimState s)) =>
Int > m ()
at Foo.hs:(18,7)(20,23)
‘v’ is a rigid type variable bound by
the type signature for modify :: Int > Bar * v r at Foo.hs:16:11
Expected type: v1 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeWrite’, namely ‘y’
...
Failed, modules loaded: Bar.
```
After much digging, I found that enabling `XPolyKinds` in Foo.hs gives a more meaningful error:
```
Foo.hs:19:23:
Could not deduce ((~) (* > k > *) v v0)
...
Expected type: v0 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeRead’, namely ‘y’
In a stmt of a 'do' block: a < unsafeRead y i
Foo.hs:20:19:
Could not deduce ((~) (* > k > *) v v1)
...
Expected type: v1 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeWrite’, namely ‘y’
In a stmt of a 'do' block: unsafeWrite y i a
Failed, modules loaded: Bar.
```
Adding `PolyKinds` to Foo.hs *and* uncommenting `return a` results in the error:
```
Foo.hs:17:12:
Couldn't match kind ‘k’ with ‘k1’
because type variable ‘k1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for modify :: Int > Bar k1 v r
at Foo.hs:16:1124
Expected type: Bar k1 v r
Actual type: Bar k v0 r0
...
In the expression:
Bar (p  1)
$ \ y
> do { let ...;
forM_ [0 .. (p  1)] go }
...
Foo.hs:18:7:
Kind incompatibility when matching types:
v0 :: * > k > *
v1 :: * > * > *
...
When checking that ‘go’
has the inferred type ‘forall (k :: BOX)
(m :: * > *)
b
(v :: * > * > *)
(v1 :: * > * > *).
((~) (* > k > *) v0 v, (~) k r0 b, (~) (* > k > *) v0 v1,
Monad m, (~) * (PrimState m) (PrimState s)) =>
Int > m b’
Probable cause: the inferred type is ambiguous
In the expression:
do { let go i = ...;
forM_ [0 .. (p  1)] go }
...
Failed, modules loaded: Bar.
```
These errors can be resolved by modifying the original code above in any of the following ways:
1. Remove `XPolyKinds` from Bar.hs
1. Add an explicit kind signature to the `v :: * > * > *` parameter of type `Bar`
1. With `PolyKinds` in Bar but \*not\* Foo, uncommenting `return a` make GHC 7.8.3. compile
What I'm trying to understand is
1. Why there is different behavior from 7.8.2 to 7.8.3. There doesn't seem to be anything addressing `PolyKinds` in the [release notes vs 7.8.2](http://www.haskell.org/ghc/docs/7.8.3/html/users_guide/release783.html) .
1. In the event the above code should not compile with 7.8.3, there error message could be much clearer. The first error message above didn't help me understand that `PolyKinds` was to blame, while the second error did a better job, and the third was very clearly a `PolyKinds` issue (i.e. `kind mismatch`)
1. For the third resolution option above, I can't see any reason that adding `return a` to the inner `go` function should make the code compile while leaving it out makes the code somehow ambiguous. This, if nothing else, seems like a bug.The following code **compiles** with GHC 7.8.2.
This code has been distilled down from a larger example where I needed `XPolyKinds` in Bar.hs but not in Foo.hs. In addition, the `modify` function is supposed to modify a mutable `Data.Vector`, hence the inner `go` function has the intended type of `Int > m ()`, though strictly speaking it could return any value since everything is discarded by the `forM_`.
```
 {# LANGUAGE PolyKinds #}
module Foo where
import Control.Monad (forM_)
import Bar
 Vector signatures
unsafeRead :: (Monad m) => v (PrimState m) a > Int > m a
unsafeRead = error "type only"
unsafeWrite :: (Monad m) => v (PrimState m) a > Int > a > m ()
unsafeWrite = error "type only"
modify :: Int > Bar v r
modify p = Bar (p1) $ \y > do
let go i = do
a < unsafeRead y i
unsafeWrite y i a
return a
forM_ [0..(p1)] go
```
```
{# LANGUAGE RankNTypes, KindSignatures, TypeFamilies, PolyKinds #}
module Bar where
type family PrimState (m :: * > *) :: *
data Bar v r = Bar Int (forall s . (Monad s) => v (PrimState s) r > s ())
```
In 7.8.3, this above code results in the error (with `fprintexplicitkinds`)
```
Foo.hs:19:23:
Couldn't match type ‘a0’ with ‘r’
‘a0’ is untouchable
inside the constraints (Monad m,
(~) * (PrimState m) (PrimState s))
bound by the inferred type of
go :: (Monad m, (~) * (PrimState m) (PrimState s)) =>
Int > m ()
at Foo.hs:(18,7)(20,23)
‘r’ is a rigid type variable bound by
the type signature for modify :: Int > Bar * v r at Foo.hs:16:11
Expected type: v0 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeRead’, namely ‘y’
In a stmt of a 'do' block: a < unsafeRead y i
Foo.hs:20:19:
Couldn't match type ‘v1’ with ‘v’
‘v1’ is untouchable
inside the constraints (Monad m,
(~) * (PrimState m) (PrimState s))
bound by the inferred type of
go :: (Monad m, (~) * (PrimState m) (PrimState s)) =>
Int > m ()
at Foo.hs:(18,7)(20,23)
‘v’ is a rigid type variable bound by
the type signature for modify :: Int > Bar * v r at Foo.hs:16:11
Expected type: v1 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeWrite’, namely ‘y’
...
Failed, modules loaded: Bar.
```
After much digging, I found that enabling `XPolyKinds` in Foo.hs gives a more meaningful error:
```
Foo.hs:19:23:
Could not deduce ((~) (* > k > *) v v0)
...
Expected type: v0 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeRead’, namely ‘y’
In a stmt of a 'do' block: a < unsafeRead y i
Foo.hs:20:19:
Could not deduce ((~) (* > k > *) v v1)
...
Expected type: v1 (PrimState m) a0
Actual type: v (PrimState s) r
...
In the first argument of ‘unsafeWrite’, namely ‘y’
In a stmt of a 'do' block: unsafeWrite y i a
Failed, modules loaded: Bar.
```
Adding `PolyKinds` to Foo.hs *and* uncommenting `return a` results in the error:
```
Foo.hs:17:12:
Couldn't match kind ‘k’ with ‘k1’
because type variable ‘k1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for modify :: Int > Bar k1 v r
at Foo.hs:16:1124
Expected type: Bar k1 v r
Actual type: Bar k v0 r0
...
In the expression:
Bar (p  1)
$ \ y
> do { let ...;
forM_ [0 .. (p  1)] go }
...
Foo.hs:18:7:
Kind incompatibility when matching types:
v0 :: * > k > *
v1 :: * > * > *
...
When checking that ‘go’
has the inferred type ‘forall (k :: BOX)
(m :: * > *)
b
(v :: * > * > *)
(v1 :: * > * > *).
((~) (* > k > *) v0 v, (~) k r0 b, (~) (* > k > *) v0 v1,
Monad m, (~) * (PrimState m) (PrimState s)) =>
Int > m b’
Probable cause: the inferred type is ambiguous
In the expression:
do { let go i = ...;
forM_ [0 .. (p  1)] go }
...
Failed, modules loaded: Bar.
```
These errors can be resolved by modifying the original code above in any of the following ways:
1. Remove `XPolyKinds` from Bar.hs
1. Add an explicit kind signature to the `v :: * > * > *` parameter of type `Bar`
1. With `PolyKinds` in Bar but \*not\* Foo, uncommenting `return a` make GHC 7.8.3. compile
What I'm trying to understand is
1. Why there is different behavior from 7.8.2 to 7.8.3. There doesn't seem to be anything addressing `PolyKinds` in the [release notes vs 7.8.2](http://www.haskell.org/ghc/docs/7.8.3/html/users_guide/release783.html) .
1. In the event the above code should not compile with 7.8.3, there error message could be much clearer. The first error message above didn't help me understand that `PolyKinds` was to blame, while the second error did a better job, and the third was very clearly a `PolyKinds` issue (i.e. `kind mismatch`)
1. For the third resolution option above, I can't see any reason that adding `return a` to the inner `go` function should make the code compile while leaving it out makes the code somehow ambiguous. This, if nothing else, seems like a bug.7.10.1https://gitlab.haskell.org/ghc/ghc//issues/11480UndecidableSuperClasses causes the compiler to spin with UndecidableInstances20190707T18:30:14ZEdward KmettUndecidableSuperClasses causes the compiler to spin with UndecidableInstancesLooks like I spoke too soon when I said all my examples worked in #10318  it doesn't seem to work when the superclass cycle gets sufficiently interesting, possibly caused by the use of `PolyKinds` in the style mentioned in #9201.
I took my `hask` code, and removed the shimming hacks above, and the following stripped down example sends the compiler into an infinite loop, which I believe should be able to work:
```hs
{# language KindSignatures, PolyKinds, TypeFamilies,
NoImplicitPrelude, FlexibleContexts,
MultiParamTypeClasses, GADTs,
ConstraintKinds, FlexibleInstances,
FunctionalDependencies, UndecidableSuperClasses #}
import GHC.Types (Constraint)
import qualified Prelude
data Nat (c :: i > i > *) (d :: j > j > *) (f :: i > j) (g :: i > j)
class Functor p (Nat p (>)) p => Category (p :: i > i > *)
class (Category dom, Category cod) => Functor (dom :: i > i > *) (cod :: j > j > *) (f :: i > j)  f > dom cod
instance (Category c, Category d) => Category (Nat c d)
instance (Category c, Category d) => Functor (Nat c d) (Nat (Nat c d) (>)) (Nat c d)
instance (Category c, Category d) => Functor (Nat c d) (>) (Nat c d f)
instance Category (>)
instance Functor (>) (>) ((>) e)
instance Functor (>) (Nat (>) (>)) (>)
```
Sorry for the largish example, but I don't know how to strip it down smaller than the 6 instances that remain.
One potentially telling observation is that without the instances it compiles, and produces what I expect, so the `UndecidableSuperClasses` part seems to be letting the classes compile, but there seems to be a bad interaction with the way the instances work.
Also, in this stripped down form, I can remove the use of `UndecidableInstances` and that avoids the spinning problem, but once I flesh it out further I need `UndecidableInstances` in the "real" version of the problem.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.10.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"UndecidableSuperClasses causes the compiler to spin with UndecidableInstances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":["PolyKinds,","UndecidableSuperClasses"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Looks like I spoke too soon when I said all my examples worked in #10318  it doesn't seem to work when the superclass cycle gets sufficiently interesting, possibly caused by the use of `PolyKinds` in the style mentioned in #9201.\r\n\r\nI took my `hask` code, and removed the shimming hacks above, and the following stripped down example sends the compiler into an infinite loop, which I believe should be able to work:\r\n\r\n{{{#!hs\r\n{# language KindSignatures, PolyKinds, TypeFamilies, \r\n NoImplicitPrelude, FlexibleContexts,\r\n MultiParamTypeClasses, GADTs, \r\n ConstraintKinds, FlexibleInstances, \r\n FunctionalDependencies, UndecidableSuperClasses #}\r\n\r\nimport GHC.Types (Constraint)\r\nimport qualified Prelude\r\n\r\ndata Nat (c :: i > i > *) (d :: j > j > *) (f :: i > j) (g :: i > j)\r\n\r\nclass Functor p (Nat p (>)) p => Category (p :: i > i > *)\r\nclass (Category dom, Category cod) => Functor (dom :: i > i > *) (cod :: j > j > *) (f :: i > j)  f > dom cod\r\n\r\ninstance (Category c, Category d) => Category (Nat c d)\r\ninstance (Category c, Category d) => Functor (Nat c d) (Nat (Nat c d) (>)) (Nat c d)\r\ninstance (Category c, Category d) => Functor (Nat c d) (>) (Nat c d f)\r\n\r\ninstance Category (>)\r\ninstance Functor (>) (>) ((>) e)\r\ninstance Functor (>) (Nat (>) (>)) (>)\r\n}}}\r\n\r\nSorry for the largish example, but I don't know how to strip it down smaller than the 6 instances that remain.\r\n\r\nOne potentially telling observation is that without the instances it compiles, and produces what I expect, so the `UndecidableSuperClasses` part seems to be letting the classes compile, but there seems to be a bad interaction with the way the instances work.\r\n\r\nAlso, in this stripped down form, I can remove the use of `UndecidableInstances` and that avoids the spinning problem, but once I flesh it out further I need `UndecidableInstances` in the \"real\" version of the problem.","type_of_failure":"OtherFailure","blocking":[]} >Looks like I spoke too soon when I said all my examples worked in #10318  it doesn't seem to work when the superclass cycle gets sufficiently interesting, possibly caused by the use of `PolyKinds` in the style mentioned in #9201.
I took my `hask` code, and removed the shimming hacks above, and the following stripped down example sends the compiler into an infinite loop, which I believe should be able to work:
```hs
{# language KindSignatures, PolyKinds, TypeFamilies,
NoImplicitPrelude, FlexibleContexts,
MultiParamTypeClasses, GADTs,
ConstraintKinds, FlexibleInstances,
FunctionalDependencies, UndecidableSuperClasses #}
import GHC.Types (Constraint)
import qualified Prelude
data Nat (c :: i > i > *) (d :: j > j > *) (f :: i > j) (g :: i > j)
class Functor p (Nat p (>)) p => Category (p :: i > i > *)
class (Category dom, Category cod) => Functor (dom :: i > i > *) (cod :: j > j > *) (f :: i > j)  f > dom cod
instance (Category c, Category d) => Category (Nat c d)
instance (Category c, Category d) => Functor (Nat c d) (Nat (Nat c d) (>)) (Nat c d)
instance (Category c, Category d) => Functor (Nat c d) (>) (Nat c d f)
instance Category (>)
instance Functor (>) (>) ((>) e)
instance Functor (>) (Nat (>) (>)) (>)
```
Sorry for the largish example, but I don't know how to strip it down smaller than the 6 instances that remain.
One potentially telling observation is that without the instances it compiles, and produces what I expect, so the `UndecidableSuperClasses` part seems to be letting the classes compile, but there seems to be a bad interaction with the way the instances work.
Also, in this stripped down form, I can remove the use of `UndecidableInstances` and that avoids the spinning problem, but once I flesh it out further I need `UndecidableInstances` in the "real" version of the problem.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.10.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"UndecidableSuperClasses causes the compiler to spin with UndecidableInstances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":["PolyKinds,","UndecidableSuperClasses"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Looks like I spoke too soon when I said all my examples worked in #10318  it doesn't seem to work when the superclass cycle gets sufficiently interesting, possibly caused by the use of `PolyKinds` in the style mentioned in #9201.\r\n\r\nI took my `hask` code, and removed the shimming hacks above, and the following stripped down example sends the compiler into an infinite loop, which I believe should be able to work:\r\n\r\n{{{#!hs\r\n{# language KindSignatures, PolyKinds, TypeFamilies, \r\n NoImplicitPrelude, FlexibleContexts,\r\n MultiParamTypeClasses, GADTs, \r\n ConstraintKinds, FlexibleInstances, \r\n FunctionalDependencies, UndecidableSuperClasses #}\r\n\r\nimport GHC.Types (Constraint)\r\nimport qualified Prelude\r\n\r\ndata Nat (c :: i > i > *) (d :: j > j > *) (f :: i > j) (g :: i > j)\r\n\r\nclass Functor p (Nat p (>)) p => Category (p :: i > i > *)\r\nclass (Category dom, Category cod) => Functor (dom :: i > i > *) (cod :: j > j > *) (f :: i > j)  f > dom cod\r\n\r\ninstance (Category c, Category d) => Category (Nat c d)\r\ninstance (Category c, Category d) => Functor (Nat c d) (Nat (Nat c d) (>)) (Nat c d)\r\ninstance (Category c, Category d) => Functor (Nat c d) (>) (Nat c d f)\r\n\r\ninstance Category (>)\r\ninstance Functor (>) (>) ((>) e)\r\ninstance Functor (>) (Nat (>) (>)) (>)\r\n}}}\r\n\r\nSorry for the largish example, but I don't know how to strip it down smaller than the 6 instances that remain.\r\n\r\nOne potentially telling observation is that without the instances it compiles, and produces what I expect, so the `UndecidableSuperClasses` part seems to be letting the classes compile, but there seems to be a bad interaction with the way the instances work.\r\n\r\nAlso, in this stripped down form, I can remove the use of `UndecidableInstances` and that avoids the spinning problem, but once I flesh it out further I need `UndecidableInstances` in the \"real\" version of the problem.","type_of_failure":"OtherFailure","blocking":[]} >8.0.1https://gitlab.haskell.org/ghc/ghc//issues/14450GHCi spins forever20190707T18:16:59ZIcelandjackGHCi spins foreverThe following code compiles just fine (8.3.20170920)
```hs
{# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #}
import Data.Kind
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
type Cat ob = ob > ob > Type
type SameKind (a :: k) (b :: k) = (() :: Constraint)
type family
Apply (f :: a ~> b) (x :: a) :: b where
Apply IddSym0 x = Idd x
class Varpi (f :: i ~> j) where
type Dom (f :: i ~> j) :: Cat i
type Cod (f :: i ~> j) :: Cat j
varpa :: Dom f a a' > Cod f (Apply f a) (Apply f a')
type family
Idd (a::k) :: k where
Idd (a::k) = a
data IddSym0 :: k ~> k where
IddSym0KindInference :: IddSym0 l
instance Varpi (IddSym0 :: Type ~> Type) where
type Dom (IddSym0 :: Type ~> Type) = (>)
type Cod (IddSym0 :: Type ~> Type) = (>)
varpa :: (a > a') > (a > a')
varpa = id
```
But if you change the final instance to
```hs
instance Varpi (IddSym0 :: k ~> k) where
type Dom (IddSym0 :: Type ~> Type) = (>)
```
it sends GHC for a spin.
<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":"GHCi spins forever","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PolyKinds","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code compiles just fine (8.3.20170920)\r\n\r\n{{{#!hs\r\n{# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #}\r\n\r\nimport Data.Kind\r\n\r\ndata TyFun :: Type > Type > Type\r\n\r\ntype a ~> b = TyFun a b > Type\r\n\r\ntype Cat ob = ob > ob > Type\r\n\r\ntype SameKind (a :: k) (b :: k) = (() :: Constraint)\r\n\r\ntype family \r\n Apply (f :: a ~> b) (x :: a) :: b where\r\n Apply IddSym0 x = Idd x\r\n\r\nclass Varpi (f :: i ~> j) where\r\n type Dom (f :: i ~> j) :: Cat i\r\n type Cod (f :: i ~> j) :: Cat j\r\n\r\n varpa :: Dom f a a' > Cod f (Apply f a) (Apply f a')\r\n\r\ntype family \r\n Idd (a::k) :: k where\r\n Idd (a::k) = a\r\n\r\ndata IddSym0 :: k ~> k where\r\n IddSym0KindInference :: IddSym0 l\r\n\r\ninstance Varpi (IddSym0 :: Type ~> Type) where\r\n type Dom (IddSym0 :: Type ~> Type) = (>)\r\n type Cod (IddSym0 :: Type ~> Type) = (>)\r\n\r\n varpa :: (a > a') > (a > a')\r\n varpa = id\r\n}}}\r\n\r\nBut if you change the final instance to\r\n\r\n{{{#!hs\r\ninstance Varpi (IddSym0 :: k ~> k) where\r\n type Dom (IddSym0 :: Type ~> Type) = (>)\r\n}}}\r\n\r\nit sends GHC for a spin.","type_of_failure":"OtherFailure","blocking":[]} >The following code compiles just fine (8.3.20170920)
```hs
{# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #}
import Data.Kind
data TyFun :: Type > Type > Type
type a ~> b = TyFun a b > Type
type Cat ob = ob > ob > Type
type SameKind (a :: k) (b :: k) = (() :: Constraint)
type family
Apply (f :: a ~> b) (x :: a) :: b where
Apply IddSym0 x = Idd x
class Varpi (f :: i ~> j) where
type Dom (f :: i ~> j) :: Cat i
type Cod (f :: i ~> j) :: Cat j
varpa :: Dom f a a' > Cod f (Apply f a) (Apply f a')
type family
Idd (a::k) :: k where
Idd (a::k) = a
data IddSym0 :: k ~> k where
IddSym0KindInference :: IddSym0 l
instance Varpi (IddSym0 :: Type ~> Type) where
type Dom (IddSym0 :: Type ~> Type) = (>)
type Cod (IddSym0 :: Type ~> Type) = (>)
varpa :: (a > a') > (a > a')
varpa = id
```
But if you change the final instance to
```hs
instance Varpi (IddSym0 :: k ~> k) where
type Dom (IddSym0 :: Type ~> Type) = (>)
```
it sends GHC for a spin.
<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":"GHCi spins forever","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PolyKinds","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code compiles just fine (8.3.20170920)\r\n\r\n{{{#!hs\r\n{# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #}\r\n\r\nimport Data.Kind\r\n\r\ndata TyFun :: Type > Type > Type\r\n\r\ntype a ~> b = TyFun a b > Type\r\n\r\ntype Cat ob = ob > ob > Type\r\n\r\ntype SameKind (a :: k) (b :: k) = (() :: Constraint)\r\n\r\ntype family \r\n Apply (f :: a ~> b) (x :: a) :: b where\r\n Apply IddSym0 x = Idd x\r\n\r\nclass Varpi (f :: i ~> j) where\r\n type Dom (f :: i ~> j) :: Cat i\r\n type Cod (f :: i ~> j) :: Cat j\r\n\r\n varpa :: Dom f a a' > Cod f (Apply f a) (Apply f a')\r\n\r\ntype family \r\n Idd (a::k) :: k where\r\n Idd (a::k) = a\r\n\r\ndata IddSym0 :: k ~> k where\r\n IddSym0KindInference :: IddSym0 l\r\n\r\ninstance Varpi (IddSym0 :: Type ~> Type) where\r\n type Dom (IddSym0 :: Type ~> Type) = (>)\r\n type Cod (IddSym0 :: Type ~> Type) = (>)\r\n\r\n varpa :: (a > a') > (a > a')\r\n varpa = id\r\n}}}\r\n\r\nBut if you change the final instance to\r\n\r\n{{{#!hs\r\ninstance Varpi (IddSym0 :: k ~> k) where\r\n type Dom (IddSym0 :: Type ~> Type) = (>)\r\n}}}\r\n\r\nit sends GHC for a spin.","type_of_failure":"OtherFailure","blocking":[]} >8.4.1https://gitlab.haskell.org/ghc/ghc//issues/14710GHC 8.4.1alpha allows the use of kind polymorphism without PolyKinds20190707T18:15:55ZRyan ScottGHC 8.4.1alpha allows the use of kind polymorphism without PolyKindsThis program:
```hs
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# OPTIONS_GHC ddumpderiv #}
module Bug where
import Data.Coerce
import Data.Proxy
class C a b where
c :: Proxy (x :: a) > b
newtype I a = MkI a
instance C x a => C x (Bug.I a) where
c = coerce @(forall (z :: x). Proxy z > a)
@(forall (z :: x). Proxy z > I a)
c
```
is rightfully rejected by GHC 8.2.2:
```
$ /opt/ghc/8.2.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:20:16: error:
Unexpected kind variables Perhaps you intended to use PolyKinds
In a type argument

20  c = coerce @(forall (z :: x). Proxy z > a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:21:16: error:
Unexpected kind variables Perhaps you intended to use PolyKinds
In a type argument

21  @(forall (z :: x). Proxy z > I a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But GHC 8.4.1alpha2 actually //accepts// this program!
```
$ /opt/ghc/8.4.1/bin/ghci Bug.hs
GHCi, version 8.4.0.20180118: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, one module loaded.
```
This is almost certainly bogus.
<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 allows the use of kind polymorphism without PolyKinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1alpha1","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE ImpredicativeTypes #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# OPTIONS_GHC ddumpderiv #}\r\nmodule Bug where\r\n\r\nimport Data.Coerce\r\nimport Data.Proxy\r\n\r\nclass C a b where\r\n c :: Proxy (x :: a) > b\r\n\r\nnewtype I a = MkI a\r\n\r\ninstance C x a => C x (Bug.I a) where\r\n c = coerce @(forall (z :: x). Proxy z > a)\r\n @(forall (z :: x). Proxy z > I a)\r\n c\r\n}}}\r\n\r\nis rightfully rejected by GHC 8.2.2:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:20:16: error:\r\n Unexpected kind variables Perhaps you intended to use PolyKinds\r\n In a type argument\r\n \r\n20  c = coerce @(forall (z :: x). Proxy z > a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:21:16: error:\r\n Unexpected kind variables Perhaps you intended to use PolyKinds\r\n In a type argument\r\n \r\n21  @(forall (z :: x). Proxy z > I a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nBut GHC 8.4.1alpha2 actually //accepts// this program!\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghci Bug.hs\r\nGHCi, version 8.4.0.20180118: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nOk, one module loaded.\r\n}}}\r\n\r\nThis is almost certainly bogus.","type_of_failure":"OtherFailure","blocking":[]} >This program:
```hs
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE KindSignatures #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# OPTIONS_GHC ddumpderiv #}
module Bug where
import Data.Coerce
import Data.Proxy
class C a b where
c :: Proxy (x :: a) > b
newtype I a = MkI a
instance C x a => C x (Bug.I a) where
c = coerce @(forall (z :: x). Proxy z > a)
@(forall (z :: x). Proxy z > I a)
c
```
is rightfully rejected by GHC 8.2.2:
```
$ /opt/ghc/8.2.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:20:16: error:
Unexpected kind variables Perhaps you intended to use PolyKinds
In a type argument

20  c = coerce @(forall (z :: x). Proxy z > a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:21:16: error:
Unexpected kind variables Perhaps you intended to use PolyKinds
In a type argument

21  @(forall (z :: x). Proxy z > I a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But GHC 8.4.1alpha2 actually //accepts// this program!
```
$ /opt/ghc/8.4.1/bin/ghci Bug.hs
GHCi, version 8.4.0.20180118: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, one module loaded.
```
This is almost certainly bogus.
<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 allows the use of kind polymorphism without PolyKinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1alpha1","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program:\r\n\r\n{{{#!hs\r\n{# LANGUAGE FlexibleInstances #}\r\n{# LANGUAGE ImpredicativeTypes #}\r\n{# LANGUAGE KindSignatures #}\r\n{# LANGUAGE MultiParamTypeClasses #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# OPTIONS_GHC ddumpderiv #}\r\nmodule Bug where\r\n\r\nimport Data.Coerce\r\nimport Data.Proxy\r\n\r\nclass C a b where\r\n c :: Proxy (x :: a) > b\r\n\r\nnewtype I a = MkI a\r\n\r\ninstance C x a => C x (Bug.I a) where\r\n c = coerce @(forall (z :: x). Proxy z > a)\r\n @(forall (z :: x). Proxy z > I a)\r\n c\r\n}}}\r\n\r\nis rightfully rejected by GHC 8.2.2:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:20:16: error:\r\n Unexpected kind variables Perhaps you intended to use PolyKinds\r\n In a type argument\r\n \r\n20  c = coerce @(forall (z :: x). Proxy z > a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:21:16: error:\r\n Unexpected kind variables Perhaps you intended to use PolyKinds\r\n In a type argument\r\n \r\n21  @(forall (z :: x). Proxy z > I a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nBut GHC 8.4.1alpha2 actually //accepts// this program!\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghci Bug.hs\r\nGHCi, version 8.4.0.20180118: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nOk, one module loaded.\r\n}}}\r\n\r\nThis is almost certainly bogus.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1https://gitlab.haskell.org/ghc/ghc//issues/16728GHC HEADonly panic with PartialTypeSignatures20190707T18:00:04ZRyan ScottGHC HEADonly panic with PartialTypeSignaturesThe following program typechecks on GHC 8.8.1:
```hs
{# LANGUAGE PartialTypeSignatures #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
module Bug where
import Data.Proxy
f :: forall a (x :: a). Proxy (x :: _)
f = Proxy
```
However, it panics on GHC HEAD:
```
$ ~/Software/ghc5/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:37: warning: [Wpartialtypesignatures]ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.9.0.20190522:
No skolem info:
[a_avg[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1173:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2927:5 in ghc:TcErrors
```
This regression was introduced in commit 80dfcee61e3bfb67f131cd674f96467e16c0f9d8. cc'ing @simonpj, the author of that patch.The following program typechecks on GHC 8.8.1:
```hs
{# LANGUAGE PartialTypeSignatures #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
module Bug where
import Data.Proxy
f :: forall a (x :: a). Proxy (x :: _)
f = Proxy
```
However, it panics on GHC HEAD:
```
$ ~/Software/ghc5/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:37: warning: [Wpartialtypesignatures]ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.9.0.20190522:
No skolem info:
[a_avg[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1173:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2927:5 in ghc:TcErrors
```
This regression was introduced in commit 80dfcee61e3bfb67f131cd674f96467e16c0f9d8. cc'ing @simonpj, the author of that patch.8.10.1Richard Eisenbergrae@richarde.devRyan ScottRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/16731GHC internal error when combining TLKSs and deriving20190925T18:06:24ZRyan ScottGHC internal error when combining TLKSs and derivingGHC freaks out when given this code:
```hs
{# LANGUAGE DeriveAnyClass #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TopLevelKindSignatures #}
module Bug where
import Data.Kind
class C (a :: Type) (b :: Type)
type T :: a > Type
data T (x :: z) deriving (C z)
```
```
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:29: error:
• GHC internal error: ‘z’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [as1 :> Type variable ‘a’ = a :: *,
aWI :> Type variable ‘x’ = x :: a]
• In the first argument of ‘C’, namely ‘z’
In the data declaration for ‘T’

12  data T (x :: z) deriving (C z)
 ^
```
The code works as written if the TLKS is omitted.GHC freaks out when given this code:
```hs
{# LANGUAGE DeriveAnyClass #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TopLevelKindSignatures #}
module Bug where
import Data.Kind
class C (a :: Type) (b :: Type)
type T :: a > Type
data T (x :: z) deriving (C z)
```
```
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:29: error:
• GHC internal error: ‘z’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [as1 :> Type variable ‘a’ = a :: *,
aWI :> Type variable ‘x’ = x :: a]
• In the first argument of ‘C’, namely ‘z’
In the data declaration for ‘T’

12  data T (x :: z) deriving (C z)
 ^
```
The code works as written if the TLKS is omitted.8.10.1Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc//issues/17566GHC 8.10 regression: Core Lint error when defining instance of CUSKless class20201019T09:14:39ZRyan ScottGHC 8.10 regression: Core Lint error when defining instance of CUSKless classHere are two files:
```hs
 Lib.hs
{# LANGUAGE DataKinds #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
module Lib where
import Data.Kind
class C (f :: k > Type) z where
type T (x :: f a) :: f a
```
```hs
 App.hs
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
module App where
import Data.Kind
import Data.Proxy
import Lib
type family F (x :: Proxy a) :: Proxy a
instance C Proxy z where
type T x = F x
```
Compiling this with GHC 8.8.1 passes Core Lint:
```
$ /opt/ghc/8.8.1/bin/ghc c Lib.hs && /opt/ghc/8.8.1/bin/ghc c App.hs dcorelint
```
But it does _not_ pass Core Lint on GHC 8.10.1alpha1:
```
$ /opt/ghc/8.10.1/bin/ghc c Lib.hs && /opt/ghc/8.10.1/bin/ghc c App.hs dcorelint
ghc: panic! (the 'impossible' happened)
(GHC version 8.10.0.20191122:
Core Lint error
<no location info>: warning:
The variable @ k1_aiz is out of scope
Substitution: [TCvSubst
In scope: InScope {}
Type env: []
Co env: []]
T
[TCvSubst
In scope: InScope {k1_aiz a_awk x_awl}
Type env: [aig :> x_awl, awg :> a_awk]
Co env: []]
[a_awk, x_awl]
[]
[k1_aiz, Proxy, a_awk, x_awl]
F x_awl
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/FamInst.hs:184:31 in ghc:FamInst
```

Another curious thing is that if you load `Lib.hs` into GHCi, you'll observe something strange about the kind of `T`:
```
$ /opt/ghc/8.10.1/bin/ghci Lib.hs
GHCi, version 8.10.0.20191122: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Lib ( Lib.hs, interpreted )
Ok, one module loaded.
λ> :i T
type C :: forall k k1. (k1 > *) > k > Constraint
class C f z where
type T :: forall k2 (f :: k1 > *) (a :: k2). f a > f a
type family T x
 Defined at Lib.hs:11:3
```
Note that `T` has kind `forall k2 (f :: k1 > *) (a :: k2). f a > f a`, which does not appear to be well kinded. It's unclear to me if this is the cause behind the Core Lint error or not.Here are two files:
```hs
 Lib.hs
{# LANGUAGE DataKinds #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
module Lib where
import Data.Kind
class C (f :: k > Type) z where
type T (x :: f a) :: f a
```
```hs
 App.hs
{# LANGUAGE DataKinds #}
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE TypeFamilies #}
module App where
import Data.Kind
import Data.Proxy
import Lib
type family F (x :: Proxy a) :: Proxy a
instance C Proxy z where
type T x = F x
```
Compiling this with GHC 8.8.1 passes Core Lint:
```
$ /opt/ghc/8.8.1/bin/ghc c Lib.hs && /opt/ghc/8.8.1/bin/ghc c App.hs dcorelint
```
But it does _not_ pass Core Lint on GHC 8.10.1alpha1:
```
$ /opt/ghc/8.10.1/bin/ghc c Lib.hs && /opt/ghc/8.10.1/bin/ghc c App.hs dcorelint
ghc: panic! (the 'impossible' happened)
(GHC version 8.10.0.20191122:
Core Lint error
<no location info>: warning:
The variable @ k1_aiz is out of scope
Substitution: [TCvSubst
In scope: InScope {}
Type env: []
Co env: []]
T
[TCvSubst
In scope: InScope {k1_aiz a_awk x_awl}
Type env: [aig :> x_awl, awg :> a_awk]
Co env: []]
[a_awk, x_awl]
[]
[k1_aiz, Proxy, a_awk, x_awl]
F x_awl
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/FamInst.hs:184:31 in ghc:FamInst
```

Another curious thing is that if you load `Lib.hs` into GHCi, you'll observe something strange about the kind of `T`:
```
$ /opt/ghc/8.10.1/bin/ghci Lib.hs
GHCi, version 8.10.0.20191122: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Lib ( Lib.hs, interpreted )
Ok, one module loaded.
λ> :i T
type C :: forall k k1. (k1 > *) > k > Constraint
class C f z where
type T :: forall k2 (f :: k1 > *) (a :: k2). f a > f a
type family T x
 Defined at Lib.hs:11:3
```
Note that `T` has kind `forall k2 (f :: k1 > *) (a :: k2). f a > f a`, which does not appear to be well kinded. It's unclear to me if this is the cause behind the Core Lint error or not.8.10.2https://gitlab.haskell.org/ghc/ghc//issues/17841"No skolem info" panic with PolyKinds20201019T09:16:46ZJakob Brünker"No skolem info" panic with PolyKinds## Summary
Making a class with a kindpolymorphic parameter and a single method can lead to a GHC panic stating "No skolem info".
## Steps to reproduce
The following program
```haskell
{# LANGUAGE PolyKinds #}
data Proxy a = Proxy
class Foo (t :: k) where foo :: Proxy (a :: t)
```
results in the error
```
Bug.hs:5:40: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.11.0.20200215:
No skolem info:
[k_a1q3[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1187:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2793:17 in ghc:TcErrors
```
On 8.6.5, it instead emits the error message
```
Bug.hs:5:45: error:
• Expected a type, but ‘t’ has kind ‘k’
• In the kind ‘t’
In the first argument of ‘Proxy’, namely ‘(a :: t)’
In the type signature: foo :: Proxy (a :: t)

5  class Foo (t :: k) where foo :: Proxy (a :: t)

```
I thought at first it might be https://gitlab.haskell.org/ghc/ghc/issues/16245 but for the facts that that issue specifically mentions RankNTypes, and produces an error already on GHC 8.6, which this example doesn't.
## Expected behavior
It should probably emit the same error message it emitted in 8.6.
## Environment
* GHC versions used: 8.8.1, HEAD
* Does *not* happen on 8.6.5
Optional:
* Operating System: linux
* System Architecture: x86_64## Summary
Making a class with a kindpolymorphic parameter and a single method can lead to a GHC panic stating "No skolem info".
## Steps to reproduce
The following program
```haskell
{# LANGUAGE PolyKinds #}
data Proxy a = Proxy
class Foo (t :: k) where foo :: Proxy (a :: t)
```
results in the error
```
Bug.hs:5:40: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.11.0.20200215:
No skolem info:
[k_a1q3[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1187:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2793:17 in ghc:TcErrors
```
On 8.6.5, it instead emits the error message
```
Bug.hs:5:45: error:
• Expected a type, but ‘t’ has kind ‘k’
• In the kind ‘t’
In the first argument of ‘Proxy’, namely ‘(a :: t)’
In the type signature: foo :: Proxy (a :: t)

5  class Foo (t :: k) where foo :: Proxy (a :: t)

```
I thought at first it might be https://gitlab.haskell.org/ghc/ghc/issues/16245 but for the facts that that issue specifically mentions RankNTypes, and produces an error already on GHC 8.6, which this example doesn't.
## Expected behavior
It should probably emit the same error message it emitted in 8.6.
## Environment
* GHC versions used: 8.8.1, HEAD
* Does *not* happen on 8.6.5
Optional:
* Operating System: linux
* System Architecture: x86_648.10.2https://gitlab.haskell.org/ghc/ghc//issues/18855GHC 9.0+ regression in checking program with higherrank kinds20201023T15:11:08ZRyan ScottGHC 9.0+ regression in checking program with higherrank kindsGHC 8.10.2 typechecks the following program:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE StandaloneKindSignatures #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
type TyFun :: Type > Type > Type
data TyFun a b
type (~>) :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type Apply :: (a ~> b) > a > b
type family Apply f x
type Nat :: Type
data Nat = Z  S Nat
type Vec :: Type > Nat > Type
data Vec :: Type > Nat > Type where
VNil :: Vec a Z
VCons :: a > Vec a n > Vec a (S n)
type ElimVec :: forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type)
> forall (n :: Nat).
forall (v :: Vec a n)
> Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v
type family ElimVec p v pVNil pVCons where
forall a (p :: forall (k :: Nat). Vec a k ~> Type)
(pVNil :: Apply p VNil)
(pVCons :: forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs)).
ElimVec p VNil pVNil pVCons = pVNil
forall a (p :: forall (k :: Nat). Vec a k ~> Type)
(pVNil :: Apply p VNil)
(pVCons :: forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs)) l x xs.
ElimVec p (VCons x (xs :: Vec a l)) pVNil pVCons =
Apply (pVCons x xs) (ElimVec @a p @l xs pVNil pVCons)
```
However, GHC 9.0.1alpha1 and HEAD reject it:
```
$ ~/Software/ghc9.0.1alpha1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:40:26: error:
• Couldn't match kind ‘k1’ with ‘m’
Expected kind ‘Vec a k1’, but ‘xs’ has kind ‘Vec a m’
because kind variable ‘m’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs)’
at Bug.hs:(38,18)(40,51)
• In the second argument of ‘Apply’, namely ‘xs’
In the first argument of ‘(~>)’, namely ‘Apply p xs’
In a standalone kind signature for ‘ElimVec’:
forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type) >
forall (n :: Nat).
forall (v :: Vec a n) >
Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v

40  Apply p xs ~> Apply p (VCons x xs))
 ^^
Bug.hs:41:25: error:
• Couldn't match kind ‘k0’ with ‘n’
Expected kind ‘Vec a k0’, but ‘v’ has kind ‘Vec a n’
because kind variable ‘n’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (n :: Nat).
forall (v :: Vec a n) >
Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v’
at Bug.hs:(35,17)(41,25)
• In the second argument of ‘Apply’, namely ‘v’
In a standalone kind signature for ‘ElimVec’:
forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type) >
forall (n :: Nat).
forall (v :: Vec a n) >
Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v

41  > Apply p v
 ^
```GHC 8.10.2 typechecks the following program:
```hs
{# LANGUAGE AllowAmbiguousTypes #}
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE StandaloneKindSignatures #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE UndecidableInstances #}
module Bug where
import Data.Kind
type TyFun :: Type > Type > Type
data TyFun a b
type (~>) :: Type > Type > Type
type a ~> b = TyFun a b > Type
infixr 0 ~>
type Apply :: (a ~> b) > a > b
type family Apply f x
type Nat :: Type
data Nat = Z  S Nat
type Vec :: Type > Nat > Type
data Vec :: Type > Nat > Type where
VNil :: Vec a Z
VCons :: a > Vec a n > Vec a (S n)
type ElimVec :: forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type)
> forall (n :: Nat).
forall (v :: Vec a n)
> Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v
type family ElimVec p v pVNil pVCons where
forall a (p :: forall (k :: Nat). Vec a k ~> Type)
(pVNil :: Apply p VNil)
(pVCons :: forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs)).
ElimVec p VNil pVNil pVCons = pVNil
forall a (p :: forall (k :: Nat). Vec a k ~> Type)
(pVNil :: Apply p VNil)
(pVCons :: forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs)) l x xs.
ElimVec p (VCons x (xs :: Vec a l)) pVNil pVCons =
Apply (pVCons x xs) (ElimVec @a p @l xs pVNil pVCons)
```
However, GHC 9.0.1alpha1 and HEAD reject it:
```
$ ~/Software/ghc9.0.1alpha1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:40:26: error:
• Couldn't match kind ‘k1’ with ‘m’
Expected kind ‘Vec a k1’, but ‘xs’ has kind ‘Vec a m’
because kind variable ‘m’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs)’
at Bug.hs:(38,18)(40,51)
• In the second argument of ‘Apply’, namely ‘xs’
In the first argument of ‘(~>)’, namely ‘Apply p xs’
In a standalone kind signature for ‘ElimVec’:
forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type) >
forall (n :: Nat).
forall (v :: Vec a n) >
Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v

40  Apply p xs ~> Apply p (VCons x xs))
 ^^
Bug.hs:41:25: error:
• Couldn't match kind ‘k0’ with ‘n’
Expected kind ‘Vec a k0’, but ‘v’ has kind ‘Vec a n’
because kind variable ‘n’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (n :: Nat).
forall (v :: Vec a n) >
Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v’
at Bug.hs:(35,17)(41,25)
• In the second argument of ‘Apply’, namely ‘v’
In a standalone kind signature for ‘ElimVec’:
forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type) >
forall (n :: Nat).
forall (v :: Vec a n) >
Apply p VNil
> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) >
Apply p xs ~> Apply p (VCons x xs))
> Apply p v

41  > Apply p v
 ^
```9.0.1https://gitlab.haskell.org/ghc/ghc//issues/17710Polykinded rewrite rule fails to typecheck (HEAD only)20200315T18:51:16ZRyan ScottPolykinded rewrite rule fails to typecheck (HEAD only)I originally noticed this issue since it prevents the `freealgebras0.0.8.1` library from building with HEAD (build log [here](https://gitlab.haskell.org/RyanGlScott/head.hackage//jobs/240129)). Here is a minimized example that demonstrates the issue:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
module Bug where
import Data.Proxy
foo :: forall k (b :: k). (forall (a :: k). Proxy a > Proxy a) > Proxy b
foo g = g Proxy
{# INLINABLE [1] foo #}
{# RULES "foo" forall (g :: forall (a :: k). Proxy a > Proxy a). foo g = g Proxy #}
```
This typechecks on GHC 8.8.2 and 8.10.1alpha2, but on HEAD it fails to typecheck:
```
$ ~/Software/ghc5/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:10:11: error:
• Cannot generalise type; skolem ‘k’ would escape its scope
if I tried to quantify (b0 :: k) in this type:
forall k. Proxy @{k} b0
(Indeed, I sometimes struggle even printing this correctly,
due to its illscoped nature.)
• When checking the transformation rule "foo"

10  {# RULES "foo" forall (g :: forall (a :: k). Proxy a > Proxy a). foo g = g Proxy #}
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Judging by the error message, this regression was likely introduced in commit 350e2b78788d47255d27489dfc62d664498b5de4 (`Don't zap to Any; error instead`). cc'ing @rae, the author of that commit.I originally noticed this issue since it prevents the `freealgebras0.0.8.1` library from building with HEAD (build log [here](https://gitlab.haskell.org/RyanGlScott/head.hackage//jobs/240129)). Here is a minimized example that demonstrates the issue:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
module Bug where
import Data.Proxy
foo :: forall k (b :: k). (forall (a :: k). Proxy a > Proxy a) > Proxy b
foo g = g Proxy
{# INLINABLE [1] foo #}
{# RULES "foo" forall (g :: forall (a :: k). Proxy a > Proxy a). foo g = g Proxy #}
```
This typechecks on GHC 8.8.2 and 8.10.1alpha2, but on HEAD it fails to typecheck:
```
$ ~/Software/ghc5/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:10:11: error:
• Cannot generalise type; skolem ‘k’ would escape its scope
if I tried to quantify (b0 :: k) in this type:
forall k. Proxy @{k} b0
(Indeed, I sometimes struggle even printing this correctly,
due to its illscoped nature.)
• When checking the transformation rule "foo"

10  {# RULES "foo" forall (g :: forall (a :: k). Proxy a > Proxy a). foo g = g Proxy #}
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Judging by the error message, this regression was likely introduced in commit 350e2b78788d47255d27489dfc62d664498b5de4 (`Don't zap to Any; error instead`). cc'ing @rae, the author of that commit.9.0.1https://gitlab.haskell.org/ghc/ghc//issues/18488DerivingVia: Kinding information isn't propagated20200722T00:36:30ZGeshDerivingVia: Kinding information isn't propagated## Summary
Using `DerivingVia` unexpectedly restricts the flow of kinding information. This is problematic in modules with `PolyKinds` enabled, since it limits what sources of kinding information are available
## Steps to reproduce
Consider the following snippet.
```haskell
{# LANGUAGE DerivingVia #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE StandaloneDeriving #}
class C t
newtype Tag t a = T a
newtype Tag' t a = T' a
instance (C t, Eq t) => Eq (Tag t a)
deriving via (Tag t a) instance (C t, Eq t) => Eq (Tag' t a)
```
Clearly, from the context `Eq t`, we infer `t :: Type`. GHC disagrees:
```
• Expected a type, but ‘t’ has kind ‘k’
• In the first argument of ‘Eq’, namely ‘t’
In the standalone deriving instance for
‘(C t, Eq t) => Eq (Tag' t a)’
deriving via (Tag t a) instance (C t, Eq t) => Eq (Tag' t a)
^
```
OK, fine. Maybe GHC doesn't take the context into consideration. Let's try monomorphising other indeces involved. Surprise, both writing `class C (t :: *)` and `newtype Tag' (t :: *) a` fail to give enough kinding information to satisfy GHC.
However, writing `newtype Tag (t :: *) a` unexpectedly works. This leads me to the hypothesis that `DerivingVia` only uses kinding information of the via type, even with `StandaloneDeriving` providing extra context.
## Expected behavior
`DerivingVia` should use all the kinding information available in the declaration. If this is too much, at least have it do so for standalone derivations.
## Environment
* GHC version used: 8.8.1## Summary
Using `DerivingVia` unexpectedly restricts the flow of kinding information. This is problematic in modules with `PolyKinds` enabled, since it limits what sources of kinding information are available
## Steps to reproduce
Consider the following snippet.
```haskell
{# LANGUAGE DerivingVia #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE StandaloneDeriving #}
class C t
newtype Tag t a = T a
newtype Tag' t a = T' a
instance (C t, Eq t) => Eq (Tag t a)
deriving via (Tag t a) instance (C t, Eq t) => Eq (Tag' t a)
```
Clearly, from the context `Eq t`, we infer `t :: Type`. GHC disagrees:
```
• Expected a type, but ‘t’ has kind ‘k’
• In the first argument of ‘Eq’, namely ‘t’
In the standalone deriving instance for
‘(C t, Eq t) => Eq (Tag' t a)’
deriving via (Tag t a) instance (C t, Eq t) => Eq (Tag' t a)
^
```
OK, fine. Maybe GHC doesn't take the context into consideration. Let's try monomorphising other indeces involved. Surprise, both writing `class C (t :: *)` and `newtype Tag' (t :: *) a` fail to give enough kinding information to satisfy GHC.
However, writing `newtype Tag (t :: *) a` unexpectedly works. This leads me to the hypothesis that `DerivingVia` only uses kinding information of the via type, even with `StandaloneDeriving` providing extra context.
## Expected behavior
`DerivingVia` should use all the kinding information available in the declaration. If this is too much, at least have it do so for standalone derivations.
## Environment
* GHC version used: 8.8.1https://gitlab.haskell.org/ghc/ghc//issues/18831GHC requires PolyKinds in places without any kind polymorphism20201014T16:36:06ZRyan ScottGHC requires PolyKinds in places without any kind polymorphismI would expect the following to typecheck:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
import Data.Proxy
data T :: Proxy 0 > Type
```
Surprisingly, however, it doesn't.
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:17: error:
Illegal kind: 0
Did you mean to enable PolyKinds?

8  data T :: Proxy 0 > Type
 ^
```
I find it quite surprising that using a typelevel literal would require `PolyKinds`, as there's nothing inherently polykinded about it.
This isn't even the only example of strange `PolyKinds` requirements. The following programs are also rejected for similar reasons:
* Kindlevel uses of `=>`:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
data T :: () => Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:11: error:
Illegal kind: () => Type
Did you mean to enable PolyKinds?

7  data T :: () => Type
 ^^^^^^^^^^
```
</details>
* Kindlevel uses of explicit annotations:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
data T :: (Type :: Type) > Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:12: error:
Illegal kind: Type :: Type
Did you mean to enable PolyKinds?

7  data T :: (Type :: Type) > Type
 ^^^^^^^^^^^^
```
</details>
* Kindlevel uses of promoted lists:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
import Data.Proxy
data T :: Proxy '[Type,Type] > Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:17: error:
Illegal kind: '[Type, Type]
Did you mean to enable PolyKinds?

8  data T :: Proxy '[Type,Type] > Type
 ^^^^^^^^^^^^
```
</details>
* Kindlevel uses of promoted tuples:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
import Data.Proxy
data T :: Proxy '(Type,Type) > Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:17: error:
Illegal kind: '(Type, Type)
Did you mean to enable PolyKinds?

8  data T :: Proxy '(Type,Type) > Type
 ^^^^^^^^^^^^
```
</details>I would expect the following to typecheck:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
import Data.Proxy
data T :: Proxy 0 > Type
```
Surprisingly, however, it doesn't.
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:17: error:
Illegal kind: 0
Did you mean to enable PolyKinds?

8  data T :: Proxy 0 > Type
 ^
```
I find it quite surprising that using a typelevel literal would require `PolyKinds`, as there's nothing inherently polykinded about it.
This isn't even the only example of strange `PolyKinds` requirements. The following programs are also rejected for similar reasons:
* Kindlevel uses of `=>`:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
data T :: () => Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:11: error:
Illegal kind: () => Type
Did you mean to enable PolyKinds?

7  data T :: () => Type
 ^^^^^^^^^^
```
</details>
* Kindlevel uses of explicit annotations:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
data T :: (Type :: Type) > Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:7:12: error:
Illegal kind: Type :: Type
Did you mean to enable PolyKinds?

7  data T :: (Type :: Type) > Type
 ^^^^^^^^^^^^
```
</details>
* Kindlevel uses of promoted lists:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
import Data.Proxy
data T :: Proxy '[Type,Type] > Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:17: error:
Illegal kind: '[Type, Type]
Did you mean to enable PolyKinds?

8  data T :: Proxy '[Type,Type] > Type
 ^^^^^^^^^^^^
```
</details>
* Kindlevel uses of promoted tuples:
```hs
{# LANGUAGE DataKinds #}
{# LANGUAGE KindSignatures #}
module Bug where
import Data.Kind
import Data.Proxy
data T :: Proxy '(Type,Type) > Type
```
<details>
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:17: error:
Illegal kind: '(Type, Type)
Did you mean to enable PolyKinds?

8  data T :: Proxy '(Type,Type) > Type
 ^^^^^^^^^^^^
```
</details>https://gitlab.haskell.org/ghc/ghc//issues/17838Unused type variable error misidentifies the name of the type variable20200331T20:55:29ZRyan ScottUnused type variable error misidentifies the name of the type variableIf you compile the following (erroneous) program on GHC 8.8.2 or later:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
module Bug where
import Data.Kind
type Const (a :: Type) (b :: Type) = a
type family F (x :: a) :: Type where
forall a x. F x = Const Int a
```
You'll get the following error:
```
$ /opt/ghc/8.8.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:10: error:
• Type variable ‘a2’ is mentioned in the RHS,
but not bound on the LHS of the family instance
• In the equations for closed type family ‘F’
In the type family declaration for ‘F’

11  forall a x. F x = Const Int a
 ^
```
This points to the type variable `a` in the source code, but names it `a2` in the error message! This appears to be the result of having a kind variable named `a` in the type family header, since renaming that kind variable to something else makes the issue go away. For example, this variant of the program above:
```hs
type family F (x :: b) :: Type where
forall a x. F x = Const Int a
```
Gives a sensible error message:
```
$ /opt/ghc/8.8.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:10: error:
• Type variable ‘a’ is mentioned in the RHS,
but not bound on the LHS of the family instance
• In the equations for closed type family ‘F’
In the type family declaration for ‘F’

11  forall a x. F x = Const Int a
 ^
```If you compile the following (erroneous) program on GHC 8.8.2 or later:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
module Bug where
import Data.Kind
type Const (a :: Type) (b :: Type) = a
type family F (x :: a) :: Type where
forall a x. F x = Const Int a
```
You'll get the following error:
```
$ /opt/ghc/8.8.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:10: error:
• Type variable ‘a2’ is mentioned in the RHS,
but not bound on the LHS of the family instance
• In the equations for closed type family ‘F’
In the type family declaration for ‘F’

11  forall a x. F x = Const Int a
 ^
```
This points to the type variable `a` in the source code, but names it `a2` in the error message! This appears to be the result of having a kind variable named `a` in the type family header, since renaming that kind variable to something else makes the issue go away. For example, this variant of the program above:
```hs
type family F (x :: b) :: Type where
forall a x. F x = Const Int a
```
Gives a sensible error message:
```
$ /opt/ghc/8.8.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:10: error:
• Type variable ‘a’ is mentioned in the RHS,
but not bound on the LHS of the family instance
• In the equations for closed type family ‘F’
In the type family declaration for ‘F’

11  forall a x. F x = Const Int a
 ^
```https://gitlab.haskell.org/ghc/ghc//issues/17772CUSKless class typechecks on 8.4, but not on 8.6+20200608T10:56:41ZRyan ScottCUSKless class typechecks on 8.4, but not on 8.6+This code will typecheck with GHC 8.0.2 through 8.4.4:
```hs
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
import Data.Proxy
class C f where
type T (x :: f a) :: Type
sT :: forall a (x :: f a).
Proxy x > T x
```
However, it mysteriously _does_ not typecheck on GHC 8.6.5 or later:
```
$ /opt/ghc/8.8.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:13:22: error:
• Expected kind ‘f a’, but ‘x’ has kind ‘f a1’
• In the first argument of ‘T’, namely ‘x’
In the type signature: sT :: forall a (x :: f a). Proxy x > T x
In the class declaration for ‘C’

13  Proxy x > T x
 ^
```
I cannot think of a good reason why this shouldn't typecheck, especially since there appears to be no polymorphic recursion happening in `C`, `T`, or `sT`.
Some observations:
* Giving `C` a CUSK (i.e., `class C (f :: k > Type) where ...`) makes it typecheck:
* Splitting up `C` into two classes like so also makes it typecheck:
```hs
class C1 f where
type T (x :: f a) :: Type
class C2 f where
sT :: forall a (x :: f a).
Proxy x > T x
```This code will typecheck with GHC 8.0.2 through 8.4.4:
```hs
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
import Data.Proxy
class C f where
type T (x :: f a) :: Type
sT :: forall a (x :: f a).
Proxy x > T x
```
However, it mysteriously _does_ not typecheck on GHC 8.6.5 or later:
```
$ /opt/ghc/8.8.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:13:22: error:
• Expected kind ‘f a’, but ‘x’ has kind ‘f a1’
• In the first argument of ‘T’, namely ‘x’
In the type signature: sT :: forall a (x :: f a). Proxy x > T x
In the class declaration for ‘C’

13  Proxy x > T x
 ^
```
I cannot think of a good reason why this shouldn't typecheck, especially since there appears to be no polymorphic recursion happening in `C`, `T`, or `sT`.
Some observations:
* Giving `C` a CUSK (i.e., `class C (f :: k > Type) where ...`) makes it typecheck:
* Splitting up `C` into two classes like so also makes it typecheck:
```hs
class C1 f where
type T (x :: f a) :: Type
class C2 f where
sT :: forall a (x :: f a).
Proxy x > T x
```https://gitlab.haskell.org/ghc/ghc//issues/17397Annotation of PolyKinded structures (unhelpfully) prompts UndecidableInstances20191031T22:30:53ZMax HarmsAnnotation of PolyKinded structures (unhelpfully) prompts UndecidableInstances## Summary
The error message provided when GHC infers the kind of an otherwise polykinded structure is unhelpful. I recognize that this might not be the highest priority, but I do think Haskell's error messages here could be better.
## Steps to reproduce
Let's say I have a little program like
```
{# LANGUAGE PolyKinds #}
class Foo a
data Bar (f :: * > *)
instance (Foo (f Bool)) => Foo (Bar f)
main :: IO ()
main = pure ()
```
Everything compiles and is happy and fun.
(This is stripped down for clarity; imagine lots of irrelevant methods and constructors and other spinning parts in the case where I actually hit this.)
Now let's say you foolishly add a method to `Foo` like so:
```
class Foo a where
foo :: Int > [a]
```
GHC errors, saying:
```
• The constraint ‘Foo (f Bool)’
is no smaller than the instance head ‘Foo (Bar f)’
(Use UndecidableInstances to permit this)
• In the instance declaration for ‘Foo (Bar f)’
```
What happened here was that by mentioning `[a]` we've pinned down the kind of `a`. A similar effect can be produced simply by annotating the kind of `a` like so:
```
class Foo (a :: *)
```
Before this kind was specified, the decidability checker on the instance was satisfied, but afterwards it chokes and demands `UndecidableInstances`. My guess of why it's doing this is that there's an implicit kind showing up in the context afterwards, and so it no longer knows that the context is smaller than the head. *\*shrug\**
## Expected behavior
I would hope that annotating the kind of a class would not affect knowntobevalid instances of that class elsewhere. At the very least I'd hope that the decidability checker would report in its error that it only failed because of an inferred kind when PolyKinds is active. Best of all would be if the decidability checker could handle having kinds specified in cases like this.
## Environment
Tested on GHC 8.6 and 8.8.## Summary
The error message provided when GHC infers the kind of an otherwise polykinded structure is unhelpful. I recognize that this might not be the highest priority, but I do think Haskell's error messages here could be better.
## Steps to reproduce
Let's say I have a little program like
```
{# LANGUAGE PolyKinds #}
class Foo a
data Bar (f :: * > *)
instance (Foo (f Bool)) => Foo (Bar f)
main :: IO ()
main = pure ()
```
Everything compiles and is happy and fun.
(This is stripped down for clarity; imagine lots of irrelevant methods and constructors and other spinning parts in the case where I actually hit this.)
Now let's say you foolishly add a method to `Foo` like so:
```
class Foo a where
foo :: Int > [a]
```
GHC errors, saying:
```
• The constraint ‘Foo (f Bool)’
is no smaller than the instance head ‘Foo (Bar f)’
(Use UndecidableInstances to permit this)
• In the instance declaration for ‘Foo (Bar f)’
```
What happened here was that by mentioning `[a]` we've pinned down the kind of `a`. A similar effect can be produced simply by annotating the kind of `a` like so:
```
class Foo (a :: *)
```
Before this kind was specified, the decidability checker on the instance was satisfied, but afterwards it chokes and demands `UndecidableInstances`. My guess of why it's doing this is that there's an implicit kind showing up in the context afterwards, and so it no longer knows that the context is smaller than the head. *\*shrug\**
## Expected behavior
I would hope that annotating the kind of a class would not affect knowntobevalid instances of that class elsewhere. At the very least I'd hope that the decidability checker would report in its error that it only failed because of an inferred kind when PolyKinds is active. Best of all would be if the decidability checker could handle having kinds specified in cases like this.
## Environment
Tested on GHC 8.6 and 8.8.https://gitlab.haskell.org/ghc/ghc//issues/15120Default methods don't pass implicit kind parameters properly20190707T18:14:11ZmbieleckDefault methods don't pass implicit kind parameters properlyWhen compiling the following module:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE DefaultSignatures #}
module TestCase where
import Data.Proxy
class Describe a where
describe :: Proxy a > String
default describe :: Proxy a > String
describe _ = ""
data Foo = Foo
instance Describe Foo
```
I get the following error (on GHC 8.0.2 and 8.2.2, with `fprintexplicitkinds`):
```
TestCase.hs:15:10: error:
• Couldn't match type ‘*’ with ‘Foo’
Expected type: Proxy * Foo > String
Actual type: Proxy Foo Foo > String
• In the expression: TestCase.$dmdescribe @Foo
In an equation for ‘describe’: describe = TestCase.$dmdescribe @Foo
In the instance declaration for ‘Describe * Foo’

15  instance Describe Foo
 ^^^^^^^^^^^^
```
The Core generated for `$dmdescribe` has the following type signature:
```
TestCase.$dmdescribe
:: forall k (a :: k). Describe k a => Proxy k a > String
```
I believe the failure results from the fact that the type application `TestCase.$dmdescribe @Foo` passes `Foo` as the `k` parameter instead of `a`.
Seems related to #13998 .
<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":"Default methods don't pass implicit kind parameters properly","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["DefaultSignatures","PolyKinds,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When compiling the following module:\r\n\r\n{{{#!hs\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE DefaultSignatures #}\r\nmodule TestCase where\r\n\r\nimport Data.Proxy\r\n\r\nclass Describe a where\r\n describe :: Proxy a > String\r\n\r\n default describe :: Proxy a > String\r\n describe _ = \"\"\r\n\r\ndata Foo = Foo\r\n\r\ninstance Describe Foo\r\n}}}\r\n\r\nI get the following error (on GHC 8.0.2 and 8.2.2, with `fprintexplicitkinds`):\r\n\r\n{{{\r\nTestCase.hs:15:10: error:\r\n • Couldn't match type ‘*’ with ‘Foo’\r\n Expected type: Proxy * Foo > String\r\n Actual type: Proxy Foo Foo > String\r\n • In the expression: TestCase.$dmdescribe @Foo\r\n In an equation for ‘describe’: describe = TestCase.$dmdescribe @Foo\r\n In the instance declaration for ‘Describe * Foo’\r\n \r\n15  instance Describe Foo\r\n  ^^^^^^^^^^^^\r\n}}}\r\n\r\nThe Core generated for `$dmdescribe` has the following type signature:\r\n\r\n{{{\r\nTestCase.$dmdescribe\r\n :: forall k (a :: k). Describe k a => Proxy k a > String\r\n}}}\r\n\r\nI believe the failure results from the fact that the type application `TestCase.$dmdescribe @Foo` passes `Foo` as the `k` parameter instead of `a`.\r\n\r\nSeems related to https://ghc.haskell.org/trac/ghc/ticket/13998 .","type_of_failure":"OtherFailure","blocking":[]} >When compiling the following module:
```hs
{# LANGUAGE PolyKinds #}
{# LANGUAGE DefaultSignatures #}
module TestCase where
import Data.Proxy
class Describe a where
describe :: Proxy a > String
default describe :: Proxy a > String
describe _ = ""
data Foo = Foo
instance Describe Foo
```
I get the following error (on GHC 8.0.2 and 8.2.2, with `fprintexplicitkinds`):
```
TestCase.hs:15:10: error:
• Couldn't match type ‘*’ with ‘Foo’
Expected type: Proxy * Foo > String
Actual type: Proxy Foo Foo > String
• In the expression: TestCase.$dmdescribe @Foo
In an equation for ‘describe’: describe = TestCase.$dmdescribe @Foo
In the instance declaration for ‘Describe * Foo’

15  instance Describe Foo
 ^^^^^^^^^^^^
```
The Core generated for `$dmdescribe` has the following type signature:
```
TestCase.$dmdescribe
:: forall k (a :: k). Describe k a => Proxy k a > String
```
I believe the failure results from the fact that the type application `TestCase.$dmdescribe @Foo` passes `Foo` as the `k` parameter instead of `a`.
Seems related to #13998 .
<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":"Default methods don't pass implicit kind parameters properly","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["DefaultSignatures","PolyKinds,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When compiling the following module:\r\n\r\n{{{#!hs\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE DefaultSignatures #}\r\nmodule TestCase where\r\n\r\nimport Data.Proxy\r\n\r\nclass Describe a where\r\n describe :: Proxy a > String\r\n\r\n default describe :: Proxy a > String\r\n describe _ = \"\"\r\n\r\ndata Foo = Foo\r\n\r\ninstance Describe Foo\r\n}}}\r\n\r\nI get the following error (on GHC 8.0.2 and 8.2.2, with `fprintexplicitkinds`):\r\n\r\n{{{\r\nTestCase.hs:15:10: error:\r\n • Couldn't match type ‘*’ with ‘Foo’\r\n Expected type: Proxy * Foo > String\r\n Actual type: Proxy Foo Foo > String\r\n • In the expression: TestCase.$dmdescribe @Foo\r\n In an equation for ‘describe’: describe = TestCase.$dmdescribe @Foo\r\n In the instance declaration for ‘Describe * Foo’\r\n \r\n15  instance Describe Foo\r\n  ^^^^^^^^^^^^\r\n}}}\r\n\r\nThe Core generated for `$dmdescribe` has the following type signature:\r\n\r\n{{{\r\nTestCase.$dmdescribe\r\n :: forall k (a :: k). Describe k a => Proxy k a > String\r\n}}}\r\n\r\nI believe the failure results from the fact that the type application `TestCase.$dmdescribe @Foo` passes `Foo` as the `k` parameter instead of `a`.\r\n\r\nSeems related to https://ghc.haskell.org/trac/ghc/ticket/13998 .","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14554Core Lint error mixing20190707T18:16:32ZIcelandjackCore Lint error mixingWhile trying to deeply embed *Singletons*style defunctionalization symbol application using the code from [System FC with Explicit Kind Equality](http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs), I ran into the following `dcorelint` error:
```hs
{# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #}
import Data.Kind
import Data.Proxy
type a ~> b = (a, b) > Type
type family (@@) (f::k ~> k') (a::k)::k'
data IdSym0 :: Type ~> Type
type instance IdSym0 @@ 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') = IK k ~> IK k'
type family
IT (ty::TY kind) :: IK kind where
IT ID = IdSym0
IT (FNAPP f x) = IT f @@ IT x
zero :: TyRep X a > IT a
zero = \case
TFnApp TID a > undefined
```
```
$ ghci ignoredotghci dcorelint ~/hs/123bug.hs
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /home/baldur/hs/123bug.hs, interpreted )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171122 for x86_64unknownlinux):
ASSERT failed!
Bad coercion hole {a2UN}: (IT
(a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])
(IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])
nominal
<(IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])>_N
IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N)
IT (a_a1S5[ssk:3] > Sym (TY (Sym co_a2UC))_N)
nominal
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1205:22 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1203:5 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
<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":"Core Lint error mixing","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"While trying to deeply embed ''Singletons''style defunctionalization symbol application using the code from [http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs System FC with Explicit Kind Equality], I ran into the following `dcorelint` error:\r\n\r\n{{{#!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\ntype a ~> b = (a, b) > Type\r\n\r\ntype family (@@) (f::k ~> k') (a::k)::k'\r\n\r\ndata IdSym0 :: Type ~> Type\r\n\r\ntype instance IdSym0 @@ 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') = IK k ~> IK k'\r\n\r\ntype family\r\n IT (ty::TY kind) :: IK kind where\r\n IT ID = IdSym0\r\n IT (FNAPP f x) = IT f @@ IT x\r\n\r\nzero :: TyRep X a > IT a\r\nzero = \\case\r\n TFnApp TID a > undefined \r\n}}}\r\n\r\n{{{\r\n$ ghci ignoredotghci dcorelint ~/hs/123bug.hs\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /home/baldur/hs/123bug.hs, interpreted )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171122 for x86_64unknownlinux):\r\n\tASSERT failed!\r\n Bad coercion hole {a2UN}: (IT\r\n (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])\r\n (IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])\r\n nominal\r\n <(IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])>_N\r\n IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N)\r\n IT (a_a1S5[ssk:3] > Sym (TY (Sym co_a2UC))_N)\r\n nominal\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1205:22 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType\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/utils/Outputable.hs:1203:5 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >While trying to deeply embed *Singletons*style defunctionalization symbol application using the code from [System FC with Explicit Kind Equality](http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs), I ran into the following `dcorelint` error:
```hs
{# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #}
import Data.Kind
import Data.Proxy
type a ~> b = (a, b) > Type
type family (@@) (f::k ~> k') (a::k)::k'
data IdSym0 :: Type ~> Type
type instance IdSym0 @@ 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') = IK k ~> IK k'
type family
IT (ty::TY kind) :: IK kind where
IT ID = IdSym0
IT (FNAPP f x) = IT f @@ IT x
zero :: TyRep X a > IT a
zero = \case
TFnApp TID a > undefined
```
```
$ ghci ignoredotghci dcorelint ~/hs/123bug.hs
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /home/baldur/hs/123bug.hs, interpreted )
ghcstage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171122 for x86_64unknownlinux):
ASSERT failed!
Bad coercion hole {a2UN}: (IT
(a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])
(IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])
nominal
<(IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])>_N
IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N)
IT (a_a1S5[ssk:3] > Sym (TY (Sym co_a2UC))_N)
nominal
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1205:22 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1203:5 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
<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":"Core Lint error mixing","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"While trying to deeply embed ''Singletons''style defunctionalization symbol application using the code from [http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs System FC with Explicit Kind Equality], I ran into the following `dcorelint` error:\r\n\r\n{{{#!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\ntype a ~> b = (a, b) > Type\r\n\r\ntype family (@@) (f::k ~> k') (a::k)::k'\r\n\r\ndata IdSym0 :: Type ~> Type\r\n\r\ntype instance IdSym0 @@ 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') = IK k ~> IK k'\r\n\r\ntype family\r\n IT (ty::TY kind) :: IK kind where\r\n IT ID = IdSym0\r\n IT (FNAPP f x) = IT f @@ IT x\r\n\r\nzero :: TyRep X a > IT a\r\nzero = \\case\r\n TFnApp TID a > undefined \r\n}}}\r\n\r\n{{{\r\n$ ghci ignoredotghci dcorelint ~/hs/123bug.hs\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /home/baldur/hs/123bug.hs, interpreted )\r\nghcstage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171122 for x86_64unknownlinux):\r\n\tASSERT failed!\r\n Bad coercion hole {a2UN}: (IT\r\n (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])\r\n (IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])\r\n nominal\r\n <(IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N) > D:R:IK[0])>_N\r\n IT (a_a1S5 > Sym (TY (Sym co_a2UC))_N)\r\n IT (a_a1S5[ssk:3] > Sym (TY (Sym co_a2UC))_N)\r\n nominal\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1205:22 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType\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/utils/Outputable.hs:1203:5 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >