GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-09-18T09:57:07Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/23154Core Lint error with representation polymorphism and partial type sigs2023-09-18T09:57:07ZKrzysztof GogolewskiCore Lint error with representation polymorphism and partial type sigsThe following program slips through the representation polymorphism check and creates a polymorphic binder, causing a panic or a Lint error
```haskell
{-# LANGUAGE PartialTypeSignatures #-}
module M where
import GHC.Exts
f x = x :: (_...The following program slips through the representation polymorphism check and creates a polymorphic binder, causing a panic or a Lint error
```haskell
{-# LANGUAGE PartialTypeSignatures #-}
module M where
import GHC.Exts
f x = x :: (_ :: (TYPE (_ _)))
```
I've tried pinpointing the problem. The call to `newInferExpTypeFRR` in `Tc/Utils/Unify.hs` creates an `ExpType` with `ir_frr` containing the fixed representation constraint. But apparently that information is not acted upon.9.6.2sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/15433Internal error with PartialTypeSignatures and TH2022-02-26T08:48:32ZKrzysztof GogolewskiInternal error with PartialTypeSignatures and THFile:
```
{-# LANGUAGE TemplateHaskell #-}
type T = $([t| _ |])
```
gives a bad error message in 8.4 and HEAD:
```
• GHC internal error: ‘_’ is not in scope during type checking, but it passed the renamer
tcl_env of environm...File:
```
{-# LANGUAGE TemplateHaskell #-}
type T = $([t| _ |])
```
gives a bad error message in 8.4 and HEAD:
```
• GHC internal error: ‘_’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [r1sn :-> ATcTyCon T :: k0]
• In the type ‘(_)’
In the type declaration for ‘T’
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.4.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Internal error with PartialTypeSignatures and TH","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"File:\r\n\r\n{{{\r\n{-# LANGUAGE TemplateHaskell #-}\r\ntype T = $([t| _ |])\r\n}}}\r\n\r\ngives a bad error message in 8.4 and HEAD:\r\n\r\n{{{\r\n • GHC internal error: ‘_’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [r1sn :-> ATcTyCon T :: k0]\r\n • In the type ‘(_)’\r\n In the type declaration for ‘T’\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->9.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/18008Regression with PartialTypeSignatures in 8.102020-09-03T16:47:28ZadamRegression with PartialTypeSignatures in 8.10This is a regression in 8.10, the code was fine in 8.8.2.
```haskell
-- Bug.hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PartialTypeSignatures #-}
module Bug where
import Control.Exception
data WrappedException = Wra...This is a regression in 8.10, the code was fine in 8.8.2.
```haskell
-- Bug.hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PartialTypeSignatures #-}
module Bug where
import Control.Exception
data WrappedException = WrappedException
deriving (Show)
fromSomeException :: SomeException -> WrappedException
fromSomeException _ = WrappedException
instance Exception WrappedException
fun :: IO () -> (forall e. (Exception e) => e -> IO ()) -> _ -- If I say IO () here it works
fun someComputation reportException =
try someComputation >>= \x -> case x of
Left someException -> reportException (fromSomeException someException) -- or if I turn on TypeApplications and put @_ as the first argument here
Right _ -> pure ()
```
Problem:
```
$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 8.10.1
$ ghc Bug.hs -fforce-recomp
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:18:27: error:
• Couldn't match kind ‘Constraint’ with ‘*’
When matching types
WrappedException :: *
Exception e0 :: Constraint
Expected type: WrappedException -> e0 -> IO ()
Actual type: Exception e0 => e0 -> IO ()
• The function ‘reportException’ is applied to one argument,
but its type ‘Exception e0 => e0 -> IO ()’ has none
In the expression:
reportException (fromSomeException someException)
In a case alternative:
Left someException
-> reportException (fromSomeException someException)
|
18 | Left someException -> reportException (fromSomeException someException)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```8.10.2https://gitlab.haskell.org/ghc/ghc/-/issues/16775Don't zap naughty quantification candidates: error instead2020-12-15T12:32:56ZRichard Eisenbergrae@richarde.devDon't zap naughty quantification candidates: error insteadNote [Naughty quantification candidates] in TcMType describes a scenario like `forall arg. ... (alpha[tau] :: arg) ...`, where `alpha`, a unification variable, has a bound skolem in its type. If `alpha` is otherwise unconstrained, we sim...Note [Naughty quantification candidates] in TcMType describes a scenario like `forall arg. ... (alpha[tau] :: arg) ...`, where `alpha`, a unification variable, has a bound skolem in its type. If `alpha` is otherwise unconstrained, we simply don't know what to do with it. So, as the Note explains, we zap it to `Any`.
However, we recently decided not to `Any`-ify in type declarations. And I think we are wrong to `Any`-ify here, too. We should just error. If not, we risk having `Any` leak in error messages, and it seems a nice goal not to ever let users see `Any` (short of TH or reflection or other dastardly deeds).
The example is `partial-sigs/should_fail/T14040a`. You can find the program in question at the top of #14040. https://gitlab.haskell.org/ghc/ghc/issues/14040#note_168778 reports HEAD's error message. (The program and error message are all very intricate. Don't get distracted by reading them.) However, some of the wildcards in that error message have locally-bound types, meaning there is no hope for them, regardless of other errors about. In other work (some refactoring to be posted soon), I spotted that `tcHsPartialSigType` was missing out on the action in Note [Naughty quantification candidates] and so fixed the problem. This means that the error for that program now mentions `Any`.
Here is a simpler test case:
```
foo :: forall (f :: forall a (b :: a -> Type). b _). f _
foo = foo
```
Note that the type of the first `_` must be `a`, which is locally quantified. In HEAD, this program trips an assertion failure around the substitution invariant (and I have not investigated further). In my branch that duly checks partial signatures for naught quantification candidates, we get
```
• Expected kind ‘k -> *’, but ‘f’ has kind ‘k -> Any @*’
• In the type ‘f _’
In the type signature:
foo :: forall (f :: forall a (b :: a -> Type). b _). f _
```
This is correct enough, but there's `Any` in the error message. I think it would be much better just to reject the type signature a priori.
If I make the program correct (by wrapping the `f _` in a call to `Proxy`, I get
```
Scratch.hs:44:50: warning: [-Wpartial-type-signatures]
• Found type wildcard ‘_’ standing for ‘Any @a :: a’
Where: ‘a’ is a rigid type variable bound by
‘forall a (b :: a -> Type). b _’
at Scratch.hs:44:28
• In the first argument of ‘b’, namely ‘_’
In the kind ‘forall a (b :: a -> Type). b _’
In the type signature:
foo :: forall (f :: forall a (b :: a -> Type). b _). Proxy (f _)
|
44 | foo :: forall (f :: forall a (b :: a -> Type). b _). Proxy (f _)
| ^
Scratch.hs:44:63: warning: [-Wpartial-type-signatures]
• Found type wildcard ‘_’ standing for ‘_ :: k’
Where: ‘k’, ‘_’ are rigid type variables bound by
the inferred type of
foo :: Proxy
@{Any @Type} (f @Type @((->) @{'LiftedRep} @{'LiftedRep} k) _)
at Scratch.hs:45:1-9
• In the first argument of ‘f’, namely ‘_’
In the first argument of ‘Proxy’, namely ‘(f _)’
In the type ‘Proxy (f _)’
|
44 | foo :: forall (f :: forall a (b :: a -> Type). b _). Proxy (f _)
| ^
```
More `Any`s. No! Reject!
What think you (for any value of you)?8.8.2https://gitlab.haskell.org/ghc/ghc/-/issues/16728GHC HEAD-only panic with PartialTypeSignatures2019-07-07T18:00:04ZRyan ScottGHC HEAD-only panic with PartialTypeSignaturesThe following program typechecks on GHC 8.8.1:
```hs
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where
import Data.Proxy
f :: forall a (x :: a). Proxy (x :: _)
f = ...The following program typechecks on GHC 8.8.1:
```hs
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where
import Data.Proxy
f :: forall a (x :: a). Proxy (x :: _)
f = Proxy
```
However, it panics on GHC HEAD:
```
$ ~/Software/ghc5/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:8:37: warning: [-Wpartial-type-signatures]ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.9.0.20190522:
No skolem info:
[a_avg[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1173:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2927:5 in ghc:TcErrors
```
This regression was introduced in commit 80dfcee61e3bfb67f131cd674f96467e16c0f9d8. cc'ing @simonpj, the author of that patch.8.10.1Ryan ScottRichard Eisenbergrae@richarde.devRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/16334Named wildcards in kinds2020-03-26T11:47:19ZVladislav ZavialovNamed wildcards in kindsThis works:
```
Prelude> :set -XNamedWildCards -XPartialTypeSignatures -XPolyKinds
Prelude> k :: (Int :: _); k = 42
<interactive>:2:14: warning: [-Wpartial-type-signatures]
• Found type wildcard ‘_’ standing for ‘*’
• In the t...This works:
```
Prelude> :set -XNamedWildCards -XPartialTypeSignatures -XPolyKinds
Prelude> k :: (Int :: _); k = 42
<interactive>:2:14: warning: [-Wpartial-type-signatures]
• Found type wildcard ‘_’ standing for ‘*’
• In the type signature: k :: (Int :: _)
```
And this doesn't:
```
Prelude> k :: (Int :: _t); k = 42
<interactive>:3:7: error:
• Expected kind ‘_t’, but ‘Int’ has kind ‘*’
• In the type signature: k :: (Int :: _t)
```
The issue, I suspect, is in `partition_nwcs`, which ignores kind variables for some reason.8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/15039Bizarre pretty-printing of inferred Coercible constraint in partial type sign...2019-07-07T18:14:36ZRyan ScottBizarre pretty-printing of inferred Coercible constraint in partial type signatureConsider the following GHCi session:
```
$ ghci
GHCi, version 8.4.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> import Data.Type.Coercion
λ> foo :: _ => Coercion a b; foo = Coercion
<...Consider the following GHCi session:
```
$ ghci
GHCi, version 8.4.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> import Data.Type.Coercion
λ> foo :: _ => Coercion a b; foo = Coercion
<interactive>:2:8: error:
• Found type wildcard ‘_’
standing for ‘Coercible a b :: TYPE ('GHC.Types.TupleRep '[])’
Where: ‘a’, ‘b’ are rigid type variables bound by
the inferred type of foo :: Coercible a b => Coercion a b
at <interactive>:2:27-40
To use the inferred type, enable PartialTypeSignatures
• In the type signature: foo :: _ => Coercion a b
λ> :set -fprint-explicit-kinds
λ> foo :: _ => Coercion a b; foo = Coercion
<interactive>:4:8: error:
• Found type wildcard ‘_’
standing for ‘(a :: *) ~~ (b :: *) :: TYPE
('GHC.Types.TupleRep ('[] GHC.Types.RuntimeRep))’
Where: ‘a’, ‘b’ are rigid type variables bound by
the inferred type of
foo :: ((a :: *) ~~ (b :: *)) => Coercion * a b
at <interactive>:4:27-40
To use the inferred type, enable PartialTypeSignatures
• In the type signature: foo :: _ => Coercion a b
```
There are two things quite strange about this:
1. In both error messages, GHC claims that `Coercible a b`/`a ~~ b` has kind `TYPE (TupleRep '[])`. This is wrong, and should be `Coercible`.
1. For some reason, enabling `-fprint-explicit-kinds` causes the inferred constraint to be `(~~)` instead of `Coercible`, which is just plain wrong.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.4.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Bizarre pretty-printing of inferred Coercible constraint in partial type signature","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1","keywords":["PartialTypeSignatures"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following GHCi session:\r\n\r\n{{{\r\n$ ghci\r\nGHCi, version 8.4.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\nλ> import Data.Type.Coercion\r\nλ> foo :: _ => Coercion a b; foo = Coercion\r\n\r\n<interactive>:2:8: error:\r\n • Found type wildcard ‘_’\r\n standing for ‘Coercible a b :: TYPE ('GHC.Types.TupleRep '[])’\r\n Where: ‘a’, ‘b’ are rigid type variables bound by\r\n the inferred type of foo :: Coercible a b => Coercion a b\r\n at <interactive>:2:27-40\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature: foo :: _ => Coercion a b\r\nλ> :set -fprint-explicit-kinds \r\nλ> foo :: _ => Coercion a b; foo = Coercion\r\n\r\n<interactive>:4:8: error:\r\n • Found type wildcard ‘_’\r\n standing for ‘(a :: *) ~~ (b :: *) :: TYPE\r\n ('GHC.Types.TupleRep ('[] GHC.Types.RuntimeRep))’\r\n Where: ‘a’, ‘b’ are rigid type variables bound by\r\n the inferred type of\r\n foo :: ((a :: *) ~~ (b :: *)) => Coercion * a b\r\n at <interactive>:4:27-40\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature: foo :: _ => Coercion a b\r\n}}}\r\n\r\nThere are two things quite strange about this:\r\n\r\n1. In both error messages, GHC claims that `Coercible a b`/`a ~~ b` has kind `TYPE (TupleRep '[])`. This is wrong, and should be `Coercible`.\r\n2. For some reason, enabling `-fprint-explicit-kinds` causes the inferred constraint to be `(~~)` instead of `Coercible`, which is just plain wrong.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/14715GHC 8.4.1-alpha regression with PartialTypeSignatures2019-07-07T18:15:54ZRyan ScottGHC 8.4.1-alpha regression with PartialTypeSignaturesThis bug prevents `lol-apps`' tests and benchmarks from building with GHC 8.4.1-alpha2. This is as much as I'm able to minimize the issue:
```hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Parti...This bug prevents `lol-apps`' tests and benchmarks from building with GHC 8.4.1-alpha2. This is as much as I'm able to minimize the issue:
```hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
module Bug (bench_mulPublic) where
data Cyc r
data CT zp r'q
class Reduce a b
type family LiftOf b
bench_mulPublic :: forall z zp zq . (z ~ LiftOf zq, _) => Cyc zp -> Cyc z -> IO (zp,zq)
bench_mulPublic pt sk = do
ct :: CT zp (Cyc zq) <- encrypt sk pt
undefined ct
encrypt :: forall z zp zq. Reduce z zq => Cyc z -> Cyc zp -> IO (CT zp (Cyc zq))
encrypt = undefined
```
On GHC 8.2.2, this compiles without issue. But on GHC 8.4.1-alpha2, this errors with:
```
$ /opt/ghc/8.4.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:1: error:
• Could not deduce (Reduce fsk0 zq)
from the context: (z ~ LiftOf zq, Reduce fsk zq)
bound by the inferred type for ‘bench_mulPublic’:
forall z zp zq fsk.
(z ~ LiftOf zq, Reduce fsk zq) =>
Cyc zp -> Cyc z -> IO (zp, zq)
at Bug.hs:(15,1)-(17,14)
The type variable ‘fsk0’ is ambiguous
• In the ambiguity check for the inferred type for ‘bench_mulPublic’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the inferred type
bench_mulPublic :: forall z zp zq fsk.
(z ~ LiftOf zq, Reduce fsk zq) =>
Cyc zp -> Cyc z -> IO (zp, zq)
|
15 | bench_mulPublic pt sk = do
| ^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.4.1-alpha1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC 8.4.1-alpha regression with PartialTypeSignatures","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1-alpha1","keywords":["PartialTypeSignatures"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This bug prevents `lol-apps`' tests and benchmarks from building with GHC 8.4.1-alpha2. This is as much as I'm able to minimize the issue:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE MultiParamTypeClasses #-}\r\n{-# LANGUAGE PartialTypeSignatures #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# OPTIONS_GHC -Wno-partial-type-signatures #-}\r\nmodule Bug (bench_mulPublic) where\r\n\r\ndata Cyc r\r\ndata CT zp r'q\r\nclass Reduce a b\r\ntype family LiftOf b\r\n\r\nbench_mulPublic :: forall z zp zq . (z ~ LiftOf zq, _) => Cyc zp -> Cyc z -> IO (zp,zq)\r\nbench_mulPublic pt sk = do\r\n ct :: CT zp (Cyc zq) <- encrypt sk pt\r\n undefined ct\r\n\r\nencrypt :: forall z zp zq. Reduce z zq => Cyc z -> Cyc zp -> IO (CT zp (Cyc zq))\r\nencrypt = undefined\r\n}}}\r\n\r\nOn GHC 8.2.2, this compiles without issue. But on GHC 8.4.1-alpha2, this errors with:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:1: error:\r\n • Could not deduce (Reduce fsk0 zq)\r\n from the context: (z ~ LiftOf zq, Reduce fsk zq)\r\n bound by the inferred type for ‘bench_mulPublic’:\r\n forall z zp zq fsk.\r\n (z ~ LiftOf zq, Reduce fsk zq) =>\r\n Cyc zp -> Cyc z -> IO (zp, zq)\r\n at Bug.hs:(15,1)-(17,14)\r\n The type variable ‘fsk0’ is ambiguous\r\n • In the ambiguity check for the inferred type for ‘bench_mulPublic’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n When checking the inferred type\r\n bench_mulPublic :: forall z zp zq fsk.\r\n (z ~ LiftOf zq, Reduce fsk zq) =>\r\n Cyc zp -> Cyc z -> IO (zp, zq)\r\n |\r\n15 | bench_mulPublic pt sk = do\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/14643Partial type signatures in class constraints behave unexpectedly2019-07-07T18:16:10ZmnislaihPartial type signatures in class constraints behave unexpectedlyMinimal example:
```hs
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
module Minimal where
id [d|
f :: (Monad m, _) => [m a] -> m [a]
f' :: (Monad m, _) => [m a] -> m [a]
f = f'
f' [] = return [...Minimal example:
```hs
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
module Minimal where
id [d|
f :: (Monad m, _) => [m a] -> m [a]
f' :: (Monad m, _) => [m a] -> m [a]
f = f'
f' [] = return []
f' (x:xx) = f xx
|]
```
```
[1 of 1] Compiling Minimal ( /Users/pepe/Dropbox/code/debug-hoed/test/minimal.hs, interpreted )
/Users/pepe/Dropbox/code/debug-hoed/test/minimal.hs:5:1: warning: [-Wpartial-type-signatures]
• Found type wildcard ‘_’ standing for ‘()’
• In the type signature:
f :: (Monad m_a7NN, _) => [m_a7NN a_a7NO] -> m_a7NN [a_a7NO]
|
5 | id [d|
| ^^^^^^...
/Users/pepe/Dropbox/code/debug-hoed/test/minimal.hs:5:1: warning: [-Wpartial-type-signatures]
• Found type wildcard ‘_’ standing for ‘()’
• In the type signature:
f' :: (Monad m_a7NL, _) => [m_a7NL a_a7NM] -> m_a7NL [a_a7NM]
|
5 | id [d|
| ^^^^^^...
Ok, one module loaded.
:browse
f :: (Monad m, Monad m) => [m a] -> m [a]
f' :: (Monad m, Monad m) => [m a] -> m [a]
```
Notice the duplicate Monad m constraint.
Things get even more weird if the type signatures are declared together:
```hs
id [d|
f, f' :: (Monad m, _) => [m a] -> m [a]
f = f'
f' [] = return []
f' (x:xx) = f xx
|]
```
```
[1 of 1] Compiling Minimal ( /Users/pepe/Dropbox/code/debug-hoed/test/minimal.hs, interpreted )
/Users/pepe/Dropbox/code/debug-hoed/test/minimal.hs:5:1: warning: [-Wpartial-type-signatures]
• Found type wildcard ‘_’ standing for ‘()’
• In the type signature:
f :: (Monad m_a88E, _) => [m_a88E a_a88F] -> m_a88E [a_a88F]
|
5 | id [d|
| ^^^^^^...
/Users/pepe/Dropbox/code/debug-hoed/test/minimal.hs:5:1: warning: [-Wpartial-type-signatures]
• Found type wildcard ‘_’ standing for ‘()’
• In the type signature:
f' :: (Monad m_a88E, _) => [m_a88E a_a88F] -> m_a88E [a_a88F]
|
5 | id [d|
| ^^^^^^...
Ok, one module loaded.
:browse
f ::
(Monad ghc-prim-0.5.1.1:GHC.Types.Any, Monad m) =>
[ghc-prim-0.5.1.1:GHC.Types.Any ghc-prim-0.5.1.1:GHC.Types.Any]
-> ghc-prim-0.5.1.1:GHC.Types.Any [ghc-prim-0.5.1.1:GHC.Types.Any]
f' ::
(Monad ghc-prim-0.5.1.1:GHC.Types.Any, Monad m) => [m a] -> m [a]
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Partial type signatures in spliced TH declarations behave unexpectedly","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Minimal example:\r\n{{{#!hs\r\n{-# LANGUAGE PartialTypeSignatures #-}\r\n{-# LANGUAGE TemplateHaskell #-}\r\nmodule Minimal where\r\n\r\nid [d|\r\n f :: (Monad m, _) => [m a] -> m [a]\r\n f' :: (Monad m, _) => [m a] -> m [a]\r\n f = f'\r\n f' [] = return []\r\n f' (x:xx) = f xx\r\n |]\r\n}}}\r\n\r\n{{{\r\n[1 of 1] Compiling Minimal ( /Users/pepe/Dropbox/code/debug-hoed/test/minimal.hs, interpreted )\r\n\r\n/Users/pepe/Dropbox/code/debug-hoed/test/minimal.hs:5:1: warning: [-Wpartial-type-signatures]\r\n • Found type wildcard ‘_’ standing for ‘()’\r\n • In the type signature:\r\n f :: (Monad m_a7NN, _) => [m_a7NN a_a7NO] -> m_a7NN [a_a7NO]\r\n |\r\n5 | id [d|\r\n | ^^^^^^...\r\n\r\n/Users/pepe/Dropbox/code/debug-hoed/test/minimal.hs:5:1: warning: [-Wpartial-type-signatures]\r\n • Found type wildcard ‘_’ standing for ‘()’\r\n • In the type signature:\r\n f' :: (Monad m_a7NL, _) => [m_a7NL a_a7NM] -> m_a7NL [a_a7NM]\r\n |\r\n5 | id [d|\r\n | ^^^^^^...\r\nOk, one module loaded.\r\n :browse\r\nf :: (Monad m, Monad m) => [m a] -> m [a]\r\nf' :: (Monad m, Monad m) => [m a] -> m [a]\r\n}}}\r\n\r\nNotice the duplicate Monad m constraint.\r\n\r\nThings get even more weird if the type signatures are declared together:\r\n{{{#!hs\r\nid [d|\r\n f, f' :: (Monad m, _) => [m a] -> m [a]\r\n f = f'\r\n f' [] = return []\r\n f' (x:xx) = f xx\r\n |]\r\n}}}\r\n{{{\r\n[1 of 1] Compiling Minimal ( /Users/pepe/Dropbox/code/debug-hoed/test/minimal.hs, interpreted )\r\n\r\n/Users/pepe/Dropbox/code/debug-hoed/test/minimal.hs:5:1: warning: [-Wpartial-type-signatures]\r\n • Found type wildcard ‘_’ standing for ‘()’\r\n • In the type signature:\r\n f :: (Monad m_a88E, _) => [m_a88E a_a88F] -> m_a88E [a_a88F]\r\n |\r\n5 | id [d|\r\n | ^^^^^^...\r\n\r\n/Users/pepe/Dropbox/code/debug-hoed/test/minimal.hs:5:1: warning: [-Wpartial-type-signatures]\r\n • Found type wildcard ‘_’ standing for ‘()’\r\n • In the type signature:\r\n f' :: (Monad m_a88E, _) => [m_a88E a_a88F] -> m_a88E [a_a88F]\r\n |\r\n5 | id [d|\r\n | ^^^^^^...\r\nOk, one module loaded.\r\n :browse\r\nf ::\r\n (Monad ghc-prim-0.5.1.1:GHC.Types.Any, Monad m) =>\r\n [ghc-prim-0.5.1.1:GHC.Types.Any ghc-prim-0.5.1.1:GHC.Types.Any]\r\n -> ghc-prim-0.5.1.1:GHC.Types.Any [ghc-prim-0.5.1.1:GHC.Types.Any]\r\nf' ::\r\n (Monad ghc-prim-0.5.1.1:GHC.Types.Any, Monad m) => [m a] -> m [a]\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/14265kinded holes2019-07-07T18:17:42Zlspitznerkinded holesFor value-level holes, ghc kindly mentions the expected type. It does not do the same for holes in type signatures: mentioning the expected kind.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| -...For value-level holes, ghc kindly mentions the expected type. It does not do the same for holes in type signatures: mentioning the expected kind.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.2.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"kinded holes","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"For value-level holes, ghc kindly mentions the expected type. It does not do the same for holes in type signatures: mentioning the expected kind.","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/10242Multiple constraint wildcards allowed with PartialTypeSignatures2019-07-07T18:36:56ZMatthew PickeringMultiple constraint wildcards allowed with PartialTypeSignaturesThe [wiki](https://ghc.haskell.org/trac/ghc/wiki/PartialTypeSignatures) states that
> As a single extra-constraints wildcard is enough to infer any number of constraints, only one is allowed in a type signature and it should come last i...The [wiki](https://ghc.haskell.org/trac/ghc/wiki/PartialTypeSignatures) states that
> As a single extra-constraints wildcard is enough to infer any number of constraints, only one is allowed in a type signature and it should come last in the list of constraints.
However the following program compiles with GHC 7.10.1
```hs
{-# LANGUAGE PartialTypeSignatures #-}
f :: (Eq a, _, _) => a -> a -> Bool
f x y = x == y
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.10.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | alanz |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Multiple constraint wildcards allowed with PartialTypeSignatures","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.1","keywords":["PartialTypeSignatures"],"differentials":[],"test_case":"","architecture":"","cc":["alanz"],"type":"Bug","description":"The [https://ghc.haskell.org/trac/ghc/wiki/PartialTypeSignatures wiki] states that \r\n\r\n> As a single extra-constraints wildcard is enough to infer any number of constraints, only one is allowed in a type signature and it should come last in the list of constraints.\r\n\r\nHowever the following program compiles with GHC 7.10.1\r\n\r\n{{{#!hs\r\n{-# LANGUAGE PartialTypeSignatures #-}\r\n\r\nf :: (Eq a, _, _) => a -> a -> Bool\r\nf x y = x == y\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1thomaswthomaswhttps://gitlab.haskell.org/ghc/ghc/-/issues/20921Regression in ambiguity checking for partial type signatures in GHC 9.22022-02-21T11:13:10Zsheafsam.derbyshire@gmail.comRegression in ambiguity checking for partial type signatures in GHC 9.2The following program compiles on all GHC versions ranging from `8.6` to `9.0`, but fails on `9.2` and HEAD:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ...The following program compiles on all GHC versions ranging from `8.6` to `9.0`, but fails on `9.2` and HEAD:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module PsigBug where
import Data.Kind
( Constraint )
import GHC.TypeLits
( ErrorMessage(..), TypeError )
import GHC.TypeNats ( Nat )
type family OK (i :: Nat) :: Constraint where
OK 1 = ()
OK 2 = ()
OK n = TypeError (ShowType n :<>: Text "is not OK")
class C (i :: Nat) where
foo :: Int
instance C 1 where
foo = 1
instance C 2 where
foo = 2
type family Boo (i :: Nat) :: Nat where
Boo i = i
bar :: Int
bar =
let
quux :: forall (i :: Nat). ( OK (Boo i), _ ) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
```
```
PsigBug.hs:38:5: error:
* Could not deduce: OK i0
from the context: (OK (Boo i), C i)
bound by the inferred type for `quux':
forall (i :: Nat). (OK (Boo i), C i) => Int
at PsigBug.hs:38:5-23
* When checking that the inferred type
quux :: forall {i :: Nat}. (OK (Boo i), OK i, C i) => Int
is as general as its (partial) signature
quux :: forall (i :: Nat). (OK (Boo i), C i) => Int
In the expression:
let
quux :: forall (i :: Nat). (OK (Boo i), _) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
In an equation for `bar':
bar
= let
quux :: forall (i :: Nat). (OK (Boo i), _) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
|
38 | quux = foo @(Boo i)
| ^^^^^^^^^^^^^^^^^^^
PsigBug.hs:38:5: error:
* Could not deduce (C i0)
from the context: (OK (Boo i), C i)
bound by the inferred type for `quux':
forall (i :: Nat). (OK (Boo i), C i) => Int
at PsigBug.hs:38:5-23
The type variable `i0' is ambiguous
* When checking that the inferred type
quux :: forall {i :: Nat}. (OK (Boo i), OK i, C i) => Int
is as general as its (partial) signature
quux :: forall (i :: Nat). (OK (Boo i), C i) => Int
In the expression:
let
quux :: forall (i :: Nat). (OK (Boo i), _) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
In an equation for `bar':
bar
= let
quux :: forall (i :: Nat). (OK (Boo i), _) => Int
quux = foo @(Boo i)
in quux @1 + quux @2
|
38 | quux = foo @(Boo i)
| ^^^^^^^^^^^^^^^^^^^
```
These messages mention an ambiguous variable `i0`... but it doesn't actually appear anywhere in the rest of the messages!
This bug prevents one of my libraries from compiling (and I couldn't find a workaround), so this is not only of theoretical interest.9.2.2Simon Peyton JonesSimon Peyton Joneshttps://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/23223Misleading error message when lacking an extra-constraints wildcard2023-05-08T16:21:37ZSimon Peyton JonesMisleading error message when lacking an extra-constraints wildcardConsider this module
```
{-# LANGUAGE PartialTypeSignatures #-}
module Foo where
f :: (Show a) => a -> _ -> Bool
f x y = x>x
```
Note the partial type signature. We get `[W] Ord a` from the `x>x`, but there is no extra-constraints wild...Consider this module
```
{-# LANGUAGE PartialTypeSignatures #-}
module Foo where
f :: (Show a) => a -> _ -> Bool
f x y = x>x
```
Note the partial type signature. We get `[W] Ord a` from the `x>x`, but there is no extra-constraints wildcard, so we can't solve it. Currently GHC reports this:
```
Foo.hs:5:1: error: [GHC-39999]
Could not deduce ‘Ord a’
GHC Bug #20076 <https://gitlab.haskell.org/ghc/ghc/-/issues/20076>
Assuming you have a partial type signature, you can avoid this error
by either adding an extra-constraints wildcard (like `(..., _) => ...`,
with the underscore at the end of the constraint), or by avoiding the
use of a simplifiable constraint in your partial type signature.
from the context: Eq a
bound by the inferred type for ‘f’:
forall a {w}. Show a => a -> w -> Bool
at Foo.hs:5:1-11
```
The reference to #20076 is entirely bogus: there is no simplifiable constraint in sight. We simply have a constraint we can't solve.
#20076 remains valid...we "ought" to be able to solve that one. But the program reported above is much more likely to happen (who writes simplifiable constraints like #20076?), and is not a GHC error. The right thing is to add the extra-constraints wildcard.
--------------------
A second complication. If the program was like this (with no `Show a` constraint):
```
f2 :: a -> _ -> Bool
f2 x y = x>x
```
then we don't get the above error. We just get the fairly resonable:
```
Foo.hs:5:10: error: [GHC-39999]
• No instance for ‘Ord a’ arising from a use of ‘>’
Possible fix:
add (Ord a) to the context of
the inferred type of f2 :: a -> w -> Bool
```
Why the difference, just from adding or removing an unrelated (and unused) constraint?
It turns out to be because of `Note [Partial type signatures and the monomorphism restriction]`. We apply the MR to a binding group that has partial signature(s), none of which have an extra-constraints wildcard.
Is this a good idea? I don't know. But it took me 15 mins to track down so I'm recording it here.Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/22065Core Lint error from PartialTypeSignatures2022-08-18T20:59:40ZIcelandjackCore Lint error from PartialTypeSignaturesRunning on ghc-9.2.3, produces a Core Lint error:
```haskell
{-# Options_GHC -dcore-lint #-}
{-# Language PartialTypeSignatures #-}
data Foo where
Apply :: (x -> Int) -> x -> Foo
foo :: Foo
foo = Apply f x :: forall a. _ where
f ...Running on ghc-9.2.3, produces a Core Lint error:
```haskell
{-# Options_GHC -dcore-lint #-}
{-# Language PartialTypeSignatures #-}
data Foo where
Apply :: (x -> Int) -> x -> Foo
foo :: Foo
foo = Apply f x :: forall a. _ where
f :: [_] -> Int
f = length @[] @_
x :: [_]
x = mempty @[_]
```
```
ghci> :load ~/hs/5613.hs
[1 of 1] Compiling Main ( /home/baldur/hs/5613.hs, interpreted )
*** Core Lint errors : in result of Desugar (before optimization) ***
/home/baldur/hs/5613.hs:8:20: warning:
The type variable @k_a9Dn[sk:1] is out of scope
In the RHS of foo :: Foo
In the body of letrec with binders x_a9sr :: forall {w}. [w]
In the body of letrec with binders f_a9sq :: forall {w}. [w] -> Int
In the body of lambda with binder a_a9Dz :: k_a9Dn[sk:1]
Substitution: [TCvSubst
In scope: InScope {}
Type env: []
Co env: []]
*** Offending Program ***
Rec {
$tcFoo :: TyCon
[LclIdX]
$tcFoo
= TyCon
13795410111426859749##
2910294326838708211##
$trModule
(TrNameS "Foo"#)
0#
krep$*
$tc'Apply :: TyCon
[LclIdX]
$tc'Apply
= TyCon
16548517680761376676##
14341609333725595319##
$trModule
(TrNameS "'Apply"#)
1#
$krep_a9DG
$krep_a9DI [InlPrag=[~]] :: KindRep
[LclId]
$krep_a9DI = $WKindRepVar (I# 0#)
$krep_a9DH [InlPrag=[~]] :: KindRep
[LclId]
$krep_a9DH = KindRepFun $krep_a9DI $krep_a9DJ
$krep_a9DK [InlPrag=[~]] :: KindRep
[LclId]
$krep_a9DK = KindRepFun $krep_a9DI $krep_a9DL
$krep_a9DG [InlPrag=[~]] :: KindRep
[LclId]
$krep_a9DG = KindRepFun $krep_a9DH $krep_a9DK
$krep_a9DJ [InlPrag=[~]] :: KindRep
[LclId]
$krep_a9DJ = KindRepTyConApp $tcInt ([] @KindRep)
$krep_a9DL [InlPrag=[~]] :: KindRep
[LclId]
$krep_a9DL = KindRepTyConApp $tcFoo ([] @KindRep)
$trModule :: Module
[LclIdX]
$trModule
= Module (TrNameS "plutarch-core-0.1.0-inplace"#) (TrNameS "Main"#)
foo :: Foo
[LclIdX]
foo
= letrec {
x_a9sr :: forall {w}. [w]
[LclId]
x_a9sr
= \ (@w_a9CP) ->
let {
$dMonoid_a9CV :: Monoid [w_a9CP]
[LclId]
$dMonoid_a9CV = $fMonoid[] @w_a9CP } in
letrec {
x_a9CR :: [w_a9CP]
[LclId]
x_a9CR = break<0>() mempty @[w_a9CP] $dMonoid_a9CV; } in
x_a9CR; } in
letrec {
f_a9sq :: forall {w}. [w] -> Int
[LclId]
f_a9sq
= \ (@w_a9D6) ->
let {
$dFoldable_a9De :: Foldable []
[LclId]
$dFoldable_a9De = $fFoldable[] } in
letrec {
f_a9D8 :: [w_a9D6] -> Int
[LclId]
f_a9D8 = break<1>() length @[] $dFoldable_a9De @w_a9D6; } in
f_a9D8; } in
break<2>(x_a9sr,f_a9sq)
(\ (@(a_a9Dz :: k_a9Dn[sk:1])) ->
(\ (@k_a9Dn) (@(a_a9Do :: k_a9Dn)) ->
(\ (@x_X0) (ds_d9DO :: x_X0 -> Int) (ds_d9DP :: x_X0) ->
Apply @x_X0 ds_d9DO ds_d9DP)
@[Any @Type] (f_a9sq @(Any @Type)) (x_a9sr @(Any @Type)))
@(Any @Type) @(Any @(Any @Type)))
@(Any @k_a9Dn[sk:1])
end Rec }
*** End of Offense ***
<no location info>: error:
Compilation had errors
*** Exception: ExitFailure 1
ghci>
```https://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 Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/21416Extra-constraints wildcards in instance declarations2023-07-14T16:53:10ZAdam GundryExtra-constraints wildcards in instance declarationsExtra-constraints wildcards are sometimes handy for figuring out the constraints to put on a function definition. However, they cannot be used in instance declarations:
```
GHCi, version 9.2.2: https://www.haskell.org/ghc/ :? for help
g...Extra-constraints wildcards are sometimes handy for figuring out the constraints to put on a function definition. However, they cannot be used in instance declarations:
```
GHCi, version 9.2.2: https://www.haskell.org/ghc/ :? for help
ghci> let { foo :: _ => a -> String ; foo = show }
<interactive>:1:14: error:
• Found extra-constraints wildcard standing for ‘Show a’
Where: ‘a’ is a rigid type variable bound by
the inferred type of foo :: Show a => a -> String
at <interactive>:1:7-29
To use the inferred type, enable PartialTypeSignatures
• In the type signature: foo :: _ => a -> String
ghci> data I a = I a
ghci> instance _ => Show (I a) where show (I x) = show x
<interactive>:3:10: error:
Wildcard ‘_’ not allowed
in an instance declaration
```
Is there a fundamental reason for this restriction? It seems to me that it should be possible to infer the extra constraints required by an instance, just as GHC already does for functions (though I can imagine the implementation might be slightly less trivial because it would need to gather the wanted constraints from all the methods, then simplify them).https://gitlab.haskell.org/ghc/ghc/-/issues/20154Partial kind signatures and synonyms2023-07-14T19:19:51ZKrzysztof GogolewskiPartial kind signatures and synonymsThis works:
```
ghci> :kind (Maybe :: _)
<interactive>:1:11: error:
• Found type wildcard ‘_’ standing for ‘* -> *’
To use the inferred type, enable PartialTypeSignatures
• In the kind ‘_’
In the type ‘(Maybe :: _)’...This works:
```
ghci> :kind (Maybe :: _)
<interactive>:1:11: error:
• Found type wildcard ‘_’ standing for ‘* -> *’
To use the inferred type, enable PartialTypeSignatures
• In the kind ‘_’
In the type ‘(Maybe :: _)’
```
This doesn't work:
```
ghci> type T = (Maybe :: _)
<interactive>:2:20: error:
Wildcard ‘_’ not allowed
in the declaration for type synonym ‘T’
```
Maybe there's a deeper reason why, but I naively expect the second command to show the partial kind signature.https://gitlab.haskell.org/ghc/ghc/-/issues/20076Partial type signatures regression around simplifiable constraints2023-06-14T11:03:30ZRichard Eisenbergrae@richarde.devPartial type signatures regression around simplifiable constraints**Important**: see #23223.
Consider
```hs
{-# LANGUAGE FlexibleContexts, PartialTypeSignatures #-}
module Bug where
f :: Eq [a] => a -> _
f x = [x] == [x]
```
This program is accepted in GHC 9.0.1, but rejected by HEAD. The problem ...**Important**: see #23223.
Consider
```hs
{-# LANGUAGE FlexibleContexts, PartialTypeSignatures #-}
module Bug where
f :: Eq [a] => a -> _
f x = [x] == [x]
```
This program is accepted in GHC 9.0.1, but rejected by HEAD. The problem is that we get a `[W] Eq [a]` from the function body, and then this is simplified to `[W] Eq a`... which cannot be satisfied.
The solution, I think, is to bring `Eq [a]` into scope as a Given, not a Wanted.
I have not tested it, but I smell the culprit in 5650c79e0087fb37311fbe81a2ce6f63b36b91d3, @simonpj.https://gitlab.haskell.org/ghc/ghc/-/issues/19106Partial type signature variable confuses instance solving2023-04-06T09:45:59ZRichard Eisenbergrae@richarde.devPartial type signature variable confuses instance solvingWhen I say
```hs
{-# LANGUAGE TypeFamilies, GADTs #-}
module Bug where
f :: (a ~ [b]) => T a -> _ -> String
f (MkT x) _ = show x
data T a where
MkT :: G a => a -> T a
type family G a where
G [b] = Show b
```
I get
```
Bug.hs:6...When I say
```hs
{-# LANGUAGE TypeFamilies, GADTs #-}
module Bug where
f :: (a ~ [b]) => T a -> _ -> String
f (MkT x) _ = show x
data T a where
MkT :: G a => a -> T a
type family G a where
G [b] = Show b
```
I get
```
Bug.hs:6:1: error:
• Could not deduce (Show b)
from the context: a ~ [b]
bound by the inferred type for ‘f’:
forall a b {w}. (a ~ [b]) => T a -> w -> String
at Bug.hs:6:1-20
• When checking that the inferred type
f :: forall {a} {b} {w}. (a ~ [b], Show [b]) => T a -> w -> String
is as general as its (partial) signature
f :: forall a b {w}. (a ~ [b]) => T a -> w -> String
```
We end up with
```
[G] Show b[tyv:1]
[W] Show [b[tyv:1]]
```
The check in `matchableGivens` considers `b` a meta-variable. This isn't entirely wrong, but `b` is a `TyVarTv`, and should not be considered unifiable in `matchableGivens`. The solution is very easy: just change `matchableGivens` to treat `TyVarTv`s like skolems.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.dev