GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-09-29T01:57:52Zhttps://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/23589Confusing error message "Could not deduce ‘(Bool :: Type) ~ (Bool :: Type)’"2024-02-08T11:24:09ZMikolaj KonarskiConfusing error message "Could not deduce ‘(Bool :: Type) ~ (Bool :: Type)’"[Edit: this commit fails on HEAD+head.hackage later than the original one and closer to the right place: https://github.com/Mikolaj/horde-ad/commit/999e4575c4e84638505abd26fba98965c4a50ffc]
[Edit2: a tentative summary after the first co...[Edit: this commit fails on HEAD+head.hackage later than the original one and closer to the right place: https://github.com/Mikolaj/horde-ad/commit/999e4575c4e84638505abd26fba98965c4a50ffc]
[Edit2: a tentative summary after the first couple dozen comments up to https://gitlab.haskell.org/ghc/ghc/-/issues/23589#note_511022: in GHC 9.4.5 the `Could not deduce Bool ~ Bool` message is a symptom that the workaround from https://gitlab.haskell.org/ghc/ghc/-/issues/14860#note_495352 doesn't work ~where it should work~[see below]; in GHC 9.6.2 the silly message only appears when the programmer abuses the workaround (uses it for type families of rank 2 instead of rank 1), so this is only an error message quality issue; in HEAD, compilation fails earlier when faced with the abuse and has a plausible error message, which however gives no hint that the abuse of a workaround is the underlying problem.]
[Edit3: Edsko confirms I've used the workaround wrongly even in the simpler examples where GHC 9.4.5 emits `Bool~Bool` --- I was quantifying over a variable that is involved in the resolution of the type family (appears in a type expression within the arity of the type family instead of later on). So the only problem is GHC reacting badly (with `Bool~Bool`) to an abuse of a workaround, which may or may not indicate deeper problems in GHC and certainly the error message could be improved.]
To reproduce, with GHC 9.6.2 do `cabal test simplifiedOnlyTest --disable-optimization -ftest_seq --allow-newer` on this commit
https://github.com/Mikolaj/horde-ad/commit/ac95ff02c660b95eb40a56ea8f38fbe25e3bb15b
The second error from the bottom will be presented with the following absurd error message. The extra kinds come from `-fprint-explicit-kinds`. I'm pretty sure I don't define any other `Bool` type in this repo.
```
test/tool/CrossTesting.hs:83:12: error: [GHC-39999]
• Could not deduce ‘(Bool :: Type) ~ (Bool :: Type)’
arising from the head of a quantified constraint
arising from a use of ‘interpretAst’
from the context: (KnownNat n, KnownNat m, ADReady AstRanked r,
InterpretAstR (Flip @{GHC.TypeNats.Nat} @{Type} OR.Array) r,
InterpretAstR
(ADVal
@GHC.TypeNats.Nat (Flip @{GHC.TypeNats.Nat} @{Type} OR.Array))
r,
(v :: Type)
~ (Flip @{GHC.TypeNats.Nat} @{Type} OR.Array r m :: Type),
(g :: Type)
~ (Flip @{GHC.TypeNats.Nat} @{Type} OR.Array r n :: Type))
bound by the type signature for:
rev' :: forall r (m :: GHC.TypeNats.Nat) (n :: GHC.TypeNats.Nat) v
g.
(KnownNat n, KnownNat m, ADReady AstRanked r,
InterpretAstR (Flip @{GHC.TypeNats.Nat} @{Type} OR.Array) r,
InterpretAstR
(ADVal
@GHC.TypeNats.Nat (Flip @{GHC.TypeNats.Nat} @{Type} OR.Array))
r,
(v :: Type)
~ (Flip @{GHC.TypeNats.Nat} @{Type} OR.Array r m :: Type),
(g :: Type)
~ (Flip @{GHC.TypeNats.Nat} @{Type} OR.Array r n :: Type)) =>
(forall (f :: Type -> GHC.TypeNats.Nat -> Type) x.
ADReady f x =>
f x n -> f x m)
-> g
-> (v, v, v, v, v, v, v, v, g, g, g, g, g, g, g, AstRanked r m,
AstRanked r m, v, v, v, v, v, v, v, v, v, v, v, v, v, v, g, g, g,
g, g, g, g, g, g, g, g, g, g, g)
at test/tool/CrossTesting.hs:(40,1)-(50,52)
or from: ADReady f1 r
bound by the type signature for:
h :: forall (f1 :: Type -> GHC.TypeNats.Nat -> Type).
ADReady f1 r =>
(f1 r m -> AstRanked r m)
-> (AstRanked r n -> f1 r n)
-> (AstRanked r m -> AstRanked r m)
-> Domains @{Type} (ADValClown OD.Array) r
-> ADVal
@GHC.TypeNats.Nat (Flip @{GHC.TypeNats.Nat} @{Type} OR.Array) r m
at test/tool/CrossTesting.hs:(76,7)-(79,36)
or from: GoodScalar rb41
bound by a quantified context at test/tool/CrossTesting.hs:83:12-23
• In the expression: interpretAst env (gx ast)
In the expression:
let
(var, ast) = funToAstR (tshape vals) (fx1 . f . fx2)
env = extendEnvR var (parseDomains vals inputs) EM.empty
in interpretAst env (gx ast)
In an equation for ‘h’:
h fx1 fx2 gx inputs
= let
(var, ast) = funToAstR (tshape vals) (fx1 . f . fx2)
env = extendEnvR var (parseDomains vals inputs) EM.empty
in interpretAst env (gx ast)
|
83 | in interpretAst env (gx ast)
| ^^^^^^^^^^^^
```
The message may stem from a quantified constraint where type family applications eventually reduce the "head" of the constraint to `Bool ~ Bool`, but a "context" of the constraint is a constraint that can't be satisfied due to ambiguous type variables. That's just a guess.
The program fails with GHCs <= 9.4.* much earlier due to another GHC bug (to be reported). The program actually has, sort of, a type error and it's, sort of, signalled by the other error messages. It's that the `GoodScalar` constraint in `class (forall rb41. GoodScalar rb41 => c ranked rb41)` is not needed, but can't be satisfied in some cases due to non-injective type families applied to all occurrences of `r`, which makes `r` ambiguous. After removing the constraint, the program compiles fine in GHC 9.6.2.https://gitlab.haskell.org/ghc/ghc/-/issues/23460No position information nor a chain of custody in an error message about a no...2023-08-24T10:42:00ZMikolaj KonarskiNo position information nor a chain of custody in an error message about a not satisfied quantified constraintIt's really hard to debug code with many quantified constraints (unless variable names are unique across all constraints in the program, which requires duplicating the code of the constraints), because GHC doesn't say which of them is no...It's really hard to debug code with many quantified constraints (unless variable names are unique across all constraints in the program, which requires duplicating the code of the constraints), because GHC doesn't say which of them is not satisfied and why it's being considered . E.g.,
```hs
{-# LANGUAGE QuantifiedConstraints, UndecidableInstances #-}
module M where
data Array
instance (forall x. Eq x) => Num Array where
a + b = undefined
f :: Num Array => Array -> Array
f y = y + y
g :: Num Array => Array -> Array
g z = f z
h :: Array -> Array
h c = g c
```
(the same code is at https://play.haskell.org/saved/IhRdWBxb for a quick repro with different GHC versions)
with GHC 9.6.2 produces
```
Main.hs:16:7: error: [GHC-39999]
• No instance for ‘Eq x’
arising from the head of a quantified constraint
arising from a use of ‘g’
Possible fix: add (Eq x) to the context of a quantified context
• In the expression: g c
In an equation for ‘h’: h c = g c
|
16 | h c = g c
| ^
```
Note how `Num Array`, `f` and the location of the constraint are not mentioned. The `Eq` and `x` are completely out of the blue at this point.
Now imagine this scaled to dozens of constraints and intermediate function calls.https://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/22535Regression: infinite loop on quantified constraints2022-12-13T00:10:12ZThomas WinantRegression: infinite loop on quantified constraints```haskell
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
module Test where
class Eq r => Op op r
class (forall r. Eq r => Op op r) => HasResult op
foo :: HasResult op => op -> Bool
foo _ = True == False
...```haskell
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
module Test where
class Eq r => Op op r
class (forall r. Eq r => Op op r) => HasResult op
foo :: HasResult op => op -> Bool
foo _ = True == False
```
GHC 8.10.7 accepts the above program, but GHC 9.0.2, 9.2.5, 9.4.3, and a [recent git release](https://gitlab.haskell.org/ghc/ghc/-/commit/11627c422cfba5e1d84afb08f427007dbc801f10/) all reject it with:
```
Test.hs:9:14: error:
• Reduction stack overflow; size = 201
When simplifying the following type: Eq Bool
Use -freduction-depth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
you're sure that type checking should terminate)
• In the expression: True == False
In an equation for ‘foo’: foo _ = True == False
```
Raising the bound or disabling the check doesn't help.
Removing the `HasResult op` constraint from `foo` makes the program compile again.
It seems that GHC, when it tries to solve the `Eq Bool` constraint, is not using the top-level instance, but looping via the quantified constraint of the local `HasResult` constraint.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/21210Quantified constraint should be accepted in RHS of type family equation2022-03-15T15:33:45ZRichard Eisenbergrae@richarde.devQuantified constraint should be accepted in RHS of type family equationThis is rejected, but it shouldn't be:
```hs
{-# LANGUAGE QuantifiedConstraints, DataKinds, TypeFamilies #-}
module Bug4 where
import Data.Kind
newtype Phant p = MkPhant Int
deriving Eq
f1 :: forall p. (forall x. Eq (p x)) => p Ch...This is rejected, but it shouldn't be:
```hs
{-# LANGUAGE QuantifiedConstraints, DataKinds, TypeFamilies #-}
module Bug4 where
import Data.Kind
newtype Phant p = MkPhant Int
deriving Eq
f1 :: forall p. (forall x. Eq (p x)) => p Char -> p Double -> Bool
f1 p1 p2 = p1 == p1 && p2 == p2
type ForallEq p = forall x. Eq (p x)
f2 :: ForallEq p => p Char -> p Double -> Bool
f2 p1 p2 = p1 == p1 && p2 == p2
type ForallEqs :: [Type -> Type] -> Constraint
type family ForallEqs ps where
ForallEqs '[] = ()
ForallEqs (p : ps) = (ForallEq p, ForallEqs ps)
```
The `forall` in a quantified constraint is really a different `forall` than the one used in normal types, and it should be acceptable in the RHS of a type family equation.https://gitlab.haskell.org/ghc/ghc/-/issues/20845Cannot satisfy QuantifiedConstraints2022-02-25T11:02:21ZAshley YakeleyCannot satisfy QuantifiedConstraints<!--
READ THIS FIRST: If the feature you are proposing changes the language that GHC accepts
or adds any warnings to `-Wall`, it should be written as a [GHC Proposal](https://github.com/ghc-proposals/ghc-proposals/).
Other features, appr...<!--
READ THIS FIRST: If the feature you are proposing changes the language that GHC accepts
or adds any warnings to `-Wall`, it should be written as a [GHC Proposal](https://github.com/ghc-proposals/ghc-proposals/).
Other features, appropriate for a GitLab feature request, include GHC API/plugin
innovations, new low-impact compiler flags, or other similar additions to GHC.
-->
## Motivation
I cannot satisfy a quantified constraint, even if I can satisfy the constraint for every value of the type variable.
Example:
```haskell
{-# LANGUAGE QuantifiedConstraints, UndecidableInstances, RankNTypes,
KindSignatures, TypeApplications, ScopedTypeVariables, GADTs #-}
module QuantifiedConstraints where
import Data.Kind
class IsUnit (a :: Type) where
isUnit :: forall r. (a ~ () => r) -> r
class C (a :: Type)
instance C ()
-- requires quantified constraint I want to satisfy
f1 :: (forall a. IsUnit a => C a) => Int
f1 = 3
-- can satisfy C for any particular a (that has IsUnit)
f2 :: forall a r. IsUnit a => (C a => r) -> r
f2 cr = isUnit @a cr
f :: Int
f = f2 f1 -- GHC (correctly) rejects this, but no other option
```
## Proposal
Provide some way of satisfying quantified constraints in this manner.
Sorry I don't have a concrete proposal, nor is this strictly a defect in GHC, I just want to raise the issue.ZubinZubinhttps://gitlab.haskell.org/ghc/ghc/-/issues/20538Strange Behavior with QuanitifiedConstraints, DerivingStrategies, and GND2024-01-11T02:06:41ZMatthew MongeauStrange Behavior with QuanitifiedConstraints, DerivingStrategies, and GND## Summary
Code that should compile whilst using a newtype deriving strategy fails to compile unless using Standalone deriving.
## Steps to reproduce
The following program fails to compile:
```haskell
{-# LANGUAGE DerivingStrategies ...## Summary
Code that should compile whilst using a newtype deriving strategy fails to compile unless using Standalone deriving.
## Steps to reproduce
The following program fails to compile:
```haskell
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE StandaloneDeriving #-}
module Main where
import Control.Monad.Reader
import Data.Coerce
class (forall a b. Coercible a b => Coercible (f a) (f b)) => CoerceRole f
instance (forall a b. Coercible a b => Coercible (f a) (f b)) => CoerceRole f
data Env = Env
data Message = Message
class Run a where
run :: forall m. (MonadReader Env m, CoerceRole m) => Message -> a -> m a
data Inner = Inner
instance Run Inner where
run _ = pure
newtype Wrapper = Wrapper Inner
deriving newtype Run
-- deriving newtype instance Run Wrapper
main :: IO ()
main = pure ()
```
The observed error is:
```
/private/tmp/CoerceBug/app/Main.hs:28:20-22: error:
• Couldn't match representation of type ‘m Inner’
with that of ‘m Wrapper’
arising from the coercion of the method ‘run’
from type ‘forall (m :: * -> *).
(MonadReader Env m, CoerceRole m) =>
Message -> Inner -> m Inner’
to type ‘forall (m :: * -> *).
(MonadReader Env m, CoerceRole m) =>
Message -> Wrapper -> m Wrapper’
NB: We cannot know what roles the parameters to ‘m’ have;
we must assume that the role is nominal
• When deriving the instance for (Run Wrapper)
|
28 | deriving newtype Run
| ^^^
```
However, commenting out ` deriving newtype Run` and uncommenting `deriving newtype instance Run Wrapper` will cause compilation to succeed.
## Expected behavior
Both programs should be considered valid programs.
## Environment
* GHC version used: ghc-8.10.7
Optional:
* Operating System: macOS 11.6
* System Architecture: x86_649.4.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/20318GHC complains about impredicativity in type synonym for a quantified constraint2021-09-07T14:37:54ZRichard Eisenbergrae@richarde.devGHC complains about impredicativity in type synonym for a quantified constraintIf I say
```hs
{-# LANGUAGE ConstraintKinds, QuantifiedConstraints #-}
module Bug where
type T b = (Ord b, forall a. Eq a)
```
then GHC HEAD says
```
Bug.hs:5:1: error:
• Illegal polymorphic type: forall a. Eq a
Perhaps yo...If I say
```hs
{-# LANGUAGE ConstraintKinds, QuantifiedConstraints #-}
module Bug where
type T b = (Ord b, forall a. Eq a)
```
then GHC HEAD says
```
Bug.hs:5:1: error:
• Illegal polymorphic type: forall a. Eq a
Perhaps you intended to use ImpredicativeTypes
• In the type synonym declaration for ‘T’
|
5 | type T b = (Ord b, forall a. Eq a)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Note that `T` defines a *constraint* synonym, not a type synonym. Accordingly, `QuantifiedConstraints` should be enough to accept this definition.
Inspired by https://mail.haskell.org/pipermail/haskell-cafe/2021-August/134388.htmlhttps://gitlab.haskell.org/ghc/ghc/-/issues/20304Constraint solver loop with quantified constraints2023-08-17T16:14:55Zsheafsam.derbyshire@gmail.comConstraint solver loop with quantified constraintsIn https://gitlab.haskell.org/ghc/ghc/-/issues/17025#note_220235, Simon writes the following program:
```haskell
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAG...In https://gitlab.haskell.org/ghc/ghc/-/issues/17025#note_220235, Simon writes the following program:
```haskell
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
module QC where
class (forall c d. (d ~ F f) => C (d c) c) => C f b where
type F f :: * -> * -> *
f :: (c -> b) -> F f c a -> f a
```
This program seems to make the constraint solver loop, without even hitting a "too many iterations" error.
GHC versions tested: 9.0, HEAD.https://gitlab.haskell.org/ghc/ghc/-/issues/19922Give MonadTrans a QuantifiedConstraints superclass2022-02-02T11:04:26ZIcelandjackGive MonadTrans a QuantifiedConstraints superclassI made a [patch for *transformers*](https://hub.darcs.net/Icelandjack/transformers/patch/65b965a5495d73d8201943338d3c7a25fb1be233) ([issue](https://hub.darcs.net/ross/transformers/issue/71)) adding a superclass to `MonadTrans`. This is t...I made a [patch for *transformers*](https://hub.darcs.net/Icelandjack/transformers/patch/65b965a5495d73d8201943338d3c7a25fb1be233) ([issue](https://hub.darcs.net/ross/transformers/issue/71)) adding a superclass to `MonadTrans`. This is the posterboy of the `QuantifiedConstraints` extension; indicating that `MonadTrans trans` lifts `Monad m` to `Monad (trans m)`.
```haskell
class (forall m. Monad m => Monad (t m)) => MonadTrans t where
lift :: Monad m => m a -> t m a
```
I haven't contributed using darcs before so I am making a ticket here as well to attract discussion and making sure I'm doing everything right.https://gitlab.haskell.org/ghc/ghc/-/issues/18873Quantified equality constraints are not used for rewriting2020-12-10T20:30:27ZRichard Eisenbergrae@richarde.devQuantified equality constraints are not used for rewritingIf I say
```hs
type family F a b where
F [_] b = b
f :: forall a b. (a ~ [b]) => F a b -> b
f x = x
```
GHC smiles upon me: the equality constraint rewrites `a` to `[b]`, and then `F [b] b` can reduce to `b`, and all is well.
But i...If I say
```hs
type family F a b where
F [_] b = b
f :: forall a b. (a ~ [b]) => F a b -> b
f x = x
```
GHC smiles upon me: the equality constraint rewrites `a` to `[b]`, and then `F [b] b` can reduce to `b`, and all is well.
But if I say
```hs
type family F a b where
F [_] b = b
class Truth
instance Truth
f :: forall a b. (Truth => a ~ [b]) => F a b -> b
f x = x
```
I get an error, saying `F a b` does not match `b`. This is because the equality, hidden behind `Truth`, is not used for rewriting, and thus GHC cannot figure out that `F a b` can reduce.
I don't see an easy solution here.
This isn't just me grousing: a problem on !4149 could be worked around if GHC used such equalities for rewriting. And so if we can solve this problem, we can solve the other one. My expectation is that we won't solve this one, though.https://gitlab.haskell.org/ghc/ghc/-/issues/18213GND generates code that instantiates coerce too much2020-10-31T21:03:41ZRyan ScottGND generates code that instantiates coerce too muchConsider this code from https://gitlab.haskell.org/ghc/ghc/issues/18148#note_270603:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUA...Consider this code from https://gitlab.haskell.org/ghc/ghc/issues/18148#note_270603:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
module Bug where
class Foo a where
bar :: forall (x :: a). ()
bar = ()
instance Foo Int
newtype Quux a = Quux a
-- deriving newtype instance _ => Foo (Quux Int)
deriving newtype instance Foo (Quux Int)
```
This typechecks in GHC 8.10.1. However, if you comment out the original `deriving newtype instance Foo (Quux Int)` line and uncomment the very similar line above it, it no longer typechecks:
```
Bug.hs:19:1: error:
• Couldn't match type ‘Int’ with ‘Quux Int’
arising from the coercion of the method ‘bar’
from type ‘forall (x :: Int). ()’
to type ‘forall (x :: Quux Int). ()’
• When deriving the instance for (Foo (Quux Int))
|
19 | deriving newtype instance _ => Foo (Quux Int)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is a strange inconsistency, given how similar these standalone `deriving` declarations are. Why does the original succeed but the line above it fail?
As it turns out, both of these really ought to fail, but the original only succeeds due to an unfortunate fluke in the way `GeneralizedNewtypeDeriving` works. Here is the code that the original declaration generates (with `-ddump-deriv`):
```
==================== Derived instances ====================
Derived class instances:
instance Bug.Foo (Bug.Quux GHC.Types.Int) where
Bug.bar
= GHC.Prim.coerce @() @() (Bug.bar @GHC.Types.Int) ::
forall (x_aKF :: Bug.Quux GHC.Types.Int). ()
```
Notice that we are instantiating `coerce` with `@() @()`. But this is blatantly wrong—it really ought to be `coerce @(forall (x :: Int). ()) @(forall (x :: Quux Int). ())`, which the typechecker would reject (as it should). But GND generates `coerce @() @()` instead, and as a result, the use of `bar` on the RHS gets instantiated with `@Any`, which is not what was intended at all.
In contrast, the `deriving newtype instance _ => Foo (Quux Int)` line infers a `Coercible (forall (x :: Int). ()) (forall (x :: Quux Int). ())` constraint, which the constraint solver rejects (as it should). The original line does not use the same constraint-inference machinery, so it bypasses this step.
What can be done about this? It's tempting to have the original declaration generate this code instead:
```hs
instance Foo (Quux Int) where
bar = coerce @(forall (x :: Int). ())
@(forall (x :: Quux Int). ())
bar
```
Sadly, doing so would break a number of test cases that involve quantified constraints in instance contexts, such as `T15290`. See [`Note [GND and QuantifiedConstraints]`](https://gitlab.haskell.org/ghc/ghc/-/blob/9afd92512b41cf6c6de3a17b474d8d4bb01158c3/compiler/GHC/Tc/Deriv/Generate.hs#L1686-1773) for the full story. In order to make these test cases succeed (as a part of the fix for #15290), we employed an [ugly hack](132273f34e394bf7e900d0c15e01e91edd711890) where we split the `forall`s off of any types used to instantiate `coerce` in GND-generated code. But, as the example above demonstrates, this hack creates just as many problems as it solves.
@simonpj believes that this hack (and all of `Note [GND and QuantifiedConstraints]`) could be avoided. I don't quite understand his grand vision, so I'll let him comment here about what his vision entails.
Another similar example of this bug arising can be found in #18148. However, that issue is ensnared in a separate discussion about the roles of arguments to type classes, as the examples in #18148 crucially involve `ConstrainedClassMethods`. The underlying bug in this issue, on the other hand, does not fundamentally involve `ConstrainedClassMethods` in any way, so @simonpj and I have decided to track it separately here.https://gitlab.haskell.org/ghc/ghc/-/issues/18150QuantifiedConstraints cannot refer to KnownNat2020-05-19T15:35:06ZKoz RossQuantifiedConstraints cannot refer to KnownNat## Summary
If you attempt to write a quantified constraint involving ``KnownNat``, GHC will inform you that ``Class KnownNat does not support user-specified instances``. Given that no instances are being defined here (see 'Steps to repr...## Summary
If you attempt to write a quantified constraint involving ``KnownNat``, GHC will inform you that ``Class KnownNat does not support user-specified instances``. Given that no instances are being defined here (see 'Steps to reproduce' for an example), this is at least an unclear error message. It's also strange that it's not possible to express quantified constraints with ``KnownNat``.
## Steps to reproduce
Attempt to compile the following code:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
module Baz where
import Data.Kind (Type)
import GHC.TypeNats (KnownNat, Nat)
class (forall n. KnownNat n => KnownNat (f n)) => Foo (f :: Nat -> Nat) where
type Bar n :: Nat
```
This will emit the error message described in the summary.
## Expected behavior
Either to compile, or to give an error message more indicative of what the true problem is.
## Environment
* GHC version used: 8.10.1
Optional:
* Operating System: GNU/Linux
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc/-/issues/17959Cannot use Type Synonym with QuantifiedConstraints in GHC 8.8: "Illegal type ...2022-09-07T12:30:43ZFabio MogaveroCannot use Type Synonym with QuantifiedConstraints in GHC 8.8: "Illegal type synonym family application"Consider the following simple snippet with three classes, one of which has an associated type synonym:
~~~haskell
{-# LANGUAGE FlexibleContexts, QuantifiedConstraints, TypeFamilies #-}
class A c
class B c
class (A (D c) => B (D c)...Consider the following simple snippet with three classes, one of which has an associated type synonym:
~~~haskell
{-# LANGUAGE FlexibleContexts, QuantifiedConstraints, TypeFamilies #-}
class A c
class B c
class (A (D c) => B (D c)) => C c where
type D c
~~~
GHC 8.6.5 compiles it like a charm, but both GHC 8.8.2 and 8.8.3 fail to compile with the following message:
~~~"compiler crash"
• Illegal type synonym family application ‘D c’ in instance:
B (D c)
• In the quantified constraint ‘A (D c) => B (D c)’
In the context: A (D c) => B (D c)
While checking the super-classes of class ‘C’
In the class declaration for ‘C’
~~~
Now, I am not sure if this is really a bug or, instead, a correction to the compiler, but I do not actually see why the snippet should fail to compile.
/label ~"needs triage"
/label ~bug
/label ~TypeFamilies
/label ~QuantifiedConstraintshttps://gitlab.haskell.org/ghc/ghc/-/issues/17934Consider using specificity to disambiguate quantified constraints2021-02-21T15:37:18ZRichard Eisenbergrae@richarde.devConsider using specificity to disambiguate quantified constraints**Summary:** Currently, quantified constraints shadow global instances. This ticket proposes to use specificity (in the sense used by overlapping instances) instead of shadowing.
**Motivation**
This looks like a sensible way of having ...**Summary:** Currently, quantified constraints shadow global instances. This ticket proposes to use specificity (in the sense used by overlapping instances) instead of shadowing.
**Motivation**
This looks like a sensible way of having a datatype that can store something of a type that supports some class interface:
```haskell
data Some (c :: Type -> Constraint) where
Some :: c a => a -> Some c
```
But now I want to write a `Show` instance. I can do this only when the existential `a` supports `Show`. But I don't wish to require that `c ~ Show` -- maybe `c a` implies `Show a`. So I write this:
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
```
But now this fails. The problem is that the instance gets expanded to
```haskell
instance (forall x . c x => Show x) => Show (Some c) where
showsPrec n (Some a) = showsPrec n a
show = $dmshow
```
where `$dmshow :: Show a => a -> String` is the default method implementation for `show`. When type-checking this method, GHC needs to satisfy `Show (Some c)`. The context includes two possibilities: the quantified constraint, and the top-level instance declaration. Because local instances (= quantified constraints) shadow global ones, we use the first. So we reduce `[W] Show (Some c)` to `[W] c (Some c)`, which cannot be solved, leading to disaster.
This example first came to light in https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501, where it was copied from #17794.
Taking this new approach will likely fix #16502 and allow the original program in #17202 to be accepted. See also https://gitlab.haskell.org/ghc/ghc/issues/16502#note_253501 and https://gitlab.haskell.org/ghc/ghc/issues/16502#note_259055 for more test cases.
**Background**:
The current instance lookup (as documented [here](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#instance-lookup)) works as follows to solve a `[W] C T` constraint (for some class `C` and type `T`).
1. Look for local (non-quantified) assumptions for `[G] C T`.
2. Look for local quantified constraints whose conclusions match `C T`. If exactly one matches, select the constraint. Then, check whether any quantified constraints *unify* with `C T` (allowing any variables in `C T` to be bound). If any do, abort, complaining about potential incoherence. Otherwise, reduce `[W] C T` to the premise of the quantified constraint.
3. Same as (2), but using the global instance table.
**Proposal**:
Use specificity to disambiguate.
* Let `<=spec` denote a partial order on instance heads. `C T1 <=spec C T2` iff there exists a substitution `S` such that `S(T2) = T1` -- just as is used with overlapping instances today.
* Let metavariable `I` denote givens. These can be non-quantified, quantified (local), or global.
* Define `locality(I)` be a number that denotes how local `I` is. The locality of a non-quantified given is 1, of a quantified local given is 2, and of a global is 3.
* Define partial order `<=` on instances as follows:
1. If `I1 <=spec I2` and `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
2. If neither `I1 <=spec I2` nor `I2 <=spec I1`, then `I1 <= I2` is `locality(I1) <= locality(I2)`.
3. Otherwise, `I1 <= I2` if `I1 <=spec I2`.
Here is the proposed instance lookup procedure:
1. Collect all givens `I` (of all localities) that match a target. Call this set `Is`. If `Is` is empty, fail.
2. Let `I0` be the minimum element of `Is` with respect to `<=`. (Consider `Is` to be set-like, discarding duplicates.) If `I0` is not defined, fail.
3. Let `Is'` be the set `Is` excluding `I0`. Case on the locality of `I0`:
* `locality(I0) = 1`: Succeed with `I0` (skipping last check, below).
* `locality(I0) = 2`: Go on to next step if `Is'` contains only global instances. If `Is'` contains local instances, fail.
* `locality(I0) = 3`: Fail if any element in `Is'` is a local quantified instance. Go on to next step if, for every `I'` in `Is'`, either `I0` is *overlapping* or `I'` is *overlappable*.
4. Collect all givens (of all localities) that *unify* with a target, excluding those in `Is`. If `IncoherentInstances` is off and this set contains at least one instances not labeled **incoherent**, fail.
5. Succeed with `I0`.
**Discussion**:
This new algorithm is meant to replicate current behavior, except in the scenario where a global instance is more specific than a local one, in which the global instance should be selected. I have tried to capture current behavior w.r.t. incoherent and overlapping instances. In any case, if my algorithm deviates from current behavior w.r.t. incoherent or overlapping instances, this deviation is unintentional.
Another possible approach is to put local and global instances on even footing (that is, set both to have locality 2) but to allow users to explicitly label local instances as overlapping. I prefer the tiered approach above, but there's something simpler about local overlapping instances, in that it's one mechanism to think about.https://gitlab.haskell.org/ghc/ghc/-/issues/17802QuantifiedConstraints don't work with equality constraints on type families2020-02-20T16:46:33ZSebastian GrafQuantifiedConstraints don't work with equality constraints on type familiesI'm quite confident that this is a duplicate of some prior issue (#14860?), but this is different enough from all tickets I skimmed so far. This program is rejected:
```hs
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies...I'm quite confident that this is a duplicate of some prior issue (#14860?), but this is different enough from all tickets I skimmed so far. This program is rejected:
```hs
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
module Lib where
data T a = T a
type family F a
x :: (forall a. T a ~ F a) => F Int
x = T 42
```
```
src.hs:10:6: error:
• Couldn't match type ‘F a’ with ‘T a’
• In the ambiguity check for ‘x’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: x :: (forall a. T a ~ F a) => F Int
|
10 | x :: (forall a. T a ~ F a) => F Int
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
And I'm unsure why. In my head this should just work.
@matheus23 and I would really like to use it in !2315 to generalise constraints of the form `XRec pass (HsExpr pass) ~ Located (HsExpr pass)` (generalise over the syntactic entity `HsExpr pass`, that is).https://gitlab.haskell.org/ghc/ghc/-/issues/17737Recursive superclass check is defeated by quantified constraints2020-03-10T14:21:59ZRichard Eisenbergrae@richarde.devRecursive superclass check is defeated by quantified constraintsThis is accepted:
```hs
{-# LANGUAGE QuantifiedConstraints, KindSignatures, ConstraintKinds #-}
module Bug where
import Data.Kind
class ((() :: Constraint) => C a) => C a
```
The vacuous constraint `()` hides the recursive superclas...This is accepted:
```hs
{-# LANGUAGE QuantifiedConstraints, KindSignatures, ConstraintKinds #-}
module Bug where
import Data.Kind
class ((() :: Constraint) => C a) => C a
```
The vacuous constraint `()` hides the recursive superclass `C a`. Note that I do not have `RecursiveSuperclasses` enabled.
The culprit is `TcTyDecls.checkClassCycles`.
This is not a "real" bug report, in that I found the problem only by reading the source code, not by observing the misbehavior. Still, it shouldn't be hard to fix. Should we just look through quantified constraints always?Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/17719Note [Do not add duplicate quantified instances] is simplistic, causing rejec...2020-07-14T19:14:38ZRichard Eisenbergrae@richarde.devNote [Do not add duplicate quantified instances] is simplistic, causing rejection of programsCopied wholesale from https://gitlab.haskell.org/ghc/ghc/merge_requests/2283#note_242042:
Consider
```haskell
{-# LANGUAGE QuantifiedConstraints, ConstraintKinds,
ExistentialQuantification #-}
module Bug where
class C1 a...Copied wholesale from https://gitlab.haskell.org/ghc/ghc/merge_requests/2283#note_242042:
Consider
```haskell
{-# LANGUAGE QuantifiedConstraints, ConstraintKinds,
ExistentialQuantification #-}
module Bug where
class C1 a
class (forall z. C1 z) => C2 y
class (forall y. C2 y) => C3 x
data Dict c = c => Dict
foo :: (C2 a, C3 a) => a -> Dict (C1 a)
foo _ = Dict
```
Amazingly, with *either* `C2 a` or `C3 a`, `foo` is accepted. But with both, it is rejected.
The problem is that, after eagerly expanding superclasses of quantified constraints (that's the new bit), we end up with
```
[G] g1 :: forall z. C1 z -- from the C2 a constraint
[G] g2 :: forall y z. C1 z -- from the C3 a constraint
```
So when we want to solve `C1 a`, we don't know which quantified constraint to use, and so we stop. (Also strange: `g2` is quantified over the unused `y`. It's clear where this comes from, and it seems harmless, but it's a bit strange. This detail is *not* salient. It is *not* the reason we're struggling here.) This has been seen before, in another guise: #15244. And we have
```
{- Note [Do not add duplicate quantified instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this (#15244):
f :: (C g, D g) => ....
class S g => C g where ...
class S g => D g where ...
class (forall a. Eq a => Eq (g a)) => S g where ...
Then in f's RHS there are two identical quantified constraints
available, one via the superclasses of C and one via the superclasses
of D. The two are identical, and it seems wrong to reject the program
because of that. But without doing duplicate-elimination we will have
two matching QCInsts when we try to solve constraints arising from f's
RHS.
The simplest thing is simply to eliminate duplicates, which we do here.
-}
```
which is duly implemented. However, here, we don't have duplicates -- we have near-duplicates, which are not caught by the simple (`tcEqType`) check.
I wonder if the way forward is to really try to "solve" quantified instances. That is, before labeling them inert, we try to interact them with inerts. Then, we might discover that one constraint is implied by another, which will get rid of this problem (and replace that Note).