Banish reportFloatingViaTvs to the shadow realm (#15831, #16181)

GHC used to reject programs of this form:

```
newtype Age = MkAge Int
  deriving Eq via Const Int a
```

That's because an earlier implementation of `DerivingVia` would
generate the following instance:

```
instance Eq Age where
  (==) = coerce @(Const Int a -> Const Int a -> Bool)
                @(Age         -> Age         -> Bool)
                (==)
```

Note that the `a` in `Const Int a` is not bound anywhere, which
causes all sorts of issues. I figured that no one would ever want to
write code like this anyway, so I simply banned "floating" `via` type
variables like `a`, checking for their presence in the aptly named
`reportFloatingViaTvs` function.

`reportFloatingViaTvs` ended up being implemented in a subtly
incorrect way, as #15831 demonstrates. Following counsel with the
sage of gold fire, I decided to abandon `reportFloatingViaTvs`
entirely and opt for a different approach that would _accept_
the instance above. This is because GHC now generates this instance
instead:

```
instance forall a. Eq Age where
  (==) = coerce @(Const Int a -> Const Int a -> Bool)
                @(Age         -> Age         -> Bool)
                (==)
```

Notice that we now explicitly quantify the `a` in
`instance forall a. Eq Age`, so everything is peachy scoping-wise.
See `Note [Floating `via` type variables]` in `TcDeriv` for the full
scoop.

A pleasant benefit of this refactoring is that it made it much easier
to catch the problem observed in #16181, so this patch fixes that
issue too.

Fixes #15831. Fixes #16181.

3 files changed, 168 insertions, 140 deletions

diff --git a/compiler/hsSyn/HsDecls.hs b/compiler/hsSyn/HsDecls.hs
index bd0bcb527d..3cac82ed2f 100644
--- a/compiler/hsSyn/HsDecls.hs
+++ b/compiler/hsSyn/HsDecls.hs
@@ -47,7 +47,8 @@ module HsDecls (
   -- ** Standalone deriving declarations
   DerivDecl(..), LDerivDecl,
   -- ** Deriving strategies
-  DerivStrategy(..), LDerivStrategy, derivStrategyName,
+  DerivStrategy(..), LDerivStrategy,
+  derivStrategyName, foldDerivStrategy, mapDerivStrategy,
   -- ** @RULE@ declarations
   LRuleDecls,RuleDecls(..),RuleDecl(..),LRuleDecl,HsRuleRn(..),
   RuleBndr(..),LRuleBndr,
@@ -1936,6 +1937,21 @@ derivStrategyName = text . go
     go NewtypeStrategy  = "newtype"
     go (ViaStrategy {}) = "via"
 
+-- | Eliminate a 'DerivStrategy'.
+foldDerivStrategy :: (p ~ GhcPass pass)
+                  => r -> (XViaStrategy p -> r) -> DerivStrategy p -> r
+foldDerivStrategy other _   StockStrategy    = other
+foldDerivStrategy other _   AnyclassStrategy = other
+foldDerivStrategy other _   NewtypeStrategy  = other
+foldDerivStrategy _     via (ViaStrategy t)  = via t
+
+-- | Map over the @via@ type if dealing with 'ViaStrategy'. Otherwise,
+-- return the 'DerivStrategy' unchanged.
+mapDerivStrategy :: (p ~ GhcPass pass)
+                 => (XViaStrategy p -> XViaStrategy p)
+                 -> DerivStrategy p -> DerivStrategy p
+mapDerivStrategy f ds = foldDerivStrategy ds (ViaStrategy . f) ds
+
 {-
 ************************************************************************
 *                                                                      *
diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs
index aea4b0d5eb..8f85fac28b 100644
--- a/compiler/rename/RnSource.hs
+++ b/compiler/rename/RnSource.hs
@@ -971,8 +971,7 @@ rnSrcDerivDecl (DerivDecl _ ty mds overlap)
   = do { standalone_deriv_ok <- xoptM LangExt.StandaloneDeriving
        ; unless standalone_deriv_ok (addErr standaloneDerivErr)
        ; (mds', ty', fvs)
-           <- rnLDerivStrategy DerivDeclCtx mds $ \strat_tvs ppr_via_ty ->
-              rnAndReportFloatingViaTvs strat_tvs loc ppr_via_ty "instance" $
+           <- rnLDerivStrategy DerivDeclCtx mds $
               rnHsSigWcType BindUnlessForall DerivDeclCtx ty
        ; warnNoDerivStrat mds' loc
        ; return (DerivDecl noExtField ty' mds' overlap, fvs) }
@@ -1725,20 +1724,12 @@ rnLHsDerivingClause doc
                               , deriv_clause_strategy = dcs
                               , deriv_clause_tys = (dL->L loc' dct) }))
   = do { (dcs', dct', fvs)
-           <- rnLDerivStrategy doc dcs $ \strat_tvs ppr_via_ty ->
-              mapFvRn (rn_deriv_ty strat_tvs ppr_via_ty) dct
+           <- rnLDerivStrategy doc dcs $ mapFvRn (rnHsSigType doc) dct
        ; warnNoDerivStrat dcs' loc
        ; pure ( cL loc (HsDerivingClause { deriv_clause_ext = noExtField
                                          , deriv_clause_strategy = dcs'
                                          , deriv_clause_tys = cL loc' dct' })
               , fvs ) }
-  where
-    rn_deriv_ty :: [Name] -> SDoc -> LHsSigType GhcPs
-                -> RnM (LHsSigType GhcRn, FreeVars)
-    rn_deriv_ty strat_tvs ppr_via_ty deriv_ty@(HsIB {hsib_body = dL->L loc _}) =
-      rnAndReportFloatingViaTvs strat_tvs loc ppr_via_ty "class" $
-      rnHsSigType doc deriv_ty
-    rn_deriv_ty _ _ (XHsImplicitBndrs nec) = noExtCon nec
 rnLHsDerivingClause _ (dL->L _ (XHsDerivingClause nec))
   = noExtCon nec
 rnLHsDerivingClause _ _ = panic "rnLHsDerivingClause: Impossible Match"
@@ -1747,20 +1738,19 @@ rnLHsDerivingClause _ _ = panic "rnLHsDerivingClause: Impossible Match"
 rnLDerivStrategy :: forall a.
                     HsDocContext
                  -> Maybe (LDerivStrategy GhcPs)
-                 -> ([Name]   -- The tyvars bound by the via type
-                      -> SDoc -- The pretty-printed via type (used for
-                              -- error message reporting)
-                      -> RnM (a, FreeVars))
+                 -> RnM (a, FreeVars)
                  -> RnM (Maybe (LDerivStrategy GhcRn), a, FreeVars)
 rnLDerivStrategy doc mds thing_inside
   = case mds of
       Nothing -> boring_case Nothing
-      Just ds -> do (ds', thing, fvs) <- rn_deriv_strat ds
-                    pure (Just ds', thing, fvs)
+      Just (dL->L loc ds) ->
+        setSrcSpan loc $ do
+          (ds', thing, fvs) <- rn_deriv_strat ds
+          pure (Just (cL loc ds'), thing, fvs)
   where
-    rn_deriv_strat :: LDerivStrategy GhcPs
-                   -> RnM (LDerivStrategy GhcRn, a, FreeVars)
-    rn_deriv_strat (dL->L loc ds) = do
+    rn_deriv_strat :: DerivStrategy GhcPs
+                   -> RnM (DerivStrategy GhcRn, a, FreeVars)
+    rn_deriv_strat ds = do
       let extNeeded :: LangExt.Extension
           extNeeded
             | ViaStrategy{} <- ds
@@ -1772,9 +1762,9 @@ rnLDerivStrategy doc mds thing_inside
         failWith $ illegalDerivStrategyErr ds
 
       case ds of
-        StockStrategy    -> boring_case (cL loc StockStrategy)
-        AnyclassStrategy -> boring_case (cL loc AnyclassStrategy)
-        NewtypeStrategy  -> boring_case (cL loc NewtypeStrategy)
+        StockStrategy    -> boring_case StockStrategy
+        AnyclassStrategy -> boring_case AnyclassStrategy
+        NewtypeStrategy  -> boring_case NewtypeStrategy
         ViaStrategy via_ty ->
           do (via_ty', fvs1) <- rnHsSigType doc via_ty
              let HsIB { hsib_ext  = via_imp_tvs
@@ -1782,65 +1772,13 @@ rnLDerivStrategy doc mds thing_inside
                  (via_exp_tv_bndrs, _, _) = splitLHsSigmaTy via_body
                  via_exp_tvs = hsLTyVarNames via_exp_tv_bndrs
                  via_tvs = via_imp_tvs ++ via_exp_tvs
-             (thing, fvs2) <- extendTyVarEnvFVRn via_tvs $
-                              thing_inside via_tvs (ppr via_ty')
-             pure (cL loc (ViaStrategy via_ty'), thing, fvs1 `plusFV` fvs2)
-
-    boring_case :: mds
-                -> RnM (mds, a, FreeVars)
-    boring_case mds = do
-      (thing, fvs) <- thing_inside [] empty
-      pure (mds, thing, fvs)
-
--- | Errors if a @via@ type binds any floating type variables.
--- See @Note [Floating `via` type variables]@
-rnAndReportFloatingViaTvs
-  :: forall a. Outputable a
-  => [Name]  -- ^ The bound type variables from a @via@ type.
-  -> SrcSpan -- ^ The source span (for error reporting only).
-  -> SDoc    -- ^ The pretty-printed @via@ type (for error reporting only).
-  -> String  -- ^ A description of what the @via@ type scopes over
-             --   (for error reporting only).
-  -> RnM (a, FreeVars) -- ^ The thing the @via@ type scopes over.
-  -> RnM (a, FreeVars)
-rnAndReportFloatingViaTvs tv_names loc ppr_via_ty via_scope_desc thing_inside
-  = do (thing, thing_fvs) <- thing_inside
-       setSrcSpan loc $ mapM_ (report_floating_via_tv thing thing_fvs) tv_names
-       pure (thing, thing_fvs)
-  where
-    report_floating_via_tv :: a -> FreeVars -> Name -> RnM ()
-    report_floating_via_tv thing used_names tv_name
-      = unless (tv_name `elemNameSet` used_names) $ addErr $ vcat
-          [ text "Type variable" <+> quotes (ppr tv_name) <+>
-            text "is bound in the" <+> quotes (text "via") <+>
-            text "type" <+> quotes ppr_via_ty
-          , text "but is not mentioned in the derived" <+>
-            text via_scope_desc <+> quotes (ppr thing) <>
-            text ", which is illegal" ]
-
-{-
-Note [Floating `via` type variables]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Imagine the following `deriving via` clause:
-
-    data Quux
-      deriving Eq via (Const a Quux)
+             (thing, fvs2) <- extendTyVarEnvFVRn via_tvs thing_inside
+             pure (ViaStrategy via_ty', thing, fvs1 `plusFV` fvs2)
 
-This should be rejected. Why? Because it would generate the following instance:
-
-    instance Eq Quux where
-      (==) = coerce @(Quux         -> Quux         -> Bool)
-                    @(Const a Quux -> Const a Quux -> Bool)
-                    (==) :: Const a Quux -> Const a Quux -> Bool
-
-This instance is ill-formed, as the `a` in `Const a Quux` is unbound. The
-problem is that `a` is never used anywhere in the derived class `Eq`. Since
-`a` is bound but has no use sites, we refer to it as "floating".
-
-We use the rnAndReportFloatingViaTvs function to check that any type renamed
-within the context of the `via` deriving strategy actually uses all bound
-`via` type variables, and if it doesn't, it throws an error.
--}
+    boring_case :: ds -> RnM (ds, a, FreeVars)
+    boring_case ds = do
+      (thing, fvs) <- thing_inside
+      pure (ds, thing, fvs)
 
 badGadtStupidTheta :: HsDocContext -> SDoc
 badGadtStupidTheta _
diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index c8617b89d1..0863e22cb9 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -685,22 +685,22 @@ deriveStandalone (L loc (DerivDecl _ deriv_ty mb_lderiv_strat overlap_mode))
        ; let ctxt = TcType.InstDeclCtxt True
        ; traceTc "Deriving strategy (standalone deriving)" $
            vcat [ppr mb_lderiv_strat, ppr deriv_ty]
-       ; (mb_lderiv_strat', via_tvs') <- tcDerivStrategy mb_lderiv_strat
-       ; (cls_tvs', deriv_ctxt', cls, inst_tys')
-           <- tcExtendTyVarEnv via_tvs' $
+       ; (mb_lderiv_strat, via_tvs) <- tcDerivStrategy mb_lderiv_strat
+       ; (cls_tvs, deriv_ctxt, cls, inst_tys)
+           <- tcExtendTyVarEnv via_tvs $
               tcStandaloneDerivInstType ctxt deriv_ty
-       ; checkTc (not (null inst_tys')) derivingNullaryErr
-       ; let mb_deriv_strat' = fmap unLoc mb_lderiv_strat'
-             tvs'            = via_tvs' ++ cls_tvs'
-             inst_ty'        = last inst_tys'
+       ; checkTc (not (null inst_tys)) derivingNullaryErr
+       ; let mb_deriv_strat = fmap unLoc mb_lderiv_strat
+             tvs            = via_tvs ++ cls_tvs
+             inst_ty        = last inst_tys
          -- See Note [Unify kinds in deriving]
-       ; (tvs, deriv_ctxt, inst_tys) <-
-           case mb_deriv_strat' of
+       ; (tvs', deriv_ctxt', inst_tys', mb_deriv_strat') <-
+           case mb_deriv_strat of
              -- Perform an additional unification with the kind of the `via`
              -- type and the result of the previous kind unification.
              Just (ViaStrategy via_ty) -> do
                let via_kind     = tcTypeKind via_ty
-                   inst_ty_kind = tcTypeKind inst_ty'
+                   inst_ty_kind = tcTypeKind inst_ty
                    mb_match     = tcUnifyTy inst_ty_kind via_kind
 
                checkTc (isJust mb_match)
@@ -712,38 +712,42 @@ deriveStandalone (L loc (DerivDecl _ deriv_ty mb_lderiv_strat overlap_mode))
                    -- See Note [Unification of two kind variables in deriving]
                    unmapped_tkvs = filter (\v -> v `notElemTCvSubst` kind_subst
                                         && not (v `elemVarSet` ki_subst_range))
-                                          tvs'
+                                          tvs
                    (subst, _)    = substTyVarBndrs kind_subst unmapped_tkvs
                    (final_deriv_ctxt, final_deriv_ctxt_tys)
-                     = case deriv_ctxt' of
+                     = case deriv_ctxt of
                          InferContext wc -> (InferContext wc, [])
                          SupplyContext theta ->
                            let final_theta = substTheta subst theta
                            in (SupplyContext final_theta, final_theta)
-                   final_inst_tys   = substTys subst inst_tys'
+                   final_inst_tys   = substTys subst inst_tys
+                   final_via_ty     = substTy  subst via_ty
+                   -- See Note [Floating `via` type variables]
                    final_tvs        = tyCoVarsOfTypesWellScoped $
                                       final_deriv_ctxt_tys ++ final_inst_tys
-               pure (final_tvs, final_deriv_ctxt, final_inst_tys)
+                                        ++ [final_via_ty]
+               pure ( final_tvs, final_deriv_ctxt, final_inst_tys
+                    , Just (ViaStrategy final_via_ty) )
 
-             _ -> pure (tvs', deriv_ctxt', inst_tys')
-       ; let cls_tys = take (length inst_tys - 1) inst_tys
-             inst_ty = last inst_tys
+             _ -> pure (tvs, deriv_ctxt, inst_tys, mb_deriv_strat)
+       ; let cls_tys' = take (length inst_tys' - 1) inst_tys'
+             inst_ty' = last inst_tys'
        ; traceTc "Standalone deriving;" $ vcat
-              [ text "tvs:" <+> ppr tvs
-              , text "mb_deriv_strat:" <+> ppr mb_deriv_strat'
-              , text "deriv_ctxt:" <+> ppr deriv_ctxt
+              [ text "tvs':" <+> ppr tvs'
+              , text "mb_deriv_strat':" <+> ppr mb_deriv_strat'
+              , text "deriv_ctxt':" <+> ppr deriv_ctxt'
               , text "cls:" <+> ppr cls
-              , text "tys:" <+> ppr inst_tys ]
+              , text "inst_tys':" <+> ppr inst_tys' ]
                 -- C.f. TcInstDcls.tcLocalInstDecl1
        ; traceTc "Standalone deriving:" $ vcat
               [ text "class:" <+> ppr cls
-              , text "class types:" <+> ppr cls_tys
-              , text "type:" <+> ppr inst_ty ]
+              , text "class types:" <+> ppr cls_tys'
+              , text "type:" <+> ppr inst_ty' ]
 
-       ; let bale_out msg = failWithTc (derivingThingErr False cls cls_tys
-                              inst_ty mb_deriv_strat' msg)
+       ; let bale_out msg = failWithTc (derivingThingErr False cls cls_tys'
+                              inst_ty' mb_deriv_strat' msg)
 
-       ; case tcSplitTyConApp_maybe inst_ty of
+       ; case tcSplitTyConApp_maybe inst_ty' of
            Just (tc, tc_args)
               | className cls == typeableClassName
               -> do warnUselessTypeable
@@ -751,8 +755,8 @@ deriveStandalone (L loc (DerivDecl _ deriv_ty mb_lderiv_strat overlap_mode))
 
               | otherwise
               -> Just <$> mkEqnHelp (fmap unLoc overlap_mode)
-                                    tvs cls cls_tys tc tc_args
-                                    deriv_ctxt mb_deriv_strat'
+                                    tvs' cls cls_tys' tc tc_args
+                                    deriv_ctxt' mb_deriv_strat'
 
            _  -> -- Complain about functions, primitive types, etc,
                  bale_out $
@@ -851,66 +855,69 @@ deriveTyData tc tc_args mb_deriv_strat deriv_tvs cls cls_tys cls_arg_kind
         ; checkTc (enough_args && isJust mb_match)
                   (derivingKindErr tc cls cls_tys cls_arg_kind enough_args)
 
-        ; let propagate_subst kind_subst tkvs' cls_tys' tc_args'
-                = (final_tkvs, final_cls_tys, final_tc_args)
+        ; let -- Returns a singleton-element list if using ViaStrategy and an
+              -- empty list otherwise. Useful for free-variable calculations.
+              deriv_strat_tys :: Maybe (DerivStrategy GhcTc) -> [Type]
+              deriv_strat_tys = foldMap (foldDerivStrategy [] (:[]))
+
+              propagate_subst kind_subst tkvs' cls_tys' tc_args' mb_deriv_strat'
+                = (final_tkvs, final_cls_tys, final_tc_args, final_mb_deriv_strat)
                 where
                   ki_subst_range  = getTCvSubstRangeFVs kind_subst
                   -- See Note [Unification of two kind variables in deriving]
                   unmapped_tkvs   = filter (\v -> v `notElemTCvSubst` kind_subst
                                          && not (v `elemVarSet` ki_subst_range))
                                            tkvs'
-                  (subst, _)      = substTyVarBndrs kind_subst unmapped_tkvs
-                  final_tc_args   = substTys subst tc_args'
-                  final_cls_tys   = substTys subst cls_tys'
-                  final_tkvs      = tyCoVarsOfTypesWellScoped $
-                                    final_cls_tys ++ final_tc_args
+                  (subst, _)           = substTyVarBndrs kind_subst unmapped_tkvs
+                  final_tc_args        = substTys subst tc_args'
+                  final_cls_tys        = substTys subst cls_tys'
+                  final_mb_deriv_strat = fmap (mapDerivStrategy (substTy subst))
+                                              mb_deriv_strat'
+                  -- See Note [Floating `via` type variables]
+                  final_tkvs           = tyCoVarsOfTypesWellScoped $
+                                         final_cls_tys ++ final_tc_args
+                                           ++ deriv_strat_tys final_mb_deriv_strat
 
         ; let tkvs = scopedSort $ fvVarList $
                      unionFV (tyCoFVsOfTypes tc_args_to_keep)
                              (FV.mkFVs deriv_tvs)
               Just kind_subst = mb_match
-              (tkvs', final_cls_tys', final_tc_args')
-                = propagate_subst kind_subst tkvs cls_tys tc_args_to_keep
+              (tkvs', cls_tys', tc_args', mb_deriv_strat')
+                = propagate_subst kind_subst tkvs cls_tys
+                                  tc_args_to_keep mb_deriv_strat
 
           -- See Note [Unify kinds in deriving]
-        ; (tkvs, final_cls_tys, final_tc_args, final_mb_deriv_strat) <-
-            case mb_deriv_strat of
+        ; (final_tkvs, final_cls_tys, final_tc_args, final_mb_deriv_strat) <-
+            case mb_deriv_strat' of
               -- Perform an additional unification with the kind of the `via`
               -- type and the result of the previous kind unification.
               Just (ViaStrategy via_ty) -> do
-                let final_via_ty   = via_ty
-                    final_via_kind = tcTypeKind final_via_ty
-                    final_inst_ty_kind
-                              = tcTypeKind (mkTyConApp tc final_tc_args')
-                    via_match = tcUnifyTy final_inst_ty_kind final_via_kind
+                let via_kind = tcTypeKind via_ty
+                    inst_ty_kind
+                              = tcTypeKind (mkTyConApp tc tc_args')
+                    via_match = tcUnifyTy inst_ty_kind via_kind
 
                 checkTc (isJust via_match)
-                        (derivingViaKindErr cls final_inst_ty_kind
-                                            final_via_ty final_via_kind)
+                        (derivingViaKindErr cls inst_ty_kind via_ty via_kind)
 
                 let Just via_subst = via_match
-                    (final_tkvs, final_cls_tys, final_tc_args)
-                      = propagate_subst via_subst tkvs'
-                                        final_cls_tys' final_tc_args'
-                pure ( final_tkvs, final_cls_tys, final_tc_args
-                     , Just $ ViaStrategy $ substTy via_subst via_ty
-                     )
+                pure $ propagate_subst via_subst tkvs' cls_tys'
+                                       tc_args' mb_deriv_strat'
 
-              _ -> pure ( tkvs', final_cls_tys', final_tc_args'
-                        , mb_deriv_strat )
+              _ -> pure (tkvs', cls_tys', tc_args', mb_deriv_strat')
 
         ; traceTc "deriveTyData 1" $ vcat
-            [ ppr mb_deriv_strat, pprTyVars deriv_tvs, ppr tc, ppr tc_args
+            [ ppr final_mb_deriv_strat, pprTyVars deriv_tvs, ppr tc, ppr tc_args
             , pprTyVars (tyCoVarsOfTypesList tc_args)
             , ppr n_args_to_keep, ppr n_args_to_drop
             , ppr inst_ty_kind, ppr cls_arg_kind, ppr mb_match
             , ppr final_tc_args, ppr final_cls_tys ]
 
         ; traceTc "deriveTyData 2" $ vcat
-            [ ppr tkvs ]
+            [ ppr final_tkvs ]
 
         ; let final_tc_app = mkTyConApp tc final_tc_args
-        ; checkTc (allDistinctTyVars (mkVarSet tkvs) args_to_drop)     -- (a, b, c)
+        ; checkTc (allDistinctTyVars (mkVarSet final_tkvs) args_to_drop) -- (a, b, c)
                   (derivingEtaErr cls final_cls_tys final_tc_app)
                 -- Check that
                 --  (a) The args to drop are all type variables; eg reject:
@@ -932,7 +939,7 @@ deriveTyData tc tc_args mb_deriv_strat deriv_tvs cls cls_tys cls_arg_kind
                 -- Check that we aren't deriving an instance of a magical
                 -- type like (~) or Coercible (#14916).
 
-        ; spec <- mkEqnHelp Nothing tkvs
+        ; spec <- mkEqnHelp Nothing final_tkvs
                             cls final_cls_tys tc final_tc_args
                             (InferContext Nothing) final_mb_deriv_strat
         ; traceTc "deriveTyData 3" (ppr spec)
@@ -1137,6 +1144,73 @@ synonym, we will mistakenly believe that f is an eta-reduced type variable and
 fail to derive Functor, even though the code above is correct (see #11416,
 where this was first noticed). For this reason, we expand the type synonyms in
 the eta-reduced types before doing any analysis.
+
+Note [Floating `via` type variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When generating a derived instance, it will be of the form:
+
+  instance forall ???. C c_args (D d_args) where ...
+
+To fill in ???, GHC computes the free variables of `c_args` and `d_args`.
+`DerivingVia` adds an extra wrinkle to this formula, since we must also
+include the variables bound by the `via` type when computing the binders
+used to fill in ???. This might seem strange, since if a `via` type binds
+any type variables, then in almost all scenarios it will appear free in
+`c_args` or `d_args`. There are certain corner cases where this does not hold,
+however, such as in the following example (adapted from #15831):
+
+  newtype Age = MkAge Int
+    deriving Eq via Const Int a
+
+In this example, the `via` type binds the type variable `a`, but `a` appears
+nowhere in `Eq Age`. Nevertheless, we include it in the generated instance:
+
+  instance forall a. Eq Age where
+    (==) = coerce @(Const Int a -> Const Int a -> Bool)
+                  @(Age         -> Age         -> Bool)
+                  (==)
+
+The use of `forall a` is certainly required here, since the `a` in
+`Const Int a` would not be in scope otherwise. This instance is somewhat
+strange in that nothing in the instance head `Eq Age` ever determines what `a`
+will be, so any code that uses this instance will invariably instantiate `a`
+to be `Any`. We refer to this property of `a` as being a "floating" `via`
+type variable. Programs with floating `via` type variables are the only known
+class of program in which the `via` type quantifies type variables that aren't
+mentioned in the instance head in the generated instance.
+
+Fortunately, the choice to instantiate floating `via` type variables to `Any`
+is one that is completely transparent to the user (since the instance will
+work as expected regardless of what `a` is instantiated to), so we decide to
+permit them. An alternative design would make programs with floating `via`
+variables illegal, by requiring that every variable mentioned in the `via` type
+is also mentioned in the data header or the derived class. That restriction
+would require the user to pick a particular type (the choice does not matter);
+for example:
+
+  newtype Age = MkAge Int
+    -- deriving Eq via Const Int a  -- Floating 'a'
+    deriving Eq via Const Int ()    -- Choose a=()
+    deriving Eq via Const Int Any   -- Choose a=Any
+
+No expressiveness would be lost thereby, but stylistically it seems preferable
+to allow a type variable to indicate "it doesn't matter".
+
+Note that by quantifying the `a` in `forall a. Eq Age`, we are deferring the
+work of instantiating `a` to `Any` at every use site of the instance. An
+alternative approach would be to generate an instance that directly defaulted
+to `Any`:
+
+  instance Eq Age where
+    (==) = coerce @(Const Int Any -> Const Int Any -> Bool)
+                  @(Age           -> Age           -> Bool)
+                  (==)
+
+We do not implement this approach since it would require a nontrivial amount
+of implementation effort to substitute `Any` for the floating `via` type
+variables, and since the end result isn't distinguishable from the former
+instance (at least from the user's perspective), the amount of engineering
+required to obtain the latter instance just isn't worth it.
 -}
 
 mkEqnHelp :: Maybe OverlapMode