Stream: Beginner Questions

Topic: ✔ debug unification


view this post on Zulip Qiyuan Xu (Dec 08 2021 at 08:50):

Is there any eyesight-saving way to debug the type error (or type-class error) in unification (e.g. RS, OF, THEN)? Either the RS, THEN, OF just tell me "no unifiers!", but so many times because of the covert type-class mismatch I just cannot find out "why?".

Any suggestion or best practice about this?

view this post on Zulip Qiyuan Xu (Dec 08 2021 at 08:56):

I hope something can tell me what the mismatch is, about which type mismatches another, just like the verbose type-error printing by ML compiler.

I know some switches like Pattern.unify_trace_failure can let the unifier more verbose, but I still haven't found a way to use them in Isar code thm A[THEN B] or ML "@{thm A} RS @{thm B}" (mainly, the RS is context free so those switchers do not work with it)

view this post on Zulip Qiyuan Xu (Dec 08 2021 at 09:05):

uhmm.. by the tedious code

val ctxt = @{context} |>
 Config.put Pattern.unify_trace_failure true
val x = Thm.biresolution (SOME ctxt) false [(false, @{thm A})] 1 @{thm B}

I get the verbose error info...

view this post on Zulip Manuel Eberl (Dec 08 2021 at 11:18):

You can just do note [[unify_trace_failure]] in Isar, or using [[unify_trace_failure]] in proof mode, or declare [[unify_trace_failure]] on toplevel.

view this post on Zulip Manuel Eberl (Dec 08 2021 at 11:19):

That's what I usually do when unification doesn't work and I don't understand why. Sometimes it helps to also add a show_types or show_sorts when polymorphism is involved (and it often is).

view this post on Zulip Qiyuan Xu (Dec 08 2021 at 14:04):

uhmm, ok I'm fool...

view this post on Zulip Notification Bot (Dec 08 2021 at 14:04):

Qiyuan Xu has marked this topic as resolved.


Last updated: Mar 28 2024 at 20:16 UTC