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,246
    • Issues 5,246
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 562
    • Merge requests 562
  • 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
  • #17368
Closed
Open
Issue created Oct 16, 2019 by Richard Eisenberg@raeDeveloper

Implement homogeneous equality

As observed in two papers, the primitive equality type in GHC can be made homogeneous. This is both a simplification over the status quo (heterogeneous equality) and an important step toward implementing dependent types.

This ticket is to track this change.

Step 1: Modify the type-checker to use predicates instead of types internally. This will essentially be a glorification of PredTree (renamed Pred), and a CtEvidence will now store a Pred, not a PredType.

See also https://gitlab.haskell.org/ghc/ghc/wikis/dependent-haskell/phase2, which has much discussion.

Edited Oct 16, 2019 by Richard Eisenberg
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking