[isabelle-dev] [isabelle] Problem "exception TYPE raised: Loose bound variable"

[Makarius]

On Tue, 15 Oct 2013, Lawrence Paulson wrote:

> It makes sense to move this discussion to the developers' list, as it 
> concerns the release candidate.

Release candidates are discussed on isabelle-users -- they are de-facto 
the release already. This problem is also present in Isabelle2013, so by 
default it is not for Isabelle2013-1 anymore, unless there is a special 
need to push it onto the train in the last moment (with the usual risks). 
Thus it is correct on isabelle-dev, which is about whatever comes after 
Isabelle2013-1.


It is not so easy to get an exception trace here.  Wrapping up 
Simplifier.generic_simp_tac as shown in the included changeset produces 
the following result:

Exception trace - TYPE ("Loose bound variable: B.7", [], [Bound 7])
Sign.type_check(2)typ_of(2)
Sign.type_check(2)typ_of(2)
Sign.type_check(2)typ_of(2)
Sign.type_check(2)typ_of(2)
Sign.type_check(2)typ_of(2)
Sign.type_check(2)
Sign.certify'(6)
Splitter().mk_case_split_tac(1)inst_lift(7)
Splitter().mk_case_split_tac(1)split_tac(2)lift_tac(1)(1)(1)(1)
Splitter().mk_case_split_tac(1)split_tac(2)lift_split_tac(1)
Splitter().mk_case_split_tac(1)split_tac(2)lift_split_tac(1)
Splitter().mk_case_split_tac(1)split_tac(2)lift_split_tac(1)
Splitter().mk_case_split_tac(1)split_tac(2)lift_split_tac(1)
Splitter().mk_case_split_tac(1)split_tac(2)lift_split_tac(1)
Splitter().mk_case_split_tac(1)split_tac(2)lift_split_tac(1)
Splitter().mk_case_split_tac(1)split_tac(2)lift_split_tac(1)
Splitter().mk_case_split_tac(1)split_tac(2)lift_split_tac(1)
Splitter().mk_case_split_tac(1)split_tac(2)lift_split_tac(1)
Splitter().mk_case_split_tac(1)split_tac(2)lift_split_tac(1)
Splitter().mk_case_split_tac(1)split_tac(2)lift_split_tac(1)
Splitter().mk_case_split_tac(1)split_tac(2)lift_split_tac(1)
Splitter().mk_case_split_tac(1)split_tac(2)lift_split_tac(1)
Splitter().mk_case_split_tac(1)split_tac(2)lift_split_tac(1)
Splitter().mk_case_split_tac(1)split_tac(2)lift_split_tac(1)
Splitter().mk_case_split_tac(1)split_tac(2)lift_split_tac(1)
Splitter().mk_case_split_tac(1)split_tac(2)lift_split_tac(1)
Splitter().mk_case_split_tac(1)split_tac(2)lift_split_tac(1)
Splitter().mk_case_split_tac(1)split_tac(2)lift_split_tac(1)
Seq.maps(2)(1)
Tactical.ORELSE(1)(1)
Tactical.ORELSE(1)(1)
Seq.maps(2)(1)
Seq.append(2)copy(1)(1)
Seq.maps(2)(1)
Simplifier.generic_simp_tac(5)(1)


So at first sight it looks like some old problem of the Splitter.


 	Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1381932466 -7200
# Node ID 7c6c3db23edb8c31d2d2e208537e14970e82a481
# Parent  eb53dc22840604cef35d0b069e7468b88fd4416c
test;

diff -r eb53dc228406 -r 7c6c3db23edb src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Oct 16 13:02:35 2013 +0200
+++ b/src/Pure/simplifier.ML	Wed Oct 16 16:07:46 2013 +0200
@@ -207,7 +207,7 @@
   in DEPTH_SOLVE (solve_tac 1) end;
 
 (*NOTE: may instantiate unknowns that appear also in other subgoals*)
-fun generic_simp_tac safe mode ctxt =
+fun generic_simp_tac' safe mode ctxt =
   let
     val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) =
       Raw_Simplifier.internal_ss (simpset_of ctxt);
@@ -220,6 +220,11 @@
       (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
   in PREFER_GOAL (simp_loop_tac 1) end;
 
+fun generic_simp_tac safe mode ctxt i st =
+  print_exception_trace General.exnMessage (fn () =>
+    let val res = Seq.pull (generic_simp_tac' safe mode ctxt i st)
+    in Seq.make (fn () => res) end);
+
 local
 
 fun simp rew mode ctxt thm =