Hi Clemens, > This is what I expected. Type inference of locale expressions is inherently heuristic and probably you are hitting this. (This could be verified further with a stack trace). For more background, see also this earlier message: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-February/003821.html
thanks for that hint.
The problem the class target faces is to determine the so called base
sort of the class specification, i.e. the sort that is inferred for the
type parameter 'a from the import *and* the fixes/assumes as given by
the user. For this I cannot fix 'a in the first place.
I think I can circumvent this problem by adding a suitable plugin to the
term/type check phase. Let's see…
Best,
Florian
>
> Clemens
>
>
> On 05 September, 2014 20:12 CEST, Florian Haftmann
> <florian.haftm...@informatik.tu-muenchen.de> wrote:
>
>>> Is this a regression in the type inference of locale expressions, or has it
>>> always (i.e. since 2009) been like this?
>>
>> Using the attached retrofitted theory, the same behaviour occurs:
>>
>>> $ /opt/Isabelle2009/Isabelle2009/bin/isabelle tty
>>>> val it = () : unit
>>> val commit = fn : unit -> bool
>>> Welcome to Isabelle/HOL (Isabelle2009: April 2009)
>>>> theory Foo imports Class_Clash begin
>>> Loading theory "Class_Clash"
>>> parameters
>>> f :: "'a => 'a => 'a"
>>> constants
>>> F :: "'a => 'a => 'a"
>>> parameters
>>> f :: "'a => 'a => 'a"
>>> constants
>>> F :: "'a => 'a => 'a"
>>> "plus"
>>> :: "'a => 'a => 'a"
>>> "inf"
>>> :: "'b => 'b => 'b"
>>> "plus"
>>> :: "'a => 'a => 'a"
>>> "inf"
>>> :: "'a => 'a => 'a"
>>> "plus"
>>> :: "'a => 'a => 'a"
>>> "inf"
>>> :: "'a => 'a => 'a"
>>> *** Type unification failed
>>> *** Type error in application: Incompatible operand type
>>> ***
>>> *** Operator: op = inf :: ('b => 'b => 'b) => bool
>>> *** Operand: plus :: 'a => 'a => 'a
>>> ***
>>> *** At command "locale" (line 64 of "/data/tum/drawer/thy/Class_Clash.thy").
>>>> Error - Database is not opened for writing.
>>>> val it = () : unit
>>
>> There is strong evidence that it has always been like this.
>>
>> Shall I just chance my luck and dive into the sources?
>>
>> Cheers,
>> Florian
>>
>>
>>>
>>> On 04 September, 2014 09:21 CEST, Florian Haftmann
>>> <florian.haftm...@informatik.tu-muenchen.de> wrote:
>>>
>>>> At d6a2e3567f95, I am currently analysing a problem with type inference
>>>> in locale expressions: when leaving types implicit, imported parameters
>>>> are given disjoint types despite they could be unified, and are so if
>>>> given explicit type annotations. The problem occurs if the imported
>>>> locales themselves have dependencies on other locales containing a
>>>> definition.
>>>>
>>>> The reason why this is really annyoing is that it breaks certain class>>
>>>> specifications to typecheck and currently effectively prevents me from>>
>>>> adding such a simple thing as product over lists.
>>>>
>>>> See attached theory for quite minimal examples.
>>>>
>>>> I will have to investigate this further.
>>>>
>>>> Florian
>>>>
>>>> --
>>>>
>>>> PGP available:
>>>> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>>>
>>>
>>>
>>>
>>>
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-...@in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>
>>
>> --
>>
>> PGP available:
>> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>
>
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
