[isabelle-dev] [isabelle] TYPE_MATCH exception with adhoc_overloading

[Christian Sternagel]

Thanks for the valuable pointers Florian!

As far as I understand, type inference is a necessary prerequisite for 
"expand_abbrevs" (so that afterwards matching and instantiating by the 
obtained substitution suffice for getting the proper type).

Two thoughts:

1) I wouldn't want to add yet another layer of type-inference directly 
before the adhoc_overloading check. Anyway, currently it doesn't even 
seem possible to inject something after type inference but before 
expand_abbrevs.

2) Even if full type inference was done before the adhoc_overloading 
check is executed, matching alone wouldn't suffice.

The reason for 2 is that often (adhoc) overloaded constants have a very 
general type (which can't be made more specific while still supporting 
all desired variants). Consider e.g. monadic "bind", whose type is "'a 
=> ('b => 'c) => 'd" or "pure :: 'a => 'b" from Andreas' example. More 
specifically, for the term "pure id" type inference will infer type "'b" 
while the corresponding "id" has type "'a => 'a" and this instance of 
"pure" has type "('a => 'a) => 'b". Thus there is no connection between 
the domain- and range-type of "pure" whatsoever. Now the type of 
"pure_stream :: 'a1 => 'a1 stream" cannot be instantiated to "('a => 'a) 
=> 'b". Only via unification we can find that with

   "['a1 -> ('a => 'a), b' -> ('a => 'a) stream]"

we actually can insert "pure_stream" here. The problem (I think) is that 
by unification we might inject schematic type variables that stem from 
types of variants (like "'a1" above). Into the ongoing check phase whose 
context doesn't know about them.

Thus again my questions. Does this seem plausible? And is there a way to 
turn such "alien" schematic type variables into known ones?

cheers

chris

On 11/27/2014 08:50 AM, Florian Haftmann wrote:
> Hi Christian,
>
>> I'm mostly guessing here. Maybe somebody with deeper knowledge of the
>> system could comment whether this would be feasible (and also the right
>> way to go).
>
> I have not spent much thought on the code, but tried to take a bird's
> perspective.
>
> The whole matter is about overloaded abbreviations.  Hence, it's about
> abbreviation expansion intermingled with type inference.
>
> Having a look syntax_phases.ML
>
>> (* standard phases *)
>>
>> val _ = Context.>>
>>   (typ_check 0 "standard" Proof_Context.standard_typ_check #>
>>    term_check 0 "standard"
>>      (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #>
>>    term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #>
>>    term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);
>
> I see that type inference and abbreviation expansion occur on the same
> term check level.  Hence the overloading mechanisms could go here.
>
> Proof_Context.expand_abbrevs essentially boils down to Consts.certify.
>
> Maybe a comparision of these with the current implementation of
> adhoc-overloading can give some clues.
>
> Cheers,
> 	Florian
>