GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2024-01-23T18:13:25Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/22762eqType, tcEqType, and foralls2024-01-23T18:13:25ZRyan ScotteqType, tcEqType, and forallsSee also
* https://gitlab.haskell.org/ghc/ghc/-/wikis/DH-Current-Status, and
* [GHC proposal issue #558](https://github.com/ghc-proposals/ghc-proposals/issues/558) "Apartness of visible and invisible forall".
The following program pas...See also
* https://gitlab.haskell.org/ghc/ghc/-/wikis/DH-Current-Status, and
* [GHC proposal issue #558](https://github.com/ghc-proposals/ghc-proposals/issues/558) "Apartness of visible and invisible forall".
The following program passes Core Lint on GHC 9.4 and earlier:
```hs
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
type Const :: a -> b -> a
type family Const x y where
Const x _ = x
type F :: (forall (b :: Bool) -> Const Type b) -> Type
data F f
type G :: forall (b :: Bool) -> Type
data G b
type H :: Type
type family H where
H = F G
```
But fails on GHC 9.6.1-alpha1:
```
$ ghc-9.6.0.20230111 Bug.hs -dcore-lint -fforce-recomp
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of TcGblEnv axioms ***
Bug.hs:20:13: warning:
From-kind of Cast differs from kind of enclosed type
From-kind: forall (b :: Bool) -> *
Kind of enclosed type: forall {b :: Bool}. *
Actual enclosed type: G
Coercion used in cast: forall (b :: <Bool>_N).
Sym (D:R:Const[0] <*>_N <Bool>_N <b>_N <*>_N)
In the coercion axiom
axiom D:R:H
{H = F (G |> forall (b :: <Bool>_N).
Sym (D:R:Const[0] <*>_N <Bool>_N <b>_N <*>_N))
-- Defined at Bug.hs:21:3}
Substitution: <InScope = {}
IdSubst = []
TvSubst = []
CvSubst = []>
*** Offending Program ***
axiom D:R:Const
{forall {a} {b} {x :: a}.
Const x _ = x_ahb -- Defined at Bug.hs:11:3}
axiom D:R:H
{H = F (G |> forall (b :: <Bool>_N).
Sym (D:R:Const[0] <*>_N <Bool>_N <b>_N <*>_N))
-- Defined at Bug.hs:21:3}
*** End of Offense ***
<no location info>: error:
Compilation had errors
<no location info>: error: ExitFailure 1
```9.10.1Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/23884Unexpected representation-polymorphism error when using default signatures2024-01-11T21:24:47Zsheafsam.derbyshire@gmail.comUnexpected representation-polymorphism error when using default signaturesI would expect the following program from @adamgundry to work, but it doesn't:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FunctionalDependencies #-}
module T23884 where
import Data....I would expect the following program from @adamgundry to work, but it doesn't:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FunctionalDependencies #-}
module T23884 where
import Data.Kind
import GHC.Exts
type SetField :: forall {k} {r_rep} {a_rep} . k -> TYPE r_rep -> TYPE a_rep -> Constraint
class SetField x r a | x r -> a where
modifyField :: (a -> a) -> r -> r
setField :: a -> r -> r
default setField :: (a_rep ~ LiftedRep) => a -> r -> r
setField x = modifyField (\ _ -> x)
```
```
T23884.hs:16:3: error: [GHC-55287]
The first pattern in the equation for `setField'
does not have a fixed runtime representation.
Its type is:
a :: TYPE a_rep
|
16 | setField x = modifyField (\ _ -> x)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
T23884.hs:16:36: error: [GHC-55287]
* The binder of the lambda expression
does not have a fixed runtime representation.
Its type is:
a0 :: TYPE a_rep0
Cannot unify `a_rep' with the type variable `a_rep0'
because the former is not a concrete `RuntimeRep'.
* In the expression: x
In the first argument of `modifyField', namely `(\ _ -> x)'
In the expression: modifyField (\ _ -> x)
```https://gitlab.haskell.org/ghc/ghc/-/issues/24213"Unbound RULE binders" conditions too restrictive?2023-11-29T14:00:15ZBen Gamari"Unbound RULE binders" conditions too restrictive?While debugging a client project a colleague encountered Core Lint error after simplification:
```
*** Core Lint errors : in result of Simplifier ***
<no location info>: error: [-Werror]
Rule "SC:$j0": unbound [sg_svBxD]
In the ...While debugging a client project a colleague encountered Core Lint error after simplification:
```
*** Core Lint errors : in result of Simplifier ***
<no location info>: error: [-Werror]
Rule "SC:$j0": unbound [sg_svBxD]
In the RHS of $w$ctoSQL_svxsI :: ByteArray#
-> Int#
-> Int#
-> TableName
-> SetExp
-> Maybe FromExp
-> Maybe WhereFrag
-> Maybe RetExp
-> (# ArrayWriter, Int#, Int# #)
In the body of lambda with binder ww_svxsv :: ByteArray#
In the body of lambda with binder ww_svxsw :: Int#
In the body of lambda with binder ww_svxsx :: Int#
In the body of lambda with binder ww_svxsz :: TableName
In the body of lambda with binder ww_svxsB :: SetExp
In the body of lambda with binder ww_svxsC :: Maybe FromExp
In the body of lambda with binder ww_svxsD :: Maybe WhereFrag
In the body of lambda with binder ww_svxsE :: Maybe RetExp
In a case alternative: (TextBuilder ww_av2BQ :: ArrayWriter,
ww1_av2BR :: Int#,
ww2_av2BS :: Int#)
In a case alternative: ((#,,#) ww5_iv2AG :: ArrayWriter,
ww6_iv2AH :: Int#,
ww7_iv2AI :: Int#)
In a case alternative: ((#,,#) ww_svy6c :: ArrayWriter,
ww_svy6d :: Int#,
ww_svy6e :: Int#)
In the body of lambda with binder sc_svBxy :: Int#
In the body of lambda with binder sc_svBxx :: Int#
In the body of lambda with binder sg_svBxw :: (forall {s}.
MArray s
-> Int -> State# s -> (# State# s, Int #))
~R# ArrayWriter
In the body of letrec with binders $s$j_svBxQ :: Int#
-> Int#
-> ((forall {s}.
MArray s
-> Int -> State# s -> (# State# s, Int #))
~R# ArrayWriter) =>
(# ArrayWriter, Int#, Int# #)
In the body of lambda with binder ww_XoV :: ArrayWriter
In the body of lambda with binder ww1_XoW :: Int#
In the body of lambda with binder ww2_XoX :: Int#
In the body of letrec with binders $s$j_svBxJ :: Int#
-> Int#
-> ((forall {s}.
MArray s
-> Int -> State# s -> (# State# s, Int #))
~R# ArrayWriter) =>
(# ArrayWriter, Int#, Int# #)
In a rule attached to $j_sv2DD :: ArrayWriter
-> Int# -> Int# -> (# ArrayWriter, Int#, Int# #)
Substitution: <InScope = {sg_svBxw sg_svBxD}
IdSubst = []
TvSubst = []
CvSubst = [svBxw :-> sg_svBxw, svBxD :-> sg_svBxD]
```
As seen in the relevant Core (see below), the problem is the occurrence of an coercion variable in the RHS of a spec-constr rule which is *not* bound in the rule's LHS. This coercion witnesses the equality of the `ArrayWriter` newtype and its representation:
```haskell
newtype ArrayWriter
= ArrayWriter (forall s. TextArray.MArray s -> Int -> ST s Int)
```
The coercion variable appears to have arisen from the `(N:ArrayWriter[0] :: ArrayWriter ~R# (forall s. MArray s -> Int -> ST s Int))` coercion appearing in the unspecialised binding's RHS (perhaps introduced by SpecConstr itself? we are currently checking this). If SpecConstr is indeed the source of the coercion variable then this seems like a bug; afterall, there should be no need to abstract over closed coercions.
However, this also seems quite similar to the issue observed in `Note [Unbound RULE binders]`. Specifically, that Note specifies that we allow certain (namely, reflexive) coercion variables to occur in a rule's RHS despite being not bound by the LHS. The Note says that, while such occurrences are a bit strange, they are hard to avoid as the result of simplification.
The Core Lint offense suggests to me that the reflexivity restriction of `Note [Unbound RULE binders]` may be too strict: Newtype coercions seem just as benign as reflexive coercions. Sadly, I don't have a minimal reproducer to demonstrate the issue.
<details><summary>Binding and questionable rule</summary>
```haskell
...
join {
$j_sv2DD
:: ArrayWriter -> Int# -> Int# -> (# ArrayWriter, Int#, Int# #)
[LclId[JoinId(3)(Nothing)],
Arity=3,
Str=<SC(L,C(1,C(1,L)))><L><L>,
Unf=Unf{Src=<vanilla>, TopLvl=False,
Value=True, ConLike=True, WorkFree=True, Expandable=True,
Guidance=IF_ARGS [20 0 0] 432 10},
RULES: "SC:$j0"
forall (sc_svBxF :: Int#)
(sc_svBxE :: Int#)
(sg_svBxD
:: (forall {s}.
MArray s -> Int -> State# s -> (# State# s, Int #))
~R# ArrayWriter).
$j_sv2DD ($fMonoidBuilder3
`cast` (sg_svBxw
:: (forall {s}.
MArray s
-> Int -> State# s -> (# State# s, Int #))
~R# ArrayWriter))
sc_svBxE
sc_svBxF
= jump $s$j_svBxJ
sc_svBxF
sc_svBxE
@~(sg_svBxD
:: (forall {s}.
MArray s -> Int -> State# s -> (# State# s, Int #))
~R# ArrayWriter)]
$j_sv2DD (ww3_av2BZ [Dmd=SC(L,C(1,C(1,L))), OS=OneShot]
:: ArrayWriter)
(ww4_av2C0 [OS=OneShot] :: Int#)
(ww5_av2C1 [OS=OneShot] :: Int#)
= case ww3_av2BZ
`cast` (N:ArrayWriter[0]
:: ArrayWriter ~R# (forall s. MArray s -> Int -> ST s Int))
of nt_sv85q [Dmd=LC(S,C(S,C(S,L)))]
...
```
</details>
Full error: https://gitlab.haskell.org/ghc/ghc/-/snippets/5737https://gitlab.haskell.org/ghc/ghc/-/issues/24099Kind Inference fails when working with TypeFamilies of levity polymorphic kind2023-11-16T12:09:52ZMathias SvenKind Inference fails when working with TypeFamilies of levity polymorphic kind## Summary
This [code](https://github.com/goldfirere/video-resources/blob/main/2021-12-28-tuple/TupleSimpler.hs) (usecase) used to typecheck on `GHC 8.10.7`, but it no longer works on either `GHC 9.4.6` or `GHC 9.7.20230527`, here is a ...## Summary
This [code](https://github.com/goldfirere/video-resources/blob/main/2021-12-28-tuple/TupleSimpler.hs) (usecase) used to typecheck on `GHC 8.10.7`, but it no longer works on either `GHC 9.4.6` or `GHC 9.7.20230527`, here is a minimal example of the issue:
```hs
{-# LANGUAGE MagicHash, TypeFamilyDependencies, DataKinds #-}
module Test where
import Data.Kind (Type)
import GHC.Exts ( Int#, TYPE, RuntimeRep )
type FooKind :: RuntimeRep -> Type
type family FooKind rep = r | r -> rep where
FooKind rep = TYPE rep
type Foo :: forall (rep :: RuntimeRep). FooKind rep
type family Foo where
Foo = Int#
t :: () -> Foo
t _ = 42#
```
```
• Couldn't match a lifted type with an unlifted type
When matching types
Foo :: FooKind LiftedRep
Int# :: TYPE 'IntRep
• In the expression: 42#
In an equation for ‘t’: t _ = 42#typecheck(-Wdeferred-type-errors)
```
It seems that `rep` is too eager to resolve to `LiftedRep`, strangely, enabling `PartialTypeSignatures` and simply giving a wildcard type annotation to `Foo` in `t` fixes the inference problem.
```hs
t :: () -> (Foo :: _)
t _ = 42#
```
Now this typechecks correctly.Krzysztof GogolewskiKrzysztof Gogolewskihttps://gitlab.haskell.org/ghc/ghc/-/issues/24095Parse error when annotating type-class instance functions.2023-10-24T14:44:06Zsyd@cs-syd.euParse error when annotating type-class instance functions.## Summary
Please read the guidance in [https://gitlab.haskell.org/ghc/ghc/-/wikis/report-a-bug] and write a brief description of the issue.
## Steps to reproduce
Code:
```
instance Show Foo where
{-# ANN show "hi" #-}
show _ = "F...## Summary
Please read the guidance in [https://gitlab.haskell.org/ghc/ghc/-/wikis/report-a-bug] and write a brief description of the issue.
## Steps to reproduce
Code:
```
instance Show Foo where
{-# ANN show "hi" #-}
show _ = "Foo"
```
Parse error:
```
ann.hs:2:3: error: parse error on input ‘{-# ANN’
|
2 | {-# ANN show "hi" #-}
| ^^^^^^^
```
## Expected behavior
Succesful parse
## Environment
* GHC version used: `9.2.8` and `9.7.20230505`
Optional:
* Operating System: NixOS
* System Architecture: x86_64-linuxhttps://gitlab.haskell.org/ghc/ghc/-/issues/24037GHC 9.8 regression: Fixity declaration for prefix type family in class no lon...2023-10-10T12:51:59ZRyan ScottGHC 9.8 regression: Fixity declaration for prefix type family in class no longer acceptedGHC 9.8 and HEAD reject the following program (minimized from the [`singletons-base`](https://hackage.haskell.org/package/singletons-base) test suite), which GHC 9.6 and earlier accept:
```hs
{-# LANGUAGE TypeFamilies #-}
module Bug whe...GHC 9.8 and HEAD reject the following program (minimized from the [`singletons-base`](https://hackage.haskell.org/package/singletons-base) test suite), which GHC 9.6 and earlier accept:
```hs
{-# LANGUAGE TypeFamilies #-}
module Bug where
class POrd a where
type Geq a b
infixr 6 `Geq`
```
```
$ ghc-9.6.2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
$ ghc-9.8.0.20230929 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:6:12: error: [GHC-54721]
‘Geq’ is not a (visible) method of class ‘POrd’
|
6 | infixr 6 `Geq`
| ^^^^^
```
This is likely related to #23664, except that that bug can only be triggered if the type family name consists of symbolic characters. This bug, on the other hand, occurs when the name has alphanumeric characters.9.8.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23664HEAD regression: GHC no longer accepts fixity declaration in class2023-10-05T20:22:43ZRyan ScottHEAD regression: GHC no longer accepts fixity declaration in class_(Originally observed in a `head.hackage` issue: https://gitlab.haskell.org/ghc/head.hackage/-/issues/88)_
GHC HEAD (at commit eb1a6ab1df473c7ec0e1cbb20fc7124706326ce1) rejects the following program, which earlier versions of GHC accept..._(Originally observed in a `head.hackage` issue: https://gitlab.haskell.org/ghc/head.hackage/-/issues/88)_
GHC HEAD (at commit eb1a6ab1df473c7ec0e1cbb20fc7124706326ce1) rejects the following program, which earlier versions of GHC accept:
```hs
{-# LANGUAGE TypeFamilies #-}
module Bug where
class POrd a where
type a >= b
infix 4 >=
```
```
$ ghc-9.6.2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
$ ghc-9.9.20230716 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:6:11: error: [GHC-54721]
‘>=’ is not a (visible) method of class ‘POrd’
|
6 | infix 4 >=
| ^^
```
Note that:
* It is important that `>=` also be the name of another identifier already in scope. If I rename `>=` to, say, `>==`, then the error disappears.
* It is also important that `>=` be an associated type family. If I change `>=` to an ordinary class method, then the error disappears.9.8.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21360Gratuitous -Wincomplete-record-updates warning in do-notation2023-09-18T09:57:07ZJakob BrünkerGratuitous -Wincomplete-record-updates warning in do-notation## Summary
```haskell
{-# OPTIONS_GHC -Wincomplete-record-updates #-}
data Foo = A {a :: Int} | B deriving Show
foo = A 4
-- wibble is safe - no warning
wibble = do
case foo of
bar@A{} -> Just bar{a = 9}
_ -> fail ":("
-- u...## Summary
```haskell
{-# OPTIONS_GHC -Wincomplete-record-updates #-}
data Foo = A {a :: Int} | B deriving Show
foo = A 4
-- wibble is safe - no warning
wibble = do
case foo of
bar@A{} -> Just bar{a = 9}
_ -> fail ":("
-- using guards doesn't throw a warning
twomble | bar@A{} <- foo = Just bar{a = 9}
| otherwise = fail ":("
-- sworble has the same semantics as wibble and twomble - but we get a warning!
sworble = do
bar@A{} <- Just foo
Just bar{a = 9}
```
Output:
```
DoBug.hs:19:8: warning: [-Wincomplete-record-updates]
Pattern match(es) are non-exhaustive
In a record-update construct: Patterns of type `Foo' not matched: B
|
19 | Just bar{a = 9}
| ^^^^^^^^^^
```
## Expected behavior
Don't warn
## Environment
* GHC version used: 9.3.20220401sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23796TemplateHaskell typechecking regression in HEAD2023-08-08T13:08:41ZRyan ScottTemplateHaskell typechecking regression in HEAD_(Originally observed in a `head.hackage` CI job [here](https://gitlab.haskell.org/ghc/head.hackage/-/jobs/1632860).)_
The `what4-1.4` Hackage library currently fails to build with GHC HEAD + `head.hackage`. Here is a minimized example ..._(Originally observed in a `head.hackage` CI job [here](https://gitlab.haskell.org/ghc/head.hackage/-/jobs/1632860).)_
The `what4-1.4` Hackage library currently fails to build with GHC HEAD + `head.hackage`. Here is a minimized example of the issue:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
module Bug where
good :: (forall a. a -> a) -> b -> b
good = \g x -> g x
bad :: (forall a. a -> a) -> b -> b
bad = $([| \g x -> g x |])
```
This compiles with GHC 9.8 and earlier, but fails to typecheck with GHC HEAD at commit b938950d98945f437f1e28b15a0a3629bfe336c2:
```
$ ghc-head Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:9:8: error: [GHC-83865]
• Couldn't match type: b -> b
with: forall a. a -> a
Expected: (forall a. a -> a) -> b -> b
Actual: (b -> b) -> b -> b
• In the expression: \ g_a24j x_a24k -> g_a24j x_a24k
In an equation for ‘bad’: bad = (\ g_a24j x_a24k -> g_a24j x_a24k)
• Relevant bindings include
bad :: (forall a. a -> a) -> b -> b (bound at Bug.hs:9:1)
|
9 | bad = $([| \g x -> g x |])
| ^^^^^^^^^^^^^^^^^^^
```
I think both of these should be accepted, as the only difference between `good` and `bad` is the presence of a Template Haskell splice.
While I haven't had time to bisect the issue just yet, my first hunch is to suspect commit !10911 (`Look through TH splices in splitHsApps`).9.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/17190Backpack signatures fail to compile when referencing class associated types w...2023-08-08T10:32:35ZEdward KmettBackpack signatures fail to compile when referencing class associated types with defaults## Summary
Backpack signatures fail to compile when they reference class associated types with default definitions.
## Steps to reproduce
Build a library that contains a class associated type along with a default definition and requir...## Summary
Backpack signatures fail to compile when they reference class associated types with default definitions.
## Steps to reproduce
Build a library that contains a class associated type along with a default definition and require an instance of that class in a backpack signature.
Example:
`backpack-test.cabal`:
```
cabal-version: 2.4
name: backpack-test
version: 0
library common
build-depends: base
default-language: Haskell2010
exposed-modules: Class
hs-source-dirs: common
library consumer
build-depends: base, common
default-language: Haskell2010
signatures: Instance
hs-source-dirs: consumer
```
`common/Class.hs`:
```haskell
{-# language TypeFamilies #-}
module Class where
class C x where
type T x
type T x = ()
```
`consumer/Instance.hsig`:
```haskell
signature Instance where
import Class
data I
instance C I
```
Error given:
```
<no location info>: error:
The identifier R:TI does not exist in the local signature.
(Try adding it to the export list of the hsig file.)
```
Note: Removing the default `type T x = ()` results in this code compiling.
## Expected behavior
I'd expect this to work.
## Environment
* GHC version used: 8.8
Optional:
* Operating System: All
* System Architecture: AllJohn EricsonJohn Ericsonhttps://gitlab.haskell.org/ghc/ghc/-/issues/21077GHC 9.2.1 typechecking regression with RankNTypes, TemplateHaskell, and compo...2023-08-04T17:02:49ZRyan ScottGHC 9.2.1 typechecking regression with RankNTypes, TemplateHaskell, and compound expressions_(Originally spun off from https://gitlab.haskell.org/ghc/ghc/-/issues/21038#note_407457)_
The `crux-llvm` library (specifically, [this code](https://github.com/GaloisInc/crucible/blob/e1308319eef8e0fcb55ed04df7eb2e9d5e87aac5/crux-llvm/..._(Originally spun off from https://gitlab.haskell.org/ghc/ghc/-/issues/21038#note_407457)_
The `crux-llvm` library (specifically, [this code](https://github.com/GaloisInc/crucible/blob/e1308319eef8e0fcb55ed04df7eb2e9d5e87aac5/crux-llvm/src/Crux/LLVM/Overrides.hs#L149-L153)) typechecks on GHC 9.0.2 and earlier, but fails to typecheck with GHC 9.2.1. I made an attempt to minimize the issue in #21038, but after trying again with that patch, I discovered that `crux-llvm` _still_ does not typecheck. It turns out that my minimization of the issue was a bit too minimal. Here is an example that better illustrates what is going on:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
module Bug where
data Foo = MkFoo () (forall a. a -> a)
worksOnAllGHCs1 :: Foo
worksOnAllGHCs1 = MkFoo () (\x -> x)
worksOnAllGHCs2 :: Foo
worksOnAllGHCs2 = MkFoo () $ \x -> x
worksOnAllGHCs42 :: Foo
worksOnAllGHCs42 = (MkFoo ()) $ \x -> x
doesn'tWorkOnGHC9'2 :: Foo
doesn'tWorkOnGHC9'2 = $([| MkFoo () |]) $ \x -> x
```
As the names suggest, all of the things functions will typecheck on GHC 9.0.2 and earlier. The `worksOnAllGHCs{1,2,3}` functions will typecheck on GHC 9.2.1, but `doesn'tWorkOnGHC9'2` will not:
```
$ ghc-9.2.1 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o, Bug.dyn_o )
Bug.hs:17:24: error:
• Couldn't match type: forall a. a -> a
with: p0 -> p0
Expected: (p0 -> p0) -> Foo
Actual: (forall a. a -> a) -> Foo
• In the first argument of ‘($)’, namely ‘(MkFoo ())’
In the expression: (MkFoo ()) $ \ x -> x
In an equation for ‘doesn'tWorkOnGHC9'2’:
doesn'tWorkOnGHC9'2 = (MkFoo ()) $ \ x -> x
|
17 | doesn'tWorkOnGHC9'2 = $([| MkFoo () |]) $ \x -> x
| ^^^^^^^^^^^^^^^^
```
The commit which introduced this regression is 9632f413dc90f39bc64586c064805f515a672ca0 (`Implement Quick Look impredicativity`).
Note that unlike the example in #21038, the expression being spliced isn't a simple identifier (i.e., a "head", to use Quick Look terminology), but rather a compound expression. @simonpj suggests [the following fix](https://gitlab.haskell.org/ghc/ghc/-/issues/21038#note_407705):
> Ah yes. Hmm. Reflecting on this, I think the Right Thing is *to treat a splice that is run in the renamer (i.e. an untyped TH splice) as using the "HsExpansion" mechanism*. See `Note [Handling overloaded and rebindable constructs]` in GHC.Tc.Rename.Expr.
>
> That is, the splice `$(expr)` turns into `HsExpanded $(expr) <result-of-running-splice>`. After all, it really *is* an expansion! Then the stuff in the type checker will deal smoothly with application chains. See `Note [Looking through HsExpanded]` in GHC.Tc.Gen.Head.
>
> In principle that should be pretty easy. But `Note [Delaying modFinalizers in untyped splices]` in GHC.Rename.Splice is a painful wart that will hurt us here.
>
> * Where might we store these modFinalizdrs in the HsExpanded? Maybe in the first (original expression) field?
> * Actually I think I favour separating them out entirely into a new extension constructor for `HsExpr GhcRn`. Currenlty we have
>
> ```
> type instance XXExpr GhcRn = HsExpansion (HsExpr GhcRn) (HsExpr GhcRn)
> type instance XXExpr GhcTc = XXExprGhcTc
> ```
>
> We could instead have
>
> ```
> type instance XXExpr GhcRn = XXExprGhcRn
>
> data XXExprGhcRn = ExpansionRn (HsExpansion (HsExpr GhcRn) (HsExpr GhcRn))
> | AddModFinalizedrs ThModFinalizers (HsExpr GhcRn)
> ```
>
> In exchange we can get rid of `HsSpliced` altogether.
> * We still need to call `addModFinalizersWithLclEnv` on those finalisers; so it looks as if we'd need to make `splitHsApps` monadic. That's a pain, but not actually difficult.
>
> I'm not certain of this. But *something* along these lines seems like the right solution.Ryan ScottRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/22004Pattern synonyms in do notation require MonadFail although one-clause pattern...2023-05-30T14:31:00ZMateusz GoślinowskiPattern synonyms in do notation require MonadFail although one-clause pattern match does not emit warnings## Summary
GHC reports a pattern synonym as failable and requires a `MonadFail m` instance when used in do-notation, but does not emit incomplete patterns warning when used in a single-clause pattern matching.
## Steps to reproduce
Co...## Summary
GHC reports a pattern synonym as failable and requires a `MonadFail m` instance when used in do-notation, but does not emit incomplete patterns warning when used in a single-clause pattern matching.
## Steps to reproduce
Consider the following code:
```haskell
{-# OPTIONS_GHC -Wall -Werror #-}
{-# LANGUAGE PatternSynonyms
, GADTs
, TypeApplications
, RankNTypes
, ScopedTypeVariables
, ViewPatterns
#-}
-- GADT of possible types
data Type a where
TInt :: Type Int
class ToType a where
toType :: Type a
instance ToType Int where
toType = TInt
instance Show (Type a) where
show TInt = "TInt"
-- type of expressions
data Expr a where
EInt :: Expr Int
-- existential adding info of ToType dictionary
data SomeExpr where
Expr :: ToType a => Expr a -> SomeExpr
-- explicit use of dictionary
typeof :: forall a. ToType a => Expr a -> Type a
typeof _ = toType @a
{-# COMPLETE (:::) #-}
pattern (:::) :: () => ToType a => Expr a -> Type a -> SomeExpr
pattern expr ::: tt <- Expr expr@(typeof -> tt)
where expr ::: _ = Expr expr
test :: Monad m => m String
test = do
_e ::: t <- pure $ Expr EInt
case t of
TInt -> pure "TInt"
main :: IO ()
main = do
case Expr EInt of
_ ::: t -> print t
test >>= putStrLn
```
The following error is produced:
```
Main.hs:42:3: error:
• Could not deduce (MonadFail m)
arising from a do statement
with the failable pattern ‘_e ::: t’
from the context: Monad m
bound by the type signature for:
test :: forall (m :: * -> *). Monad m => m String
at Main.hs:40:1-29
Possible fix:
add (MonadFail m) to the context of
the type signature for:
test :: forall (m :: * -> *). Monad m => m String
• In a stmt of a 'do' block: _e ::: t <- pure $ Expr EInt
In the expression:
do _e ::: t <- pure $ Expr EInt
case t of { TInt -> pure "TInt" }
In an equation for ‘test’:
test
= do _e ::: t <- pure $ Expr EInt
case t of { TInt -> pure "TInt" }
|
42 | _e ::: t <- pure $ Expr EInt
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
## Expected behavior
Compiles correctly and prints "TInt" twice.
## Environment
* GHC version used: tried 8.10.{6,7}
Optional:
* Operating System & architecture: Any (tried both on Mac and in online repl)https://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/22717Instance not transitively forwarded2023-04-18T18:14:53ZLemmingInstance not transitively forwarded## Summary
When compiling the tests of synthesizer-llvm/HEAD I get:
~~~~
testsuite/Test/Synthesizer/LLVM/Utility.hs:77:30: error:
• Couldn't match type ‘CausalClass.SignalOf
(CausalClass.ProcessOf Sig.T...## Summary
When compiling the tests of synthesizer-llvm/HEAD I get:
~~~~
testsuite/Test/Synthesizer/LLVM/Utility.hs:77:30: error:
• Couldn't match type ‘CausalClass.SignalOf
(CausalClass.ProcessOf Sig.T)’
with ‘Sig.T’
Expected: Sig.T (al, bl)
-> CausalClass.ProcessOf Sig.T () (MultiValue.T a, MultiValue.T b)
Actual: CausalClass.SignalOf
(CausalClass.ProcessOf Sig.T) (MultiValue.T a, MultiValue.T b)
-> CausalClass.ProcessOf Sig.T () (MultiValue.T a, MultiValue.T b)
• In the first argument of ‘(.)’, namely ‘CausalClass.fromSignal’
In the first argument of ‘CausalRender.run’, namely
‘(CausalClass.fromSignal . sig)’
In a stmt of a 'do' block:
proc <- CausalRender.run (CausalClass.fromSignal . sig)
~~~~
If I add `import qualified Synthesizer.LLVM.Causal.Process ()` then the error goes away. However, the import should not be necessary, because the module imports `Synthesizer.LLVM.Generator.Signal` and this in turn imports `Synthesizer.LLVM.Causal.Private` which contains the required instance. This instance is not even orphan.
## Steps to reproduce
You need some unreleased versions of dependent packages for reproduction:
* https://hackage.haskell.org/package/llvm-tf-12.1/candidate
* https://hackage.haskell.org/package/llvm-extra-0.11/candidate
* https://hackage.haskell.org/package/llvm-dsl-0.1/candidate
* https://hackage.haskell.org/package/synthesizer-core-0.8.3/candidate
* https://hackage.haskell.org/package/synthesizer-llvm-1.0/candidate
You should also respect the building hints of
https://hackage.haskell.org/package/llvm-ffi
e.g. manually provide the paths to libLLVM.so and the LLVM C-header files.
Then you can compile with
~~~~
synthesizer-llvm$ PATH=/usr/local/ghc/9.4.4/bin:$PATH cabal-3.8 build all --enable-tests --disable-optimization --disable-documentation
~~~~
## Environment
* GHC version used: 9.4
In GHC before 9.4 this works.9.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/17551TemplateHaskell reify fails with fields from DuplicateRecordFields2023-03-30T13:28:39ZMaxim KoltsovTemplateHaskell reify fails with fields from DuplicateRecordFields## Summary
Trying to `reify` fields from a record defined with `DuplicateRecordFields` extension leads to a confusing error message:
```
Exp.hs:11:1: error:
Ambiguous occurrence ‘Exp.foo’
It could refer to
either the fie...## Summary
Trying to `reify` fields from a record defined with `DuplicateRecordFields` extension leads to a confusing error message:
```
Exp.hs:11:1: error:
Ambiguous occurrence ‘Exp.foo’
It could refer to
either the field ‘foo’, defined at Exp.hs:9:18
or the field ‘foo’, defined at Exp.hs:8:18
```
Even if the name itself is not present in spliced code.
## Steps to reproduce
Complete code snippet is here:
https://gist.github.com/maksbotan/146b250ad295c0f5896a2313ce918cd0
Briefly:
- Write TemplateHaskell function of type `Name -> Q [Dec]`, where `Name` is supposed to refer to a data type.
- `reify` the `Name` to get `RecC` info with `Name`s of the
- call `reify` on those `Name`s to get their types
```haskell
make :: Name -> Q [Dec]
make name = do
TyConI (DataD _ _ _ _ [RecC con fields'] _) <- reify name
let fields = [ field | (field, _, _) <- fields' ]
fieldInfos <- mapM reify fields
return []
```
When the record in question is defined in a file with `DuplicateRecordFields` and really has duplicate fields, GHC will
emit a compilation error with confusing message.
## Expected behavior
Since I `reify`ed concrete record type, I expect to be able to extras its fields without any ambiguity.
## Environment
* GHC version used: 8.6.3 (Stack LTS-13.6), 8.6.5 (nix), 8.8.1 (nix)
* Operating System: macOS mojave
This looks related to #14848 and #17381, but in my case I don't do any quasiquoting. Another difference is that in my
case the error message is really misleading.sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21443GHC calls an unambiguous record update ambiguous2023-03-30T13:28:39ZRichard Eisenbergrae@richarde.devGHC calls an unambiguous record update ambiguousInspired by https://github.com/haskell/error-messages/issues/57
Here is the example:
```hs
data R = MkR1 { foo :: Int }
| MkR2 { bar :: Int }
data S = MkS { foo :: Int, bar :: Int }
blah x = x { foo = 5, bar = 6 }
```
GHC say...Inspired by https://github.com/haskell/error-messages/issues/57
Here is the example:
```hs
data R = MkR1 { foo :: Int }
| MkR2 { bar :: Int }
data S = MkS { foo :: Int, bar :: Int }
blah x = x { foo = 5, bar = 6 }
```
GHC says
```
Scratch.hs:37:10: error:
* Record update is ambiguous, and requires a type signature
* In the expression: x {foo = 5, bar = 6}
In an equation for `blah': blah x = x {foo = 5, bar = 6}
|
37 | blah x = x { foo = 5, bar = 6 }
| ^^^^^^^^^^^^^^^^^^^^^^
```
But it's not ambiguous. GHC rightly rejects that record-update if I write `blah :: R -> R` as a type signature, because `foo` and `bar` are in different constructors. In the record-update ambiguity check, GHC should take constructor choice into account.sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/22519head.hackage: package "what4" no longer compiles2023-02-15T22:36:28ZBryan Rbryan@haskell.foundationhead.hackage: package "what4" no longer compilesSee also #22663
Triggers error GHC-18872
First occurrence on 27 November: https://gitlab.haskell.org/ghc/head.hackage/-/jobs/1245011
```
src/What4/Interface.hs:2593:3: error: [GHC-18872]
• Couldn't match representation of type: IO (S...See also #22663
Triggers error GHC-18872
First occurrence on 27 November: https://gitlab.haskell.org/ghc/head.hackage/-/jobs/1245011
```
src/What4/Interface.hs:2593:3: error: [GHC-18872]
• Couldn't match representation of type: IO (SymBV' sym (n * w))
with that of: IO (SymExpr sym (BaseBVType (n * w)))
arising from a use of ‘coerce’
The data constructor ‘GHC.Types.IO’ of newtype ‘IO’ is not in scope
src/What4/Interface.hs:2611:3: error: [GHC-18872]
• Couldn't match representation of type: IO (Vector.Vector n (SymBV' sym w))
with that of: IO (Vector.Vector n (SymExpr sym (BaseBVType w)))
arising from a use of ‘coerce’
The data constructor ‘GHC.Types.IO’ of newtype ‘IO’ is not in scope
```9.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/19847Type application in pattern does not substitute correctly2023-02-09T17:22:09ZRichard Eisenbergrae@richarde.devType application in pattern does not substitute correctlySee also
* #19577
* #22383
* #21501
Inspired by @Icelandjack's https://gitlab.haskell.org/ghc/ghc/-/issues/19691#note_352594, I typed in
```hs
pattern Is :: forall (b :: Type) (a :: Type). Typeable b => (a ~ b) => TypeRep a
pattern Is ...See also
* #19577
* #22383
* #21501
Inspired by @Icelandjack's https://gitlab.haskell.org/ghc/ghc/-/issues/19691#note_352594, I typed in
```hs
pattern Is :: forall (b :: Type) (a :: Type). Typeable b => (a ~ b) => TypeRep a
pattern Is <- (eqTypeRep (typeRep @b) -> Just HRefl)
where Is = typeRep
def :: TypeRep a -> a
def = \case
Is @Int -> 10
Is @Bool -> False
```
which looks pretty sensible to me. HEAD tells me
```
Scratch.hs:40:3: error:
• No instance for (Typeable b0) arising from a use of ‘Is’
• In the pattern: Is @Int
In a case alternative: Is @Int -> 10
In the expression:
\case
Is @Int -> 10
Is @Bool -> False
|
40 | Is @Int -> 10
| ^^^^^^^
Scratch.hs:40:3: error:
• Could not deduce: a ~ Int
from the context: a ~ b0
bound by a pattern with pattern synonym:
Is :: forall b a. Typeable b => (a ~ b) => TypeRep a,
in a case alternative
at Scratch.hs:40:3-9
Expected: b0
Actual: Int
‘a’ is a rigid type variable bound by
the type signature for:
def :: forall a. TypeRep a -> a
at Scratch.hs:38:1-21
• In the pattern: Is @Int
In a case alternative: Is @Int -> 10
In the expression:
\case
Is @Int -> 10
Is @Bool -> False
• Relevant bindings include
def :: TypeRep a -> a (bound at Scratch.hs:39:1)
|
40 | Is @Int -> 10
| ^^^^^^^
Scratch.hs:41:3: error:
• No instance for (Typeable b1) arising from a use of ‘Is’
• In the pattern: Is @Bool
In a case alternative: Is @Bool -> False
In the expression:
\case
Is @Int -> 10
Is @Bool -> False
|
41 | Is @Bool -> False
| ^^^^^^^^
Scratch.hs:41:15: error:
• Could not deduce: a ~ Bool
from the context: a ~ b1
bound by a pattern with pattern synonym:
Is :: forall b a. Typeable b => (a ~ b) => TypeRep a,
in a case alternative
at Scratch.hs:41:3-10
‘a’ is a rigid type variable bound by
the type signature for:
def :: forall a. TypeRep a -> a
at Scratch.hs:38:1-21
• In the expression: False
In a case alternative: Is @Bool -> False
In the expression:
\case
Is @Int -> 10
Is @Bool -> False
• Relevant bindings include
def :: TypeRep a -> a (bound at Scratch.hs:39:1)
|
41 | Is @Bool -> False
|
```
But that looks wrong: it shouldn't be looking for `Typeable b0` or `Typeable b1`, it should be looking for `Typeable Int` or `Typeable Bool`. While I have not investigated further, this smells like a missing application of a substitution somewhere.https://gitlab.haskell.org/ghc/ghc/-/issues/21149servant-0.19 fails to compile on HEAD due to TypeErrors triggering more eagerly2022-08-24T17:52:16ZRyan Scottservant-0.19 fails to compile on HEAD due to TypeErrors triggering more eagerly`servant-0.19` fails to build on GHC HEAD. Here is a minimized version of the issue:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE PolyKi...`servant-0.19` fails to build on GHC HEAD. Here is a minimized version of the issue:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
import GHC.TypeLits
-- | No instance exists for @tycls (expr :> ...)@ because
-- @expr@ is not recognised.
type NoInstanceForSub (tycls :: k) (expr :: k') =
Text "There is no instance for " :<>: ShowType tycls
:<>: Text " (" :<>: ShowType expr :<>: Text " :> ...)"
-- | No instance exists for @expr@.
type NoInstanceFor (expr :: k) =
Text "There is no instance for " :<>: ShowType expr
-- | No instance exists for @tycls (expr :> ...)@ because @expr@ is not fully saturated.
type PartialApplication (tycls :: k) (expr :: k') =
NoInstanceForSub tycls expr
:$$: ShowType expr :<>: Text " expects " :<>: ShowType (Arity expr) :<>: Text " more arguments"
-- The arity of a combinator, i.e. the number of required arguments.
type Arity (ty :: k) = Arity' k
type Arity' :: k -> Nat
type family Arity' (ty :: k) :: Nat where
Arity' (_ -> ty) = 1 + Arity' ty
Arity' _ = 0
data (path :: k) :> (a :: *)
class HasLink endpoint where
instance TypeError (PartialApplication HasLink arr) => HasLink ((arr :: a -> b) :> sub)
```
This compiles with GHC 9.0.2 and 9.2.1, but fails to compile with HEAD:
```
$ ~/Software/ghc-9.3.20220216/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:40:10: error:
• There is no instance for HasLink (arr :> ...)
arr expects 1 + Arity' b more arguments
• In the ambiguity check for an instance declaration
In the instance declaration for ‘HasLink ((arr :: a -> b) :> sub)’
|
40 | instance TypeError (PartialApplication HasLink arr) => HasLink ((arr :: a -> b) :> sub)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
I'm unclear if this change is intended behavior or not, but since I couldn't find any mention of `TypeError`'s behavior changing in the [9.4 release notes](https://gitlab.haskell.org/ghc/ghc/-/blob/d734ef8f78203b856dcfaf19eaebfed6ec623850/docs/users_guide/9.4.1-notes.rst), I decided to open an issue.9.4.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/21719Type checking with PartialTypeSignatures is broken2022-08-17T10:21:48ZDanil BerestovType checking with PartialTypeSignatures is broken## Steps to reproduce
```haskell
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE BlockArguments #-}
impor...## Steps to reproduce
```haskell
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE BlockArguments #-}
import Control.Exception
data Foo = Foo
deriving (Show, Exception)
class CanThrow e
qux :: Monad m => (CanThrow Foo => m a) -> m a
qux _ = undefined
class Monad m => MonadCheckedThrow m where
throwChecked :: (Exception e, CanThrow e) => e -> m a
foo :: MonadCheckedThrow m => m Int
foo = do
qux do
_ <- baz
pure 5
where
baz :: (CanThrow Foo, _) => _
baz = throwChecked Foo
```
```
error:
• Could not deduce (CanThrow Foo)
from the context: MonadCheckedThrow m
bound by the type signature for:
foo :: forall (m :: * -> *). MonadCheckedThrow m => m Int
at _
or from: MonadCheckedThrow m1
bound by the inferred type for ‘baz’:
forall (m1 :: * -> *) a. MonadCheckedThrow m1 => m1 a
at _
• When checking that the inferred type
baz :: forall (m :: * -> *) a.
(CanThrow Foo, MonadCheckedThrow m) =>
m a
is as general as its (partial) signature
baz :: forall (m :: * -> *) a. MonadCheckedThrow m => m a
In an equation for ‘foo’:
foo
= do qux
do _ <- baz
....
where
baz :: (CanThrow Foo, _) => _
baz = throwChecked Foo
```
## Expected behavior
GHC must check `bar`'s type.
By the way the following code is checked:
```haskell
baz :: (c ~ CanThrow, c Foo, _) => _
baz = throwChecked Foo
-- and
baz :: (f ~ Foo, CanThrow f, _) => _
baz = throwChecked Foo
-- and even
baz :: _ => CanThrow Foo => _
baz = throwChecked Foo
```
## Environment
* GHC version used: 8.10.7Matthew PickeringMatthew Pickering