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,242
    • Issues 5,242
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 567
    • Merge requests 567
  • 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
  • #14198
Closed
Open
Issue created Sep 08, 2017 by Ryan Scott@RyanGlScottMaintainer

Inconsistent treatment of implicitly bound kind variables as free-floating

(Spun off from the discussion starting at https://phabricator.haskell.org/D3872#109927.)

This program is accepted:

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}

import Data.Proxy

data Foo = MkFoo (forall a. Proxy a)

There's something interesting going on here, however. Because PolyKinds is enabled, the kind of a is generalized to k. But where does k get quantified? It turns out that it's implicitly quantified as an existential type variable to MkFoo:

λ> :i Foo
data Foo = forall k. MkFoo (forall (a :: k). Proxy a)

This was brought up some time ago in #7873 (closed), where the conclusion was to keep this behavior. But it's strange becuase the k is existential, so the definition is probably unusable.

But to make things stranger, it you write out the kind of a explicitly:

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}

import Data.Proxy

data Foo2 = MkFoo2 (forall (a :: k). Proxy a)

Then GHC will reject it:

Bug.hs:7:1: error:
    Kind variable ‘k’ is implicitly bound in data type
    ‘Foo2’, but does not appear as the kind of any
    of its type variables. Perhaps you meant
    to bind it (with TypeInType) explicitly somewhere?
  |
7 | data Foo2 = MkFoo2 (forall (a :: k). Proxy a)
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

So GHC's treatment is inconsistent. What should GHC do? We could:

  1. Have both be an error.

  2. Have both be accepted, and implicitly quantify k as an existential type variable

  3. Have both be accepted, and implicitly quantify k in the forall itself. That is:

    MkFoo :: (forall {k} (a :: k). Proxy k a) -> Foo
  4. Something else. When you try a similar trick with type synonyms:

    {-# LANGUAGE ExistentialQuantification #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    
    import Data.Proxy
    
    type Foo3 = forall a. Proxy a

    Instead of generalizing the kind of a, its kind will default to Any:

    λ> :i Foo3
    type Foo3 = forall (a :: GHC.Types.Any). Proxy a

    Would that be an appropriate trick for data types as well?

Edited Apr 03, 2019 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