Zulip Chat Archive

Stream: new members

Topic: Synth Instance Tracing

N Gelwan (Nov 21 2023 at 20:54):

Anyone have any pointers into debugging instance synthesis?

Here I'm attempting to construct a union of terms which depend upon a typeclass instance. I've done this twice; in the first example I'm encountering the synthesis failure, in the second I've provided some of the implicit arguments explicitly.

class Domain (Φ : Type) (s : Type) where
  domain : Φ → Set s

set_option trace.Meta.synthInstance true

variable {Φ : Type} {s : Type} [inst : Domain Φ s] (φ ψ : Φ)

def domainUnion₁ :=
  (Domain.domain φ)
  ∪
  /-
  typeclass instance problem is stuck, it is often due to metavariables
    Domain Φ ?m.9227
  -/
  (Domain.domain ψ)

def domainUnion₂ :=
  (Domain.domain φ)
  ∪
  (@Domain.domain Φ s inst ψ)

I'm not surprised that synthesis fails; it would be hard to figure out that s is the type argument we need here, but I'm trying to dig into this example to get some insight out of it and have two questions:

1) Why does synthesis not fail on the first argument of the union?

2) How can I interpret the results of synthesis tracing?
Here's the trace of the synthesis of the successfully traced first argument of the union in the first example:

Trace

Here's the failing instance:

Trace

Ruben Van de Velde (Nov 21 2023 at 20:59):

  1. It does fail, but it only shows one error

Kevin Buzzard (Nov 21 2023 at 23:28):

Why not [inst : Domain Φ s]?

N Gelwan (Nov 22 2023 at 03:22):

Oh yeah, sorry-- no reason. That was an artifact from some earlier experiments. Changing it doesn't make a difference.

Kevin Buzzard (Nov 22 2023 at 19:53):

It doesn't even make a difference to the traces?? Are the traces from before or after this change?

Last updated: Dec 20 2023 at 11:08 UTC