Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,384
    • Issues 4,384
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 372
    • Merge Requests 372
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #16684

Closed
Open
Opened May 22, 2019 by Iavor S. Diatchki@yavDeveloper

Relax local equality check

Consider the following example:

{-# Language RankNTypes, TypeFamilies #-}
  
type family F a

q :: (forall b. (F b ~ Int) => (a,b)) -> ()
q _ = ()

Currently GHC rejects this program as ambiguous. The reason is that during the ambiguity check, GHC needs to solve a constraint of the form:

forall a. forall b. (F b ~ Int) => (a ~ alpha)

where alpha is a unification variable corresponding to the type parameter of q when used. At present, this constraint cannot be solved, as the local assumption F B ~ Int causes alpha to be untouchable. In general, this is the safe thing to do, as in the presence of local assumptions unifying alpha with a might not be the most general solution (and, in fact, there may be no most general solution).

However, in this case it seems that the current rules are bit too conservative: the local assumption cannot affect the goal in any way, so q is not really ambiguous, and perhaps we can relax the current restrictions a bit. @simonpj proposed the following possible refinements [1]:

  • (A) An implication is considered to “bind local equalities” iff it has at least one given equality whose free variables are not all bound by the same implication.

That loosens up Note [Let-bound skolems] in TcSMonad, perhaps significantly. In particular, it woudl accept the example above.

The same email [1] proposed a second possiblity, (B), but it looks dodgy. So this ticket is about implementing (A).

References:

  • [1] https://mail.haskell.org/pipermail/ghc-devs/2019-May/017669.html
  • [2] Note [Let-bound skolems] in TcSMonad
Edited May 23, 2019 by Simon Peyton Jones
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#16684