diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs
index 42ca03c92bc7e2c605115a42bdec543564508ca4..3471b327fa736faf7bf93840a35339fdb0c4ef2c 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