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