[commit: ghc] master: Explain why TcAxiomInstCo carries [TcCoercion], and not [TcType] (59cb44a)

git at git.haskell.org git at git.haskell.org
Mon Jan 20 15:15:14 UTC 2014


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

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/59cb44a3ee4b25fce6dc19816e9647e92e5ff743/ghc

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

commit 59cb44a3ee4b25fce6dc19816e9647e92e5ff743
Author: Joachim Breitner <mail at joachim-breitner.de>
Date:   Mon Jan 20 15:16:06 2014 +0000

    Explain why TcAxiomInstCo carries [TcCoercion], and not [TcType]


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

59cb44a3ee4b25fce6dc19816e9647e92e5ff743
 compiler/typecheck/TcEvidence.lhs |    6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs
index 42ca03c..3471b32 100644
--- a/compiler/typecheck/TcEvidence.lhs
+++ b/compiler/typecheck/TcEvidence.lhs
@@ -90,6 +90,12 @@ differences
      - TcSubCo is not applied as deep as done with mkSubCo
     Reason: they'll get established when we desugar to Coercion
 
+  * TcAxiomInstCo has a [TcCoercion] parameter, and not a [Type] parameter.
+    This differs from the formalism, but corresponds to AxiomInstCo (see
+    [Coercion axioms applied to coercions]).
+    Why can't we use [TcType] here, in code not relevant for the simplifier?
+    Because of coercionToTcCoercion.
+
 \begin{code}
 data TcCoercion 
   = TcRefl Role TcType



More information about the ghc-commits mailing list