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 |