GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20190707T18:03:41Zhttps://gitlab.haskell.org/ghc/ghc//issues/15628Higherrank kinds20190707T18:03:41ZIcelandjackHigherrank 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, 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/ghcstage2 interactive ignoredotghci 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, `fprintexplicitkinds` 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 higherrank 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.1beta1 
 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":"Higherrank kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1beta1","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/ghcstage2 interactive ignoredotghci 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, `fprintexplicitkinds` 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 higherrank 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":[]} >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/ghcstage2 interactive ignoredotghci 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, `fprintexplicitkinds` 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 higherrank 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.1beta1 
 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":"Higherrank kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1beta1","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/ghcstage2 interactive ignoredotghci 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, `fprintexplicitkinds` 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 higherrank 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?20190707T18: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 => 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":[]} >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