Email Gateway (Aug 19 2022 at 11:46): Email Gateway (Aug 19 2022 at 11:46):From: Makarius <makarius@sketis.net>
On Thu, 12 Sep 2013, Peter Lammich wrote:
I encountered the following strange behaviour
term "(\<exists>a::_::order. a\<le>a) \<and> (\<exists>b::_::type. b=b)"
*** Inconsistent sort constraints for type variable "'_dummy_"
*** At command "term"However,
term "(\<exists>a::_. a\<le>a) \<and> (\<exists>b::_::type. b=b)"works as expected, and yields:
"(\<exists>a\<Colon>'a\<Colon>ord. a \<le> a) \<and> (\<exists>b
\<Colon>'b\<Colon>type. b = b)"
:: "bool"What has happened here.
That is indeed a bit strange. After some hours of studying the sources
and the history the explanation is as follows:
Dummy type variables with sort constraints were introduced in 2000 for
Isabelle99-1 -- back then a quick and easy "feature" addition.
12 years later, Isabelle2012 clarified the handling of sort constraints as
follows (see NEWS):
* Sort constraints are now propagated in simultaneous statements, just
like type constraints. INCOMPATIBILITY in rare situations, where
distinct sorts used to be assigned accidentally. For example:
lemma "P (x::'a::foo)" and "Q (y::'a::bar)" -- "now illegal"
lemma "P (x::'a)" and "Q (y::'a::bar)"
-- "now uniform 'a::bar instead of default sort for first occurrence (!)"
This improvement on one side disrupted the simplistic implementation of
dummy type variables on the other side. You can toss a coin which is the
"bug" and which the "feature", but these words are meaningless anyway.
Old things often need the environment to act in an old way.
And why does the second example work at all?
Dummy types "_" are quite different from dummy type variables "_::sort".
The former are used all the time, the latter hardly at all.
Why are type constraints checked before dummy-patterns are
instantiated?
Because the system is so complex that its complexity is hard to grasp, and
it is very hard to change without breaking anything else, even for myself.
Nonetheless, I count this as minor incident, and don't see a reason to
remove that old feature. In the next release the dummy type variables
should work better again.
Anyway, just by accident I've come across the very existence of that half
forgotten thing just recently, but removed the dummies by plain named type
variables for clarity. (These were regular toplevel theorem statements,
without any special requirements.)
So just for curiosity, what are your applications where the dummies with
sorts make a difference?
Makarius
Email Gateway (Aug 19 2022 at 12:00):From: Peter Lammich <lammich@in.tum.de>
Hi all,
I encountered the following strange behaviour (also in isabelle-dev
2b68f4109075):
term "(\<exists>a::_::order. a\<le>a) \<and> (\<exists>b::_::type. b=b)"
*** Inconsistent sort constraints for type variable "'_dummy_"
*** At command "term"
However,
term "(\<exists>a::_. a\<le>a) \<and> (\<exists>b::_::type. b=b)"
works as expected, and yields:
"(\<exists>a\<Colon>'a\<Colon>ord. a \<le> a) \<and> (\<exists>b
\<Colon>'b\<Colon>type. b = b)"
:: "bool"
What has happened here. Why are type constraints checked before
dummy-patterns are instantiated? And why does the second example work at
all?
Last updated: Apr 16 2024 at 20:15 UTC