From 2d7b7b427b102ddd6fc7dfc8072cdb4f302a6aba Mon Sep 17 00:00:00 2001 From: Lucas Kramer Date: Mon, 13 Apr 2026 12:58:51 -0700 Subject: [PATCH 01/12] Fix #890 by expanding type functions in tiExpl Also adds tests including the ones added by @quark17 in #909 --- src/comp/CtxRed.hs | 5 +--- src/comp/TCheck.hs | 9 ++++++- .../primtcons/ExpSizeOf_FieldSyn_BS.bs | 20 +++++++++++++++ .../primtcons/ExpSizeOf_FieldSyn_Minimal.bs | 10 ++++++++ .../primtcons/ExpSizeOf_Let_NoCtx.bs | 11 ++++++++ .../ExpSizeOf_Let_NoCtx.bs.bsc-out.expected | 12 +++++++++ .../primtcons/ExpSizeOf_StringOf_NoCtx.bs | 12 +++++++++ ...pSizeOf_StringOf_NoCtx.bs.bsc-out.expected | 12 +++++++++ .../primtcons/ExpSizeOf_StringOf_WithCtx.bs | 12 +++++++++ .../primtcons/ExpSizeOf_ValueOf_NoCtx.bs | 12 +++++++++ ...xpSizeOf_ValueOf_NoCtx.bs.bsc-out.expected | 12 +++++++++ .../primtcons/ExpSizeOf_ValueOf_WithCtx.bs | 12 +++++++++ .../primtcons/ValueOf_KindMismatch_Arity.bs | 4 +++ .../primtcons/ValueOf_KindMismatch_Res.bs | 4 +++ .../bsc.typechecker/primtcons/primtcons.exp | 25 ++++++++++++++++++- .../typeclasses/ATFPolyDataWidth.bs | 7 +++--- .../typeclasses/ATFUnifyError.bs | 14 +++++++---- .../ATFUnifyError.bs.bsc-out.expected | 6 ++--- .../typeclasses/ATFUnifyHKError.bs | 9 +++++-- .../ATFUnifyHKError.bs.bsc-out.expected | 7 +++--- 20 files changed, 192 insertions(+), 23 deletions(-) create mode 100644 testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_BS.bs create mode 100644 testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Minimal.bs create mode 100644 testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs create mode 100644 testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs.bsc-out.expected create mode 100644 testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_NoCtx.bs create mode 100644 testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_NoCtx.bs.bsc-out.expected create mode 100644 testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_WithCtx.bs create mode 100644 testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_NoCtx.bs create mode 100644 testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_NoCtx.bs.bsc-out.expected create mode 100644 testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_WithCtx.bs create mode 100644 testsuite/bsc.typechecker/primtcons/ValueOf_KindMismatch_Arity.bs create mode 100644 testsuite/bsc.typechecker/primtcons/ValueOf_KindMismatch_Res.bs diff --git a/src/comp/CtxRed.hs b/src/comp/CtxRed.hs index 13b0ea91e..bfde8da3d 100644 --- a/src/comp/CtxRed.hs +++ b/src/comp/CtxRed.hs @@ -385,10 +385,7 @@ ctxRedCQType' isInstHead cqt = do -- (and do it here, after "convCQType", so that "expTFun" sees -- the qualified types) (qs, t) <- if isInstHead - then do -- XXX disable expanding of type synonyms until - -- XXX failures with TLM instances are resolved - -- XXX (vqs_extra, t1) <- expTFun t0 (expandSyn t0) - (vqs_extra, t1) <- expTFun t0 + then do (vqs_extra, t1) <- expTFun (expandSyn t0) let qs_extra = map toPredWithPositions vqs_extra return (qs0 ++ qs_extra, t1) else return (qs0, t0) diff --git a/src/comp/TCheck.hs b/src/comp/TCheck.hs index e6d0cd09c..68e284a18 100644 --- a/src/comp/TCheck.hs +++ b/src/comp/TCheck.hs @@ -2394,7 +2394,14 @@ tiExpl''' as0 i sc alts me (oqt@(oqs :=> ot), vts) = do -- type functions like SizeOf could have crept into the predicates -- via unification, so we expand them out so that they can be satisfied - ps <- concatMapM (expTConPred . expandSynVPred) ps0 + ps1 <- concatMapM (expTConPred . expandSynVPred) ps0 + + -- Expand type synonyms and type functions in the declared type to generate + -- implicit class predicates (e.g. SizeOf a generates Bits a n). + s_ot <- getSubst + let ot_expanded = expandSyn (apSub s_ot ot) + (ot_ps, _) <- expTFun ot_expanded + let ps = ps1 ++ ot_ps satTraceM ("tiExpl " ++ ppReadable i ++ " ps: " ++ ppReadable ps) diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_BS.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_BS.bs new file mode 100644 index 000000000..87f0d453a --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_BS.bs @@ -0,0 +1,20 @@ +package ExpSizeOf_FieldSyn_BS where + +-- Classic syntax version of ExpSizeOf_FieldSyn. +-- A struct with a field whose type uses SizeOf through a synonym chain. + +type T t = UInt (S t) +type S t = SizeOf t + +struct Node dataType = + dat :: dataType + unused :: T dataType + deriving (Bits, Eq) + +{-# synthesize sysExpSizeOf_FieldSyn_BS #-} +sysExpSizeOf_FieldSyn_BS :: Module Empty +sysExpSizeOf_FieldSyn_BS = module + r_node :: Reg (Node (UInt 3)) <- mkRegU + r_data :: Reg (UInt 3) <- mkRegU + rules + when True ==> r_data := r_node.dat diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Minimal.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Minimal.bs new file mode 100644 index 000000000..5d89fdd6d --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Minimal.bs @@ -0,0 +1,10 @@ +package ExpSizeOf_FieldSyn_Minimal where + +-- Minimal reproduction: a struct with a field type that uses SizeOf +-- through a type synonym. Without expanding synonyms in ctxRedCQType, +-- we fail to inject the needed Bits context in the derived Generic instance. + +type S t = SizeOf t + +struct Foo a = + x :: Bit (S a) diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs new file mode 100644 index 000000000..b8bb7ca7d --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs @@ -0,0 +1,11 @@ +package ExpSizeOf_Let_NoCtx where + +-- A let binding with a type annotation containing SizeOf should require +-- a Bits context, but currently doesn't (the CHasType path in tiExpr +-- handles inline annotations but not let bindings). +-- This is filed as a known bug. + +foo :: a -> String +foo _ = let x :: Bit (SizeOf a) + x = _ + in printType $ typeOf $ x diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs.bsc-out.expected b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs.bsc-out.expected new file mode 100644 index 000000000..6a9a0a6ed --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs.bsc-out.expected @@ -0,0 +1,12 @@ +checking package dependencies +compiling ExpSizeOf_Let_NoCtx.bs +Error: "ExpSizeOf_Let_NoCtx.bs", line 8, column 0: (T0030) + The contexts for this expression are too general. + Given type: + a -> Prelude.String + The following contexts are needed: + Prelude.Bits a a__ + Introduced at the following locations: + "ExpSizeOf_Let_NoCtx.bs", line 9, column 22 + The type variables are from the following positions: + "a__" at "ExpSizeOf_Let_NoCtx.bs", line 9, column 22 diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_NoCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_NoCtx.bs new file mode 100644 index 000000000..3f09c2ff7 --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_NoCtx.bs @@ -0,0 +1,12 @@ +package ExpSizeOf_StringOf_NoCtx where + +data Thing = Thing (UInt 42) deriving (Bits) + +foo :: a -> String +foo _ = stringOf (TNumToStr (SizeOf a)) + +{-# synthesize main #-} +main :: Module Empty +main = module + rules + "asdf": when True ==> $display (foo $ Thing _) diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_NoCtx.bs.bsc-out.expected b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_NoCtx.bs.bsc-out.expected new file mode 100644 index 000000000..adfc6019e --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_NoCtx.bs.bsc-out.expected @@ -0,0 +1,12 @@ +checking package dependencies +compiling ExpSizeOf_StringOf_NoCtx.bs +Error: "ExpSizeOf_StringOf_NoCtx.bs", line 5, column 0: (T0030) + The contexts for this expression are too general. + Given type: + a -> Prelude.String + The following contexts are needed: + Prelude.Bits a a__ + Introduced at the following locations: + "ExpSizeOf_StringOf_NoCtx.bs", line 6, column 29 + The type variables are from the following positions: + "a__" at "ExpSizeOf_StringOf_NoCtx.bs", line 6, column 29 diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_WithCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_WithCtx.bs new file mode 100644 index 000000000..c3692d8a3 --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_WithCtx.bs @@ -0,0 +1,12 @@ +package ExpSizeOf_StringOf_WithCtx where + +data Thing = Thing (UInt 42) deriving (Bits) + +foo :: (Bits a sz) => a -> String +foo _ = stringOf (TNumToStr (SizeOf a)) + +{-# synthesize main #-} +main :: Module Empty +main = module + rules + "asdf": when True ==> $display (foo $ Thing _) diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_NoCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_NoCtx.bs new file mode 100644 index 000000000..227418f74 --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_NoCtx.bs @@ -0,0 +1,12 @@ +package ExpSizeOf_ValueOf_NoCtx where + +data Thing = Thing (UInt 42) deriving (Bits) + +foo :: a -> Integer +foo _ = valueOf (SizeOf a) + +{-# synthesize main #-} +main :: Module Empty +main = module + rules + "asdf": when True ==> $display (foo $ Thing _) diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_NoCtx.bs.bsc-out.expected b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_NoCtx.bs.bsc-out.expected new file mode 100644 index 000000000..38ff942da --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_NoCtx.bs.bsc-out.expected @@ -0,0 +1,12 @@ +checking package dependencies +compiling ExpSizeOf_ValueOf_NoCtx.bs +Error: "ExpSizeOf_ValueOf_NoCtx.bs", line 5, column 0: (T0030) + The contexts for this expression are too general. + Given type: + a -> Prelude.Integer + The following contexts are needed: + Prelude.Bits a a__ + Introduced at the following locations: + "ExpSizeOf_ValueOf_NoCtx.bs", line 6, column 17 + The type variables are from the following positions: + "a__" at "ExpSizeOf_ValueOf_NoCtx.bs", line 6, column 17 diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_WithCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_WithCtx.bs new file mode 100644 index 000000000..e1f08665d --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_WithCtx.bs @@ -0,0 +1,12 @@ +package ExpSizeOf_ValueOf_WithCtx where + +data Thing = Thing (UInt 42) deriving (Bits) + +foo :: (Bits a sz) => a -> Integer +foo _ = valueOf (SizeOf a) + +{-# synthesize main #-} +main :: Module Empty +main = module + rules + "asdf": when True ==> $display (foo $ Thing _) diff --git a/testsuite/bsc.typechecker/primtcons/ValueOf_KindMismatch_Arity.bs b/testsuite/bsc.typechecker/primtcons/ValueOf_KindMismatch_Arity.bs new file mode 100644 index 000000000..a13e418c3 --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ValueOf_KindMismatch_Arity.bs @@ -0,0 +1,4 @@ +package ValueOf_KindMismatch_Arity where + +bar :: Integer +bar = valueOf (SizeOf Int) diff --git a/testsuite/bsc.typechecker/primtcons/ValueOf_KindMismatch_Res.bs b/testsuite/bsc.typechecker/primtcons/ValueOf_KindMismatch_Res.bs new file mode 100644 index 000000000..aa14a1bd9 --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ValueOf_KindMismatch_Res.bs @@ -0,0 +1,4 @@ +package ValueOf_KindMismatch_Res where + +baz :: Integer +baz = valueOf Bool diff --git a/testsuite/bsc.typechecker/primtcons/primtcons.exp b/testsuite/bsc.typechecker/primtcons/primtcons.exp index 51712df07..78636b367 100644 --- a/testsuite/bsc.typechecker/primtcons/primtcons.exp +++ b/testsuite/bsc.typechecker/primtcons/primtcons.exp @@ -19,7 +19,7 @@ compile_pass ExpSizeOf_Instances.bsv compile_pass ExpSizeOf_InstancesBase.bsv # Test that SizeOf is expanded even when it's buried in a type synonym -compile_pass_bug ExpSizeOf_InstancesBaseSyn.bsv 1729 +compile_pass ExpSizeOf_InstancesBaseSyn.bsv # --------------- # Test that SizeOf introduced through the type of a field in a struct value @@ -32,6 +32,29 @@ compile_verilog_pass ExpSizeOf_Field.bsv # but after adding the normtypes pass (later replaced by extra normalization in expanded), # it succeeds. compile_verilog_pass ExpSizeOf_FieldSyn.bsv +compile_verilog_pass ExpSizeOf_FieldSyn_BS.bs +compile_pass ExpSizeOf_FieldSyn_Minimal.bs + +# --------------- +# Test that SizeOf is expanded inside 'valueOf' (GitHub Issue #890) + +compile_fail_error ExpSizeOf_ValueOf_NoCtx.bs T0030 +compare_file [make_bsc_output_name ExpSizeOf_ValueOf_NoCtx.bs] + +compile_pass ExpSizeOf_ValueOf_WithCtx.bs + +# Perform the same tests for 'stringOf' +compile_fail_error ExpSizeOf_StringOf_NoCtx.bs T0030 +compare_file [make_bsc_output_name ExpSizeOf_StringOf_NoCtx.bs] +compile_pass ExpSizeOf_StringOf_WithCtx.bs + +# Kind errors in valueOf type argument +compile_fail_error ValueOf_KindMismatch_Arity.bs T0025 +compile_fail_error ValueOf_KindMismatch_Res.bs T0026 + +# SizeOf in a let binding type annotation requires a Bits context +compile_fail_error ExpSizeOf_Let_NoCtx.bs T0030 +compare_file [make_bsc_output_name ExpSizeOf_Let_NoCtx.bs] # --------------- diff --git a/testsuite/bsc.typechecker/typeclasses/ATFPolyDataWidth.bs b/testsuite/bsc.typechecker/typeclasses/ATFPolyDataWidth.bs index 6e66f7c25..8fe017726 100644 --- a/testsuite/bsc.typechecker/typeclasses/ATFPolyDataWidth.bs +++ b/testsuite/bsc.typechecker/typeclasses/ATFPolyDataWidth.bs @@ -31,11 +31,12 @@ mkEncoded val = let raw = toBit val in Encoded raw (zeroExtend raw) --- Polymorphic pattern match -getRaw :: Encoded f -> Bit (Width f) +-- Polymorphic pattern match: need HasWidth context because Width f +-- in the return type generates an implicit HasWidth predicate. +getRaw :: (HasWidth f n) => Encoded f -> Bit (Width f) getRaw (Encoded r _) = r -getExtended :: Encoded f -> Bit (TAdd (Width f) 1) +getExtended :: (HasWidth f n, Add (Width f) 1 m) => Encoded f -> Bit (TAdd (Width f) 1) getExtended (Encoded _ e) = e -- Concrete: Width Byte = 8, TAdd 8 1 = 9 diff --git a/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs b/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs index eac7a1e73..05a05bf88 100644 --- a/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs +++ b/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs @@ -1,7 +1,7 @@ package ATFUnifyError where --- Test that unification of two different type function applications fails --- when they cannot be proven equal. +-- Test that unification of a type function application with a concrete type +-- fails when the needed class context is missing. class Container f e | f -> e where type Elem f = e @@ -14,6 +14,10 @@ instance Container (Box a) a where wrap = Box unwrap (Box x) = x --- Unification creates an unsatisfied context Container a Bool -conv :: a -> Elem a -> Bool -conv _ = id +-- Reading a struct field whose type is Elem f, and assigning to Bool, +-- requires Container f Bool which is not in scope. +struct Holder f = + val :: Elem f + +getBool :: Holder a -> Bool +getBool h = h.val diff --git a/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs.bsc-out.expected b/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs.bsc-out.expected index 5fbec0d16..cb7992976 100644 --- a/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs.bsc-out.expected +++ b/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs.bsc-out.expected @@ -1,10 +1,10 @@ checking package dependencies compiling ATFUnifyError.bs -Error: "ATFUnifyError.bs", line 18, column 0: (T0030) +Error: "ATFUnifyError.bs", line 22, column 0: (T0030) The contexts for this expression are too general. Given type: - a -> ATFUnifyError.Elem a -> Prelude.Bool + ATFUnifyError.Holder a -> Prelude.Bool The following contexts are needed: ATFUnifyError.Container a Prelude.Bool Introduced at the following locations: - "ATFUnifyError.bs", line 19, column 9 + "ATFUnifyError.bs", line 23, column 12 diff --git a/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs b/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs index ff3a22444..6109f9889 100644 --- a/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs +++ b/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs @@ -7,5 +7,10 @@ class (Container :: * -> (* -> *) -> *) a s | a -> s where data Foo f = Foo (f Bool) -conv :: a -> Foo (Elem a) -> Foo Maybe -conv _ = id +-- Reading a struct field whose type uses a higher-kinded ATF (Elem a), +-- and assigning to Foo Maybe, requires Container a Maybe which is missing. +struct Holder a = + val :: Foo (Elem a) + +getMaybe :: Holder a -> Foo Maybe +getMaybe h = h.val diff --git a/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs.bsc-out.expected b/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs.bsc-out.expected index 83bf6d1a4..f4e338eb3 100644 --- a/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs.bsc-out.expected +++ b/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs.bsc-out.expected @@ -1,11 +1,10 @@ checking package dependencies compiling ATFUnifyHKError.bs -Error: "ATFUnifyHKError.bs", line 10, column 0: (T0030) +Error: "ATFUnifyHKError.bs", line 15, column 0: (T0030) The contexts for this expression are too general. Given type: - a -> ATFUnifyHKError.Foo (ATFUnifyHKError.Elem a) -> ATFUnifyHKError.Foo - Prelude.Maybe + ATFUnifyHKError.Holder a -> ATFUnifyHKError.Foo Prelude.Maybe The following contexts are needed: ATFUnifyHKError.Container a Prelude.Maybe Introduced at the following locations: - "ATFUnifyHKError.bs", line 11, column 9 + "ATFUnifyHKError.bs", line 16, column 13 From c30964f85c9a10737bed9cef493b3922e766df5d Mon Sep 17 00:00:00 2001 From: Lucas Kramer Date: Mon, 13 Apr 2026 13:43:33 -0700 Subject: [PATCH 02/12] Remove unneeded context --- testsuite/bsc.typechecker/typeclasses/ATFPolyDataWidth.bs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/testsuite/bsc.typechecker/typeclasses/ATFPolyDataWidth.bs b/testsuite/bsc.typechecker/typeclasses/ATFPolyDataWidth.bs index 8fe017726..679fec40c 100644 --- a/testsuite/bsc.typechecker/typeclasses/ATFPolyDataWidth.bs +++ b/testsuite/bsc.typechecker/typeclasses/ATFPolyDataWidth.bs @@ -36,7 +36,7 @@ mkEncoded val = getRaw :: (HasWidth f n) => Encoded f -> Bit (Width f) getRaw (Encoded r _) = r -getExtended :: (HasWidth f n, Add (Width f) 1 m) => Encoded f -> Bit (TAdd (Width f) 1) +getExtended :: (HasWidth f n) => Encoded f -> Bit (TAdd (Width f) 1) getExtended (Encoded _ e) = e -- Concrete: Width Byte = 8, TAdd 8 1 = 9 From 78c6feab016fb5f7ea1a701f3d935e1a77544245 Mon Sep 17 00:00:00 2001 From: Lucas Kramer Date: Mon, 13 Apr 2026 13:43:40 -0700 Subject: [PATCH 03/12] Update expected result --- .../commands/type.tcl.bluetcl-bh-out.expected | 26 +++++++++---------- .../type_bh.tcl.bluetcl-bh-out.expected | 26 +++++++++---------- 2 files changed, 26 insertions(+), 26 deletions(-) diff --git a/testsuite/bsc.bluetcl/commands/type.tcl.bluetcl-bh-out.expected b/testsuite/bsc.bluetcl/commands/type.tcl.bluetcl-bh-out.expected index 2793563d9..bfaf32c42 100644 --- a/testsuite/bsc.bluetcl/commands/type.tcl.bluetcl-bh-out.expected +++ b/testsuite/bsc.bluetcl/commands/type.tcl.bluetcl-bh-out.expected @@ -99,7 +99,7 @@ Typeclass Prelude.Arith Prelude.Integer Prelude.Arith Prelude.Real Prelude.Arith Prelude.String - position {%/Libraries/Prelude.bs 530 21 {Library Prelude}} + position {%/Libraries/Prelude.bs 583 21 {Library Prelude}} Bits a n Typeclass @@ -129,7 +129,7 @@ Typeclass Prelude.Bits PreludeBSV.SaturationMode 2 Prelude.Bits Test.Bar 2 Prelude.Bits Test.BarSet 2 - position {%/Libraries/Prelude.bs 351 15 {Library Prelude}} + position {%/Libraries/Prelude.bs 403 15 {Library Prelude}} Typeclass (Prelude.Bits :: * -> # -> *) a n dependencies @@ -157,7 +157,7 @@ Typeclass Prelude.Bits PreludeBSV.SaturationMode 2 Prelude.Bits Test.Bar 2 Prelude.Bits Test.BarSet 2 - position {%/Libraries/Prelude.bs 351 15 {Library Prelude}} + position {%/Libraries/Prelude.bs 403 15 {Library Prelude}} Typeclass (Prelude.Bits :: * -> # -> *) a n dependencies @@ -185,7 +185,7 @@ Typeclass Prelude.Bits PreludeBSV.SaturationMode 2 Prelude.Bits Test.Bar 2 Prelude.Bits Test.BarSet 2 - position {%/Libraries/Prelude.bs 351 15 {Library Prelude}} + position {%/Libraries/Prelude.bs 403 15 {Library Prelude}} Typeclass (Prelude.Bits :: * -> # -> *) a n dependencies @@ -213,7 +213,7 @@ Typeclass Prelude.Bits PreludeBSV.SaturationMode 2 Prelude.Bits Test.Bar 2 Prelude.Bits Test.BarSet 2 - position {%/Libraries/Prelude.bs 351 15 {Library Prelude}} + position {%/Libraries/Prelude.bs 403 15 {Library Prelude}} Has_tpl_1 t a Typeclass @@ -224,14 +224,14 @@ Typeclass members {t -> a} tpl_1 instances - Prelude.Has_tpl_1 (Prelude.Tuple2 a b) a - Prelude.Has_tpl_1 (Prelude.Tuple3 a b c) a - Prelude.Has_tpl_1 (Prelude.Tuple4 a b c d) a - Prelude.Has_tpl_1 (Prelude.Tuple5 a b c d e) a - Prelude.Has_tpl_1 (Prelude.Tuple6 a b c d e f) a - Prelude.Has_tpl_1 (Prelude.Tuple7 a b c d e f g) a - Prelude.Has_tpl_1 (Prelude.Tuple8 a b c d e f g h) a - position {%/Libraries/Prelude.bs 3321 17 {Library Prelude}} + Prelude.Has_tpl_1 (a, b) a + Prelude.Has_tpl_1 (a, b, c) a + Prelude.Has_tpl_1 (a, b, c, d) a + Prelude.Has_tpl_1 (a, b, c, d, e) a + Prelude.Has_tpl_1 (a, b, c, d, e, f) a + Prelude.Has_tpl_1 (a, b, c, d, e, f, g) a + Prelude.Has_tpl_1 (a, b, c, d, e, f, g, h) a + position {%/Libraries/Prelude.bs 3463 17 {Library Prelude}} Bitify Baz (int, n): UNKNOWN diff --git a/testsuite/bsc.bluetcl/commands/type_bh.tcl.bluetcl-bh-out.expected b/testsuite/bsc.bluetcl/commands/type_bh.tcl.bluetcl-bh-out.expected index c33683ccb..556fdb303 100644 --- a/testsuite/bsc.bluetcl/commands/type_bh.tcl.bluetcl-bh-out.expected +++ b/testsuite/bsc.bluetcl/commands/type_bh.tcl.bluetcl-bh-out.expected @@ -99,7 +99,7 @@ Typeclass Prelude.Arith Prelude.Integer Prelude.Arith Prelude.Real Prelude.Arith Prelude.String - position {%/Libraries/Prelude.bs 530 21 {Library Prelude}} + position {%/Libraries/Prelude.bs 583 21 {Library Prelude}} Bits a n Typeclass @@ -129,7 +129,7 @@ Typeclass Prelude.Bits PreludeBSV.SaturationMode 2 Prelude.Bits Test.Bar 2 Prelude.Bits Test.BarSet 2 - position {%/Libraries/Prelude.bs 351 15 {Library Prelude}} + position {%/Libraries/Prelude.bs 403 15 {Library Prelude}} Typeclass (Prelude.Bits :: * -> # -> *) a n dependencies @@ -157,7 +157,7 @@ Typeclass Prelude.Bits PreludeBSV.SaturationMode 2 Prelude.Bits Test.Bar 2 Prelude.Bits Test.BarSet 2 - position {%/Libraries/Prelude.bs 351 15 {Library Prelude}} + position {%/Libraries/Prelude.bs 403 15 {Library Prelude}} Typeclass (Prelude.Bits :: * -> # -> *) a n dependencies @@ -185,7 +185,7 @@ Typeclass Prelude.Bits PreludeBSV.SaturationMode 2 Prelude.Bits Test.Bar 2 Prelude.Bits Test.BarSet 2 - position {%/Libraries/Prelude.bs 351 15 {Library Prelude}} + position {%/Libraries/Prelude.bs 403 15 {Library Prelude}} Typeclass (Prelude.Bits :: * -> # -> *) a n dependencies @@ -213,7 +213,7 @@ Typeclass Prelude.Bits PreludeBSV.SaturationMode 2 Prelude.Bits Test.Bar 2 Prelude.Bits Test.BarSet 2 - position {%/Libraries/Prelude.bs 351 15 {Library Prelude}} + position {%/Libraries/Prelude.bs 403 15 {Library Prelude}} Has_tpl_1 t a Typeclass @@ -224,14 +224,14 @@ Typeclass members {t -> a} tpl_1 instances - Prelude.Has_tpl_1 (Prelude.Tuple2 a b) a - Prelude.Has_tpl_1 (Prelude.Tuple3 a b c) a - Prelude.Has_tpl_1 (Prelude.Tuple4 a b c d) a - Prelude.Has_tpl_1 (Prelude.Tuple5 a b c d e) a - Prelude.Has_tpl_1 (Prelude.Tuple6 a b c d e f) a - Prelude.Has_tpl_1 (Prelude.Tuple7 a b c d e f g) a - Prelude.Has_tpl_1 (Prelude.Tuple8 a b c d e f g h) a - position {%/Libraries/Prelude.bs 3321 17 {Library Prelude}} + Prelude.Has_tpl_1 (a, b) a + Prelude.Has_tpl_1 (a, b, c) a + Prelude.Has_tpl_1 (a, b, c, d) a + Prelude.Has_tpl_1 (a, b, c, d, e) a + Prelude.Has_tpl_1 (a, b, c, d, e, f) a + Prelude.Has_tpl_1 (a, b, c, d, e, f, g) a + Prelude.Has_tpl_1 (a, b, c, d, e, f, g, h) a + position {%/Libraries/Prelude.bs 3463 17 {Library Prelude}} Bitify Baz (Int 32) n: UNKNOWN From 5578a946e2c0d78468982b0ea5ba3d3c7f7fc963 Mon Sep 17 00:00:00 2001 From: Lucas Kramer Date: Mon, 13 Apr 2026 16:14:21 -0700 Subject: [PATCH 04/12] Re-enable expanding type synonyms in tiField1 --- src/comp/TCheck.hs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/comp/TCheck.hs b/src/comp/TCheck.hs index 68e284a18..79fbd2e1d 100644 --- a/src/comp/TCheck.hs +++ b/src/comp/TCheck.hs @@ -2092,10 +2092,7 @@ tiField1 as rt (f, e) = do (qs :=> ft0, xts) <- freshInstT "G" f sc rt -- Fields might be defined using type constructors (like SizeOf), -- so replace them with vars and return the preds that determine the vars - -- XXX disable expanding of type synonyms until failures with TLM - -- XXX (type synonyms which drop parameters) is resolved - -- XXX (tcon_ps, ft) <- expTFun (expandSyn ft0) - (tcon_ps, ft) <- expTFun ft0 + (tcon_ps, ft) <- expTFun (expandSyn ft0) -- Unify the field type and the context expected return type, -- possibly returning preds which express type equality (t,eq_ps) <- unifyFnTo f e ft rt From 204cf6fbb0d54d3a39a601cda2435c8a5fb11a6f Mon Sep 17 00:00:00 2001 From: Lucas Kramer Date: Sun, 19 Apr 2026 16:59:55 -0700 Subject: [PATCH 05/12] Revert "Re-enable expanding type synonyms in tiField1" This reverts commit de377a9f89f39f108f68a3b9d67cdd12fc03296b. --- src/comp/TCheck.hs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/comp/TCheck.hs b/src/comp/TCheck.hs index 79fbd2e1d..68e284a18 100644 --- a/src/comp/TCheck.hs +++ b/src/comp/TCheck.hs @@ -2092,7 +2092,10 @@ tiField1 as rt (f, e) = do (qs :=> ft0, xts) <- freshInstT "G" f sc rt -- Fields might be defined using type constructors (like SizeOf), -- so replace them with vars and return the preds that determine the vars - (tcon_ps, ft) <- expTFun (expandSyn ft0) + -- XXX disable expanding of type synonyms until failures with TLM + -- XXX (type synonyms which drop parameters) is resolved + -- XXX (tcon_ps, ft) <- expTFun (expandSyn ft0) + (tcon_ps, ft) <- expTFun ft0 -- Unify the field type and the context expected return type, -- possibly returning preds which express type equality (t,eq_ps) <- unifyFnTo f e ft rt From bfb0ee62495e646364c95c82592c894e6e05562a Mon Sep 17 00:00:00 2001 From: Lucas Kramer Date: Mon, 20 Apr 2026 13:51:41 -0700 Subject: [PATCH 06/12] Add Julie's minimal example as a test case --- .../primtcons/CExtendSynonym.bsv | 46 +++++++++++++++++++ .../bsc.typechecker/primtcons/primtcons.exp | 3 ++ 2 files changed, 49 insertions(+) create mode 100644 testsuite/bsc.typechecker/primtcons/CExtendSynonym.bsv diff --git a/testsuite/bsc.typechecker/primtcons/CExtendSynonym.bsv b/testsuite/bsc.typechecker/primtcons/CExtendSynonym.bsv new file mode 100644 index 000000000..6cc29db46 --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/CExtendSynonym.bsv @@ -0,0 +1,46 @@ +// Reduced version of bsc-contrib AMBA_TLM library. +// Check that we can use type synonyms in instance heads. + +function Bit#(m) zExtend(Bit#(n) value) + provisos(Add#(n,m,k)); + Bit#(k) out = zeroExtend(value); + if (valueOf(m) == 0) + return ?; + else + return out[valueOf(m) - 1:0]; +endfunction + +function a cExtend(b value) + provisos(Bits#(a, sa), Bits#(b, sb)); + + let out = unpack(zExtend(pack(value))); + + return out; +endfunction + +`define TLM_PRM_DCL numeric type id_size, \ + numeric type addr_size + +`define TLM_PRM id_size, \ + addr_size + +typedef Bit#(id_size) TLMId#(`TLM_PRM_DCL); +typedef Bit#(id_size) AxiId#(`TLM_PRM_DCL); + +typedef struct { + AxiId#(`TLM_PRM) id; + } AxiAddrCmd#(`TLM_PRM_DCL); + +function TLMId#(`TLM_PRM) fromAxiId(AxiId#(`TLM_PRM) id); + return cExtend(id); +endfunction + +typeclass BusPayload#(type a, type b) dependencies(a determines b); + function b getId(a payload); +endtypeclass + +instance BusPayload#(AxiAddrCmd#(`TLM_PRM), TLMId#(`TLM_PRM)); + function getId(payload); + return fromAxiId(payload.id); + endfunction +endinstance diff --git a/testsuite/bsc.typechecker/primtcons/primtcons.exp b/testsuite/bsc.typechecker/primtcons/primtcons.exp index 78636b367..c895c89c5 100644 --- a/testsuite/bsc.typechecker/primtcons/primtcons.exp +++ b/testsuite/bsc.typechecker/primtcons/primtcons.exp @@ -56,5 +56,8 @@ compile_fail_error ValueOf_KindMismatch_Res.bs T0026 compile_fail_error ExpSizeOf_Let_NoCtx.bs T0030 compare_file [make_bsc_output_name ExpSizeOf_Let_NoCtx.bs] +# Test that cExtend works when type synonyms are expanded in instance heads +compile_pass CExtendSynonym.bsv + # --------------- From 6d332e4f6e823129da3123617d7e80396db7f264 Mon Sep 17 00:00:00 2001 From: Lucas Kramer Date: Mon, 20 Apr 2026 13:55:02 -0700 Subject: [PATCH 07/12] For now, only expand synonyms in ctxRedCQType' when expTFun actually did something --- src/comp/CtxRed.hs | 9 ++++++++- .../commands/type.tcl.bluetcl-bh-out.expected | 14 +++++++------- .../commands/type_bh.tcl.bluetcl-bh-out.expected | 14 +++++++------- 3 files changed, 22 insertions(+), 15 deletions(-) diff --git a/src/comp/CtxRed.hs b/src/comp/CtxRed.hs index bfde8da3d..5b35fd549 100644 --- a/src/comp/CtxRed.hs +++ b/src/comp/CtxRed.hs @@ -387,7 +387,14 @@ ctxRedCQType' isInstHead cqt = do (qs, t) <- if isInstHead then do (vqs_extra, t1) <- expTFun (expandSyn t0) let qs_extra = map toPredWithPositions vqs_extra - return (qs0 ++ qs_extra, t1) + -- Use the expanded type t1 only if expTFun actually + -- found something to expand (i.e. generated predicates). + -- Otherwise keep the original t0. + -- XXX we should probably be unconditionally expanding synonymns + -- here and in tiField1, but there is existing code that relies on + -- the current behavior, so changing this requires more thought. + let t' = if null vqs_extra then t0 else t1 + return (qs0 ++ qs_extra, t') else return (qs0, t0) -- construct the predicates and try to reduce them diff --git a/testsuite/bsc.bluetcl/commands/type.tcl.bluetcl-bh-out.expected b/testsuite/bsc.bluetcl/commands/type.tcl.bluetcl-bh-out.expected index bfaf32c42..4ebcfc0b1 100644 --- a/testsuite/bsc.bluetcl/commands/type.tcl.bluetcl-bh-out.expected +++ b/testsuite/bsc.bluetcl/commands/type.tcl.bluetcl-bh-out.expected @@ -224,13 +224,13 @@ Typeclass members {t -> a} tpl_1 instances - Prelude.Has_tpl_1 (a, b) a - Prelude.Has_tpl_1 (a, b, c) a - Prelude.Has_tpl_1 (a, b, c, d) a - Prelude.Has_tpl_1 (a, b, c, d, e) a - Prelude.Has_tpl_1 (a, b, c, d, e, f) a - Prelude.Has_tpl_1 (a, b, c, d, e, f, g) a - Prelude.Has_tpl_1 (a, b, c, d, e, f, g, h) a + Prelude.Has_tpl_1 (Prelude.Tuple2 a b) a + Prelude.Has_tpl_1 (Prelude.Tuple3 a b c) a + Prelude.Has_tpl_1 (Prelude.Tuple4 a b c d) a + Prelude.Has_tpl_1 (Prelude.Tuple5 a b c d e) a + Prelude.Has_tpl_1 (Prelude.Tuple6 a b c d e f) a + Prelude.Has_tpl_1 (Prelude.Tuple7 a b c d e f g) a + Prelude.Has_tpl_1 (Prelude.Tuple8 a b c d e f g h) a position {%/Libraries/Prelude.bs 3463 17 {Library Prelude}} Bitify Baz (int, n): diff --git a/testsuite/bsc.bluetcl/commands/type_bh.tcl.bluetcl-bh-out.expected b/testsuite/bsc.bluetcl/commands/type_bh.tcl.bluetcl-bh-out.expected index 556fdb303..855a73d0a 100644 --- a/testsuite/bsc.bluetcl/commands/type_bh.tcl.bluetcl-bh-out.expected +++ b/testsuite/bsc.bluetcl/commands/type_bh.tcl.bluetcl-bh-out.expected @@ -224,13 +224,13 @@ Typeclass members {t -> a} tpl_1 instances - Prelude.Has_tpl_1 (a, b) a - Prelude.Has_tpl_1 (a, b, c) a - Prelude.Has_tpl_1 (a, b, c, d) a - Prelude.Has_tpl_1 (a, b, c, d, e) a - Prelude.Has_tpl_1 (a, b, c, d, e, f) a - Prelude.Has_tpl_1 (a, b, c, d, e, f, g) a - Prelude.Has_tpl_1 (a, b, c, d, e, f, g, h) a + Prelude.Has_tpl_1 (Prelude.Tuple2 a b) a + Prelude.Has_tpl_1 (Prelude.Tuple3 a b c) a + Prelude.Has_tpl_1 (Prelude.Tuple4 a b c d) a + Prelude.Has_tpl_1 (Prelude.Tuple5 a b c d e) a + Prelude.Has_tpl_1 (Prelude.Tuple6 a b c d e f) a + Prelude.Has_tpl_1 (Prelude.Tuple7 a b c d e f g) a + Prelude.Has_tpl_1 (Prelude.Tuple8 a b c d e f g h) a position {%/Libraries/Prelude.bs 3463 17 {Library Prelude}} Bitify Baz (Int 32) n: From 890be1fcd5c7e865392a04ef45d58b9e72cec61f Mon Sep 17 00:00:00 2001 From: Lucas Kramer Date: Mon, 20 Apr 2026 14:02:37 -0700 Subject: [PATCH 08/12] Revert irrelevant changes to bsc.bluetcl test expected outputs that are being filtered anyway --- .../commands/type.tcl.bluetcl-bh-out.expected | 12 ++++++------ .../commands/type_bh.tcl.bluetcl-bh-out.expected | 12 ++++++------ 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/testsuite/bsc.bluetcl/commands/type.tcl.bluetcl-bh-out.expected b/testsuite/bsc.bluetcl/commands/type.tcl.bluetcl-bh-out.expected index 4ebcfc0b1..2793563d9 100644 --- a/testsuite/bsc.bluetcl/commands/type.tcl.bluetcl-bh-out.expected +++ b/testsuite/bsc.bluetcl/commands/type.tcl.bluetcl-bh-out.expected @@ -99,7 +99,7 @@ Typeclass Prelude.Arith Prelude.Integer Prelude.Arith Prelude.Real Prelude.Arith Prelude.String - position {%/Libraries/Prelude.bs 583 21 {Library Prelude}} + position {%/Libraries/Prelude.bs 530 21 {Library Prelude}} Bits a n Typeclass @@ -129,7 +129,7 @@ Typeclass Prelude.Bits PreludeBSV.SaturationMode 2 Prelude.Bits Test.Bar 2 Prelude.Bits Test.BarSet 2 - position {%/Libraries/Prelude.bs 403 15 {Library Prelude}} + position {%/Libraries/Prelude.bs 351 15 {Library Prelude}} Typeclass (Prelude.Bits :: * -> # -> *) a n dependencies @@ -157,7 +157,7 @@ Typeclass Prelude.Bits PreludeBSV.SaturationMode 2 Prelude.Bits Test.Bar 2 Prelude.Bits Test.BarSet 2 - position {%/Libraries/Prelude.bs 403 15 {Library Prelude}} + position {%/Libraries/Prelude.bs 351 15 {Library Prelude}} Typeclass (Prelude.Bits :: * -> # -> *) a n dependencies @@ -185,7 +185,7 @@ Typeclass Prelude.Bits PreludeBSV.SaturationMode 2 Prelude.Bits Test.Bar 2 Prelude.Bits Test.BarSet 2 - position {%/Libraries/Prelude.bs 403 15 {Library Prelude}} + position {%/Libraries/Prelude.bs 351 15 {Library Prelude}} Typeclass (Prelude.Bits :: * -> # -> *) a n dependencies @@ -213,7 +213,7 @@ Typeclass Prelude.Bits PreludeBSV.SaturationMode 2 Prelude.Bits Test.Bar 2 Prelude.Bits Test.BarSet 2 - position {%/Libraries/Prelude.bs 403 15 {Library Prelude}} + position {%/Libraries/Prelude.bs 351 15 {Library Prelude}} Has_tpl_1 t a Typeclass @@ -231,7 +231,7 @@ Typeclass Prelude.Has_tpl_1 (Prelude.Tuple6 a b c d e f) a Prelude.Has_tpl_1 (Prelude.Tuple7 a b c d e f g) a Prelude.Has_tpl_1 (Prelude.Tuple8 a b c d e f g h) a - position {%/Libraries/Prelude.bs 3463 17 {Library Prelude}} + position {%/Libraries/Prelude.bs 3321 17 {Library Prelude}} Bitify Baz (int, n): UNKNOWN diff --git a/testsuite/bsc.bluetcl/commands/type_bh.tcl.bluetcl-bh-out.expected b/testsuite/bsc.bluetcl/commands/type_bh.tcl.bluetcl-bh-out.expected index 855a73d0a..c33683ccb 100644 --- a/testsuite/bsc.bluetcl/commands/type_bh.tcl.bluetcl-bh-out.expected +++ b/testsuite/bsc.bluetcl/commands/type_bh.tcl.bluetcl-bh-out.expected @@ -99,7 +99,7 @@ Typeclass Prelude.Arith Prelude.Integer Prelude.Arith Prelude.Real Prelude.Arith Prelude.String - position {%/Libraries/Prelude.bs 583 21 {Library Prelude}} + position {%/Libraries/Prelude.bs 530 21 {Library Prelude}} Bits a n Typeclass @@ -129,7 +129,7 @@ Typeclass Prelude.Bits PreludeBSV.SaturationMode 2 Prelude.Bits Test.Bar 2 Prelude.Bits Test.BarSet 2 - position {%/Libraries/Prelude.bs 403 15 {Library Prelude}} + position {%/Libraries/Prelude.bs 351 15 {Library Prelude}} Typeclass (Prelude.Bits :: * -> # -> *) a n dependencies @@ -157,7 +157,7 @@ Typeclass Prelude.Bits PreludeBSV.SaturationMode 2 Prelude.Bits Test.Bar 2 Prelude.Bits Test.BarSet 2 - position {%/Libraries/Prelude.bs 403 15 {Library Prelude}} + position {%/Libraries/Prelude.bs 351 15 {Library Prelude}} Typeclass (Prelude.Bits :: * -> # -> *) a n dependencies @@ -185,7 +185,7 @@ Typeclass Prelude.Bits PreludeBSV.SaturationMode 2 Prelude.Bits Test.Bar 2 Prelude.Bits Test.BarSet 2 - position {%/Libraries/Prelude.bs 403 15 {Library Prelude}} + position {%/Libraries/Prelude.bs 351 15 {Library Prelude}} Typeclass (Prelude.Bits :: * -> # -> *) a n dependencies @@ -213,7 +213,7 @@ Typeclass Prelude.Bits PreludeBSV.SaturationMode 2 Prelude.Bits Test.Bar 2 Prelude.Bits Test.BarSet 2 - position {%/Libraries/Prelude.bs 403 15 {Library Prelude}} + position {%/Libraries/Prelude.bs 351 15 {Library Prelude}} Has_tpl_1 t a Typeclass @@ -231,7 +231,7 @@ Typeclass Prelude.Has_tpl_1 (Prelude.Tuple6 a b c d e f) a Prelude.Has_tpl_1 (Prelude.Tuple7 a b c d e f g) a Prelude.Has_tpl_1 (Prelude.Tuple8 a b c d e f g h) a - position {%/Libraries/Prelude.bs 3463 17 {Library Prelude}} + position {%/Libraries/Prelude.bs 3321 17 {Library Prelude}} Bitify Baz (Int 32) n: UNKNOWN From faaf1bc476340d93521f818c3426f2b94ac508b7 Mon Sep 17 00:00:00 2001 From: Lucas Kramer Date: Tue, 30 Jun 2026 20:49:51 -0700 Subject: [PATCH 09/12] Address PR #916 review: expand type-function expansion tests Testsuite-only changes responding to review feedback: - Keep the original id-based ATFUnify{,HK}Error tests and add struct-field-access variants (ATFFieldUnify{,HK}Error); refresh the expected output for the id-based tests. - Add struct-field tests for the SizeOf-through-synonym context requirement: field use (ExpSizeOf_FieldSyn_Use_{NoCtx,WithCtx}) and a field whose type variable is not a struct parameter (ExpSizeOf_FieldSyn_Unbound_{NoCtx,WithCtx}). - Add a type-annotated-expression test (ExpSizeOf_TypedExpr_{NoCtx,WithCtx}) and regroup the explicit-type tests (valueOf/stringOf/typed-expr/let) under a corrected header. - Add CExtendATF{,Explicit}: an ATF variant of CExtendSynonym that still fails without explicit method types, demonstrating GitHub Issue #311. - Add ExpSizeOf_VectorIfc for GitHub Issue #313 (typechecks, but fails to synthesize; not fixed by PR #916). - Record bug numbers (Bluespec Inc Bug 1729, GitHub #310/#311/#313, bsc-contrib PR 46) and update stale comments. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../bsc.typechecker/primtcons/CExtendATF.bsv | 64 +++++++++++++++++ .../primtcons/CExtendATFExplicit.bsv | 55 +++++++++++++++ .../primtcons/CExtendSynonym.bsv | 13 +++- .../primtcons/ExpSizeOf_FieldSyn_Minimal.bs | 6 +- .../ExpSizeOf_FieldSyn_Unbound_NoCtx.bs | 15 ++++ .../ExpSizeOf_FieldSyn_Unbound_WithCtx.bs | 11 +++ .../primtcons/ExpSizeOf_FieldSyn_Use_NoCtx.bs | 19 +++++ ...eOf_FieldSyn_Use_NoCtx.bs.bsc-out.expected | 12 ++++ .../ExpSizeOf_FieldSyn_Use_WithCtx.bs | 15 ++++ .../primtcons/ExpSizeOf_Let_NoCtx.bs | 9 +-- .../ExpSizeOf_Let_NoCtx.bs.bsc-out.expected | 6 +- .../primtcons/ExpSizeOf_TypedExpr_NoCtx.bs | 9 +++ ...SizeOf_TypedExpr_NoCtx.bs.bsc-out.expected | 12 ++++ .../primtcons/ExpSizeOf_TypedExpr_WithCtx.bs | 7 ++ .../primtcons/ExpSizeOf_VectorIfc.bsv | 27 ++++++++ .../bsc.typechecker/primtcons/primtcons.exp | 69 ++++++++++++++++--- .../typeclasses/ATFFieldUnifyError.bs | 25 +++++++ .../ATFFieldUnifyError.bs.bsc-out.expected | 10 +++ .../typeclasses/ATFFieldUnifyHKError.bs | 18 +++++ .../ATFFieldUnifyHKError.bs.bsc-out.expected | 10 +++ .../typeclasses/ATFUnifyError.bs | 17 +++-- .../ATFUnifyError.bs.bsc-out.expected | 7 +- .../typeclasses/ATFUnifyHKError.bs | 16 ++--- .../ATFUnifyHKError.bs.bsc-out.expected | 6 +- .../typeclasses/typeclasses.exp | 6 ++ 25 files changed, 422 insertions(+), 42 deletions(-) create mode 100644 testsuite/bsc.typechecker/primtcons/CExtendATF.bsv create mode 100644 testsuite/bsc.typechecker/primtcons/CExtendATFExplicit.bsv create mode 100644 testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Unbound_NoCtx.bs create mode 100644 testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Unbound_WithCtx.bs create mode 100644 testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_NoCtx.bs create mode 100644 testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_NoCtx.bs.bsc-out.expected create mode 100644 testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_WithCtx.bs create mode 100644 testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_NoCtx.bs create mode 100644 testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_NoCtx.bs.bsc-out.expected create mode 100644 testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_WithCtx.bs create mode 100644 testsuite/bsc.typechecker/primtcons/ExpSizeOf_VectorIfc.bsv create mode 100644 testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyError.bs create mode 100644 testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyError.bs.bsc-out.expected create mode 100644 testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyHKError.bs create mode 100644 testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyHKError.bs.bsc-out.expected diff --git a/testsuite/bsc.typechecker/primtcons/CExtendATF.bsv b/testsuite/bsc.typechecker/primtcons/CExtendATF.bsv new file mode 100644 index 000000000..e1c8fa619 --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/CExtendATF.bsv @@ -0,0 +1,64 @@ +// A variant of CExtendSynonym that puts a type function (here a user-defined +// ATF, 'IdW') into the id-type synonyms, so that expanding the synonyms in the +// instance head *does* reveal a type function. That forces the conditional +// synonym expansion in 'CtxRed.ctxRedCQType'' to fire (unlike CExtendSynonym, +// where the plain synonyms are left unexpanded), which re-introduces the +// dangling 'addr_size' parameter and makes typecheck fail with T0035. +// +// This is the case that is *still broken* -- see the XXX in ctxRedCQType' and +// GitHub Issue #311 (and bsc-contrib PR 46, which worked around the analogous +// AMBA_TLM failure by adding explicit method types). CExtendATFExplicit.bsv +// shows that adding explicit types makes it compile, which suggests the +// problem is one of inference ordering rather than anything fundamental. +// The same failure occurs with the builtin type function SizeOf in place of +// the ATF 'IdW'. + +function Bit#(m) zExtend(Bit#(n) value) + provisos(Add#(n,m,k)); + Bit#(k) out = zeroExtend(value); + if (valueOf(m) == 0) + return ?; + else + return out[valueOf(m) - 1:0]; +endfunction + +function a cExtend(b value) + provisos(Bits#(a, sa), Bits#(b, sb)); + let out = unpack(zExtend(pack(value))); + return out; +endfunction + +// A user-defined ATF: IdW#(Bit#(n)) = n (i.e. it plays the role of SizeOf). +typeclass HasIdW#(type t, numeric type n) dependencies (t determines n); + type IdW#(type t) = n; +endtypeclass + +instance HasIdW#(Bit#(n), n); +endinstance + +`define TLM_PRM_DCL numeric type id_size, \ + numeric type addr_size + +`define TLM_PRM id_size, \ + addr_size + +typedef Bit#(IdW#(Bit#(id_size))) TLMId#(`TLM_PRM_DCL); +typedef Bit#(IdW#(Bit#(id_size))) AxiId#(`TLM_PRM_DCL); + +typedef struct { + AxiId#(`TLM_PRM) id; + } AxiAddrCmd#(`TLM_PRM_DCL); + +function TLMId#(`TLM_PRM) fromAxiId(AxiId#(`TLM_PRM) id); + return cExtend(id); +endfunction + +typeclass BusPayload#(type a, type b) dependencies(a determines b); + function b getId(a payload); +endtypeclass + +instance BusPayload#(AxiAddrCmd#(`TLM_PRM), TLMId#(`TLM_PRM)); + function getId(payload); + return fromAxiId(payload.id); + endfunction +endinstance diff --git a/testsuite/bsc.typechecker/primtcons/CExtendATFExplicit.bsv b/testsuite/bsc.typechecker/primtcons/CExtendATFExplicit.bsv new file mode 100644 index 000000000..3229e2c69 --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/CExtendATFExplicit.bsv @@ -0,0 +1,55 @@ +// As CExtendATF.bsv, but with an explicit type on the 'getId' method. With +// the explicit type, typecheck succeeds despite the ATF-triggered synonym +// expansion in the instance head. This is the workaround used in bsc-contrib +// PR 46, and it shows that the CExtendATF failure is not fundamental (see the +// XXX in CtxRed.ctxRedCQType' and GitHub Issue #311). + +function Bit#(m) zExtend(Bit#(n) value) + provisos(Add#(n,m,k)); + Bit#(k) out = zeroExtend(value); + if (valueOf(m) == 0) + return ?; + else + return out[valueOf(m) - 1:0]; +endfunction + +function a cExtend(b value) + provisos(Bits#(a, sa), Bits#(b, sb)); + let out = unpack(zExtend(pack(value))); + return out; +endfunction + +// A user-defined ATF: IdW#(Bit#(n)) = n (i.e. it plays the role of SizeOf). +typeclass HasIdW#(type t, numeric type n) dependencies (t determines n); + type IdW#(type t) = n; +endtypeclass + +instance HasIdW#(Bit#(n), n); +endinstance + +`define TLM_PRM_DCL numeric type id_size, \ + numeric type addr_size + +`define TLM_PRM id_size, \ + addr_size + +typedef Bit#(IdW#(Bit#(id_size))) TLMId#(`TLM_PRM_DCL); +typedef Bit#(IdW#(Bit#(id_size))) AxiId#(`TLM_PRM_DCL); + +typedef struct { + AxiId#(`TLM_PRM) id; + } AxiAddrCmd#(`TLM_PRM_DCL); + +function TLMId#(`TLM_PRM) fromAxiId(AxiId#(`TLM_PRM) id); + return cExtend(id); +endfunction + +typeclass BusPayload#(type a, type b) dependencies(a determines b); + function b getId(a payload); +endtypeclass + +instance BusPayload#(AxiAddrCmd#(`TLM_PRM), TLMId#(`TLM_PRM)); + function TLMId#(`TLM_PRM) getId(AxiAddrCmd#(`TLM_PRM) payload); + return fromAxiId(payload.id); + endfunction +endinstance diff --git a/testsuite/bsc.typechecker/primtcons/CExtendSynonym.bsv b/testsuite/bsc.typechecker/primtcons/CExtendSynonym.bsv index 6cc29db46..4e47ea575 100644 --- a/testsuite/bsc.typechecker/primtcons/CExtendSynonym.bsv +++ b/testsuite/bsc.typechecker/primtcons/CExtendSynonym.bsv @@ -1,5 +1,14 @@ -// Reduced version of bsc-contrib AMBA_TLM library. -// Check that we can use type synonyms in instance heads. +// Reduced version of the bsc-contrib AMBA_TLM library (see bsc-contrib PR 46). +// Check that we can use type synonyms in instance heads. The synonyms 'TLMId' +// and 'AxiId' drop the 'addr_size' parameter; expanding them fully in the +// instance head would leave 'addr_size' dangling and break unification. This +// exercises the (now conditional) synonym expansion in CtxRed.ctxRedCQType' -- +// see the XXX there and GitHub Issue #311. Because these synonyms contain no +// type function, the conditional expansion leaves them alone, so this compiles; +// bsc-contrib PR 46 added explicit method types to work around the earlier +// (unconditional-expansion) failure, and those are no longer needed here. +// CExtendATF.bsv shows a variant that *does* still fail, because it puts a type +// function in the synonyms and so triggers the expansion. function Bit#(m) zExtend(Bit#(n) value) provisos(Add#(n,m,k)); diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Minimal.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Minimal.bs index 5d89fdd6d..ae7c63d00 100644 --- a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Minimal.bs +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Minimal.bs @@ -1,8 +1,10 @@ package ExpSizeOf_FieldSyn_Minimal where -- Minimal reproduction: a struct with a field type that uses SizeOf --- through a type synonym. Without expanding synonyms in ctxRedCQType, --- we fail to inject the needed Bits context in the derived Generic instance. +-- through a type synonym. Without expanding synonyms in ctxRedCQType, the +-- needed Bits context is not injected into the derived Generic instance, and +-- that instance then fails to typecheck -- i.e. the failure is a compile +-- error, so compile_pass is a sufficient regression guard here. type S t = SizeOf t diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Unbound_NoCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Unbound_NoCtx.bs new file mode 100644 index 000000000..9307d1c1f --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Unbound_NoCtx.bs @@ -0,0 +1,15 @@ +package ExpSizeOf_FieldSyn_Unbound_NoCtx where + +-- A struct field whose type uses SizeOf through a synonym, where the type +-- variable is *not* a parameter of the struct. Because the variable is +-- unbound in the struct type, the field's implicit Bits context cannot be +-- satisfied by the struct itself, so the field must declare it explicitly. +-- Here it does not, so typecheck reports the missing context (T0030). +-- (GitHub Issues #890 and #310: the field's context requirement is not +-- wrongly exempted here, despite the XXX in TCheck.tiField1.) + +type T t = UInt (S t) +type S t = SizeOf t + +struct MyS = + sfield :: T dataType diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Unbound_WithCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Unbound_WithCtx.bs new file mode 100644 index 000000000..223ca6012 --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Unbound_WithCtx.bs @@ -0,0 +1,11 @@ +package ExpSizeOf_FieldSyn_Unbound_WithCtx where + +-- As ExpSizeOf_FieldSyn_Unbound_NoCtx, but the field declares the Bits +-- context that its SizeOf-using type requires, so typecheck succeeds. +-- (GitHub Issues #890 and #310) + +type T t = UInt (S t) +type S t = SizeOf t + +struct MyS = + sfield :: (Bits dataType sz) => T dataType diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_NoCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_NoCtx.bs new file mode 100644 index 000000000..2b39de54f --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_NoCtx.bs @@ -0,0 +1,19 @@ +package ExpSizeOf_FieldSyn_Use_NoCtx where + +-- Reading a struct field whose type uses SizeOf through a synonym chain +-- requires a Bits context on the struct's type parameter. The field type +-- 'T a' expands to 'UInt (SizeOf a)', and reading the field during typecheck +-- introduces the implicit 'Bits a' context. Here it is not provided, so +-- typecheck reports the missing context (T0030), confirming that the field's +-- context requirement is handled during typecheck. (GitHub Issue #890) + +type T t = UInt (S t) +type S t = SizeOf t + +struct Node dataType = + dat :: dataType + wide :: T dataType + deriving (Bits, Eq) + +fnNeedsCtx :: Node a -> Bool +fnNeedsCtx n = n.wide == 0 diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_NoCtx.bs.bsc-out.expected b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_NoCtx.bs.bsc-out.expected new file mode 100644 index 000000000..a854839a6 --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_NoCtx.bs.bsc-out.expected @@ -0,0 +1,12 @@ +checking package dependencies +compiling ExpSizeOf_FieldSyn_Use_NoCtx.bs +Error: "ExpSizeOf_FieldSyn_Use_NoCtx.bs", line 18, column 0: (T0030) + The contexts for this expression are too general. + Given type: + ExpSizeOf_FieldSyn_Use_NoCtx.Node a -> Prelude.Bool + The following contexts are needed: + Prelude.Bits a a__ + Introduced at the following locations: + "ExpSizeOf_FieldSyn_Use_NoCtx.bs", line 15, column 10 + The type variables are from the following positions: + "a__" at "ExpSizeOf_FieldSyn_Use_NoCtx.bs", line 15, column 10 diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_WithCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_WithCtx.bs new file mode 100644 index 000000000..490091a50 --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_WithCtx.bs @@ -0,0 +1,15 @@ +package ExpSizeOf_FieldSyn_Use_WithCtx where + +-- As ExpSizeOf_FieldSyn_Use_NoCtx, but with the explicit Bits context that +-- reading the field requires, so typecheck succeeds. (GitHub Issue #890) + +type T t = UInt (S t) +type S t = SizeOf t + +struct Node dataType = + dat :: dataType + wide :: T dataType + deriving (Bits, Eq) + +fnNeedsCtx :: (Bits a sa) => Node a -> Bool +fnNeedsCtx n = n.wide == 0 diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs index b8bb7ca7d..f746af2c4 100644 --- a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs @@ -1,9 +1,10 @@ package ExpSizeOf_Let_NoCtx where --- A let binding with a type annotation containing SizeOf should require --- a Bits context, but currently doesn't (the CHasType path in tiExpr --- handles inline annotations but not let bindings). --- This is filed as a known bug. +-- A let binding whose type annotation contains SizeOf requires a Bits +-- context: expanding the SizeOf in the declared type introduces an implicit +-- Bits context, which must be provided by an explicit context on the +-- enclosing definition. Here none is given, so typecheck reports the +-- missing context (T0030). (GitHub Issue #890) foo :: a -> String foo _ = let x :: Bit (SizeOf a) diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs.bsc-out.expected b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs.bsc-out.expected index 6a9a0a6ed..bacb7541a 100644 --- a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs.bsc-out.expected +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs.bsc-out.expected @@ -1,12 +1,12 @@ checking package dependencies compiling ExpSizeOf_Let_NoCtx.bs -Error: "ExpSizeOf_Let_NoCtx.bs", line 8, column 0: (T0030) +Error: "ExpSizeOf_Let_NoCtx.bs", line 9, column 0: (T0030) The contexts for this expression are too general. Given type: a -> Prelude.String The following contexts are needed: Prelude.Bits a a__ Introduced at the following locations: - "ExpSizeOf_Let_NoCtx.bs", line 9, column 22 + "ExpSizeOf_Let_NoCtx.bs", line 10, column 22 The type variables are from the following positions: - "a__" at "ExpSizeOf_Let_NoCtx.bs", line 9, column 22 + "a__" at "ExpSizeOf_Let_NoCtx.bs", line 10, column 22 diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_NoCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_NoCtx.bs new file mode 100644 index 000000000..9536b37b0 --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_NoCtx.bs @@ -0,0 +1,9 @@ +package ExpSizeOf_TypedExpr_NoCtx where + +-- A type-annotated expression whose type mentions SizeOf introduces an +-- implicit Bits context, the same way 'valueOf'/'stringOf' do (they are +-- implemented using type-annotated expressions). Here the context is not +-- provided, so typecheck reports it (T0030). (GitHub Issue #890) + +foo :: a -> String +foo _ = printType $ typeOf (_ :: Bit (SizeOf a)) diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_NoCtx.bs.bsc-out.expected b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_NoCtx.bs.bsc-out.expected new file mode 100644 index 000000000..1aa140360 --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_NoCtx.bs.bsc-out.expected @@ -0,0 +1,12 @@ +checking package dependencies +compiling ExpSizeOf_TypedExpr_NoCtx.bs +Error: "ExpSizeOf_TypedExpr_NoCtx.bs", line 8, column 0: (T0030) + The contexts for this expression are too general. + Given type: + a -> Prelude.String + The following contexts are needed: + Prelude.Bits a a__ + Introduced at the following locations: + "ExpSizeOf_TypedExpr_NoCtx.bs", line 9, column 38 + The type variables are from the following positions: + "a__" at "ExpSizeOf_TypedExpr_NoCtx.bs", line 9, column 38 diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_WithCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_WithCtx.bs new file mode 100644 index 000000000..ce6dd6b4c --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_WithCtx.bs @@ -0,0 +1,7 @@ +package ExpSizeOf_TypedExpr_WithCtx where + +-- With an explicit Bits context, the SizeOf in a type-annotated expression +-- can be reduced during typecheck. (GitHub Issue #890) + +foo :: (Bits a sz) => a -> String +foo _ = printType $ typeOf (_ :: Bit (SizeOf a)) diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_VectorIfc.bsv b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_VectorIfc.bsv new file mode 100644 index 000000000..03649e02c --- /dev/null +++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_VectorIfc.bsv @@ -0,0 +1,27 @@ +// GitHub Issue #313 (Bluespec Inc Bug 1917): a SizeOf in the length parameter +// of a Vector of subinterfaces confuses GenWrap's method-vs-subinterface +// determination, which happens before typecheck and so cannot reduce +// SizeOf#(Bit#(2)) to 2. BSC therefore treats 'example' as a method and +// requires its element type to be bitifiable. +// +// This is not fixed by the type-function expansion added in PR #916: the +// example still typechecks fine (see the companion compile_pass), but fails when +// synthesized (compile_verilog_fail_error, T0043). The test documents the +// current behavior; if #313 is fixed, this should become a compile_verilog_pass. + +import Vector::*; + +// Using 'SizeOf#(Bit#(2))' triggers the bug; 'typedef 2 Length' would not. +typedef SizeOf#(Bit#(2)) Length; + +typedef Bit#(1) Data; + +interface Example; + interface Vector#(Length, WriteOnly#(Data)) example; +endinterface + +(* synthesize *) +module mkExample (Example); + Vector#(Length, Reg#(Data)) ex <- replicateM(mkRegU); + interface example = ?; +endmodule diff --git a/testsuite/bsc.typechecker/primtcons/primtcons.exp b/testsuite/bsc.typechecker/primtcons/primtcons.exp index c895c89c5..f9295be37 100644 --- a/testsuite/bsc.typechecker/primtcons/primtcons.exp +++ b/testsuite/bsc.typechecker/primtcons/primtcons.exp @@ -18,7 +18,8 @@ compile_pass ExpSizeOf_Instances.bsv compile_pass ExpSizeOf_InstancesBase.bsv -# Test that SizeOf is expanded even when it's buried in a type synonym +# Test that SizeOf is expanded even when it's buried in a type synonym. +# This was Bluespec Inc Bug 1729 (also GitHub Issue #311). compile_pass ExpSizeOf_InstancesBaseSyn.bsv # --------------- @@ -33,31 +34,81 @@ compile_verilog_pass ExpSizeOf_Field.bsv # it succeeds. compile_verilog_pass ExpSizeOf_FieldSyn.bsv compile_verilog_pass ExpSizeOf_FieldSyn_BS.bs + +# Minimal reproduction: without expanding the synonym in ctxRedCQType, the +# derived Generic instance fails to typecheck (the needed Bits context is not +# injected), so it fails to compile. A plain compile_pass is therefore a +# sufficient regression guard -- no intermediate dump is needed. compile_pass ExpSizeOf_FieldSyn_Minimal.bs -# --------------- -# Test that SizeOf is expanded inside 'valueOf' (GitHub Issue #890) +# Using a struct field whose type uses SizeOf through a synonym requires a Bits +# context on the struct's type parameter. The requirement is introduced during +# typecheck of the field access, so it must be provided (GitHub Issue #890). +compile_fail_error ExpSizeOf_FieldSyn_Use_NoCtx.bs T0030 +compare_file [make_bsc_output_name ExpSizeOf_FieldSyn_Use_NoCtx.bs] +compile_pass ExpSizeOf_FieldSyn_Use_WithCtx.bs + +# A struct field whose SizeOf-using type has a type variable that is not a +# parameter of the struct is not exempted from the Bits requirement: the field +# must declare the context explicitly (GitHub Issues #890 and #310). BSC +# currently reports two T0030 errors here (one of which lacks a source +# position), so this uses an expected count of 2 rather than compare_file. +compile_fail_error ExpSizeOf_FieldSyn_Unbound_NoCtx.bs T0030 2 +compile_pass ExpSizeOf_FieldSyn_Unbound_WithCtx.bs +# --------------- +# Test that type functions like SizeOf are expanded in explicitly-typed +# expressions, introducing the implicit contexts they require and reporting an +# error when those contexts are not provided (GitHub Issue #890). This covers +# 'valueOf', 'stringOf', type-annotated expressions, and explicitly-typed let +# bindings (valueOf and stringOf are themselves implemented using type-annotated +# expressions). + +# valueOf compile_fail_error ExpSizeOf_ValueOf_NoCtx.bs T0030 compare_file [make_bsc_output_name ExpSizeOf_ValueOf_NoCtx.bs] - compile_pass ExpSizeOf_ValueOf_WithCtx.bs -# Perform the same tests for 'stringOf' +# stringOf compile_fail_error ExpSizeOf_StringOf_NoCtx.bs T0030 compare_file [make_bsc_output_name ExpSizeOf_StringOf_NoCtx.bs] compile_pass ExpSizeOf_StringOf_WithCtx.bs +# type-annotated expression, e.g. '(_ :: Bit (SizeOf a))' +compile_fail_error ExpSizeOf_TypedExpr_NoCtx.bs T0030 +compare_file [make_bsc_output_name ExpSizeOf_TypedExpr_NoCtx.bs] +compile_pass ExpSizeOf_TypedExpr_WithCtx.bs + +# explicitly-typed let binding +compile_fail_error ExpSizeOf_Let_NoCtx.bs T0030 +compare_file [make_bsc_output_name ExpSizeOf_Let_NoCtx.bs] + # Kind errors in valueOf type argument compile_fail_error ValueOf_KindMismatch_Arity.bs T0025 compile_fail_error ValueOf_KindMismatch_Res.bs T0026 -# SizeOf in a let binding type annotation requires a Bits context -compile_fail_error ExpSizeOf_Let_NoCtx.bs T0030 -compare_file [make_bsc_output_name ExpSizeOf_Let_NoCtx.bs] +# --------------- +# Type synonyms and type functions in instance heads +# (GitHub Issue #311, bsc-contrib PR 46) -# Test that cExtend works when type synonyms are expanded in instance heads +# Plain type synonyms in an instance head are left unexpanded, so this compiles +# without the explicit method types that bsc-contrib PR 46 previously needed. compile_pass CExtendSynonym.bsv +# A type function (here a user-defined ATF) in the instance-head synonyms forces +# the conditional expansion in ctxRedCQType', which re-introduces the dangling +# parameter and still fails -- unless explicit method types are given. This is +# the case that remains broken (GitHub Issue #311). +compile_fail_error CExtendATF.bsv T0035 +compile_pass CExtendATFExplicit.bsv + +# --------------- +# SizeOf in the length of a Vector of subinterfaces (GitHub Issue #313, +# Bluespec Inc Bug 1917). This is not fixed by PR #916: the example typechecks, +# but fails when synthesized, because GenWrap decides whether the field is a +# method or a subinterface before typecheck and cannot reduce the SizeOf. +compile_pass ExpSizeOf_VectorIfc.bsv +compile_verilog_fail_error ExpSizeOf_VectorIfc.bsv T0043 + # --------------- diff --git a/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyError.bs b/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyError.bs new file mode 100644 index 000000000..440b5d381 --- /dev/null +++ b/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyError.bs @@ -0,0 +1,25 @@ +package ATFFieldUnifyError where + +-- Like ATFUnifyError, but the unification of a type function application with +-- a concrete type is forced by reading a struct field. Reading a field whose +-- type is 'Elem f' and assigning it to Bool requires 'Container f Bool', which +-- is not in scope, so typecheck reports the missing context (T0030). + +class Container f e | f -> e where + type Elem f = e + wrap :: e -> f + unwrap :: f -> e + +data Box a = Box a + +instance Container (Box a) a where + wrap = Box + unwrap (Box x) = x + +-- Reading a struct field whose type is Elem f, and assigning to Bool, +-- requires Container f Bool which is not in scope. +struct Holder f = + val :: Elem f + +getBool :: Holder a -> Bool +getBool h = h.val diff --git a/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyError.bs.bsc-out.expected b/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyError.bs.bsc-out.expected new file mode 100644 index 000000000..705fc1423 --- /dev/null +++ b/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyError.bs.bsc-out.expected @@ -0,0 +1,10 @@ +checking package dependencies +compiling ATFFieldUnifyError.bs +Error: "ATFFieldUnifyError.bs", line 24, column 0: (T0030) + The contexts for this expression are too general. + Given type: + ATFFieldUnifyError.Holder a -> Prelude.Bool + The following contexts are needed: + ATFFieldUnifyError.Container a Prelude.Bool + Introduced at the following locations: + "ATFFieldUnifyError.bs", line 25, column 12 diff --git a/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyHKError.bs b/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyHKError.bs new file mode 100644 index 000000000..ed9bf01fa --- /dev/null +++ b/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyHKError.bs @@ -0,0 +1,18 @@ +package ATFFieldUnifyHKError where + +-- Like ATFUnifyHKError, but the unification of a higher-kinded type function +-- application with a concrete type constructor is forced by reading a struct +-- field. Reading a field whose type uses the higher-kinded ATF (Elem a), and +-- assigning it to Foo Maybe, requires Container a Maybe which is not in scope, +-- so typecheck reports the missing context (T0030). + +class (Container :: * -> (* -> *) -> *) a s | a -> s where + type Elem a = s + +data Foo f = Foo (f Bool) + +struct Holder a = + val :: Foo (Elem a) + +getMaybe :: Holder a -> Foo Maybe +getMaybe h = h.val diff --git a/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyHKError.bs.bsc-out.expected b/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyHKError.bs.bsc-out.expected new file mode 100644 index 000000000..bed5d2fb7 --- /dev/null +++ b/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyHKError.bs.bsc-out.expected @@ -0,0 +1,10 @@ +checking package dependencies +compiling ATFFieldUnifyHKError.bs +Error: "ATFFieldUnifyHKError.bs", line 17, column 0: (T0030) + The contexts for this expression are too general. + Given type: + ATFFieldUnifyHKError.Holder a -> ATFFieldUnifyHKError.Foo Prelude.Maybe + The following contexts are needed: + ATFFieldUnifyHKError.Container a Prelude.Maybe + Introduced at the following locations: + "ATFFieldUnifyHKError.bs", line 18, column 13 diff --git a/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs b/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs index 05a05bf88..d8a6f808c 100644 --- a/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs +++ b/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs @@ -1,7 +1,10 @@ package ATFUnifyError where --- Test that unification of a type function application with a concrete type --- fails when the needed class context is missing. +-- Test that unifying a type function application (Elem a) with a concrete +-- type (Bool) requires the corresponding class context (Container a Bool). +-- Here it is missing, so typecheck reports it (T0030). The unification is +-- forced by giving 'id' the explicit type 'a -> Elem a -> Bool'. +-- (See ATFFieldUnifyError for the same check via struct field access.) class Container f e | f -> e where type Elem f = e @@ -14,10 +17,6 @@ instance Container (Box a) a where wrap = Box unwrap (Box x) = x --- Reading a struct field whose type is Elem f, and assigning to Bool, --- requires Container f Bool which is not in scope. -struct Holder f = - val :: Elem f - -getBool :: Holder a -> Bool -getBool h = h.val +-- Unification creates an unsatisfied context Container a Bool +conv :: a -> Elem a -> Bool +conv _ = id diff --git a/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs.bsc-out.expected b/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs.bsc-out.expected index cb7992976..f23e0e286 100644 --- a/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs.bsc-out.expected +++ b/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs.bsc-out.expected @@ -1,10 +1,11 @@ checking package dependencies compiling ATFUnifyError.bs -Error: "ATFUnifyError.bs", line 22, column 0: (T0030) +Error: "ATFUnifyError.bs", line 21, column 0: (T0030) The contexts for this expression are too general. Given type: - ATFUnifyError.Holder a -> Prelude.Bool + a -> ATFUnifyError.Elem a -> Prelude.Bool The following contexts are needed: ATFUnifyError.Container a Prelude.Bool Introduced at the following locations: - "ATFUnifyError.bs", line 23, column 12 + "ATFUnifyError.bs", line 21, column 13 + "ATFUnifyError.bs", line 22, column 9 diff --git a/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs b/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs index 6109f9889..0bfcdb188 100644 --- a/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs +++ b/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs @@ -1,16 +1,16 @@ package ATFUnifyHKError where --- Test that higher-kinded type function constraints fail properly. +-- Test that unifying a higher-kinded type function application (Elem a, +-- of kind * -> *) with a concrete type constructor (Maybe) requires the +-- corresponding class context (Container a Maybe). Here it is missing, so +-- typecheck reports it (T0030). The unification is forced by giving 'id' +-- the explicit type 'a -> Foo (Elem a) -> Foo Maybe'. +-- (See ATFFieldUnifyHKError for the same check via struct field access.) class (Container :: * -> (* -> *) -> *) a s | a -> s where type Elem a = s data Foo f = Foo (f Bool) --- Reading a struct field whose type uses a higher-kinded ATF (Elem a), --- and assigning to Foo Maybe, requires Container a Maybe which is missing. -struct Holder a = - val :: Foo (Elem a) - -getMaybe :: Holder a -> Foo Maybe -getMaybe h = h.val +conv :: a -> Foo (Elem a) -> Foo Maybe +conv _ = id diff --git a/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs.bsc-out.expected b/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs.bsc-out.expected index f4e338eb3..ac04359d7 100644 --- a/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs.bsc-out.expected +++ b/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs.bsc-out.expected @@ -3,8 +3,10 @@ compiling ATFUnifyHKError.bs Error: "ATFUnifyHKError.bs", line 15, column 0: (T0030) The contexts for this expression are too general. Given type: - ATFUnifyHKError.Holder a -> ATFUnifyHKError.Foo Prelude.Maybe + a -> ATFUnifyHKError.Foo (ATFUnifyHKError.Elem a) -> ATFUnifyHKError.Foo + Prelude.Maybe The following contexts are needed: ATFUnifyHKError.Container a Prelude.Maybe Introduced at the following locations: - "ATFUnifyHKError.bs", line 16, column 13 + "ATFUnifyHKError.bs", line 15, column 18 + "ATFUnifyHKError.bs", line 16, column 9 diff --git a/testsuite/bsc.typechecker/typeclasses/typeclasses.exp b/testsuite/bsc.typechecker/typeclasses/typeclasses.exp index 709629a59..c3572f55f 100644 --- a/testsuite/bsc.typechecker/typeclasses/typeclasses.exp +++ b/testsuite/bsc.typechecker/typeclasses/typeclasses.exp @@ -134,6 +134,12 @@ compile_fail_error ATFUnifyError.bs T0030 compare_file ATFUnifyError.bs.bsc-out compile_fail_error ATFUnifyHKError.bs T0030 compare_file ATFUnifyHKError.bs.bsc-out +# Same checks as ATFUnify{,HK}Error, but forcing the unification via struct +# field access instead of via 'id' +compile_fail_error ATFFieldUnifyError.bs T0030 +compare_file ATFFieldUnifyError.bs.bsc-out +compile_fail_error ATFFieldUnifyHKError.bs T0030 +compare_file ATFFieldUnifyHKError.bs.bsc-out compile_fail_error ATFAmbig.bs T0079 compare_file ATFAmbig.bs.bsc-out compile_fail_error ATFNameClashTwoClasses.bs T0011 From 95cce711598d99b9c97769a783f9002bdbf8973c Mon Sep 17 00:00:00 2001 From: Ravi Nanavati Date: Wed, 8 Jul 2026 00:39:22 +0000 Subject: [PATCH 10/12] Fix spurious T0029 when a field reaches an ATF through a type synonym When a data/struct field type refers to an associated type function through a type synonym (e.g. `type ElemSyn f = Elem f`), the auto-derived Generic instance failed to typecheck with a spurious "signature too general" (T0029) error, while the same field written with the ATF applied directly (`Elem f`) compiled fine. The instance head (the "given" scheme) is processed by ctxRedCQType', which expands synonyms and generalizes the exposed ATF application into a fresh class-constrained variable: instance (Container f e) => Generic (WrapSyn f) (... Conc e ...) But when the derived method bodies are typechecked, the constructor and field types are instantiated with the synonym unexpanded, and unifying the head's variable `e` against `ElemSyn c` did not recognize the synonym-hidden ATF: mgu structurally bound `e := ElemSyn c`, pinning the fundep-determined variable. The deduced scheme then quantified one fewer variable than the given scheme, and the syntactic scheme comparison in tiExpl''' reported T0029. The direct case works because mgu recognizes ATF applications (isATFAp) and routes them to atfUnify, which refuses to bind bound type variables and instead defers a type equality that eqToPred turns into the class predicate `Container c e` -- satisfiable from the instance context, leaving `e` generic. Fix: in mgu, expand a saturated type-synonym application when (and only when) its expansion is a fully applied ATF application, so that a synonym-hidden ATF unifies exactly like the direct one. Synonyms whose expansion is not ATF-headed -- notably the parameter-dropping TLM-style synonyms that caused earlier synonym-expansion attempts to be reverted (see the XXX comments in CtxRed/TCheck and the CExtendSynonym test) -- keep the existing structural behavior. This also makes the missing-context error for a synonym-hidden ATF (e.g. assigning a field of type `ElemSyn f` to Bool) identical to the direct-ATF case (T0030 naming the needed Container context), and genuinely-too-general signatures still fail with T0029. Adds ATFSynonymField.bs (the reproducer: data and struct fields whose types reach the ATF through a synonym must compile) and ATFSynonymFieldUse.bs (exercises the same shapes through Bits derivation, Generic from/to, and Verilog elaboration). Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01M8cZoDh1jk24UJbB51y5tU --- src/comp/Unify.hs | 25 +++++++++- .../typeclasses/ATFSynonymField.bs | 29 +++++++++++ .../typeclasses/ATFSynonymFieldUse.bs | 48 +++++++++++++++++++ .../typeclasses/typeclasses.exp | 4 ++ 4 files changed, 105 insertions(+), 1 deletion(-) create mode 100644 testsuite/bsc.typechecker/typeclasses/ATFSynonymField.bs create mode 100644 testsuite/bsc.typechecker/typeclasses/ATFSynonymFieldUse.bs diff --git a/src/comp/Unify.hs b/src/comp/Unify.hs index a121c88ac..61254a247 100644 --- a/src/comp/Unify.hs +++ b/src/comp/Unify.hs @@ -3,6 +3,7 @@ module Unify(Unify(..), matchList) where import Type import Subst import CType +import Pred(expandSyn) import ErrorUtil(internalError) import Util(fastNub) @@ -24,8 +25,15 @@ class Unify t where instance Unify Type where -- an unreducable ATF application: identical types unify cleanly (reflexivity); -- different types generate a deferred equality constraint. + -- A type synonym is expanded when (and only when) that exposes an ATF + -- application, so that a synonym-hidden ATF unifies exactly like the + -- direct ATF application, instead of a variable being structurally + -- bound to the unexpanded synonym (which pins a fundep-determined + -- variable and makes derived-instance schemes spuriously mismatch). mgu bound_tyvars t1 t2 - | isATFAp t1 || isATFAp t2 = atfUnify bound_tyvars t1 t2 + | isATFAp t1' || isATFAp t2' = atfUnify bound_tyvars t1' t2' + where t1' = expandSynATF t1 + t2' = expandSynATF t2 mgu bound_tyvars t1 t2 | kind t1 == KNum = case kind t2 of @@ -42,6 +50,21 @@ instance Unify Type where mgu bound_tyvars (TCon tc1) (TCon tc2) | tc1==tc2 = Just (nullSubst, []) mgu bound_tyvars _ _ = Nothing +-- Expand a saturated type-synonym application when (and only when) the +-- expansion is a fully applied type-function (ATF) application, so that +-- unification treats it exactly like the direct ATF application. +-- Synonyms whose expansion does not reveal an ATF at the head are left +-- unexpanded, because existing code relies on structural unification of +-- unexpanded synonyms (e.g. synonyms that drop some of their parameters). +expandSynATF :: Type -> Type +expandSynATF t + | isSynAp t, not (isUnSatSyn t), isATFAp t' = t' + | otherwise = t + where t' = expandSyn t + isSynAp tt = case fst (splitTAp tt) of + TCon (TyCon _ _ (TItype _ _)) -> True + _ -> False + atfUnify :: [TyVar] -> Type -> Type -> Maybe (Subst, [(Type, Type)]) atfUnify bound_tyvars t1 t2 | t1 == t2 = Just (nullSubst, []) diff --git a/testsuite/bsc.typechecker/typeclasses/ATFSynonymField.bs b/testsuite/bsc.typechecker/typeclasses/ATFSynonymField.bs new file mode 100644 index 000000000..e79cae657 --- /dev/null +++ b/testsuite/bsc.typechecker/typeclasses/ATFSynonymField.bs @@ -0,0 +1,29 @@ +package ATFSynonymField where + +-- Test that a data/struct field whose type reaches an associated type +-- function through a type synonym compiles. The auto-derived Generic +-- instance must not report a spurious "signature too general" (T0029) +-- error: the given scheme (from the instance head, where synonyms are +-- expanded and the type function is generalized to a fresh variable +-- constrained by the class predicate) and the deduced scheme (where the +-- field type keeps the unexpanded synonym) are equal up to the +-- fundep-forced substitution. + +class Container f e | f -> e where + type Elem f = e + extract :: f -> e + +type ElemSyn f = Elem f + +data WrapSyn f = + WrapSyn (ElemSyn f) + | NoElem + +struct SBox f = + field :: ElemSyn f + +-- A field applying the type function directly (not via a synonym) +-- already compiled; check that it stays working. +data WrapDirect f = + WrapDirect (Elem f) + | NoElemDirect diff --git a/testsuite/bsc.typechecker/typeclasses/ATFSynonymFieldUse.bs b/testsuite/bsc.typechecker/typeclasses/ATFSynonymFieldUse.bs new file mode 100644 index 000000000..4a5ea49d4 --- /dev/null +++ b/testsuite/bsc.typechecker/typeclasses/ATFSynonymFieldUse.bs @@ -0,0 +1,48 @@ +package ATFSynonymFieldUse where + +-- Companion to ATFSynonymField: exercise data/struct fields whose types +-- reach an ATF through a type synonym, all the way through elaboration. +-- The derived Generic instances are used explicitly (via from/to) and +-- the types are stored in registers, so the synonym-hidden ATF must +-- survive typecheck, Bits derivation, and synthesis. + +class Container f e | f -> e where + type Elem f = e + extract :: f -> e + +type ElemSyn f = Elem f + +data Box a = Box a + +instance Container (Box a) a where + extract (Box x) = x + +data WrapSyn f = + WrapSyn (ElemSyn f) + | NoElem + deriving (Bits) + +struct SBox f = + field :: ElemSyn f + deriving (Bits) + +-- Round trip through the derived Generic representation. +roundTrip :: (Generic a r) => a -> a +roundTrip x = to (from x) + +sboxVal :: SBox (Box (UInt 8)) +sboxVal = SBox { field = 42 } + +wrapVal :: WrapSyn (Box (UInt 8)) +wrapVal = WrapSyn 42 + +{-# synthesize sysATFSynonymFieldUse #-} +sysATFSynonymFieldUse :: Module Empty +sysATFSynonymFieldUse = module + r1 :: Reg (SBox (Box (UInt 8))) <- mkReg (roundTrip sboxVal) + r2 :: Reg (WrapSyn (Box (UInt 8))) <- mkReg (roundTrip wrapVal) + + rules + when True ==> do + r1 := SBox { field = extract (Box (r1.field + 1)) } + r2 := roundTrip (WrapSyn r1.field) diff --git a/testsuite/bsc.typechecker/typeclasses/typeclasses.exp b/testsuite/bsc.typechecker/typeclasses/typeclasses.exp index c3572f55f..8c6845de6 100644 --- a/testsuite/bsc.typechecker/typeclasses/typeclasses.exp +++ b/testsuite/bsc.typechecker/typeclasses/typeclasses.exp @@ -89,7 +89,11 @@ compile_pass ATFInInstHeadDetermined.bs compile_pass ATFInjective.bs compile_pass ATFFieldAccess.bs compile_pass ATFPartialApp.bs +# A field type that reaches an ATF through a type synonym must not make +# the auto-derived Generic instance fail with a spurious T0029 +compile_pass ATFSynonymField.bs +compile_verilog_pass ATFSynonymFieldUse.bs compile_verilog_pass ATFSizeOf.bs compile_verilog_pass ATFPoly.bs compile_verilog_pass ATFSynthIfc.bs From 4560905ba782e4e875569c899e41131c22ee3551 Mon Sep 17 00:00:00 2001 From: Ravi Nanavati Date: Wed, 8 Jul 2026 02:02:23 +0000 Subject: [PATCH 11/12] Detect unmatchable ATFs hidden behind type synonyms in instance heads checkNoTypeFunInHead scanned instance-head arguments syntactically, so a type function reaching a non-determined head position through a type synonym escaped the T0156 check that rejects the directly-written form. Depending on the shape, the synonym form then either failed with a confusing ambiguity error (T0079) or was silently accepted with instance-head expansion rewriting the head into something other than what was written -- while the identical head written without the synonym was rejected. Since the check runs on raw definitions (before context reduction), the type constructors may not yet carry their symbol-table sorts, so the check now resolves them (updTypes) and expands each saturated synonym application, rejecting any type function application in the expansion that mentions a type variable or is not fully applied: such an application can neither be reduced away nor used for instance matching. The error is reported at the position of the synonym use, naming the type function. Ground applications hidden behind synonyms remain allowed: context reduction expands and reduces them to a concrete type, which is the Bug 1729 / GitHub #311 behavior that ExpSizeOf_InstancesBaseSyn pins (e.g. `typedef SizeOf#(T) ST' used as an instance argument). Note this remains more permissive than the directly-written ground form, which T0156 still rejects (as pinned by ATFInInstHead); relaxing that for reducible applications could be considered separately. Determined positions remain exempt, synonym or not, since they are never used for instance matching. Adds ATFInInstHeadSynonym.bs and ATFInInstHeadSynonymElsewhere.bs (variable applications, rejected with T0156 like the direct forms), ATFInInstHeadSynonymGround.bs (ground application, still accepted), and ATFInInstHeadDeterminedSynonym.bs (determined position, still accepted). Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01M8cZoDh1jk24UJbB51y5tU --- src/comp/MakeSymTab.hs | 29 ++++++++++++++++++- .../ATFInInstHeadDeterminedSynonym.bs | 22 ++++++++++++++ .../typeclasses/ATFInInstHeadSynonym.bs | 19 ++++++++++++ .../ATFInInstHeadSynonym.bs.bsc-out.expected | 4 +++ .../ATFInInstHeadSynonymElsewhere.bs | 21 ++++++++++++++ ...stHeadSynonymElsewhere.bs.bsc-out.expected | 5 ++++ .../typeclasses/ATFInInstHeadSynonymGround.bs | 24 +++++++++++++++ .../typeclasses/typeclasses.exp | 7 +++++ 8 files changed, 130 insertions(+), 1 deletion(-) create mode 100644 testsuite/bsc.typechecker/typeclasses/ATFInInstHeadDeterminedSynonym.bs create mode 100644 testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonym.bs create mode 100644 testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonym.bs.bsc-out.expected create mode 100644 testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymElsewhere.bs create mode 100644 testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymElsewhere.bs.bsc-out.expected create mode 100644 testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymGround.bs diff --git a/src/comp/MakeSymTab.hs b/src/comp/MakeSymTab.hs index 4739d27be..fb4de691e 100644 --- a/src/comp/MakeSymTab.hs +++ b/src/comp/MakeSymTab.hs @@ -464,10 +464,37 @@ checkNoTypeFunInHead errh r mi clsId args = | otherwise = [] findTypeFun (TAp f a) = findTypeFun f ++ findTypeFun a findTypeFun _ = [] + -- A type function can also be hidden behind a type synonym. + -- Expand each saturated synonym application and reject any type + -- function application in it that mentions a type variable (or + -- is not fully applied): such an application can neither be + -- reduced away nor used for instance matching. Ground + -- applications are left alone; context reduction expands and + -- reduces them to a concrete type (Bug 1729, GitHub issue #311; + -- see ExpSizeOf_InstancesBaseSyn in the testsuite). The error + -- is reported at the position of the synonym use. + synArity i | Just (TypeInfo { ti_sort = TItype n _ }) <- findType r i = Just n + | otherwise = Nothing + findSynTypeFun t = + case splitTAp t of + (TCon (TyCon i _ _), as) + | Just n <- synArity i, toInteger (length as) >= n -> + [ (getPosition i, tf) + | tf <- varTypeFuns (expandSyn (updTypes r t)) ] + (_, as) -> concatMap findSynTypeFun as + varTypeFuns t = + case splitTAp t of + (TCon (TyCon i _ (TIatf { atf_param_idxs = pIdxs })), as) + | length as /= length pIdxs || not (null (tv as)) -> + i : concatMap varTypeFuns as + (_, as) -> concatMap varTypeFuns as -- Only check non-determined positions nonDetArgs = [ arg | (idx, arg) <- zip [0..] args , not (S.member idx determinedIdxs) ] - found = concatMap findTypeFun nonDetArgs + checkArg a = case findTypeFun a of + [] -> findSynTypeFun a + ds -> ds + found = concatMap checkArg nonDetArgs in if null found then () else bsErrorUnsafe errh [ (pos, EATFInInstanceHead (pfpString tfId)) diff --git a/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadDeterminedSynonym.bs b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadDeterminedSynonym.bs new file mode 100644 index 000000000..2bba5307d --- /dev/null +++ b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadDeterminedSynonym.bs @@ -0,0 +1,22 @@ +package ATFInInstHeadDeterminedSynonym where + +-- Like ATFInInstHeadDetermined, but the type function reaches the +-- determined position through a type synonym. Determined positions +-- are never used for instance matching, so this must stay allowed, +-- synonym or not. + +class Container f e | f -> e where + type Elem f = e + wrap :: e -> f + +type ElemSyn f = Elem f + +data Box a = Box a +instance Container (Box a) a where + wrap = Box + +class Bar a b | a -> b where + bar :: a -> b + +instance Bar (Box a) (ElemSyn (Box a)) where + bar (Box x) = x diff --git a/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonym.bs b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonym.bs new file mode 100644 index 000000000..552956414 --- /dev/null +++ b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonym.bs @@ -0,0 +1,19 @@ +package ATFInInstHeadSynonym where + +-- Like ATFInInstHead, but the type function reaches the instance head +-- through a type synonym, applied to a type variable. The check must +-- see through the synonym and reject this the same way it rejects the +-- directly-written form: the application can neither be reduced away +-- nor used for instance matching. + +class Container f e | f -> e where + type Elem f = e + wrap :: e -> f + +type ElemSyn f = Elem f + +class Foo a where + foo :: a -> Bool + +instance Foo (ElemSyn f) where + foo _ = True diff --git a/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonym.bs.bsc-out.expected b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonym.bs.bsc-out.expected new file mode 100644 index 000000000..e0bc4b615 --- /dev/null +++ b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonym.bs.bsc-out.expected @@ -0,0 +1,4 @@ +checking package dependencies +compiling ATFInInstHeadSynonym.bs +Error: "ATFInInstHeadSynonym.bs", line 18, column 14: (T0156) + Type function `ATFInInstHeadSynonym.Elem' cannot be used in an instance head diff --git a/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymElsewhere.bs b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymElsewhere.bs new file mode 100644 index 000000000..11edf6574 --- /dev/null +++ b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymElsewhere.bs @@ -0,0 +1,21 @@ +package ATFInInstHeadSynonymElsewhere where + +-- Like ATFInInstHeadSynonym, but the type function's argument also +-- appears elsewhere in the instance head. Before the check saw +-- through synonyms, this form was silently accepted (the head was +-- rewritten by instance-head expansion), while the directly-written +-- form was rejected with T0156. Both must be rejected identically. + +class Container f e | f -> e where + type Elem f = e + wrap :: e -> f + +type ElemSyn f = Elem f + +data Pair a b = Pair a b + +class Foo a where + foo :: a -> Bool + +instance Foo (Pair f (ElemSyn f)) where + foo _ = True diff --git a/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymElsewhere.bs.bsc-out.expected b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymElsewhere.bs.bsc-out.expected new file mode 100644 index 000000000..cebea81ba --- /dev/null +++ b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymElsewhere.bs.bsc-out.expected @@ -0,0 +1,5 @@ +checking package dependencies +compiling ATFInInstHeadSynonymElsewhere.bs +Error: "ATFInInstHeadSynonymElsewhere.bs", line 20, column 22: (T0156) + Type function `ATFInInstHeadSynonymElsewhere.Elem' cannot be used in an + instance head diff --git a/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymGround.bs b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymGround.bs new file mode 100644 index 000000000..d18641547 --- /dev/null +++ b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymGround.bs @@ -0,0 +1,24 @@ +package ATFInInstHeadSynonymGround where + +-- A type function hidden behind a type synonym in an instance head is +-- allowed when its application is ground: context reduction expands +-- and reduces it to a concrete type (here Elem (Box Integer) reduces +-- to Integer). Same behavior as ExpSizeOf_InstancesBaseSyn (Bug 1729, +-- GitHub issue #311), with a user-defined ATF. + +class Container f e | f -> e where + type Elem f = e + wrap :: e -> f + +type ElemSyn f = Elem f + +data Box a = Box a + +instance Container (Box a) a where + wrap = Box + +class Foo a where + foo :: a -> Bool + +instance Foo (ElemSyn (Box Integer)) where + foo _ = True diff --git a/testsuite/bsc.typechecker/typeclasses/typeclasses.exp b/testsuite/bsc.typechecker/typeclasses/typeclasses.exp index 8c6845de6..264a05dc3 100644 --- a/testsuite/bsc.typechecker/typeclasses/typeclasses.exp +++ b/testsuite/bsc.typechecker/typeclasses/typeclasses.exp @@ -86,6 +86,8 @@ compile_pass ATFImported.bs compile_pass ATFUnify.bs compile_pass ATFUnifyHK.bs compile_pass ATFInInstHeadDetermined.bs +compile_pass ATFInInstHeadDeterminedSynonym.bs +compile_pass ATFInInstHeadSynonymGround.bs compile_pass ATFInjective.bs compile_pass ATFFieldAccess.bs compile_pass ATFPartialApp.bs @@ -132,6 +134,11 @@ compile_fail_error ATFInInstHead.bs T0156 compare_file ATFInInstHead.bs.bsc-out compile_fail_error ATFInInstHeadBiDirectional.bs T0156 compare_file ATFInInstHeadBiDirectional.bs.bsc-out +# Same checks with the type function hidden behind a type synonym +compile_fail_error ATFInInstHeadSynonym.bs T0156 +compare_file ATFInInstHeadSynonym.bs.bsc-out +compile_fail_error ATFInInstHeadSynonymElsewhere.bs T0156 +compare_file ATFInInstHeadSynonymElsewhere.bs.bsc-out compile_fail_error ATFResultNotDetermined.bs T0155 compare_file ATFResultNotDetermined.bs.bsc-out compile_fail_error ATFUnifyError.bs T0030 From eb08b72375121865de1e7e092abea7ccccd31f0a Mon Sep 17 00:00:00 2001 From: Ravi Nanavati Date: Thu, 9 Jul 2026 03:17:59 +0000 Subject: [PATCH 12/12] Address PR #1028 review Unify.hs: merge the ATF check into a single asATFAp function that returns the type as a fully applied type-function application (either directly, or behind a saturated type synonym), and document why synonyms are not expanded unconditionally: unification is a hot path and expandSyn is a deep expansion; expandSyn fails on unsaturated synonym applications; and a synonym whose expansion is not an ATF application must keep the existing structural unification of the unexpanded synonym (e.g. parameter-dropping synonyms, GitHub issue 311). MakeSymTab.hs: checkNoTypeFunInHead now reports both the directly written type functions and the synonym-hidden ones (deduplicated), instead of omitting the synonym-hidden errors whenever a directly written one is present. Adds ATFInInstHeadSynonymBoth.bs: a direct and a synonym-hidden type function in the same instance head, both reported with T0156. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01M8cZoDh1jk24UJbB51y5tU --- src/comp/MakeSymTab.hs | 8 +++-- src/comp/Unify.hs | 34 ++++++++++++------- .../typeclasses/ATFInInstHeadSynonymBoth.bs | 19 +++++++++++ ...FInInstHeadSynonymBoth.bs.bsc-out.expected | 7 ++++ .../typeclasses/typeclasses.exp | 3 ++ 5 files changed, 55 insertions(+), 16 deletions(-) create mode 100644 testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymBoth.bs create mode 100644 testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymBoth.bs.bsc-out.expected diff --git a/src/comp/MakeSymTab.hs b/src/comp/MakeSymTab.hs index fb4de691e..7e047560c 100644 --- a/src/comp/MakeSymTab.hs +++ b/src/comp/MakeSymTab.hs @@ -491,9 +491,11 @@ checkNoTypeFunInHead errh r mi clsId args = -- Only check non-determined positions nonDetArgs = [ arg | (idx, arg) <- zip [0..] args , not (S.member idx determinedIdxs) ] - checkArg a = case findTypeFun a of - [] -> findSynTypeFun a - ds -> ds + -- Report both the directly-written type functions and the ones + -- hidden behind synonyms, deduplicated (a directly-written type + -- function inside a synonym's argument can also appear in the + -- synonym's expansion). + checkArg a = nub (findTypeFun a ++ findSynTypeFun a) found = concatMap checkArg nonDetArgs in if null found then () else bsErrorUnsafe errh diff --git a/src/comp/Unify.hs b/src/comp/Unify.hs index 61254a247..0f71b8df7 100644 --- a/src/comp/Unify.hs +++ b/src/comp/Unify.hs @@ -1,5 +1,6 @@ {-# LANGUAGE PatternGuards #-} module Unify(Unify(..), matchList) where +import Data.Maybe(fromMaybe, isJust) import Type import Subst import CType @@ -31,9 +32,10 @@ instance Unify Type where -- bound to the unexpanded synonym (which pins a fundep-determined -- variable and makes derived-instance schemes spuriously mismatch). mgu bound_tyvars t1 t2 - | isATFAp t1' || isATFAp t2' = atfUnify bound_tyvars t1' t2' - where t1' = expandSynATF t1 - t2' = expandSynATF t2 + | isJust m1 || isJust m2 = + atfUnify bound_tyvars (fromMaybe t1 m1) (fromMaybe t2 m2) + where m1 = asATFAp t1 + m2 = asATFAp t2 mgu bound_tyvars t1 t2 | kind t1 == KNum = case kind t2 of @@ -50,16 +52,22 @@ instance Unify Type where mgu bound_tyvars (TCon tc1) (TCon tc2) | tc1==tc2 = Just (nullSubst, []) mgu bound_tyvars _ _ = Nothing --- Expand a saturated type-synonym application when (and only when) the --- expansion is a fully applied type-function (ATF) application, so that --- unification treats it exactly like the direct ATF application. --- Synonyms whose expansion does not reveal an ATF at the head are left --- unexpanded, because existing code relies on structural unification of --- unexpanded synonyms (e.g. synonyms that drop some of their parameters). -expandSynATF :: Type -> Type -expandSynATF t - | isSynAp t, not (isUnSatSyn t), isATFAp t' = t' - | otherwise = t +-- Return the type as a fully applied type-function (ATF) application, +-- if it is one -- either directly, or behind a saturated type synonym. +-- Synonyms are not expanded unconditionally, for three reasons: +-- * unification is a hot path and expandSyn is a deep expansion, so +-- only synonym-headed types should pay for it; +-- * expandSyn fails on unsaturated synonym applications, so saturation +-- must be checked first; and +-- * a synonym whose expansion is not an ATF application must keep the +-- existing structural unification of the unexpanded synonym, which +-- existing code relies on (e.g. synonyms that drop some of their +-- parameters; see GitHub issue #311). +asATFAp :: Type -> Maybe Type +asATFAp t + | isATFAp t = Just t + | isSynAp t, not (isUnSatSyn t), isATFAp t' = Just t' + | otherwise = Nothing where t' = expandSyn t isSynAp tt = case fst (splitTAp tt) of TCon (TyCon _ _ (TItype _ _)) -> True diff --git a/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymBoth.bs b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymBoth.bs new file mode 100644 index 000000000..caeac07ca --- /dev/null +++ b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymBoth.bs @@ -0,0 +1,19 @@ +package ATFInInstHeadSynonymBoth where + +-- Both a directly-written and a synonym-hidden type function in the +-- same instance head: both must be reported (two T0156 errors), not +-- just the directly-written one. + +class Container f e | f -> e where + type Elem f = e + wrap :: e -> f + +type ElemSyn f = Elem f + +data Pair a b = Pair a b + +class Foo a where + foo :: a -> Bool + +instance Foo (Pair (Elem f) (ElemSyn g)) where + foo _ = True diff --git a/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymBoth.bs.bsc-out.expected b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymBoth.bs.bsc-out.expected new file mode 100644 index 000000000..ceb5ab5ad --- /dev/null +++ b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymBoth.bs.bsc-out.expected @@ -0,0 +1,7 @@ +checking package dependencies +compiling ATFInInstHeadSynonymBoth.bs +Error: "ATFInInstHeadSynonymBoth.bs", line 18, column 20: (T0156) + Type function `Elem' cannot be used in an instance head +Error: "ATFInInstHeadSynonymBoth.bs", line 18, column 29: (T0156) + Type function `ATFInInstHeadSynonymBoth.Elem' cannot be used in an instance + head diff --git a/testsuite/bsc.typechecker/typeclasses/typeclasses.exp b/testsuite/bsc.typechecker/typeclasses/typeclasses.exp index 264a05dc3..87cfe6ad1 100644 --- a/testsuite/bsc.typechecker/typeclasses/typeclasses.exp +++ b/testsuite/bsc.typechecker/typeclasses/typeclasses.exp @@ -139,6 +139,9 @@ compile_fail_error ATFInInstHeadSynonym.bs T0156 compare_file ATFInInstHeadSynonym.bs.bsc-out compile_fail_error ATFInInstHeadSynonymElsewhere.bs T0156 compare_file ATFInInstHeadSynonymElsewhere.bs.bsc-out +# A direct and a synonym-hidden type function in the same head: both reported +compile_fail_error ATFInInstHeadSynonymBoth.bs T0156 2 +compare_file ATFInInstHeadSynonymBoth.bs.bsc-out compile_fail_error ATFResultNotDetermined.bs T0155 compare_file ATFResultNotDetermined.bs.bsc-out compile_fail_error ATFUnifyError.bs T0030