From ccba5d35d07a448fab14c0e391c8105df6e2564c Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Fri, 1 Dec 2023 08:07:16 -0800 Subject: [PATCH] Fix: use exprToSyntax in `comefrom` elaborator (#28) 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)