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,869
    • Issues 4,869
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 456
    • Merge requests 456
  • 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
  • #18873
Closed
Open
Created Oct 21, 2020 by Richard Eisenberg@raeDeveloper

Quantified equality constraints are not used for rewriting

If I say

type family F a b where
  F [_] b = b

f :: forall a b. (a ~ [b]) => F a b -> b
f x = x

GHC smiles upon me: the equality constraint rewrites a to [b], and then F [b] b can reduce to b, and all is well.

But if I say

type family F a b where
  F [_] b = b

class Truth
instance Truth

f :: forall a b. (Truth => a ~ [b]) => F a b -> b
f x = x

I get an error, saying F a b does not match b. This is because the equality, hidden behind Truth, is not used for rewriting, and thus GHC cannot figure out that F a b can reduce.

I don't see an easy solution here.

This isn't just me grousing: a problem on !4149 (closed) could be worked around if GHC used such equalities for rewriting. And so if we can solve this problem, we can solve the other one. My expectation is that we won't solve this one, though.

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