#8020: Closed type families break substitution -------------------------------------+------------------------------------ Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by eir@…): commit bd0ab6c2b478aea308ec405a3c24d0068bb96569 {{{ Author: Richard Eisenberg <eir@cis.upenn.edu> Date: Fri Aug 2 10:51:35 2013 +0100 Fix Trac #8020. The solution is to use a different notion of apartness. See http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f /axioms-extended.pdf for the gory details. Some comments are also in Notes [Compatibility] and [Apartness] in FamInstEnv. compiler/coreSyn/TrieMap.lhs | 11 +++- compiler/ghc.mk | 2 +- compiler/types/FamInstEnv.lhs | 136 ++++++++++++++++++++++++++++++++++++-- compiler/types/OptCoercion.lhs | 15 +++-- compiler/types/Unify.lhs | 143 +++++++++++----------------------------- docs/core-spec/core-spec.mng | 14 ++-- docs/core-spec/core-spec.pdf | Bin 347921 -> 349150 bytes 7 files changed, 197 insertions(+), 124 deletions(-) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8020#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler