[pull] main from B-Lang-org:main

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.

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)

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
+
+# ---------------