Hi, I'd like to implement type synonyms containing wildcards. The idea is that if you have `type MySyn a = MyType a _ Int`, then during typechecking, every occurrence of `MySyn T` would be expanded into `MyType T w123 Int`, with a fresh type (meta)variable `w123`. One worrying thing I noticed in my initial exploration of the GHC codebase is that the Core representation of `Type`s can still contain type synonym occurrences. And this doesn't seem like just an artefact of sharing the `Type` representation with `TcType`, since the `coreView` function also has code to look through type synonyms. What is the reason for this? I would have expected type synonyms to be only relevant during typechecking, and then fully resolved in the elaborated Core output. If that were the case, then a new version of `expand_syn` could live in `TcM` and take care of making these fresh metavariables. Beside this concrete question, taking a step back, I would also like to hear from people who know their way around this part of GHC, what they think about this and how they'd approach implementing it. Thanks, Gergo