GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:30:05Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/11519Inferring non-tau kinds2019-07-07T18:30:05ZRichard Eisenbergrae@richarde.devInferring non-tau kindsWhile up to my usual type-level shenanigans, I found that I want this definition:
```
data TypeRep (a :: k) -- abstract
data TypeRepX :: (forall k. k -> Constraint) -> Type where
TypeRepX :: forall k (c :: forall k'. k' -> Constraint...While up to my usual type-level shenanigans, I found that I want this definition:
```
data TypeRep (a :: k) -- abstract
data TypeRepX :: (forall k. k -> Constraint) -> Type where
TypeRepX :: forall k (c :: forall k'. k' -> Constraint) (a :: k).
c a => TypeRep a -> TypeRepX c
```
Note `TypeRepX`'s higher-rank kind. The idea is that I want to optionally constrain `TypeRepX`'s payload. Without using a higher-rank kind, the constraint would necessary fix the kind of the payload, and I don't want that. For example, I sometimes use `TypeRepX ConstTrue`, where
```
class ConstTrue (a :: k)
instance ConstTrue a
```
This actually works just fine, and I've been using the above definition to good effect.
But then I wanted a `Show` instance:
```
instance Show (TypeRep a) -- elsewhere
instance Show (TypeRepX c) where
show (TypeRepX tr) = show t
```
Looks sensible. But GHC complains. This is because it tries to infer `c`'s kind, by inventing a unification variable and then unifying. But this doesn't work, of course, because `c`'s kind is not a tau-type, so unification fails, lest we let impredicativity sneak in. What's particularly vexing is that, even if I annotate `c` with the correct kind, unification *still* fails. This is because that `c` is a *usage* of `c`, not a *binding* of `c`. Indeed, there is no place in an instance declaration to bind a type variable explicitly, so I have no recourse.
I'm not sure what the solution is here. Somehow, it feels that inferring a non-tau kind for `c` is perfectly safe, because the kind is known from the use of `TypeRepX`. This would allow me to drop the kind annotation in the definition of `TypeRepX`, which looks redundant to me. But I'm not fully sure about this assumption.
At the least, we could introduce a spot for explicit binding of type variables in instance declarations.
I think, actually, I just figured it out. Use `ExpType`s when kind-checking types. Then I think the normal bidirectional thing (actually already implemented) will do the Right Thing.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"Inferring non-tau kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"While up to my usual type-level shenanigans, I found that I want this definition:\r\n\r\n{{{\r\ndata TypeRep (a :: k) -- abstract\r\n\r\ndata TypeRepX :: (forall k. k -> Constraint) -> Type where\r\n TypeRepX :: forall k (c :: forall k'. k' -> Constraint) (a :: k).\r\n c a => TypeRep a -> TypeRepX c\r\n}}}\r\n\r\nNote `TypeRepX`'s higher-rank kind. The idea is that I want to optionally constrain `TypeRepX`'s payload. Without using a higher-rank kind, the constraint would necessary fix the kind of the payload, and I don't want that. For example, I sometimes use `TypeRepX ConstTrue`, where\r\n\r\n{{{\r\nclass ConstTrue (a :: k)\r\ninstance ConstTrue a\r\n}}}\r\n\r\nThis actually works just fine, and I've been using the above definition to good effect.\r\n\r\nBut then I wanted a `Show` instance:\r\n\r\n{{{\r\ninstance Show (TypeRep a) -- elsewhere\r\n\r\ninstance Show (TypeRepX c) where\r\n show (TypeRepX tr) = show t\r\n}}}\r\n\r\nLooks sensible. But GHC complains. This is because it tries to infer `c`'s kind, by inventing a unification variable and then unifying. But this doesn't work, of course, because `c`'s kind is not a tau-type, so unification fails, lest we let impredicativity sneak in. What's particularly vexing is that, even if I annotate `c` with the correct kind, unification ''still'' fails. This is because that `c` is a ''usage'' of `c`, not a ''binding'' of `c`. Indeed, there is no place in an instance declaration to bind a type variable explicitly, so I have no recourse.\r\n\r\nI'm not sure what the solution is here. Somehow, it feels that inferring a non-tau kind for `c` is perfectly safe, because the kind is known from the use of `TypeRepX`. This would allow me to drop the kind annotation in the definition of `TypeRepX`, which looks redundant to me. But I'm not fully sure about this assumption.\r\n\r\nAt the least, we could introduce a spot for explicit binding of type variables in instance declarations.\r\n\r\nI think, actually, I just figured it out. Use `ExpType`s when kind-checking types. Then I think the normal bidirectional thing (actually already implemented) will do the Right Thing.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11485Very unhelpful message resulting from kind mismatch2019-07-07T18:30:13ZRyan ScottVery unhelpful message resulting from kind mismatchThe following code:
```hs
module Foo where
import Data.Typeable
tyConOf :: Typeable a => Proxy a -> TyCon
tyConOf = typeRepTyCon . typeRep
tcList :: TyCon
tcList = tyConOf (Proxy :: Proxy [])
```
fails because `-XPolyKinds` is not e...The following code:
```hs
module Foo where
import Data.Typeable
tyConOf :: Typeable a => Proxy a -> TyCon
tyConOf = typeRepTyCon . typeRep
tcList :: TyCon
tcList = tyConOf (Proxy :: Proxy [])
```
fails because `-XPolyKinds` is not enabled. But the error message that you get is quite different on GHC 7.10 and 8.0.
On GHC 7.10.3:
```
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
Foo.hs:9:19:
Couldn't match kind ‘* -> *’ with ‘*’
Expected type: Proxy a0
Actual type: Proxy []
In the first argument of ‘tyConOf’, namely ‘(Proxy :: Proxy [])’
In the expression: tyConOf (Proxy :: Proxy [])
In an equation for ‘tcList’: tcList = tyConOf (Proxy :: Proxy [])
```
But on GHC 8.0.1-rc1:
```
Foo.hs:9:19: error:
• Expected kind ‘Proxy []’,
but ‘Data.Proxy.Proxy :: Proxy []’ has kind ‘Proxy []’
• In the first argument of ‘tyConOf’, namely ‘(Proxy :: Proxy [])’
In the expression: tyConOf (Proxy :: Proxy [])
In an equation for ‘tcList’: tcList = tyConOf (Proxy :: Proxy [])
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc1 |
| 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":"Very unhelpful message resulting from kind mismatch","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code:\r\n\r\n{{{#!hs\r\nmodule Foo where\r\n\r\nimport Data.Typeable\r\n\r\ntyConOf :: Typeable a => Proxy a -> TyCon\r\ntyConOf = typeRepTyCon . typeRep\r\n\r\ntcList :: TyCon\r\ntcList = tyConOf (Proxy :: Proxy [])\r\n}}}\r\n\r\nfails because `-XPolyKinds` is not enabled. But the error message that you get is quite different on GHC 7.10 and 8.0.\r\n\r\nOn GHC 7.10.3:\r\n\r\n{{{\r\n[1 of 1] Compiling Foo ( Foo.hs, Foo.o )\r\n\r\nFoo.hs:9:19:\r\n Couldn't match kind ‘* -> *’ with ‘*’\r\n Expected type: Proxy a0\r\n Actual type: Proxy []\r\n In the first argument of ‘tyConOf’, namely ‘(Proxy :: Proxy [])’\r\n In the expression: tyConOf (Proxy :: Proxy [])\r\n In an equation for ‘tcList’: tcList = tyConOf (Proxy :: Proxy [])\r\n}}}\r\n\r\nBut on GHC 8.0.1-rc1:\r\n\r\n{{{\r\nFoo.hs:9:19: error: \r\n • Expected kind ‘Proxy []’, \r\n but ‘Data.Proxy.Proxy :: Proxy []’ has kind ‘Proxy []’ \r\n • In the first argument of ‘tyConOf’, namely ‘(Proxy :: Proxy [])’ \r\n In the expression: tyConOf (Proxy :: Proxy [])\r\n In an equation for ‘tcList’: tcList = tyConOf (Proxy :: Proxy [])\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11471Kind polymorphism and unboxed types: bad things are happening2019-07-07T18:30:16ZBen GamariKind polymorphism and unboxed types: bad things are happeningThis Note, found in TyCoRep, needs to be updated to reflect `TypeInType`. It should not reference `OpenKind`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---...This Note, found in TyCoRep, needs to be updated to reflect `TypeInType`. It should not reference `OpenKind`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.3 |
| Type | Task |
| 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":"Note [The kind invariant] in TyCoRep needs to be updated","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"This Note, found in TyCoRep, needs to be updated to reflect `TypeInType`. It should not reference `OpenKind`.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11463Template Haskell applies too many arguments to kind synonym2022-02-08T15:14:11ZRyan ScottTemplate Haskell applies too many arguments to kind synonymRunning the following code:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeInType #-}
module IdStarK where
import Data.Kind
import Language.Haskell.TH
type Id a = a
data Proxy (a :: Id k) = Proxy
$(return [])
main :: IO ()
...Running the following code:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeInType #-}
module IdStarK where
import Data.Kind
import Language.Haskell.TH
type Id a = a
data Proxy (a :: Id k) = Proxy
$(return [])
main :: IO ()
main = do
putStrLn $(reify ''Proxy >>= stringE . pprint)
putStrLn $(reify ''Proxy >>= stringE . show)
```
Gives a result I wouldn't have expected:
```
$ /opt/ghc/head/bin/runghc IdStarK.hs
data IdStarK.Proxy (a_0 :: IdStarK.Id * k_1) = IdStarK.Proxy
TyConI (DataD [] IdStarK.Proxy [KindedTV a_1627394516 (AppT (AppT (ConT IdStarK.Id) StarT) (VarT k_1627394515))] Nothing [NormalC IdStarK.Proxy []] [])
```
From the output, it appears that `Id` is being applied to *two* arguments, both `*` and `k`! Perhaps this indirectly (or directly) a consequence of #11376?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---------------- |
| Version | 8.0.1-rc1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Template Haskell |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | #11376 |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Template Haskell applies too many arguments to kind synonym","status":"New","operating_system":"","component":"Template Haskell","related":[11376],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc1","keywords":["TypeApplications","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"Running the following code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule IdStarK where\r\n\r\nimport Data.Kind\r\nimport Language.Haskell.TH\r\n\r\ntype Id a = a\r\ndata Proxy (a :: Id k) = Proxy\r\n\r\n$(return [])\r\n\r\nmain :: IO ()\r\nmain = do\r\n putStrLn $(reify ''Proxy >>= stringE . pprint)\r\n putStrLn $(reify ''Proxy >>= stringE . show)\r\n}}}\r\n\r\nGives a result I wouldn't have expected:\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/runghc IdStarK.hs \r\ndata IdStarK.Proxy (a_0 :: IdStarK.Id * k_1) = IdStarK.Proxy\r\nTyConI (DataD [] IdStarK.Proxy [KindedTV a_1627394516 (AppT (AppT (ConT IdStarK.Id) StarT) (VarT k_1627394515))] Nothing [NormalC IdStarK.Proxy []] [])\r\n}}}\r\n\r\nFrom the output, it appears that `Id` is being applied to ''two'' arguments, both `*` and `k`! Perhaps this indirectly (or directly) a consequence of #11376?","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11416GHC mistakenly believes datatype with type synonym in its type can't be eta-r...2019-07-07T18:30:31ZRyan ScottGHC mistakenly believes datatype with type synonym in its type can't be eta-reducedI uncovered this when playing around with `-XTypeInType`:
```hs
{-# LANGUAGE DeriveFunctor, TypeInType #-}
module CantEtaReduce1 where
import Data.Kind
type ConstantT a b = a
newtype T (f :: * -> *) (a :: ConstantT * f) = T (f a) deri...I uncovered this when playing around with `-XTypeInType`:
```hs
{-# LANGUAGE DeriveFunctor, TypeInType #-}
module CantEtaReduce1 where
import Data.Kind
type ConstantT a b = a
newtype T (f :: * -> *) (a :: ConstantT * f) = T (f a) deriving Functor
```
This fails because it thinks that you can't reduce the last type variable of `T`, since it mentions another type variable (`f`):
```
• Cannot eta-reduce to an instance of form
instance (...) => Functor (T f)
• In the newtype declaration for ‘T
```
But it *should* be able to, since `ConstantT * f` reduces to `*`, and the equivalent declaration `newtype T (f :: * -> *) (a :: *) = ...` eta-reduces just fine.
I marked this as appearing in GHC 8.1 since you need `-XTypeInType` to have kind synonyms, but this can also happen in earlier GHC versions with data families:
```hs
{-# LANGUAGE DeriveFunctor, PolyKinds, TypeFamilies #-}
module CantEtaReduce2 where
type ConstantT a b = a
data family T (f :: * -> *) (a :: *)
newtype instance T f (ConstantT a f) = T (f a) deriving Functor
```
I believe the fix will be to apply `coreView` with precision to parts of the code which typecheck `deriving` statements so that these type synonyms are peeled off.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC mistakenly believes datatype with type synonym in its type can't be eta-reduced","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"I uncovered this when playing around with `-XTypeInType`:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DeriveFunctor, TypeInType #-}\r\nmodule CantEtaReduce1 where\r\n\r\nimport Data.Kind\r\n\r\ntype ConstantT a b = a\r\nnewtype T (f :: * -> *) (a :: ConstantT * f) = T (f a) deriving Functor\r\n}}}\r\n\r\nThis fails because it thinks that you can't reduce the last type variable of `T`, since it mentions another type variable (`f`):\r\n\r\n{{{\r\n • Cannot eta-reduce to an instance of form\r\n instance (...) => Functor (T f)\r\n • In the newtype declaration for ‘T\r\n}}}\r\n\r\nBut it ''should'' be able to, since `ConstantT * f` reduces to `*`, and the equivalent declaration `newtype T (f :: * -> *) (a :: *) = ...` eta-reduces just fine.\r\n\r\nI marked this as appearing in GHC 8.1 since you need `-XTypeInType` to have kind synonyms, but this can also happen in earlier GHC versions with data families:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DeriveFunctor, PolyKinds, TypeFamilies #-}\r\nmodule CantEtaReduce2 where\r\n\r\ntype ConstantT a b = a\r\ndata family T (f :: * -> *) (a :: *)\r\nnewtype instance T f (ConstantT a f) = T (f a) deriving Functor\r\n}}}\r\n\r\nI believe the fix will be to apply `coreView` with precision to parts of the code which typecheck `deriving` statements so that these type synonyms are peeled off.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11404The type variable used in a kind is still used2019-07-07T18:30:34ZRichard Eisenbergrae@richarde.devThe type variable used in a kind is still usedFrom [D1739](https://phabricator.haskell.org/D1739).
When you say
```
undefined :: forall (v :: Levity) (a :: TYPE v). (?callStack :: CallStack) => a
```
you get a warning that `v` is unused.
I will fix.
<details><summary>Trac metad...From [D1739](https://phabricator.haskell.org/D1739).
When you say
```
undefined :: forall (v :: Levity) (a :: TYPE v). (?callStack :: CallStack) => a
```
you get a warning that `v` is unused.
I will fix.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.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":"The type variable used in a kind is still used","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"From Phab:D1739.\r\n\r\nWhen you say\r\n\r\n{{{\r\nundefined :: forall (v :: Levity) (a :: TYPE v). (?callStack :: CallStack) => a\r\n}}}\r\n\r\nyou get a warning that `v` is unused.\r\n\r\nI will fix.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11376Inconsistent specified type variables among functions and datatypes/classes w...2019-07-07T18:30:40ZRyan ScottInconsistent specified type variables among functions and datatypes/classes when using -XTypeApplicationsOriginally reported [here](https://mail.haskell.org/pipermail/ghc-devs/2016-January/010915.html). When applying types via `-XTypeApplications`, the type/kind that gets instantiated seems to be different depending on whether you're using ...Originally reported [here](https://mail.haskell.org/pipermail/ghc-devs/2016-January/010915.html). When applying types via `-XTypeApplications`, the type/kind that gets instantiated seems to be different depending on whether you're using functions, datatypes, or typeclasses.
Here's an example contrasting functions and datatypes:
```
$ /opt/ghc/head/bin/ghci
GHCi, version 8.1.20160106: http://www.haskell.org/ghc/ :? for help
λ> :set -fprint-explicit-kinds -XTypeApplications -XTypeInType
λ> data Prox a = Prox
λ> prox :: Prox a; prox = Prox
λ> :t prox
prox :: forall k (a :: k). Prox k a
λ> :t prox @Int
prox @Int :: Prox * Int
λ> :t Prox
Prox :: forall k (a :: k). Prox k a
λ> :t Prox @Int
Prox @Int :: Prox Int a
```
This is the core of the problem: with a function, `Int` seems to be applied to type variable `a`, whereas with data types, `Int` appears to be applied to the kind variable `k`. This confuses me, since `k` wasn't specified anywhere in the definition of `Prox`.
Andres Löh also [observed](https://mail.haskell.org/pipermail/ghc-devs/2016-January/010916.html) a similar discrepancy between functions and typeclasses:
```
λ> :set -XScopedTypeVariables
λ> class C a where c :: ()
λ> d :: forall a. C a => (); d = c @_ @a
λ> :t d
d :: forall k (a :: k). C k a => ()
λ> :t d @Int
d @Int :: C * Int => ()
λ> :t c
c :: forall k (a :: k). C k a => ()
λ> :t c @Int
c @Int :: C Int a => ()
λ> :t c @_ @Int
c @_ @Int :: C * Int => ()
```
EDIT: See also documentation infelicity in [ticket:11376\#comment:113518](https://gitlab.haskell.org//ghc/ghc/issues/11376#note_113518).
EDIT: Most of this is fix, as of March 25. But the data family stuff in [ticket:11376\#comment:114637](https://gitlab.haskell.org//ghc/ghc/issues/11376#note_114637) is still outstanding, and we need a test case.8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11362T6137 doesn't pass with reversed uniques2019-07-07T18:30:44ZniteriaT6137 doesn't pass with reversed uniquesIt fails with (full trace https://phabricator.haskell.org/P81):
```
*** Core Lint errors : in result of Tidy Core ***
<no location info>: warning:
[in body of lambda with binder dt_a18nYf :: In
...It fails with (full trace https://phabricator.haskell.org/P81):
```
*** Core Lint errors : in result of Tidy Core ***
<no location info>: warning:
[in body of lambda with binder dt_a18nYf :: In
f_a18o2M
(Sum1 r_a18o2L (In ('F f_a18o2M) r_a18o2L))
o_a18o2K]
Kind application error in
coercion ‘Sym
(TFCo:R:InioFro[0]
<o_a18nYC>_N <i_a18nYD>_N <f_a18o2M>_N) <r_a18o2L>_N <o_a18o2K>_N’
Function kind = Code (Sum i_a18nYD o_a18nYC) o_a18nYC -> *
Arg kinds = [(o_a18o2K, o_a18nYC)]
<no location info>: warning:
[in body of lambda with binder dt_a18nYf :: In
f_a18o2M
(Sum1 r_a18o2L (In ('F f_a18o2M) r_a18o2L))
o_a18o2K]
Kind application error in
coercion ‘Sym
(TFCo:R:InioFro[0]
<o_a18nYC>_N <i_a18nYD>_N <f_a18o2M>_N) <r_a18o2L>_N <o_a18o2K>_N’
Function kind = Code (Sum i_a18nYD o_a18nYC) o_a18nYC -> *
Arg kinds = [(o_a18o2K, o_a18nYC)]
```
Steps to reproduce:
1. Add line
`TEST_HC_OPTS += -dinitial-unique=16777000 -dunique-increment=-1`
after line
`TEST_HC_OPTS = -fforce-recomp -dcore-lint -dcmm-lint -dno-debug-output -no-user-$(GhcPackageDbFlag) -rtsopts $(EXTRA_HC_OPTS)`
in `mk/test.mk`
1. `make TESTS=T6137`
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | --------------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire, simonmar, simonpj |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"T6137 doesn't pass with reversed uniques","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","simonmar","simonpj"],"type":"Bug","description":"It fails with (full trace https://phabricator.haskell.org/P81):\r\n\r\n{{{\r\n*** Core Lint errors : in result of Tidy Core ***\r\n<no location info>: warning:\r\n [in body of lambda with binder dt_a18nYf :: In\r\n f_a18o2M\r\n (Sum1 r_a18o2L (In ('F f_a18o2M) r_a18o2L))\r\n o_a18o2K]\r\n Kind application error in\r\n coercion ‘Sym\r\n (TFCo:R:InioFro[0]\r\n <o_a18nYC>_N <i_a18nYD>_N <f_a18o2M>_N) <r_a18o2L>_N <o_a18o2K>_N’\r\n Function kind = Code (Sum i_a18nYD o_a18nYC) o_a18nYC -> *\r\n Arg kinds = [(o_a18o2K, o_a18nYC)]\r\n<no location info>: warning:\r\n [in body of lambda with binder dt_a18nYf :: In\r\n f_a18o2M\r\n (Sum1 r_a18o2L (In ('F f_a18o2M) r_a18o2L))\r\n o_a18o2K]\r\n Kind application error in\r\n coercion ‘Sym\r\n (TFCo:R:InioFro[0]\r\n <o_a18nYC>_N <i_a18nYD>_N <f_a18o2M>_N) <r_a18o2L>_N <o_a18o2K>_N’\r\n Function kind = Code (Sum i_a18nYD o_a18nYC) o_a18nYC -> *\r\n Arg kinds = [(o_a18o2K, o_a18nYC)]\r\n}}}\r\n\r\n\r\nSteps to reproduce:\r\n\r\n1. Add line\r\n`TEST_HC_OPTS += -dinitial-unique=16777000 -dunique-increment=-1` \r\n\r\nafter line\r\n\r\n`TEST_HC_OPTS = -fforce-recomp -dcore-lint -dcmm-lint -dno-debug-output -no-user-$(GhcPackageDbFlag) -rtsopts $(EXTRA_HC_OPTS)` \r\n\r\nin `mk/test.mk`\r\n\r\n2. `make TESTS=T6137`\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1niterianiteriahttps://gitlab.haskell.org/ghc/ghc/-/issues/11356GHC panic2019-07-07T18:30:46ZIcelandjackGHC panicThe attached file causes GHC (version 8.1.20160102) panic.
I tried shrinking, attached code is bogus at this point.
Interestingly inlining the type synonym `T = Nat` into Category's superclass context fixes the panic, and causes a regu...The attached file causes GHC (version 8.1.20160102) panic.
I tried shrinking, attached code is bogus at this point.
Interestingly inlining the type synonym `T = Nat` into Category's superclass context fixes the panic, and causes a regular error.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The attached file causes GHC (version 8.1.20160102) panic.\r\n\r\nI tried shrinking, attached code is bogus at this point.\r\n\r\nInterestingly inlining the type synonym `T = Nat` into Category's superclass context fixes the panic, and causes a regular error.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/11252:kind command hides the explicit kind2019-07-07T18:31:15ZIcelandjack:kind command hides the explicit kind```hs
-- /tmp/test.hs
{-# LANGUAGE TypeInType #-}
data Proxy1 k (a :: k) = P1
data Proxy2 (a :: k) = P2
```
if I load the following into ghci (head) the `:kind` command gives the same result
```haskell
% ghci -ignore-dot-ghci /tmp/t...```hs
-- /tmp/test.hs
{-# LANGUAGE TypeInType #-}
data Proxy1 k (a :: k) = P1
data Proxy2 (a :: k) = P2
```
if I load the following into ghci (head) the `:kind` command gives the same result
```haskell
% ghci -ignore-dot-ghci /tmp/test.hs
GHCi, version 7.11.20151216: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( test.hs, interpreted )
Ok, modules loaded: Main.
*Main> :kind Proxy1
Proxy1 :: k -> *
*Main> :kind Proxy2
Proxy2 :: k -> *
```
edit: I asked on \#ghc, was told this was undesirable8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11241Kind-level PartialTypeSignatures causes internal error2019-07-07T18:31:19ZAdam GundryKind-level PartialTypeSignatures causes internal errorConsider the following module:
```hs
{-# LANGUAGE ExplicitForAll, KindSignatures, PartialTypeSignatures #-}
foo :: forall (a :: _) . a -> a
foo = id
```
In HEAD, this fails with an internal errror:
```
• GHC internal error: ‘_’...Consider the following module:
```hs
{-# LANGUAGE ExplicitForAll, KindSignatures, PartialTypeSignatures #-}
foo :: forall (a :: _) . a -> a
foo = id
```
In HEAD, this fails with an internal errror:
```
• GHC internal error: ‘_’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: []
• In the kind ‘_’
In the type signature:
foo :: forall (a :: _). a -> a
```
I would expect it to succeed and figure out that the wildcard is `*`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Kind-level PartialTypeSignatures causes internal error","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"Consider the following module:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ExplicitForAll, KindSignatures, PartialTypeSignatures #-}\r\n\r\nfoo :: forall (a :: _) . a -> a \r\nfoo = id \r\n}}}\r\n\r\nIn HEAD, this fails with an internal errror:\r\n\r\n{{{\r\n • GHC internal error: ‘_’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: []\r\n • In the kind ‘_’\r\n In the type signature:\r\n foo :: forall (a :: _). a -> a\r\n}}}\r\n\r\nI would expect it to succeed and figure out that the wildcard is `*`.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11339Possible type-checker regression in GHC 8.02019-07-07T18:30:52ZHerbert Valerio Riedelhvr@gnu.orgPossible type-checker regression in GHC 8.0The following code (extracted from hackage:microlens) type-checks on GHC 7.10 but **not** on GHC 8.0/8.1:
```hs
{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
module Failing where
import Control.Applicative ( Const(Const, getConst) ...The following code (extracted from hackage:microlens) type-checks on GHC 7.10 but **not** on GHC 8.0/8.1:
```hs
{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
module Failing where
import Control.Applicative ( Const(Const, getConst) )
import Data.Functor.Identity ( Identity(Identity) )
type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
failing :: forall s t a b . Traversal s t a b -> Traversal s t a b -> Traversal s t a b
failing left right afb s = case pins t of
[] -> right afb s
_ -> t afb
where
-- t :: (a -> f b) -> f t
-- TYPECHECKS with GHC 7.10, but not with GHC 8.x:
Bazaar { getBazaar = t } = left sell s
-- FAILS TO TYPECHECK with GHC 7.10 and GHC 8.x:
-- t = getBazaar (left sell s)
sell :: a -> Bazaar a b b
sell w = Bazaar ($ w)
pins :: ((a -> Const [Identity a] b) -> Const [Identity a] t) -> [Identity a]
pins f = getConst (f (\ra -> Const [Identity ra]))
newtype Bazaar a b t = Bazaar { getBazaar :: (forall f. Applicative f => (a -> f b) -> f t) }
instance Functor (Bazaar a b) where
fmap f (Bazaar k) = Bazaar (fmap f . k)
instance Applicative (Bazaar a b) where
pure a = Bazaar $ \_ -> pure a
Bazaar mf <*> Bazaar ma = Bazaar $ \afb -> mf afb <*> ma afb
```
The following error is emitted on GHC 8.0:
```
failing.hs:13:11: error:
• Couldn't match type ‘f’ with ‘Const [Identity a]’
‘f’ is a rigid type variable bound by
the type signature for:
failing :: forall (f :: * -> *). Applicative f => Traversal s t a b -> Traversal s t a b -> (a -> f b) -> s -> f t
at failing.hs:11:1
Expected type: a -> Const [Identity a] b
Actual type: a -> f b
• In the first argument of ‘t’, namely ‘afb’
In the expression: t afb
In a case alternative: _ -> t afb
• Relevant bindings include
t :: (a -> Const [Identity a] b) -> Const [Identity a] t (bound at failing.hs:18:26)
sell :: a -> Bazaar a b b (bound at failing.hs:24:5)
pins :: ((a -> Const [Identity a] b) -> Const [Identity a] t) -> [Identity a] (bound at failing.hs:27:5)
afb :: a -> f b (bound at failing.hs:11:20)
right :: Traversal s t a b (bound at failing.hs:11:14)
left :: Traversal s t a b (bound at failing.hs:11:9)
failing :: Traversal s t a b -> Traversal s t a b -> Traversal s t a b (bound at failing.hs:11:1)
```
I don't understand why `Bazaar t = ...` vs `t = getBazaar ...` makes a difference in GHC 7.10 at all. So I'm not sure if this is a regression or actually something that got fixed in GHC 8.0...
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | bgamari, simonpj |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Possible type-checker regression in GHC 8.0","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["bgamari","simonpj"],"type":"Bug","description":"The following code (extracted from hackage:microlens) type-checks on GHC 7.10 but '''not''' on GHC 8.0/8.1:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}\r\n\r\nmodule Failing where\r\n\r\nimport Control.Applicative ( Const(Const, getConst) )\r\nimport Data.Functor.Identity ( Identity(Identity) )\r\n\r\ntype Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t\r\n\r\nfailing :: forall s t a b . Traversal s t a b -> Traversal s t a b -> Traversal s t a b\r\nfailing left right afb s = case pins t of\r\n [] -> right afb s\r\n _ -> t afb\r\n where\r\n -- t :: (a -> f b) -> f t\r\n\r\n -- TYPECHECKS with GHC 7.10, but not with GHC 8.x:\r\n Bazaar { getBazaar = t } = left sell s\r\n\r\n -- FAILS TO TYPECHECK with GHC 7.10 and GHC 8.x:\r\n -- t = getBazaar (left sell s)\r\n\r\n sell :: a -> Bazaar a b b\r\n sell w = Bazaar ($ w)\r\n\r\n pins :: ((a -> Const [Identity a] b) -> Const [Identity a] t) -> [Identity a]\r\n pins f = getConst (f (\\ra -> Const [Identity ra]))\r\n\r\nnewtype Bazaar a b t = Bazaar { getBazaar :: (forall f. Applicative f => (a -> f b) -> f t) }\r\n\r\ninstance Functor (Bazaar a b) where\r\n fmap f (Bazaar k) = Bazaar (fmap f . k)\r\n\r\ninstance Applicative (Bazaar a b) where\r\n pure a = Bazaar $ \\_ -> pure a\r\n Bazaar mf <*> Bazaar ma = Bazaar $ \\afb -> mf afb <*> ma afb\r\n}}}\r\n\r\nThe following error is emitted on GHC 8.0:\r\n\r\n{{{\r\nfailing.hs:13:11: error:\r\n • Couldn't match type ‘f’ with ‘Const [Identity a]’\r\n ‘f’ is a rigid type variable bound by\r\n the type signature for:\r\n failing :: forall (f :: * -> *). Applicative f => Traversal s t a b -> Traversal s t a b -> (a -> f b) -> s -> f t\r\n at failing.hs:11:1\r\n Expected type: a -> Const [Identity a] b\r\n Actual type: a -> f b\r\n • In the first argument of ‘t’, namely ‘afb’\r\n In the expression: t afb\r\n In a case alternative: _ -> t afb\r\n • Relevant bindings include\r\n t :: (a -> Const [Identity a] b) -> Const [Identity a] t (bound at failing.hs:18:26)\r\n sell :: a -> Bazaar a b b (bound at failing.hs:24:5)\r\n pins :: ((a -> Const [Identity a] b) -> Const [Identity a] t) -> [Identity a] (bound at failing.hs:27:5)\r\n afb :: a -> f b (bound at failing.hs:11:20)\r\n right :: Traversal s t a b (bound at failing.hs:11:14)\r\n left :: Traversal s t a b (bound at failing.hs:11:9)\r\n failing :: Traversal s t a b -> Traversal s t a b -> Traversal s t a b (bound at failing.hs:11:1)\r\n}}}\r\n\r\n\r\nI don't understand why `Bazaar t = ...` vs `t = getBazaar ...` makes a difference in GHC 7.10 at all. So I'm not sure if this is a regression or actually something that got fixed in GHC 8.0...","type_of_failure":"OtherFailure","blocking":[]} -->8.0.2Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/11821Internal error: not in scope during type checking, but it passed the renamer2019-07-07T18:28:23ZdarchonInternal error: not in scope during type checking, but it passed the renamerWhile trying to get the singletons package to compile on GHC8 (https://github.com/goldfirere/singletons/pull/142), I encountered the following error while trying to track down a bug:
```
[1 of 1] Compiling NotInScope ( NotInScope....While trying to get the singletons package to compile on GHC8 (https://github.com/goldfirere/singletons/pull/142), I encountered the following error while trying to track down a bug:
```
[1 of 1] Compiling NotInScope ( NotInScope.hs, interpreted )
NotInScope.hs:22:20: error:
• GHC internal error: ‘b’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [a1lm :-> Type variable ‘b’ = b,
a1lA :-> Type variable ‘l1’ = l1, a1lB :-> Type variable ‘l2’ = l2,
a1lC :-> Type variable ‘l3’ = l3, a1lE :-> Type variable ‘a’ = a,
a1lF :-> Type variable ‘l4’ = l4, r1aq :-> ATcTyCon Lgo,
r1aG :-> ATcTyCon Lgo1, r1aI :-> ATcTyCon Lgo2]
• In the kind ‘b’
In the definition of data constructor ‘Lgo1KindInference’
In the data declaration for ‘Lgo1’
```
for the following code:
```
{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances #-}
module NotInScope where
import Data.Proxy
type KindOf (a :: k) = ('KProxy :: KProxy k)
data TyFun :: * -> * -> *
type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
data Lgo2 l1
l2
l3
(l4 :: b)
(l5 :: TyFun [a] b)
= forall (arg :: [a]) . KindOf (Apply (Lgo2 l1 l2 l3 l4) arg) ~ KindOf (Lgo l1 l2 l3 l4 arg) =>
Lgo2KindInference
data Lgo1 l1
l2
l3
(l4 :: TyFun b (TyFun [a] b -> *))
= forall (arg :: b) . KindOf (Apply (Lgo1 l1 l2 l3) arg) ~ KindOf (Lgo2 l1 l2 l3 arg) =>
Lgo1KindInference
type family Lgo f
z0
xs0
(a1 :: b)
(a2 :: [a]) :: b where
Lgo f z0 xs0 z '[] = z
Lgo f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 f z0 xs0) (Apply (Apply f z) x)) xs
```
Note that the above code works fine in GHC 7.10.2.
There are two options to make the code compile on GHC8-rc3:
- Remove the kind annotations on the `forall arg .` binders
- Or make the following changes using TypeInType:
```
{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances, TypeInType #-}
module NotInScope where
import Data.Proxy
import GHC.Types
type KindOf (a :: k) = ('KProxy :: KProxy k)
data TyFun :: * -> * -> *
type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
data Lgo2 a
b
l1
l2
l3
(l4 :: b)
(l5 :: TyFun [a] b)
= forall (arg :: [a]) . KindOf (Apply (Lgo2 a b l1 l2 l3 l4) arg) ~ KindOf (Lgo a b l1 l2 l3 l4 arg) =>
Lgo2KindInference
data Lgo1 a
b
l1
l2
l3
(l4 :: TyFun b (TyFun [a] b -> *))
= forall (arg :: b) . KindOf (Apply (Lgo1 a b l1 l2 l3) arg) ~ KindOf (Lgo2 a b l1 l2 l3 arg) =>
Lgo1KindInference
type family Lgo a
b
f
z0
xs0
(a1 :: b)
(a2 :: [a]) :: b where
Lgo a b f z0 xs0 z '[] = z
Lgo a b f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 a b f z0 xs0) (Apply (Apply f z) x)) xs
```
I'm sorry I didn't create a smaller test case. Let me know if one is required and I'll try.
The error seems to be related to the recursive aspect of the three definitions and how implicit kind variables are handled in ghc8.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1-rc3 |
| 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":"Internal error: not in scope during type checking, but it passed the renamer","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"While trying to get the singletons package to compile on GHC8 (https://github.com/goldfirere/singletons/pull/142), I encountered the following error while trying to track down a bug:\r\n\r\n{{{\r\n[1 of 1] Compiling NotInScope ( NotInScope.hs, interpreted )\r\n\r\nNotInScope.hs:22:20: error:\r\n • GHC internal error: ‘b’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [a1lm :-> Type variable ‘b’ = b,\r\n a1lA :-> Type variable ‘l1’ = l1, a1lB :-> Type variable ‘l2’ = l2,\r\n a1lC :-> Type variable ‘l3’ = l3, a1lE :-> Type variable ‘a’ = a,\r\n a1lF :-> Type variable ‘l4’ = l4, r1aq :-> ATcTyCon Lgo,\r\n r1aG :-> ATcTyCon Lgo1, r1aI :-> ATcTyCon Lgo2]\r\n • In the kind ‘b’\r\n In the definition of data constructor ‘Lgo1KindInference’\r\n In the data declaration for ‘Lgo1’\r\n}}}\r\n\r\nfor the following code:\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances #-}\r\nmodule NotInScope where\r\n\r\nimport Data.Proxy\r\n\r\ntype KindOf (a :: k) = ('KProxy :: KProxy k)\r\ndata TyFun :: * -> * -> *\r\ntype family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2\r\n\r\ndata Lgo2 l1\r\n l2\r\n l3\r\n (l4 :: b)\r\n (l5 :: TyFun [a] b)\r\n = forall (arg :: [a]) . KindOf (Apply (Lgo2 l1 l2 l3 l4) arg) ~ KindOf (Lgo l1 l2 l3 l4 arg) =>\r\n Lgo2KindInference\r\n\r\ndata Lgo1 l1\r\n l2\r\n l3\r\n (l4 :: TyFun b (TyFun [a] b -> *))\r\n = forall (arg :: b) . KindOf (Apply (Lgo1 l1 l2 l3) arg) ~ KindOf (Lgo2 l1 l2 l3 arg) =>\r\n Lgo1KindInference\r\n\r\ntype family Lgo f\r\n z0\r\n xs0\r\n (a1 :: b)\r\n (a2 :: [a]) :: b where\r\n Lgo f z0 xs0 z '[] = z\r\n Lgo f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 f z0 xs0) (Apply (Apply f z) x)) xs\r\n}}}\r\n\r\nNote that the above code works fine in GHC 7.10.2.\r\n\r\nThere are two options to make the code compile on GHC8-rc3:\r\n* Remove the kind annotations on the {{{forall arg .}}} binders\r\n* Or make the following changes using TypeInType:\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances, TypeInType #-}\r\nmodule NotInScope where\r\n\r\nimport Data.Proxy\r\nimport GHC.Types\r\n\r\ntype KindOf (a :: k) = ('KProxy :: KProxy k)\r\ndata TyFun :: * -> * -> *\r\ntype family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2\r\n\r\ndata Lgo2 a\r\n b\r\n l1\r\n l2\r\n l3\r\n (l4 :: b)\r\n (l5 :: TyFun [a] b)\r\n = forall (arg :: [a]) . KindOf (Apply (Lgo2 a b l1 l2 l3 l4) arg) ~ KindOf (Lgo a b l1 l2 l3 l4 arg) =>\r\n Lgo2KindInference\r\n\r\ndata Lgo1 a\r\n b\r\n l1\r\n l2\r\n l3\r\n (l4 :: TyFun b (TyFun [a] b -> *))\r\n = forall (arg :: b) . KindOf (Apply (Lgo1 a b l1 l2 l3) arg) ~ KindOf (Lgo2 a b l1 l2 l3 arg) =>\r\n Lgo1KindInference\r\n\r\ntype family Lgo a\r\n b\r\n f\r\n z0\r\n xs0\r\n (a1 :: b)\r\n (a2 :: [a]) :: b where\r\n Lgo a b f z0 xs0 z '[] = z\r\n Lgo a b f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 a b f z0 xs0) (Apply (Apply f z) x)) xs\r\n}}}\r\n\r\nI'm sorry I didn't create a smaller test case. Let me know if one is required and I'll try.\r\nThe error seems to be related to the recursive aspect of the three definitions and how implicit kind variables are handled in ghc8.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.2https://gitlab.haskell.org/ghc/ghc/-/issues/11484Type synonym using -XTypeInType can't be spliced with TH2019-07-07T18:30:13ZRyan ScottType synonym using -XTypeInType can't be spliced with THThe following code compiles:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -ddump-splices #-}
module Foo where
import Data.Kind
type TySyn (k :: *) (a :: k) = ()
-- $([d| type TySyn2 (k :: *) (a :...The following code compiles:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -ddump-splices #-}
module Foo where
import Data.Kind
type TySyn (k :: *) (a :: k) = ()
-- $([d| type TySyn2 (k :: *) (a :: k) = () |])
```
But uncomment the last line, and it doesn't compile:
```
$ /opt/ghc/head/bin/ghc Foo.hs
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
Foo.hs:10:3-43: Splicing declarations
[d| type TySyn2_aBH (k_aBI :: *) (a_aBJ :: k_aBI) = () |]
======>
type TySyn2_a4BF (k_a4BG :: Type) (a_a4BH :: k_a4BG) = ()
Foo.hs:10:3: error:
• Couldn't match expected kind ‘GHC.Prim.Any’ with actual kind ‘k1’
• In the type declaration for ‘TySyn2’
Foo.hs:10:3: error:
• Kind variable ‘k_a4BG’ is implicitly bound in datatype
‘TySyn2’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it (with TypeInType) explicitly somewhere?
Type variables with inferred kinds: k_a4BG (a_a4BH :: GHC.Prim.Any)
• In the type declaration for ‘TySyn2’
```
There are two issues here:
1. The error message claims that `TySyn2` is a datatype when it is actually a type synonym. This should be easy enough to fix; just change [the code](http://git.haskell.org/ghc.git/blob/89bdac7635e6ed08927d760aa885d3e7ef3edb81:/compiler/typecheck/TcHsType.hs#l1874) that throws the error message to invoke [tyConFlavour](http://git.haskell.org/ghc.git/blob/89bdac7635e6ed08927d760aa885d3e7ef3edb81:/compiler/types/TyCon.hs#l1957).
1. For some reason, the type variable `a` in `TySyn2` fails to kind-check. Somehow, an `Any` got in there, but I'm not sure where it snuck in.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---------------- |
| Version | 8.0.1-rc1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Template Haskell |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Type synonym using -XTypeInType can't be spliced with TH","status":"New","operating_system":"","component":"Template Haskell","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"The following code compiles:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# OPTIONS_GHC -ddump-splices #-}\r\nmodule Foo where\r\n\r\nimport Data.Kind\r\n\r\ntype TySyn (k :: *) (a :: k) = ()\r\n\r\n-- $([d| type TySyn2 (k :: *) (a :: k) = () |])\r\n}}}\r\n\r\nBut uncomment the last line, and it doesn't compile:\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/ghc Foo.hs \r\n[1 of 1] Compiling Foo ( Foo.hs, Foo.o )\r\nFoo.hs:10:3-43: Splicing declarations\r\n [d| type TySyn2_aBH (k_aBI :: *) (a_aBJ :: k_aBI) = () |]\r\n ======>\r\n type TySyn2_a4BF (k_a4BG :: Type) (a_a4BH :: k_a4BG) = ()\r\n\r\nFoo.hs:10:3: error:\r\n • Couldn't match expected kind ‘GHC.Prim.Any’ with actual kind ‘k1’\r\n • In the type declaration for ‘TySyn2’\r\n\r\nFoo.hs:10:3: error:\r\n • Kind variable ‘k_a4BG’ is implicitly bound in datatype\r\n ‘TySyn2’, but does not appear as the kind of any\r\n of its type variables. Perhaps you meant\r\n to bind it (with TypeInType) explicitly somewhere?\r\n Type variables with inferred kinds: k_a4BG (a_a4BH :: GHC.Prim.Any)\r\n • In the type declaration for ‘TySyn2’\r\n}}}\r\n\r\nThere are two issues here:\r\n\r\n1. The error message claims that `TySyn2` is a datatype when it is actually a type synonym. This should be easy enough to fix; just change [http://git.haskell.org/ghc.git/blob/89bdac7635e6ed08927d760aa885d3e7ef3edb81:/compiler/typecheck/TcHsType.hs#l1874 the code] that throws the error message to invoke [http://git.haskell.org/ghc.git/blob/89bdac7635e6ed08927d760aa885d3e7ef3edb81:/compiler/types/TyCon.hs#l1957 tyConFlavour].\r\n2. For some reason, the type variable `a` in `TySyn2` fails to kind-check. Somehow, an `Any` got in there, but I'm not sure where it snuck in.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.2https://gitlab.haskell.org/ghc/ghc/-/issues/13585ala from Control.Lens.Wrapped panics2019-07-07T18:21:10ZFumiaki Kinoshitaala from Control.Lens.Wrapped panicsPanic.hs:
```
module Panic where
import Control.Lens.Wrapped
import Data.Monoid
foo :: Maybe String
foo = ala Last foldMap [Just "foo"]
```
main.hs:
```
module Main where
import Panic (foo)
main :: IO ()
main = print foo
```
```
$...Panic.hs:
```
module Panic where
import Control.Lens.Wrapped
import Data.Monoid
foo :: Maybe String
foo = ala Last foldMap [Just "foo"]
```
main.hs:
```
module Main where
import Panic (foo)
main :: IO ()
main = print foo
```
```
$ ghc -c -O2 Panic.hs
$ ghc -c -O2 main.hs
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.0.20170404 for x86_64-unknown-linux):
splitTyConApp
(Exchange (Unwrapped (Last String)) (Unwrapped (Last String)) |> <*
-> * -> *>_N) (Maybe
[Char]) ((Identity |> <*
-> *>_N) (Maybe
[Char]))
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1134:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1105:34 in ghc:Type
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
The GHC version is 8134f7d4ba2c14b2f24d2f4c1f5260fcaff3304a.
Control.Lens.Wrapped is from the latest version of lens on GitHub: https://github.com/ekmett/lens/blob/9c4447de7ef57f67dbe293320d45bd8a546be522/src/Control/Lens/Wrapped.hs8.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/13333Typeable regression in GHC HEAD2019-07-07T18:22:24ZRyan ScottTypeable regression in GHC HEADI recently wrote some code while exploring a fix for #13327 that heavily uses poly-kinded `Typeable`. This compiles without issue on GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGU...I recently wrote some code while exploring a fix for #13327 that heavily uses poly-kinded `Typeable`. This compiles without issue on GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module DataCast where
import Data.Data
import GHC.Exts (Constraint)
data T (phantom :: k) = T
data D (p :: k -> Constraint) (x :: j) where
D :: forall (p :: k -> Constraint) (x :: k). p x => D p x
class Possibly p x where
possibly :: proxy1 p -> proxy2 x -> Maybe (D p x)
dataCast1T :: forall k c t (phantom :: k).
(Typeable k, Typeable t, Typeable phantom, Possibly Data phantom)
=> (forall d. Data d => c (t d))
-> Maybe (c (T phantom))
dataCast1T f = case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of
Nothing -> Nothing
Just D -> gcast1 f
```
But on GHC HEAD, it barfs this error:
```
$ ~/Software/ghc2/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.1.20170223: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling DataCast ( Bug.hs, interpreted )
Bug.hs:28:29: error:
• Could not deduce (Typeable T) arising from a use of ‘gcast1’
GHC can't yet do polykinded Typeable (T :: * -> *)
from the context: (Typeable k, Typeable t, Typeable phantom,
Possibly Data phantom)
bound by the type signature for:
dataCast1T :: (Typeable k, Typeable t, Typeable phantom,
Possibly Data phantom) =>
(forall d. Data d => c (t d)) -> Maybe (c (T phantom))
at Bug.hs:(22,1)-(25,35)
or from: (k ~ *, (phantom :: k) ~~ (x :: *), Data x)
bound by a pattern with constructor:
D :: forall k (p :: k -> Constraint) (x :: k). p x => D p x,
in a case alternative
at Bug.hs:28:23
• In the expression: gcast1 f
In a case alternative: Just D -> gcast1 f
In the expression:
case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of
Nothing -> Nothing
Just D -> gcast1 f
|
28 | Just D -> gcast1 f
| ^^^^^^^^
```
That error message itself is hilariously strange, since GHC certainly has the power to do polykinded `Typeable` nowadays.
Marking as high priority since this is a regression—feel free to lower the priority if you disagree.8.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12174Recursive use of type-in-type results in infinite loop2020-09-19T19:52:25ZEdward Z. YangRecursive use of type-in-type results in infinite loopTypechecking this module results in an infinite loop:
```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeInType #-}
module X where
data V a
data T = forall (a :: S...Typechecking this module results in an infinite loop:
```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeInType #-}
module X where
data V a
data T = forall (a :: S). MkT (V a)
data S = forall (a :: T). MkS (V a)
```
There's a mutually recursive reference so it should be rejected but maybe the check is not happening early enough (or the existing check is only for self-reference.)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Recursive use of type-in-type results in infinite loop","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Typechecking this module results in an infinite loop:\r\n\r\n{{{\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE ExistentialQuantification #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule X where\r\n\r\ndata V a\r\ndata T = forall (a :: S). MkT (V a)\r\ndata S = forall (a :: T). MkS (V a)\r\n}}}\r\n\r\nThere's a mutually recursive reference so it should be rejected but maybe the check is not happening early enough (or the existing check is only for self-reference.)","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/13915GHC 8.2 regression: "Can't find interface-file declaration" for promoted data...2019-07-07T18:19:30ZRyan ScottGHC 8.2 regression: "Can't find interface-file declaration" for promoted data family instanceDue to #12088, you can't define a data family instance and promote it in the same module. One could, up until GHC 8.2, work around this using (somewhat obscure) wisdom: define the data family instance in a separate module from where it's...Due to #12088, you can't define a data family instance and promote it in the same module. One could, up until GHC 8.2, work around this using (somewhat obscure) wisdom: define the data family instance in a separate module from where it's promoted. For example, `Bug` typechecks in GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE TypeFamilies #-}
module Foo where
data family T a
data instance T Int = MkT
```
```hs
{-# LANGUAGE TypeInType #-}
module Bug where
import Foo
data Proxy (a :: k)
data S = MkS (Proxy 'MkT)
```
However, this stopped typechecking in GHC 8.2:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 2] Compiling Foo ( Foo.hs, interpreted )
[2 of 2] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:1:1: error:
Can't find interface-file declaration for variable Foo.$tc'MkT
Probable cause: bug in .hi-boot file, or inconsistent .hi file
Use -ddump-if-trace to get an idea of which file caused the error
|
1 | {-# LANGUAGE TypeInType #-}
| ^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC 8.2 regression: \"Can't find interface-file declaration\" for promoted data family instance","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Due to #12088, you can't define a data family instance and promote it in the same module. One could, up until GHC 8.2, work around this using (somewhat obscure) wisdom: define the data family instance in a separate module from where it's promoted. For example, `Bug` typechecks in GHC 8.0.1 and 8.0.2:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\nmodule Foo where\r\n\r\ndata family T a\r\ndata instance T Int = MkT\r\n}}}\r\n{{{#!hs\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Foo\r\n\r\ndata Proxy (a :: k)\r\ndata S = MkS (Proxy 'MkT)\r\n}}}\r\n\r\nHowever, this stopped typechecking in GHC 8.2:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 2] Compiling Foo ( Foo.hs, interpreted )\r\n[2 of 2] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:1:1: error:\r\n Can't find interface-file declaration for variable Foo.$tc'MkT\r\n Probable cause: bug in .hi-boot file, or inconsistent .hi file\r\n Use -ddump-if-trace to get an idea of which file caused the error\r\n |\r\n1 | {-# LANGUAGE TypeInType #-}\r\n | ^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/13871GHC panic in 8.2 only: typeIsTypeable(Coercion)2019-07-07T18:19:45ZRyan ScottGHC panic in 8.2 only: typeIsTypeable(Coercion)This code works fine in GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind
data...This code works fine in GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind
data Foo (a :: Type) (b :: Type) where
MkFoo :: (a ~ Int, b ~ Char) => Foo a b
data family Sing (a :: k)
data SFoo (z :: Foo a b) where
SMkFoo :: SFoo MkFoo
```
But in GHC 8.2 and HEAD, it panics:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170622: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Bug.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.0.20170622 for x86_64-unknown-linux):
typeIsTypeable(Coercion)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1-rc2 |
| 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 panic in 8.2 only: typeIsTypeable(Coercion)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":["TypeInType,","Typeable"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code works fine in GHC 8.0.1 and 8.0.2:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ConstraintKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Foo where\r\n\r\nimport Data.Kind\r\n\r\ndata Foo (a :: Type) (b :: Type) where\r\n MkFoo :: (a ~ Int, b ~ Char) => Foo a b\r\n\r\ndata family Sing (a :: k)\r\ndata SFoo (z :: Foo a b) where\r\n SMkFoo :: SFoo MkFoo\r\n}}}\r\n\r\nBut in GHC 8.2 and HEAD, it panics:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170622: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Foo ( Bug.hs, interpreted )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.2.0.20170622 for x86_64-unknown-linux):\r\n\ttypeIsTypeable(Coercion)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1Ben GamariBen Gamarihttps://gitlab.haskell.org/ghc/ghc/-/issues/13555Typechecker regression when combining PolyKinds and MonoLocalBinds2019-07-07T18:21:21ZRyan ScottTypechecker regression when combining PolyKinds and MonoLocalBinds`lol-0.6.0.0` from Hackage currently fails to build with GHC 8.2.1 because of this regression. Here is a minimized example:
```hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUA...`lol-0.6.0.0` from Hackage currently fails to build with GHC 8.2.1 because of this regression. Here is a minimized example:
```hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Crypto.Lol.Types.FiniteField (GF(..)) where
import Data.Functor.Identity (Identity(..))
data T a
type Polynomial a = T a
newtype GF fp d = GF (Polynomial fp)
type CRTInfo r = (Int -> r, r)
type Tagged s b = TaggedT s Identity b
newtype TaggedT s m b = TagT { untagT :: m b }
class Reflects a i where
value :: Tagged a i
class CRTrans mon r where
crtInfo :: Reflects m Int => TaggedT m mon (CRTInfo r)
instance CRTrans Maybe (GF fp d) where
crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))
crtInfo = undefined
```
This typechecks OK with GHC 8.0.2, but with 8.2.1, it complains:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170403: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Crypto.Lol.Types.FiniteField ( Bug.hs, interpreted )
Bug.hs:25:14: error:
• Couldn't match type ‘k0’ with ‘k2’
because type variable ‘k2’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for:
crtInfo :: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
at Bug.hs:25:14-79
Expected type: TaggedT m Maybe (CRTInfo (GF fp d))
Actual type: TaggedT m Maybe (CRTInfo (GF fp d))
• When checking that instance signature for ‘crtInfo’
is more general than its signature in the class
Instance sig: forall (m :: k0).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
Class sig: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
In the instance declaration for ‘CRTrans Maybe (GF fp d)’
|
25 | crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:25:14: error:
• Could not deduce (Reflects m Int)
from the context: Reflects m Int
bound by the type signature for:
crtInfo :: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
at Bug.hs:25:14-79
The type variable ‘k0’ is ambiguous
• When checking that instance signature for ‘crtInfo’
is more general than its signature in the class
Instance sig: forall (m :: k0).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
Class sig: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
In the instance declaration for ‘CRTrans Maybe (GF fp d)’
|
25 | crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Notably, both `PolyKinds` and `MonoLocalBinds` are required to trigger this bug.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typechecker regression when combining PolyKinds and MonoLocalBinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"`lol-0.6.0.0` from Hackage currently fails to build with GHC 8.2.1 because of this regression. Here is a minimized example:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE InstanceSigs #-}\r\n{-# LANGUAGE MonoLocalBinds #-}\r\n{-# LANGUAGE MultiParamTypeClasses #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\nmodule Crypto.Lol.Types.FiniteField (GF(..)) where\r\n\r\nimport Data.Functor.Identity (Identity(..))\r\n\r\ndata T a\r\ntype Polynomial a = T a\r\nnewtype GF fp d = GF (Polynomial fp)\r\ntype CRTInfo r = (Int -> r, r)\r\ntype Tagged s b = TaggedT s Identity b\r\nnewtype TaggedT s m b = TagT { untagT :: m b }\r\n\r\nclass Reflects a i where\r\n value :: Tagged a i\r\n\r\nclass CRTrans mon r where\r\n crtInfo :: Reflects m Int => TaggedT m mon (CRTInfo r)\r\n\r\ninstance CRTrans Maybe (GF fp d) where\r\n crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))\r\n crtInfo = undefined\r\n}}}\r\n\r\nThis typechecks OK with GHC 8.0.2, but with 8.2.1, it complains:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170403: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Crypto.Lol.Types.FiniteField ( Bug.hs, interpreted )\r\n\r\nBug.hs:25:14: error:\r\n • Couldn't match type ‘k0’ with ‘k2’\r\n because type variable ‘k2’ would escape its scope\r\n This (rigid, skolem) type variable is bound by\r\n the type signature for:\r\n crtInfo :: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n at Bug.hs:25:14-79\r\n Expected type: TaggedT m Maybe (CRTInfo (GF fp d))\r\n Actual type: TaggedT m Maybe (CRTInfo (GF fp d))\r\n • When checking that instance signature for ‘crtInfo’\r\n is more general than its signature in the class\r\n Instance sig: forall (m :: k0).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n Class sig: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n In the instance declaration for ‘CRTrans Maybe (GF fp d)’\r\n |\r\n25 | crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:25:14: error:\r\n • Could not deduce (Reflects m Int)\r\n from the context: Reflects m Int\r\n bound by the type signature for:\r\n crtInfo :: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n at Bug.hs:25:14-79\r\n The type variable ‘k0’ is ambiguous\r\n • When checking that instance signature for ‘crtInfo’\r\n is more general than its signature in the class\r\n Instance sig: forall (m :: k0).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n Class sig: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n In the instance declaration for ‘CRTrans Maybe (GF fp d)’\r\n |\r\n25 | crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nNotably, both `PolyKinds` and `MonoLocalBinds` are required to trigger this bug.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1