From b0b0c34ca6b53b37cc9c6c51c8a8f3b554f98ef7 Mon Sep 17 00:00:00 2001 From: Kristian Larsson Date: Tue, 28 Jul 2026 20:15:59 +0200 Subject: [PATCH 1/2] Pin cross-module witness resolution outcomes Three build-failure projects capture how witness resolution behaves when extensions of one class are spread over modules. witness_rival_direct__bf: two modules, neither importing the other, each declare a conditional Pick extension for Box. Both witnesses are genuine rival implementations, so resolving Pick[Box[Both]] is ambiguous. This must keep failing. witness_rival_ancestry__bf: the same rivalry, except each module implements Pick through its own child protocol, so both witnesses reach Pick through their inheritance ancestry rather than declaring it directly. Equally ambiguous, and it must also keep failing, in either import order. witness_canonical_import__bf: module points declares Pt and extends it with Ord, which covers Eq; module hashpt extends Pt with Hashable, whose inherited Eq slots are thereby finalized, so hashpt implements none of them. There is exactly one Eq[Pt] implementation, yet declaring the Hashable extension makes every == involving Pt fail to resolve, both inside hashpt and in any module importing both. This failure is a deficiency; the next commit makes resolution find the one implementation, and flips this project into a running test. --- .../witness_canonical_import__bf/Build.act | 2 ++ .../src/hashpt.act | 11 +++++++ .../src/points.act | 13 ++++++++ .../src/witness_canonical_import__bf.act | 23 ++++++++++++++ .../witness_rival_ancestry__bf/Build.act | 2 ++ .../witness_rival_ancestry__bf/src/model.act | 31 +++++++++++++++++++ .../src/provider_a.act | 7 +++++ .../src/provider_b.act | 7 +++++ .../src/witness_rival_ancestry__bf.act | 16 ++++++++++ .../witness_rival_direct__bf/Build.act | 2 ++ .../witness_rival_direct__bf/src/model.act | 21 +++++++++++++ .../src/provider_a.act | 5 +++ .../src/provider_b.act | 5 +++ .../src/witness_rival_direct__bf.act | 15 +++++++++ 14 files changed, 160 insertions(+) create mode 100644 test/regression_auto/witness_canonical_import__bf/Build.act create mode 100644 test/regression_auto/witness_canonical_import__bf/src/hashpt.act create mode 100644 test/regression_auto/witness_canonical_import__bf/src/points.act create mode 100644 test/regression_auto/witness_canonical_import__bf/src/witness_canonical_import__bf.act create mode 100644 test/regression_auto/witness_rival_ancestry__bf/Build.act create mode 100644 test/regression_auto/witness_rival_ancestry__bf/src/model.act create mode 100644 test/regression_auto/witness_rival_ancestry__bf/src/provider_a.act create mode 100644 test/regression_auto/witness_rival_ancestry__bf/src/provider_b.act create mode 100644 test/regression_auto/witness_rival_ancestry__bf/src/witness_rival_ancestry__bf.act create mode 100644 test/regression_auto/witness_rival_direct__bf/Build.act create mode 100644 test/regression_auto/witness_rival_direct__bf/src/model.act create mode 100644 test/regression_auto/witness_rival_direct__bf/src/provider_a.act create mode 100644 test/regression_auto/witness_rival_direct__bf/src/provider_b.act create mode 100644 test/regression_auto/witness_rival_direct__bf/src/witness_rival_direct__bf.act diff --git a/test/regression_auto/witness_canonical_import__bf/Build.act b/test/regression_auto/witness_canonical_import__bf/Build.act new file mode 100644 index 000000000..1f373f19e --- /dev/null +++ b/test/regression_auto/witness_canonical_import__bf/Build.act @@ -0,0 +1,2 @@ +name = "witness_canonical_import__bf" +fingerprint = 0x333146d440f0f96c diff --git a/test/regression_auto/witness_canonical_import__bf/src/hashpt.act b/test/regression_auto/witness_canonical_import__bf/src/hashpt.act new file mode 100644 index 000000000..1901c4de5 --- /dev/null +++ b/test/regression_auto/witness_canonical_import__bf/src/hashpt.act @@ -0,0 +1,11 @@ +# The extending module: Hashable inherits Eq, but Eq[Pt] was finalized by +# points' Ord extension, so this extension implements none of Eq. + +import points + +extension points.Pt (Hashable): + def hash(self, h): + self.x.hash(h) + +def same_here(a: points.Pt, b: points.Pt) -> bool: + return a == b diff --git a/test/regression_auto/witness_canonical_import__bf/src/points.act b/test/regression_auto/witness_canonical_import__bf/src/points.act new file mode 100644 index 000000000..e1bccb900 --- /dev/null +++ b/test/regression_auto/witness_canonical_import__bf/src/points.act @@ -0,0 +1,13 @@ +# The providing module: declares the class and extends it with Ord, which +# covers Eq, so this module owns the one Eq[Pt] implementation. + +class Pt(object): + x: int + def __init__(self, x: int): + self.x = x + +extension Pt (Ord): + def __eq__(a: Pt, b: Pt) -> bool: + return a.x == b.x + def __lt__(a: Pt, b: Pt) -> bool: + return a.x < b.x diff --git a/test/regression_auto/witness_canonical_import__bf/src/witness_canonical_import__bf.act b/test/regression_auto/witness_canonical_import__bf/src/witness_canonical_import__bf.act new file mode 100644 index 000000000..212b3c5c9 --- /dev/null +++ b/test/regression_auto/witness_canonical_import__bf/src/witness_canonical_import__bf.act @@ -0,0 +1,23 @@ +# There is exactly one Eq[Pt] implementation, in points. Yet declaring the +# Hashable extension makes every == involving Pt fail to resolve, here and +# inside hashpt itself: hashpt's extension registers a second Eq witness for +# Pt via its ancestry, and the solver requires a single candidate. This +# build failure documents the deficiency the next commit removes. + +import points +import hashpt + +actor main(env): + a = points.Pt(1) + b = points.Pt(1) + if not (a == b) or a == points.Pt(2): + print("FAIL: == through the imported Ord witness") + await async env.exit(1) + if not hashpt.same_here(a, b): + print("FAIL: == inside the extending module") + await async env.exit(1) + l = sorted([points.Pt(3), points.Pt(1), points.Pt(2)]) + if l[0].x != 1 or l[1].x != 2 or l[2].x != 3: + print("FAIL: sorted through the imported Ord witness") + await async env.exit(1) + await async env.exit(0) diff --git a/test/regression_auto/witness_rival_ancestry__bf/Build.act b/test/regression_auto/witness_rival_ancestry__bf/Build.act new file mode 100644 index 000000000..759e0ce94 --- /dev/null +++ b/test/regression_auto/witness_rival_ancestry__bf/Build.act @@ -0,0 +1,2 @@ +name = "witness_rival_ancestry__bf" +fingerprint = 0x24c532a6a1b59c10 diff --git a/test/regression_auto/witness_rival_ancestry__bf/src/model.act b/test/regression_auto/witness_rival_ancestry__bf/src/model.act new file mode 100644 index 000000000..22e0c02e6 --- /dev/null +++ b/test/regression_auto/witness_rival_ancestry__bf/src/model.act @@ -0,0 +1,31 @@ +protocol NeedA: + a : () -> int + +protocol NeedB: + b : () -> int + +protocol Pick: + pick : () -> int + +protocol PickA (Pick): + xa : () -> int + +protocol PickB (Pick): + xb : () -> int + +class Box[X](object): + item: X + def __init__(self, item: X): + self.item = item + +class Both(object): + def __init__(self): + pass + +extension Both (NeedA): + def a(self) -> int: + return 1 + +extension Both (NeedB): + def b(self) -> int: + return 2 diff --git a/test/regression_auto/witness_rival_ancestry__bf/src/provider_a.act b/test/regression_auto/witness_rival_ancestry__bf/src/provider_a.act new file mode 100644 index 000000000..f90967749 --- /dev/null +++ b/test/regression_auto/witness_rival_ancestry__bf/src/provider_a.act @@ -0,0 +1,7 @@ +from model import Box, NeedA, PickA + +extension Box[X(NeedA)] (PickA): + def pick(self) -> int: + return 1 + def xa(self) -> int: + return 0 diff --git a/test/regression_auto/witness_rival_ancestry__bf/src/provider_b.act b/test/regression_auto/witness_rival_ancestry__bf/src/provider_b.act new file mode 100644 index 000000000..2841646d9 --- /dev/null +++ b/test/regression_auto/witness_rival_ancestry__bf/src/provider_b.act @@ -0,0 +1,7 @@ +from model import Box, NeedB, PickB + +extension Box[Y(NeedB)] (PickB): + def pick(self) -> int: + return 2 + def xb(self) -> int: + return 0 diff --git a/test/regression_auto/witness_rival_ancestry__bf/src/witness_rival_ancestry__bf.act b/test/regression_auto/witness_rival_ancestry__bf/src/witness_rival_ancestry__bf.act new file mode 100644 index 000000000..10789d783 --- /dev/null +++ b/test/regression_auto/witness_rival_ancestry__bf/src/witness_rival_ancestry__bf.act @@ -0,0 +1,16 @@ +# Two independent modules each implement Pick for Box through their own child +# protocol; neither saw the other, so both registrations carry genuine rival +# implementations reached through ancestry. Resolving Pick[Box[Both]] must be +# rejected as ambiguous, never silently decided by import or path shape. + +from model import Box, Both, Pick +import provider_a +import provider_b + +def choose[T(Pick)](x: T) -> int: + return x.pick() + +actor main(env): + if choose(Box(Both())) == 2: + await async env.exit(0) + await async env.exit(1) diff --git a/test/regression_auto/witness_rival_direct__bf/Build.act b/test/regression_auto/witness_rival_direct__bf/Build.act new file mode 100644 index 000000000..e5ec7def9 --- /dev/null +++ b/test/regression_auto/witness_rival_direct__bf/Build.act @@ -0,0 +1,2 @@ +name = "witness_rival_direct__bf" +fingerprint = 0x2f9c66edab2fa26f diff --git a/test/regression_auto/witness_rival_direct__bf/src/model.act b/test/regression_auto/witness_rival_direct__bf/src/model.act new file mode 100644 index 000000000..430ff5e42 --- /dev/null +++ b/test/regression_auto/witness_rival_direct__bf/src/model.act @@ -0,0 +1,21 @@ +protocol NeedA: + a : () -> int + +protocol NeedB: + b : () -> int + +protocol Pick: + pick : () -> int + +class Box[X](object): + item: X + def __init__(self, item: X): + self.item = item + +class OnlyB(object): + def __init__(self): + pass + +extension OnlyB (NeedB): + def b(self) -> int: + return 2 diff --git a/test/regression_auto/witness_rival_direct__bf/src/provider_a.act b/test/regression_auto/witness_rival_direct__bf/src/provider_a.act new file mode 100644 index 000000000..7704ba618 --- /dev/null +++ b/test/regression_auto/witness_rival_direct__bf/src/provider_a.act @@ -0,0 +1,5 @@ +from model import Box, NeedA, Pick + +extension Box[X(NeedA)] (Pick): + def pick(self) -> int: + return 1 diff --git a/test/regression_auto/witness_rival_direct__bf/src/provider_b.act b/test/regression_auto/witness_rival_direct__bf/src/provider_b.act new file mode 100644 index 000000000..c589f61dd --- /dev/null +++ b/test/regression_auto/witness_rival_direct__bf/src/provider_b.act @@ -0,0 +1,5 @@ +from model import Box, NeedB, Pick + +extension Box[Y(NeedB)] (Pick): + def pick(self) -> int: + return 2 diff --git a/test/regression_auto/witness_rival_direct__bf/src/witness_rival_direct__bf.act b/test/regression_auto/witness_rival_direct__bf/src/witness_rival_direct__bf.act new file mode 100644 index 000000000..4f552656c --- /dev/null +++ b/test/regression_auto/witness_rival_direct__bf/src/witness_rival_direct__bf.act @@ -0,0 +1,15 @@ +# Two independent modules each declare a conditional Pick extension for Box. +# Neither shadows the other, so any use of a Pick[Box[...]] witness is +# ambiguous and must be rejected regardless of import order. + +from model import Box, OnlyB, Pick +import provider_a +import provider_b + +def choose[T(Pick)](x: T) -> int: + return x.pick() + +actor main(env): + if choose(Box(OnlyB())) == 2: + await async env.exit(0) + await async env.exit(1) From 839ce3edb8ca8c5283963071615b0943766a3a2d Mon Sep 17 00:00:00 2001 From: Kristian Larsson Date: Tue, 28 Jul 2026 20:17:57 +0200 Subject: [PATCH 2/2] Register no witness for finalized protocols An extension covers its protocol's whole inheritance ancestry: extending Pt with Ord also makes the extension a witness for Eq, because Ord inherits Eq. The first extension to cover a protocol owns it: the type checker requires it to implement the protocol's methods, and every later extension covering the same protocol is forbidden from implementing them again (checkAttributes calls these methods finalized). So for each protocol and type there is exactly one implementation, held by whichever extension came first. Witness registration did not follow that rule. An extension registered a witness for every protocol in its ancestry, including the finalized ones it holds no implementation for. Such an entry is an empty shell: resolution that lands on it finds methods the extension was not allowed to write. Within one module the shells were harmless, because registration deduplicates against the local table and the owning extension's earlier entry wins. Across modules there was no deduplication at all, since the local table and the imported interfaces are enumerated separately: # module points extension Pt (Ord): def __eq__(a, b): ... # the one Eq[Pt] implementation ... # module hashpt extension points.Pt (Hashable): # Hashable inherits Eq def hash(self, h): ... hashpt's extension implements nothing of Eq, which is finalized by points' Ord extension, yet it registered a second Eq witness for Pt. The constraint solver requires exactly one candidate per witness lookup, so every == involving Pt stopped compiling, inside hashpt and in every module importing both. In practice, extending an imported class with any protocol that inherits something was unusable. Nothing about a registration itself distinguishes a shell from a genuine implementation declared in an unrelated module; the distinction exists only at the moment the extension is checked, when hasWitness tells us whether an earlier witness covers the protocol. So record that answer: NExt gains a field listing the extension's finalized protocols (bumping the .tydb interface version), and those protocols are skipped everywhere witnesses are registered: the local type table (setupWits), the extension's own self-witnesses used while checking its body (tydefineInst), and the entries importers read from its interface (extWitnesses). Every remaining registration is backed by an implementation. A protocol with one implementation resolves to it from any module, in any import order. And nothing is silently legalized: if two independent modules, neither importing the other, both implement the same protocol for the same type, then neither was finalized, both register, and every use remains ambiguous and rejected in either import order, whether they cover the protocol directly or through their ancestry. Of the three projects pinned by the previous commit, the two rival ones keep failing unchanged; witness_canonical_import, previously rejected despite its single Eq implementation, now builds and runs. --- compiler/acton/test_incremental.hs | 2 +- compiler/lib/src/Acton/Completion.hs | 2 +- compiler/lib/src/Acton/Converter.hs | 2 +- compiler/lib/src/Acton/DocPrinter.hs | 2 +- compiler/lib/src/Acton/Env.hs | 10 +++---- compiler/lib/src/Acton/Hashing.hs | 6 ++--- compiler/lib/src/Acton/NameInfo.hs | 26 +++++++++---------- compiler/lib/src/Acton/Solver.hs | 4 +++ compiler/lib/src/Acton/Syntax.hs | 2 +- compiler/lib/src/Acton/TypeEnv.hs | 4 +-- compiler/lib/src/Acton/Types.hs | 11 +++++--- compiler/lib/src/Acton/WitKnots.hs | 4 +-- compiler/lib/src/InterfaceFiles.hs | 6 ++--- compiler/lib/test/ActonSpec.hs | 3 ++- .../witness_canonical_import/Build.act | 2 ++ .../src/hashpt.act | 0 .../src/points.act | 0 .../src/witness_canonical_import.act} | 9 +++---- .../witness_canonical_import__bf/Build.act | 2 -- 19 files changed, 52 insertions(+), 45 deletions(-) create mode 100644 test/regression_auto/witness_canonical_import/Build.act rename test/regression_auto/{witness_canonical_import__bf => witness_canonical_import}/src/hashpt.act (100%) rename test/regression_auto/{witness_canonical_import__bf => witness_canonical_import}/src/points.act (100%) rename test/regression_auto/{witness_canonical_import__bf/src/witness_canonical_import__bf.act => witness_canonical_import/src/witness_canonical_import.act} (61%) delete mode 100644 test/regression_auto/witness_canonical_import__bf/Build.act diff --git a/compiler/acton/test_incremental.hs b/compiler/acton/test_incremental.hs index 7fefeced0..910dcb963 100644 --- a/compiler/acton/test_incremental.hs +++ b/compiler/acton/test_incremental.hs @@ -1442,7 +1442,7 @@ p28_protocol_extension_deps = testCase "28-protocol/extension deps are recorded let I.NModule _ iface _ = nmod extMatch (n, _) = prstr n == "BarProtoD_Widget" case find extMatch iface of - Just (_, I.NExt _ _ ps _ _ _) -> do + Just (_, I.NExt _ _ ps _ _ _ _) -> do let protoNames = sort [ prstr (A.tcname p) | (_, p) <- ps ] assertEqual "extension protocol mro" (sort ["incremental_cases.a.BarProto", "incremental_cases.a.BazProto", "incremental_cases.a.FooProto"]) protoNames _ -> assertFailure "missing extension NameInfo for BarProtoD_Widget" diff --git a/compiler/lib/src/Acton/Completion.hs b/compiler/lib/src/Acton/Completion.hs index 9e88a6535..ce60c9701 100644 --- a/compiler/lib/src/Acton/Completion.hs +++ b/compiler/lib/src/Acton/Completion.hs @@ -847,7 +847,7 @@ docOfInfo info = I.NClass _ _ _ doc -> doc I.NProto _ _ _ doc -> doc I.NType _ _ doc -> doc - I.NExt _ _ _ _ _ doc -> doc + I.NExt _ _ _ _ _ _ doc -> doc _ -> Nothing typeDoc :: Env.Env0 -> S.Type -> Maybe String diff --git a/compiler/lib/src/Acton/Converter.hs b/compiler/lib/src/Acton/Converter.hs index 467b64994..ccedec3b9 100644 --- a/compiler/lib/src/Acton/Converter.hs +++ b/compiler/lib/src/Acton/Converter.hs @@ -248,7 +248,7 @@ convEnvProtos env = convertModules convSources conv env conv m (n, NAct q p k te doc) = [(n, NAct (noqual env q) (qualWRow env q p) k (concat $ map (conv m) te) doc)] conv m ni@(n, NProto q us te doc) = map (fromClass env) $ convProtocol (define [ni] env) n q us [] [] (fromTEnv te) - conv m ni@(n, NExt q c us te opts doc) + conv m ni@(n, NExt q c us te opts _ doc) = map (fromClass env) $ convExtension (define [ni] env) n c q us [] [] (fromTEnv te) opts conv m (n, NClass q us te doc) = [(n, NClass (noqual env q) us (witSigs ++ convClassTEnv env q te) doc)] where witSigs = [ (w, NSig (monotype t) Property Nothing) | (w,t) <- qualWits env q ] diff --git a/compiler/lib/src/Acton/DocPrinter.hs b/compiler/lib/src/Acton/DocPrinter.hs index a67c7d1d1..4b55fb508 100644 --- a/compiler/lib/src/Acton/DocPrinter.hs +++ b/compiler/lib/src/Acton/DocPrinter.hs @@ -99,7 +99,7 @@ extractNameDocstring (NAct _ _ _ _ mdoc) = mdoc extractNameDocstring (NClass _ _ _ mdoc) = mdoc extractNameDocstring (NProto _ _ _ mdoc) = mdoc extractNameDocstring (NType _ _ mdoc) = mdoc -extractNameDocstring (NExt _ _ _ _ _ mdoc) = mdoc +extractNameDocstring (NExt _ _ _ _ _ _ mdoc) = mdoc extractNameDocstring _ = Nothing -- | Document a declaration in Markdown format with types diff --git a/compiler/lib/src/Acton/Env.hs b/compiler/lib/src/Acton/Env.hs index 8ab2b39f9..068ef127c 100644 --- a/compiler/lib/src/Acton/Env.hs +++ b/compiler/lib/src/Acton/Env.hs @@ -268,7 +268,7 @@ moduleQNameKeys _ qn = [qn] extWitnesses :: ModName -> TEnv -> [Witness] extWitnesses m exts = fst (foldl' add ([], Map.empty) wits) - where wits = [ WClass q (tCon c) p (GName m n) ws (length opts) | (n, NExt q c ps _ opts _) <- exts, (ws,p) <- ps ] + where wits = [ WClass q (tCon c) p (GName m n) ws (length opts) | (n, NExt q c ps _ opts fnl _) <- exts, (ws,p) <- ps, tcname p `notElem` fnl ] -- Duplicate checking scans only the (proto name, type name) bucket instead -- of every accumulated witness: `same` implies equal proto names and equal -- wtypes (hence equal type-name keys), so bucketing loses no duplicates, @@ -392,7 +392,7 @@ instance Unalias NameInfo where unalias env (NClass q us te doc)= NClass (unalias env q) (unalias env us) (unalias env te) doc unalias env (NProto q us te doc)= NProto (unalias env q) (unalias env us) (unalias env te) doc unalias env (NType q t doc) = NType (unalias env q) (unalias env t) doc - unalias env (NExt q c ps te opts doc)= NExt (unalias env q) (unalias env c) (unalias env ps) (unalias env te) opts doc + unalias env (NExt q c ps te opts fnl doc)= NExt (unalias env q) (unalias env c) (unalias env ps) (unalias env te) opts (unalias env fnl) doc unalias env (NTVar k c ps) = NTVar k (unalias env c) (unalias env ps) unalias env (NAlias qn) = NAlias (unalias env qn) unalias env NReserved = NReserved @@ -829,7 +829,7 @@ findConName n env = case findQName n env of NClass q us te _ -> (q, us, te) NProto q us te _ -> (q, us, te) NType q t _ -> (q, [], []) - NExt q c us te _ _ -> (q, us, te) + NExt q c us te _ _ _ -> (q, us, te) NReserved -> nameReserved n i -> err1 n ("findConName: Class or protocol name expected, got " ++ show i ++ " --- ") @@ -1604,8 +1604,8 @@ instance Simp (Name, NameInfo) where where env' = defineTVars (stripQual q) env simp env (n, NType q t doc) = (n, NType (simp env' q) (simp env' t) doc) where env' = defineTVars (stripQual q) env - simp env (n, NExt q c us te opts doc) - = (n, NExt q' (vsubst s $ simp env' c) (vsubst s $ simp env' us) (vsubst s $ simp env' te) opts doc) + simp env (n, NExt q c us te opts fnl doc) + = (n, NExt q' (vsubst s $ simp env' c) (vsubst s $ simp env' us) (vsubst s $ simp env' te) opts fnl doc) where (q', s) = simpQuant env (simp env' q) (vfree c ++ vfree us ++ vfree te) env' = defineTVars (stripQual q) env simp env (n, NAct q p k te doc) = (n, NAct (simp env' q) (simp env' p) (simp env' k) (simp env' $ notHidden te) doc) diff --git a/compiler/lib/src/Acton/Hashing.hs b/compiler/lib/src/Acton/Hashing.hs index a419f162f..490c5aba5 100644 --- a/compiler/lib/src/Acton/Hashing.hs +++ b/compiler/lib/src/Acton/Hashing.hs @@ -706,9 +706,9 @@ feedNameInfo info sink = feedTag 249 sink >> case info of I.NClass q cs te _ -> feedTag 5 sink >> feedQBinds q sink >> feedList feedWTCon cs sink >> feedTEnv te sink I.NProto q ps te _ -> feedTag 6 sink >> feedQBinds q sink >> feedList feedWTCon ps sink >> feedTEnv te sink I.NType q t _ -> feedTag 10 sink >> feedQBinds q sink >> feedType t sink - I.NExt q c ps te o _ -> + I.NExt q c ps te o fnl _ -> feedTag 7 sink >> feedQBinds q sink >> feedTCon c sink >> feedList feedWTCon ps sink >> - feedTEnv te sink >> feedList feedName o sink + feedTEnv te sink >> feedList feedName o sink >> feedList feedQName fnl sink I.NTVar k c ps -> feedTag 8 sink >> feedKind k sink >> feedTCon c sink >> feedList feedTCon ps sink I.NAlias qn -> feedTag 9 sink >> feedQName qn sink I.NReserved -> feedTag 12 sink @@ -871,7 +871,7 @@ foldNameInfoDeps add info acc = case info of I.NClass q ws te _ -> foldDepsTEnv add te (foldDepsList (foldDepsWTCon add) ws (foldDepsList (foldDepsQBind add) q acc)) I.NProto q ws te _ -> foldDepsTEnv add te (foldDepsList (foldDepsWTCon add) ws (foldDepsList (foldDepsQBind add) q acc)) I.NType q t _ -> foldDepsType add t (foldDepsList (foldDepsQBind add) q acc) - I.NExt q c ws te _ _ -> foldDepsTEnv add te (foldDepsList (foldDepsWTCon add) ws (foldDepsTCon add c (foldDepsList (foldDepsQBind add) q acc))) + I.NExt q c ws te _ fnl _ -> foldDepsTEnv add te (foldDepsList (foldDepsWTCon add) ws (foldDepsTCon add c (foldDepsList (foldDepsQBind add) q (foldDepsList (\qn a -> add qn a) fnl acc)))) I.NTVar _ c ps -> foldDepsList (foldDepsTCon add) ps (foldDepsTCon add c acc) I.NAlias qn -> add qn acc I.NReserved -> acc diff --git a/compiler/lib/src/Acton/NameInfo.hs b/compiler/lib/src/Acton/NameInfo.hs index d5ad0fd90..5ee495192 100644 --- a/compiler/lib/src/Acton/NameInfo.hs +++ b/compiler/lib/src/Acton/NameInfo.hs @@ -57,7 +57,7 @@ data NameInfo = NVar Type | NClass QBinds [WTCon] TEnv (Maybe String) | NProto QBinds [WTCon] TEnv (Maybe String) | NType QBinds Type (Maybe String) - | NExt QBinds TCon [WTCon] TEnv [Name] (Maybe String) + | NExt QBinds TCon [WTCon] TEnv [Name] [QName] (Maybe String) | NTVar Kind CCon [PCon] | NAlias QName | NReserved @@ -83,7 +83,7 @@ stripDocsNI ni = case ni of NClass q cs te _ -> NClass q cs (map stripBind te) Nothing NProto q ps te _ -> NProto q ps (map stripBind te) Nothing NType q t _ -> NType q t Nothing - NExt q c ps te o _ -> NExt q c ps (map stripBind te) o Nothing + NExt q c ps te o fn _ -> NExt q c ps (map stripBind te) o fn Nothing NDef sc dec _ -> NDef sc dec Nothing NSig sc dec _ -> NSig sc dec Nothing other -> other @@ -108,8 +108,8 @@ stripLocsNI ni = case ni of NClass q cs te doc -> NClass (stripLocsQBinds q) (map stripLocsWTCon cs) (stripLocsTEnv te) doc NProto q ps te doc -> NProto (stripLocsQBinds q) (map stripLocsWTCon ps) (stripLocsTEnv te) doc NType q t doc -> NType (stripLocsQBinds q) (stripLocsType t) doc - NExt q c ps te o doc -> - NExt (stripLocsQBinds q) (stripLocsTCon c) (map stripLocsWTCon ps) (stripLocsTEnv te) (map stripLocsName o) doc + NExt q c ps te o fn doc -> + NExt (stripLocsQBinds q) (stripLocsTCon c) (map stripLocsWTCon ps) (stripLocsTEnv te) (map stripLocsName o) (map stripLocsQName fn) doc NTVar k c ps -> NTVar k (stripLocsTCon c) (map stripLocsTCon ps) NAlias qn -> NAlias (stripLocsQName qn) NReserved -> NReserved @@ -206,11 +206,11 @@ instance Pretty (Name,NameInfo) where = text "protocol" <+> pretty n <> nonEmpty brackets commaList q <+> nonEmpty parens commaList us <> colon $+$ nest 4 (prettyDocstring doc) $+$ (nest 4 $ prettyOrPass te) pretty (n, NType q t doc) = text "type" <+> pretty n <> nonEmpty brackets commaList q <+> equals <+> pretty t $+$ nest 4 (prettyDocstring doc) - pretty (w, NExt [] c ps te opts doc) + pretty (w, NExt [] c ps te opts _ doc) = {-pretty w <+> colon <+> -} text "extension" <+> pretty c <+> parens (commaList ps) <> colon $+$ nest 4 (prettyDocstring doc) $+$ (nest 4 $ prettyOrPass te) - pretty (w, NExt q c ps te opts doc) + pretty (w, NExt q c ps te opts _ doc) = {-pretty w <+> colon <+> -} text "extension" <+> pretty q <+> text "=>" <+> pretty c <+> parens (commaList ps) <> colon $+$ nest 4 (prettyDocstring doc) $+$ (nest 4 $ prettyOrPass te) @@ -236,7 +236,7 @@ instance VFree NameInfo where vfree (NClass q us te _) = (vfree q ++ vfree us ++ vfree te) \\ (tvSelf : qbound q) vfree (NProto q us te _) = (vfree q ++ vfree us ++ vfree te) \\ (tvSelf : qbound q) vfree (NType q t _) = (vfree q ++ vfree t) \\ qbound q - vfree (NExt q c ps te _ _) = (vfree q ++ vfree c ++ vfree ps ++ vfree te) \\ (tvSelf : qbound q) + vfree (NExt q c ps te _ _ _) = (vfree q ++ vfree c ++ vfree ps ++ vfree te) \\ (tvSelf : qbound q) vfree (NTVar k c ps) = vfree c ++ vfree ps vfree (NAlias qn) = [] vfree NReserved = [] @@ -250,7 +250,7 @@ instance VSubst NameInfo where vsubst s (NClass q us te x) = NClass (vsubst s q) (vsubst s us) (vsubst s te) x vsubst s (NProto q us te x) = NProto (vsubst s q) (vsubst s us) (vsubst s te) x vsubst s (NType q t x) = NType (vsubst s q) (vsubst s t) x - vsubst s (NExt q c ps te opts x) = NExt (vsubst s q) (vsubst s c) (vsubst s ps) (vsubst s te) opts x + vsubst s (NExt q c ps te opts fn x) = NExt (vsubst s q) (vsubst s c) (vsubst s ps) (vsubst s te) opts fn x vsubst s (NTVar k c ps) = NTVar k (vsubst s c) (vsubst s ps) vsubst s (NAlias qn) = NAlias qn vsubst s NReserved = NReserved @@ -264,7 +264,7 @@ instance UFree NameInfo where ufree (NClass q us te _) = ufree q ++ ufree us ++ ufree te ufree (NProto q us te _) = ufree q ++ ufree us ++ ufree te ufree (NType q t _) = ufree q ++ ufree t - ufree (NExt q c ps te _ _) = ufree q ++ ufree c ++ ufree ps ++ ufree te + ufree (NExt q c ps te _ _ _) = ufree q ++ ufree c ++ ufree ps ++ ufree te ufree (NTVar k c ps) = ufree c ++ ufree ps ufree (NAlias qn) = [] ufree NReserved = [] @@ -281,7 +281,7 @@ instance Polarity NameInfo where polvars (NClass q us te _) = polvars q `polcat` polvars us `polcat` polvars te polvars (NProto q us te _) = polvars q `polcat` polvars us `polcat` polvars te polvars (NType q t _) = polvars q `polcat` polvars t - polvars (NExt q c ps te _ _) = polvars q `polcat` polvars c `polcat` polvars ps `polcat` polvars te + polvars (NExt q c ps te _ _ _) = polvars q `polcat` polvars c `polcat` polvars ps `polcat` polvars te polvars (NTVar k c ps) = polvars c `polcat` polvars ps polvars _ = ([],[]) @@ -297,7 +297,7 @@ wildargs i = [ tWild | _ <- nbinds i ] nbinds (NClass q _ _ _) = q nbinds (NProto q _ _ _) = q nbinds (NType q _ _) = q - nbinds (NExt q _ _ _ _ _) = q + nbinds (NExt q _ _ _ _ _ _) = q -- TEnv filters -------------------------------------------------------------------------------------------------------- @@ -397,7 +397,7 @@ instance Vars NameInfo where NClass q ws te _ -> freeQ q ++ freeQ ws ++ freeQ te NProto q ws te _ -> freeQ q ++ freeQ ws ++ freeQ te NType q t _ -> freeQ q ++ freeQ t - NExt q c ws te _ _ -> freeQ q ++ freeQ c ++ freeQ ws ++ freeQ te + NExt q c ws te _ fn _ -> freeQ q ++ freeQ c ++ freeQ ws ++ freeQ te ++ fn NTVar _ c ps -> freeQ c ++ freeQ ps NAlias qn -> freeQ qn NReserved -> [] @@ -410,7 +410,7 @@ instance Vars NameInfo where nmap f (NClass q ws te s) = NClass (nmap f q) (nmap f ws) (nmap f te) s nmap f (NProto q ws te s) = NProto (nmap f q) (nmap f ws) (nmap f te) s nmap f (NType q t s) = NType (nmap f q) (nmap f t) s - nmap f (NExt q c ws te o s) = NExt (nmap f q) (nmap f c) (nmap f ws) (nmap f te) o s + nmap f (NExt q c ws te o fn s) = NExt (nmap f q) (nmap f c) (nmap f ws) (nmap f te) o fn s nmap f (NTVar k c ps) = NTVar k (nmap f c) (nmap f ps) nmap f (NAlias n) = NAlias (nmap f n) nmap f i = i diff --git a/compiler/lib/src/Acton/Solver.hs b/compiler/lib/src/Acton/Solver.hs index 4b7487f74..9c94dda88 100644 --- a/compiler/lib/src/Acton/Solver.hs +++ b/compiler/lib/src/Acton/Solver.hs @@ -791,6 +791,10 @@ solveMutAttr (wf,sc,dec) c@(Mut info env t1 n t2) -- are small and enumerated lazily, so we never force the whole, ever-growing -- proto-keyed list. Only the rare TFX goal falls back to the proto-keyed bucket. -- Imported witnesses are merged in lazily by witsByTName/witsByPName. +-- An extension registers no witness for a protocol whose slots were finalized +-- by an earlier witness (see the NExt finals field), so every registration is +-- a genuine implementation and multiple matches mean rival extensions, which +-- stay unresolved. findWitness :: Env -> Type -> PCon -> [Witness] findWitness env t p = filter match $ candidates t where eqhead (TCon _ c) (TCon _ c') = tcname c == tcname c' diff --git a/compiler/lib/src/Acton/Syntax.hs b/compiler/lib/src/Acton/Syntax.hs index 1d64146e6..fe05bda3c 100644 --- a/compiler/lib/src/Acton/Syntax.hs +++ b/compiler/lib/src/Acton/Syntax.hs @@ -26,7 +26,7 @@ import Control.DeepSeq import Prelude hiding((<>)) version :: [Int] -version = [0,34] +version = [0,35] data Module = Module { modname::ModName, imps::[Import], mdoc::Maybe String, mbody::Suite } deriving (Eq,Show,Generic,NFData) diff --git a/compiler/lib/src/Acton/TypeEnv.hs b/compiler/lib/src/Acton/TypeEnv.hs index 50f55f109..e63cb469c 100644 --- a/compiler/lib/src/Acton/TypeEnv.hs +++ b/compiler/lib/src/Acton/TypeEnv.hs @@ -282,7 +282,7 @@ setupCons f te x = foldl' (addconinfo f) x te setupWits :: (TypeX -> Witness -> TypeX) -> TEnv -> TypeX -> TypeX setupWits add te x = foldl' add x wits - where wits = [ WClass q (tCon c) p (NoQ n) ws (length opts) | (n, NExt q c ps _ opts _) <- te, (ws,p) <- ps ] + where wits = [ WClass q (tCon c) p (NoQ n) ws (length opts) | (n, NExt q c ps _ opts fnl _) <- te, (ws,p) <- ps, tcname p `notElem` fnl ] addvarinfo x (tv, c, _) = x{ tyids = Map.insert qn tid (tyids x), tyidHash = HashMap.insert qn tid (tyidHash x), @@ -975,7 +975,7 @@ instance USubst NameInfo where usubstWith s (NClass q us te doc) = NClass (usubstWith s q) (usubstWith s us) (usubstWith s te) doc usubstWith s (NProto q us te doc) = NProto (usubstWith s q) (usubstWith s us) (usubstWith s te) doc usubstWith s (NType q t doc) = NType (usubstWith s q) (usubstWith s t) doc - usubstWith s (NExt q c ps te opts doc) = NExt (usubstWith s q) (usubstWith s c) (usubstWith s ps) (usubstWith s te) opts doc + usubstWith s (NExt q c ps te opts fnl doc) = NExt (usubstWith s q) (usubstWith s c) (usubstWith s ps) (usubstWith s te) opts fnl doc usubstWith s (NTVar k c ps) = NTVar k (usubstWith s c) (usubstWith s ps) usubstWith s (NAlias qn) = NAlias qn usubstWith s NReserved = NReserved diff --git a/compiler/lib/src/Acton/Types.hs b/compiler/lib/src/Acton/Types.hs index fa740eb5d..3015e2d58 100644 --- a/compiler/lib/src/Acton/Types.hs +++ b/compiler/lib/src/Acton/Types.hs @@ -1131,13 +1131,15 @@ instance InfEnv Decl where let te1 = unSig $ selfSubst n q asigs te2 = te ++ te1 b2 = addImpl te1 b1 - return ([], [(extensionName us c, NExt q c ps te2 [] ddoc)], Extension l q c us b2 ddoc) + return ([], [(extensionName us c, NExt q c ps te2 [] fnl ddoc)], Extension l q c us b2 ddoc) where TC n ts = c env1 = define (toSigs te') $ reserve (assigned b) $ tydefineVars (stripQual q') $ setInClass env witsearch = findWitness env (tCon c) u u = head us ps = selfSubst n q $ mro1 env us -- TODO: check that ps doesn't contradict any previous extension mro for c - final = concat [ conAttrs env (tcname p) | (_,p) <- tail ps, hasWitness env (tCon c) p ] + covered = [ p | (_,p) <- tail ps, hasWitness env (tCon c) p ] + fnl = nub (map tcname covered) + final = concat [ conAttrs env (tcname p) | p <- covered ] te' = parentTEnv env ps q' = selfQuant n q @@ -1831,10 +1833,11 @@ instance Check Decl where (cs1,eq1) <- markScoped env n' q' te (csu++csb) b' <- usubst b' return (cs1, convExtension env n' c q ps eq1 wmap b' []) - where env1 = tydefineInst c ps thisKW' $ tydefineVars q' $ setInClass env + where env1 = tydefineInst c ps' thisKW' $ tydefineVars q' $ setInClass env + ps' = [ (ws,p) | (ws,p) <- ps, tcname p `notElem` fnl ] n = tcname c n' = extensionName us c - NExt _ _ ps te _ _ = findName n' env + NExt _ _ ps te _ fnl _ = findName n' env te' = selfSubst n q te q' = selfQuant n q tc = TC n (map tVar $ qbound q) diff --git a/compiler/lib/src/Acton/WitKnots.hs b/compiler/lib/src/Acton/WitKnots.hs index bd6c88554..74f9f0673 100644 --- a/compiler/lib/src/Acton/WitKnots.hs +++ b/compiler/lib/src/Acton/WitKnots.hs @@ -153,9 +153,9 @@ depsof w cycledeps = case lookup w cycledeps of _ -> [] -addopts cycledeps (n, NExt q c us te _ doc) +addopts cycledeps (n, NExt q c us te _ fnl doc) = --trace ("#### Extending " ++ prstr n ++ " with opts " ++ prstrs opts) $ - (n, NExt q c us te opts doc) + (n, NExt q c us te opts fnl doc) where opts = depsof n cycledeps addopts cycledeps ni = ni diff --git a/compiler/lib/src/InterfaceFiles.hs b/compiler/lib/src/InterfaceFiles.hs index 61fa5fe27..5f5e0f49b 100644 --- a/compiler/lib/src/InterfaceFiles.hs +++ b/compiler/lib/src/InterfaceFiles.hs @@ -1096,7 +1096,7 @@ extensionIndexFromNameInfo :: A.ModName -> I.NModule -> ExtensionIndex extensionIndexFromNameInfo mn (I.NModule _ te _) = foldl addExt emptyExtensionIndex te where - addExt acc (ext, I.NExt _ c ps _ _ _) = + addExt acc (ext, I.NExt _ c ps _ _ _ _) = let cls = localQName (A.tcname c) protos = [ p | (_, pcon) <- ps, Just p <- [localQName (A.tcname pcon)] ] withClass = @@ -1254,8 +1254,8 @@ queryIndexes (I.NModule _ te _) = QueryIndexes (map fst pte) cons actors conattr conattrs = indexMap [ (a, n) | (n, i) <- pte, isCon i, a <- attrs i ] protoattrs = indexMap [ (a, n) | (n, i@I.NProto{}) <- pte, a <- attrs i ] descendants = indexMap [ (A.tcname c, n) | (n, i) <- pte, (_, c) <- ancestry i ] - extprotos = indexMap [ (A.tcname p, n) | (n, I.NExt _ _ ps _ _ _) <- pte, (_, p) <- ps ] - exttypes = indexMap [ (A.tcname c, n) | (n, I.NExt _ c _ _ _ _) <- pte ] + extprotos = indexMap [ (A.tcname p, n) | (n, I.NExt _ _ ps _ _ _ _) <- pte, (_, p) <- ps ] + exttypes = indexMap [ (A.tcname c, n) | (n, I.NExt _ c _ _ _ _ _) <- pte ] isCons I.NClass{} = True isCons I.NProto{} = True isCons I.NAct{} = True diff --git a/compiler/lib/test/ActonSpec.hs b/compiler/lib/test/ActonSpec.hs index b0a641264..9bb2d95dd 100644 --- a/compiler/lib/test/ActonSpec.hs +++ b/compiler/lib/test/ActonSpec.hs @@ -306,7 +306,7 @@ main = do , (actorName, I.NAct [] S.posNil S.kwdNil [(actorAttr, I.NVar S.tWild)] Nothing) , (protoName, I.NProto [] [] [(protoAttr, I.NVar S.tWild)] Nothing) , (subProtoName, I.NProto [] [([], protoTC)] [] Nothing) - , (extName, I.NExt [] clsTC [([], protoTC)] [] [] Nothing) + , (extName, I.NExt [] clsTC [([], protoTC)] [] [] [] Nothing) ] nmod = I.NModule [] iface Nothing tmod = S.Module mn [] Nothing [] @@ -578,6 +578,7 @@ main = do , (S.name "unboxed_field", I.NSig (S.tSchema [] depDType) S.NoDec Nothing) ] [] + [] Nothing infos = M.singleton hashTestName info expectedDeps = M.singleton hashTestName (Set.fromList [depA, depB, depC, depD, localDep]) diff --git a/test/regression_auto/witness_canonical_import/Build.act b/test/regression_auto/witness_canonical_import/Build.act new file mode 100644 index 000000000..f4d0eabee --- /dev/null +++ b/test/regression_auto/witness_canonical_import/Build.act @@ -0,0 +1,2 @@ +name = "witness_canonical_import" +fingerprint = 0xbebfbb5fe4bdc7e2 diff --git a/test/regression_auto/witness_canonical_import__bf/src/hashpt.act b/test/regression_auto/witness_canonical_import/src/hashpt.act similarity index 100% rename from test/regression_auto/witness_canonical_import__bf/src/hashpt.act rename to test/regression_auto/witness_canonical_import/src/hashpt.act diff --git a/test/regression_auto/witness_canonical_import__bf/src/points.act b/test/regression_auto/witness_canonical_import/src/points.act similarity index 100% rename from test/regression_auto/witness_canonical_import__bf/src/points.act rename to test/regression_auto/witness_canonical_import/src/points.act diff --git a/test/regression_auto/witness_canonical_import__bf/src/witness_canonical_import__bf.act b/test/regression_auto/witness_canonical_import/src/witness_canonical_import.act similarity index 61% rename from test/regression_auto/witness_canonical_import__bf/src/witness_canonical_import__bf.act rename to test/regression_auto/witness_canonical_import/src/witness_canonical_import.act index 212b3c5c9..35b7011de 100644 --- a/test/regression_auto/witness_canonical_import__bf/src/witness_canonical_import__bf.act +++ b/test/regression_auto/witness_canonical_import/src/witness_canonical_import.act @@ -1,8 +1,7 @@ -# There is exactly one Eq[Pt] implementation, in points. Yet declaring the -# Hashable extension makes every == involving Pt fail to resolve, here and -# inside hashpt itself: hashpt's extension registers a second Eq witness for -# Pt via its ancestry, and the solver requires a single candidate. This -# build failure documents the deficiency the next commit removes. +# There is exactly one Eq[Pt] implementation, in points. hashpt's Hashable +# extension no longer registers a witness for the finalized Eq, so == on Pt +# resolves to points' witness everywhere: inside hashpt and in this module, +# which imports both. import points import hashpt diff --git a/test/regression_auto/witness_canonical_import__bf/Build.act b/test/regression_auto/witness_canonical_import__bf/Build.act deleted file mode 100644 index 1f373f19e..000000000 --- a/test/regression_auto/witness_canonical_import__bf/Build.act +++ /dev/null @@ -1,2 +0,0 @@ -name = "witness_canonical_import__bf" -fingerprint = 0x333146d440f0f96c