Email Gateway (Aug 19 2022 at 08:24): Email Gateway (Aug 19 2022 at 08:24):From: Peter Lammich <lammich@in.tum.de>
Hi all,
upon interpreting a locale, I get the following error:
interpretation StdMap hm_ops
*** exception TYPE raised (line 414 of "type.ML"):
*** Type variable "?'a" has two distinct sorts
*** ?'a\<Colon>type
*** ?'a\<Colon>hashable
whereas interpretation StdMap lm_ops works as expected.
term hm_ops
:: "('a, 'b, ('a, 'b) HashMap.hashmap) map_ops"
where 'a is of sort hashable (Not displayed, even with show_sorts?)
term lm_ops
:: "('a, 'b, ('a, 'b) assoc_list) map_ops"
where 'a has no sort constraints.
Boiling down to a simple example seems to be difficult. The error seems
to be triggered by a sublocale relation that I introduced. Moreover, the
term "StdMap hm_ops" is type-correct, and actually proven as a lemma.
If anyone has an idea what it is, or has experienced a similar behaviour
and knows what it is, please respond ... otherwise I will invest
probably quite much time to boil it down to a simple example that I can
post on the list.
Last updated: May 01 2024 at 20:18 UTC