Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,249
    • Issues 5,249
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 578
    • Merge requests 578
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #16371
Closed
Open
Issue created Feb 27, 2019 by Ryan Scott@RyanGlScottMaintainer

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
Edited May 31, 2020 by Ryan Scott
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking