New restrictions to open type families

Hi, Looking at the ticket [1] and a draft paper linked there [2] , I learned that in GHC 7.8, two type family instances are considered overlapping if the argument lists unify in the presence of infinite types. My question is, why is this restriction necessary? A footnote in the paper states that it was not possible with GHC 7.6 to actually exploit the inconsistency. Would it be difficult to solve the problem by making this behaviour part of the specification, rather than accepting fewer programs? [1] http://ghc.haskell.org/trac/ghc/ticket/8154 [2] http://www.cis.upenn.edu/~eir/papers/2014/axioms/axioms-extended.pdf Regards, Takano Akio