From bec0bbc351281ccc7a983032ce5ef960b502ee68 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 30 Jun 2022 13:03:50 +0200 Subject: [PATCH] fix: replace dangerous instance by CoeTail In order to guarantee termination of type class synthesis when resolving coercions, a good rule of thumb is that the instances should not introduce metavariables (during TC synthesis). For common coercion type classes this means: - `Coe T S`, `CoeTail T S`: the variables of `T` must be a subset of those of `S` - `CoeHead T S`: the variables of `S` must be a subset of those of `T` If these rules are not followed, we can easily get nontermination. In this case: `CoeTC Foo Syntax` is reduced to `CoeTC Foo (TSyntax ?m_1)` using the (dangerous) `Coe (TSyntax k) Syntax` instance, to which we can then apply the otherwise fine `Coe (TSyntax [k]) (TSyntax (k'::ks))` coercion infinitely often. --- src/Init/Notation.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index d3b4d503c7..952bec26d4 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -23,7 +23,7 @@ end Lean.Parser.Syntax namespace Lean -instance : Coe (TSyntax ks) Syntax where +instance : CoeHead (TSyntax ks) Syntax where coe stx := stx.raw instance : Coe SyntaxNodeKind SyntaxNodeKinds where