#15635 closed feature request (duplicate)

Implication introduction for quantified constraints

Reported by: dfeuer Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.6.1-beta1
Keywords: QuantifiedConstraints Cc: Bj0rn
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #14937 Differential Rev(s):
Wiki Page:


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:

  :: ((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.

Change History (3)

comment:1 Changed 10 months ago by Bj0rn

This is the same as #14937.

comment:2 Changed 10 months ago by Bj0rn

Cc: Bj0rn added

comment:3 Changed 10 months ago by dfeuer

Resolution: duplicate
Status: newclosed
Note: See TracTickets for help on using tickets.