From d2203aa5a0c9770db08dcd2dbd1701e81dce50bc Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 6 Dec 2022 12:32:37 -0800 Subject: [PATCH] chore: restrict dangerous typed syntax coercions --- src/Init/Meta.lean | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 5dbd30f84d..43a4ed078d 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -1100,23 +1100,21 @@ instance : EmptyCollection (SepArray sep) where instance : EmptyCollection (TSepArray sep k) where emptyCollection := ⟨∅⟩ -/- -We use `CoeTail` here instead of `Coe` to avoid a "loop" when computing `CoeTC`. -The "loop" is interrupted using the maximum instance size threshold, but it is a performance bottleneck. -The loop occurs because the predicate `isNewAnswer` is too imprecise. --/ -instance : CoeTail (SepArray sep) (Array Syntax) where +instance : CoeHead (SepArray sep) (Array Syntax) where coe := SepArray.getElems -instance : Coe (TSepArray k sep) (TSyntaxArray k) where +instance : CoeHead (TSepArray k sep) (TSyntaxArray k) where coe := TSepArray.getElems instance [Coe (TSyntax k) (TSyntax k')] : Coe (TSyntaxArray k) (TSyntaxArray k') where coe a := a.map Coe.coe -instance : Coe (TSyntaxArray k) (Array Syntax) where +instance : CoeHead (TSyntaxArray k) (Array Syntax) where coe a := a.raw +instance : CoeHead (TSepArray k sep) (Array Syntax) where + coe a := (a : TSyntaxArray k) + instance : Coe Ident (TSyntax `Lean.Parser.Command.declId) where coe id := mkNode _ #[id, mkNullNode #[]]