ATF cache: record only coherent resolutions; pin the hit path with tests

An incoherent match is an information-dependent choice (it varies with
-allow-incoherent-matches, in-scope instances, and import order), so
persisting its ATF projection into the .bo cache would deliver a
context-dependent answer to importing compiles as if it were canonical.
Drop the recordATFs call from the incoherent arm; coherent full
discharges still record.

The cache previously had only miss-path tests, so a lost recording site
would go unnoticed by a green suite.  Add hit tests: a same-package hit
(ground resolution recorded by a monomorphic definition, consumed when
elaborating a polymorphic body) and a cross-package hit delivered
through the .bo cache, both asserted via -trace-atf-cache.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019cqQdWKp7jr73GHQYnvhiq

Author: 2 people

src/comp/TCMisc.hs

@@ -403,7 +403,11 @@ sat dvs ps p =
                 (ps@(_:_), sbs, s_final) -> return $ (ps, sbs, s_final)
                 ([], sbs, s_final) -> do
                   recordPackageUse mpkg
-                  recordATFs s_final
+                  -- No recordATFs here: an incoherent match is an
+                  -- information-dependent choice (context-, flag- and
+                  -- import-order-dependent), so its ATF projection must
+                  -- not be recorded where the .bo cache would deliver it
+                  -- to importing compiles as if it were canonical.
                   let (vp_pred, inst_pred) = niceTypes (apSub s_final (toPred p, h))
                   let pos = getPosition $ getVPredPositions p
                   let VPred dictId _ = p

testsuite/bsc.typechecker/typeclasses/ATFCacheHit.bs

@@ -0,0 +1,48 @@
+package ATFCacheHit where
+
+-- Test that a ground ATF resolution recorded by ctxreduce during
+-- typecheck is delivered to iExpand and HITS in the ATF cache.
+-- forceGround solves Encode ((UInt 5, UInt 5)) monomorphically at
+-- typecheck time, so EncSize ((UInt 5, UInt 5)) is recorded ground;
+-- elaborating checkPair's polymorphic body at (UInt 5, UInt 5) then
+-- finds it in the cache instead of falling back to normTFun.
+-- (Cache-hit twin of ATFPolyCacheMiss.bs.)
+
+class Encode a n | a -> n where
+    type EncSize a = n
+    encode :: a -> Bit n
+
+instance Encode (UInt k) k where
+    encode x = pack x
+
+instance Encode Bool 1 where
+    encode True  = 1
+    encode False = 0
+
+instance (Encode a sa, Encode b sb) => Encode (a, b) (TAdd sa sb) where
+    encode (x, y) = encode x ++ encode y
+
+data Encoded a = Encoded (Bit (EncSize a))
+
+wrap :: (Encode a sa) => a -> Encoded a
+wrap x = Encoded (encode x)
+
+checkPair :: (Encode a sa) => a -> Bool
+checkPair x = case wrap (x, x) of
+                 Encoded b -> msb b == 1
+
+-- The monomorphic forcing definition: typechecking this solves
+-- Encode ((UInt 5, UInt 5)) ground and records its EncSize result.
+forceGround :: (UInt 5, UInt 5) -> Encoded (UInt 5, UInt 5)
+forceGround p = wrap p
+
+{-# verilog sysATFCacheHit #-}
+sysATFCacheHit :: Module Empty
+sysATFCacheHit = module
+  r :: Reg (UInt 5) <- mkReg 7
+  rules
+    "test": when True ==>
+      action
+        let result = checkPair r
+        $display "result: %b" (pack result)
+        $finish 0

testsuite/bsc.typechecker/typeclasses/ATFCacheHitDef.bs

@@ -0,0 +1,32 @@
+package ATFCacheHitDef where
+
+-- Cross-package half of the ATF cache-hit test: the ground
+-- resolution EncSize ((UInt 5, UInt 5)) is solved and recorded
+-- HERE (by forceGround), stored in this package's .bo cache, and
+-- must be delivered to the importing package's elaboration.
+
+class Encode a n | a -> n where
+    type EncSize a = n
+    encode :: a -> Bit n
+
+instance Encode (UInt k) k where
+    encode x = pack x
+
+instance Encode Bool 1 where
+    encode True  = 1
+    encode False = 0
+
+instance (Encode a sa, Encode b sb) => Encode (a, b) (TAdd sa sb) where
+    encode (x, y) = encode x ++ encode y
+
+data Encoded a = Encoded (Bit (EncSize a))
+
+wrap :: (Encode a sa) => a -> Encoded a
+wrap x = Encoded (encode x)
+
+checkPair :: (Encode a sa) => a -> Bool
+checkPair x = case wrap (x, x) of
+                 Encoded b -> msb b == 1
+
+forceGround :: (UInt 5, UInt 5) -> Encoded (UInt 5, UInt 5)
+forceGround p = wrap p

testsuite/bsc.typechecker/typeclasses/ATFCacheHitUse.bs

@@ -0,0 +1,19 @@
+package ATFCacheHitUse where
+
+import ATFCacheHitDef
+
+-- The only ground pred THIS package's typecheck solves is
+-- Encode (UInt 5) (checkPair's proviso), so a hit on the
+-- pair-shaped EncSize ((UInt 5, UInt 5)) during elaboration can
+-- only come from ATFCacheHitDef's .bo-delivered cache.
+
+{-# verilog sysATFCacheHitUse #-}
+sysATFCacheHitUse :: Module Empty
+sysATFCacheHitUse = module
+  r :: Reg (UInt 5) <- mkReg 7
+  rules
+    "test": when True ==>
+      action
+        let result = checkPair r
+        $display "result: %b" (pack result)
+        $finish 0

testsuite/bsc.typechecker/typeclasses/typeclasses.exp

@@ -118,6 +118,19 @@ compile_verilog_pass ATFPolyStructMultiParam.bs
 compile_verilog_pass ATFPolyCacheMiss.bs {} "-dexpanded=expanded_%m.out"
 find_n_strings expanded_sysATFPolyCacheMiss.out "EncSize" 0
 
+# Test that a ground ATF resolution recorded at typecheck time HITS
+# the cache during iExpand (same package)
+compile_backend_pass ATFCacheHit.bs {-trace-atf-cache}
+find_regexp ATFCacheHit.bs.bsc-out {ATF cache hit: .*EncSize.*PrimPair}
+find_n_strings ATFCacheHit.bs.bsc-out {ATF cache miss: ATFCacheHit.EncSize} 0
+
+# Test that a ground ATF resolution recorded in an imported package
+# is delivered through its .bo file and HITS in the importer's iExpand
+compile_pass ATFCacheHitDef.bs
+compile_backend_pass ATFCacheHitUse.bs {-trace-atf-cache} 1
+find_regexp ATFCacheHitUse.bs.bsc-out {ATF cache hit: .*EncSize.*PrimPair}
+find_n_strings ATFCacheHitUse.bs.bsc-out {ATF cache miss: ATFCacheHitDef.EncSize} 0
+
 # Test ATF error cases
 
 compile_fail_error ATFWrongArity.bs T0025