Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • 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,829
    • Issues 4,829
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 445
    • Merge requests 445
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
    • Value stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #15757

Closed
Open
Created Oct 17, 2018 by Ningning Xie@ningning

Coercion Variable Almost Devoid Checking in ForAllCo

In Richard's thesis Section 5.8.5.2, there is a restriction on where a coercion variable can appear in ForAllCo for the sake of consistency: the coercion variable can appear nowhere except in coherence coercions.

Currently this restriction is missing in coercion quantification (see #15497 (closed)). The goal of this ticket is to add the missing restriction.

After discussion with Richard, we restate the restriction a little bit: the coercion variable can appear nowhere except in GRefl and Refl. Allowing it to appear in Refl should not break consistency.

Notice that this also means liftCoSubst might fail when it lifts a ForAllTy over a coercion variable to a ForAllCo.

Trac metadata
Trac field Value
Version
Type Task
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking