Skip to content

Register no witness for finalized protocols #3045

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
plajjan wants to merge 2 commits into from
Closed

Register no witness for finalized protocols #3045

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b0b0c34
Pin cross-module witness resolution outcomes
Jul 28, 2026
839ce3e
Register no witness for finalized protocols
Jul 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion compiler/acton/test_incremental.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
2 changes: 1 addition & 1 deletion compiler/lib/src/Acton/Completion.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion compiler/lib/src/Acton/Converter.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ]
Expand Down
2 changes: 1 addition & 1 deletion compiler/lib/src/Acton/DocPrinter.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 5 additions & 5 deletions compiler/lib/src/Acton/Env.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 ++ " --- ")

Expand Down Expand Up @@ -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)
Expand Down
6 changes: 3 additions & 3 deletions compiler/lib/src/Acton/Hashing.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
26 changes: 13 additions & 13 deletions compiler/lib/src/Acton/NameInfo.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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)
Expand All @@ -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 = []
Expand All @@ -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
Expand All @@ -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 = []
Expand All @@ -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 _ = ([],[])

Expand All @@ -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 --------------------------------------------------------------------------------------------------------

Expand Down Expand Up @@ -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 -> []
Expand All @@ -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
Expand Down
4 changes: 4 additions & 0 deletions compiler/lib/src/Acton/Solver.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Expand Down
2 changes: 1 addition & 1 deletion compiler/lib/src/Acton/Syntax.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
4 changes: 2 additions & 2 deletions compiler/lib/src/Acton/TypeEnv.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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),
Expand Down Expand Up @@ -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
Expand Down
11 changes: 7 additions & 4 deletions compiler/lib/src/Acton/Types.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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)
Expand Down
4 changes: 2 additions & 2 deletions compiler/lib/src/Acton/WitKnots.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
Loading
Loading