<div dir="ltr">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 <br><br>(,) :: Constraint -> Constraint -> Constraint.<br><br>With UndecidableInstances, etc. you can fabricate a class like<div><br></div><div>class (a,b) => a & b<br>instance (a,b) => a & b<br><br>and then use (&) partially applied, and modulo a little bit of plumbing on the backend.<br><br>Maybe this would be enough to unblock you?</div><div><br></div><div>-Edward</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Sep 17, 2019 at 9:15 AM Joe Crayne <<a href="mailto:oh.hello.joe@gmail.com">oh.hello.joe@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">My question arrised in the following context:<br><div class="gmail_quote"><div dir="ltr"><br>```<br>module ForEachHelper where<br><br>import Data.Kind<br>import GHC.TypeLits<br><br>type family ForEach (c :: k -> Constraint) (xs :: [k]) :: Constraint where<br>    ForEach c '[] = ()<br>    ForEach c (x:xs) = (c x, ForEach c xs)<br><br>type family Replicate n x where<br>    Replicate 0 x = '[]<br>    Replicate n x = x : Replicate (n-1) x<br><br>data ForEachHelper n c x where<br>    ForEachHelper :: ForEach c (Replicate n x) => ForEachHelper n c x<br><br>-- The following solve function was actually in another module from the definitions above:<br><br>solve :: ( KnownNat n, c x<br>         -- Solved via plugin:<br>         -- , ForEach c (Replicate n x)<br>         ) => p c -> q x -> ForEachHelper n c x<br>solve pc px = ForEachHelper<br>```<br><br>I was trying to write a plugin that could solve the (ForEach c (Replicate n x)) constraint.<br>I need an EvTerm that this constraint.  The first thing I tried was to use the given EvTerm<br>for the (c x) constraint without change.  This causes the program to compile but ultimately<br>and, perhaps not surprisingly, it segfaults when code relies upon the constraint.<br><br>Then I decided that (ForEach c (Replicate n x)) is a constraint tuple and the<br>proof term should be a tuple constructed using a constraint tuple data<br>constructor.  However, this is apparently not possible.  When I tried the<br>following code in the initialization of my plugin:<br><br>    cpairCon <- tcLookupDataCon (cTupleDataConName 2)<br><br>it triggers an error:<br><br>    Can't find interface-file declaration for data constructor GHC.Classes.(%,%)<br><br>Searching GHC source, I cannot find where or how constraint data constructors<br>are used and notes on commit ffc21506894c7887d3620423aaf86bc6113a1071 were not<br>helpful to me either.  Why do constraint tuple data constructor names exist at<br>all if we cannot use them for anything?  Is it possible for a plugin to solve<br>the (ForEach c (Replicate n x)) constraint by some other means?<br></div>
</div></div>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>