can't synthesize instance?

Stream: general

[dagit]

I'm having an issue where I've created an instance and then I immediately try to use that instance and lean says it can't synthesize that instance. If I explicitly pass the instance as an argument (using @), that does type check. #print instances shows my instance too. Any ideas on how to debug why it can't find the instance?

[Patrick Massot]

You can trace the instance search

[dagit]

I was looking at the docs for a command to do that but I couldn't find it. Do you know the command?

[Patrick Massot]

But showing your instance here would probably be quicker

[Patrick Massot]

https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#managing-type-class-inference

[Patrick Massot]

You need to read that whole chapter anyway

[Johannes Hölzl]

you can activate the tracing with set_option trace.class_instances true

[Johannes Hölzl]

but it is a little bit hard to read

[dagit]

Thanks for the links and the command. In the trace it considered the one I want it to use but discarded it because of a metavar.

[Simon Hudon]

I think unless some of your type class parameters are marked as out_param, they can't be meta variables while doing type class resolution. It's a bit like functional dependencies in Haskell.

[Kevin Buzzard]

Can you post a MWE?

[dagit]

Sorry, I was gone at a meeting.

[dagit]

I've tried to make a minimal example but so far I've failed on that front.

[dagit]

The class is defined like this:

universes u v w

namespace sexpr

class is_atom (α : Type _) :=
(to_char_buffer : α → char_buffer)
(read {m} [char_reader string m] (n:ℕ) : m α)

end sexpr

[dagit]

And there is a function like this:
def repr {α:Type} [h : is_atom α] : sexpr α -> string := render buffer.to_string

[dagit]

And it's when I try to use that repr function that lean fails to synthesize the instance

[Simon Hudon]

What's the type of render?

[dagit]

The type of render is a bit involved, here is a link to tha code: https://github.com/GaloisInc/reopt-vcg/blob/master/lean/deps/sexpr/src/galois/sexpr.lean#L51

[Kevin Buzzard]

I guess it all looks OK to my inexpert eyes. So you have some explicit type alpha and some explicit instance is_atom alpha. Does example : is_atom alpha := by apply_instance work?

Independent of this, I have never seen Type _ before. Does it change anything if you change it to Type*?

[Simon Hudon]

try:

def repr {α:Type} [h : is_atom α] (x : sexpr α) : string := render buffer.to_string x

I think having an argument to force a choice for argument α might help with type class resolution

[dagit]

Kevin, that example also fails to find the instance. I was trying something like that earlier today.

[dagit]

I'll try that Simon and get back to you.

[Simon Hudon]

:+1:

[dagit]

Hmm...same error message. I'll try what Kevin ask about with Type*

[dagit]

Wait, what is the syntax you wanted me to try? I don't think Type* is valid.

[dagit]

Removing the _ so that it's just Type doesn't resolve the issue either.

[Kevin Buzzard]

I didn't know (alpha : Type _) was valid syntax. I am pretty sure (alpha : Type*) is. You're using Lean 3.4 right?

[Kevin Buzzard]

If by apply_instance can't find the instance then this is a step in the right direction.

[Kevin Buzzard]

That's just asking type class inference to look up the instance.

[dagit]

3.4.1 to be precise

[Kevin Buzzard]

That should be fine.

[dagit]

oh, Type* without a space makes a difference?

[Patrick Massot]

yes

[dagit]

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : is_atom sexp.atom := nat_expr.atom_is_atom
[class_instances] trying next solution, current solution has metavars

[dagit]

Is there a way to learn more about the metavar?

[dagit]

Ah, we solved it.

[dagit]

It was a universe level metavar

[dagit]

In the definition of is_atom we added that the m used by read needs to have type Type -> Type

[dagit]

Now it works as expected in my code

[dagit]

Thanks everyone

[dagit]

Also, set_option pp.all true allowed us to see the universe level variable.

[Simon Hudon]

That's always a fun challenge!

[Joe Hendrix]

Thanks for the help. I understand why Lean behaves the way it does in this case, but I found the behavior sufficiently counterintuitive that I filed an issue: https://github.com/leanprover/lean/issues/1995

[Kevin Buzzard]

Hey Joe, long time no see. I'm sure you're aware of this, but nobody is reading Lean 3 issues at the minute, as far as we know. Lean 3 has basically been abandoned. There was one Lean update to 3.4.2 which Sebastian Ullrich put together after a request from the community, but we think that's pretty much it now.

[Joe Hendrix]

Hi Kevin, I understand -- I only filed the issue as I don't see any rush on addressing this, but also didn't want to forget the problem either. I'm hoping that Lean 4 could address this once the new core capabilities are stable.
I'm still using Lean and work with Jason, but also need to focus on other projects.

[Kevin Buzzard]

These structures which introduce new universes in structure fields can be problematic. Mario urged me to avoid them in some Lean maths project I'm working on (the perfectoid project) and we actually had to do some work to work around it. Ultimately our definition structure Spv (R : Type u) contained a field which mentioned a new type Gamma : Type u (note: same universe as R) and then we had to make a custom constructor which took Gamma of type v and created another Gamma in the same universe as R. We were assured by Mario that this would avoid problems further down the line.