Changes for supporting ghost applications and ghost bind in Steel

[aseemr]

This PR has changes to support ghost applications and ghost bind in Steel. The changes are over #3004.

Changes specific to this PR are:

• Changes to the core typechecker and reflection typechecker callback APIs to return the effect (total or ghost) of the term
• Introduction of a non_informative token and a reflection typechecker callback API to get that token
• Addition of a new token rule to the non_informative g e typing judgment---if you can exhibit a non-informative token for e, you get to derive non-informative g e using the token.

There is also some minor cleanup to use the types from FStar.TypeChecker.Core, using the stubs setup.

[nikswamy]

Thanks Aseem! I got an everest green with this and corresponding steel branch. Merging both.