Why cannot inferred type signatures restrict (potentially) ambiguous type variables?

[adam vogt]

Hello,

I have code:

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

class C a b where c :: a -> b
instance (int ~ Integer) => C Integer int where c = (+1)

c2 :: forall a b c. (C a b, C b c) => a -> c
c2 x = c (c x :: b)
c2 x = c ((c :: a -> b) x)


Why are the type signatures needed? If I leave all of them off, I get:

    Could not deduce (C a1 a0)
      arising from the ambiguity check for ‛c2’
    from the context (C a b, C a1 a)
      bound by the inferred type for ‛c2’: (C a b, C a1 a) => a1 -> b

from the line: c2 x = c (c x)


>From my perspective, it seems that the type signature ghc infers
should be able to restrict the ambiguous types as the hand-written
signature does.

These concerns apply to HEAD (using -XAllowAmbiguousTypes) and ghc-7.6 too.

Regards,
Adam