Fwd: Why do Constraint Tuple data constructors exist?

Joe Crayne oh.hello.joe at gmail.com
Tue Sep 17 16:15:22 UTC 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

Then I decided that (ForEach c (Replicate n x)) is a constraint tuple and
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

Searching GHC source, I cannot find where or how constraint data
are used and notes on commit ffc21506894c7887d3620423aaf86bc6113a1071 were
helpful to me either.  Why do constraint tuple data constructor names exist
all if we cannot use them for anything?  Is it possible for a plugin to
the (ForEach c (Replicate n x)) constraint by some other means?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20190917/3a0529ba/attachment.html>

More information about the ghc-devs mailing list