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,256
    • Issues 5,256
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 563
    • Merge requests 563
  • 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
  • #18875
Closed
Open
Issue created Oct 22, 2020 by Richard Eisenberg@raeDeveloper

Occurs-check-y Givens rewrite once, but not twice

GHC remarkably accepts this program:

type family UnMaybe a where
  UnMaybe (Maybe b) = b

class C c where
  meth :: c

instance C (Maybe d) where
  meth = Nothing

f :: (e ~ Maybe (UnMaybe e)) => e
f = meth

This is remarkable because satisfying the C e constraint arising from the use of meth requires using the e ~ Maybe (UnMaybe e) given, despite the fact that it has an occurs-check failure. That is, GHC must rewrite e to Maybe (UnMaybe e) to solve the class constraint, yet not fall into a look trying to expand e further. This works due to the way GHC currently uses flattening-skolems to deal with type family applications. (The program above does not work on the current tip of !4149 (closed), which avoids this flattening mechanism.)

However, GHC rejects this program:

type family G a b where
  G (Maybe c) d = d

h :: (e ~ Maybe (G e f)) => e -> f
h (Just x) = x

Here, h has a similar given with an occurs-check failure. In contrast to the first example, though, we need to use the equation twice in order to accept this program. Specifically, we have

[G] e ~ Maybe (G e f)
[W] e ~ Maybe f

Using the Given for rewriting once gives us

[W] Maybe (G e f) ~ Maybe f

which decomposes to

[W] G e f ~ f

But now, we must use the given again to get

[W] G (Maybe (G e f)) f ~ f

so that can reduce to

[W] f ~ f

and be solved.

I think this will be hard to achieve in practice (rewriting twice). Might we need even more rewrites in pathological scenarios? I don't know.

The purpose of this ticket is more to record the incompleteness than to actively agitate for a solution. This did not arise in a real application and would likely be hard to fix.

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