[isabelle-dev] Type error in metis call with Toplevel.debug

[Makarius]

> On 12 Jun 2009, at 12:46, Alexander Krauss wrote:
>
>> Andy Schropp found the following weird behaviour, which seems to be both in 
>> Isabelle2009 and the current developer version (reproduced in 
>> b63d253ed9e2).
>> 
>> Steps to reproduce:
>> 
>> - Starting from Pure or HOL-Plain, load List.thy in PG
>> - Enable Toplevel.debug
>> - The metis call in lemma "sorted_distinct_set_unique", fails with
>> 
>> *** exception TERM raised: fastype_of: expected function type
>> 
>> When Toplevel.debug is switched off then it works, so my guess is that it 
>> is related to the pretty printing of some of the debug messages, but I am 
>> not sure.
>> 
>> Any ideas? Anybody inclined to debug this further?

Since Toplevel.debug is already enabled, you merely need to inspect the 
exception trace (which only appears in the *isabelle* buffer in Proof 
General).

Exception trace for exception - TERM

Term.fastype_of1(2)
Pattern.match(3)
Pattern.rewrite_term(4)rew(1)/2
Pattern.rewrite_term(4)rew(1)
Pattern.rewrite_term(4)rew1(3)
Pattern.rewrite_term(4)rew2(3)
Pattern.rewrite_term(4)rew1(3)
Pattern.rewrite_term(4)
List.map(2)
Overloading.improve_term_uncheck(2)
Library.perhaps_loop(1)(1)
Syntax.gen_check(4)
MetisTools.fol_terms_to_hol(2)
...

This reveals that Overloading.improve_term_uncheck essentially assumes a 
well-typed term, because it uses Pattern.rewrite_term.  This assumption is 
a bit strong: even if one would basically expect that only well-typed 
terms are printed, the perhaps_loop/uncheck phase can gradually remove 
type information, so any participant needs to be ready to operate on 
partially typed terms.  See also contract_abbrevs in 
src/Pure/Isar/proof_context.ML as a more robust example.


On Mon, 15 Jun 2009, Lawrence Paulson wrote:

> The offending code is here:
>
> fun fol_terms_to_hol ctxt fol_tms =
>   let val ts = map (fol_term_to_hol_RAW ctxt) fol_tms
>       val _ = Output.debug (fn () => "  calling type inference:")
>       val _ = app (fn t => Output.debug (fn () => Syntax.string_of_term ctxt 
> t)) ts
>       val ts' = infer_types ctxt ts;
>       val _ = app (fn t => Output.debug
>                     (fn () => "  final term: " ^ Syntax.string_of_term ctxt 
> t ^
>                               "  of type  " ^ Syntax.string_of_typ ctxt 
> (type_of t)))
>                   ts'
>   in  ts'  end;
>
> We call the function Syntax.string_of_term on a list of terms ts prior 
> to type inference, so it is unsurprising that some of these terms are 
> not type correct. In fact, the only surprise is that we don't get an 
> error message more often. I was under the impression that that 
> particular function did not perform type-checking. Is there a more 
> appropriate function to call?

We did get similar problems occasionally, when trace_simp or debug_simp 
attempt to output terms that "normally" do not occur in user space.

The general observation is that debug code is very hard to get right, and 
it is better deleted as soon as possible.  Note that global Output.debug 
is particularly bad as a permanent tracing facility, because it will 
interfere with any debugging that users attempt out there. (The Metis 
linkup is particularly verbose, and many people have already asked about 
these odd messages that usually occur without context.  In the worst case 
there will be even a denial-of-service in Proof General.)


 	Makarius