A bidirectional typechecking puzzle in the Grace programming language