quotient.lift_on elaboration

Stream: general

[Kenny Lau]

import data.set.basic

-- works
example {α β : Type*} [setoid α] (s : set β) [setoid s]
  (f : α → β) (hf1 : ∀ x, f x ∈ s) (hf2 : ∀ x y, x ≈ y → (⟨f x, hf1 x⟩ : s) ≈ ⟨f y, hf1 y⟩) :
  quotient _inst_1 → quotient _inst_2 :=
λ x, quotient.lift_on x (λ r, ⟦(⟨f r, hf1 r⟩ : s)⟧) $ λ x y hxy, quotient.sound $ hf2 x y hxy

/-
invalid constructor ⟨...⟩, expected type is not an inductive type
  ?m_1
-/
example {α β : Type*} [setoid α] (s : set β) [setoid s]
  (f : α → β) (hf1 : ∀ x, f x ∈ s) (hf2 : ∀ x y, x ≈ y → (⟨f x, hf1 x⟩ : s) ≈ ⟨f y, hf1 y⟩) :
  quotient _inst_1 → quotient _inst_2 :=
λ x, quotient.lift_on x (λ r, ⟦⟨f r, hf1 r⟩⟧) $ λ x y hxy, quotient.sound $ hf2 x y hxy

[Kenny Lau]

why does it fail when I have an inductive type?

[Mario Carneiro]

it's an elaboration order problem. Anonymous constructors must resolve to an inductive type straight away, but I guess the other stuff is getting elaborated before lean knows what the target type is of the function