
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 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