Fwd: Why do Constraint Tuple data constructors exist?

17 Sep 2019

      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?

Fwd: Why do Constraint Tuple data constructors exist?

Joe Crayne