Subtype type inference problem

Stream: new members

[Iain Monro]

The following #mwe fails to build:

import data.multiset.basic

variables {α : Type} {p: α → Prop}

example (s: multiset (subtype p)) : ∀ y ∈ s, y.val = y.val := sorry

I'm not exactly sure what the issue is - the VS code plugin makes it look like Lean is figuring out that y ought to be a subtype p, so y.val = y.val should be a valid Prop?

[Mario Carneiro]

It's a timing thing. Lean can't figure out that y has type subtype p until after it has read y.val, which doesn't even make it past name resolution if we don't know the type of y. If you use subtype.val y = y.val then it will work

[Iain Monro]

Okay, got there. While multiset.mem has type α → multiset α → Prop, has_mem.mem in general has type α → γ → Prop, so merely having y ∈ s isn't enough to infer y : subtype p even having s : multiset (subtype p).

[Iain Monro]

It feels like has_mem in some sense should be smarter? Don't really know enough to say how or properly clarify what that even really means though :p

[Mario Carneiro]

It does, actually, the first argument of has_mem is an out_param so this absolutely works to determine the type of y. The problem is that it doesn't come soon enough; projection notation specifically requires typing infornation very early because we don't even know which function is being called when we see y.val, and the type of this function (or if it's even a function, as opposed to a constant y.val in namespace y) can affect type class inference and everything else. Basically we can't even start type class inference until we have some basic idea of what we're dealing with, and inferring the type of y from the has_mem instance is too late.

[Iain Monro]

Hmm, so we need to fully determine the type of the proposition before we can perform type class inference, and since that determination would require type class inference, it fails? That makes sense, though I don't feel particularly up to learning enough about the dependencies involved to fully understand it myself just yet...

[Eric Wieser]

In this case you can use type ascriptions instead of .val anyway, right?

example (s: multiset (subtype p)) : ∀ y ∈ s, (y : \a) = y := sorry