GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:03:41Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/15628Higher-rank kinds2019-07-07T18:03:41ZIcelandjackHigher-rank kindsTaken from [Data.Eq.Type.Hetero](https://github.com/ekmett/eq/blob/master/src/Data/Eq/Type/Hetero.hs#L73).
`(:==)` (called `HEq` to avoid unnecessary extensions) fails if you add a `Proxy x ->` argument.
```hs
{-# Language RankNTypes, ...Taken from [Data.Eq.Type.Hetero](https://github.com/ekmett/eq/blob/master/src/Data/Eq/Type/Hetero.hs#L73).
`(:==)` (called `HEq` to avoid unnecessary extensions) fails if you add a `Proxy x ->` argument.
```hs
{-# Language RankNTypes, KindSignatures, PolyKinds, GADTs, DataKinds #-}
import Data.Kind
import Data.Proxy
newtype HEq :: forall j. j -> forall k. k -> Type where
HEq
:: (forall (x::forall xx. xx -> Type). Proxy x -> x a -> x b)
-> HEq a b
```
```
$ ~/code/latestghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 398.hs
GHCi, version 8.7.20180828: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 398.hs, interpreted )
398.hs:7:2: error:
• A newtype constructor cannot have existential type variables
HEq :: forall j k xx (a :: j) (b :: k).
(forall (x :: forall xx1. xx1 -> *). Proxy x -> x a -> x b)
-> HEq a b
• In the definition of data constructor ‘HEq’
In the newtype declaration for ‘HEq’
|
7 | HEq
| ^^^...
Failed, no modules loaded.
Prelude>
```
It compiles fine without `Proxy x ->`. Now my question is what existential type variable does `HEq` have, `-fprint-explicit-kinds` shows that `Proxy` is actually being instantiated at `(xx -> Type)` and not `(forall xx. xx -> Type)`
```
398.hs:10:2: error:
• A newtype constructor cannot have existential type variables
HEq :: forall j k xx (a :: j) (b :: k).
(forall (x :: forall xx1. xx1 -> *).
Proxy (xx -> *) (x xx) -> x j a -> x k b)
-> HEq j a k b
• In the definition of data constructor ‘HEq’
In the newtype declaration for ‘HEq’
|
10 | HEq
| ^^^...
```
so I suppose my question is, can we instantiate `Proxy` at a higher-rank kind? (#12045: `Proxy @FOO`)
```
>> type FOO = (forall xx. xx -> Type)
>> :kind (Proxy :: FOO -> Type)
<interactive>:1:2: error:
• Expected kind ‘FOO -> *’, but ‘Proxy’ has kind ‘k0 -> *’
• In the type ‘(Proxy :: FOO -> Type)’
```
It is possible to create a bespoke `Proxy`
```hs
type FOO = (forall x. x -> Type)
data BespokeProxy :: FOO -> Type where
BespokeProxy :: forall (c :: FOO). BespokeProxy c
newtype HEq :: forall j. j -> forall k. k -> Type where
HEq
:: (forall (x::forall xx. xx -> Type). BespokeProxy x -> x a -> x b)
-> HEq a b
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.1-beta1 |
| 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":"Higher-rank kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1-beta1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Taken from [https://github.com/ekmett/eq/blob/master/src/Data/Eq/Type/Hetero.hs#L73 Data.Eq.Type.Hetero].\r\n\r\n`(:==)` (called `HEq` to avoid unnecessary extensions) fails if you add a `Proxy x ->` argument.\r\n\r\n{{{#!hs\r\n{-# Language RankNTypes, KindSignatures, PolyKinds, GADTs, DataKinds #-}\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\nnewtype HEq :: forall j. j -> forall k. k -> Type where\r\n HEq\r\n :: (forall (x::forall xx. xx -> Type). Proxy x -> x a -> x b)\r\n -> HEq a b\r\n}}}\r\n{{{\r\n$ ~/code/latestghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 398.hs\r\nGHCi, version 8.7.20180828: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 398.hs, interpreted )\r\n\r\n398.hs:7:2: error:\r\n • A newtype constructor cannot have existential type variables\r\n HEq :: forall j k xx (a :: j) (b :: k).\r\n (forall (x :: forall xx1. xx1 -> *). Proxy x -> x a -> x b)\r\n -> HEq a b\r\n • In the definition of data constructor ‘HEq’\r\n In the newtype declaration for ‘HEq’\r\n |\r\n7 | HEq\r\n | ^^^...\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}\r\n\r\nIt compiles fine without `Proxy x ->`. Now my question is what existential type variable does `HEq` have, `-fprint-explicit-kinds` shows that `Proxy` is actually being instantiated at `(xx -> Type)` and not `(forall xx. xx -> Type)`\r\n\r\n{{{\r\n398.hs:10:2: error:\r\n • A newtype constructor cannot have existential type variables\r\n HEq :: forall j k xx (a :: j) (b :: k).\r\n (forall (x :: forall xx1. xx1 -> *).\r\n Proxy (xx -> *) (x xx) -> x j a -> x k b)\r\n -> HEq j a k b\r\n • In the definition of data constructor ‘HEq’\r\n In the newtype declaration for ‘HEq’\r\n |\r\n10 | HEq\r\n | ^^^...\r\n}}}\r\n\r\nso I suppose my question is, can we instantiate `Proxy` at a higher-rank kind? (#12045: `Proxy @FOO`)\r\n\r\n{{{\r\n>> type FOO = (forall xx. xx -> Type)\r\n>> :kind (Proxy :: FOO -> Type)\r\n\r\n<interactive>:1:2: error:\r\n • Expected kind ‘FOO -> *’, but ‘Proxy’ has kind ‘k0 -> *’\r\n • In the type ‘(Proxy :: FOO -> Type)’\r\n}}}\r\n\r\nIt is possible to create a bespoke `Proxy`\r\n\r\n{{{#!hs\r\ntype FOO = (forall x. x -> Type)\r\n\r\ndata BespokeProxy :: FOO -> Type where\r\n BespokeProxy :: forall (c :: FOO). BespokeProxy c\r\n\r\nnewtype HEq :: forall j. j -> forall k. k -> Type where\r\n HEq\r\n :: (forall (x::forall xx. xx -> Type). BespokeProxy x -> x a -> x b)\r\n -> HEq a b\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/13895"Illegal constraint in a type" error - is it fixable?2019-07-07T18:19:36ZRyan Scott"Illegal constraint in a type" error - is it fixable?I recently sketched out a solution to #13327. Here is the type signature that I wanted to write:
```hs
dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). k -> Type).
Typeable t
=> (forall d. Data d ...I recently sketched out a solution to #13327. Here is the type signature that I wanted to write:
```hs
dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). k -> Type).
Typeable t
=> (forall d. Data d => c (t d))
-> Maybe (c a)
```
But this doesn't typecheck:
```
• Could not deduce (Typeable (t k0))
from the context: (Data a, Typeable (t k))
bound by the type signature for:
dataCast1 :: forall a.
Data a =>
forall k (c :: * -> *) (t :: forall k1. k1 -> *).
Typeable (t k) =>
(forall d. Data d => c (t * d)) -> Maybe (c a)
at NewData.hs:(170,3)-(173,26)
The type variable ‘k0’ is ambiguous
• In the ambiguity check for ‘dataCast1’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the class method:
dataCast1 :: forall a.
Data a =>
forall k (c :: * -> *) (t :: forall k1. k1 -> *).
Typeable (t k) =>
(forall d. Data d => c (t * d)) -> Maybe (c a)
In the class declaration for ‘Data’
|
170 | dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). k -> Type).
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
This makes sense, since GHC has no way to conclude that the `k` in `t`'s kind is also `Typeable`. I tried to convince GHC of that fact:
```hs
dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). Typeable k => k -> Type).
Typeable t
=> (forall d. Data d => c (t d))
-> Maybe (c a)
```
But this also doesn't work:
```
NewData.hs:171:25: error:
• Illegal constraint in a type: Typeable k0
• In the first argument of ‘Typeable’, namely ‘t’
In the type signature:
dataCast1 :: forall (c :: Type -> Type)
(t :: forall (k :: Type). Typeable k => k -> Type).
Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
In the class declaration for ‘Data’
|
171 | Typeable t
| ^
NewData.hs:172:40: error:
• Illegal constraint in a type: Typeable k0
• In the first argument of ‘c’, namely ‘(t d)’
In the type signature:
dataCast1 :: forall (c :: Type -> Type)
(t :: forall (k :: Type). Typeable k => k -> Type).
Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
In the class declaration for ‘Data’
|
172 | => (forall d. Data d => c (t d))
| ^^^
```
At this point, I'm stuck, since I have no idea how to work around this `Illegal constraint in a type` error. This error message appears to have originated as a part of the `TypeInType` patch, since there's even a [test case](http://git.haskell.org/ghc.git/blob/58c781da4861faab11e4c5804e07e6892908ef72:/testsuite/tests/dependent/should_fail/PromotedClass.hs) checking for this behavior.
But is this a fundamental limitation of kind equalities? Or would it be possible to lift this restriction?
<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":"\"Illegal constraint in a type\" error - is it fixable?","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I recently sketched out a solution to #13327. Here is the type signature that I wanted to write:\r\n\r\n{{{#!hs\r\ndataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). k -> Type).\r\n Typeable t\r\n => (forall d. Data d => c (t d))\r\n -> Maybe (c a)\r\n}}}\r\n\r\nBut this doesn't typecheck:\r\n\r\n{{{\r\n • Could not deduce (Typeable (t k0))\r\n from the context: (Data a, Typeable (t k))\r\n bound by the type signature for:\r\n dataCast1 :: forall a.\r\n Data a =>\r\n forall k (c :: * -> *) (t :: forall k1. k1 -> *).\r\n Typeable (t k) =>\r\n (forall d. Data d => c (t * d)) -> Maybe (c a)\r\n at NewData.hs:(170,3)-(173,26)\r\n The type variable ‘k0’ is ambiguous\r\n • In the ambiguity check for ‘dataCast1’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n When checking the class method:\r\n dataCast1 :: forall a.\r\n Data a =>\r\n forall k (c :: * -> *) (t :: forall k1. k1 -> *).\r\n Typeable (t k) =>\r\n (forall d. Data d => c (t * d)) -> Maybe (c a)\r\n In the class declaration for ‘Data’\r\n |\r\n170 | dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). k -> Type).\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n}}}\r\n\r\nThis makes sense, since GHC has no way to conclude that the `k` in `t`'s kind is also `Typeable`. I tried to convince GHC of that fact:\r\n\r\n{{{#!hs\r\ndataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). Typeable k => k -> Type).\r\n Typeable t\r\n => (forall d. Data d => c (t d))\r\n -> Maybe (c a)\r\n}}}\r\n\r\nBut this also doesn't work:\r\n\r\n{{{\r\nNewData.hs:171:25: error:\r\n • Illegal constraint in a type: Typeable k0\r\n • In the first argument of ‘Typeable’, namely ‘t’\r\n In the type signature:\r\n dataCast1 :: forall (c :: Type -> Type)\r\n (t :: forall (k :: Type). Typeable k => k -> Type).\r\n Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)\r\n In the class declaration for ‘Data’\r\n |\r\n171 | Typeable t\r\n | ^\r\n\r\nNewData.hs:172:40: error:\r\n • Illegal constraint in a type: Typeable k0\r\n • In the first argument of ‘c’, namely ‘(t d)’\r\n In the type signature:\r\n dataCast1 :: forall (c :: Type -> Type)\r\n (t :: forall (k :: Type). Typeable k => k -> Type).\r\n Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)\r\n In the class declaration for ‘Data’\r\n |\r\n172 | => (forall d. Data d => c (t d))\r\n | ^^^\r\n}}}\r\n\r\nAt this point, I'm stuck, since I have no idea how to work around this `Illegal constraint in a type` error. This error message appears to have originated as a part of the `TypeInType` patch, since there's even a [http://git.haskell.org/ghc.git/blob/58c781da4861faab11e4c5804e07e6892908ef72:/testsuite/tests/dependent/should_fail/PromotedClass.hs test case] checking for this behavior.\r\n\r\nBut is this a fundamental limitation of kind equalities? Or would it be possible to lift this restriction?","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1