GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2024-03-26T15:29:03Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/24572RequiredTypeArguments: application of infix type fails when combined with Tem...2024-03-26T15:29:03ZRyan ScottRequiredTypeArguments: application of infix type fails when combined with TemplateHaskellI am using the `master` branch of GHC on commit da2a10ceab7498fbbd5723dee0393ce75f2bb562. That includes a fix for https://gitlab.haskell.org/ghc/ghc/-/issues/24570, so this program now typechecks:
```hs
{-# LANGUAGE GHC2024 #-}
{-# LANG...I am using the `master` branch of GHC on commit da2a10ceab7498fbbd5723dee0393ce75f2bb562. That includes a fix for https://gitlab.haskell.org/ghc/ghc/-/issues/24570, so this program now typechecks:
```hs
{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE RequiredTypeArguments #-}
{-# LANGUAGE TemplateHaskell #-}
module Foo where
import Language.Haskell.TH
idee :: forall a -> a -> a
idee _ x = x
type (!@#) = Bool
f :: Bool -> Bool
f = idee (!@#)
```
Surprisingly, however, this variation of `f` does not typecheck:
```hs
g :: Bool -> Bool
g = $([| idee (!@#) |])
```
```
~/Software/ghc/_build/stage1/bin/ghc Foo.hs
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
Foo.hs:17:6: error: [GHC-55017]
• Illegal data constructor name: ‘!@#’
When splicing a TH expression: Foo.idee (Foo.!@#)
• In the untyped splice: $([| idee (!@#) |])
|
17 | g = $([| idee (!@#) |])
| ^^^^^^^^^^^^^^^^^^
```
Why is GHC complaining about a data constructor name when `(!@#)` is a type name? If you compile this program with `-ddump-simpl`, you'll see:
```
$ ~/Software/ghc/_build/stage1/bin/ghc Foo.hs -ddump-simpl
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
==================== Simplified expression ====================
Language.Haskell.TH.Lib.Internal.appE
@Language.Haskell.TH.Syntax.Q
Language.Haskell.TH.Syntax.$fQuoteQ
(Language.Haskell.TH.Lib.Internal.varE
@Language.Haskell.TH.Syntax.Q
Language.Haskell.TH.Syntax.$fQuoteQ
(Language.Haskell.TH.Syntax.mkNameG_v
(GHC.CString.unpackCString# "main"#)
(GHC.CString.unpackCString# "Foo"#)
(GHC.CString.unpackCString# "idee"#)))
(Language.Haskell.TH.Lib.Internal.conE
@Language.Haskell.TH.Syntax.Q
Language.Haskell.TH.Syntax.$fQuoteQ
(Language.Haskell.TH.Syntax.mkNameG_tc
(GHC.CString.unpackCString# "main"#)
(GHC.CString.unpackCString# "Foo"#)
(GHC.CString.unpackCString# "!@#"#)))
```
Which reveals that GHC is desugaring `g` to something like this:
```hs
g :: Bool -> Bool
g = $(varE 'idee `appE` conE ''(!@#))
```
I believe `conE` is the culprit here. If you look into how `conE` is desugared, you'll find that it calls [`cName`](https://gitlab.haskell.org/ghc/ghc/-/blob/da2a10ceab7498fbbd5723dee0393ce75f2bb562/compiler/GHC/ThToHs.hs#L2101):
```hs
cName n = cvtName OccName.dataName n
```
Where [`cvtName`](https://gitlab.haskell.org/ghc/ghc/-/blob/da2a10ceab7498fbbd5723dee0393ce75f2bb562/compiler/GHC/ThToHs.hs#L2127-2136) is defined as:
```hs
cvtName :: OccName.NameSpace -> TH.Name -> CvtM RdrName
cvtName ctxt_ns (TH.Name occ flavour)
| not (okOcc ctxt_ns occ_str) = failWith (IllegalOccName ctxt_ns occ_str)
| otherwise
= do { loc <- getL
; let rdr_name = thRdrName loc ctxt_ns occ_str flavour
; force rdr_name
; return rdr_name }
where
occ_str = TH.occString occ
```
Note the `not (okOcc ctxt_ns occ_str)` check. When calling `cName`, `ctxt_ns` is `dataName`, so this check will only succeed if the supplied `Name` is a valid data constructor. `''(!@#)` isn't a valid data constructor `Name`, so it fails this check.
-----
Two possible ways of fixing this include:
1. Relaxing this check. (I'm not sure what the consequences of this would be.)
2. Change the way `RequiredTypeArguments` applications are desugared so that `[| idee (!@#) |]` is desugared to ``varE 'idee `appE` typeE (conT ''(!@#))`` instead. This would have the downside that `[| idee (!@#) |]` would be indistinguishable from `[| idee (type (!@#$)) |]` after desugaring, however.https://gitlab.haskell.org/ghc/ghc/-/issues/24570RequiredTypeArguments: unexpected parse error for infix type2024-03-26T15:32:05ZRyan ScottRequiredTypeArguments: unexpected parse error for infix typeI am using GHC 9.10.1-alpha1, which introduces the `RequiredTypeArguments` extension. My understanding is that a visible `forall` can be instantiated with a type (without needing a `type` disambiguator) when the name of the type is unamb...I am using GHC 9.10.1-alpha1, which introduces the `RequiredTypeArguments` extension. My understanding is that a visible `forall` can be instantiated with a type (without needing a `type` disambiguator) when the name of the type is unambiguously in the type syntax. For example, the following works as I would expect, since `(:!@#)` is unambiguously in the type syntax:
```hs
{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE RequiredTypeArguments #-}
module Foo where
import Language.Haskell.TH
idee :: forall a -> a -> a
idee _ x = x
type (:!@#) = Bool
f :: Bool -> Bool
f = idee (:!@#) -- Relies on RequiredTypeArguments to work
```
So far, so good. Now consider what happens if we change the name of the type slightly:
```hs
-- No longer starts with a colon
type (!@#) = Bool
f :: Bool -> Bool
f = idee (!@#)
```
The name has changed to `(!@#)`, but it's still unambiguously in the type syntax. Despite this, GHC no longer accepts the program!
```
$ ghc-9.10 Foo.hs
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
Foo.hs:14:5: error: [GHC-76037]
• Not in scope: ‘!@#’
• In the expression: idee (!@#)
In an equation for ‘f’: f = idee (!@#)
|
14 | f = idee (!@#)
| ^^^^^^^^^^
```
This error message is very surprising, as `(!@#)` _is_ in scope. Surely this ought to be accepted? At the very least, I didn't see this limitation of `RequiredTypeArguments` mentioned in the [relevant section of the GHC User's Guide](https://gitlab.haskell.org/ghc/ghc/-/blob/cdfe6e01f113dbed9df6703c97207c02fc60303b/docs/users_guide/exts/required_type_arguments.rst).9.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/24318Error message with RequiredTypeArguments2024-03-07T21:28:44ZKrzysztof GogolewskiError message with RequiredTypeArgumentsProgram:
```haskell
{-# LANGUAGE ExplicitNamespaces, RequiredTypeArguments #-}
module M where
import Data.Kind
f :: forall (a :: Type) -> Bool
f (type t) x = True
```
```
M.hs:5:1: error: [GHC-83865]
• Couldn't match expected type ...Program:
```haskell
{-# LANGUAGE ExplicitNamespaces, RequiredTypeArguments #-}
module M where
import Data.Kind
f :: forall (a :: Type) -> Bool
f (type t) x = True
```
```
M.hs:5:1: error: [GHC-83865]
• Couldn't match expected type ‘Bool’ with actual type ‘p0 -> Bool’
• The equation for ‘f’ has two value arguments,
but its type ‘forall a -> Bool’ has only one
|
5 | f (type t) x = True
| ^^^^^^^^^^^^^^^^^^^
```
The error says that `f` has two value arguments - but `f (type t) x` is one type argument and one value argument. Either it should say that, or "value arguments" should be "visible arguments".9.10.1Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/24313Suggest "Possible fix: turn on -XImpredicativeTypes" for error number 910282024-01-09T16:58:56ZArtin Ghasivandghasivand.artin@gmail.comSuggest "Possible fix: turn on -XImpredicativeTypes" for error number 91028Consider the following example:
```haskell
{-# LANGUAGE RequiredTypeArguments #-}
module VDQ where
sizeOf :: forall a -> Show a => Int
sizeOf = undefined
```
It produces the error:
```plaintext
VDQ.hs:7:10: error: [GHC-91028]
• ...Consider the following example:
```haskell
{-# LANGUAGE RequiredTypeArguments #-}
module VDQ where
sizeOf :: forall a -> Show a => Int
sizeOf = undefined
```
It produces the error:
```plaintext
VDQ.hs:7:10: error: [GHC-91028]
• Couldn't match expected type ‘forall a -> Show a => Int’
with actual type ‘a0’
Cannot instantiate unification variable ‘a0’
with a type involving polytypes: forall a -> Show a => Int
• In the expression: undefined
In an equation for ‘sizeOf’: sizeOf = undefined
|
7 | sizeOf = undefined
| ^^^^^^^^^
```
I think there is room for a lot of improvement. It is easily solvable by turning on Impredicative types.
In my opinion "Turn on ImpredicativeTypes" would be great. Another less good improvement would be to replace "cannot instantiate unification variable with a type involving polytypes" with something else. Because intuitively, if the user is unaware that instantiation variables are just unification variables that GHC keeps track of, in order to avoid implicit instantiation, he would read it and think: "Okay, I know that unification variables stand for monotypes, my code must be wrong then".
GHC version: 9.9.20240105https://gitlab.haskell.org/ghc/ghc/-/issues/24231Error message hints: use the env instead of the namespace2023-12-07T17:52:24ZVladislav ZavialovError message hints: use the env instead of the namespaceThis ticket describes a problem related to `RequiredTypeArguments`.
## Background
When a type variable is used at the term level, GHC assumes the user might
have made a typo and suggests a term variable with a similar name.
For exampl...This ticket describes a problem related to `RequiredTypeArguments`.
## Background
When a type variable is used at the term level, GHC assumes the user might
have made a typo and suggests a term variable with a similar name.
For example, if the user writes
```haskell
f (Proxy :: Proxy nap) (Proxy :: Proxy gap) = nap (+1) [1,2,3]
```
then GHC will helpfully suggest `map` instead of `nap`
```
• Illegal term-level use of the type variable ‘nap’
• Perhaps use ‘map’ (imported from Prelude)
```
Importantly, GHC does _not_ suggest `gap`, which is in scope.
* **Question:** How does GHC know not to suggest `gap`? After all, the edit distance between `map`, `nap`, and `gap` is equally short.
* **Answer:** GHC takes the namespace into consideration. `gap` is a `tvName`, and GHC would only suggest a `varName` at the term level.
In other words, the current hint infrastructure assumes that the namespace of an
entity is a reliable indicator of its level
* term-level name <=> term-level entity
* type-level name <=> type-level entity
## Problem
With `RequiredTypeArguments`, the above assumption does not hold. Consider
```
bad :: forall a b -> ...
bad nap gap = nap
```
This use of `nap` on the RHS is illegal because `nap` stands for a type
variable. It cannot be returned as the result of a function. At the same time,
it is bound as a `varName`, i.e. in the term-level namespace.
Unless we suppress hints, GHC gets awfully confused
```
• Illegal term-level use of the variable ‘nap’
• Perhaps use one of these:
‘nap’ (line 2), ‘gap’ (line 2), ‘map’ (imported from Prelude)
```
GHC shouldn't suggest `gap`, which is also a type variable; using it would
result in the same error. And it especially shouldn't suggest using `nap`
instead of `nap`, which is absurd.
## Workaround
A simple workaround is to suppress the hints as long as `RequiredTypeArguments` is enabled.
Naturally, this also means that error messages are less helpful with `RequiredTypeArguments`,
so it's not a proper solution.
## Solution
The proper solution is to overhaul the hint system to consider what a name
stands for instead of looking at its namespace alone. This information is present in the type checking environment.
## Plan
My plan is to go with the workaround in !11682 and implement the proper solution afterwards. This ticket is to track this task.Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/24226Function type mistaken for ViewPatterns in T2T VDQ2023-11-28T14:55:55ZArtin Ghasivandghasivand.artin@gmail.comFunction type mistaken for ViewPatterns in T2T VDQPassing 'function type\` arguments to VDQ functions, without the `type` keyword, causes GHC to get confused, and think it's a view pattern.
Example (`card` is defined in #24225):
```haskell
t1 = card (type (Bool -> Bool)) -- Fine
-- F...Passing 'function type\` arguments to VDQ functions, without the `type` keyword, causes GHC to get confused, and think it's a view pattern.
Example (`card` is defined in #24225):
```haskell
t1 = card (type (Bool -> Bool)) -- Fine
-- Fails and triggers the error message below
t2 = card (Bool -> Bool)
{-
src/VDQ.hs:71:11-22: error: [GHC-66228] …
View pattern in expression context: Bool -> Bool
|
Compilation failed.
-}
```
GHC version: 9.9.20231126Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/24225Wrong error message for type argument with an identifier that occupies both t...2023-11-28T15:45:41ZArtin Ghasivandghasivand.artin@gmail.comWrong error message for type argument with an identifier that occupies both the term and type namespace, without the `type` keywordPassing type arguments without the `type` keyword to VDQ functions results in the wrong error message.
As an example:
```haskell
class Cardinality a where
cardinality :: Maybe Int
instance Cardinality Bool where
cardinality = Just...Passing type arguments without the `type` keyword to VDQ functions results in the wrong error message.
As an example:
```haskell
class Cardinality a where
cardinality :: Maybe Int
instance Cardinality Bool where
cardinality = Just 2
instance Cardinality () where
cardinality = Just 1
instance Cardinality Void where
cardinality = Just 0
instance (Cardinality a, Cardinality b) => Cardinality (a -> b) where
cardinality = (^) <$> (cardinality @b) <*> (cardinality @a)
card :: forall a -> Cardinality a => Maybe Int
card (type x) = cardinality @x
-- These would typecheck
t1 = card Bool
t2 = card (type Bool)
t3 = card (type ())
-- t4 results in a weird error message
t4 = card ()
{-
<interactive>:233:1-4: error: [GHC-39999]
* No instance for `Cardinality '()' arising from a use of `card'
* In the expression: card ()
In an equation for `it': it = card ()
-}
-- We can clearly see that there is an instance for ()
```
Now, strangely, if we create a type synonym for **`()`**, and pass it to `card`, typechecking succeeds.
```haskell
type Unit = ()
t5 = card Unit -- typechecks
```
But now, if we create some type that has `Unit` as a data constructor, we get the same error message:
```haskell
data Foo = Unit | FC
t6 = card Unit -- fails
{-
<interactive>:247:1-4: error: [GHC-39999]
* No instance for `Cardinality 'Unit' arising from a use of `card'
* In the expression: card Unit
In an equation for `it': it = card Unit
-}
```
I think the term-2-type mapping fails when the identifier occupies both the term and type namespace at the same time.
GHC version used: 9.9.20231126https://gitlab.haskell.org/ghc/ghc/-/issues/24176Panic with QuantifiedConstraints + RequiredTypeArguments2023-12-04T16:47:17ZKrzysztof GogolewskiPanic with QuantifiedConstraints + RequiredTypeArgumentsThis code causes a panic in master:
```haskell
{-# LANGUAGE QuantifiedConstraints, RequiredTypeArguments #-}
module T where
f :: (forall a -> Eq a) => a
f = f
```
```
<no location info>: error:
panic! (the 'impossible' happened)
...This code causes a panic in master:
```haskell
{-# LANGUAGE QuantifiedConstraints, RequiredTypeArguments #-}
module T where
f :: (forall a -> Eq a) => a
f = f
```
```
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.9.20231110:
instDFunTypes
df_aIu
[Just a_aIB[sk:2]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:186:37 in ghc-9.9-inplace:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Tc/Utils/Instantiate.hs:371:16 in ghc-9.9-inplace:GHC.Tc.Utils.Instantiate
CallStack (from HasCallStack):
panic, called at compiler/GHC/Utils/Error.hs:511:29 in ghc-9.9-inplace:GHC.Utils.Error
```
I think we should enforce that `forall a -> ...` is always used with `TYPE rep`. For `forall a. ...`, the body can also be a constraint; the situation is more complicated and covered by #22063. Finally, we accept `forall {a}. Eq a` which seems to give the same result as `forall a. Eq a`, presumably we should reject it.Krzysztof GogolewskiKrzysztof Gogolewskihttps://gitlab.haskell.org/ghc/ghc/-/issues/24159The types-in-terms syntax (forall, ->, =>)2023-11-27T11:46:09ZVladislav ZavialovThe types-in-terms syntax (forall, ->, =>)In accordance with GHC Proposal [#281](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst), the syntax of expressions must be extended with several constructs that previously could only occur at ...In accordance with GHC Proposal [#281](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst), the syntax of expressions must be extended with several constructs that previously could only occur at the type level:
* Function arrows: `a -> b`
* Multiplicity-polymorphic function arrows: `a %m -> b` (under `-XLinearTypes`)
* Constraint arrows: `a => b`
* Universal quantification: `forall a. b`
* Visible universal quantification: `forall a -> b`
The purpose of the new syntax is to be used in required type arguments (via T2T). Using it in a free-standing expression is an error.Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/24153Rejects puns in T2T2023-11-27T12:09:54ZVladislav ZavialovRejects puns in T2TConsider this example
```haskell
x = 42
f, g :: forall a -> ...
f (type x) = g x
```
The `g x` function call is renamed as a term, so the `x` refers to the top-level binding `x = 42`, not to the type variable binding `type x`, even tho...Consider this example
```haskell
x = 42
f, g :: forall a -> ...
f (type x) = g x
```
The `g x` function call is renamed as a term, so the `x` refers to the top-level binding `x = 42`, not to the type variable binding `type x`, even though `g` is expecting a type argument. Such behavior is well-defined, and [GHC Proposal #281](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst) goes to great lengths to specify it (see the "Resolved Syntax Tree" section). Nonetheless, users who are not intimately familiar with the compiler pipeline might find it surprising or confusing. We want a dedicated error message for such conflicts. So the proposal also says:
> In the type checking environment, there should be no variable of the same name but from a different namespace, or else raise an ambiguity error (does not apply to constructors).
This ticket is to track the implementation of this side condition.https://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/23739T2T (term-to-type) transformation in patterns2023-12-21T21:18:00ZVladislav ZavialovT2T (term-to-type) transformation in patternsThe T2T transformation introduced in [GHC Proposal #281: Visible forall in types of terms](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst) is defined for expressions (see #23738). However, a ...The T2T transformation introduced in [GHC Proposal #281: Visible forall in types of terms](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst) is defined for expressions (see #23738). However, a similar transformation is needed in patterns:
```haskell
f :: forall x -> ...
f = \x -> ...
```
The lambda-bound `x` looks like a term-level pattern, but it's actually a type pattern checked by `tc_forall_pat` (as opposed to `tc_pat`) in `GHC/Tc/Gen/Pat.hs`. This necessiates a variant of T2T that operates on patterns. Let's call it `p2tp` (pattern-to-type-pattern) to distinguish it from `t2t` in expressions:
```haskell
p2tp :: Pat GhcRn -> TcM (HsTyPat GhcRn)
```9.10.1Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/23717Visible forall in types of terms, Part 22023-12-11T09:44:53ZVladislav ZavialovVisible forall in types of terms, Part 2[GHC Proposal #281: Visible forall in types of terms](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst) is presented in two parts:
1. Part 1 introduces the `forall a ->` quantifier in types of...[GHC Proposal #281: Visible forall in types of terms](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst) is presented in two parts:
1. Part 1 introduces the `forall a ->` quantifier in types of terms but also requires a syntactic marker at use sites.
2. Part 2 specifies when it is permissible to omit the `type` herald.
See also https://gitlab.haskell.org/ghc/ghc/-/wikis/DH-current-status.
The first part was tracked at #22326 and implemented in 33b6850aaaa4b3a4760d4b384cd15611b159045b. This new ticket is to track the implementation of the remaining parts of the proposal, i.e. Part 2. To that end, I identified the following subtasks:
* [x] #23738 T2T (term-to-type) transformation in expressions (at call sites)
* [ ] #24153 Reject puns in T2T
* [x] #23739 T2T (term-to-type) transformation in patterns (at binding sites)
* [ ] #24159 The types-in-terms syntax (`forall`, `->`, `=>`)
* [x] #23719 Make `forall` a keyword
* [x] #23740 Term variable capture and implicit quantification
Here are a few examples of code that we aim to allow:
* A variant of `id` that uses visible `forall`:
```haskell
-- Definition:
idv :: forall a -> a -> a
idv a x = x :: a
-- Usage:
n = idv Double 42
```
This is equivalent to `n = (42 :: Double)`.
* A wrapper around `typeRep` that uses visible `forall`:
```haskell
-- Definition:
typeRepVis :: forall a -> Typeable a => TypeRep a
typeRepVis a = typeRep @a
-- Usage:
t = typeRepVis (Maybe String)
```
* A wrapper around `sizeOf` that uses visible `forall` instead of `Proxy`:
```haskell
-- Definition:
sizeOfVis :: forall a -> Storable a => Int
sizeOfVis a = sizeOf (Proxy :: Proxy a)
-- Usage:
n = sizeOfVis Int
```
* A wrapper around `symbolVal` that uses visible `forall` instead of `Proxy`:
```haskell
-- Definition:
symbolValVis :: forall s -> KnownSymbol s => String
symbolValVis s = symbolVal (Proxy :: Proxy s)
-- Usage
str = symbolValVis "Hello, World"
```9.10.1Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/23704Visible forall in pattern synonyms2023-08-23T17:14:43ZVladislav ZavialovVisible forall in pattern synonymsGHC Proposals [#281](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst) and [#402](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0402-gadt-syntax.rst) allow the use of vis...GHC Proposals [#281](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst) and [#402](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0402-gadt-syntax.rst) allow the use of visible forall in data constructors. That is, we should be able to write
```haskell
data T a where
MkT :: forall a -> a -> T a
```
A quite relevant ticket that also mentions this is #18389. But what about pattern synonyms?
```haskell
pattern P :: forall a -> a -> T a
pattern P a x = MkT a x
```
The interaction between `PatternSynonyms` and `RequiredTypeArguments` simply hasn't been discussed or specified anywhere.
It's a feature that makes sense. If we are able to define data constructor `MkT`, then we should also be able to define a synonym for it. I don't see any obstacles to implementing this. However, it would be nice to have a real world use case before putting effort into it.https://gitlab.haskell.org/ghc/ghc/-/issues/21272Can't unify `k -> Type` with visible dependent quantification that ignores it...2022-04-02T12:46:00ZIcelandjackCan't unify `k -> Type` with visible dependent quantification that ignores its quantifiee `forall (x :: k) -> Type`I'm making sure this is intended or not, it is possible to wrap `k -> Type` in a VDQ that ignores its argument `forall (x :: k) -> Type` (`Dep`).
But `Indep` fails to compile:
```haskell
{-# Language GADTs #-}
{-# La...I'm making sure this is intended or not, it is possible to wrap `k -> Type` in a VDQ that ignores its argument `forall (x :: k) -> Type` (`Dep`).
But `Indep` fails to compile:
```haskell
{-# Language GADTs #-}
{-# Language PolyKinds #-}
{-# Language RankNTypes #-}
{-# Language StandaloneKindSignatures #-}
import Data.Kind
type Dep :: (k -> Type) -> (forall (x :: k) -> Type)
newtype Dep f a where
Dep :: f a -> Dep f a
{-
• Expected kind ‘forall (x :: k0) -> Type’,
but ‘f’ has kind ‘k0 -> Type’
• In the first argument of ‘Indep’, namely ‘f’
In the type ‘Indep f a’
In the definition of data constructor ‘Indep’
-}
-- type Indep :: (forall (x :: k) -> Type) -> (k -> Type)
-- newtype Indep f a where
-- Indep :: f a -> Indep f a
```https://gitlab.haskell.org/ghc/ghc/-/issues/21040Curious kind-checking failure with GHC 9.2.1 and visible dependent quantifica...2022-02-04T14:33:59ZRyan ScottCurious kind-checking failure with GHC 9.2.1 and visible dependent quantificationWhile porting some code over to GHC 9.2.1 recently, I noticed an unusual quirk in the way kind inference interacts with visible dependent quantification. Consider these two modules:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTyp...While porting some code over to GHC 9.2.1 recently, I noticed an unusual quirk in the way kind inference interacts with visible dependent quantification. Consider these two modules:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
module A where
import Data.Kind
type T1 :: Type -> Type
data T1 a = MkT1
t1FunA :: (forall a. T1 a -> r) -> r
t1FunA g = g MkT1
t1FunB :: T1 a -> T1 a -> ()
t1FunB _ _ = ()
type T2 :: forall (a :: Type) -> Type
data T2 a = MkT2
t2FunA :: (forall a. T2 a -> r) -> r
t2FunA g = g MkT2
t2FunB :: T2 a -> T2 a -> ()
t2FunB _ _ = ()
```
```hs
{-# LANGUAGE NoPolyKinds #-}
module B where
import A
g1 :: ()
g1 = t1FunA $ \x ->
let y = MkT1
in t1FunB x y
g2 :: ()
g2 = t2FunA $ \x ->
let y = MkT2
in t2FunB x y
```
The `A` module defines two data types, `T1` and `T2`, as well as some functions which use them. The only difference between `T1` and `T2` is that the latter uses visible dependent quantification while the former does not. The `B` module uses these functions in a relatively straightforward way. Note that `B` does _not_ enable `PolyKinds` (I distilled this from a `cabal` project which uses `Haskell2010`).
What's curious about this is that while both `g1` and `g2` will typecheck on GHC 9.0.2, only `g1` typechecks on GHC 9.2.1. On the other hand, `g2` will fail to typecheck in GHC 9.2.1:
```
$ ghc-9.2.1 B.hs
[1 of 2] Compiling A ( A.hs, A.o )
[2 of 2] Compiling B ( B.hs, B.o )
B.hs:14:18: error:
• Couldn't match type ‘a’ with ‘*’
Expected: T2 a
Actual: T2 (*)
‘a’ is a rigid type variable bound by
a type expected by the context:
forall a. T2 a -> ()
at B.hs:(12,15)-(14,18)
• In the second argument of ‘t2FunB’, namely ‘y’
In the expression: t2FunB x y
In the expression: let y = MkT2 in t2FunB x y
• Relevant bindings include x :: T2 a (bound at B.hs:12:16)
|
14 | in t2FunB x y
| ^
```
I'm not confident enough to claim with 100% certainty that this is a regression, since the use of `NoPolyKinds` might be throwing a wrench into things. Indeed, enabling `PolyKinds` is enough to make the program accepted again. Still, the fact that this _only_ fails if the data type uses visible dependent quantification (and _only_ with GHC 9.2.1) is rather strange, so I wanted to file an issue to ask people more knowledgeable in this space than I am.https://gitlab.haskell.org/ghc/ghc/-/issues/19775Visible type application (VTA) and datatype contexts are incompatible2021-05-07T20:05:50ZSimon Peyton JonesVisible type application (VTA) and datatype contexts are incompatibleConsider
```
data Ord a => T a = MkT (Maybe a)
foo = MkT @Int
```
Currently we get
```
Foo.hs:8:7: error:
• Cannot apply expression of type ‘Maybe a0 -> T a0’
to a visible type argument ‘Int’
• In the expression: MkT @Int
...Consider
```
data Ord a => T a = MkT (Maybe a)
foo = MkT @Int
```
Currently we get
```
Foo.hs:8:7: error:
• Cannot apply expression of type ‘Maybe a0 -> T a0’
to a visible type argument ‘Int’
• In the expression: MkT @Int
In an equation for ‘foo’: foo = MkT @Int
|
8 | foo = MkT @Int
| ^^^^^^^^
```
This a known infelicity, and perhaps not an important one.
But it turns out to be easy to fix as part of other work on #18481https://gitlab.haskell.org/ghc/ghc/-/issues/18939Data family instance with visible forall in return kind is incorrectly rejected2020-11-15T12:41:19ZRyan ScottData family instance with visible forall in return kind is incorrectly rejectedGHC 8.10 and later reject this program:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
import Data.Kind
...GHC 8.10 and later reject this program:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
import Data.Kind
data family Hm :: forall a -> a -> Type
data instance Hm :: forall a -> a -> Type
```
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:1: error:
• Expecting one more argument to ‘Hm’
Expected kind ‘a -> *’, but ‘Hm’ has kind ‘forall a -> a -> *’
• In the data instance declaration for ‘Hm’
|
11 | data instance Hm :: forall a -> a -> Type
| ^^^^^^^^^^^^^^^^
```
I claim that this should be accepted, however. This is especially strange since GHC _does_ accept this program if `Hm` is changed from a data family to a normal data type:
```hs
data Hm :: forall a -> a -> Type
```
The culprit is [this code in `tcDataFamInstHeader`](https://gitlab.haskell.org/ghc/ghc/-/blob/a1f34d37b47826e86343e368a5c00f1a4b1f2bce/compiler/GHC/Tc/TyCl/Instance.hs#L931-938):
```haskell
-- See Note [Result kind signature for a data family instance]
tc_kind_sig (Just hs_kind)
= do { sig_kind <- tcLHsKindSig data_ctxt hs_kind
; let (tvs, inner_kind) = tcSplitForAllTys sig_kind
; lvl <- getTcLevel
; (subst, _tvs') <- tcInstSkolTyVarsAt lvl False emptyTCvSubst tvs
-- Perhaps surprisingly, we don't need the skolemised tvs themselves
; return (substTy subst inner_kind) }
```
The use of `tcSplitForAllTys` above incorrectly splits off the `forall a` in `forall a -> a -> Type`, but really, we should only be splitting off _invisible_ `forall`s in the result kind. Changing `tcSplitForAllTys` to `tcSplitForAllTysInvis` would fix this issue.
In fact, there are a number of places where we ought to use `tcSplitForAllTysInvis` instead of `tcSplitForAllTys`. This was originally noticed in https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4417#note_311329, but this bug can be understood independently of !4417.9.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/18660Make the forall-or-nothing rule only apply to invisible foralls2020-09-08T23:16:01ZRyan ScottMake the forall-or-nothing rule only apply to invisible forallsCurrently, the `forall`-or-nothing rule is defined ([according to the GHC User's Guide](https://gitlab.haskell.org/ghc/ghc/-/blob/a1f34d37b47826e86343e368a5c00f1a4b1f2bce/docs/users_guide/exts/explicit_forall.rst#L54-56)) as: if a type h...Currently, the `forall`-or-nothing rule is defined ([according to the GHC User's Guide](https://gitlab.haskell.org/ghc/ghc/-/blob/a1f34d37b47826e86343e368a5c00f1a4b1f2bce/docs/users_guide/exts/explicit_forall.rst#L54-56)) as: if a type has an outermost, explicit `forall`, then all of the type variables in the type must be explicitly quantified. This does not say anything about whether the `forall` is visible or invisible, and indeed, GHC currently applies this rule equally to both forms of `forall`s. As a consequence, the following will be rejected:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
module Foo where
type F :: forall a -> b -> b
type F x y = y
```
While the `forall`-or-nothing rule has long been established for invisible `forall`s, it's less clear that it should apply to visible `forall`s like in the program above. @rae lays out the case against the `forall`-or-nothing rule applying to visible `forall`s quite clearly in https://gitlab.haskell.org/ghc/ghc/-/issues/16762#note_297270:
> * Listing variables in a visible `forall` has a concrete, unignorable impact on the type. So if a visible `forall` triggers forall-or-nothing, users will almost certainly have to write a second, invisible `forall` to deal with an unscoped variables.
> * A user who explicitly wants forall-or-nothing can always write `forall.` at the top of every type.
> * A user who explicitly wants to manually scope all type variables can enable `-XNoImplicitForAll`. (https://github.com/ghc-proposals/ghc-proposals/pull/285, which is not yet implemented, as far as I know)
The consensus reached after discussion in #16762 is to revise the `forall`-or-nothing rule to only apply to invisible `forall`s. Although this changes the semantics of the language ever-so-slightly, I would argue that this falls below the bar needed for a GHC proposal, since:
* It it strictly backwards-compatible, as no current programs will break under the new scheme.
* Since visible `forall`s can only be used in kinds, the only way one can observe this behavior is to write a standalone kind signature. And standalone kind signatures are an experimental feature that is subject to change, as [mentioned in the GHC 8.10.1 release notes](https://downloads.haskell.org/~ghc/8.10.1/docs/html/users_guide/8.10.1-notes.html#language).
A knock-on benefit of making this change is that it will make implementing a fix for #16762 much easier. The full details aren't terribly important, but read https://gitlab.haskell.org/ghc/ghc/-/issues/16762#note_294998 if you want to know more.9.2.1Ryan ScottRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/18271Visible dependent quantification permitted in standalone deriving declarations2020-07-01T11:20:08ZRyan ScottVisible dependent quantification permitted in standalone deriving declarationsGHC 8.10.1 and later incorrectly allow VDQ in the type of a standalone `deriving` declaration:
```hs
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
module Bug where
class C a
deriving in...GHC 8.10.1 and later incorrectly allow VDQ in the type of a standalone `deriving` declaration:
```hs
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
module Bug where
class C a
deriving instance forall a -> C (Maybe a)
```
Note that this only applies to standalone-derived instances. If you remove the `deriving` part of the last line, then GHC will reject it as expected.9.0.1Ryan ScottRyan Scott