search

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

Unexpected failure of generic type unification #142

Open yvting opened 2 years ago

yvting commented 2 years ago

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.