
typecheck-subtypes                       := ();
typecheck-context                        := ();
typecheck-constructors                   := ();
typecheck-types-have-changed             := ();
typecheck-global-context                 := ();
typecheck-size                           := ();
typecheck-fragment-types                 := ();

typecheck := λprogram . (tail(
   (local p)
   (set p program)
   (local ordered-type-exprs)
   (set ordered-type-exprs ())
   (while p (tail(
      (set ordered-type-exprs (ordered-type-exprs (tail p)))
      (set p (head p))
   )))
   (while ordered-type-exprs (tail(
      (typecheck-infer-type-expr( (tail ordered-type-exprs) ))
      (set ordered-type-exprs (head ordered-type-exprs))
   )))
   (set typecheck-types-have-changed True)
   (while typecheck-types-have-changed (tail(
      (set typecheck-types-have-changed ())
      (typecheck-infer-prog program)
   )))
   (typecheck-assert-complete program)
   (debug-memory-usage 'typecheck)
   program
));

typecheck-assert-complete := λp . (if p (tail(
   (typecheck-assert-complete( head p ))
   (typecheck-assert-expr( tail p ))
)) ());

typecheck-assert-one := λe . (
   (if (typecheck-lookup e) () (tail(
      (print-s (typecheck-show-ascript parse-parsed-program))(print-s \n)
      (fail (UnableToInferTypeOfExpression (typecheck-show-ascript e)))
   )))
);

typecheck-assert-expr := λe . (tail(
   (match e (
      ()
      ( () () )
      ( (GExpr ge) (
         (typecheck-assert-expr( ge ))
      ))
      ( (Global( 'main (Lambda( lhs rhs )) )) (
         (typecheck-assert-expr( rhs ))
      ))
      ( (Global( gln gle )) (
         (typecheck-assert-expr( gle ))
      ))
      ( (Type( l ds )) ())
      ( (Fragment( fln fle )) ())
      ( Nil (
         (typecheck-assert-one( e ))
      ))
      ( (App( (Lambda( (Variable lname) Nil )) rhs )) (
         (typecheck-assert-expr( rhs ))
         (typecheck-assert-one( e ))
      ))
      ( (App( (Variable 'gensym-label) _ )) (
      ))
      ( (App( (Variable 'label) (Variable l) )) (
      ))
      ( (App( (App( (Variable 'while) cond )) body )) (tail(
         (typecheck-assert-expr( cond ))
         (typecheck-assert-expr( body ))
         (typecheck-assert-one( e ))
      )))
      ( (App( (App( (App( (Variable 'if) cond )) t )) f )) (tail(
         (typecheck-assert-expr( cond ))
         (typecheck-assert-expr( t ))
         (typecheck-assert-expr( f ))
         (typecheck-assert-one( e ))
      )))
      ( (App( (App( (Variable 'set) (Variable lhs) )) rhs )) (
         (typecheck-assert-expr( rhs ))
         (typecheck-assert-one( e ))
      ))
      ( (App( (App( (Literal ':) (Literal _) )) tt )) (
         (typecheck-assert-one( e ))
      ))
      ( (App( (Variable 'sizeof) (Literal tt) )) (
         (typecheck-assert-one( e ))
      ))
      ( (App( (App( (Literal ':) te )) tt )) (
         (typecheck-assert-expr( te ))
         (typecheck-assert-one( e ))
      ))
      ( (App( (App( (Variable 'as) te )) tt )) (
         (typecheck-assert-expr( te ))
         (typecheck-assert-one( e ))
      ))
      ( (Literal lit) (
         (typecheck-assert-one( e ))
      ))
      ( (App( (Variable 'tail) (App( l r )) )) (tail(
         (typecheck-assert-expr( r ))
         (typecheck-assert-expr( l ))
         (typecheck-assert-one( e ))
      )))
      ( (App( (Variable 'maybe-deref) r )) (tail(
         (typecheck-assert-expr( r ))
         (typecheck-assert-one( e ))
      )))
      ( (App( l r )) (
         (typecheck-assert-expr( r ))
         (typecheck-assert-expr( l ))
         (typecheck-assert-one( e ))
      ))
      ( (Lambda( lhs rhs )) (
         (typecheck-assert-expr( rhs ))
         (typecheck-assert-one( e ))
      ))
      ( (Variable v) (
         (typecheck-assert-one( e ))
      ))
      ( u (fail (UnknownAssertTyped u)) )
   ))
));

typecheck-lookup := λterm . (tail(
   (local tctx)
   (set tctx typecheck-context)
   (local found)
   (local ttt)
   (while tctx (tail(
      (set ttt (head tctx))
      (if (is( (head ttt) term )) (tail(
         (set found (tail ttt))
         (set tctx ())
      )) (
         (set tctx (tail tctx))
      ))
   )))
   found
));

typecheck-deep-eq := λt1 t2 . if (is( t1 t2 )) True (match (t1 t2) (
   ()
   ( (() ()) True )
   ( ( (And(l1 l2)) (And(r1 r2)) ) True )
   ( ( (And(l1 l2)) r ) (
      if (typecheck-deep-eq(l1 r)) True
         (typecheck-deep-eq(l2 r))
   ))
   ( ( l (And(r1 r2)) ) (
      if (typecheck-deep-eq(l r1)) True
         (typecheck-deep-eq(l r2))
   ))
   ( ((l1 l2) (r1 r2)) (
      if (typecheck-deep-eq(l1 r1))
         (typecheck-deep-eq(l2 r2))
         ()
   ))
   ( (l r) (eq( l r )) )
));

typecheck-assert-not-nil := λt whole-tt tt . (match tt (
   ()
   ( (lt rt) (tail(
      (typecheck-assert-not-nil( t whole-tt lt ))
      (typecheck-assert-not-nil( t whole-tt rt ))
   )))
   ( () (tail(
      (fail (Type Was Nil whole-tt t))
   )))
   ( _ ())
));

typecheck-sizeall := λtt . (match (typecheck-slot( tt Sized )) (
   ()
   ( (Sized _) tt )
   ( _ (tail(
      (local size)
      (set size (typecheck-sizeof tt))
      (set tt (typecheck-sizeall-children tt))
      (if size (
         (And( tt (Sized size) ))
      ) tt)
   )))
));
typecheck-sizeall-children := λtt . (match tt (
   ()
   ( (Array( bt sz )) (Array( (typecheck-sizeall bt) sz )))
   ( (lt rt) ( (typecheck-sizeall-children lt) (typecheck-sizeall-children rt) ))
   ( _ tt )
));

typecheck-ascript := λt tt . (tail(
   (if tt (tail(
      (typecheck-assert-not-nil( t tt tt ))
      (local lt)
      (set lt (typecheck-lookup t))
      (if lt (
         (if (typecheck-deep-eq( lt tt )) () (
            fail (TypeAscriptionInequality lt tt t)
         ))
      ) (
         (set tt (typecheck-sizeall tt))
         (set typecheck-context ((t tt) typecheck-context))
         (set typecheck-types-have-changed True)
      ))
   )) ())
   t
));

typecheck-show-ascript := λp . (tail(
   (local term)
   (set term (match p (
      ()
      ( () () )
      ( Nil p )
      ( (Variable _) p )
      ( (Literal _) p )
      ( (App( f x )) (
         (App( (typecheck-show-ascript f) (typecheck-show-ascript x) ))
      ))
      ( (Lambda( lhs rhs )) (
         (Lambda( (typecheck-show-ascript lhs) (typecheck-show-ascript rhs) ))
      ))
      ( (prog (GExpr( g ))) (
         ( (typecheck-show-ascript prog) (GExpr( typecheck-show-ascript g )) )
      ))
      ( (prog (Global( n v ))) (
         ( (typecheck-show-ascript prog) (Global( n (typecheck-show-ascript v) )) )
      ))
      ( (prog (Type( tn td ))) (
         ((typecheck-show-ascript prog) (Type( tn td )))
      ))
      ( (prog (Fragment( (Variable fragf) body ))) (
         (typecheck-show-ascript prog)
      ))
      ( (prog (Fragment( typf body ))) (
         (typecheck-show-ascript prog)
      ))
      ( unknown (
         fail (UnknownTerm unknown)
      ))
   )))

   (local type)
   (set type (typecheck-lookup p))
   (if type (
      (if (eq( type '? )) (
         term
      ) ( 
         (:( term type ))
      ))
   ) (
      term
   ))
));

typecheck-infer-prog := λp . (
   (while p (tail(
      (typecheck-infer-expr( () (tail p) Used ))
      (set p (head p))
   )))
);

typecheck-infer-ctx := λctx e . (match e (
   ()
   ( (App( (App( (Literal :) (Variable v) )) tt )) (
      (ctx (v (And( LocalVariable (typecheck-infer-type-compound tt) )) ))
   ))
   ( (App( ps (App( (App( (Literal :) (Variable v) )) tt )) )) (
      ( (typecheck-infer-ctx( ctx ps )) (v (And( LocalVariable (typecheck-infer-type-compound tt) )) ))
   ))
   ( (Variable v) (
      (ctx (v S))
   ))
   ( (App( ps (Variable v) )) (
      ( (typecheck-infer-ctx( ctx ps )) (v S))
   ))
   ( Nil (
      ctx
   ))
   ( u (
      fail (UnknownLhsInferCtx u)
   ))
));

typecheck-typeof-gvar := λv . (tail(
   (local gctx)
   (set gctx typecheck-global-context)
   (local tt)
   (while gctx (tail(
      (match (tail gctx) (
         ()
         ( (Global( gn gt )) (
            (if (eq( v gn )) (
               (if tt (
                  (set tt (And(tt gt)) )
               ) (
                  (set tt gt)
               ))
            ) ())
         ))
      ))
      (set gctx (head gctx))
   )))
   tt
));

typecheck-typeof-var := λctx v . (match ctx (
   ()
   ( () (typecheck-typeof-gvar v) )
   ( (cs (cv ct)) (
      if (eq( v cv )) (
         ct
      ) (
         (typecheck-typeof-var( cs v ))
      )
   ))
));

typecheck-typeof-lhs := λlhs . (match lhs (
   ()
   ( (App( (App( (Literal :) (Variable v) )) tt )) (
      (typecheck-infer-type-compound tt)
   ))
   ( (App( ps (App( (App( (Literal :) (Variable v) )) tt )) )) (
      (Cons( (typecheck-typeof-lhs ps) (typecheck-infer-type-compound tt) ))
   ))
   ( (Variable v) (
      S
   ))
   ( (App( ps (Variable v) )) (
      (Cons( (typecheck-typeof-lhs ps) S ))
   ))
   ( Nil (
      Nil
   ))
   ( u (
      fail (UnknownLhsTypeofLhs u)
   ))
));

typecheck-unify-sub := λctx v . (match ctx (
   ()
   ( Accept v )
   ( (Bind( s1 s2 )) (
      if (eq( v s1 )) s2 v
   ))
   ( (ctxl ctxr) (tail(
      (local lv)
      (set lv (typecheck-unify-sub( ctxl v )))
      (local rv)
      (set rv (typecheck-unify-sub( ctxr v )))
      (if (is( lv v )) (
         (if (is( rv v )) () (set v rv))
      ) (set v lv))
      v
   )))
));

typecheck-unify-ctx := λctx v . (match v (
   ()
   ( (vl vr) (tail(
      (set v ( (typecheck-unify-ctx( ctx vl )) (typecheck-unify-ctx( ctx vr )) ))
      v
   )))
   ( _ (tail(
      (set v (typecheck-unify-sub( ctx v )))
      v
   )))
));

typecheck-unify-implies := λlt rt . (if (eq(lt rt)) True (match lt (
   ()
   ( (And( lt1 lt2 )) (
      (if (typecheck-unify-implies( lt1 rt )) True (
         (typecheck-unify-implies( lt2 rt ))
      ))
   ))
   ( lt1 (tail(
      (local accept)
      (local subtypes)
      (local st)
      (set subtypes typecheck-subtypes)
      (while subtypes (tail(
         (set st (tail subtypes))
         (if (eq( (head st) lt1 )) (
            (if (eq( (tail st) rt )) (
               (set accept True)
            ) ())
         ) ())
         (set subtypes (head subtypes))
      )))
      accept
   )))
)));

# rt must imply lt, rt is realized, lt is expected
typecheck-unify-args := λlt rt . (tail(
   (local result)
   (set result (typecheck-unify-args-inner( lt rt )))
   result
));

typecheck-unify-args-inner := λlt rt . (match (lt rt) (
   ()
   ( ( (And( lt1 lt2 )) rt ) (
      (match ( (typecheck-unify-args(lt1 rt)) (typecheck-unify-args(lt2 rt)) ) (
         ()
         ( (() _) () )
         ( (_ ()) () )
         ( (lctx rctx) (lctx rctx) )
      ))
   ))
   ( ( lt (And( rt1 rt2 )) ) (
      (match ( (typecheck-unify-args(lt rt1)) (typecheck-unify-args(lt rt2)) ) (
         ()
         ( (() ()) () )
         ( (() ctx) ctx )
         ( (ctx ()) ctx )
         ( (lctx rctx) (lctx rctx) )
      ))
   ))
   ( ((lt1 rt1) (lt2 rt2)) (
      (match ( (typecheck-unify-args(lt1 lt2)) (typecheck-unify-args(rt1 rt2)) ) (
         ()
         ( (() _) () )
         ( (_ ()) () )
         ( (lctx rctx) (lctx rctx) )
      ))
   ))
   ( (a1 a2) (
      (if (typecheck-unify-implies( a2 a1 )) ( # argument type must imply parameter type
         Accept
      ) (
         (if (is-variable a1) (
            (if (is-variable a2) (
               Accept
            ) (
               (Bind( a1 a2 ))
            ))
         ) (
            (if (is-variable a2) (
               (Bind( a2 a1 ))
            ) (
               ()
            ))
         ))
      ))
   ))
   (_ (tail(
      (fail (UnknownUnify lt rt))
      '?
   )))
));

typecheck-apply-plural := λmany pt . (match many(
   ()
   ( (And( t1 t2 )) (tail(
      (local r)
      (set r (typecheck-apply-plural( t1 pt )))
      (if r r (typecheck-apply-plural( t2 pt )))
   )))
   ( ('->(lt rt)) (tail(
      (local result)
      (local ctx)
      (set ctx (typecheck-unify-args(lt pt)))
      (if ctx (
         (set result (typecheck-unify-ctx( ctx rt )))
      ) ())
      result
   )))
   ( u ())
));

typecheck-safe-apply-plural := λterm many pt . (tail(
   (local r)
   (set r (typecheck-apply-plural( many pt )))
   (if r r (tail(
      (print-s TypeError)(print-s \s)(print-s InvalidArgument)(print-s \n)
      (print-s Argument:)(print-s \n)
      (print-s \t)(print-s pt)(print-s \n)
      (print-s Candidates:)(print-s \n)
      (while many (match many (
         ()
         ( (And( lmt rmt )) (tail(
            (print-s \t)(print-s rmt)(print-s \n)
            (set many lmt)
         )))
         ( mt (tail(
            (print-s \t)(print-s mt)(print-s \n)
            (set many ())
         )))
      )))
      (print-s Term:)(print-s \n)
      (print-s \t)(print-s term)(print-s \n)
      (exit 1)
   )))
));

typecheck-infer-type-compound := λcompound . (tail(
   (local result)
   (set result (match compound (
      ()
      ((Literal tt) (parse-type tt))
      ((Variable tt) (parse-type tt))
      ( (App( (Literal And) (App( lt rt )) )) (
         (And( (typecheck-infer-type-compound lt) (typecheck-infer-type-compound rt) ))
      ))
      ( (App( (Literal Array) (App( lt rt )) )) (
         (Array( (typecheck-infer-type-compound lt) (typecheck-infer-type-compound rt) ))
      ))
      ((App( (App( lt (Literal ',) )) rt )) (Cons( (typecheck-infer-type-compound lt) (typecheck-infer-type-compound rt) )) )
      ((App( (Literal lt) rt )) ( lt (typecheck-infer-type-compound rt) ) )
      ((App( lt rt )) (Cons( (typecheck-infer-type-compound lt) (typecheck-infer-type-compound rt) )) )
      (u (fail (UnknownTypeCompound u)))
   )))
   result
));

typecheck-is-constructor := λtt . (match tt (
   ()
   ( (And( lt rt )) (
      if (typecheck-is-constructor lt) True
         (typecheck-is-constructor rt)
   ))
   ( () () )
   ( (_ _) () )
   ( ta (typecheck-is-constructor-atom ta))
));
typecheck-is-constructor-atom := λta . (tail(
   (local is-constructor)
   (local constructors)
   (set constructors typecheck-constructors)
   (while constructors (tail(
      (if (eq( (head(tail constructors)) ta )) (
         (set is-constructor True)
      ) ())
      (if (eq( (tail(tail constructors)) ta )) (
         (set is-constructor True)
      ) ())
      (set constructors (head constructors))
   )))
   is-constructor
));

typecheck-infer-type-constructor := λbase-type body . (match body (
   ()
   ( (Literal tag) (tail(
      (set typecheck-constructors ( typecheck-constructors (tag base-type) ))
      8
   )))
   ( (App( (Literal tag) args )) (tail(
      (local ctype)
      (set ctype (typecheck-infer-type-compound args))
      (set typecheck-constructors ( typecheck-constructors (tag ('->(ctype (And( base-type tag )) ))) ))
      (local size)
      (set size (i2s(add( (s2i 8) (s2i( typecheck-sizeof ctype )) ))) )
      size
   )))
   ( () 0 )
   ( u ( fail (UnknownTypeConstructor u)))
));

typecheck-infer-type-definition := λbase-type def . (match def (
   ()
   ( (App( (App( tds (Variable '|) )) body )) (max(
      (typecheck-infer-type-definition( base-type tds ))
      (typecheck-infer-type-constructor( base-type body ))
   )))
   ( body (
      (typecheck-infer-type-constructor( base-type body ))
   ))
));

typecheck-infer-constructor-type := λtag . (tail(
   (local ctype)
   (local constructors)
   (set constructors typecheck-constructors)
   (while constructors (tail(
      (if (eq( tag (head(tail(constructors))) )) (
         (if ctype (
            (set ctype (And( ctype (tail(tail(constructors))) )))
         ) (
            (set ctype (tail(tail(constructors))))
         ))
      ) ())
      (set constructors (head constructors))
   )))
   ctype
));

typecheck-set-size := λ tt sz . (if sz (tail(
   (local sizes)
   (local has-size)
   (while sizes (tail(
      (if (deep-eq( (head (tail sizes)) tt )) (
         (set has-size True)
      ) ())
      (set sizes (head sizes))
   )))
   (if has-size () (
      (if (eq( sz Unsized )) (
         (set typecheck-size ( typecheck-size ( tt () )))
      ) (
         (set typecheck-size ( typecheck-size ( tt sz )))
      ))
   ))
)) ());

typecheck-repr := λsz . (match (typecheck-sizeof sz) (
   ()
   ( 1 Reg8 )
   ( 2 Reg16 )
   ( 4 Reg32 )
   ( 8 Reg64 )
   ( _ LocalVariable)
));

typecheck-infer-type-expr := λe . (match e (
   ()
   ( (Type( l ds )) (
      (local base-type)
      (set base-type (typecheck-infer-type-compound l))
      (local sz)
      (set sz (typecheck-infer-type-definition( base-type ds )))
      (if (typecheck-is-fragment base-type) () (
         (typecheck-set-size( base-type sz ))
      ))
      (typecheck-ascript( e '? ))

      (local constructors)
      (set constructors typecheck-constructors)
      (while constructors (tail(
         (match (tail constructors) (
            ()
            ( (tag ('->(ctype (And( my-type tag )) ))) (tail(
               (if (deep-eq( my-type base-type )) (tail(
                  (typecheck-set-size( tag sz ))
                  (if (typecheck-is-fragment base-type) () (
                     (typecheck-annotate-accessors( base-type tag ctype ))
                  ))
               )) ())
            )))
            ( (tag my-type) (tail(
               (if (deep-eq( my-type base-type )) (tail(
                  (typecheck-set-size( tag sz ))
                  (if (typecheck-is-fragment base-type) () (
                     (typecheck-annotate-accessors( base-type tag () ))
                  ))
               )) ())
            )))
         ))
         (set constructors (head constructors))
      )))
   ))
   ( (Global( 'main (Lambda( _ _ )) )) (tail(
      (set typecheck-global-context ( typecheck-global-context (Global( 'argc (parse-type 'U64+GlobalVariable) )) ))
      (set typecheck-global-context ( typecheck-global-context (Global( 'argv (parse-type 'String[?]+GlobalVariable) )) ))
   )))
   ( (Global( gln (Lambda( glp (App( (App( (Literal ':) _ )) rtype )) )) )) (tail(
      (local lt)
      (set lt (typecheck-typeof-lhs glp))
      (local rt)
      (set rt (typecheck-as-return (typecheck-infer-type-compound rtype)))
      (set typecheck-global-context ( typecheck-global-context (Global( gln ('->( lt rt )) )) ))
      (typecheck-ascript( e ('->( lt rt )) ))
   )))
   ( (Fragment( (Variable fln) (Lambda( flp (App( (App( (Literal ':) _ )) rtype )) )) )) (tail(
      (local lt)
      (set lt (typecheck-typeof-lhs flp))
      (local rt)
      (set rt (typecheck-infer-type-compound rtype))
      (set typecheck-global-context ( typecheck-global-context (Global( fln ('->( lt rt )) )) ))
   )))
   ( (Fragment( (Variable gln) (Lambda( _ _ )) )) (tail(
      (fail (Global Fragments Must Be Annotated gln))
   )))
   ( (Global( gln (App( (App( (Literal ':) body )) tt )) )) (tail(
      (set tt (typecheck-infer-type-compound tt))
      (set tt (And( (typecheck-not-representation tt) GlobalVariable )))
      (set typecheck-global-context ( typecheck-global-context (Global( gln tt )) ))
      (typecheck-ascript( e tt ))
   )))
   (_ ())
));



typecheck-annotate-accessors := λ base-type tag fields-type . (tail(
   (set fields-type (Cons( fields-type U64 )))
   (local field-number)
   (while fields-type (match fields-type (
      ()
      ( (Cons( lt rt )) (tail(
         (if field-number (
            (set base-type tag)
         ) ())
         (set typecheck-global-context ( typecheck-global-context (
            (Global( (clone-rope( '. (i2s field-number) )) ('->( base-type (And( rt (typecheck-repr rt) )) )) ))
         )))
         (set field-number (inc field-number))
         (set fields-type lt)
      )))
      ( tt (tail(
         (if field-number (
            (set base-type tag)
         ) ())
         (set typecheck-global-context ( typecheck-global-context (
            (Global( (clone-rope( '. (i2s field-number) )) ('->( base-type (And( tt (typecheck-repr tt) )) )) ))
         )))
         (set fields-type ())
      )))
   )))
));

typecheck-infer-expr := λctx e used . (tail(
   (match e (
      ()
      ( () () )
      ( (GExpr ge) (
         (typecheck-infer-expr( ctx ge Unused ))
      ))
      ( (Type( l ds )) ())
      ( (Global( 'main (Lambda( lhs rhs )) )) (
         (typecheck-infer-expr( ctx rhs Used ))
      ))
      ( (Global( gln gle )) (
         (typecheck-ascript( gle (typecheck-lookup e) ))
         (typecheck-infer-expr( ctx gle Used ))
      ))
      ( (Fragment( fln fle )) (
         (match fle (
            ()
            ( (Lambda( lhs (App( (App( (Literal ':) rhs )) rhst )) )) (
               (set rhst (typecheck-infer-type-compound rhst))
               (local flt)
               (set flt ('->( (typecheck-typeof-lhs lhs) rhst )) )
               (typecheck-ascript( fle flt ))
            ))
         ))
      ))
      ( Nil (
         (typecheck-ascript( e Nil ))
      ))
      ( (App( (Variable 'gensym-label) (Variable lname) )) (
         (set ctx ( ctx (lname (And( Constant Label ))) ))
         (typecheck-ascript( e Nil ))
      ))
      ( (App( (Variable 'label) (Variable lname) )) (
         (typecheck-ascript( e Nil ))
      ))
      ( (App( (App( (Literal ':) (Literal maybe-tag) )) tt )) (
         (local ctype)
         (local mtype)
         (set mtype (typecheck-infer-type-compound tt))
         (set ctype (typecheck-infer-constructor-type maybe-tag))
         (if ctype (
            (set mtype (And( mtype maybe-tag )))
         ) ())
         (typecheck-ascript( (tail (tail (head (tail e)))) (And( Constant mtype )) ))
         (typecheck-ascript( e (And( Constant mtype )) ))
      ))
      ( (App( (App( (Literal ':) asc )) tt )) (
         (typecheck-infer-expr( ctx asc used ))
         (typecheck-ascript( asc (typecheck-infer-type-compound tt) ))
         (typecheck-ascript( e (typecheck-infer-type-compound tt) ))
      ))
      ( (App( (App( (Variable 'as) asc )) tt )) (
         (typecheck-infer-expr( ctx asc used ))
         (local asc_t)
         (set asc_t (typecheck-lookup asc))
         (if asc_t (
            (typecheck-ascript( e
               (typecheck-as( asc_t (typecheck-infer-type-compound tt) ))
            ))
         ) ())
      ))
      ( (Literal lit) (
         (local ctype)
         (set ctype (typecheck-infer-constructor-type lit))
         (if ctype (
            (typecheck-ascript( e (And( (And( lit ctype )) Constant )) ))
         ) (
            (typecheck-ascript( e Atom ))
         ))
      ))
      ( (App( (App( (Variable 'set) (Variable lhs) )) rhs )) (tail(
         (typecheck-infer-expr( ctx rhs Used ))
         (typecheck-ascript( e Nil ))
      )))
      ( (App( (Variable 'sizeof) (Literal tt) )) (tail(
         (typecheck-ascript( e (parse-type( U64+Literal+Constant )) ))
      )))
      ( (App( (App( (App( (Variable 'if) cond )) t )) f )) (tail(
         (set ctx (typecheck-infer-expr( ctx cond Used )))
         (set ctx (typecheck-infer-expr( ctx t Used )))
         (typecheck-infer-expr( ctx f Used ))
         (typecheck-ascript( e (typecheck-lookup t) ))
      )))
      ( (App( (App( (Variable 'while) cond )) body )) (
         (typecheck-infer-expr( ctx cond Used ))
         (typecheck-infer-expr( ctx body Unused ))
         (typecheck-ascript( e Nil ))
      ))
      ( (App( (Variable 'tail) (App( l r )) )) (tail(
         (set ctx (typecheck-infer-expr( ctx l Unused )))
         (set ctx (typecheck-infer-expr( ctx r used )))
         (if (typecheck-lookup r) (
            (typecheck-ascript( e (typecheck-lookup r) ))
         ) ())
      )))
      ( (App( (Variable 'maybe-deref) r )) (tail(
         (set ctx (typecheck-infer-expr( ctx r used )))
         (local rtype)
         (set rtype (typecheck-lookup r))
         (if rtype (
            (match (typecheck-slot( (typecheck-lookup r) Array )) (
               ()
               ( (Array( x '? )) (
                  (if (typecheck-unify-implies( x '? )) () (
                     (set rtype x)
                  ))
               ))
            ))
            (typecheck-ascript( e rtype ))
         ) ())
      )))
      ( (App( (Lambda( (Variable lname) Nil )) rhs )) (tail(
         (set ctx (typecheck-infer-expr( ctx rhs Used )))
         (if (typecheck-lookup rhs) (
            (set ctx ( ctx (lname (And( LocalVariable (typecheck-not-representation (typecheck-lookup rhs)) )) ) ))
         ) (
            (set ctx ( ctx (lname ()) ))
         ))
         (typecheck-ascript( e Nil ))
      )))
      ( (App( l r )) (tail(
         (set ctx (typecheck-infer-expr( ctx l used )))
         (set ctx (typecheck-infer-expr( ctx r used )))
         (match ( (typecheck-slot( (typecheck-lookup l) '-> )) (typecheck-lookup r) ) (
            ()
            ( (() _) () )
            ( (_ ()) () )
            ( ( ('->(lt rt)) pt ) (
               (typecheck-ascript( e (typecheck-safe-apply-plural( e (typecheck-lookup l) pt )) ))
            ))
            ( (lt rt) (
               (typecheck-ascript( e (Cons(lt rt)) ))
            ))
         ))
      )))
      ( (Lambda( lhs rhs )) (tail(
         (set ctx (typecheck-infer-ctx( ctx lhs )))
         (typecheck-infer-expr( ctx rhs Used ))
         (match (typecheck-lookup rhs) (
            ()
            ( () () )
            ( rt (
               (typecheck-ascript( e ('->( (typecheck-typeof-lhs lhs) (typecheck-as-return rt) )) ))
            ))
         ))
      )))
      ( (Variable v) (
         (match (typecheck-typeof-var( ctx v )) (
            ()
            ( () () )
            ( tt (typecheck-ascript( e tt )) )
         ))
      ))
      ( u (fail (UnknownTerm u)) )
   ))
   ctx
));

typecheck-sizeof := λtt . (tail(
   (local sz)
   (set sz (typecheck-sizeof-impl tt))
   sz
));
typecheck-sizeof-impl := λtt . (match tt (
   ()
   ( Nil 0 )
   ( '? () )
   ( 'Label () )
   ( 'Literal () )
   ( 'Constant () )
   ( 'LocalVariable () )
   ( 'GlobalVariable () )
   ( 'StackVariable () )
   ( 'BranchConditional () )
   ( (Array( bt '? )) 8 )
   ( (Array( bt sz )) (
      (i2s(mul(
         (s2i (typecheck-sizeof bt))
         (s2i sz)
      )))
   ))
   ( (And( lt rt )) (tail(
      (local sz)
      (set sz (typecheck-sizeof lt))
      (if sz () (set sz (typecheck-sizeof rt)))
      sz
   )))
   ( (Cons( lt rt )) (
      (i2s(add(
         (s2i(max( 8 (typecheck-sizeof( lt )) )))
         (s2i(max( 8 (typecheck-sizeof( rt )) )))
      )))
   ))
   ( (Sized sz) sz )
   ( ('->(_ _)) () )
   ( (lt rt) (fail (UnexpectedSizeof tt)))
   ( () () )
   ( _ (tail(
      (if (typecheck-is-cyclical( tt () )) (
         (fail (TypeIsCyclical tt))
      ) ())
      (local sz)
      (local sizes)
      (set sizes typecheck-size)
      (while sizes (tail(
         (if (eq( (head (tail sizes)) tt )) (
            (set sz (tail (tail sizes)))
         ) ())
         (set sizes (head sizes))
      )))
      sz
   )))
));

typecheck-assign-representation := λtt . (tail(
   (print-s (AssignRepr tt))(print-s \n)
   (if (not(typecheck-has-representation tt)) (
      (set tt (And( LocalVariable tt )))
      (print-s (Repr tt))(print-s \n)
   ) ())
   tt
));

typecheck-has-representation := λtt . (match tt (
   ()
   ( (lt rt) (
      if (typecheck-has-representation lt) True
         (typecheck-has-representation rt)
   ))
   ( () () )
   ( Constant True )
   ( Reg8 True )
   ( Reg16 True )
   ( Reg32 True )
   ( Reg64 True )
   ( LocalVariable True )
   ( StackVariable True )
   ( GlobalVariable True )
   ( _ () )
));

typecheck-not-representation := λtt . (match tt (
   ()
   ( (And( Constant rt )) (typecheck-not-representation rt) )
   ( (And( lt Constant )) (typecheck-not-representation lt) )
   ( (And( LocalVariable rt )) (typecheck-not-representation rt) )
   ( (And( lt LocalVariable )) (typecheck-not-representation lt) )
   ( (And( GlobalVariable rt )) (typecheck-not-representation rt) )
   ( (And( lt GlobalVariable )) (typecheck-not-representation lt) )
   ( (And( Reg8 rt )) (typecheck-not-representation rt) )
   ( (And( lt Reg8 )) (typecheck-not-representation lt) )
   ( (And( Reg16 rt )) (typecheck-not-representation rt) )
   ( (And( lt Reg16 )) (typecheck-not-representation lt) )
   ( (And( Reg32 rt )) (typecheck-not-representation rt) )
   ( (And( lt Reg32 )) (typecheck-not-representation lt) )
   ( (And( Reg64 rt )) (typecheck-not-representation rt) )
   ( (And( lt Reg64 )) (typecheck-not-representation lt) )
   ( (And( lt rt )) (And(
      (typecheck-not-representation lt)
      (typecheck-not-representation rt)
   )))
   ( _ tt )
));

typecheck-as := λlt rt . (tail(
   (set lt (typecheck-modifiers( lt )))
   (if lt (
      (And( lt rt ))
   ) rt )
));
typecheck-modifiers := λtt . (match tt (
   ()
   ( (And( lt rt )) (tail(
      (set lt (typecheck-modifiers lt))
      (set rt (typecheck-modifiers rt))
      (match (lt rt) (
         ()
         ( (() ()) () )
         ( (() rt) rt )
         ( (lt ()) lt )
         ( (lt rt) (And( lt rt )) )
      ))
   )))
   ( LocalVariable tt )
   ( GlobalVariable tt )
   ( StackVariable tt )
   ( Constant tt )
   ( Literal tt )
   ( Label tt )
   ( Reg8 tt )
   ( Reg16 tt )
   ( Reg32 tt )
   ( Reg64 tt )
   ( (Sized _) tt )
   ( _ () )
));

typecheck-as-return := λrt . (tail(
   (set rt (typecheck-not-representation rt))
   (match (typecheck-sizeof rt) (
      ()
      (0 rt)
      (1 (And( Reg8 rt )))
      (2 (And( Reg16 rt )))
      (4 (And( Reg32 rt )))
      (8 (And( Reg64 rt )))
      (_ (And( LocalVariable rt )))
   ))
));

typecheck-slot := λtt tag . (tail(
   (local return)
   (set return (typecheck-slot-inner( tt tag )))
   (if return return tt)
));

typecheck-slot-inner := λtt tag . (tail(
   (local return)
   (set return (match tt (
      ()
      ( (And( lt rt )) (tail(
         (local lts)
         (set lts (typecheck-slot-inner( lt tag )))
         (if lts lts (typecheck-slot-inner( rt tag )))
      )))
      ( ( (_ _) _ ) () )
      ( ( t r ) (
         if (eq( t tag )) tt ()
      ))
      ( () () )
      ( t1 (if (eq( tag t1 )) tag () ))
   )))
   return
));

typecheck-rvalue := λtt . (match tt (
   ()
   ( (->( _ rt )) rt )
   ( _ (fail( 'typecheck-rvalue 'expected 'arrow tt )))
));

typecheck-is-fragment := λtt . (tail(
   (local is-fragment)
   (local fragment-types)
   (set fragment-types typecheck-fragment-types)
   (while fragment-types (tail(
      (if (deep-eq( tt (tail fragment-types) )) (
         (set is-fragment True)
      ) ())
      (set fragment-types (head fragment-types))
   )))
   is-fragment
));

typecheck-is-cyclical := λ tt descent . (tail(
   ()
   (match descent (
      ()
      ( () (tail(
         (local cyclical)
         (local constructors)
         (set constructors typecheck-constructors)
         (while constructors (tail(
            (match (tail constructors) (
               ()
               ( (case ('->( args (And( base-type case_ )) ))) (
                  (if (eq( base-type tt )) (
                     (if (typecheck-is-cyclical( tt args )) (
                        (set cyclical True)
                     ) ())
                  ) ())
               ))
            ))
            (set constructors (head constructors))
         )))
         cyclical
      )))
      ( (Array( _ '? )) () )
      ( (lt rt) (
         if (typecheck-is-cyclical( tt lt )) True
            (typecheck-is-cyclical( tt rt ))
      ))
      ( _ (if (eq( tt descent )) True (tail(
         (local cyclical)
         (local constructors)
         (set constructors typecheck-constructors)
         (while constructors (tail(
            (match (tail constructors) (
               ()
               ( (case ('->( args (And( base-type case_ )) ))) (
                  (if (eq( base-type descent )) (
                     (if (typecheck-is-cyclical( tt args )) (
                        (set cyclical True)
                     ) ())
                  ) ())
               ))
            ))
            (set constructors (head constructors))
         )))
         cyclical
      ))))
   ))
));

typecheck-datatype := λtt . (match tt (
   ()
   ( () () )
   ( (And( lt rt )) (
      if (typecheck-datatype lt) (typecheck-datatype lt) (typecheck-datatype rt)
   ))
   ( (_ _) () )
   ( _ (match tt (
      ()
      (I8 I8)
      (I16 I16)
      (I32 I32)
      (I64 I64)
      (U8 U8)
      (U16 U16)
      (U32 U32)
      (U64 U64)
      (_ ())
   )))
));
