TightTyping

Tight typing ⊢]

Set Implicit Arguments.

Require Import Coq.Program.Equality.
Require Import Definitions PreciseTyping.

Reserved Notation "G '⊢#' t ':' T" (at level 40, t at level 59).
Reserved Notation "G '⊢#' T '<:' U" (at level 40, T at level 59).

Tight typing is very similar to general typing, and could be obtained by replacing all occurrences of ⊢ with ⊢_#, except for the following:

in the type selection subtyping rules Sel-<: and <:-Sel (subtyp_sel1, subtyp_sel2) the premise is precise typing of a type declaration with equal bounds;
in the singleton subtyping rules Sngl-<: and <:-Sngl (subtyp_sngl_pq, and subtyp_sngl_qp) the premise is precise typing;
whenever a typing judgement in a premise extends the environment (for example, ty_all_intro_t), it is typed under general typing ⊢ and not tight typing ⊢_#.

Inductive ty_trm_t : ctx → trm → typ → Prop :=

(x) = T
――――――――――
⊢_# x: T

| ty_var_t : ∀ x T,
binds x T →
⊢_# tvar x : T

, x: T ⊢ t^x: U^x
x fresh
――――――――――――――――――――――――
⊢_# lambda(T)t: ∀(T)U

| ty_all_intro_t : ∀ t T U L,
    (∀ x, x \notin L →
       & x ~ T ⊢ open_trm x t : open_typ x U) →
     ⊢_# trm_val (λ (T ) t) : ∀(T ) U

⊢_# p: ∀(S)T
⊢_# q: S
―――――――――――――――
⊢ p q: T^q

| ty_all_elim_t : ∀ p q S T,
     ⊢_# trm_path p : ∀(S ) T →
     ⊢_# trm_path q : S →
     ⊢_# trm_app p q : open_typ_p q T

z; , z: T^z ⊢ ds^z :: T^z
z fresh
―――――――――――――――――――――――――――――――
⊢_# nu(T)ds :: mu(T)

| ty_new_intro_t : ∀ ds T L,
    (∀ z, z \notin L →
      z ; nil; & (z ~ open_typ z T) ⊢ open_defs z ds :: open_typ z T) →
     ⊢_# trm_val (ν (T ) ds) : μ T

⊢_# p: {a: T}
―――――――――――――
⊢_# p.a: T

| ty_new_elim_t : ∀ p a T,
⊢_# trm_path p : typ_rcd {a ⦂ T } →
⊢_# trm_path p • a : T

⊢_# p.a: T
――――――――――――――
⊢_# p: {a: T}

| ty_rec_intro_t : ∀ p a T,
⊢_# trm_path p •a : T →
⊢_# trm_path p : typ_rcd { a ⦂ T }

⊢_# t: T
, x: T ⊢ u^x: U
x fresh
――――――――――――――――
⊢_# let t in u: U

| ty_let_t : ∀ t u T U L,
     ⊢_# t : T →
    (∀ x, x \notin L →
       & x ~ T ⊢ open_trm x u : U) →
     ⊢_# trm_let t u : U

⊢_# p: q.type
⊢_# q
―――――――――――――――
⊢_# p: T

| ty_sngl_t : ∀ p q T,
     ⊢_# trm_path p : {{ q }} →
     ⊢_# trm_path q : T →
     ⊢_# trm_path p : T

⊢_# p.: T
――――――――――――――
⊢_# p: {a: T}

| ty_path_elim_t : ∀ p q a T,
     ⊢_# trm_path p : {{ q }} →
     ⊢_# trm_path q • a : T →
     ⊢_# trm_path p • a : {{ q •a }}

⊢_# p: T^p
――――――――――――
⊢_# p: mu(T)

| ty_rcd_intro_t : ∀ p T,
⊢_# trm_path p : open_typ_p p T →
⊢_# trm_path p : μ T

⊢_# p: mu(T)
――――――――――――
⊢_# p: T^p

| ty_rec_elim_t : ∀ p T,
⊢_# trm_path p : μ T →
⊢_# trm_path p : open_typ_p p T

⊢_# p: T
⊢_# p: U
――――――――――――
⊢_# p: T ∧ U

| ty_and_intro_t : ∀ p T U,
     ⊢_# trm_path p : T →
     ⊢_# trm_path p : U →
     ⊢_# trm_path p : T ∧ U

⊢_# t: T
⊢_# T <: U
―――――――――――――
⊢_# t: U

| ty_sub_t : ∀ t T U,
     ⊢_# t : T →
     ⊢_# T <: U →
     ⊢_# t : U
where "G '⊢#' t ':' T" := (ty_trm_t t T)

Tight subtyping G ⊢_# T <: U

with subtyp_t : ctx → typ → typ → Prop :=

⊢_# T <: top

| subtyp_top_t: ∀ T,
⊢_# T <: ⊤

⊢_# bot <: T

| subtyp_bot_t: ∀ T,
⊢_# ⊥ <: T

⊢_# T <: T

| subtyp_refl_t: ∀ T,
⊢_# T <: T

⊢_# S <: T
⊢_# T <: U
―――――――――――――
⊢_# S <: U

| subtyp_trans_t: ∀ S T U,
     ⊢_# S <: T →
     ⊢_# T <: U →
     ⊢_# S <: U

⊢_# T ∧ U <: T

| subtyp_and11_t: ∀ T U,
⊢_# T ∧ U <: T

⊢_# T ∧ U <: U

| subtyp_and12_t: ∀ T U,
⊢_# T ∧ U <: U

⊢_# S <: T
⊢_# S <: U
――――――――――――――――
⊢_# S <: T ∧ U

| subtyp_and2_t: ∀ S T U,
     ⊢_# S <: T →
     ⊢_# S <: U →
     ⊢_# S <: T ∧ U

⊢_# T <: U
――――――――――――――――――――――
⊢_# {a: T} <: {a: U}

| subtyp_fld_t: ∀ T U a,
⊢_# T <: U →
⊢_# typ_rcd {a ⦂ T } <: typ_rcd {a ⦂ U }

⊢_# <:
⊢_# <:
――――――――――――――――――――――――――――――――
⊢_# {A: ..} <: {A: ..}

| subtyp_typ_t: ∀ A,
     ⊢_# <: →
     ⊢_# <: →
     ⊢_# typ_rcd { A >: <: } <: typ_rcd { A >: <: }

⊢!!! p: q.type
⊢!!! q: U
――――――――――――――――――――――――――――――――
⊢_# T <: [T[q/p,n]]

| subtyp_sngl_pq_t : ∀ p q T T' U,
     ⊢!!! p : {{ q }} →
     ⊢!!! q : U →
    repl_typ p q T T' →
     ⊢_# T <: T'

⊢!!! p: q.type
⊢!!! q: U
――――――――――――――――――――――――――――――――
⊢_# T <: [T[p/q,n]]

| subtyp_sngl_qp_t : ∀ p q T T' U,
     ⊢!!! p : {{ q }} →
     ⊢!!! q : U →
    repl_typ q p T T' →
     ⊢_# T <: T'

⊢!!! p: {A: T..T}
―――――――――――――――――――
⊢_# T <: p.A

| subtyp_sel2_t: ∀ p A T ,
⊢!!! p : typ_rcd { A >: T <: T } →
⊢_# T <: p ↓ A

⊢!!! p: {A: T..T}
―――――――――――――――――――
⊢_# p.A <: T

| subtyp_sel1_t: ∀ p A T,
⊢!!! p : typ_rcd { A >: T <: T } →
⊢_# p ↓A <: T

⊢_# <:
, x: ⊢ ^x <: ^x
x fresh
――――――――――――――――――――――――
⊢_# ∀() <: ∀()

| subtyp_all_t: ∀ L,
     ⊢_# <: →
    (∀ x, x \notin L →
        & x ~ ⊢ open_typ x <: open_typ x ) →
     ⊢_# ∀() <: ∀()
where "G '⊢#' T '<:' U" := (subtyp_t T U).

Hint Constructors ty_trm_t subtyp_t.

Scheme ts_ty_trm_mut_ts := Induction for ty_trm_t Sort Prop
with ts_subtyp_ts := Induction for subtyp_t Sort Prop.
Combined Scheme ts_mutind_ts from ts_ty_trm_mut_ts, ts_subtyp_ts.

Tight typing implies general typing.

Lemma tight_to_general:
  (∀ t T,
      ⊢_# t : T →
      ⊢ t : T) ∧
  (∀ S U,
      ⊢_# S <: U →
      ⊢ S <: U).
Proof.
  apply ts_mutind_ts; intros; subst; eauto using precise_to_general3.
Qed.

TightTyping

Tight typing ⊢]

Tight subtyping G ⊢# T <: U

Tight subtyping G ⊢_# T <: U