Shadowing of type variables is problematic in static semantics

[jaccokrijnen]

Consider this term

const x y = x

Implemented in PIR like this:

(Λ(α : *) λ(x : α) Λ(α : *) λ(y : α). x)

Apply this to arguments:

  (Λ(α : *) λ(x : α) Λ(α : *) λ(y : α). x) String "foo" Bool True

it should have type String

However, the inner derivation looks like

  --------------------------------------- T-Var
  [α : * , α : *] ; [y: α, x : α] ⊢ x : α
  ----------------------------------------------
  [α : * , α : *] ; [x : α] ⊢ λ(y : α) . x : α -> α
  ----------------------------------------------
  [α : *] ; [x : α] ⊢ Λα. λ(y : α). x : ∀α. α -> α
  ----------------------------------------------------
                      ... 
  --------------------------------------------------------------------
    ⊢ (Λ(α : *) λ(x : α) Λ(α : *) λ(y : α). x) : ∀α. (α -> (∀α. α -> α))          !!! this type is wrong, the rightmost α refers to the shadowed α
  --------------------------------------------------------------------------
    ⊢ (Λ(α : *) λ(x : α) Λ(α : *) λ(y : α). x) String : (String -> (∀α. α -> α))
  --------------------------------------------------------------------------
    ⊢ (Λ(α : *) λ(x : α) Λ(α : *) λ(y : α). x) String "foo" Bool : Bool -> Bool
  --------------------------------------------------------------------------
    ⊢ (Λ(α : *) λ(x : α) Λ(α : *) λ(y : α). x) String "foo" Bool True : Bool

[jaccokrijnen]

Ilya Sergey mentioned they had found a similar problem in the type checker of Scilla: https://icfp22.sigplan.org/details/icfp-2022-papers/33/Random-Testing-of-a-Higher-Order-Blockchain-Language

[jaccokrijnen]

This must be solved before, it's regular system F anyways.

[jaccokrijnen]

Possible solutions

• In T_TyAbs require $\alpha \notin FV(\Gamma)$, i.e. alpha may not occur in any term's type in gamma (requires #8 , lists for envs)
• In T_TyAbs require $\forall x \in FV(t). \alpha \notin FV(\Gamma(x))$, more expensive than 1, but does not require #8
• Just don't allow tyvar shadowing in $\Gamma$, does not require #8

[jaccokrijnen]

I was writing a small proof of concept in Coq to demonstrate the problem

WIP:

From PlutusCert Require Import
  PlutusIR
  Static.
Import NamedTerm.
From Coq Require Import
  Strings.String.

Local Open Scope string_scope.
Definition t := TyAbs "α" Kind_Base (LamAbs "x" (Ty_Var "α") (TyAbs "α" Kind_Base (Var "x"))).
Definition t_ty :=
  Ty_Forall "α" Kind_Base (
    Ty_Fun
      (Ty_Var "α")
      (Ty_Forall "α" Kind_Base
        (Ty_Var "α")
      )
  ).

Lemma t_typing : empty,, empty |-+ t : t_ty.
Proof.
  unfold t, t_ty.
  apply T_TyAbs.
  apply T_LamAbs.
    - eauto with typing.
    - eauto with typing.
    - apply T_TyAbs.
      eapply T_Var.
      + cbn. reflexivity.
      + eauto with typing.
Qed.

Definition Ty_int : Ty := Ty_Builtin (Some (TypeIn DefaultUniInteger)).
Definition Ty_bool : Ty := Ty_Builtin (Some (TypeIn DefaultUniBool)).
Definition t_true : Term := Constant (Some (ValueOf DefaultUniBool true)).

Definition t' := TyInst (Apply (TyInst t Ty_bool) (t_true)) (Ty_int).

Lemma t'_typing : empty,, empty |-+ t' : Ty_int.
Proof with eauto with typing.
  unfold t'.
  eapply T_TyInst...
  - eapply T_Apply...
    eapply T_TyInst...
    + apply t_typing...
    + apply N_TyBuiltin.
    + simpl.

[jaccokrijnen]

I now wonder what type preservation theorem would look like, because then we could prove "foo" : Bool by reducing this program:

  (Λ(α : *) λ(x : α) Λ(α : *) λ(y : α). x) String "foo" Bool True

TODO: figure out if there is a type preservation/subject reduction proof in Joris' work, and if that makes any assumptions to avoid this case.

Perhaps it uses this axiom:

• There is this axiom https://github.com/jaccokrijnen/plutus-cert/blob/3085ba37d7e95061594b3ddf41c455880388d9f3/src/Language/PlutusIR/Semantics/Misc/Axiom.v#L8 , which would directly contradict with the above term.