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