GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20200123T19:42:31Zhttps://gitlab.haskell.org/ghc/ghc//issues/17072Dependent quantification prevents unification20200123T19:42:31ZVladislav ZavialovDependent quantification prevents unification## Summary
Replacing `k > Type` with `forall (a :: k) > Type` in a kind of a type constructor should not have any effect. The latter gives a name to the variable, but is otherwise equivalent... or so I thought.
Consider these definitions:
```
data B1 :: k > Type
type family F1 :: k > Type where
F1 = B1
```
GHC happily accepts them, unifying the kinds of `B1` and `F1`. However, if I make use of dependent quantification in `B` but not in `F`:
```
data B2 :: forall (a :: k) > Type
type family F2 :: k > Type where
F2 = B2
```
... GHC gets confused:
```
• Expected kind ‘k1 > Type’,
but ‘B2’ has kind ‘forall (a :: k0) > Type’
• In the type ‘B2’
In the type family declaration for ‘F2’

14  F2 = B2
 ^^
```
## Steps to reproduce
Load this in GHCi:
```
{# LANGUAGE PolyKinds, TypeFamilies, RankNTypes #}
module T where
import Data.Kind (Type)
data B1 :: k > Type
type family F1 :: k > Type where
F1 = B1
data B2 :: forall (a :: k) > Type
type family F2 :: k > Type where
F2 = B2
```
## Expected behavior
Both `F1` and `F2` should be accepted.
## Environment
* GHC version used: HEAD## Summary
Replacing `k > Type` with `forall (a :: k) > Type` in a kind of a type constructor should not have any effect. The latter gives a name to the variable, but is otherwise equivalent... or so I thought.
Consider these definitions:
```
data B1 :: k > Type
type family F1 :: k > Type where
F1 = B1
```
GHC happily accepts them, unifying the kinds of `B1` and `F1`. However, if I make use of dependent quantification in `B` but not in `F`:
```
data B2 :: forall (a :: k) > Type
type family F2 :: k > Type where
F2 = B2
```
... GHC gets confused:
```
• Expected kind ‘k1 > Type’,
but ‘B2’ has kind ‘forall (a :: k0) > Type’
• In the type ‘B2’
In the type family declaration for ‘F2’

14  F2 = B2
 ^^
```
## Steps to reproduce
Load this in GHCi:
```
{# LANGUAGE PolyKinds, TypeFamilies, RankNTypes #}
module T where
import Data.Kind (Type)
data B1 :: k > Type
type family F1 :: k > Type where
F1 = B1
data B2 :: forall (a :: k) > Type
type family F2 :: k > Type where
F2 = B2
```
## Expected behavior
Both `F1` and `F2` should be accepted.
## Environment
* GHC version used: HEADVladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc//issues/16371GHC should be more forgiving with visible dependent quantification in visible...20201109T15:26:20ZRyan ScottGHC should be more forgiving with visible dependent quantification in visible type applicationsGHC HEAD currently rejects the following code:
```hs
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
module Bug where
import Data.Kind
import Data.Proxy
f :: forall k (a :: k). Proxy a
f = Proxy
g :: forall (a :: forall x > x > Type). Proxy a
g = f @(forall x > x > Type) @a
```
```
GHCi, version 8.9.20190227: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:14:6: error:
• Illegal visible, dependent quantification in the type of a term:
forall x > x > *
(GHC does not yet support this)
• In the type signature:
g :: forall (a :: forall x > x > Type). Proxy a

14  g :: forall (a :: forall x > x > Type). Proxy a
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This test is implemented in `TcValidity.vdqAllowed`.
But GHC is being too conservative here. `forall x > x > *` _isn't_ the type of a term here, but rather the kind of a type variable, and it's perfectly admissible to use visible dependent quantification in such a scenario.
The immediate reason that this happens is because of this code:
```hs
vdqAllowed (TypeAppCtxt {}) = False
```
Unfortunately, fixing this bug isn't as simply as changing `False` to `True`. If you do that, then GHC becomes _too_ forgiving and allows things like this:
```hs
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeApplications #}
lol :: forall a. a
lol = undefined
t2 = lol @(forall a > a > a)
```
Here, visible dependent quantification is leaking into the type of a term, which we definitely don't want to happen.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.9 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC should be more forgiving with visible dependent quantification in visible type applications","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.9","keywords":["VisibleDependentQuantification"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC HEAD currently rejects the following code:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ImpredicativeTypes #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\nf :: forall k a. Proxy a\r\nf = Proxy\r\n\r\ng :: forall (a :: forall x > x > Type). Proxy a\r\ng = f @(forall x > x > Type) @a\r\n}}}\r\n{{{\r\nGHCi, version 8.9.20190227: https://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:14:6: error:\r\n • Illegal visible, dependent quantification in the type of a term:\r\n forall x > x > *\r\n (GHC does not yet support this)\r\n • In the type signature:\r\n g :: forall (a :: forall x > x > Type). Proxy a\r\n \r\n14  g :: forall (a :: forall x > x > Type). Proxy a\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nBut GHC is being too conservative here. `forall x > x > *` //isn't// the type of a term here, but rather the kind of a type variable, and it's perfectly admissible to use visible dependent quantification in such a scenario.\r\n\r\nThe immediate reason that this happens is because of this code:\r\n\r\n{{{#!hs\r\nvdqAllowed (TypeAppCtxt {}) = False\r\n}}}\r\n\r\nUnfortunately, fixing this bug isn't as simply as changing `False` to `True`. If you do that, then GHC becomes //too// forgiving and allows things like this:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ImpredicativeTypes #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeApplications #}\r\n\r\nlol :: forall a. a\r\nlol = undefined\r\n\r\nt2 = lol @(forall a > a > a)\r\n}}}\r\n\r\nHere, visible dependent quantification is leaking into the type of a term, which we definitely don't want to happen.","type_of_failure":"OtherFailure","blocking":[]} >GHC HEAD currently rejects the following code:
```hs
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
module Bug where
import Data.Kind
import Data.Proxy
f :: forall k (a :: k). Proxy a
f = Proxy
g :: forall (a :: forall x > x > Type). Proxy a
g = f @(forall x > x > Type) @a
```
```
GHCi, version 8.9.20190227: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:14:6: error:
• Illegal visible, dependent quantification in the type of a term:
forall x > x > *
(GHC does not yet support this)
• In the type signature:
g :: forall (a :: forall x > x > Type). Proxy a

14  g :: forall (a :: forall x > x > Type). Proxy a
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This test is implemented in `TcValidity.vdqAllowed`.
But GHC is being too conservative here. `forall x > x > *` _isn't_ the type of a term here, but rather the kind of a type variable, and it's perfectly admissible to use visible dependent quantification in such a scenario.
The immediate reason that this happens is because of this code:
```hs
vdqAllowed (TypeAppCtxt {}) = False
```
Unfortunately, fixing this bug isn't as simply as changing `False` to `True`. If you do that, then GHC becomes _too_ forgiving and allows things like this:
```hs
{# LANGUAGE ImpredicativeTypes #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE TypeApplications #}
lol :: forall a. a
lol = undefined
t2 = lol @(forall a > a > a)
```
Here, visible dependent quantification is leaking into the type of a term, which we definitely don't want to happen.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.9 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"GHC should be more forgiving with visible dependent quantification in visible type applications","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.9","keywords":["VisibleDependentQuantification"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC HEAD currently rejects the following code:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ImpredicativeTypes #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\nf :: forall k a. Proxy a\r\nf = Proxy\r\n\r\ng :: forall (a :: forall x > x > Type). Proxy a\r\ng = f @(forall x > x > Type) @a\r\n}}}\r\n{{{\r\nGHCi, version 8.9.20190227: https://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:14:6: error:\r\n • Illegal visible, dependent quantification in the type of a term:\r\n forall x > x > *\r\n (GHC does not yet support this)\r\n • In the type signature:\r\n g :: forall (a :: forall x > x > Type). Proxy a\r\n \r\n14  g :: forall (a :: forall x > x > Type). Proxy a\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nBut GHC is being too conservative here. `forall x > x > *` //isn't// the type of a term here, but rather the kind of a type variable, and it's perfectly admissible to use visible dependent quantification in such a scenario.\r\n\r\nThe immediate reason that this happens is because of this code:\r\n\r\n{{{#!hs\r\nvdqAllowed (TypeAppCtxt {}) = False\r\n}}}\r\n\r\nUnfortunately, fixing this bug isn't as simply as changing `False` to `True`. If you do that, then GHC becomes //too// forgiving and allows things like this:\r\n\r\n{{{#!hs\r\n{# LANGUAGE ImpredicativeTypes #}\r\n{# LANGUAGE PolyKinds #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE TypeApplications #}\r\n\r\nlol :: forall a. a\r\nlol = undefined\r\n\r\nt2 = lol @(forall a > a > a)\r\n}}}\r\n\r\nHere, visible dependent quantification is leaking into the type of a term, which we definitely don't want to happen.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/14419Check kinds for ambiguity20200621T12:03:16ZRichard Eisenbergrae@richarde.devCheck kinds for ambiguityGHC does an ambiguity check on types. It should also do the same for kinds. Here is a program that should be rejected:
```hs
type family F a
data T :: F a > Type
```
`T`'s kind is ambiguous, and any occurrence of `T` will be rejected. Instead of rejecting usage sites, let's just reject the definition site.
This check would be disabled by `AllowAmbiguousTypes`.
Happily, I think the implementation should be easy, and that the current algorithm to check for ambiguous types should work for kinds, too. After all, types and kinds are the same these days.
This was inspired by #14203, but no need to read that ticket to understand this one.
EDIT: See [ticket:14419\#comment:160844](https://gitlab.haskell.org//ghc/ghc/issues/14419#note_160844) and [ticket:14419\#comment:163265](https://gitlab.haskell.org//ghc/ghc/issues/14419#note_163265) for the nub of what needs to be done here.GHC does an ambiguity check on types. It should also do the same for kinds. Here is a program that should be rejected:
```hs
type family F a
data T :: F a > Type
```
`T`'s kind is ambiguous, and any occurrence of `T` will be rejected. Instead of rejecting usage sites, let's just reject the definition site.
This check would be disabled by `AllowAmbiguousTypes`.
Happily, I think the implementation should be easy, and that the current algorithm to check for ambiguous types should work for kinds, too. After all, types and kinds are the same these days.
This was inspired by #14203, but no need to read that ticket to understand this one.
EDIT: See [ticket:14419\#comment:160844](https://gitlab.haskell.org//ghc/ghc/issues/14419#note_160844) and [ticket:14419\#comment:163265](https://gitlab.haskell.org//ghc/ghc/issues/14419#note_163265) for the nub of what needs to be done here.https://gitlab.haskell.org/ghc/ghc//issues/13408Consider inferring a higherrank kind for type synonyms20200925T17:22:29ZRichard Eisenbergrae@richarde.devConsider inferring a higherrank kind for type synonymsIn terms, a definition comprising one nonrecursive equation may have a higherrank type inferred. For example:
```hs
f :: (forall a. a > a > a) > Int
f z = z 0 1
g = f
```
`g` gets an inferred type equal to `f`'s. However, this fails at the type level:
```hs
type F (z :: forall a. a > a > a) = z 0 1
type G = F
```
If anything is strange here, it's that the termlevel definition is accepted. GHC should not be in the business of inferring higherrank types. But there is an exception for definitions comprising one nonrecursive equation.
This ticket proposes expanding this behavior to the type level, allowing `G` to be accepted.
This is spun off from #13399, but is not tightly coupled to that ticket.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Consider inferring a higherrank kind for type synonyms","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"In terms, a definition comprising one nonrecursive equation may have a higherrank type inferred. For example:\r\n\r\n{{{#!hs\r\nf :: (forall a. a > a > a) > Int\r\nf z = z 0 1\r\n\r\ng = f\r\n}}}\r\n\r\n`g` gets an inferred type equal to `f`'s. However, this fails at the type level:\r\n\r\n{{{#!hs\r\ntype F (z :: forall a. a > a > a) = z 0 1\r\n\r\ntype G = F\r\n}}}\r\n\r\nIf anything is strange here, it's that the termlevel definition is accepted. GHC should not be in the business of inferring higherrank types. But there is an exception for definitions comprising one nonrecursive equation.\r\n\r\nThis ticket proposes expanding this behavior to the type level, allowing `G` to be accepted.\r\n\r\nThis is spun off from #13399, but is not tightly coupled to that ticket.","type_of_failure":"OtherFailure","blocking":[]} >In terms, a definition comprising one nonrecursive equation may have a higherrank type inferred. For example:
```hs
f :: (forall a. a > a > a) > Int
f z = z 0 1
g = f
```
`g` gets an inferred type equal to `f`'s. However, this fails at the type level:
```hs
type F (z :: forall a. a > a > a) = z 0 1
type G = F
```
If anything is strange here, it's that the termlevel definition is accepted. GHC should not be in the business of inferring higherrank types. But there is an exception for definitions comprising one nonrecursive equation.
This ticket proposes expanding this behavior to the type level, allowing `G` to be accepted.
This is spun off from #13399, but is not tightly coupled to that ticket.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.1 
 Type  FeatureRequest 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Consider inferring a higherrank kind for type synonyms","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"In terms, a definition comprising one nonrecursive equation may have a higherrank type inferred. For example:\r\n\r\n{{{#!hs\r\nf :: (forall a. a > a > a) > Int\r\nf z = z 0 1\r\n\r\ng = f\r\n}}}\r\n\r\n`g` gets an inferred type equal to `f`'s. However, this fails at the type level:\r\n\r\n{{{#!hs\r\ntype F (z :: forall a. a > a > a) = z 0 1\r\n\r\ntype G = F\r\n}}}\r\n\r\nIf anything is strange here, it's that the termlevel definition is accepted. GHC should not be in the business of inferring higherrank types. But there is an exception for definitions comprising one nonrecursive equation.\r\n\r\nThis ticket proposes expanding this behavior to the type level, allowing `G` to be accepted.\r\n\r\nThis is spun off from #13399, but is not tightly coupled to that ticket.","type_of_failure":"OtherFailure","blocking":[]} >