Re: [isabelle] TYPE_MATCH exception with adhoc_overloading



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]]

notepad
begin
  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.

cheers

chris

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.

Best,
Andreas




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