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,249
    • Issues 4,249
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 391
    • Merge Requests 391
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Security & Compliance
    • Security & Compliance
    • Dependency List
    • License Compliance
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #15635

Closed
Open
Opened Sep 12, 2018 by David Feuer@treeowlReporter

Implication introduction for quantified constraints

Now that we have QuantifiedConstraints, it seems we need some implication introduction form. The constraints package has these types:

data Dict a where
  Dict :: a => Dict a

newtype a :- b = Sub (a => Dict b)

QuantifiedConstraints suggests another version of :-:

newtype Imp a b = Imp
  { unImp :: forall r. ((a => b) => r) -> r}

We can write

fromImp :: Imp a b -> a :- b
fromImp (Imp f) = Sub (f Dict)

But ... there's no way to go the other way!

Let's try it:

toImp :: a :- Dict b -> a :- b
toImp (Sub ab) = Imp $ \r -> _

We get

* Found hole: _ :: r
* Relevant bindings include
    r :: (a => b) => r
    ab :: a => Dict b

There's no way to put these things together. But there's no terribly obvious reason they ''can't* be combined. a => b is a function from an a dictionary to a b dictionary. a => Dict b is a function from an a dictionary to a value that *contains'' a b dictionary. We just need some way to plumb these things together: some sort of implication introduction. The simplest thing might be a bit of magic:

implIntro
  :: ((a => b) => q)
  -> (forall r. (b => r) -> (a => r))
  -> q

In Core (modulo type abstraction and application), we could simply write

implIntro f g = f (g id)

Unfortunately, I doubt that implIntro is really general enough to do everything people will want in this space.

Trac metadata
Trac field Value
Version 8.6.1-beta1
Type FeatureRequest
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
Assignee
Assign to
8.6.1
Milestone
8.6.1 (Past due)
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#15635