diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 9eae79ee2c..76586e495d 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -287,6 +287,12 @@ instance : Coe NumLit Term where
 instance : Coe CharLit Term where
   coe s := ⟨s.raw⟩
 
+instance : Coe Ident Syntax.Level where
+  coe s := ⟨s.raw⟩
+
+instance : Coe NumLit Prio where
+  coe s := ⟨s.raw⟩
+
 instance : Coe NumLit Prec where
   coe s := ⟨s.raw⟩