Hey Tom,

there is a paper "Bidirectional type class instances" [1] about a similar concept.

However, the approach is not implemented in GHC. At the moment, the dictionary for 'C (a, b)' does not explicitly include a dictionary for C a and C b. It is only implicitly referenced in the implementation of C's class methods.
For it to be explicitly available for further usage, the dictionary data type for classes of C would have to be extended by an argument. This is not trivial and is discussed in the mentioned paper.

The discussion at the GHC proposal show some alternative approaches how something like this can be achieved with the current GHC (e.g. [2]).

Best,
Kai

[1] https://dl.acm.org/doi/abs/10.1145/3331545.3342596
[2] https://github.com/ghc-proposals/ghc-proposals/pull/284#issuecomment-542322728

Hi Cafe,

With this class definition with this instance:

    class C a where

    instance C b => C (a, b)

GHC can of course infer, given 'C b', that 'C (a, b)'. This is nothing more

than the meaning of the instance declaration above.

However, GHC cannot infer the inverse:

    {-# LANGUAGE FlexibleContexts #-}

    foo :: C a => a -> Int

    foo = undefined

    bar1 :: C (a, b) => a -> b -> Int

    bar1 _ = foo

This gives an error on the right-hand side of 'bar1': "Could not deduce (C b)

arising from a use of ‘foo’; from the context: C (a, b)". The same happens in

similar cases:

    {-# LANGUAGE GADTs #-}

    bar2 :: (C p, p ~ (a, b)) => a -> b -> Int

    bar2 _ = foo

    data Thing a where

        Tup :: a -> b -> Thing (a, b)

    bar3 :: C a => Thing a -> Int

    bar3 (Tup x y) = foo y

Both these usages of 'foo' yield the same error.

My use-case is 'bar3', where I would like GHC to determine that the call to

'foo' is valid. (I don't actually care directly about bar1 and bar2.)

Is there a way to make 'bar3' compile?

Note that:

- In my actual use case, 'C' is of course not empty.

- In my actual use case, my type class instances _are_ in fact injective, even

  though I do enable FlexibleInstances to be able to write e.g.

  'instance C (T a Int)'.

- Above, the dictionary for 'C (a, b)' includes a dictionary for 'C b', doesn't

  it? So if inference can resolve 'C b', then the compilation to Core can find

  the right dictionary, I think? (Not sure about this part.)

Thanks a lot for your help.

Cheers,

Tom

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.