Explain why TcAxiomInstCo carries [TcCoercion], and not [TcType]
authorJoachim Breitner <mail@joachim-breitner.de>
Mon, 20 Jan 2014 15:16:06 +0000 (15:16 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Mon, 20 Jan 2014 15:16:06 +0000 (15:16 +0000)
compiler/typecheck/TcEvidence.lhs

index 42ca03c..3471b32 100644 (file)
@@ -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