Qiyuan Xu (Dec 08 2021 at 08:50): 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?
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)
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...
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.
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).
Qiyuan Xu (Dec 08 2021 at 14:04):uhmm, ok I'm fool...
Notification Bot (Dec 08 2021 at 14:04):Qiyuan Xu has marked this topic as resolved.
Last updated: Dec 21 2024 at 16:20 UTC