Output language of typechecking pass?

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. 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? 2. Does the output of type checking contain type lambdas? 3. Does the type checking pass determine where to add dictionary arguments? 4. Are there any other resources I should be looking at? I am confused about #3, because the `-ddump-tc` output doesn't seem to show any type dictionaries in function bodies themselves, but it does seem to contain some kind of info about dictionaries as "evidence" -- but I am not sure what "evidence" is, or how it links into the AST for a function body. I did briefly look at `-ddump-tc-ast`, but not in detail yet. -BenRI

On Oct 27, 2021, at 9:54 AM, Benjamin Redelings
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

Hi,
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.
I guess I asked this question wrong. I mean to say, if we did the two passes in the reverse order (desugaring first, followed by typechecking), that would not work, right? As the wiki says: "This late desugaring is somewhat unusual. It is much more common to desugar the program before typechecking, or renaming, because that presents the renamer and typechecker with a much smaller language to deal with. However, GHC's organisation means that * error messages can display precisely the syntax that the user wrote; and * desugaring is not required to preserve type-inference properties. "
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
Hmm... so, I think I see how this works now. I don't think '-fprint-explicit-coercions' does anything here though. $ ghc -ddump-tc Test2.hs -fprint-typechecker-elaboration ... AbsBinds [a_a2hp] [$dNum_a2hB] {Exports: [g <= g_a2hz wrap: <>] Exported types: g :: forall a. Num a => a -> a -> a [LclId] Binds: g x_aYk y_aYl = (y_aYl * x_aYk) + 1 Evidence: [EvBinds{[W] $dNum_a2hs = $dNum_a2hq [W] $dNum_a2hw = $dNum_a2hq [W] $dNum_a2hq = $dNum_a2hB}]} ... The type and dictionary arguments are visible here (along with the evidence bindings), but type and dictionary applications are only visible if you use -ddump-tc-ast, which is a lot more verbose. (I don't think there is another flag that shows these applications?) Since I didn't initially know what "evidence" was, and there is nothing to say that a_a2hp is a type lambda argument, this was pretty opaque until I managed to read the tc-ast and the light went on. I can see now that the type and dictionary arguments are added by annotating the AST. Is there anywhere on the GHC wiki that explains how to interpret this output, and says that the type and dictionary applications ARE there, just not shown by '-ddump-tc'? Perhaps it would be helpful to add some basic description of what comes out of the typechecker to a page like this one? (below) https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/hsc-main -BenRI

Is there anywhere on the GHC wiki that explains how to interpret this output, and says that the type and dictionary applications ARE there, just not shown by '-ddump-tc'?
Perhaps it would be helpful to add some basic description of what comes out of the typechecker to a page like this one? (below)
https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/hsc-mainhttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2F-%2Fwikis%2Fcommentary%2Fcompiler%2Fhsc-main&data=04%7C01%7Csimonpj%40microsoft.com%7Cab59b17d2f394945ad1e08d9a2b96c81%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637719740212483767%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=WZL1VADZPUlaOACd58K1XZO5MzPOKrfLFMSuBD%2FGW44%3D&reserved=0
Yes it would! Would you care to start such a wiki page (a new one; don't just clutter up the one you point to)? You can write down what you know. Don't worry if you aren't 100% sure - we can correct it. And if you outright don't know, leave a "What should I say here?" note.
"This late desugaring is somewhat unusual. It is much more common to desugar the program before typechecking, or renaming, because that presents the renamer and typechecker with a much smaller language to deal with. However, GHC's organisation means that
This note is now slightly out of date. We are now, very carefully, doing some desugaring before typechecking. See
* Note [Handling overloaded and rebindable constructs] in GHC.Rename.Expr
* Note [Rebindable syntax and HsExpansion] in GHC.Hs.Expr
You can and should point to these and similar Notes from the wiki page you write. Indeed there may be some part of what you write that would be better framed as Note in GHC's source code.
Thanks!
Simon
PS: I am leaving Microsoft at the end of November 2021, at which point simonpj@microsoft.commailto:simonpj@microsoft.com will cease to work. Use simon.peytonjones@gmail.commailto:simon.peytonjones@gmail.com instead. (For now, it just forwards to simonpj@microsoft.com.)
From: ghc-devs

I was thinking about the relationship between the wiki and the notes in the GHC source. Would it be possible to link directly to [compiler notes] in the GHC source from the wiki, using hyperlinks? Right now, I'm seeing references that look like: (See |Note [Constraint flavours]|.) (I can see the motivation to include comments in the source, but I also think that the wiki is more discoverable than the compiler source code. So, in the interests of pursuing both approaches, it would be nice to be able to link to notes FROM the wiki. I suppose one could include a hyperlink to the file on github that contains the note...) I'm not sure how much web infrastructure would be required to make hyperlinks for notes... -BenRI On 11/8/21 5:35 AM, Simon Peyton Jones wrote:
Is there anywhere on the GHC wiki that explains how to interpret this output, and says that the type and dictionary applications ARE there, just not shown by '-ddump-tc'?
Perhaps it would be helpful to add some basic description of what comes out of the typechecker to a page like this one? (below)
https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/hsc-main https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2F-%2Fwikis%2Fcommentary%2Fcompiler%2Fhsc-main&data=04%7C01%7Csimonpj%40microsoft.com%7Cab59b17d2f394945ad1e08d9a2b96c81%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637719740212483767%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=WZL1VADZPUlaOACd58K1XZO5MzPOKrfLFMSuBD%2FGW44%3D&reserved=0
Yes it would! Would you care to start such a wiki page (a new one; don’t just clutter up the one you point to)? You can write down what you know. Don’t worry if you aren’t 100% sure – we can correct it. And if you outright don’t know, leave a “What should I say here?” note.
"This late desugaring is somewhat unusual. It is much more common to desugar the program before typechecking, or renaming, because that presents the renamer and typechecker with a much smaller language to deal with. However, GHC's organisation means that
This note is now slightly out of date. We are now, very carefully, doing some desugaring *before* typechecking. See
* Note [Handling overloaded and rebindable constructs] in GHC.Rename.Expr * Note [Rebindable syntax and HsExpansion] in GHC.Hs.Expr
You can and should point to these and similar Notes from the wiki page you write. Indeed there may be some part of what you write that would be better framed as Note in GHC’s source code.
Thanks!
Simon
PS: I am leaving Microsoft at the end of November 2021, at which point simonpj@microsoft.com mailto:simonpj@microsoft.com will cease to work. Use simon.peytonjones@gmail.com mailto:simon.peytonjones@gmail.com instead. (For now, it just forwards to simonpj@microsoft.com.)
*From:*ghc-devs
*On Behalf Of *Benjamin Redelings *Sent:* 08 November 2021 13:12 *To:* Richard Eisenberg *Cc:* ghc-devs@haskell.org *Subject:* Re: Output language of typechecking pass? Hi,
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.
I guess I asked this question wrong. I mean to say, if we did the two passes in the reverse order (desugaring first, followed by typechecking), that would not work, right?
As the wiki says:
"This late desugaring is somewhat unusual. It is much more common to desugar the program before typechecking, or renaming, because that presents the renamer and typechecker with a much smaller language to deal with. However, GHC's organisation means that
* error messages can display precisely the syntax that the user wrote; and * desugaring is not required to preserve type-inference properties.
"
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
Hmm... so, I think I see how this works now. I don't think '-fprint-explicit-coercions' does anything here though.
$ ghc -ddump-tc Test2.hs -fprint-typechecker-elaboration
...
AbsBinds [a_a2hp] [$dNum_a2hB] {Exports: [g <= g_a2hz wrap: <>] Exported types: g :: forall a. Num a => a -> a -> a [LclId] Binds: g x_aYk y_aYl = (y_aYl * x_aYk) + 1 Evidence: [EvBinds{[W] $dNum_a2hs = $dNum_a2hq [W] $dNum_a2hw = $dNum_a2hq [W] $dNum_a2hq = $dNum_a2hB}]}
...
The type and dictionary arguments are visible here (along with the evidence bindings), but type and dictionary applications are only visible if you use -ddump-tc-ast, which is a lot more verbose. (I don't think there is another flag that shows these applications?) Since I didn't initially know what "evidence" was, and there is nothing to say that a_a2hp is a type lambda argument, this was pretty opaque until I managed to read the tc-ast and the light went on.
I can see now that the type and dictionary arguments are added by annotating the AST.
Is there anywhere on the GHC wiki that explains how to interpret this output, and says that the type and dictionary applications ARE there, just not shown by '-ddump-tc'?
Perhaps it would be helpful to add some basic description of what comes out of the typechecker to a page like this one? (below)
https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/hsc-main https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2F-%2Fwikis%2Fcommentary%2Fcompiler%2Fhsc-main&data=04%7C01%7Csimonpj%40microsoft.com%7Cab59b17d2f394945ad1e08d9a2b96c81%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637719740212483767%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=WZL1VADZPUlaOACd58K1XZO5MzPOKrfLFMSuBD%2FGW44%3D&reserved=0
-BenRI

We could always make a hyperlink to the source code as hosted on GitLab. But I actually argue not to: such links would quickly become outdated, in one of two ways: either we make a permalink, in which case the linked Note text will become outdated; or we make a link to a particular file & line, in which case the Note might move somewhere else. Instead, just by naming the Note title, we have a slightly-harder-to-use link, where you use it by grepping the source code. This is less convenient, but it will stay up-to-date. Until we have better tooling to, say, create an HTML anchor based on a Note, I think this is the best we can do. Richard
On Dec 28, 2021, at 12:10 PM, Benjamin Redelings
wrote: I was thinking about the relationship between the wiki and the notes in the GHC source.
Would it be possible to link directly to [compiler notes] in the GHC source from the wiki, using hyperlinks? Right now, I'm seeing references that look like: (See Note [Constraint flavours].)
(I can see the motivation to include comments in the source, but I also think that the wiki is more discoverable than the compiler source code. So, in the interests of pursuing both approaches, it would be nice to be able to link to notes FROM the wiki. I suppose one could include a hyperlink to the file on github that contains the note...)
I'm not sure how much web infrastructure would be required to make hyperlinks for notes...
-BenRI
On 11/8/21 5:35 AM, Simon Peyton Jones wrote:
Is there anywhere on the GHC wiki that explains how to interpret this output, and says that the type and dictionary applications ARE there, just not shown by '-ddump-tc'?
Perhaps it would be helpful to add some basic description of what comes out of the typechecker to a page like this one? (below)
https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/hsc-main https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2F-%2Fwikis%2Fcommentary%2Fcompiler%2Fhsc-main&data=04%7C01%7Csimonpj%40microsoft.com%7Cab59b17d2f394945ad1e08d9a2b96c81%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637719740212483767%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=WZL1VADZPUlaOACd58K1XZO5MzPOKrfLFMSuBD%2FGW44%3D&reserved=0 Yes it would! Would you care to start such a wiki page (a new one; don’t just clutter up the one you point to)? You can write down what you know. Don’t worry if you aren’t 100% sure – we can correct it. And if you outright don’t know, leave a “What should I say here?” note.
"This late desugaring is somewhat unusual. It is much more common to desugar the program before typechecking, or renaming, because that presents the renamer and typechecker with a much smaller language to deal with. However, GHC's organisation means that
This note is now slightly out of date. We are now, very carefully, doing some desugaring before typechecking. See Note [Handling overloaded and rebindable constructs] in GHC.Rename.Expr Note [Rebindable syntax and HsExpansion] in GHC.Hs.Expr
You can and should point to these and similar Notes from the wiki page you write. Indeed there may be some part of what you write that would be better framed as Note in GHC’s source code.
Thanks!
Simon
PS: I am leaving Microsoft at the end of November 2021, at which point simonpj@microsoft.com mailto:simonpj@microsoft.com will cease to work. Use simon.peytonjones@gmail.com mailto:simon.peytonjones@gmail.com instead. (For now, it just forwards to simonpj@microsoft.com mailto:simonpj@microsoft.com.)
From: ghc-devs
mailto:ghc-devs-bounces@haskell.org On Behalf Of Benjamin Redelings Sent: 08 November 2021 13:12 To: Richard Eisenberg mailto:lists@richarde.dev Cc: ghc-devs@haskell.org mailto:ghc-devs@haskell.org Subject: Re: Output language of typechecking pass? Hi,
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. I guess I asked this question wrong. I mean to say, if we did the two passes in the reverse order (desugaring first, followed by typechecking), that would not work, right?
As the wiki says:
"This late desugaring is somewhat unusual. It is much more common to desugar the program before typechecking, or renaming, because that presents the renamer and typechecker with a much smaller language to deal with. However, GHC's organisation means that
error messages can display precisely the syntax that the user wrote; and desugaring is not required to preserve type-inference properties. "
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 Hmm... so, I think I see how this works now. I don't think '-fprint-explicit-coercions' does anything here though.
$ ghc -ddump-tc Test2.hs -fprint-typechecker-elaboration
...
AbsBinds [a_a2hp] [$dNum_a2hB] {Exports: [g <= g_a2hz wrap: <>] Exported types: g :: forall a. Num a => a -> a -> a [LclId] Binds: g x_aYk y_aYl = (y_aYl * x_aYk) + 1 Evidence: [EvBinds{[W] $dNum_a2hs = $dNum_a2hq [W] $dNum_a2hw = $dNum_a2hq [W] $dNum_a2hq = $dNum_a2hB}]}
...
The type and dictionary arguments are visible here (along with the evidence bindings), but type and dictionary applications are only visible if you use -ddump-tc-ast, which is a lot more verbose. (I don't think there is another flag that shows these applications?) Since I didn't initially know what "evidence" was, and there is nothing to say that a_a2hp is a type lambda argument, this was pretty opaque until I managed to read the tc-ast and the light went on.
I can see now that the type and dictionary arguments are added by annotating the AST.
Is there anywhere on the GHC wiki that explains how to interpret this output, and says that the type and dictionary applications ARE there, just not shown by '-ddump-tc'?
Perhaps it would be helpful to add some basic description of what comes out of the typechecker to a page like this one? (below)
https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/hsc-main https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2F-%2Fwikis%2Fcommentary%2Fcompiler%2Fhsc-main&data=04%7C01%7Csimonpj%40microsoft.com%7Cab59b17d2f394945ad1e08d9a2b96c81%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637719740212483767%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=WZL1VADZPUlaOACd58K1XZO5MzPOKrfLFMSuBD%2FGW44%3D&reserved=0 -BenRI

FYI, it is possible to make a "permalink" on github, which points to the
code at a specific commit. Perhaps gitlab has something similar?
Alan
On Tue, 28 Dec 2021 at 19:28, Richard Eisenberg
We could always make a hyperlink to the source code as hosted on GitLab. But I actually argue not to: such links would quickly become outdated, in one of two ways: either we make a permalink, in which case the linked Note text will become outdated; or we make a link to a particular file & line, in which case the Note might move somewhere else. Instead, just by naming the Note title, we have a slightly-harder-to-use link, where you use it by grepping the source code. This is less convenient, but it will stay up-to-date. Until we have better tooling to, say, create an HTML anchor based on a Note, I think this is the best we can do.
Richard
On Dec 28, 2021, at 12:10 PM, Benjamin Redelings < benjamin.redelings@gmail.com> wrote:
I was thinking about the relationship between the wiki and the notes in the GHC source.
Would it be possible to link directly to [compiler notes] in the GHC source from the wiki, using hyperlinks? Right now, I'm seeing references that look like: (See Note [Constraint flavours].)
(I can see the motivation to include comments in the source, but I also think that the wiki is more discoverable than the compiler source code. So, in the interests of pursuing both approaches, it would be nice to be able to link to notes FROM the wiki. I suppose one could include a hyperlink to the file on github that contains the note...)
I'm not sure how much web infrastructure would be required to make hyperlinks for notes...
-BenRI On 11/8/21 5:35 AM, Simon Peyton Jones wrote:
Is there anywhere on the GHC wiki that explains how to interpret this output, and says that the type and dictionary applications ARE there, just not shown by '-ddump-tc'?
Perhaps it would be helpful to add some basic description of what comes out of the typechecker to a page like this one? (below)
https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/hsc-main https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2F-%2Fwikis%2Fcommentary%2Fcompiler%2Fhsc-main&data=04%7C01%7Csimonpj%40microsoft.com%7Cab59b17d2f394945ad1e08d9a2b96c81%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637719740212483767%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=WZL1VADZPUlaOACd58K1XZO5MzPOKrfLFMSuBD%2FGW44%3D&reserved=0 Yes it would! Would you care to start such a wiki page (a new one; don’t just clutter up the one you point to)? You can write down what you know. Don’t worry if you aren’t 100% sure – we can correct it. And if you outright don’t know, leave a “What should I say here?” note.
"This late desugaring is somewhat unusual. It is much more common to desugar the program before typechecking, or renaming, because that presents the renamer and typechecker with a much smaller language to deal with. However, GHC's organisation means that This note is now slightly out of date. We are now, very carefully, doing some desugaring *before* typechecking. See
- Note [Handling overloaded and rebindable constructs] in GHC.Rename.Expr - Note [Rebindable syntax and HsExpansion] in GHC.Hs.Expr
You can and should point to these and similar Notes from the wiki page you write. Indeed there may be some part of what you write that would be better framed as Note in GHC’s source code.
Thanks!
Simon
PS: I am leaving Microsoft at the end of November 2021, at which point simonpj@microsoft.com will cease to work. Use simon.peytonjones@gmail.com instead. (For now, it just forwards to simonpj@microsoft.com.)
*From:* ghc-devs
*On Behalf Of *Benjamin Redelings *Sent:* 08 November 2021 13:12 *To:* Richard Eisenberg *Cc:* ghc-devs@haskell.org *Subject:* Re: Output language of typechecking pass? Hi,
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.
I guess I asked this question wrong. I mean to say, if we did the two passes in the reverse order (desugaring first, followed by typechecking), that would not work, right?
As the wiki says:
"This late desugaring is somewhat unusual. It is much more common to desugar the program before typechecking, or renaming, because that presents the renamer and typechecker with a much smaller language to deal with. However, GHC's organisation means that
- error messages can display precisely the syntax that the user wrote; and - desugaring is not required to preserve type-inference properties.
"
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
Hmm... so, I think I see how this works now. I don't think '-fprint-explicit-coercions' does anything here though.
$ ghc -ddump-tc Test2.hs -fprint-typechecker-elaboration
...
AbsBinds [a_a2hp] [$dNum_a2hB] {Exports: [g <= g_a2hz wrap: <>] Exported types: g :: forall a. Num a => a -> a -> a [LclId] Binds: g x_aYk y_aYl = (y_aYl * x_aYk) + 1 Evidence: [EvBinds{[W] $dNum_a2hs = $dNum_a2hq [W] $dNum_a2hw = $dNum_a2hq [W] $dNum_a2hq = $dNum_a2hB}]}
...
The type and dictionary arguments are visible here (along with the evidence bindings), but type and dictionary applications are only visible if you use -ddump-tc-ast, which is a lot more verbose. (I don't think there is another flag that shows these applications?) Since I didn't initially know what "evidence" was, and there is nothing to say that a_a2hp is a type lambda argument, this was pretty opaque until I managed to read the tc-ast and the light went on.
I can see now that the type and dictionary arguments are added by annotating the AST.
Is there anywhere on the GHC wiki that explains how to interpret this output, and says that the type and dictionary applications ARE there, just not shown by '-ddump-tc'?
Perhaps it would be helpful to add some basic description of what comes out of the typechecker to a page like this one? (below)
https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/hsc-main https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2F-%2Fwikis%2Fcommentary%2Fcompiler%2Fhsc-main&data=04%7C01%7Csimonpj%40microsoft.com%7Cab59b17d2f394945ad1e08d9a2b96c81%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637719740212483767%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=WZL1VADZPUlaOACd58K1XZO5MzPOKrfLFMSuBD%2FGW44%3D&reserved=0
-BenRI
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Yes, GitLab supports such a permalink. The problem is that we frequently revise Notes as we understand problems better / improve the implementation. So a reader might link to a Note from the wiki only to study an old implementation that has been superseded. Richard
On Dec 28, 2021, at 3:52 PM, Alan & Kim Zimmerman
wrote: FYI, it is possible to make a "permalink" on github, which points to the code at a specific commit. Perhaps gitlab has something similar?
Alan
On Tue, 28 Dec 2021 at 19:28, Richard Eisenberg
mailto:lists@richarde.dev> wrote: We could always make a hyperlink to the source code as hosted on GitLab. But I actually argue not to: such links would quickly become outdated, in one of two ways: either we make a permalink, in which case the linked Note text will become outdated; or we make a link to a particular file & line, in which case the Note might move somewhere else. Instead, just by naming the Note title, we have a slightly-harder-to-use link, where you use it by grepping the source code. This is less convenient, but it will stay up-to-date. Until we have better tooling to, say, create an HTML anchor based on a Note, I think this is the best we can do. Richard
On Dec 28, 2021, at 12:10 PM, Benjamin Redelings
mailto:benjamin.redelings@gmail.com> wrote: I was thinking about the relationship between the wiki and the notes in the GHC source.
Would it be possible to link directly to [compiler notes] in the GHC source from the wiki, using hyperlinks? Right now, I'm seeing references that look like: (See Note [Constraint flavours].)
(I can see the motivation to include comments in the source, but I also think that the wiki is more discoverable than the compiler source code. So, in the interests of pursuing both approaches, it would be nice to be able to link to notes FROM the wiki. I suppose one could include a hyperlink to the file on github that contains the note...)
I'm not sure how much web infrastructure would be required to make hyperlinks for notes...
-BenRI
On 11/8/21 5:35 AM, Simon Peyton Jones wrote:
Is there anywhere on the GHC wiki that explains how to interpret this output, and says that the type and dictionary applications ARE there, just not shown by '-ddump-tc'?
Perhaps it would be helpful to add some basic description of what comes out of the typechecker to a page like this one? (below)
https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/hsc-main https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2F-%2Fwikis%2Fcommentary%2Fcompiler%2Fhsc-main&data=04%7C01%7Csimonpj%40microsoft.com%7Cab59b17d2f394945ad1e08d9a2b96c81%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637719740212483767%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=WZL1VADZPUlaOACd58K1XZO5MzPOKrfLFMSuBD%2FGW44%3D&reserved=0 Yes it would! Would you care to start such a wiki page (a new one; don’t just clutter up the one you point to)? You can write down what you know. Don’t worry if you aren’t 100% sure – we can correct it. And if you outright don’t know, leave a “What should I say here?” note.
"This late desugaring is somewhat unusual. It is much more common to desugar the program before typechecking, or renaming, because that presents the renamer and typechecker with a much smaller language to deal with. However, GHC's organisation means that
This note is now slightly out of date. We are now, very carefully, doing some desugaring before typechecking. See Note [Handling overloaded and rebindable constructs] in GHC.Rename.Expr Note [Rebindable syntax and HsExpansion] in GHC.Hs.Expr
You can and should point to these and similar Notes from the wiki page you write. Indeed there may be some part of what you write that would be better framed as Note in GHC’s source code.
Thanks!
Simon
PS: I am leaving Microsoft at the end of November 2021, at which point simonpj@microsoft.com mailto:simonpj@microsoft.com will cease to work. Use simon.peytonjones@gmail.com mailto:simon.peytonjones@gmail.com instead. (For now, it just forwards to simonpj@microsoft.com mailto:simonpj@microsoft.com.)
From: ghc-devs
mailto:ghc-devs-bounces@haskell.org On Behalf Of Benjamin Redelings Sent: 08 November 2021 13:12 To: Richard Eisenberg mailto:lists@richarde.dev Cc: ghc-devs@haskell.org mailto:ghc-devs@haskell.org Subject: Re: Output language of typechecking pass? Hi,
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. I guess I asked this question wrong. I mean to say, if we did the two passes in the reverse order (desugaring first, followed by typechecking), that would not work, right?
As the wiki says:
"This late desugaring is somewhat unusual. It is much more common to desugar the program before typechecking, or renaming, because that presents the renamer and typechecker with a much smaller language to deal with. However, GHC's organisation means that
error messages can display precisely the syntax that the user wrote; and desugaring is not required to preserve type-inference properties. "
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 Hmm... so, I think I see how this works now. I don't think '-fprint-explicit-coercions' does anything here though.
$ ghc -ddump-tc Test2.hs -fprint-typechecker-elaboration
...
AbsBinds [a_a2hp] [$dNum_a2hB] {Exports: [g <= g_a2hz wrap: <>] Exported types: g :: forall a. Num a => a -> a -> a [LclId] Binds: g x_aYk y_aYl = (y_aYl * x_aYk) + 1 Evidence: [EvBinds{[W] $dNum_a2hs = $dNum_a2hq [W] $dNum_a2hw = $dNum_a2hq [W] $dNum_a2hq = $dNum_a2hB}]}
...
The type and dictionary arguments are visible here (along with the evidence bindings), but type and dictionary applications are only visible if you use -ddump-tc-ast, which is a lot more verbose. (I don't think there is another flag that shows these applications?) Since I didn't initially know what "evidence" was, and there is nothing to say that a_a2hp is a type lambda argument, this was pretty opaque until I managed to read the tc-ast and the light went on.
I can see now that the type and dictionary arguments are added by annotating the AST.
Is there anywhere on the GHC wiki that explains how to interpret this output, and says that the type and dictionary applications ARE there, just not shown by '-ddump-tc'?
Perhaps it would be helpful to add some basic description of what comes out of the typechecker to a page like this one? (below)
https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/hsc-main https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2F-%2Fwikis%2Fcommentary%2Fcompiler%2Fhsc-main&data=04%7C01%7Csimonpj%40microsoft.com%7Cab59b17d2f394945ad1e08d9a2b96c81%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637719740212483767%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=WZL1VADZPUlaOACd58K1XZO5MzPOKrfLFMSuBD%2FGW44%3D&reserved=0 -BenRI
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org mailto:ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
participants (4)
-
Alan & Kim Zimmerman
-
Benjamin Redelings
-
Richard Eisenberg
-
Simon Peyton Jones