Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] exception TYPE when instantiating type variabl...

Email Gateway (Jan 24 2024 at 19:18):

From: Kevin Kappelmann <kevin.kappelmann@tum.de>
Dear list,

I am using a tactic that, among other things, instantiates type
variables. Unfortunately, it seems that the instantiation of type
variables as part of an Isar proof raises TYPE exceptions ("Variable has
two distinct types") in some cases. Below, you can find a minimal example.

The exception is not raised by the tactic itself, as illustrated in the
minimal example. I suspect it is raised at some outer layer (maybe the
Isar toplevel?). I know very little of this side of Isabelle and find it
very difficult to debug. Any help would be greatly appreciated!

Isabelle version: f1f08ca40d96 (development version)

Best wishes,

Kevin

theory Scratch
   imports Pure
begin

declare [[show_types, show_sorts, show_hyps]]
ML‹
   val inst_tac = Thm.instantiate
     (TVars.make [((("'a", 0), []), @{ctyp prop})], Vars.empty) #>
Seq.single
›

schematic_goal "PROP ((?f :: ?'a ⇒ _) (x :: ?'a))"
   (*this works*)
   ML_val‹@{Isar.goal} |> #goal |> inst_tac |> Seq.list_of›
   (*exception TYPE raised (line 116 of "envir.ML"): Variable has two
distinct types*)
   apply (tactic ‹inst_tac›)
   oops

schematic_goal "PROP ((f :: ?'a ⇒ _) (x :: ?'a))"
   (*in contrast, this works*)
   apply (tactic ‹inst_tac›)
   oops

end

Email Gateway (Jan 25 2024 at 13:04):

From: Kevin Kappelmann <kevin.kappelmann@tum.de>
I was reminded that there is an ML exception trace option. Enabling it
provides me with the following output, indicating a problem in
Proof_Display.pretty_goal_inst:

Exception trace - exception TYPE raised (line 116 of "envir.ML"):
Variable has two distinct types
Envir.var_clash (line 115 of "envir.ML")
Envir.lookup_check (line 118 of "envir.ML")
Envir.subst_term2(2)subst (line 361 of "envir.ML")
Same.commit (line 33 of "General/same.ML")
Proof_Display.pretty_goal_inst(3)prt_inst(1)inst (line 280 of
"Isar/proof_display.ML")
Proof_Display.pretty_goal_inst(3)prt_inst (line 265 of
"Isar/proof_display.ML")
Proof_Display.pretty_goal_inst (line 261 of "Isar/proof_display.ML")
Proof.pretty_state(1)prt_goal (line 380 of "Isar/proof.ML")
Proof.pretty_state (line 373 of "Isar/proof.ML")
Toplevel.pretty_state (line 239 of "Isar/toplevel.ML")
_-(4)(1)(1) (line 484 of "PIDE/command.ML")
Command.make_print(8)process(1)(1) (line 327 of "PIDE/command.ML")

Email Gateway (Jan 29 2024 at 11:34):

From: Makarius <makarius@sketis.net>

On 24.01.24 20:17, Kevin Kappelmann wrote:

I am using a tactic that, among other things, instantiates type variables.
Unfortunately, it seems that the instantiation of type variables as part of
an Isar proof raises TYPE exceptions ("Variable has two distinct types") in
some cases. Below, you can find a minimal example.

The exception is not raised by the tactic itself, as illustrated in the
minimal example. I suspect it is raised at some outer layer (maybe the Isar
toplevel?). I know very little of this side of Isabelle and find it very
difficult to debug. Any help would be greatly appreciated!

Isabelle version: f1f08ca40d96 (development version)

```isabelle

theory Scratch
   imports Pure
begin

declare [[show_types, show_sorts, show_hyps]]
ML‹
   val inst_tac = Thm.instantiate
     (TVars.make [((("'a", 0), []), @{ctyp prop})], Vars.empty) #> Seq.single
›

schematic_goal "PROP ((?f :: ?'a ⇒ _) (x :: ?'a))"
   (this works)
   ML_val‹@{Isar.goal} |> #goal |> inst_tac |> Seq.list_of›
   (*exception TYPE raised (line 116 of "envir.ML"): Variable has two
distinct types*)
   apply (tactic ‹inst_tac›)
   oops

schematic_goal "PROP ((f :: ?'a ⇒ _) (x :: ?'a))"
   (in contrast, this works)
   apply (tactic ‹inst_tac›)
   oops

end

```

ch

Last updated: Apr 29 2024 at 04:18 UTC