Making coercions assign metavariables

Stream: lean4

[Thomas Murrills]

Is there a way to make the following coercion work somehow without annotating the type of a, changing f or Foo, or supplying b directly at the call site? I feel as though outParams might be relevant, but I'm not totally sure how to use them here.

structure Foo (b : Bool) where
structure Bar (b : Bool) where

instance {b : Bool} : Coe (Foo b) (Bar b) where
  coe := fun ⟨⟩ => ⟨⟩

variable (a : Foo true) (f : {b : Bool} → Bar b → Unit)

#check (f a) /- application type mismatch
  f a
argument
  a
has type
  Foo true : Type
but is expected to have type
  Bar b : Type -/

[Kyle Miller]

Do you want f : Bar b → Unit specifically instead of f : {b : Bool} → Bar b → Unit? I'd expect it to work if you make b be an additional implicit argument to f.

[Thomas Murrills]

Oops, I guess autoimplicits work differently in variable? (Fixed)

[Thomas Murrills]

In any case, it doesn't work when b is an implicit argument either. :(

[Kyle Miller]

It looks like it does consider the instance, but it doesn't succeed for some reason:

set_option trace.Meta.synthInstance true
#check f a
-- [tryResolve] 💥 Coe (Foo true) (Bar ?m.537) ≟ Coe (Foo ?m.613) (Bar ?m.613)

[Kyle Miller]

Re outParam, I think that's only for class definitions, not instances.

[Kevin Buzzard]

Do all the variants of Coe like CoeTC or CoeTail or whatever, help here? I have no idea what any of these mean in Lean 4 or where to read about them (I just about understood them in Lean 3)

[Arthur Adjedj]

Kevin Buzzard said:

Do all the variants of Coe like CoeTC or CoeTail or whatever, help here? I have no idea what any of these mean in Lean 4 or where to read about them (I just about understood them in Lean 3)

None of the variants fix the issues

[Thomas Murrills]

Seconded—I was just about to report the same thing :)

[Thomas Murrills]

Kyle Miller said:

It looks like it does consider the instance, but it doesn't succeed for some reason:

set_option trace.Meta.synthInstance true
#check f a
-- [tryResolve] 💥 Coe (Foo true) (Bar ?m.537) ≟ Coe (Foo ?m.613) (Bar ?m.613)

Is the MCtxDepth bumped at some point for some reason? (Btw, I wonder: is there a way we can trace that? I imagine it would be helpful in general to be able to see that certain mvars aren't currently assignable in defeq traces!)

[Thomas Murrills]

My current guess is that the withNewMCtxDepth in synthInstance? prevents ?m.537 in the above trace from being assigned.

If that's correct, then this is actually an issue that has come up several times in the past. I wonder if there's a way around this, in principle. E.g. maybe it'd be useful if metavariables created for implicit arguments could be assigned freely by TC search. (This would presumably require a new field in MetavarDecl to keep track of a metavariable's original BinderInfo, if it was originally created for an expression that had a BinderInfo associated with it.) Or maybe that would be problematic for some reason; still, it could be interesting to explore.