Email Gateway (Mar 02 2022 at 16:16): Email Gateway (Mar 02 2022 at 16:16):From: Tobias Nipkow <nipkow@in.tum.de>
does not work:
datatype t = T "t list"
lemma "(x::t) = y"
quickcheck
Type unification failed: No type arity t :: full_exhaustive
Is there anything I can do about it?
Tobias
PS nitpick works
smime.p7s
Email Gateway (Mar 02 2022 at 16:32):From: Jasmin Blanchette <cl-isabelle-users@lists.cam.ac.uk>
I think you could manually instantiate full_exhaustive (or one of the other type classes used by Quickcheck), but that's probably something you'd like to avoid.
The short story is: Nitpick's author crippled Quickcheck.
The long story is: When we introduced the new datatypes in 2014, we broke Quickcheck without noticing it. Quickcheck had some regression tests but none covering nested types. It took quite some time (until 2016?) before anybody pointed out the breakage on the mailing list, and it has been hanging on my TODO list (and my conscience) ever since then.
I'll move it to the top of my TODO list, but it's a quite daunting task that will take a good chunk of free time to concentrate. I can't promise I'll find the time to do it in the coming 2-3 months.
Jasmin
Email Gateway (Mar 02 2022 at 16:36):From: Dmitriy Traytel <traytel@di.ku.dk>
In the meantime, adding
datatype_compat t
after the datatype, makes quickcheck work (in this case).
Best wishes,
Dmitriy
Email Gateway (Mar 02 2022 at 16:39):From: Tobias Nipkow <nipkow@in.tum.de>
Dmitriy,
Thanbks a lot for that, because it immediately gave me a counterexample to my
main theorem, something I had been suspecting ...
Tobias
smime.p7s
Last updated: Jul 15 2022 at 23:21 UTC