Skip to content

GitLab

  • Menu
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 4,868
    • Issues 4,868
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 458
    • Merge requests 458
  • 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 Compiler
  • GHCGHC
  • Issues
  • #17674
Closed
Open
Created Jan 13, 2020 by Richard Eisenberg@raeDeveloper

Kill EQ1

Note [Respecting definitional equality] introduces invariant EQ1:

  (EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable
        cast is one that relates either a FunTy to a FunTy or a
        ForAllTy to a ForAllTy.

This invariant is a small pain to uphold. And perhaps we don't need to. If, instead, we modified eqType to look at the kind of arguments to AppTys, then we wouldn't need EQ1, significantly simplifying mkAppTy. (Actually, it will just remove 2 lines. But it removes two calls to decomposePiCos. This will allow the one remaining call to this function to have more sway in the design of decomposePiCos, simplifying that bit of code, as well.)

Another nice benefit: by removing this invariant, we have an opportunity to explore different solutions to #17644, which hit a dead end in EQ1. See #17644 (comment 245757).

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking