| structure A := | |
| (a : Nat) | |
| structure B := | |
| (a : Nat) | |
| structure C := | |
| (a : Nat) | |
| instance : Coe A B := ⟨fun s => ⟨s.1⟩⟩ | |
| instance : Coe 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 ↑y; | |
| let a2 := f ↑y z; | |
| forceB x (forceC z (forceA y (a1, a2))) -- works because we manually added the coercions above | |
| #exit | |
| 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))) |