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 565
    • Merge requests 565
  • 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
  • #7961
Closed
Open
Issue created Jun 05, 2013 by danharaj@trac-danharaj

Remove restrictions on promoting GADT's

(Also allow the promotion of data types whose kind is not (* -> ... -> *))

I have been using -XDataKinds lately to explore the sorts of dependently typed programming that are currently possible in GHC. I am particularly interested in DSL's and embedding other languages' type systems into Haskell so that GHC can help verify the correctness of the program fragments I construct for those languages. From my point of view as an end-user, the restrictions on what data get promoted is inconsistent and oftentimes annoying to deal with. There are two related issues on my end:

  1. The restriction that a data type cannot have a kind mentioning a promoted kind means that the way I stratify my type machinery impacts whether or not GHC will promote everything as I would like.
  2. The inability to use promoted GADT's forces me to encode relationships between my type building blocks in trickier ways, and sometimes I am simply unable to come up with an alternative.

I have found that these issues get in my way as a programmer of modest skill. Oftentimes I will explore a particular design but be forced to abandon it because my "natural" line of reasoning runs into GHC's restrictions. With sufficient cleverness you can do quite a lot of impressive stuff with the current system, but I am often not sufficiently clever nor am I equipped to determine when something is outright impossible.

Lifting these restriction, from my point of view, would simplify the machinery a great deal and allow me to do type-level programming that is currently out of my reach. It would make the kind extensions more uniform and more complete to us end-users. #6024 (closed) would complete them in another way.

Edited Mar 09, 2019 by Simon Peyton Jones
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking