Why do I have to constantly specify the type with singletons

Stream: new members

[Dan Abramov]

This doesn't work:

def foo := {1}
-- typeclass instance problem is stuck, it is often due to metavariables
--  Singleton ℕ ?m.57

OK, fair enough, we don't know if I meant a natural, an integer, or something else.

What about this?

import Mathlib

def foo := {1:ℕ}
-- unsupported structure instance field abbreviation, expecting identifier

Ugh, right, that's invalid syntax, we have to wrap it up.

Let's try:

import Mathlib

def foo := {(1:ℕ)}
-- typeclass instance problem is stuck, it is often due to metavariables
--  Singleton ℕ ?m.57

Nope! But at this point, haven't I given it enough information? I clearly want a singleton of a natural; why is this not enough for a conservative estimate that I want a set of naturals?

I'd like to both understand the technical reason why it can't do that and the design reason (shouldn't it be able to infer this?)

For the record, these do work:

import Mathlib

def foo: Set ℕ := {1} -- works
def foo' := ({1}: Set ℕ) --works

But for more complex types, it requires repeating the type fully.

For a slightly more realistic example:

import Mathlib.Tactic

def pair (a b : Nat) : Set (Set Nat) := {{a}, {a, b}}

def foo := pair 1 1
def bar := ({foo}: Set (Set (Set ℕ)))

Why can't I just write

def foo := pair 1 1
def bar := {foo}

here? Why is it hard or bad to infer that I just want a Set of the thing I'm passing?

Thanks!

[Kenny Lau]

@Dan Abramov firstly in def it's always better to specify the type. Please don't ever write := without the :.

secondly, if you do:

#check Singleton

then you'll see that singleton can be from any type to any type.

More importantly, you actually need to change types, because both Set X and Finset X use the singleton notation, so just from {(1:Nat)} there is no way for Lean to know if you meant the set, or the finset.

[Dan Abramov]

Ah right, so we have many Set-like containers so it has to be explicit. Makes sense.

[Dan Abramov]

and I guess for my last example, this would've worked

import Mathlib.Tactic

def pair (a b : Nat) : Set (Set Nat) := {{a}, {a, b}}

def foo := pair 1 1
def bar := ({foo}: Set _)

so then at least I don't have to repeat the type.

(I hear you re: def, I just used that for the demo, iirc the actual problems I was running into were deeper in proofs)

[Eric Wieser]

The other problem here is that {} is also notation for structure constructors like { fst := _, snd := _ }