GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2021-02-15T03:51:51Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/13655Spurious untouchable type variable in connection with rank-2 type and constra...2021-02-15T03:51:51ZWolfgang JeltschSpurious untouchable type variable in connection with rank-2 type and constraint familyThe following code cannot be compiled:
```hs
{-# LANGUAGE ConstraintKinds, Rank2Types, TypeFamilies #-}
import GHC.Exts (Constraint)
type family F a b :: Constraint
data T b c = T
f :: (forall b . F a b => T b c) -> a
f _ = undefine...The following code cannot be compiled:
```hs
{-# LANGUAGE ConstraintKinds, Rank2Types, TypeFamilies #-}
import GHC.Exts (Constraint)
type family F a b :: Constraint
data T b c = T
f :: (forall b . F a b => T b c) -> a
f _ = undefined
```
GHC outputs the following error message:
```
Untouchable.hs:9:6: error:
• Couldn't match type ‘c0’ with ‘c’
‘c0’ is untouchable
inside the constraints: F a b
bound by the type signature for:
f :: F a b => T b c0
at Untouchable.hs:9:6-37
‘c’ is a rigid type variable bound by
the type signature for:
f :: forall a c. (forall b. F a b => T b c) -> a
at Untouchable.hs:9:6
Expected type: T b c0
Actual type: T b c
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
f :: (forall b. F a b => T b c) -> a
```
<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":"Spurious untouchable type variable in connection with rank-2 type and constraint family","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":"The following code cannot be compiled:\r\n{{{#!hs\r\n{-# LANGUAGE ConstraintKinds, Rank2Types, TypeFamilies #-}\r\n\r\nimport GHC.Exts (Constraint)\r\n\r\ntype family F a b :: Constraint\r\n\r\ndata T b c = T\r\n\r\nf :: (forall b . F a b => T b c) -> a\r\nf _ = undefined\r\n}}}\r\nGHC outputs the following error message:\r\n{{{\r\nUntouchable.hs:9:6: error:\r\n • Couldn't match type ‘c0’ with ‘c’\r\n ‘c0’ is untouchable\r\n inside the constraints: F a b\r\n bound by the type signature for:\r\n f :: F a b => T b c0\r\n at Untouchable.hs:9:6-37\r\n ‘c’ is a rigid type variable bound by\r\n the type signature for:\r\n f :: forall a c. (forall b. F a b => T b c) -> a\r\n at Untouchable.hs:9:6\r\n Expected type: T b c0\r\n Actual type: T b c\r\n • In the ambiguity check for ‘f’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n In the type signature:\r\n f :: (forall b. F a b => T b c) -> a\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/24460Strange typechecking errors to do with Generics in a module with ANN and a ty...2024-02-27T15:12:18ZTeo CamarasuStrange typechecking errors to do with Generics in a module with ANN and a type error## Summary
This is a reproducer extracted from something we encountered in the wild.
Adding a new field to datatype led to a bunch of strange errors about `Generic`s.
In this minimal reproducer, the generics error is quite small, but i...## Summary
This is a reproducer extracted from something we encountered in the wild.
Adding a new field to datatype led to a bunch of strange errors about `Generic`s.
In this minimal reproducer, the generics error is quite small, but it becomes huge in any non-trivial example.
## Steps to reproduce
Compile the following module:
```
{-# LANGUAGE DeriveAnyClass #-}
module Repro where
import GHC.Generics
data IHaveNoFields = IHaveNoFields { } deriving (Generic)
getField
(IHaveNoFields field1 )
= field1
{-# ANN iHaveAnn ("" :: String) #-}
iHaveAnn = undefined
```
Here is the output:
```
Repro.hs:5:50: error:
• Couldn't match type: Rep IHaveNoFields
with: M1 i0 c0 (M1 i1 c1 U1)
Expected: Rep IHaveNoFields x
Actual: M1 i0 c0 (M1 i1 c1 U1) x
• In the expression: M1 (case x of IHaveNoFields -> M1 U1)
In an equation for ‘from’:
from x = M1 (case x of IHaveNoFields -> M1 U1)
When typechecking the code for ‘from’
in a derived instance for ‘Generic IHaveNoFields’:
To see the code I am typechecking, use -ddump-deriv
In the instance declaration for ‘Generic IHaveNoFields’
|
5 | data IHaveNoFields = IHaveNoFields { } deriving (Generic)
| ^^^^^^^
Repro.hs:5:50: error:
• Couldn't match type: Rep IHaveNoFields
with: M1 i2 c2 (M1 i3 c3 U1)
Expected: Rep IHaveNoFields x
Actual: M1 i2 c2 (M1 i3 c3 U1) x
• In the pattern: M1 x
In an equation for ‘to’:
to (M1 x) = case x of (M1 U1) -> IHaveNoFields
When typechecking the code for ‘to’
in a derived instance for ‘Generic IHaveNoFields’:
To see the code I am typechecking, use -ddump-deriv
In the instance declaration for ‘Generic IHaveNoFields’
|
5 | data IHaveNoFields = IHaveNoFields { } deriving (Generic)
| ^^^^^^^
Repro.hs:8:4: error:
• The constructor ‘IHaveNoFields’ should have no arguments, but has been given 1
• In the pattern: IHaveNoFields field1
In an equation for ‘getField’:
getField (IHaveNoFields field1) = field1
|
8 | (IHaveNoFields field1 )
|
```
## Expected behavior
This should error but should only output:
And indeed this is what we get if we comment out the `ANN` line.
```
Repro.hs:8:4: error:
• The constructor ‘IHaveNoFields’ should have no arguments, but has been given 1
• In the pattern: IHaveNoFields field1
In an equation for ‘getField’:
getField (IHaveNoFields field1) = field1
|
8 | (IHaveNoFields field1 )
| ^^^^^^^^^^^^^^^^^^^^
```
## Environment
* GHC version used: 9.4.8, 9.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/14319Stuck type families can lead to lousy error messages2020-01-23T19:27:40ZDavid FeuerStuck type families can lead to lousy error messagesI first noticed this problem at the type level:
```hs
{-# language TypeFamilies, TypeInType, ScopedTypeVariables #-}
module ArityError where
import Data.Kind
import GHC.TypeLits
import Data.Proxy
type family F (s :: Symbol) :: Type
ty...I first noticed this problem at the type level:
```hs
{-# language TypeFamilies, TypeInType, ScopedTypeVariables #-}
module ArityError where
import Data.Kind
import GHC.TypeLits
import Data.Proxy
type family F (s :: Symbol) :: Type
type family G (s :: Symbol) :: F s
type instance G "Hi" = Maybe
```
This produces the error message
```hs
ArityError.hs:10:24: error:
• Expecting one more argument to ‘Maybe’
Expected kind ‘F "Hi"’, but ‘Maybe’ has kind ‘* -> *’
• In the type ‘Maybe’
In the type instance declaration for ‘G’
|
10 | type instance G "Hi" = Maybe
| ^^^^^
```
This looks utterly bogus: `F "Hi"` is stuck, so we have no idea what arity it indicates.
----
I just realized we have a similar problem at the term level:
```hs
f :: forall (s :: Symbol). Proxy s -> F s
f _ _ = undefined
```
produces
```hs
ArityError.hs:14:1: error:
• Couldn't match expected type ‘F s’ with actual type ‘p0 -> a0’
The type variables ‘p0’, ‘a0’ are ambiguous
• The equation(s) for ‘f’ have two arguments,
but its type ‘Proxy s -> F s’ has only one
• Relevant bindings include
f :: Proxy s -> F s (bound at ArityError.hs:14:1)
|
14 | f _ _ = undefined
| ^^^^^^^^^^^^^^^^^
```
The claim that `Proxy s -> F s` has only one argument is bogus; we only know that it has *at least* one argument. The fix (I imagine) is to refrain from reporting arity errors when we don't know enough about the relevant arities.https://gitlab.haskell.org/ghc/ghc/-/issues/18413Suboptimal constraint solving2021-09-06T08:27:32ZSimon Peyton JonesSuboptimal constraint solvingHere a summary of `-ddump-tc-trace` for this program (part of test T12427a)
```
data T where
T1 :: a -> ((forall b. [b]->[b]) -> Int) -> T
h11 y = case y of T1 _ v -> v
```
I see this sequence
```
{co_awA} {0}:: ((forall b. [b] -> [...Here a summary of `-ddump-tc-trace` for this program (part of test T12427a)
```
data T where
T1 :: a -> ((forall b. [b]->[b]) -> Int) -> T
h11 y = case y of T1 _ v -> v
```
I see this sequence
```
{co_awA} {0}:: ((forall b. [b] -> [b]) -> Int)
~# p_awz[tau:1] (CNonCanonical)
==> Hetero equality gives rise to kind equality
inert: {co_awG} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int |> (TYPE {co_awF})_N)
work item: {co_awF} :: 'GHC.Types.LiftedRep ~# p_awy[tau:1]
co_awA := Sym ({co_awG} ; Sym (GRefl nominal ((forall b.[b] -> [b]) -> Int)
(TYPE {co_awF})_N))
==> Swap awF, kick out awG
work item: {co_awG} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int |> (TYPE {co_awF})_N)
inert (because p_awy is untouchable):
{co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
co_awF := Sym co_awH
==> flatten awG (strange double GRefl)
inert: {co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
inert: {co_awI} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int |> (TYPE (Sym {co_awH}))_N)
co_awG := {co_awI} ; (Sym (GRefl nominal ((forall b. [b] -> [b]) -> Int)
(TYPE (Sym {co_awH}))_N)
; GRefl nominal ((forall b. [b] -> [b]) -> Int)
(TYPE {co_awF})_N)
at this point we also make a derived shadow of awI, for some reason.
Solving stops here, but we float out awI, and awH, and then have another go
work: {co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
work: {co_awI} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int |> (TYPE (Sym {co_awH}))_N)
==> flatten awI (why?)
work: {co_awH} :: p_awy[tau:1] ~# 'GHC.Types.LiftedRep
inert: {co_awJ} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int |> (TYPE (Sym {co_awH}))_N)
co_awI := {co_awJ} ; (Sym (GRefl nominal ((forall b. [b] -> [b]) -> Int)
(TYPE (Sym {co_awH}))_N) ; GRefl nominal ((forall b. [b] -> [b])
-> Int)
(TYPE (Sym {co_awH}))_N)
==> solve awH: p_awy := LiftedRep, kick out awJ
{co_awJ} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int |> (TYPE (Sym {co_awH}))_N)
==> flatten awJ
co_awJ := {co_awK} ; GRefl nominal ((forall b. [b] -> [b]) -> Int)
(TYPE (Sym {co_awH}))_N
{co_awK} :: p_awz[tau:1] ~# ((forall b. [b] -> [b]) -> Int)
```
This seems like we are doing too much work, esp the double GRefls. Why did awI get flattened?
It's not a disaster, but pretty heavy handed.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/6065Suggested type signature causes a type error (even though it appears correct)2019-07-07T18:52:21ZtvynrSuggested type signature causes a type error (even though it appears correct)The attached file, MWE.hs, contains an experiment attempting a rudimentary encoding of extensible ASTs in Haskell (without using compdata or a similar package relying upon OverlappingInstances and so forth). The definition of the upcast ...The attached file, MWE.hs, contains an experiment attempting a rudimentary encoding of extensible ASTs in Haskell (without using compdata or a similar package relying upon OverlappingInstances and so forth). The definition of the upcast function appears to be correct. Compiling without a type signature produces a warning and the suggestion to include a type signature. Including the suggested type signature (which appears to be the correct one) causes a type error.
<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 | zep_haskell_trac@bahj.com |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Suggested type signature causes a type error (even though it appears correct)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1","keywords":["forall","instance","signature","type","typeclass"],"differentials":[],"test_case":"","architecture":"","cc":["zep_haskell_trac@bahj.com"],"type":"Bug","description":"The attached file, MWE.hs, contains an experiment attempting a rudimentary encoding of extensible ASTs in Haskell (without using compdata or a similar package relying upon OverlappingInstances and so forth). The definition of the upcast function appears to be correct. Compiling without a type signature produces a warning and the suggestion to include a type signature. Including the suggested type signature (which appears to be the correct one) causes a type error.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12975Suggested type signature for a pattern synonym causes program to fail to type...2022-05-24T16:50:02ZOllie CharlesSuggested type signature for a pattern synonym causes program to fail to type checkTake the following program:
```hs
{-# LANGUAGE ViewPatterns, PatternSynonyms, RankNTypes, GADTs #-}
import Data.Typeable
data T where
MkT :: Typeable a => a -> T
pattern Cast a <- MkT (cast -> Just a)
```
When compiled with `-Wall...Take the following program:
```hs
{-# LANGUAGE ViewPatterns, PatternSynonyms, RankNTypes, GADTs #-}
import Data.Typeable
data T where
MkT :: Typeable a => a -> T
pattern Cast a <- MkT (cast -> Just a)
```
When compiled with `-Wall`, GHC rightly prompts about a missing signature on `Cast`:
```
Top-level binding with no type signature:
Cast :: forall b. Typeable b => forall a. Typeable a => b -> T
```
However, using this suggested type signature causes the program to fail to type check:
```hs
• Could not deduce (Typeable a0)
arising from the "provided" constraints claimed by
the signature of ‘Cast’
from the context: Typeable a
bound by a pattern with constructor:
MkT :: forall a. Typeable a => a -> T,
in a pattern synonym declaration
at ../foo.hs:9:19-38
In other words, a successful match on the pattern
MkT (cast -> Just a)
does not provide the constraint (Typeable a0)
The type variable ‘a0’ is ambiguous
• In the declaration for pattern synonym ‘Cast’
```
<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":"Suggested type signature for a pattern synonym causes program to fail to type check","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["patternsynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Take the following program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ViewPatterns, PatternSynonyms, RankNTypes, GADTs #-}\r\n\r\nimport Data.Typeable\r\n\r\ndata T where\r\n MkT :: Typeable a => a -> T\r\n\r\npattern Cast a <- MkT (cast -> Just a)\r\n}}}\r\n\r\nWhen compiled with `-Wall`, GHC rightly prompts about a missing signature on `Cast`:\r\n\r\n{{{\r\n Top-level binding with no type signature:\r\n Cast :: forall b. Typeable b => forall a. Typeable a => b -> T\r\n}}}\r\n\r\nHowever, using this suggested type signature causes the program to fail to type check:\r\n\r\n{{{#!hs\r\n • Could not deduce (Typeable a0)\r\n arising from the \"provided\" constraints claimed by\r\n the signature of ‘Cast’\r\n from the context: Typeable a\r\n bound by a pattern with constructor:\r\n MkT :: forall a. Typeable a => a -> T,\r\n in a pattern synonym declaration\r\n at ../foo.hs:9:19-38\r\n In other words, a successful match on the pattern\r\n MkT (cast -> Just a)\r\n does not provide the constraint (Typeable a0)\r\n The type variable ‘a0’ is ambiguous\r\n • In the declaration for pattern synonym ‘Cast’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/17679Superclass expansion fails in instance declaration2020-01-15T18:01:59ZRichard Eisenbergrae@richarde.devSuperclass expansion fails in instance declarationI'm sure I'm doing something very silly.
```hs
{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
module Bug where
class A a
class A a => B a
class A a => C a
instance B a => C a
```
GHC rejects, saying it can't prove `A a`, r...I'm sure I'm doing something very silly.
```hs
{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
module Bug where
class A a
class A a => B a
class A a => C a
instance B a => C a
```
GHC rejects, saying it can't prove `A a`, required in order to write the `C a` instance. But shouldn't my `B a` constraint imply `A a`?
Help?https://gitlab.haskell.org/ghc/ghc/-/issues/472Supertyping of classes2019-07-07T19:17:50ZnobodySupertyping of classessee
[Supertyping Suggestion for Haskell](http://repetae.net/john/recent/out/supertyping.html)
example:
```
class Num a <= Group a where
(+) :: a -> a -> a
negate :: a -> a
```
apart from multiple inheritance, it could work like thi...see
[Supertyping Suggestion for Haskell](http://repetae.net/john/recent/out/supertyping.html)
example:
```
class Num a <= Group a where
(+) :: a -> a -> a
negate :: a -> a
```
apart from multiple inheritance, it could work like this:
```
import Prelude hiding ((+),negate)
import qualified Prelude ((+),negate)
class Group a where
(+) :: a -> a -> a
negate :: a -> a
instance Num a => Group a where
(+) = (Prelude.+)
negate = Prelude.negate
```
- coeus_at_gmx_dehttps://gitlab.haskell.org/ghc/ghc/-/issues/10150Suppress orphan instance warning per instance2019-07-07T18:37:19ZEdward Z. YangSuppress orphan instance warning per instanceIn the same way we have overlapping/incoherent instance pragmas which can be applied on a per instance basis, it would be good to have a `-fno-warn-orphan-instance` pragma which can be applied on a per-instance basis.
Annoyingly, there ...In the same way we have overlapping/incoherent instance pragmas which can be applied on a per instance basis, it would be good to have a `-fno-warn-orphan-instance` pragma which can be applied on a per-instance basis.
Annoyingly, there is not an obvious syntax to use for this case, since SOP for a module with orphan instances is `{-# GHC_OPTIONS -fno-warn-orphans #-}`
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | low |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Suppress orphan instance warning per instance","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"In the same way we have overlapping/incoherent instance pragmas which can be applied on a per instance basis, it would be good to have a `-fno-warn-orphan-instance` pragma which can be applied on a per-instance basis.\r\n\r\nAnnoyingly, there is not an obvious syntax to use for this case, since SOP for a module with orphan instances is `{-# GHC_OPTIONS -fno-warn-orphans #-}`","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11369Suppress redundant-constraint warnings in case of empty classes2020-01-23T19:37:34ZHerbert Valerio Riedelhvr@gnu.orgSuppress redundant-constraint warnings in case of empty classesThe technique described in
http://www.well-typed.com/blog/2015/07/checked-exceptions/
makes use of a class without any methods, i.e.
```hs
class Throws e
```
However, this by definition results in redundant constraints, e.g.
```hs
r...The technique described in
http://www.well-typed.com/blog/2015/07/checked-exceptions/
makes use of a class without any methods, i.e.
```hs
class Throws e
```
However, this by definition results in redundant constraints, e.g.
```hs
readFoo :: Throws IOError => FilePath -> IO Foo
readFoo fn = {- ... -}
```
which GHC 8.0 warns about.
I propose to suppress warnings in case a class which has no methods is used as seemingly redundant constraint.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | bgamari, edsko |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Suppress redundant-constraint warnings in case of empty classes","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"simonpj"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["bgamari","edsko"],"type":"Bug","description":"The technique described in\r\n\r\nhttp://www.well-typed.com/blog/2015/07/checked-exceptions/\r\n\r\nmakes use of a class without any methods, i.e.\r\n\r\n{{{#!hs\r\nclass Throws e\r\n}}}\r\n\r\nHowever, this by definition results in redundant constraints, e.g.\r\n\r\n{{{#!hs\r\nreadFoo :: Throws IOError => FilePath -> IO Foo\r\nreadFoo fn = {- ... -}\r\n}}}\r\n\r\nwhich GHC 8.0 warns about.\r\n\r\nI propose to suppress warnings in case a class which has no methods is used as seemingly redundant constraint.","type_of_failure":"OtherFailure","blocking":[]} -->Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/15639Surprising failure combining QuantifiedConstraints with Coercible2019-07-07T18:03:38ZDavid FeuerSurprising failure combining QuantifiedConstraints with CoercibleI don't understand what's going wrong here.
```hs
-- Fishy.hs
{-# language RankNTypes, QuantifiedConstraints, RoleAnnotations #-}
module Fishy (Yeah, yeahCoercible) where
import Data.Coerce
data Yeah_ a = Yeah_ Int
newtype Yeah a = Yea...I don't understand what's going wrong here.
```hs
-- Fishy.hs
{-# language RankNTypes, QuantifiedConstraints, RoleAnnotations #-}
module Fishy (Yeah, yeahCoercible) where
import Data.Coerce
data Yeah_ a = Yeah_ Int
newtype Yeah a = Yeah (Yeah_ a)
type role Yeah representational
yeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) -> r
yeahCoercible r = r
-- Fishy2.hs
module Fishy2 where
import Fishy
import Data.Type.Coercion
import Data.Coerce
yeah :: Coercion [Yeah a] [Yeah b]
yeah = yeahCoercible Coercion
```
I get
```
Fishy2.hs:8:22: error:
• Couldn't match representation of type ‘a’ with that of ‘b’
arising from a use of ‘Coercion’
‘a’ is a rigid type variable bound by
the type signature for:
yeah :: forall a b. Coercion [Yeah a] [Yeah b]
at Fishy2.hs:7:1-34
‘b’ is a rigid type variable bound by
the type signature for:
yeah :: forall a b. Coercion [Yeah a] [Yeah b]
at Fishy2.hs:7:1-34
• In the first argument of ‘yeahCoercible’, namely ‘Coercion’
In the expression: yeahCoercible Coercion
In an equation for ‘yeah’: yeah = yeahCoercible Coercion
• Relevant bindings include
yeah :: Coercion [Yeah a] [Yeah b] (bound at Fishy2.hs:8:1)
|
8 | yeah = yeahCoercible Coercion
|
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.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":"Surprising failure combining QuantifiedConstraints with Coercible","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I don't understand what's going wrong here.\r\n\r\n{{{#!hs\r\n-- Fishy.hs\r\n{-# language RankNTypes, QuantifiedConstraints, RoleAnnotations #-}\r\nmodule Fishy (Yeah, yeahCoercible) where\r\nimport Data.Coerce\r\n\r\ndata Yeah_ a = Yeah_ Int\r\nnewtype Yeah a = Yeah (Yeah_ a)\r\ntype role Yeah representational\r\n\r\nyeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) -> r\r\nyeahCoercible r = r\r\n\r\n\r\n-- Fishy2.hs\r\n\r\nmodule Fishy2 where\r\n\r\nimport Fishy\r\nimport Data.Type.Coercion\r\nimport Data.Coerce\r\n\r\nyeah :: Coercion [Yeah a] [Yeah b]\r\nyeah = yeahCoercible Coercion\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nFishy2.hs:8:22: error:\r\n • Couldn't match representation of type ‘a’ with that of ‘b’\r\n arising from a use of ‘Coercion’\r\n ‘a’ is a rigid type variable bound by\r\n the type signature for:\r\n yeah :: forall a b. Coercion [Yeah a] [Yeah b]\r\n at Fishy2.hs:7:1-34\r\n ‘b’ is a rigid type variable bound by\r\n the type signature for:\r\n yeah :: forall a b. Coercion [Yeah a] [Yeah b]\r\n at Fishy2.hs:7:1-34\r\n • In the first argument of ‘yeahCoercible’, namely ‘Coercion’\r\n In the expression: yeahCoercible Coercion\r\n In an equation for ‘yeah’: yeah = yeahCoercible Coercion\r\n • Relevant bindings include\r\n yeah :: Coercion [Yeah a] [Yeah b] (bound at Fishy2.hs:8:1)\r\n |\r\n8 | yeah = yeahCoercible Coercion\r\n |\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/19396Surprising lack of generalisation using MonoLocalBinds2024-03-16T18:34:37ZTom EllisSurprising lack of generalisation using MonoLocalBinds## Motivation
It seems to me that `MonoLocalBinds` is too aggressive in avoiding generalisation. Please observe the example below. In `pFG1`, `pBD` is not generalised. The reason is roughly because `pBArg` does not have a monomorphic ...## Motivation
It seems to me that `MonoLocalBinds` is too aggressive in avoiding generalisation. Please observe the example below. In `pFG1`, `pBD` is not generalised. The reason is roughly because `pBArg` does not have a monomorphic type signature, and indeed providing one, as in `pFG2`, leads to a generalised definition.
But this seems too aggressive to me. In `pFG1` the type of `pBArg` *is* known and monomorphic. Its type occurs in the type signature of `pFG1`! Could we generalise `pBD` in this case?
This is a simplified and anonymised version of real word code. This really does happen. The cause puzzled me and I'm an experienced Haskell user. I feel bad for a less experienced colleague who might try something similar but would receive a type error for code which seems like it really ought to type check.
## Proposal
Extend [the definition of "closed"](https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/let_generalisation.html) to encompass lambda bound variables whose type, from the explicit type signature of the lambda, is known and contains no free type variables.
## Notes
This issue was [discussed between @tomjaguarpaw1 and @rae on Haskell-Cafe](https://mail.haskell.org/pipermail/haskell-cafe/2021-February/133381.html).
I have included `pFG3` for *information only* in case anyone is curious what happens in the polymorphic case. They don't work even with an explicit type signature.
## Example
```haskell
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
-- This code came up in the context of writing a parser, but that's
-- not terribly important
import Prelude hiding ((<$>))
data B = B
data D f = GF AP f
| DF AM f
data AM = AM
data AP = AP
pB :: Parser B
pB = Parser
-- Does not type check
pFG1 :: Parser B -> Parser (D B)
pFG1 pBArg = pBD GF AP <|> pBD DF AM
where pBD f p = f p <$> pBArg
-- Does type check
pFG2 :: Parser B -> Parser (D B)
pFG2 pBArg = pBD GF AP <|> pBD DF AM
where pBArg' :: Parser B
pBArg' = pBArg
pBD f p = f p <$> pBArg'
-- Does not type check
pFG3 :: forall b. Parser b -> Parser (D b)
pFG3 pBArg = pBD GF AP <|> pBD DF AM
where pBArg' :: Parser b
pBArg' = pBArg
pBD f p = f p <$> pBArg'
-- The specifics of the parser don't matter
data Parser a = Parser
(<|>) :: Parser a -> Parser a -> Parser a
(<|>) _ _ = Parser
(<$>) :: (a -> b) -> Parser a -> Parser b
(<$>) _ _ = Parser
```https://gitlab.haskell.org/ghc/ghc/-/issues/23333Swapping arguments of type comparison operator ~ induces a type error2023-09-13T12:23:20ZMikolaj KonarskiSwapping arguments of type comparison operator ~ induces a type error## Summary
Edit2: see later comments for an even smaller repro.
Edit: a minimal repro is at https://play.haskell.org/saved/EtiAllWh (uncomment the bit swapping `~` arguments to make it fail)
The following commit, swapping arguments of...## Summary
Edit2: see later comments for an even smaller repro.
Edit: a minimal repro is at https://play.haskell.org/saved/EtiAllWh (uncomment the bit swapping `~` arguments to make it fail)
The following commit, swapping arguments of an application of the type comparison operator `~` induces, a type error. No plugins are used in this file.
https://github.com/Mikolaj/horde-ad/commit/3905cf0515ce5ce2723b4b0140184e4c8dcc9599
## Steps to reproduce
Compile with and without this commit, using `cabal build -j1` (for GHC 9.6 add `--allow-newer`). It should compile fine without the commit and with it it should fail emitting
```
simplified/HordeAd/Core/AstInterpret.hs:200:16: error: [GHC-05617]
• Could not deduce ‘BooleanOf (Ranked (Primal a) n)
~ BooleanOf (IntOf a)’
from the context: InterpretAst a
bound by the type signature for:
interpretAstBool :: forall a.
InterpretAst a =>
AstEnv a
-> AstMemo a
-> AstBool (ScalarOf a)
-> (AstMemo a, BooleanOf (Primal a))
at simplified/HordeAd/Core/AstInterpret.hs:(190,1)-(192,77)
Expected: BooleanOf (Primal a)
Actual: BooleanOf (Ranked (Primal a) n)
NB: ‘BooleanOf’ is a non-injective type family
• In the expression: interpretAstRelOp opCodeRel args2
In the expression: (memo2, interpretAstRelOp opCodeRel args2)
In the expression:
let (memo2, args2) = mapAccumR (interpretAstPrimal env) memo args
in (memo2, interpretAstRelOp opCodeRel args2)
• Relevant bindings include
memo2 :: AstMemo a
(bound at simplified/HordeAd/Core/AstInterpret.hs:199:10)
args2 :: [Ranked (Primal a) n]
(bound at simplified/HordeAd/Core/AstInterpret.hs:199:17)
args :: [AstPrimalPart n (ScalarOf a)]
(bound at simplified/HordeAd/Core/AstInterpret.hs:198:20)
memo :: AstMemo a
(bound at simplified/HordeAd/Core/AstInterpret.hs:193:22)
env :: AstEnv a
(bound at simplified/HordeAd/Core/AstInterpret.hs:193:18)
interpretAstBool :: AstEnv a
-> AstMemo a
-> AstBool (ScalarOf a)
-> (AstMemo a, BooleanOf (Primal a))
(bound at simplified/HordeAd/Core/AstInterpret.hs:193:1)
|
200 | in (memo2, interpretAstRelOp opCodeRel args2)
```
## Expected behavior
Compiles both with and without the commit.
## Environment
* GHC version used: 9.4.5 and 9.6.1
BTW, a different version of this code, one that does not require `QuantifiedConstraints` and has `forall`s in a very different place, is similarly fragile (flip argumenta in both `BooleanOf (IntOf a) ~ BooleanOf (Ranked (Primal a) n)` to make it fail): https://github.com/Mikolaj/horde-ad/blob/f40c4706657b80e8326468bb299456d319cce325/simplified/HordeAd/Core/AstInterpret.hs#L102-L1229.6.2https://gitlab.haskell.org/ghc/ghc/-/issues/20805Take a Quick Look at lists2021-12-22T14:05:05ZRichard Eisenbergrae@richarde.devTake a Quick Look at listsI want to make a video about Quick Look. But I also want it to have more content than just the venerable `head ids`. So I thought a bit about what would make a nice use case for impredicative polymorphism. I came up with the idea of usin...I want to make a video about Quick Look. But I also want it to have more content than just the venerable `head ids`. So I thought a bit about what would make a nice use case for impredicative polymorphism. I came up with the idea of using `forall a. Tree a -> Maybe a` as the type of indices into a tree structure. I could now search in one tree for a value that satisfies a predicate returning a `forall a. Tree a -> Maybe a` to then retrieve a corresponding value (if the tree has the right shape) in another tree. Here is the code:
```hs
data Tree a
= Leaf a
| Node (Tree a) a (Tree a)
deriving (Show, Functor)
type TreeIndex = forall a. Tree a -> Maybe a
lookupTree :: forall a. (a -> Bool) -> Tree a -> Maybe TreeIndex
lookupTree p = go
where
go :: Tree a -> Maybe TreeIndex
go (Leaf x)
| p x = Just (\case Leaf y -> Just y
Node _ y _ -> Just y)
| otherwise = Nothing
go (Node left x right)
| p x = Just (\case Leaf y -> Just y
Node _ y _ -> Just y)
| otherwise = asum [go left, go right] -- (go left : go right : [])
```
(This doesn't work, as written, because the last line just returns the `TreeIndex` from the recursive call. But never mind this.)
(NB to GHC aficionados: `asum` is the same as GHC's `firstJusts`.)
What's sad is that the last line fails to type-check. However, if I remove the list argument and replace it with the commented-out cons-and-nil argument, all is well. This is because GHC doesn't take a Quick Look at lists. But it really should. And probably tuples, too.https://gitlab.haskell.org/ghc/ghc/-/issues/23207Taking too much and Memory overflow while compiling2023-04-19T21:57:44ZAbdul HananTaking too much and Memory overflow while compiling## Summary
I am currently using GHC version 9.4.2 in conjunction with a Haskell program that appears to be experiencing difficulties compiling, potentially due to its non-deterministic nature. Despite my efforts, the program has been co...## Summary
I am currently using GHC version 9.4.2 in conjunction with a Haskell program that appears to be experiencing difficulties compiling, potentially due to its non-deterministic nature. Despite my efforts, the program has been consuming an extensive amount of time during compilation, leading to the termination of the process by the operating system. It is worth noting that my machine contains 16 GB of RAM and approximately 16 GB of swap memory.
The program in question is utilizing complex type-level operations. I have been using the following GHC options to facilitate the compilation process: `--ghc-options="-O0 -dshow-passes -fsimpl-tick-factor=0 -ddump-simpl`. However, it appears that the compiler has encountered an issue and is currently stuck at the "***Simplifier" stage. please note the memory consumption of Desugar stage (167.558621 GB) as well. after some time OS terminates the process stating that its taking too much momery.
```
*** Renamer/typechecker [Diurnum.Server]:
!!! Renamer/typechecker [Diurnum.Server]: finished in 68888.49 milliseconds, allocated 10161.548 megabytes
*** Desugar [Diurnum.Server]:
Result size of Desugar (before optimization)
= {terms: 37,569,
types: 1,016,600,
coercions: 209,765,050,
joins: 0/1,770}
Result size of Desugar (after optimization)
= {terms: 26,176,
types: 822,356,
coercions: 228,399,163,
joins: 0/264}
!!! Desugar [Diurnum.Server]: finished in 252049.07 milliseconds, allocated 167558.621 megabytes
*** Simplifier [Diurnum.Server]:
```
## Steps to reproduce[diurnum.zip](/uploads/5c9c378f7d04b7fde4c811ba930a19bf/diurnum.zip)
1. unzip it in Nixos
2. flake support for Nixos should be enabled
3. switch the git branch to `add-pagination-search-sort-in-list` --if not already in it.
4. nix develop
5. cabal run diurnum --ghc-options="-O0 -dshow-passes -fsimpl-tick-factor=0 -ddump-simpl"
## Expected behavior
The program should be compiled in minimal time and resources.
## Environment
NixOS with flake support
* GHC version used: 9.4.2
Optional:
* Operating System: NixOS
* System Architecture:x86https://gitlab.haskell.org/ghc/ghc/-/issues/24299`tc_infer_hs_type` doesn't add module finalisers2024-03-28T14:05:28ZAndrei Borzenkov`tc_infer_hs_type` doesn't add module finalisers## Summary
I investigated https://gitlab.haskell.org/ghc/ghc/-/issues/23639 and found that `tc_hs_type` calls `addModFinalizersWithLclEnv` on untyped top-level splices, but `tc_infer_hs_type` does not. I found this behavior to be strang...## Summary
I investigated https://gitlab.haskell.org/ghc/ghc/-/issues/23639 and found that `tc_hs_type` calls `addModFinalizersWithLclEnv` on untyped top-level splices, but `tc_infer_hs_type` does not. I found this behavior to be strange and is likely a bug. After some investigation, I came up with a test case that exhibits the problem. Luckily, the fix for this bug should be a one line change.
## Steps to reproduce
```haskell
{-# LANGUAGE TemplateHaskell #-}
module T where
import Language.Haskell.TH.Syntax (addModFinalizer, runIO)
import GHC.Types (Type)
type Proxy :: forall a. a -> Type
data Proxy a = MkProxy
check :: ($(addModFinalizer (runIO (putStrLn "check")) >>
[t| Proxy |]) :: Type -> Type) Int -- There is kind signature, we are in check mode
check = MkProxy
infer :: ($(addModFinalizer (runIO (putStrLn "infer")) >>
[t| Proxy |]) ) Int -- no kind signature, inference mode is enabled
infer = MkProxy
```
Attempt to compile this code will result in the following stdout:
```
$ ghc T.hs -fforce-recomp
[1 of 1] Compiling T ( T.hs, T.o )
check
```
## Expected behavior
```
$ ghc T.hs -fforce-recomp
[1 of 1] Compiling T ( T.hs, T.o )
check
infer
```
## Environment
* GHC version used: masterAndrei BorzenkovAndrei Borzenkovhttps://gitlab.haskell.org/ghc/ghc/-/issues/12034Template Haskell + hs-boot = Not in scope during type checking, but it passed...2019-07-07T18:27:54ZEdward Z. YangTemplate Haskell + hs-boot = Not in scope during type checking, but it passed the renamerI don't think this is a very harmful bug but it definitely is a bug. Consider:
```
-- A.hs-boot
module A where
data T
-- B.hs
module B (module A) where
import {-# SOURCE #-} A
-- A.hs
{-# LANGUAGE TemplateHaskell #-}
module A where
im...I don't think this is a very harmful bug but it definitely is a bug. Consider:
```
-- A.hs-boot
module A where
data T
-- B.hs
module B (module A) where
import {-# SOURCE #-} A
-- A.hs
{-# LANGUAGE TemplateHaskell #-}
module A where
import qualified B
import Language.Haskell.TH
f :: B.T -> B.T
f x = x
$( return [] )
data T = T B.T
```
The point of the splice is to convince GHC to typecheck `f :: B.T -> B.T` before it typechecks the type declaration. But this is not going to work, because `tcLookupGlobal` is going to bail if (1) T is not in the `tcg_type_env` and (2) T comes from this module.
It would be a simple matter to improve the error message but from a user's perspective, there is no good reason for this to not typecheck. On the implementation side, I am sympathetic to not letting this typecheck: if it does typecheck, then some `TyCon`s will incorrectly refer to the definition from the hs-boot file, rather than our local definition.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | low |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Template Haskell + hs-boot = Not in scope during type checking, but it passed the renamer","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc2","keywords":["backpack"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I don't think this is a very harmful bug but it definitely is a bug. Consider:\r\n\r\n{{{\r\n-- A.hs-boot\r\nmodule A where\r\ndata T\r\n\r\n-- B.hs\r\nmodule B (module A) where\r\nimport {-# SOURCE #-} A\r\n\r\n-- A.hs\r\n{-# LANGUAGE TemplateHaskell #-}\r\nmodule A where\r\nimport qualified B\r\nimport Language.Haskell.TH\r\nf :: B.T -> B.T\r\nf x = x\r\n$( return [] )\r\ndata T = T B.T\r\n}}}\r\n\r\nThe point of the splice is to convince GHC to typecheck `f :: B.T -> B.T` before it typechecks the type declaration. But this is not going to work, because `tcLookupGlobal` is going to bail if (1) T is not in the `tcg_type_env` and (2) T comes from this module.\r\n\r\nIt would be a simple matter to improve the error message but from a user's perspective, there is no good reason for this to not typecheck. On the implementation side, I am sympathetic to not letting this typecheck: if it does typecheck, then some `TyCon`s will incorrectly refer to the definition from the hs-boot file, rather than our local definition.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/24022The documented FlexibleInstances grammar is incorrect and also out of date2023-10-03T17:19:23ZMarioThe documented FlexibleInstances grammar is incorrect and also out of date## Summary
The GHC User's Guide contains a simplified formal grammar of `instance` declarations in presence of `FlexibleInstances`:
https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/instances.html#formal-syntax-for-instanc...## Summary
The GHC User's Guide contains a simplified formal grammar of `instance` declarations in presence of `FlexibleInstances`:
https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/instances.html#formal-syntax-for-instance-declaration-types
The left-hand side of the production
```
arg_type ::= <empty>
| arg_type arg_types
```
therein is erroneous, it should be defining `arg_types` (plural) instead.
Another problem is that the grammar is out of date in that it doesn't allow type applications in instance head. This is legal nowadays:
```
type C :: forall k. k -> Constraint
class C a
instance C @Type Int
```
## Proposed improvements or changes
The missing letter `s` should definitely be inserted.
As for the type applications in instance heads, they should should be documented *somewhere*. I don't see them mentioned in the `TypeApplications` section. I'm not sure if the above-mentioned grammar is meant to showcase the full syntax of `instance` declarations with all extensions enabled, or only what `FlexibleInstances` brings. In the former case it should be extended with type applications, in the latter it doesn't need the infix operator case nor multiple class parameters.Ben GamariBen Gamarihttps://gitlab.haskell.org/ghc/ghc/-/issues/19559The GHCi debugger loses type constraints2022-01-20T10:27:34ZRoland SennThe GHCi debugger loses type constraints## Summary
The GHCi debugger loses the type constraints of the breakpoint variables..
## Steps to reproduce
`Foo.hs` is a simplified version of testcase `break012`:
````
foo :: (Num a1, Num a2) => a2 -> (a2, a1 -> a1 -> a1)
foo i = l...## Summary
The GHCi debugger loses the type constraints of the breakpoint variables..
## Steps to reproduce
`Foo.hs` is a simplified version of testcase `break012`:
````
foo :: (Num a1, Num a2) => a2 -> (a2, a1 -> a1 -> a1)
foo i = let incr = i + 1
add = (+)
in (incr,add)
````
Observe the following GHCi session:
````
$ ghci Foo.hs
GHCi, version 9.0.1: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( Foo.hs, interpreted )
Ok, one module loaded.
ghci> :st foo 5 `seq` ()
Stopped in Main.foo, Foo.hs:4:12-21
_result :: (a2, a1 -> a1 -> a1) = _
add :: a1 -> a1 -> a1 = _
incr :: a2 = _
[Foo.hs:4:12-21] ghci> add 40 2
<interactive>:2:5: error:
• No instance for (Num a1) arising from the literal ‘40’
Cannot resolve unknown runtime type ‘a1’
Use :print or :force to determine these types
Relevant bindings include it :: a1 (bound at <interactive>:2:1)
These potential instances exist:
instance Num Integer -- Defined in ‘GHC.Num’
instance Num Double -- Defined in ‘GHC.Float’
instance Num Float -- Defined in ‘GHC.Float’
...plus two others
...plus one instance involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the first argument of ‘add’, namely ‘40’
In the expression: add 40 2
In an equation for ‘it’: it = add 40 2
[Foo.hs:4:12-21] ghci>
````
The types of all breakpoint variables lack `Num` contraints!
## Expected behavior
The types of the 2 breakpoint variables (`_result`, `add`) should have a `Num` constraint for `a1`.
The type of `incr` should be `Integer`. The correct types are:
````
_result :: Num a1 => Integer -> (Integer, a1 -> a1 -> a1) = _
add :: Num a1 => a1 -> a1 -> a1 = _
incr :: Integer = _
````
The result of `add 40 2` should be `42` and not an error message.
## Environment
* GHC versions used: 7.10.3, 8.10.2, 9.0.1, HEAD
(in 7.10.3 only the `_result` breakpoint variable is shown)
* Operating System: Linux Debian 10
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc/-/issues/21502The hint to add missing context to the type signature is not produced by GHC ...2022-05-06T07:26:20ZSergey VinokurovThe hint to add missing context to the type signature is not produced by GHC when using non-trivial constraint## Intro
When a user didn't specify typeclass constraints for all variables in a function signature the GHC sometimes suggests to add relevant constraint to the signature, like this:
```
• No instance for (Foo a) arising from a use...## Intro
When a user didn't specify typeclass constraints for all variables in a function signature the GHC sometimes suggests to add relevant constraint to the signature, like this:
```
• No instance for (Foo a) arising from a use of ‘foo’
Possible fix:
add (Foo a) to the context of
the type signature for:
bar :: forall a. a -> Sum a
```
However if the constraint is a "non-trivial" one, in particular if it uses multiparameter typeclass and some of the parameters not variables then the suggestion is not produced. My expectation is that suggestion should be produced.
A bit of context, the Haskell Language Server uses GHC's error messages to suggest fixes. When error message contains the `Possible fix` similar to the one shows before then in can add the constraint to the type signature automatically as a code action. But if the suggestion is missing then it's just not possible. It appears that only GHC has all the necessary info regarding whether to produce `Possible fix` or not so the issue cannot be worked around in HLS (nor should it be since GHC's error messages are useful even for users that don't use HLS).
## Specific cases
For the following program the suggestion is not produced:
```haskell
{-# LANGUAGE MultiParamTypeClasses #-}
import Data.Kind
import Data.Monoid
class Foo (a :: Type) (b :: Type) where
foo :: Monoid m => (a -> m) -> b -> m
bar :: a -> Sum Int
bar x = foo Sum x
```
```
/tmp/test2.hs:10:9: error:
• No instance for (Foo Int a) arising from a use of ‘foo’
• In the expression: foo Sum x
In an equation for ‘bar’: bar x = foo Sum x
|
10 | bar x = foo Sum x
| ^^^
```
But for a slightly simpler program the suggestion is present
```haskell
{-# LANGUAGE MultiParamTypeClasses #-}
import Data.Kind
import Data.Monoid
class Foo (a :: Type) where
foo :: Monoid m => (a -> m) -> a -> m
bar :: a -> Sum a
bar x = foo Sum x
```
```
/tmp/test2.hs:10:9: error:
• No instance for (Foo a) arising from a use of ‘foo’
Possible fix:
add (Foo a) to the context of
the type signature for:
bar :: forall a. a -> Sum a
• In the expression: foo Sum x
In an equation for ‘bar’: bar x = foo Sum x
|
10 | bar x = foo Sum x
| ^^^
```
## A bit of investigation
I found out that call to `isTyVarClassPred` at https://gitlab.haskell.org/ghc/ghc/-/blob/master/compiler/GHC/Tc/Errors/Ppr.hs#L2844 is responsible for GHC's decision to omit the suggestion. The call appears to check that typeclass is only applied to variables and thus fails for a constraint like `Foo Int a` which has constants mixed in.
Perhaps the check should be relaxed to require that constraint to be suggested has some variables in its parameters? Or maybe the check shouldn't be performed at all (not really sure about this one though)?
One thing to probably watch out for is that the variable can occur as part of some other type in the constraint as illustrated by following modification to the program
```haskell
{-# LANGUAGE MultiParamTypeClasses #-}
import Data.Kind
import Data.Monoid
class Foo (a :: Type) (b :: Type) where
foo :: Monoid m => (a -> m) -> b -> m
newtype Quux a = Quux { unQuux :: a }
bar :: a -> Sum Int
bar x = foo Sum (Quux x)
```
```
/tmp/test2.hs:12:9: error:
• No instance for (Foo Int (Quux a)) arising from a use of ‘foo’
• In the expression: foo Sum (Quux x)
In an equation for ‘bar’: bar x = foo Sum (Quux x)
|
12 | bar x = foo Sum (Quux x)
| ^^^
```
NB if I just omit the call to `isTyVarClassPred` the patched ghc produces the error message I was expecting all along:
```
• No instance for (Foo Int (Quux a)) arising from a use of ‘foo’
Possible fix:
add (Foo Int (Quux a)) to the context of
the type signature for:
bar :: forall a. a -> Sum Int
• In the expression: foo Sum (Quux x)
In an equation for ‘bar’: bar x = foo Sum (Quux x)
|
12 | bar x = foo Sum (Quux x)
| ^^^
```
## Environment
* GHC version used: 9.2.2, HEAD
Optional:
* Operating System: Linux
* System Architecture: x86_64