[commit: ghc] master: Private axiom comment in Backpack (1d225d1)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/1d225d1ec56624eb235fcc9d27e0d31ae30ed399/ghc

>---------------------------------------------------------------

commit 1d225d1ec56624eb235fcc9d27e0d31ae30ed399
Author: Edward Z. Yang <ezyang at cs.stanford.edu>
Date:   Mon Jul 7 14:54:13 2014 +0100

    Private axiom comment in Backpack
    
    Signed-off-by: Edward Z. Yang <ezyang at cs.stanford.edu>


>---------------------------------------------------------------

1d225d1ec56624eb235fcc9d27e0d31ae30ed399
 docs/backpack/backpack-impl.tex | 29 +++++++++++++++++++++++++++--
 1 file changed, 27 insertions(+), 2 deletions(-)

diff --git a/docs/backpack/backpack-impl.tex b/docs/backpack/backpack-impl.tex
index e45cead..66b62bb 100644
--- a/docs/backpack/backpack-impl.tex
+++ b/docs/backpack/backpack-impl.tex
@@ -1357,8 +1357,33 @@ Now it is illegal for \verb|A = B|, because when the type families are
 unified, the instances now fail the apartness check.  However, if the second
 instance was \verb|F Int = Char|, the families would be able to link together.
 
-It would be nice to solve this problem before getting to the linking phase. (But,
-channeling SPJ for a moment, ``Why would anyone want to do that?!'')
+To make matters worse, an implementation may define more axioms than are
+visible in the signature:
+
+\begin{verbatim}
+package a where
+    A :: [
+        type family F a :: *
+        type instance F Int = Bool
+    ]
+package b where
+    include a
+    B = [
+        import A
+        type instance F Bool = Bool
+        ...
+    ]
+package c where
+    A = [
+        type family F a :: *
+        type instance F Int = Bool
+        type instance F Bool = Int
+    ]
+    include b
+\end{verbatim}
+
+It would seem that private axioms cannot be naively supported. Is
+there any way that thinning axioms could be made to work?
 
 \section{Open questions}\label{sec:open-questions}