Deriving mechanisms in GHC

[Ryan Scott]

(Disclaimer: I have never used hs-to-coq before, so everything below is
merely an educated guess.)

Looking at the source code for hs-to-coq, I see this [1]:

addDerivedInstances :: GhcMonad m => TypecheckedModule -> m
> TypecheckedModule
> addDerivedInstances tcm = do
>     let Just (hsgroup, a, b, c) = tm_renamed_source tcm
>
>     (_gbl_env, inst_infos, _rn_binds) <- initTcHack tcm $ do
>         let tcg_env = fst (tm_internals_ tcm)
>             tcg_env_hack = tcg_env { tcg_mod = fakeDerivingMod,
> tcg_semantic_mod = fakeDerivingMod }
>                 -- Set the module to make it look like we are in GHCi
>                 -- so that GHC will allow us to re-typecheck existing
> instances
>         setGblEnv tcg_env_hack $
> #if __GLASGOW_HASKELL__ >= 810
>             tcInstDeclsDeriv [] (hs_derivds hsgroup)
> #else
>             tcInstDeclsDeriv [] (hs_tyclds hsgroup >>= group_tyclds)
> (hs_derivds hsgroup)
> #endif


If I understand this code correctly, it is using the GHC API to produce
deriving-generated code and typecheck it, which seems reasonable. The part
that confuses me is the #if __GLASGOW_HASKELL__ >= 810 bit. Prior to GHC
8.10, this code would obtain deriving-related information from two places:

   1. The deriving clauses of data type declarations (i.e., the hs_tyclds)
   2. Standalone deriving declarations (i.e., the hs_derivds)

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.

In order to give advice on what you *should* be doing, let me briefly
describe why the type of tcInstDeclsDeriv changed in GHC 8.10. The commit
that changed tcInstDeclsDeriv is [2]. Prior to that commit, tcInstDeclsDeriv
would obtain information related to deriving clauses via its first two
arguments:

   1. The first argument (of type [DerivInfo]) contained all of the
   deriving clauses for data family instances. (Note that hs-to-coq uses an
   empty list, so this means that hs-to-coq 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.)
   2. The second argument (of type [LTyClDecl GhcRn]) contained all of the
   data type definitions, which might have deriving clauses attached to them.

The linked commit changes things so that *all* deriving clause–related
information (both for ordinary data types as well as data family instances)
is passed as a [DerivInfo] list. This means that hs-to-coq needs to produce
those DerivInfo values somehow. As inspiration, you might want to look at
how GHC calls tcInstDeclsDeriv here [3]. GHC first calls the
tcTyAndClassDecls function to produce the DerivInfo values, and then it
passes the DerivInfo values to tcInstDeclsDeriv. I would hope that
something similar would work for hs-to-coq.

Best,

Ryan
-----
[1]
https://github.com/plclub/hs-to-coq/blob/03e823972fc7c5f85a300e554c691563f89a3e5f/src/lib/HsToCoq/Util/GHC/Deriving.hs#L50-L64
[2]
https://gitlab.haskell.org/ghc/ghc/-/commit/679427f878e50ba5a9981bac4c2f9c76f4de3c3c#4c1af4850cb90ab2963edb06b69b57e87ccdf9c1
[3]
https://gitlab.haskell.org/ghc/ghc/-/blob/bc1d435e399d8376b4e33d5d936424ff76cb686a/compiler/GHC/Tc/Module.hs#L1704-L1723
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20240703/e7d4fbe1/attachment.html>