GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2024-03-11T09:00:53Zhttps://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/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/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/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/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.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/19051Allow named wildcards in constraints2020-12-23T15:23:55Zsheafsam.derbyshire@gmail.comAllow named wildcards in constraints```haskell
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE NamedWildCards #-}
{-# LANGUAGE PartialTypeSignatures #-}
module Test where
class C a where
meth :: a
unnamed :: _ => a
unnamed = meth
named :: _c => a
named = m...```haskell
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE NamedWildCards #-}
{-# LANGUAGE PartialTypeSignatures #-}
module Test where
class C a where
meth :: a
unnamed :: _ => a
unnamed = meth
named :: _c => a
named = meth
```
The `unnamed` version causes no problems, however `named` causes the following error:
```
* Could not deduce: _0
from the context: _
bound by the inferred type for `named':
forall a (_ :: Constraint). _ => a
at Test.hs:14:1-12
* In the ambiguity check for the inferred type for `named'
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the inferred type
named :: forall a (_ :: Constraint). _ => a
|
14 | named = meth
| ^^^^^^^^^^^^
```
That is, in this example, `_c` is **not** a named wildcard, but is instead universally quantified. So GHC unsurprisingly throws the same error as if we had written
```haskell
universal :: c => a
universal = meth
```
I would have expected that the named wildcard `_c` behave just like the wildcard `_`, except that it would give me the ability to refer to the inferred constraint at the type-level inside the body of `named`.
(I came across this while thinking about #19010.)https://gitlab.haskell.org/ghc/ghc/-/issues/19013Type wildcard infers differently than no type signature2020-12-10T00:22:10ZdminuosoType wildcard infers differently than no type signature```haskell
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PartialTypeSignatures #-}
module Main where
import Optics
main :: IO ()
main = putStrLn "Hello, Haskell!"
g :: Lens' String Char ...```haskell
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PartialTypeSignatures #-}
module Main where
import Optics
main :: IO ()
main = putStrLn "Hello, Haskell!"
g :: Lens' String Char
g = undefined
f :: _
f o = "foo" & (g%o) .~ 10
```
Full source code of the test case at: https://gitlab.haskell.org/dminuoso/ghc-wildcard-bug/
The above code fails to type check with:
Without the wildcard type annotation on `f` it compiles and infers the following type for `f`:
```
*Main> :t f
f :: (Is (Join A_Lens l) A_Setter, Is l (Join A_Lens l),
Is A_Lens (Join A_Lens l), Num b) =>
Optic l js Char Char a b -> String
*Main>
```
Leaving the wildcard in, the type checker bails out.
```
[nix-shell:~/git/ghc-wildcard-bug]$ cabal build
Build profile: -w ghc-8.8.4 -O1
In order, the following will be built (use -v for more details):
- ghc-wildcard-bug-0.1.0.0 (exe:ghc-wildcard-bug) (file Main.hs changed)
Preprocessing executable 'ghc-wildcard-bug' for ghc-wildcard-bug-0.1.0.0..
Building executable 'ghc-wildcard-bug' for ghc-wildcard-bug-0.1.0.0..
[1 of 1] Compiling Main ( Main.hs, /home/dminuoso/git/ghc-wildcard-bug/dist-newstyle/build/x86_64-linux/ghc-8.8.4/ghc-wildcard-bug-0.1.0.0/x/ghc-wildcard-bug/build/ghc-wildcard-bug/ghc-wildcard-bug-tmp/Main.o )
Main.hs:15:15: error:
• Overlapping instances for Is (Join A_Lens l0) A_Setter
arising from a use of ‘.~’
Matching instances:
instance [overlappable] (TypeError ...) => Is k l
-- Defined in ‘optics-core-0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is k k
-- Defined in ‘optics-core-0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is A_Lens A_Setter
-- Defined in ‘optics-core-0.3.0.1:Optics.Internal.Optic.Subtyping’
...plus four others
(use -fprint-potential-instances to see them all)
(The choice depends on the instantiation of ‘l0’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the second argument of ‘(&)’, namely ‘(g % o) .~ 10’
In the expression: "foo" & (g % o) .~ 10
In an equation for ‘f’: f o = "foo" & (g % o) .~ 10
|
15 | f o = "foo" & (g%o) .~ 10
| ^^^^^^^^^^^
Main.hs:15:16: error:
• Overlapping instances for Is l0 (Join A_Lens l0)
arising from a use of ‘%’
Matching instances:
instance [overlappable] (TypeError ...) => Is k l
-- Defined in ‘optics-core-0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is k k
-- Defined in ‘optics-core-0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is A_Getter A_Fold
-- Defined in ‘optics-core-0.3.0.1:Optics.Internal.Optic.Subtyping’
...plus 35 others
(use -fprint-potential-instances to see them all)
(The choice depends on the instantiation of ‘l0’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the first argument of ‘(.~)’, namely ‘(g % o)’
In the second argument of ‘(&)’, namely ‘(g % o) .~ 10’
In the expression: "foo" & (g % o) .~ 10
|
15 | f o = "foo" & (g%o) .~ 10
|
```
Also tried enabling NoMonomorphismRestriction to no avail.https://gitlab.haskell.org/ghc/ghc/-/issues/19010Partial type signature algorithm fails to infer constraints in the presence o...2020-12-20T03:26:43Zsheafsam.derbyshire@gmail.comPartial type signature algorithm fails to infer constraints in the presence of GADTsI've been running into a few issues with partial type signatures as of late.
In my [graphics shader library](https://gitlab.com/sheaf/fir), users write programs using an indexed monad which keeps track of various pieces of informati...I've been running into a few issues with partial type signatures as of late.
In my [graphics shader library](https://gitlab.com/sheaf/fir), users write programs using an indexed monad which keeps track of various pieces of information as they write the program, which are used to perform validation using type families. It would be impossible for the user to manually write the types of the indexed monad (they can become very large), so partial type signatures are a crucial tool in this situation.
However, I'm running into some situations in which GHC fails to infer a constraint, even though it is happy to report error messages that say exactly which constraints are missing.
After a fair bit of effort, I've finally managed to come up with a small reproducer:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where
data SBool ( bool :: Bool ) where
STrue :: SBool True
SFalse :: SBool False
class C a where
methC :: a -> Float
class D a where
methD :: a -> Float
foo :: forall bool a. _ => SBool bool -> a -> Float
foo sBool a = meth a
where
meth :: _ => a -> Float
meth = case sBool of
STrue -> methC
SFalse -> methD
```
produces the following error:
```
[1 of 1] Compiling Bug ( bug.hs, bug.o )
bug.hs:23:17: error:
* Could not deduce (C a) arising from a use of `methC'
from the context: bool ~ 'True
bound by a pattern with constructor: STrue :: SBool 'True,
in a case alternative
at bug.hs:23:7-11
Possible fix:
add (C a) to the context of
the inferred type of foo :: SBool bool -> a -> Float
* In the expression: methC
In a case alternative: STrue -> methC
In the expression:
case sBool of
STrue -> methC
SFalse -> methD
|
23 | STrue -> methC
| ^^^^^
bug.hs:24:17: error:
* Could not deduce (D a) arising from a use of `methD'
from the context: bool ~ 'False
bound by a pattern with constructor: SFalse :: SBool 'False,
in a case alternative
at bug.hs:24:7-12
Possible fix:
add (D a) to the context of
the inferred type of foo :: SBool bool -> a -> Float
* In the expression: methD
In a case alternative: SFalse -> methD
In the expression:
case sBool of
STrue -> methC
SFalse -> methD
|
24 | SFalse -> methD
| ^^^^^
```
If one follows the error messages that GHC provides, by adding the constraint `( C a, D a )` to `meth`, then the program compiles. So it's curious that GHC is able to pinpoint the missing constraints, but not actually put them in the hole.
I also notice that this issue remains if one uses `methC` in both branches. If one changes `SBool` to `Bool` then of course it works fine.
I assume that this happens because the partial type signature algorithm is conservative in the presence of GADTs: one could potentially learn information upon matching a GADT that would help solve the constraints, and one would not want that evidence to float out in any way. However, in this case, I think we can agree that the evidence provided by the GADT match doesn't interact in any way with the constraints on the RHS (as nothing involves `bool`), i.e. it's as if we had just matched on a `Bool`.
<hr>
Versions of GHC tried: 8.8, 8.10, 9.0 (all with the same result).https://gitlab.haskell.org/ghc/ghc/-/issues/18929Investigate touchable meta-variables in Givens2021-01-02T14:14:41ZRichard Eisenbergrae@richarde.devInvestigate touchable meta-variables in Givens@simonpj believes it would be disastrous to ever have a touchable meta-variable in a Given. I'm not quite as sure what the disaster would be, but I admit such a situation is suspect. But we can concoct such a thing:
```hs
{-# LANGUAGE P...@simonpj believes it would be disastrous to ever have a touchable meta-variable in a Given. I'm not quite as sure what the disaster would be, but I admit such a situation is suspect. But we can concoct such a thing:
```hs
{-# LANGUAGE PolyKinds, PartialTypeSignatures #-}
module Bug where
import Data.Proxy
class C a where
meth :: Proxy a -> ()
f :: C a => Proxy a -> _
f p = meth p
```
The partial signature for `f` is not kind-generalized (the fact that it is partial means that we might want the definition of `f` to inform the kind of `a`) and thus the kind of `a` remains as a meta-variable `kappa`. In the body of `f`, we have `[G] C kappa a`. We can see this in this snippet of `-ddump-tc-trace` (with `-fprint-explicit-kinds` enabled):
```
tclevel = 1
work item = [WD] $dC_aoV {0}:: C @{k_aoT[tau:1]}
a_aoU[tau:1] (CNonCanonical)
inerts = {Dictionaries = [G] $dC_aoX {0}:: C @{k_aoT[tau:1]}
a_aoJ[tyv:1] (CDictCan)
```
The variable `k_aoT[tau:1]` is touchable and is not yet filled in. (It ends up being skolemised and quantified over, quite correctly.)
This ticket is to determine whether this situation is pernicious, and, if it is, figure out a way to rule it out.https://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/17432Wildcards in standalone kind signatures2023-07-14T19:19:52ZRichard Eisenbergrae@richarde.devWildcards in standalone kind signaturesWe should allow partial kind signatures as well as partial type signatures:
```hs
type Maybe :: _ -> Type
data Maybe a = Nothing | Just a
type Proxy :: forall (k :: _). k -> _
data Proxy = MkP
```
Of course, this would mean that polym...We should allow partial kind signatures as well as partial type signatures:
```hs
type Maybe :: _ -> Type
data Maybe a = Nothing | Just a
type Proxy :: forall (k :: _). k -> _
data Proxy = MkP
```
Of course, this would mean that polymorphic recursion would not be allowed. It's all just like at the term level.https://gitlab.haskell.org/ghc/ghc/-/issues/17024Poor interaction between functional dependencies and partial type signatures2020-03-12T13:58:57ZDavid FeuerPoor interaction between functional dependencies and partial type signatures## Summary
A fundep is surprisingly unable to fill in a partial type signature
## Steps to reproduce
```haskell
{-# language TypeFamilies, FunctionalDependencies, GADTs, DataKinds, TypeOperators, ScopedTypeVariables, FlexibleInstances...## Summary
A fundep is surprisingly unable to fill in a partial type signature
## Steps to reproduce
```haskell
{-# language TypeFamilies, FunctionalDependencies, GADTs, DataKinds, TypeOperators, ScopedTypeVariables, FlexibleInstances , UndecidableInstances, PartialTypeSignatures #-}
infixr 6 :::
data HList xs where
HNil :: HList '[]
(:::) :: a -> HList as -> HList (a ': as)
class AppHList ts o f | ts f -> o, ts o -> f where
appHList :: f -> HList ts -> o
instance AppHList '[] o o where
appHList x HNil = x
instance AppHList ts o f => AppHList (t : ts) o (t -> f) where
appHList f (x ::: xs) = appHList (f x) xs
foo :: (a -> b -> c) -> HList '[a, b] -> _
foo = appHList
```
This fails with
```
AbstractList.hs:35:7: error:
• Couldn't match type ‘c’ with ‘w0’
arising from a functional dependency between:
constraint ‘AppHList '[] w0 c’ arising from a use of ‘appHList’
instance ‘AppHList '[] o o’ at AbstractList.hs:29:10-25
‘c’ is a rigid type variable bound by
the inferred type of foo :: (a -> b -> c) -> HList '[a, b] -> w0
at AbstractList.hs:35:1-14
• In the expression: appHList
In an equation for ‘foo’: foo = appHList
• Relevant bindings include
foo :: (a -> b -> c) -> HList '[a, b] -> w0
(bound at AbstractList.hs:35:1)
```
## Expected behavior
I'd expect GHC to fill in `_` with `c`. Indeed, if I leave out the type signature and write
```haskell
foo (f :: a -> b -> c) (args :: HList '[a, b]) = appHList f args
```
then GHC correctly infers `foo :: (a -> b -> c) -> HList '[a, b] -> c`.
## Environment
* GHC version used: 8.6.3
Optional:
* Operating System:
* System Architecture:https://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/16763Partial type signatures sometimes gets their ordering wrong2019-06-08T12:28:07ZRichard Eisenbergrae@richarde.devPartial type signatures sometimes gets their ordering wrongIf I write
```
f1 :: forall b a. a -> b -> _
f1 x _ = x
```
GHC cleverly quantifies `b` before `a`, allowing visible type application to work as the user might expect.
But here are two cases where GHC is not so clever:
*Case 1:*
```...If I write
```
f1 :: forall b a. a -> b -> _
f1 x _ = x
```
GHC cleverly quantifies `b` before `a`, allowing visible type application to work as the user might expect.
But here are two cases where GHC is not so clever:
*Case 1:*
```
f2 :: forall k (a :: k). k -> Proxy (a :: k)
f2 _ = Proxy
f3 :: forall a k. k -> Proxy (a :: _)
f3 = f2
```
Of course, `f3`'s type is bogus: `k` has to come before `a`. And indeed GHC swizzles these around -- but it shouldn't. Better would be to reject, because the user has requested the impossible.
*Case 2:*
```
f4 :: forall a b. a -> b -> _
f5 :: forall b a. a -> b -> _
f4 = f5
f5 = f4
```
Note that the ordering of variables in `f4` and `f5` is different. Yet GHC assigns the same quantification order to both.
*Solution:*
Currently, the working case works because of a series of delicate dependencies, starting with code in `decideQuantifiedTyVars` that sets an initial (correct) order, and blindly hopes that various data structures and functions preserve the order. They do, most of the time, but not in the cases above. Yet these functions are not really concerned with ordering, and so this might change in the future.
Better would be to fix the ordering in `chooseInferredQuantifiers`, which happens right at the end. At this point, we have the `psig_tvs`, which are the tvs as the user wrote them; and the `qtvs`, which are the variables that `simplifyInfer` has indicated should be quantified over. It should always be the case that `qtvs` is a superset of `psig_tvs`.
1. Compute `inferred = qtvs \\ psig_tvs`, where `\\` denotes set-subtraction.
2. Compute `final_qtvs = scopedSort (inferred ++ psig_tvs)`. That is, we seed `scopedSort` with the correct ordering. And we suggest that the `inferred` should go first.
3. Check that the ordering of the `psig_tvs` within `final_qtvs` is as expected. (That is, `psig_tvs` should be a subsequence of `final_qtvs`.) If not, error.
4. Label the qtvs correctly as `Specified` or `Inferred` (perhaps this can be done while doing step 3).
And off you go!Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://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 Scott