Re: [isabelle] TYPE_MATCH exception with adhoc_overloading

Hi Christian,

just a few weeks ago, I learned that Envir.subst_term_types is indeed the wrong function when substituting with a unifier (instead it is intended for matchers).

The right functions for unifiers in envir.ML are the ones prefixed with "norm".

Hope that helps,

On 22.11.2014 21:02, Christian Sternagel wrote:
I'm currently a bit confused by the result of "Sign.typ_unify" (or rather the result of applying the corresponding "unifier"). So maybe the problem stems from my ignorance w.r.t. to its intended result.

After applying the attached "debug" patch for the following

  consts pure :: "'a ⇒ 'b"

  definition pure_stream :: "'a ⇒ 'a stream"
  where "pure_stream = sconst"

  adhoc_overloading pure pure_stream

consts ap_stream :: "('a ⇒ 'b) stream ⇒ 'a stream ⇒ 'b stream" (infixl "◇" 70)
  consts S_stream :: "(('a ⇒ 'b ⇒ 'c) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'c) stream"

  declare [[show_variants]]

  term "pure id :: ('b ⇒ 'b) stream"

we obtain the output

oconst type: (??'a ⇒ ??'a) ⇒ ('b ⇒ 'b) stream
variant type: ?'a ⇒ ?'a stream
 {(("'a", 0), (["HOL.type"], "??'a ⇒ ??'a")),
   (("?'a", 0),
"'b"))}) (line 165 of "/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML")
("candidate term:",
 Const ("Scratch.pure_stream",
⇒ ?'a")) (line 167 of "/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML")
("after unification:",
 Const ("Scratch.pure_stream",
        "(??'a ⇒ ??'a)
         ⇒ (??'a
⇒ ??'a)")) (line 168 of "/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML")
"pure_stream id"
  :: "('a ⇒ 'a) stream"

The result of unification is a bit surprising to me, since the obtained "unifier" seems to claim that

  ('b => 'b) => ('b => 'b) stream


  (??'a => ??'a) => (??'a => ??'a) stream

are equal. What am I missing here? Maybe Envir.subst_term_types is not the way to apply the typenv obtained by typ_unify? (In this special case, if I would call subst_term_types twice with the same typenv, the result would be as I expected.)



Btw: the "delete" patch (which is to be applied before "debug") fixes a typo in the description of "no_adhoc_overloading". It is entirely unrelated to the issue at hand, but maybe somebody could apply it anyway.

On 11/21/2014 07:31 PM, Christian Sternagel wrote:
Dear Andreas,

Thanks for the report, I'll have a look. First an immediate observation:

When adding the following to Scratch.thy

declare [[show_variants]]

   fix f :: "('b ⇒ 'b ⇒ 'a) stream"
   and x :: "'b stream"
   term "pure id :: ('b => 'b) stream"

the first "term" results in

"pure_stream id"
   :: "('c ⇒ 'c) stream"

while the second results in

"pure_stream id"
   :: "('b ⇒ 'b) stream"

So it is not surprising that the first causes problems while matching.
Why, however "'c" is produced instead of "'b" is not immediately clear
to me. I'll investigate.



On 11/21/2014 04:09 PM, Andreas Lochbihler wrote:
Dear experts on adhoc overloading,

When I want to instantiate variables in a theorem using the attribute
"of", sometimes the exception TYPE_MATCH gets raised. This seems strange
to me because I would expect that adhoc_overloading either complains
about not being able to uniquely resolve an overloaded constant or
exchanges the constant in the AST.

By adding more type annotations, I have so far been able to circumvent
the exception, but there seems to be a check missing. Attached you find
a small example.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.