abella
abella copied to clipboard
Unexpected failure of generic type unification
Run the following script with Abella in the master branch:
Kind pair type -> type -> type.
Define map : (A -> B) -> prop by
map F.
Set types on.
Theorem map_destr_cons [A,B]: forall (F: (pair A B) -> A),
map F -> false.
induction on 1. intros. case H1.
The last case analysis fails with the following message:
Error: Unification error during case analysis: the generic type variable A cannot be instantiated; instead it is instantiated to (pair A B).
Variables:
F : (pair A B) -> A
IH : forall F, map F * -> false
H1 : map F @
============================
false
However, it is obvious the unification should have succeeded with the schematic type variables A
and B
in the definition of map
instantiated with types pair A B
and A
, respectively, in which A
and B
are generic type variables.
It seems that the type unification algorithm incorrectly conflates the schematic type variable A
in the definition of map
with the generic type variable A
in the proof.