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

Reply via email to