CODEWITHSUNDEEP
type-inferenceisabelle
Søren Debois
Søren Debois

Reputation: 5688

Why would adding a definition change type-correctness of a locale import?

Consider this example—note that F1 and F2 are identical. 

theory Scratch  
  imports Main
begin

locale F0 =   
  fixes meaning :: ‹'model ⇒ 'a set›  ("⟦_⟧")

locale F1 = F0 +
  fixes γ :: ‹'a set ⇒ 'model›
  assumes sound: ‹L ⊆ ⟦γ L⟧›
  (* Typechecks. *)

definition (in F0) "models m L ≡ L ⊆ ⟦m⟧"  

locale F2 = F0 +
  fixes γ :: ‹'a set ⇒ 'model›
  assumes sound: ‹L ⊆ ⟦γ L⟧›
  (* Does not typecheck, see below. *)

end

The locale F2—which is the same as the well-typed F1 except we've added a definition to F0—fails type-checking with the error message: 

Type unification failed

Type error in application: incompatible operand type

Operator:  meaning :: 'a ⇒ 'b set
Operand:   γ L :: 'model

Apparently, when type-checking F2, does the type checker suddenly decide that the free type variables 'a and 'model cannot be the same thing?

Upvotes: 2

Views: 54

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8278

Isabelle tools have a tendency to ‘normalize’ the names of type variables everywhere, including locales. When they do this, all type variables get replaced by 'a, 'b, 'c, etc left-to-right. Apparently, the definition command somehow triggers this. Therefore, the 'a and 'model in F0 suddenly become 'b and 'a.

If you want to override this, you can respecify the type variables explicitly:

locale F2 = F0 meaning
  for meaning :: "'model ⇒ 'a set" +
  fixes γ :: ‹'a set ⇒ 'model›
  assumes sound: ‹L ⊆ meaning (γ L)›

or

locale F2 = F0 +
  constrains meaning :: "'model ⇒ 'a set"
  fixes γ :: ‹'a set ⇒ 'model›
  assumes sound: ‹L ⊆ meaning (γ L)›

Upvotes: 1

Related Questions