#7804: Ambiguity check too eager in presence of RankNTypes and TypeFamilies --------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Component: Compiler Version: 7.7 | Keywords: AmbiguityCheck Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC rejects valid program | Blockedby: Blocking: | Related: --------------------------------------+------------------------------------- The following code compiles in 7.6.1 but not in 7.7: {{{ {-# LANGUAGE TypeFamilies, RankNTypes #-} type family F f a type family G f data Proxy a = P sDFMap :: (forall a. Proxy f -> Proxy a -> Proxy (F f a)) -> Proxy (G f) sDFMap _ = P }}} Here is the error message: {{{ Couldn't match type `G f0' with `G f' NB: `G' is a type function, and may not be injective The type variable `f0' is ambiguous Expected type: (forall a. Proxy f -> Proxy a -> Proxy (F f a)) -> Proxy (G f) Actual type: (forall a. Proxy f0 -> Proxy a -> Proxy (F f0 a)) -> Proxy (G f0) In the ambiguity check for: forall f. (forall a. Proxy f -> Proxy a -> Proxy (F f a)) -> Proxy (G f) In the type signature for `sDFMap': sDFMap :: (forall a. Proxy f -> Proxy a -> Proxy (F f a)) -> Proxy (G f) }}} It is true that {{{sDFMap}}} is ''sometimes'' ambiguous, but it is not ''always'' ambiguous. For example, if we have {{{ foo :: Proxy Bool -> Proxy a -> Proxy (F Bool a) foo _ _ = P bar = sDFMap foo }}} the call to {{{sDFMap}}} is well defined, with {{{f ~ Bool}}}. If the type signature for {{{foo}}} did not specify the value of {{{f}}}, the call to {{{sDFMap}}} would indeed be ambiguous and should be rejected. GHC 7.6.1 does catch the error when the type of {{{foo}}} uses a variable instead of {{{Bool}}}. -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7804 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler