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,263
    • Issues 5,263
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 567
    • Merge requests 567
  • 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
  • #17719
Closed
Open
Issue created Jan 20, 2020 by Richard Eisenberg@raeDeveloper

Note [Do not add duplicate quantified instances] is simplistic, causing rejection of programs

Copied wholesale from !2283 (comment 242042):

Consider

{-# LANGUAGE QuantifiedConstraints, ConstraintKinds,
             ExistentialQuantification #-}

module Bug where

class C1 a

class (forall z. C1 z) => C2 y
class (forall y. C2 y) => C3 x

data Dict c = c => Dict

foo :: (C2 a, C3 a) => a -> Dict (C1 a)
foo _ = Dict

Amazingly, with either C2 a or C3 a, foo is accepted. But with both, it is rejected.

The problem is that, after eagerly expanding superclasses of quantified constraints (that's the new bit), we end up with

[G] g1 :: forall z. C1 z     -- from the C2 a constraint
[G] g2 :: forall y z. C1 z   -- from the C3 a constraint

So when we want to solve C1 a, we don't know which quantified constraint to use, and so we stop. (Also strange: g2 is quantified over the unused y. It's clear where this comes from, and it seems harmless, but it's a bit strange. This detail is not salient. It is not the reason we're struggling here.) This has been seen before, in another guise: #15244 (closed). And we have

{- Note [Do not add duplicate quantified instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this (#15244):

  f :: (C g, D g) => ....
  class S g => C g where ...
  class S g => D g where ...
  class (forall a. Eq a => Eq (g a)) => S g where ...

Then in f's RHS there are two identical quantified constraints
available, one via the superclasses of C and one via the superclasses
of D.  The two are identical, and it seems wrong to reject the program
because of that. But without doing duplicate-elimination we will have
two matching QCInsts when we try to solve constraints arising from f's
RHS.

The simplest thing is simply to eliminate duplicates, which we do here.
-}

which is duly implemented. However, here, we don't have duplicates -- we have near-duplicates, which are not caught by the simple (tcEqType) check.

I wonder if the way forward is to really try to "solve" quantified instances. That is, before labeling them inert, we try to interact them with inerts. Then, we might discover that one constraint is implied by another, which will get rid of this problem (and replace that Note).

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