# [isabelle] Weird error with locale interpretation

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.
--
Peter
p.s.
Here is the trace for the exception, but I don't know how to interpret
it, not why it stops at Locale.roundup, that does not contain a call to
Type.tvar_clash where the exception comes from.
Locale.roundup(8)dependencies'-(2)
List.filter(2)
List.filter(2)
List.filter(2)
List.filter(2)
List.filter(2)
List.filter(2)
List.filter(2)
List.filter(2)
List.filter(2)
List.filter(2)
List.filter(2)
List.filter(2)
List.filter(2)
List.filter(2)
List.filter(2)
List.filter(2)
List.filter(2)
List.filter(2)
Locale.roundup(8)
o(2)(1)
Expression.prep_full_context_statement(15)prep_insts_cumulative(6)
Expression.prep_full_context_statement(15)
Expression.prep_full_context_statement(1)(1)(1)(1)(1)(1)(1)(1)(1)(1)(1)(1)
Expression.prep_goal_expression(4)
Expression.prep_goal_expression(1)(1)(1)
Expression.gen_interpretation(6)
Toplevel.theory_to_proof(1)(1)(1)
Toplevel.begin_proof(1)(1)(1)

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*