GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2024-01-30T16:46:12Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/24030Relax restrictions on required foralls2024-01-30T16:46:12ZKrzysztof GogolewskiRelax restrictions on required forallsWe now support `RequiredTypeArguments`, `forall a -> ty`.
The arrow `forall a -> ty` was created as a modification of `forall a. ty`. However, it has a lot of common with other types such as the normal function arrow, `a -> ty`. Require...We now support `RequiredTypeArguments`, `forall a -> ty`.
The arrow `forall a -> ty` was created as a modification of `forall a. ty`. However, it has a lot of common with other types such as the normal function arrow, `a -> ty`. Required foralls don't have implicit instantiation or generalization, a lot of complexity around implicit arguments disappears.
I think that `forall a -> ty` should be treated as a tau-type rather than a sigma-type in GHC.
For example, given
```hs
myId :: forall a -> a -> a
myId = myId
single x = [x]
l = single myId
```
We want `l :: [forall a -> a -> a]`. Currently, typechecking `l` requires `ImpredicativeTypes`. But there should be no need for Quick Look inference. Contrast this with `single id`, where the type argument is implicit: it can be typed either as `forall a. [a -> a]` or `[forall a. a -> a]`.
Likewise, in Template Haskell we currently don't allow quantification, as this variant of T11452 shows:
```hs
{-# LANGUAGE RankNTypes, TemplateHaskell, RequiredTypeArguments, ExplicitNamespaces #-}
module T11452a where
impred :: forall a -> a -> a
impred = $$( [|| (\(type _) x -> x) :: (forall a -> a -> a) ||] )
```
But I think this should just work.
[Added later] One more example that I think should work:
```hs
f :: (forall a -> a) -> ()
f x = undefined x
g :: (forall a -> a) -> ()
g (undefined -> ()) = ()
```
`f` works only when `ImpredicativeTypes` are on; `g` doesn't work even with this flag.https://gitlab.haskell.org/ghc/ghc/-/issues/20188Instances for ImpredicativeTypes2021-08-11T12:01:17ZparsonsmattInstances for ImpredicativeTypesNow that we have [ImpredicativeTypes](https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/impredicative_types.html#impredicative-polymorphism) available in a nice way, it'd be cool if we could use them in type class instances.
## Mo...Now that we have [ImpredicativeTypes](https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/impredicative_types.html#impredicative-polymorphism) available in a nice way, it'd be cool if we could use them in type class instances.
## Motivation
I'm playing with `OverloadedRecordDot` and running into the problem that I can't write a polymorphic virtual method. For example:
```haskell
data User = User { name :: String }
instance HasField "showWithName" User (forall a . Show a => a -> String) where
getField self a =
concat [self.name, " : ", show a]
```
What's actually *worse* is that I can't include *any* type variables, at all, so I can't even write, like,
```haskell
instance HasField "identity" User (forall a. a -> a) where
getField _ a =
a
```
## More simply,
Actually, the problem is that we can't write an instance for an impredicative type, at all.
```haskell
{-# Language ImpredicativeTypes, FlexibleInstances #-}
class C a
instance C (forall a . a -> a)
```
This fails with the error message:
```
src/Impl/TH.hs:30:10-30: error:
• Illegal polymorphic type: forall a. a -> a
• In the instance declaration for ‘C (forall a. a -> a)’
|
30 | instance C (forall a . a -> a)
| ^^^^^^^^^^^^^^^^^^^^^
```
I don't know if this is properly a bug or a feature request - on the one hand, I am asking for new functionality, and on the other hand, I am asking for the intersection of existing functionality to work.Research neededhttps://gitlab.haskell.org/ghc/ghc/-/issues/20818Simplified subsumption hurts ImplicitParams usability2022-05-10T16:20:36ZjchiaSimplified subsumption hurts ImplicitParams usability## Motivation
Under GHC 8.10.7, the following code compiles but under GHC 9.0.1, due to simplified subsumption, it fails to compile. The function `bar` has an error but the function `baz`, the eta-expanded version of `bar`, is fine. The...## Motivation
Under GHC 8.10.7, the following code compiles but under GHC 9.0.1, due to simplified subsumption, it fails to compile. The function `bar` has an error but the function `baz`, the eta-expanded version of `bar`, is fine. The need to do eta-expansion makes ImplicitParams unergonomic to use.
```
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE RankNTypes #-}
module Lib where
foo :: Int -> ((?self :: Int) => Char) -> Char
foo x y = undefined
bar :: Int -> (Char -> Char)
bar x = ((let ?self = x in foo) :: Int -> Char -> Char) x
baz :: Int -> (Char -> Char)
baz x = (let ?self = x in (\u v -> foo u v)) x
```
**ERROR**
```
/home/jchia/gh/ip-bug/src/Lib.hs:10:28: error:
• Couldn't match type ‘(?self::Int) => Char’ with ‘Char’
Expected: Int -> Char -> Char
Actual: Int -> ((?self::Int) => Char) -> Char
• In the expression: foo
In the expression: (let ?self = x in foo) :: Int -> Char -> Char
In the expression:
((let ?self = x in foo) :: Int -> Char -> Char) x
|
10 | bar x = ((let ?self = x in foo) :: Int -> Char -> Char) x
```
## Proposal
Modify GHC or the mechanics of simplified subsumption somehow to allow ImplicitParams to be used the same way is in GHC 8.10.7. However, I am not proposing the actual mechanics to achieve this, which is a matter for discussion.https://gitlab.haskell.org/ghc/ghc/-/issues/9269Type families returning quantified types2021-04-20T11:44:40ZpumpkinType families returning quantified typesIs there a fundamental reason for not being able to use quantification in a type family? I'd very much like to be able to do it, obviously turning on RankNTypes if necessary.
I'm looking for things like this:
```haskell
type family Foo...Is there a fundamental reason for not being able to use quantification in a type family? I'd very much like to be able to do it, obviously turning on RankNTypes if necessary.
I'm looking for things like this:
```haskell
type family Foo (x :: Bool) where
Foo True = forall a. [a]
Foo False = ()
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 7.8.2 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Type families returning quantified types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Is there a fundamental reason for not being able to use quantification in a type family? I'd very much like to be able to do it, obviously turning on RankNTypes if necessary.\r\n\r\nI'm looking for things like this:\r\n\r\n{{{#!haskell\r\ntype family Foo (x :: Bool) where\r\n Foo True = forall a. [a]\r\n Foo False = ()\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/24419GHCi statements to use HsExpansions route2024-02-15T15:43:46ZApoorv IngleGHCi statements to use HsExpansions route## Summary
Currently GHCi statements are typechecked using `tcStmtsAndThen` in `GHC.Tc.Gen.TcGhciStmts`.
`tcStmtsAndThen` internally uses `tcSyntaxOp` to typecheck statements.
We should instead be using `GHC.Tc.Gen.Do.expandDoStmts` ...## Summary
Currently GHCi statements are typechecked using `tcStmtsAndThen` in `GHC.Tc.Gen.TcGhciStmts`.
`tcStmtsAndThen` internally uses `tcSyntaxOp` to typecheck statements.
We should instead be using `GHC.Tc.Gen.Do.expandDoStmts` so that we can start removing the dependency from `tcSyntaxOp`
## Steps to reproduce
ghci script
```haskell
:set -XImpredicativeTypes
type Id = forall a. a -> a
t :: IO Id; t = return id
p :: Id -> (Bool, Int); p f = (f True, f 3)
x <- t
```
fails with the following error message:
```
Couldn't match type ‘a0’ with ‘Id’
Expected: IO a0
Actual: IO Id
Cannot instantiate unification variable ‘a0’
with a type involving polytypes: Id
In a stmt of an interactive GHCi command:
x <- GHC.GHCi.ghciStepIO :: IO a -> IO a t
```
Expected output is that it should assign polymorphic typed value `id` to `x`
## GHC
version: 9.9 (Head)Apoorv IngleApoorv Inglehttps://gitlab.haskell.org/ghc/ghc/-/issues/24406Applicative Do should go via HsExpansion Route2024-03-28T05:02:38ZApoorv IngleApplicative Do should go via HsExpansion Route## Summary
Impredicativity does not play well with `do`-blocks expanding under `ApplicativeDo` Language pragma due to ill-designed `tcSyntaxOp` (c.f. issues documented in [wiki page](https://gitlab.haskell.org/ghc/ghc/-/wikis/Rebindable...## Summary
Impredicativity does not play well with `do`-blocks expanding under `ApplicativeDo` Language pragma due to ill-designed `tcSyntaxOp` (c.f. issues documented in [wiki page](https://gitlab.haskell.org/ghc/ghc/-/wikis/Rebindable-syntax))
## Steps to reproduce
```haskell
-- test.hs
{-# LANGUAGE ImpredicativeTypes, ApplicativeDo #-}
module T where
t :: IO (forall a. a -> a)
t = return id
p :: (forall a. a -> a) -> (Bool, Int)
p f = (f True, f 3)
-- This typechecks (with QL)
foo1 = t >>= \x -> return (p x)
-- But this does *not* type check:
foo2 = do { x <- t ; return (p x) }
```
```
$ ghc test.hs
```
Error:
```
test.hs:14:18: error: [GHC-91028]
• Couldn't match type ‘a0’ with ‘forall a. a -> a’
Expected: IO a0
Actual: IO (forall a. a -> a)
Cannot instantiate unification variable ‘a0’
with a type involving polytypes: forall a. a -> a
• In a stmt of a 'do' block: x <- t
In the expression:
do x <- t
return (p x)
In an equation for ‘foo2’:
foo2
= do x <- t
return (p x)
|
14 | foo2 = do { x <- t ; return (p x) }
| ^
test.hs:14:32: error: [GHC-46956]
• Couldn't match expected type ‘a -> a’ with actual type ‘a0’
because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context:
forall a. a -> a
at test.hs:14:32
• In the first argument of ‘p’, namely ‘x’
In a stmt of a 'do' block: return (p x)
In the expression:
do x <- t
return (p x)
• Relevant bindings include x :: a0 (bound at test.hs:14:13)
|
14 | foo2 = do { x <- t ; return (p x) }
```
## Expected behavior
It should type check and execute as expected
## Environment
* GHC version used: 9.6, 9.9Apoorv IngleApoorv Inglehttps://gitlab.haskell.org/ghc/ghc/-/issues/24405polymorphic instantiation of universally quantified types in type constructor...2024-02-07T12:25:02ZArtin Ghasivandghasivand.artin@gmail.compolymorphic instantiation of universally quantified types in type constructors gets accepted depending on the order of argumentsAssume we have the following definition:
```haskell
{-# LANGUAGE ImpredicativeTypes, GADTSyntax #-}
data T2 a b where
K2 :: a -> T2 a a
-- accepted
h1 :: T2 (forall c. c -> c) b -> (Char, Bool)
h1 (K2 x) = (x 'z', x True)
-- reject...Assume we have the following definition:
```haskell
{-# LANGUAGE ImpredicativeTypes, GADTSyntax #-}
data T2 a b where
K2 :: a -> T2 a a
-- accepted
h1 :: T2 (forall c. c -> c) b -> (Char, Bool)
h1 (K2 x) = (x 'z', x True)
-- rejected
h2 :: T2 b (forall c. c -> c) -> (Char, Bool)
h2 (K2 x) = (x 'z', x True)
```
`h2` gets rejected, while `h1` doesn't; when in fact, both of them should be rejected!
@simonpj @raehttps://gitlab.haskell.org/ghc/ghc/-/issues/23241Incorrect inaccessibility warnings with impredicative types and GADTs2023-04-25T11:01:51ZJaro ReindersIncorrect inaccessibility warnings with impredicative types and GADTsConsider this code:
```haskell
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE GADTs #-}
data AB a where
A :: (x ~ (forall a b. a -> b -> b)) => x -> AB x
B :: (x ~ (forall p. p -> forall q. q -> q)) => x -> AB x
data SomeAB = fo...Consider this code:
```haskell
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE GADTs #-}
data AB a where
A :: (x ~ (forall a b. a -> b -> b)) => x -> AB x
B :: (x ~ (forall p. p -> forall q. q -> q)) => x -> AB x
data SomeAB = forall x. SomeAB (AB x)
showAB :: SomeAB -> String
showAB (SomeAB A{}) = "A"
showAB (SomeAB B{}) = "B"
main = putStrLn (showAB (SomeAB (A @(forall a b. a -> b -> b) (\_ x -> x))))
```
Gives the warnings:
```
S.hs:15:1: warning: [GHC-94210] [-Woverlapping-patterns]
Pattern match has inaccessible right hand side
In an equation for ‘showAB’: showAB (SomeAB A {}) = ...
|
15 | showAB (SomeAB A{}) = "A"
| ^^^^^^^^^^^^^^^^^^^^^^^^^
S.hs:15:16: warning: [GHC-40564] [-Winaccessible-code]
• Inaccessible code in
a pattern with constructor:
A :: forall x. (x ~ (forall a b. a -> b -> b)) => x -> AB x,
in an equation for ‘showAB’
Couldn't match type ‘x’ with ‘forall a b. a -> b -> b’
Cannot equate type variable ‘x’
with a type involving polytypes: forall a b. a -> b -> b
‘x’ is a rigid type variable bound by
a pattern with constructor: SomeAB :: forall x. AB x -> SomeAB,
in an equation for ‘showAB’
at S.hs:15:9-18
• In the pattern: A {}
In the pattern: SomeAB A {}
In an equation for ‘showAB’: showAB (SomeAB A {}) = "A"
|
15 | showAB (SomeAB A{}) = "A"
| ^^^
S.hs:16:1: warning: [GHC-53633] [-Woverlapping-patterns]
Pattern match is redundant
In an equation for ‘showAB’: showAB (SomeAB B {}) = ...
|
16 | showAB (SomeAB B{}) = "B"
| ^^^^^^^^^^^^^^^^^^^^^^^^^
S.hs:16:16: warning: [GHC-40564] [-Winaccessible-code]
• Inaccessible code in
a pattern with constructor:
B :: forall x.
(x ~ (forall p. p -> forall q. q -> q)) =>
x -> AB x,
in an equation for ‘showAB’
Couldn't match type ‘x’ with ‘forall p. p -> forall q. q -> q’
Cannot equate type variable ‘x’
with a type involving polytypes: forall p. p -> forall q. q -> q
‘x’ is a rigid type variable bound by
a pattern with constructor: SomeAB :: forall x. AB x -> SomeAB,
in an equation for ‘showAB’
at S.hs:16:9-18
• In the pattern: B {}
In the pattern: SomeAB B {}
In an equation for ‘showAB’: showAB (SomeAB B {}) = "B"
|
16 | showAB (SomeAB B{}) = "B"
| ^^^
```
But it runs just fine and prints:
```
A
```
## Expected behavior
No warnings.
## Environment
* GHC version used: GHC 9.2.6 and GHC 9.6.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/22796ImpredicativeTypes Type Inference Failure with Misleading Error Message2023-01-24T16:30:13ZNathaniel BurkeImpredicativeTypes Type Inference Failure with Misleading Error Message## Summary
ImpredicativeTypes can sometimes give misleading error messages where it cannot resolve ambiguity.
## Steps to reproduce
```hs
{-# LANGUAGE ImpredicativeTypes #-}
import Data.Kind (Type)
type Exis (f :: (a -> Type)) = for...## Summary
ImpredicativeTypes can sometimes give misleading error messages where it cannot resolve ambiguity.
## Steps to reproduce
```hs
{-# LANGUAGE ImpredicativeTypes #-}
import Data.Kind (Type)
type Exis (f :: (a -> Type)) = forall r. (forall x. f x -> r) -> r
exis :: c p -> Exis c
exis x c = c x
newtype Foo a =
Foo a
tmp :: Exis Foo
tmp = exis (Foo 3)
-- Succeeds
tmp2 :: Exis Foo
tmp2 = (tmp :: (forall x. Foo x -> Exis Foo) -> Exis Foo) exis
-- Fails
tmp2b :: Exis Foo
tmp2b = tmp exis
```
Trying to compile this code will output:
```
error:
* Couldn't match type: forall r1. (forall x1. Foo x1 -> r1) -> r1
with: (forall x1. Foo x1 -> r) -> r
Expected: Foo x -> (forall x1. Foo x1 -> r) -> r
Actual: Foo x -> Exis Foo
* In the first argument of `tmp', namely `exis'
In the expression: tmp exis
In an equation for `tmp2b': tmp2b = tmp exis
* Relevant bindings include
tmp2b :: (forall x. Foo x -> r) -> r
(bound at HaskellHasASkillIssue.hs:24:1)
|
24 | tmp2b = tmp exis
| ^^^^
Failed, no modules loaded.
```
## Expected behavior
Either correctly inferring the type of `r` in `tmp` (and not outputting an error), or giving a better error message. The provided error message seems to imply that the code simply does not typecheck, while it really is a case where GHC cannot resolve the ambiguity.
## Environment
* GHC version used: 9.4.4https://gitlab.haskell.org/ghc/ghc/-/issues/22543A `a` -> `id a` transformation does not preserve "it type-checks"2022-12-06T15:14:49Zsyd@cs-syd.euA `a` -> `id a` transformation does not preserve "it type-checks"## Summary
I am trying to write a ghc plugin for code coverage:
See the plan here: https://github.com/NorfairKing/dekking#source-to-source-transformation
Replacing every expression `a` by `id a` produces code that does not type-check.
...## Summary
I am trying to write a ghc plugin for code coverage:
See the plan here: https://github.com/NorfairKing/dekking#source-to-source-transformation
Replacing every expression `a` by `id a` produces code that does not type-check.
## Steps to reproduce
Examples (using `servant-server-19.2`:
This type-checks:
```
hoistExampleServer :: Server EmptyAPI
hoistExampleServer = hoistServerWithContext (Proxy :: Proxy EmptyAPI) (Proxy :: Proxy '[]) id emptyServer
```
This does not:
```
hoistExampleServer :: Server EmptyAPI
hoistExampleServer = (id hoistServerWithContext) (Proxy :: Proxy EmptyAPI) (Proxy :: Proxy '[]) id emptyServer
```
This is the error (with GHC 9.0.2):
```
src/ServantExample.hs:47:26: error:
• Couldn't match type: forall x. m0 x -> Handler x
with: a0 -> a0
Expected: Proxy EmptyAPI
-> Proxy '[]
-> (a0 -> a0)
-> Tagged m0 EmptyServer
-> Tagged Handler EmptyServer
Actual: Proxy EmptyAPI
-> Proxy '[]
-> (forall x. m0 x -> Handler x)
-> ServerT EmptyAPI m0
-> ServerT EmptyAPI Handler
• In the first argument of ‘id’, namely ‘hoistServerWithContext’
In the expression:
(id hoistServerWithContext)
(Proxy :: Proxy EmptyAPI) (Proxy :: Proxy '[]) id emptyServer
In an equation for ‘hoistExampleServer’:
hoistExampleServer
= (id hoistServerWithContext)
(Proxy :: Proxy EmptyAPI) (Proxy :: Proxy '[]) id emptyServer
|
47 | hoistExampleServer = (id hoistServerWithContext) (Proxy :: Proxy EmptyAPI) (Proxy :: Proxy '[]) id emptyServer
```
This is the error (with GHC 9.2.4):
```
src/ServantExample.hs:47:26: error:
• Couldn't match expected type: forall x. m0 x -> Handler x
with actual type: a0 -> a0
• In the first argument of ‘id’, namely ‘hoistServerWithContext’
In the expression:
(id hoistServerWithContext)
(Proxy :: Proxy EmptyAPI) (Proxy :: Proxy '[]) id emptyServer
In an equation for ‘hoistExampleServer’:
hoistExampleServer
= (id hoistServerWithContext)
(Proxy :: Proxy EmptyAPI) (Proxy :: Proxy '[]) id emptyServer
|
47 | hoistExampleServer = (id hoistServerWithContext) (Proxy :: Proxy EmptyAPI) (Proxy :: Proxy '[]) id emptyServer
| ^^^^^^^^^^^^^^^^^^^^^^
```
Even with `ImpredicateTypes` and `DeepSubsumption`, this does not compile.
## Expected behavior
GHC should accept this (I think).
## Environment
* GHC version used: GHC 9.0.2 and GHC 9.2.4
Optional:
* Operating System: NixOS
* System Architecture: x86_64-linuxhttps://gitlab.haskell.org/ghc/ghc/-/issues/22526Impredicative kinds & type synonyms seemingly don't work together2023-01-26T11:56:59ZLas SafinImpredicative kinds & type synonyms seemingly don't work together## Steps to reproduce
```haskell
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
import Data.Proxy (Proxy)
import Data.Functor.Identity (Identity (Identity))
import Data.Kind (Type)
-- Changing ...## Steps to reproduce
```haskell
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
import Data.Proxy (Proxy)
import Data.Functor.Identity (Identity (Identity))
import Data.Kind (Type)
-- Changing this to a type family doesn't work either (EDIT: see new comment)
type P :: forall a. a -> Type
type P = Proxy
type Good :: Identity (forall a. a -> Type)
type Good = 'Identity @(forall a. a -> Type) Proxy
type Bad :: Identity (forall a. a -> Type)
type Bad = 'Identity @(forall a. a -> Type) P
{-
Example.hs:17:45: error:
• Expected kind ‘forall a. a -> Type’,
but ‘P’ has kind ‘a0 -> Type’
• In the second argument of ‘'Identity’, namely ‘P’
In the type ‘'Identity @(forall a. a -> Type) P’
In the type declaration for ‘Bad’
|
17 | type Bad = 'Identity @(forall a. a -> Type) P
-}
```
## Expected behavior
`Bad` should seemingly also work, but I would be satisfied with a work-around if there is one.
## Environment
* GHC version used: 9.4.2https://gitlab.haskell.org/ghc/ghc/-/issues/22508Floating 'forall x. Dict (cls x)' inwards 'Dict (forall x. cls x)'2022-11-29T15:36:38ZIcelandjackFloating 'forall x. Dict (cls x)' inwards 'Dict (forall x. cls x)'This is more of an inquiry than an issue,
1. Is it sound to float the quantifier in `forall x. Dict (cls x)` into the dict: `Dict (forall x. cls x)`
2. If sound, is it possible to implement this `float` function in GHC?
3. If not possi...This is more of an inquiry than an issue,
1. Is it sound to float the quantifier in `forall x. Dict (cls x)` into the dict: `Dict (forall x. cls x)`
2. If sound, is it possible to implement this `float` function in GHC?
3. If not possible, what modification to the surface language would allow it?
Here is an example program where we are able to define a `Dict (cls a)` for any `a`. Question 1. asks if `float = unsafeCoerce` is correct:
```haskell
{-# Language ConstraintKinds #-}
{-# Language GADTs #-}
{-# Language ImpredicativeTypes #-}
{-# Language InstanceSigs #-}
{-# Language StandaloneKindSignatures #-}
import Data.Kind
import Unsafe.Coerce
type Dict :: Constraint -> Type
data Dict cls where
Dict :: cls => Dict cls
type AlwaysList :: (Type -> Constraint) -> Constraint
class AlwaysList cls where
alwaysList :: Dict (cls [a])
instance AlwaysList Semigroup where
alwaysList :: Dict (Semigroup [a])
alwaysList = Dict
instance AlwaysList Monoid where
alwaysList :: Dict (Monoid [a])
alwaysList = Dict
-- float alwaysList :: AlwaysList cls => Dict (forall x. cls [x])
float :: (forall x. Dict (cls [x])) -> Dict (forall x. cls [x])
float = unsafeCoerce
```https://gitlab.haskell.org/ghc/ghc/-/issues/22063Forall-types should be of a TYPE kind2023-12-04T13:51:21ZmniipForall-types should be of a TYPE kindThis is the main ticket for a bunch of related tickets, relating to the kind of `(forall a. ty)`. Specifically
* #22063 (this ticket)
* #8388
* #15979
* #19573
## Summary
With or without impredicativity, we usually intend a `forall`...This is the main ticket for a bunch of related tickets, relating to the kind of `(forall a. ty)`. Specifically
* #22063 (this ticket)
* #8388
* #15979
* #19573
## Summary
With or without impredicativity, we usually intend a `forall`-quantified type to be inhabited by values, i.e. that `forall a. {- ... -} :: TYPE r` for some `r`. Apparently this is never checked in GHC and we have roughly:
```
Gamma, a |- t :: k
---------------------------
Gamma |- (forall a. t) :: k
```
This implies that all kinds (even closed) are lifted: `forall a. a :: k`. Of course in presence of TypeFamilies+UndecidableInstances all kinds are already lifted, but this seems somehow worse.
Furthermore such a type can be used to trigger a core lint error, the wording of which ("Non-*-like kind when *-like expected") suggests that at least on some level it is expected that `forall a. ... :: *`. Applying a type constructor (other than `->`) to a type like `forall a. a` requires ImpredicativeTypes, but (and this might be an unrelated issue) apparently the type can appear on the left side of an application even without ImpredicativeTypes.
## Steps to reproduce
GHCi says:
```hs
> :kind forall a. a
forall a. a :: k
```
The following are accepted by GHC 9.2.3, 8.6.5 and HEAD:
```hs
{-# LANGUAGE RankNTypes, DataKinds, KindSignatures #-}
module M where
type F = (forall (f :: * -> *). f) ()
f :: F
f = f
```
```hs
{-# LANGUAGE RankNTypes, DataKinds, KindSignatures, ImpredicativeTypes #-}
module M where
type B = forall (a :: Bool). a
b :: proxy B
b = b
```
but with `-dcore-lint` they explode:
```hs
*** Core Lint errors : in result of Desugar (before optimization) ***
a.hs:5:1: warning:
Non-Type-like kind when Type-like expected: * -> *
when checking the body of forall: f_agw
In the type of a binder: f
In the type ‘F’
Substitution: [TCvSubst
In scope: InScope {f_agw}
Type env: [agw :-> f_agw]
Co env: []]
*** Offending Program ***
Rec {
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "M"#)
f :: F
[LclIdX]
f = f
end Rec }
*** End of Offense ***
```
```hs
*** Core Lint errors : in result of Desugar (before optimization) ***
b.hs:5:1: warning:
Non-Type-like kind when Type-like expected: Bool
when checking the body of forall: a_auh
In the type of a binder: b
In the type ‘forall (proxy :: Bool -> *). proxy B’
Substitution: [TCvSubst
In scope: InScope {a_auh proxy_aui}
Type env: [auh :-> a_auh, aui :-> proxy_aui]
Co env: []]
*** Offending Program ***
Rec {
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "M"#)
b :: forall (proxy :: Bool -> *). proxy B
[LclIdX]
b = \ (@(proxy_awC :: Bool -> *)) -> b @proxy_awC
end Rec }
*** End of Offense ***
```
GHC 8.4.4 will fail the first program with an impredicativity error, but will still accept it with ImpredicativeTypes enabled, and will still crash with a core lint.
## Expected behavior
`forall a. e` should constrain `e :: TYPE r`, meaning GHCi should report `forall a. a :: *` or `forall a. a :: TYPE r`. Both programs should be rejected with a type error for the above reason. The first program (or programs like it) should raise an "Illegal impredicative type".
## Environment
* GHC version used: 8.4.4, 8.6.5, 9.2.3, HEAD
Optional:
* Operating System: GNU/Linux
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc/-/issues/21925Weird behaviour when passing polytypes to type families2022-10-31T15:05:46ZLas SafinWeird behaviour when passing polytypes to type families## Summary
In the type of a definition, passing polytypes to type families
seems to lead to all sorts of weird behaviour.
## Steps to reproduce
```haskell
import Data.Proxy (Proxy)
import Data.Kind (Type)
type family F (b :: Bool) (t...## Summary
In the type of a definition, passing polytypes to type families
seems to lead to all sorts of weird behaviour.
## Steps to reproduce
```haskell
import Data.Proxy (Proxy)
import Data.Kind (Type)
type family F (b :: Bool) (t1 :: Type) (t2 :: Type) :: Type where
F 'True t1 t2 = t1
F 'False t1 t2 = t2
-- almost works, but gives error when using:
-- f :: forall (a :: Type) (b :: Bool). Proxy a -> Proxy b -> F b (forall (x :: ()). ()) ()
-- f :: forall (a :: Type) (b :: Bool). Proxy a -> Proxy b -> F 'True (forall (x :: a). ()) ()
-- gives nonsense error when checking ambiguity:
f :: forall (a :: Type) (b :: Bool). Proxy a -> Proxy b -> F b (forall (x :: a). ()) ()
f = undefined
```
The error:
```
Test.hs:11:6: error:
• Couldn't match type: F b (forall (x :: a). ()) ()
with: F b (forall (x :: a). ()) ()
Expected: Proxy @{Type} a
-> Proxy @{Bool} b -> F b (forall (x :: a). ()) ()
Actual: Proxy @{Type} a
-> Proxy @{Bool} b -> F b (forall (x :: a). ()) ()
NB: ‘F’ is a non-injective type family
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
f :: forall (a :: Type) (b :: Bool). Proxy a
-> Proxy b -> F b (forall (x :: a). ()) ()
|
11 | f :: forall (a :: Type) (b :: Bool). Proxy a -> Proxy b -> F b (forall (x :: a). ()) ()
```
With `-XAllowAmbiguousTypes`:
```
Test.hs:11:6: error:
• Couldn't match type: F b (forall (x :: a). ()) ()
with: F b (forall (x :: a). ()) ()
Expected: Proxy @{Type} a
-> Proxy @{Bool} b -> F b (forall (x :: a). ()) ()
Actual: Proxy @{Type} a
-> Proxy @{Bool} b -> F b (forall (x :: a). ()) ()
NB: ‘F’ is a non-injective type family
• In the ambiguity check for ‘f’
In the type signature:
f :: forall (a :: Type) (b :: Bool). Proxy a
-> Proxy b -> F b (forall (x :: a). ()) ()
|
11 | f :: forall (a :: Type) (b :: Bool). Proxy a -> Proxy b -> F b (forall (x :: a). ()) ()
```
In the case where it *looks* like it should work, notably
```haskell
f :: forall (a :: Type) (b :: Bool). Proxy a -> Proxy b -> F 'True (forall (x :: a). ()) ()
```
We get the following behaviour:
```
>>> :t f
f :: forall a (b :: Bool).
Proxy @{Type} a
-> Proxy @{Bool} b -> F 'True (forall (x :: a). ()) ()
>>> :t f (Proxy @Int)
f (Proxy @Int)
:: forall {b :: Bool}. Proxy @{Bool} b -> forall (x :: Int). ()
>>> :t f (Proxy @Int) (Proxy @'True)
f (Proxy @Int) (Proxy @'True) :: forall (x :: Int). ()
>>> f (Proxy @Int) (Proxy @'True)
<interactive>:45:1: error:
• Couldn't match type ‘forall (x1 :: Int). ()’ with ‘()’
Expected: ()
Actual: F 'True (forall (x :: Int). ()) ()
• When checking that the inferred type
it :: F 'True (forall (x :: Int). ()) ()
is as general as its inferred signature
it :: forall (x :: Int). ()
```
## Expected behavior
Either they should work, or give a useful error message.
Optimally they would work, since I'm trying to work around returning polytypes
from type families.
## Environment
* GHC version used: 9.2.3https://gitlab.haskell.org/ghc/ghc/-/issues/21425Something related to ImpredicativeTypes breaks due to "involving polytypes" p...2022-12-01T16:53:48ZMikolaj KonarskiSomething related to ImpredicativeTypes breaks due to "involving polytypes" preventing GHC.Exts.inline application from type-checkingThe below fails, but very similar examples, e.g., without the `r`, succeed. This is rather important, because it breaks `GHC.Exts.inline f` for functions `f` like that in my (almost) real life code.
```
GHCi, version 9.3.20220316: https...The below fails, but very similar examples, e.g., without the `r`, succeed. This is rather important, because it breaks `GHC.Exts.inline f` for functions `f` like that in my (almost) real life code.
```
GHCi, version 9.3.20220316: https://www.haskell.org/ghc/ :? for help
ghci> :set -XImpredicativeTypes
ghci> f :: forall r. (forall a. Either a r -> Either a r) -> (); f _ = ()
ghci> id f
<interactive>:3:4: error:
• Couldn't match expected type ‘a’
with actual type ‘(forall a. Either a r0 -> Either a r0) -> ()’
• Cannot equate type variable ‘a’
with a type involving polytypes:
(forall a1. Either a1 r0 -> Either a1 r0) -> ()
‘a’ is a rigid type variable bound by
the inferred type of it :: a
at <interactive>:3:1-4
• In the first argument of ‘id’, namely ‘f’
In the expression: id f
In an equation for ‘it’: it = id f
• Relevant bindings include it :: a (bound at <interactive>:3:1)
ghci> (\x -> id x) (\x -> f x)
<interactive>:4:23: error:
• Couldn't match expected type ‘Either a r0 -> Either a r0’
with actual type ‘p’
‘p’ is a rigid type variable bound by
the inferred type of it :: p -> ()
at <interactive>:4:1-24
• In the first argument of ‘f’, namely ‘x’
In the expression: f x
In the first argument of ‘\ x -> id x’, namely ‘(\ x -> f x)’
• Relevant bindings include
x :: p (bound at <interactive>:4:16)
it :: p -> () (bound at <interactive>:4:1)
```https://gitlab.haskell.org/ghc/ghc/-/issues/20805Take a Quick Look at lists2021-12-22T14:05:05ZRichard Eisenbergrae@richarde.devTake a Quick Look at listsI want to make a video about Quick Look. But I also want it to have more content than just the venerable `head ids`. So I thought a bit about what would make a nice use case for impredicative polymorphism. I came up with the idea of usin...I want to make a video about Quick Look. But I also want it to have more content than just the venerable `head ids`. So I thought a bit about what would make a nice use case for impredicative polymorphism. I came up with the idea of using `forall a. Tree a -> Maybe a` as the type of indices into a tree structure. I could now search in one tree for a value that satisfies a predicate returning a `forall a. Tree a -> Maybe a` to then retrieve a corresponding value (if the tree has the right shape) in another tree. Here is the code:
```hs
data Tree a
= Leaf a
| Node (Tree a) a (Tree a)
deriving (Show, Functor)
type TreeIndex = forall a. Tree a -> Maybe a
lookupTree :: forall a. (a -> Bool) -> Tree a -> Maybe TreeIndex
lookupTree p = go
where
go :: Tree a -> Maybe TreeIndex
go (Leaf x)
| p x = Just (\case Leaf y -> Just y
Node _ y _ -> Just y)
| otherwise = Nothing
go (Node left x right)
| p x = Just (\case Leaf y -> Just y
Node _ y _ -> Just y)
| otherwise = asum [go left, go right] -- (go left : go right : [])
```
(This doesn't work, as written, because the last line just returns the `TreeIndex` from the recursive call. But never mind this.)
(NB to GHC aficionados: `asum` is the same as GHC's `firstJusts`.)
What's sad is that the last line fails to type-check. However, if I remove the list argument and replace it with the commented-out cons-and-nil argument, all is well. This is because GHC doesn't take a Quick Look at lists. But it really should. And probably tuples, too.https://gitlab.haskell.org/ghc/ghc/-/issues/20318GHC complains about impredicativity in type synonym for a quantified constraint2021-09-07T14:37:54ZRichard Eisenbergrae@richarde.devGHC complains about impredicativity in type synonym for a quantified constraintIf I say
```hs
{-# LANGUAGE ConstraintKinds, QuantifiedConstraints #-}
module Bug where
type T b = (Ord b, forall a. Eq a)
```
then GHC HEAD says
```
Bug.hs:5:1: error:
• Illegal polymorphic type: forall a. Eq a
Perhaps yo...If I say
```hs
{-# LANGUAGE ConstraintKinds, QuantifiedConstraints #-}
module Bug where
type T b = (Ord b, forall a. Eq a)
```
then GHC HEAD says
```
Bug.hs:5:1: error:
• Illegal polymorphic type: forall a. Eq a
Perhaps you intended to use ImpredicativeTypes
• In the type synonym declaration for ‘T’
|
5 | type T b = (Ord b, forall a. Eq a)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Note that `T` defines a *constraint* synonym, not a type synonym. Accordingly, `QuantifiedConstraints` should be enough to accept this definition.
Inspired by https://mail.haskell.org/pipermail/haskell-cafe/2021-August/134388.htmlhttps://gitlab.haskell.org/ghc/ghc/-/issues/20169Hidden rigid type variable in GHCi2023-09-19T14:35:41ZJaro ReindersHidden rigid type variable in GHCi## Summary
I'm getting an error in GHCi which mentions a rigid type variable that I didn't define myself. I thought rigid type variables were always user-defined, is that not true? Does GHCi insert rigid type variables without my knowle...## Summary
I'm getting an error in GHCi which mentions a rigid type variable that I didn't define myself. I thought rigid type variables were always user-defined, is that not true? Does GHCi insert rigid type variables without my knowledge?
## Steps to reproduce
```
ghci> :set -XRankNTypes
ghci> data Jet a
ghci> :{
ghci| run :: forall a. Jet a -> forall s. (s -> Bool) -> (s -> a -> IO s) -> s -> IO s
ghci| run x = undefined x
ghci| :}
ghci> :t map run
<interactive>:1:5: error:
• Couldn't match type ‘b’
with ‘forall s. (s -> Bool) -> (s -> a -> IO s) -> s -> IO s’
Expected: Jet a -> b
Actual: Jet a
-> forall s. (s -> Bool) -> (s -> a -> IO s) -> s -> IO s
‘b’ is a rigid type variable bound by
the inferred type of it :: [Jet a] -> [b]
at <interactive>:1:1
• In the first argument of ‘map’, namely ‘run’
In the expression: map run
```
## Expected behavior
I expected an error like "Cannot instantiate unification variable ‘b’ with a type involving polytypes".
## Environment
* GHC version used: 9.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/18762Validity checker should reject polytypes passed to type functions2022-07-27T16:19:21ZRichard Eisenbergrae@richarde.devValidity checker should reject polytypes passed to type functions@RyanGlScott points out in https://gitlab.haskell.org/ghc/ghc/-/issues/11715#note_303067 that we can now say
```hs
λ> :set -XTypeFamilies -XImpredicativeTypes -XFlexibleContexts
λ> type family F a where F (a -> b) = a -> b
λ> :kind! F (...@RyanGlScott points out in https://gitlab.haskell.org/ghc/ghc/-/issues/11715#note_303067 that we can now say
```hs
λ> :set -XTypeFamilies -XImpredicativeTypes -XFlexibleContexts
λ> type family F a where F (a -> b) = a -> b
λ> :kind! F (Eq Int => Int)
F (Eq Int => Int) :: *
= Eq Int -> Int
```
Ew. While indeed this does show a problem around confusing `Constraint` and `Type`, there is a simpler problem here: type families are designed to work only with plain old "tau" types. These types have no dependency or invisible arguments.
<details>
<summary>Why type families work over tau-types only</summary>
The restriction around tau-types is necessary to guide type inference. Suppose we have
```hs
type family Id a where
Id a = a
f :: Id (forall a. a -> a) -> Char
f x = x 'z'
```
When GHC checks the definition of `f`, it knows is that the type of `x` is `Id (forall a. a -> a)`. The type checker has not yet tried to reduce type families. (Even if it did, which is plausible, more complicated scenarios would still exist -- such as a type family being stuck on a variable that we learn only through a GADT pattern-match equals some concrete type -- that witness the fundamental problem.) The type checker sees `x` applied to an argument of type `Char` and returning a result of type `Char`, so it concludes that `Id (forall a. a -> a) ~ (Char -> Char)`. Later, GHC reduces `Id (forall a. a -> a)` to `forall a. a -> a`. Yet we're now stuck, because it is not the case that `(forall a. a -> a) ~ (Char -> Char)`. The former is a subtype of the latter, but that's different (and GHC does not yet track subtype relationships in its constraint-solving).
Bottom line: type families mustn't return something that isn't a tau-type, or strange things like this can ensue.
Note that there is *no* type safety issue here. It's all about type inference.
</details>
So we should stop this nonsense in the validity checker.
But, actually, that's probably not enough, because an innocent-looking `F a` could get instantiated to `F (forall b. b -> b)` at some call-site, due to Quick Look. Maybe any variable used in the argument to a type function should be excluded from Quick Look. @trupill @simonpj will want to think about that.https://gitlab.haskell.org/ghc/ghc/-/issues/18759Types with different forall placements don't unify with QL ImpredicativeTypes2022-06-30T00:52:03ZAndrzej RybczakTypes with different forall placements don't unify with QL ImpredicativeTypesThe following program:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE KindSignatures...The following program:
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}
import GHC.TypeLits
main :: IO ()
main = pure ()
data X = X { x :: forall a. a -> a }
class HasField (name :: Symbol) s a | name s -> a where
getField :: s -> a
instance a ~ (forall x. x -> x) => HasField "x" X a where
getField = x
getX_Ok_sel :: X -> forall a. a -> a
getX_Ok_sel = x
getX_Bad_sel :: forall a. X -> a -> a
getX_Bad_sel = x
getX_Ok_class :: X -> forall a. a -> a
getX_Ok_class = getField @"x"
getX_Bad_class :: forall a. X -> a -> a
getX_Bad_class = getField @"x"
getX_Bad_classUsage :: String
getX_Bad_classUsage = getField @"x" (X id) "hello world"
```
produces errors with GHC 9.1.0.20200927:
```
unknown@electronics _build $ ./ghc-stage1 it.hs
[1 of 1] Compiling Main ( it.hs, it.o )
it.hs:29:16: error:
• Couldn't match type: forall a1. a1 -> a1
with: a -> a
Expected: X -> a -> a
Actual: X -> forall a. a -> a
• In the expression: x
In an equation for ‘getX_Bad_sel’: getX_Bad_sel = x
• Relevant bindings include
getX_Bad_sel :: X -> a -> a (bound at it.hs:29:1)
|
29 | getX_Bad_sel = x
| ^
it.hs:35:18: error:
• Couldn't match type: a -> a
with: forall x. x -> x
arising from a use of ‘getField’
• In the expression: getField @"x"
In an equation for ‘getX_Bad_class’: getX_Bad_class = getField @"x"
• Relevant bindings include
getX_Bad_class :: X -> a -> a (bound at it.hs:35:1)
|
35 | getX_Bad_class = getField @"x"
| ^^^^^^^^
it.hs:38:23: error:
• Couldn't match type: String -> String
with: forall x. x -> x
arising from a use of ‘getField’
• In the expression: getField @"x" (X id) "hello world"
In an equation for ‘getX_Bad_classUsage’:
getX_Bad_classUsage = getField @"x" (X id) "hello world"
|
38 | getX_Bad_classUsage = getField @"x" (X id) "hello world"
```
The `Bad_sel` and `Bad_class` issues look very similar, but produce error messages with flipped actual and expected types, which confuses me a bit.
`Bad_classUsage` looks like a consequence of `Bad_class` not working.