diff --git a/library/Init/Lean/MetavarContext.lean b/library/Init/Lean/MetavarContext.lean
index 42c5f103e2..7f4fe1467b 100644
--- a/library/Init/Lean/MetavarContext.lean
+++ b/library/Init/Lean/MetavarContext.lean
@@ -16,6 +16,8 @@ structure MetavarContext :=
 
 namespace MetavarContext
 
+instance : Inhabited MetavarContext := ⟨{}⟩
+
 @[export lean_mk_metavar_ctx]
 def mkMetavarContext : Unit → MetavarContext :=
 fun _ => {}