with-size := λ(: tt Type). (: (
   (if (not(is-sized tt)) (
      (let sz (sizeof-type tt))
      (set tt (with-size-recurse tt))
      (set tt (and( tt (t2( 'Sized_s (t1(to-string sz)) )) )))
   ) ())
   (match tt (
      ()
      ( (TGround( 'Cons_s (LCons( p2 (LCons( p1 LEOF )) )) )) (
         (set tt (t3( 'Cons_s (with-size p1) (with-size p2) )))
      ))
      ( _ () )
   ))
   tt
) Type);

with-size := λ(: tt List<Type>). (: (
   (match tt (
      ()
      ( LEOF () )
      ( (LCons( p1 ps )) (
         (set tt (cons( (with-size p1) (with-size ps) )))
      ))
   ))
   tt
) List<Type>);

with-size-recurse := λ(: tt Type). (: (
   (match tt (
      ()
      ( (TAnd( lt rt )) (
         (set tt (and(
            (with-size-recurse lt)
            (with-size-recurse rt)
         )))
      ))
      ( (TGround( 'Tag_s _ )) () )
      ( (TGround( 'Sized_s _ )) () )
      ( (TGround( 'Fields_s _ )) () )
      ( (TGround( 'FieldsSized_s _ )) () )
      ( (TGround( tag ps )) (
         (set tt (TGround( tag (close(with-size ps)) )))
      ))
      ( _ () )
   ))
   tt
) Type);