Output language of typechecking pass?

[Richard Eisenberg]

> On Oct 27, 2021, at 9:54 AM, Benjamin Redelings <benjamin.redelings at gmail.com> wrote:
> 
> Hi,
> 
>     I have been looking for info on what actually comes out of the type-checking pass in GHC.  This is mostly because it seems like the "Type classes in Haskell" paper implements both type checking and translation to dictionary-passing in one pass, whereas it seems like GHC separates this into (i) type checking and (ii) desugaring.

This is correct: GHC takes two different passes to do this work. The big reason is around error messages: we want to have the code that the user wrote when reporting error messages. Since errors arise during type-checking, we thus want the output of the type checker to look like what the user wrote.

> 
> Questions:
> 
> 1. It seems like this separation is actually necessary, in order to apply generalization only to let arguments written by the programmer, and not to let bindings introduced during desugaring. Is that right?

I don't think so. That is, if we did it all in one pass, I still think we could get generalization right.

> 
> 2. Does the output of type checking contain type lambdas?

Yes. See below.

> 
> 3. Does the type checking pass determine where to add dictionary arguments?

Yes. See below.

> 
> 4. Are there any other resources I should be looking at?

Yes. You want to enable -fprint-typechecker-elaboration (and possible -fprint-explicit-coercions). With the former, you get to see all this stuff you're looking for. It's normally suppressed so that the output resembles the user's code.

I hope this helps!
Richard