unify-hint := λ(: hint Type)(: tt Type). (: (
   (match (Tuple( hint tt )) (
      ()
      ( (Tuple( (TGround( hint-tag hint-args )) (TGround( tt-tag tt-args )) )) (
         (if (==( hint-tag tt-tag )) (
            (set tt hint)
         ) (
            (set tt (TGround( tt-tag (close(unify-hint( hint tt-args ))) )))
         ))
      ))
      ( (Tuple( _ (TAnd( lt rt )) )) (
         (set tt (TAnd(
            (close(unify-hint( hint lt )))
            (close(unify-hint( hint rt )))
         )))
      ))
      ( _ () )
   ))
   tt
) Type);

unify-hint := λ(: hint Type)(: tt List<Type>). (: (
   (match tt (
      ()
      ( LEOF () )
      ( (LCons( p1 rst )) (
         (set tt (cons(
            (unify-hint( hint p1 ))
            (unify-hint( hint rst ))
         )))
      ))
      ( _ () )
   ))
   tt
) List<Type>);