diff options
| author | Richard Eisenberg <eir@cis.upenn.edu> | 2013-08-02 10:51:35 +0100 |
|---|---|---|
| committer | Richard Eisenberg <eir@cis.upenn.edu> | 2013-08-02 11:33:00 +0100 |
| commit | bd0ab6c2b478aea308ec405a3c24d0068bb96569 (patch) | |
| tree | e951a647179ac2638ace832d2f6266aa95c966e8 /docs/core-spec | |
| parent | abb3a9faa88fad3562ac41a148dd683765f47565 (diff) | |
| download | haskell-bd0ab6c2b478aea308ec405a3c24d0068bb96569.tar.gz | |
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.
Diffstat (limited to 'docs/core-spec')
| -rw-r--r-- | docs/core-spec/core-spec.mng | 14 | ||||
| -rw-r--r-- | docs/core-spec/core-spec.pdf | bin | 347921 -> 349150 bytes |
2 files changed, 9 insertions, 5 deletions
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng index 40560df1ec..246be067fc 100644 --- a/docs/core-spec/core-spec.mng +++ b/docs/core-spec/core-spec.mng @@ -29,7 +29,7 @@ System FC, as implemented in GHC\footnote{This document was originally prepared by Richard Eisenberg (\texttt{eir@cis.upenn.edu}), but it should be maintained by anyone who edits the functions or data structures mentioned in this file. Please feel free to contact Richard for more information.}\\ -\Large 8 July, 2013 +\Large 2 August, 2013 \end{center} \section{Introduction} @@ -339,10 +339,14 @@ check for compatibility here. \ottdefncheckXXnoXXconflict{} -The judgment $[[apart]]$ checks to see whether two lists of types are surely apart. -It checks to see if \coderef{types/Unify.lhs}{tcApartTys} returns \texttt{SurelyApart}. -Two types are apart if neither type is a type family application and if they do not -unify. +The judgment $[[apart]]$ checks to see whether two lists of types are surely +apart. $[[apart( </ ti // i />, </ si // i /> )]]$, where $[[ </ ti // i /> +]]$ is a list of types and $[[ </ si // i /> ]]$ is a list of type +\emph{patterns} (as in a type family equation), first flattens the $[[ </ ti + // i /> ]]$ using \coderef{types/FamInstEnv.lhs}{flattenTys} and then checks to +see if \coderef{types/Unify.lhs}{tcUnifyTysFG} returns \texttt{SurelyApart}. +Flattening takes all type family applications and replaces them with fresh variables, +taking care to map identical type family applications to the same fresh variable. The algorithm $[[unify]]$ is implemented in \coderef{types/Unify.lhs}{tcUnifyTys}. It performs a standard unification, returning a substitution upon success. diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf Binary files differindex 11f52d6476..180d9bed78 100644 --- a/docs/core-spec/core-spec.pdf +++ b/docs/core-spec/core-spec.pdf |