<div dir="ltr">Ah that looks like the reason. Thank you for catching that! Thanks for the pointers to the specific commit in GHC as well as the example!<div><br></div><div>I am also curious if there is a recommended way to check the GHC API changes across different versions. We use GHC APIs extensively in hs-to-coq and there seem to be a number of changes between 8.4 and 8.10, so it's possible that we will run into other similar issues at some point, or when we update hs-to-coq to newer GHC versions in the future... Or are there any community recommendations on the best way to maintain our code base, which relies on GHC APIs?</div><div><br></div><div>Thanks,</div><div>Yao</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Jul 3, 2024 at 7:46 AM Ryan Scott <<a href="mailto:ryan.gl.scott@gmail.com">ryan.gl.scott@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>(Disclaimer: I have never used <span style="font-family:monospace">hs-to-coq</span> before, so everything below is merely an educated guess.)</div><div><br></div><div>Looking at the source code for <span style="font-family:monospace">hs-to-coq</span>, I see this [1]:</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span style="font-family:monospace">addDerivedInstances :: GhcMonad m => TypecheckedModule -> m TypecheckedModule<br>addDerivedInstances tcm = do<br> let Just (hsgroup, a, b, c) = tm_renamed_source tcm<br><br> (_gbl_env, inst_infos, _rn_binds) <- initTcHack tcm $ do<br> let tcg_env = fst (tm_internals_ tcm)<br> tcg_env_hack = tcg_env { tcg_mod = fakeDerivingMod, tcg_semantic_mod = fakeDerivingMod }<br> -- Set the module to make it look like we are in GHCi<br> -- so that GHC will allow us to re-typecheck existing instances<br> setGblEnv tcg_env_hack $<br>#if __GLASGOW_HASKELL__ >= 810<br> tcInstDeclsDeriv [] (hs_derivds hsgroup)<br>#else<br> tcInstDeclsDeriv [] (hs_tyclds hsgroup >>= group_tyclds) (hs_derivds hsgroup)<br>#endif</span></blockquote><div><br></div><div>If I understand this code correctly, it is using the GHC API to produce <span style="font-family:monospace">deriving</span>-generated code and typecheck it, which seems reasonable. The part that confuses me is the <span style="font-family:monospace">#if __GLASGOW_HASKELL__ >= 810</span> bit. Prior to GHC 8.10, this code would obtain <span style="font-family:monospace">deriving</span>-related information from two places:</div><div><ol><li>The <span style="font-family:monospace">deriving</span> clauses of data type declarations (i.e., the <span style="font-family:monospace">hs_tyclds</span>)</li><li>Standalone deriving declarations (i.e., the <span style="font-family:monospace">hs_derivds</span>)</li></ol><div>In GHC 8.10 and later, however, the code only obtains deriving-related information from standalone deriving declarations. This means that you'll completely skip over any derived instances that arise from deriving clauses, which is likely the source of the trouble you're encountering.</div><div><br></div><div>In order to give advice on what you <i>should</i> be doing, let me briefly describe why the type of <span style="font-family:monospace">tcInstDeclsDeriv</span> changed in GHC 8.10. The commit that changed <span style="font-family:monospace">tcInstDeclsDeriv</span> is [2]. Prior to that commit, <span style="font-family:monospace">tcInstDeclsDeriv</span> would obtain information related to <span style="font-family:monospace">deriving</span> clauses via its first two arguments:</div><div><ol><li>The first argument (of type <code><span><span>[</span><span>DerivInfo</span><span>]</span></span></code>) contained all of the deriving clauses for data family instances. (Note that hs-to-coq uses an empty list, so this means that <span style="font-family:monospace">hs-to-coq</span> will always skip over data family instances, before or after GHC 8.10. I'm not sure if this should be considered as a separate bug.)</li><li>The second argument (of type <code><span><span>[</span><span>LTyClDecl</span> <span>GhcRn</span><span>]</span></span></code>) contained all of the data type definitions, which might have deriving clauses attached to them.<br></li></ol></div></div><div>The linked commit changes things so that <i>all</i> <span style="font-family:monospace">deriving</span> clause–related information (both for ordinary data types as well as data family instances) is passed as a <code><span><span>[</span><span>DerivInfo</span><span>]</span></span></code> list. This means that hs-to-coq needs to produce those <span style="font-family:monospace">DerivInfo</span> values somehow. As inspiration, you might want to look at how GHC calls <span style="font-family:monospace">tcInstDeclsDeriv</span> here [3]. GHC first calls the <code>tcTyAndClassDecls</code> function to produce the <span style="font-family:monospace">DerivInfo</span> values, and then it passes the <span style="font-family:monospace">DerivInfo</span> values to <span style="font-family:monospace">tcInstDeclsDeriv</span>. I would hope that something similar would work for <span style="font-family:monospace">hs-to-coq</span>.<br></div><div><br></div><div>Best,</div><div><br></div><div>Ryan</div><div>-----</div><div>[1] <a href="https://github.com/plclub/hs-to-coq/blob/03e823972fc7c5f85a300e554c691563f89a3e5f/src/lib/HsToCoq/Util/GHC/Deriving.hs#L50-L64" target="_blank">https://github.com/plclub/hs-to-coq/blob/03e823972fc7c5f85a300e554c691563f89a3e5f/src/lib/HsToCoq/Util/GHC/Deriving.hs#L50-L64</a></div><div>[2] <a href="https://gitlab.haskell.org/ghc/ghc/-/commit/679427f878e50ba5a9981bac4c2f9c76f4de3c3c#4c1af4850cb90ab2963edb06b69b57e87ccdf9c1" target="_blank">https://gitlab.haskell.org/ghc/ghc/-/commit/679427f878e50ba5a9981bac4c2f9c76f4de3c3c#4c1af4850cb90ab2963edb06b69b57e87ccdf9c1</a></div><div>[3] <a href="https://gitlab.haskell.org/ghc/ghc/-/blob/bc1d435e399d8376b4e33d5d936424ff76cb686a/compiler/GHC/Tc/Module.hs#L1704-L1723" target="_blank">https://gitlab.haskell.org/ghc/ghc/-/blob/bc1d435e399d8376b4e33d5d936424ff76cb686a/compiler/GHC/Tc/Module.hs#L1704-L1723</a></div></div>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>