[isabelle-dev] [isabelle] TYPE_MATCH exception with adhoc_overloading
c.sternagel at gmail.com
Mon Dec 1 13:56:01 CET 2014
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).
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
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?
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
> 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.
More information about the isabelle-dev