<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div>Hallo Fabian,</div><div><br></div><div>This is the issue that was discussed here:</div><div><br></div><div></div><div><a href="https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2022-03/msg00005.html">https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2022-03/msg00005.html</a><br></div><br><div>
<meta charset="UTF-8"><div>In short, I broke this in 2014 when moving to the new datatypes and it's not easy to repair. I doubt I will ever find the time to do it myself -- it requires some concentration. If anybody is interested in repairing this, I would be more than happy to supervise them.</div><div><br></div><div>Best,</div><div>Jasmin</div><div><br></div><div>--<br>Prof. Dr. Jasmin Blanchette<br>Chair of Theoretical Computer Science<br>Ludwig-Maximilians-Universität München<br>Oettingenstr. 67, 80538 München, Germany<br>Tel.: +49 (0)89 2180 9337<br>Email: jasmin.blanchette@ifi.lmu.de<br>Web: https://www.tcs.ifi.lmu.de/<br><br></div>
</div>
<div><br><blockquote type="cite"><div>On 26. Jun 2023, at 12:36, Fabian Huch <huch@in.tum.de> wrote:</div><br class="Apple-interchange-newline"><div><div>In the following minimal example:<br><br>datatype t = A | B "t × t"<br><br>fun f :: "t ⇒ bool" where<br> "f A ⟷ True"<br>| "f _ ⟷ False"<br><br>quickcheck throws an error if you invoke it (both Isabelle2022 and latest devel):<br><br>lemma "f x = True" quickcheck<br><br><br>Does anyone have an idea what's going on? The error is as follows:<br><br><br>Type unification failed: No type arity t :: full_exhaustive<br><br>Type error in application: incompatible operand type<br><br>Operator: full_exhaustive_class.full_exhaustive :: (??'a × (unit ⇒ term) ⇒ (bool × term list) option) ⇒ natural ⇒ (bool × term list) option<br>Operand:<br> λ(t, t_t__).<br> Quickcheck_Random.catch_match<br> (if equal_bool_inst.equal_bool (f t) True then None<br> else Some<br> (True,<br> [t_t__ (),<br> Quickcheck_Random.catch_match (term_of_bool_inst.term_of_bool True)<br> (Code_Evaluation.Const<br> (String.Literal True False False False True False True<br> (String.Literal True False True False True True True<br> (String.Literal True False False True False True True<br> (String.Literal True True False False False True True<br> (String.Literal True True False True False True True<br> (String.Literal True True False False False True True<br> (String.Literal False False False True False True True<br> (String.Literal True False True False False True True<br> (String.Literal True True False False False True True<br> (String.Literal True True False True False True True<br> (String.Literal True True True True True False True<br> (String.Literal True False True False False False True<br> (String.Literal False False False True True True True<br> (String.Literal False False False True False True True<br> (String.Literal True False False False False True True<br> (String.Literal True False True False True True True<br> (String.Literal True True False False True True True<br>(String.Literal False False True False True True True<br>(String.Literal True False False True False True True<br>(String.Literal False True True False True True True<br>(String.Literal True False True False False True True<br>(String.Literal False True True True False True False<br>(String.Literal True False True False True True True<br>(String.Literal False True True True False True True<br>(String.Literal True True False True False True True<br>(String.Literal False True True True False True True<br>(String.Literal True True True True False True True<br>(String.Literal True True True False True True True<br>(String.Literal False True True True False True True zero_literal_inst.zero_literal)))))))))))))))))))))))))))))<br> (typerep.Typerep<br> (String.Literal False False False True False False True<br> (String.Literal True True True True False False True<br> (String.Literal False False True True False False True<br> (String.Literal False True True True False True False<br> (String.Literal False True False False False True True<br> (String.Literal True True True True False True True<br> (String.Literal True True True True False True True (String.Literal False False True True False True True zero_literal_inst.zero_literal))))))))<br> [])),<br> Quickcheck_Random.catch_match (term_of_bool_inst.term_of_bool (f t))<br> (Code_Evaluation.Const<br> (String.Literal True False False False True False True<br> (String.Literal True False True False True True True<br> (String.Literal True False False True False True True<br> (String.Literal True True False False False True True<br> (String.Literal True True False True False True True<br> (String.Literal True True False False False True True<br> (String.Literal False False False True False True True<br> (String.Literal True False True False False True True<br> (String.Literal True True False False False True True<br> (String.Literal True True False True False True True<br> (String.Literal True True True True True False True<br> (String.Literal True False True False False False True<br> (String.Literal False False False True True True True<br> (String.Literal False False False True False True True<br> (String.Literal True False False False False True True<br> (String.Literal True False True False True True True<br> (String.Literal True True False False True True True<br>(String.Literal False False True False True True True<br>(String.Literal True False False True False True True<br>(String.Literal False True True False True True True<br>(String.Literal True False True False False True True<br>(String.Literal False True True True False True False<br>(String.Literal True False True False True True True<br>(String.Literal False True True True False True True<br>(String.Literal True True False True False True True<br>(String.Literal False True True True False True True<br>(String.Literal True True True True False True True<br>(String.Literal True True True False True True True<br>(String.Literal False True True True False True True zero_literal_inst.zero_literal)))))))))))))))))))))))))))))<br> (typerep.Typerep<br> (String.Literal False False False True False False True<br> (String.Literal True True True True False False True<br> (String.Literal False False True True False False True<br> (String.Literal False True True True False True False<br> (String.Literal False True False False False True True<br> (String.Literal True True True True False True True<br> (String.Literal True True True True False True True (String.Literal False False True True False True True zero_literal_inst.zero_literal))))))))<br> []))]))<br> (if genuine_only__ then None<br> else Some<br> (False,<br> [t_t__ (),<br> Quickcheck_Random.catch_match (term_of_bool_inst.term_of_bool True)<br> (Code_Evaluation.Const<br> (String.Literal True False False False True False True<br> (String.Literal True False True False True True True<br> (String.Literal True False False True False True True<br> (String.Literal True True False False False True True<br> (String.Literal True True False True False True True<br> (String.Literal True True False False False True True<br> (String.Literal False False False True False True True<br> (String.Literal True False True False False True True<br> (String.Literal True True False False False True True<br> (String.Literal True True False True False True True<br> (String.Literal True True True True True False True<br> (String.Literal True False True False False False True<br> (String.Literal False False False True True True True<br> (String.Literal False False False True False True True<br> (String.Literal True False False False False True True<br> (String.Literal True False True False True True True<br> (String.Literal True True False False True True True<br>(String.Literal False False True False True True True<br>(String.Literal True False False True False True True<br>(String.Literal False True True False True True True<br>(String.Literal True False True False False True True<br>(String.Literal False True True True False True False<br>(String.Literal True False True False True True True<br>(String.Literal False True True True False True True<br>(String.Literal True True False True False True True<br>(String.Literal False True True True False True True<br>(String.Literal True True True True False True True<br>(String.Literal True True True False True True True<br>(String.Literal False True True True False True True zero_literal_inst.zero_literal)))))))))))))))))))))))))))))<br> (typerep.Typerep<br> (String.Literal False False False True False False True<br> (String.Literal True True True True False False True<br> (String.Literal False False True True False False True<br> (String.Literal False True True True False True False<br> (String.Literal False True False False False True True<br> (String.Literal True True True True False True True<br> (String.Literal True True True True False True True (String.Literal False False True True False True True zero_literal_inst.zero_literal))))))))<br> [])),<br> Quickcheck_Random.catch_match (term_of_bool_inst.term_of_bool (f t))<br> (Code_Evaluation.Const<br> (String.Literal True False False False True False True<br> (String.Literal True False True False True True True<br> (String.Literal True False False True False True True<br> (String.Literal True True False False False True True<br> (String.Literal True True False True False True True<br> (String.Literal True True False False False True True<br> (String.Literal False False False True False True True<br> (String.Literal True False True False False True True<br> (String.Literal True True False False False True True<br> (String.Literal True True False True False True True<br> (String.Literal True True True True True False True<br> (String.Literal True False True False False False True<br> (String.Literal False False False True True True True<br> (String.Literal False False False True False True True<br> (String.Literal True False False False False True True<br> (String.Literal True False True False True True True<br> (String.Literal True True False False True True True<br>(String.Literal False False True False True True True<br>(String.Literal True False False True False True True<br>(String.Literal False True True False True True True<br>(String.Literal True False True False False True True<br>(String.Literal False True True True False True False<br>(String.Literal True False True False True True True<br>(String.Literal False True True True False True True<br>(String.Literal True True False True False True True<br>(String.Literal False True True True False True True<br>(String.Literal True True True True False True True<br>(String.Literal True True True False True True True<br>(String.Literal False True True True False True True zero_literal_inst.zero_literal)))))))))))))))))))))))))))))<br> (typerep.Typerep<br> (String.Literal False False False True False False True<br> (String.Literal True True True True False False True<br> (String.Literal False False True True False False True<br> (String.Literal False True True True False True False<br> (String.Literal False True False False False True True<br> (String.Literal True True True True False True True<br> (String.Literal True True True True False True True (String.Literal False False True True False True True zero_literal_inst.zero_literal))))))))<br> []))])) ::<br> t × (unit ⇒ term) ⇒ (bool × term list) option<br><br><br>Fabian<br><br>_______________________________________________<br>isabelle-dev mailing list<br>isabelle-dev@in.tum.de<br>https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev<br></div></div></blockquote></div><br></body></html>