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
(,) :: Constraint -> Constraint -> Constraint.
With UndecidableInstances, etc. you can fabricate a class like
class (a,b) => a & b
instance (a,b) => a & b
and then use (&) partially applied, and modulo a little bit of plumbing on
the backend.
Maybe this would be enough to unblock you?
-Edward
On Tue, Sep 17, 2019 at 9:15 AM Joe Crayne
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? _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs