noncomputable tainting

Stream: general

[Eric Wieser]

Is this expected behavior:

noncomputable def foo : ℕ := classical.some (show ∃ x, x = 1, from ⟨1, rfl⟩)

structure bar (n : ℕ) :=
(x : ℕ)

def baz : bar foo := ⟨1⟩  -- error: not marked noncomputable

Surely the computability of types is irrelevant, so foo shouldn't poison baz

[Gabriel Ebner]

I'm pretty sure it complains about the foo in @bar.mk foo 1.

[Eric Wieser]

Ah right, and then this is just the simpler case that lean doesn't track computability at that level

[Eric Wieser]

This came up when wanting to show a galois_insertion between two noncomputable functions, with a computable choice operation