GHC should be more forgiving with visible dependent quantification in visible type applications
GHC HEAD currently rejects the following code:
{-# 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:
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:
{-# 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.
Trac metadata
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 |