Require Import List.

Inductive pure_term : Type :=
  | pure_var : nat -> pure_term
  | pure_app : pure_term -> pure_term -> pure_term
  | pure_abs : pure_term -> pure_term.

Inductive poly_type : Type :=
  | poly_var : nat -> poly_type
  | poly_arr : poly_type -> poly_type -> poly_type
  | poly_abs : poly_type -> poly_type.

Definition environment := list poly_type.

Definition funcomp {X Y Z} (g : Y -> Z) (f : X -> Y) :=
  fun x => g (f x).

Definition scons {X: Type} (x : X) (xi : nat -> X) :=
  fun n => match n with | 0 => x | S n => xi n end.

Fixpoint ren_poly_type (xi : nat -> nat) (s : poly_type) : poly_type :=
  match s return poly_type with
  | poly_var x => poly_var (xi x)
  | poly_arr s t => poly_arr (ren_poly_type xi s) (ren_poly_type xi t)
  | poly_abs s => poly_abs (ren_poly_type (scons 0 (funcomp S xi)) s)
  end.

Fixpoint subst_poly_type (sigma : nat -> poly_type) (s : poly_type) : poly_type :=
  match s return poly_type with
  | poly_var s => sigma s
  | poly_arr s t => poly_arr (subst_poly_type sigma s) (subst_poly_type sigma t)
  | poly_abs s => poly_abs (subst_poly_type (scons (poly_var 0) (funcomp (ren_poly_type S) sigma)) s)
  end.

Inductive type_assignment : environment -> pure_term -> poly_type -> Prop :=
| type_assignment_var {Gamma x t} :
    nth_error Gamma x = Some t ->
    type_assignment Gamma (pure_var x) t
| type_assignment_app {Gamma M N s t} :
    type_assignment Gamma M (poly_arr s t) -> type_assignment Gamma N s ->
    type_assignment Gamma (pure_app M N) t
| type_assignment_abs {Gamma M s t} :
    type_assignment (s :: Gamma) M t ->
    type_assignment Gamma (pure_abs M) (poly_arr s t)
| type_assignment_inst {Gamma M s t} :
    type_assignment Gamma M (poly_abs s) ->
    type_assignment Gamma M (subst_poly_type (scons t poly_var) s)
| type_assignment_gen {Gamma M s} :
    type_assignment (map (ren_poly_type S) Gamma) M s ->
    type_assignment Gamma M (poly_abs s).

Definition SysF_TC : environment * pure_term * poly_type -> Prop :=
  fun '(Gamma, M, t) => type_assignment Gamma M t.

Definition SysF_TYP : pure_term -> Prop :=
  fun M => exists Gamma t, type_assignment Gamma M t.

Definition SysF_INH : environment * poly_type -> Prop :=
  fun '(Gamma, t) => exists M, type_assignment Gamma M t.