[isabelle-dev] Problem with type inference in locale expressions

[Clemens Ballarin]

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

Clemens


On 05 September, 2014 20:12 CEST, Florian Haftmann <florian.haftmann at 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.haftmann at 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-dev at 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