GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:15:53Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/14720GHC 8.4.1-alpha regression with TypeInType2019-07-07T18:15:53ZRyan ScottGHC 8.4.1-alpha regression with TypeInTypeGHC 8.2.2 is able to typecheck this code:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Ty...GHC 8.2.2 is able to typecheck this code:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module SGenerics where
import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..), sym, trans)
import Data.Void
data family Sing (z :: k)
class Generic (a :: Type) where
type Rep a :: Type
from :: a -> Rep a
to :: Rep a -> a
class PGeneric (a :: Type) where
type PFrom (x :: a) :: Rep a
type PTo (x :: Rep a) :: a
class SGeneric k where
sFrom :: forall (a :: k). Sing a -> Sing (PFrom a)
sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)
class (PGeneric k, SGeneric k) => VGeneric k where
sTof :: forall (a :: k). Sing a -> PTo (PFrom a) :~: a
sFot :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a
data Decision a = Proved a
| Disproved (a -> Void)
class SDecide k where
(%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
default (%~) :: forall (a :: k) (b :: k). (VGeneric k, SDecide (Rep k))
=> Sing a -> Sing b -> Decision (a :~: b)
s1 %~ s2 = case sFrom s1 %~ sFrom s2 of
Proved (Refl :: PFrom a :~: PFrom b) ->
case (sTof s1, sTof s2) of
(Refl, Refl) -> Proved Refl
Disproved contra -> Disproved (\Refl -> contra Refl)
```
But GHC 8.4.1-alpha2 cannot:
```
$ /opt/ghc/8.4.1/bin/ghc Bug.hs
[1 of 1] Compiling SGenerics ( Bug.hs, Bug.o )
Bug.hs:44:52: error:
• Could not deduce: PFrom a ~ PFrom a
from the context: b ~ a
bound by a pattern with constructor:
Refl :: forall k (a :: k). a :~: a,
in a lambda abstraction
at Bug.hs:44:37-40
Expected type: PFrom a :~: PFrom b
Actual type: PFrom a :~: PFrom a
NB: ‘PFrom’ is a non-injective type family
• In the first argument of ‘contra’, namely ‘Refl’
In the expression: contra Refl
In the first argument of ‘Disproved’, namely
‘(\ Refl -> contra Refl)’
• Relevant bindings include
contra :: (PFrom a :~: PFrom b) -> Void (bound at Bug.hs:44:15)
s2 :: Sing b (bound at Bug.hs:40:9)
s1 :: Sing a (bound at Bug.hs:40:3)
(%~) :: Sing a -> Sing b -> Decision (a :~: b)
(bound at Bug.hs:40:3)
|
44 | Disproved contra -> Disproved (\Refl -> contra Refl)
| ^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.4.1-alpha1 |
| 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.1-alpha regression with TypeInType","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1-alpha1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC 8.2.2 is able to typecheck this code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AllowAmbiguousTypes #-}\r\n{-# LANGUAGE DefaultSignatures #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule SGenerics where\r\n\r\nimport Data.Kind (Type)\r\nimport Data.Type.Equality ((:~:)(..), sym, trans)\r\nimport Data.Void\r\n\r\ndata family Sing (z :: k)\r\n\r\nclass Generic (a :: Type) where\r\n type Rep a :: Type\r\n from :: a -> Rep a\r\n to :: Rep a -> a\r\n\r\nclass PGeneric (a :: Type) where\r\n type PFrom (x :: a) :: Rep a\r\n type PTo (x :: Rep a) :: a\r\n\r\nclass SGeneric k where\r\n sFrom :: forall (a :: k). Sing a -> Sing (PFrom a)\r\n sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)\r\n\r\nclass (PGeneric k, SGeneric k) => VGeneric k where\r\n sTof :: forall (a :: k). Sing a -> PTo (PFrom a) :~: a\r\n sFot :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a\r\n\r\ndata Decision a = Proved a\r\n | Disproved (a -> Void)\r\n\r\nclass SDecide k where\r\n (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)\r\n default (%~) :: forall (a :: k) (b :: k). (VGeneric k, SDecide (Rep k))\r\n => Sing a -> Sing b -> Decision (a :~: b)\r\n s1 %~ s2 = case sFrom s1 %~ sFrom s2 of\r\n Proved (Refl :: PFrom a :~: PFrom b) ->\r\n case (sTof s1, sTof s2) of\r\n (Refl, Refl) -> Proved Refl\r\n Disproved contra -> Disproved (\\Refl -> contra Refl)\r\n}}}\r\n\r\nBut GHC 8.4.1-alpha2 cannot:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling SGenerics ( Bug.hs, Bug.o )\r\n\r\nBug.hs:44:52: error:\r\n • Could not deduce: PFrom a ~ PFrom a\r\n from the context: b ~ a\r\n bound by a pattern with constructor:\r\n Refl :: forall k (a :: k). a :~: a,\r\n in a lambda abstraction\r\n at Bug.hs:44:37-40\r\n Expected type: PFrom a :~: PFrom b\r\n Actual type: PFrom a :~: PFrom a\r\n NB: ‘PFrom’ is a non-injective type family\r\n • In the first argument of ‘contra’, namely ‘Refl’\r\n In the expression: contra Refl\r\n In the first argument of ‘Disproved’, namely\r\n ‘(\\ Refl -> contra Refl)’\r\n • Relevant bindings include\r\n contra :: (PFrom a :~: PFrom b) -> Void (bound at Bug.hs:44:15)\r\n s2 :: Sing b (bound at Bug.hs:40:9)\r\n s1 :: Sing a (bound at Bug.hs:40:3)\r\n (%~) :: Sing a -> Sing b -> Decision (a :~: b)\r\n (bound at Bug.hs:40:3)\r\n |\r\n44 | Disproved contra -> Disproved (\\Refl -> contra Refl)\r\n | ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/14710GHC 8.4.1-alpha allows the use of kind polymorphism without PolyKinds2019-07-07T18:15:55ZRyan ScottGHC 8.4.1-alpha allows the use of kind polymorphism without PolyKindsThis program:
```hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGU...This program:
```hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -ddump-deriv #-}
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.1-alpha2 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.1-alpha1 |
| 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.1-alpha 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.1-alpha1","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 -ddump-deriv #-}\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.1-alpha2 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/14350Infinite loop when typechecking incorrect implementation (GHC HEAD only)2019-07-07T18:17:22ZRyan ScottInfinite loop when typechecking incorrect implementation (GHC HEAD only)On GHC HEAD, typechecking this program loops infinitely:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ...On GHC HEAD, typechecking this program loops infinitely:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data Proxy a = Proxy
data family Sing (a :: k)
data SomeSing k where
SomeSing :: Sing (a :: k) -> SomeSing k
class SingKind k where
type Demote k :: Type
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
data instance Sing (x :: Proxy k) where
SProxy :: Sing 'Proxy
instance SingKind (Proxy k) where
type Demote (Proxy k) = Proxy k
fromSing SProxy = Proxy
toSing Proxy = SomeSing SProxy
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type a @@ b = Apply a b
infixl 9 @@
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }
instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where
type Demote (k1 ~> k2) = Demote k1 -> Demote k2
fromSing sFun x = case toSing x of SomeSing y -> fromSing (applySing sFun y)
toSing = undefined
dcomp :: forall (a :: Type)
(b :: a ~> Type)
(c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
(f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
(g :: forall (x :: a). Proxy x ~> b @@ x)
(x :: a).
Sing f
-> Sing g
-> Sing x
-> c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x))
dcomp f g x = applySing f Proxy Proxy
```
This is a regression from GHC 8.2.1/8.2.2, where it gives a proper error message:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:59:15: error:
• Couldn't match expected type ‘Proxy a2
-> Apply (Apply (c x4) 'Proxy) (Apply (g x4) 'Proxy)’
with actual type ‘Sing (f x y @@ t0)’
• The function ‘applySing’ is applied to three arguments,
but its type ‘Sing (f x y) -> Sing t0 -> Sing (f x y @@ t0)’
has only two
In the expression: applySing f Proxy Proxy
In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy
• Relevant bindings include
x :: Sing x4 (bound at Bug.hs:59:11)
g :: Sing (g x3) (bound at Bug.hs:59:9)
f :: Sing (f x2 y) (bound at Bug.hs:59:7)
dcomp :: Sing (f x2 y)
-> Sing (g x3) -> Sing x4 -> (c x4 @@ 'Proxy) @@ (g x4 @@ 'Proxy)
(bound at Bug.hs:59:1)
|
59 | dcomp f g x = applySing f Proxy Proxy
| ^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:59:27: error:
• Couldn't match expected type ‘Sing t0’
with actual type ‘Proxy a0’
• In the second argument of ‘applySing’, namely ‘Proxy’
In the expression: applySing f Proxy Proxy
In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy
• Relevant bindings include
x :: Sing x4 (bound at Bug.hs:59:11)
g :: Sing (g x3) (bound at Bug.hs:59:9)
f :: Sing (f x2 y) (bound at Bug.hs:59:7)
dcomp :: Sing (f x2 y)
-> Sing (g x3) -> Sing x4 -> (c x4 @@ 'Proxy) @@ (g x4 @@ 'Proxy)
(bound at Bug.hs:59:1)
|
59 | dcomp f g x = applySing f Proxy Proxy
| ^^^^^
```8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/14339GHC 8.2.1 regression when combining GND with TypeError (solveDerivEqns: proba...2023-01-03T20:56:12ZRyan ScottGHC 8.2.1 regression when combining GND with TypeError (solveDerivEqns: probable loop)This code panics on GHC 8.2.1 and later:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import GHC.TypeLits
newtype Baz = Baz Foo
deriving Bar
new...This code panics on GHC 8.2.1 and later:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import GHC.TypeLits
newtype Baz = Baz Foo
deriving Bar
newtype Foo = Foo Int
class Bar a where
bar :: a
instance (TypeError (Text "Boo")) => Bar Foo where
bar = undefined
```
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.1 for x86_64-unknown-linux):
solveDerivEqns: probable loop
DerivSpec
ds_loc = Bug.hs:9:12-14
ds_name = $fBarBaz
ds_tvs = []
ds_cls = Bar
ds_tys = [Baz]
ds_theta = [ThetaOrigin
to_tvs = []
to_givens = []
to_wanted_origins = [Bar Foo, (Foo :: *) ~R# (Baz :: *)]]
ds_mechanism = newtype
[[s0_a1D7[fuv:0]]]
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcDerivInfer.hs:515:9 in ghc:TcDerivInfer
```
This is a regression since GHC 8.0.2, in which it does compile successfully.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| 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.2.1 regression when combining GND with TypeError (solveDerivEqns: probable loop)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["CustomTypeErrors","deriving,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code panics on GHC 8.2.1 and later:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE GeneralizedNewtypeDeriving #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\nmodule Bug where\r\n\r\nimport GHC.TypeLits\r\n\r\nnewtype Baz = Baz Foo\r\n deriving Bar\r\n\r\nnewtype Foo = Foo Int\r\n\r\nclass Bar a where\r\n bar :: a\r\n\r\ninstance (TypeError (Text \"Boo\")) => Bar Foo where\r\n bar = undefined\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.1: 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\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.2.1 for x86_64-unknown-linux):\r\n solveDerivEqns: probable loop\r\n DerivSpec\r\n ds_loc = Bug.hs:9:12-14\r\n ds_name = $fBarBaz\r\n ds_tvs = []\r\n ds_cls = Bar\r\n ds_tys = [Baz]\r\n ds_theta = [ThetaOrigin\r\n to_tvs = []\r\n to_givens = []\r\n to_wanted_origins = [Bar Foo, (Foo :: *) ~R# (Baz :: *)]]\r\n ds_mechanism = newtype\r\n [[s0_a1D7[fuv:0]]]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable\r\n callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcDerivInfer.hs:515:9 in ghc:TcDerivInfer\r\n}}}\r\n\r\nThis is a regression since GHC 8.0.2, in which it does compile successfully.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.2https://gitlab.haskell.org/ghc/ghc/-/issues/14230Gruesome kind mismatch errors for associated data family instances2019-07-07T18:17:51ZRyan ScottGruesome kind mismatch errors for associated data family instancesSpun off from #14175\##14230. This program, which can only really be compiled on GHC HEAD at the moment:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
...Spun off from #14175\##14230. This program, which can only really be compiled on GHC HEAD at the moment:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
class C k where
data CD :: k -> k -> *
instance C (Maybe a) where
data CD :: (k -> *) -> (k -> *) -> *
```
Gives a heinous error message:
```
Bug.hs:11:3: error:
• Expected kind ‘(k -> *) -> (k -> *) -> *’,
but ‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe a
-> Maybe a -> *’
• In the data instance declaration for ‘CD’
In the instance declaration for ‘C (Maybe a)’
|
11 | data CD :: (k -> *) -> (k -> *) -> *
| ^^^^^^^
```
- We shouldn't be expecting kind `(k -> *) -> (k -> *) -> *`, but rather kind `Maybe a -> Maybe a -> *`, due to the instance head itself.
- The phrase `‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe -> Maybe a -> *’` is similarly confusing. This doesn't point out that the real issue is the use of `(k -> *)`.
Another program in a similar vein:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
class C a where
data CD k (a :: k) :: k -> *
instance C (Maybe a) where
data CD k (a :: k -> *) :: (k -> *) -> *
```
```
Bug.hs:13:3: error:
• Expected kind ‘(k -> *) -> *’,
but ‘CD k (a :: k -> *) :: (k -> *) -> *’ has kind ‘k -> *’
• In the data instance declaration for ‘CD’
In the instance declaration for ‘C (Maybe a)’
|
13 | data CD k (a :: k -> *) :: (k -> *) -> *
| ^^^^^^^^^^^^^^^^^^^^^^^
```
This error message is further muddled by the incorrect use of `k` as the first type pattern (instead of `k -> *`, as subsequent kind signatures would suggest).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.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":"Gruesome kind mismatch errors for associated data family instances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Spun off from https://ghc.haskell.org/trac/ghc/ticket/14175#comment:9. This program, which can only really be compiled on GHC HEAD at the moment:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\nmodule Bug where\r\n\r\nclass C k where\r\n data CD :: k -> k -> *\r\n\r\ninstance C (Maybe a) where\r\n data CD :: (k -> *) -> (k -> *) -> *\r\n}}}\r\n\r\nGives a heinous error message:\r\n\r\n{{{\r\nBug.hs:11:3: error:\r\n • Expected kind ‘(k -> *) -> (k -> *) -> *’,\r\n but ‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe a\r\n -> Maybe a -> *’\r\n • In the data instance declaration for ‘CD’\r\n In the instance declaration for ‘C (Maybe a)’\r\n |\r\n11 | data CD :: (k -> *) -> (k -> *) -> *\r\n | ^^^^^^^\r\n}}}\r\n\r\n* We shouldn't be expecting kind `(k -> *) -> (k -> *) -> *`, but rather kind `Maybe a -> Maybe a -> *`, due to the instance head itself.\r\n* The phrase `‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe -> Maybe a -> *’` is similarly confusing. This doesn't point out that the real issue is the use of `(k -> *)`.\r\n\r\nAnother program in a similar vein:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nclass C a where\r\n data CD k (a :: k) :: k -> *\r\n\r\ninstance C (Maybe a) where\r\n data CD k (a :: k -> *) :: (k -> *) -> *\r\n}}}\r\n{{{\r\nBug.hs:13:3: error:\r\n • Expected kind ‘(k -> *) -> *’,\r\n but ‘CD k (a :: k -> *) :: (k -> *) -> *’ has kind ‘k -> *’\r\n • In the data instance declaration for ‘CD’\r\n In the instance declaration for ‘C (Maybe a)’\r\n |\r\n13 | data CD k (a :: k -> *) :: (k -> *) -> *\r\n | ^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nThis error message is further muddled by the incorrect use of `k` as the first type pattern (instead of `k -> *`, as subsequent kind signatures would suggest).","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/14209GHC 8.2.1 regression involving telescoping kind signature2019-07-07T18:17:56ZRyan ScottGHC 8.2.1 regression involving telescoping kind signatureThe following program typechecks in GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
module Bug where
data MyProxy k (a :: k) = MyProxy
data Foo (z :: MyProxy k (a :: k))
```
But in GHC 8.2.1, it's rejecte...The following program typechecks in GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
module Bug where
data MyProxy k (a :: k) = MyProxy
data Foo (z :: MyProxy k (a :: k))
```
But in GHC 8.2.1, it's rejected:
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:6:1: error:
Kind variable ‘k’ is implicitly bound in datatype
‘Foo’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it explicitly somewhere?
Type variables with inferred kinds:
(k :: *) (a :: k) (z :: MyProxy k a)
|
6 | data Foo (z :: MyProxy k (a :: k))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| 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.2.1 regression involving telescoping kind signature","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program typechecks in GHC 8.0.1 and 8.0.2:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\ndata MyProxy k (a :: k) = MyProxy\r\ndata Foo (z :: MyProxy k (a :: k))\r\n}}}\r\n\r\nBut in GHC 8.2.1, it's rejected:\r\n\r\n{{{\r\nGHCi, version 8.2.1: 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\n\r\nBug.hs:6:1: error:\r\n Kind variable ‘k’ is implicitly bound in datatype\r\n ‘Foo’, but does not appear as the kind of any\r\n of its type variables. Perhaps you meant\r\n to bind it explicitly somewhere?\r\n Type variables with inferred kinds:\r\n (k :: *) (a :: k) (z :: MyProxy k a)\r\n |\r\n6 | data Foo (z :: MyProxy k (a :: k))\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/14038TypeApplications regression in GHC HEAD: ‘p0’ is untouchable inside the const...2019-07-07T18:18:45ZRyan ScottTypeApplications regression in GHC HEAD: ‘p0’ is untouchable inside the constraints: ()This file:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeA...This file:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Eliminator where
import Data.Kind (Type)
data family Sing (a :: k)
data instance Sing (z :: [a]) where
SNil :: Sing '[]
SCons :: Sing x -> Sing xs -> Sing (x:xs)
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type a @@ b = Apply a b
infixl 9 @@
data FunArrow = (:->) -- ^ '(->)'
| (:~>) -- ^ '(~>)'
class FunType (arr :: FunArrow) where
type Fun (k1 :: Type) arr (k2 :: Type) :: Type
class FunType arr => AppType (arr :: FunArrow) where
type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
type FunApp arr = (FunType arr, AppType arr)
instance FunType (:->) where
type Fun k1 (:->) k2 = k1 -> k2
instance AppType (:->) where
type App k1 (:->) k2 (f :: k1 -> k2) x = f x
instance FunType (:~>) where
type Fun k1 (:~>) k2 = k1 ~> k2
instance AppType (:~>) where
type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
infixr 0 -?>
type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).
Sing l
-> p '[]
-> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))
-> p l
elimList = elimListPoly @(:->)
elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).
Sing l
-> p @@ '[]
-> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))
-> p @@ l
elimListTyFun = elimListPoly @(:~>) @_ @p
elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).
FunApp arr
=> Sing l
-> App [a] arr Type p '[]
-> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))
-> App [a] arr Type p l
elimListPoly SNil pNil _ = pNil
elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)
```
Typechecks in GHC 8.2.1 without issue, but fails in GHC HEAD:
```
$ ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.3.20170725: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Eliminator ( Bug.hs, interpreted )
Bug.hs:59:12: error:
• Couldn't match type ‘p0’ with ‘p’
because type variables ‘a1’, ‘p’ would escape their scope
These (rigid, skolem) type variables are bound by
the type signature for:
elimList :: forall a1 (p :: [a1] -> *) (l :: [a1]).
Sing l
-> p '[]
-> (forall (x :: a1) (xs :: [a1]).
Sing x -> Sing xs -> p xs -> p (x : xs))
-> p l
at Bug.hs:(54,1)-(58,15)
Expected type: Sing l
-> p '[]
-> (forall (x :: a1) (xs :: [a1]).
Sing x -> Sing xs -> p xs -> p (x : xs))
-> p l
Actual type: Sing l
-> App [a1] (':->) * p0 '[]
-> (forall (x :: a1) (xs :: [a1]).
Sing x
-> Sing xs
-> App [a1] (':->) * p0 xs
-> App [a1] (':->) * p0 (x : xs))
-> App [a1] (':->) * p0 l
• In the expression: elimListPoly @(:->)
In an equation for ‘elimList’: elimList = elimListPoly @(:->)
• Relevant bindings include
elimList :: Sing l
-> p '[]
-> (forall (x :: a1) (xs :: [a1]).
Sing x -> Sing xs -> p xs -> p (x : xs))
-> p l
(bound at Bug.hs:59:1)
|
59 | elimList = elimListPoly @(:->)
| ^^^^^^^^^^^^^^^^^^^
Bug.hs:59:12: error:
• Couldn't match type ‘p0’ with ‘p’
‘p0’ is untouchable
inside the constraints: ()
bound by a type expected by the context:
forall (x :: a1) (xs :: [a1]).
Sing x
-> Sing xs
-> App [a1] (':->) * p0 xs
-> App [a1] (':->) * p0 (x : xs)
at Bug.hs:59:12-30
‘p’ is a rigid type variable bound by
the type signature for:
elimList :: forall a1 (p :: [a1] -> *) (l :: [a1]).
Sing l
-> p '[]
-> (forall (x :: a1) (xs :: [a1]).
Sing x -> Sing xs -> p xs -> p (x : xs))
-> p l
at Bug.hs:(54,1)-(58,15)
Expected type: Sing x
-> Sing xs
-> App [a1] (':->) * p0 xs
-> App [a1] (':->) * p0 (x : xs)
Actual type: Sing x -> Sing xs -> p xs -> p (x : xs)
• In the expression: elimListPoly @(:->)
In an equation for ‘elimList’: elimList = elimListPoly @(:->)
• Relevant bindings include
elimList :: Sing l
-> p '[]
-> (forall (x :: a1) (xs :: [a1]).
Sing x -> Sing xs -> p xs -> p (x : xs))
-> p l
(bound at Bug.hs:59:1)
|
59 | elimList = elimListPoly @(:->)
| ^^^^^^^^^^^^^^^^^^^
```
A workaround is to explicitly apply `p` with `TypeApplications` in line 59:
```hs
elimList = elimListPoly @(:->) @_ @p
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"TypeApplications regression in GHC HEAD: ‘p0’ is untouchable inside the constraints: ()","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeApplications"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This file:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AllowAmbiguousTypes #-}\r\n{-# LANGUAGE ConstraintKinds #-}\r\n{-# LANGUAGE ExistentialQuantification #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Eliminator where\r\n\r\nimport Data.Kind (Type)\r\n\r\ndata family Sing (a :: k)\r\ndata instance Sing (z :: [a]) where\r\n SNil :: Sing '[]\r\n SCons :: Sing x -> Sing xs -> Sing (x:xs)\r\n\r\ndata TyFun :: Type -> Type -> Type\r\ntype a ~> b = TyFun a b -> Type\r\ninfixr 0 ~>\r\n\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\ntype a @@ b = Apply a b\r\ninfixl 9 @@\r\n\r\ndata FunArrow = (:->) -- ^ '(->)'\r\n | (:~>) -- ^ '(~>)'\r\n\r\nclass FunType (arr :: FunArrow) where\r\n type Fun (k1 :: Type) arr (k2 :: Type) :: Type\r\n\r\nclass FunType arr => AppType (arr :: FunArrow) where\r\n type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2\r\n\r\ntype FunApp arr = (FunType arr, AppType arr)\r\n\r\ninstance FunType (:->) where\r\n type Fun k1 (:->) k2 = k1 -> k2\r\n\r\ninstance AppType (:->) where\r\n type App k1 (:->) k2 (f :: k1 -> k2) x = f x\r\n\r\ninstance FunType (:~>) where\r\n type Fun k1 (:~>) k2 = k1 ~> k2\r\n\r\ninstance AppType (:~>) where\r\n type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x\r\n\r\ninfixr 0 -?>\r\ntype (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2\r\n\r\nelimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).\r\n Sing l\r\n -> p '[]\r\n -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))\r\n -> p l\r\nelimList = elimListPoly @(:->)\r\n\r\nelimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).\r\n Sing l\r\n -> p @@ '[]\r\n -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))\r\n -> p @@ l\r\nelimListTyFun = elimListPoly @(:~>) @_ @p\r\n\r\nelimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).\r\n FunApp arr\r\n => Sing l\r\n -> App [a] arr Type p '[]\r\n -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))\r\n -> App [a] arr Type p l\r\nelimListPoly SNil pNil _ = pNil\r\nelimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)\r\n}}}\r\n\r\nTypechecks in GHC 8.2.1 without issue, but fails in GHC HEAD:\r\n\r\n{{{\r\n$ ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs\r\nGHCi, version 8.3.20170725: http://www.haskell.org/ghc/ :? for help \r\nLoaded GHCi configuration from /home/rgscott/.ghci \r\n[1 of 1] Compiling Eliminator ( Bug.hs, interpreted ) \r\n \r\nBug.hs:59:12: error: \r\n • Couldn't match type ‘p0’ with ‘p’ \r\n because type variables ‘a1’, ‘p’ would escape their scope \r\n These (rigid, skolem) type variables are bound by \r\n the type signature for: \r\n elimList :: forall a1 (p :: [a1] -> *) (l :: [a1]). \r\n Sing l \r\n -> p '[] \r\n -> (forall (x :: a1) (xs :: [a1]). \r\n Sing x -> Sing xs -> p xs -> p (x : xs)) \r\n -> p l \r\n at Bug.hs:(54,1)-(58,15) \r\n Expected type: Sing l \r\n -> p '[] \r\n -> (forall (x :: a1) (xs :: [a1]).\r\n Sing x -> Sing xs -> p xs -> p (x : xs))\r\n -> p l\r\n Actual type: Sing l\r\n -> App [a1] (':->) * p0 '[]\r\n -> (forall (x :: a1) (xs :: [a1]).\r\n Sing x\r\n -> Sing xs\r\n -> App [a1] (':->) * p0 xs\r\n -> App [a1] (':->) * p0 (x : xs))\r\n -> App [a1] (':->) * p0 l\r\n • In the expression: elimListPoly @(:->)\r\n In an equation for ‘elimList’: elimList = elimListPoly @(:->)\r\n • Relevant bindings include\r\n elimList :: Sing l\r\n -> p '[]\r\n -> (forall (x :: a1) (xs :: [a1]).\r\n Sing x -> Sing xs -> p xs -> p (x : xs))\r\n -> p l\r\n (bound at Bug.hs:59:1)\r\n |\r\n59 | elimList = elimListPoly @(:->)\r\n | ^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:59:12: error:\r\n • Couldn't match type ‘p0’ with ‘p’\r\n ‘p0’ is untouchable\r\n inside the constraints: ()\r\n bound by a type expected by the context:\r\n forall (x :: a1) (xs :: [a1]).\r\n Sing x\r\n -> Sing xs\r\n -> App [a1] (':->) * p0 xs\r\n -> App [a1] (':->) * p0 (x : xs)\r\n at Bug.hs:59:12-30\r\n ‘p’ is a rigid type variable bound by\r\n the type signature for:\r\n elimList :: forall a1 (p :: [a1] -> *) (l :: [a1]).\r\n Sing l\r\n -> p '[]\r\n -> (forall (x :: a1) (xs :: [a1]).\r\n Sing x -> Sing xs -> p xs -> p (x : xs))\r\n -> p l\r\n at Bug.hs:(54,1)-(58,15)\r\n Expected type: Sing x\r\n -> Sing xs\r\n -> App [a1] (':->) * p0 xs\r\n -> App [a1] (':->) * p0 (x : xs)\r\n Actual type: Sing x -> Sing xs -> p xs -> p (x : xs)\r\n • In the expression: elimListPoly @(:->)\r\n In an equation for ‘elimList’: elimList = elimListPoly @(:->)\r\n • Relevant bindings include\r\n elimList :: Sing l\r\n -> p '[]\r\n -> (forall (x :: a1) (xs :: [a1]).\r\n Sing x -> Sing xs -> p xs -> p (x : xs))\r\n -> p l\r\n (bound at Bug.hs:59:1)\r\n |\r\n59 | elimList = elimListPoly @(:->)\r\n | ^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nA workaround is to explicitly apply `p` with `TypeApplications` in line 59:\r\n\r\n{{{#!hs\r\nelimList = elimListPoly @(:->) @_ @p\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.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/13819TypeApplications-related GHC panic2019-07-07T18:19:57ZIcelandjackTypeApplications-related GHC panic```hs
{-# LANGUAGE DeriveFunctor, TypeApplications #-}
-- {-# Language ViewPatterns #-}
-- {-# Language InstanceSigs, ViewPatterns, TupleSections, GeneralizedNewtypeDeriving, TemplateHaskell, LambdaCase #-}
module D where
import Dat...```hs
{-# LANGUAGE DeriveFunctor, TypeApplications #-}
-- {-# Language ViewPatterns #-}
-- {-# Language InstanceSigs, ViewPatterns, TupleSections, GeneralizedNewtypeDeriving, TemplateHaskell, LambdaCase #-}
module D where
import Data.Coerce
import Control.Applicative
newtype A a = A (IO a)
deriving Functor
instance Applicative A where
pure = pure @(_ -> WrappedMonad A _) @(_ -> A _) pure
instance Monad A where
```
causes a panic
```
$ ghci -ignore-dot-ghci /tmp/a.hs
GHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling D ( /tmp/a.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 8.3.20170605 for x86_64-unknown-linux):
repSplitAppTys
w0_a1xc[tau:4]
WrappedMonad A w0_a1xe[tau:4]
[]
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:809:9 in ghc:Type
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC Panics","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# LANGUAGE DeriveFunctor, TypeApplications #-}\r\n-- {-# Language ViewPatterns #-}\r\n-- {-# Language InstanceSigs, ViewPatterns, TupleSections, GeneralizedNewtypeDeriving, TemplateHaskell, LambdaCase #-}\r\n\r\nmodule D where\r\n\r\nimport Data.Coerce\r\nimport Control.Applicative\r\n\r\nnewtype A a = A (IO a)\r\n deriving Functor\r\n\r\ninstance Applicative A where\r\n pure = pure @(_ -> WrappedMonad A _) @(_ -> A _) pure\r\n \r\ninstance Monad A where\r\n}}}\r\n\r\ncauses a panic\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci /tmp/a.hs\r\nGHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling D ( /tmp/a.hs, interpreted )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20170605 for x86_64-unknown-linux):\r\n\trepSplitAppTys\r\n w0_a1xc[tau:4]\r\n WrappedMonad A w0_a1xe[tau:4]\r\n []\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable\r\n callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:809:9 in ghc:Type\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":[]} -->8.4.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/13594Typechecker behavior w.r.t. BangPatterns and nested foralls has changed in 8.22019-07-07T18:21:07ZRyan ScottTypechecker behavior w.r.t. BangPatterns and nested foralls has changed in 8.2Try running this code in GHCi:
```
λ> :set -XBangPatterns -XRankNTypes -XTypeFamilies
λ> let x :: forall a . a ~ Integer => forall b. b ~ Integer => (a, b); !x = (1, 2)
```
In GHC 8.0.1 and 8.0.2, this works. But in GHC 8.2.1:
```
<...Try running this code in GHCi:
```
λ> :set -XBangPatterns -XRankNTypes -XTypeFamilies
λ> let x :: forall a . a ~ Integer => forall b. b ~ Integer => (a, b); !x = (1, 2)
```
In GHC 8.0.1 and 8.0.2, this works. But in GHC 8.2.1:
```
<interactive>:3:74:
Couldn't match expected type ‘forall a.
(a ~ Integer) =>
forall b. (b ~ Integer) => (a, b)’
with actual type ‘(Integer, Integer)’
In the expression: (1, 2)
In a pattern binding: !x = (1, 2)
```
If you put this code into a source file:
```hs
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
module Bug where
x :: forall a . a ~ Integer => forall b. b ~ Integer => (a, b)
!x = (1, 2)
```
Then it also works in GHC 8.0.1. and 8.0.2, but it errors on GHC 8.2 (this time with a different error):
```
GHCi, version 8.2.0.20170413: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:6:1: error:
Overloaded signature conflicts with monomorphism restriction
x :: forall a. a ~ Integer => forall b. b ~ Integer => (a, b)
|
6 | x :: forall a . a ~ Integer => forall b. b ~ Integer => (a, b)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1-rc2 |
| 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":"Typechecker behavior w.r.t. BangPatterns and nested foralls has changed in 8.2","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Try running this code in GHCi:\r\n\r\n{{{\r\nλ> :set -XBangPatterns -XRankNTypes -XTypeFamilies \r\nλ> let x :: forall a . a ~ Integer => forall b. b ~ Integer => (a, b); !x = (1, 2)\r\n}}}\r\n\r\nIn GHC 8.0.1 and 8.0.2, this works. But in GHC 8.2.1:\r\n\r\n{{{\r\n<interactive>:3:74:\r\n Couldn't match expected type ‘forall a.\r\n (a ~ Integer) =>\r\n forall b. (b ~ Integer) => (a, b)’\r\n with actual type ‘(Integer, Integer)’\r\n In the expression: (1, 2)\r\n In a pattern binding: !x = (1, 2)\r\n}}}\r\n\r\nIf you put this code into a source file:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE BangPatterns #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\nmodule Bug where\r\n\r\nx :: forall a . a ~ Integer => forall b. b ~ Integer => (a, b)\r\n!x = (1, 2)\r\n}}}\r\n\r\nThen it also works in GHC 8.0.1. and 8.0.2, but it errors on GHC 8.2 (this time with a different error):\r\n\r\n{{{\r\nGHCi, version 8.2.0.20170413: 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\n\r\nBug.hs:6:1: error:\r\n Overloaded signature conflicts with monomorphism restriction\r\n x :: forall a. a ~ Integer => forall b. b ~ Integer => (a, b)\r\n |\r\n6 | x :: forall a . a ~ Integer => forall b. b ~ Integer => (a, b)\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\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.1https://gitlab.haskell.org/ghc/ghc/-/issues/13371instance selection too eager2019-07-07T18:22:14Zaavogtinstance selection too eagerI see a regression in 8.0.2: the `g_f'` definition is rejected. The error goes away if I do one of:
- -XNoMonoLocalBinds
- -XNoPolyKinds
- pasting the inferred type of `g_f`
<details><summary>Trac metadata</summary>
| Trac field ...I see a regression in 8.0.2: the `g_f'` definition is rejected. The error goes away if I do one of:
- -XNoMonoLocalBinds
- -XNoPolyKinds
- pasting the inferred type of `g_f`
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"instance selection too eager","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I see a regression in 8.0.2: the `g_f'` definition is rejected. The error goes away if I do one of:\r\n\r\n * -XNoMonoLocalBinds\r\n\r\n * -XNoPolyKinds\r\n\r\n * pasting the inferred type of `g_f`","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/13272DeriveAnyClass regression involving a rigid type variable2019-07-07T18:22:39ZRyan ScottDeriveAnyClass regression involving a rigid type variableI was writing up an example to show off how `DeriveAnyClass` has improved since 639e702b6129f501c539b158b982ed8489e3d09c, and wouldn't you know it, the example doesn't actually compile anymore post-639e702b6129f501c539b158b982ed8489e3d09...I was writing up an example to show off how `DeriveAnyClass` has improved since 639e702b6129f501c539b158b982ed8489e3d09c, and wouldn't you know it, the example doesn't actually compile anymore post-639e702b6129f501c539b158b982ed8489e3d09c. Oopsie.
```hs
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module TypeName where
import GHC.Generics
class TypeName a where
typeName :: forall proxy.
proxy a -> String
default typeName :: forall proxy d f.
(Generic a, Rep a ~ D1 d f, Datatype d)
=> proxy a -> String
typeName _ = gtypeName $ from (undefined :: a)
gtypeName :: Datatype d => D1 d f p -> String
gtypeName = datatypeName
data T a = MkT a
deriving (Generic, TypeName)
```
This compiles before that commit. After it, however, it fails with the error:
```
[1 of 1] Compiling TypeName ( Bug.hs, interpreted )
Bug.hs:23:22: error:
• Couldn't match type ‘f’
with ‘C1
('MetaCons "MkT" 'PrefixI 'False)
(S1
('MetaSel
'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
(Rec0 a))’
arising from the 'deriving' clause of a data type declaration
‘f’ is a rigid type variable bound by
the deriving clause for ‘TypeName (T a)’ at Bug.hs:14:38
• When deriving the instance for (TypeName (T a))
|
23 | deriving (Generic, TypeName)
| ^^^^^^^^
```
I'm not sure why it's complaining only about `f` and not, say, `d`.8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/12945Backpack signature matching doesn't pick up orphan instances2019-07-07T18:24:31ZEdward Z. YangBackpack signature matching doesn't pick up orphan instancesRepro:
```
unit impl where
module A where
data T = T
module B(module A, module B) where
import A
instance Show T where
show T = "T"
unit sig where
signature B where
data T = T
...Repro:
```
unit impl where
module A where
data T = T
module B(module A, module B) where
import A
instance Show T where
show T = "T"
unit sig where
signature B where
data T = T
instance Show T
module App where
import B
app = print T
unit main where
dependency sig[B=impl:B]
module Main where
import App
main = app
```
I get:
```
ezyang@sabre:~$ ghc-head --backpack foo.bkp
[1 of 3] Processing impl
Instantiating impl
[1 of 2] Compiling A (.hs -> .o)
[2 of 2] Compiling B (.hs -> .o)
[2 of 3] Processing sig
[3 of 3] Processing main
Instantiating main
[1 of 1] Including sig[B=impl:B]
Instantiating sig[B=impl:B]
[1 of 2] Compiling B[sig] (.hsig -> .o)
sig/sig-HVnmSw44WZeBfwnUur4wzl/../B.hi:1:1: error:
No instance for (GHC.Show.Show impl:A.T)
arising when attempting to show that
instance [safe] GHC.Show.Show impl:A.T -- Defined in ‘impl:B’
is provided by ‘impl:B’
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| 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":"Backpack signature matching doesn't pick up orphan instances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"ezyang"},"version":"8.1","keywords":["backpack"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Repro:\r\n\r\n{{{\r\nunit impl where\r\n module A where\r\n data T = T\r\n module B(module A, module B) where\r\n import A\r\n instance Show T where\r\n show T = \"T\"\r\n\r\nunit sig where\r\n signature B where\r\n data T = T\r\n instance Show T\r\n module App where\r\n import B\r\n app = print T\r\n\r\nunit main where\r\n dependency sig[B=impl:B]\r\n module Main where\r\n import App\r\n main = app\r\n}}}\r\n\r\nI get:\r\n\r\n{{{\r\nezyang@sabre:~$ ghc-head --backpack foo.bkp\r\n[1 of 3] Processing impl\r\n Instantiating impl\r\n [1 of 2] Compiling A (.hs -> .o)\r\n [2 of 2] Compiling B (.hs -> .o)\r\n[2 of 3] Processing sig\r\n[3 of 3] Processing main\r\n Instantiating main\r\n [1 of 1] Including sig[B=impl:B]\r\n Instantiating sig[B=impl:B]\r\n [1 of 2] Compiling B[sig] (.hsig -> .o)\r\n\r\nsig/sig-HVnmSw44WZeBfwnUur4wzl/../B.hi:1:1: error:\r\n No instance for (GHC.Show.Show impl:A.T)\r\n arising when attempting to show that\r\n instance [safe] GHC.Show.Show impl:A.T -- Defined in ‘impl:B’\r\n is provided by ‘impl:B’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1Edward Z. YangEdward Z. Yanghttps://gitlab.haskell.org/ghc/ghc/-/issues/12936Type inference regression in GHC HEAD2019-07-07T18:24:34ZRyan ScottType inference regression in GHC HEADFirst noticed in #12790\##12936. This causes `parsec-3.1.11` to fail to build with GHC HEAD.
Here is as small of a test case that I can manage, with no dependencies:
```hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDepend...First noticed in #12790\##12936. This causes `parsec-3.1.11` to fail to build with GHC HEAD.
Here is as small of a test case that I can manage, with no dependencies:
```hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Parsec (makeTokenParser) where
import Data.Char (digitToInt)
data ParsecT s u (m :: * -> *) a
instance Functor (ParsecT s u m) where
fmap = undefined
instance Applicative (ParsecT s u m) where
pure = undefined
(<*>) = undefined
instance Monad (ParsecT s u m) where
return = undefined
(>>=) = undefined
fail = undefined
parserZero :: ParsecT s u m a
parserZero = undefined
infixr 1 <|>
(<|>) :: (ParsecT s u m a) -> (ParsecT s u m a) -> (ParsecT s u m a)
(<|>) = undefined
class (Monad m) => Stream s m t | s -> t where
digit :: (Stream s m Char) => ParsecT s u m Char
digit = undefined
hexDigit :: (Stream s m Char) => ParsecT s u m Char
hexDigit = undefined
octDigit :: (Stream s m Char) => ParsecT s u m Char
octDigit = undefined
option :: (Stream s m t) => a -> ParsecT s u m a -> ParsecT s u m a
option = undefined
many1 :: (Stream s m t) => ParsecT s u m a -> ParsecT s u m [a]
many1 = undefined
data GenTokenParser s u m
= TokenParser {
float :: ParsecT s u m Double,
naturalOrFloat :: ParsecT s u m (Either Integer Double)
}
makeTokenParser :: (Stream s m Char) => GenTokenParser s u m
makeTokenParser
= TokenParser{
float = float_
, naturalOrFloat = naturalOrFloat_
}
where
-----------------------------------------------------------
-- Numbers
-----------------------------------------------------------
naturalOrFloat_ = lexeme natFloat
float_ = lexeme floating
-- floats
floating = do{ n <- decimal
; fractExponent n
}
natFloat = zeroNumFloat
<|> decimalFloat
zeroNumFloat = do{ n <- hexadecimal <|> octal
; return (Left n)
}
<|> decimalFloat
decimalFloat = do{ n <- decimal
; option (Left n)
(fractFloat n)
}
fractFloat n = do{ f <- fractExponent n
; return (Right f)
}
fractExponent n = do{ fract <- fraction
; expo <- option "" exponent'
; readDouble (show n ++ fract ++ expo)
}
<|>
do{ expo <- exponent'
; readDouble (show n ++ expo)
}
where
readDouble s =
case reads s of
[(x, "")] -> return x
_ -> parserZero
fraction = do{ digits <- many1 digit
; return ('.' : digits)
}
exponent' = do{ e <- decimal
; return (show e)
}
-- integers and naturals
decimal = number 10 digit
hexadecimal = number 16 hexDigit
octal = number 8 octDigit
number base baseDigit
= do{ digits <- many1 baseDigit
; let n = foldl (\x d -> base*x + toInteger (digitToInt d)) 0 digits
; seq n (return n)
}
-----------------------------------------------------------
-- White space & symbols
-----------------------------------------------------------
lexeme p = do{ x <- p; whiteSpace; return x }
whiteSpace = return ()
```
In GHC 8.0.1 and 8.0.2, this compiles without issue. But on GHC HEAD:
```
$ ~/Software/ghc/inplace/bin/ghc-stage2 Parsec.hs
[1 of 1] Compiling Parsec ( Parsec.hs, Parsec.o )
Parsec.hs:83:27: error:
• Could not deduce (Stream s m t0) arising from a use of ‘option’
from the context: Stream s m Char
bound by the type signature for:
makeTokenParser :: Stream s m Char => GenTokenParser s u m
at Parsec.hs:53:1-60
The type variable ‘t0’ is ambiguous
Relevant bindings include
decimalFloat :: ParsecT s u1 m (Either Integer Double)
(bound at Parsec.hs:82:5)
fractFloat :: forall b a1 u a2.
(Read b, Show a2) =>
a2 -> ParsecT s u m (Either a1 b)
(bound at Parsec.hs:87:5)
fractExponent :: forall a1 u a2.
(Show a2, Read a1) =>
a2 -> ParsecT s u m a1
(bound at Parsec.hs:91:5)
fraction :: forall u. ParsecT s u m [Char]
(bound at Parsec.hs:105:5)
exponent' :: forall u. ParsecT s u m String
(bound at Parsec.hs:109:5)
decimal :: forall u. ParsecT s u m Integer
(bound at Parsec.hs:114:5)
lexeme :: forall b. ParsecT s u m b -> ParsecT s u m b
(bound at Parsec.hs:127:5)
(Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
• In a stmt of a 'do' block: option (Left n) (fractFloat n)
In the expression:
do { n <- decimal;
option (Left n) (fractFloat n) }
In an equation for ‘decimalFloat’:
decimalFloat
= do { n <- decimal;
option (Left n) (fractFloat n) }
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| 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":"Type inference regression in GHC HEAD","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":"First noticed in https://ghc.haskell.org/trac/ghc/ticket/12790#comment:8. This causes `parsec-3.1.11` to fail to build with GHC HEAD.\r\n\r\nHere is as small of a test case that I can manage, with no dependencies:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE FunctionalDependencies #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE MultiParamTypeClasses #-}\r\nmodule Parsec (makeTokenParser) where\r\n\r\nimport Data.Char (digitToInt)\r\n\r\ndata ParsecT s u (m :: * -> *) a\r\n\r\ninstance Functor (ParsecT s u m) where\r\n fmap = undefined\r\n\r\ninstance Applicative (ParsecT s u m) where\r\n pure = undefined\r\n (<*>) = undefined\r\n\r\ninstance Monad (ParsecT s u m) where\r\n return = undefined\r\n (>>=) = undefined\r\n fail = undefined\r\n\r\nparserZero :: ParsecT s u m a\r\nparserZero = undefined\r\n\r\ninfixr 1 <|>\r\n(<|>) :: (ParsecT s u m a) -> (ParsecT s u m a) -> (ParsecT s u m a)\r\n(<|>) = undefined\r\n\r\nclass (Monad m) => Stream s m t | s -> t where\r\n\r\ndigit :: (Stream s m Char) => ParsecT s u m Char\r\ndigit = undefined\r\n\r\nhexDigit :: (Stream s m Char) => ParsecT s u m Char\r\nhexDigit = undefined\r\n\r\noctDigit :: (Stream s m Char) => ParsecT s u m Char\r\noctDigit = undefined\r\n\r\noption :: (Stream s m t) => a -> ParsecT s u m a -> ParsecT s u m a\r\noption = undefined\r\n\r\nmany1 :: (Stream s m t) => ParsecT s u m a -> ParsecT s u m [a]\r\nmany1 = undefined\r\n\r\ndata GenTokenParser s u m\r\n = TokenParser {\r\n float :: ParsecT s u m Double,\r\n naturalOrFloat :: ParsecT s u m (Either Integer Double)\r\n }\r\n\r\nmakeTokenParser :: (Stream s m Char) => GenTokenParser s u m\r\nmakeTokenParser\r\n = TokenParser{\r\n float = float_\r\n , naturalOrFloat = naturalOrFloat_\r\n }\r\n where\r\n\r\n -----------------------------------------------------------\r\n -- Numbers\r\n -----------------------------------------------------------\r\n naturalOrFloat_ = lexeme natFloat\r\n\r\n float_ = lexeme floating\r\n\r\n -- floats\r\n floating = do{ n <- decimal\r\n ; fractExponent n\r\n }\r\n\r\n\r\n natFloat = zeroNumFloat\r\n <|> decimalFloat\r\n\r\n zeroNumFloat = do{ n <- hexadecimal <|> octal\r\n ; return (Left n)\r\n }\r\n <|> decimalFloat\r\n\r\n decimalFloat = do{ n <- decimal\r\n ; option (Left n)\r\n (fractFloat n)\r\n }\r\n\r\n fractFloat n = do{ f <- fractExponent n\r\n ; return (Right f)\r\n }\r\n\r\n fractExponent n = do{ fract <- fraction\r\n ; expo <- option \"\" exponent'\r\n ; readDouble (show n ++ fract ++ expo)\r\n }\r\n <|>\r\n do{ expo <- exponent'\r\n ; readDouble (show n ++ expo)\r\n }\r\n where\r\n readDouble s =\r\n case reads s of\r\n [(x, \"\")] -> return x\r\n _ -> parserZero\r\n\r\n fraction = do{ digits <- many1 digit\r\n ; return ('.' : digits)\r\n }\r\n\r\n exponent' = do{ e <- decimal\r\n ; return (show e)\r\n }\r\n\r\n -- integers and naturals\r\n decimal = number 10 digit\r\n hexadecimal = number 16 hexDigit\r\n octal = number 8 octDigit\r\n\r\n number base baseDigit\r\n = do{ digits <- many1 baseDigit\r\n ; let n = foldl (\\x d -> base*x + toInteger (digitToInt d)) 0 digits\r\n ; seq n (return n)\r\n }\r\n\r\n -----------------------------------------------------------\r\n -- White space & symbols\r\n -----------------------------------------------------------\r\n lexeme p = do{ x <- p; whiteSpace; return x }\r\n whiteSpace = return ()\r\n}}}\r\n\r\nIn GHC 8.0.1 and 8.0.2, this compiles without issue. But on GHC HEAD:\r\n\r\n{{{\r\n$ ~/Software/ghc/inplace/bin/ghc-stage2 Parsec.hs\r\n[1 of 1] Compiling Parsec ( Parsec.hs, Parsec.o )\r\n\r\nParsec.hs:83:27: error:\r\n • Could not deduce (Stream s m t0) arising from a use of ‘option’\r\n from the context: Stream s m Char\r\n bound by the type signature for:\r\n makeTokenParser :: Stream s m Char => GenTokenParser s u m\r\n at Parsec.hs:53:1-60\r\n The type variable ‘t0’ is ambiguous\r\n Relevant bindings include\r\n decimalFloat :: ParsecT s u1 m (Either Integer Double)\r\n (bound at Parsec.hs:82:5)\r\n fractFloat :: forall b a1 u a2.\r\n (Read b, Show a2) =>\r\n a2 -> ParsecT s u m (Either a1 b)\r\n (bound at Parsec.hs:87:5)\r\n fractExponent :: forall a1 u a2.\r\n (Show a2, Read a1) =>\r\n a2 -> ParsecT s u m a1\r\n (bound at Parsec.hs:91:5)\r\n fraction :: forall u. ParsecT s u m [Char]\r\n (bound at Parsec.hs:105:5)\r\n exponent' :: forall u. ParsecT s u m String\r\n (bound at Parsec.hs:109:5)\r\n decimal :: forall u. ParsecT s u m Integer\r\n (bound at Parsec.hs:114:5)\r\n lexeme :: forall b. ParsecT s u m b -> ParsecT s u m b\r\n (bound at Parsec.hs:127:5)\r\n (Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)\r\n • In a stmt of a 'do' block: option (Left n) (fractFloat n)\r\n In the expression:\r\n do { n <- decimal;\r\n option (Left n) (fractFloat n) }\r\n In an equation for ‘decimalFloat’:\r\n decimalFloat\r\n = do { n <- decimal;\r\n option (Left n) (fractFloat n) }\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/12928Too easy to trigger CUSK condition using TH2019-07-07T18:24:36ZVladislav ZavialovToo easy to trigger CUSK condition using THWhile trying to make `singletons` class promotion work with kind-polymorphic type variables, I've encountered a problem regarding CUSKs.
Consider this class:
```
$(promoteOnly [d|
class Cls a where
fff :: Proxy a -> ()
|])
```...While trying to make `singletons` class promotion work with kind-polymorphic type variables, I've encountered a problem regarding CUSKs.
Consider this class:
```
$(promoteOnly [d|
class Cls a where
fff :: Proxy a -> ()
|])
```
The generated TH (slightly simplified by hand) looks like this:
```
type FffSym1 (t_alvm :: Proxy a1627472612) = Fff t_alvm
data FffSym0 (l_alvn :: TyFun (Proxy a1627472612) ())
type instance Apply FffSym0 l_alvn = FffSym1 l_alvn
class PCls a_alve where
type Fff (arg_alvl :: Proxy a_alve) :: ()
```
However, it fails to compile with the following error:
```
cusk.hs:25:1: error:
You have written a *complete user-suppled kind signature*,
but the following variable is undetermined: k0 :: *
Perhaps add a kind signature.
Inferred kinds of user-written variables:
a1627472612 :: k0
l_alvn :: TyFun (Proxy a1627472612) ()
```
As suggested by the error message, we need to specify the kind in its entirety (write a proper CUSK). So to sidestep the issue, we can write
```
data FffSym0 (l_alvn :: TyFun (Proxy (a1627472612 :: k)) ())
```
and it'll work. However, this means that the TH code generator should perform some guesswork to modify kind annotations. It sounds like a minefield — too much can go wrong, so it'd be great to avoid doing so.
Looking at the module `TcHsType` in the GHC sources, I see that the error is reported by the `kcHsTyVarBndrs` function:
```
-- If there are any meta-tvs left, the user has
-- lied about having a CUSK. Error.
; let (meta_tvs, good_tvs) = partition isMetaTyVar qkvs
; when (not (null meta_tvs)) $
report_non_cusk_tvs (qkvs ++ tc_tvs)
```
However, I don't see why we can't generalize over `meta_tvs` instead of reporting a failure. I asked on IRC \#ghc and ezyang suggested that it should be sound.
Below I attach a self-contained example that demonstrates the issue and has no dependencies except `base`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| Type | FeatureRequest |
| 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":"Too easy to trigger CUSK condition using TH","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"While trying to make `singletons` class promotion work with kind-polymorphic type variables, I've encountered a problem regarding CUSKs.\r\n\r\nConsider this class:\r\n\r\n{{{\r\n$(promoteOnly [d|\r\n class Cls a where\r\n fff :: Proxy a -> ()\r\n |])\r\n}}}\r\n\r\nThe generated TH (slightly simplified by hand) looks like this:\r\n\r\n{{{\r\ntype FffSym1 (t_alvm :: Proxy a1627472612) = Fff t_alvm\r\n\r\ndata FffSym0 (l_alvn :: TyFun (Proxy a1627472612) ())\r\n\r\ntype instance Apply FffSym0 l_alvn = FffSym1 l_alvn\r\n\r\nclass PCls a_alve where\r\n type Fff (arg_alvl :: Proxy a_alve) :: ()\r\n}}}\r\n\r\nHowever, it fails to compile with the following error:\r\n\r\n{{{\r\ncusk.hs:25:1: error:\r\n You have written a *complete user-suppled kind signature*,\r\n but the following variable is undetermined: k0 :: *\r\n Perhaps add a kind signature.\r\n Inferred kinds of user-written variables:\r\n a1627472612 :: k0\r\n l_alvn :: TyFun (Proxy a1627472612) ()\r\n}}}\r\n\r\nAs suggested by the error message, we need to specify the kind in its entirety (write a proper CUSK). So to sidestep the issue, we can write\r\n\r\n{{{\r\ndata FffSym0 (l_alvn :: TyFun (Proxy (a1627472612 :: k)) ())\r\n}}}\r\n\r\nand it'll work. However, this means that the TH code generator should perform some guesswork to modify kind annotations. It sounds like a minefield — too much can go wrong, so it'd be great to avoid doing so.\r\n\r\nLooking at the module `TcHsType` in the GHC sources, I see that the error is reported by the `kcHsTyVarBndrs` function:\r\n\r\n{{{\r\n -- If there are any meta-tvs left, the user has\r\n -- lied about having a CUSK. Error.\r\n ; let (meta_tvs, good_tvs) = partition isMetaTyVar qkvs\r\n ; when (not (null meta_tvs)) $\r\n report_non_cusk_tvs (qkvs ++ tc_tvs)\r\n}}}\r\n\r\nHowever, I don't see why we can't generalize over `meta_tvs` instead of reporting a failure. I asked on IRC #ghc and ezyang suggested that it should be sound.\r\n\r\nBelow I attach a self-contained example that demonstrates the issue and has no dependencies except `base`.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12907ExtendedDefaultRules-related regression in GHC 8.0.22019-07-07T18:24:41ZRyan ScottExtendedDefaultRules-related regression in GHC 8.0.2Commit https://git.haskell.org/ghc.git/commit/9a34bf1985035858ece043bf38b47b6ff4b88efb introduced a regression between GHC 8.0.1 and 8.0.2 regarding the behavior of `ExtendedDefaultRules`. In GHC 8.0.1, this program
```hs
module Bug whe...Commit https://git.haskell.org/ghc.git/commit/9a34bf1985035858ece043bf38b47b6ff4b88efb introduced a regression between GHC 8.0.1 and 8.0.2 regarding the behavior of `ExtendedDefaultRules`. In GHC 8.0.1, this program
```hs
module Bug where
default (Bool)
```
would compile without issue. On GHC 8.0.2, however, it is rejected with this error message:
```
$ /opt/ghc/8.0.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:3:1: error:
• The default type ‘Bool’ is not an instance of ‘Num’
• When checking the types in a default declaration
```
As a result, the `shelly` library now fails to compile with GHC 8.0.2 (see https://github.com/yesodweb/Shelly.hs/issues/130). A workaround is to explicitly enable `ExtendedDefaultRules` at the top of the module.
Richard, do you understand what's going on here? I'm not sure if this is a real regression or just GHC being more particular (admittedly, I don't understand many of the intricacies of `ExtendedDefaultRules`).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.2-rc1 |
| 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":"ExtendedDefaultRules-related regression in GHC 8.0.2","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2-rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Commit https://git.haskell.org/ghc.git/commit/9a34bf1985035858ece043bf38b47b6ff4b88efb introduced a regression between GHC 8.0.1 and 8.0.2 regarding the behavior of `ExtendedDefaultRules`. In GHC 8.0.1, this program\r\n\r\n{{{#!hs\r\nmodule Bug where\r\n\r\ndefault (Bool)\r\n}}}\r\n\r\nwould compile without issue. On GHC 8.0.2, however, it is rejected with this error message:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:3:1: error:\r\n • The default type ‘Bool’ is not an instance of ‘Num’\r\n • When checking the types in a default declaration\r\n}}}\r\n\r\nAs a result, the `shelly` library now fails to compile with GHC 8.0.2 (see https://github.com/yesodweb/Shelly.hs/issues/130). A workaround is to explicitly enable `ExtendedDefaultRules` at the top of the module.\r\n\r\nRichard, do you understand what's going on here? I'm not sure if this is a real regression or just GHC being more particular (admittedly, I don't understand many of the intricacies of `ExtendedDefaultRules`).","type_of_failure":"OtherFailure","blocking":[]} -->8.0.2https://gitlab.haskell.org/ghc/ghc/-/issues/12749Typechecker regression involving RankNTypes2019-07-07T18:25:18ZRyan ScottTypechecker regression involving RankNTypesThe following code compiles on GHC 7.0.4 through 7.10.3, but not with GHC 8.0.1, 8.0.2, or HEAD:
```hs
{-# LANGUAGE RankNTypes #-}
module Bug where
type NatTrans f g = forall x. f x -> g x
-- NatTrans analog of id
applyNT :: NatTrans ...The following code compiles on GHC 7.0.4 through 7.10.3, but not with GHC 8.0.1, 8.0.2, or HEAD:
```hs
{-# LANGUAGE RankNTypes #-}
module Bug where
type NatTrans f g = forall x. f x -> g x
-- NatTrans analog of id
applyNT :: NatTrans f g -> NatTrans f g
applyNT x = x
b :: Bool
b = True
eitherToMaybe :: NatTrans (Either a) Maybe
eitherToMaybe (Left _) = Nothing
eitherToMaybe (Right x) = Just x
trans :: NatTrans (Either a) Maybe -> NatTrans (Either a) Maybe
trans x = x
applyNTCheck :: NatTrans (Either a) Maybe
applyNTCheck = (if b then trans else applyNT) eitherToMaybe
```
```
$ /opt/ghc/8.0.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:21:27: error:
• Couldn't match type ‘NatTrans (Either a) Maybe’
with ‘Either a0 x0 -> Maybe x0’
Expected type: (Either a0 x0 -> Maybe x0) -> Either a x -> Maybe x
Actual type: NatTrans (Either a) Maybe -> Either a x -> Maybe x
• In the expression: trans
In the expression: if b then trans else applyNT
In the expression: (if b then trans else applyNT) eitherToMaybe
• Relevant bindings include
applyNTCheck :: Either a x -> Maybe x (bound at Bug.hs:21:1)
```
(Originally spotted [here](https://github.com/ku-fpg/natural-transformation/pull/13#issuecomment-255378141).)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | simonpj |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typechecker regression involving RankNTypes","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["simonpj"],"type":"Bug","description":"The following code compiles on GHC 7.0.4 through 7.10.3, but not with GHC 8.0.1, 8.0.2, or HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\nmodule Bug where\r\n\r\ntype NatTrans f g = forall x. f x -> g x\r\n\r\n-- NatTrans analog of id\r\napplyNT :: NatTrans f g -> NatTrans f g\r\napplyNT x = x\r\n\r\nb :: Bool\r\nb = True\r\n\r\neitherToMaybe :: NatTrans (Either a) Maybe\r\neitherToMaybe (Left _) = Nothing\r\neitherToMaybe (Right x) = Just x\r\n\r\ntrans :: NatTrans (Either a) Maybe -> NatTrans (Either a) Maybe\r\ntrans x = x\r\n\r\napplyNTCheck :: NatTrans (Either a) Maybe\r\napplyNTCheck = (if b then trans else applyNT) eitherToMaybe\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.0.1/bin/ghc Bug.hs \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:21:27: error:\r\n • Couldn't match type ‘NatTrans (Either a) Maybe’\r\n with ‘Either a0 x0 -> Maybe x0’\r\n Expected type: (Either a0 x0 -> Maybe x0) -> Either a x -> Maybe x\r\n Actual type: NatTrans (Either a) Maybe -> Either a x -> Maybe x\r\n • In the expression: trans\r\n In the expression: if b then trans else applyNT\r\n In the expression: (if b then trans else applyNT) eitherToMaybe\r\n • Relevant bindings include\r\n applyNTCheck :: Either a x -> Maybe x (bound at Bug.hs:21:1)\r\n}}}\r\n\r\n(Originally spotted [https://github.com/ku-fpg/natural-transformation/pull/13#issuecomment-255378141 here].)","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12670Representation polymorphism validity check is too strict2019-07-07T18:25:38ZBen GamariRepresentation polymorphism validity check is too strictAs of 465c6c5d15f8fb54afb78408f3a79e75e74d2cd4 GHC rejects this program,
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE RankNTypes #-}
module Hi where
import GHC.Exts
data TypeRep (a :: k) where
TrFun :: foral...As of 465c6c5d15f8fb54afb78408f3a79e75e74d2cd4 GHC rejects this program,
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE RankNTypes #-}
module Hi where
import GHC.Exts
data TypeRep (a :: k) where
TrFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (a :: TYPE r1) (b :: TYPE r2).
TypeRep a
-> TypeRep b
-> TypeRep (a -> b)
```
Claiming that it has inappropriate polymorphism over `RuntimeRep`,
```
$ ghc hi2.hs
[1 of 1] Compiling Hi ( hi2.hs, hi2.o )
hi2.hs:7:5: error:
• A representation-polymorphic type is not allowed here:
Type: a
Kind: TYPE r1
• In the definition of data constructor ‘TrFun’
In the data type declaration for ‘TypeRep’
```
I suspect this check is unnecessarily strict since we never need to store a value of type `a` to represent `TypeRep a` at runtime.
<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":"Representation polymorphism validity check is too strict","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["typeable"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"As of 465c6c5d15f8fb54afb78408f3a79e75e74d2cd4 GHC rejects this program,\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE RankNTypes #-}\r\nmodule Hi where\r\nimport GHC.Exts\r\ndata TypeRep (a :: k) where\r\n TrFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (a :: TYPE r1) (b :: TYPE r2).\r\n TypeRep a\r\n -> TypeRep b\r\n -> TypeRep (a -> b)\r\n}}}\r\n\r\nClaiming that it has inappropriate polymorphism over `RuntimeRep`,\r\n{{{\r\n$ ghc hi2.hs\r\n[1 of 1] Compiling Hi ( hi2.hs, hi2.o )\r\n\r\nhi2.hs:7:5: error:\r\n • A representation-polymorphic type is not allowed here:\r\n Type: a\r\n Kind: TYPE r1\r\n • In the definition of data constructor ‘TrFun’\r\n In the data type declaration for ‘TypeRep’\r\n}}}\r\n\r\nI suspect this check is unnecessarily strict since we never need to store a value of type `a` to represent `TypeRep a` at runtime.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12666ApplicativeDo fails to sequence actions2019-07-07T18:25:39ZBen GamariApplicativeDo fails to sequence actionsConsider the following,
```hs
{-# LANGUAGE ApplicativeDo #-}
module Fail where
data P a = P
instance Functor (P) where
fmap _ P = P
instance Applicative (P) where
P <*> P = P
pure _ = P
action :: P Int
action = P
works...Consider the following,
```hs
{-# LANGUAGE ApplicativeDo #-}
module Fail where
data P a = P
instance Functor (P) where
fmap _ P = P
instance Applicative (P) where
P <*> P = P
pure _ = P
action :: P Int
action = P
works :: P (Int, Int)
works = do
a <- action
b <- action
return (a,b)
thisWorks :: P Int
thisWorks = action *> action
-- It seems like this should be equivalent to thisWorks.
shouldThisWork :: P Int
shouldThisWork = do
action
action
```
It seems to me that `thisWorks` and `shouldThisWork` are equivalent, yet the latter fails to typecheck. It seems that `ApplicativeDo` fails to catch the fact that the result of the first `action` is not bound and therefore can be sequenced with `*>`.8.0.2Simon MarlowSimon Marlow