Aladdin Proposals about portfolio HOT 1 OPEN

module TC.

from Std import Aladdin.MetaAladdin as MA.

data ty : * where
  all : (ty -> ty) -> ty.
  arr : ty -> ty -> ty.

data tm : * where
  abs : (tm -> tm) -> tm.
  app : tm -> tm -> tm.
  let : tm -> (tm -> tm) -> tm.

check (let Rhs Body) Tau :-
  MA.runMeta (MA.mkNewVar (Sigma0\ MA.solve (check Rhs Sigma0) (Res Sigma0))),
  -- Res := Sigma0\ sigma (Alpha_1\ ... sigma (Alpha_n\ Sigma = Gen Alpha_1 ... Alpha_n)) for some skeleton Gen 
  generalize (Res _) Scheme,
  -- Scheme := all (Alpha_1\ ... all (Alpha_n\ Gen Alpha_1 ... Alpha_n))
  pi (X\ check X Scheme => check (Body X) Tau).