[isabelle-dev] auto raises a TYPE exception

[Makarius]

On Wed, 29 May 2013, Makarius wrote:

> Without the latter, src/HOL/Metis_Examples/Clausification.thy crashes at 
> the very end, due to divergence of types of certain Vars, types that 
> cannot be unified.  This is very odd, but should not be a problem at the 
> moment: Metis should work as before.

Just for completeness, here is the original crash of Metis proof 
reconstruction at Isabelle/0fa3b456a267:

   lemma ex_tl: "EX ys. tl ys = xs"
     using tl.simps(2) by fast

   lemma "(∃ys∷nat list. tl ys = xs) ∧ (∃bs∷int list. tl bs = as)"
     by (metis ex_tl)

Metis: Failed to replay Metis proof
inst_inference: ("COMP", 1,
                  ["Meson.skolem (Meson.COMBK (tl ((?MesonSK_0_0_0_ys1∷nat 
list ⇒ nat list) (xs∷nat \
list)) = xs) (0∷nat)) ⟹
                    tl ((?MesonSK_0_0_0_ys1∷int list ⇒ int list) 
(?MesonV_0_1_0_xs1∷int list)) = (as\
∷int list) ⟹ False"
                     [.],
                   "PROP ?psi2 ⟹ PROP ?psi2"])

The failure of COMP is via cterm_instantiate/instantiate_normalize: after 
the instantiation, there are ?ys1 of different types, so the extra type 
unification of Vars in COMP will fail.

(Note that the pretty-printed exception content is produced via regular 
and documented @{make_string} sneaked into the proper spot in the ML code, 
without committing that.  Many people only know the "secret" 
PolyML.makestring, with its unformatted text-only output.)


In 6ba76ad4e679 this crash is avoided: already incremented composition 
problems omit the extra type unification, just like plain resolution. This 
merely pushed the inherent problem elsewhere, so in 568b2cd65d50 
resolve_inc_tyvars is back where types of equal Vars are *not* unified, 
despite its lengthy workaround for exactly that.


 	Makarius