GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-07-03T09:33:13Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/23156GHC version 9.4.4: heap overflow; the same with 9.6.1, but 9.2.7 compiles fine2023-07-03T09:33:13ZMikolaj KonarskiGHC version 9.4.4: heap overflow; the same with 9.6.1, but 9.2.7 compiles fine## Summary
Heap overflow when compiling, both with -O0 and with -O1.
Edit: Disclaimer: lots of `UndecidableInstances` in this code, though not in the file on which GHC diverges.
## Steps to reproduce
Clone this repo at this commit
h...## Summary
Heap overflow when compiling, both with -O0 and with -O1.
Edit: Disclaimer: lots of `UndecidableInstances` in this code, though not in the file on which GHC diverges.
## Steps to reproduce
Clone this repo at this commit
https://github.com/Mikolaj/horde-ad/commit/773bc01382748b073fddee776b6fd8e6657c35df
then run (you can ignore `cabal.project`, the fork of `mnist-idx` is no longer needed)
`cabal build -j1 --disable-optimization`
Or any other `build` invocation. I haven't found a set of options for which it does compile.
## Expected behavior
Compiles.
## Environment
Fails the same with 9.4.4 and 9.6.1 (with `--allow-newer`). Fails the same in CI:
https://github.com/Mikolaj/horde-ad/actions/runs/4492044812/jobs/7901371200#step:18:629
Compiles and all tests pass with 9.2.7.Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/23152DerivingError constraint failures are too lazy2023-03-28T13:45:39ZDavid FeuerDerivingError constraint failures are too lazy## Summary
Constraints on instances derived using `DerivingVia` aren't checked eagerly enough.
## Steps to reproduce
```haskell
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DataKinds #-}
import GHC.Ty...## Summary
Constraints on instances derived using `DerivingVia` aren't checked eagerly enough.
## Steps to reproduce
```haskell
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DataKinds #-}
import GHC.TypeLits
class Crumb a
newtype Fool a = Fool a
instance TypeError ('Text "You can't do that") => Crumb (Fool a)
deriving via Fool Int
instance Crumb Int
```
This compiles with no warnings or errors.
## Expected behavior
I expect the above program to be rejected, since it produces an instance for `Crumb Int` with no constraints when the ground instance it's based on has an unsatisfiable constraint. I don't *think* this is a soundness problem per se, but it does make me slightly nervous.
This example is a highly boring reduction of a more interesting one in `linear-generics`. I'd like to produce a custom type error when attempting to derive an instance of `Generics.Linear.Generic1` via `Generics.Linear.Unsafe.ViaGHCGenerics.GHCGenerically1`. This sort of works, but only because the derived *methods* fail to typecheck. Since there are two methods, we get two type errors. And since the errors are on the methods, they end up being considerably more confusing to read than they should be.
## Environment
* GHC version used: 9.6.1
Optional:
* Operating System:
* System Architecture:https://gitlab.haskell.org/ghc/ghc/-/issues/23135Type checking influenced by definition2023-10-30T14:49:04ZKrzysztof GogolewskiType checking influenced by definitionHere's a program, taken from https://gitlab.haskell.org/ghc/ghc/-/merge_requests/8820#note_486855
```haskell
{-# LANGUAGE DataKinds, TypeFamilies, TypeFamilyDependencies #-}
module M where
import Data.Kind
import GHC.TypeLits
data Tup...Here's a program, taken from https://gitlab.haskell.org/ghc/ghc/-/merge_requests/8820#note_486855
```haskell
{-# LANGUAGE DataKinds, TypeFamilies, TypeFamilyDependencies #-}
module M where
import Data.Kind
import GHC.TypeLits
data Tuple2 x y = MkTuple2 x y
type TupleArgKind :: Nat -> Type
type family TupleArgKind n = r | r -> n where
TupleArgKind 2 = Tuple2 Type Type
type Tuple :: forall (n :: Nat). TupleArgKind n -> Type
type family Tuple ts = r | r -> ts where
Tuple (MkTuple2 a b) = Tuple2 a b
-- works
f :: Tuple (MkTuple2 a b) -> ()
f (MkTuple2 _ _) = ()
-- fails
g :: Tuple (MkTuple2 a b) -> ()
g x = ()
-- works
h :: Tuple @2 (MkTuple2 a b) -> ()
h x = ()
```
`f` and `g` have the same type signature - but only `g` is rejected because of an error in the type. This violates the principle that a type signature should stand on its own and not be influenced by the definition (unless `PartialTypeSignatures` is enabled).
When typechecking the signature for `f`, the relevant part from `-ddump-tc-trace` (with `wanted` added) is
```
kindGeneralizeSome
type: forall (a :: x_aFQ[tau:2]) (b :: y_aFR[tau:2]).
(Tuple (MkTuple2 a b |> {co_aFS}) -> () |> (TYPE {co_aMe})_N)
dvs: DV {dv_kvs = {x_aFQ[tau:2], y_aFR[tau:2], n_aFP[tau:2]},
dv_tvs = {}, dv_cvs = {co_aMh}}
wanted: WC {wc_impl =
Implic {
TcLevel = 2
Skolems = (a_aDb[sk:2] :: k_aFL[tau:2])
(b_aDc[sk:2] :: k_aFM[tau:2])
Given-eqs = NoGivenEqs
Status = Unsolved
Given =
Wanted =
WC {wc_simple =
[W] hole{co_aMh} {0}:: TupleArgKind n_aFP[tau:2]
GHC.Prim.~# Tuple2
x_aFQ[tau:2] y_aFR[tau:2] (CEqCan)}
Binds = CoEvBindsVar<aMf>
the type signature for ‘f’ }}
filtered_dvs: DV {dv_kvs = {}, dv_tvs = {}, dv_cvs = {co_aMh}}
```
Given `a :: x, b :: y`, the expression `Tuple @n (MkTuple2 a b)` is legal when `TupleArgKind n ~ Tuple2 x y`. If generalized, the full type would be
```
f :: forall (n :: Nat) (x :: Type) (y :: Type) (a :: x) (b :: y). TupleArgKind n ~ Tuple2 x y => Tuple (MkTuple2 a b) -> ()
```
but that would require coercion quantification. So we do not generalize over `x, y, n`. Later, in the case of `f`, they are inferred to be `Type, Type, 2` while in the case of `g`, there are no further constraints and we error. Looks like we should reject `f` just like `g`.https://gitlab.haskell.org/ghc/ghc/-/issues/23070Refactor the constraint solver2023-05-23T17:42:06ZSimon Peyton JonesRefactor the constraint solverFor some time Richard and I have wanted to refactor the constraint solver. Currently every constraint travels down a "pipeline" consisting of
* Canonicalisation
* Interact with the inert set
* Do top level reactions (e.g. instance decls...For some time Richard and I have wanted to refactor the constraint solver. Currently every constraint travels down a "pipeline" consisting of
* Canonicalisation
* Interact with the inert set
* Do top level reactions (e.g. instance decls)
This turns out to clumsy, especially for equality constraints. So instead we just want a solver for equalities, a solver for class constraints, and so on. We think that will modularise the code, and make it easier to modify. This ticket tracks progress.Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/22977Extremely confused type error2023-03-06T09:58:35ZDavid FeuerExtremely confused type error## Summary
Accidentally using an `ArrayArray#` operation with the wrong type leads to a truly bizarre error message referencing a type that has nothing to do with what's going on. The result is *extremely* delicate, depending on whether...## Summary
Accidentally using an `ArrayArray#` operation with the wrong type leads to a truly bizarre error message referencing a type that has nothing to do with what's going on. The result is *extremely* delicate, depending on whether an import is qualified.
## Steps to reproduce
```
dfeuer@squirrel:~/src> ghc-9.6 --version
The Glorious Glasgow Haskell Compilation System, version 9.6.0.20230111
```
```haskell
{-# language CPP #-}
{-# language MagicHash #-}
{-# language UnboxedTuples #-}
{-# language RoleAnnotations #-}
{-# language UnliftedNewtypes #-}
{-# language KindSignatures #-}
{-# language DataKinds #-}
module ExtremeConfusion where
import Data.Coerce (coerce)
import GHC.Exts ( Int#, State#, ArrayArray#, MutableArrayArray#
, UnliftedType)
import qualified GHC.Exts as Exts
newtype UnliftedArray# (a :: UnliftedType) = UnliftedArray# ArrayArray#
type role UnliftedArray# representational
newtype MutableUnliftedArray# s (a :: UnliftedType) = MutableUnliftedArray# (MutableArrayArray# s)
type role MutableUnliftedArray# nominal representational
newUnliftedArray# :: Int# -> a -> State# s -> (# State# s, MutableUnliftedArray# s a #)
newUnliftedArray# sz a s = coerce (Exts.newArray# sz a s)
```
This gives me the error
```
ExtremeConfusion.hs:23:28: error: [GHC-10283]
• Couldn't match representation of type ‘a’
with that of ‘Exts.ByteArray#’
arising from a use of ‘coerce’
‘a’ is a rigid type variable bound by
the type signature for:
newUnliftedArray# :: forall (a :: UnliftedType) s.
Int# -> a -> State# s -> (# State# s, MutableUnliftedArray# s a #)
at ExtremeConfusion.hs:22:1-87
• In the expression: coerce (Exts.newArray# sz a s)
In an equation for ‘newUnliftedArray#’:
newUnliftedArray# sz a s = coerce (Exts.newArray# sz a s)
• Relevant bindings include
a :: a (bound at ExtremeConfusion.hs:23:22)
newUnliftedArray# :: Int#
-> a -> State# s -> (# State# s, MutableUnliftedArray# s a #)
(bound at ExtremeConfusion.hs:23:1)
|
23 | newUnliftedArray# sz a s = coerce (Exts.newArray# sz a s)
| ^^^^^^
```
## Expected behavior
If I add `newArray#` to the list of imports from `GHC.Exts` and use it unqualified, I get a much nicer message:
```
ExtremeConfusion.hs:23:28: error: [GHC-18872]
• Couldn't match representation of type: MutableArrayArray# s
with that of: GHC.Prim.MutableArray# s a
arising from a use of ‘coerce’
The data constructor ‘GHC.ArrayArray.MutableArrayArray#’
of newtype ‘MutableArrayArray#’ is not in scope
• In the expression: coerce (newArray# sz a s)
In an equation for ‘newUnliftedArray#’:
newUnliftedArray# sz a s = coerce (newArray# sz a s)
• Relevant bindings include
s :: State# s (bound at ExtremeConfusion.hs:23:24)
a :: a (bound at ExtremeConfusion.hs:23:22)
newUnliftedArray# :: Int#
-> a -> State# s -> (# State# s, MutableUnliftedArray# s a #)
(bound at ExtremeConfusion.hs:23:1)
|
23 | newUnliftedArray# sz a s = coerce (newArray# sz a s)
| ^^^^^^
```
I would love to get this message regardless. If that's not doable, I suspect the situation can at least be ameliorated by using `Any` instead of `ByteArray#` in the definition of `ArrayArray#`.
## Environment
* GHC version used: 9.6
Optional:
* Operating System:
* System Architecture:https://gitlab.haskell.org/ghc/ghc/-/issues/22960EPS contention may be slowing down parallel make2023-02-27T20:15:03ZTeo CamarasuEPS contention may be slowing down parallel make### Summary
I think it's likely that contention of the EPS is blocking parallel make from reaching its full potential on large shallow module graphs.
The EPS is stored in a global IORef and is regularly checked during typechecking.
If a...### Summary
I think it's likely that contention of the EPS is blocking parallel make from reaching its full potential on large shallow module graphs.
The EPS is stored in a global IORef and is regularly checked during typechecking.
If an interface hasn't yet been loaded, then it will be loaded, typecheched (potentially loading further interfaces), and then atomically merged with the current value of the EPS.
From a quick glance at the code I'm seeing two potential issues:
1) Duplicated work due to two threads racing:
In a situation where two threads both discover that an interface is missing from the EPS, I think, they will duplicate work to load it.
2) Atomically updating the EPS blocks reads:
AFAIK using `atomicModifyIORef'` blocks reads, as it updates the IORef with a thunk that it then evaluates. While the thunk is under evaluation, other threads will be blocked if they try to look at it.
I say potential issues because I haven't done enough investigating to confirm if this is actually an issue.
I'll try to do that in the next couple of weeks and come up with some strategies to mitigate it if it does turn out to be a problem.
### Context
I was led to the EPS by looking at the DWARF decoded stacks of threads blocking on blackholes while compiling `Cabal`.
Code that was looking things up in the EPS stood out to me. I used this branch of ghc https://gitlab.haskell.org/teo/ghc/-/commits/wip/blackhole-introspectionBen GamariBen Gamarihttps://gitlab.haskell.org/ghc/ghc/-/issues/22924Regression in Coercible solver with type constructor variables2023-02-20T13:40:14ZXia Li-yaoRegression in Coercible solver with type constructor variables## Summary
GHC 9.6.0 alpha2 rejects the following use of `coerce` that was accepted in 9.4
## Steps to reproduce
```haskell
{-# LANGUAGE FlexibleInstances #-}
module G where
import Data.Functor.Const (Const ())
import Data.Coerce
f ...## Summary
GHC 9.6.0 alpha2 rejects the following use of `coerce` that was accepted in 9.4
## Steps to reproduce
```haskell
{-# LANGUAGE FlexibleInstances #-}
module G where
import Data.Functor.Const (Const ())
import Data.Coerce
f :: Coercible (f a) a => Const a () -> Const (f a) ()
f = coerce
```
## Expected behavior
That compiles on GHC 9.4.
On 9.6 alpha2:
```
G.hs:8:5: error: [GHC-18872]
• Couldn't match representation of type: Const a ()
with that of: Const (f a) ()
arising from a use of ‘coerce’
The data constructor ‘Data.Functor.Const.Const’
of newtype ‘Const’ is not in scope
• In the expression: coerce
In an equation for ‘f’: f = coerce
• Relevant bindings include
f :: Const a () -> Const (f a) () (bound at G.hs:8:1)
|
8 | f = coerce
| ^^^^^^
```https://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/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/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/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/22463GHC.Types.Any leaks in -Wincomplete-patterns warning2022-11-15T15:17:24ZMorrowMGHC.Types.Any leaks in -Wincomplete-patterns warning## Summary
```hs
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Bug where
foo :: Either a Char
foo = Right 'x'
bar :: String
bar = case foo of
Right c -> [c]
```
we get a warning message:
```
Bug.hs:9:7: warning: [-Wincomplete-...## Summary
```hs
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Bug where
foo :: Either a Char
foo = Right 'x'
bar :: String
bar = case foo of
Right c -> [c]
```
we get a warning message:
```
Bug.hs:9:7: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In a case alternative:
Patterns of type ‘Either GHC.Types.Any Char’ not matched: Left _
|
9 | bar = case foo of
| ^^^^^^^^^^^...
```
which leaks details about `GHC.Types.Any`.
## Environment
* GHC version used: 9.2.4, 9.4.2
The bug does not occur in GHC 8.10.7 or GHC 9.0.2. Those versions do not have a `Patterns of type` clause in the warning.sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/22436Infinite loop in typechecker/renamer on ghc 9.2.42023-02-07T17:14:17ZjberrymanInfinite loop in typechecker/renamer on ghc 9.2.4## Summary
While working on our app I noticed a small change seems to lead to an infinite loop during typechecking / renaming, during `cabal repl` or compiling without optimizations.
`-ddump-tc-trace -ddump-rn-trace` Seems to stream ...## Summary
While working on our app I noticed a small change seems to lead to an infinite loop during typechecking / renaming, during `cabal repl` or compiling without optimizations.
`-ddump-tc-trace -ddump-rn-trace` Seems to stream output forever, it also looks like all memory was consumed
maybe this is a dupe of : https://gitlab.haskell.org/ghc/ghc/-/issues/21530
## Steps to reproduce
sorry for lack of small reproducer
- clone this branch: https://github.com/jberryman/graphql-engine/tree/jberryman/11-9-22-ghc-bug-DONT-DELETE
- `$ echo 12345 > "$(git rev-parse --show-toplevel)/server/CURRENT_VERSION"`
- you likely need to install the system libraries mentioned in: `packaging/graphql-engine-base/ubuntu.dockerfile`
- `$ cabal repl lib:graphql-engine`
reverting the commit at HEAD of that branch `55937fa5` no longer exhibits issue
## Expected behavior
compilation or type error
## Environment
* GHC version used: 9.2.4
Optional:
* Operating System: debian linux
* System Architecture: x86-64Matthew PickeringMatthew Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/22336Better desugaring failures when boxing fails2023-09-07T09:26:44ZSimon Peyton JonesBetter desugaring failures when boxing failsThe new type-vs-constraint patch (!8750), when it lands, allows us to do things like
```haskell
[ I# (x2 +# y2) | I# x <- xs, let x2 = x +# 1 | I# y <- ys, let y2 = y -# 1 ]
```
This is a parallel list comprehension where we want to coll...The new type-vs-constraint patch (!8750), when it lands, allows us to do things like
```haskell
[ I# (x2 +# y2) | I# x <- xs, let x2 = x +# 1 | I# y <- ys, let y2 = y -# 1 ]
```
This is a parallel list comprehension where we want to collect a bunch of pairs `(x2,y2)`, but we can't make a pair of unboxed values. So we box them before building the pair.
* This is done in `GHC.Core.Make.wrapBox` and friends.
* See also `Note [Boxing constructors]` in GHC.Builtin.Types
But
* We can't (currently) *guarantee* to do this - notably for nested unboxed tuples.
* If we fail to box, GHC crashes
But really we should make the desugarer stop with a civilised error message.
Should not be hard, but requires some careful attention to the various call sites of `mkBigCoreTup` etc.
**Closely related ticket**: #21165https://gitlab.haskell.org/ghc/ghc/-/issues/22267OverloadedRecordDot is broken when records have a constraint2023-06-07T10:31:18ZGautier DI FOLCOOverloadedRecordDot is broken when records have a constraint## Summary
Whenever I try to reference a function with a constraint with OverloadedRecordDot syntax, I have an error.
## Steps to reproduce
While this code compiles:
```
{-# LANGUAGE OverloadedRecordDot #-}
module B where
data R = R...## Summary
Whenever I try to reference a function with a constraint with OverloadedRecordDot syntax, I have an error.
## Steps to reproduce
While this code compiles:
```
{-# LANGUAGE OverloadedRecordDot #-}
module B where
data R = R {myFunc :: String -> Int}
myUsage :: R -> Int
myUsage r = r.myFunc "42"
```
Adding a constraint:
```
{-# LANGUAGE OverloadedRecordDot #-}
module B where
import GHC.Stack
data R = R {myFunc :: HasCallStack => String -> Int}
myUsage :: R -> Int
myUsage r = r.myFunc "42"
```
gives me an error:
```
B.hs:9:13: error:
• No instance for (GHC.Records.HasField "myFunc" R (String -> Int))
arising from selecting the field ‘myFunc’
(maybe you haven't applied a function to enough arguments?)
• In the expression: r.myFunc
In the expression: r.myFunc "42"
In an equation for ‘myUsage’: myUsage r = r.myFunc "42"
|
9 | myUsage r = r.myFunc "42"
```
it also fails with a more classic one:
```
{-# LANGUAGE OverloadedRecordDot #-}
module B where
data R = R {myFunc :: forall a. Show a => a -> Int}
myUsage :: R -> Int
myUsage r = r.myFunc "42"
```
which gives
```
B.hs:7:13: error:
• No instance for (GHC.Records.HasField "myFunc" R (String -> Int))
arising from selecting the field ‘myFunc’
(maybe you haven't applied a function to enough arguments?)
• In the expression: r.myFunc
In the expression: r.myFunc "42"
In an equation for ‘myUsage’: myUsage r = r.myFunc "42"
|
7 | myUsage r = r.myFunc "42"
```
## Expected behavior
I expects the type-check works as there's no constraint (while propagating it).
## Environment
* GHC version used: 9.4.2 / 9.2.2
Optional:
* Operating System: NixOS unstable
* System Architecture: x86_64Gautier DI FOLCOGautier DI FOLCOhttps://gitlab.haskell.org/ghc/ghc/-/issues/22257Dependent type families cannot be separated from their instances2023-06-30T17:25:47ZXia Li-yaoDependent type families cannot be separated from their instances## Summary
I'm doing experiments with some very dependently typed type families. It works all nice when everything is in a single file, but not when trying to split it into different modules.
## Steps to reproduce
Minimal example: two...## Summary
I'm doing experiments with some very dependently typed type families. It works all nice when everything is in a single file, but not when trying to split it into different modules.
## Steps to reproduce
Minimal example: two type families F and G, where G's second argument depends on the first, and one instance for each family.
```haskell
{-# LANGUAGE TypeFamilies #-}
module A where
import Data.Kind (Type)
type family F (x :: Type) :: Type
type family G (x :: Type) (y :: F x) :: Type
type instance F () = Type
type instance G () k = k
```
That compiles (tried on GHC 9.4). But if we move the last two lines to another module, we get:
```
B.hs:9:20: error:
• Expected kind ‘F ()’, but ‘k’ has kind ‘*’
• In the second argument of ‘G’, namely ‘k’
In the type instance declaration for ‘G’
|
9 | type instance G () k = k
|
```
If we then move the last line to yet another module, it compiles again.
It seems that when typechecking the G instance, GHC somehow does not see F's instance.
Even more weirdness: this behavior is not stable under expansion/folding of type synonyms.
The following refactoring of the instances does compile when separated from the family declarations:
```haskell
type W = ()
type instance F () = Type
type instance G W k = k
```
(And other combinations of W and () don't compile.)
## Expected behavior
These declarations should compile regardless of whether they are in separate files.
## Environment
* GHC version used: 9.0, 9.2, 9.4https://gitlab.haskell.org/ghc/ghc/-/issues/22230Uninferrable type variable in type family2022-09-29T13:06:44ZDenis StoyanovUninferrable type variable in type familyHello everyone. I have this code (I use ghc-9.2.4)
```haskell
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE Undecid...Hello everyone. I have this code (I use ghc-9.2.4)
```haskell
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
module Main where
import Data.Proxy
import Data.Kind
import Data.Type.Equality
import qualified GHC.TypeLits as TL
import qualified Data.Type.Bool as TB
type Undefined :: k
type family Undefined where {}
type LoT :: Type -> Type
data LoT k where
LoT0 :: LoT Type
(:&&:) :: k -> LoT ks -> LoT (k -> ks)
type HeadLoT :: forall k k'. LoT (k -> k') -> k
type family HeadLoT tys where
HeadLoT (a ':&&: _) = a
type TailLoT :: forall k k'. LoT (k -> k') -> LoT k'
type family TailLoT tys where
TailLoT (_ ':&&: as) = as
type (:@@:) :: forall k. k -> LoT k -> Type
type family f :@@: tys where
f :@@: _ = f
f :@@: as = f (HeadLoT as) :@@: TailLoT as
type (~>) :: forall k1 k2. k1 -> k2 -> Type
type (~>) f g = Proxy f -> Proxy g -> Type
type Eval :: forall as f g. (f ~> g) -> f :@@: as -> g :@@: as
type family Eval nat t
-- >>> :k Eval
-- Eval :: forall {k} (as :: LoT k) (f :: k) (g :: k).
-- (f ~> g) -> (f :@@: as) -> g :@@: as
type Exp_ :: forall k. k -> Type
type Exp_ a = () ~> a
type Eval_ :: forall k. Exp_ k -> k
type Eval_ (e :: Exp_ a) = Eval e '()
```
And I got this error
```
• Uninferrable type variable (as0 :: LoT (*)) in
the type synonym right-hand side: Eval @{*} @as0 @() @k e '()
• In the type declaration for 'Eval_'
|
| type Eval_ (e :: Exp_ a) = Eval e '()
```
In ghc-8.10.7 it’s ok, and compile, but Eval has different kind
```haskell
-- >>> :kind Eval
-- Eval :: forall k (as :: LoT k) (f :: k) (g :: k).
-- (f ~> g) -> (f :@@: as) -> g :@@: as
```https://gitlab.haskell.org/ghc/ghc/-/issues/22224Regression with type families in quantified constraints breaking inference2022-10-10T20:19:51ZLas SafinRegression with type families in quantified constraints breaking inference## Summary
Given something like `f :: forall a. ((forall b. C) => a) -> A` where `C`'s context mentions a type family,
`f x` where `x`'s type isn't `forall a. a` fails without a type application. `f undefined` does OTOH still work.
This...## Summary
Given something like `f :: forall a. ((forall b. C) => a) -> A` where `C`'s context mentions a type family,
`f x` where `x`'s type isn't `forall a. a` fails without a type application. `f undefined` does OTOH still work.
This works for me in 9.0.2, but not since at least 9.2.3.
## Steps to reproduce
```haskell
import Data.Kind (Type, Constraint)
type family C :: Type
class (C ~ ()) => D where
f :: forall a. ((forall b. D) => a) -> ()
f _ = ()
x :: ()
x = f ()
```
Error:
```
Test.hs:19:7: error:
• Couldn't match expected type ‘a0’ with actual type ‘()’
• ‘a0’ is untouchable
inside the constraints: forall b. D
bound by a type expected by the context:
(forall b. D) => a0
at Test.hs:19:7-8
• In the first argument of ‘f’, namely ‘()’
In the expression: f ()
In an equation for ‘x’: x = f ()
|
19 | x = f ()
```
## Expected behavior
This should work. The type of `a` is obviously `()`.
## Environment
* GHC version used: 9.2.4https://gitlab.haskell.org/ghc/ghc/-/issues/22145Allow promotion of one-to-one pattern synonyms2022-09-06T13:36:09ZOleg GrenrusAllow promotion of one-to-one pattern synonyms```haskell
{-# LANGUAGE PatternSynonyms, DataKinds #-}
import Data.Proxy
import Data.Kind
pattern JustJust :: a -> Maybe (Maybe a)
pattern JustJust x = Just (Just x)
p :: Proxy (JustJust Type)
p = Proxy
```
is rejected because of
``...```haskell
{-# LANGUAGE PatternSynonyms, DataKinds #-}
import Data.Proxy
import Data.Kind
pattern JustJust :: a -> Maybe (Maybe a)
pattern JustJust x = Just (Just x)
p :: Proxy (JustJust Type)
p = Proxy
```
is rejected because of
```
• Pattern synonym ‘JustJust’ cannot be used here
(pattern synonyms cannot be promoted)
```
but I don't see why not.
This issue allows to distinguish between pattern synonym and real constructor, e.g. a pattern synonym like
```haskell
pattern Some :: a -> Maybe a
pattern Some x = Just x
```
cannot be used to provide backwards compatibility when renaming constructors! (e.g. upcoming `Solo` to `MkSolo` is a real example).