nested return in do-notation

Stream: lean4

[Marcus Rossel]

I think this is might be a known issue, but here's a quiz: What does Lean do in the following four examples?

def a : Id String := do
  let x ← return "Lean"

def b : Id String := do
  let _ ← return "Lean"

def c : Id String := do
  let x ← (return "Lean")

def d : Id String := do
  let x ← pure "Lean"

Solution

def a : Id String := do
  let x ← return "Lean"

#eval a -- "Lean"

def b : Id String := do
  let _ ← return "Lean"
/-
`do` element is unreachable
-/

def c : Id String := do
  let x ← (return "Lean")
/-
Application type mismatch: The argument
  PUnit.unit
has type
  PUnit
but is expected to have type
  String
in the application
  pure PUnit.unit
-/

def d : Id String := do
  let x ← pure "Lean"
/-
Application type mismatch: The argument
  PUnit.unit
has type
  PUnit
but is expected to have type
  String
in the application
  pure PUnit.unit
-/

Examples c and d feel reasonable to me, but I find a and b rather strange. Would it be possible for the linter to give an unused variable warning on a?

[Marcus Rossel]

For context, I ran into an example of a when looking at Grind.realizeEqProof:

private partial def realizeEqProof (lhs rhs : Expr) (h : Expr) (flipped : Bool) (heq : Bool) : GoalM Expr := do
  let h ← if h == congrPlaceholderProof then
    mkCongrProof lhs rhs heq
  else
    flipProof h flipped heq

... where I was unsure if the let h ← can just be omitted.

[Aaron Liu]

that's a bit strance

[Robin Arnez]

Honestly, I don't find any of a, b, c, d particularly strange; I find

example : Id String := do
  let a ← if true then pure "uhh" else pure "what"

very strange though.

[Eric Wieser]

def foo : Id String := do
  let a := ← if true then pure "uhh" else pure "what"

behaves correctly at least