[isabelle-dev] quickcheck throws "Type unification failed: No type arity t :: full_exhaustive" on simple example
Jasmin Blanchette
jasmin.blanchette at ifi.lmu.de
Mon Jun 26 12:52:11 CEST 2023
Hallo Fabian,
This is the issue that was discussed here:
https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2022-03/msg00005.html
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.
Best,
Jasmin
--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9337
Email: jasmin.blanchette at ifi.lmu.de
Web: https://www.tcs.ifi.lmu.de/
> On 26. Jun 2023, at 12:36, Fabian Huch <huch at in.tum.de> wrote:
>
> In the following minimal example:
>
> datatype t = A | B "t × t"
>
> fun f :: "t ⇒ bool" where
> "f A ⟷ True"
> | "f _ ⟷ False"
>
> quickcheck throws an error if you invoke it (both Isabelle2022 and latest devel):
>
> lemma "f x = True" quickcheck
>
>
> Does anyone have an idea what's going on? The error is as follows:
>
>
> Type unification failed: No type arity t :: full_exhaustive
>
> Type error in application: incompatible operand type
>
> Operator: full_exhaustive_class.full_exhaustive :: (??'a × (unit ⇒ term) ⇒ (bool × term list) option) ⇒ natural ⇒ (bool × term list) option
> Operand:
> λ(t, t_t__).
> Quickcheck_Random.catch_match
> (if equal_bool_inst.equal_bool (f t) True then None
> else Some
> (True,
> [t_t__ (),
> Quickcheck_Random.catch_match (term_of_bool_inst.term_of_bool True)
> (Code_Evaluation.Const
> (String.Literal True False False False True False True
> (String.Literal True False True False True True True
> (String.Literal True False False True False True True
> (String.Literal True True False False False True True
> (String.Literal True True False True False True True
> (String.Literal True True False False False True True
> (String.Literal False False False True False True True
> (String.Literal True False True False False True True
> (String.Literal True True False False False True True
> (String.Literal True True False True False True True
> (String.Literal True True True True True False True
> (String.Literal True False True False False False True
> (String.Literal False False False True True True True
> (String.Literal False False False True False True True
> (String.Literal True False False False False True True
> (String.Literal True False True False True True True
> (String.Literal True True False False True True True
> (String.Literal False False True False True True True
> (String.Literal True False False True False True True
> (String.Literal False True True False True True True
> (String.Literal True False True False False True True
> (String.Literal False True True True False True False
> (String.Literal True False True False True True True
> (String.Literal False True True True False True True
> (String.Literal True True False True False True True
> (String.Literal False True True True False True True
> (String.Literal True True True True False True True
> (String.Literal True True True False True True True
> (String.Literal False True True True False True True zero_literal_inst.zero_literal)))))))))))))))))))))))))))))
> (typerep.Typerep
> (String.Literal False False False True False False True
> (String.Literal True True True True False False True
> (String.Literal False False True True False False True
> (String.Literal False True True True False True False
> (String.Literal False True False False False True True
> (String.Literal True True True True False True True
> (String.Literal True True True True False True True (String.Literal False False True True False True True zero_literal_inst.zero_literal))))))))
> [])),
> Quickcheck_Random.catch_match (term_of_bool_inst.term_of_bool (f t))
> (Code_Evaluation.Const
> (String.Literal True False False False True False True
> (String.Literal True False True False True True True
> (String.Literal True False False True False True True
> (String.Literal True True False False False True True
> (String.Literal True True False True False True True
> (String.Literal True True False False False True True
> (String.Literal False False False True False True True
> (String.Literal True False True False False True True
> (String.Literal True True False False False True True
> (String.Literal True True False True False True True
> (String.Literal True True True True True False True
> (String.Literal True False True False False False True
> (String.Literal False False False True True True True
> (String.Literal False False False True False True True
> (String.Literal True False False False False True True
> (String.Literal True False True False True True True
> (String.Literal True True False False True True True
> (String.Literal False False True False True True True
> (String.Literal True False False True False True True
> (String.Literal False True True False True True True
> (String.Literal True False True False False True True
> (String.Literal False True True True False True False
> (String.Literal True False True False True True True
> (String.Literal False True True True False True True
> (String.Literal True True False True False True True
> (String.Literal False True True True False True True
> (String.Literal True True True True False True True
> (String.Literal True True True False True True True
> (String.Literal False True True True False True True zero_literal_inst.zero_literal)))))))))))))))))))))))))))))
> (typerep.Typerep
> (String.Literal False False False True False False True
> (String.Literal True True True True False False True
> (String.Literal False False True True False False True
> (String.Literal False True True True False True False
> (String.Literal False True False False False True True
> (String.Literal True True True True False True True
> (String.Literal True True True True False True True (String.Literal False False True True False True True zero_literal_inst.zero_literal))))))))
> []))]))
> (if genuine_only__ then None
> else Some
> (False,
> [t_t__ (),
> Quickcheck_Random.catch_match (term_of_bool_inst.term_of_bool True)
> (Code_Evaluation.Const
> (String.Literal True False False False True False True
> (String.Literal True False True False True True True
> (String.Literal True False False True False True True
> (String.Literal True True False False False True True
> (String.Literal True True False True False True True
> (String.Literal True True False False False True True
> (String.Literal False False False True False True True
> (String.Literal True False True False False True True
> (String.Literal True True False False False True True
> (String.Literal True True False True False True True
> (String.Literal True True True True True False True
> (String.Literal True False True False False False True
> (String.Literal False False False True True True True
> (String.Literal False False False True False True True
> (String.Literal True False False False False True True
> (String.Literal True False True False True True True
> (String.Literal True True False False True True True
> (String.Literal False False True False True True True
> (String.Literal True False False True False True True
> (String.Literal False True True False True True True
> (String.Literal True False True False False True True
> (String.Literal False True True True False True False
> (String.Literal True False True False True True True
> (String.Literal False True True True False True True
> (String.Literal True True False True False True True
> (String.Literal False True True True False True True
> (String.Literal True True True True False True True
> (String.Literal True True True False True True True
> (String.Literal False True True True False True True zero_literal_inst.zero_literal)))))))))))))))))))))))))))))
> (typerep.Typerep
> (String.Literal False False False True False False True
> (String.Literal True True True True False False True
> (String.Literal False False True True False False True
> (String.Literal False True True True False True False
> (String.Literal False True False False False True True
> (String.Literal True True True True False True True
> (String.Literal True True True True False True True (String.Literal False False True True False True True zero_literal_inst.zero_literal))))))))
> [])),
> Quickcheck_Random.catch_match (term_of_bool_inst.term_of_bool (f t))
> (Code_Evaluation.Const
> (String.Literal True False False False True False True
> (String.Literal True False True False True True True
> (String.Literal True False False True False True True
> (String.Literal True True False False False True True
> (String.Literal True True False True False True True
> (String.Literal True True False False False True True
> (String.Literal False False False True False True True
> (String.Literal True False True False False True True
> (String.Literal True True False False False True True
> (String.Literal True True False True False True True
> (String.Literal True True True True True False True
> (String.Literal True False True False False False True
> (String.Literal False False False True True True True
> (String.Literal False False False True False True True
> (String.Literal True False False False False True True
> (String.Literal True False True False True True True
> (String.Literal True True False False True True True
> (String.Literal False False True False True True True
> (String.Literal True False False True False True True
> (String.Literal False True True False True True True
> (String.Literal True False True False False True True
> (String.Literal False True True True False True False
> (String.Literal True False True False True True True
> (String.Literal False True True True False True True
> (String.Literal True True False True False True True
> (String.Literal False True True True False True True
> (String.Literal True True True True False True True
> (String.Literal True True True False True True True
> (String.Literal False True True True False True True zero_literal_inst.zero_literal)))))))))))))))))))))))))))))
> (typerep.Typerep
> (String.Literal False False False True False False True
> (String.Literal True True True True False False True
> (String.Literal False False True True False False True
> (String.Literal False True True True False True False
> (String.Literal False True False False False True True
> (String.Literal True True True True False True True
> (String.Literal True True True True False True True (String.Literal False False True True False True True zero_literal_inst.zero_literal))))))))
> []))])) ::
> t × (unit ⇒ term) ⇒ (bool × term list) option
>
>
> Fabian
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20230626/d655ed7f/attachment-0001.htm>
More information about the isabelle-dev
mailing list