Ambiguity check and type families

[Wolfgang Jeltsch]

Hi,

the following (contrived) code is accepted by GHC 7.8.3, but not 7.10.1:

> {-# LANGUAGE TypeFamilies #-}
> 
> type family F a :: *
> 
> type family G b :: *
> 
> x :: G (F a) ~ a => F a
> x = undefined

GHC 7.10.1 reports:

> Could not deduce (F a0 ~ F a)
> from the context (G (F a) ~ a)
>   bound by the type signature for x :: (G (F a) ~ a) => F a
>   at Test.hs:7:6-23
> NB: ‘F’ is a type function, and may not be injective
> The type variable ‘a0’ is ambiguous
> In the ambiguity check for the type signature for ‘x’:
>   x :: forall a. (G (F a) ~ a) => F a
> To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
> In the type signature for ‘x’: x :: G (F a) ~ a => F a

At a first look, this complaint seems reasonable, and I have already
wondered why GHC 7.8.3 actually accepts the above code.

>From an intuitive standpoint, however, the code seems actually
acceptable to me. While it is true that type families are generally not
injective, it is possible to derive the type a from F a by applying G.

It would great if this code would be accepted by GHC again and if there
was a workaround to make it work with GHC 7.10.1. At the moment, this
change in the type checker from 7.8.3 to 7.10.1 breaks the
incremental-computing package in a rather fundamental way.

All the best,
Wolfgang