diff options
| author | Joachim Breitner <mail@joachim-breitner.de> | 2014-01-20 15:16:06 +0000 |
|---|---|---|
| committer | Joachim Breitner <mail@joachim-breitner.de> | 2014-01-20 15:16:06 +0000 |
| commit | 59cb44a3ee4b25fce6dc19816e9647e92e5ff743 (patch) | |
| tree | 3f9b48ff258b8757376f2cc26a9ad41730e75e6e /compiler | |
| parent | da66a8dff05f656cb379edf61827af426e1b05e7 (diff) | |
| download | haskell-59cb44a3ee4b25fce6dc19816e9647e92e5ff743.tar.gz | |
Explain why TcAxiomInstCo carries [TcCoercion], and not [TcType]
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/typecheck/TcEvidence.lhs | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs index 42ca03c92b..3471b327fa 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 |