ghc derives different type signature for equal functions with overlapping instances

[int-e]

Insert "This flag does not change ghc's behaviour when no verlapping instances are present." after "The -fallow-overlapping-instances lag instructs GHC to allow more than one instance to match, provided here is a most specific one." in http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#instance-overlap

(old description follows for reference)

The code below derives two different type signatures for the same function in two different modules.

One of these modules defines a new instance for the Monad class. What's interesting is that this causes the type checker to derive a more general type than before. I think that's a bug.

Another interesting point is that the code below works without -fallow-overlapping-instances, but if the instances from A.hs and from B.hs are combined in a single file, the compiler complains very loudly. The derived types are unaffected by -fallow-overlapping-instances.

==> A.hs <==
{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
module A (MaybeT (..), module Control.Monad) where

import Control.Monad

newtype MaybeT m a = MaybeT {runMaybeT :: m (Maybe a)}

instance Monad m => Monad (MaybeT m)

==> B.hs <==
{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
module B (qqq) where

import A

data Foo a = Foo

instance Monad (MaybeT Foo) where

qqq _ = runMaybeT (runMaybeT (return 1) >> return 2)

==> C.hs <==
{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
module C (rrr) where

import A

rrr _ = runMaybeT (runMaybeT (return 1) >> return 2)

==> D.hs <==
module D (qqq, rrr) where

import B
import C

{-
# ghci -fallow-overlapping-instances D.hs
GHCi, version 6.7.20070716: http://www.haskell.org/ghc/  :? for help
(...)
Ok, modules loaded: C, D, A, B.
*D> :t qqq
qqq :: (Monad (A.MaybeT m), Num t1) => t -> m (Maybe t1)
*D> :t rrr
rrr :: (Monad m, Num t1) => t -> m (Maybe t1)
*D> :i MaybeT
newtype MaybeT m a = MaybeT {runMaybeT :: m (Maybe a)}
        -- Defined at A.hs:6:8-13
instance [overlap ok] (Monad m) => Monad (MaybeT m)
  -- Defined at A.hs:8:0-35
-}

I think that the type derived for qqq is correct in the presence of overlapping instances.

[simonpj]

The rules for instance overlap are described here: http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#instance-overlap

When compiling B.hs, GHC sees that there is an overlapping instance and so refrains from simplifying the constraint Monad (A.MaybeT m), becuase m might be instantiated to Foo. But when compiling C.hs, it sees no such overlap, so it simplifies the constraint. It doesn't see the overlap because B is not in the transitive imports of C.

That's why you get different types. To get the same types, we'd have to refrain from ever using an instance declaration in case it was later overlapped, and that seems impractical becuase it would percolate all constraints up to main.

In short, this seems to be the documented behaviour. But the documentation may not be adequately clear. If you can suggest concrete improvements (E.g. Add ".." after "...") then that would be v helpful. Thanks.

Simon

[int-e]

Thank you.

The connection that I hadn't made is that type inference (in particular, choosing an instance to use for type classes for a monotype) and constraint simplification (which affects polymorphic types) are really the same thing.

Once that misconception is resolved the behaviour is just as expected. The documentation could be clearer about the fact that allowing overlapping instances does not change the behaviour for the case when none are present though.

Maybe inserting "This flag does not change ghc's behaviour when no overlapping instances are present." after "The -fallow-overlapping-instances flag instructs GHC to allow more than one instance to match, provided there is a most specific one." would clear that up?

Bertram

[simonpj]

Looking at it again, I this would be better to add this after "without complaining about the problem of subsequent instantiations":

Notice that we gave a type signature to f so GHC had to check that f has the specified type. Suppose instead we do not give a type signature, asking GHC to infer it instead. In this case, GHC will refrain from simplifying the constraint C Int [Int] (for the same reason as before) but, rather than rejecting the program, it will infer the type

  f :: C Int b => [b] -> [b]

That postpones the question of which instance to pick to the call site for f by which time more is known about the type b

[int-e]

I forgot to follow up on this last week. Your proposed change sounds good to me, it addresses exactly the problem that I had.

[simonpj]

OK, I've committed the documentation fix, and am closing the bug. Thanks for your help.

Simon