Conversation

Is there a type-checking analog of normalization-by-evaluation where one reuses the host language's type checker to produce inferred types and error messages?
7
21