GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2022-11-01T08:49:22Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/22384Visible type application in record patterns2022-11-01T08:49:22ZTarmeanVisible type application in record patterns## Motivation
I've been using type applications in patterns quite a bit recently and struggled when adding or removing an argument from the constructors because all pattern matches must add/remove wildcards.
```haskell
lookupQMap :: fo...## Motivation
I've been using type applications in patterns quite a bit recently and struggled when adding or removing an argument from the constructors because all pattern matches must add/remove wildcards.
```haskell
lookupQMap :: forall a. Typeable a => QKey a -> QMap -> Maybe a
lookupQMap qid qmap =
-- This could use a Data.Typeable.cast, but it's simplified from some more complex code
case lookupQ qid qmap of
ResultEntry @r' dat _
| Just Refl <- eqT @r @r' -> ...
```
The nice way to avoid the problem would be to use record patterns. But mixing type applications with record patterns results in a parse error!
```haskell
case lookupQ qid qmap of
ResultEntry @r {resultData=dat}
-- [parser] [E] parser error on input '{'
```
I'm not sure if this is intentional, an oversight, or whether I'm missing the right syntax. It'd be really useful, though!
## Proposal
If the missing syntax is an oversight it hopefully could be added without making the grammar overly ambiguous. I do not know whether this would require a separate proposal.
If the feature already exists or is intentionally missing it maybe could be documented somewhere, though I'm not sure what the right place would be. I couldn't find a mention in the proposal or paper at least.https://gitlab.haskell.org/ghc/ghc/-/issues/15782Visible type/kind applications in declaration of data/type constructors2021-07-22T06:34:07ZIcelandjackVisible type/kind applications in declaration of data/type constructorsI'm making this ticket to keep track of this, I don't know if it's a good idea.
Allow visible type/kind applications when declaring data/type constructors on the LHS of `::` (from [Phab comment](https://phabricator.haskell.org/D5229#144...I'm making this ticket to keep track of this, I don't know if it's a good idea.
Allow visible type/kind applications when declaring data/type constructors on the LHS of `::` (from [Phab comment](https://phabricator.haskell.org/D5229#144558)).
```hs
data
Proxy @k :: k -> Type where
MkProxy @k :: Proxy @k (a :: k)
```
&
```hs
data
Fin :: N -> Type where
FinO @n :: Fin (S n)
FinS @n :: Fin n -> Fin (S n)
```
&
```hs
data
Elem @k @n :: Vec n k -> Type where
ElemO @a @as :: Elem @k @(S n) (a:>as)
ElemS @a @as :: Elem @k @n as
-> Elem @k @(S n) (a:>as)
```https://gitlab.haskell.org/ghc/ghc/-/issues/15596When a type application cannot be applied to an identifier due to the absence...2021-09-07T15:54:40ZkindaroWhen a type application cannot be applied to an identifier due to the absence of an explicit type signature, let the error just say so!Consider this code:
```hs
{-# language TypeApplications #-}
module TypeApplicationsErrorMessage where
f = (+)
g = f @Integer
```
This is what happens when I try to compile it:
```hs
% ghc TypeApplicationsErrorMessage.hs
[1 of 1] Com...Consider this code:
```hs
{-# language TypeApplications #-}
module TypeApplicationsErrorMessage where
f = (+)
g = f @Integer
```
This is what happens when I try to compile it:
```hs
% ghc TypeApplicationsErrorMessage.hs
[1 of 1] Compiling TypeApplicationsErrorMessage ( TypeApplicationsErrorMessage.hs, TypeApplicationsErrorMessage.o )
TypeApplicationsErrorMessage.hs:6:5: error:
• Cannot apply expression of type ‘a0 -> a0 -> a0’
to a visible type argument ‘Integer’
• In the expression: f @Integer
In an equation for ‘g’: g = f @Integer
|
6 | g = f @Integer
| ^^^^^^^^^^
```
This error is easily fixed by supplying an explicit type signature to `f`. So, perhaps the error message could just say so?
I am observing this with `The Glorious Glasgow Haskell Compilation System, version 8.6.0.20180810`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | |
| 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":"When a type application cannot be applied to an identifier due to the absence of an explicit type signature, let the error just say so!","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Consider this code:\r\n\r\n{{{#!hs\r\n{-# language TypeApplications #-}\r\n\r\nmodule TypeApplicationsErrorMessage where\r\n\r\nf = (+)\r\ng = f @Integer\r\n}}}\r\n\r\nThis is what happens when I try to compile it:\r\n\r\n{{{#!hs\r\n% ghc TypeApplicationsErrorMessage.hs\r\n[1 of 1] Compiling TypeApplicationsErrorMessage ( TypeApplicationsErrorMessage.hs, TypeApplicationsErrorMessage.o )\r\n\r\nTypeApplicationsErrorMessage.hs:6:5: error:\r\n • Cannot apply expression of type ‘a0 -> a0 -> a0’\r\n to a visible type argument ‘Integer’\r\n • In the expression: f @Integer\r\n In an equation for ‘g’: g = f @Integer\r\n |\r\n6 | g = f @Integer\r\n | ^^^^^^^^^^\r\n}}}\r\n\r\nThis error is easily fixed by supplying an explicit type signature to `f`. So, perhaps the error message could just say so?\r\n\r\nI am observing this with `The Glorious Glasgow Haskell Compilation System, version 8.6.0.20180810`.","type_of_failure":"OtherFailure","blocking":[]} -->⊥https://gitlab.haskell.org/ghc/ghc/-/issues/13512GHC incorrectly warns that a scoped type variable used in a term's body is un...2023-08-02T10:36:39ZRyan ScottGHC incorrectly warns that a scoped type variable used in a term's body is unusedThis bug is reproducible on GHC 8.0.1, 8.0.2, 8.2, and HEAD.
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -Wunused-foralls #-}
module Bu...This bug is reproducible on GHC 8.0.1, 8.0.2, 8.2, and HEAD.
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -Wunused-foralls #-}
module Bug where
import Data.Proxy
proxy :: forall k (a :: k). Proxy a
proxy = Proxy
data SomeProxy where
SomeProxy :: forall k (a :: k). Proxy a -> SomeProxy
someProxy :: forall k (a :: k). SomeProxy
someProxy = SomeProxy (proxy @k @a)
```
```
$ /opt/ghc/head/bin/ghci Bug.hs
GHCi, version 8.3.20170327: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:17:23: warning: [-Wunused-foralls]
Unused quantified type variable ‘(a :: k)’
In the type ‘forall k (a :: k). SomeProxy’
|
17 | someProxy :: forall k (a :: k). SomeProxy
| ^^^^^^^^
Ok, modules loaded: Bug.
```
But that `a` is used in `proxy @k @a`!
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| 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 incorrectly warns that a variable used in a type application is unused","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeApplications"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This bug is reproducible on GHC 8.0.1, 8.0.2, 8.2, and HEAD.\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE TypeInType #-}\r\n\r\n{-# OPTIONS_GHC -Wunused-foralls #-}\r\nmodule Bug where\r\n\r\nimport Data.Proxy\r\n\r\nproxy :: forall k (a :: k). Proxy a\r\nproxy = Proxy\r\n\r\ndata SomeProxy where\r\n SomeProxy :: forall k (a :: k). Proxy a -> SomeProxy\r\n\r\nsomeProxy :: forall k (a :: k). SomeProxy\r\nsomeProxy = SomeProxy (proxy @k @a)\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/ghci Bug.hs\r\nGHCi, version 8.3.20170327: http://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:17:23: warning: [-Wunused-foralls]\r\n Unused quantified type variable ‘(a :: k)’\r\n In the type ‘forall k (a :: k). SomeProxy’\r\n |\r\n17 | someProxy :: forall k (a :: k). SomeProxy\r\n | ^^^^^^^^\r\nOk, modules loaded: Bug.\r\n}}}\r\n\r\nBut that `a` is used in `proxy @k @a`!","type_of_failure":"OtherFailure","blocking":[]} -->Ryan ScottRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/13042Allow type annotations / visible type application in pattern synonyms2019-07-07T18:23:57ZIcelandjackAllow type annotations / visible type application in pattern synonyms```hs
data Lift f a = Pure a | Other (f a)
data V0 a
```
To make a pattern synonym for `a -> Lift V0 a` I would like to be able to write either
```hs
pattern A a = Pure @V0 a
```
or
```hs
pattern B a = (Pure :: _ -> _ V0 _) a
```
t...```hs
data Lift f a = Pure a | Other (f a)
data V0 a
```
To make a pattern synonym for `a -> Lift V0 a` I would like to be able to write either
```hs
pattern A a = Pure @V0 a
```
or
```hs
pattern B a = (Pure :: _ -> _ V0 _) a
```
to be equivalent to
```hs
pattern C :: a -> Lift V0 a
pattern C a = Pure a
```
<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":"Allow type annotations / visible type application in pattern synonyms","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["PatternSynonyms","TypeApplications,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"{{{#!hs\r\ndata Lift f a = Pure a | Other (f a)\r\ndata V0 a\r\n}}}\r\n\r\nTo make a pattern synonym for `a -> Lift V0 a` I would like to be able to write either\r\n\r\n{{{#!hs\r\npattern A a = Pure @V0 a\r\n}}}\r\n\r\nor \r\n\r\n{{{#!hs\r\npattern B a = (Pure :: _ -> _ V0 _) a \r\n}}}\r\n\r\nto be equivalent to \r\n\r\n{{{#!hs\r\npattern C :: a -> Lift V0 a\r\npattern C a = Pure a\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12569TypeApplications allows instantiation of implicitly-quantified kind variables2019-07-07T18:26:02ZAlexey VagarenkoTypeApplications allows instantiation of implicitly-quantified kind variablesTypeApplications doesn't allow unticked list constructor even when it is unambiguous:
```
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
> :set -XDataKinds
> :set -XTypeApplications
> :set -XScopedTypeVariables
> :set -XK...TypeApplications doesn't allow unticked list constructor even when it is unambiguous:
```
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
> :set -XDataKinds
> :set -XTypeApplications
> :set -XScopedTypeVariables
> :set -XKindSignatures
> let foo :: forall (xs :: [Nat]). (); foo = ()
> foo @'[0]
()
> foo @[0]
<interactive>:17:6: error:
* Expected kind `[Nat]', but `[0]' has kind `*'
* In the type `[0]'
In the expression: foo @[0]
In an equation for `it': it = foo @[0]
<interactive>:17:7: error:
* Expected a type, but `0' has kind `Nat'
* In the type `[0]'
In the expression: foo @[0]
In an equation for `it': it = foo @[0]
```
why `[0]` has kind `*` here?
However this is legal:
```
> let foo :: forall (x :: Bool). (); foo = ()
> foo @True
()
> foo @'True
()
```
and this is wierd:
```
> :set -XPolyKinds
> let foo :: forall (x :: k). (); foo = ()
> foo @'True
<interactive>:12:6: error:
* Expected a type, but 'True has kind `Bool'
* In the type `True'
In the expression: foo @True
In an equation for `it': it = foo @True
> foo @True
<interactive>:13:6: error:
* Expected a type, but 'True has kind `Bool'
* In the type `True'
In the expression: foo @True
In an equation for `it': it = foo @True
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"TypeApplications doesn't allow unticked list constructors.","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"TypeApplications doesn't allow unticked list constructor even when it is unambiguous:\r\n\r\n{{{\r\nGHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help\r\n> :set -XDataKinds\r\n> :set -XTypeApplications\r\n> :set -XScopedTypeVariables\r\n> :set -XKindSignatures\r\n> let foo :: forall (xs :: [Nat]). (); foo = ()\r\n> foo @'[0]\r\n()\r\n> foo @[0]\r\n\r\n<interactive>:17:6: error:\r\n * Expected kind `[Nat]', but `[0]' has kind `*'\r\n * In the type `[0]'\r\n In the expression: foo @[0]\r\n In an equation for `it': it = foo @[0]\r\n\r\n<interactive>:17:7: error:\r\n * Expected a type, but `0' has kind `Nat'\r\n * In the type `[0]'\r\n In the expression: foo @[0]\r\n In an equation for `it': it = foo @[0]\r\n}}}\r\nwhy `[0]` has kind `*` here?\r\n\r\nHowever this is legal:\r\n{{{\r\n> let foo :: forall (x :: Bool). (); foo = ()\r\n> foo @True\r\n()\r\n> foo @'True\r\n()\r\n}}}\r\n\r\nand this is wierd: \r\n{{{\r\n> :set -XPolyKinds\r\n> let foo :: forall (x :: k). (); foo = ()\r\n> foo @'True\r\n\r\n<interactive>:12:6: error:\r\n * Expected a type, but 'True has kind `Bool'\r\n * In the type `True'\r\n In the expression: foo @True\r\n In an equation for `it': it = foo @True\r\n> foo @True\r\n\r\n<interactive>:13:6: error:\r\n * Expected a type, but 'True has kind `Bool'\r\n * In the type `True'\r\n In the expression: foo @True\r\n In an equation for `it': it = foo @True\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12363Type application for infix2020-06-08T17:40:48ZIcelandjackType application for infix`1 + @Int 10` is a parse error, I would like it to mean the same as
```hs
(+) @Int 1 10
```
Thoughts?
----
Also
```hs
>>> pure `foldMap` @Maybe @[_] Just 'a'
"a"
>>> foldMap @Maybe @[_] pure (Just 'a')
"a"
```
<details><summary>Tr...`1 + @Int 10` is a parse error, I would like it to mean the same as
```hs
(+) @Int 1 10
```
Thoughts?
----
Also
```hs
>>> pure `foldMap` @Maybe @[_] Just 'a'
"a"
>>> foldMap @Maybe @[_] pure (Just 'a')
"a"
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------- |
| Version | 8.0.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | lowest |
| Resolution | Unresolved |
| Component | Compiler (Parser) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Type application for infix","status":"New","operating_system":"","component":"Compiler (Parser)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeApplications"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"`1 + @Int 10` is a parse error, I would like it to mean the same as\r\n\r\n{{{#!hs\r\n(+) @Int 1 10\r\n}}}\r\n\r\nThoughts?\r\n\r\n----\r\n\r\nAlso\r\n\r\n{{{#!hs\r\n>>> pure `foldMap` @Maybe @[_] Just 'a'\r\n\"a\"\r\n\r\n>>> foldMap @Maybe @[_] pure (Just 'a')\r\n\"a\"\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12085Premature defaulting and variable not in scope2019-07-07T18:27:42ZIcelandjackPremature defaulting and variable not in scope```hs
{-# Language RankNTypes, ScopedTypeVariables, TypeFamilies,
TypeOperators, UnboxedTuples, UnicodeSyntax, ViewPatterns,
QuasiQuotes, TypeInType, ApplicativeDo, TypeApplications,
AllowAmbiguousTypes
#-}
import Data.Kind...```hs
{-# Language RankNTypes, ScopedTypeVariables, TypeFamilies,
TypeOperators, UnboxedTuples, UnicodeSyntax, ViewPatterns,
QuasiQuotes, TypeInType, ApplicativeDo, TypeApplications,
AllowAmbiguousTypes
#-}
import Data.Kind
todo :: forall (a::Type). (Read a, Show a) => String
todo = show @a (read @a "42")
```
there are two things I notice, even with `AllowAmbiguousTypes` the `a` gets defaulted prematurely
```
$ ghci -ignore-dot-ghci -fwarn-type-defaults /tmp/tl0z.hs
GHCi, version 8.0.0.20160511: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/tl0z.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t todo
<interactive>:1:1: warning: [-Wtype-defaults]
Defaulting the following constraints to type ‘()’
(Read a0) arising from a use of ‘it’ at <interactive>:1:1
(Show a0) arising from a use of ‘it’ at <interactive>:1:1
foo :: String
*Main>
```
instead of something like `todo :: forall a. (Read a, Show a) => String`, it can be applied to types
```
*Main> foo @Int
"42"
*Main> foo @Float
"42.0"
```
----
The second thing is that if you want to add an argument independent of `a`
```hs
-- ghci> foo @Int False
-- "100"
-- ghci> foo @Float True
-- "42.0"
foo :: forall (a::Type). (Read a, Show a) => Bool -> String
foo b = show @a (read @a (if b then "42" else "100"))
```
I found no way to define it as
```hs
-- ghci> foo False @Int
-- "100"
-- ghci> foo True @Float
-- "42.0"
foo :: Bool -> forall (a::Type). (Read a, Show a) => String
foo b = show @a (read @a (if b then "42" else "100"))
```
to which GHC persists
```
$ ghci -ignore-dot-ghci -fwarn-type-defaults /tmp/tl0z.hs
GHCi, version 8.0.0.20160511: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/tl0z.hs, interpreted )
/tmp/tl0z.hs:10:15: error: Not in scope: type variable ‘a’
/tmp/tl0z.hs:10:24: error: Not in scope: type variable ‘a’
Failed, modules loaded: none.
Prelude>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Task |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Premature defaulting and variable not in scope","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeApplications"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"{{{#!hs\r\n{-# Language RankNTypes, ScopedTypeVariables, TypeFamilies,\r\n TypeOperators, UnboxedTuples, UnicodeSyntax, ViewPatterns,\r\n QuasiQuotes, TypeInType, ApplicativeDo, TypeApplications,\r\n AllowAmbiguousTypes \r\n#-}\r\n\r\nimport Data.Kind\r\n\r\ntodo :: forall (a::Type). (Read a, Show a) => String\r\ntodo = show @a (read @a \"42\")\r\n}}}\r\n\r\nthere are two things I notice, even with `AllowAmbiguousTypes` the `a` gets defaulted prematurely\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci -fwarn-type-defaults /tmp/tl0z.hs \r\nGHCi, version 8.0.0.20160511: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/tl0z.hs, interpreted )\r\nOk, modules loaded: Main.\r\n*Main> :t todo\r\n\r\n<interactive>:1:1: warning: [-Wtype-defaults]\r\n Defaulting the following constraints to type ‘()’\r\n (Read a0) arising from a use of ‘it’ at <interactive>:1:1\r\n (Show a0) arising from a use of ‘it’ at <interactive>:1:1\r\nfoo :: String\r\n*Main> \r\n}}}\r\n\r\ninstead of something like `todo :: forall a. (Read a, Show a) => String`, it can be applied to types\r\n\r\n{{{\r\n*Main> foo @Int\r\n\"42\"\r\n*Main> foo @Float\r\n\"42.0\"\r\n}}}\r\n\r\n----\r\n\r\nThe second thing is that if you want to add an argument independent of `a`\r\n\r\n{{{#!hs\r\n-- ghci> foo @Int False\r\n-- \"100\"\r\n-- ghci> foo @Float True\r\n-- \"42.0\"\r\n\r\nfoo :: forall (a::Type). (Read a, Show a) => Bool -> String\r\nfoo b = show @a (read @a (if b then \"42\" else \"100\"))\r\n}}}\r\n\r\nI found no way to define it as\r\n\r\n{{{#!hs\r\n-- ghci> foo False @Int \r\n-- \"100\"\r\n-- ghci> foo True @Float \r\n-- \"42.0\"\r\nfoo :: Bool -> forall (a::Type). (Read a, Show a) => String\r\nfoo b = show @a (read @a (if b then \"42\" else \"100\"))\r\n}}}\r\n\r\nto which GHC persists \r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci -fwarn-type-defaults /tmp/tl0z.hs \r\nGHCi, version 8.0.0.20160511: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/tl0z.hs, interpreted )\r\n\r\n/tmp/tl0z.hs:10:15: error: Not in scope: type variable ‘a’\r\n\r\n/tmp/tl0z.hs:10:24: error: Not in scope: type variable ‘a’\r\nFailed, modules loaded: none.\r\nPrelude> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11409Cannot instantiate literals using TypeApplications2020-01-23T19:37:34ZFeuerbachCannot instantiate literals using TypeApplicationsRelevant [reddit post](https://www.reddit.com/r/haskell/comments/60seia/type_application_on_literals/).
----
```
GHCi, version 8.0.1.20160110: http://www.haskell.org/ghc/ :? for help
Prelude> :set -XTypeApplications -fprint-explicit-f...Relevant [reddit post](https://www.reddit.com/r/haskell/comments/60seia/type_application_on_literals/).
----
```
GHCi, version 8.0.1.20160110: http://www.haskell.org/ghc/ :? for help
Prelude> :set -XTypeApplications -fprint-explicit-foralls
Prelude> :t 42
42 :: forall {a}. Num a => a
Prelude> 42 @Int
<interactive>:3:1: error:
• Cannot not apply expression of type ‘a0’
to a visible type argument ‘Int’
• In the expression: 42 @Int
In an equation for ‘it’: it = 42 @Int
```
(Also, "cannot not" looks like a typo.)Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11398Type application for operator sections2019-07-07T18:30:35ZIcelandjackType application for operator sectionsWith `-fprint-explicit-foralls`
```hs
(+ 1) :: forall {a}. Num a => a -> a
```
This means we cannot apply it to a type:
```hs
(+ 1) @Int :: Int -> Int
```
Since sections are sugar `(+ 1)` could be given the type `forall a. Num a => a...With `-fprint-explicit-foralls`
```hs
(+ 1) :: forall {a}. Num a => a -> a
```
This means we cannot apply it to a type:
```hs
(+ 1) @Int :: Int -> Int
```
Since sections are sugar `(+ 1)` could be given the type `forall a. Num a => a -> a` instead.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 7.10.3 |
| 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 application for operator sections","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":["TypeApplications"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"With `-fprint-explicit-foralls`\r\n\r\n{{{#!hs\r\n(+ 1) :: forall {a}. Num a => a -> a\r\n}}}\r\n\r\nThis means we cannot apply it to a type:\r\n\r\n{{{#!hs\r\n(+ 1) @Int :: Int -> Int\r\n}}}\r\n\r\nSince sections are sugar `(+ 1)` could be given the type `forall a. Num a => a -> a` instead.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11387Typecasting using type application syntax2019-07-07T18:30:38ZIcelandjackTypecasting using type application syntaxI created #11350 to allow visible (static) type applications in patterns. I had a [thought](https://ghc.haskell.org/trac/ghc/ticket/11350#comment:2) about translating non-parametric type applications in patterns as a runtime type check (...I created #11350 to allow visible (static) type applications in patterns. I had a [thought](https://ghc.haskell.org/trac/ghc/ticket/11350#comment:2) about translating non-parametric type applications in patterns as a runtime type check (`Typeable`) and decided to create a ticket in case it made any sense. Example:
```hs
doubleWhenInt :: forall a. Typeable a => a -> a
doubleWhenInt x =
case eqT @Int @a of
Just Refl -> x + x
Nothing -> x
-- Becomes…
doubleWhenInt :: Typeable a => a -> a
doubleWhenInt @Int n = n + n
doubleWhenInt @_ x = x
```
Thoughts?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | |
| 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":"Typecasting using type application syntax","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":["TypeApplications"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"I created #11350 to allow visible (static) type applications in patterns. I had a [https://ghc.haskell.org/trac/ghc/ticket/11350#comment:2 thought] about translating non-parametric type applications in patterns as a runtime type check (`Typeable`) and decided to create a ticket in case it made any sense. Example:\r\n\r\n{{{#!hs\r\ndoubleWhenInt :: forall a. Typeable a => a -> a\r\ndoubleWhenInt x =\r\n case eqT @Int @a of\r\n Just Refl -> x + x\r\n Nothing -> x\r\n\r\n-- Becomes…\r\ndoubleWhenInt :: Typeable a => a -> a\r\ndoubleWhenInt @Int n = n + n\r\ndoubleWhenInt @_ x = x\r\n}}}\r\n\r\nThoughts?","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11352Allow applying type to label2023-06-05T11:55:16ZIcelandjackAllow applying type to label```hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DataKinds #...```hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DataKinds #-}
import GHC.TypeLits
import GHC.OverloadedLabels
instance IsLabel "answer" Int where
fromLabel _ = 42
answer :: IsLabel "answer" a => a
answer = #answer
```
The follow works:
```hs
>>> answer @Int
42
```
but fails with a label:
```hs
>>> #answer @Int
<interactive>:...:1: error:
• Cannot not apply expression of type ‘t0’
to a visible type argument ‘Int’
• In the expression: #answer @Int
In an equation for ‘it’: it = #answer @Int
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 7.10.3 |
| 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":"Allow applying type to label","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"{{{#!hs\r\n{-# LANGUAGE FlexibleInstances #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE OverloadedLabels #-}\r\n{-# LANGUAGE MultiParamTypeClasses #-}\r\n{-# LANGUAGE DataKinds #-}\r\n\r\nimport GHC.TypeLits\r\nimport GHC.OverloadedLabels\r\n\r\ninstance IsLabel \"answer\" Int where\r\n fromLabel _ = 42\r\n\r\nanswer :: IsLabel \"answer\" a => a\r\nanswer = #answer\r\n}}}\r\n\r\nThe follow works:\r\n\r\n{{{#!hs\r\n>>> answer @Int\r\n42\r\n}}}\r\n\r\nbut fails with a label:\r\n\r\n{{{#!hs\r\n>>> #answer @Int\r\n<interactive>:...:1: error:\r\n • Cannot not apply expression of type ‘t0’\r\n to a visible type argument ‘Int’\r\n • In the expression: #answer @Int\r\n In an equation for ‘it’: it = #answer @Int\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->isovectorisovectorhttps://gitlab.haskell.org/ghc/ghc/-/issues/11349[TypeApplications] Create Proxy-free alternatives of functions in base2019-07-07T18:30:48ZIcelandjack[TypeApplications] Create Proxy-free alternatives of functions in baseNow that we have [TypeApplications](https://phabricator.haskell.org/D1138) how about we create a Proxy-free version of functions in base that currently require it:
```hs
tr :: forall a. Typeable a => TypeRep
tr = typeRep @Proxy @a Proxy...Now that we have [TypeApplications](https://phabricator.haskell.org/D1138) how about we create a Proxy-free version of functions in base that currently require it:
```hs
tr :: forall a. Typeable a => TypeRep
tr = typeRep @Proxy @a Proxy
symbol :: forall s. KnownSymbol s => String
symbol = symbolVal @s Proxy
nat :: forall n. KnownNat n => Integer
nat = natVal @n Proxy
```
While we're at it let's use [Natural](https://hackage.haskell.org/package/base/docs/Numeric-Natural.html) as the value-level representation of Nat, avoiding `Maybe` in `someNatVal :: Integer -> Maybe SomeNat`:
```hs
nat :: forall n. KnownNat n => Natural
nat = natVal @n Proxy
someNatVal :: Natural -> SomeNat
someNatVal = ...
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 7.10.3 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Core Libraries |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | ekmett |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"[TypeApplications] Create Proxy-free alternatives of functions in base","status":"New","operating_system":"","component":"Core Libraries","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":["TypeApplications"],"differentials":[],"test_case":"","architecture":"","cc":["ekmett"],"type":"FeatureRequest","description":"Now that we have [https://phabricator.haskell.org/D1138 TypeApplications] how about we create a Proxy-free version of functions in base that currently require it:\r\n\r\n{{{#!hs\r\ntr :: forall a. Typeable a => TypeRep\r\ntr = typeRep @Proxy @a Proxy\r\n\r\nsymbol :: forall s. KnownSymbol s => String\r\nsymbol = symbolVal @s Proxy\r\n\r\nnat :: forall n. KnownNat n => Integer\r\nnat = natVal @n Proxy\r\n}}}\r\n\r\nWhile we're at it let's use [https://hackage.haskell.org/package/base/docs/Numeric-Natural.html Natural] as the value-level representation of Nat, avoiding `Maybe` in `someNatVal :: Integer -> Maybe SomeNat`: \r\n\r\n{{{#!hs\r\nnat :: forall n. KnownNat n => Natural\r\nnat = natVal @n Proxy\r\n\r\nsomeNatVal :: Natural -> SomeNat\r\nsomeNatVal = ...\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->