From 59cb44a3ee4b25fce6dc19816e9647e92e5ff743 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 20 Jan 2014 15:16:06 +0000
Subject: [PATCH] Explain why TcAxiomInstCo carries [TcCoercion], and not
[TcType]
---
compiler/typecheck/TcEvidence.lhs | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs
index 42ca03c92bc7..3471b327fa73 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
--
GitLab