Ill-typed code with schematic polymorphism

[RandomActsOfGrammar]

We can write ill-typed code which Abella accepts by using a polymorphic type constructor.

Some definitions to provide types to demonstrate the issue:

Kind aty   type.  Type a   aty.
Kind bty   type.  Type b   bty.

The code showing the actual issue:

Kind typeHider   type.
Type typeHider_c   A -> typeHider.

Define hideType : A -> typeHider -> prop by
   hideType X (typeHider_c X).

Define hiderHelper : aty -> bty -> prop by
  hiderHelper A B := hideType A (typeHider_c B).

By using hideType to produce a typeHider_c, we are able to use a term of type aty (the variable B) as the second argument of hiderHelper, which is supposed to take a term of type bty.

If Abella disallowed constructors having type variables in argument types which don't appear in the type being built, I don't think it would be possible to build ill-typed code like this. We would not be able to write the typeHider_c constructor because A does not occur in typeHider, and typeHider_c is what lets us hide the true type of B.

[chaudhuri]

Sorry for the long delay with this. I think this is an interesting issue with polymorphism that I remember discussing with Andrew, Gopalan, Yuting the last time I was in Minneapolis. I believe at that point I was convinced that we would need some kind of range restriction for type arguments. However, Yuting ended up implementing a version without the restriction. Maybe this is explained in the paper Yuting and Gopalan wrote about schematic polymorphism?

Ping @yvting, @gnadathur97.

[yvting]

Given a definition, the type variables in its type are schematic over its entire body. Such a schematic definition represents an infinite set of definitions obtained by instantiating the type variables with ground types.

The example above can be restated as follows where the scope of type variables is made explicit:

Define hideType [A] : A -> typeHider -> prop by
   hideType X (typeHider_c X).

Here, the type variable A ranges over a single clause. Note that in the current implementation we implicitly derive schematic type variables from types and do not allow this form of definitions. This can be changed if people think the explicit syntax will improve readability.

With regards to the example, I do not see any ill-typed code. Once hideType is defined, it may be freely used in other schematic definitions as long as its occurrences are well-typed. This is the case for the occurrence of hideType in hideHelper which has a type instance aty -> typeHider -> prop.

Also notice that the constant typeHider_c has different type instances in hideType and hiderHelper. The former is A -> typeHider (this A is the schematic type variable of hideType), while the latter is bty -> typeHider.

Finally, because the types of A and B are different while the single definitional clause of hideType only allows such occurrences of variables to have the same type, we can prove that hiderHelper never holds:

Theorem hiderHelper_false: forall A B,
  hiderHelper A B -> false.
intros.
  case H1.
  case H2.