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 <g9ks1...@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
>
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
