GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2024-03-14T09:09:32Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/24508Do not emit `-Winaccessible-code` warnings when the pattern-match checker wou...2024-03-14T09:09:32ZSebastian GrafDo not emit `-Winaccessible-code` warnings when the pattern-match checker would warn as wellhttps://discourse.haskell.org/t/inaccessible-vs-redundant-warnings-in-gadt-pattern-matching/8952 had one more user confused by the apparent redundancy of `-Winaccessible-code` warnings with those of the pattern-match checker.
In https:/...https://discourse.haskell.org/t/inaccessible-vs-redundant-warnings-in-gadt-pattern-matching/8952 had one more user confused by the apparent redundancy of `-Winaccessible-code` warnings with those of the pattern-match checker.
In https://gitlab.haskell.org/ghc/ghc/-/issues/19428 I proposed to deprecate `-Winaccessible-code` for this reason, but @RyanGlScott correctly pointed out that there are inaccessible code warnings that have no equivalent in the pattern-match checker.
So in this ticket, I instead propose not to generate `-Winaccessible-code` warnings inside patterns.https://gitlab.haskell.org/ghc/ghc/-/issues/24494A type equality constraint is necessary despite GHC warning that it's redundant2024-03-05T17:42:19ZMikolaj KonarskiA type equality constraint is necessary despite GHC warning that it's redundant## Summary
The first [type equality](https://github.com/Mikolaj/horde-ad/blob/b42aeabc0cb9fdbc8933ddd444143d008a5b986f/src/HordeAd/Core/Engine.hs#L308) in this type signature
```hs
cfwd
:: forall r y f vals advals.
( RankedOf f ...## Summary
The first [type equality](https://github.com/Mikolaj/horde-ad/blob/b42aeabc0cb9fdbc8933ddd444143d008a5b986f/src/HordeAd/Core/Engine.hs#L308) in this type signature
```hs
cfwd
:: forall r y f vals advals.
( RankedOf f ~ Flip OR.Array
, AdaptableHVector (ADVal (Flip OR.Array)) advals
, AdaptableHVector (ADVal (Flip OR.Array)) (ADVal f r y)
, AdaptableHVector (Flip OR.Array) vals
, AdaptableHVector (Flip OR.Array) (f r y)
, DualNumberValue advals, vals ~ DValue advals )
=> (advals -> ADVal f r y) -> vals -> vals -> f r y
```
is reported as redundant by GHC 9.8.1 (with both -O0 and -O1, with GHC 9.6.4 only with -O1) but the typing fails with the equality removed with
```
test/simplified/TestAdaptorSimplified.hs:1629:22: error: [GHC-40404]
• Reduction stack overflow; size = 201
When simplifying the following type:
Show
(HordeAd.Core.Delta.DeltaS
(ShapedOf
@GHC.TypeNats.Nat
(RankedOf
@[GHC.TypeNats.Nat]
(ShapedOf
@GHC.TypeNats.Nat
(RankedOf
@[GHC.TypeNats.Nat]
(ShapedOf
```
etc.
## Steps to reproduce
Checkout https://github.com/Mikolaj/horde-ad/blob/b42aeabc0cb9fdbc8933ddd444143d008a5b986f.
Run with GHC 9.8.1 or later (probably):
```
cabal test simplifiedOnlyTest -ftest_seq --test-options='-p 4Sin' --allow-newer --disable-optimization
```
After a dozen files tt should warn the equality is redundant and after another dozen it should start running the tests (all run fine). Remove the equality, run again, a few files later the error from above should pop up.
## Expected behavior
I have no idea if the type equality is really needed (or maybe a much weaker equality would be enough, e.g., `RankedOf (ShapedOf ranked) ~ ranked`?). I expect GHC to tell what it is so that I don't have to think.
## Environment
* GHC version used: 9.8.1 and 9.6.4https://gitlab.haskell.org/ghc/ghc/-/issues/24460Strange typechecking errors to do with Generics in a module with ANN and a ty...2024-02-27T15:12:18ZTeo CamarasuStrange typechecking errors to do with Generics in a module with ANN and a type error## Summary
This is a reproducer extracted from something we encountered in the wild.
Adding a new field to datatype led to a bunch of strange errors about `Generic`s.
In this minimal reproducer, the generics error is quite small, but i...## Summary
This is a reproducer extracted from something we encountered in the wild.
Adding a new field to datatype led to a bunch of strange errors about `Generic`s.
In this minimal reproducer, the generics error is quite small, but it becomes huge in any non-trivial example.
## Steps to reproduce
Compile the following module:
```
{-# LANGUAGE DeriveAnyClass #-}
module Repro where
import GHC.Generics
data IHaveNoFields = IHaveNoFields { } deriving (Generic)
getField
(IHaveNoFields field1 )
= field1
{-# ANN iHaveAnn ("" :: String) #-}
iHaveAnn = undefined
```
Here is the output:
```
Repro.hs:5:50: error:
• Couldn't match type: Rep IHaveNoFields
with: M1 i0 c0 (M1 i1 c1 U1)
Expected: Rep IHaveNoFields x
Actual: M1 i0 c0 (M1 i1 c1 U1) x
• In the expression: M1 (case x of IHaveNoFields -> M1 U1)
In an equation for ‘from’:
from x = M1 (case x of IHaveNoFields -> M1 U1)
When typechecking the code for ‘from’
in a derived instance for ‘Generic IHaveNoFields’:
To see the code I am typechecking, use -ddump-deriv
In the instance declaration for ‘Generic IHaveNoFields’
|
5 | data IHaveNoFields = IHaveNoFields { } deriving (Generic)
| ^^^^^^^
Repro.hs:5:50: error:
• Couldn't match type: Rep IHaveNoFields
with: M1 i2 c2 (M1 i3 c3 U1)
Expected: Rep IHaveNoFields x
Actual: M1 i2 c2 (M1 i3 c3 U1) x
• In the pattern: M1 x
In an equation for ‘to’:
to (M1 x) = case x of (M1 U1) -> IHaveNoFields
When typechecking the code for ‘to’
in a derived instance for ‘Generic IHaveNoFields’:
To see the code I am typechecking, use -ddump-deriv
In the instance declaration for ‘Generic IHaveNoFields’
|
5 | data IHaveNoFields = IHaveNoFields { } deriving (Generic)
| ^^^^^^^
Repro.hs:8:4: error:
• The constructor ‘IHaveNoFields’ should have no arguments, but has been given 1
• In the pattern: IHaveNoFields field1
In an equation for ‘getField’:
getField (IHaveNoFields field1) = field1
|
8 | (IHaveNoFields field1 )
|
```
## Expected behavior
This should error but should only output:
And indeed this is what we get if we comment out the `ANN` line.
```
Repro.hs:8:4: error:
• The constructor ‘IHaveNoFields’ should have no arguments, but has been given 1
• In the pattern: IHaveNoFields field1
In an equation for ‘getField’:
getField (IHaveNoFields field1) = field1
|
8 | (IHaveNoFields field1 )
| ^^^^^^^^^^^^^^^^^^^^
```
## Environment
* GHC version used: 9.4.8, 9.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/24425PartialTypeSignatures regression in 9.82024-03-11T09:00:53ZMatthías Páll GissurarsonPartialTypeSignatures regression in 9.8## Summary
There seems to be a regression in `-XPartialTypeSignatures`,
with GHC asking me to add a constraint to the context of an *inferred* type,
where as previously this constraint would have been inferred as well.
## Steps to repr...## Summary
There seems to be a regression in `-XPartialTypeSignatures`,
with GHC asking me to add a constraint to the context of an *inferred* type,
where as previously this constraint would have been inferred as well.
## Steps to reproduce
This compiles and runs fine in 9.6.3:
```
{-# LANGUAGE PartialTypeSignatures #-}
module Main where
checkFunc :: _ -> Bool
checkFunc f = f == 3
main :: IO ()
main = print (checkFunc 3)
```
```
$ ghc test.hs && ./test
[1 of 2] Compiling Main ( test.hs, test.o ) [Source file changed]
test.hs:4:14: warning: [GHC-88464] [-Wpartial-type-signatures]
• Found type wildcard ‘_’ standing for ‘Integer’
• In the type signature: checkFunc :: _ -> Bool
|
4 | checkFunc :: _ -> Bool
| ^
[2 of 2] Linking test [Objects changed]
$ ./test
True
```
but when compiled with 9.8.1:
```
$ ghc test.hs && ./test
[1 of 2] Compiling Main ( test.hs, test.o )
test.hs:5:17: error: [GHC-39999]
• No instance for ‘Eq a’ arising from a use of ‘==’
Possible fix:
add (Eq a) to the context of
the inferred type of checkFunc :: a -> Bool
• In the expression: f == 3
In an equation for ‘checkFunc’: checkFunc f = f == 3
|
5 | checkFunc f = f == 3
| ^^
test.hs:5:20: error: [GHC-39999]
• No instance for ‘Num a’ arising from the literal ‘3’
Possible fix:
add (Num a) to the context of
the inferred type of checkFunc :: a -> Bool
• In the second argument of ‘(==)’, namely ‘3’
In the expression: f == 3
In an equation for ‘checkFunc’: checkFunc f = f == 3
|
5 | checkFunc f = f == 3
|
```
## Expected behavior
I would expect it to compile as it did in 9.6.
## Environment
* GHC version used: 9.6.3, 9.8.1
Optional:
* Operating System: Ubuntu 22.04
* System Architecture: WSL2https://gitlab.haskell.org/ghc/ghc/-/issues/24405polymorphic instantiation of universally quantified types in type constructor...2024-02-07T12:25:02ZArtin Ghasivandghasivand.artin@gmail.compolymorphic instantiation of universally quantified types in type constructors gets accepted depending on the order of argumentsAssume we have the following definition:
```haskell
{-# LANGUAGE ImpredicativeTypes, GADTSyntax #-}
data T2 a b where
K2 :: a -> T2 a a
-- accepted
h1 :: T2 (forall c. c -> c) b -> (Char, Bool)
h1 (K2 x) = (x 'z', x True)
-- reject...Assume we have the following definition:
```haskell
{-# LANGUAGE ImpredicativeTypes, GADTSyntax #-}
data T2 a b where
K2 :: a -> T2 a a
-- accepted
h1 :: T2 (forall c. c -> c) b -> (Char, Bool)
h1 (K2 x) = (x 'z', x True)
-- rejected
h2 :: T2 b (forall c. c -> c) -> (Char, Bool)
h2 (K2 x) = (x 'z', x True)
```
`h2` gets rejected, while `h1` doesn't; when in fact, both of them should be rejected!
@simonpj @raehttps://gitlab.haskell.org/ghc/ghc/-/issues/24323Non-standalone deriving clause does not pick up superclass quantified coercib...2024-01-16T15:13:54ZShea Levyshea@shealevy.comNon-standalone deriving clause does not pick up superclass quantified coercible constraint## Summary
I have a case where a standalone deriving via typechecks but the non-standalone equivalent does not due to unknown roles, despite the derived class constraining the roles appropriately:
```haskell
{-# LANGUAGE DerivingVia #-...## Summary
I have a case where a standalone deriving via typechecks but the non-standalone equivalent does not due to unknown roles, despite the derived class constraining the roles appropriately:
```haskell
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE QuantifiedConstraints #-}
module Test where
import Control.Exception
import Data.Coerce
import Control.Monad.Trans.Reader
class (Monad m, forall x y. Coercible x y => Coercible (m x) (m y)) => MonadWith m where
stateThreadingGeneralWith
:: GeneralAllocate m SomeException releaseReturn b a
-> (a -> m b)
-> m (b, releaseReturn)
{-
newtype FooT m a = FooT (ReaderT Int m a) deriving newtype (Functor, Applicative, Monad) deriving MonadWith via ReaderT Int m
Test.hs:46:99: error:
• Couldn't match representation of type: m (GeneralAllocated
(ReaderT Int m) SomeException releaseReturn b a)
with that of: m (GeneralAllocated
(FooT m) SomeException releaseReturn b a)
arising from the coercion of the method ‘stateThreadingGeneralWith’
from type ‘forall releaseReturn b a.
GeneralAllocate (ReaderT Int m) SomeException releaseReturn b a
-> (a -> ReaderT Int m b) -> ReaderT Int m (b, releaseReturn)’
to type ‘forall releaseReturn b a.
GeneralAllocate (FooT m) SomeException releaseReturn b a
-> (a -> FooT m b) -> FooT m (b, releaseReturn)’
NB: We cannot know what roles the parameters to ‘m’ have;
we must assume that the role is nominal
• When deriving the instance for (MonadWith (FooT m))
|
46 | newtype FooT m a = FooT (ReaderT Int m a) deriving newtype (Functor, Applicative, Monad) deriving MonadWith via ReaderT Int m
| ^^^^^^^^^
Same issue with:
newtype FooT m a = FooT (ReaderT Int m a) deriving newtype (Functor, Applicative, Monad, MonadWith)
-}
newtype FooT m a = FooT (ReaderT Int m a) deriving newtype (Functor, Applicative, Monad)
deriving via ReaderT Int m instance (MonadWith m) => MonadWith (FooT m)
newtype GeneralAllocate m e releaseReturn releaseArg a
= GeneralAllocate ((forall x. m x -> m x) -> m (GeneralAllocated m e releaseReturn releaseArg a))
data GeneralAllocated m e releaseReturn releaseArg a = GeneralAllocated
{ allocatedResource :: !a
, releaseAllocated :: !(Either e releaseArg -> m releaseReturn)
}
instance (MonadWith m) => MonadWith (ReaderT r m) where
stateThreadingGeneralWith
:: forall a b releaseReturn
. GeneralAllocate (ReaderT r m) SomeException releaseReturn b a
-> (a -> ReaderT r m b)
-> ReaderT r m (b, releaseReturn)
stateThreadingGeneralWith (GeneralAllocate allocA) go = ReaderT $ \r -> do
let
allocA' :: (forall x. m x -> m x) -> m (GeneralAllocated m SomeException releaseReturn b a)
allocA' restore = do
let
restore' :: forall x. ReaderT r m x -> ReaderT r m x
restore' mx = ReaderT $ restore . runReaderT mx
GeneralAllocated a releaseA <- runReaderT (allocA restore') r
let
releaseA' relTy = runReaderT (releaseA relTy) r
pure $ GeneralAllocated a releaseA'
stateThreadingGeneralWith (GeneralAllocate allocA') (flip runReaderT r . go)
```
## Expected behavior
Both of these should behave the same, and should both work. I think this should also work with `deriving newtype` instead of having to specify the `via` type.
## Environment
* GHC version used: 9.2.4, 9.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/24299`tc_infer_hs_type` doesn't add module finalisers2024-03-28T14:05:28ZAndrei Borzenkov`tc_infer_hs_type` doesn't add module finalisers## Summary
I investigated https://gitlab.haskell.org/ghc/ghc/-/issues/23639 and found that `tc_hs_type` calls `addModFinalizersWithLclEnv` on untyped top-level splices, but `tc_infer_hs_type` does not. I found this behavior to be strang...## Summary
I investigated https://gitlab.haskell.org/ghc/ghc/-/issues/23639 and found that `tc_hs_type` calls `addModFinalizersWithLclEnv` on untyped top-level splices, but `tc_infer_hs_type` does not. I found this behavior to be strange and is likely a bug. After some investigation, I came up with a test case that exhibits the problem. Luckily, the fix for this bug should be a one line change.
## Steps to reproduce
```haskell
{-# LANGUAGE TemplateHaskell #-}
module T where
import Language.Haskell.TH.Syntax (addModFinalizer, runIO)
import GHC.Types (Type)
type Proxy :: forall a. a -> Type
data Proxy a = MkProxy
check :: ($(addModFinalizer (runIO (putStrLn "check")) >>
[t| Proxy |]) :: Type -> Type) Int -- There is kind signature, we are in check mode
check = MkProxy
infer :: ($(addModFinalizer (runIO (putStrLn "infer")) >>
[t| Proxy |]) ) Int -- no kind signature, inference mode is enabled
infer = MkProxy
```
Attempt to compile this code will result in the following stdout:
```
$ ghc T.hs -fforce-recomp
[1 of 1] Compiling T ( T.hs, T.o )
check
```
## Expected behavior
```
$ ghc T.hs -fforce-recomp
[1 of 1] Compiling T ( T.hs, T.o )
check
infer
```
## Environment
* GHC version used: masterAndrei BorzenkovAndrei Borzenkovhttps://gitlab.haskell.org/ghc/ghc/-/issues/24279Make Constraint and Type apart, in Core2024-02-05T17:53:13ZOleg GrenrusMake Constraint and Type apart, in CoreI'm running into issues related to this and https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0032-constraint-vs-type.rst doesn't do it for me fully.
TL;DR My use case is kind of implementing something like `TypeRep`,...I'm running into issues related to this and https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0032-constraint-vs-type.rst doesn't do it for me fully.
TL;DR My use case is kind of implementing something like `TypeRep`, and I need to be able to tell `Type` and `Constraint` apart. I can now, because `CONSTRAINT` and `TYPE` are apart, but could not in GHC-9.4. I consider this to be lucky coincidence, but also wrong. `TYPE` and `CONSTRAINT` are apart, but `TYPE LiftedRep` and `CONSTRAINT LiftedRep` are not.
```
{-# LANGUAGE GHC2021, DataKinds, TypeFamilies #-}
import GHC.Exts
type family Equals a b where
Equals a a = True
Equals a b = False
type Ex1 = Equals TYPE CONSTRAINT
type Ex2 = Equals (TYPE LiftedRep) (CONSTRAINT LiftedRep)
{-
This is not right:
*Main> :kind! Ex1
Ex1 :: Bool
= False
*Main> :kind! Ex2
Ex2 :: Bool
= Equals (*) Constraint
-}
```
---
I think that `Type` and `Constraint` should be nominally distinct in Core, but could have the same representation, i.e. using casts to make types align, but make the abstraction zero cost.https://gitlab.haskell.org/ghc/ghc/-/issues/24260Coercion application broken by newtype constructor2023-12-19T15:18:57ZmniipCoercion application broken by newtype constructor## Summary
In core-spec there's an inference rule for applying a coercion to an argument (Co_AppCo) that amounts to the following haskell type:
```hs
coAppCo :: Coercion f g -> x :~: y -> Coercion (f x) (g y)
```
and indeed the type-c...## Summary
In core-spec there's an inference rule for applying a coercion to an argument (Co_AppCo) that amounts to the following haskell type:
```hs
coAppCo :: Coercion f g -> x :~: y -> Coercion (f x) (g y)
```
and indeed the type-checker is able to use this rule since the following implementation type-checks:
```hs
coAppCo Coercion Refl = Coercion
```
However, if we specialize the type signature by substituting `f` and `g` with uses of a newtype type constructor whose data constructor is not in scope, the implementation fails.
```hs
import Control.Monad.ST (ST)
coAppCo' :: Coercion (ST s) (ST s') -> x :~: y -> Coercion (ST s x) (ST s' y)
coAppCo' Coercion Refl = Coercion
<interactive>:12:26: error: [GHC-18872]
• Couldn't match representation of type: ST s x
with that of: ST s' x
arising from a use of ‘Coercion’
The data constructor ‘GHC.ST.ST’ of newtype ‘ST’ is not in scope
• In the expression: Coercion
In an equation for ‘coAppCo'’: coAppCo' Coercion Refl = Coercion
• Relevant bindings include
coAppCo' :: Coercion (ST s) (ST s')
-> (x :~: y) -> Coercion (ST s x) (ST s' y)
(bound at <interactive>:12:1)
```
Note that an implementation that simply delegates to the more general version (`coAppCo' = coAppCo`) type-checks just fine. Likewise if instead of `ST` I use something that is not a newtype, it also type-checks just fine.
## Steps to reproduce
```hs
import Control.Monad.ST (ST)
import Data.Type.Coercion
import Data.Type.Equality
coAppCo' :: Coercion (ST s) (ST s') -> x :~: y -> Coercion (ST s x) (ST s' y)
coAppCo' Coercion Refl = Coercion
```
## Expected behavior
`coAppCo'` should type-check
## Environment
* GHC version used: 9.6.2https://gitlab.haskell.org/ghc/ghc/-/issues/24257Implicit param allowed, but doesn't work.2023-12-19T15:53:25ZOleg GrenrusImplicit param allowed, but doesn't work.ImplicitParams are awkward, I think it's awkward that they are `Constraint`s.
They are not allowed as superclasses (makes sense, but then not really):
```haskell
Prelude> :set -XConstraintKinds -XUndecidableSuperClasses -XImplicitParam...ImplicitParams are awkward, I think it's awkward that they are `Constraint`s.
They are not allowed as superclasses (makes sense, but then not really):
```haskell
Prelude> :set -XConstraintKinds -XUndecidableSuperClasses -XImplicitParams -XAllowAmbiguousTypes
Prelude> class (?foo :: Int) => Foo a where
<interactive>:22:1: error:
• Illegal implicit parameter ‘?foo::Int’
• In the context: ?foo::Int
While checking the super-classes of class ‘Foo’
In the class declaration for ‘Foo’
```
However, one can "work-around" that, by tricking GHC, making syntactic `?foo` not so obvious to the compiler:
```haskell
Prelude> class c => Id c where
Prelude> class (c, c ~ (?foo :: Int)) => Id c where bar :: Int; bar = ?foo
```
That is accepted.
But (not so obviously) it doesn't work:
```haskell
Prelude> let ?foo = 42 :: Int in bar @(?foo :: Int)
<interactive>:9:25: error: [GHC-39999]
• Could not deduce ‘Id (?foo::Int)’ arising from a use of ‘bar’
from the context: ?foo::Int
bound by the implicit-parameter binding for ?foo
at <interactive>:9:1-42
• In the expression: bar @(?foo :: Int)
In the expression: let ?foo = 42 :: Int in bar @(?foo :: Int)
In an equation for ‘it’:
it = let ?foo = 42 :: Int in bar @(?foo :: Int)
```
I feel that GHC should error earlier. It's the `Id`s class (or rather `bar`) definition which is wrong already.https://gitlab.haskell.org/ghc/ghc/-/issues/24201Tidy up Do Expansion implimentation/Kill `GHC.Types.Basic.Origin`2024-02-15T15:32:43ZApoorv IngleTidy up Do Expansion implimentation/Kill `GHC.Types.Basic.Origin`This ticket tracks various tidying up tasks for HsExpansion
Here are some ideas:
1. Get rid `Origin` to beautify and stream line the `Generated` code vs `FromSource` Code meta-data.
See discussion here: https://gitlab.haskell.org/ghc/gh...This ticket tracks various tidying up tasks for HsExpansion
Here are some ideas:
1. Get rid `Origin` to beautify and stream line the `Generated` code vs `FromSource` Code meta-data.
See discussion here: https://gitlab.haskell.org/ghc/ghc/-/merge_requests/10140#note_535779
The current design depends on `GHC.Types.Basic.Origin` and also `GHC.Types.SrcLoc.GenLocated` to figure out whether a source code's origin is user written or not.
The objective is that we should only be using one thing to identify the source codes origin. The current `tcExpr` already uses `GHC.Types.SrcLoc.GenLocated` to identify the src origin using `isGeneratedCode :: TcRn Bool` and we would be able to reuse that functionality rather than depending on `GHC.Types.Basic.Origin`.
2. Kill `GenReason` in `GHC.Types.Basic.Origin` and clean up smelly code like this one in [GHC.HstoCore.Match.matchWrapper](https://gitlab.haskell.org/ghc/ghc/-/blob/master/compiler/GHC/HsToCore/Match.hs#L773)
```haskell
= do { dflags <- getDynFlags
; locn <- getSrcSpanDs
; let matches
= if any (is_pat_syn_match origin) matches'
then filter (non_gen_wc origin) matches'
-- filter out the wild pattern fail alternatives
-- which have a do expansion origin
-- They generate spurious overlapping warnings
-- Due to pattern synonyms treated as refutable patterns
-- See Part 1's Wrinkle 1 in Note [Expanding HsDo with XXExprGhcRn] in GHC.Tc.Gen.Do
```Apoorv IngleApoorv Inglehttps://gitlab.haskell.org/ghc/ghc/-/issues/24069GHCi 9.8 includes solved class contraints when printing `:type`2023-10-12T16:23:37ZZubinGHCi 9.8 includes solved class contraints when printing `:type`
```haskell
-- 9.6
λ> :type show @Int
show @Int :: Int -> String
-- 9.8
λ> :type show @Int
show @Int :: Show Int => Int -> String
```
```haskell
-- 9.6
λ> :type show @Int
show @Int :: Int -> String
-- 9.8
λ> :type show @Int
show @Int :: Show Int => Int -> String
```ZubinZubinhttps://gitlab.haskell.org/ghc/ghc/-/issues/24065panic: Given constraint without given origin2023-10-10T14:18:53ZRodrigo Mesquitapanic: Given constraint without given origin## Summary
During compilation of a backpack heavy library I get the following error:
```
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.6.2:
Given constraint without given origin
$dApplicative_aafq
...## Summary
During compilation of a backpack heavy library I get the following error:
```
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.6.2:
Given constraint without given origin
$dApplicative_aafq
arising when attempting to show that
instance [safe] Applicative m => Applicative (CommandM m)
-- Defined in ‘Ghengin.Vulkan.Renderer.Command’
is provided by ‘Ghengin.Vulkan.Renderer.Command’
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/Solver/Canonical.hs:600:31 in ghc:GHC.Tc.Solver.Canonical
CallStack (from HasCallStack):
panic, called at compiler/GHC/Utils/Error.hs:454:29 in ghc:GHC.Utils.Error
```
Unfortunately, my reproducer is *far* from minimal.
It's reproducible by cloning at a particular commit a considerably large project...
Nonetheless, I figured I should report it.
## Steps to reproduce
```
git clone https://github.com/alt-romes/ghengin.git && cd ghengin
git checkout 2e007f0c9bf88018db424d11c96b2de9b0b4d14a
cabal build ghengin-core
```
## Environment
* GHC version used: 9.6.2
Optional:
* Operating System: macOS
* System Architecture: M2 / Aarch64https://gitlab.haskell.org/ghc/ghc/-/issues/24059Some type family applications in instances are fine actually2023-10-10T14:30:23ZGergő ÉrdiSome type family applications in instances are fine actuallyA typeclass instance that uses a type family is currently rejected unconditionally by GHC. But I believe there are special cases where it should be fine to accept them.
The basic idea is to think about the simplest possible case: if the...A typeclass instance that uses a type family is currently rejected unconditionally by GHC. But I believe there are special cases where it should be fine to accept them.
The basic idea is to think about the simplest possible case: if the type family is closed and the application is completely monomorphic. In this case, writing something like `instance C (F Int Bool) where ...` should really mean exactly the same as if `F Int Bool` was manually expanded by the user.
But I think we can go further, by classifying each type family parameter as whether the type family is parametric in that parameter. So something like
```
type family F a b where
F Int b = Maybe b
F Bool b = [b]
```
is not parametric in `a`, but is parametric in `b`. And so an instance `instance C (F Int x)` could, again, be expanded by the user manually into `instance C (Maybe x)`, so why not offer to do it for them.
For open type families, we can't mark any parameter as parametric, but it should still be fine to allow the degenerate case of fully monomorphic applications; after all, GHC already rejects conflicting type family instance declarations.https://gitlab.haskell.org/ghc/ghc/-/issues/24030Relax restrictions on required foralls2024-01-30T16:46:12ZKrzysztof GogolewskiRelax restrictions on required forallsWe now support `RequiredTypeArguments`, `forall a -> ty`.
The arrow `forall a -> ty` was created as a modification of `forall a. ty`. However, it has a lot of common with other types such as the normal function arrow, `a -> ty`. Require...We now support `RequiredTypeArguments`, `forall a -> ty`.
The arrow `forall a -> ty` was created as a modification of `forall a. ty`. However, it has a lot of common with other types such as the normal function arrow, `a -> ty`. Required foralls don't have implicit instantiation or generalization, a lot of complexity around implicit arguments disappears.
I think that `forall a -> ty` should be treated as a tau-type rather than a sigma-type in GHC.
For example, given
```hs
myId :: forall a -> a -> a
myId = myId
single x = [x]
l = single myId
```
We want `l :: [forall a -> a -> a]`. Currently, typechecking `l` requires `ImpredicativeTypes`. But there should be no need for Quick Look inference. Contrast this with `single id`, where the type argument is implicit: it can be typed either as `forall a. [a -> a]` or `[forall a. a -> a]`.
Likewise, in Template Haskell we currently don't allow quantification, as this variant of T11452 shows:
```hs
{-# LANGUAGE RankNTypes, TemplateHaskell, RequiredTypeArguments, ExplicitNamespaces #-}
module T11452a where
impred :: forall a -> a -> a
impred = $$( [|| (\(type _) x -> x) :: (forall a -> a -> a) ||] )
```
But I think this should just work.
[Added later] One more example that I think should work:
```hs
f :: (forall a -> a) -> ()
f x = undefined x
g :: (forall a -> a) -> ()
g (undefined -> ()) = ()
```
`f` works only when `ImpredicativeTypes` are on; `g` doesn't work even with this flag.https://gitlab.haskell.org/ghc/ghc/-/issues/24022The documented FlexibleInstances grammar is incorrect and also out of date2023-10-03T17:19:23ZMarioThe documented FlexibleInstances grammar is incorrect and also out of date## Summary
The GHC User's Guide contains a simplified formal grammar of `instance` declarations in presence of `FlexibleInstances`:
https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/instances.html#formal-syntax-for-instanc...## Summary
The GHC User's Guide contains a simplified formal grammar of `instance` declarations in presence of `FlexibleInstances`:
https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/instances.html#formal-syntax-for-instance-declaration-types
The left-hand side of the production
```
arg_type ::= <empty>
| arg_type arg_types
```
therein is erroneous, it should be defining `arg_types` (plural) instead.
Another problem is that the grammar is out of date in that it doesn't allow type applications in instance head. This is legal nowadays:
```
type C :: forall k. k -> Constraint
class C a
instance C @Type Int
```
## Proposed improvements or changes
The missing letter `s` should definitely be inserted.
As for the type applications in instance heads, they should should be documented *somewhere*. I don't see them mentioned in the `TypeApplications` section. I'm not sure if the above-mentioned grammar is meant to showcase the full syntax of `instance` declarations with all extensions enabled, or only what `FlexibleInstances` brings. In the former case it should be extended with type applications, in the latter it doesn't need the infix operator case nor multiple class parameters.Ben GamariBen Gamarihttps://gitlab.haskell.org/ghc/ghc/-/issues/23972GHC-9.4 panics due to failing lookupIdSubst for KnownNat2023-09-19T19:09:46ZLars KuhtzGHC-9.4 panics due to failing lookupIdSubst for KnownNat## Summary
GHC panics when compiling the module that is shown below.
The issue happens with GHC-9.4 (tested with GHC 9.4.6 and 9.4.7) and optimization enabled (`-O1` and `-O2`) on all tested operating systems and platforms.
GHC-8.10.7...## Summary
GHC panics when compiling the module that is shown below.
The issue happens with GHC-9.4 (tested with GHC 9.4.6 and 9.4.7) and optimization enabled (`-O1` and `-O2`) on all tested operating systems and platforms.
GHC-8.10.7, GHC-9.2 and GHC-9.6 are not affected.
## Steps to reproduce
```hs
{-# LANGUAGE DataKinds #-}
module Bug where
import Numeric.Natural (Natural)
import GHC.TypeNats (KnownNat, natVal)
import Data.Proxy (Proxy(..))
newtype M (n :: Natural) = M Natural
-- Using a smaller value for `PC` makes the issue go away.
type PC :: Natural
type PC = 0x1_0000_0000_0000_0000
-- remove (or simplifying) one case makes the issue go away.
f :: forall n . KnownNat n => M n -> M n
f (M 0) = M 0
f (M x) = M (natVal @n Proxy + x)
-- removing one invocation of `f` makes the issue go away.
g :: KnownNat n => M n -> M n
g x = f (f x)
-- removing the let binding or one invocation of `g` makes the issue go away.
h :: M PC -> M PC
h x = let a = g (g x) in a
```
Compiling this module with GHC-9.4.7 and `-O1` or `-O2` as follows
```sh
ghc -O1 Bug.hs
```
Results in the output
```
[1 of 1] Compiling Bug ( Bug.hs, Bug.o ) [Source file changed]
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.4.7:
lookupIdSubst
$dKnownNat_sUW
InScope {wild_X2 z_anJ $krep_aQG $krep_aQH $krep_aQI $krep_aQJ
$krep_aQK h $tc'M $trModule $tcM f g $trModule_sUK $trModule_sUL
$trModule_sUM $trModule_sUN $krep_sUO $tcM_sUP $tcM_sUQ $krep_sUR
$tc'M_sUS $tc'M_sUT $sg_sV3}
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:182:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Core/Subst.hs:260:17 in ghc:GHC.Core.Subst
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
## Expected behavior
GHC compiles the module.
## Environment
The issue was reproduced with
* GHC-9.4.6 and GHC-9.6.7
* ubuntu/linux (amd64) and macOS (amd64 as well as aarch64).https://gitlab.haskell.org/ghc/ghc/-/issues/23970Odd interaction with TypeError, ImplicitParams, and constraints in scope2023-09-19T14:54:51ZparsonsmattOdd interaction with TypeError, ImplicitParams, and constraints in scope## Summary
The [`require-callstack`](https://hackage.haskell.org/package/require-callstack-0.2.0.0/docs/RequireCallStack.html) library provides a variant of `HasCallStack` that gets propagated like a normal constraint. This makes it eas...## Summary
The [`require-callstack`](https://hackage.haskell.org/package/require-callstack-0.2.0.0/docs/RequireCallStack.html) library provides a variant of `HasCallStack` that gets propagated like a normal constraint. This makes it easy to find callsites of a function and update them to also provide a callstack. A custom `TypeError` is used to provide a better error message for the end user.
However, there's some odd behavior. Consider this:
```haskell
someFunc :: RequireCallStack => IO ()
someFunc = do
errorRequireCallStack "asdf"
let bar = errorRequireCallStack "qwer"
bar
```
The first `errorRequireCallStack` picks up the `RequireCallStackImpl` in the constraint of `someFunc`, and is fine. However, the `let bar = errorRequireCallStack` triggers the `TypeError`.
If I remove the `TypeError` instance, then the code works fine, but missing `RequireCallStack` constraints only show the usual error message about a missing implicit parameter.
## Steps to reproduce
[This repository contains the code, in full](https://github.com/parsonsmatt/require-callstack-repro/blob/master/src/Lib.hs).
Clone the repository and run `cabal build`.
The code is short enough that I'll include it inline too:
```haskell
{-# language RankNTypes, TypeFamilies, KindSignatures, MultiParamTypeClasses, DataKinds, ConstraintKinds, ImplicitParams, UndecidableInstances, FlexibleContexts, FlexibleInstances #-}
{-# OPTIONS_GHC -Wno-orphans -Wno-missing-methods #-}
module Lib where
import Data.Kind
import GHC.Stack (HasCallStack)
import GHC.Classes (IP(..))
import GHC.TypeLits (TypeError, ErrorMessage(..))
-- The Problem:
--
-- GHC complains about `bar` with the `TypeError` in the `instance IP
-- "provideCallStack" ProvideCallStack`.
--
-- Removing the type error allows the program to compile without error.
--
-- Adding a type signature to `bar` that specifies `RequireCallStack` also
-- fixes the issue.
someFunc :: RequireCallStack => IO ()
someFunc = do
errorRequireCallStack "asdf"
let bar = errorRequireCallStack "qwer"
bar
alsoWeird :: IO ()
alsoWeird = provideCallStack $ do
-- `RequireCallStack` should be a satisfied constraint here, as
-- evidenced by this building:
someFunc
-- But we get an error in this let binding.
let bar = errorRequireCallStack "qwer"
bar
errorRequireCallStack :: RequireCallStack => String -> x
errorRequireCallStack = error
instance TypeError ('Text "Add RequireCallStack to your function context or use provideCallStack") => IP "provideCallStack" ProvideCallStack
type RequireCallStack = (HasCallStack, RequireCallStackImpl)
type RequireCallStackImpl = ?provideCallStack :: ProvideCallStack
data ProvideCallStack = ProvideCallStack
provideCallStack :: (RequireCallStackImpl => r) -> r
provideCallStack r = r
where
?provideCallStack = ProvideCallStack
```
You can work around the behavior by providing a type signature for `bar` or using `provideCallStack`:
```haskell
someFunc :: RequireCallStack => IO ()
someFunc = do
errorRequireCallStack "asdf"
let bar :: RequireCallStack => a
bar = errorRequireCallStack "qwer"
-- or,
bar = provideCallStack errorRequireCallStack "qwer"
bar
```
But both of these feel redundant with `RequireCallStack` already present in the constraint.
## Expected behavior
I would expect that a constraint like `RequireCallStack` is satisfied even in `let` bindings.
## Environment
* GHC version used: 8.10.7, 9.2.7, 9.6.2
Optional:
* Operating System: Ubuntu Unity
* System Architecture:https://gitlab.haskell.org/ghc/ghc/-/issues/23967Runtime Loop from QuantifiedConstraints and UndecidableInstances2023-09-29T01:57:52ZNathaniel BurkeRuntime Loop from QuantifiedConstraints and UndecidableInstances## Summary
This might be an already known bug (I realise there are quite a few other GHC issues mentioning loops related to superclasses) but I am not getting any `-Wloopy-superclass-solve` warnings GHC 9.6.2, which makes me think this ...## Summary
This might be an already known bug (I realise there are quite a few other GHC issues mentioning loops related to superclasses) but I am not getting any `-Wloopy-superclass-solve` warnings GHC 9.6.2, which makes me think this is distinct from the cases in https://gitlab.haskell.org/ghc/ghc/-/issues/20666.
## Steps to reproduce
Run the following program (Haskell Playground: https://play.haskell.org/saved/Bt2c9wRx). Note there is no explicit recursion anywhere in the code.
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Kind (Constraint)
class Bottom where
giveMeAString :: String
main :: IO ()
main = putStrLn (case veryBad of MkDict -> giveMeAString)
data Set = Empty | Russel
-- Note the perhaps more natural superclass constraints
-- `b ~ Empty => Bottom` or `forall t. In t Empty => Bottom`
-- do lead to loops at compile time
type In :: Set -> Set -> Constraint
class (In Russel Empty => Bottom) => In a b
instance (In t Russel, In t t) => In t Empty
instance (In t t => In t Empty) => In t Russel
data Dict a where
MkDict :: c => Dict c
bad :: Dict (In Russel Empty)
bad = MkDict
veryBad :: Dict Bottom
veryBad = case bad of MkDict -> MkDict
```
## Expected behavior
Either loop at compile time or give a specific error message. Indeed GHC 9.4.7 outputs:
```
Main.hs:21:10: error:
• Could not deduce Bottom
arising from the superclasses of an instance declaration
from the context: In t t => In t 'Void
bound by the instance declaration at Main.hs:21:10-45
or from: In 'Russel 'Void
bound by a quantified context at Main.hs:21:10-45
Possible fix: add Bottom to the context of the instance declaration
• In the instance declaration for ‘In t 'Russel’
|
21 | instance (In t t => In t Void) => In t Russel
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
## Environment
* GHC versions used: 9.6.2 and 9.8.1-alphahttps://gitlab.haskell.org/ghc/ghc/-/issues/23939Apparent violation of TcLevel invariant in T71732023-09-12T16:20:48Zsheafsam.derbyshire@gmail.comApparent violation of TcLevel invariant in T7173This is `T7173`:
```haskell
showEnv' env t = se 10 env t
where
se p env (Bind n b sc) = sb env n b
sb env n t = se 10 env t
data TT n = Bind n (TT n) (TT n)
```
In `GHC.Tc.Solver.decideQuantification`, if I collect ...This is `T7173`:
```haskell
showEnv' env t = se 10 env t
where
se p env (Bind n b sc) = sb env n b
sb env n t = se 10 env t
data TT n = Bind n (TT n) (TT n)
```
In `GHC.Tc.Solver.decideQuantification`, if I collect all metavariables and inspect their `TcLevel`s, say with a patch like the following
```diff
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index e9d59946d3..20326f4f63 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -1689,7 +1689,7 @@ decideQuantification
decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates
= do { -- Step 1: find the mono_tvs
; (candidates, co_vars, mono_tvs0)
- <- decidePromotedTyVars infer_mode name_taus psigs candidates
+ <- decidePromotedTyVars infer_mode rhs_tclvl name_taus psigs candidates
-- Step 2: default any non-mono tyvars, and re-simplify
-- This step may do some unification, but result candidates is zonked
@@ -1797,6 +1797,7 @@ Some rationale and observations
-}
decidePromotedTyVars :: InferMode
+ -> TcLevel
-> [(Name,TcType)]
-> [TcIdSigInst]
-> [PredType]
@@ -1818,7 +1819,7 @@ decidePromotedTyVars :: InferMode
--
-- Also return CoVars that appear free in the final quantified types
-- we can't quantify over these, and we must make sure they are in scope
-decidePromotedTyVars infer_mode name_taus psigs candidates
+decidePromotedTyVars infer_mode rhs_tclvl name_taus psigs candidates
= do { tc_lvl <- TcM.getTcLevel
; (no_quant, maybe_quant) <- pick infer_mode candidates
@@ -1833,7 +1834,18 @@ decidePromotedTyVars infer_mode name_taus psigs candidates
; return (psig_qtvs, psig_theta, taus) }
; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta
-
+ all_tvs = tyCoVarsOfTypesList (psig_tys ++ candidates ++ taus)
+
+ ; let bad_tvs = filter (\ tv -> isMetaTyVar tv && metaTyVarTcLevel tv `strictlyDeeperThan` rhs_tclvl) all_tvs
+ ; forM_ bad_tvs $ \ bad_tv ->
+ do { tv_contents <- TcM.readTcRef (metaTyVarRef bad_tv)
+ ; pprTraceM "decideQuantification: bad_tv" $
+ vcat [ text "curr_tclvl:" <+> ppr tc_lvl
+ , text "rhs_tclvl:" <+> ppr rhs_tclvl
+ , text "bad_tv:" <+> ppr bad_tv
+ , text "contents:" <+> ppr tv_contents ] }
+
+ ; let
-- (b) The co_var_tvs are tvs mentioned in the types of covars or
-- coercion holes. We can't quantify over these covars, so we
-- must include the variable in their types in the mono_tvs.
```
then we find that, when processing the outer `showEnv'` binding after having handled the recursive group `{se, sb}`, we see a metavariable that violates the `TcLevel` invariant:
```
decideQuantification: bad_tv
curr_tclvl: 0
rhs_tclvl: 1
bad_tv: p_aBU[tau:2]
contents: Flexi
```
That is, we're at `TcLevel` 1 but we encounter a metavariable with level 2!
It's perhaps a bit clearer to use named wildcards (with a patch like !10170 to be able to see the user-written variable names):
```haskell
showEnv' :: _env2 -> TT _n -> _res
showEnv' env t = se 10 env t
where
se :: Num _bad => _bad -> _env -> TT _n -> _res
se p env (Bind n b sc) = sb env n b
sb :: _env -> _n -> TT _n -> _res
sb env n t = se 10 env t
```
```
decideQuantification: bad_tv
curr_tclvl: 0
rhs_tclvl: 1
bad_tv: _bad_aBL[tau:2]
contents: Flexi
```
Note that, for some reason, if I change the metavariable `_env2` to `_env`, then the problem goes away.
I came across this while attempting to implement the defaulting plan in #20686. @simonpj @rae