Re: [isabelle] Problems with coercions
> On 4 Oct 2017, at 12:31, Yamada, Akihisa <Akihisa.Yamada at uibk.ac.at> wrote:
> Dear Dmitriy,
>> It is the other way round: the show statement yields "sr :: real" annotations (since sr is fixed in the context). In the lemma statement "sr" is just a free type variable and its precise type is the result of type inference.
> ah, I see. So if I understand correctly, coercion is performed before
> the type inference, and its behavior will change when types are inferred.
Chapter 3 of the implementation manual (isabelle doc implementation) gives a high-level overview of how type checking/inference work in Isabelle. Coercion inference is implemented as a "check phase" and runs quite early in the stack of check phases. (Most check phases assume their input to be well-typed, while the coercion inference tries to repairs badly-typed terms. For well-typed terms, coercion inference behaves as plain Hindley-Milner type inference.)
>> I guess you are not surprised that the following fails (fortunately):
>> "f x = x"
>> proof -
>> define f :: "'a â 'a" where "f = id"
>> show "f x = x" unfolding f_def by simp
> Definitely not, because everyone sees that `define f' will define f. I
> hope not all Isabelle users have to understand the behavior of coercion
I'd say all users of coercions (not equal to all Isabelle users) need to understand what they are "buying into" by using coercions:
- coercion inference will not modify type-correct terms
- for not type-correct terms it will try to repair them using the coercions it knows
- in case there are different ways to repair a term, one way will be chosen (the choice depends on the input term*)
The potential ambiguity makes it necessary to carefully inspect the terms and if needed to manually adjust them by adding type annotations or coercion functions.
[*] To be very precise: the input term that coercion inference receives when the user writes a string s in the context ctxt is:
|> Syntax.parse_term ctxt
|> singleton (snd o Proof_Context.prepare_sorts ctxt)
|> singleton (fst o Type_Infer_Context.prepare_positions ctxt)
|> singleton (snd o Type_Infer_Context.prepare ctxt)
This archive was generated by a fusion of
Pipermail (Mailman edition) and