GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-02-27T20:15:03Zhttps://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/22144GHC accepts ambiguous type2022-09-06T11:25:10ZOleg GrenrusGHC accepts ambiguous type```haskell
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE DataKinds, PolyKinds, ConstraintKinds, RankNTypes #-}
{-# LANGUAGE MultiParamTypeClasses, TypeOperators, FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}
i...```haskell
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE DataKinds, PolyKinds, ConstraintKinds, RankNTypes #-}
{-# LANGUAGE MultiParamTypeClasses, TypeOperators, FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}
import Data.Kind (Constraint)
class ElimList (c :: k -> Constraint) (l :: [k]) where
elimList :: f '[] -> (forall (x :: k) (xs :: [k]). c x => ElimList c xs => f xs -> f (x : xs)) -> f l
```
GHC-9.0, 9.2 and 9.4 accept the following, GHC-8.10 and previous doens't.
The type is ambiguous, as `c` can vary. It's made clear if we want to define instances for that class:
```haskell
instance ElimList c '[] where
elimList fNil _ = fNil
instance (c x, ElimList c xs) => ElimList c (x : xs) where
elimList fNil fCons = fCons (elimList fNil fCons)
```
the nil case is fine, but the recursive case (as all other use-sites of `elimList`) fail with
```
Ambiguous.hs:15:34: error:
• Could not deduce (ElimList c0 xs)
arising from a use of ‘elimList’
```
and have to be "fixed" by using type-applications:
```haskell
instance (c x, ElimList c xs) => ElimList c (x : xs) where
elimList fNil fCons = fCons (elimList @_ @c fNil fCons)
```
(first argument is `k`).https://gitlab.haskell.org/ghc/ghc/-/issues/22127decomposeRuleLhs reports bogus error2022-09-03T21:05:00ZSimon Peyton JonesdecomposeRuleLhs reports bogus errorConsider
```
f :: Int -> Int
f x = x
{-# RULES "foo" forall a (x::a) (g :: a -> Int). f (g x) = 2 #-}
```
Currently compiling with -O gives
```
Foo.hs:8:11: error:
Rule "foo": Forall'd variable ‘a’ does not appear on left hand side
...Consider
```
f :: Int -> Int
f x = x
{-# RULES "foo" forall a (x::a) (g :: a -> Int). f (g x) = 2 #-}
```
Currently compiling with -O gives
```
Foo.hs:8:11: error:
Rule "foo": Forall'd variable ‘a’ does not appear on left hand side
|
8 | {-# RULES "foo" forall a (x::a) (g :: a -> Int). f (g x) = 2 #-}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
## Diagnosis
`GHC.HsToCore.Binds.decomposeRuleLhs` takes the free vars of the LHS and checks that all of those free vars are among the binders. But the (shallow) free vars of `f (g x)` are are just `{f,g,x}`, but not `a`. Yet `a` is a binder.
Clearly we want the *deep* free vars of the LHS for this error check.Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/22101Redundant constraint warning does not account for pattern checking2022-09-23T21:47:18ZDavid FeuerRedundant constraint warning does not account for pattern checking## Summary
Constraints that are only required for pattern checking are falsely reported as redundant.
## Steps to reproduce
```haskell
{-# language DataKinds, GADTs, TypeOperators, AllowAmbiguousTypes #-}
{-# options_ghc -Wall -Wredun...## Summary
Constraints that are only required for pattern checking are falsely reported as redundant.
## Steps to reproduce
```haskell
{-# language DataKinds, GADTs, TypeOperators, AllowAmbiguousTypes #-}
{-# options_ghc -Wall -Wredundant-constraints #-}
import Data.Type.Bool
import Data.Type.Equality
-- | Singletons for 'Bool'
data SBool b where
SFalse :: SBool 'False
STrue :: SBool 'True
-- | If a disjunction is false, so is its left argument.
orL :: (a || b) ~ 'False => SBool a -> a :~: 'False
orL SFalse = Refl
```
GHC tells me the `(a || b) ~ 'False` constraint is redundant.
## Expected behavior
I expect the above to compile without warnings.
## Discussion
The constraint is redundant—for type checking: `orR` will pass the type checker if it's removed. However, it's *not* redundant for pattern checking—the pattern checker will produce a warning if it's removed. Is there a way to account for which constraints the pattern checker "uses", and avoid warning about ones that it does?
## Environment
* GHC version used: 9.4.1
Optional:
* Operating System:
* System Architecture:https://gitlab.haskell.org/ghc/ghc/-/issues/22079Free variable finders are confused about coercion holes2022-08-30T22:17:45ZRichard Eisenbergrae@richarde.devFree variable finders are confused about coercion holes**Definition.** A *deep* traversal to collect free variables means that the traversal collects also the free variables in the kinds of free variables. These are also sometimes called the deep free variables.
When collecting free variabl...**Definition.** A *deep* traversal to collect free variables means that the traversal collects also the free variables in the kinds of free variables. These are also sometimes called the deep free variables.
When collecting free variables deeply of a type, GHC does a strange thing when recurring into the kinds of the variables: it zaps the set of in-scope variables, as documented in Note [Closing over free variable kinds] in GHC.Core.TyCo.Rep (and summarized in this para). For example, if we are collecting the free variables of `forall a b. a -> b -> Proxy c`, we do not want to return `a` and `b` as free variables. We thus remember these as locally in scope, so that we skip occurrences. However, we do *not* want to retain `a` and `b` as in scope when traversing the kind of `c`. Why not? Let's imagine `c :: Either a b`, so that we have `forall a b. a -> b -> Proxy (c :: Either a b)`. Now, are `a` and `b` free? Yes! That's because `c` is not locally bound -- it must have come into scope previously. Accordingly, the `a` and `b` in its kind are *not* the `a` and `b` bound by that `forall` we're all looking at -- they also must be bound further up. The simple solution is to drop the in-scope set when traversing a free variable kind. This is implemented today.
The problem is for coercion holes. (The problem presumably *also* happens for metavariables, but it came up in the context of coercion holes.) Specifically, look at this function:
```hs
-- | Returns free variables of Implication as a composable FV computation.
-- See Note [Deterministic FV] in "GHC.Utils.FV".
tyCoFVsOfImplic :: Implication -> FV
-- Only called on *zonked* things
tyCoFVsOfImplic (Implic { ic_skols = skols
, ic_given = givens
, ic_wanted = wanted })
| isEmptyWC wanted
= emptyFV
| otherwise
= tyCoFVsVarBndrs skols $
tyCoFVsVarBndrs givens $
tyCoFVsOfWC wanted
```
In the main body of this function, we bind the skolems and the givens and then traverse (deeply) the wanteds. The fact that we bind the skolems and the givens means that skolems and givens will *not* be considered free (good). But now consider this:
```
forall a. [W] hole_abc :: a ~ Bool
[W] hole_def :: ... |> hole_abc ...
```
When traversing the type of `hole_abc`, we see that the `a` is a skolem and refuse to add it to the fv set. Good. But when traversing the type of `hole_def`, we see an *occurrence* of `hole_abc` and then look in its type *without an in-scope set*. So we report `a` as free! Disaster!
The root problem here is that coercion holes (resp. metavariables) aren't really bound. They *are* local to a certain TcLevel, which could in theory be used to know whether to consider them "bound-like" or "free-like" (i.e. the level could be used to set whether to zap the in-scope set when traversing an occurrence's kind), but that would add considerable complication to free-variable finding.
There is not, as far as I know, a live bug around this issue. That's because the implementation doesn't meet the specification, as we can see in this code:
```hs
tyCoFVsOfCo (HoleCo h) fv_cand in_scope acc
= tyCoFVsOfCoVar (coHoleCoVar h) fv_cand in_scope acc
tyCoFVsOfCoVar v fv_cand in_scope acc
= (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc
```
Note that the `in_scope` set is *not* zapped when recurring in `varType v`. So, despite the logic at the top of this post, we don't actually apply it in `tyCoFVsOfCoVar`. (We do apply it in lots of other places.) Interestingly, the lack of zapping affects ordinary covars, not just coercion holes, and so is quite possibly a bug-in-waiting. (We just don't have enough locally bound covars to notice.)
My Tweag intern @yiyunliu is revamping free-variable finders. In his new version, he fixed the bug, but then that caused the "Disaster!" described above. (If it's helpful, I imagine he can provide more concrete details.)
I think the right answer here is to add the zapping logic to the recurrence into covar kinds, but then also to add logic to `tyCoFVsOfImplic` to consider the coercion holes bound when traversing the types of the wanteds in a WC. Then, the free-var finder won't traverse the holes' kinds at all, avoiding the problem described here.
This whole area still makes me nervous though: given that a coercion hole (resp. metavariable) stands for an as-yet-unknown coercion (resp. type), taking the free variables of any type that has holes (metavars) seems dodgy, even though it's quite useful.https://gitlab.haskell.org/ghc/ghc/-/issues/22063Forall-types should be of a TYPE kind2023-12-04T13:51:21ZmniipForall-types should be of a TYPE kindThis is the main ticket for a bunch of related tickets, relating to the kind of `(forall a. ty)`. Specifically
* #22063 (this ticket)
* #8388
* #15979
* #19573
## Summary
With or without impredicativity, we usually intend a `forall`...This is the main ticket for a bunch of related tickets, relating to the kind of `(forall a. ty)`. Specifically
* #22063 (this ticket)
* #8388
* #15979
* #19573
## Summary
With or without impredicativity, we usually intend a `forall`-quantified type to be inhabited by values, i.e. that `forall a. {- ... -} :: TYPE r` for some `r`. Apparently this is never checked in GHC and we have roughly:
```
Gamma, a |- t :: k
---------------------------
Gamma |- (forall a. t) :: k
```
This implies that all kinds (even closed) are lifted: `forall a. a :: k`. Of course in presence of TypeFamilies+UndecidableInstances all kinds are already lifted, but this seems somehow worse.
Furthermore such a type can be used to trigger a core lint error, the wording of which ("Non-*-like kind when *-like expected") suggests that at least on some level it is expected that `forall a. ... :: *`. Applying a type constructor (other than `->`) to a type like `forall a. a` requires ImpredicativeTypes, but (and this might be an unrelated issue) apparently the type can appear on the left side of an application even without ImpredicativeTypes.
## Steps to reproduce
GHCi says:
```hs
> :kind forall a. a
forall a. a :: k
```
The following are accepted by GHC 9.2.3, 8.6.5 and HEAD:
```hs
{-# LANGUAGE RankNTypes, DataKinds, KindSignatures #-}
module M where
type F = (forall (f :: * -> *). f) ()
f :: F
f = f
```
```hs
{-# LANGUAGE RankNTypes, DataKinds, KindSignatures, ImpredicativeTypes #-}
module M where
type B = forall (a :: Bool). a
b :: proxy B
b = b
```
but with `-dcore-lint` they explode:
```hs
*** Core Lint errors : in result of Desugar (before optimization) ***
a.hs:5:1: warning:
Non-Type-like kind when Type-like expected: * -> *
when checking the body of forall: f_agw
In the type of a binder: f
In the type ‘F’
Substitution: [TCvSubst
In scope: InScope {f_agw}
Type env: [agw :-> f_agw]
Co env: []]
*** Offending Program ***
Rec {
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "M"#)
f :: F
[LclIdX]
f = f
end Rec }
*** End of Offense ***
```
```hs
*** Core Lint errors : in result of Desugar (before optimization) ***
b.hs:5:1: warning:
Non-Type-like kind when Type-like expected: Bool
when checking the body of forall: a_auh
In the type of a binder: b
In the type ‘forall (proxy :: Bool -> *). proxy B’
Substitution: [TCvSubst
In scope: InScope {a_auh proxy_aui}
Type env: [auh :-> a_auh, aui :-> proxy_aui]
Co env: []]
*** Offending Program ***
Rec {
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "M"#)
b :: forall (proxy :: Bool -> *). proxy B
[LclIdX]
b = \ (@(proxy_awC :: Bool -> *)) -> b @proxy_awC
end Rec }
*** End of Offense ***
```
GHC 8.4.4 will fail the first program with an impredicativity error, but will still accept it with ImpredicativeTypes enabled, and will still crash with a core lint.
## Expected behavior
`forall a. e` should constrain `e :: TYPE r`, meaning GHCi should report `forall a. a :: *` or `forall a. a :: TYPE r`. Both programs should be rejected with a type error for the above reason. The first program (or programs like it) should raise an "Illegal impredicative type".
## Environment
* GHC version used: 8.4.4, 8.6.5, 9.2.3, HEAD
Optional:
* Operating System: GNU/Linux
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc/-/issues/21935Implementation of GHC.TypeLits.<= is still not quite right2023-03-21T15:21:25ZChristiaan BaaijImplementation of GHC.TypeLits.<= is still not quite right`base-4.6` (GHC 7.6) introduced:
```haskell
module GHC.TypeLits where
class (m :: Nat) <= (n :: Nat)
type family (m :: Nat) <=? (n :: Nat) :: Bool
```
where both `<=` and `<=?` had hard-coded resolution rules.
Then in `base-4.7` (GHC ...`base-4.6` (GHC 7.6) introduced:
```haskell
module GHC.TypeLits where
class (m :: Nat) <= (n :: Nat)
type family (m :: Nat) <=? (n :: Nat) :: Bool
```
where both `<=` and `<=?` had hard-coded resolution rules.
Then in `base-4.7` (GHC 7.8) we got:
```haskell
type x <= y = (x <=? y) ~ True
type family (m :: Nat) <=? (n :: Nat) :: Bool
```
Where only `<=?` had hard-coded resolution rules.
And for a very long time all was right with the world.
Then, in `base-4.16` (GHC 9.2) we suddenly got:
```haskell
type x <= y = (x <=? y) ~ True
type (<=?) :: k -> k -> Bool
type m <=? n = OrdCond (Compare m n) 'True 'True 'False
type OrdCond :: Ordering -> k -> k -> k -> k
type family OrdCond o lt eq gt where
OrdCond 'LT lt eq gt = lt
OrdCond 'EQ lt eq gt = eq
OrdCond 'GT lt eq gt = gt
type Compare :: k -> k -> Ordering
type family Compare a b
type instance Compare (a :: Natural) b = CmpNat a b
type family CmpNat (m :: Natural) (n :: Natural) :: Ordering
```
Where only `CmpNat` has hard-coded resolution rules.
This new implementation of `<=` had error messages of much porer quality than previous implementations, which was reported in #20009.
For the following code:
```haskell
{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
module TestInEq where
import Data.Proxy
import GHC.TypeLits
proxyInEq :: (a <= b) => Proxy a -> Proxy b -> ()
proxyInEq _ _ = ()
proxyInEq1 :: Proxy a -> Proxy (a+1) -> ()
proxyInEq1 = proxyInEq
```
we went from this error message in GHC 9.0:
```
$ ghci TestInEq.hs
GHCi, version 9.0.1: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling TestInEq ( TestInEq.hs, interpreted )
TestInEq.hs:11:14: error:
• Couldn't match type ‘a <=? (a + 1)’ with ‘'True’
arising from a use of ‘proxyInEq’
• In the expression: proxyInEq
In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
• Relevant bindings include
proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()
(bound at TestInEq.hs:11:1)
|
11 | proxyInEq1 = proxyInEq
| ^^^^^^^^^
Failed, no modules loaded.
```
to this error message in GHC 9.2:
```
$ ghci TestInEq.hs
GHCi, version 9.2.0.20210422: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling TestInEq ( TestInEq.hs, interpreted )
TestInEq.hs:11:14: error:
• Couldn't match type ‘Data.Type.Ord.OrdCond
(CmpNat a (a + 1)) 'True 'True 'False’
with ‘'True’
arising from a use of ‘proxyInEq’
• In the expression: proxyInEq
In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
• Relevant bindings include
proxyInEq1 :: Proxy a -> Proxy (a + 1) -> ()
(bound at TestInEq.hs:11:1)
|
11 | proxyInEq1 = proxyInEq
| ^^^^^^^^^
Failed, no modules loaded.
ghci>
```
The quality of the error message was fixed in !6066, which is currently included to be part of the GHC 9.4.1 release.
In !6066 the implementation of `<=` was changed to:
```haskell
type x <= y = Assert (x <=? y) (LeErrMsg x y)
type LeErrMsg x y = TypeError ('Text "Cannot satisfy: " ':<>: 'ShowType x ':<>: 'Text " <= " ':<>: 'ShowType y)
type Assert :: Bool -> Constraint -> Constraint
type family Assert check errMsg where
Assert 'True _ = ()
Assert _ errMsg = errMsg
```
which would create error messages of the following shape instead:
```
• Cannot satisfy: a <= a + 1
• In the expression: proxyInEq
In an equation for ‘proxyInEq1’: proxyInEq1 = proxyInEq
```
## Remaining issue
The problem with the !6066 implementation is that the following code:
```haskell
{-# LANGUAGE DataKinds, TypeFamilies #-}
module KnownNat2 where
import GHC.TypeLits
class KnownNat2 (name :: Symbol) (a :: Nat) (b :: Nat) where {}
instance (b <= a) => KnownNat2 "-" a b
```
that used to compile without errors, now gives the following error (this is with the GHC 9.4.1-rc1 release):
```
GHCi, version 9.4.0.20220721: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling KnownNat2 ( KnownNat2.hs, interpreted )
KnownNat2.hs:9:10: error:
* Variables `b, a' occur more often
in the constraint `b <= a'
than in the instance head `KnownNat2 "-" a b'
(Use UndecidableInstances to permit this)
* In the instance declaration for `KnownNat2 "-" a b'
|
9 | instance (KnownNat a, KnownNat b, b <= a) => KnownNat2 "-" a b
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
```