‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐ On Sunday, February 16, 2020 3:44 PM, Juan Casanova wrote:

Arjen,

Indeed, I think the fundamental point of disagreement is whether t ~ String is a valid potential unification or not. In general it is, but let me bring to you the following example that I put on the initial example on my Stack Overflow question:

aretheyreallyeq :: (Eq a, Eq b) => Either a b -> Either a b -> Bool

aretheyreallyeq (Left a1) (Right b2) = a1 == b2

This does not compile, and rightly so. Because a and b need not be equal, so it is not guaranteed that you will be able to use an Eq instance between them. In other words, within a function body, type variables in the definition of that function are not unifiable, they cannot be instantiated (within the function's body). There cannot be parts of the function's body whose potential outcome depends on what the type variables are instantiated to. Of course, and as the error message on my first example says itself, the thing is that it depends on the instantiation of t.

But here is the thing, and please evaluate this statement carefully as, if not entirely correct, it might be the entire source of the confusion:

A) There is no Class1 constraint on the function createBar. Therefore, the Class1 instance that the function uses is going to be fixed and will not vary on different calls of the function.

The type 't' will be determined by the calling context of createBar, and I do not see why it could not be String.

Sure, that instance may rely on other constraints of the function, for example. If there were other instances whose head matched but did not have matching constraints we would be in a different situation, and I understand why in those cases the overlapping errors are necessary: it is undecidable in general to solve the problem of transitive constraint satisfaction and therefore if the head matches, it is a potential overlap and that's the end of the story.

My apologies, I expected the compiler to complain about overlapping instances, even without anything other than the instance definitions. It turns out that it only starts complaining when the instances are used. I'm afraid it would appear that I don't really know how multiple-parameter classes and existential types influence the overlap checking as implemented in GHC.

But that is not what happens here. The head of the constraint will only match if t ~ String, but then the Class1 instance used within createBar would need to be variable for different type instantiations of createBar, which contradicts the statement A). Thus, the only sensible thing to do is to use the only instance that matches regardless of the instantiation of t.

I would expect that the type checker, when it cannot prove something in general, takes the safe approach of disallowing it. Whether your particular use of this class in your program might be proven to be correct, I really don't know, sorry.

And to circle back, as I said, this comes back to the fact that if you remove the instance that does not depend on the instantiation of t, then you suddenly get a compile error that says there are no instances. So the compiler itself knows that it cannot use an instance that depends on the instantiation of t, but still brings it up to flag an overlapping instances error.

I hope that clarifies at the very least what the core of the disagreement is. It is quite possible that there is something I am overlooking, but until you provide me with an example of code that, if the compiler worked the way I want it to, would have an ambiguous instance, or an ambiguous implementation of some function at all, I'll still believe that the compiler is flagging up the overlapping instances error too soon without really checking whether they are really valid instances.

kind regards, Arjen

Please keep the discussion coming. The fact that I'm not convinced (for now) doesn't mean I don't appreciate your answers. I wouldn't want to come out as hostile. I'd be very happy for you to convince me that I am understanding something the wrong way and learn how to do what I want in the right way, which is what has happened essentially every time I had a similar issue like this one. But until I am convinced please allow me to argue back.

Didn't Arjen already provide such an example? Should `g "Hello"` return a `Left` or a `Right`?

g :: String -> Either String String g x = foo x

The g you are defining there should not compile indeed, because that is an ambiguous usage of foo. But that is not what I defined. And this relates to the rest of your reply.

I think the difficulty may be due to the error being flagged in a misleading way. There's nothing wrong with your intended usage of the type classes, individually. The problem is that the instances both exist in the same codebase. The error message about overlap *appears* at the use sites but I believe that this is an implementation detail.

The instances you have written can cause problems in *other* parts of the codebase, perhaps completely unrelated parts that have merely transitively imported your module through dependencies (someone may define `g` above, for example). Thefore the instances should not be both allowed to exist in the same codebase. This particular piece of information is flagged at the use sites but perhaps should be flagged at the instance definition sites.

I simply do not agree with this, and I don't think (?) that GHCi implementors and designers agree with you either, as exemplified by the fact that indeed overlapping instances appear when using instances and not when defining them. While it doesn't clearly agree with what I said, the general phrasing and approach followed here: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts... makes me think indeed the approach is that potentially overlapping instances are allowed so long as each of their uses are unambiguous. To address your point more specifically, you worry that if potentially overlapping instances exist, then someone somewhere else in the codebase might flag up the overlapping instances error. But in order for someone to do so, they need to *use* an instance of the class that has the potentially overlapping instances. In your example, they need to implement g and use foo within its definition, which means that they are willfully utilizing a Class1 instance that they are thinking of. If there are potentially overlapping instances that match, then they need to take care that they use the one they really want. Now, it is true that a good argument is that, for example in the g example you presented, it is quite hard for the implementor to actually indicate which instance they wish to use, since in this case type annotations will not do the job. This is a problem I have also had to deal with myself, and generally solve on a case by case basis with various tricks and hacks (normally involving wrapping things in newtypes). In my application case for this problem we are discussing now, the newtype wrapping would in principle work, but would make my code extremely more complicated due to the amount of type classes that use each other that I am considering here and the fact that they are multi-parameter type classes. All in all I am not very happy anytime the solution to trying to do something legitimate is "wrap everything up in newtypes and coerce stuff all over the place until it works". I think it is too rampant and clutters the code way too much. Perhaps the fact that no tools are given in GHCi to explicitly indicate which instance we wish to use is an argument in favour of your perspective that instances should not overlap even on their definition? Maybe someone reading this who's more closely situated to the Haskell / GHCi development and design principles could throw some light on this? I don't feel like it is made clear on any of the documentation I've read, but I may have overlooked it. Rest assured, if it is like this by design as you claim it may be, I would have a big amount of complaints about that as well. Things that are absolutely sensible to do that would be made very noticeably harder to do by this design decision. But it would certainly address this particular issue. Juan. -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.

On Sun, Feb 16, 2020 at 03:46:25PM +0000, Juan Casanova wrote:

This may be an argument in favour of your notion, that any kind of overlap is wrong by definition and it just so happens that it only flags up when used. I'd still love some comment from someone with a bit more authority about this.

This is an area where an expert language designer needs to chime in I think and they don't tend to hang out on haskell-cafe. If you are trying to solve a practical problem, then based on the discussion so far I am around 90% confident that you would be better off without using typeclasses at all. How would your design look if you just passed around first class values instead? Tom

On Sun, Feb 16, 2020 at 03:39:24PM +0000, Juan Casanova wrote:

I simply do not agree with this, and I don't think (?) that GHCi implementors and designers agree with you either, as exemplified by the fact that indeed overlapping instances appear when using instances and not when defining them. While it doesn't clearly agree with what I said, the general phrasing and approach followed here: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts... makes me think indeed the approach is that potentially overlapping instances are allowed so long as each of their uses are unambiguous.

And yet the particular overlapping instances leave room for unexpected results. For example, if the code is specialized a bit to impose "Eq a" and "Typeable b, Eq b" constaints on "Bar", and one implements a heterogenous comparison function for "Bar", not quite the right thing happens: {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ExistentialQuantification #-} module Main (main) where import Data.Typeable (Typeable, cast) class Class1 a b where foo :: a -> b instance {-# INCOHERENT #-} Monoid a => Class1 a (Either b a) where foo x = Right (x <> x) instance {-# INCOHERENT #-} Monoid a => Class1 a (Either a b) where foo x = Left x data Bar a = Dir a | forall b. (Typeable b, Eq b, Class1 b a) => FromB b instance Eq a => Eq (Bar a) where (Dir x) == (Dir y) = x == y (FromB x) == (FromB y) = case cast x of Just x' -> x' == y _ -> False _ == _ = False getA :: Bar a -> a getA (Dir a) = a getA (FromB b) = foo b createBar :: Eq t => Bar (Either String t) createBar = FromB "abc" createBar2 :: Eq t => Bar (Either t String) createBar2 = FromB "abc" main :: IO () main = do let x = createBar :: Bar (Either String String) y = createBar2 :: Bar (Either String String) print $ map getA [x, y] print $ x == y If your run the above, the output you get is: [Left "abc",Right "abcabc"] True Which shows some of the trouble one can run into with incoherent definitions. Structurally equal terms are no longer equivalent. -- Viktor.

On Feb 16, 2020, at 2:37 PM, Juan Casanova wrote:

I'm not that familiar with Typeable. If I understand correctly, what is going on here is that by pattern-matching on the FromB constructor and using Typeable, you are bypassing the instance checking and comparing two things that should not be compared. Is this a more or less correct understanding?

Somewhat, but "should not be compared" is not how I see it. I prefer types in which structural equivalence is equivalence. Types that violate this cannot be handled generically. Typeable allows one to ask whether two terms of a-priori distinct (polymorphic) types are in fact of the same actual type, and if so, for example, "cast" one to the other: cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b The type-safe cast operation In your example (jazzed up with Typeable and some Eq constraints) however, it is possible to construct two terms, both of the *same* type: Bar (Either String String), constructor "FromB" and data "abc", which are not in fact equivalent because they're bound to different instances of Class1. The different instance bindings are not apparent in the types of the terms or their data, so the reflection machinery fails tell them apart, and yet they're not the same. This is best avoided IMHO. -- -- Viktor.