Why do Constraint Tuple data constructors exist?
Edward Kmett
ekmett at gmail.com
Tue Sep 17 18:13:03 UTC 2019
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 <oh.hello.joe at gmail.com> 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
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20190917/9833c5a4/attachment.html>
More information about the ghc-devs
mailing list