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
El Tue, Mar 30, 2021 at 07:27:11AM +0000, Tom Smeding escribió:
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:
Because the inverse doesn't need to hold. A priori, nothing prevents the existence of (a, b) instances where b isn't an instance. For example, if Ord a and Ord b hold, then Ord (a, b) holds, but not the opposite. If, for example, you have Ord a but not Ord b, you can make (a, b) an instance of Ord by simply defining (a1, b1) `compare` (a2, b2) = a1 `compare` a2. Best, Antonio
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-5423227... On 30.03.21 09:27, Tom Smeding wrote:
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.
Hi Kai,
Thanks for the links! Your [2] is a workaround that works perfectly for my purposes. I had already considered using an associated type, but that puts the GHC type checker into an infinite loop... Using a separate type family fixes my issue.
Cheers,
Tom
‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐
On Tuesday, March 30, 2021 10:01 AM, Kai-Oliver Prott
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-5423227...
On 30.03.21 09:27, Tom Smeding wrote:
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.
On Tue, 30 Mar 2021, Tom Smeding wrote:
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.)
How shall GHC find the method implementations for 'b' if it only has the methods for '(a,b)'?
On Tuesday, March 30, 2021 4:36 PM, Henning Thielemann
On Tue, 30 Mar 2021, Tom Smeding wrote:
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.)
How shall GHC find the method implementations for 'b' if it only has the methods for '(a,b)'?
Because the instance for '(a,b)' includes a type class constraint for 'b', I expected that the relevant dictionary (which is surely needed for implementing the methods contained in the dictionary for '(a,b)') would be available. However, I understand from a sibling post that this dictionary for 'b' is only contained in the closures for the methods in the dictionary for '(a,b)', and GHC cannot easily access that. In any case, I have a workaround, as I posted in a reply to Kai's email. Nevertheless, thanks for the help! :) Cheers, Tom
participants (4)
-
Antonio Regidor Garcia -
Henning Thielemann -
Kai-Oliver Prott -
Tom Smeding