meta
   (description (
      'Use\sa\sContext\sto\sinfer\sthe\stype\sof\san\sexpression.
   ))
;
infer-expr := λ(: tctx TContext)(: term AST)(: scoped IsScoped)(: hint Type)(: used IsUsed). (: (
   (match term (
      ()
      ( ASTNil (ascript-normal( term (t1 'Nil_s) )) )
      ( ASTEOF (ascript-normal( term (t1 'Nil_s) )) )
      ( (Seq( l r )) (
         (infer-expr( tctx l Unscoped TAny Used ))
         (infer-expr( tctx r Unscoped TAny Used ))
      ))
      ( (Typedef( _ _ )) () )
      ( (Glb( k v )) (
         (if (is-open(typeof term)) () (
            (infer-expr( tctx v Unscoped TAny Used ))
         ))
      ))
      ( (Frg( _ v )) (
         (ascript-normal( v (typeof term) ))
      ))
      ( (App( (Lit( ':_s _ )) (App( (Lit( _ _ )) (AType tt) )) )) (
         (match term (
            ()
            ( (App( _ (App( t _ )) )) (
               (match (slot( tt 'String_s )) (
                  ()
                  ( (TGround( 'String_s _ )) () )
                  ( _ (infer-expr( tctx t Unscoped tt used )) )
               ))
               (let inner-tt (typeof t))
               (if (non-zero inner-tt) (
                  (set tt (and( tt inner-tt )))
               ) (
                  (ascript-normal( t tt ))
               ))
               (ascript-normal( term tt ))
            ))
         ))
      ))
      ( (App( (Lit( ':_s _ )) (App( t (AType tt) )) )) (
         (set tctx (infer-expr( tctx t Unscoped tt used )))
         (let inner-tt (typeof t))
         (if (non-zero inner-tt) (
            (let nn (with-only-representation inner-tt))
            (if (non-zero nn) (
               (let tt-2 (and(
                  tt
                  nn
               )))
               (set tt tt-2)
            ) ())
            (ascript-normal( t tt ))
            (ascript-normal( term tt ))
            (match term (
               ()
               ( (App( las ras )) (
                  (ascript-normal( las tt ))
                  (ascript-normal( ras tt ))
               ))
            ))
         ) ())
      ))
      ( (App( (Var( 'gensym-label_s _ )) (Var( lname _ )) )) (
         (set tctx (TCtxBind(
            (close tctx) lname (t1 'Label_s) ASTEOF
         )))
         (ascript-normal( term (t1 'Nil_s) ))
      ))
      ( (App( (App( (Var( 'set_s _ )) (Var( v _ )) )) rhs )) (
         (infer-expr( tctx rhs Unscoped TAny Tail ))
         (ascript-normal( rhs (typeof-var( term tctx v )) ))
         (ascript-normal( term (t1 'Nil_s) ))
      ))
      ( (App( (Var( 'label_s _ )) (Var( lname _ )) )) (
         (ascript-normal( term (t1 'Nil_s) ))
      ))
      ( (App( (App( (App( (Var( 'if_s _ )) cond )) t )) f )) (
         (if (is( scoped Scoped )) (
            (let tctx-inner (infer-expr( tctx cond Unscoped TAny Used )))
            (infer-expr( tctx-inner t Unscoped TAny Tail ))
         ) (
            (set tctx (infer-expr( tctx cond Unscoped TAny Used )))
            (set tctx (infer-expr( tctx t Unscoped TAny Tail )))
         ))
         (infer-expr( tctx f Unscoped TAny Tail ))
         (ascript-normal( term (guess-representation(without-representation(typeof t))) ))
      ))
      ( (App( (App( (Var( 'while_s _ )) cond )) body )) (
         (set tctx (infer-expr( tctx cond Unscoped TAny Used )))
         (infer-expr( tctx body Unscoped TAny Tail ))
         (ascript-normal( term (t1 'Nil_s) ))
      ))
      ( (App( (Var( 'as_s _ )) (App( t (AType tt) )) )) (
         (set tctx (infer-expr( tctx t Unscoped TAny used )))
         (let inner-tt (typeof t))
         (match t (
            ()
            ( (Lit( l _ )) (
               (if (is-reg8 l) (set inner-tt (t1 'Reg8_s)) ())
               (if (is-reg16 l) (set inner-tt (t1 'Reg16_s)) ())
               (if (is-reg32 l) (set inner-tt (t1 'Reg32_s)) ())
               (if (is-reg64 l) (set inner-tt (t1 'Reg64_s)) ())
            ))
            ( _ () )
         ))
         (if (non-zero inner-tt) (
            (let inner-repr (with-only-representation inner-tt))
            (if (non-zero inner-repr) (
               (set tt (and( tt inner-repr )))
            ) ())
            (if (non-zero(slot( tt 'AsOnly_s ))) () (
               (let inner-class (with-only-class inner-tt))
               (if (non-zero inner-class) (
                  (set tt (and( tt inner-class )))
               ) ())
               (set tt (with-fields( tt )))
            ))
            (ascript-normal( term tt ))
         ) ())
      ))
      ( (App( (Var( 'sizeof_s _ )) (AType _) )) (
         (let tt (as-constant(parse-type 'U64_s)))
         (ascript-normal( term tt ))
         (match term (
            ()
            ( (App( s _ )) (ascript-normal( s tt )) )
         ))
      ))
      ( (App( (Var( 'scope_s _ )) r )) (
         (infer-expr( tctx r Scoped TAny Tail ))
         (ascript-normal( term (typeof r) ))
      ))
      ( (App( (Var( 'open_s _ )) r )) (
         (set tctx (infer-expr( tctx r Unscoped TAny Used )))
         (let deref-type (typeof r))
         (match (slot( deref-type 'Array_s )) (
            ()
            ( (TGround( 'Array_s (LCons( _ (LCons( TAny LEOF )) )) )) () )
            ( (TGround( 'Array_s (LCons( TAny (LCons( array-base LEOF )) )) )) (
               (set deref-type (and( array-base (t1 'StackVariable_s) )))
            ))
            ( _ () )
         ))
         (ascript-normal( term deref-type ))
      ))
      ( (App( (Abs( (Var( lname _ )) ASTNil tlt )) rhs )) (
         (let prev-tt (typeof-var-raw( term tctx lname )))
         (if (non-zero prev-tt) (
            (if (not(is-arrow prev-tt)) (
               (exit-error( 'Variable\sName\sIs\sAlready\sBound\sIn\sOuter\sScope_s term ))
            ) ())
         ) ())
         (infer-expr( tctx rhs Unscoped TAny Tail ))
         (let tt (typeof rhs))
         (let rt (as-local-variable tt))
         (if (non-zero tt) () (
            (exit-error( 'Unable\sto\sinfer\stype\sof\sexpression_s rhs ))
         ))
         (if (non-zero rt) () (
            (exit-error( 'Unable\sto\sinfer\stype\sof\sexpression_s rhs ))
         ))
         (match term (
            ()
            ( (App( (Abs( lname-var _ _ )) _ )) (
               (ascript-normal( lname-var rt ))
            ))
         ))
         (set tctx (TCtxBind(
            (close tctx) lname rt ASTEOF
         )))
         (ascript-normal( term (t1 'Nil_s) ))

         (apply-or-cons-and-specialize(
            'del_s
            (typeof-var-raw( term tctx 'del_s ))
            rt
            term
         ))
      ))
      ( (App( l r )) (
         (let l-used Unused)
         (if (is( used Call )) (set l-used Call) ())
         (let r-used Used)
         (if (is( used Unused )) (set r-used Unused) ())
         (set tctx (infer-expr( tctx l Unscoped TAny l-used )))
         (if (is-arrow(typeof l)) (set r-used Call) ())
         (set tctx (infer-expr( tctx r Unscoped TAny r-used )))
         (let rt (apply-or-cons-and-specialize(
            (var-name-if-var l)
            (typeof l)
            (typeof r)
            term
         )))
         (if (is( l-used Unused )) (
            (set rt (implicit-tail rt))
         ) ())
         (ascript-normal( term rt ))
         (if (==( (var-name-if-var l) 'Rc_s )) (
            (apply-or-cons-and-specialize(
               'inc_s
               (typeof-var-raw( term tctx 'inc_s ))
               (t2( 'Rc_s (p2(slot( (p2(slot( (p1 (typeof r)) 'Array_s ))) 'Tuple_s ))) )) # invert Rc constructor to get type parameter
               term
            ))
         ) ())
      ))
      ( (Abs( lhs rhs tlt )) (
         (set tctx (infer-ctx( tctx lhs )))
         (infer-expr( tctx rhs Unscoped TAny Tail ))
         (let lt (typeof-lhs lhs))
         (let rt (typeof rhs))
         (ascript-normal( term (enrich( (t3( 'Arrow_s lt rt )) tlt )) ))
      ))
      ( (Var( v vtk )) (
         (let vt (typeof-var( term tctx v )))
         (ascript-normal( term (typeof-var( term tctx v )) ))
      ))
      ( (Lit( l _ )) (
         (if (non-zero(typeof term)) () (
            (let tt (typeof-tag l))
            (if (non-zero tt) (
               (if (non-zero hint) (
                  (set tt (unify-hint( hint tt )))
               ) ())
               (ascript-normal( term tt ))
            ) ())
         ))
      ))
      ( (Meta( _ )) (ascript-normal( term (t1 'Nil_s) )) )
      ( _ (
         (print 'Unknown\sTerm\sIn\sType\sInference\n_s)
         (print term)
         (print '\n_s)
         (exit 1_u64)
      ))
   ))
   tctx
) TContext);