GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-09-25T17:22:29Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/13408Consider inferring a higher-rank kind for type synonyms2020-09-25T17:22:29ZRichard Eisenbergrae@richarde.devConsider inferring a higher-rank kind for type synonymsIn terms, a definition comprising one non-recursive equation may have a higher-rank type inferred. For example:
```hs
f :: (forall a. a -> a -> a) -> Int
f z = z 0 1
g = f
```
`g` gets an inferred type equal to `f`'s. However, this fa...In terms, a definition comprising one non-recursive equation may have a higher-rank type inferred. For example:
```hs
f :: (forall a. a -> a -> a) -> Int
f z = z 0 1
g = f
```
`g` gets an inferred type equal to `f`'s. However, this fails at the type level:
```hs
type F (z :: forall a. a -> a -> a) = z 0 1
type G = F
```
If anything is strange here, it's that the term-level definition is accepted. GHC should not be in the business of inferring higher-rank types. But there is an exception for definitions comprising one non-recursive equation.
This ticket proposes expanding this behavior to the type level, allowing `G` to be accepted.
This is spun off from #13399, but is not tightly coupled to that ticket.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.0.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Consider inferring a higher-rank kind for type synonyms","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"In terms, a definition comprising one non-recursive equation may have a higher-rank type inferred. For example:\r\n\r\n{{{#!hs\r\nf :: (forall a. a -> a -> a) -> Int\r\nf z = z 0 1\r\n\r\ng = f\r\n}}}\r\n\r\n`g` gets an inferred type equal to `f`'s. However, this fails at the type level:\r\n\r\n{{{#!hs\r\ntype F (z :: forall a. a -> a -> a) = z 0 1\r\n\r\ntype G = F\r\n}}}\r\n\r\nIf anything is strange here, it's that the term-level definition is accepted. GHC should not be in the business of inferring higher-rank types. But there is an exception for definitions comprising one non-recursive equation.\r\n\r\nThis ticket proposes expanding this behavior to the type level, allowing `G` to be accepted.\r\n\r\nThis is spun off from #13399, but is not tightly coupled to that ticket.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14419Check kinds for ambiguity2020-06-21T12:03:16ZRichard Eisenbergrae@richarde.devCheck kinds for ambiguityGHC does an ambiguity check on types. It should also do the same for kinds. Here is a program that should be rejected:
```hs
type family F a
data T :: F a -> Type
```
`T`'s kind is ambiguous, and any occurrence of `T` will be rejected....GHC does an ambiguity check on types. It should also do the same for kinds. Here is a program that should be rejected:
```hs
type family F a
data T :: F a -> Type
```
`T`'s kind is ambiguous, and any occurrence of `T` will be rejected. Instead of rejecting usage sites, let's just reject the definition site.
This check would be disabled by `AllowAmbiguousTypes`.
Happily, I think the implementation should be easy, and that the current algorithm to check for ambiguous types should work for kinds, too. After all, types and kinds are the same these days.
This was inspired by #14203, but no need to read that ticket to understand this one.
EDIT: See [ticket:14419\#comment:160844](https://gitlab.haskell.org//ghc/ghc/issues/14419#note_160844) and [ticket:14419\#comment:163265](https://gitlab.haskell.org//ghc/ghc/issues/14419#note_163265) for the nub of what needs to be done here.https://gitlab.haskell.org/ghc/ghc/-/issues/16371GHC should be more forgiving with visible dependent quantification in visible...2020-11-09T15:26:20ZRyan ScottGHC should be more forgiving with visible dependent quantification in visible type applicationsGHC HEAD currently rejects the following code:
```hs
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
imp...GHC HEAD currently rejects the following code:
```hs
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
import Data.Kind
import Data.Proxy
f :: forall k (a :: k). Proxy a
f = Proxy
g :: forall (a :: forall x -> x -> Type). Proxy a
g = f @(forall x -> x -> Type) @a
```
```
GHCi, version 8.9.20190227: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:14:6: error:
• Illegal visible, dependent quantification in the type of a term:
forall x -> x -> *
(GHC does not yet support this)
• In the type signature:
g :: forall (a :: forall x -> x -> Type). Proxy a
|
14 | g :: forall (a :: forall x -> x -> Type). Proxy a
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This test is implemented in `TcValidity.vdqAllowed`.
But GHC is being too conservative here. `forall x -> x -> *` _isn't_ the type of a term here, but rather the kind of a type variable, and it's perfectly admissible to use visible dependent quantification in such a scenario.
The immediate reason that this happens is because of this code:
```hs
vdqAllowed (TypeAppCtxt {}) = False
```
Unfortunately, fixing this bug isn't as simply as changing `False` to `True`. If you do that, then GHC becomes _too_ forgiving and allows things like this:
```hs
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
lol :: forall a. a
lol = undefined
t2 = lol @(forall a -> a -> a)
```
Here, visible dependent quantification is leaking into the type of a term, which we definitely don't want to happen.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.9 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC should be more forgiving with visible dependent quantification in visible type applications","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.9","keywords":["VisibleDependentQuantification"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC HEAD currently rejects the following code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ImpredicativeTypes #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeApplications #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\nf :: forall k a. Proxy a\r\nf = Proxy\r\n\r\ng :: forall (a :: forall x -> x -> Type). Proxy a\r\ng = f @(forall x -> x -> Type) @a\r\n}}}\r\n{{{\r\nGHCi, version 8.9.20190227: https://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:14:6: error:\r\n • Illegal visible, dependent quantification in the type of a term:\r\n forall x -> x -> *\r\n (GHC does not yet support this)\r\n • In the type signature:\r\n g :: forall (a :: forall x -> x -> Type). Proxy a\r\n |\r\n14 | g :: forall (a :: forall x -> x -> Type). Proxy a\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nBut GHC is being too conservative here. `forall x -> x -> *` //isn't// the type of a term here, but rather the kind of a type variable, and it's perfectly admissible to use visible dependent quantification in such a scenario.\r\n\r\nThe immediate reason that this happens is because of this code:\r\n\r\n{{{#!hs\r\nvdqAllowed (TypeAppCtxt {}) = False\r\n}}}\r\n\r\nUnfortunately, fixing this bug isn't as simply as changing `False` to `True`. If you do that, then GHC becomes //too// forgiving and allows things like this:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ImpredicativeTypes #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n\r\nlol :: forall a. a\r\nlol = undefined\r\n\r\nt2 = lol @(forall a -> a -> a)\r\n}}}\r\n\r\nHere, visible dependent quantification is leaking into the type of a term, which we definitely don't want to happen.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/17072Dependent quantification prevents unification2022-03-21T13:45:41ZVladislav ZavialovDependent quantification prevents unification## Summary
Replacing `k -> Type` with `forall (a :: k) -> Type` in a kind of a type constructor should not have any effect. The latter gives a name to the variable, but is otherwise equivalent... or so I thought.
Consider these definit...## Summary
Replacing `k -> Type` with `forall (a :: k) -> Type` in a kind of a type constructor should not have any effect. The latter gives a name to the variable, but is otherwise equivalent... or so I thought.
Consider these definitions:
```
data B1 :: k -> Type
type family F1 :: k -> Type where
F1 = B1
```
GHC happily accepts them, unifying the kinds of `B1` and `F1`. However, if I make use of dependent quantification in `B` but not in `F`:
```
data B2 :: forall (a :: k) -> Type
type family F2 :: k -> Type where
F2 = B2
```
... GHC gets confused:
```
• Expected kind ‘k1 -> Type’,
but ‘B2’ has kind ‘forall (a :: k0) -> Type’
• In the type ‘B2’
In the type family declaration for ‘F2’
|
14 | F2 = B2
| ^^
```
## Steps to reproduce
Load this in GHCi:
```
{-# LANGUAGE PolyKinds, TypeFamilies, RankNTypes #-}
module T where
import Data.Kind (Type)
data B1 :: k -> Type
type family F1 :: k -> Type where
F1 = B1
data B2 :: forall (a :: k) -> Type
type family F2 :: k -> Type where
F2 = B2
```
## Expected behavior
Both `F1` and `F2` should be accepted.
## Environment
* GHC version used: HEADVladislav ZavialovVladislav Zavialovhttps://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/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/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/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/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/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/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/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/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/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.