[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.