Fwd: Why do Constraint Tuple data constructors exist?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

Fwd: Why do Constraint Tuple data constructors exist?

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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Why do Constraint Tuple data constructors exist?

Edward Kmett-2
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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs