[Haskell-cafe] Injective type classes?

[Tom Smeding]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210330/984d4b59/attachment.html>