GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-04-02T20:27:10Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/22912Introduce a warning for possibly loopy superclass solve2023-04-02T20:27:10Zsheafsam.derbyshire@gmail.comIntroduce a warning for possibly loopy superclass solveIn https://gitlab.haskell.org/ghc/ghc/-/issues/20666#note_479125, @simonpj suggests a mechanism which would allow us to provide a deprecation period for the changes introduced by MR !7050. These changes are necessary to avoid constructin...In https://gitlab.haskell.org/ghc/ghc/-/issues/20666#note_479125, @simonpj suggests a mechanism which would allow us to provide a deprecation period for the changes introduced by MR !7050. These changes are necessary to avoid constructing non-terminating class dictionaries, as explained in `Note [Recursive superclasses]` in `GHC.Tc.TyCl.Instance`, but can be counter-intuitive to users and cause breakage to their libraries. So it seems more prudent to introduce a flag, on by default, which temporarily allows this prohibited superclass solving mechanism but emits a loud warning whenever this happens, suggesting that the user fix the code and turn off the flag.
These tickets are examples of the breakage that immediate adoption caused:
* #22891
* #20666
* #22894
* #22905
* #11762
* #114279.6.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/22911Kind equality should be part of `checkEqType`2023-03-30T07:14:37ZSimon Peyton JonesKind equality should be part of `checkEqType`The function `GHC.Tc.Utils.checkEqType` checks the invariants demanded of a canonical equality constraint, and reports which ones do not hold. Alas, it omits one very important one: checking that
```
typeKind t1 `eqType` typeKind t2
...The function `GHC.Tc.Utils.checkEqType` checks the invariants demanded of a canonical equality constraint, and reports which ones do not hold. Alas, it omits one very important one: checking that
```
typeKind t1 `eqType` typeKind t2
```
This ticket is to propose that we move that test into `checkEqType`.
In the call from `GHC.Tc.Utils.Unify` that would be a nice improvement. But in `GHC.Tc.Solver.Canonical` we check for the kind-inhomogenity` rather early, and it's not immediately obvious to me how to refactor. And yet it would clearly be a Good Thing to do so.
@rae: any opinions?https://gitlab.haskell.org/ghc/ghc/-/issues/22908too eager constraint simplification(?) for nullary type classes without exist...2023-10-12T15:54:29ZBertram Felgenhauertoo eager constraint simplification(?) for nullary type classes without existing instance## Summary
Type inference involving nullary classes without any instance is too eager.
## Steps to reproduce
Consider the following interaction with `ghci`:
```
ghci> :set -XMultiParamTypeClasses
ghci> class Foo where foo :: Int
ghc...## Summary
Type inference involving nullary classes without any instance is too eager.
## Steps to reproduce
Consider the following interaction with `ghci`:
```
ghci> :set -XMultiParamTypeClasses
ghci> class Foo where foo :: Int
ghci> :t foo -- expected: foo :: Foo => Int
<interactive>:1:1: error:
• No instance for Foo arising from a use of ‘foo’
• In the expression: foo
ghci> bar () = foo -- expected to work without type signature
<interactive>:4:10: error:
• No instance for Foo arising from a use of ‘foo’
• In the expression: foo
In an equation for ‘bar’: bar () = foo
ghci> bar :: Foo => () -> Int; bar () = foo
```
or the following module which fails to compile:
```
{-# LANGUAGE MultiParamTypeClasses #-}
class Foo where foo :: Int
-- bar :: Foo => () -> Int
bar () = foo
{-
[1 of 2] Compiling Main ( Foo.hs, Foo.o )
Foo.hs:6:10: error:
• No instance for Foo arising from a use of ‘foo’
• In the expression: foo
In an equation for ‘bar’: bar () = foo
|
6 | bar () = foo
| ^^^
-}
```
These examples start working once an instance for `Foo` is provided.
## Expected behavior
I expected GHC to infer types of the shape `Foo => ...` rather than producing type errors.
## Environment
* GHC version used: 9.4.2https://gitlab.haskell.org/ghc/ghc/-/issues/22899type-checking regression in 9.6.1-alpha2 - interaction between ApplicativeDo ...2023-02-07T16:33:08ZGanesh Sittampalamtype-checking regression in 9.6.1-alpha2 - interaction between ApplicativeDo and polymorphic arguments?## Summary
There's a compilation regression between GHC 9.4.3 and GHC 9.6.1-alpha2 which seems to be some interaction between `ApplicativeDo` and polymorphic arguments.
Cut down example below, which compiles in GHC 9.4.3 but fails in 9...## Summary
There's a compilation regression between GHC 9.4.3 and GHC 9.6.1-alpha2 which seems to be some interaction between `ApplicativeDo` and polymorphic arguments.
Cut down example below, which compiles in GHC 9.4.3 but fails in 9.6. It compiles fine in GHC 9.6 if I do any of:
- remove `ApplicativeDo`
- reorder the first two statements in the `do`
- remove the `pure ()`
- inline `go`.
It may be related to the `ApplicativeDo` desugaring itself as I've tried and failed to reproduce the regression with manually desugaring. I also later ran into another example of a regression in an applicative do block, this time with implicit parameters, that was also fixed by reorganising the code; I can also turn that into a test case if wanted.
Now that I understand the triggers I can probably work around it fairly easily in my real code, but I thought it may still be worth investigating as I can't spot any mention in [the migration guide](https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.6) or other issues.
## Steps to reproduce
```
{-# LANGUAGE ApplicativeDo #-}
module X where
x :: Maybe ()
x = do
pure ()
let go = Nothing
f go
f :: (forall p . Maybe p) -> Maybe ()
f _ = Nothing
```
With GHC 9.4.3 this compiles fine.
With GHC 9.6.0-alpha2 I get:
```
X.hs:8:5: error: [GHC-46956]
• Couldn't match type ‘a0’ with ‘p’
Expected: Maybe p
Actual: Maybe a0
because type variable ‘p’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context:
forall p. Maybe p
at X.hs:8:5-6
• In the first argument of ‘f’, namely ‘go’
In a stmt of a 'do' block: f go
In the expression:
do pure ()
let go = Nothing
f go
• Relevant bindings include go :: Maybe a0 (bound at X.hs:7:7)
|
8 | f go
| ^^
```
## Expected behavior
I'm not sure. Maybe it should work in GHC 9.6? Maybe my code is wrong and I just get lucky with earlier GHCs?
## Environment
* GHC version used: 9.6.1-alpha2sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/22891Regression in superclass inference between GHC 9.6.0 alpha1 and alpha22023-03-03T16:25:41ZBodigrimRegression in superclass inference between GHC 9.6.0 alpha1 and alpha2**See master ticket #22912**
```haskell
{-# LANGUAGE UndecidableInstances #-}
module Foo where
class Foo f
class Foo f => Bar f g
instance Bar f f => Bar f (h k)
```
This program used to compile with GHC 9.2, 9.4 and 9.6.0-alpha1, ...**See master ticket #22912**
```haskell
{-# LANGUAGE UndecidableInstances #-}
module Foo where
class Foo f
class Foo f => Bar f g
instance Bar f f => Bar f (h k)
```
This program used to compile with GHC 9.2, 9.4 and 9.6.0-alpha1, but suddenly stopped to compile with 9.6.0-alpha2, which now complains that
```
programs$ ghc-9.6.0.20230128 -fforce-recomp Foo.hs
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
Foo.hs:9:10: error: [GHC-39999]
• Could not deduce ‘Foo f’
arising from the superclasses of an instance declaration
from the context: Bar f f
bound by the instance declaration at Foo.hs:9:10-31
Possible fix:
add (Foo f) to the context of the instance declaration
• In the instance declaration for ‘Bar f (h k3)’
|
9 | instance Bar f f => Bar f (h k)
| ^^^^^^^^^^^^^^^^^^^^^^
```
Is this regression expected? [Release notes](https://gitlab.haskell.org/ghc/ghc/-/blob/master/docs/users_guide/9.6.1-notes.rst) are silent about it. [Migration guide](https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.6#superclass-expansion-is-more-conservative) mentions changes to superclass expansion involving type families (BTW this is missing from release notes), but there are no type families in my example and there is no suggestion of "Possible fix: If the constraint looks soluble from a superclass of the instance context, read 'Undecidable instances and loopy superclasses' in the user manual".
If this regression is still an expected consequence of #20666 / !7050, please include it in the release notes and amend migration guide, clarifying that regressions are not limited to superclasses involving type families. I suggest to use it instead the current example in the migration guide: this case is clearly much simpler (and much more surprising, if I may say). I would also expect to receive a suggestion to read "Undecidable instances and loopy superclasses", as the migration guide advertises.9.6.1Simon Peyton JonesRichard Eisenbergrae@richarde.devsheafsam.derbyshire@gmail.comSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/22828Reification of invisible type variable binders2023-10-12T11:24:50ZVladislav ZavialovReification of invisible type variable bindersConsider the following declaration:
```haskell
data P @k (a :: k) = MkP
```
Should `reify` return the `@k` binder or not? See the discussion at https://gitlab.haskell.org/ghc/ghc/-/merge_requests/9480#note_474879, cited below for comp...Consider the following declaration:
```haskell
data P @k (a :: k) = MkP
```
Should `reify` return the `@k` binder or not? See the discussion at https://gitlab.haskell.org/ghc/ghc/-/merge_requests/9480#note_474879, cited below for completeness.
**Ryan:**
This change makes me somewhat nervous. There is quite a bit of TH code in the wild that assumes that all of the `TyVarBndr`s in a reified type-level declaration are visible. I wouldn't be surprised if there was code that simply computed the `length` of the list of `TyVarBndr`s, and that sort of code would be subtly broken if there were any invisible binders that snuck in when upgrading GHC.
Granted, this is all somewhat speculative. I haven't actually tried building a substantial number of Hackage libraries with this patch, and for good reason: not even low-level dependencies like `th-abstraction` would compile with this patch. But the possibility of subtle breakage seems very real.
Here is a somewhat radical proposition: what if we didn't reify invisible binders at all? That might sound restrictive, but this is a restriction that Template Haskell already adheres to today. For instance, if you reify the type of `blah :: Proxy Int`, it will be reified as `Proxy Int`, not `Proxy @Type Int`. Omitting invisible binders would be consistent with this precedent, although I don't know if this precedent is something that was intentionally decided or simply an accident of how the implementation evolved.
**Vlad:**
This is a breaking change, yes, but I believe there are good reasons to make it. In the ascending order of importance:
1. The type of the reified binders is changed from `TyVarBndr ()` to `TyVarBndr BndrVis`, so there is a good chance that the breakage won't be silent.
2. Clients of `template-haskell` that don't care about invisible binders can easily filter them out *after* reification (this is something that `th-abstraction` could do, too). On the other hand, if we filtered out those binders during reification, then a client that needs those binders would be hard-pressed to reconstruct them.
3. [#425](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst#arity-inference) removes arity inference in favor of using `@k`-binders to control the arity. The presence or absence of a trailing `@k`-binder could then affect the arity of a type synonym or a type family:
```haskell
type F1 :: Type -> forall k. Maybe k
type family F1 a -- arity = 1
type F2 :: Type -> forall k. Maybe k
type family F2 a @k -- arity = 2
```
We probably shouldn't lose this information during reification, or else we may not be able to splice the reified declaration back in.
**Ryan:**
> 1. The type of the reified binders is changed from `TyVarBndr ()` to `TyVarBndr BndrVis`, so there is a good chance that the breakage won't be silent.
True, but I claim that the type change from `()` to `BndrVis` is a different kind of breakage from the one I am envisioning in https://gitlab.haskell.org/ghc/ghc/-/merge_requests/9480#note_474879. As one example, consider [this code in ](https://hackage-search.serokell.io/viewfile/aeson-2.1.1.0/src/Data/Aeson/TH.hs#line-1725)`aeson`, which calls `length` on a type family declaration's binders. Even if someone were to patch up all of the uses of `()` and replace them with `BndrVis`, it's quite possible that they'd overlook the call to `length` here, which is now computing a different quantity than before.
> 2. Clients of `template-haskell` that don't care about invisible binders can easily filter them out *after* reification (this is something that `th-abstraction` could do, too). On the other hand, if we filtered out those binders during reification, then a client that needs those binders would be hard-pressed to reconstruct them.
This is also true, but again, I claim that this reasoning applies just as much to *applying* types invisibly (e.g., reifying `Proxy Int` as `Proxy @Type Int`) as it does *abstracting* types invisibly (e.g., reifying `data D (a :: k)` as `data D @k (a :: k)`). I'm somewhat bothered by the lack of symmetry here.
> 3. [#425](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst#arity-inference) removes arity inference in favor of using `@k`-binders to control the arity. The presence or absence of a trailing `@k`-binder could then affect the arity of a type synonym or a type family:
>
> ```haskell
> type F1 :: Type -> forall k. Maybe k
> type family F1 a -- arity = 1
>
> type F2 :: Type -> forall k. Maybe k
> type family F2 a @k -- arity = 2
> ```
>
> We probably shouldn't lose this information during reification, or else we may not be able to splice the reified declaration back in.
Indeed, there are similar TH interactions with visible kind applications in today's GHC. Consider:
```haskell
type P :: forall k. Type
data P = MkP
f :: P @Bool
f = MkP
```
Template Haskell will reify the type of `f` as:
```
λ> putStrLn $(reify 'f >>= stringE . pprint)
Foo.f :: Foo.P
```
But this is more polymorphic than the actual definition of `f`!
I'm not sure what the right approach is here. One could make an argument that invisible type abstractions are less common than invisible type applications, so it's less invasive to reify the former but not the latter. And indeed, GHC already makes an attempt to insert extra kind annotations in various places when things would be otherwise ambiguous. For example, given this code:
```haskell
data P2 (a :: k) = MkP2
g :: P2 @Bool Any
g = MkP2
```
TH reifies `f` as:
```
λ> putStrLn $(reify 'g >>= stringE . pprint)
Foo.g :: Foo.P2 (GHC.Types.Any :: GHC.Types.Bool)
```
As shown in the `f` example above, however, TH doesn't always catch everything that could potentially be ambiguous. But perhaps that is something that could be improved.
In any case, it seems like we ought to come to a conclusion about TH's philosophy towards reifying invisible things. We could:
1. Reify invisible type binders, but not reify invisible type applications
2. Reify both invisible type binders and invisble type applications
3. Avoid reifying either of them
4. Something else?
We should spell out the choice that we make somewhere as a guiding design philosophy.
**Vlad:** Right. I agree that option (1) creates an inconsistency, so let's cross it off.
Short-term, let's go with option (3) to avoid breakage. I will revert reification of invisible binders in this patch. Long-term, option (2) seems more attractive to me, since it provides the clients of `template-haskell` with more information. It seems like The Right Thing to return this information instead of discarding it, but I understand that this is a weak argument unless I can back it with a concrete use case, which I do not have at the moment.9.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/22811Typechecking Failure When Going From Two “Forall”-quantified Variables to a S...2023-01-24T16:04:09ZNathaniel BurkeTypechecking Failure When Going From Two “Forall”-quantified Variables to a Single One (But Works Fine in Reverse)## Summary
GHC will accept converting from `forall (a :: Type) (b :: Type). Foo '(a, b)` to `forall (p :: (Type, Type)). Foo p` but not the other way around.
## Steps to reproduce
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-...## Summary
GHC will accept converting from `forall (a :: Type) (b :: Type). Foo '(a, b)` to `forall (p :: (Type, Type)). Foo p` but not the other way around.
## Steps to reproduce
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
import Data.Kind (Type)
data Foo :: (Type, Type) -> Type where
Foo :: forall p. Foo p
test1 :: forall p. Foo p
test1 = Foo
test2 :: forall a b. Foo '( a, b)
test2 = test1
test3 :: forall a b. Foo '( a, b)
test3 = Foo
-- Error here
test4 :: forall p. Foo p
test4 = test3
```
Trying to compile this code will output:
```
Test.hs:20:9: error:
* Couldn't match type `p' with '(a0, b0)
Expected: Foo p
Actual: Foo '(a0, b0)
`p' is a rigid type variable bound by
the type signature for:
test4 :: forall (p :: (*, *)). Foo p
at Test.hs:19:1-24
* In the expression: test3
In an equation for `test4': test4 = test3
* Relevant bindings include test4 :: Foo p (bound at Test.hs:20:1)
|
20 | test4 = test3
| ^^^^^
Failed, no modules loaded.
```
Explicitly annotating the kind of `p` like:
```hs
test4 :: forall (p :: (Type, Type)). Foo p
test4 = test3
```
does not help.
## Expected behavior
No compile error, definition of `test4` typechecks.
## Environment
* GHC version used: 9.4.4https://gitlab.haskell.org/ghc/ghc/-/issues/22793Type checker crash with some polykinded junk2023-03-04T07:32:24ZDavid FeuerType checker crash with some polykinded junk## Summary
I was doing something kind of impractical with quantified constraints
and such, and crashed the type checker. Fortunately (?) I was able to
reproduce the crash with a greatly stripped down example.
## Steps to reproduce
```...## Summary
I was doing something kind of impractical with quantified constraints
and such, and crashed the type checker. Fortunately (?) I was able to
reproduce the crash with a greatly stripped down example.
## Steps to reproduce
```haskell
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Buggle where
import Data.Kind
type Foo :: forall k. k -> k -> Constraint
class Foo s a
bob :: forall {k1} {ks} {ka} q (p :: k1 -> q -> Type) (f :: ka -> q) (s :: ks) (t :: ks) (a :: ka) (b :: ka). Foo s a => p a (f b) -> p s (f t)
bob f = undefined
```
When I compile this, I see no error messages, but also no compilation products. `-ddump-tc-trace` includes a bunch of call stacks for whatever reason. The first to come up:
```
newNoTcEvBinds unique = axp
attemptM recovering with insoluble constraints
WC {wc_impl =
Implic {
TcLevel = 1
Skolems =
Given-eqs = NoGivenEqs
Status = Unsolved
Given =
Wanted =
WC {wc_impl =
Implic {
TcLevel = 1
Skolems =
Given-eqs = NoGivenEqs
Status = Unsolved
Given =
Wanted =
WC {wc_impl =
Implic {
TcLevel = 2
Skolems = k1_auh[sk:2]
ks_aui[sk:2]
ka_auj[sk:2]
q_auk[sk:2]
(p_aul[sk:2] :: k1_auh[sk:2] -> q_auk[sk:2] -> *)
(f_aum[sk:2] :: ka_auj[sk:2] -> q_auk[sk:2])
(s_aun[sk:2] :: ks_aui[sk:2])
(t_auo[sk:2] :: ks_aui[sk:2])
(a_aup[sk:2] :: ka_auj[sk:2])
(b_auq[sk:2] :: ka_auj[sk:2])
Given-eqs = NoGivenEqs
Status = Unsolved
Given =
Wanted =
WC {wc_simple =
[W] hole{co_avp} {1;{{co_ave}}}:: ks_aui[sk:2]
GHC.Prim.~# k1_auh[sk:2] (CNonCanonical)
[W] hole{co_avt} {1;{{co_avp}}}:: ka_auj[sk:2]
GHC.Prim.~# k1_auh[sk:2] (CNonCanonical)}
Binds = CoEvBindsVar<avn>
an explicit forall {k1_auh} {ks_aui} {ka_auj} q_auk
(p_aul :: k1_auh -> q_auk -> Type)
(f_aum :: ka_auj -> q_auk) (s_aun :: ks_aui)
(t_auo :: ks_aui) (a_aup :: ka_auj)
(b_auq :: ka_auj) }}
Binds = CoEvBindsVar<axn>
the type signature for ‘bob’ }}
Binds = CoEvBindsVar<axp>
UnkSkol (please report this as a bug)
Call stack:
CallStack (from HasCallStack):
unkSkolAnon, called at compiler/GHC/Tc/Solver.hs:231:57 in ghc:GHC.Tc.Solver }}
```
## Expected behavior
I expect compilation to either succeed or produce an error message.
## Environment
* GHC version used: 9.4.4
Optional:
* Operating System:
* System Architecture:https://gitlab.haskell.org/ghc/ghc/-/issues/22742ghc panic: runtimeRepLevity_maybe2023-01-23T14:30:43ZVladislav Zavialovghc panic: runtimeRepLevity_maybe## Summary
An ill-typed program triggers a panic while printing an error message.
## Steps to reproduce
Compile this:
```haskell
module Bug where
import GHC.Exts (TYPE)
data T (a :: TYPE r) = MkT
f :: T @(f a b) () -> ()
f MkT = (...## Summary
An ill-typed program triggers a panic while printing an error message.
## Steps to reproduce
Compile this:
```haskell
module Bug where
import GHC.Exts (TYPE)
data T (a :: TYPE r) = MkT
f :: T @(f a b) () -> ()
f MkT = ()
```
GHC tries to print an error message (as can be seen from the error code `GHC-83865`) but then panics:
```
Bug.hs:7:17: error: [GHC-83865]ghc: panic! (the 'impossible' happened)
GHC version 9.7.20230110:
runtimeRepLevity_maybe
'BoxedRep
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:189:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Core/Type.hs:796:22 in ghc:GHC.Core.Type
```
## Expected behavior
A proper error message.
## Environment
* GHC version used: HEAD.Rinat Striungislazybonesxp@gmail.comRinat Striungislazybonesxp@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/22717Instance not transitively forwarded2023-04-18T18:14:53ZLemmingInstance not transitively forwarded## Summary
When compiling the tests of synthesizer-llvm/HEAD I get:
~~~~
testsuite/Test/Synthesizer/LLVM/Utility.hs:77:30: error:
• Couldn't match type ‘CausalClass.SignalOf
(CausalClass.ProcessOf Sig.T...## Summary
When compiling the tests of synthesizer-llvm/HEAD I get:
~~~~
testsuite/Test/Synthesizer/LLVM/Utility.hs:77:30: error:
• Couldn't match type ‘CausalClass.SignalOf
(CausalClass.ProcessOf Sig.T)’
with ‘Sig.T’
Expected: Sig.T (al, bl)
-> CausalClass.ProcessOf Sig.T () (MultiValue.T a, MultiValue.T b)
Actual: CausalClass.SignalOf
(CausalClass.ProcessOf Sig.T) (MultiValue.T a, MultiValue.T b)
-> CausalClass.ProcessOf Sig.T () (MultiValue.T a, MultiValue.T b)
• In the first argument of ‘(.)’, namely ‘CausalClass.fromSignal’
In the first argument of ‘CausalRender.run’, namely
‘(CausalClass.fromSignal . sig)’
In a stmt of a 'do' block:
proc <- CausalRender.run (CausalClass.fromSignal . sig)
~~~~
If I add `import qualified Synthesizer.LLVM.Causal.Process ()` then the error goes away. However, the import should not be necessary, because the module imports `Synthesizer.LLVM.Generator.Signal` and this in turn imports `Synthesizer.LLVM.Causal.Private` which contains the required instance. This instance is not even orphan.
## Steps to reproduce
You need some unreleased versions of dependent packages for reproduction:
* https://hackage.haskell.org/package/llvm-tf-12.1/candidate
* https://hackage.haskell.org/package/llvm-extra-0.11/candidate
* https://hackage.haskell.org/package/llvm-dsl-0.1/candidate
* https://hackage.haskell.org/package/synthesizer-core-0.8.3/candidate
* https://hackage.haskell.org/package/synthesizer-llvm-1.0/candidate
You should also respect the building hints of
https://hackage.haskell.org/package/llvm-ffi
e.g. manually provide the paths to libLLVM.so and the LLVM C-header files.
Then you can compile with
~~~~
synthesizer-llvm$ PATH=/usr/local/ghc/9.4.4/bin:$PATH cabal-3.8 build all --enable-tests --disable-optimization --disable-documentation
~~~~
## Environment
* GHC version used: 9.4
In GHC before 9.4 this works.9.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/22707panic when compiling recursive function on type changing continuations2023-09-13T12:06:55Zeldritch cookiepanic when compiling recursive function on type changing continuations## Summary
when compiling a certain function i get the following error
```
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.4.2:
lookupIdSubst
$dApplicative_aKX
InScope {p_aKS $creturn_aLA}
Call s...## Summary
when compiling a certain function i get the following error
```
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.4.2:
lookupIdSubst
$dApplicative_aKX
InScope {p_aKS $creturn_aLA}
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:182:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Core/Subst.hs:260:17 in ghc:GHC.Core.Subst
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
## Steps to reproduce
paste the following code in a source file and try to compile it
```haskell
newtype Cont o i a = Cont {runCont ::(a -> i) -> o }
t1:: Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1)
t1 c = Cont $ \ati1tti2 -> (runCont c) (ati1tti2 $ \a -> evalCont (t1 c) >>== \ati1 -> return ati1 a )
evalCont:: Cont o a a -> o
evalCont c = (runCont c)id
instance Monad (Cont p p) where
return a = Cont ($ a)
(>>=) = (>>==)
class PMonad m where
(>>==):: m p q a -> (a -> m q r b) -> m p r b
instance PMonad Cont where
(Cont cont) >>== afmb = Cont $ \bti -> cont $ \a -> (runCont . afmb) a bti
main:: IO ()
main = putStrLn "bug"
```
for some reason the code doesn't type check if i remove the class and define >>== as a top level function. the t1 function is the problematic one.
i do believe it shouldn't type check at all as evalCont is applied to (t1 c) which is of type Cont o i2 (a -> i1) which most definitely isn't of type Cont o a a for all types o i2 a and i1
## Expected behavior
the code should compile normally or it should report a compile error not panic
## Environment
* GHC version used: 9.4.2
Optional:
* Operating System: Linux
* System Architecture:9.8.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/22670Unclear error message for ambigous instance when instance type does not occur...2023-02-04T09:21:38ZAndreas KlebingerUnclear error message for ambigous instance when instance type does not occur in any function argument.Consider a definition like this:
```
{-# LANGUAGE ScopedTypeVariables #-}
mfbs :: forall a. FiniteBits a => Int
mfbs = finiteBitSize (undefined :: a)
```
And the resulting error message:
```
lib\BitFields\ObjFields.hs:14:9: error:
...Consider a definition like this:
```
{-# LANGUAGE ScopedTypeVariables #-}
mfbs :: forall a. FiniteBits a => Int
mfbs = finiteBitSize (undefined :: a)
```
And the resulting error message:
```
lib\BitFields\ObjFields.hs:14:9: error:
* Could not deduce (FiniteBits a0)
from the context: FiniteBits a
bound by the type signature for:
mfbs :: forall a. FiniteBits a => Int
at lib\BitFields\ObjFields.hs:14:9-37
The type variable `a0' is ambiguous
Potentially matching instances:
instance FiniteBits a => FiniteBits (And a)
-- Defined in `Data.Bits'
instance FiniteBits a => FiniteBits (Iff a)
-- Defined in `Data.Bits'
...plus five others
(use -fprint-potential-instances to see them all)
* In the ambiguity check for `mfbs'
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: mfbs :: forall a. FiniteBits a => Int
|
14 | mfbs :: forall a. FiniteBits a => Int
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This makes sense. At a call site to `mfbs` there is "obviously" no way to tell the compiler which instance to use.
But I found the error message here very unhelpful if not harmful. It says `Could not deduce (FiniteBits a0) from the context: FiniteBits a`. Why does it refer to a0 when there should be only one `a` given the use of scoped type variables? I assume this is the fallout of an implementation detail in the ambiguity check.
Maybe for a function with a type like `f :: (C a,...) => ...` we could check if `a` occurs only in the constraints and if so give a more specific warning.https://gitlab.haskell.org/ghc/ghc/-/issues/22648Order of inferred quantification is observable2023-01-16T12:18:02ZVladislav ZavialovOrder of inferred quantification is observable# Background
In GHC, a forall-bound variable may have one of the three visibilities:
* required, written `forall a ->`
* specified, written `forall a.`
* inferred, written `forall {a}.`
With type applications, it is easy to observe th...# Background
In GHC, a forall-bound variable may have one of the three visibilities:
* required, written `forall a ->`
* specified, written `forall a.`
* inferred, written `forall {a}.`
With type applications, it is easy to observe the order of specified variables. `f @Int @Bool` means different things depending on whether we have:
* `f1 :: forall a b. (a, b) -> ...`
* `f2 :: forall b a. (a, b) -> ... -- not the same!`
However, the order of _inferred_ variables is supposed to be unobservable by the programmer:
* `g1 :: forall {a} {b}. (a, b) -> ...`
* `g2 :: forall {b} {a}. (a, b) -> ... -- indistinguishable from g1`
Inferred variables are ignored by type applications for this reason.
# Bug
I have constructed examples that allow the programmer to observe the order of inferred quantification.
## Term-level example
Let us define `const_inf1` and `const_inf2` as follows:
```haskell
const_inf1 :: () -> forall {a} {b}. a -> b -> a
const_inf2 :: () -> forall {b} {a}. a -> b -> a
const_inf1 _ x _ = x
const_inf2 _ x _ = x
```
We would like `const_inf1` and `const_inf2` to be interchangeable in all contexts. However, consider this definition:
```
const_spec :: () -> forall a b. a -> b -> a
const_spec = const_inf1
```
This is accepted by GHC, but if we replace `const_inf1` with `const_inf2`, the definition is rejected with the following error message:
```
• Couldn't match type ‘a’ with ‘b’
Expected: () -> forall a b. a -> b -> a
Actual: () -> forall {b} {a}. a -> b -> a
```
Interestingly enough, the type variables `{a}` and `{b}` are "inferred" only de jure; in the actual program, they are very much specified by an explicit `forall`. In other words, their order is determined by the source code, not by implementation details of the compiler, so this is only mildly unsatisfactory. The situation is much worse at the type level.
## Type-level example
Let us define `D` as follows (no explicit signature):
```haskell
data D a b
```
What kind does GHC infer for `D`? There are two options:
* `D :: forall {k1} {k2}. k1 -> k2 -> Type`
* `D :: forall {k2} {k1}. k1 -> k2 -> Type`
This time, the choice between these options *is* determined by implementation details, so it is important to make sure that the order of quantification is not observable. We can define `D1` and `D2` with explicit signatures to aid the investigation:
```haskell
type D1 :: forall {k1} {k2}. k1 -> k2 -> Type
type D2 :: forall {k2} {k1}. k1 -> k2 -> Type
data D1 a b
data D2 a b
```
Note that the kinds of `D1` and `D2` correspond to the possible inferred kinds for `D`. So any program that can distinguish `D`, `D1`, and `D2`, depends on GHC's implementation details. Behold:
```haskell
type family F :: forall k1 k2. k1 -> k2 -> Type
type instance F = D1
```
This is accepted as long as we use `D1`, but rejected if we use `D2` with the following error:
```
• Couldn't match kind ‘k2’ with ‘k1’
Expected kind ‘forall k1 k2. k1 -> k2 -> Type’,
but ‘D2’ has kind ‘forall {k2} {k1}. k1 -> k2 -> Type’
```
# Cause
The bug occurs when `eqType` is used to compare types for equality, because `eqType` and `tcEqType` ignore the distinction between inferred and specified variables. This design decision is described in `Note [ForAllTy and type equality]`:
<details><summary>Click to expand</summary>
```
{- Note [ForAllTy and type equality]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we compare (ForAllTy (Bndr tv1 vis1) ty1)
and (ForAllTy (Bndr tv2 vis2) ty2)
what should we do about `vis1` vs `vis2`.
First, we always compare with `eqForAllVis`.
But what decision do we make?
Should GHC type-check the following program (adapted from #15740)?
{-# LANGUAGE PolyKinds, ... #-}
data D a
type family F :: forall k. k -> Type
type instance F = D
Due to the way F is declared, any instance of F must have a right-hand side
whose kind is equal to `forall k. k -> Type`. The kind of D is
`forall {k}. k -> Type`, which is very close, but technically uses distinct
Core:
-----------------------------------------------------------
| Source Haskell | Core |
-----------------------------------------------------------
| forall k. <...> | ForAllTy (Bndr k Specified) (<...>) |
| forall {k}. <...> | ForAllTy (Bndr k Inferred) (<...>) |
-----------------------------------------------------------
We could deem these kinds to be unequal, but that would imply rejecting
programs like the one above. Whether a kind variable binder ends up being
specified or inferred can be somewhat subtle, however, especially for kinds
that aren't explicitly written out in the source code (like in D above).
For now, we decide
the specified/inferred status of an invisible type variable binder
does not affect GHC's notion of equality.
That is, we have the following:
--------------------------------------------------
| Type 1 | Type 2 | Equal? |
--------------------|-----------------------------
| forall k. <...> | forall k. <...> | Yes |
| | forall {k}. <...> | Yes |
| | forall k -> <...> | No |
--------------------------------------------------
| forall {k}. <...> | forall k. <...> | Yes |
| | forall {k}. <...> | Yes |
| | forall k -> <...> | No |
--------------------------------------------------
| forall k -> <...> | forall k. <...> | No |
| | forall {k}. <...> | No |
| | forall k -> <...> | Yes |
--------------------------------------------------
IMPORTANT NOTE: if we want to change this decision, ForAllCo will need to carry
visiblity (by taking a ForAllTyBinder rathre than a TyCoVar), so that
coercionLKind/RKind build forall types that match (are equal to) the desired
ones. Otherwise we get an infinite loop in the solver via canEqCanLHSHetero.
Examples: T16946, T15079.
```
</details>
As far as examples reported in this ticket are concerned, the following uses of `tcEqType` are involved:
1. In `uType`:
```haskell
defer ty1 ty2 -- See Note [Check for equality before deferring]
| ty1 `tcEqType` ty2 = return (mkNomReflCo ty1)
| otherwise = uType_defer t_or_k origin ty1 ty2
```
2. In `checkExpectedKind`:
```haskell
; if act_kind' `tcEqType` exp_kind
then return res_ty -- This is very common
else ...
```Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/22647GHC 9.2 fails to select an instance based on kinds in the presence of type fa...2023-04-11T05:24:59ZlierdakilGHC 9.2 fails to select an instance based on kinds in the presence of type families## Summary
I'm observing an instance resolution regression between GHC 9.0.2 and 9.2.4/9.2.5. Consider the following code:
```haskell
{-# LANGUAGE KindSignatures, DataKinds, TypeFamilies, FlexibleInstances #-}
module Bug where
import...## Summary
I'm observing an instance resolution regression between GHC 9.0.2 and 9.2.4/9.2.5. Consider the following code:
```haskell
{-# LANGUAGE KindSignatures, DataKinds, TypeFamilies, FlexibleInstances #-}
module Bug where
import Data.Kind
data D = D
type family F :: D -> Type
-- data F (x :: D)
class C f where
meth :: f
instance C (f (p :: D))
instance C (f (p :: Type))
_ = meth :: F 'D
_ = meth :: [Type]
```
The problem is in `_ = meth :: F 'D`. By all accounts, `F 'D` should match with `f (p :: D)`, and it does in GHC 9.0. GHC 9.2, however, produces an inane error message:
```
error:
• Overlapping instances for C (F 'D) arising from a use of ‘meth’
Matching instances: instance C (f p) -- Defined at test.hs:12:10
There exists a (perhaps superclass) match:
(The choice depends on the result of evaluating ‘F’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the expression: meth :: F 'D
In a pattern binding: _ = meth :: F 'D
```
Notice it only shows a single matching instance, but says there are many!
Switching `type family F` for `data F` makes it resolve the instance as expected again, so this is type-family-specific.
#21208, #21515 seem related.
## Steps to reproduce
Try to compile/load the example code above.
## Expected behavior
To typecheck.
## Environment
* GHC version used: tested on 9.2.4 and 9.2.59.2.6sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/22623singletons-base assertion failures2023-04-11T04:53:16ZMatthew Pickeringsingletons-base assertion failuresSee https://gitlab.haskell.org/ghc/head.hackage/-/jobs/1263130 from head.hackage
```
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.5.20221214:
ASSERT failed!
:%|
[a_iyZ0, a1_iyZ1]
[n1_iyZ2, n2_...See https://gitlab.haskell.org/ghc/head.hackage/-/jobs/1263130 from head.hackage
```
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.5.20221214:
ASSERT failed!
:%|
[a_iyZ0, a1_iyZ1]
[n1_iyZ2, n2_iyZ3]
[a1_iyZ1 ~# (n1_iyZ2 ':| n2_iyZ3), Sing n1_iyZ2, Sing n2_iyZ3]
[TYPE: b_a1AFo,
TYPE: Apply
(Lambda_6989586621679297343Sym2 t_a1AFp t_a1AFq) n1_a1Ax8,
TYPE: n1_a1AzX, TYPE: n2_a1AzY, CO: co_a1AzZ, ds_d1Eby, ds_d1Ebz]
[TYPE: n1_a1AzX, TYPE: n2_a1AzY]
[CO: co_a1AzZ, ds_d1Eby, ds_d1Ebz]
Sub (Sym (D:R:SingNonEmpty[0]
<b_a1AFo>_N)) (D:R:Applyk3k2Lambda_6989586621679297343Sym2arg_69895866216792970096989586621679297345[0]
<NonEmpty a_a1AFn>_N
<NonEmpty b_a1AFo>_N
<a_a1AFn>_N
<t_a1AFp>_N
<t_a1AFq>_N
<n1_X6>_N
; D:R:Lambda_6989586621679297343[0]
<NonEmpty a_a1AFn>_N
<NonEmpty b_a1AFo>_N
<a_a1AFn>_N
<t_a1AFp>_N
<t_a1AFq>_N
<n1_X6>_N
; D:R:Case_6989586621679297346[0]
<a_a1AFn>_N
<NonEmpty a_a1AFn>_N
<NonEmpty b_a1AFo>_N
<a_a1AFn>_N
<n1_X6>_N
<n1_X6>_N
<t_a1AFp>_N
<t_a1AFq>_N)
; Sub (D:R:SingNonEmpty[0]
<b_a1AFo>_N) (Sym (D:R:Case_6989586621679297346[0]
<a_a1AFn>_N
<NonEmpty a_a1AFn>_N
<NonEmpty b_a1AFo>_N
<a_a1AFn>_N
<n1_i1ble>_N
<n1_i1ble>_N
<t_a1AFp>_N
<t_a1AFq>_N)
; Sym (D:R:Lambda_6989586621679297343[0]
<NonEmpty a_a1AFn>_N
<NonEmpty b_a1AFo>_N
<a_a1AFn>_N
<t_a1AFp>_N
<t_a1AFq>_N
<n1_i1ble>_N)
; Sym (D:R:Applyk3k2Lambda_6989586621679297343Sym2arg_69895866216792970096989586621679297345[0]
<NonEmpty a_a1AFn>_N
<NonEmpty b_a1AFo>_N
<a_a1AFn>_N
<t_a1AFp>_N
<t_a1AFq>_N
<n1_i1ble>_N))
SNonEmpty
(Apply (Lambda_6989586621679297343Sym2 t_a1AFp t_a1AFq) n1_X6)
SNonEmpty
(Apply (Lambda_6989586621679297343Sym2 t_a1AFp t_a1AFq) n1_i1ble)
SNonEmpty
SNonEmpty
(Apply (Lambda_6989586621679297343Sym2 t_a1AFp t_a1AFq) n1_a1Ax8)
Call stack:
CallStack (from HasCallStack):
assertPpr, called at compiler/GHC/Core/Opt/Arity.hs:2982:5 in ghc:GHC.Core.Opt.Arity
CallStack (from HasCallStack):
panic, called at compiler/GHC/Utils/Error.hs:454:29 in ghc:GHC.Utils.Error
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
which arises from this assertion in `Core.Opt.Arity`.
```
assertPpr (eqType from_ty (mkTyConApp to_tc (map exprToType $ takeList dc_univ_tyvars dc_args))) dump_doc $
assertPpr (equalLength val_args arg_tys) dump_doc $
Just (dc, to_tc_arg_tys, to_ex_args ++ new_val_args)
```https://gitlab.haskell.org/ghc/ghc/-/issues/22560Invisible binders in type declarations2023-06-09T22:59:26ZVladislav ZavialovInvisible binders in type declarations[GHC Proposal #425 "Invisible binders in type declarations"](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst) has two aspects to it:
1. Introduce `@`-binders in type declarations
2. Conso...[GHC Proposal #425 "Invisible binders in type declarations"](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst) has two aspects to it:
1. Introduce `@`-binders in type declarations
2. Consolidate the language (remove arity inference, remove implicit RHS quantification, require type instantiations to be determined by the LHS)
This ticket is to track the implementation of the first part only: `@`-binders is type declarations. Here are some examples of code that we aim to allow:
```haskell
-- Class declarations
class C @k (a :: k) where ...
-- Data declarations
data D @k @j (a :: k) (b :: j) = ...
-- Type family declarations
type family F @p @q (a :: p) (b :: q) where ...
```9.8.1Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/22537Strange polytype unification behavior2023-07-17T10:00:41ZMatthew Cravenclyring@gmail.comStrange polytype unification behavior## Summary
While looking into https://github.com/ghc-proposals/ghc-proposals/issues/558, I noticed some strangeness around `can_eq_nc_forall`, which I thought I should record while it is fresh. Specifically:
## Bug
* When there are ne...## Summary
While looking into https://github.com/ghc-proposals/ghc-proposals/issues/558, I noticed some strangeness around `can_eq_nc_forall`, which I thought I should record while it is fresh. Specifically:
## Bug
* When there are nested `forall`s, we only check that the _outermost_ visibilities match:
* We (correctly) reject unifying `forall b -> (a, b)` with `forall b. (a, b)`, but
* we (wrongly) succeed unifying `forall a. forall b -> (a, b)` with `forall a. forall b. (a, b)`.
## Opportuntity
* We only match successfully if the `forall` nesting depth is the same for both types. For nominal equality, this is expected (I think), but it's a bit odd for representational equality. If we have `newtype P a = PC (forall c. (a, c))`:
* We (correctly?) representationally unify `P a` with `forall b. (a, b)`, but
* we reject representationally unifying `forall a. P a` with `forall a. forall b. (a, b)`.
Here is a concrete example:
```
import Data.Coerce
newtype M = MkM (forall a b. a -> b -> b)
newtype N a = MkN (forall b. a -> b -> b)
newtype P = MkP (forall a. N a)
g1 :: M -> P
g1 x = coerce x
g2 :: P -> M
g2 x = coerce x
```
It is not unreasonable to expect `g1` and `g2` to typecheck; there are perfectly well-behaved coercions that connect them.
## Expected behavior
* We should definitely reject matching `forall a. forall b -> (a, b)` with `forall a. forall b. (a, b)`, at least when matching for nominal equality.
* It's surprising and neat-o that representational equality solving with newtypes around polytypes even sort-of works. But I don't have an informed opinion about whether this "should" be expected to generally work.https://gitlab.haskell.org/ghc/ghc/-/issues/22526Impredicative kinds & type synonyms seemingly don't work together2023-01-26T11:56:59ZLas SafinImpredicative kinds & type synonyms seemingly don't work together## Steps to reproduce
```haskell
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
import Data.Proxy (Proxy)
import Data.Functor.Identity (Identity (Identity))
import Data.Kind (Type)
-- Changing ...## Steps to reproduce
```haskell
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
import Data.Proxy (Proxy)
import Data.Functor.Identity (Identity (Identity))
import Data.Kind (Type)
-- Changing this to a type family doesn't work either (EDIT: see new comment)
type P :: forall a. a -> Type
type P = Proxy
type Good :: Identity (forall a. a -> Type)
type Good = 'Identity @(forall a. a -> Type) Proxy
type Bad :: Identity (forall a. a -> Type)
type Bad = 'Identity @(forall a. a -> Type) P
{-
Example.hs:17:45: error:
• Expected kind ‘forall a. a -> Type’,
but ‘P’ has kind ‘a0 -> Type’
• In the second argument of ‘'Identity’, namely ‘P’
In the type ‘'Identity @(forall a. a -> Type) P’
In the type declaration for ‘Bad’
|
17 | type Bad = 'Identity @(forall a. a -> Type) P
-}
```
## Expected behavior
`Bad` should seemingly also work, but I would be satisfied with a work-around if there is one.
## Environment
* GHC version used: 9.4.2https://gitlab.haskell.org/ghc/ghc/-/issues/22521HEAD panics (typeOrConstraint) when building lens-5.22022-11-30T17:31:37ZRyan ScottHEAD panics (typeOrConstraint) when building lens-5.2GHC HEAD (using commit 11627c422cfba5e1d84afb08f427007dbc801f10) panics when building the `lens-5.2` library on Hackage. Here is a minimized example:
```hs
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewP...GHC HEAD (using commit 11627c422cfba5e1d84afb08f427007dbc801f10) panics when building the `lens-5.2` library on Hackage. Here is a minimized example:
```hs
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
module Bug (pattern P) where
pattern P :: C a => a
pattern P <- (m -> True)
class C a where
m :: a -> Bool
```
```
$ ghc-9.5.20221124/bin/ghc Bug.hs -fforce-recomp
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.5.20221124:
typeOrConstraint
a_aw0[sk:2] :: k_awr[tau:2]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler\GHC\Utils\Panic.hs:189:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler\GHC\Core\Type.hs:2631:14 in ghc:GHC.Core.Type
typeTypeOrConstraint, called at compiler\GHC\Core\TyCo\Rep.hs:829:20 in ghc:GHC.Core.TyCo.Rep
mkInvisFunTys, called at compiler\GHC\Tc\Utils\TcType.hs:1303:11 in ghc:GHC.Tc.Utils.TcType
mkPhiTy, called at compiler\GHC\Tc\Gen\Sig.hs:488:9 in ghc:GHC.Tc.Gen.Sig
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```9.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/22516GHC 9.4 regression: solveWanteds: too many iterations2023-04-11T11:15:21ZRyan ScottGHC 9.4 regression: solveWanteds: too many iterations_(Originally spun out of a discussion at https://github.com/well-typed/generics-sop/issues/158.)_
GHC 9.2 and earlier accept the following program:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAG..._(Originally spun out of a discussion at https://github.com/well-typed/generics-sop/issues/158.)_
GHC 9.2 and earlier accept the following program:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Bug where
import Data.Kind (Constraint, Type)
data D a
f :: Generic (D a) => ()
f = ()
type family
AllF (c :: k -> Constraint) (xs :: [k]) :: Constraint where
AllF _c '[] = ()
AllF c (x ': xs) = (c x, All c xs)
class (AllF c xs, SListI xs) => All (c :: k -> Constraint) (xs :: [k]) where
type SListI = All Top
class Top x
instance Top x
class All SListI (Code a) => Generic a where
type Code a :: [[Type]]
```
GHC 9.4.3, however, rejects it with the following error message:
```
$ ghc-9.4.3 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:20:6: error:
* solveWanteds: too many iterations (limit = 4)
Unsolved: WC {wc_simple =
[W] irred_aEQ {0}:: AllF SListI (Code (D a0)) (CIrredCan(irred))
[W] irred_aEW {0}:: AllF Top (Code (D a0)) (CIrredCan(irred))
[W] $dGeneric_aEH {0}:: Generic (D a0) (CDictCan)
[W] $dAll_aEP {0}:: All SListI (Code (D a0)) (CDictCan)
[W] $dAll_aEX {0}:: All Top (Code (D a0)) (CDictCan(psc))}
Simples: {[W] irred_aEQ {0}:: AllF
SListI (Code (D a0)) (CIrredCan(irred)),
[W] irred_aEW {0}:: AllF Top (Code (D a0)) (CIrredCan(irred)),
[W] $dGeneric_aEH {0}:: Generic (D a0) (CDictCan),
[W] $dAll_aEP {0}:: All SListI (Code (D a0)) (CDictCan),
[W] $dAll_aEX {0}:: All Top (Code (D a0)) (CDictCan(psc))}
* In the type signature: f :: Generic (D a) => ()
Suggested fix:
Set limit with -fconstraint-solver-iterations=n; n=0 for no limit
|
20 | f :: Generic (D a) => ()
| ^^^^^^^^^^^^^^^^^^^
```
I've tried increasing the value of `-fconstraint-solver-iterations` up to `1000`, but the error message persists.9.4.5Simon Peyton JonesSimon Peyton Jones