nonassignable

Stream: lean4

[Kevin Buzzard]

Looking through traces I see

                            [] ❌ ?m.6557 x =?= ↑s ▼
                              [] ?m.6557 x [nonassignable] =?= ↑s [nonassignable]

Here s : Finset K, and ↑s : Set K and x : ?m.6547. I think that this should be solvable, with ?m.6557 x := ↑s. What does nonassignable mean? I have

set_option trace.profiler true in
set_option trace.Meta.isDefEq true in
set_option maxHeartbeats 950000 in

and I'm assuming that the trace in question is coming from trace.Meta.isDefEq. Is this question too vague? The trace is right in the middle of a really gnarly calculation which depends on a lot of mathlib.

[Mario Carneiro]

nonassignable means that we are in a sub-scope in which that metavariable is supposed to be treated like a constant

[Kevin Buzzard]

But s is a constant, it's just some variable. Is there some situation where it's not possible to assign the metavariables to make it all work? 6557 is just the constant function to \u s and 6547 is whatever the type of x is

[Mario Carneiro]

It is likely that you are just looking at the wrong part of the trace. This metavariable is not assignable at this point in the computation, because it is in a scope which said "assume everything is nonassignable except for these mvars and try to solve for them"

[Kevin Buzzard]

Thanks. Whilst I have no desire to learn about exprs and CS-monads (the really nitty-gritty stuff), I think that learning something about how the typeclass and unification algorithms work would be of some benefit to me -- I have no clue at all about when and where one assigns metavariables.