[isabelle-dev] quickcheck throws "Type unification failed: No type arity t :: full_exhaustive" on simple example
Fabian Huch
huch at in.tum.de
Mon Jun 26 12:36:00 CEST 2023
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
More information about the isabelle-dev
mailing list