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/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/16203Unhelpful names for wildcard type variables2023-08-07T07:43:35ZSimon Peyton JonesUnhelpful names for wildcard type variablesConsider
```
{-# LANGUAGE PartialTypeSignatures #-}
f :: _ -> _
f x = x
```
With GHC 8.6 we got
```
T16152.hs:10:6: warning: [-Wpartial-type-signatures]
• Found type wildcard ‘_’ standing for ‘w’
Where: ‘w’ is a rigid type ...Consider
```
{-# LANGUAGE PartialTypeSignatures #-}
f :: _ -> _
f x = x
```
With GHC 8.6 we got
```
T16152.hs:10:6: warning: [-Wpartial-type-signatures]
• Found type wildcard ‘_’ standing for ‘w’
Where: ‘w’ is a rigid type variable bound by
the inferred type of f :: w -> w
at T16152.hs:11:1-7
• In the type signature: f :: _ -> _
|
10 | f :: _ -> _
| ^
T16152.hs:10:11: warning: [-Wpartial-type-signatures]
• Found type wildcard ‘_’ standing for ‘w’
Where: ‘w’ is a rigid type variable bound by
the inferred type of f :: w -> w
at T16152.hs:11:1-7
• In the type signature: f :: _ -> _
|
10 | f :: _ -> _
| ^
```
But with HEAD we get
```
T16152.hs:10:6: warning: [-Wpartial-type-signatures]
• Found type wildcard ‘_’ standing for ‘_’
Where: ‘_’ is a rigid type variable bound by
the inferred type of f :: _ -> _
at T16152.hs:11:1-7
• In the type ‘_ -> _’
In the type signature: f :: _ -> _
|
10 | f :: _ -> _
| ^
T16152.hs:10:11: warning: [-Wpartial-type-signatures]
• Found type wildcard ‘_’ standing for ‘_’
Where: ‘_’ is a rigid type variable bound by
the inferred type of f :: _ -> _
at T16152.hs:11:1-7
• In the type ‘_ -> _’
In the type signature: f :: _ -> _
|
10 | f :: _ -> _
| ^
```
Saying "Found type wildcard ‘_’ standing for ‘_’" is unhelpful. The "w" form is much better.
The change is caused by
```
commit 17bd163566153babbf51adaff8397f948ae363ca
Author: mynguyen <mnguyen1@brynmawr.edu>
Date: Tue Dec 18 11:52:26 2018 -0500
Visible kind application
```
which has this patch
```
-newWildTyVar _name
+newWildTyVar
= do { kind <- newMetaKindVar
; uniq <- newUnique
; details <- newMetaDetails TauTv
- ; let name = mkSysTvName uniq (fsLit "w")
+ ; let name = mkSysTvName uniq (fsLit "_")
tyvar = (mkTcTyVar name kind details)
; traceTc "newWildTyVar" (ppr tyvar)
; return tyvar }
```
What was the reason for this change? Can we change "_" back to "w" please?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.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":"Unhelpful names for wildcard type variables","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider\r\n{{{\r\n{-# LANGUAGE PartialTypeSignatures #-}\r\n\r\nf :: _ -> _\r\nf x = x\r\n}}}\r\nWith GHC 8.6 we got\r\n{{{\r\nT16152.hs:10:6: warning: [-Wpartial-type-signatures]\r\n • Found type wildcard ‘_’ standing for ‘w’\r\n Where: ‘w’ is a rigid type variable bound by\r\n the inferred type of f :: w -> w\r\n at T16152.hs:11:1-7\r\n • In the type signature: f :: _ -> _\r\n |\r\n10 | f :: _ -> _\r\n | ^\r\n\r\nT16152.hs:10:11: warning: [-Wpartial-type-signatures]\r\n • Found type wildcard ‘_’ standing for ‘w’\r\n Where: ‘w’ is a rigid type variable bound by\r\n the inferred type of f :: w -> w\r\n at T16152.hs:11:1-7\r\n • In the type signature: f :: _ -> _\r\n |\r\n10 | f :: _ -> _\r\n | ^\r\n}}}\r\nBut with HEAD we get\r\n{{{\r\nT16152.hs:10:6: warning: [-Wpartial-type-signatures]\r\n • Found type wildcard ‘_’ standing for ‘_’\r\n Where: ‘_’ is a rigid type variable bound by\r\n the inferred type of f :: _ -> _\r\n at T16152.hs:11:1-7\r\n • In the type ‘_ -> _’\r\n In the type signature: f :: _ -> _\r\n |\r\n10 | f :: _ -> _\r\n | ^\r\n\r\nT16152.hs:10:11: warning: [-Wpartial-type-signatures]\r\n • Found type wildcard ‘_’ standing for ‘_’\r\n Where: ‘_’ is a rigid type variable bound by\r\n the inferred type of f :: _ -> _\r\n at T16152.hs:11:1-7\r\n • In the type ‘_ -> _’\r\n In the type signature: f :: _ -> _\r\n |\r\n10 | f :: _ -> _\r\n | ^\r\n}}}\r\nSaying \"Found type wildcard ‘_’ standing for ‘_’\" is unhelpful. The \"w\" form is much better.\r\n\r\nThe change is caused by\r\n{{{\r\ncommit 17bd163566153babbf51adaff8397f948ae363ca\r\nAuthor: mynguyen <mnguyen1@brynmawr.edu>\r\nDate: Tue Dec 18 11:52:26 2018 -0500\r\n\r\n Visible kind application\r\n}}}\r\nwhich has this patch\r\n{{{\r\n-newWildTyVar _name\r\n+newWildTyVar\r\n = do { kind <- newMetaKindVar\r\n ; uniq <- newUnique\r\n ; details <- newMetaDetails TauTv\r\n- ; let name = mkSysTvName uniq (fsLit \"w\")\r\n+ ; let name = mkSysTvName uniq (fsLit \"_\")\r\n tyvar = (mkTcTyVar name kind details)\r\n ; traceTc \"newWildTyVar\" (ppr tyvar)\r\n ; return tyvar }\r\n}}}\r\nWhat was the reason for this change? Can we change \"_\" back to \"w\" please?\r\n","type_of_failure":"OtherFailure","blocking":[]} -->Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://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/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/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/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/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/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/14766Hole-y partial type signatures greatly slow down compile times2023-02-09T11:00:59ZAlec TheriaultHole-y partial type signatures greatly slow down compile timesThis time, I actually mean it. :)
Originally reported [here](https://github.com/simonmar/happy/issues/109), I distilled the example from [this comment](https://github.com/simonmar/happy/issues/109#issuecomment-362957245) into a one file...This time, I actually mean it. :)
Originally reported [here](https://github.com/simonmar/happy/issues/109), I distilled the example from [this comment](https://github.com/simonmar/happy/issues/109#issuecomment-362957245) into a one file test case. `Sigs.hs` is exactly like `NoSigs.hs`, except for the fact that it has a bunch of extra type signatures that have a lot of holes. On my machine, this is what compilation times are (I gave up timing after 15 minutes):
<table><tr><td> GHC version </td>
<td> 8.0.2 </td>
<td> 8.2.1 </td>
<td> 8.4.1 (445554b6d9a2263f969e25bb9f532dd0c3a9dc8c) </td></tr>
<tr><td> `NoSigs.hs` </td>
<td> 24.13s </td>
<td> 22.93s </td>
<td> 34.05s </td></tr>
<tr><td> `Sigs.hs` </td>
<td> \>15m </td>
<td> \~13m </td>
<td> \>15m </td></tr></table>https://gitlab.haskell.org/ghc/ghc/-/issues/16152Core lint error from PartialTypeSignatures2022-10-27T21:15:59ZIcelandjackCore lint error from PartialTypeSignatures```hs
{-# Language PartialTypeSignatures #-}
{-# Language PolyKinds #-}
{-# Language ScopedTypeVariables #-}
{-# Options_GHC -dcore-lint #-}
top :: forall f. _
top = undefined where
x :: forall a. f a
x = undefined
`...```hs
{-# Language PartialTypeSignatures #-}
{-# Language PolyKinds #-}
{-# Language ScopedTypeVariables #-}
{-# Options_GHC -dcore-lint #-}
top :: forall f. _
top = undefined where
x :: forall a. f a
x = undefined
```
causes Core lint errors:
```
$ ~/../inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 922_bug.hs
GHCi, version 8.7.20181230: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 922_bug.hs, interpreted )
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
In the type ‘forall (f :: k_a1z6 -> *) w. w’
@ k_a1z6 is out of scope
*** Offending Program ***
Rec {
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "Main"#)
top :: forall (f :: k_a1z6 -> *) w. w
[LclIdX]
top
= \ (@ (f_a2BY :: k_a1z6 -> *)) (@ w_a2BZ) ->
(\ (@ k_a1z6) (@ (f_a1yV :: k_a1z6 -> *)) (@ w_a1yN) ->
let {
$dIP_a2BO :: ?callStack::CallStack
[LclId]
$dIP_a2BO
= emptyCallStack
`cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
:: CallStack ~R# (?callStack::CallStack)) } in
let {
$dIP_a2BD :: HasCallStack
[LclId]
$dIP_a2BD
= (pushCallStack
(unpackCString# "undefined"#,
SrcLoc
(unpackCString# "main"#)
(unpackCString# "Main"#)
(unpackCString# "922_bug.hs"#)
(I# 8#)
(I# 7#)
(I# 8#)
(I# 16#))
($dIP_a2BO
`cast` (N:IP[0] <"callStack">_N <CallStack>_N
:: (?callStack::CallStack) ~R# CallStack)))
`cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
:: CallStack ~R# (?callStack::CallStack)) } in
letrec {
top_a1yW :: w_a1yN
[LclId]
top_a1yW
= letrec {
x_a1yv :: forall (a :: k_a1z6). f_a1yV a
[LclId]
x_a1yv
= \ (@ (a_a1zd :: k_a1z6)) ->
let {
$dIP_a2BP :: ?callStack::CallStack
[LclId]
$dIP_a2BP
= emptyCallStack
`cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
:: CallStack ~R# (?callStack::CallStack)) } in
let {
$dIP_a2Bz :: HasCallStack
[LclId]
$dIP_a2Bz
= (pushCallStack
(unpackCString# "undefined"#,
SrcLoc
(unpackCString# "main"#)
(unpackCString# "Main"#)
(unpackCString# "922_bug.hs"#)
(I# 11#)
(I# 7#)
(I# 11#)
(I# 16#))
($dIP_a2BP
`cast` (N:IP[0] <"callStack">_N <CallStack>_N
:: (?callStack::CallStack) ~R# CallStack)))
`cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
:: CallStack ~R# (?callStack::CallStack)) } in
break<0>() undefined @ 'LiftedRep @ (f_a1yV a_a1zd) $dIP_a2Bz; } in
break<1>() undefined @ 'LiftedRep @ w_a1yN $dIP_a2BD; } in
top_a1yW)
@ Any @ Any @ w_a2BZ
end Rec }
*** End of Offense ***
<no location info>: error:
Compilation had errors
*** Exception: ExitFailure 1
>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.7 |
| 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":"Core lint error from PartialTypeSignatures","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":["PartialTypeSignatures"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# Language PartialTypeSignatures #-}\r\n{-# Language PolyKinds #-}\r\n{-# Language ScopedTypeVariables #-}\r\n\r\n{-# Options_GHC -dcore-lint #-}\r\n\r\ntop :: forall f. _\r\ntop = undefined where\r\n\r\n x :: forall a. f a\r\n x = undefined\r\n}}}\r\n\r\ncauses Core lint errors:\r\n\r\n{{{\r\n$ ~/../inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 922_bug.hs\r\nGHCi, version 8.7.20181230: https://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 922_bug.hs, interpreted )\r\n*** Core Lint errors : in result of Desugar (before optimization) ***\r\n<no location info>: warning:\r\n In the type ‘forall (f :: k_a1z6 -> *) w. w’\r\n @ k_a1z6 is out of scope\r\n*** Offending Program ***\r\nRec {\r\n$trModule :: Module\r\n[LclIdX]\r\n$trModule = Module (TrNameS \"main\"#) (TrNameS \"Main\"#)\r\n\r\ntop :: forall (f :: k_a1z6 -> *) w. w\r\n[LclIdX]\r\ntop\r\n = \\ (@ (f_a2BY :: k_a1z6 -> *)) (@ w_a2BZ) ->\r\n (\\ (@ k_a1z6) (@ (f_a1yV :: k_a1z6 -> *)) (@ w_a1yN) ->\r\n let {\r\n $dIP_a2BO :: ?callStack::CallStack\r\n [LclId]\r\n $dIP_a2BO\r\n = emptyCallStack\r\n `cast` (Sym (N:IP[0] <\"callStack\">_N <CallStack>_N)\r\n :: CallStack ~R# (?callStack::CallStack)) } in\r\n let {\r\n $dIP_a2BD :: HasCallStack\r\n [LclId]\r\n $dIP_a2BD\r\n = (pushCallStack\r\n (unpackCString# \"undefined\"#,\r\n SrcLoc\r\n (unpackCString# \"main\"#)\r\n (unpackCString# \"Main\"#)\r\n (unpackCString# \"922_bug.hs\"#)\r\n (I# 8#)\r\n (I# 7#)\r\n (I# 8#)\r\n (I# 16#))\r\n ($dIP_a2BO\r\n `cast` (N:IP[0] <\"callStack\">_N <CallStack>_N\r\n :: (?callStack::CallStack) ~R# CallStack)))\r\n `cast` (Sym (N:IP[0] <\"callStack\">_N <CallStack>_N)\r\n :: CallStack ~R# (?callStack::CallStack)) } in\r\n letrec {\r\n top_a1yW :: w_a1yN\r\n [LclId]\r\n top_a1yW\r\n = letrec {\r\n x_a1yv :: forall (a :: k_a1z6). f_a1yV a\r\n [LclId]\r\n x_a1yv\r\n = \\ (@ (a_a1zd :: k_a1z6)) ->\r\n let {\r\n $dIP_a2BP :: ?callStack::CallStack\r\n [LclId]\r\n $dIP_a2BP\r\n = emptyCallStack\r\n `cast` (Sym (N:IP[0] <\"callStack\">_N <CallStack>_N)\r\n :: CallStack ~R# (?callStack::CallStack)) } in\r\n let {\r\n $dIP_a2Bz :: HasCallStack\r\n [LclId]\r\n $dIP_a2Bz\r\n = (pushCallStack\r\n (unpackCString# \"undefined\"#,\r\n SrcLoc\r\n (unpackCString# \"main\"#)\r\n (unpackCString# \"Main\"#)\r\n (unpackCString# \"922_bug.hs\"#)\r\n (I# 11#)\r\n (I# 7#)\r\n (I# 11#)\r\n (I# 16#))\r\n ($dIP_a2BP\r\n `cast` (N:IP[0] <\"callStack\">_N <CallStack>_N\r\n :: (?callStack::CallStack) ~R# CallStack)))\r\n `cast` (Sym (N:IP[0] <\"callStack\">_N <CallStack>_N)\r\n :: CallStack ~R# (?callStack::CallStack)) } in\r\n break<0>() undefined @ 'LiftedRep @ (f_a1yV a_a1zd) $dIP_a2Bz; } in\r\n break<1>() undefined @ 'LiftedRep @ w_a1yN $dIP_a2BD; } in\r\n top_a1yW)\r\n @ Any @ Any @ w_a2BZ\r\nend Rec }\r\n\r\n*** End of Offense ***\r\n\r\n\r\n<no location info>: error:\r\nCompilation had errors\r\n\r\n\r\n*** Exception: ExitFailure 1\r\n>\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11641Allow wildcards for parameters functionally determined (also type synonyms)2022-09-06T11:41:35ZIcelandjackAllow wildcards for parameters functionally determined (also type synonyms)```hs
class F a b | a -> b where
foo :: a
-- ...
myFoo :: F a b => a
myFoo = foo
```
Since *b* is not used and fully determined by *a* could the restriction on wildcards in constraints be lifted?
```hs
myFoo :: F a _ => a
myFoo = ...```hs
class F a b | a -> b where
foo :: a
-- ...
myFoo :: F a b => a
myFoo = foo
```
Since *b* is not used and fully determined by *a* could the restriction on wildcards in constraints be lifted?
```hs
myFoo :: F a _ => a
myFoo = foo
```
and eventually hiding it behind a type synonym:
```hs
type F' a = F a _
myFoo' :: F' a => a
myFoo' = foo
```
I raised this issue at ICFP 2014, I haven't looked into whether dominique's response to [my comment](https://haskell-phabricator.global.ssl.fastly.net/D168#4818) applies.
----
I could achieve similar things with a type family but not quite.
----
Or CPP :)https://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/14040Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]2022-03-22T09:23:50ZRyan ScottTyped holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2](Originally spun off from #13877.)
The following program gives a somewhat decent error message in GHC 8.0.1:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-...(Originally spun off from #13877.)
The following program gives a somewhat decent error message in GHC 8.0.1:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data family Sing (a :: k)
data WeirdList :: Type -> Type where
WeirdNil :: WeirdList a
WeirdCons :: a -> WeirdList (WeirdList a) -> WeirdList a
data instance Sing (z :: WeirdList a) where
SWeirdNil :: Sing WeirdNil
SWeirdCons :: Sing w -> Sing wws -> Sing (WeirdCons w wws)
elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
(p :: forall (x :: Type). x -> WeirdList x -> Type).
Sing wl
-> (forall (y :: Type). p _ WeirdNil)
-> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs
-> p _ (WeirdCons x xs))
-> p _ wl
elimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil
elimWeirdList (SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil pWeirdCons
= pWeirdCons @z @x @xs x xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
```
```
$ /opt/ghc/8.0.1/bin/ghci Foo.hs
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:34:8: error:
• Cannot apply expression of type ‘Sing wl
-> (forall y. p x0 t3 'WeirdNil)
-> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
-> Sing xs
-> p (WeirdList z) t2 xs
-> p z t1 ('WeirdCons x xs))
-> p a t0 wl’
to a visible type argument ‘WeirdList z’
• In the sixth argument of ‘pWeirdCons’, namely
‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
In the expression:
pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
In an equation for ‘elimWeirdList’:
elimWeirdList
(SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil
pWeirdCons
= pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
```
But in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:
```
$ /opt/ghc/8.0.2/bin/ghci Foo.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘t0’
Where: ‘t0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x -> WeirdList x -> Type).
Sing wl
-> (forall (y :: Type). p _ WeirdNil)
-> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
-> p _ wl
• Relevant bindings include
elimWeirdList :: Sing wl
-> (forall y. p x0 t0 'WeirdNil)
-> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
-> Sing xs -> p (WeirdList z) t1 xs -> p z t2 ('WeirdCons x xs))
-> p a t3 wl
(bound at Foo.hs:29:1)
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.0.2 for x86_64-unknown-linux):
No skolem info: z_a13X[sk]
```
```
$ /opt/ghc/8.2.1/bin/ghci Foo.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:21:18: error:
• The kind of variable ‘wl1’, namely ‘WeirdList a1’,
depends on variable ‘a1’ from an inner scope
Perhaps bind ‘wl1’ sometime after binding ‘a1’
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x -> WeirdList x -> Type).
Sing wl
-> (forall (y :: Type). p _ WeirdNil)
-> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
-> p _ wl
|
21 | elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘w0’
Where: ‘w0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x -> WeirdList x -> Type).
Sing wl
-> (forall (y :: Type). p _ WeirdNil)
-> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
-> p _ wl
|
24 | -> (forall (y :: Type). p _ WeirdNil)
| ^
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.2.1 for x86_64-unknown-linux):
No skolem info:
z_a1sY[sk:2]
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors
```
(The error messages from HEAD, at commit 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | #13877 |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[13877],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":["PartialTypeSignatures","TypeFamilies,","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"(Originally spun off from #13877.)\r\n\r\nThe following program gives a somewhat decent error message in GHC 8.0.1:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata WeirdList :: Type -> Type where\r\n WeirdNil :: WeirdList a\r\n WeirdCons :: a -> WeirdList (WeirdList a) -> WeirdList a\r\n\r\ndata instance Sing (z :: WeirdList a) where\r\n SWeirdNil :: Sing WeirdNil\r\n SWeirdCons :: Sing w -> Sing wws -> Sing (WeirdCons w wws)\r\n\r\nelimWeirdList :: forall (a :: Type) (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x -> WeirdList x -> Type).\r\n Sing wl\r\n -> (forall (y :: Type). p _ WeirdNil)\r\n -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x -> Sing xs -> p _ xs\r\n -> p _ (WeirdCons x xs))\r\n -> p _ wl\r\nelimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil\r\nelimWeirdList (SWeirdCons (x :: Sing (x :: z))\r\n (xs :: Sing (xs :: WeirdList (WeirdList z))))\r\n pWeirdNil pWeirdCons\r\n = pWeirdCons @z @x @xs x xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.0.1/bin/ghci Foo.hs \r\nGHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:34:8: error:\r\n • Cannot apply expression of type ‘Sing wl\r\n -> (forall y. p x0 t3 'WeirdNil)\r\n -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x\r\n -> Sing xs\r\n -> p (WeirdList z) t2 xs\r\n -> p z t1 ('WeirdCons x xs))\r\n -> p a t0 wl’\r\n to a visible type argument ‘WeirdList z’\r\n • In the sixth argument of ‘pWeirdCons’, namely\r\n ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’\r\n In the expression:\r\n pWeirdCons\r\n @z\r\n @x\r\n @xs\r\n x\r\n xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n In an equation for ‘elimWeirdList’:\r\n elimWeirdList\r\n (SWeirdCons (x :: Sing (x :: z))\r\n (xs :: Sing (xs :: WeirdList (WeirdList z))))\r\n pWeirdNil\r\n pWeirdCons\r\n = pWeirdCons\r\n @z\r\n @x\r\n @xs\r\n x\r\n xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n}}}\r\n\r\nBut in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghci Foo.hs \r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:24:41: error:\r\n • Found type wildcard ‘_’ standing for ‘t0’\r\n Where: ‘t0’ is an ambiguous type variable\r\n ‘x0’ is an ambiguous type variable\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x -> WeirdList x -> Type).\r\n Sing wl\r\n -> (forall (y :: Type). p _ WeirdNil)\r\n -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))\r\n -> p _ wl\r\n • Relevant bindings include\r\n elimWeirdList :: Sing wl\r\n -> (forall y. p x0 t0 'WeirdNil)\r\n -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x\r\n -> Sing xs -> p (WeirdList z) t1 xs -> p z t2 ('WeirdCons x xs))\r\n -> p a t3 wl\r\n (bound at Foo.hs:29:1)\r\n\r\nFoo.hs:26:44: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.2 for x86_64-unknown-linux):\r\n\tNo skolem info: z_a13X[sk]\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Foo.hs \r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:21:18: error:\r\n • The kind of variable ‘wl1’, namely ‘WeirdList a1’,\r\n depends on variable ‘a1’ from an inner scope\r\n Perhaps bind ‘wl1’ sometime after binding ‘a1’\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x -> WeirdList x -> Type).\r\n Sing wl\r\n -> (forall (y :: Type). p _ WeirdNil)\r\n -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))\r\n -> p _ wl\r\n |\r\n21 | elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\nFoo.hs:24:41: error:\r\n • Found type wildcard ‘_’ standing for ‘w0’\r\n Where: ‘w0’ is an ambiguous type variable\r\n ‘x0’ is an ambiguous type variable\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x -> WeirdList x -> Type).\r\n Sing wl\r\n -> (forall (y :: Type). p _ WeirdNil)\r\n -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))\r\n -> p _ wl\r\n |\r\n24 | -> (forall (y :: Type). p _ WeirdNil)\r\n | ^\r\n\r\nFoo.hs:26:44: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.2.1 for x86_64-unknown-linux):\r\n\tNo skolem info:\r\n z_a1sY[sk:2]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable\r\n callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors\r\n}}}\r\n\r\n(The error messages from HEAD, at commit 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)","type_of_failure":"OtherFailure","blocking":[]} -->Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://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/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/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/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/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).