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

@@ -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)