GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-08-23T13:13:37Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/23467GHC internal error when pattern synonym has wrong type signature2023-08-23T13:13:37ZAndreas AbelGHC internal error when pattern synonym has wrong type signatureWhen I forgot an argument in the type signature of a pattern synonym, I got, in addition to the expected error, also a GHC internal error.
MWE:
```haskell
{-# LANGUAGE PatternSynonyms #-}
data ConData = ConData { _pars :: Int }
data De...When I forgot an argument in the type signature of a pattern synonym, I got, in addition to the expected error, also a GHC internal error.
MWE:
```haskell
{-# LANGUAGE PatternSynonyms #-}
data ConData = ConData { _pars :: Int }
data Decl = ConDecl ConData
pattern Con :: Decl -- The correct type would be Int -> Decl
pattern Con { pars } = ConDecl (ConData pars)
foo :: Decl -> Int
foo (Con { pars }) = pars
```
Reported errors are:
```
PatternSyn.hs:7:1: error:
• Pattern synonym ‘Con’ has one argument
but its type signature has 1 fewer arrows
• In the declaration for pattern synonym ‘Con’
|
7 | pattern Con { pars } = ConDecl (ConData pars)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
PatternSyn.hs:10:6: error:
• GHC internal error: ‘pars’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [rh1 :-> Identifier[foo::Decl
-> Int, TopLevelLet {} True]]
• In the pattern: Con {pars}
In an equation for ‘foo’: foo (Con {pars}) = pars
|
10 | foo (Con { pars }) = pars
| ^^^^^^^^^^^^
```
Seems GHC does not recover well from the original error and then throws an internal error.
The internal error is reported by GHC 8.6 and above (tested 8.6.5, 8.8.4, 8.10.7, 9.0.2, 9.2.8, 9.4.5, 9.6.2).
Evidence in CI run, e.g.: https://github.com/agda/agda/actions/runs/5155818185/jobs/9285983967#step:12:3379.8.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23446GHC 9.4.5, 9.6.1: Fails to differentiate between Constraint and Type when che...2023-07-23T02:19:50ZlierdakilGHC 9.4.5, 9.6.1: Fails to differentiate between Constraint and Type when checking for instance overlap## Summary
GHC since 9.4 apparently fails to differentiate instances between kinds `Type` and `Constraint` when checking for overlap.
## Steps to reproduce
```haskell
{-# LANGUAGE PolyKinds, FlexibleInstances #-}
module Lib where
im...## Summary
GHC since 9.4 apparently fails to differentiate instances between kinds `Type` and `Constraint` when checking for overlap.
## Steps to reproduce
```haskell
{-# LANGUAGE PolyKinds, FlexibleInstances #-}
module Lib where
import Data.Kind
class Foo (a :: k) where
bar :: proxy a -> ()
instance Foo (a :: Type) where
bar = undefined
instance Foo (a :: Constraint) where
bar = undefined
test :: proxy (k :: Constraint) -> ()
test = bar -- Overlapping instances for Foo k arising from a use of ‘bar’
test2 :: proxy (k :: Type) -> ()
test2 = bar -- Overlapping instances for Foo k arising from a use of ‘bar’
```
Compiles fine on GHC 9.2.7, fails on GHC 9.4.5 and 9.6.1.
The instance choice should be unambiguous, as arguments are of different kinds. But GHC doesn't see that.
FWIW, it's still able to differentiate between `Type` and data kinds.
## Expected behavior
To compile.
## Environment
* GHC version used: 9.4.5, 9.6.1
Optional:
* Operating System: Linux
* System Architecture: amd64https://gitlab.haskell.org/ghc/ghc/-/issues/23445GHC 9.6.1: equality constraints are apparently not propagated everywhere (spe...2023-09-13T12:06:53ZlierdakilGHC 9.6.1: equality constraints are apparently not propagated everywhere (specifically in record update syntax)## Summary
Encountered this with GHC 9.6.1. Works fine on GHC 9.4.5, 9.2.7
## Steps to reproduce
Here is a reproducer:
```haskell
{-# OPTIONS_GHC -Werror -Wincomplete-patterns #-}
{-# LANGUAGE TypeFamilies, GADTs, TypeOperators #-}
...## Summary
Encountered this with GHC 9.6.1. Works fine on GHC 9.4.5, 9.2.7
## Steps to reproduce
Here is a reproducer:
```haskell
{-# OPTIONS_GHC -Werror -Wincomplete-patterns #-}
{-# LANGUAGE TypeFamilies, GADTs, TypeOperators #-}
module Lib where
data GADT where
GADT :: d ~ () => d -> GADT
data SomeRec = SomeRec { srField :: () }
data FooBar p where
Foo :: FooBar ()
Bar :: FooBar Int
getFooBar :: d -> FooBar d
getFooBar = undefined
falsePositive :: GADT -> SomeRec -> SomeRec
falsePositive (GADT di) cd =
cd
{ srField = case getFooBar di of -- Patterns of type ‘FooBar d’ not matched: Bar
Foo -> ()
}
fine :: GADT -> SomeRec -> SomeRec
fine (GADT di) cd = case getFooBar di of
Foo -> cd { srField = () }
```
Notice moving `case` out of the record update fixes this (but it has different strictness characteristics).
Matching on `GADT` puts `d ~ ()` into scope, so matching on `getFooBar di` has only one possible alternative. But apparently the constraint is not propagated into the record update?
## Expected behavior
To compile without incomplete pattern warning.
## Environment
* GHC version used: 9.6.1
Optional:
* Operating System: Linux
* System Architecture: amd64sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23438`TypeError` thrown in standalone `via` deriving but not attached `via` deriving2023-05-31T18:33:03Zparsonsmatt`TypeError` thrown in standalone `via` deriving but not attached `via` deriving## Summary
A `newtype` for `via` deriving is provided that gives a `TypeError`, effectively banning the instance from use, but with a nice error message. We use this at work to prevent folks from running database operations in the "main...## Summary
A `newtype` for `via` deriving is provided that gives a `TypeError`, effectively banning the instance from use, but with a nice error message. We use this at work to prevent folks from running database operations in the "main" monad, and instead guide them towards `runDB` which handles transactions.
## Steps to reproduce
```haskell
{-# language DerivingVia #-}
{-# language DataKinds #-}
{-# language UndecidableInstances #-}
{-# language StandaloneDeriving #-}
module Woops where
import GHC.TypeLits
class C a where
f :: a -> a
newtype Can'tBeC a = Can'tBeC a
instance ( TypeError ('Text "No")) => C (Can'tBeC a) where
f = error "unreachable"
instance C Int where f = id
data Good = Good
deriving C via (Can'tBeC Good)
data Bad = Bad
deriving via Can'tBeC Bad instance C Bad
```
With GHC 9.6.1, I get the following result:
```
λ ~/Projects/ghc-woops/ master* cabal build
Build profile: -w ghc-9.6.1 -O1
In order, the following will be built (use -v for more details):
- ghc-woops-0.1.0.0 (lib) (file src/Woops.hs changed)
Preprocessing library for ghc-woops-0.1.0.0..
Building library for ghc-woops-0.1.0.0..
[2 of 2] Compiling Woops ( src/Woops.hs, /home/matt/Projects/ghc-woops/dist-newstyle/build/x86_64-linux/ghc-9.6.1/ghc-woops-0.1.0.0/build/Woops.o, /
home/matt/Projects/ghc-woops/dist-newstyle/build/x86_64-linux/ghc-9.6.1/ghc-woops-0.1.0.0/build/Woops.dyn_o ) [Source file changed]
src/Woops.hs:25:1: error: [GHC-64725]
• No
• In the third argument of ‘ghc-prim-0.10.0:GHC.Prim.coerce’, namely
‘(f @(Can'tBeC Bad))’
In the expression:
ghc-prim-0.10.0:GHC.Prim.coerce
@(Can'tBeC Bad -> Can'tBeC Bad) @(Bad -> Bad) (f @(Can'tBeC Bad))
In an equation for ‘f’:
f = ghc-prim-0.10.0:GHC.Prim.coerce
@(Can'tBeC Bad -> Can'tBeC Bad) @(Bad -> Bad) (f @(Can'tBeC Bad))
When typechecking the code for ‘f’
in a derived instance for ‘C Bad’:
To see the code I am typechecking, use -ddump-deriv
|
25 | deriving via Can'tBeC Bad instance C Bad
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is consistent going back to GHC 8.10.7.
## Expected behavior
I expect that the `StandaloneDeriving` and attached deriving have the same behavior.
But, to be totally specific, I do want both instances to be *accepted*. The purpose of providing the `TypeError` instance here is to provide helpful error messages to folks that are using these, so instead of seeing `No instance for C Bad` they see `You need to do X if you want to use C in the Bad type` or similar.
## Environment
* GHC version used: 9.6.1, 9.4.5, 9.2.7, 8.10.7
Optional:
* Operating System: Ubuntu
* System Architecture: x86sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23413Insoluble constraints and dead code (again)2023-12-15T13:50:17ZSimon Peyton JonesInsoluble constraints and dead code (again)This ticket concerns GHC's treatment of insoluble constraints, a dark corner but alas one
that is not unoccupied. Relevant prior discussion:
* #17543: a careful discussion of dead code
* #12466: examples where dead-given signatures mig...This ticket concerns GHC's treatment of insoluble constraints, a dark corner but alas one
that is not unoccupied. Relevant prior discussion:
* #17543: a careful discussion of dead code
* #12466: examples where dead-given signatures might show up
Consider these definitions:
```
f :: (Int ~ Bool) => Int -> Bool
f x = f x
g1 :: (Int ~ Bool) => Int -> Bool
g1 x = f x
g2 :: (Bool ~ Int) => Int -> Bool
g2 x = f x
h :: (Int ~ Bool) => Int -> Bool
h x = x
```
Currently, GHC accepts `f` and `g1` but rejects `g2` and `h`. This is wildly inconsistent.
There are two things to consider
1. Whether the type signatures pass the ambiguity check
2. Whether the value definitions (e.g. `g2 x = f x`) typecheck
## Background
Reminder: `t1 ~ t2` is a class constraint for a class that behaves much as if we had:
```
class (a ~# b) => a ~ b where {}
instance (a ~# b) => a ~ b
```
So
* The unboxed coercion `(a ~# b)` is superclass of the boxed dictionary constraint `a ~ b`.
* To solve `(a ~ b)` we can instead solve `(a ~# b)`, and box up the result.
## Typechecking the terms: item 2
Let's begin with (2), assuming that the type signatures are accepted.
Here's what happens:
* In `f` and `g1` we have:
```
[G] Int ~ Bool
[W] Int ~ Bool
```
and we solve the Wanted from the Given.
* In `g2` we have
```
[G] Int ~ Bool
[W] Bool ~ Int
```
The Wanted is not precisely equal to the Given, so we instead simplify to
```
[W] Bool ~# Int
```
We do have available `[G] Int ~# Bool` (via the superclass of `[G] Int ~ Bool`), but we always decline to use a Given to
solve an *insoluble* Wanted. We could change that, but it's a deliberate choice
in GHC.Tc.Solver.Interact
```
interactIrred inerts ct_w@(CIrredCan { cc_ev = ev_w, cc_reason = reason })
| isInsolubleReason reason
-- For insolubles, don't allow the constraint to be dropped
-- which can happen with solveOneFromTheOther, so that
-- we get distinct error messages with -fdefer-type-errors
```
* In `h` we have
```
[G] Int ~ Bool
[W] Int ~# Bool
```
Just like in `g2` we decline to use the Given to solve the insoluble Wanted.
So whether we reject or not is dependent in a very fragile way on (a) the orientation of the Wanted `(Int ~ Bool)`, and (b) whether we decompose it to `Int ~# Bool`. The latter should be utterly innocuous, and indeed in !10415 I am decomposing equalities `t1 ~ t2` into primitive equalities `t1 ~~ t2` much more aggressively than before (for good, but unrelated, reasons).
Gah! We should either accept them all (by solving the Wanteds from the (unsatisfiable) Givens), or reject them all.
## The ambiguity check: item 1
The [user manual says](https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/ambiguous_types.html?highlight=switching%20off#ambiguous-types-and-the-ambiguity-check): "even with ambiguity checking switched off `-XAllowAmbiguousTypes`, GHC will complain about a function that can never be called, such as this one:"
```
f :: (Int ~ Bool) => a -> a
```
This simply isn't true. Function `f` above is accepted with or without `-XAllowAmbiguousTypes`. Why?
Because the ambiguity check tries, in effect, to typecheck the definition `f = f`, which gives rise to
```
[G] Int ~ Bool
[W] Int ~ Bool
```
which, as we have seen, is (fragile-ly) accepted.
So GHC isn't obeying its own user manual.
## What to do
There seem to be two consistent courses of action:
* **PermissivePlan**: allow insoluble Wanteds to be solved from (identical) insoluble Givens. This would accept all four definitions above.
* **RestrictivePlan**: do not allow insoluble Wanteds to be solved (at all). This would reject all four definitions.
**RestrictivePlan** is simple and consistent. But:
* It would reject some programs that are currently accepted, which might annoy some people.
* In particular, the ambiguity check would reject the above type signatures, just as the user manual claims. One possiblity is to say that `-XAllowAmbiguousTypes` would simply drop the ambiguity check altogether (just like it says!), so you could use that to accept such signatures.
* Consider the signature `hr :: ((Int~Bool) => Int -> Bool) -> Int`. Now the un-callable function is on the left of an arrow, so it wan't cause problems for the caller of `hr`. Arguably, then, it should not give rise to any ambiguity-check complaints. But under RestrictivePlan, if we *also* use `-XDeepSubsumption` I think we would get an error in the ambiguity check; and it is one that is hard to avoid. (With the default simple-subsumption there is no problem -- we drop to equality.)
* See #12466 and #17543
**PermissivePlan** might annoy fewer people, but:
* It is a bit fragile. For example consider
```
[G] Int ~# Bool
[W] F Int ~# Int
```
and suppose we have `type instance F Bool = Int`. Maybe we can use that Given to rewrite the Wnated to `[W] F Bool ~# Int`, and now we could solve it. But we really, really are not going to do this. It would be difficult. The most we can do is solve an insoluble Wanted from an identical Given.
* It defers type errors. Ambiguity checking rejects `f :: Eq a => Int -> Int` on the grounds that caller of `f` will get an ambiguous constraint `Eq alpha`. But a constraint like `f :: (Int~Bool) => blah` is even worse: the caller has no chance of satisfying that! So if we like the ambiguity check at all, we should like it even more for insoluble constraints.https://gitlab.haskell.org/ghc/ghc/-/issues/23409Replace TcLclEnv in CtLoc with a specific datatype2023-06-05T20:00:10ZMatthew PickeringReplace TcLclEnv in CtLoc with a specific datatypeThe `TcLclEnv` is used in a `CtLoc` for some error reporting but a large part of it isn't used.
It is problematic because it induces an import of `GHC.Tc.Types` from where `CtLoc` is defined which creates a big module cycle, because `Tc...The `TcLclEnv` is used in a `CtLoc` for some error reporting but a large part of it isn't used.
It is problematic because it induces an import of `GHC.Tc.Types` from where `CtLoc` is defined which creates a big module cycle, because `TcLclEnv` contains `WantedConstraints` which contain `Ct`s which contains `CtLocs` and so on.
From a module graph perspective this is bad, because having loops like this harms compile time.
From a logic perspective this is bad, because a CtLoc can contain a TcLclEnv which in theory could contain more CtLoc and so on. There is also no reason to presuppose that what is needed in a CtLocEnv is precisely, or a subset of a `TcLclEnv`. There could easily be more/different information in the `CtLocEnv` which is not needed by a `TcLclEnv`.
The solution is to define a separate type `CtLocEnv` which contains just what is needed for error reporting and provide a function to create a `CtLocEnv` from a `TcLclEnv` when it's needed.Matthew PickeringMatthew Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/23408Potential bug/oddity in resolving `Coercible` constraints2023-05-23T17:42:04ZparsonsmattPotential bug/oddity in resolving `Coercible` constraints## Summary
The work codebase uses `persistent` and `esqueleto`, and `esqueleto` defines a bunch of operators that overlap/conflict with the `persistent` ones. This has become enough of an issue that I'm working on creating an abstractio...## Summary
The work codebase uses `persistent` and `esqueleto`, and `esqueleto` defines a bunch of operators that overlap/conflict with the `persistent` ones. This has become enough of an issue that I'm working on creating an abstraction for them.
```haskell
(Persistent.=.) :: (PersistField typ) => EntityField rec typ -> typ -> Update rec
class SqlAssignment lhs rhs result where
(=.) :: lhs -> rhs -> result
instance
( PersistField typ, field ~ EntityField rec' typ', rec ~ rec', typ ~ typ'
) => SqlAssignment field typ (Persistent.Update rec) where
(=.) = (Persistent.=.)
```
While working on this, I ran into an issue where `Coercible` constraints aren't being inferred correctly for instances of a data family. We have several lines like:
```haskell
let fooId = coerce otherId
update fooId [FooName =. "hello"]
```
These lines compile fine with the `=.` from `persistent`, but fail with a "Couldn't match representation of type 'UUID' with that of 'Key Foo'` error.
`update` is a class member, given type:
```haskell
class PersistStoreWrite backend where
update :: forall record m. (MonadIO m, PersistRecordBackend record backend)
=> Key record -> [Update record] -> ReaderT backend m ()
```
So, here's my best guess:
GHC sees `update (coerce barId) [FooCount =. 1]`, which causes it to start Inferring things:
1. `FooCount :: EntityField Foo Int` - this is known.
2. `update :: Key rec -> [Update rec]` - this is known.
3. `FooCount =. 1` turns into a constraint `(Num a, SqlAssignment lhs a result)`.
4. The `update` causes `result` to be known as `Update Foo`, which is sufficient to select the `SqlAssignment lhs rhs (Persistent.Update rec)` instance.
5. This introduces some wanted constraints: `lhs ~ EntityField rec' typ'`, `rhs ~ typ'`, and finally `rec ~ rec'`. Crucially, we introduce these as *type equality constraints*.
6. `lhs ~ EntityField rec' typ'` is fine - we get `EntityField Foo Int`, which propagates to `rhs ~ tyc ~ Int` and `rec' ~ Foo ~ rec`, so we have inferred `Update Foo` as our `result` type.
7. Finally, to `update` - we have a type of `update :: (rec ~ Foo) => Key rec -> [Update rec]`. But our subexpression on the `update` is `coerce barId`.
8. `coerce barId` has a type `Coercible (Key Bar) r => r`. `Coercible` is a magically instantiated class, and something about how the `r ~ Foo` is provided as an instance constraint defeats how the class can be solved out.
## Steps to reproduce
Hey, fortunately a minimal reproducer fits in a single file!
```haskell
{-# language TypeFamilies, TypeApplications, GADTs, FunctionalDependencies, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses #-}
module Lib where
import Data.Coerce
import Data.Proxy
update :: Key a -> [Proxy a] -> IO ()
update _ _ = pure ()
data User
data family Key a
newtype instance Key User = UserKey String
(=.) :: p a -> b -> Proxy a
(=.) _ _ = Proxy
class SqlAssignment lhs result where
assignment :: proxy lhs -> rhs -> Proxy result
instance (rec ~ rec') => SqlAssignment rec rec' where
assignment = (=.)
-- wtf
assignmentNoClass :: (rec ~ rec') => proxy rec -> b -> Proxy rec'
assignmentNoClass = assignment
userName :: Proxy User
userName = Proxy
someFunc :: IO ()
someFunc = do
-- works: no class on `=.`
update (coerce "hello") [userName =. "asdf"]
-- works: type annotation on `coerce`
update (coerce "asdf" :: Key User) [userName `assignment` "asdf"]
-- works: somehow adding a top-level non-class-member makes this ok???
update (coerce "asdf") [userName `assignmentNoClass` "asdf"]
-- works: type signature on result of `assignment`
update (coerce "asdf") [userName `assignment` "asdf" :: Proxy User]
-- does not work
update (coerce "asdf") [userName `assignment` "asdf"]
```
The data family appears to be relevant, here - given a `newtype Key a = Key String`, GHC is always able to deduce the `Coercible (Key a) String`. So I think the issue must be related to the data family in particular - just knowing `(a ~ User)` isn't enough to "unlock" that `Coercible (Key User) String` is valid, since that's a `newtype`. But literally any other type hint brings that information into scope.
## Expected behavior
I expect that GHC can solve a `Coercible a b` constraint when `b` is known, even if that knowledge comes about through type equality constraints from instance resolution.
## Environment
* GHC version used: 8.10.7, 9.0.2, 9.2.7, 9.4.5, 9.6.1
Optional:
* Operating System: Ubuntu
* System Architecture: x86https://gitlab.haskell.org/ghc/ghc/-/issues/23401Removing errors from the zonker2023-05-23T13:51:38Zsheafsam.derbyshire@gmail.comRemoving errors from the zonkerIt seems to me that we don't want the zonker to add error messages. One motivation is that, when reporting an error, we rely on an action stored in
```haskell
type ErrCtxt = (Bool, TidyEnv -> TcM (TidyEnv, SDoc))
```
In practice, these...It seems to me that we don't want the zonker to add error messages. One motivation is that, when reporting an error, we rely on an action stored in
```haskell
type ErrCtxt = (Bool, TidyEnv -> TcM (TidyEnv, SDoc))
```
In practice, these actions **only** do zonking and tidying; it seems the inner action should not be adding errors, while we are already reporting an error. If we remove the ability for the zonker to emit errors, then we avoid this problem.
Currently, the only error we throw in the zonker is when we can't default a concrete type variable. This comes from cases like
```haskell
f1 :: forall r s (a :: TYPE (r s)). a -> ()
f1 = f1
g1 h = f1 (h ())
f2 :: forall r s t u (a :: TYPE (r s t u)). a -> ()
f2 = f1
g2 h = f2 (h ())
```
The issue is that we create concrete metavariables `r[conc]`, `s[conc]`, `t[conc]`, `u[conc]`, but because they don't have kind `RuntimeRep` we don't know how to default them.
However, I would want to say:
- for `g1`, we can default `r[conc] s[conc]` as a whole to `BoxedRep Lifted` (even though technically it could be something else, like `r ~ VecRep Vec2`, `s ~ DoubleElemRep`).
- for `f2`, there is no way to unify `r s t u` with a concrete `RuntimeRep`, so we should emit a kind error in `f2` (before we even get to `g2`).
If we implement some logic like this, I imagine we could remove the error.https://gitlab.haskell.org/ghc/ghc/-/issues/23390setLclEnv in solveForAll should be restoreLclEnv2023-05-18T07:31:59ZMatthew PickeringsetLclEnv in solveForAll should be restoreLclEnvI am pretty sure that the `setLclEnv` call in `solveForAll` should be a `restoreLclEnv` call.
See note "restoreLclEnv vs setLclEnv".
cc @simonpjI am pretty sure that the `setLclEnv` call in `solveForAll` should be a `restoreLclEnv` call.
See note "restoreLclEnv vs setLclEnv".
cc @simonpjhttps://gitlab.haskell.org/ghc/ghc/-/issues/23389Split up TcLclEnv to break module loop between GHC.Tc.Types.Constraint and GH...2023-06-05T20:00:10Zsheafsam.derbyshire@gmail.comSplit up TcLclEnv to break module loop between GHC.Tc.Types.Constraint and GHC.Tc.TypesCurrently, `TcLclEnv` stores a `WantedConstraints`, and each constraint `Ct` stores a `CtLoc` which stores a `TcLclEnv`. This means that `Ct` and `TcLclEnv` are mutually recursive, but it doesn't need to be that way as we only need a sub...Currently, `TcLclEnv` stores a `WantedConstraints`, and each constraint `Ct` stores a `CtLoc` which stores a `TcLclEnv`. This means that `Ct` and `TcLclEnv` are mutually recursive, but it doesn't need to be that way as we only need a subset of `TcLclEnv` for `Ct`s; I don't think we want this infinite nesting of contexts.
I suggest splitting up `TcLclEnv`, e.g.:
```haskell
data TcLclEnv
= TcLclEnv {
tcl_ctxt :: TcLclCtxt
tcl_lie :: TcRef WantedConstraints,
tcl_errs :: TcRef (Messages TcRnMessage),
tcl_usage :: TcRef UsageEnv,
}
data TcLclCtxt
= TcLclCtxt {
tcl_loc :: RealSrcSpan,
tcl_err_ctxt :: [ErrCtxt],
tcl_in_gen_code :: Bool,
tcl_tclvl :: TcLevel,
tcl_th_ctxt :: ThStage,
tcl_th_bndrs :: ThBindEnv,
tcl_arrow_ctxt :: ArrowCtxt,
tcl_rdr :: LocalRdrEnv,
tcl_env :: TcTypeEnv,
tcl_bndrs :: TcBinderStack,
}
```
The idea would be to put `TcLclCtxt` in its own module, lower down in the module hierarchy. It would be imported by both `GHC.Tc.Types` and `GHC.Tc.Types.Constraint`, but those latter two modules would no longer need to import each other.https://gitlab.haskell.org/ghc/ghc/-/issues/23371GHC enters endless loop in ghc 9.4 (fixed in ghc >= 9.6)2023-05-16T14:29:27ZMagnus ViernickelGHC enters endless loop in ghc 9.4 (fixed in ghc >= 9.6)## Summary
I was playing around with some constraints stuff and encountered a weird thing where the compiler (apparently) enters an endless loop when trying to add a `Show` instance. This is indeed an erroneous program, but I still don'...## Summary
I was playing around with some constraints stuff and encountered a weird thing where the compiler (apparently) enters an endless loop when trying to add a `Show` instance. This is indeed an erroneous program, but I still don't want the compiler enters an endless loop.
I hope this is no duplicate (didn't quite read through all 1000 issues that contain "loop")
## Steps to reproduce
```haskell
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}
module Has where
import Data.Functor.Identity (Identity (Identity))
import Data.Kind (Constraint, Type)
type Has :: forall k. (k -> Constraint) -> (k -> Type) -> k -> Type
data Has c f a where
Proves :: c a => f a -> Has c f a
type Top :: forall k. k -> Constraint
class Top a
instance Top a
class CFunctor c f | f -> c where
cfmap :: c b => (a -> b) -> f a -> (c b => f b -> r) -> r
instance CFunctor c (Has (c :: Type -> Constraint) f) where
cfmap f x k = k $ Proves (cfmap f x \(Proves y) -> y)
newtype Unconstrained f a = MkUnconstrained {getFunctor :: f a}
instance Functor f => CFunctor Top (Unconstrained f) where
cfmap f x k = k $ MkUnconstrained (f <$> getFunctor x)
deriving via (Unconstrained Identity) instance CFunctor Top Identity
-- instance Show (Has c f a) where
-- show = cfmap show
```
comment out the last two lines, ghci should hang
## Expected behavior
The compiler terminates.
## Environment
* GHC version used: 945
Optional:
- system: `"x86_64-linux"`
- host os: `Linux 6.3.1-zen1, NixOS, 23.05 (Stoat), 23.05.20230506.897876e`
## Additional information
- the issue does not occur with 961
- commenting out TypeFamilies causes a warning to be show by the `deriving via` declaration9.4.6sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23351Introduce a zonking monad to reduce inter-module dependencies2023-06-08T08:17:58Zsheafsam.derbyshire@gmail.comIntroduce a zonking monad to reduce inter-module dependenciesCurrently, zonking is done in the `TcM` monad, but it seems that only a very limited amount of functionality is needed:
1. `IO`, for reading and writing metavariables (obviously),
2. access to a logger for `traceTc` messages,
3. a...Currently, zonking is done in the `TcM` monad, but it seems that only a very limited amount of functionality is needed:
1. `IO`, for reading and writing metavariables (obviously),
2. access to a logger for `traceTc` messages,
3. ability to add error messages, e.g. as added by @monoidal's [commit adding an error when encountering a concrete metavariable in `zonkTcTypeToType`](https://gitlab.haskell.org/ghc/ghc/-/commit/0da18eb79540181ae9835e73d52ba47ec79fff6b)
So I think it would be good to introduce a slimmer version of the `TcM` monad which has just enough to be able to do zonking. I would like to ask @simonpj if that seems possible, or if there's something I'm missing which means that zonking indirectly needs access to full `TcM` functionality.
I would also like to remove the ability for zonking to add errors, as this zonking monad is (I believe) the monad we end up needing in the `ErrCtxt` type (defined currently in `GHC.Tc.Types`); it seems worthwhile to rule out any erroring operations and guarantee that the monad only supports reading/writing of metavariables (and logging).
My main motivation for this is to remove inter-module dependencies. This would make the module graph more parallelisable, increase modularity, and help avoid having so many `hs-boot` files.
Such a refactor would also facilitate the insertion of assertions that are only true "up to zonking".https://gitlab.haskell.org/ghc/ghc/-/issues/23344Backpack accepts invalid impredicativity in implementation of abstract data2023-05-15T22:33:56Zsheafsam.derbyshire@gmail.comBackpack accepts invalid impredicativity in implementation of abstract dataWhen checking that `type T = rhs` is a valid implementation of an abstract data declaration `data T`, backpack fails to check whether `rhs` contains any nested foralls, which means it accepts e.g.
```haskell
{-# LANGUAGE StandaloneKindS...When checking that `type T = rhs` is a valid implementation of an abstract data declaration `data T`, backpack fails to check whether `rhs` contains any nested foralls, which means it accepts e.g.
```haskell
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ImpredicativeTypes #-}
unit p where
module M where
import Data.Kind
type C :: Type -> Constraint
class C a where
type family F a :: Type
unit q where
dependency p
signature H where
data T
module N where
import M ( C(F) )
import H ( T )
instance C T where
type F T = T
unit r where
dependency p
module H where
import Data.Kind
type S :: Type -> Type
data S a = MkS
type T = S (forall (a :: Type). a -> a)
unit s where
dependency p
dependency r
dependency q[H=r:H]
```
There should be a check that mirrors the check that there are no type family applications in the RHS.sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23342Backpack: poor error message implementing abstract data with a forall type2023-05-15T22:33:56Zsheafsam.derbyshire@gmail.comBackpack: poor error message implementing abstract data with a forall typeBackpack currently accepts an abstract data type to be implemented as a forall or quantified type:
```haskell
unit p where
signature H where
data T1
data T2
data T3
unit q where
module H where
class C a where {}
...Backpack currently accepts an abstract data type to be implemented as a forall or quantified type:
```haskell
unit p where
signature H where
data T1
data T2
data T3
unit q where
module H where
class C a where {}
data S
type T1 = forall a. a -> a
type T2 = forall a. C a => a
type T3 = C S => S -> S
unit r where
dependency q
dependency p[H=q:H]
```
We get errors like the following:
```
* Type constructor `T3' has conflicting definitions in the module
and its hsig file
Main module: type T3 :: *
type T3 = C S => S -> S
Hsig file: type T3 :: *
data T3
```
It doesn't specify what the issue is (that a quantified type is not allowed in the RHS of the type synonym implementing the abstract datatype).sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23333Swapping arguments of type comparison operator ~ induces a type error2023-09-13T12:23:20ZMikolaj KonarskiSwapping arguments of type comparison operator ~ induces a type error## Summary
Edit2: see later comments for an even smaller repro.
Edit: a minimal repro is at https://play.haskell.org/saved/EtiAllWh (uncomment the bit swapping `~` arguments to make it fail)
The following commit, swapping arguments of...## Summary
Edit2: see later comments for an even smaller repro.
Edit: a minimal repro is at https://play.haskell.org/saved/EtiAllWh (uncomment the bit swapping `~` arguments to make it fail)
The following commit, swapping arguments of an application of the type comparison operator `~` induces, a type error. No plugins are used in this file.
https://github.com/Mikolaj/horde-ad/commit/3905cf0515ce5ce2723b4b0140184e4c8dcc9599
## Steps to reproduce
Compile with and without this commit, using `cabal build -j1` (for GHC 9.6 add `--allow-newer`). It should compile fine without the commit and with it it should fail emitting
```
simplified/HordeAd/Core/AstInterpret.hs:200:16: error: [GHC-05617]
• Could not deduce ‘BooleanOf (Ranked (Primal a) n)
~ BooleanOf (IntOf a)’
from the context: InterpretAst a
bound by the type signature for:
interpretAstBool :: forall a.
InterpretAst a =>
AstEnv a
-> AstMemo a
-> AstBool (ScalarOf a)
-> (AstMemo a, BooleanOf (Primal a))
at simplified/HordeAd/Core/AstInterpret.hs:(190,1)-(192,77)
Expected: BooleanOf (Primal a)
Actual: BooleanOf (Ranked (Primal a) n)
NB: ‘BooleanOf’ is a non-injective type family
• In the expression: interpretAstRelOp opCodeRel args2
In the expression: (memo2, interpretAstRelOp opCodeRel args2)
In the expression:
let (memo2, args2) = mapAccumR (interpretAstPrimal env) memo args
in (memo2, interpretAstRelOp opCodeRel args2)
• Relevant bindings include
memo2 :: AstMemo a
(bound at simplified/HordeAd/Core/AstInterpret.hs:199:10)
args2 :: [Ranked (Primal a) n]
(bound at simplified/HordeAd/Core/AstInterpret.hs:199:17)
args :: [AstPrimalPart n (ScalarOf a)]
(bound at simplified/HordeAd/Core/AstInterpret.hs:198:20)
memo :: AstMemo a
(bound at simplified/HordeAd/Core/AstInterpret.hs:193:22)
env :: AstEnv a
(bound at simplified/HordeAd/Core/AstInterpret.hs:193:18)
interpretAstBool :: AstEnv a
-> AstMemo a
-> AstBool (ScalarOf a)
-> (AstMemo a, BooleanOf (Primal a))
(bound at simplified/HordeAd/Core/AstInterpret.hs:193:1)
|
200 | in (memo2, interpretAstRelOp opCodeRel args2)
```
## Expected behavior
Compiles both with and without the commit.
## Environment
* GHC version used: 9.4.5 and 9.6.1
BTW, a different version of this code, one that does not require `QuantifiedConstraints` and has `forall`s in a very different place, is similarly fragile (flip argumenta in both `BooleanOf (IntOf a) ~ BooleanOf (Ranked (Primal a) n)` to make it fail): https://github.com/Mikolaj/horde-ad/blob/f40c4706657b80e8326468bb299456d319cce325/simplified/HordeAd/Core/AstInterpret.hs#L102-L1229.6.2https://gitlab.haskell.org/ghc/ghc/-/issues/23332panic! (the 'impossible' happened) GHC version 9.6.1: ltPSize Ranked2023-05-30T09:30:23ZMikolaj Konarskipanic! (the 'impossible' happened) GHC version 9.6.1: ltPSize Ranked## Summary
GHC 9.4.5 says
```
[17 of 22] Compiling HordeAd.Core.AstInterpret ( simplified/HordeAd/Core/AstInterpret.hs, /home/mikolaj/r/horde-ad/dist-newstyle/build/x86_64-linux/ghc-9.4.5/horde-ad-0.1.0.0/l/horde-ad-simplified/noopt/bu...## Summary
GHC 9.4.5 says
```
[17 of 22] Compiling HordeAd.Core.AstInterpret ( simplified/HordeAd/Core/AstInterpret.hs, /home/mikolaj/r/horde-ad/dist-newstyle/build/x86_64-linux/ghc-9.4.5/horde-ad-0.1.0.0/l/horde-ad-simplified/noopt/build/horde-ad-simplified/HordeAd/Core/AstInterpret.o, /home/mikolaj/r/horde-ad/dist-newstyle/build/x86_64-linux/ghc-9.4.5/horde-ad-0.1.0.0/l/horde-ad-simplified/noopt/build/horde-ad-simplified/HordeAd/Core/AstInterpret.dyn_o ) [Source file changed]
simplified/HordeAd/Core/AstInterpret.hs:102:10: error:
• Illegal nested constraint ‘c (Ranked r y)’
(Use UndecidableInstances to permit this)
• In the instance declaration for ‘CRanked2 c r’
|
102 | instance (forall y. KnownNat y => c (Ranked r y)) => CRanked2 c r where
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: cabal: Failed to build lib:horde-ad-simplified from horde-ad-0.1.0.0
(which is required by test:shortTestForCISimplified from horde-ad-0.1.0.0,
test:extremelyLongTestSimplified from horde-ad-0.1.0.0 and others).
```
while GHC 9.6.1 panics
```
[17 of 22] Compiling HordeAd.Core.AstInterpret ( simplified/HordeAd/Core/AstInterpret.hs, /home/mikolaj/r/horde-ad/dist-newstyle/build/x86_64-linux/ghc-9.6.1/horde-ad-0.1.0.0/l/horde-ad-simplified/noopt/build/horde-ad-simplified/HordeAd/Core/AstInterpret.o, /home/mikolaj/r/horde-ad/dist-newstyle/build/x86_64-linux/ghc-9.6.1/horde-ad-0.1.0.0/l/horde-ad-simplified/noopt/build/horde-ad-simplified/HordeAd/Core/AstInterpret.dyn_o )
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.6.1:
ltPSize
Ranked
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:189:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Tc/Utils/TcType.hs:2431:5 in ghc:GHC.Tc.Utils.TcType
CallStack (from HasCallStack):
panic, called at compiler/GHC/Utils/Error.hs:454:29 in ghc:GHC.Utils.Error
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
Error: cabal: Failed to build lib:horde-ad-simplified from horde-ad-0.1.0.0
(which is required by test:shortTestForCISimplified from horde-ad-0.1.0.0,
test:extremelyLongTestSimplified from horde-ad-0.1.0.0 and others).
```
This may or may not be related to https://gitlab.haskell.org/ghc/ghc/-/issues/23323
## Steps to reproduce
Compile
https://github.com/Mikolaj/horde-ad/commit/2f463b2d10e697dcccc65bc61633e63e3ea2418d
with `cabal build -j1` (adding `--allow-newer` for GHC 9.6.1).
## Expected behavior
No panichttps://gitlab.haskell.org/ghc/ghc/-/issues/23323Regression in GHC 9.6.1: spurious "Redundant constraint", where the constrain...2023-09-28T08:19:10ZMikolaj KonarskiRegression in GHC 9.6.1: spurious "Redundant constraint", where the constraint is inside a quantified constraint## Summary
GHC 9.6.1 with this commit
https://github.com/Mikolaj/horde-ad/commit/0152cfac4569ade762e4aa0bd7fda661ee94a6f5
and `cabal test simplifiedOnlyTest` [Edit: and `--allow-newer`] emit hundreds of `Redundant constraint: KnownNat...## Summary
GHC 9.6.1 with this commit
https://github.com/Mikolaj/horde-ad/commit/0152cfac4569ade762e4aa0bd7fda661ee94a6f5
and `cabal test simplifiedOnlyTest` [Edit: and `--allow-newer`] emit hundreds of `Redundant constraint: KnownNat x` warnings that are wrong and refer to one of these three `x` variables:
https://github.com/Mikolaj/horde-ad/blob/0152cfac4569ade762e4aa0bd7fda661ee94a6f5/simplified/HordeAd/Core/AstInterpret.hs#L118C2-L120
OTOH, GHC 9.4.5 [Edit: with no `--allow-newer`]. compiles a very similar commit (the reason it can't compile the same commit will be described in another ticket)
https://github.com/Mikolaj/horde-ad/commit/da16d0d4650f96e70917ea39dc830bd39c103734
without even a single such warning. The supposedly redundant constraints are necessary to compile the code, under both GHC versions.
## Steps to reproduce
Clone and check out the commits, build, inspect the log.
## Expected behavior
I'd expect no such warning.
## Environment
* GHC version used: 9.6.1 vs 9.4.5
BTW, I have reasons to suspect GHC 9.4.5 can't specialize this code (e.g., it executes it slower) and that, if it would, it would complain similarly. So GHC 9.6.1 may be more correct under the hood, though the spurious warning makes it appear as a regression in behaviour.
Edit: if that helps, here's a commit that exhibits the same behaviour as above, but works for both GHC 9.4.5 and 9.6.1: https://github.com/Mikolaj/horde-ad/commit/c65e21b671edc94d492a1f9c928afa0ac1465de0
Edit2: and here is yet another one that does not require `ImpredicativeTypes`: https://github.com/Mikolaj/horde-ad/commit/bc734c7dbe11daeb98b377872f6f25e63c73dd34sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23321Panic on piResultTys12023-05-02T15:39:25ZRodrigo MesquitaPanic on piResultTys1I've come across a GHC panic which I wasn't able to reproduce after I cleaned cabal's build directory.
Unfortunately there might not be much to do about this except for a quick audit of the code that might lead to the bug.
Otherwise, I...I've come across a GHC panic which I wasn't able to reproduce after I cleaned cabal's build directory.
Unfortunately there might not be much to do about this except for a quick audit of the code that might lead to the bug.
Otherwise, I think we can close this until it comes up in a reproducible environment.
I just thought it might be useful to at least report.
```
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.4.4:
piResultTys1
Type
[MappedBuffer]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:182:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Core/Type.hs:1397:5 in ghc:GHC.Core.Type
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```https://gitlab.haskell.org/ghc/ghc/-/issues/23308Panic on malformed newtype2023-05-18T20:00:47ZPedro MiniczPanic on malformed newtypeThe following causes a panic on GHC 9.6.1:
```haskell
data A = A !B
newtype B = B C C
data C = C A
```
Result:
```text
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.6.1:
mkNewTyConRhs
B [C, C...The following causes a panic on GHC 9.6.1:
```haskell
data A = A !B
newtype B = B C C
data C = C A
```
Result:
```text
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.6.1:
mkNewTyConRhs
B [C, C]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:189:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Tc/TyCl/Build.hs:70:27 in ghc:GHC.Tc.TyCl.Build
CallStack (from HasCallStack):
panic, called at compiler/GHC/Utils/Error.hs:454:29 in ghc:GHC.Utils.Error
```
GHC versions 9.4.5 and 9.2.5 do not panic and report the error correctly. I haven't tested other versions.
This is similar to #15523.sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23258-fdefer-typed-holes will raise "(deferred type error)" exception, and that na...2023-06-10T12:20:55Zjwaldmann-fdefer-typed-holes will raise "(deferred type error)" exception, and that name looks wrongwith ghc-9.6.1,
```
:set -fdefer-typed-holes
ghci> x = [True,_] -- gives warning, as expected
ghci> print x
[True,*** Exception: <interactive>:11:11: error: [GHC-88464]
...
(deferred type error)
```
that last line looks wrong to me, s...with ghc-9.6.1,
```
:set -fdefer-typed-holes
ghci> x = [True,_] -- gives warning, as expected
ghci> print x
[True,*** Exception: <interactive>:11:11: error: [GHC-88464]
...
(deferred type error)
```
that last line looks wrong to me, since there is no type error. Documentation says "a hole ... will behave like undefined", and for that I would get no type error.