Fix data-family R: rewrite to substitute rep tyvars with use-site args

The previous rewrite (commit 723a7c3) called tyConFamInst_maybe and
fed parentArgs straight into typeArg. parentArgs reference the rep
TyCon's *internal* type variables, not the use-site args; without a
substitution they leak through typeArg's TyVar lookup as
@OtherArg "<reptv>"@ because they're absent from boundTvs. So
@R:CrateList Int@ was rewriting to @Crate [<reptv>]@ — which broke
both the rendering (the user saw rep-internal names) and the chain
resolution (replaceFamilyApp's biUnify still succeeded by luck of
the wildcard rule, but the visible label was wrong).

Build a Subst from the rep's tyConTyVars to the actual use-site args
and apply it to parentArgs before recursing. With this fix
@R:CrateList Int@ extracts as @FamilyApp Crate [TyConApp List
[TyConApp Int []]]@ and renders as @Crate [Int]@; the polymorphic
case @R:CrateList a@ in an instance head extracts as
@FamilyApp Crate [TyConApp List [TyVarRef 0]]@ and renders as
@Crate [a]@.

Demo gains a @CrateBound (Crate [a])@ instance so the polymorphic-rep
path is regression-covered.

Co-Authored-By: Claude Opus 4.7 (1M context) <[email protected]>

diff --git a/examples/demo/src/Demo/MoreFamilies.hs b/examples/demo/src/Demo/MoreFamilies.hs
index f9d627533258a5ecdaf864d0387264475ad3a331..9d3b5336cb5e7ef3ff4651ff989f45ac2c7e1b7a 100644 (file)
--- a/examples/demo/src/Demo/MoreFamilies.hs
+++ b/examples/demo/src/Demo/MoreFamilies.hs
@@ -54,6 +54,18 @@ data instance Crate Int  = CrateInt  Int
 data instance Crate Bool = CrateBool Bool
 data instance Crate [a]  = CrateList [a]
 
+-- Exercises the data-family rep-tyvar substitution: a polymorphic
+-- instance whose head mentions @Crate [a]@. After typechecking GHC
+-- represents the head as the synthetic rep TyCon @R:CrateList a@; the
+-- viewer should rewrite that back to the abstract @Crate [a]@ form
+-- with @a@ properly bound to the instance's tyvar (NOT leak the rep
+-- TyCon's internal tyvar as @OtherArg "a"@).
+class CrateBound a where
+  cbDescribe :: proxy a -> String
+
+instance CrateBound (Crate [a]) where
+  cbDescribe _ = "list crate"
+
 -- A class parameterised by a /promoted-list/ kind. Demonstrates that
 -- the viewer renders `'[Int, Bool]` as `[Int, Bool]`, not the
 -- nested-cons `(: Int (: Bool []))` shape.

diff --git a/src/Classgraph/Extract.hs b/src/Classgraph/Extract.hs
index c620aa1d3f698f16eba3853c3043706e103740db..ebd0b8d40d821a408317ee5be376f975d17507ca 100644 (file)
--- a/src/Classgraph/Extract.hs
+++ b/src/Classgraph/Extract.hs
@@ -73,6 +73,8 @@ import GHC.Core.Type
   , isLitTy
   , splitTyConApp_maybe
   , splitVisibleFunTy_maybe
+  , substTys
+  , zipTvSubst
   )
 import GHC.Hs.Doc (Docs (..), HsDoc, hsDocString)
 import GHC.Hs.DocString (renderHsDocString)
@@ -439,8 +441,19 @@ typeArg boundTvs t =
           -- finding the matching @data instance@ row and connecting
           -- it to any class instance of e.g. @NoThunks (Foo Args)@.
           | Just (parent, parentArgs) <- tyConFamInst_maybe tc ->
-              FamilyApp (qualName (tyConName parent))
-                        (map (typeArg boundTvs) parentArgs)
+              -- @parentArgs@ are the abstract data-instance LHS args
+              -- (e.g. @[ShelleyBlock <reptv1> <reptv2>]@), referencing
+              -- the *rep TyCon's* type variables — NOT the use-site
+              -- args. Without substitution those rep tyvars leak into
+              -- the rendered form as @OtherArg "<reptv1>"@ because
+              -- they're not in the caller's @boundTvs@. Build a
+              -- Subst from the rep's tyvars to the actual use-site
+              -- args and apply it before recursing.
+              let repTvs       = tyConTyVars tc
+                  sub          = zipTvSubst repTvs args
+                  instantiated = substTys sub parentArgs
+               in FamilyApp (qualName (tyConName parent))
+                            (map (typeArg boundTvs) instantiated)
           | otherwise ->
               let visArgs = visibleArgs tc args
                   kids    = map (typeArg boundTvs) visArgs