Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] quickcheck throws "Type unification failed...

view this post on Zulip Email Gateway (Jun 26 2023 at 10:36):

From: Fabian Huch <huch@in.tum.de>
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 Tru
[message truncated]

view this post on Zulip Email Gateway (Jun 26 2023 at 10:52):

From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
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

Last updated: Apr 27 2024 at 20:14 UTC