GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2024-03-26T15:32:05Zhttps://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/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/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/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 Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/17687ASSERT failure with visible dependent quantification2020-01-27T17:46:33ZRichard Eisenbergrae@richarde.devASSERT failure with visible dependent quantificationIf I say
```hs
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where
x :: forall a -> a -> a
x = x
```
I get
```
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.11.0.20200108:
ASSERT failed! file compiler/GHC/Hs/Typ...If I say
```hs
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where
x :: forall a -> a -> a
x = x
```
I get
```
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.11.0.20200108:
ASSERT failed! file compiler/GHC/Hs/Types.hs, line 970
```
Of course, my program should be rejected, but not with an ASSERTion failure.
Tagging @RyanGlScott, Mr. VDQ.https://gitlab.haskell.org/ghc/ghc/-/issues/17164Standalone kind signature with VDQ does not roundtrip through Template Haskell2020-01-15T11:39:35ZRyan ScottStandalone kind signature with VDQ does not roundtrip through Template HaskellI would expect the following program to compile:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_...I would expect the following program to compile:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -ddump-splices #-}
module Bug where
import Data.Kind
$([d| type T :: forall k -> k -> Type
type family T :: forall k -> k -> Type
|])
```
But it doesn't:
```
$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o, Bug.dyn_o )
Bug.hs:(11,3)-(13,6): Splicing declarations
[d| type T_arW :: forall k_aWR -> k_aWR -> Type
type family T_arW :: forall k_arX -> k_arX -> Type |]
======>
type T_a4bz :: forall k_aWR. k_aWR -> Type
type family T_a4bz :: forall k_a4bA -> k_a4bA -> Type
Bug.hs:11:3: error:
• Couldn't match expected kind ‘forall k0 -> k0 -> *’
with actual kind ‘k -> *’
• In the type family declaration for ‘T’
|
11 | $([d| type T :: forall k -> k -> Type
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
As the `-ddump-splices` output reveals, roundtripping through Template Haskell appears to have turned `type T :: forall k -> k -> Type` into `forall k. k -> Type`, which is a different thing altogether. Note that the `forall k -> k -> Type` in the explicit return kind of `type family T` is _not_ affected.Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/15658strange inferred kind with TypeInType2019-07-07T18:03:34Zdmwitstrange inferred kind with TypeInTypeThis type family has a strange kind to begin with:
```
{-# Language TypeFamilies , TypeInType #-}
type family F f a :: a
```
But it gets even stranger when you ask ghci what it thinks about F:
```
> :k F
F :: * -> forall a -> a
```
T...This type family has a strange kind to begin with:
```
{-# Language TypeFamilies , TypeInType #-}
type family F f a :: a
```
But it gets even stranger when you ask ghci what it thinks about F:
```
> :k F
F :: * -> forall a -> a
```
There is a forall which doesn't seem to bind any variables and hasn't got the customary delimiting dot.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.4.2 |
| 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":"strange inferred kind with TypeInType","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This type family has a strange kind to begin with:\r\n\r\n{{{\r\n{-# Language TypeFamilies , TypeInType #-}\r\ntype family F f a :: a\r\n}}}\r\n\r\nBut it gets even stranger when you ask ghci what it thinks about F:\r\n\r\n{{{\r\n> :k F\r\nF :: * -> forall a -> a\r\n}}}\r\n\r\nThere is a forall which doesn't seem to bind any variables and hasn't got the customary delimiting dot.","type_of_failure":"OtherFailure","blocking":[]} -->8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/15869Discrepancy between seemingly equivalent type synonym and type family2019-07-07T18:02:38ZRyan ScottDiscrepancy between seemingly equivalent type synonym and type familyConsider the following code:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug wher...Consider the following code:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
type KindOf1 (a :: k) = k
type family KindOf2 (a :: k) :: Type where
KindOf2 (a :: k) = k
data A (a :: Type) :: a -> Type
type family Apply1 (f :: KindOf1 A) (a :: Type) (x :: a) :: Type where
Apply1 f a x = f a x
```
`Apply1` kind-checks, which is just peachy. Note that `Apply1` uses `KindOf1`, which is a type synonym. Suppose I wanted to swap out `KindOf1` for `KindOf2`, which is (seemingly) an equivalent type family. I can define this:
```hs
type family Apply2 (f :: KindOf2 A) -- (f :: forall a -> a -> Type)
(a :: Type)
(x :: a)
:: Type where
Apply2 f a x = f a x
```
However, GHC rejects this!
```
$ /opt/ghc/8.6.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:25:10: error:
• Expecting two more arguments to ‘f’
Expected kind ‘KindOf2 A’, but ‘f’ has kind ‘* -> a -> *’
• In the first argument of ‘Apply2’, namely ‘f’
In the type family declaration for ‘Apply2’
|
25 | Apply2 f a x = f a x
| ^
```
I find this quite surprising, since I would have expected `KindOf1` and `KindOf2` to be functionally equivalent. Even providing explicit `forall`s does not make it kind-check:
```hs
type family Apply2 (f :: KindOf2 A) -- (f :: forall a -> a -> Type)
(a :: Type)
(x :: a)
:: Type where
forall (f :: KindOf2 A) (a :: Type) (x :: a).
Apply2 f a x = f a x
```
Although the error message does change a bit:
```
$ ~/Software/ghc3/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:26:20: error:
• Expected kind ‘* -> a -> *’, but ‘f’ has kind ‘KindOf2 A’
• In the type ‘f a x’
In the type family declaration for ‘Apply2’
|
26 | Apply2 f a x = f a x
| ^^^^^
```https://gitlab.haskell.org/ghc/ghc/-/issues/16326Implement visible dependent quantification2019-07-07T18:00:29ZRyan ScottImplement visible dependent quantificationGHC proposal 35 ([A syntax for visible dependent quantification](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0035-forall-arrow.rst)) has been accepted. This ticket tracks its implementation.
Along with implement...GHC proposal 35 ([A syntax for visible dependent quantification](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0035-forall-arrow.rst)) has been accepted. This ticket tracks its implementation.
Along with implementing it, we should also document it in the users' guide (the subject of #15658).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.7 |
| 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":"Implement visible dependent quantification","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.10.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":["GHCProposal"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"GHC proposal 35 ([https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0035-forall-arrow.rst A syntax for visible dependent quantification]) has been accepted. This ticket tracks its implementation.\r\n\r\nAlong with implementing it, we should also document it in the users' guide (the subject of #15658).","type_of_failure":"OtherFailure","blocking":[]} -->8.10.1