Zulip Chat Archive

Stream: new members

Topic: Subtype type inference problem


view this post on Zulip Iain Monro (Aug 15 2020 at 17:51):

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?

view this post on Zulip Mario Carneiro (Aug 15 2020 at 18:36):

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

view this post on Zulip Iain Monro (Aug 15 2020 at 22:13):

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).

view this post on Zulip Iain Monro (Aug 15 2020 at 22:15):

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 22:27):

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.

view this post on Zulip Iain Monro (Aug 15 2020 at 22:55):

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...

view this post on Zulip Eric Wieser (Aug 16 2020 at 08:37):

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

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

Last updated: May 11 2021 at 12:15 UTC