Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Register
  • Sign in
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
    • Locked files
  • Issues 5.5k
    • Issues 5.5k
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 634
    • Merge requests 634
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Artifacts
    • Schedules
    • Test cases
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Model experiments
  • Analytics
    • Analytics
    • 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
  • #15359

Quantified constraints do not work with equality constraints

Feeling abusive toward GHC this morning, I tried this:

class C a b

data Dict c where
  Dict :: c => Dict c

foo :: (forall a b. C a b => a ~ b) => Dict (C a b) -> a -> b
foo Dict x = x

I thought it wouldn't work, and I was right:

    • Class ‘~’ does not support user-specified instances
    • In the quantified constraint ‘forall (a :: k) (b :: k).
                                    C a b =>
                                    a ~ b’
      In the type signature:
        foo :: (forall a b. C a b => a ~ b) => Dict (C a b) -> a -> b

Good. But then I tried something more devious:

class C a b
class a ~ b => D a b

data Dict c where
  Dict :: c => Dict c

foo :: (forall a b. C a b => D a b) => Dict (C a b) -> a -> b
foo Dict x = x

This also fails, with Couldn't match expected type ‘b’ with actual type ‘a’.

I'm fine with the second case failing (because I think anything else would be very challenging), but the error message is unfortunate. According to the semantics of class constraints and quantified constraints, this case should be accepted. So if we reject it, we should have a good reason -- like we offer in the first case. Essentially, we need to explain that any logical entailment of an equality constraint simply doesn't hold in the presence of a quantified constraint. I neither know a good pithy way of explaining that to users nor how to detect when to do so.

Trac metadata
Trac field Value
Version 8.5
Type Bug
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