Hi,

that's an interesting example. To me this looks like a bug in GHC, although the issue is certainly a bit subtle.

The reason I think it is a bug is that, if we name all the type functions in the signature and apply improvements using the fact that we are working with functions, then we get:

x :: (F a ~ b, G b ~ a) => b

x = undefined

Now, this should be equivalent, and it is quite clear that there is no ambiguity here, as the `b` determines the `a` via the `G`. Interestingly, GHC accepts the program in this form. Also, if you ask it for the type of `x` using `:t` (which means instantiate the type and the generalize it again), we get another equivalent formulation: `x :: (F (G b) ~ b) => b`, which is also accepted by GHC.

-Iavor

On Tue, Jun 2, 2015 at 9:28 AM, Wolfgang Jeltsch <g9ks157k@acme.softbase.org> wrote:

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

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users