STLC terms differ from untyped terms in lambda abstractions — every binding should be typed: ```haskell (\(x :: A) -> t) a ``` We need to have a parser for such terms.