<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>