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

[Clemens Ballarin]

Hi Lars,

As already suggested, this is a limitation of parsing and type  
inference of locale expressions, which is fairly complex and the  
implementation is only a heuristic solution.  It aims at making syntax  
(in particular, definitions) from previous instances available in the  
parameter instantiation of subsequent instances.

A workaround is to make the types in the locale declaration explicit:

locale module = R: cring R + M: abelian_group M
   for R :: "('a, 'y) ring_scheme" (structure)
   and M :: "('a, 'b, 'z) module_scheme" (structure) + ...

The problem seems unrelated to overloading, for if the definition is  
changed to

context group begin
definition f :: "'a => 'a" where
    "f == (%x. inv x)"
end

it persists.  I don't know whether this can be fixed easily.

Clemens


Quoting Lars Noschinski <noschinl at in.tum.de>:

> 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?
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>