From 42da18cf3aebd2a97b22452c75d40d5a583d5271 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Mon, 4 Mar 2024 14:30:58 +0100
Subject: [PATCH] Reference a bug in polymorphic class implementation

---
 .../Test_Polymorphic_Classes.thy              | 20 +++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy b/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy
index 0d5aa30..0814421 100644
--- a/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy
+++ b/Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy
@@ -693,4 +693,24 @@ lemma*[e5::E] testtest : "xx + testtest_level = yy + testtest_level \<Longrighta
 text\<open>Indeed this fails:\<close>
 (*lemma*[e6::E] testtest : "xx + the (level @{test2 \<open>testtest2''\<close>}) = yy + the (level @{test2 \<open>testtest2''\<close>}) \<Longrightarrow> xx = yy" by simp*)
 
+text\<open>Bug: Checking of text* type against declare_reference is not done.
+Should be compatible with type unification mechanism. See the record package\<close>
+doc_class 'a AAA_test =
+aaa::"'a list"
+
+doc_class 'a BBB_test =
+bbb::"'a list"
+
+declare_reference*[aaa_test::"'a::one AAA"]
+text\<open>@{AAA (unchecked) \<open>aaa_test\<close>}\<close>
+
+text\<open>bbb_test should fails and trigger an error \<close>
+text*[bbb_test::"'a::one BBB"]\<open>\<close>
+
+text*[aaa_test::"int AAA"]\<open>\<close>
+
+text\<open>bbb_test should fails and trigger an error \<close>
+text*[aaa_test'::"string AAA"]\<open>\<close>
+
+
 end
\ No newline at end of file