GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:52:23Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/6055panic: ctFlavId: derived constraint cannot have id2019-07-07T18:52:23ZLemmingpanic: ctFlavId: derived constraint cannot have idWhen trying to check, whether GHC-7.5 still suffers from #5970 I found another bug: When I compile the attached module I get the type error:
```
ghc: panic! (the 'impossible' happened)
(GHC version 7.5.20120426 for i386-unknown-linux)...When trying to check, whether GHC-7.5 still suffers from #5970 I found another bug: When I compile the attached module I get the type error:
```
ghc: panic! (the 'impossible' happened)
(GHC version 7.5.20120426 for i386-unknown-linux):
ctFlavId: derived constraint cannot have id
pty = llvm-extra-0.4:LLVM.Extra.Extension.X86.Add'{tc rj}
llvm-extra-0.4:LLVM.Extra.Extension.X86.D1{tc ri}
llvm-extra-0.4:LLVM.Extra.Extension.X86.D1{tc ri}
llvm-extra-0.4:LLVM.Extra.Extension.X86.D2{tc rh}
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
I tried hard to simplify the example and to remove all dependencies (llvm, type-level), but the test case is still rather involved.
Unfortunately it is again a problem with functional dependencies and I want to get rid of them anyway, but instead switching to type families and then to type level natural numbers I prefer to switch to type level numbers immediately.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"panic: ctFlavId: derived constraint cannot have id","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When trying to check, whether GHC-7.5 still suffers from #5970 I found another bug: When I compile the attached module I get the type error:\r\n{{{\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 7.5.20120426 for i386-unknown-linux):\r\n ctFlavId: derived constraint cannot have id\r\n pty = llvm-extra-0.4:LLVM.Extra.Extension.X86.Add'{tc rj}\r\n llvm-extra-0.4:LLVM.Extra.Extension.X86.D1{tc ri}\r\n llvm-extra-0.4:LLVM.Extra.Extension.X86.D1{tc ri}\r\n llvm-extra-0.4:LLVM.Extra.Extension.X86.D2{tc rh}\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\nI tried hard to simplify the example and to remove all dependencies (llvm, type-level), but the test case is still rather involved.\r\n\r\nUnfortunately it is again a problem with functional dependencies and I want to get rid of them anyway, but instead switching to type families and then to type level natural numbers I prefer to switch to type level numbers immediately.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/6049Kind variable generalization error in GADTs2019-07-07T18:52:25ZRichard Eisenbergrae@richarde.devKind variable generalization error in GADTsThe following code fails to compile with 7.5.20120426:
```
{-# LANGUAGE DataKinds, KindSignatures, PolyKinds, GADTs, ExistentialQuantification #-}
data SMaybe :: (k -> *) -> Maybe k -> * where
SNothing :: forall (s :: k -> *). SMaybe...The following code fails to compile with 7.5.20120426:
```
{-# LANGUAGE DataKinds, KindSignatures, PolyKinds, GADTs, ExistentialQuantification #-}
data SMaybe :: (k -> *) -> Maybe k -> * where
SNothing :: forall (s :: k -> *). SMaybe s Nothing
SJust :: forall (s :: k -> *) (a :: k). s a -> SMaybe s (Just a)
```
The reported error is
```
Kind mis-match
The first argument of `SMaybe' should have kind `k1 -> *',
but `s' has kind `k -> *'
In the type `SMaybe s (Just a)'
In the definition of data constructor `SJust'
In the data declaration for `SMaybe'
```
The code compiles fine without the explicit `forall` annotations, but other, more involved code I'm working on (involving `Proxy`) requires the annotations, so simply omitting the explicit kind annotations is not always a viable workaround.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Kind variable generalization error in GADTs","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.5","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code fails to compile with 7.5.20120426:\r\n\r\n{{{\r\n{-# LANGUAGE DataKinds, KindSignatures, PolyKinds, GADTs, ExistentialQuantification #-}\r\n\r\ndata SMaybe :: (k -> *) -> Maybe k -> * where\r\n SNothing :: forall (s :: k -> *). SMaybe s Nothing\r\n SJust :: forall (s :: k -> *) (a :: k). s a -> SMaybe s (Just a)\r\n}}}\r\n\r\nThe reported error is\r\n\r\n{{{\r\n Kind mis-match\r\n The first argument of `SMaybe' should have kind `k1 -> *',\r\n but `s' has kind `k -> *'\r\n In the type `SMaybe s (Just a)'\r\n In the definition of data constructor `SJust'\r\n In the data declaration for `SMaybe'\r\n}}}\r\n\r\nThe code compiles fine without the explicit {{{forall}}} annotations, but other, more involved code I'm working on (involving {{{Proxy}}}) requires the annotations, so simply omitting the explicit kind annotations is not always a viable workaround.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/6044Regression error: Kind variables don't work inside of kind constructors in ty...2019-07-07T18:52:26ZRichard Eisenbergrae@richarde.devRegression error: Kind variables don't work inside of kind constructors in type familiesMany thanks for the quick bug fixes around kind variables recently.
With the newest build (7.5.20120425), the following code fails:
```
{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, KindSignatures #-}
type family Foo (a :: k) :: Ma...Many thanks for the quick bug fixes around kind variables recently.
With the newest build (7.5.20120425), the following code fails:
```
{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, KindSignatures #-}
type family Foo (a :: k) :: Maybe k
type instance Foo a = Just a
```
The error is:
```
Kind mis-match
The first argument of `Just' should have kind `k0',
but `a' has kind `k'
In the type `Just a'
In the type instance declaration for `Foo'
```
The above code compiles without error on, e.g., 7.5.20120329.
I think it's worth noting that the following compiles fine, which surprised me given the error above:
```
type family Id (a :: k) :: k
type instance Id a = a
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Regression error: Kind variables don't work inside of kind constructors in type families","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.5","keywords":["PolyKinds","TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Many thanks for the quick bug fixes around kind variables recently.\r\n\r\nWith the newest build (7.5.20120425), the following code fails:\r\n\r\n{{{\r\n{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, KindSignatures #-}\r\n\r\ntype family Foo (a :: k) :: Maybe k\r\ntype instance Foo a = Just a\r\n}}}\r\n\r\nThe error is:\r\n\r\n{{{\r\n Kind mis-match\r\n The first argument of `Just' should have kind `k0',\r\n but `a' has kind `k'\r\n In the type `Just a'\r\n In the type instance declaration for `Foo'\r\n}}}\r\n\r\nThe above code compiles without error on, e.g., 7.5.20120329.\r\n\r\nI think it's worth noting that the following compiles fine, which surprised me given the error above:\r\n\r\n{{{\r\ntype family Id (a :: k) :: k\r\ntype instance Id a = a\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/6036Kind generalization fails in data family instance GADT2019-07-07T18:52:27ZRichard Eisenbergrae@richarde.devKind generalization fails in data family instance GADTThe following code fails to compile:
```
{-# LANGUAGE DataKinds, TypeFamilies, PolyKinds, GADTs #-}
data family Sing (a :: k)
data instance Sing (a :: Maybe k) where
SNothing :: Sing 'Nothing
SJust :: Sing b -> Sing ('Just b)
```
...The following code fails to compile:
```
{-# LANGUAGE DataKinds, TypeFamilies, PolyKinds, GADTs #-}
data family Sing (a :: k)
data instance Sing (a :: Maybe k) where
SNothing :: Sing 'Nothing
SJust :: Sing b -> Sing ('Just b)
```
The error is
```
Data constructor `SNothing' returns type `Sing
(Maybe k0) ('Nothing k0)'
instead of an instance of its parent type `Sing (Maybe k) a'
In the definition of data constructor `SNothing'
In the data instance declaration for `Sing'
```
It seems that the `k` kind parameter is not being allowed to generalize over other kind parameters. The following (seemingly equivalent) formulation compiles:
```
{-# LANGUAGE ..., ExistentialQuantification #-}
data instance Sing (a :: Maybe k) =
a ~ 'Nothing => SNothing
| forall b. a ~ 'Just b => SJust (Sing b)
```
This was tested on 7.5.20120420.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Kind generalization fails in data family instance GADT","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code fails to compile:\r\n\r\n{{{\r\n{-# LANGUAGE DataKinds, TypeFamilies, PolyKinds, GADTs #-}\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata instance Sing (a :: Maybe k) where\r\n SNothing :: Sing 'Nothing\r\n SJust :: Sing b -> Sing ('Just b)\r\n}}}\r\n\r\nThe error is\r\n\r\n{{{\r\n Data constructor `SNothing' returns type `Sing\r\n (Maybe k0) ('Nothing k0)'\r\n instead of an instance of its parent type `Sing (Maybe k) a'\r\n In the definition of data constructor `SNothing'\r\n In the data instance declaration for `Sing'\r\n}}}\r\n\r\nIt seems that the {{{k}}} kind parameter is not being allowed to generalize over other kind parameters. The following (seemingly equivalent) formulation compiles:\r\n\r\n{{{\r\n{-# LANGUAGE ..., ExistentialQuantification #-}\r\n\r\ndata instance Sing (a :: Maybe k) =\r\n a ~ 'Nothing => SNothing\r\n | forall b. a ~ 'Just b => SJust (Sing b)\r\n}}}\r\n\r\nThis was tested on 7.5.20120420.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/6035Kind-indexed type family failure with polymorphic kinds2019-07-07T18:52:28ZRichard Eisenbergrae@richarde.devKind-indexed type family failure with polymorphic kindsThe following code fails to compile:
```
{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, KindSignatures, GADTs, TypeOperators
#-}
data Nat = Zero | Succ Nat
type family Sing (a :: k) :: k -> *
data SNat n where
SZero :: SNat Zero...The following code fails to compile:
```
{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, KindSignatures, GADTs, TypeOperators
#-}
data Nat = Zero | Succ Nat
type family Sing (a :: k) :: k -> *
data SNat n where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
data SList (a :: [k]) where
SNil :: SList '[]
SCons :: Sing h h -> SList t -> SList (h ': t)
type instance Sing (a :: Nat) = SNat
type instance Sing (a :: [k]) = SList
term :: SList '[ '[Zero], '[]]
term = SCons (SCons SZero SNil) (SCons SNil SNil)
```
The error generated is
```
/Users/rae/temp/Scratch.hs:27:15:
Couldn't match type `Sing [Nat] ((':) Nat 'Zero ('[] Nat))'
with `SList Nat'
Expected type: Sing
[Nat] ((':) Nat 'Zero ('[] Nat)) ((':) Nat 'Zero ('[] Nat))
Actual type: SList Nat ((':) Nat 'Zero ('[] Nat))
In the return type of a call of `SCons'
In the first argument of `SCons', namely `(SCons SZero SNil)'
In the expression: SCons (SCons SZero SNil) (SCons SNil SNil)
/Users/rae/temp/Scratch.hs:27:40:
Couldn't match type `Sing [Nat] ('[] Nat)' with `SList Nat'
Expected type: Sing [Nat] ('[] Nat) ('[] Nat)
Actual type: SList Nat ('[] Nat)
In the first argument of `SCons', namely `SNil'
In the second argument of `SCons', namely `(SCons SNil SNil)'
In the expression: SCons (SCons SZero SNil) (SCons SNil SNil)
```
It seems that the `Sing` kind-indexed type family isn't quite working. My guess is that the problem is that we really want, say, `Sing '[Zero]` to be `SList Nat`, where `Nat` is the implicit kind parameter to `SList`. But, we can't say that. I would hope that the explicit kind annotation on the result of `Sing` would fix the implicit kind parameter to `SList`, but it doesn't seem to.
This was tested on 7.5.20120420.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Kind-indexed type family failure with polymorphic kinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.5","keywords":["PolyKinds","TypeFamilies"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code fails to compile:\r\n\r\n{{{\r\n{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, KindSignatures, GADTs, TypeOperators\r\n #-}\r\n\r\ndata Nat = Zero | Succ Nat\r\n\r\ntype family Sing (a :: k) :: k -> *\r\n\r\ndata SNat n where\r\n SZero :: SNat Zero\r\n SSucc :: SNat n -> SNat (Succ n)\r\n\r\ndata SList (a :: [k]) where\r\n SNil :: SList '[]\r\n SCons :: Sing h h -> SList t -> SList (h ': t)\r\n\r\ntype instance Sing (a :: Nat) = SNat\r\ntype instance Sing (a :: [k]) = SList\r\n\r\nterm :: SList '[ '[Zero], '[]]\r\nterm = SCons (SCons SZero SNil) (SCons SNil SNil)\r\n}}}\r\n\r\nThe error generated is\r\n\r\n{{{\r\n\r\n/Users/rae/temp/Scratch.hs:27:15:\r\n Couldn't match type `Sing [Nat] ((':) Nat 'Zero ('[] Nat))'\r\n with `SList Nat'\r\n Expected type: Sing\r\n [Nat] ((':) Nat 'Zero ('[] Nat)) ((':) Nat 'Zero ('[] Nat))\r\n Actual type: SList Nat ((':) Nat 'Zero ('[] Nat))\r\n In the return type of a call of `SCons'\r\n In the first argument of `SCons', namely `(SCons SZero SNil)'\r\n In the expression: SCons (SCons SZero SNil) (SCons SNil SNil)\r\n\r\n/Users/rae/temp/Scratch.hs:27:40:\r\n Couldn't match type `Sing [Nat] ('[] Nat)' with `SList Nat'\r\n Expected type: Sing [Nat] ('[] Nat) ('[] Nat)\r\n Actual type: SList Nat ('[] Nat)\r\n In the first argument of `SCons', namely `SNil'\r\n In the second argument of `SCons', namely `(SCons SNil SNil)'\r\n In the expression: SCons (SCons SZero SNil) (SCons SNil SNil)\r\n}}}\r\n\r\nIt seems that the {{{Sing}}} kind-indexed type family isn't quite working. My guess is that the problem is that we really want, say, {{{Sing '[Zero]}}} to be {{{SList Nat}}}, where {{{Nat}}} is the implicit kind parameter to {{{SList}}}. But, we can't say that. I would hope that the explicit kind annotation on the result of {{{Sing}}} would fix the implicit kind parameter to {{{SList}}}, but it doesn't seem to.\r\n\r\nThis was tested on 7.5.20120420.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/6013the 'impossible' happened2019-07-07T18:52:35Ztlvbthe 'impossible' happenedPlease forgive me if this is a duplicate or irrelevant, bug reporting and Haskell are two things I work with seldom enough that I cannot be considered good at either, but as what happened should be 'impossible' I thought I'd at least giv...Please forgive me if this is a duplicate or irrelevant, bug reporting and Haskell are two things I work with seldom enough that I cannot be considered good at either, but as what happened should be 'impossible' I thought I'd at least give you a heads up. I tried looking for similar bugs, but I do not really know what I would be looking for...
GHCi (newly opened, -v flag):
```
[leo@derse brutelift]$ ghci -v
GHCi, version 7.4.1: http://www.haskell.org/ghc/ :? for help
Glasgow Haskell Compiler, Version 7.4.1, stage 2 booted by GHC version 7.4.1
Using binary package database: /usr/lib/ghc-7.4.1/package.conf.d/package.cache
wired-in package ghc-prim mapped to ghc-prim-0.2.0.0-c2ff696e5b8ec4d4b2bc2e42085fe471
wired-in package integer-gmp mapped to integer-gmp-0.4.0.0-3cccac07aef8e27023f605c1f45bdf74
wired-in package base mapped to base-4.5.0.0-40b99d05fae6a4eea95ea69e6e0c9702
wired-in package rts mapped to builtin_rts
wired-in package template-haskell mapped to template-haskell-2.7.0.0-8c8cd20e21666657195efabced685fe1
wired-in package dph-seq not found.
wired-in package dph-par not found.
Hsc static flags: -static
Loading package ghc-prim ... linking ... done.
*** gcc:
'/usr/bin/gcc' '-fno-stack-protector' '-Wl,--hash-size=31' '-Wl,--reduce-memory-overheads' '-L/usr/lib/ghc-7.4.1/integer-gmp-0.4.0.0' '--print-file-name' 'libgmp.so'
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :load brutelift
*** Chasing dependencies:
Chasing modules from:
Stable obj: []
Stable BCO: []
unload: retaining objs []
unload: retaining bcos []
Ready for upsweep []
Upsweep completely successful.
*** Deleting temp files:
Deleting:
*** Chasing dependencies:
Chasing modules from: *brutelift.hs
Stable obj: []
Stable BCO: []
unload: retaining objs []
unload: retaining bcos []
Ready for upsweep
[NONREC
ModSummary {
ms_hs_date = Tue Apr 17 18:10:32 CEST 2012
ms_mod = main:Main,
ms_textual_imps = [import (implicit) Prelude, import Data.List]
ms_srcimps = []
}]
*** Deleting temp files:
Deleting:
compile: input file brutelift.hs
Created temporary directory: /tmp/ghc5399_0
*** Checking old interface for main:Main:
[1 of 1] Compiling Main ( brutelift.hs, interpreted )
*** Parser:
*** Renamer/typechecker:
ghc: panic! (the 'impossible' happened)
(GHC version 7.4.1 for x86_64-unknown-linux):
nameModule show{tv abQ}
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
brutelift.hs:
```
import Data.List
data Transfer = Load | Unload
data Action = Left Transfer Int | Right Transfer Int
data BlockDispersion = Blocks {top :: [Int]
, bottom :: [Int]
, left :: [Int]
, right :: [Int]}
deriving (Show)
data Machine = MOK BlockDispersion [Action] | MError BlockDispersion [Action] deriving (show)
rSplitAt i xs = let (a, b) = splitAt i $ reverse xs in
(reverse b, reverse a)
moveR :: Int -> ([a], [a]) -> ([a], [a])
moveR i (a, b) = let (c, d) = rSplitAt i a
in (c, d++b)
moveL :: Int -> ([a], [a]) -> ([a], [a])
moveL i (a, b) = let (c, d) = splitAt i b
in (a++c, d)
```
I am not sure what additional info to provide...
Running an Arch linux system, 8GB ram, installed ghc packgage should be as vanilla as can be...
```
[leo@derse brutelift]$ uname -a
Linux derse 3.3.1-1-ARCH #1 SMP PREEMPT Tue Apr 3 06:46:17 UTC 2012 x86_64 Intel(R) Core(TM) i5-2500K CPU @ 3.30GHz GenuineIntel GNU/Linux
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.4.1 |
| Type | Bug |
| TypeOfFailure | GhciCrash |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"the 'impossible' happened","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1","keywords":["checker,","impossible,","panic,","renamer","type"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Please forgive me if this is a duplicate or irrelevant, bug reporting and Haskell are two things I work with seldom enough that I cannot be considered good at either, but as what happened should be 'impossible' I thought I'd at least give you a heads up. I tried looking for similar bugs, but I do not really know what I would be looking for...\r\n\r\nGHCi (newly opened, -v flag):\r\n{{{\r\n[leo@derse brutelift]$ ghci -v\r\nGHCi, version 7.4.1: http://www.haskell.org/ghc/ :? for help\r\nGlasgow Haskell Compiler, Version 7.4.1, stage 2 booted by GHC version 7.4.1\r\nUsing binary package database: /usr/lib/ghc-7.4.1/package.conf.d/package.cache\r\nwired-in package ghc-prim mapped to ghc-prim-0.2.0.0-c2ff696e5b8ec4d4b2bc2e42085fe471\r\nwired-in package integer-gmp mapped to integer-gmp-0.4.0.0-3cccac07aef8e27023f605c1f45bdf74\r\nwired-in package base mapped to base-4.5.0.0-40b99d05fae6a4eea95ea69e6e0c9702\r\nwired-in package rts mapped to builtin_rts\r\nwired-in package template-haskell mapped to template-haskell-2.7.0.0-8c8cd20e21666657195efabced685fe1\r\nwired-in package dph-seq not found.\r\nwired-in package dph-par not found.\r\nHsc static flags: -static\r\nLoading package ghc-prim ... linking ... done.\r\n*** gcc:\r\n'/usr/bin/gcc' '-fno-stack-protector' '-Wl,--hash-size=31' '-Wl,--reduce-memory-overheads' '-L/usr/lib/ghc-7.4.1/integer-gmp-0.4.0.0' '--print-file-name' 'libgmp.so'\r\nLoading package integer-gmp ... linking ... done.\r\nLoading package base ... linking ... done.\r\nPrelude> :load brutelift\r\n*** Chasing dependencies:\r\nChasing modules from: \r\nStable obj: []\r\nStable BCO: []\r\nunload: retaining objs []\r\nunload: retaining bcos []\r\nReady for upsweep []\r\nUpsweep completely successful.\r\n*** Deleting temp files:\r\nDeleting: \r\n*** Chasing dependencies:\r\nChasing modules from: *brutelift.hs\r\nStable obj: []\r\nStable BCO: []\r\nunload: retaining objs []\r\nunload: retaining bcos []\r\nReady for upsweep\r\n [NONREC\r\n ModSummary {\r\n ms_hs_date = Tue Apr 17 18:10:32 CEST 2012\r\n ms_mod = main:Main,\r\n ms_textual_imps = [import (implicit) Prelude, import Data.List]\r\n ms_srcimps = []\r\n }]\r\n*** Deleting temp files:\r\nDeleting: \r\ncompile: input file brutelift.hs\r\nCreated temporary directory: /tmp/ghc5399_0\r\n*** Checking old interface for main:Main:\r\n[1 of 1] Compiling Main ( brutelift.hs, interpreted )\r\n*** Parser:\r\n*** Renamer/typechecker:\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 7.4.1 for x86_64-unknown-linux):\r\n\tnameModule show{tv abQ}\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n>\r\n}}}\r\n\r\nbrutelift.hs:\r\n\r\n{{{\r\nimport Data.List\r\n\r\ndata Transfer = Load | Unload\r\ndata Action = Left Transfer Int | Right Transfer Int\r\n\r\ndata BlockDispersion = Blocks {top :: [Int]\r\n\t\t\t\t, bottom :: [Int]\r\n\t\t\t\t, left :: [Int]\r\n\t\t\t\t, right :: [Int]}\r\n\t\t\t\tderiving (Show)\r\n\r\ndata Machine = MOK BlockDispersion [Action] | MError BlockDispersion [Action] deriving (show)\r\n\r\n\r\nrSplitAt i xs = let (a, b) = splitAt i $ reverse xs in\r\n\t(reverse b, reverse a)\r\n\t\r\nmoveR :: Int -> ([a], [a]) -> ([a], [a])\r\nmoveR i (a, b) = let (c, d) = rSplitAt i a\r\n\t\t\tin (c, d++b)\r\nmoveL :: Int -> ([a], [a]) -> ([a], [a])\r\nmoveL i (a, b) = let (c, d) = splitAt i b\r\n\t\t\tin (a++c, d)\r\n}}}\r\n\r\n\r\nI am not sure what additional info to provide...\r\nRunning an Arch linux system, 8GB ram, installed ghc packgage should be as vanilla as can be...\r\n\r\n{{{\r\n[leo@derse brutelift]$ uname -a\r\nLinux derse 3.3.1-1-ARCH #1 SMP PREEMPT Tue Apr 3 06:46:17 UTC 2012 x86_64 Intel(R) Core(TM) i5-2500K CPU @ 3.30GHz GenuineIntel GNU/Linux\r\n}}}\r\n\r\n","type_of_failure":"GhciCrash","blocking":[]} -->7.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/5978Type error in one function causes wrong type error report in another function...2019-07-07T18:52:44ZLemmingType error in one function causes wrong type error report in another function in the presence of functionally dependent typesWhen trying to reduce my problem in #5970 to a simple program I encountered an even more obvious bug. The problem is essentially as follows: I have
```
correct :: T
correct = ...
wrong :: T
wrong = f correct
```
where 'wrong' has a ty...When trying to reduce my problem in #5970 to a simple program I encountered an even more obvious bug. The problem is essentially as follows: I have
```
correct :: T
correct = ...
wrong :: T
wrong = f correct
```
where 'wrong' has a type error and 'correct' is type correct. If I outcomment 'wrong' then GHC correctly confirms type-correctness of 'correct', but if 'wrong' is enabled then GHC claims a type error in both 'wrong' and 'correct'.
To me it looks like the type-checker is trying to unify types across function boundaries. This would explain both non-linear growth of type-checking time and the observed effect of incorrect type errors.
See attached program for a working example.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.4.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":"Type error in one function causes wrong type error report in another function in the presence of functionally dependent types","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When trying to reduce my problem in #5970 to a simple program I encountered an even more obvious bug. The problem is essentially as follows: I have\r\n{{{\r\ncorrect :: T\r\ncorrect = ...\r\n\r\nwrong :: T\r\nwrong = f correct\r\n}}}\r\nwhere 'wrong' has a type error and 'correct' is type correct. If I outcomment 'wrong' then GHC correctly confirms type-correctness of 'correct', but if 'wrong' is enabled then GHC claims a type error in both 'wrong' and 'correct'.\r\nTo me it looks like the type-checker is trying to unify types across function boundaries. This would explain both non-linear growth of type-checking time and the observed effect of incorrect type errors.\r\nSee attached program for a working example.","type_of_failure":"OtherFailure","blocking":[]} -->7.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/5970Type checker hangs2019-07-07T18:52:47ZLemmingType checker hangsWhen compiling my synthesizer-llvm package, GHC-7.4.1 hangs in the type checking phase for the module
http://code.haskell.org/synthesizer/llvm/src/Synthesizer/LLVM/Server/Packed/Instrument.hs
This module always needed more than a minute...When compiling my synthesizer-llvm package, GHC-7.4.1 hangs in the type checking phase for the module
http://code.haskell.org/synthesizer/llvm/src/Synthesizer/LLVM/Server/Packed/Instrument.hs
This module always needed more than a minute for type-checking in GHC-7.2.2 and before. I guess this was because it is a module where functions with a lot of type-level arithmetic from the type-level package are applied to values of concrete types. Maybe with GHC-7.4.1 the compilation time simply became even longer - at least several minutes.
I tried to simplify the example and reduce the dependencies. This is not so simple because reducing the module size also decreases type checking time and when drastically simplified the compilation time for that module is ok. Now I am trying to construct an example where I repeat the same (simple) function definition. I already observed that repeating a function definition n times does not multiply the type checking by n but it needs considerably more time. I think this can be considered a bug.
I am investigating further. If you have some advice, I like to know. Maybe you remember a 'foldl' that should be a 'foldr' in the type checker, that may cause a quadratic type checking time ... If so then this would be a good opportunity to fix it. ;-)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.4.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":"Type checker hangs","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When compiling my synthesizer-llvm package, GHC-7.4.1 hangs in the type checking phase for the module\r\nhttp://code.haskell.org/synthesizer/llvm/src/Synthesizer/LLVM/Server/Packed/Instrument.hs\r\n\r\nThis module always needed more than a minute for type-checking in GHC-7.2.2 and before. I guess this was because it is a module where functions with a lot of type-level arithmetic from the type-level package are applied to values of concrete types. Maybe with GHC-7.4.1 the compilation time simply became even longer - at least several minutes.\r\n\r\nI tried to simplify the example and reduce the dependencies. This is not so simple because reducing the module size also decreases type checking time and when drastically simplified the compilation time for that module is ok. Now I am trying to construct an example where I repeat the same (simple) function definition. I already observed that repeating a function definition n times does not multiply the type checking by n but it needs considerably more time. I think this can be considered a bug.\r\n\r\nI am investigating further. If you have some advice, I like to know. Maybe you remember a 'foldl' that should be a 'foldr' in the type checker, that may cause a quadratic type checking time ... If so then this would be a good opportunity to fix it. ;-)\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/5957signatures are too permissive2019-07-07T18:52:51ZChristian Maedersignatures are too permissiveghc should reject the following (accidentally mistyped) signature, unless `-XFlexibleContexts` is used.
```
flex :: Int -> Show a => a -> String
flex i a = show a ++ show i
```
hugs and ghc version below 7 rejected this correctly:
```...ghc should reject the following (accidentally mistyped) signature, unless `-XFlexibleContexts` is used.
```
flex :: Int -> Show a => a -> String
flex i a = show a ++ show i
```
hugs and ghc version below 7 rejected this correctly:
```
All of the type variables in the constraint `Show a'
are already in scope (at least one must be universally quantified here)
(Use -XFlexibleContexts to lift this restriction)
In the type signature for `flex':
flex :: Int -> (Show a) => a -> String
```
It is not Haskell98 nor Haskell2010 (I believe).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.4.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":"signatures are too permissive","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"ghc should reject the following (accidentally mistyped) signature, unless `-XFlexibleContexts` is used.\r\n\r\n{{{\r\nflex :: Int -> Show a => a -> String\r\nflex i a = show a ++ show i\r\n}}}\r\n\r\nhugs and ghc version below 7 rejected this correctly:\r\n\r\n{{{\r\n All of the type variables in the constraint `Show a'\r\n are already in scope (at least one must be universally quantified here)\r\n (Use -XFlexibleContexts to lift this restriction)\r\n In the type signature for `flex':\r\n flex :: Int -> (Show a) => a -> String\r\n}}}\r\n\r\nIt is not Haskell98 nor Haskell2010 (I believe).\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/5952Extra ' in error output concerning promoted kinds2019-07-07T18:52:52ZRichard Eisenbergrae@richarde.devExtra ' in error output concerning promoted kindsWhen I try to compile the following code, a slightly erroneous error message is produced:
```
{-# LANGUAGE DataKinds #-}
foo :: 'False
foo = undefined
```
The error message is
```
Kind mis-match
Expected kind `ArgKind', but `False' h...When I try to compile the following code, a slightly erroneous error message is produced:
```
{-# LANGUAGE DataKinds #-}
foo :: 'False
foo = undefined
```
The error message is
```
Kind mis-match
Expected kind `ArgKind', but `False' has kind 'Bool
In the type signature for `foo': foo :: False
```
The problem is that the kind of `'False` is reported as `'Bool`. However, if you use a kind written `'Bool` in a program, that program fails to compile. As I understand it, the only way to write the kind of `'False` is `Bool`, without the initial tick.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Extra ' in error output concerning promoted kinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.5","keywords":["DataKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I try to compile the following code, a slightly erroneous error message is produced:\r\n\r\n{{{\r\n{-# LANGUAGE DataKinds #-}\r\n\r\nfoo :: 'False\r\nfoo = undefined\r\n}}}\r\n\r\nThe error message is\r\n\r\n{{{\r\nKind mis-match\r\nExpected kind `ArgKind', but `False' has kind 'Bool\r\nIn the type signature for `foo': foo :: False\r\n}}}\r\n\r\nThe problem is that the kind of {{{'False}}} is reported as {{{'Bool}}}. However, if you use a kind written {{{'Bool}}} in a program, that program fails to compile. As I understand it, the only way to write the kind of {{{'False}}} is {{{Bool}}}, without the initial tick.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/5938Kind variables not allowed in type family instance declarations2019-07-07T18:52:55ZRichard Eisenbergrae@richarde.devKind variables not allowed in type family instance declarationsI am trying to create a kind-indexed type family, but I cannot use kind variables in my kind annotations:
```
{-# LANGUAGE PolyKinds, TypeFamilies, DataKinds #-}
type family KindFam a
type instance KindFam (a :: *) = Int
type instance ...I am trying to create a kind-indexed type family, but I cannot use kind variables in my kind annotations:
```
{-# LANGUAGE PolyKinds, TypeFamilies, DataKinds #-}
type family KindFam a
type instance KindFam (a :: *) = Int
type instance KindFam (a :: Bool) = Bool
type instance KindFam (a :: Maybe k) = Char -- doesn't work
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Kind variables not allowed in type family instance declarations","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I am trying to create a kind-indexed type family, but I cannot use kind variables in my kind annotations:\r\n\r\n{{{\r\n{-# LANGUAGE PolyKinds, TypeFamilies, DataKinds #-}\r\n\r\ntype family KindFam a\r\ntype instance KindFam (a :: *) = Int\r\ntype instance KindFam (a :: Bool) = Bool\r\ntype instance KindFam (a :: Maybe k) = Char -- doesn't work\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/5937Kind variables not allowed in data declaration kind annotation2019-07-07T18:52:55ZRichard Eisenbergrae@richarde.devKind variables not allowed in data declaration kind annotationGHC won't accept kind variables stated directly in a data declaration. For example, the following does not compile:
```
data SMaybe :: (k -> *) -> Maybe k -> * where
SNothing :: SMaybe s 'Nothing
SJust :: s a -> SMaybe s ('Just a)
`...GHC won't accept kind variables stated directly in a data declaration. For example, the following does not compile:
```
data SMaybe :: (k -> *) -> Maybe k -> * where
SNothing :: SMaybe s 'Nothing
SJust :: s a -> SMaybe s ('Just a)
```
However, the following does compile:
```
data SMaybe' (s :: k -> *) (m :: Maybe k) where
SNothing' :: SMaybe' s 'Nothing
SJust' :: s a -> SMaybe' s ('Just a)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Kind variables not allowed in data declaration kind annotation","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.5","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC won't accept kind variables stated directly in a data declaration. For example, the following does not compile:\r\n\r\n{{{\r\ndata SMaybe :: (k -> *) -> Maybe k -> * where\r\n SNothing :: SMaybe s 'Nothing\r\n SJust :: s a -> SMaybe s ('Just a)\r\n}}}\r\n\r\nHowever, the following does compile:\r\n\r\n{{{\r\ndata SMaybe' (s :: k -> *) (m :: Maybe k) where\r\n SNothing' :: SMaybe' s 'Nothing\r\n SJust' :: s a -> SMaybe' s ('Just a)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/5935Failure to resolve AnyK2019-07-07T18:52:56ZRichard Eisenbergrae@richarde.devFailure to resolve AnyKConsider the following code:
```
{-# LANGUAGE PolyKinds,
GADTs,
DataKinds,
KindSignatures
#-}
data SList a where
SNil :: SList '[]
x :: SList ('[] :: [Bool])
x = SNil
```
Compiling this code ...Consider the following code:
```
{-# LANGUAGE PolyKinds,
GADTs,
DataKinds,
KindSignatures
#-}
data SList a where
SNil :: SList '[]
x :: SList ('[] :: [Bool])
x = SNil
```
Compiling this code causes GHC to emit an error saying that `AnyK` cannot be unified with `Bool`. It seems that `AnyK` is a placeholder for an undetermined kind and that it should unify with any well-formed kind.
As a much smaller issue, the error emitted speaks about "types" where it means "kinds".
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.4.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":"Failure to resolve AnyK","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1","keywords":["DataKinds","PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following code:\r\n\r\n{{{\r\n{-# LANGUAGE PolyKinds,\r\n GADTs,\r\n DataKinds,\r\n KindSignatures\r\n #-}\r\n\r\ndata SList a where\r\n SNil :: SList '[]\r\n\r\nx :: SList ('[] :: [Bool])\r\nx = SNil\r\n}}}\r\n\r\nCompiling this code causes GHC to emit an error saying that {{{AnyK}}} cannot be unified with {{{Bool}}}. It seems that {{{AnyK}}} is a placeholder for an undetermined kind and that it should unify with any well-formed kind.\r\n\r\nAs a much smaller issue, the error emitted speaks about \"types\" where it means \"kinds\".","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/5927A type-level "implies" constraint on Constraints2020-02-05T20:35:11ZillissiusA type-level "implies" constraint on ConstraintsI have a datatype:
```
data Exists c where Exists :: c a => a -> Exists c
```
I have an instance for it:
```
instance Show (Exists Show) where
show (Exists a) = show a
```
And that's alright, as far as it goes: any Exists Show ca...I have a datatype:
```
data Exists c where Exists :: c a => a -> Exists c
```
I have an instance for it:
```
instance Show (Exists Show) where
show (Exists a) = show a
```
And that's alright, as far as it goes: any Exists Show can indeed itself be shown. But I want more. I want to be able to say:
```
instance (c `Implies` Show) => Show (Exists c) where
show (Exists a) = show a
```
In other words, I want to be able to say that any (Exists c) where the constraint c implies Show can be shown. For example, if Num still had a Show constraint, I wouldn't want to have to write a separate instance Show (Exists Num) to be able to show an Exists Num; I would want to be able to write a single instance (along the lines of the above) which works for both.
GHC clearly has this information: it lets me use a function of type `forall a. Eq a => a -> r` as one of type `forall a. Ord a => a -> r`, but not vice versa, so it knows that Ord implies Eq, but not vice versa. I've attached a file which demonstrates this and a couple of other examples.
What's not completely clear to me is what would be the appropriate way to be able to ask it about this. An Implies constraint to parallel the (\~) constraint would work, but with what syntax? (Just straightforwardly call it Implies?) And what semantics -- what would be the kind of Implies? It's notable that in the above example its arguments aren't of type Constraint, but rather \* -\> Constraint, and for (\* -\> \*) -\> Constraint it could similarly work, and with MPTCs \* -\> \* -\> Constraint and (\* -\> \*) -\> (\* -\> \*) -\> Constraint and \* -\> (\* -\> \*) -\> Constraint and so on probably also make sense... but I have no idea how to formalize this, where the boundaries lie, and whether it makes any kind of sense. I can try to think harder about it if that would help, but hopefully the outlines of the situation are more immediately obvious to someone on the GHC team.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.4.1 |
| Type | FeatureRequest |
| 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":"A type-level \"implies\" constraint on Constraints","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"I have a datatype:\r\n\r\n{{{\r\ndata Exists c where Exists :: c a => a -> Exists c\r\n}}}\r\n\r\nI have an instance for it:\r\n\r\n{{{\r\ninstance Show (Exists Show) where\r\n show (Exists a) = show a\r\n}}}\r\n\r\nAnd that's alright, as far as it goes: any Exists Show can indeed itself be shown. But I want more. I want to be able to say:\r\n\r\n{{{\r\ninstance (c `Implies` Show) => Show (Exists c) where\r\n show (Exists a) = show a\r\n}}}\r\n\r\nIn other words, I want to be able to say that any (Exists c) where the constraint c implies Show can be shown. For example, if Num still had a Show constraint, I wouldn't want to have to write a separate instance Show (Exists Num) to be able to show an Exists Num; I would want to be able to write a single instance (along the lines of the above) which works for both.\r\n\r\nGHC clearly has this information: it lets me use a function of type {{{forall a. Eq a => a -> r}}} as one of type {{{forall a. Ord a => a -> r}}}, but not vice versa, so it knows that Ord implies Eq, but not vice versa. I've attached a file which demonstrates this and a couple of other examples.\r\n\r\nWhat's not completely clear to me is what would be the appropriate way to be able to ask it about this. An Implies constraint to parallel the (~) constraint would work, but with what syntax? (Just straightforwardly call it Implies?) And what semantics -- what would be the kind of Implies? It's notable that in the above example its arguments aren't of type Constraint, but rather * -> Constraint, and for (* -> *) -> Constraint it could similarly work, and with MPTCs * -> * -> Constraint and (* -> *) -> (* -> *) -> Constraint and * -> (* -> *) -> Constraint and so on probably also make sense... but I have no idea how to formalize this, where the boundaries lie, and whether it makes any kind of sense. I can try to think harder about it if that would help, but hopefully the outlines of the situation are more immediately obvious to someone on the GHC team.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/5910Holes with other constraints2024-01-22T12:03:56ZxnyhpsHoles with other constraintsHello. As can be seen on http://hackage.haskell.org/trac/ghc/wiki/Holes and http://www.haskell.org/pipermail/glasgow-haskell-users/2012-January/021670.html, we've been working on adding holes to GHC. I'm opening this ticket about a speci...Hello. As can be seen on http://hackage.haskell.org/trac/ghc/wiki/Holes and http://www.haskell.org/pipermail/glasgow-haskell-users/2012-January/021670.html, we've been working on adding holes to GHC. I'm opening this ticket about a specific problem I've been having, and I hope someone has a suggestion of how to do it correctly.
As holes work quite similarly to implicit parameters (see the wiki-page for a comparison), we started out in the same way as implicit parameters. Typechecking of a hole generates a constraint (a new type of constraint), and the constraint solver will try to find the right type for each hole. The difference is that hole constraints never show up in a type, but their type is printed separately. This currently works correctly for simple typechecking, but it has some problems when other constraints are generated too. A simple example:
```
test :: String
test = show _h
```
Here, the `_h` denotes a hole named "h". If this function is defined like this inside a module it will currently fail:
```
test2.hs:2:8:
No instance for (Show a0)
arising from a use of `show'
The type variable `a0' is ambiguous
Possible fix: add a type signature that fixes these type variable(s)
In the expression: show (_h)
In an equation for `test': test = show (_h)
Failed, modules loaded: none.
```
The problem is that the `Show` constraint is still there. If the type signature is omitted and the monomorphism restriction off, we can see that the types found are:
```
Found the following holes:
_h :: GHC.Show.Show a => a
...
test :: Show a => String
```
The problem is the `Show a` that is irrelevant to the actual type of `test`, but nevertheless it's there.
How do other approaches handle this?
**undefined**:
```
test :: String
test = show undefined
```
Gives the same ambiguity error, even if the signature is omitted.
**Implicit parameters**:
```
test = show ?h
```
This works, but generates the following type signature:
```
test :: (Show a, ?h::a) => String
```
So, as I'd want to use it, this is wrong. It has the right ingredients, but I'd want:
```
test :: (?h :: (Show a) => a) => String
```
For implicit parameters the difference doesn't matter too much, as implicit parameters are still parameters: they still show up in the type signature. A hole is not required to be a parameter, so it's more important that every constraint only shows up where it's necessary.
So the problem is that I don't know how to select from the constraints only those that are applicable to the expression/function itself, and those that apply to which of the holes. I've tried typechecking all of the holes first, but I don't know how to determine how to change the constraint set after that. If you need more information about how it currently works, or have any feedback on this approach, please let me know. I'm still quite unfamiliar with the architecture of GHC. :)
----
I'm attaching a patch against the master branch on git with my current work in case someone is interested in trying it. Note that the code generation is pretty much a stub and it will panic if you try to run a function with a hole. It will print the holes of an expression if you invoke `:t` (it doesn't currently print the holes when loading a module, but it should still print them with `:t` on a function from the module). Also, I do not recommend building stage 1 with this, as some packages have some issues. Easiest is to build stage 1 and the packages without these changes and then applying the patch and then building only stage 2.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.5 |
| Type | FeatureRequest |
| TypeOfFailure | IncorrectWarning |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Holes with other constraints","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.5","keywords":["holes"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Hello. As can be seen on http://hackage.haskell.org/trac/ghc/wiki/Holes and http://www.haskell.org/pipermail/glasgow-haskell-users/2012-January/021670.html, we've been working on adding holes to GHC. I'm opening this ticket about a specific problem I've been having, and I hope someone has a suggestion of how to do it correctly.\r\n\r\nAs holes work quite similarly to implicit parameters (see the wiki-page for a comparison), we started out in the same way as implicit parameters. Typechecking of a hole generates a constraint (a new type of constraint), and the constraint solver will try to find the right type for each hole. The difference is that hole constraints never show up in a type, but their type is printed separately. This currently works correctly for simple typechecking, but it has some problems when other constraints are generated too. A simple example:\r\n\r\n{{{\r\ntest :: String\r\ntest = show _h\r\n}}}\r\n\r\nHere, the {{{_h}}} denotes a hole named \"h\". If this function is defined like this inside a module it will currently fail:\r\n\r\n{{{\r\ntest2.hs:2:8:\r\n No instance for (Show a0)\r\n arising from a use of `show'\r\n The type variable `a0' is ambiguous\r\n Possible fix: add a type signature that fixes these type variable(s)\r\n In the expression: show (_h)\r\n In an equation for `test': test = show (_h)\r\nFailed, modules loaded: none.\r\n}}}\r\n\r\nThe problem is that the {{{Show}}} constraint is still there. If the type signature is omitted and the monomorphism restriction off, we can see that the types found are:\r\n\r\n{{{\r\nFound the following holes: \r\n_h :: GHC.Show.Show a => a\r\n...\r\ntest :: Show a => String\r\n}}}\r\n\r\nThe problem is the {{{Show a}}} that is irrelevant to the actual type of {{{test}}}, but nevertheless it's there.\r\n\r\n\r\nHow do other approaches handle this?\r\n\r\n'''undefined''':\r\n{{{\r\ntest :: String\r\ntest = show undefined\r\n}}}\r\n\r\nGives the same ambiguity error, even if the signature is omitted.\r\n\r\n'''Implicit parameters''':\r\n{{{\r\ntest = show ?h\r\n}}}\r\n\r\nThis works, but generates the following type signature:\r\n\r\n{{{\r\ntest :: (Show a, ?h::a) => String\r\n}}}\r\n\r\nSo, as I'd want to use it, this is wrong. It has the right ingredients, but I'd want:\r\n\r\n{{{\r\ntest :: (?h :: (Show a) => a) => String\r\n}}}\r\n\r\nFor implicit parameters the difference doesn't matter too much, as implicit parameters are still parameters: they still show up in the type signature. A hole is not required to be a parameter, so it's more important that every constraint only shows up where it's necessary.\r\n\r\nSo the problem is that I don't know how to select from the constraints only those that are applicable to the expression/function itself, and those that apply to which of the holes. I've tried typechecking all of the holes first, but I don't know how to determine how to change the constraint set after that. If you need more information about how it currently works, or have any feedback on this approach, please let me know. I'm still quite unfamiliar with the architecture of GHC. :)\r\n\r\n----\r\n\r\nI'm attaching a patch against the master branch on git with my current work in case someone is interested in trying it. Note that the code generation is pretty much a stub and it will panic if you try to run a function with a hole. It will print the holes of an expression if you invoke {{{:t}}} (it doesn't currently print the holes when loading a module, but it should still print them with {{{:t}}} on a function from the module). Also, I do not recommend building stage 1 with this, as some packages have some issues. Easiest is to build stage 1 and the packages without these changes and then applying the patch and then building only stage 2.","type_of_failure":"IncorrectWarning","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/5837Context reduction stack overflow can take very long2019-07-07T18:53:23ZdreixelContext reduction stack overflow can take very longThe following code, taken from the "Haskell Type Constraints Unleashed" paper:
```
{-# LANGUAGE TypeFamilies #-}
type family TF a :: *
type instance TF (a,b) = (TF a, TF b)
t :: (a ~ TF (a,Int)) => Int
t = undefined
```
fails almost ...The following code, taken from the "Haskell Type Constraints Unleashed" paper:
```
{-# LANGUAGE TypeFamilies #-}
type family TF a :: *
type instance TF (a,b) = (TF a, TF b)
t :: (a ~ TF (a,Int)) => Int
t = undefined
```
fails almost immediately with `Context reduction stack overflow` on GHC 7.2, but seems to loop forever with 7.4.1-rc2. Setting `-fcontext-stack` to `20` results in near immediate termination with the same error. But #5395 raised the context stack size default to `200`, which makes this code (that does not use `-XUndecidableInstances`) take "forever" to compile.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.4.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":"Context reduction stack overflow can take very long","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code, taken from the \"Haskell Type Constraints Unleashed\" paper:\r\n{{{\r\n{-# LANGUAGE TypeFamilies #-}\r\n\r\ntype family TF a :: *\r\ntype instance TF (a,b) = (TF a, TF b)\r\n\r\nt :: (a ~ TF (a,Int)) => Int\r\nt = undefined\r\n}}}\r\nfails almost immediately with `Context reduction stack overflow` on GHC 7.2, but seems to loop forever with 7.4.1-rc2. Setting `-fcontext-stack` to `20` results in near immediate termination with the same error. But #5395 raised the context stack size default to `200`, which makes this code (that does not use `-XUndecidableInstances`) take \"forever\" to compile.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->7.6.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/5802GHC Panic with PolyKinds and TypeFamilies2019-07-07T18:53:31ZdominiquedevrieseGHC Panic with PolyKinds and TypeFamiliesThe following crashes:
```
{-# LANGUAGE TypeOperators, PolyKinds, TypeFamilies, ExplicitForAll, GADTs #-}
module GHCBug where
data Nat = Zero | Succ Nat
data NatV (a :: Nat) where
ZeroV :: NatV Zero
SuccV :: NatV n ->...The following crashes:
```
{-# LANGUAGE TypeOperators, PolyKinds, TypeFamilies, ExplicitForAll, GADTs #-}
module GHCBug where
data Nat = Zero | Succ Nat
data NatV (a :: Nat) where
ZeroV :: NatV Zero
SuccV :: NatV n -> NatV (Succ n)
data Phantom t = Whoo
data ListV (a :: [*]) where
NilV :: ListV '[]
(:::) :: Phantom a -> ListV as -> ListV (a ': as)
type family (:+:) (a :: Nat) (b :: Nat) :: Nat
type instance Zero :+: b = b
type instance (Succ a) :+: b = Succ (a :+: b)
type family TReplicate (n :: Nat) (t :: *) :: [*]
type instance TReplicate Zero t = '[]
type instance TReplicate (Succ n) t = t ': TReplicate n t
replicateTList :: forall (n :: Nat). forall t.
NatV n -> Phantom t -> ListV (TReplicate n t)
replicateTList ZeroV _ = NilV
replicateTList (SuccV n) t = t ::: replicateTList n t
```
Potentially related to 5717 and 5768, although those two seem to be related to ScopedTypeVariables? They also seem to have a different panic message, although maybe this is because I'm using a debug-built GHC?
I'm not actually using 7.4.1-rc1, but 7.4 HEAD at the time of this writing.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.4.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":"GHC Panic with PolyKinds and TypeFamilies","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1-rc1","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following crashes:\r\n\r\n{{{\r\n {-# LANGUAGE TypeOperators, PolyKinds, TypeFamilies, ExplicitForAll, GADTs #-}\r\n\r\n module GHCBug where\r\n\r\n data Nat = Zero | Succ Nat\r\n\r\n data NatV (a :: Nat) where\r\n ZeroV :: NatV Zero\r\n SuccV :: NatV n -> NatV (Succ n)\r\n\r\n data Phantom t = Whoo\r\n\r\n data ListV (a :: [*]) where\r\n NilV :: ListV '[]\r\n (:::) :: Phantom a -> ListV as -> ListV (a ': as)\r\n\r\n type family (:+:) (a :: Nat) (b :: Nat) :: Nat\r\n type instance Zero :+: b = b\r\n type instance (Succ a) :+: b = Succ (a :+: b)\r\n\r\n type family TReplicate (n :: Nat) (t :: *) :: [*]\r\n type instance TReplicate Zero t = '[]\r\n type instance TReplicate (Succ n) t = t ': TReplicate n t\r\n\r\n replicateTList :: forall (n :: Nat). forall t.\r\n\t\t NatV n -> Phantom t -> ListV (TReplicate n t)\r\n replicateTList ZeroV _ = NilV\r\n replicateTList (SuccV n) t = t ::: replicateTList n t\r\n}}}\r\n\r\nPotentially related to 5717 and 5768, although those two seem to be related to ScopedTypeVariables? They also seem to have a different panic message, although maybe this is because I'm using a debug-built GHC?\r\n\r\nI'm not actually using 7.4.1-rc1, but 7.4 HEAD at the time of this writing.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/5798PolyKinds: couldn't match kind `BOX' against `*'2019-07-07T18:53:32ZreinerpPolyKinds: couldn't match kind `BOX' against `*'This module fails to compile:
```
{-# LANGUAGE PolyKinds #-}
module Test where
data Proxy t = ProxyC
test :: Proxy '[Int, Bool]
test = ProxyC -- doesn't compile
-- test = undefined -- compiles
```
The compilation error...This module fails to compile:
```
{-# LANGUAGE PolyKinds #-}
module Test where
data Proxy t = ProxyC
test :: Proxy '[Int, Bool]
test = ProxyC -- doesn't compile
-- test = undefined -- compiles
```
The compilation error is
```
Test.hs:8:8:
Couldn't match kind `BOX' against `*'
Kind incompatibility when matching types:
k0 :: BOX
[*] :: *
In the expression: ProxyC
In an equation for `test': test = ProxyC
```
However, this module is indeed well-typed, -sorted, and -kinded. The types and kinds should be as follows:
```
Proxy :: forall (k :: BOX). k -> *
ProxyC :: forall (k :: BOX). forall (t :: k). Proxy t
'[Int, Bool] :: [*]
[*] :: BOX
```
However, the error message suggests that GHC gives `[*]` the sort `*`, instead of `BOX`. This is wrong.
Note that the module compiles if `test = ProxyC` is replaced with `test = undefined`. So it seems that type-checking of type signature sets `[*] :: BOX`, whereas type-checking of the value expression sets `[*] :: *`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.4.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":"PolyKinds: couldn't match kind `BOX' against `*'","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1-rc1","keywords":["PolyKinds"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This module fails to compile:\r\n\r\n{{{\r\n{-# LANGUAGE PolyKinds #-}\r\n\r\nmodule Test where\r\n\r\ndata Proxy t = ProxyC\r\n\r\ntest :: Proxy '[Int, Bool]\r\ntest = ProxyC -- doesn't compile\r\n-- test = undefined -- compiles\r\n}}}\r\n\r\nThe compilation error is \r\n{{{\r\nTest.hs:8:8:\r\n Couldn't match kind `BOX' against `*'\r\n Kind incompatibility when matching types:\r\n k0 :: BOX\r\n [*] :: *\r\n In the expression: ProxyC\r\n In an equation for `test': test = ProxyC\r\n}}}\r\n\r\nHowever, this module is indeed well-typed, -sorted, and -kinded. The types and kinds should be as follows:\r\n\r\n{{{\r\nProxy :: forall (k :: BOX). k -> *\r\nProxyC :: forall (k :: BOX). forall (t :: k). Proxy t\r\n'[Int, Bool] :: [*]\r\n[*] :: BOX\r\n}}}\r\n\r\nHowever, the error message suggests that GHC gives {{{[*]}}} the sort {{{*}}}, instead of {{{BOX}}}. This is wrong.\r\n\r\nNote that the module compiles if {{{test = ProxyC}}} is replaced with {{{test = undefined}}}. So it seems that type-checking of type signature sets {{{[*] :: BOX}}}, whereas type-checking of the value expression sets {{{[*] :: *}}}.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->7.4.2https://gitlab.haskell.org/ghc/ghc/-/issues/5792PolyKinds and recompilation causes internal error2019-07-07T18:53:35ZreinerpPolyKinds and recompilation causes internal errorGiven these two files:
```
module A where
-- empty
```
and
```
{-# LANGUAGE PolyKinds, TypeFamilies, UndecidableInstances #-}
module B where
import A
data T = TT
type family Compare (m :: T) :: Ordering
type instance Compare TT = C...Given these two files:
```
module A where
-- empty
```
and
```
{-# LANGUAGE PolyKinds, TypeFamilies, UndecidableInstances #-}
module B where
import A
data T = TT
type family Compare (m :: T) :: Ordering
type instance Compare TT = Compare TT
type Compare' a = Compare a
```
We can cause an internal GHC error as follows:
```
$ rm *.o *.hi
$ ghc B.hs
[1 of 2] Compiling A ( A.hs, A.o )
[2 of 2] Compiling B ( B.hs, B.o )
$ sleep 1
$ touch B.hs
$ ghc B.hs
[2 of 2] Compiling B ( B.hs, B.o )
B.hs:11:19:
GHC internal error: `Compare' is not in scope during type checking, but it passed the renamer
tcl_env of environment: [(a9R, AThing k_a9U)]
In the type `Compare a'
In the type synonym declaration for Compare'
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.4.1-rc1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | MacOS X |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"PolyKinds and recompilation causes internal error","status":"New","operating_system":"MacOS X","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1-rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Given these two files:\r\n{{{\r\nmodule A where\r\n-- empty\r\n}}}\r\n\r\nand\r\n\r\n{{{\r\n\r\n{-# LANGUAGE PolyKinds, TypeFamilies, UndecidableInstances #-}\r\nmodule B where\r\n\r\nimport A\r\n\r\ndata T = TT\r\n\r\ntype family Compare (m :: T) :: Ordering\r\ntype instance Compare TT = Compare TT\r\n\r\ntype Compare' a = Compare a\r\n}}}\r\n\r\nWe can cause an internal GHC error as follows:\r\n\r\n{{{\r\n$ rm *.o *.hi\r\n$ ghc B.hs\r\n[1 of 2] Compiling A ( A.hs, A.o )\r\n[2 of 2] Compiling B ( B.hs, B.o )\r\n$ sleep 1\r\n$ touch B.hs\r\n$ ghc B.hs\r\n[2 of 2] Compiling B ( B.hs, B.o )\r\n\r\nB.hs:11:19:\r\n GHC internal error: `Compare' is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [(a9R, AThing k_a9U)]\r\n In the type `Compare a'\r\n In the type synonym declaration for Compare'\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->7.4.2Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/5772Failed kind inference in class declaration (regression error)2019-07-07T18:53:40ZRichard Eisenbergrae@richarde.devFailed kind inference in class declaration (regression error)Consider the following code:
```
{-# LANGUAGE MultiParamTypeClasses
#-}
class Foo a b
class Foo a b => Bar a b where
baz :: a b
```
This compiles fine in 7.2.1 but fails in 7.4.1-rc1, with the following error:
```
Sandbox.hs:7:...Consider the following code:
```
{-# LANGUAGE MultiParamTypeClasses
#-}
class Foo a b
class Foo a b => Bar a b where
baz :: a b
```
This compiles fine in 7.2.1 but fails in 7.4.1-rc1, with the following error:
```
Sandbox.hs:7:12:
`a' is applied to too many type arguments
In the type `a b'
In the class declaration for `Bar'
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.4.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":"Failed kind inference in class declaration (regression error)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1-rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following code:\r\n\r\n{{{\r\n{-# LANGUAGE MultiParamTypeClasses\r\n #-}\r\n\r\nclass Foo a b\r\n\r\nclass Foo a b => Bar a b where\r\n baz :: a b\r\n}}}\r\n\r\nThis compiles fine in 7.2.1 but fails in 7.4.1-rc1, with the following error:\r\n\r\n{{{\r\nSandbox.hs:7:12:\r\n `a' is applied to too many type arguments\r\n In the type `a b'\r\n In the class declaration for `Bar'\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->