From ef960ea064deebe84c5655a1a5e7142403f88f82 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 28 Nov 2023 12:57:06 -0800 Subject: [PATCH] Fix: use exprToSyntax in `comefrom` elaborator The current logic to embed an expression into syntax is buggy since it doesn't unify types while doing the metavariable assignment. This can leave unassigned universe metavariables. Switching to core's `exprToSyntax` resolves this issue. I discovered this while working on lean4#2973. Without this fix, all the `match` examples in this repository fail when using that PR's version of Lean. --- Qq/Match.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Qq/Match.lean b/Qq/Match.lean index 8ae3267..78c871e 100644 --- a/Qq/Match.lean +++ b/Qq/Match.lean @@ -248,8 +248,8 @@ partial def isIrrefutablePattern : Term → Bool scoped elab "_comefrom" n:ident "do" b:doSeq " in " body:term : term <= expectedType => do let _ ← extractBind expectedType - (← elabTerm (← `(?m)).1.stripPos none).mvarId!.assign expectedType - elabTerm (← `(have $n:ident : ?m := (do $b:doSeq); $body)) expectedType + let ty ← exprToSyntax expectedType + elabTerm (← `(have $n:ident : $ty := (do $b:doSeq); $body)) expectedType scoped syntax "_comefrom" ident "do" doSeq : term macro_rules | `(assert! (_comefrom $n do $b); $body) => `(_comefrom $n do $b in $body)