inductive foo {n : Nat} : Prop

-- Check that the error message will print the types with implicit arguments shown
example (h : @foo 42) : @foo 23 := by
  apply h

example : (1 : Nat) = 1 := by
  apply (rfl : (1 : Int) = 1)

example : PUnit.{0} = PUnit.{0} := by
  apply Eq.refl PUnit.{1}