Why do Constraint Tuple data constructors exist?

[Edward Kmett]

I'm not sure if this is directly relevant to your issues around
GHC.Classes.(%,%), but there are some issues with using tuples for
Constraints. Namely that they can only be fully applied, and do not exist
naked as

(,) :: Constraint -> Constraint -> Constraint.

With UndecidableInstances, etc. you can fabricate a class like

class (a,b) => a & b
instance (a,b) => a & b

and then use (&) partially applied, and modulo a little bit of plumbing on
the backend.

Maybe this would be enough to unblock you?

-Edward

On Tue, Sep 17, 2019 at 9:15 AM Joe Crayne <oh.hello.joe at gmail.com> wrote:

> My question arrised in the following context:
>
> ```
> module ForEachHelper where
>
> import Data.Kind
> import GHC.TypeLits
>
> type family ForEach (c :: k -> Constraint) (xs :: [k]) :: Constraint where
>     ForEach c '[] = ()
>     ForEach c (x:xs) = (c x, ForEach c xs)
>
> type family Replicate n x where
>     Replicate 0 x = '[]
>     Replicate n x = x : Replicate (n-1) x
>
> data ForEachHelper n c x where
>     ForEachHelper :: ForEach c (Replicate n x) => ForEachHelper n c x
>
> -- The following solve function was actually in another module from the
> definitions above:
>
> solve :: ( KnownNat n, c x
>          -- Solved via plugin:
>          -- , ForEach c (Replicate n x)
>          ) => p c -> q x -> ForEachHelper n c x
> solve pc px = ForEachHelper
> ```
>
> I was trying to write a plugin that could solve the (ForEach c (Replicate
> n x)) constraint.
> I need an EvTerm that this constraint.  The first thing I tried was to use
> the given EvTerm
> for the (c x) constraint without change.  This causes the program to
> compile but ultimately
> and, perhaps not surprisingly, it segfaults when code relies upon the
> constraint.
>
> Then I decided that (ForEach c (Replicate n x)) is a constraint tuple and
> the
> proof term should be a tuple constructed using a constraint tuple data
> constructor.  However, this is apparently not possible.  When I tried the
> following code in the initialization of my plugin:
>
>     cpairCon <- tcLookupDataCon (cTupleDataConName 2)
>
> it triggers an error:
>
>     Can't find interface-file declaration for data constructor
> GHC.Classes.(%,%)
>
> Searching GHC source, I cannot find where or how constraint data
> constructors
> are used and notes on commit ffc21506894c7887d3620423aaf86bc6113a1071 were
> not
> helpful to me either.  Why do constraint tuple data constructor names
> exist at
> all if we cannot use them for anything?  Is it possible for a plugin to
> solve
> the (ForEach c (Replicate n x)) constraint by some other means?
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20190917/9833c5a4/attachment.html>