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

DEVELOP.md

@@ -41,6 +41,12 @@ The following is a running list of those writings.
 * Names that BSC has built-in knowledge of (such as definitions in the Prelude)
   are specified in `src/comp/PreStrings.hs`, which are then wrapped as identifiers
   in `src/comp/PreIds.hs`
+* For Haskell Language Server (HLS) setup see the dedicated [README file](./util/haskell-language-server/README.md)
+* The [GitHub CI](./.github/workflows/) can serve as an example of building and working with the source.
+  See, for example, [build-and-test-ubuntu.yml](./.github/workflows/build-and-test-ubuntu.yml) which contains steps for:
+  * Installing dependencies
+  * Running the Haskell Language Server (HLS)
+  * Running GHC's interactive environment (GHCi)
 
 ### Compiling
 

src/comp/ISyntaxCheck.hs

@@ -3,6 +3,7 @@ module ISyntaxCheck(iGetKind,
                     tCheckIPackage,
                     tCheckIModule) where
 
+import Data.List (mapAccumL)
 import qualified Data.Map as M
 import qualified Data.Set as S
 import qualified EquivalenceClass as EC
@@ -76,23 +77,45 @@ eqType1 _ _ _ (ITNum n) (ITNum n') = n == n'
 eqType1 _ _ _ _ _ = False
 
 -- Decide if two (numeric) types are equal by creating a NumEq proviso
--- in CSyntax and applying "satisfy".
+-- in CSyntax and applying "satisfy".  In addition to the explicit
+-- preds from the env's PredEnv, we inject the env's numeric-kind EC
+-- equivalences as NumEq preds.  Without that, predicates implied by
+-- the env --- e.g. `Bits (a, b) sab <= (Bits a sa, Bits b sb, Add sa
+-- sb sab)` decomposes the parent's `SizeOf (a, b) ≡ sab` link into
+-- only the three sub-preds; fundep-derived sub-goals like `NumEq sa
+-- sa'` (when the env has two `Bits a _` dicts with different result
+-- vars) cannot be discharged even though the EC records `sa ≡ sa'`.
 eqTypeNum :: Flags -> SymTab -> Env -> IType -> IType -> Bool
-eqTypeNum flags symt r t1 t2
+eqTypeNum flags symt r@(E _ _ ecRaw _) t1 t2
     -- Attempt to save time by weeding out cases without TAdd, SizeOf, etc
     -- (since there's no use trying to equate "n" and "m", for instance)
     -- XXX can we also weed out when the kind is not numeric?
     | isITAp t1 || isITAp t2 =
     let numEqCls = mustFindClass symt (CTypeclass idNumEq)
         (r', t1') = convType r t1
-        (E _ _ _ (PredEnv _ m s), t2') = convType r' t2
-        --satisfyEq :: TI ([VPred], [CDefl])
+        (rWithT2@(E _ _ _ (PredEnv _ m s)), t2') = convType r' t2
+        -- For each numeric-kind EC class, emit a spanning tree of
+        -- equalities (n-1 pairs, not all n*(n-1)/2) --- satisfy chases
+        -- transitively via unification, so this is enough.
+        ecNumEqITypes =
+            [ (x, y)
+            | cls@(x:rest) <- EC.classes ecRaw
+            , kCheck r x == Just IKNum
+            , y <- rest
+            ]
+        (_, ecNumEqTypes) =
+            mapAccumL (\env (a, b) -> let (env1, ta) = convType env a
+                                          (env2, tb) = convType env1 b
+                                      in  (env2, (ta, tb)))
+                      rWithT2 ecNumEqITypes
         satisfyEq = do
           eqs <- mapM mkEPred (S.toList s)
+          ecEqs <- mapM (\(a, b) -> mkEPred (IsIn numEqCls [a, b]))
+                        ecNumEqTypes
           addBoundTVs (M.elems m)
-          addExplPreds eqs
+          addExplPreds (eqs ++ ecEqs)
           vp <- mkVPredFromPred [] (IsIn numEqCls [t1', t2'])
-          satisfy eqs [vp]
+          satisfy (eqs ++ ecEqs) [vp]
     in  case runTI flags False symt satisfyEq of
           (Right ([],_), _, _) -> True
           res -> --trace("eqTypeNum: not satisfied: " ++ ppReadable (t1, t2, res)) $

src/comp/ISyntaxUtil.hs

@@ -1117,11 +1117,11 @@ getStateVarNames _ = []
 
 iTLog, iTAdd, iTMax, iTMin, iTMul, iTDiv :: IType
 iTLog = ITCon idTLog (IKNum `IKFun` IKNum) TIabstract
-iTAdd = ITCon idTAdd (IKNum `IKFun` IKNum `IKFun` IKNum) TIabstract
-iTMax = ITCon idTMax (IKNum `IKFun` IKNum `IKFun` IKNum) TIabstract
-iTMin = ITCon idTMin (IKNum `IKFun` IKNum `IKFun` IKNum) TIabstract
-iTMul = ITCon idTMul (IKNum `IKFun` IKNum `IKFun` IKNum) TIabstract
-iTDiv = ITCon idTDiv (IKNum `IKFun` IKNum `IKFun` IKNum) TIabstract
+iTAdd = ITCon idTAdd (IKNum `IKFun` (IKNum `IKFun` IKNum)) TIabstract
+iTMax = ITCon idTMax (IKNum `IKFun` (IKNum `IKFun` IKNum)) TIabstract
+iTMin = ITCon idTMin (IKNum `IKFun` (IKNum `IKFun` IKNum)) TIabstract
+iTMul = ITCon idTMul (IKNum `IKFun` (IKNum `IKFun` IKNum)) TIabstract
+iTDiv = ITCon idTDiv (IKNum `IKFun` (IKNum `IKFun` IKNum)) TIabstract
 
 iDefMap :: (IExpr a -> IExpr a) -> IDef a -> IDef a
 iDefMap f (IDef i t e p) = IDef i t (f e) p

testsuite/bsc.bugs/bluespec_inc/b1490/b1490.exp

@@ -20,6 +20,6 @@ compile_verilog_fail VsortOriginal.bsv {} $rtsflags
 # Confirm that the test failed in the way we expect
 find_n_strings [make_bsc_vcomp_output_name VsortOriginal.bsv] "Heap exhausted" 1
 
-compile_verilog_pass VsortWorkaround.bsv {} [rts_flags 272]
+compile_verilog_pass VsortWorkaround.bsv {} [rts_flags 275]
 
 # -----

testsuite/bsc.typechecker/typeclasses/ATFPairAddDecompose.bs

@@ -0,0 +1,28 @@
+package ATFPairAddDecompose where
+
+-- Regression test for a post-inference type-check assert ("assert
+-- failed: IAp" in ISyntaxCheck.eqTypeNum) triggered by an ATF on a
+-- class whose 2-ary instance decomposes the ATF target into TAdd of
+-- the component ATFs, used inside a rank-2 polymorphic struct field.
+--
+-- Pattern: `C (P a b) sab <= (C a sa, C b sb, Add sa sb sab)` (where
+-- `class C c sz | c -> sz; type W c = sz`). After reducing the
+-- parent dict, only the three sub-preds remain; the equation
+-- `W (P a b) ≡ sab` is destroyed.  Post-inference type checking has
+-- to reconstruct that equation in eqTypeNum to discharge the goal
+-- `Bit _v ≡ Bit (W (P c f))`.
+
+class C c sz | c -> sz where { type W c = sz }
+
+data P a b = P
+
+instance (C a sa, C b sb, Add sa sb sab) => C (P a b) sab where { }
+
+struct Table ctrl flavor =
+  access :: Bit (W (P ctrl flavor)) -> Action
+
+struct Op ctrl =
+  act :: (C (P ctrl flavor) _b) => Table ctrl flavor -> Action
+
+useIt :: (C c _x) => Op c
+useIt = Op { act = \ t -> t.access 0; }

testsuite/bsc.typechecker/typeclasses/typeclasses.exp

@@ -162,4 +162,12 @@ compare_file ATFWrongArityBSV.bsv.bsc-out
 compile_fail_error ATFDeclParamMismatchBSV.bsv T0152
 compare_file ATFDeclParamMismatchBSV.bsv.bsc-out
 
+# Regression: a rank-2 polymorphic struct field whose proviso uses
+# a class whose instance decomposes the ATF target into TAdd of the
+# component ATFs used to trigger an internal "assert failed: IAp"
+# (post-inference type check) because the parent ATF link was lost
+# during instance reduction.
+
+compile_pass ATFPairAddDecompose.bs
+
 # --------------------------------------------------