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.html#instance-overlap
> 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.