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

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