переменные типа Закрепление в расширениях локали

Question

Учитывая этот код

locale A = 
    fixes foo :: "'a" 

locale B = A + 
    fixes bar :: "'a × 'a" 

locale C' = A + 
    fixes baz :: "'a" 
begin 
    sublocale B foo "(foo, baz)". 
end 

Я получаю

Type unification failed 

Failed to meet type constraint: 

Term: (foo, baz) :: 'b × 'a 
Type: 'b × 'b 

так что кажется, что Изабель не понимает, что baz и foo должны быть одного и того же типа. Есть ли способ исправить это?

Answer 1

Проблема с вашей декларацией мест B и C. Декларация B эквивалентно следующим

locale B = A foo for foo + 
    fixes bar :: "'a * 'a" 

Locales импортирует только помнить имена параметров, но не имена переменных типа. Таким образом, как вы не указали тип для foo, наиболее общий тип для параметра B «s следующая:

foo :: 'b 
bar :: 'a * 'a 

Вы можете увидеть это с помощью команды print_locale B. То же самое происходит в декларации locale C.

Если вы хотите иметь один и тот же тип для foo и bar, вы должны сделать это явным в объявлениях локали. Есть два способа сделать это.

locale B = A foo 
    for foo :: 'a 
    + 
    fixes bar :: "'a * 'a" 

и

locale B = A + 
    constrains foo :: 'a 
    fixes bar :: "'a * 'a"