From 429e85a68fb034b6b5d071356230da83c34548f9 Mon Sep 17 00:00:00 2001
From: Lucas Kramer <lucas@matx.com>
Date: Thu, 25 Jun 2026 22:07:49 -0700
Subject: [PATCH] typecheck: apply substitution to sibling preds in satMany'
 Right branch (PR 980)

When satMany' only partially reduces a predicate (the "still-needed" /
Right branch), it commits the learned substitution s' to the accumulator
(s' @@ s) but did not apply it to the not-yet-processed sibling
predicates ps. The fully-solved (Left) branch already does this
(apSub s' ps). Because of the asymmetry, a sibling predicate that is
determined (via a functional dependency) by a variable that s' had just
grounded was matched against an unbound variable and left unreduced, so
its own fundep never fired.

This surfaced as a spurious T0029 ("Signature mismatch (given too
general)"): a partially-solved proviso grounds the input of a sibling
fundep'd proviso, but because the grounding was not propagated the
sibling stayed unreduced and the instance's determined parameter was
left general in the declared head -- while the method body grounded it.

Fix: apply s' to ps in the Right branch too, matching the Left branch.
This only propagates an already-committed substitution, so it adds no
new reduction rounds and cannot affect termination.
---
 src/comp/TCMisc.hs                            |  4 +-
 .../ctxreduce/SiblingFundepSubst.bs           | 38 +++++++++++++++++++
 .../bsc.typechecker/ctxreduce/ctxreduce.exp   |  9 +++++
 3 files changed, 50 insertions(+), 1 deletion(-)
 create mode 100644 testsuite/bsc.typechecker/ctxreduce/SiblingFundepSubst.bs

diff --git a/src/comp/TCMisc.hs b/src/comp/TCMisc.hs
index 36ea623cf..431b9804a 100644
--- a/src/comp/TCMisc.hs
+++ b/src/comp/TCMisc.hs
@@ -450,8 +450,10 @@ satMany' dvs es rs_accum sbs s (p:ps) = do
             -- prevented satisfying -- is this apSub just covering for an
             -- issue elsewhere (that should not have returned unsubst'd preds)?
             --
+            -- Since we apply "s" to "needed", we also apply it to the not-yet-
+            -- processed preds "ps".
             rtrace ("satMany Right: " ++ ppReadable needed) $
-            satMany' dvs es ((apSub s' needed) ++ rs_accum) (sbs' <++ sbs) (s' @@ s) ps
+            satMany' dvs es ((apSub s' needed) ++ rs_accum) (sbs' <++ sbs) (s' @@ s) (apSub s' ps)
         ([], sbs', s') ->
             -- If p is satisfied, we "drop" it, but add its binding and
             -- substitution.
diff --git a/testsuite/bsc.typechecker/ctxreduce/SiblingFundepSubst.bs b/testsuite/bsc.typechecker/ctxreduce/SiblingFundepSubst.bs
new file mode 100644
index 000000000..6782d7a2c
--- /dev/null
+++ b/testsuite/bsc.typechecker/ctxreduce/SiblingFundepSubst.bs
@@ -0,0 +1,38 @@
+package SiblingFundepSubst where
+
+-- Regression test: context reduction must apply a substitution learned from
+-- a *partially* solved proviso to its sibling provisos in the same pass.
+--
+-- Reducing `G (Proxy a) c` grounds `c` to Bool (via the instance below) but
+-- leaves the residual `Foo a` (no instance), so it is only partially solved.
+-- The sibling `Det c o` has a functional dependency `c -> o`, so once `c` is
+-- known to be Bool it determines `o = Port Bool`.  satMany' used to commit the
+-- `c := Bool` substitution but not apply it to the not-yet-processed sibling,
+-- so `Det c o` was matched against an unbound `c`, left unreduced, and `o`
+-- stayed quantified in the declared instance head -- while the method body
+-- grounded `o` to `Port Bool`.  That mismatch produced a spurious T0029
+-- ("Signature mismatch (given too general)").  This must compile.
+
+data Port t = Port
+data Proxy a = Proxy
+
+-- An always-residual proviso (no instances): keeps G only partially solved.
+class Foo a where {}
+
+-- Output determined from input by a fundep; resolves only for ground input.
+class Det c o | c -> o where
+  det :: c -> o
+instance Det Bool (Port Bool) where
+  det _ = Port
+
+-- Reducing G grounds c to Bool, but leaves the residual (Foo a).
+class G x c | x -> c where
+  g :: x -> c
+instance (Foo a) => G (Proxy a) Bool where
+  g _ = True
+
+-- o is determined by the sibling Det, whose input c is grounded by G.
+class S a o | a -> o where
+  s :: a -> o
+instance (G (Proxy a) c, Det c o) => S (Proxy a) o where
+  s p = det (g p)
diff --git a/testsuite/bsc.typechecker/ctxreduce/ctxreduce.exp b/testsuite/bsc.typechecker/ctxreduce/ctxreduce.exp
index 25d42dabc..81ba1af7f 100644
--- a/testsuite/bsc.typechecker/ctxreduce/ctxreduce.exp
+++ b/testsuite/bsc.typechecker/ctxreduce/ctxreduce.exp
@@ -17,3 +17,12 @@ compile_pass AliasSizeOf.bsv
 compile_pass AliasSizeOf_Instance.bsv
 
 # ---------------
+# Test that a substitution learned while *partially* solving a proviso (one
+# that grounds a variable but leaves a residual) is applied to the sibling
+# provisos in the same satMany' pass, so a sibling determined by that variable
+# via a functional dependency can reduce.  Otherwise the determined instance
+# parameter is left general and a spurious T0029 is reported.
+
+compile_pass SiblingFundepSubst.bs
+
+# ---------------