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/src/hashpt.act b/test/regression_auto/witness_canonical_import/src/hashpt.act
new file mode 100644
index 000000000..1901c4de5
--- /dev/null
+++ b/test/regression_auto/witness_canonical_import/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/src/points.act b/test/regression_auto/witness_canonical_import/src/points.act
new file mode 100644
index 000000000..e1bccb900
--- /dev/null
+++ b/test/regression_auto/witness_canonical_import/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/src/witness_canonical_import.act b/test/regression_auto/witness_canonical_import/src/witness_canonical_import.act
new file mode 100644
index 000000000..35b7011de
--- /dev/null
+++ b/test/regression_auto/witness_canonical_import/src/witness_canonical_import.act
@@ -0,0 +1,22 @@
+# 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
+
+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)