[isabelle-dev] Strange interaction of locales and constant definitions

[Lars Noschinski]

Hi everyone,

I am encountering a very strange interaction of the definition of 
specific constants with locale declarations in HOL-Algebra (as of 
06db08182c4b; but the behaviour also seems to exist in 2013).

To reproduce this behaviour, insert the following code in 
"~~/src/HOL/Algebra/Module.thy", before the definition of the "module" 
locale:

-----------------------------------------------------------
context group begin
definition f :: "'a ⇒'a" where
    "f ≡ (λx. x (^) (0::int))"
end
-----------------------------------------------------------

(interestingly, the right hand side of the constant matters; e.g. simply 
  using "undefined" or "%x. x" will not produce an error).

When doing so, the locale declaration will throw an error:

-----------------------------------------------------------
Type unification failed

Type error in application: incompatible operand type

Operator:  smult :: (??'a, 'c, ??'b) module_scheme ⇒ ??'a ⇒ 'c ⇒ 'c
Operand:   M :: ('c, 'd) ring_scheme
-----------------------------------------------------------

It is probably relevant that both locales on which "module" depends 
depend recursively on "group".

I can recover from this error by
   - removing the stray "(structure)" declaration from M (the implicit
     argument R of cring is already a structure),
   - giving M an explicit type and
   - making R an explicit argument with an explicit type.

(The type annotations are those which are inferred automatically if I 
don't define the constant f)

I.e., if I replace the head of the locale declaration by

-----------------------------------------------------------
locale module = R: cring R + M: abelian_group M
     for M :: "('a, 'd, 'c) module_scheme"
     and R :: "('a, 'b) ring_scheme" (structure) +
-----------------------------------------------------------

the locale can be defined.

Has anybody an idea what is going on there?