regression in handling of type variables in constraints on instances which do not appear in the instance head

ghc-7.7.20130720 (from here http://darcs.haskell.org/ghcBuilder/uploads/igloo-m/) rejects instances which work with ghc-7.6.2.

{-# LANGUAGE FlexibleInstances, ImplicitParams, MultiParamTypeClasses, ScopedTypeVariables, TypeFamilies, UndecidableInstances #-}

class Fun f a b where
    fun :: f -> a -> b

instance (b ~ Int, a ~ Int) => Fun F a b
    where fun _ = (+1)

data F = F

data Compose a b = Compose a b

-- ghc-7.6 version
instance (Fun f b c, Fun g a b) => Fun (Compose f g) a c where
    fun (Compose f g) a = fun f (fun g a :: b)

{- | ghc >= 7.7 accepts this second instance, which is an ugly workaround
>>> fun (Compose F F) 2
4

unsatisfactory ghc-77 workaround:

>>> let ?b = undefined in fun (Compose F F) 2
4

-}
instance (Fun f b c, Fun g a b, ?b :: b) => Fun (Compose f g) a c where
    fun (Compose f g) a = fun f (fun g a `asTypeOf` ?b)

Trac metadata

Trac field	Value
Version	7.7
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

If it helps, the error with ghc-7.7 is:

inf.hs:26:10: Warning:
    Could not deduce (Fun g a b0)
      arising from the ambiguity check for an instance declaration
    from the context (Fun f b c, Fun g a b)
      bound by an instance declaration:
                 (Fun f b c, Fun g a b) => Fun (Compose f g) a c
      at inf.hs:26:10-56
    The type variable ‛b0’ is ambiguous
    In the ambiguity check for:
      forall f g a c b. (Fun f b c, Fun g a b) => Fun (Compose f g) a c
    In the instance declaration for ‛Fun (Compose f g) a c’
Ok, modules loaded: Main.

Attached file inf2.hs ($916).

explicitly computing argument/result types with a type family

While Compose may not be so interesting, the same thing prevents HList from having both a single class for polymorphic functions (Fun above) and having higher-order functions that work for some instances of that class (ones like F).

Some faking can be done by having some associated types for Fun to calculate the argument from the result type etc. But that is uglier (see attached inf2).

closed

I found -XAllowAmbiguousTypes, added by commit 97db0edc, which allows the old behavior.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedInvalid

mentioned in issue #8392 (closed)

reopened

Though my head goes a little swimmy when I look at this for too long, I think the ambiguity checker in 7.7 is being overeager here. I can use the Compose instance for Fun without any type annotations, so therefore, its type is not ambiguous. It seems that the equality constraints on the F instance induce what are effectively functional dependencies. Once we know that the first parameter to Fun is F, we know that the next two must be Int.

I'm still a little lost as to how to characterize this behavior, and I could understand an argument saying that the ambiguity checker should reject this code. But, we should then also admit that the ambiguity checker is somewhat liberal, rejecting more than is necessary.

Trac metadata

Trac field	Value
Resolution	ResolvedInvalid → Unresolved

goldfire, you're asking for a message `suggested fix: -XAllowAmbiguousTypes'? The reasoning for rejecting the Compose f g instance by default makes sense here.

No, not quite. I think that, given that uses of the Compose instance work just fine without extra annotations, then that means that the instance is not ambiguous, tautologically by my operating definition of "ambiguous". So, I think we need to choose between these two design alternatives:

1. Permit the instance for Compose without -XAllowAmbiguousTypes.
2. Admit that the ambiguity checker is over-eager and sometimes rejects code that is unambiguous.

Or, I suppose

1. Define ambiguous differently.

It's possible that I'm very confused about something here, so if that's the case, please try to enlighten me!

Consider:

f :: Num a => Int -> Int 
f = blah

instance Num a => C Int where blah

Both cases, calling f or using the instance, will give rise to an ambiguous constraint Num a. So both are rejected in the same way.

But functions with an ambiguous times may sometimes be callable. Eg

class C a b where ...

f :: C a b => a -> Int 
f = blah

instance C a b => Eq [a] where blah

The type of f is ambiguous, in the sense that if we said

g :: C a b => a -> Int   -- Identical
g = f

type checking would fail even. But at certain types, typechecking might succeed. Example

instance C Char b where blah
foo = f 'x'

The -XAllowAmbiguousTypes flag therefore tells GHC to accept f's type even if it's ambiguous.

Thus, GHC's definition of "ambiguous" is "over-eager" in the sense that the function can be called at some types, although perhaps not at others. Hence the flag.

I don't know a less-eager-but-still-useful definition.

Certainly, I got lots of Trac tickets before saying "I had a definition f=e; I got ghci to tell me its type; I pasted in that type as a type signature for f, and it didn't typecheck". That was because the inferred type was ambiguous.

Same with instance decls. The error message now says

T8390.hs:14:10:
    Could not deduce (Fun g a b0)
      arising from the ambiguity check for an instance declaration
    from the context (Fun f b c, Fun g a b)
      bound by an instance declaration:
                 (Fun f b c, Fun g a b) => Fun (Compose f g) a c
      at T8390.hs:14:10-56
    The type variable ‛b0’ is ambiguous
    In the ambiguity check for:
      forall f g a c b. (Fun f b c, Fun g a b) => Fun (Compose f g) a c
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    In the instance declaration for ‛Fun (Compose f g) a c’

and adding -XAllowAmbiguousTypes makes it go through.

OK?

Simon

closed

That is option 3, above, fixing my definition of ambiguous.

Yes, OK. Many thanks.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedInvalid

added Pnormal label