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 <[email protected]> wrote: > 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 > [email protected] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
