Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,262
    • Issues 4,262
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 419
    • Merge Requests 419
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Security & Compliance
    • Security & Compliance
    • Dependency List
    • License Compliance
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #13399

Closed
Open
Opened Mar 09, 2017 by Eric Crockett@crockeeaReporter

Location of `forall` matters with higher-rank kind polymorphism

The following code fails to compile, but probably should:

{-# LANGUAGE RankNTypes, TypeInType #-}

import Data.Kind

data Foo :: forall k . (* -> *) -> k -> * -- Decl 1

class C (a :: forall k . k -> *)

instance C (Foo a) -- error on this line

with the error

• Expected kind ‘forall k. k -> *’, but ‘Foo a’ has kind ‘k0 -> *’
• In the first argument of ‘C’, namely ‘Foo a’
  In the instance declaration for ‘C (Foo a)’

Similarly, the following declarations of Foo also cause a similar error at the instance declaration:

Decl 2: data Foo :: (* -> *) -> k -> *

Decl 3: data Foo (a :: * -> *) (b :: k)

However, if I move the forall to a point after the first type parameter (which is where the instance is partially applied) thusly:

Decl 4: data Foo :: (* -> *) -> forall k . k -> *

then GHC happily accepts the instance of C.

From my (admittedly negligible) knowledge of type theory, the signatures for Decls 1 and 4 (and 2) are identical, since the forall can be floated to the front of Decl 4. GHC should accept any of the four versions of Foo, since they are all equivalent.

Edited Mar 10, 2019 by Ben Gamari
Assignee
Assign to
8.4.1
Milestone
8.4.1 (Past due)
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#13399