forall in constraint

[Li-yao Xia]

Hi Alan,

One way is to define a new typeclass.


type ImplicitBndrs c x thing
   = (c (XIB x thing), c (XNewImplicitBndrs x thing))

class ForallImplicitBndrs c x where
   withImplicitBndrs
     :: forall thing. (ImplicitBndrs c x thing => t) -> t


Although that requires you to write one instance for every combination 
of (c, x).
The "universal instance" of ImplicitBndrs can also be wrapped in the 
Dict type in the constraints library. In fact, constraints has an even 
more general mechanism for all of this in Data.Constraint.Forall. Pro: 
no extra instances are necessary, so it is more easily extensible. Con: 
internally relies heavily on unsafeCoerce, although the above is already 
stretching the language a lot.

We start by defining a "class synonym" instead of a type synonym, to 
enable partial application.


class (c (XIB x thing), c (XNewImplicitBndrs x thing))
   => ImplicitBndrs c x thing
instance (c (XIB x thing), c (XNewImplicitBndrs x thing))
   => ImplicitBndrs c x thing


-- "forall thing. ImplicitBndrs c x thing"
type ForallImplicitBndrs c x = Forall (ImplicitBndrs c x)

withImplicitBndrs
   :: forall c x thing
   .  ForallImplicitBndrs c x
   => (ImplicitBndrs c x thing => t) -> t
withImplicitBndrs t = case inst @(ImplicitBndrs c x) @thing of
   Sub Dict -> t


I think the ICFP paper "Quantified class constraints" talks about a more 
principled future solution, and there is an old GHC ticket or two about it.

Cheers,
Li-yao


On 10/23/2017 11:06 AM, Alan & Kim Zimmerman wrote:
> I am working on the Trees that Grow stuff, and hit a small problem
> 
> I have
> 
> type family XIB               x thing
> type family XNewImplicitBndrs x thing
> 
> type ForallXImplicitBndrs (c :: * -> Constraint) (x :: *) (thing :: *) =
>         ( c (XIB               x thing)
>         , c (XNewImplicitBndrs x thing)
>         )
> 
> and I want to extend the DataId constraint
> 
> type DataId p =
>    ( Data p
> 
>    , ForallXImplicitBndrs Data p thing
>    )
> 
> But the problem is I do not have `thing` at this point, and to get it in
> the code will involve some hs-boot nastiness.
> 
> Is there any way to require "forall thing. Data thing" inside the DataId
> constraint?
> 
> Alan
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20171023/77c963b5/attachment.html>
>