diff --git a/tests/elabissues/issues5.lean b/tests/elabissues/issues5.lean
new file mode 100644
index 0000000000..40af3d8e51
--- /dev/null
+++ b/tests/elabissues/issues5.lean
@@ -0,0 +1,15 @@
+import Init.Data.HashMap
+
+def f (a : HashMap Nat Nat) : HashMap Nat Nat :=
+a
+
+def t (as : List Nat) :=
+let xs := {};
+/- We can't elaborate r.insert at this point because we don't know the type of `r`.
+   Our plan is to suspend it by creating a metavariable, and resume later when we have
+   more information. -/
+let ys := as.foldl (fun r a => r.insert a) xs;
+/- After elaborating `f xs`, we learn that `xs` has type `HashMap Nat Nat`. Then,
+   we have enough information for resuming the elaboration of `r.insert a` -/
+let zs := f xs;
+ys
diff --git a/tests/elabissues/issues6.lean b/tests/elabissues/issues6.lean
new file mode 100644
index 0000000000..6772110e48
--- /dev/null
+++ b/tests/elabissues/issues6.lean
@@ -0,0 +1,14 @@
+def f1 (n : Nat) (i : Int) :=
+i + n -- works
+
+def f2 (n : Nat) (i : Int) :=
+n + i -- fails can't coerce Int to Nat
+
+def f3 (n : Nat) (i : Int) :=
+n + (n + (n + (n + i))) -- nested version of the previous issue
+
+def f4 (n : Nat) (i : Int) :=
+n + (n + (n * (n * i))) -- nested version of the previous issue with mixed operators
+
+def f5 (n : Nat) (i : Int) :=
+n + (n + (n * (i, i).1)) -- mixed operators and different structures
diff --git a/tests/elabissues/issues7.lean b/tests/elabissues/issues7.lean
new file mode 100644
index 0000000000..c740098d5d
--- /dev/null
+++ b/tests/elabissues/issues7.lean
@@ -0,0 +1,33 @@
+structure A :=
+(a : Nat)
+
+structure B :=
+(a : Nat)
+
+structure C :=
+(a : Nat)
+
+instance : HasCoe A B := ⟨fun s => ⟨s.1⟩⟩
+instance : HasCoe A C := ⟨fun s => ⟨s.1⟩⟩
+
+def f {α} (a b : α) := a
+def forceB {α} (b : B) (a : α) := a
+def forceC {α} (c : C) (a : α) := a
+def forceA {α} (a : A) (o : α) := o
+
+def f1 (x : _) (y : _) (z : _) :=
+let a1 := f x y;
+let a2 := f y z;
+forceB x a1 -- works
+
+def f2 (x : _) (y : _) (z : _) :=
+let a1 := f x (coe y);
+let a2 := f (coe y) z;
+forceB x (forceC z (forceA y (a1, a2))) -- works because we manually added the coercions above
+
+def f3 (x : _) (y : _) (z : _) :=
+let a1 := f x y;
+let a2 := f y z;
+/- Fails because we "missed" the opportunity to insert coercions around `y`.
+   I think we should **not** support this kind of example. -/
+forceB x (forceC z (forceA y (a1, a2)))