id summary reporter owner description type status priority milestone component version resolution keywords cc os architecture failure testcase blockedby blocking related differential wikipage
15635 Implication introduction for quantified constraints dfeuer "Now that we have `QuantifiedConstraints`, it seems we need some implication introduction form. The `constraints` package has these types:
{{{#!hs
data Dict a where
Dict :: a => Dict a
newtype a :- b = Sub (a => Dict b)
}}}
`QuantifiedConstraints` suggests another version of `:-`:
{{{#!hs
newtype Imp a b = Imp
{ unImp :: forall r. ((a => b) => r) -> r}
}}}
We can write
{{{#!hs
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:
{{{#!hs
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:
{{{#!hs
implIntro
:: ((a => b) => q)
-> (forall r. (b => r) -> (a => r))
-> q
}}}
In Core (modulo type abstraction and application), we could simply write
{{{#!hs
implIntro f g = f (g id)
}}}
Unfortunately, I doubt that `implIntro` is really general enough to do everything people will want in this space." feature request closed normal 8.6.1 Compiler 8.6.1-beta1 duplicate QuantifiedConstraints Bj0rn Unknown/Multiple Unknown/Multiple None/Unknown #14937