From 387dbbca9887b221b47b424c8d44d800a6a9530a Mon Sep 17 00:00:00 2001
From: rodrigogribeiro <rodrigogribeiro@gmail.com>
Date: Thu, 12 Mar 2026 16:10:52 -0300
Subject: [PATCH 01/21] First iteration of named instances

---
 src/Solcore/Backend/Specialise.hs             |  56 ++++++--
 src/Solcore/Desugarer/ContractDispatch.hs     |   8 +-
 src/Solcore/Desugarer/DecisionTreeCompiler.hs |  10 +-
 src/Solcore/Desugarer/FieldAccess.hs          |  15 ++-
 src/Solcore/Desugarer/IfDesugarer.hs          |   4 +-
 src/Solcore/Desugarer/IndirectCall.hs         |  14 +-
 src/Solcore/Frontend/Lexer/SolcoreLexer.x     |   2 +
 src/Solcore/Frontend/Parser/SolcoreParser.y   |   9 +-
 src/Solcore/Frontend/Pretty/ShortName.hs      |   2 +-
 src/Solcore/Frontend/Pretty/SolcorePretty.hs  |  15 ++-
 src/Solcore/Frontend/Pretty/TreePretty.hs     |   9 +-
 src/Solcore/Frontend/Syntax/Contract.hs       |   1 +
 src/Solcore/Frontend/Syntax/NameResolution.hs |  68 ++++++----
 src/Solcore/Frontend/Syntax/Stmt.hs           |   3 +-
 src/Solcore/Frontend/Syntax/SyntaxTree.hs     |   4 +
 src/Solcore/Frontend/TypeInference/Erase.hs   |   8 +-
 .../Frontend/TypeInference/InvokeGen.hs       |   4 +-
 .../Frontend/TypeInference/SccAnalysis.hs     |   4 +-
 src/Solcore/Frontend/TypeInference/TcEnv.hs   |   2 +
 src/Solcore/Frontend/TypeInference/TcMonad.hs |   7 +
 src/Solcore/Frontend/TypeInference/TcStmt.hs  | 123 ++++++++++++------
 src/Solcore/Frontend/TypeInference/TcSubst.hs |  19 +--
 22 files changed, 267 insertions(+), 120 deletions(-)

diff --git a/src/Solcore/Backend/Specialise.hs b/src/Solcore/Backend/Specialise.hs
index 60cd88e9f..9eafa5cda 100644
--- a/src/Solcore/Backend/Specialise.hs
+++ b/src/Solcore/Backend/Specialise.hs
@@ -20,7 +20,7 @@ import Solcore.Frontend.Pretty.SolcorePretty
 import Solcore.Frontend.Syntax hiding (decls, name)
 import Solcore.Frontend.TypeInference.Id (Id (..))
 import Solcore.Frontend.TypeInference.NameSupply
-import Solcore.Frontend.TypeInference.TcEnv (TcEnv (typeTable), TypeInfo (..))
+import Solcore.Frontend.TypeInference.TcEnv (TcEnv (ctx, typeTable), TypeInfo (..))
 import Solcore.Frontend.TypeInference.TcUnify (typesDoNotUnify)
 import Solcore.Primitives.Primitives
 
@@ -218,7 +218,31 @@ addDeclResolutions (TMutualDef decls) = forM_ decls addDeclResolutions
 addDeclResolutions _ = return ()
 
 addInstResolutions :: Instance Id -> SM ()
-addInstResolutions inst = forM_ (instFunctions inst) (addMethodResolution (instName inst) (mainTy inst))
+addInstResolutions inst = forM_ (instFunctions inst) addMethod
+  where
+    addMethod fd = do
+      addMethodResolution (instName inst) (mainTy inst) fd
+      -- For named instances, also register under QualName lbl methodName
+      -- so that specExp can find the definition directly by label.
+      case instLabel inst of
+        Nothing  -> return ()
+        Just lbl -> addNamedInstMethodResolution lbl (mainTy inst) fd
+
+-- Register a named-instance method under QualName lbl methodUnqualName.
+-- After type inference, method names are QualName className method; we
+-- strip the class qualifier and substitute the instance label.
+addNamedInstMethodResolution :: Name -> Ty -> TcFunDef -> SM ()
+addNamedInstMethodResolution lbl ty fd = do
+  let sig      = funSignature fd
+      methUnq  = case sigName sig of
+                   QualName _ m -> m
+                   Name s       -> s
+      qname    = QualName lbl methUnq
+      name'    = specName qname [ty]
+      funType  = typeOfTcFunDef fd
+      fd'      = FunDef sig { sigName = name' } (funDefBody fd)
+  addResolution qname funType fd'
+  debug ["+ addNamedInstMethodResolution: ", show qname, " / ", show name', " : ", pretty funType]
 
 specialiseTopDecl :: TopDecl Id -> SM [TopDecl Id]
 specialiseTopDecl (TContr (Contract name args decls)) = withLocalState do
@@ -302,10 +326,15 @@ addMethodResolution cname ty fd = do
 
 -- | `specExp` specialises an expression to given type
 specExp :: TcExp -> Ty -> SM TcExp
-specExp (Call Nothing i args) ty = do
+specExp (Call Nothing i lbl args) ty = do
   -- debug ["> specExp (Call): ", pretty e, " : ", pretty (idType i), " ~> ", pretty ty]
-  (i', args') <- specCall i args ty
-  let e' = Call Nothing i' args'
+  -- For named instance calls, resolve via QualName lbl method so the
+  -- specialiser finds the definition registered under that label.
+  let i' = case lbl of
+              Just l  -> i { idName = QualName l (pretty (idName i)) }
+              Nothing -> i
+  (i'', args') <- specCall i' args ty
+  let e' = Call Nothing i'' Nothing args'
   -- debug ["< specExp (Call): ", pretty e']
   return e'
 specExp e@(Con i es) ty = do
@@ -366,14 +395,21 @@ specCall i args ty = do
       extSpSubst phi
       subst <- getSpSubst
       let ty'' = applytv subst fty
-      ensureClosed ty'' (Call Nothing i args) subst
+      ensureClosed ty'' (Call Nothing i Nothing args) subst
       name' <- specFunDef fd
       debug ["< specCall: ", pretty name', " : ", show ty'']
       args'' <- atCurrentSubst args'
       return (Id name' ty'', args'')
     Nothing -> do
-      void $ panics ["! specCall: no resolution found for ", show name, " : ", pretty funType]
-      return (i, args')
+      -- Primitives are in primCtx but have no resolution entry; treat as monomorphic.
+      primEnv <- gets (ctx . spGlobalEnv)
+      if Map.member name primEnv
+        then do
+          debug ["< specCall (primitive): ", show name]
+          return (i', args')
+        else do
+          void $ panics ["! specCall: no resolution found for ", show name, " : ", pretty funType]
+          return (i, args')
 
 -- | `specFunDef` specialises a function definition
 -- to the given type of the form `arg1Ty -> arg2Ty -> ... -> resultTy`
@@ -554,7 +590,7 @@ typeOfTcExp e@(Con i args) = go (idType i) args
     go _ _ = error $ "typeOfTcExp: " ++ show e
 typeOfTcExp (Lit (IntLit _)) = word
 typeOfTcExp (Lit (StrLit _)) = string
-typeOfTcExp expr@(Call Nothing i args) = applyTo args funTy
+typeOfTcExp expr@(Call Nothing i _ args) = applyTo args funTy
   where
     funTy = idType i
     applyTo [] ty = ty
@@ -848,7 +884,7 @@ toMastExp :: Exp Id -> MastExp
 toMastExp (Var i) = MastVar (toMastId i)
 toMastExp (Con i es) = MastCon (toMastId i) (map toMastExp es)
 toMastExp (Lit l) = MastLit l
-toMastExp (Call Nothing i es) = MastCall (toMastId i) (map toMastExp es)
+toMastExp (Call Nothing i _ es) = MastCall (toMastId i) (map toMastExp es)
 toMastExp (TyExp e _) = toMastExp e
 toMastExp (Cond e1 e2 e3) = MastCond (toMastExp e1) (toMastExp e2) (toMastExp e3)
 toMastExp e = error $ "toMastExp: unexpected " ++ show e
diff --git a/src/Solcore/Desugarer/ContractDispatch.hs b/src/Solcore/Desugarer/ContractDispatch.hs
index d1b30c8ac..e9aef7fbb 100644
--- a/src/Solcore/Desugarer/ContractDispatch.hs
+++ b/src/Solcore/Desugarer/ContractDispatch.hs
@@ -59,7 +59,7 @@ genMainFn addMain (Contract cname tys cdecls)
     cdecls' = Set.unions (map (transformCDecl cname) cdecls'')
     defaultConstructor = CConstrDecl (Constructor {constrParams = [], constrBody = []})
     mainfn = FunDef (Signature [] [] "main" [] Nothing) body
-    body = [StmtExp (Call Nothing (QualName "RunContract" "exec") [cdata])]
+    body = [StmtExp (Call Nothing (QualName "RunContract" "exec") Nothing [cdata])]
     cdata = Con "Contract" [methods, fallback]
     methods = tupleExpFromList (fmap mkMethod (mapMaybe unwrapSigs cdecls))
     fallback =
@@ -142,6 +142,7 @@ transformConstructor contractName cons
               := Call
                 Nothing
                 "abi_decode"
+                Nothing
                 [ Var "source",
                   proxyExp argsTuple,
                   proxyExp (TyCon "MemoryWordReader" [])
@@ -163,10 +164,10 @@ transformConstructor contractName cons
         }
     startBody =
       [ Asm [yulBlock|{ mstore(64, memoryguard(128)) }|],
-        Let "conargs" (Just argsTuple) (Just (Call Nothing "copy_arguments_for_constructor" [])),
+        Let "conargs" (Just argsTuple) (Just (Call Nothing "copy_arguments_for_constructor" Nothing [])),
         -- , Match [Var "conargs"] ...
         Let "fun" Nothing (Just (Var initFunName)),
-        StmtExp $ Call Nothing "fun" [Var "conargs"],
+        StmtExp $ Call Nothing "fun" Nothing [Var "conargs"],
         Asm
           [yulBlock|{
             let size := datasize(`yulContractName`)
@@ -195,6 +196,7 @@ mkNameInst (DataTy dname [] []) fname =
       body = [Return (Lit (StrLit (show fname)))]
    in Instance
         { instDefault = False,
+          instLabel = Nothing,
           instVars = [],
           instContext = [],
           instName = "SigString",
diff --git a/src/Solcore/Desugarer/DecisionTreeCompiler.hs b/src/Solcore/Desugarer/DecisionTreeCompiler.hs
index 54e2bdd81..0fbbfbd2f 100644
--- a/src/Solcore/Desugarer/DecisionTreeCompiler.hs
+++ b/src/Solcore/Desugarer/DecisionTreeCompiler.hs
@@ -258,8 +258,8 @@ instance Compile (Exp Id) where
     flip FieldAccess n <$> compile me
   compile l@(Lit _) =
     pure l
-  compile (Call me f es) =
-    Call <$> compile me <*> pure f <*> compile es
+  compile (Call me f lbl es) =
+    Call <$> compile me <*> pure f <*> pure lbl <*> compile es
   compile (Lam ps bd mt) =
     Lam ps <$> pushCtx ("lambda (" ++ intercalate ", " (map pretty ps) ++ ")") (compile bd) <*> pure mt
   compile (TyExp e t) =
@@ -270,8 +270,8 @@ instance Compile (Exp Id) where
     Indexed <$> compile e1 <*> compile e2
 
 instance Compile (Instance Id) where
-  compile (Instance d vs ps n ts t funs) =
-    Instance d vs ps n ts t
+  compile (Instance d lbl vs ps n ts t funs) =
+    Instance d lbl vs ps n ts t
       <$> pushCtx ("instance " ++ pretty t ++ " : " ++ pretty n) (compile funs)
 
 -- compiling a decision tree into a match
@@ -633,7 +633,7 @@ scrutineeType (Var i) = pure (idType i)
 scrutineeType (Con i _) = pure (snd (splitTy (idType i)))
 scrutineeType (Lit (IntLit _)) = pure word
 scrutineeType (Lit (StrLit _)) = pure string
-scrutineeType (Call _ i _) = pure (snd (splitTy (idType i)))
+scrutineeType (Call _ i _ _) = pure (snd (splitTy (idType i)))
 scrutineeType (Lam args _body (Just tb)) = pure (funtype (map typeOfParam args) tb)
 scrutineeType (Lam _ _ Nothing) =
   throwError
diff --git a/src/Solcore/Desugarer/FieldAccess.hs b/src/Solcore/Desugarer/FieldAccess.hs
index 3759e3a33..1f619cae1 100644
--- a/src/Solcore/Desugarer/FieldAccess.hs
+++ b/src/Solcore/Desugarer/FieldAccess.hs
@@ -84,6 +84,7 @@ extraTopDeclsForContractField cname (Field fname fty _minit) offset = [selDecl,
     sfInstance =
       Instance
         { instDefault = False,
+          instLabel = Nothing,
           instVars = [],
           instContext = [],
           instName = "CStructField",
@@ -180,7 +181,7 @@ transAssignment (Indexed arr idx) rhs cenv = do
   let lhs' = traces ["lhsIndex", pretty arr, pretty idx] $ lhsIndex arr idx' cenv
   let rhs' = traces ["transRhs", pretty rhs] $ transRhs rhs cenv
   let assignName = QualName (Name "Assign") "assign"
-  StmtExp $ Call Nothing assignName [lhs', rhs']
+  StmtExp $ Call Nothing assignName Nothing [lhs', rhs']
 transAssignment lhs rhs cenv =
   traces ["Other assignment:", pretty (lhs := rhs)] $
     (lhs := rhs')
@@ -204,7 +205,7 @@ transContractFieldAssignment field rhs = do
   let lhs' = lhsAccess fieldMap
   rhs' <- transRhs rhs
   let assignName = QualName (Name "Assign") "assign"
-  pure $ StmtExp $ Call Nothing assignName [lhs', rhs']
+  pure $ StmtExp $ Call Nothing assignName Nothing [lhs', rhs']
 
 transRhs :: (HasCallStack) => NmExp -> CEM NmExp
 transRhs expr@(FieldAccess Nothing x) cenv
@@ -221,7 +222,7 @@ transRhs expr@FieldAccess {} _ = notImplemented "transRhs" expr
 transRhs expr cenv = go expr cenv
   where
     go e@(Indexed arr idx) = \env -> let e' = rhsIndex arr idx env in traces ["transRhs", pretty e, "- rhsIndex ->", pretty e'] e' -- FIXME
-    go (Call me f as) = Call me f <$> mapM transRhs as
+    go (Call me f lbl as) = Call me f lbl <$> mapM transRhs as
     go (Lam ps b mty) = Lam ps <$> transBody b <*> pure mty
     go (TyExp e ty) = TyExp <$> transRhs e <*> pure ty
     go (Cond e1 e2 e3) = Cond <$> transRhs e1 <*> transRhs e2 <*> transRhs e3
@@ -242,13 +243,13 @@ indexAccess dir exp@(FieldAccess Nothing name) idx = traces ["iA FA: " ++ pretty
       arrProxy <- memberProxyFor name
       let arrRef = lhsAccess arrProxy
       idx' <- transRhs idx
-      pure $ Call Nothing (indexFun dir) [arrRef, idx']
+      pure $ Call Nothing (indexFun dir) Nothing [arrRef, idx']
     else notImplemented "indexAccess" exp
 indexAccess dir _exp@(Indexed arr1 idx1) idx2 = traces ["iA II:", pretty arr1, pretty idx1, pretty idx2] $ do
   idx2' <- traces ["transRhs", pretty idx2] $ transRhs idx2
   idx1' <- traces ["transRhs", pretty idx1] $ transRhs idx1
   arr' <- traces ["lhsIndex", pretty arr1, pretty idx1'] $ lhsIndex arr1 idx1'
-  pure $ Call Nothing (indexFun dir) [arr', idx2']
+  pure $ Call Nothing (indexFun dir) Nothing [arr', idx2']
 indexAccess _dir exp idx = notImplemented "indexAccess" (Indexed exp idx)
 
 lhsIndex, rhsIndex :: (HasCallStack) => NmExp -> NmExp -> CEM (Exp Name)
@@ -311,10 +312,10 @@ memberProxyFor field = do
   pure fieldMap
 
 lhsAccess :: Exp Name -> Exp Name
-lhsAccess e = Call Nothing (QualName "LVA" "acc") [e]
+lhsAccess e = Call Nothing (QualName "LVA" "acc") Nothing [e]
 
 rhsAccess :: Exp Name -> Exp Name
-rhsAccess e = Call Nothing (QualName "RVA" "acc") [e]
+rhsAccess e = Call Nothing (QualName "RVA" "acc") Nothing [e]
 
 notImplemented :: (HasCallStack, Pretty a) => String -> a -> b
 notImplemented funName a = error $ concat [funName, " not implemented yet for ", pretty a]
diff --git a/src/Solcore/Desugarer/IfDesugarer.hs b/src/Solcore/Desugarer/IfDesugarer.hs
index 758864b91..a34fb3d66 100644
--- a/src/Solcore/Desugarer/IfDesugarer.hs
+++ b/src/Solcore/Desugarer/IfDesugarer.hs
@@ -35,8 +35,8 @@ desugarBoolCons (Con c@(Id n _) es)
   | otherwise = Con c (map desugarBoolCons es)
 desugarBoolCons (FieldAccess me v) =
   FieldAccess (desugarBoolCons <$> me) v
-desugarBoolCons (Call me v es) =
-  Call (desugarBoolCons <$> me) v (map desugarBoolCons es)
+desugarBoolCons (Call me v lbl es) =
+  Call (desugarBoolCons <$> me) v lbl (map desugarBoolCons es)
 desugarBoolCons (Lam ps bdy ty) =
   Lam ps (everywhere (mkT desugarBoolCons) bdy) ty
 desugarBoolCons (Cond e1 e2 e3) = Cond (d e1) (d e2) (d e3) where d = desugarBoolCons
diff --git a/src/Solcore/Desugarer/IndirectCall.hs b/src/Solcore/Desugarer/IndirectCall.hs
index 87e1e3331..c0795c932 100644
--- a/src/Solcore/Desugarer/IndirectCall.hs
+++ b/src/Solcore/Desugarer/IndirectCall.hs
@@ -2,6 +2,7 @@ module Solcore.Desugarer.IndirectCall where
 
 import Control.Monad.State
 import Data.Map qualified as Map
+import Data.Maybe (isJust)
 import Solcore.Frontend.Pretty.SolcorePretty
 import Solcore.Frontend.Syntax
 import Solcore.Frontend.TypeInference.TcEnv (primCtx)
@@ -94,18 +95,19 @@ instance Desugar (Exp Name) where
     Lam ps <$> desugar bd <*> pure t
   desugar (TyExp e t) =
     flip TyExp t <$> desugar e
-  desugar (Call m n es) =
+  desugar (Call m n lbl es) =
     do
       m' <- desugar m
       es' <- desugar es
       b <- isDirectCall n
       let qn = QualName invokableName "invoke"
           args' = [Var n, indirectArgs es']
-      if b
+      -- Named instance calls (Just lbl) are always direct: no defunctionalization
+      if b || isJust lbl
         then
-          pure $ Call m' n es'
+          pure $ Call m' n lbl es'
         else
-          pure $ Call Nothing qn args'
+          pure $ Call Nothing qn Nothing args'
   desugar (Cond e1 e2 e3) =
     Cond <$> desugar e1 <*> desugar e2 <*> desugar e3
   desugar x = pure x
@@ -114,8 +116,8 @@ instance Desugar (Equation Name) where
   desugar (ps, ss) = (ps,) <$> desugar ss
 
 instance Desugar (Instance Name) where
-  desugar (Instance d vs ps n ts t fs) =
-    Instance d vs ps n ts t <$> desugar fs
+  desugar (Instance d lbl vs ps n ts t fs) =
+    Instance d lbl vs ps n ts t <$> desugar fs
 
 -- building indirect function call arguments
 
diff --git a/src/Solcore/Frontend/Lexer/SolcoreLexer.x b/src/Solcore/Frontend/Lexer/SolcoreLexer.x
index f20f6c4f6..b5589181d 100644
--- a/src/Solcore/Frontend/Lexer/SolcoreLexer.x
+++ b/src/Solcore/Frontend/Lexer/SolcoreLexer.x
@@ -101,6 +101,7 @@ tokens :-
         <0>    "+="                              {simpleToken TPlusEq}
         <0>    "-="                              {simpleToken TMinusEq}
         <0>    "then"                            {simpleToken TThen}
+        <0>    "@{"                              {simpleToken TAtBrace}
         <0>    "@"                               {simpleToken TAt}
         <0>    @identifier                       {mkIdent}
         <0>    @number                           {mkNumber}
@@ -233,6 +234,7 @@ data Lexeme
   | TBar
   | TThen
   | TAt
+  | TAtBrace
   | TEOF
   deriving (Eq, Ord, Show)
 
diff --git a/src/Solcore/Frontend/Parser/SolcoreParser.y b/src/Solcore/Frontend/Parser/SolcoreParser.y
index df9ba397f..dc66cb62e 100644
--- a/src/Solcore/Frontend/Parser/SolcoreParser.y
+++ b/src/Solcore/Frontend/Parser/SolcoreParser.y
@@ -86,6 +86,7 @@ import Language.Yul
       '-='       {Token _ TMinusEq}
       'then'     {Token _ TThen}
       '@'        {Token _ TAt}
+      '@{'       {Token _ TAtBrace}
 
 %nonassoc '+=' '-='
 %left     ':'
@@ -324,8 +325,12 @@ Param : Name ':' Type                              {Typed $1 $3}
 
 -- instance declarations
 
+InstLabel :: { Maybe Name }
+InstLabel : '[' identifier ']'            { Just (Name $2) }
+          | {- empty -}                   { Nothing }
+
 InstDef :: { Instance }
-InstDef : SigPrefix DefaultOpt 'instance' Type ':' Name OptTypeParam InstBody { Instance $2 (fst $1) (snd $1) $6 $7 $4 $8 }
+InstDef : SigPrefix DefaultOpt 'instance' InstLabel Type ':' Name OptTypeParam InstBody { Instance $2 $4 (fst $1) (snd $1) $7 $8 $5 $9 }
 
 DefaultOpt :: { Bool }
 DefaultOpt : 'default'                        {True}
@@ -431,6 +436,8 @@ Expr : Name FunArgs                                {ExpName Nothing $1 $2}
      | '!' Expr                                    {ExpLNot $2 }
      | Conditional                                 {$1}
      | '@' Type                                    {ExpAt $2}
+     | Name '@{' identifier '}' '(' ExprCommaList ')' { ExpNameAt Nothing $1 (Name $3) $6 }
+     | Expr '.' Name '@{' identifier '}' '(' ExprCommaList ')' { ExpNameAt (Just $1) $3 (Name $5) $8 }
 
 Conditional :: { Exp }
 Conditional : 'if' Expr 'then' Expr 'else' Expr    {ExpCond $2 $4 $6}
diff --git a/src/Solcore/Frontend/Pretty/ShortName.hs b/src/Solcore/Frontend/Pretty/ShortName.hs
index 46c24d6aa..10ffcd202 100644
--- a/src/Solcore/Frontend/Pretty/ShortName.hs
+++ b/src/Solcore/Frontend/Pretty/ShortName.hs
@@ -28,7 +28,7 @@ instance (HasShortName a) => HasShortName (FunDef a) where
   shortName fd = "function " ++ shortName (funSignature fd)
 
 instance (HasShortName a) => HasShortName (Instance a) where
-  shortName (Instance _d _vs _ctx n ts t _funs) = do
+  shortName (Instance _d _ _vs _ctx n ts t _funs) = do
     unwords ["instance", pretty (InCls n t ts)]
 
 instance HasShortName Pred where
diff --git a/src/Solcore/Frontend/Pretty/SolcorePretty.hs b/src/Solcore/Frontend/Pretty/SolcorePretty.hs
index 410c46ed5..ff53993b3 100644
--- a/src/Solcore/Frontend/Pretty/SolcorePretty.hs
+++ b/src/Solcore/Frontend/Pretty/SolcorePretty.hs
@@ -230,10 +230,11 @@ pprSigPrefix vs ps =
   text "forall" <+> hsep (map ppr vs) <+> text "." $$ pprContext ps
 
 instance (Pretty a) => Pretty (Instance a) where
-  ppr (Instance d vs ctx n tys ty funs) =
+  ppr (Instance d lbl vs ctx n tys ty funs) =
     pprSigPrefix vs ctx
       <+> pprDefault d
       <> text "instance"
+      <+> pprInstLabel lbl
       <+> ppr ty
       <+> colon
       <+> ppr n
@@ -242,6 +243,10 @@ instance (Pretty a) => Pretty (Instance a) where
       $$ nest 3 (pprFunBlock funs)
       $$ rbrace
 
+pprInstLabel :: Maybe Name -> Doc
+pprInstLabel Nothing    = empty
+pprInstLabel (Just lbl) = text "[" <> ppr lbl <> text "]"
+
 pprDefault :: Bool -> Doc
 pprDefault b = if b then text "default " else empty
 
@@ -355,8 +360,8 @@ instance (Pretty a) => Pretty (Exp a) where
             then empty
             else (parens (nest 1 $ commaSep $ map ppr es))
   ppr (Lit l) = ppr l
-  ppr (Call e n es) =
-    pprE e <> ppr n <> (parens (nest 1 $ commaSep $ map ppr es))
+  ppr (Call e n lbl es) =
+    pprE e <> ppr n <> pprCallLabel lbl <> (parens (nest 1 $ commaSep $ map ppr es))
   ppr (Lam args bd _) =
     text "lam"
       <+> pprParams args
@@ -375,6 +380,10 @@ pprE :: (Pretty a) => Maybe (Exp a) -> Doc
 pprE Nothing = ""
 pprE (Just e) = ppr e <> text "."
 
+pprCallLabel :: Maybe Name -> Doc
+pprCallLabel Nothing    = empty
+pprCallLabel (Just lbl) = text "@{" <> ppr lbl <> text "}"
+
 instance (Pretty a) => Pretty (Pat a) where
   ppr (PVar n) =
     ppr n
diff --git a/src/Solcore/Frontend/Pretty/TreePretty.hs b/src/Solcore/Frontend/Pretty/TreePretty.hs
index 2072f8cb9..08a798a0a 100644
--- a/src/Solcore/Frontend/Pretty/TreePretty.hs
+++ b/src/Solcore/Frontend/Pretty/TreePretty.hs
@@ -206,7 +206,7 @@ pprSigPrefix vs ps =
   text "forall" <+> hsep (map ppr vs) <+> text "." $$ pprContext ps
 
 instance Pretty Instance where
-  ppr (Instance d vs ctx n tys ty funs) =
+  ppr (Instance d _ vs ctx n tys ty funs) =
     pprSigPrefix vs ctx
       <+> pprDefault d
       <+> text "instance"
@@ -332,6 +332,13 @@ instance Pretty Exp where
       <> parensWhen
         (not $ null es)
         (commaSep (map ppr es))
+  ppr (ExpNameAt me n lbl es) =
+    maybe empty (\e -> ppr e <> char '.') me
+      <> ppr n
+      <> text "@{"
+      <> ppr lbl
+      <> char '}'
+      <> parens (commaSep (map ppr es))
   ppr (ExpVar me v) =
     maybe empty (\e -> ppr e <> char '.') me
       <> ppr v
diff --git a/src/Solcore/Frontend/Syntax/Contract.hs b/src/Solcore/Frontend/Syntax/Contract.hs
index 2694c09f3..d10533d7a 100644
--- a/src/Solcore/Frontend/Syntax/Contract.hs
+++ b/src/Solcore/Frontend/Syntax/Contract.hs
@@ -170,6 +170,7 @@ data Signature a
 data Instance a
   = Instance
   { instDefault :: Bool,
+    instLabel :: Maybe Name,
     instVars :: [Tyvar],
     instContext :: [Pred],
     instName :: Name,
diff --git a/src/Solcore/Frontend/Syntax/NameResolution.hs b/src/Solcore/Frontend/Syntax/NameResolution.hs
index 8afda18ee..ddfe11f64 100644
--- a/src/Solcore/Frontend/Syntax/NameResolution.hs
+++ b/src/Solcore/Frontend/Syntax/NameResolution.hs
@@ -274,7 +274,7 @@ instance Resolve S.Signature where
 instance Resolve S.Instance where
   type Result S.Instance = Instance Name
 
-  resolve i@(S.Instance d vs ps n ts t funs) =
+  resolve i@(S.Instance d lbl vs ps n ts t funs) =
     withLocalCtx $ do
       let ns = map tyconName vs
       ndt <- lookupClass n
@@ -286,7 +286,7 @@ instance Resolve S.Instance where
           t' <- resolve t `wrapError` i
           funs' <- resolve funs `wrapError` i
           let vs' = map TVar ns
-          pure (Instance d vs' ps' n ts' t' funs')
+          pure (Instance d lbl vs' ps' n ts' t' funs')
         _ -> undefinedClassError n
 
 instance Resolve S.Param where
@@ -584,7 +584,7 @@ instance Resolve S.Exp where
       case (me', dt) of
         -- normal function call
         (Nothing, Just TFunction) ->
-          pure (Call Nothing n es')
+          pure (Call Nothing n Nothing es')
         (Nothing, Just TTyCon) -> do
           sameName <- isSameNameConstructor n
           if sameName
@@ -604,7 +604,7 @@ instance Resolve S.Exp where
           let qn = QualName c (pretty n)
           qdt <- lookupName qn
           case qdt of
-            Just TFunction -> pure (Call Nothing qn es')
+            Just TFunction -> pure (Call Nothing qn Nothing es')
             Just TDataCon -> Con <$> resolveQualifiedConstructorName c n <*> pure es'
             _ -> undefinedName n
         -- class functions
@@ -613,11 +613,11 @@ instance Resolve S.Exp where
           let qn = QualName c (pretty n)
           case ct of
             Just TClass ->
-              pure (Call Nothing qn es')
+              pure (Call Nothing qn Nothing es')
             Just TModule -> do
               cf <- lookupName qn
               case cf of
-                Just TFunction -> pure (Call Nothing qn es')
+                Just TFunction -> pure (Call Nothing qn Nothing es')
                 Just TDataCon -> Con <$> resolveQualifiedConstructorName c n <*> pure es'
                 _ -> undefinedName n
             _ -> undefinedName c
@@ -627,9 +627,9 @@ instance Resolve S.Exp where
           cf <- lookupName qn
           case (ct, cf) of
             (Just TClass, Just TFunction) ->
-              pure (Call Nothing qn es')
+              pure (Call Nothing qn Nothing es')
             (_, Just TFunction) ->
-              pure (Call Nothing qn es')
+              pure (Call Nothing qn Nothing es')
             (_, Just TDataCon) ->
               Con <$> resolveQualifiedConstructorName c n <*> pure es'
             _ -> do
@@ -643,13 +643,13 @@ instance Resolve S.Exp where
           let qn = QualName c (pretty n)
           cf <- gets (Map.lookup qn . scopeEnv)
           case cf of
-            Just TFunction -> pure (Call Nothing qn es')
+            Just TFunction -> pure (Call Nothing qn Nothing es')
             _ -> undefinedName n
         -- variables
         (_, Just TLocalVar) ->
-          pure (Call Nothing n es')
+          pure (Call Nothing n Nothing es')
         (_, Just TParameter) ->
-          pure (Call Nothing n es')
+          pure (Call Nothing n Nothing es')
         -- error
         _ -> do
           sameName <- isSameNameConstructor n
@@ -665,31 +665,31 @@ instance Resolve S.Exp where
       e1' <- resolve e1 `wrapError` c
       e2' <- resolve e2 `wrapError` c
       let fun = QualName (Name "Add") "add"
-      pure $ Call Nothing fun [e1', e2']
+      pure $ Call Nothing fun Nothing [e1', e2']
   resolve c@(S.ExpMinus e1 e2) =
     do
       e1' <- resolve e1 `wrapError` c
       e2' <- resolve e2 `wrapError` c
       let fun = QualName (Name "Sub") "sub"
-      pure $ Call Nothing fun [e1', e2']
+      pure $ Call Nothing fun Nothing [e1', e2']
   resolve c@(S.ExpTimes e1 e2) =
     do
       e1' <- resolve e1 `wrapError` c
       e2' <- resolve e2 `wrapError` c
       let fun = QualName (Name "Mul") "mul"
-      pure $ Call Nothing fun [e1', e2']
+      pure $ Call Nothing fun Nothing [e1', e2']
   resolve c@(S.ExpDivide e1 e2) =
     do
       e1' <- resolve e1 `wrapError` c
       e2' <- resolve e2 `wrapError` c
       let fun = QualName (Name "Div") "div"
-      pure $ Call Nothing fun [e1', e2']
+      pure $ Call Nothing fun Nothing [e1', e2']
   resolve c@(S.ExpModulo e1 e2) =
     do
       e1' <- resolve e1 `wrapError` c
       e2' <- resolve e2 `wrapError` c
       let fun = QualName (Name "Mod") "mod"
-      pure $ Call Nothing fun [e1', e2']
+      pure $ Call Nothing fun Nothing [e1', e2']
   resolve c@(S.ExpIndexed array idx) = do
     arr' <- resolve array `wrapError` c
     idx' <- resolve idx `wrapError` c
@@ -697,40 +697,40 @@ instance Resolve S.Exp where
   resolve c@(S.ExpLT e1 e2) = do
     e1' <- resolve e1 `wrapError` c
     e2' <- resolve e2 `wrapError` c
-    pure $ Call Nothing (Name "lt") [e1', e2']
+    pure $ Call Nothing (Name "lt") Nothing [e1', e2']
   resolve c@(S.ExpGT e1 e2) = do
     e1' <- resolve e1 `wrapError` c
     e2' <- resolve e2 `wrapError` c
     let fun = QualName (Name "Ord") "gt"
-    pure $ Call Nothing fun [e1', e2']
+    pure $ Call Nothing fun Nothing [e1', e2']
   resolve c@(S.ExpLE e1 e2) = do
     e1' <- resolve e1 `wrapError` c
     e2' <- resolve e2 `wrapError` c
-    pure $ Call Nothing (Name "le") [e1', e2']
+    pure $ Call Nothing (Name "le") Nothing [e1', e2']
   resolve c@(S.ExpGE e1 e2) = do
     e1' <- resolve e1 `wrapError` c
     e2' <- resolve e2 `wrapError` c
-    pure $ Call Nothing (Name "ge") [e1', e2']
+    pure $ Call Nothing (Name "ge") Nothing [e1', e2']
   resolve c@(S.ExpEE e1 e2) = do
     e1' <- resolve e1 `wrapError` c
     e2' <- resolve e2 `wrapError` c
     let fun = QualName (Name "Eq") "eq"
-    pure $ Call Nothing fun [e1', e2']
+    pure $ Call Nothing fun Nothing [e1', e2']
   resolve c@(S.ExpNE e1 e2) = do
     e1' <- resolve e1 `wrapError` c
     e2' <- resolve e2 `wrapError` c
-    pure $ Call Nothing (Name "ne") [e1', e2']
+    pure $ Call Nothing (Name "ne") Nothing [e1', e2']
   resolve c@(S.ExpLAnd e1 e2) = do
     e1' <- resolve e1 `wrapError` c
     e2' <- resolve e2 `wrapError` c
-    pure $ Call Nothing (Name "and") [e1', e2']
+    pure $ Call Nothing (Name "and") Nothing [e1', e2']
   resolve c@(S.ExpLOr e1 e2) = do
     e1' <- resolve e1 `wrapError` c
     e2' <- resolve e2 `wrapError` c
-    pure $ Call Nothing (Name "or") [e1', e2']
+    pure $ Call Nothing (Name "or") Nothing [e1', e2']
   resolve c@(S.ExpLNot e) = do
     e' <- resolve e `wrapError` c
-    pure $ Call Nothing (Name "not") [e']
+    pure $ Call Nothing (Name "not") Nothing [e']
   resolve (S.ExpCond e1 e2 e3) =
     Cond <$> resolve e1 <*> resolve e2 <*> resolve e3
   resolve (S.ExpAt t) = do
@@ -740,6 +740,16 @@ instance Resolve S.Exp where
           (Con (Name "Proxy") [])
           (TyCon (Name "Proxy") [t'])
       )
+  resolve x@(S.ExpNameAt me n lbl es) = do
+    me' <- resolve me `wrapError` x
+    es' <- resolve es `wrapError` x
+    let qn = QualName lbl (pretty n)
+    dt <- lookupName qn
+    case dt of
+      Just TFunction -> pure (Call me' n (Just lbl) es')
+      _ -> throwError $
+        "Unknown named instance label '" ++ pretty lbl
+        ++ "' for method '" ++ pretty n ++ "'"
 
 instance Resolve S.Literal where
   type Result S.Literal = Literal
@@ -929,6 +939,14 @@ addTopDecl (S.TSym (S.TySym n _ _)) env =
   addQualifiedModules n $
     env {typeEnv = Map.insert n TTyCon (typeEnv env)}
 addTopDecl (S.TExportDecl _) env = env
+addTopDecl (S.TInstDef (S.Instance _ (Just lbl) _ _ _ _ _ funs)) env =
+  env { scopeEnv =
+          foldr (\fd ac ->
+                   let qn = QualName lbl (pretty (S.sigName (S.funSignature fd)))
+                   in Map.insert qn TFunction ac)
+                (scopeEnv env)
+                funs
+      }
 addTopDecl _ env = env
 
 addModuleName :: Name -> Env -> Env
diff --git a/src/Solcore/Frontend/Syntax/Stmt.hs b/src/Solcore/Frontend/Syntax/Stmt.hs
index e8ee9e00a..660962557 100644
--- a/src/Solcore/Frontend/Syntax/Stmt.hs
+++ b/src/Solcore/Frontend/Syntax/Stmt.hs
@@ -2,6 +2,7 @@ module Solcore.Frontend.Syntax.Stmt where
 
 import Data.Generics (Data, Typeable)
 import Language.Yul
+import Solcore.Frontend.Syntax.Name
 import Solcore.Frontend.Syntax.Ty
 
 -- definition of statements
@@ -38,7 +39,7 @@ data Exp a
   | Con a [Exp a] -- data type constructor
   | FieldAccess (Maybe (Exp a)) a -- field access
   | Lit Literal -- literal
-  | Call (Maybe (Exp a)) a [Exp a] -- function call
+  | Call (Maybe (Exp a)) a (Maybe Name) [Exp a] -- function call (third arg = instance label)
   | Lam [Param a] (Body a) (Maybe Ty) -- lambda-abstraction
   | TyExp (Exp a) Ty -- type annotated expression
   | Cond (Exp a) (Exp a) (Exp a) -- conditional expression
diff --git a/src/Solcore/Frontend/Syntax/SyntaxTree.hs b/src/Solcore/Frontend/Syntax/SyntaxTree.hs
index c01e9093c..9a931830e 100644
--- a/src/Solcore/Frontend/Syntax/SyntaxTree.hs
+++ b/src/Solcore/Frontend/Syntax/SyntaxTree.hs
@@ -193,6 +193,7 @@ data Signature
 data Instance
   = Instance
   { instDefault :: Bool,
+    instLabel :: Maybe Name,
     instVars :: [Ty],
     instContext :: [Pred],
     instName :: Name,
@@ -279,6 +280,9 @@ data Exp
   | ExpLNot Exp -- ! e
   | ExpCond Exp Exp Exp -- if e1 then e2 else e3
   | ExpAt Ty -- proxy sugar
+  | ExpNameAt (Maybe Exp) Name Name [Exp]
+    -- ^ ExpNameAt receiver methodName instanceLabel args
+    --   Represents receiver.method@{label}(args) or method@{label}(args)
   deriving (Eq, Ord, Show, Data, Typeable)
 
 -- pattern matching equations
diff --git a/src/Solcore/Frontend/TypeInference/Erase.hs b/src/Solcore/Frontend/TypeInference/Erase.hs
index bb003ae51..4e6799a17 100644
--- a/src/Solcore/Frontend/TypeInference/Erase.hs
+++ b/src/Solcore/Frontend/TypeInference/Erase.hs
@@ -25,8 +25,8 @@ instance (Erase a, Erase b) => Erase (a, b) where
 instance Erase (Instance Id) where
   type EraseRes (Instance Id) = Instance Name
 
-  erase (Instance d vs ctx n ts t funs) =
-    Instance d vs ctx n ts t (erase funs)
+  erase (Instance d lbl vs ctx n ts t funs) =
+    Instance d lbl vs ctx n ts t (erase funs)
 
 instance Erase (FunDef Id) where
   type EraseRes (FunDef Id) = FunDef Name
@@ -67,8 +67,8 @@ instance Erase (Exp Id) where
     Con (idName n) (map erase es)
   erase (FieldAccess me n) =
     FieldAccess (erase me) (idName n)
-  erase (Call me n es) =
-    Call (erase me) (idName n) (erase es)
+  erase (Call me n lbl es) =
+    Call (erase me) (idName n) lbl (erase es)
   erase (Lam ps bd mt) =
     Lam (erase ps) (erase bd) mt
   erase (TyExp e t) =
diff --git a/src/Solcore/Frontend/TypeInference/InvokeGen.hs b/src/Solcore/Frontend/TypeInference/InvokeGen.hs
index c4083dd20..31842b701 100644
--- a/src/Solcore/Frontend/TypeInference/InvokeGen.hs
+++ b/src/Solcore/Frontend/TypeInference/InvokeGen.hs
@@ -65,11 +65,11 @@ createInstance udt fd sch =
         discr = epair (Var sn) (Var an)
         fname = sigName (funSignature fd)
         ssargs = take (length args) (svs ++ sarg)
-        scall = Return (Call Nothing fname ssargs)
+        scall = Return (Call Nothing fname Nothing ssargs)
         bdy = Match [discr] [([foldr1 ppair (spvs : sargs)], [scall])]
         ifd = FunDef isig [bdy]
         vs' = bv qs `union` bv [tupleArgTy, returnTy, selfTy] `union` bv ifd
-        instd = Instance False vs' qs invokableName [tupleArgTy, returnTy] selfTy [ifd]
+        instd = Instance False Nothing vs' qs invokableName [tupleArgTy, returnTy] selfTy [ifd]
     info [">> Generated invokable instance:\n", pretty instd]
     pure instd
 
diff --git a/src/Solcore/Frontend/TypeInference/SccAnalysis.hs b/src/Solcore/Frontend/TypeInference/SccAnalysis.hs
index b7088fdca..7cd4bae9c 100644
--- a/src/Solcore/Frontend/TypeInference/SccAnalysis.hs
+++ b/src/Solcore/Frontend/TypeInference/SccAnalysis.hs
@@ -159,7 +159,7 @@ instance (Names a, Names b, Names c) => Names (a, b, c) where
 instance Names (Exp Name) where
   names (Con n es) = n : names es
   names (FieldAccess me n) = n : names me
-  names (Call me n es) =
+  names (Call me n _ es) =
     n : names me `union` names es
   names (Lam ps bdy mt) = names (ps, bdy, mt)
   names (TyExp e t) = names e `union` names t
@@ -208,7 +208,7 @@ instance Names (Class Name) where
     names ctx `union` names sigs
 
 instance Names (Instance Name) where
-  names (Instance _ _ ctx n ts t funs) =
+  names (Instance _ _ _ ctx n ts t funs) =
     [n] `union` names ctx `union` names (t : ts) `union` names funs
 
 instance Names Ty where
diff --git a/src/Solcore/Frontend/TypeInference/TcEnv.hs b/src/Solcore/Frontend/TypeInference/TcEnv.hs
index a2ad6d721..416c80260 100644
--- a/src/Solcore/Frontend/TypeInference/TcEnv.hs
+++ b/src/Solcore/Frontend/TypeInference/TcEnv.hs
@@ -93,6 +93,7 @@ data TcEnv
   { ctx :: Env, -- Variable environment
     instEnv :: InstTable, -- Instance Environment
     defaultEnv :: DefTable, -- Default instance environment
+    namedInstEnv :: Map Name (Instance Name), -- Named instance environment (by label)
     typeTable :: TypeTable, -- Type information environment
     synTable :: SynTable, -- Type synonym environment
     classTable :: ClassTable, -- Class information table
@@ -125,6 +126,7 @@ initTcEnv opts =
     { ctx = primCtx,
       instEnv = primInstEnv,
       defaultEnv = Map.empty,
+      namedInstEnv = Map.empty,
       typeTable = primTypeEnv,
       synTable = Map.empty,
       classTable = primClassEnv,
diff --git a/src/Solcore/Frontend/TypeInference/TcMonad.hs b/src/Solcore/Frontend/TypeInference/TcMonad.hs
index e44176cbe..d1cf70daa 100644
--- a/src/Solcore/Frontend/TypeInference/TcMonad.hs
+++ b/src/Solcore/Frontend/TypeInference/TcMonad.hs
@@ -549,6 +549,13 @@ addDefaultInstance n inst =
           st {defaultEnv = Map.insert n inst (defaultEnv st)}
       )
 
+addNamedInstance :: Name -> Instance Name -> TcM ()
+addNamedInstance label inst =
+  modify (\st -> st { namedInstEnv = Map.insert label inst (namedInstEnv st) })
+
+askNamedInstance :: Name -> TcM (Maybe (Instance Name))
+askNamedInstance label = Map.lookup label <$> gets namedInstEnv
+
 maybeToTcM :: String -> Maybe a -> TcM a
 maybeToTcM s Nothing = throwError s
 maybeToTcM _ (Just x) = pure x
diff --git a/src/Solcore/Frontend/TypeInference/TcStmt.hs b/src/Solcore/Frontend/TypeInference/TcStmt.hs
index 9a61ac6aa..7c78834c3 100644
--- a/src/Solcore/Frontend/TypeInference/TcStmt.hs
+++ b/src/Solcore/Frontend/TypeInference/TcStmt.hs
@@ -317,8 +317,10 @@ tcExpWithExpected _ (FieldAccess (Just e) n) =
     s <- askField tn n
     (ps' :=> t') <- freshInst s
     withCurrentSubst (FieldAccess (Just e') (Id n t'), ps ++ ps', t')
-tcExpWithExpected _ ex@(Call me n args) =
+tcExpWithExpected _ ex@(Call me n Nothing args) =
   tcCall me n args `wrapError` ex
+tcExpWithExpected _ ex@(Call me n (Just lbl) args) =
+  tcCallNamed me n lbl args `wrapError` ex
 tcExpWithExpected _ (Lam args bd _) =
   do
     (args', schs, ts') <- tcArgs args
@@ -853,14 +855,14 @@ extSignature sig@(Signature _ _ n _ _) =
 -- typing instance
 
 tcInstance :: Instance Name -> TcM (Instance Id)
-tcInstance idecl@(Instance d vs predCtx n ts t funs) =
+tcInstance idecl@(Instance d lbl vs predCtx n ts t funs) =
   do
     -- checking instance type parameters
     t' <- kindCheck t `wrapError` idecl
     ts' <- mapM kindCheck ts `wrapError` idecl
     -- checking constraints
     qs' <- mapM checkConstraint predCtx `wrapError` idecl
-    tcInstance' (Instance d vs qs' n ts' t' funs)
+    tcInstance' (Instance d lbl vs qs' n ts' t' funs)
 
 checkConstraint :: Pred -> TcM Pred
 checkConstraint p@(InCls n t ts) =
@@ -875,12 +877,12 @@ checkConstraint (t :~: t') =
   (:~:) <$> kindCheck t <*> kindCheck t'
 
 tcInstance' :: Instance Name -> TcM (Instance Id)
-tcInstance' idecl@(Instance d vs predCtx n ts t funs) =
+tcInstance' idecl@(Instance d lbl vs predCtx n ts t funs) =
   do
     checkCompleteInstDef n (map (sigName . funSignature) funs) `wrapError` idecl
     (funs1, _) <- unzip <$> mapM (tcFunDef False vs predCtx) funs `wrapError` idecl
-    instd <- withCurrentSubst (Instance d vs predCtx n ts t funs1)
-    let ind@(Instance _ _ ctx' _ ts' t' funs2) = everywhere (mkT gen) instd
+    instd <- withCurrentSubst (Instance d lbl vs predCtx n ts t funs1)
+    let ind@(Instance _ _ _ ctx' _ ts' t' funs2) = everywhere (mkT gen) instd
         vs1 = bv ind
         funs3 =
           sortBy
@@ -890,10 +892,10 @@ tcInstance' idecl@(Instance d vs predCtx n ts t funs) =
                   (sigName (funSignature f'))
             )
             (map (updateSignature vs1 n) funs2)
-    verifySignatures (Instance d vs1 ctx' n ts' t' funs3)
+    verifySignatures (Instance d lbl vs1 ctx' n ts' t' funs3)
 
 verifySignatures :: Instance Id -> TcM (Instance Id)
-verifySignatures instd@(Instance _ _ ps n ts t funs) =
+verifySignatures instd@(Instance _ _ _ ps n ts t funs) =
   do
     -- get class info
     mcinfo <- Map.lookup n <$> gets classTable
@@ -1040,7 +1042,7 @@ checkConstraints :: [Pred] -> TcM ()
 checkConstraints = mapM_ checkConstraint
 
 checkInstance :: Instance Name -> TcM ()
-checkInstance idef@(Instance d vs predCtx n ts t funs) =
+checkInstance idef@(Instance d lbl vs predCtx n ts t funs) =
   do
     trustedImported <- isTrustedImportedInstance idef
     -- checking if all variables are declared
@@ -1058,31 +1060,38 @@ checkInstance idef@(Instance d vs predCtx n ts t funs) =
     tsExp <- mapM maybeExpandSynonym ts
     predCtxExp <- mapM expandPredSynonyms predCtx
     let ipred = InCls n tExp tsExp
-    -- checking the coverage condition
-    insts' <- askInstEnv n `wrapError` ipred
-    -- check overlapping only for non-default instances
-    let vs1 = bv ipred
-    ts1 <- mapM (const freshTyVar) vs1
-    let env = zip vs1 ts1
-        ipred' = insts env ipred
-    unless d (checkOverlap ipred' insts' `wrapError` idef)
-    -- check if default instance has a type variable as main argument.
-    when d (checkDefaultInst (predCtxExp :=> ipred) `wrapError` idef)
-    coverageEnabled <- askCoverage n
-    unless (trustedImported || coverageEnabled) (checkCoverage n tsExp tExp `wrapError` idef)
-    -- checking Patterson condition
-    pattersonEnabled <- askPattersonCondition n
-    unless (trustedImported || pattersonEnabled) (checkMeasure predCtxExp ipred `wrapError` idef)
-    -- checking bound variable condition
-    boundEnabled <- askBoundVariableCondition n
-    unless (trustedImported || boundEnabled) (checkBoundVariable predCtxExp (bv (tExp : tsExp)) `wrapError` idef)
-    -- checking instance methods
     mapM_ (checkMethod ipred) funs `wrapError` idef
     let ninst = anfInstance $ predCtxExp :=> ipred
-    -- add to the environment
-    if d
-      then addDefaultInstance n ninst
-      else addInstance n ninst
+    case lbl of
+      Nothing -> do
+        -- checking the coverage condition
+        insts' <- askInstEnv n `wrapError` ipred
+        -- check overlapping only for non-default instances
+        let vs1 = bv ipred
+        ts1 <- mapM (const freshTyVar) vs1
+        let env = zip vs1 ts1
+            ipred' = insts env ipred
+        unless d (checkOverlap ipred' insts' `wrapError` idef)
+        -- check if default instance has a type variable as main argument.
+        when d (checkDefaultInst (predCtxExp :=> ipred) `wrapError` idef)
+        coverageEnabled <- askCoverage n
+        unless (trustedImported || coverageEnabled) (checkCoverage n tsExp tExp `wrapError` idef)
+        -- checking Patterson condition
+        pattersonEnabled <- askPattersonCondition n
+        unless (trustedImported || pattersonEnabled) (checkMeasure predCtxExp ipred `wrapError` idef)
+        -- checking bound variable condition
+        boundEnabled <- askBoundVariableCondition n
+        unless (trustedImported || boundEnabled) (checkBoundVariable predCtxExp (bv (tExp : tsExp)) `wrapError` idef)
+        -- add to the environment
+        if d
+          then addDefaultInstance n ninst
+          else addInstance n ninst
+      Just label -> do
+        -- Named instances: skip overlap check, register by label
+        existing <- askNamedInstance label
+        unless (isNothing existing) $
+          throwError $ "Duplicate named instance label: " ++ pretty label
+        addNamedInstance label idef
 
 maybeExpandSynonym :: Ty -> TcM Ty
 maybeExpandSynonym (TyCon n ts) = do
@@ -1298,7 +1307,7 @@ tcBodyWithExpectedReturn mExpectedReturn (s : ss) =
 tcCall :: Maybe (Exp Name) -> Name -> [Exp Name] -> TcM (Exp Id, [Pred], Ty)
 tcCall Nothing n args =
   do
-    s <- askEnv n `wrapError` (Call Nothing n args)
+    s <- askEnv n `wrapError` (Call Nothing n Nothing args)
     (ps :=> t) <- freshInst s
     t' <- freshTyVar
     expectedArgTys <- mapM (const freshTyVar) args
@@ -1310,11 +1319,11 @@ tcCall Nothing n args =
     _ <- extSubst s1
     let ps' = foldr union [] (ps : pss')
         t1 = funtype ts' t'
-    withCurrentSubst (Call Nothing (Id n t1) es', ps', t')
+    withCurrentSubst (Call Nothing (Id n t1) Nothing es', ps', t')
 tcCall (Just e) n args =
   do
     (e', ps, _) <- tcExp e
-    s <- askEnv n `wrapError` (Call (Just e) n args)
+    s <- askEnv n `wrapError` (Call (Just e) n Nothing args)
     (ps1 :=> t) <- freshInst s
     t' <- freshTyVar
     expectedArgTys <- mapM (const freshTyVar) args
@@ -1325,7 +1334,45 @@ tcCall (Just e) n args =
     s' <- unify (foldr (:->) t' ts') t
     _ <- extSubst s'
     let ps' = foldr union [] ((ps ++ ps1) : pss')
-    withCurrentSubst (Call (Just e') (Id n t') es', ps', t')
+    withCurrentSubst (Call (Just e') (Id n t') Nothing es', ps', t')
+
+tcCallNamed :: Maybe (Exp Name) -> Name -> Name -> [Exp Name] -> TcM (Exp Id, [Pred], Ty)
+tcCallNamed me n lbl args =
+  do
+    let callExpr = Call me n (Just lbl) args
+    -- Look up the named instance by label
+    minst <- askNamedInstance lbl
+    inst <- maybe
+      (throwError $ "Unknown named instance label: " ++ pretty lbl)
+      pure
+      minst
+    -- Find the method in the instance's function definitions
+    let mfun = find (\fd -> sigName (funSignature fd) == n) (instFunctions inst)
+    fun <- maybe
+      (throwError $ unwords
+        ["Method", pretty n, "not found in named instance", pretty lbl])
+      pure
+      mfun
+    -- Build the type scheme from the method signature + instance context
+    let sig = funSignature fun
+        vs   = instVars inst ++ sigVars sig
+        preds = instContext inst ++ sigContext sig
+        argTys = [t | Typed _ t <- sigParams sig]
+    ret <- maybe
+      (throwError $ unwords
+        ["Method", pretty n, "in named instance", pretty lbl, "missing return type"])
+      pure
+      (sigReturn sig)
+    let scheme = Forall vs (preds :=> funtype argTys ret)
+    (ps :=> t) <- freshInst scheme
+    t' <- freshTyVar
+    me' <- mapM (\e -> (\(e', _, _) -> e') <$> tcExp e) me
+    (es', pss', ts') <- unzip3 <$> mapM tcExp args
+    s' <- unify t (funtype ts' t') `wrapError` callExpr
+    _ <- extSubst s'
+    let ps' = foldr union [] (ps : pss')
+        t1 = funtype ts' t'
+    withCurrentSubst (Call me' (Id n t1) (Just lbl) es', ps', t')
 
 tcParam :: Param Name -> TcM (Param Id)
 tcParam (Typed n t) =
@@ -1645,8 +1692,8 @@ instance Vars (Exp Id) where
   free (Con _ es) = free es
   free (FieldAccess Nothing _) = []
   free (FieldAccess (Just e) _) = free e
-  free (Call (Just e) n es) = free e `union` free n `union` free es
-  free (Call Nothing n es) = free n `union` free es
+  free (Call (Just e) n _ es) = free e `union` free n `union` free es
+  free (Call Nothing n _ es) = free n `union` free es
   free (Lam ps bd _) = free bd \\ bound ps
   free _ = []
 
diff --git a/src/Solcore/Frontend/TypeInference/TcSubst.hs b/src/Solcore/Frontend/TypeInference/TcSubst.hs
index 4037fb5a0..c1ce946dc 100644
--- a/src/Solcore/Frontend/TypeInference/TcSubst.hs
+++ b/src/Solcore/Frontend/TypeInference/TcSubst.hs
@@ -156,20 +156,21 @@ instance (HasType a) => HasType (FunDef a) where
     bv sig `union` bv bd
 
 instance (HasType a) => HasType (Instance a) where
-  apply s (Instance d vs ctx n ts t funs) =
+  apply s (Instance d lbl vs ctx n ts t funs) =
     Instance
       d
+      lbl
       vs
       (apply s ctx)
       n
       (apply s ts)
       (apply s t)
       (apply s funs)
-  fv (Instance _ _ ctx _ ts t _) =
+  fv (Instance _ _ _ ctx _ ts t _) =
     fv ctx `union` fv (t : ts)
-  mv (Instance _ _ ctx _ ts t _) =
+  mv (Instance _ _ _ ctx _ ts t _) =
     mv ctx `union` mv (t : ts)
-  bv (Instance _ vs ctx _ ts t _) =
+  bv (Instance _ _ vs ctx _ ts t _) =
     vs `union` bv ctx `union` bv (t : ts)
 
 instance (HasType a) => HasType (Exp a) where
@@ -178,8 +179,8 @@ instance (HasType a) => HasType (Exp a) where
     Con (apply s n) (apply s es)
   apply s (FieldAccess e v) =
     FieldAccess (apply s e) (apply s v)
-  apply s (Call m v es) =
-    Call (apply s <$> m) (apply s v) (apply s es)
+  apply s (Call m v lbl es) =
+    Call (apply s <$> m) (apply s v) lbl (apply s es)
   apply s (Lam ps bd mt) =
     Lam (apply s ps) (apply s bd) (apply s <$> mt)
   apply s (Cond e1 e2 e3) = Cond (apply s e1) (apply s e2) (apply s e3)
@@ -193,7 +194,7 @@ instance (HasType a) => HasType (Exp a) where
     fv n `union` fv es
   fv (FieldAccess e v) =
     fv e `union` fv v
-  fv (Call m v es) =
+  fv (Call m v _ es) =
     maybe [] fv m `union` fv v `union` fv es
   fv (Lam ps bd mt) =
     fv ps `union` fv bd `union` maybe [] fv mt
@@ -208,7 +209,7 @@ instance (HasType a) => HasType (Exp a) where
     mv n `union` mv es
   mv (FieldAccess e v) =
     mv e `union` mv v
-  mv (Call m v es) =
+  mv (Call m v _ es) =
     maybe [] mv m `union` mv v `union` mv es
   mv (Lam ps bd mt) =
     mv ps `union` mv bd `union` maybe [] mv mt
@@ -223,7 +224,7 @@ instance (HasType a) => HasType (Exp a) where
     bv n `union` bv es
   bv (FieldAccess e v) =
     bv e `union` bv v
-  bv (Call m v es) =
+  bv (Call m v _ es) =
     maybe [] bv m `union` bv v `union` bv es
   bv (Lam ps bd mt) =
     bv ps `union` bv bd `union` maybe [] bv mt

From 935858d49d9898b84d190d8caa6280d0ed5da6c7 Mon Sep 17 00:00:00 2001
From: rodrigogribeiro <rodrigogribeiro@gmail.com>
Date: Thu, 12 Mar 2026 16:11:07 -0300
Subject: [PATCH 02/21] Adding test cases for named instances

---
 test/Cases.hs                                 |  4 +++
 test/examples/cases/named-inst-basic.solc     | 31 ++++++++++++++++++
 test/examples/cases/named-inst-dup-label.solc | 25 +++++++++++++++
 .../cases/named-inst-two-instances.solc       | 32 +++++++++++++++++++
 .../cases/named-inst-unknown-label.solc       | 13 ++++++++
 5 files changed, 105 insertions(+)
 create mode 100644 test/examples/cases/named-inst-basic.solc
 create mode 100644 test/examples/cases/named-inst-dup-label.solc
 create mode 100644 test/examples/cases/named-inst-two-instances.solc
 create mode 100644 test/examples/cases/named-inst-unknown-label.solc

diff --git a/test/Cases.hs b/test/Cases.hs
index 06fea030c..f0128e7d2 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -400,6 +400,10 @@ cases =
       runTestForFile "redundant-match.solc" caseFolder,
       runTestForFile "false-redundant-warning.solc" caseFolder,
       runTestForFile "proxy-desugar.solc" caseFolder,
+      runTestForFile "named-inst-basic.solc" caseFolder,
+      runTestForFile "named-inst-two-instances.solc" caseFolder,
+      runTestExpectingFailure "named-inst-unknown-label.solc" caseFolder,
+      runTestExpectingFailure "named-inst-dup-label.solc" caseFolder,
       runTestForFile "invokable-issue.solc" caseFolder,
       runTestForFile "td.solc" caseFolder,
       runTestForFile "bar.solc" caseFolder,
diff --git a/test/examples/cases/named-inst-basic.solc b/test/examples/cases/named-inst-basic.solc
new file mode 100644
index 000000000..cb1eb1ea8
--- /dev/null
+++ b/test/examples/cases/named-inst-basic.solc
@@ -0,0 +1,31 @@
+// Basic named instance: explicit dispatch with @{label} syntax
+
+data Bool = True | False;
+
+forall a . class a : Eq {
+  function eq(x : a, y : a) -> Bool;
+}
+
+instance word : Eq {
+  function eq(x : word, y : word) -> Bool {
+    match primEqWord(x, y) {
+    | 0 => return False;
+    | _ => return True;
+    }
+  }
+}
+
+instance [myEq] word : Eq {
+  function eq(x : word, y : word) -> Bool {
+    match primEqWord(x, y) {
+    | 0 => return False;
+    | _ => return True;
+    }
+  }
+}
+
+contract NamedInstBasic {
+  function main() -> Bool {
+    return eq@{myEq}(1, 1);
+  }
+}
diff --git a/test/examples/cases/named-inst-dup-label.solc b/test/examples/cases/named-inst-dup-label.solc
new file mode 100644
index 000000000..ce5422eaf
--- /dev/null
+++ b/test/examples/cases/named-inst-dup-label.solc
@@ -0,0 +1,25 @@
+// Error case: two named instances sharing the same label
+
+data Bool = True | False;
+
+forall a . class a : Eq {
+  function eq(x : a, y : a) -> Bool;
+}
+
+instance [dupLabel] word : Eq {
+  function eq(x : word, y : word) -> Bool {
+    return True;
+  }
+}
+
+instance [dupLabel] word : Eq {
+  function eq(x : word, y : word) -> Bool {
+    return False;
+  }
+}
+
+contract NamedInstDupLabel {
+  function main() -> Bool {
+    return eq@{dupLabel}(1, 1);
+  }
+}
diff --git a/test/examples/cases/named-inst-two-instances.solc b/test/examples/cases/named-inst-two-instances.solc
new file mode 100644
index 000000000..341f349cb
--- /dev/null
+++ b/test/examples/cases/named-inst-two-instances.solc
@@ -0,0 +1,32 @@
+// Two named instances of the same class dispatched explicitly
+
+data Bool = True | False;
+
+forall a . class a : Eq {
+  function eq(x : a, y : a) -> Bool;
+}
+
+// Named instance: strict equality
+instance [strictEq] word : Eq {
+  function eq(x : word, y : word) -> Bool {
+    match primEqWord(x, y) {
+    | 0 => return False;
+    | _ => return True;
+    }
+  }
+}
+
+// Named instance: always equal (trivial equality)
+instance [trivialEq] word : Eq {
+  function eq(x : word, y : word) -> Bool {
+    return True;
+  }
+}
+
+contract TwoNamedInst {
+  function main() -> Bool {
+    let r1 : Bool = eq@{strictEq}(1, 1);
+    let r2 : Bool = eq@{trivialEq}(1, 2);
+    return r2;
+  }
+}
diff --git a/test/examples/cases/named-inst-unknown-label.solc b/test/examples/cases/named-inst-unknown-label.solc
new file mode 100644
index 000000000..ae623beee
--- /dev/null
+++ b/test/examples/cases/named-inst-unknown-label.solc
@@ -0,0 +1,13 @@
+// Error case: calling with unknown named instance label
+
+data Bool = True | False;
+
+forall a . class a : Eq {
+  function eq(x : a, y : a) -> Bool;
+}
+
+contract NamedInstUnknown {
+  function main() -> Bool {
+    return eq@{noSuchLabel}(1, 1);
+  }
+}

From c3c3df06804b5d0e82c3806ee72810c10105bd6e Mon Sep 17 00:00:00 2001
From: rodrigogribeiro <rodrigogribeiro@gmail.com>
Date: Thu, 12 Mar 2026 16:11:43 -0300
Subject: [PATCH 03/21] Ormulu formating.

---
 src/Solcore/Backend/Specialise.hs             | 22 +++++-----
 src/Solcore/Frontend/Pretty/SolcorePretty.hs  |  4 +-
 src/Solcore/Frontend/Syntax/NameResolution.hs | 27 ++++++++-----
 src/Solcore/Frontend/Syntax/SyntaxTree.hs     |  4 +-
 src/Solcore/Frontend/TypeInference/TcMonad.hs |  2 +-
 src/Solcore/Frontend/TypeInference/TcStmt.hs  | 40 +++++++++++--------
 6 files changed, 57 insertions(+), 42 deletions(-)

diff --git a/src/Solcore/Backend/Specialise.hs b/src/Solcore/Backend/Specialise.hs
index 9eafa5cda..3ccb89857 100644
--- a/src/Solcore/Backend/Specialise.hs
+++ b/src/Solcore/Backend/Specialise.hs
@@ -225,7 +225,7 @@ addInstResolutions inst = forM_ (instFunctions inst) addMethod
       -- For named instances, also register under QualName lbl methodName
       -- so that specExp can find the definition directly by label.
       case instLabel inst of
-        Nothing  -> return ()
+        Nothing -> return ()
         Just lbl -> addNamedInstMethodResolution lbl (mainTy inst) fd
 
 -- Register a named-instance method under QualName lbl methodUnqualName.
@@ -233,14 +233,14 @@ addInstResolutions inst = forM_ (instFunctions inst) addMethod
 -- strip the class qualifier and substitute the instance label.
 addNamedInstMethodResolution :: Name -> Ty -> TcFunDef -> SM ()
 addNamedInstMethodResolution lbl ty fd = do
-  let sig      = funSignature fd
-      methUnq  = case sigName sig of
-                   QualName _ m -> m
-                   Name s       -> s
-      qname    = QualName lbl methUnq
-      name'    = specName qname [ty]
-      funType  = typeOfTcFunDef fd
-      fd'      = FunDef sig { sigName = name' } (funDefBody fd)
+  let sig = funSignature fd
+      methUnq = case sigName sig of
+        QualName _ m -> m
+        Name s -> s
+      qname = QualName lbl methUnq
+      name' = specName qname [ty]
+      funType = typeOfTcFunDef fd
+      fd' = FunDef sig {sigName = name'} (funDefBody fd)
   addResolution qname funType fd'
   debug ["+ addNamedInstMethodResolution: ", show qname, " / ", show name', " : ", pretty funType]
 
@@ -331,8 +331,8 @@ specExp (Call Nothing i lbl args) ty = do
   -- For named instance calls, resolve via QualName lbl method so the
   -- specialiser finds the definition registered under that label.
   let i' = case lbl of
-              Just l  -> i { idName = QualName l (pretty (idName i)) }
-              Nothing -> i
+        Just l -> i {idName = QualName l (pretty (idName i))}
+        Nothing -> i
   (i'', args') <- specCall i' args ty
   let e' = Call Nothing i'' Nothing args'
   -- debug ["< specExp (Call): ", pretty e']
diff --git a/src/Solcore/Frontend/Pretty/SolcorePretty.hs b/src/Solcore/Frontend/Pretty/SolcorePretty.hs
index ff53993b3..cd9678660 100644
--- a/src/Solcore/Frontend/Pretty/SolcorePretty.hs
+++ b/src/Solcore/Frontend/Pretty/SolcorePretty.hs
@@ -244,7 +244,7 @@ instance (Pretty a) => Pretty (Instance a) where
       $$ rbrace
 
 pprInstLabel :: Maybe Name -> Doc
-pprInstLabel Nothing    = empty
+pprInstLabel Nothing = empty
 pprInstLabel (Just lbl) = text "[" <> ppr lbl <> text "]"
 
 pprDefault :: Bool -> Doc
@@ -381,7 +381,7 @@ pprE Nothing = ""
 pprE (Just e) = ppr e <> text "."
 
 pprCallLabel :: Maybe Name -> Doc
-pprCallLabel Nothing    = empty
+pprCallLabel Nothing = empty
 pprCallLabel (Just lbl) = text "@{" <> ppr lbl <> text "}"
 
 instance (Pretty a) => Pretty (Pat a) where
diff --git a/src/Solcore/Frontend/Syntax/NameResolution.hs b/src/Solcore/Frontend/Syntax/NameResolution.hs
index ddfe11f64..5b6d442b5 100644
--- a/src/Solcore/Frontend/Syntax/NameResolution.hs
+++ b/src/Solcore/Frontend/Syntax/NameResolution.hs
@@ -747,9 +747,13 @@ instance Resolve S.Exp where
     dt <- lookupName qn
     case dt of
       Just TFunction -> pure (Call me' n (Just lbl) es')
-      _ -> throwError $
-        "Unknown named instance label '" ++ pretty lbl
-        ++ "' for method '" ++ pretty n ++ "'"
+      _ ->
+        throwError $
+          "Unknown named instance label '"
+            ++ pretty lbl
+            ++ "' for method '"
+            ++ pretty n
+            ++ "'"
 
 instance Resolve S.Literal where
   type Result S.Literal = Literal
@@ -940,13 +944,16 @@ addTopDecl (S.TSym (S.TySym n _ _)) env =
     env {typeEnv = Map.insert n TTyCon (typeEnv env)}
 addTopDecl (S.TExportDecl _) env = env
 addTopDecl (S.TInstDef (S.Instance _ (Just lbl) _ _ _ _ _ funs)) env =
-  env { scopeEnv =
-          foldr (\fd ac ->
-                   let qn = QualName lbl (pretty (S.sigName (S.funSignature fd)))
-                   in Map.insert qn TFunction ac)
-                (scopeEnv env)
-                funs
-      }
+  env
+    { scopeEnv =
+        foldr
+          ( \fd ac ->
+              let qn = QualName lbl (pretty (S.sigName (S.funSignature fd)))
+               in Map.insert qn TFunction ac
+          )
+          (scopeEnv env)
+          funs
+    }
 addTopDecl _ env = env
 
 addModuleName :: Name -> Env -> Env
diff --git a/src/Solcore/Frontend/Syntax/SyntaxTree.hs b/src/Solcore/Frontend/Syntax/SyntaxTree.hs
index 9a931830e..8b69e4f1a 100644
--- a/src/Solcore/Frontend/Syntax/SyntaxTree.hs
+++ b/src/Solcore/Frontend/Syntax/SyntaxTree.hs
@@ -280,9 +280,9 @@ data Exp
   | ExpLNot Exp -- ! e
   | ExpCond Exp Exp Exp -- if e1 then e2 else e3
   | ExpAt Ty -- proxy sugar
-  | ExpNameAt (Maybe Exp) Name Name [Exp]
-    -- ^ ExpNameAt receiver methodName instanceLabel args
+  | -- | ExpNameAt receiver methodName instanceLabel args
     --   Represents receiver.method@{label}(args) or method@{label}(args)
+    ExpNameAt (Maybe Exp) Name Name [Exp]
   deriving (Eq, Ord, Show, Data, Typeable)
 
 -- pattern matching equations
diff --git a/src/Solcore/Frontend/TypeInference/TcMonad.hs b/src/Solcore/Frontend/TypeInference/TcMonad.hs
index d1cf70daa..5a2c2c26b 100644
--- a/src/Solcore/Frontend/TypeInference/TcMonad.hs
+++ b/src/Solcore/Frontend/TypeInference/TcMonad.hs
@@ -551,7 +551,7 @@ addDefaultInstance n inst =
 
 addNamedInstance :: Name -> Instance Name -> TcM ()
 addNamedInstance label inst =
-  modify (\st -> st { namedInstEnv = Map.insert label inst (namedInstEnv st) })
+  modify (\st -> st {namedInstEnv = Map.insert label inst (namedInstEnv st)})
 
 askNamedInstance :: Name -> TcM (Maybe (Instance Name))
 askNamedInstance label = Map.lookup label <$> gets namedInstEnv
diff --git a/src/Solcore/Frontend/TypeInference/TcStmt.hs b/src/Solcore/Frontend/TypeInference/TcStmt.hs
index 7c78834c3..3a5b6c345 100644
--- a/src/Solcore/Frontend/TypeInference/TcStmt.hs
+++ b/src/Solcore/Frontend/TypeInference/TcStmt.hs
@@ -1090,7 +1090,8 @@ checkInstance idef@(Instance d lbl vs predCtx n ts t funs) =
         -- Named instances: skip overlap check, register by label
         existing <- askNamedInstance label
         unless (isNothing existing) $
-          throwError $ "Duplicate named instance label: " ++ pretty label
+          throwError $
+            "Duplicate named instance label: " ++ pretty label
         addNamedInstance label idef
 
 maybeExpandSynonym :: Ty -> TcM Ty
@@ -1342,27 +1343,34 @@ tcCallNamed me n lbl args =
     let callExpr = Call me n (Just lbl) args
     -- Look up the named instance by label
     minst <- askNamedInstance lbl
-    inst <- maybe
-      (throwError $ "Unknown named instance label: " ++ pretty lbl)
-      pure
-      minst
+    inst <-
+      maybe
+        (throwError $ "Unknown named instance label: " ++ pretty lbl)
+        pure
+        minst
     -- Find the method in the instance's function definitions
     let mfun = find (\fd -> sigName (funSignature fd) == n) (instFunctions inst)
-    fun <- maybe
-      (throwError $ unwords
-        ["Method", pretty n, "not found in named instance", pretty lbl])
-      pure
-      mfun
+    fun <-
+      maybe
+        ( throwError $
+            unwords
+              ["Method", pretty n, "not found in named instance", pretty lbl]
+        )
+        pure
+        mfun
     -- Build the type scheme from the method signature + instance context
     let sig = funSignature fun
-        vs   = instVars inst ++ sigVars sig
+        vs = instVars inst ++ sigVars sig
         preds = instContext inst ++ sigContext sig
         argTys = [t | Typed _ t <- sigParams sig]
-    ret <- maybe
-      (throwError $ unwords
-        ["Method", pretty n, "in named instance", pretty lbl, "missing return type"])
-      pure
-      (sigReturn sig)
+    ret <-
+      maybe
+        ( throwError $
+            unwords
+              ["Method", pretty n, "in named instance", pretty lbl, "missing return type"]
+        )
+        pure
+        (sigReturn sig)
     let scheme = Forall vs (preds :=> funtype argTys ret)
     (ps :=> t) <- freshInst scheme
     t' <- freshTyVar

From a0ebdc6cce022a7249377a5f5b5a232f4d9ef353 Mon Sep 17 00:00:00 2001
From: Yoshitomo Nakanishi <yurayura.rounin.3@gmail.com>
Date: Sat, 11 Apr 2026 18:41:53 +0900
Subject: [PATCH 04/21] Fix named instance receiver dispatch

---
 src/Solcore/Frontend/Syntax/NameResolution.hs |  3 ++-
 src/Solcore/Frontend/TypeInference/TcStmt.hs  | 15 ++++++++-----
 test/Cases.hs                                 |  1 +
 test/examples/cases/named-inst-receiver.solc  | 22 +++++++++++++++++++
 4 files changed, 35 insertions(+), 6 deletions(-)
 create mode 100644 test/examples/cases/named-inst-receiver.solc

diff --git a/src/Solcore/Frontend/Syntax/NameResolution.hs b/src/Solcore/Frontend/Syntax/NameResolution.hs
index 5b6d442b5..c6fcc4b3f 100644
--- a/src/Solcore/Frontend/Syntax/NameResolution.hs
+++ b/src/Solcore/Frontend/Syntax/NameResolution.hs
@@ -744,9 +744,10 @@ instance Resolve S.Exp where
     me' <- resolve me `wrapError` x
     es' <- resolve es `wrapError` x
     let qn = QualName lbl (pretty n)
+        args = maybe es' (: es') me'
     dt <- lookupName qn
     case dt of
-      Just TFunction -> pure (Call me' n (Just lbl) es')
+      Just TFunction -> pure (Call Nothing n (Just lbl) args)
       _ ->
         throwError $
           "Unknown named instance label '"
diff --git a/src/Solcore/Frontend/TypeInference/TcStmt.hs b/src/Solcore/Frontend/TypeInference/TcStmt.hs
index 3a5b6c345..2f7186ee2 100644
--- a/src/Solcore/Frontend/TypeInference/TcStmt.hs
+++ b/src/Solcore/Frontend/TypeInference/TcStmt.hs
@@ -1374,13 +1374,18 @@ tcCallNamed me n lbl args =
     let scheme = Forall vs (preds :=> funtype argTys ret)
     (ps :=> t) <- freshInst scheme
     t' <- freshTyVar
-    me' <- mapM (\e -> (\(e', _, _) -> e') <$> tcExp e) me
+    mrecv <- mapM tcExp me
     (es', pss', ts') <- unzip3 <$> mapM tcExp args
-    s' <- unify t (funtype ts' t') `wrapError` callExpr
+    let recvArgs = maybe [] (\(e', _, _) -> [e']) mrecv
+        recvPreds = maybe [] (\(_, ps0, _) -> ps0) mrecv
+        recvTys = maybe [] (\(_, _, ty0) -> [ty0]) mrecv
+        allArgs = recvArgs ++ es'
+        allTys = recvTys ++ ts'
+    s' <- unify t (funtype allTys t') `wrapError` callExpr
     _ <- extSubst s'
-    let ps' = foldr union [] (ps : pss')
-        t1 = funtype ts' t'
-    withCurrentSubst (Call me' (Id n t1) (Just lbl) es', ps', t')
+    let ps' = foldr union [] (ps : recvPreds : pss')
+        t1 = funtype allTys t'
+    withCurrentSubst (Call Nothing (Id n t1) (Just lbl) allArgs, ps', t')
 
 tcParam :: Param Name -> TcM (Param Id)
 tcParam (Typed n t) =
diff --git a/test/Cases.hs b/test/Cases.hs
index f0128e7d2..45824bd27 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -401,6 +401,7 @@ cases =
       runTestForFile "false-redundant-warning.solc" caseFolder,
       runTestForFile "proxy-desugar.solc" caseFolder,
       runTestForFile "named-inst-basic.solc" caseFolder,
+      runTestForFile "named-inst-receiver.solc" caseFolder,
       runTestForFile "named-inst-two-instances.solc" caseFolder,
       runTestExpectingFailure "named-inst-unknown-label.solc" caseFolder,
       runTestExpectingFailure "named-inst-dup-label.solc" caseFolder,
diff --git a/test/examples/cases/named-inst-receiver.solc b/test/examples/cases/named-inst-receiver.solc
new file mode 100644
index 000000000..9c233273a
--- /dev/null
+++ b/test/examples/cases/named-inst-receiver.solc
@@ -0,0 +1,22 @@
+// Named instance dispatch should also work through receiver syntax.
+
+data Bool = True | False;
+
+forall a . class a : Eq {
+  function eq(x : a, y : a) -> Bool;
+}
+
+instance [myEq] word : Eq {
+  function eq(x : word, y : word) -> Bool {
+    match primEqWord(x, y) {
+    | 0 => return False;
+    | _ => return True;
+    }
+  }
+}
+
+contract NamedInstReceiver {
+  function main() -> Bool {
+    return 1.eq@{myEq}(1);
+  }
+}

From 814bca5add0775e996c661868d452b39789e320e Mon Sep 17 00:00:00 2001
From: Yoshitomo Nakanishi <yurayura.rounin.3@gmail.com>
Date: Sun, 12 Apr 2026 11:08:37 +0900
Subject: [PATCH 05/21] Allow named labels for distinct instance heads

---
 src/Solcore/Frontend/TypeInference/TcEnv.hs   |   2 +-
 src/Solcore/Frontend/TypeInference/TcMonad.hs |   6 +-
 src/Solcore/Frontend/TypeInference/TcStmt.hs  | 117 ++++++++++++++----
 test/Cases.hs                                 |   1 +
 .../cases/named-inst-shared-label.solc        |  30 +++++
 5 files changed, 129 insertions(+), 27 deletions(-)
 create mode 100644 test/examples/cases/named-inst-shared-label.solc

diff --git a/src/Solcore/Frontend/TypeInference/TcEnv.hs b/src/Solcore/Frontend/TypeInference/TcEnv.hs
index 416c80260..b25257b59 100644
--- a/src/Solcore/Frontend/TypeInference/TcEnv.hs
+++ b/src/Solcore/Frontend/TypeInference/TcEnv.hs
@@ -93,7 +93,7 @@ data TcEnv
   { ctx :: Env, -- Variable environment
     instEnv :: InstTable, -- Instance Environment
     defaultEnv :: DefTable, -- Default instance environment
-    namedInstEnv :: Map Name (Instance Name), -- Named instance environment (by label)
+    namedInstEnv :: Map Name [Instance Name], -- Named instance environment (by label)
     typeTable :: TypeTable, -- Type information environment
     synTable :: SynTable, -- Type synonym environment
     classTable :: ClassTable, -- Class information table
diff --git a/src/Solcore/Frontend/TypeInference/TcMonad.hs b/src/Solcore/Frontend/TypeInference/TcMonad.hs
index 5a2c2c26b..0b531d7ad 100644
--- a/src/Solcore/Frontend/TypeInference/TcMonad.hs
+++ b/src/Solcore/Frontend/TypeInference/TcMonad.hs
@@ -551,10 +551,10 @@ addDefaultInstance n inst =
 
 addNamedInstance :: Name -> Instance Name -> TcM ()
 addNamedInstance label inst =
-  modify (\st -> st {namedInstEnv = Map.insert label inst (namedInstEnv st)})
+  modify (\st -> st {namedInstEnv = Map.insertWith (++) label [inst] (namedInstEnv st)})
 
-askNamedInstance :: Name -> TcM (Maybe (Instance Name))
-askNamedInstance label = Map.lookup label <$> gets namedInstEnv
+askNamedInstances :: Name -> TcM [Instance Name]
+askNamedInstances label = Map.findWithDefault [] label <$> gets namedInstEnv
 
 maybeToTcM :: String -> Maybe a -> TcM a
 maybeToTcM s Nothing = throwError s
diff --git a/src/Solcore/Frontend/TypeInference/TcStmt.hs b/src/Solcore/Frontend/TypeInference/TcStmt.hs
index 2f7186ee2..01f54fe5f 100644
--- a/src/Solcore/Frontend/TypeInference/TcStmt.hs
+++ b/src/Solcore/Frontend/TypeInference/TcStmt.hs
@@ -1087,11 +1087,12 @@ checkInstance idef@(Instance d lbl vs predCtx n ts t funs) =
           then addDefaultInstance n ninst
           else addInstance n ninst
       Just label -> do
-        -- Named instances: skip overlap check, register by label
-        existing <- askNamedInstance label
-        unless (isNothing existing) $
+        -- Named instances: skip overlap check, register by label.
+        -- Reusing a label is allowed as long as the instance head differs.
+        existing <- askNamedInstances label
+        unless (all (differentNamedInstHead idef) existing) $
           throwError $
-            "Duplicate named instance label: " ++ pretty label
+            "Duplicate named instance label/head combination: " ++ pretty label
         addNamedInstance label idef
 
 maybeExpandSynonym :: Ty -> TcM Ty
@@ -1341,15 +1342,63 @@ tcCallNamed :: Maybe (Exp Name) -> Name -> Name -> [Exp Name] -> TcM (Exp Id, [P
 tcCallNamed me n lbl args =
   do
     let callExpr = Call me n (Just lbl) args
-    -- Look up the named instance by label
-    minst <- askNamedInstance lbl
-    inst <-
-      maybe
-        (throwError $ "Unknown named instance label: " ++ pretty lbl)
-        pure
-        minst
-    -- Find the method in the instance's function definitions
-    let mfun = find (\fd -> sigName (funSignature fd) == n) (instFunctions inst)
+    namedInsts <- askNamedInstances lbl
+    when (null namedInsts) $
+      throwError $ "Unknown named instance label: " ++ pretty lbl
+    mrecv <- mapM tcExp me
+    (es', pss', ts') <- unzip3 <$> mapM tcExp args
+    let recvArgs = maybe [] (\(e', _, _) -> [e']) mrecv
+        recvPreds = maybe [] (\(_, ps0, _) -> ps0) mrecv
+        recvTys = maybe [] (\(_, _, ty0) -> [ty0]) mrecv
+        allArgs = recvArgs ++ es'
+        allTys = recvTys ++ ts'
+        methodInsts = filter (hasNamedMethod n) namedInsts
+    when (null methodInsts) $
+      throwError $
+        unwords
+          ["Method", pretty n, "not found in named instance", pretty lbl]
+    matches <- filterM (matchesNamedCall callExpr n lbl allTys) methodInsts
+    case matches of
+      [] ->
+        throwError $
+          unwords
+            [ "No named instance labelled",
+              pretty lbl,
+              "matches call to",
+              pretty n
+            ]
+      [inst] -> tcCallNamedWithInst callExpr n lbl recvPreds allArgs pss' allTys inst
+      _ ->
+        throwError $
+          unlines $
+            [ unwords
+                [ "Ambiguous named instance label",
+                  pretty lbl,
+                  "for method",
+                  pretty n
+                ],
+              "Matching heads:"
+            ]
+              ++ map (("  " ++) . pretty . namedInstPred) matches
+
+differentNamedInstHead :: Instance Name -> Instance Name -> Bool
+differentNamedInstHead inst inst' =
+  instName inst /= instName inst'
+    || mainTy inst /= mainTy inst'
+    || paramsTy inst /= paramsTy inst'
+
+hasNamedMethod :: Name -> Instance Name -> Bool
+hasNamedMethod n = isJust . findNamedMethod n
+
+findNamedMethod :: Name -> Instance Name -> Maybe (FunDef Name)
+findNamedMethod n = find (\fd -> sigName (funSignature fd) == n) . instFunctions
+
+namedInstPred :: Instance Name -> Pred
+namedInstPred inst = InCls (instName inst) (mainTy inst) (paramsTy inst)
+
+namedMethodScheme :: Name -> Name -> Instance Name -> TcM Scheme
+namedMethodScheme n lbl inst =
+  do
     fun <-
       maybe
         ( throwError $
@@ -1357,8 +1406,7 @@ tcCallNamed me n lbl args =
               ["Method", pretty n, "not found in named instance", pretty lbl]
         )
         pure
-        mfun
-    -- Build the type scheme from the method signature + instance context
+        (findNamedMethod n inst)
     let sig = funSignature fun
         vs = instVars inst ++ sigVars sig
         preds = instContext inst ++ sigContext sig
@@ -1371,16 +1419,39 @@ tcCallNamed me n lbl args =
         )
         pure
         (sigReturn sig)
-    let scheme = Forall vs (preds :=> funtype argTys ret)
+    pure (Forall vs (preds :=> funtype argTys ret))
+
+matchesNamedCall :: Exp Name -> Name -> Name -> [Ty] -> Instance Name -> TcM Bool
+matchesNamedCall callExpr n lbl allTys inst =
+  do
+    st <- get
+    res <-
+      ( do
+          scheme <- namedMethodScheme n lbl inst
+          (_ :=> t) <- freshInst scheme
+          t' <- freshTyVar
+          _ <- unify t (funtype allTys t') `wrapError` callExpr
+          pure True
+      )
+        `catchError` (\_ -> pure False)
+    put st
+    pure res
+
+tcCallNamedWithInst ::
+  Exp Name ->
+  Name ->
+  Name ->
+  [Pred] ->
+  [Exp Id] ->
+  [[Pred]] ->
+  [Ty] ->
+  Instance Name ->
+  TcM (Exp Id, [Pred], Ty)
+tcCallNamedWithInst callExpr n lbl recvPreds allArgs pss' allTys inst =
+  do
+    scheme <- namedMethodScheme n lbl inst
     (ps :=> t) <- freshInst scheme
     t' <- freshTyVar
-    mrecv <- mapM tcExp me
-    (es', pss', ts') <- unzip3 <$> mapM tcExp args
-    let recvArgs = maybe [] (\(e', _, _) -> [e']) mrecv
-        recvPreds = maybe [] (\(_, ps0, _) -> ps0) mrecv
-        recvTys = maybe [] (\(_, _, ty0) -> [ty0]) mrecv
-        allArgs = recvArgs ++ es'
-        allTys = recvTys ++ ts'
     s' <- unify t (funtype allTys t') `wrapError` callExpr
     _ <- extSubst s'
     let ps' = foldr union [] (ps : recvPreds : pss')
diff --git a/test/Cases.hs b/test/Cases.hs
index 45824bd27..b9d727787 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -402,6 +402,7 @@ cases =
       runTestForFile "proxy-desugar.solc" caseFolder,
       runTestForFile "named-inst-basic.solc" caseFolder,
       runTestForFile "named-inst-receiver.solc" caseFolder,
+      runTestForFile "named-inst-shared-label.solc" caseFolder,
       runTestForFile "named-inst-two-instances.solc" caseFolder,
       runTestExpectingFailure "named-inst-unknown-label.solc" caseFolder,
       runTestExpectingFailure "named-inst-dup-label.solc" caseFolder,
diff --git a/test/examples/cases/named-inst-shared-label.solc b/test/examples/cases/named-inst-shared-label.solc
new file mode 100644
index 000000000..90a3d12ea
--- /dev/null
+++ b/test/examples/cases/named-inst-shared-label.solc
@@ -0,0 +1,30 @@
+// Reusing the same named-instance label for different heads should work.
+
+data Bool = True | False;
+
+forall a . class a : Eq {
+  function eq(x : a, y : a) -> Bool;
+}
+
+instance [shared] word : Eq {
+  function eq(x : word, y : word) -> Bool {
+    return True;
+  }
+}
+
+instance [shared] Bool : Eq {
+  function eq(x : Bool, y : Bool) -> Bool {
+    match x, y {
+    | True, True => return True;
+    | _, _ => return False;
+    }
+  }
+}
+
+contract NamedInstSharedLabel {
+  function main() -> Bool {
+    let x : Bool = eq@{shared}(1, 2);
+    let y : Bool = eq@{shared}(True, True);
+    return y;
+  }
+}

From a6d4d7fbbe67ce4630ef2b85288ffb78e0270c83 Mon Sep 17 00:00:00 2001
From: Yoshitomo Nakanishi <yurayura.rounin.3@gmail.com>
Date: Sun, 12 Apr 2026 16:52:06 +0900
Subject: [PATCH 06/21] Support class-qualified named calls

---
 src/Solcore/Backend/Specialise.hs             |  6 ++-
 src/Solcore/Frontend/Syntax/NameResolution.hs | 39 +++++++++++++------
 src/Solcore/Frontend/TypeInference/TcStmt.hs  | 15 ++++++-
 test/Cases.hs                                 |  1 +
 .../cases/named-inst-class-qualified.solc     | 31 +++++++++++++++
 5 files changed, 77 insertions(+), 15 deletions(-)
 create mode 100644 test/examples/cases/named-inst-class-qualified.solc

diff --git a/src/Solcore/Backend/Specialise.hs b/src/Solcore/Backend/Specialise.hs
index 3ccb89857..6e7fdb1c8 100644
--- a/src/Solcore/Backend/Specialise.hs
+++ b/src/Solcore/Backend/Specialise.hs
@@ -331,7 +331,11 @@ specExp (Call Nothing i lbl args) ty = do
   -- For named instance calls, resolve via QualName lbl method so the
   -- specialiser finds the definition registered under that label.
   let i' = case lbl of
-        Just l -> i {idName = QualName l (pretty (idName i))}
+        Just l ->
+          let meth = case idName i of
+                QualName _ m -> m
+                Name s -> s
+           in i {idName = QualName l meth}
         Nothing -> i
   (i'', args') <- specCall i' args ty
   let e' = Call Nothing i'' Nothing args'
diff --git a/src/Solcore/Frontend/Syntax/NameResolution.hs b/src/Solcore/Frontend/Syntax/NameResolution.hs
index c6fcc4b3f..b1898b87c 100644
--- a/src/Solcore/Frontend/Syntax/NameResolution.hs
+++ b/src/Solcore/Frontend/Syntax/NameResolution.hs
@@ -743,18 +743,18 @@ instance Resolve S.Exp where
   resolve x@(S.ExpNameAt me n lbl es) = do
     me' <- resolve me `wrapError` x
     es' <- resolve es `wrapError` x
-    let qn = QualName lbl (pretty n)
-        args = maybe es' (: es') me'
-    dt <- lookupName qn
-    case dt of
-      Just TFunction -> pure (Call Nothing n (Just lbl) args)
-      _ ->
-        throwError $
-          "Unknown named instance label '"
-            ++ pretty lbl
-            ++ "' for method '"
-            ++ pretty n
-            ++ "'"
+    case me' of
+      Just (Var c) -> do
+        ct <- lookupName c
+        case ct of
+          Just TClass -> do
+            let qn = QualName c (pretty n)
+            cf <- gets (Map.lookup qn . scopeEnv)
+            case cf of
+              Just TFunction -> pure (Call Nothing qn (Just lbl) es')
+              _ -> undefinedName n
+          _ -> resolveNamedCall me' n lbl es'
+      _ -> resolveNamedCall me' n lbl es'
 
 instance Resolve S.Literal where
   type Result S.Literal = Literal
@@ -966,6 +966,21 @@ addQualifiedModules (QualName qualifier _) env =
   foldr addModuleName env (modulePrefixes qualifier)
 addQualifiedModules _ env = env
 
+resolveNamedCall :: Maybe (Exp Name) -> Name -> Name -> [Exp Name] -> ResolveM (Exp Name)
+resolveNamedCall me n lbl es = do
+  let qn = QualName lbl (pretty n)
+      args = maybe es (: es) me
+  dt <- lookupName qn
+  case dt of
+    Just TFunction -> pure (Call Nothing n (Just lbl) args)
+    _ ->
+      throwError $
+        "Unknown named instance label '"
+          ++ pretty lbl
+          ++ "' for method '"
+          ++ pretty n
+          ++ "'"
+
 -- definition of a monad for name resolution
 
 type ResolveM a = StateT Env (ExceptT String IO) a
diff --git a/src/Solcore/Frontend/TypeInference/TcStmt.hs b/src/Solcore/Frontend/TypeInference/TcStmt.hs
index 01f54fe5f..7c5ee8e96 100644
--- a/src/Solcore/Frontend/TypeInference/TcStmt.hs
+++ b/src/Solcore/Frontend/TypeInference/TcStmt.hs
@@ -1388,17 +1388,28 @@ differentNamedInstHead inst inst' =
     || paramsTy inst /= paramsTy inst'
 
 hasNamedMethod :: Name -> Instance Name -> Bool
-hasNamedMethod n = isJust . findNamedMethod n
+hasNamedMethod n inst =
+  let (mcls, meth) = splitNamedMethod n
+   in maybe True (== instName inst) mcls && isJust (findNamedMethod meth inst)
 
 findNamedMethod :: Name -> Instance Name -> Maybe (FunDef Name)
 findNamedMethod n = find (\fd -> sigName (funSignature fd) == n) . instFunctions
 
+splitNamedMethod :: Name -> (Maybe Name, Name)
+splitNamedMethod (QualName cls meth) = (Just cls, Name meth)
+splitNamedMethod n = (Nothing, n)
+
 namedInstPred :: Instance Name -> Pred
 namedInstPred inst = InCls (instName inst) (mainTy inst) (paramsTy inst)
 
 namedMethodScheme :: Name -> Name -> Instance Name -> TcM Scheme
 namedMethodScheme n lbl inst =
   do
+    let (mcls, meth) = splitNamedMethod n
+    unless (maybe True (== instName inst) mcls) $
+      throwError $
+        unwords
+          ["Method", pretty n, "not found in named instance", pretty lbl]
     fun <-
       maybe
         ( throwError $
@@ -1406,7 +1417,7 @@ namedMethodScheme n lbl inst =
               ["Method", pretty n, "not found in named instance", pretty lbl]
         )
         pure
-        (findNamedMethod n inst)
+        (findNamedMethod meth inst)
     let sig = funSignature fun
         vs = instVars inst ++ sigVars sig
         preds = instContext inst ++ sigContext sig
diff --git a/test/Cases.hs b/test/Cases.hs
index b9d727787..f46e2be81 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -401,6 +401,7 @@ cases =
       runTestForFile "false-redundant-warning.solc" caseFolder,
       runTestForFile "proxy-desugar.solc" caseFolder,
       runTestForFile "named-inst-basic.solc" caseFolder,
+      runTestForFile "named-inst-class-qualified.solc" caseFolder,
       runTestForFile "named-inst-receiver.solc" caseFolder,
       runTestForFile "named-inst-shared-label.solc" caseFolder,
       runTestForFile "named-inst-two-instances.solc" caseFolder,
diff --git a/test/examples/cases/named-inst-class-qualified.solc b/test/examples/cases/named-inst-class-qualified.solc
new file mode 100644
index 000000000..fc3abcedb
--- /dev/null
+++ b/test/examples/cases/named-inst-class-qualified.solc
@@ -0,0 +1,31 @@
+// Class-qualified named calls should disambiguate instances sharing a label.
+
+data Bool = True | False;
+
+forall a . class a : Foo {
+  function run(x : a) -> Bool;
+}
+
+forall a . class a : Bar {
+  function run(x : a) -> Bool;
+}
+
+instance [shared] word : Foo {
+  function run(x : word) -> Bool {
+    return True;
+  }
+}
+
+instance [shared] word : Bar {
+  function run(x : word) -> Bool {
+    return False;
+  }
+}
+
+contract NamedInstClassQualified {
+  function main() -> Bool {
+    let x : Bool = Foo.run@{shared}(1);
+    let y : Bool = Bar.run@{shared}(1);
+    return y;
+  }
+}

From ffcd28fdc2c441b701d2c80f2eb5756d04cb2fd8 Mon Sep 17 00:00:00 2001
From: Yoshitomo Nakanishi <yurayura.rounin.3@gmail.com>
Date: Mon, 13 Apr 2026 12:34:29 +0900
Subject: [PATCH 07/21] Add shared-label parameter disambiguation test

---
 test/Cases.hs                                 |  1 +
 .../cases/named-inst-shared-label-params.solc | 28 +++++++++++++++++++
 2 files changed, 29 insertions(+)
 create mode 100644 test/examples/cases/named-inst-shared-label-params.solc

diff --git a/test/Cases.hs b/test/Cases.hs
index f46e2be81..87a946fc7 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -402,6 +402,7 @@ cases =
       runTestForFile "proxy-desugar.solc" caseFolder,
       runTestForFile "named-inst-basic.solc" caseFolder,
       runTestForFile "named-inst-class-qualified.solc" caseFolder,
+      runTestForFile "named-inst-shared-label-params.solc" caseFolder,
       runTestForFile "named-inst-receiver.solc" caseFolder,
       runTestForFile "named-inst-shared-label.solc" caseFolder,
       runTestForFile "named-inst-two-instances.solc" caseFolder,
diff --git a/test/examples/cases/named-inst-shared-label-params.solc b/test/examples/cases/named-inst-shared-label-params.solc
new file mode 100644
index 000000000..5680a6f27
--- /dev/null
+++ b/test/examples/cases/named-inst-shared-label-params.solc
@@ -0,0 +1,28 @@
+// Reusing a label across the same class/head should work when params are
+// distinguished by explicit method arguments.
+
+data Bool = True | False;
+
+forall self rep . class self : Pick(rep) {
+  function pick(x : self, y : rep) -> rep;
+}
+
+instance [shared] word : Pick(word) {
+  function pick(x : word, y : word) -> word {
+    return y;
+  }
+}
+
+instance [shared] word : Pick(Bool) {
+  function pick(x : word, y : Bool) -> Bool {
+    return y;
+  }
+}
+
+contract NamedInstSharedLabelParams {
+  function main() -> Bool {
+    let x : word = pick@{shared}(1, 2);
+    let y : Bool = pick@{shared}(1, True);
+    return y;
+  }
+}

From e60346a7f04d88458b76ff37046cae410218917f Mon Sep 17 00:00:00 2001
From: Yoshitomo Nakanishi <yurayura.rounin.3@gmail.com>
Date: Mon, 13 Apr 2026 17:11:45 +0900
Subject: [PATCH 08/21] Add named-instance ambiguity regression tests

---
 test/Cases.hs                                 |  2 ++
 .../named-inst-ambiguous-unqualified.solc     | 30 +++++++++++++++++++
 .../cases/named-inst-no-matching-head.solc    | 26 ++++++++++++++++
 3 files changed, 58 insertions(+)
 create mode 100644 test/examples/cases/named-inst-ambiguous-unqualified.solc
 create mode 100644 test/examples/cases/named-inst-no-matching-head.solc

diff --git a/test/Cases.hs b/test/Cases.hs
index 87a946fc7..71db3e217 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -401,7 +401,9 @@ cases =
       runTestForFile "false-redundant-warning.solc" caseFolder,
       runTestForFile "proxy-desugar.solc" caseFolder,
       runTestForFile "named-inst-basic.solc" caseFolder,
+      runTestExpectingFailure "named-inst-ambiguous-unqualified.solc" caseFolder,
       runTestForFile "named-inst-class-qualified.solc" caseFolder,
+      runTestExpectingFailure "named-inst-no-matching-head.solc" caseFolder,
       runTestForFile "named-inst-shared-label-params.solc" caseFolder,
       runTestForFile "named-inst-receiver.solc" caseFolder,
       runTestForFile "named-inst-shared-label.solc" caseFolder,
diff --git a/test/examples/cases/named-inst-ambiguous-unqualified.solc b/test/examples/cases/named-inst-ambiguous-unqualified.solc
new file mode 100644
index 000000000..3f304fda2
--- /dev/null
+++ b/test/examples/cases/named-inst-ambiguous-unqualified.solc
@@ -0,0 +1,30 @@
+// Unqualified named calls should fail when the same label is reused across
+// multiple classes exposing the same method name.
+
+data Bool = True | False;
+
+forall a . class a : Foo {
+  function run(x : a) -> Bool;
+}
+
+forall a . class a : Bar {
+  function run(x : a) -> Bool;
+}
+
+instance [shared] word : Foo {
+  function run(x : word) -> Bool {
+    return True;
+  }
+}
+
+instance [shared] word : Bar {
+  function run(x : word) -> Bool {
+    return False;
+  }
+}
+
+contract NamedInstAmbiguousUnqualified {
+  function main() -> Bool {
+    return run@{shared}(1);
+  }
+}
diff --git a/test/examples/cases/named-inst-no-matching-head.solc b/test/examples/cases/named-inst-no-matching-head.solc
new file mode 100644
index 000000000..721f804c7
--- /dev/null
+++ b/test/examples/cases/named-inst-no-matching-head.solc
@@ -0,0 +1,26 @@
+// A label may exist and still fail if none of its heads matches the call.
+
+data Bool = True | False;
+data Flag = F;
+
+forall self rep . class self : Pick(rep) {
+  function pick(x : self, y : rep) -> rep;
+}
+
+instance [shared] word : Pick(word) {
+  function pick(x : word, y : word) -> word {
+    return y;
+  }
+}
+
+instance [shared] word : Pick(Bool) {
+  function pick(x : word, y : Bool) -> Bool {
+    return y;
+  }
+}
+
+contract NamedInstNoMatchingHead {
+  function main() -> Bool {
+    return pick@{shared}(1, F);
+  }
+}

From 51d06122cafa5e5d64fd2b168f53407e60f1b7b0 Mon Sep 17 00:00:00 2001
From: Yoshitomo Nakanishi <yurayura.rounin.3@gmail.com>
Date: Tue, 14 Apr 2026 13:07:27 +0900
Subject: [PATCH 09/21] Fix ormolu formatting

---
 src/Solcore/Frontend/TypeInference/TcStmt.hs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Solcore/Frontend/TypeInference/TcStmt.hs b/src/Solcore/Frontend/TypeInference/TcStmt.hs
index 7c5ee8e96..e3ac066cf 100644
--- a/src/Solcore/Frontend/TypeInference/TcStmt.hs
+++ b/src/Solcore/Frontend/TypeInference/TcStmt.hs
@@ -1344,7 +1344,8 @@ tcCallNamed me n lbl args =
     let callExpr = Call me n (Just lbl) args
     namedInsts <- askNamedInstances lbl
     when (null namedInsts) $
-      throwError $ "Unknown named instance label: " ++ pretty lbl
+      throwError $
+        "Unknown named instance label: " ++ pretty lbl
     mrecv <- mapM tcExp me
     (es', pss', ts') <- unzip3 <$> mapM tcExp args
     let recvArgs = maybe [] (\(e', _, _) -> [e']) mrecv
@@ -1443,7 +1444,7 @@ matchesNamedCall callExpr n lbl allTys inst =
           t' <- freshTyVar
           _ <- unify t (funtype allTys t') `wrapError` callExpr
           pure True
-      )
+        )
         `catchError` (\_ -> pure False)
     put st
     pure res

From e9a4fb3622d29b8d63d740805622164a162e62d7 Mon Sep 17 00:00:00 2001
From: Yoshitomo Nakanishi <yurayura.rounin.3@gmail.com>
Date: Wed, 29 Apr 2026 17:11:07 +0900
Subject: [PATCH 10/21] Fix named instance rebase integration

---
 src/Solcore/Frontend/Module/Loader.hs         | 24 ++++++++++++++++++-
 .../named-inst-ambiguous-unqualified.solc     |  4 ++--
 test/examples/cases/named-inst-basic.solc     |  8 +++----
 .../cases/named-inst-class-qualified.solc     |  4 ++--
 test/examples/cases/named-inst-dup-label.solc |  4 ++--
 .../cases/named-inst-no-matching-head.solc    |  2 +-
 test/examples/cases/named-inst-receiver.solc  |  4 ++--
 .../cases/named-inst-shared-label-params.solc |  2 +-
 .../cases/named-inst-shared-label.solc        |  8 +++----
 .../cases/named-inst-two-instances.solc       |  6 ++---
 10 files changed, 44 insertions(+), 22 deletions(-)

diff --git a/src/Solcore/Frontend/Module/Loader.hs b/src/Solcore/Frontend/Module/Loader.hs
index f884c2269..ca86d56bd 100644
--- a/src/Solcore/Frontend/Module/Loader.hs
+++ b/src/Solcore/Frontend/Module/Loader.hs
@@ -1452,6 +1452,14 @@ renameExpFunctionCalls renameMap (ExpName me n es) =
       | me == Nothing = Map.findWithDefault n n renameMap
       | otherwise = n
     es' = map (renameExpFunctionCalls renameMap) es
+renameExpFunctionCalls renameMap (ExpNameAt me n lbl es) =
+  ExpNameAt me' n' lbl es'
+  where
+    me' = fmap (renameExpFunctionCalls renameMap) me
+    n'
+      | me == Nothing = Map.findWithDefault n n renameMap
+      | otherwise = n
+    es' = map (renameExpFunctionCalls renameMap) es
 renameExpFunctionCalls renameMap (ExpVar me n) =
   case qualifiedMemberName me n of
     Just qn ->
@@ -1613,6 +1621,12 @@ renameExpTypeRefs renameMap (ExpName me n es) =
     (renameMemberQualifierTypeRefs renameMap <$> me)
     n
     (map (renameExpTypeRefs renameMap) es)
+renameExpTypeRefs renameMap (ExpNameAt me n lbl es) =
+  ExpNameAt
+    (renameMemberQualifierTypeRefs renameMap <$> me)
+    n
+    lbl
+    (map (renameExpTypeRefs renameMap) es)
 renameExpTypeRefs renameMap (ExpVar Nothing n) =
   ExpVar
     (sameNameConstructorQualifier renameMap n)
@@ -1720,9 +1734,10 @@ renameClassTypeRefs renameMap (Class bvs ctx n pvs mv sigs) =
     (map (renameSignatureTypeRefs renameMap) sigs)
 
 renameInstanceTypeRefs :: Map Name Name -> Instance -> Instance
-renameInstanceTypeRefs renameMap (Instance d vs ctx n pts mt fns) =
+renameInstanceTypeRefs renameMap (Instance d lbl vs ctx n pts mt fns) =
   Instance
     d
+    lbl
     (map (renameTyTypeRefs renameMap) vs)
     (map (renamePredTypeRefs renameMap) ctx)
     n
@@ -2224,6 +2239,13 @@ expFunctionRefs (ExpName me n es) =
       case me of
         Nothing -> [n]
         _ -> maybe [] pure (qualifiedMemberName me n)
+expFunctionRefs (ExpNameAt me n _ es) =
+  directRef ++ maybe [] expFunctionRefs me ++ concatMap expFunctionRefs es
+  where
+    directRef =
+      case me of
+        Nothing -> [n]
+        _ -> maybe [] pure (qualifiedMemberName me n)
 expFunctionRefs (ExpVar me n) =
   directRef ++ maybe [] expFunctionRefs me
   where
diff --git a/test/examples/cases/named-inst-ambiguous-unqualified.solc b/test/examples/cases/named-inst-ambiguous-unqualified.solc
index 3f304fda2..acb06f0c6 100644
--- a/test/examples/cases/named-inst-ambiguous-unqualified.solc
+++ b/test/examples/cases/named-inst-ambiguous-unqualified.solc
@@ -13,13 +13,13 @@ forall a . class a : Bar {
 
 instance [shared] word : Foo {
   function run(x : word) -> Bool {
-    return True;
+    return Bool.True;
   }
 }
 
 instance [shared] word : Bar {
   function run(x : word) -> Bool {
-    return False;
+    return Bool.False;
   }
 }
 
diff --git a/test/examples/cases/named-inst-basic.solc b/test/examples/cases/named-inst-basic.solc
index cb1eb1ea8..0f236fdf4 100644
--- a/test/examples/cases/named-inst-basic.solc
+++ b/test/examples/cases/named-inst-basic.solc
@@ -9,8 +9,8 @@ forall a . class a : Eq {
 instance word : Eq {
   function eq(x : word, y : word) -> Bool {
     match primEqWord(x, y) {
-    | 0 => return False;
-    | _ => return True;
+    | 0 => return Bool.False;
+    | _ => return Bool.True;
     }
   }
 }
@@ -18,8 +18,8 @@ instance word : Eq {
 instance [myEq] word : Eq {
   function eq(x : word, y : word) -> Bool {
     match primEqWord(x, y) {
-    | 0 => return False;
-    | _ => return True;
+    | 0 => return Bool.False;
+    | _ => return Bool.True;
     }
   }
 }
diff --git a/test/examples/cases/named-inst-class-qualified.solc b/test/examples/cases/named-inst-class-qualified.solc
index fc3abcedb..7f97819a6 100644
--- a/test/examples/cases/named-inst-class-qualified.solc
+++ b/test/examples/cases/named-inst-class-qualified.solc
@@ -12,13 +12,13 @@ forall a . class a : Bar {
 
 instance [shared] word : Foo {
   function run(x : word) -> Bool {
-    return True;
+    return Bool.True;
   }
 }
 
 instance [shared] word : Bar {
   function run(x : word) -> Bool {
-    return False;
+    return Bool.False;
   }
 }
 
diff --git a/test/examples/cases/named-inst-dup-label.solc b/test/examples/cases/named-inst-dup-label.solc
index ce5422eaf..c52c1e74f 100644
--- a/test/examples/cases/named-inst-dup-label.solc
+++ b/test/examples/cases/named-inst-dup-label.solc
@@ -8,13 +8,13 @@ forall a . class a : Eq {
 
 instance [dupLabel] word : Eq {
   function eq(x : word, y : word) -> Bool {
-    return True;
+    return Bool.True;
   }
 }
 
 instance [dupLabel] word : Eq {
   function eq(x : word, y : word) -> Bool {
-    return False;
+    return Bool.False;
   }
 }
 
diff --git a/test/examples/cases/named-inst-no-matching-head.solc b/test/examples/cases/named-inst-no-matching-head.solc
index 721f804c7..18058d49b 100644
--- a/test/examples/cases/named-inst-no-matching-head.solc
+++ b/test/examples/cases/named-inst-no-matching-head.solc
@@ -21,6 +21,6 @@ instance [shared] word : Pick(Bool) {
 
 contract NamedInstNoMatchingHead {
   function main() -> Bool {
-    return pick@{shared}(1, F);
+    return pick@{shared}(1, Flag.F);
   }
 }
diff --git a/test/examples/cases/named-inst-receiver.solc b/test/examples/cases/named-inst-receiver.solc
index 9c233273a..5e2dea80e 100644
--- a/test/examples/cases/named-inst-receiver.solc
+++ b/test/examples/cases/named-inst-receiver.solc
@@ -9,8 +9,8 @@ forall a . class a : Eq {
 instance [myEq] word : Eq {
   function eq(x : word, y : word) -> Bool {
     match primEqWord(x, y) {
-    | 0 => return False;
-    | _ => return True;
+    | 0 => return Bool.False;
+    | _ => return Bool.True;
     }
   }
 }
diff --git a/test/examples/cases/named-inst-shared-label-params.solc b/test/examples/cases/named-inst-shared-label-params.solc
index 5680a6f27..b1e312bd4 100644
--- a/test/examples/cases/named-inst-shared-label-params.solc
+++ b/test/examples/cases/named-inst-shared-label-params.solc
@@ -22,7 +22,7 @@ instance [shared] word : Pick(Bool) {
 contract NamedInstSharedLabelParams {
   function main() -> Bool {
     let x : word = pick@{shared}(1, 2);
-    let y : Bool = pick@{shared}(1, True);
+    let y : Bool = pick@{shared}(1, Bool.True);
     return y;
   }
 }
diff --git a/test/examples/cases/named-inst-shared-label.solc b/test/examples/cases/named-inst-shared-label.solc
index 90a3d12ea..52f1d34e4 100644
--- a/test/examples/cases/named-inst-shared-label.solc
+++ b/test/examples/cases/named-inst-shared-label.solc
@@ -8,15 +8,15 @@ forall a . class a : Eq {
 
 instance [shared] word : Eq {
   function eq(x : word, y : word) -> Bool {
-    return True;
+    return Bool.True;
   }
 }
 
 instance [shared] Bool : Eq {
   function eq(x : Bool, y : Bool) -> Bool {
     match x, y {
-    | True, True => return True;
-    | _, _ => return False;
+    | Bool.True, Bool.True => return Bool.True;
+    | _, _ => return Bool.False;
     }
   }
 }
@@ -24,7 +24,7 @@ instance [shared] Bool : Eq {
 contract NamedInstSharedLabel {
   function main() -> Bool {
     let x : Bool = eq@{shared}(1, 2);
-    let y : Bool = eq@{shared}(True, True);
+    let y : Bool = eq@{shared}(Bool.True, Bool.True);
     return y;
   }
 }
diff --git a/test/examples/cases/named-inst-two-instances.solc b/test/examples/cases/named-inst-two-instances.solc
index 341f349cb..429fef761 100644
--- a/test/examples/cases/named-inst-two-instances.solc
+++ b/test/examples/cases/named-inst-two-instances.solc
@@ -10,8 +10,8 @@ forall a . class a : Eq {
 instance [strictEq] word : Eq {
   function eq(x : word, y : word) -> Bool {
     match primEqWord(x, y) {
-    | 0 => return False;
-    | _ => return True;
+    | 0 => return Bool.False;
+    | _ => return Bool.True;
     }
   }
 }
@@ -19,7 +19,7 @@ instance [strictEq] word : Eq {
 // Named instance: always equal (trivial equality)
 instance [trivialEq] word : Eq {
   function eq(x : word, y : word) -> Bool {
-    return True;
+    return Bool.True;
   }
 }
 

From 819680650b9376fcf6531918341a4590776524c0 Mon Sep 17 00:00:00 2001
From: Yoshitomo Nakanishi <yurayura.rounin.3@gmail.com>
Date: Thu, 30 Apr 2026 11:17:23 +0900
Subject: [PATCH 11/21] Treat named instances as declarations

---
 src/Solcore/Frontend/Module/Loader.hs         | 119 ++++++++++++++++--
 src/Solcore/Frontend/Parser/SolcoreParser.y   |   4 +-
 src/Solcore/Frontend/Syntax/NameResolution.hs |  34 +++--
 src/Solcore/Frontend/TypeInference/TcEnv.hs   |   2 +-
 src/Solcore/Frontend/TypeInference/TcMonad.hs |   6 +-
 src/Solcore/Frontend/TypeInference/TcStmt.hs  |  68 ++++------
 test/Cases.hs                                 |   5 +-
 .../cases/named-inst-class-qualified.solc     |  10 +-
 .../cases/named-inst-shared-label-params.solc |   4 +-
 .../cases/named-inst-shared-label.solc        |   2 +-
 test/imports/namedinst/a.solc                 |  11 ++
 test/imports/namedinst/b.solc                 |  11 ++
 test/imports/namedinst_qualified_main.solc    |  10 ++
 13 files changed, 201 insertions(+), 85 deletions(-)
 create mode 100644 test/imports/namedinst/a.solc
 create mode 100644 test/imports/namedinst/b.solc
 create mode 100644 test/imports/namedinst_qualified_main.solc

diff --git a/src/Solcore/Frontend/Module/Loader.hs b/src/Solcore/Frontend/Module/Loader.hs
index ca86d56bd..5577b0eeb 100644
--- a/src/Solcore/Frontend/Module/Loader.hs
+++ b/src/Solcore/Frontend/Module/Loader.hs
@@ -626,7 +626,7 @@ publicTopDeclsForModule :: ModuleGraph -> Mod.ModuleId -> Either String [TopDecl
 publicTopDeclsForModule graph modulePath = do
   publicDecls <- publicItemDeclsForModule graph modulePath
   unit <- lookupLoadedModule graph modulePath
-  pure (publicDecls ++ [decl | decl@(TInstDef _) <- topDeclsFrom unit])
+  pure (uniqueTopDecls (publicDecls ++ [decl | decl@(TInstDef _) <- topDeclsFrom unit]))
 
 publicModuleInterface :: ModuleGraph -> Mod.ModuleId -> Either String ModulePublicInterface
 publicModuleInterface graph modulePath = do
@@ -1124,7 +1124,7 @@ selectPublicItemDecls itemRefs topLevelDecls =
     filteredDecls = filter isPublicItemTopDecl topLevelDecls
 
 isPublicItemTopDecl :: TopDecl -> Bool
-isPublicItemTopDecl (TInstDef _) = False
+isPublicItemTopDecl (TInstDef inst) = isJust (instLabel inst)
 isPublicItemTopDecl d = isImportableTopDecl d
 
 isImportableTopDecl :: TopDecl -> Bool
@@ -1138,7 +1138,7 @@ topDeclNames (TSym (TySym n _ _)) = [n]
 topDeclNames (TClassDef (Class _ _ n _ _ _)) = [n]
 topDeclNames (TContr (Contract n _ _)) = [n]
 topDeclNames (TDataDef (DataTy n _ _)) = [n]
-topDeclNames (TInstDef _) = []
+topDeclNames (TInstDef inst) = maybe [] pure (instLabel inst)
 topDeclNames (TExportDecl _) = []
 topDeclNames (TPragmaDecl _) = []
 
@@ -1297,6 +1297,8 @@ qualifiedImportStubDecls graph (imp, modulePath) =
       pure $
         qualifiedFunctionStubDecls qualifier cunit
           ++ qualifiedTypeStubDecls qualifier cunit
+          ++ qualifiedClassDecls qualifier cunit
+          ++ qualifiedNamedInstanceDecls qualifier cunit
           ++ nestedDecls
 
     stubNestedModule qualifier (ExportedModuleBinding bindingName targetModule) =
@@ -1403,6 +1405,81 @@ qualifiedFunctionStubDecls qualifier cunit =
     | TFunDef fd <- topDeclsFrom cunit
   ]
 
+qualifiedNamedInstanceDecls :: Name -> CompUnit -> [TopDecl]
+qualifiedNamedInstanceDecls qualifier cunit =
+  [ TInstDef (qualifyNamedInstanceLabel qualifier (renameInstanceClassRefs classRenameMap (renameInstanceTypeRefs typeRenameMap inst)))
+    | TInstDef inst <- topDeclsFrom cunit,
+      isJust (instLabel inst)
+  ]
+  where
+    classRenameMap = localClassRenameMap qualifier (topDeclsFrom cunit)
+    typeRenameMap = localTypeRenameMap qualifier (topDeclsFrom cunit)
+
+qualifiedClassDecls :: Name -> CompUnit -> [TopDecl]
+qualifiedClassDecls qualifier cunit =
+  [ TClassDef (renameClassDeclClassRefs classRenameMap cls {className = renamedClassName (className cls)})
+    | TClassDef cls <- topDeclsFrom cunit
+  ]
+  where
+    classRenameMap = localClassRenameMap qualifier (topDeclsFrom cunit)
+    renamedClassName n = Map.findWithDefault n n classRenameMap
+
+localClassRenameMap :: Name -> [TopDecl] -> Map Name Name
+localClassRenameMap qualifier topDecls =
+  Map.fromList
+    [ (n, QualName qualifier (show n))
+      | TClassDef (Class _ _ n _ _ _) <- topDecls
+    ]
+
+localTypeRenameMap :: Name -> [TopDecl] -> Map Name Name
+localTypeRenameMap qualifier topDecls =
+  Map.fromList
+    [ (n, QualName qualifier (show n))
+      | d <- topDecls,
+        n <- topDeclImportedTypeNames d
+    ]
+
+qualifyTopDeclNamedInstanceLabel :: Name -> TopDecl -> TopDecl
+qualifyTopDeclNamedInstanceLabel qualifier (TInstDef inst)
+  | isJust (instLabel inst) = TInstDef (qualifyNamedInstanceLabel qualifier inst)
+qualifyTopDeclNamedInstanceLabel _ decl = decl
+
+qualifyNamedInstanceLabel :: Name -> Instance -> Instance
+qualifyNamedInstanceLabel qualifier inst =
+  inst {instLabel = QualName qualifier . show <$> instLabel inst}
+
+renameInstanceClassRefs :: Map Name Name -> Instance -> Instance
+renameInstanceClassRefs renameMap (Instance d lbl vs ctx n pts mt fns) =
+  Instance
+    d
+    lbl
+    vs
+    (map (renamePredClassRefs renameMap) ctx)
+    (renameClassName renameMap n)
+    pts
+    mt
+    (map (renameFunDefClassRefs renameMap) fns)
+
+renameClassDeclClassRefs :: Map Name Name -> Class -> Class
+renameClassDeclClassRefs renameMap (Class bvs ctx n pvs mv sigs) =
+  Class bvs (map (renamePredClassRefs renameMap) ctx) n pvs mv (map (renameSignatureClassRefs renameMap) sigs)
+
+renameFunDefClassRefs :: Map Name Name -> FunDef -> FunDef
+renameFunDefClassRefs renameMap (FunDef sig body) =
+  FunDef (renameSignatureClassRefs renameMap sig) body
+
+renameSignatureClassRefs :: Map Name Name -> Signature -> Signature
+renameSignatureClassRefs renameMap (Signature vs ctx n ps mt) =
+  Signature vs (map (renamePredClassRefs renameMap) ctx) n ps mt
+
+renamePredClassRefs :: Map Name Name -> Pred -> Pred
+renamePredClassRefs renameMap (InCls n t ts) =
+  InCls (renameClassName renameMap n) t ts
+
+renameClassName :: Map Name Name -> Name -> Name
+renameClassName renameMap n =
+  Map.findWithDefault n n renameMap
+
 renameBodyFunctionCalls :: Map Name Name -> Body -> Body
 renameBodyFunctionCalls renameMap =
   map (renameStmtFunctionCalls renameMap)
@@ -1874,7 +1951,7 @@ toValidationImportStub (TContr (Contract n _ _)) =
   Just (TContr (Contract n [] []))
 toValidationImportStub (TDataDef (DataTy n _ cs)) =
   Just (TDataDef (DataTy n [] [Constr (constrName c) [] | c <- cs]))
-toValidationImportStub (TInstDef _) = Nothing
+toValidationImportStub d@(TInstDef _) = Just d
 toValidationImportStub (TExportDecl _) = Nothing
 toValidationImportStub (TPragmaDecl _) = Nothing
 
@@ -1905,7 +1982,8 @@ strictCompileImportedDeclsWithSurfaces compileSurfaces collidingTypeNames graph
       publicDecls <- publicTopDeclsForModule graph modulePath
       allDecls <- compileTargetTopDecls compileSurfaces graph modulePath
       let allFunctionDecls = [fd | TFunDef fd <- allDecls]
-          supportNonFunctionDecls = filter (not . isFunctionTopDecl) allDecls
+          selectedNames = selectedNamesFromAvailable (uniqueNames (concatMap topDeclNames publicDecls)) selector
+          supportNonFunctionDecls = filter (isImportOnlySupportDecl selectedNames) allDecls
           allFunctionNames = Set.fromList [sigName (funSignature fd) | fd <- allFunctionDecls]
           renameMap = importedFunctionRenameMap moduleName allDecls
           typeRenameMap = importedTypeRenameMap collidingTypeNames moduleName publicDecls
@@ -1917,8 +1995,7 @@ strictCompileImportedDeclsWithSurfaces compileSurfaces collidingTypeNames graph
                 | fd <- allFunctionDecls
               ]
       let selectedPublicDecls =
-            let names = selectedNamesFromAvailable (uniqueNames (concatMap topDeclNames publicDecls)) selector
-             in mapMaybe (selectTopDecl names) publicDecls
+            mapMaybe (selectTopDecl selectedNames) publicDecls
           selectedFunctionNames =
             [ sigName (funSignature fd)
               | TFunDef fd <- selectedPublicDecls
@@ -1944,6 +2021,13 @@ strictCompileImportedDeclsWithSurfaces compileSurfaces collidingTypeNames graph
               renamedSupportNonFunctionDecls
         )
 
+    isImportOnlySupportDecl selectedNames (TInstDef inst) =
+      case instLabel inst of
+        Nothing -> True
+        Just lbl -> lbl `elem` selectedNames
+    isImportOnlySupportDecl _ d =
+      not (isFunctionTopDecl d)
+
     moduleImportCompileDecls qualifier targetModule = do
       moduleBindings <- publicModuleBindingsForModule graph targetModule
       publicDecls <- publicTopDeclsForModule graph targetModule
@@ -1979,7 +2063,10 @@ strictCompileImportedDeclsWithSurfaces compileSurfaces collidingTypeNames graph
             ]
           localSupportDecls =
             map
-              (renameTopDeclTypeRefs typeRenameMap . renameTopDeclFunctionCalls renameMap)
+              ( qualifyTopDeclNamedInstanceLabel qualifier
+                  . renameTopDeclTypeRefs typeRenameMap
+                  . renameTopDeclFunctionCalls renameMap
+              )
               supportNonFunctionDecls
           localSupportFunctionDecls =
             concatMap (qualifySupportImpl renameMap typeRenameMap qualifier) extraSupportFunctions
@@ -2402,9 +2489,9 @@ dedupeImportedInstanceDecls =
       | otherwise = (instanceDeclHeadKey inst : seenHeads, d : acc)
     step (seenHeads, acc) d = (seenHeads, d : acc)
 
-instanceDeclHeadKey :: Instance -> (Bool, Name, [Ty], Ty)
+instanceDeclHeadKey :: Instance -> (Maybe Name, Bool, Name, [Ty], Ty)
 instanceDeclHeadKey inst =
-  (instDefault inst, instName inst, paramsTy inst, mainTy inst)
+  (instLabel inst, instDefault inst, instName inst, paramsTy inst, mainTy inst)
 
 topDeclTermNames :: TopDecl -> [Name]
 topDeclTermNames (TFunDef (FunDef sig _)) = [sigName sig]
@@ -2446,8 +2533,9 @@ selectTopDecl names d@(TContr (Contract n _ _))
 selectTopDecl names (TDataDef (DataTy n ts cs))
   | n `elem` names = Just (TDataDef (DataTy n ts cs))
   | otherwise = Nothing
-selectTopDecl _ d@(TInstDef _) =
-  Just d
+selectTopDecl names d@(TInstDef inst)
+  | maybe False (`elem` names) (instLabel inst) = Just d
+  | otherwise = Nothing
 selectTopDecl _ (TExportDecl _) =
   Nothing
 selectTopDecl _ (TPragmaDecl _) =
@@ -2487,7 +2575,12 @@ selectTopDeclForExportRef itemRef (TDataDef (DataTy n ts cs))
           Just (TDataDef (DataTy n ts (filterVisibleConstructors visibleConstructors cs)))
         Nothing ->
           Nothing
-selectTopDeclForExportRef _ (TInstDef _) = Nothing
+selectTopDeclForExportRef itemRef d@(TInstDef inst)
+  | exportedItemConstructors itemRef == Nothing,
+    Just (exportedItemName itemRef) == instLabel inst =
+      Just d
+  | otherwise =
+      Nothing
 selectTopDeclForExportRef _ (TExportDecl _) = Nothing
 selectTopDeclForExportRef _ (TPragmaDecl _) = Nothing
 
diff --git a/src/Solcore/Frontend/Parser/SolcoreParser.y b/src/Solcore/Frontend/Parser/SolcoreParser.y
index dc66cb62e..ac7449b14 100644
--- a/src/Solcore/Frontend/Parser/SolcoreParser.y
+++ b/src/Solcore/Frontend/Parser/SolcoreParser.y
@@ -436,8 +436,8 @@ Expr : Name FunArgs                                {ExpName Nothing $1 $2}
      | '!' Expr                                    {ExpLNot $2 }
      | Conditional                                 {$1}
      | '@' Type                                    {ExpAt $2}
-     | Name '@{' identifier '}' '(' ExprCommaList ')' { ExpNameAt Nothing $1 (Name $3) $6 }
-     | Expr '.' Name '@{' identifier '}' '(' ExprCommaList ')' { ExpNameAt (Just $1) $3 (Name $5) $8 }
+     | Name '@{' TypeName '}' '(' ExprCommaList ')' { ExpNameAt Nothing $1 $3 $6 }
+     | Expr '.' Name '@{' TypeName '}' '(' ExprCommaList ')' { ExpNameAt (Just $1) $3 $5 $8 }
 
 Conditional :: { Exp }
 Conditional : 'if' Expr 'then' Expr 'else' Expr    {ExpCond $2 $4 $6}
diff --git a/src/Solcore/Frontend/Syntax/NameResolution.hs b/src/Solcore/Frontend/Syntax/NameResolution.hs
index b1898b87c..5d282ef2e 100644
--- a/src/Solcore/Frontend/Syntax/NameResolution.hs
+++ b/src/Solcore/Frontend/Syntax/NameResolution.hs
@@ -77,6 +77,7 @@ validateDuplicateNamespaces :: [S.TopDecl] -> Either String ()
 validateDuplicateNamespaces ds = do
   ensureNoDuplicateNames "type namespace" (topLevelTypeNames ds)
   ensureNoDuplicateNames "term namespace" (topLevelTermNames ds)
+  ensureNoDuplicateNames "named instance namespace" (topLevelNamedInstanceNames ds)
   mapM_ validateContractDuplicates [c | S.TContr c <- ds]
 
 validateContractDuplicates :: S.Contract -> Either String ()
@@ -104,6 +105,12 @@ topLevelTermNames = concatMap collect
       map (qualifiedConstructorName tyCon . S.constrName) cons
     collect _ = []
 
+topLevelNamedInstanceNames :: [S.TopDecl] -> [Name]
+topLevelNamedInstanceNames = concatMap collect
+  where
+    collect (S.TInstDef (S.Instance _ (Just lbl) _ _ _ _ _ _)) = [lbl]
+    collect _ = []
+
 contractTermNames :: [S.ContractDecl] -> [Name]
 contractTermNames = concatMap collect
   where
@@ -834,6 +841,7 @@ data DeclType
   | TTyCon
   | TTyVar
   | TModule
+  | TNamedInstance
   deriving (Eq, Show)
 
 data Env
@@ -947,13 +955,14 @@ addTopDecl (S.TExportDecl _) env = env
 addTopDecl (S.TInstDef (S.Instance _ (Just lbl) _ _ _ _ _ funs)) env =
   env
     { scopeEnv =
-        foldr
-          ( \fd ac ->
-              let qn = QualName lbl (pretty (S.sigName (S.funSignature fd)))
-               in Map.insert qn TFunction ac
-          )
-          (scopeEnv env)
-          funs
+        Map.insert lbl TNamedInstance $
+          foldr
+            ( \fd ac ->
+                let qn = QualName lbl (pretty (S.sigName (S.funSignature fd)))
+                 in Map.insert qn TFunction ac
+            )
+            (scopeEnv env)
+            funs
     }
 addTopDecl _ env = env
 
@@ -968,16 +977,15 @@ addQualifiedModules _ env = env
 
 resolveNamedCall :: Maybe (Exp Name) -> Name -> Name -> [Exp Name] -> ResolveM (Exp Name)
 resolveNamedCall me n lbl es = do
-  let qn = QualName lbl (pretty n)
-      args = maybe es (: es) me
-  dt <- lookupName qn
+  let args = maybe es (: es) me
+  dt <- lookupName lbl
   case dt of
-    Just TFunction -> pure (Call Nothing n (Just lbl) args)
+    Just TNamedInstance -> pure (Call Nothing n (Just lbl) args)
     _ ->
       throwError $
-        "Unknown named instance label '"
+        "Unknown named instance '"
           ++ pretty lbl
-          ++ "' for method '"
+          ++ "' for call '"
           ++ pretty n
           ++ "'"
 
diff --git a/src/Solcore/Frontend/TypeInference/TcEnv.hs b/src/Solcore/Frontend/TypeInference/TcEnv.hs
index b25257b59..f56df45b6 100644
--- a/src/Solcore/Frontend/TypeInference/TcEnv.hs
+++ b/src/Solcore/Frontend/TypeInference/TcEnv.hs
@@ -93,7 +93,7 @@ data TcEnv
   { ctx :: Env, -- Variable environment
     instEnv :: InstTable, -- Instance Environment
     defaultEnv :: DefTable, -- Default instance environment
-    namedInstEnv :: Map Name [Instance Name], -- Named instance environment (by label)
+    namedInstEnv :: Map Name (Instance Name), -- Named instance environment (by declaration name)
     typeTable :: TypeTable, -- Type information environment
     synTable :: SynTable, -- Type synonym environment
     classTable :: ClassTable, -- Class information table
diff --git a/src/Solcore/Frontend/TypeInference/TcMonad.hs b/src/Solcore/Frontend/TypeInference/TcMonad.hs
index 0b531d7ad..5a2c2c26b 100644
--- a/src/Solcore/Frontend/TypeInference/TcMonad.hs
+++ b/src/Solcore/Frontend/TypeInference/TcMonad.hs
@@ -551,10 +551,10 @@ addDefaultInstance n inst =
 
 addNamedInstance :: Name -> Instance Name -> TcM ()
 addNamedInstance label inst =
-  modify (\st -> st {namedInstEnv = Map.insertWith (++) label [inst] (namedInstEnv st)})
+  modify (\st -> st {namedInstEnv = Map.insert label inst (namedInstEnv st)})
 
-askNamedInstances :: Name -> TcM [Instance Name]
-askNamedInstances label = Map.findWithDefault [] label <$> gets namedInstEnv
+askNamedInstance :: Name -> TcM (Maybe (Instance Name))
+askNamedInstance label = Map.lookup label <$> gets namedInstEnv
 
 maybeToTcM :: String -> Maybe a -> TcM a
 maybeToTcM s Nothing = throwError s
diff --git a/src/Solcore/Frontend/TypeInference/TcStmt.hs b/src/Solcore/Frontend/TypeInference/TcStmt.hs
index e3ac066cf..4b23240c3 100644
--- a/src/Solcore/Frontend/TypeInference/TcStmt.hs
+++ b/src/Solcore/Frontend/TypeInference/TcStmt.hs
@@ -1087,12 +1087,14 @@ checkInstance idef@(Instance d lbl vs predCtx n ts t funs) =
           then addDefaultInstance n ninst
           else addInstance n ninst
       Just label -> do
-        -- Named instances: skip overlap check, register by label.
-        -- Reusing a label is allowed as long as the instance head differs.
-        existing <- askNamedInstances label
-        unless (all (differentNamedInstHead idef) existing) $
+        when d $
           throwError $
-            "Duplicate named instance label/head combination: " ++ pretty label
+            "Named default instances are not supported: " ++ pretty label
+        -- Named instances are declaration names, so the label is unique in scope.
+        existing <- askNamedInstance label
+        unless (isNothing existing) $
+          throwError $
+            "Duplicate named instance name: " ++ pretty label
         addNamedInstance label idef
 
 maybeExpandSynonym :: Ty -> TcM Ty
@@ -1342,10 +1344,13 @@ tcCallNamed :: Maybe (Exp Name) -> Name -> Name -> [Exp Name] -> TcM (Exp Id, [P
 tcCallNamed me n lbl args =
   do
     let callExpr = Call me n (Just lbl) args
-    namedInsts <- askNamedInstances lbl
-    when (null namedInsts) $
-      throwError $
-        "Unknown named instance label: " ++ pretty lbl
+    namedInst <-
+      askNamedInstance lbl >>= \mInst ->
+        case mInst of
+          Just inst -> pure inst
+          Nothing ->
+            throwError $
+              "Unknown named instance: " ++ pretty lbl
     mrecv <- mapM tcExp me
     (es', pss', ts') <- unzip3 <$> mapM tcExp args
     let recvArgs = maybe [] (\(e', _, _) -> [e']) mrecv
@@ -1353,40 +1358,20 @@ tcCallNamed me n lbl args =
         recvTys = maybe [] (\(_, _, ty0) -> [ty0]) mrecv
         allArgs = recvArgs ++ es'
         allTys = recvTys ++ ts'
-        methodInsts = filter (hasNamedMethod n) namedInsts
-    when (null methodInsts) $
+    unless (hasNamedMethod n namedInst) $
       throwError $
         unwords
           ["Method", pretty n, "not found in named instance", pretty lbl]
-    matches <- filterM (matchesNamedCall callExpr n lbl allTys) methodInsts
-    case matches of
-      [] ->
-        throwError $
-          unwords
-            [ "No named instance labelled",
-              pretty lbl,
-              "matches call to",
-              pretty n
-            ]
-      [inst] -> tcCallNamedWithInst callExpr n lbl recvPreds allArgs pss' allTys inst
-      _ ->
-        throwError $
-          unlines $
-            [ unwords
-                [ "Ambiguous named instance label",
-                  pretty lbl,
-                  "for method",
-                  pretty n
-                ],
-              "Matching heads:"
-            ]
-              ++ map (("  " ++) . pretty . namedInstPred) matches
-
-differentNamedInstHead :: Instance Name -> Instance Name -> Bool
-differentNamedInstHead inst inst' =
-  instName inst /= instName inst'
-    || mainTy inst /= mainTy inst'
-    || paramsTy inst /= paramsTy inst'
+    matches <- matchesNamedCall callExpr n lbl allTys namedInst
+    unless matches $
+      throwError $
+        unwords
+          [ "Named instance",
+            pretty lbl,
+            "does not match call to",
+            pretty n
+          ]
+    tcCallNamedWithInst callExpr n lbl recvPreds allArgs pss' allTys namedInst
 
 hasNamedMethod :: Name -> Instance Name -> Bool
 hasNamedMethod n inst =
@@ -1400,9 +1385,6 @@ splitNamedMethod :: Name -> (Maybe Name, Name)
 splitNamedMethod (QualName cls meth) = (Just cls, Name meth)
 splitNamedMethod n = (Nothing, n)
 
-namedInstPred :: Instance Name -> Pred
-namedInstPred inst = InCls (instName inst) (mainTy inst) (paramsTy inst)
-
 namedMethodScheme :: Name -> Name -> Instance Name -> TcM Scheme
 namedMethodScheme n lbl inst =
   do
diff --git a/test/Cases.hs b/test/Cases.hs
index 71db3e217..a34352f54 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -145,6 +145,7 @@ imports =
       runImportSuccess "dupqual_main.solc",
       runImportSuccess "dupqual_module_main.solc",
       runImportSuccess "private_helper_main.solc",
+      runImportSuccess "namedinst_qualified_main.solc",
       runImportSuccess "module_qualified_constructor.solc",
       runImportSuccess "module_qualified_constructor_pattern.solc",
       runImportSuccess "module_qualified_constructor_alias.solc",
@@ -404,9 +405,9 @@ cases =
       runTestExpectingFailure "named-inst-ambiguous-unqualified.solc" caseFolder,
       runTestForFile "named-inst-class-qualified.solc" caseFolder,
       runTestExpectingFailure "named-inst-no-matching-head.solc" caseFolder,
-      runTestForFile "named-inst-shared-label-params.solc" caseFolder,
+      runTestExpectingFailure "named-inst-shared-label-params.solc" caseFolder,
       runTestForFile "named-inst-receiver.solc" caseFolder,
-      runTestForFile "named-inst-shared-label.solc" caseFolder,
+      runTestExpectingFailure "named-inst-shared-label.solc" caseFolder,
       runTestForFile "named-inst-two-instances.solc" caseFolder,
       runTestExpectingFailure "named-inst-unknown-label.solc" caseFolder,
       runTestExpectingFailure "named-inst-dup-label.solc" caseFolder,
diff --git a/test/examples/cases/named-inst-class-qualified.solc b/test/examples/cases/named-inst-class-qualified.solc
index 7f97819a6..ff4dcc6fc 100644
--- a/test/examples/cases/named-inst-class-qualified.solc
+++ b/test/examples/cases/named-inst-class-qualified.solc
@@ -1,4 +1,4 @@
-// Class-qualified named calls should disambiguate instances sharing a label.
+// Class-qualified named calls should dispatch through the selected instance.
 
 data Bool = True | False;
 
@@ -10,13 +10,13 @@ forall a . class a : Bar {
   function run(x : a) -> Bool;
 }
 
-instance [shared] word : Foo {
+instance [fooShared] word : Foo {
   function run(x : word) -> Bool {
     return Bool.True;
   }
 }
 
-instance [shared] word : Bar {
+instance [barShared] word : Bar {
   function run(x : word) -> Bool {
     return Bool.False;
   }
@@ -24,8 +24,8 @@ instance [shared] word : Bar {
 
 contract NamedInstClassQualified {
   function main() -> Bool {
-    let x : Bool = Foo.run@{shared}(1);
-    let y : Bool = Bar.run@{shared}(1);
+    let x : Bool = Foo.run@{fooShared}(1);
+    let y : Bool = Bar.run@{barShared}(1);
     return y;
   }
 }
diff --git a/test/examples/cases/named-inst-shared-label-params.solc b/test/examples/cases/named-inst-shared-label-params.solc
index b1e312bd4..1d2ed1dc7 100644
--- a/test/examples/cases/named-inst-shared-label-params.solc
+++ b/test/examples/cases/named-inst-shared-label-params.solc
@@ -1,5 +1,5 @@
-// Reusing a label across the same class/head should work when params are
-// distinguished by explicit method arguments.
+// Reusing a named-instance declaration name in one module is rejected even
+// when the instance heads differ by weak parameters.
 
 data Bool = True | False;
 
diff --git a/test/examples/cases/named-inst-shared-label.solc b/test/examples/cases/named-inst-shared-label.solc
index 52f1d34e4..332d3c1e5 100644
--- a/test/examples/cases/named-inst-shared-label.solc
+++ b/test/examples/cases/named-inst-shared-label.solc
@@ -1,4 +1,4 @@
-// Reusing the same named-instance label for different heads should work.
+// Reusing the same named-instance declaration name in one module is rejected.
 
 data Bool = True | False;
 
diff --git a/test/imports/namedinst/a.solc b/test/imports/namedinst/a.solc
new file mode 100644
index 000000000..df716f9b5
--- /dev/null
+++ b/test/imports/namedinst/a.solc
@@ -0,0 +1,11 @@
+export { Score, byPriority };
+
+forall a . class a : Score {
+  function score(x : a) -> word;
+}
+
+instance [byPriority] word : Score {
+  function score(x : word) -> word {
+    return x;
+  }
+}
diff --git a/test/imports/namedinst/b.solc b/test/imports/namedinst/b.solc
new file mode 100644
index 000000000..072dd5e64
--- /dev/null
+++ b/test/imports/namedinst/b.solc
@@ -0,0 +1,11 @@
+export { Score, byPriority };
+
+forall a . class a : Score {
+  function score(x : a) -> word;
+}
+
+instance [byPriority] word : Score {
+  function score(x : word) -> word {
+    return 2;
+  }
+}
diff --git a/test/imports/namedinst_qualified_main.solc b/test/imports/namedinst_qualified_main.solc
new file mode 100644
index 000000000..c9d1c8841
--- /dev/null
+++ b/test/imports/namedinst_qualified_main.solc
@@ -0,0 +1,10 @@
+import namedinst.a as A;
+import namedinst.b as B;
+
+contract NamedInstQualifiedImport {
+  function main() -> word {
+    let x : word = score@{A.byPriority}(1);
+    let y : word = score@{B.byPriority}(1);
+    return y;
+  }
+}

From 1d56ee62039b5b69d828434604aea6ea89fa1bab Mon Sep 17 00:00:00 2001
From: Yoshitomo Nakanishi <yurayura.rounin.3@gmail.com>
Date: Thu, 30 Apr 2026 16:42:10 +0900
Subject: [PATCH 12/21] Keep named instances explicit in specialisation

---
 src/Solcore/Backend/Specialise.hs | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/Solcore/Backend/Specialise.hs b/src/Solcore/Backend/Specialise.hs
index 6e7fdb1c8..3805541d0 100644
--- a/src/Solcore/Backend/Specialise.hs
+++ b/src/Solcore/Backend/Specialise.hs
@@ -221,12 +221,13 @@ addInstResolutions :: Instance Id -> SM ()
 addInstResolutions inst = forM_ (instFunctions inst) addMethod
   where
     addMethod fd = do
-      addMethodResolution (instName inst) (mainTy inst) fd
-      -- For named instances, also register under QualName lbl methodName
-      -- so that specExp can find the definition directly by label.
       case instLabel inst of
-        Nothing -> return ()
-        Just lbl -> addNamedInstMethodResolution lbl (mainTy inst) fd
+        Nothing ->
+          addMethodResolution (instName inst) (mainTy inst) fd
+        -- Named instances are explicit evidence and should not participate in
+        -- ordinary method resolution.
+        Just lbl ->
+          addNamedInstMethodResolution lbl (mainTy inst) fd
 
 -- Register a named-instance method under QualName lbl methodUnqualName.
 -- After type inference, method names are QualName className method; we

From e4d28af92155b5b8fcf528468d4db4245aac5e79 Mon Sep 17 00:00:00 2001
From: Yoshitomo Nakanishi <yurayura.rounin.3@gmail.com>
Date: Fri, 1 May 2026 12:09:34 +0900
Subject: [PATCH 13/21] Allow named evidence on constrained calls

---
 src/Solcore/Backend/Specialise.hs             | 124 +++++++++++++++---
 src/Solcore/Frontend/TypeInference/TcStmt.hs  | 103 ++++++++++++---
 test/Cases.hs                                 |   1 +
 .../cases/named-inst-constrained-call.solc    |  27 ++++
 4 files changed, 218 insertions(+), 37 deletions(-)
 create mode 100644 test/examples/cases/named-inst-constrained-call.solc

diff --git a/src/Solcore/Backend/Specialise.hs b/src/Solcore/Backend/Specialise.hs
index 3805541d0..fb908b38f 100644
--- a/src/Solcore/Backend/Specialise.hs
+++ b/src/Solcore/Backend/Specialise.hs
@@ -10,7 +10,7 @@ import Control.Monad
 import Control.Monad.Except
 import Control.Monad.State
 import Data.Generics
-import Data.List (intercalate, union, (\\))
+import Data.List (find, intercalate, union, (\\))
 import Data.Map qualified as Map
 import Data.Maybe (fromMaybe)
 import Solcore.Backend.Mast
@@ -20,7 +20,7 @@ import Solcore.Frontend.Pretty.SolcorePretty
 import Solcore.Frontend.Syntax hiding (decls, name)
 import Solcore.Frontend.TypeInference.Id (Id (..))
 import Solcore.Frontend.TypeInference.NameSupply
-import Solcore.Frontend.TypeInference.TcEnv (TcEnv (ctx, typeTable), TypeInfo (..))
+import Solcore.Frontend.TypeInference.TcEnv (TcEnv (ctx, namedInstEnv, typeTable), TypeInfo (..))
 import Solcore.Frontend.TypeInference.TcUnify (typesDoNotUnify)
 import Solcore.Primitives.Primitives
 
@@ -46,6 +46,7 @@ data SpecState = SpecState
     spGlobalEnv :: TcEnv,
     splocalEnv :: Table Ty,
     spSubst :: TVSubst,
+    spNamedEvidence :: [(Name, Instance Name)],
     spDebug :: Bool,
     spNS :: NameSupply
   }
@@ -91,6 +92,7 @@ initSpecState debugp env =
       spGlobalEnv = env,
       splocalEnv = emptyTable,
       spSubst = emptyTVSubst,
+      spNamedEvidence = [],
       spDebug = debugp,
       spNS = namePool
     }
@@ -183,6 +185,18 @@ extSpSubst subst = modify $ \s -> s {spSubst = spSubst s <> subst}
 atCurrentSubst :: (HasTV a) => a -> SM a
 atCurrentSubst a = flip applytv a <$> getSpSubst
 
+withNamedEvidence :: Name -> SM a -> SM a
+withNamedEvidence lbl action = do
+  env <- gets spGlobalEnv
+  case Map.lookup lbl (namedInstEnv env) of
+    Nothing -> action
+    Just inst -> do
+      saved <- gets spNamedEvidence
+      modify $ \s -> s {spNamedEvidence = (lbl, inst) : saved}
+      result <- action
+      modify $ \s -> s {spNamedEvidence = saved}
+      pure result
+
 addData :: DataTy -> SM ()
 addData dt = modify (\s -> s {spDataTable = Map.insert (dataName dt) dt (spDataTable s)})
 
@@ -325,20 +339,93 @@ addMethodResolution cname ty fd = do
   addResolution qname funType fd'
   debug ["+ addMethodResolution: ", show qname, " / ", show name', " : ", pretty funType]
 
+methodNameString :: Name -> String
+methodNameString (QualName _ meth) = meth
+methodNameString (Name meth) = meth
+
+methodName :: Name -> Name
+methodName = Name . methodNameString
+
+instanceHasMethod :: Name -> Instance a -> Bool
+instanceHasMethod meth inst =
+  any ((== meth) . methodName . sigName . funSignature) (instFunctions inst)
+
+namedEvidenceHasMethod :: Name -> Id -> SM Bool
+namedEvidenceHasMethod lbl i = do
+  env <- gets spGlobalEnv
+  pure $
+    case Map.lookup lbl (namedInstEnv env) of
+      Nothing -> False
+      Just inst ->
+        case idName i of
+          QualName cls _ -> cls == instName inst && hasMethod inst
+          Name _ -> hasMethod inst
+  where
+    hasMethod = instanceHasMethod (methodName (idName i))
+
+explicitNamedEvidenceForCall :: Id -> [TcExp] -> Ty -> SM (Maybe Name)
+explicitNamedEvidenceForCall i args ty =
+  case idName i of
+    QualName cls meth -> do
+      argTypes <- atCurrentSubst (map typeOfTcExp args)
+      ty' <- atCurrentSubst ty
+      let funType = foldr (:->) ty' argTypes
+          methName = Name meth
+      evidences <- gets spNamedEvidence
+      pure $ fst <$> find (matchesNamedEvidence cls methName funType) evidences
+    Name _ -> pure Nothing
+
+matchesNamedEvidence :: Name -> Name -> Ty -> (Name, Instance Name) -> Bool
+matchesNamedEvidence cls meth funType (_, inst) =
+  instName inst == cls
+    && instanceHasMethod meth inst
+    && maybe False (`methodTypeMatches` funType) (namedInstanceMethodType meth inst)
+
+namedInstanceMethodType :: Name -> Instance Name -> Maybe Ty
+namedInstanceMethodType meth inst =
+  typeOfNamedFunDef <$> find ((== meth) . methodName . sigName . funSignature) (instFunctions inst)
+
+typeOfNamedFunDef :: FunDef Name -> Ty
+typeOfNamedFunDef (FunDef sig _) = typeOfNamedSignature sig
+
+typeOfNamedSignature :: Signature Name -> Ty
+typeOfNamedSignature sig =
+  funtype (map typeOfParam (sigParams sig)) returnType
+  where
+    returnType = case sigReturn sig of
+      Just t -> t
+      Nothing -> error ("no return type in signature of: " ++ show (sigName sig))
+    typeOfParam (Typed _ t) = t
+    typeOfParam p = error ("untyped parameter in signature of: " ++ show p)
+
+methodTypeMatches :: Ty -> Ty -> Bool
+methodTypeMatches methodTy callTy =
+  case specmgu methodTy callTy of
+    Right _ -> True
+    Left _ -> False
+
 -- | `specExp` specialises an expression to given type
 specExp :: TcExp -> Ty -> SM TcExp
-specExp (Call Nothing i lbl args) ty = do
+specExp (Call Nothing i Nothing args) ty = do
   -- debug ["> specExp (Call): ", pretty e, " : ", pretty (idType i), " ~> ", pretty ty]
-  -- For named instance calls, resolve via QualName lbl method so the
-  -- specialiser finds the definition registered under that label.
-  let i' = case lbl of
-        Just l ->
-          let meth = case idName i of
-                QualName _ m -> m
-                Name s -> s
-           in i {idName = QualName l meth}
-        Nothing -> i
-  (i'', args') <- specCall i' args ty
+  mlbl <- explicitNamedEvidenceForCall i args ty
+  case mlbl of
+    Just lbl -> specExp (Call Nothing i (Just lbl) args) ty
+    Nothing -> do
+      (i'', args') <- specCall i args ty
+      let e' = Call Nothing i'' Nothing args'
+      -- debug ["< specExp (Call): ", pretty e']
+      return e'
+specExp (Call Nothing i (Just lbl) args) ty = do
+  -- A label can either select a named instance method directly, or supply
+  -- explicit evidence to a constrained function call.
+  isNamedMethod <- namedEvidenceHasMethod lbl i
+  (i'', args') <-
+    if isNamedMethod
+      then do
+        let i' = i {idName = QualName lbl (methodNameString (idName i))}
+        specCall i' args ty
+      else specCallWithEvidence (Just lbl) i args ty
   let e' = Call Nothing i'' Nothing args'
   -- debug ["< specExp (Call): ", pretty e']
   return e'
@@ -381,8 +468,11 @@ specConApp i@(Id _n conTy) args ty = do
 -- | Specialise a function call
 -- given actual arguments and the expected result type
 specCall :: Id -> [TcExp] -> Ty -> SM (Id, [TcExp])
-specCall i@(Id (Name "revert") _) args _ = pure (i, args) -- FIXME
-specCall i args ty = do
+specCall = specCallWithEvidence Nothing
+
+specCallWithEvidence :: Maybe Name -> Id -> [TcExp] -> Ty -> SM (Id, [TcExp])
+specCallWithEvidence _ i@(Id (Name "revert") _) args _ = pure (i, args) -- FIXME
+specCallWithEvidence mEvidence i args ty = do
   i' <- atCurrentSubst i
   ty' <- atCurrentSubst ty
   -- debug ["> specCall: ", pretty i', show args, " : ", pretty ty']
@@ -401,7 +491,9 @@ specCall i args ty = do
       subst <- getSpSubst
       let ty'' = applytv subst fty
       ensureClosed ty'' (Call Nothing i Nothing args) subst
-      name' <- specFunDef fd
+      name' <- case mEvidence of
+        Just lbl -> withNamedEvidence lbl (specFunDef fd)
+        Nothing -> specFunDef fd
       debug ["< specCall: ", pretty name', " : ", show ty'']
       args'' <- atCurrentSubst args'
       return (Id name' ty'', args'')
diff --git a/src/Solcore/Frontend/TypeInference/TcStmt.hs b/src/Solcore/Frontend/TypeInference/TcStmt.hs
index 4b23240c3..1ce70fee1 100644
--- a/src/Solcore/Frontend/TypeInference/TcStmt.hs
+++ b/src/Solcore/Frontend/TypeInference/TcStmt.hs
@@ -1351,27 +1351,88 @@ tcCallNamed me n lbl args =
           Nothing ->
             throwError $
               "Unknown named instance: " ++ pretty lbl
-    mrecv <- mapM tcExp me
-    (es', pss', ts') <- unzip3 <$> mapM tcExp args
-    let recvArgs = maybe [] (\(e', _, _) -> [e']) mrecv
-        recvPreds = maybe [] (\(_, ps0, _) -> ps0) mrecv
-        recvTys = maybe [] (\(_, _, ty0) -> [ty0]) mrecv
-        allArgs = recvArgs ++ es'
-        allTys = recvTys ++ ts'
-    unless (hasNamedMethod n namedInst) $
-      throwError $
-        unwords
-          ["Method", pretty n, "not found in named instance", pretty lbl]
-    matches <- matchesNamedCall callExpr n lbl allTys namedInst
-    unless matches $
-      throwError $
-        unwords
-          [ "Named instance",
-            pretty lbl,
-            "does not match call to",
-            pretty n
-          ]
-    tcCallNamedWithInst callExpr n lbl recvPreds allArgs pss' allTys namedInst
+    if hasNamedMethod n namedInst
+      then do
+        mrecv <- mapM tcExp me
+        (es', pss', ts') <- unzip3 <$> mapM tcExp args
+        let recvArgs = maybe [] (\(e', _, _) -> [e']) mrecv
+            recvPreds = maybe [] (\(_, ps0, _) -> ps0) mrecv
+            recvTys = maybe [] (\(_, _, ty0) -> [ty0]) mrecv
+            allArgs = recvArgs ++ es'
+            allTys = recvTys ++ ts'
+        matches <- matchesNamedCall callExpr n lbl allTys namedInst
+        unless matches $
+          throwError $
+            unwords
+              [ "Named instance",
+                pretty lbl,
+                "does not match call to",
+                pretty n
+              ]
+        tcCallNamedWithInst callExpr n lbl recvPreds allArgs pss' allTys namedInst
+      else tcCallWithNamedEvidence callExpr me n lbl args namedInst
+
+tcCallWithNamedEvidence ::
+  Exp Name ->
+  Maybe (Exp Name) ->
+  Name ->
+  Name ->
+  [Exp Name] ->
+  Instance Name ->
+  TcM (Exp Id, [Pred], Ty)
+tcCallWithNamedEvidence callExpr me n lbl args inst =
+  do
+    (call, ps, ty) <- tcCall me n args
+    matching <- catMaybes <$> mapM (namedInstSolvesWanted inst) ps
+    case matching of
+      [(p, instPreds, evidenceSubst)] ->
+        case call of
+          Call me' i Nothing args' -> do
+            _ <- extSubst evidenceSubst
+            let ps' = apply evidenceSubst (instPreds ++ delete p ps)
+            withCurrentSubst (Call me' i (Just lbl) args', ps', ty)
+          _ ->
+            throwError $ "Internal error: expected a call while checking " ++ pretty callExpr
+      [] ->
+        throwError $
+          unwords
+            [ "Named instance",
+              pretty lbl,
+              "does not match any wanted constraint for",
+              pretty n
+            ]
+      _ ->
+        throwError $
+          unlines
+            [ unwords
+                [ "Named instance",
+                  pretty lbl,
+                  "matches multiple wanted constraints for",
+                  pretty n
+                ],
+              "Use an explicit constraint slot to disambiguate."
+            ]
+
+namedInstSolvesWanted :: Instance Name -> Pred -> TcM (Maybe (Pred, [Pred], Subst))
+namedInstSolvesWanted inst wanted =
+  (Just <$> solvePred)
+    `catchError` (\_ -> pure Nothing)
+  where
+    solvePred = do
+      evidenceSubst <- solveNamedInstPred (namedInstPred inst) wanted
+      pure (wanted, apply evidenceSubst (namedInstContext inst), evidenceSubst)
+
+namedInstPred :: Instance Name -> Pred
+namedInstPred inst = everywhere (mkT toMeta) (InCls (instName inst) (mainTy inst) (paramsTy inst))
+
+namedInstContext :: Instance Name -> [Pred]
+namedInstContext inst = everywhere (mkT toMeta) (instContext inst)
+
+solveNamedInstPred :: Pred -> Pred -> TcM Subst
+solveNamedInstPred (InCls c t ts) (InCls c' t' ts')
+  | c == c' = do
+      mgu (t : ts) (t' : ts')
+solveNamedInstPred _ _ = throwError "Named instance does not solve wanted predicate"
 
 hasNamedMethod :: Name -> Instance Name -> Bool
 hasNamedMethod n inst =
diff --git a/test/Cases.hs b/test/Cases.hs
index a34352f54..4cd3e4cec 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -404,6 +404,7 @@ cases =
       runTestForFile "named-inst-basic.solc" caseFolder,
       runTestExpectingFailure "named-inst-ambiguous-unqualified.solc" caseFolder,
       runTestForFile "named-inst-class-qualified.solc" caseFolder,
+      runTestForFile "named-inst-constrained-call.solc" caseFolder,
       runTestExpectingFailure "named-inst-no-matching-head.solc" caseFolder,
       runTestExpectingFailure "named-inst-shared-label-params.solc" caseFolder,
       runTestForFile "named-inst-receiver.solc" caseFolder,
diff --git a/test/examples/cases/named-inst-constrained-call.solc b/test/examples/cases/named-inst-constrained-call.solc
new file mode 100644
index 000000000..962237b19
--- /dev/null
+++ b/test/examples/cases/named-inst-constrained-call.solc
@@ -0,0 +1,27 @@
+// A named instance can be passed as explicit evidence to a constrained call.
+
+forall a . class a : Score {
+  function score(x : a) -> word;
+}
+
+forall a . a : Score => function useScore(x : a) -> word {
+  return Score.score(x);
+}
+
+instance word : Score {
+  function score(x : word) -> word {
+    return 0;
+  }
+}
+
+instance [fastScore] word : Score {
+  function score(x : word) -> word {
+    return 1;
+  }
+}
+
+contract NamedInstConstrainedCall {
+  function main() -> word {
+    return useScore@{fastScore}(3);
+  }
+}

From 393c6c08368a63d66481396efec974560a826e22 Mon Sep 17 00:00:00 2001
From: Yoshitomo Nakanishi <yurayura.rounin.3@gmail.com>
Date: Fri, 1 May 2026 18:51:27 +0900
Subject: [PATCH 14/21] Support explicit instance slots

---
 src/Solcore/Backend/Specialise.hs             |  47 +++--
 src/Solcore/Desugarer/ContractDispatch.hs     |   8 +-
 src/Solcore/Desugarer/FieldAccess.hs          |  12 +-
 src/Solcore/Desugarer/IndirectCall.hs         |  11 +-
 src/Solcore/Frontend/Module/Loader.hs         |   8 +-
 src/Solcore/Frontend/Parser/SolcoreParser.y   |  12 +-
 src/Solcore/Frontend/Pretty/SolcorePretty.hs  |  14 +-
 src/Solcore/Frontend/Pretty/TreePretty.hs     |   8 +-
 src/Solcore/Frontend/Syntax/NameResolution.hs |  73 +++----
 src/Solcore/Frontend/Syntax/Stmt.hs           |   9 +-
 src/Solcore/Frontend/Syntax/SyntaxTree.hs     |  13 +-
 .../Frontend/TypeInference/InvokeGen.hs       |   2 +-
 src/Solcore/Frontend/TypeInference/TcStmt.hs  | 179 +++++++++++-------
 test/Cases.hs                                 |   1 +
 test/examples/cases/named-inst-slot-call.solc |  33 ++++
 15 files changed, 271 insertions(+), 159 deletions(-)
 create mode 100644 test/examples/cases/named-inst-slot-call.solc

diff --git a/src/Solcore/Backend/Specialise.hs b/src/Solcore/Backend/Specialise.hs
index fb908b38f..7191a5d24 100644
--- a/src/Solcore/Backend/Specialise.hs
+++ b/src/Solcore/Backend/Specialise.hs
@@ -46,7 +46,7 @@ data SpecState = SpecState
     spGlobalEnv :: TcEnv,
     splocalEnv :: Table Ty,
     spSubst :: TVSubst,
-    spNamedEvidence :: [(Name, Instance Name)],
+    spNamedEvidence :: [(ImplArg, Instance Name)],
     spDebug :: Bool,
     spNS :: NameSupply
   }
@@ -185,18 +185,23 @@ extSpSubst subst = modify $ \s -> s {spSubst = spSubst s <> subst}
 atCurrentSubst :: (HasTV a) => a -> SM a
 atCurrentSubst a = flip applytv a <$> getSpSubst
 
-withNamedEvidence :: Name -> SM a -> SM a
-withNamedEvidence lbl action = do
+withNamedEvidence :: ImplArg -> SM a -> SM a
+withNamedEvidence implArg action = do
   env <- gets spGlobalEnv
-  case Map.lookup lbl (namedInstEnv env) of
+  case Map.lookup (implArgName implArg) (namedInstEnv env) of
     Nothing -> action
     Just inst -> do
       saved <- gets spNamedEvidence
-      modify $ \s -> s {spNamedEvidence = (lbl, inst) : saved}
+      modify $ \s -> s {spNamedEvidence = (implArg, inst) : saved}
       result <- action
       modify $ \s -> s {spNamedEvidence = saved}
       pure result
 
+withNamedEvidences :: [ImplArg] -> SM a -> SM a
+withNamedEvidences [] action = action
+withNamedEvidences (implArg : implArgs) action =
+  withNamedEvidence implArg (withNamedEvidences implArgs action)
+
 addData :: DataTy -> SM ()
 addData dt = modify (\s -> s {spDataTable = Map.insert (dataName dt) dt (spDataTable s)})
 
@@ -372,10 +377,10 @@ explicitNamedEvidenceForCall i args ty =
       let funType = foldr (:->) ty' argTypes
           methName = Name meth
       evidences <- gets spNamedEvidence
-      pure $ fst <$> find (matchesNamedEvidence cls methName funType) evidences
+      pure $ implArgName . fst <$> find (matchesNamedEvidence cls methName funType) evidences
     Name _ -> pure Nothing
 
-matchesNamedEvidence :: Name -> Name -> Ty -> (Name, Instance Name) -> Bool
+matchesNamedEvidence :: Name -> Name -> Ty -> (ImplArg, Instance Name) -> Bool
 matchesNamedEvidence cls meth funType (_, inst) =
   instName inst == cls
     && instanceHasMethod meth inst
@@ -406,29 +411,33 @@ methodTypeMatches methodTy callTy =
 
 -- | `specExp` specialises an expression to given type
 specExp :: TcExp -> Ty -> SM TcExp
-specExp (Call Nothing i Nothing args) ty = do
+specExp (Call Nothing i [] args) ty = do
   -- debug ["> specExp (Call): ", pretty e, " : ", pretty (idType i), " ~> ", pretty ty]
   mlbl <- explicitNamedEvidenceForCall i args ty
   case mlbl of
-    Just lbl -> specExp (Call Nothing i (Just lbl) args) ty
+    Just lbl -> specExp (Call Nothing i [ImplArg Nothing lbl] args) ty
     Nothing -> do
       (i'', args') <- specCall i args ty
-      let e' = Call Nothing i'' Nothing args'
+      let e' = Call Nothing i'' [] args'
       -- debug ["< specExp (Call): ", pretty e']
       return e'
-specExp (Call Nothing i (Just lbl) args) ty = do
+specExp (Call Nothing i [implArg] args) ty = do
   -- A label can either select a named instance method directly, or supply
   -- explicit evidence to a constrained function call.
+  let lbl = implArgName implArg
   isNamedMethod <- namedEvidenceHasMethod lbl i
   (i'', args') <-
     if isNamedMethod
       then do
         let i' = i {idName = QualName lbl (methodNameString (idName i))}
         specCall i' args ty
-      else specCallWithEvidence (Just lbl) i args ty
-  let e' = Call Nothing i'' Nothing args'
+      else specCallWithEvidence [implArg] i args ty
+  let e' = Call Nothing i'' [] args'
   -- debug ["< specExp (Call): ", pretty e']
   return e'
+specExp (Call Nothing i implArgs args) ty =
+  specCallWithEvidence implArgs i args ty >>= \(i'', args') ->
+    pure (Call Nothing i'' [] args')
 specExp e@(Con i es) ty = do
   debug ["> specConApp: ", pretty e, " : ", pretty (typeOfTcExp e), " ~> ", pretty ty]
   (i', es') <- specConApp i es ty
@@ -468,11 +477,11 @@ specConApp i@(Id _n conTy) args ty = do
 -- | Specialise a function call
 -- given actual arguments and the expected result type
 specCall :: Id -> [TcExp] -> Ty -> SM (Id, [TcExp])
-specCall = specCallWithEvidence Nothing
+specCall = specCallWithEvidence []
 
-specCallWithEvidence :: Maybe Name -> Id -> [TcExp] -> Ty -> SM (Id, [TcExp])
+specCallWithEvidence :: [ImplArg] -> Id -> [TcExp] -> Ty -> SM (Id, [TcExp])
 specCallWithEvidence _ i@(Id (Name "revert") _) args _ = pure (i, args) -- FIXME
-specCallWithEvidence mEvidence i args ty = do
+specCallWithEvidence implArgs i args ty = do
   i' <- atCurrentSubst i
   ty' <- atCurrentSubst ty
   -- debug ["> specCall: ", pretty i', show args, " : ", pretty ty']
@@ -490,10 +499,8 @@ specCallWithEvidence mEvidence i args ty = do
       extSpSubst phi
       subst <- getSpSubst
       let ty'' = applytv subst fty
-      ensureClosed ty'' (Call Nothing i Nothing args) subst
-      name' <- case mEvidence of
-        Just lbl -> withNamedEvidence lbl (specFunDef fd)
-        Nothing -> specFunDef fd
+      ensureClosed ty'' (Call Nothing i [] args) subst
+      name' <- withNamedEvidences implArgs (specFunDef fd)
       debug ["< specCall: ", pretty name', " : ", show ty'']
       args'' <- atCurrentSubst args'
       return (Id name' ty'', args'')
diff --git a/src/Solcore/Desugarer/ContractDispatch.hs b/src/Solcore/Desugarer/ContractDispatch.hs
index e9aef7fbb..63750132d 100644
--- a/src/Solcore/Desugarer/ContractDispatch.hs
+++ b/src/Solcore/Desugarer/ContractDispatch.hs
@@ -59,7 +59,7 @@ genMainFn addMain (Contract cname tys cdecls)
     cdecls' = Set.unions (map (transformCDecl cname) cdecls'')
     defaultConstructor = CConstrDecl (Constructor {constrParams = [], constrBody = []})
     mainfn = FunDef (Signature [] [] "main" [] Nothing) body
-    body = [StmtExp (Call Nothing (QualName "RunContract" "exec") Nothing [cdata])]
+    body = [StmtExp (Call Nothing (QualName "RunContract" "exec") [] [cdata])]
     cdata = Con "Contract" [methods, fallback]
     methods = tupleExpFromList (fmap mkMethod (mapMaybe unwrapSigs cdecls))
     fallback =
@@ -142,7 +142,7 @@ transformConstructor contractName cons
               := Call
                 Nothing
                 "abi_decode"
-                Nothing
+                []
                 [ Var "source",
                   proxyExp argsTuple,
                   proxyExp (TyCon "MemoryWordReader" [])
@@ -164,10 +164,10 @@ transformConstructor contractName cons
         }
     startBody =
       [ Asm [yulBlock|{ mstore(64, memoryguard(128)) }|],
-        Let "conargs" (Just argsTuple) (Just (Call Nothing "copy_arguments_for_constructor" Nothing [])),
+        Let "conargs" (Just argsTuple) (Just (Call Nothing "copy_arguments_for_constructor" [] [])),
         -- , Match [Var "conargs"] ...
         Let "fun" Nothing (Just (Var initFunName)),
-        StmtExp $ Call Nothing "fun" Nothing [Var "conargs"],
+        StmtExp $ Call Nothing "fun" [] [Var "conargs"],
         Asm
           [yulBlock|{
             let size := datasize(`yulContractName`)
diff --git a/src/Solcore/Desugarer/FieldAccess.hs b/src/Solcore/Desugarer/FieldAccess.hs
index 1f619cae1..f29a1b616 100644
--- a/src/Solcore/Desugarer/FieldAccess.hs
+++ b/src/Solcore/Desugarer/FieldAccess.hs
@@ -181,7 +181,7 @@ transAssignment (Indexed arr idx) rhs cenv = do
   let lhs' = traces ["lhsIndex", pretty arr, pretty idx] $ lhsIndex arr idx' cenv
   let rhs' = traces ["transRhs", pretty rhs] $ transRhs rhs cenv
   let assignName = QualName (Name "Assign") "assign"
-  StmtExp $ Call Nothing assignName Nothing [lhs', rhs']
+  StmtExp $ Call Nothing assignName [] [lhs', rhs']
 transAssignment lhs rhs cenv =
   traces ["Other assignment:", pretty (lhs := rhs)] $
     (lhs := rhs')
@@ -205,7 +205,7 @@ transContractFieldAssignment field rhs = do
   let lhs' = lhsAccess fieldMap
   rhs' <- transRhs rhs
   let assignName = QualName (Name "Assign") "assign"
-  pure $ StmtExp $ Call Nothing assignName Nothing [lhs', rhs']
+  pure $ StmtExp $ Call Nothing assignName [] [lhs', rhs']
 
 transRhs :: (HasCallStack) => NmExp -> CEM NmExp
 transRhs expr@(FieldAccess Nothing x) cenv
@@ -243,13 +243,13 @@ indexAccess dir exp@(FieldAccess Nothing name) idx = traces ["iA FA: " ++ pretty
       arrProxy <- memberProxyFor name
       let arrRef = lhsAccess arrProxy
       idx' <- transRhs idx
-      pure $ Call Nothing (indexFun dir) Nothing [arrRef, idx']
+      pure $ Call Nothing (indexFun dir) [] [arrRef, idx']
     else notImplemented "indexAccess" exp
 indexAccess dir _exp@(Indexed arr1 idx1) idx2 = traces ["iA II:", pretty arr1, pretty idx1, pretty idx2] $ do
   idx2' <- traces ["transRhs", pretty idx2] $ transRhs idx2
   idx1' <- traces ["transRhs", pretty idx1] $ transRhs idx1
   arr' <- traces ["lhsIndex", pretty arr1, pretty idx1'] $ lhsIndex arr1 idx1'
-  pure $ Call Nothing (indexFun dir) Nothing [arr', idx2']
+  pure $ Call Nothing (indexFun dir) [] [arr', idx2']
 indexAccess _dir exp idx = notImplemented "indexAccess" (Indexed exp idx)
 
 lhsIndex, rhsIndex :: (HasCallStack) => NmExp -> NmExp -> CEM (Exp Name)
@@ -312,10 +312,10 @@ memberProxyFor field = do
   pure fieldMap
 
 lhsAccess :: Exp Name -> Exp Name
-lhsAccess e = Call Nothing (QualName "LVA" "acc") Nothing [e]
+lhsAccess e = Call Nothing (QualName "LVA" "acc") [] [e]
 
 rhsAccess :: Exp Name -> Exp Name
-rhsAccess e = Call Nothing (QualName "RVA" "acc") Nothing [e]
+rhsAccess e = Call Nothing (QualName "RVA" "acc") [] [e]
 
 notImplemented :: (HasCallStack, Pretty a) => String -> a -> b
 notImplemented funName a = error $ concat [funName, " not implemented yet for ", pretty a]
diff --git a/src/Solcore/Desugarer/IndirectCall.hs b/src/Solcore/Desugarer/IndirectCall.hs
index c0795c932..df2bed2a6 100644
--- a/src/Solcore/Desugarer/IndirectCall.hs
+++ b/src/Solcore/Desugarer/IndirectCall.hs
@@ -2,7 +2,6 @@ module Solcore.Desugarer.IndirectCall where
 
 import Control.Monad.State
 import Data.Map qualified as Map
-import Data.Maybe (isJust)
 import Solcore.Frontend.Pretty.SolcorePretty
 import Solcore.Frontend.Syntax
 import Solcore.Frontend.TypeInference.TcEnv (primCtx)
@@ -95,19 +94,19 @@ instance Desugar (Exp Name) where
     Lam ps <$> desugar bd <*> pure t
   desugar (TyExp e t) =
     flip TyExp t <$> desugar e
-  desugar (Call m n lbl es) =
+  desugar (Call m n implArgs es) =
     do
       m' <- desugar m
       es' <- desugar es
       b <- isDirectCall n
       let qn = QualName invokableName "invoke"
           args' = [Var n, indirectArgs es']
-      -- Named instance calls (Just lbl) are always direct: no defunctionalization
-      if b || isJust lbl
+      -- Explicit instance calls are always direct: no defunctionalization.
+      if b || not (null implArgs)
         then
-          pure $ Call m' n lbl es'
+          pure $ Call m' n implArgs es'
         else
-          pure $ Call Nothing qn Nothing args'
+          pure $ Call Nothing qn [] args'
   desugar (Cond e1 e2 e3) =
     Cond <$> desugar e1 <*> desugar e2 <*> desugar e3
   desugar x = pure x
diff --git a/src/Solcore/Frontend/Module/Loader.hs b/src/Solcore/Frontend/Module/Loader.hs
index 5577b0eeb..6c3cb7141 100644
--- a/src/Solcore/Frontend/Module/Loader.hs
+++ b/src/Solcore/Frontend/Module/Loader.hs
@@ -1529,8 +1529,8 @@ renameExpFunctionCalls renameMap (ExpName me n es) =
       | me == Nothing = Map.findWithDefault n n renameMap
       | otherwise = n
     es' = map (renameExpFunctionCalls renameMap) es
-renameExpFunctionCalls renameMap (ExpNameAt me n lbl es) =
-  ExpNameAt me' n' lbl es'
+renameExpFunctionCalls renameMap (ExpNameAt me n implArgs es) =
+  ExpNameAt me' n' implArgs es'
   where
     me' = fmap (renameExpFunctionCalls renameMap) me
     n'
@@ -1698,11 +1698,11 @@ renameExpTypeRefs renameMap (ExpName me n es) =
     (renameMemberQualifierTypeRefs renameMap <$> me)
     n
     (map (renameExpTypeRefs renameMap) es)
-renameExpTypeRefs renameMap (ExpNameAt me n lbl es) =
+renameExpTypeRefs renameMap (ExpNameAt me n implArgs es) =
   ExpNameAt
     (renameMemberQualifierTypeRefs renameMap <$> me)
     n
-    lbl
+    implArgs
     (map (renameExpTypeRefs renameMap) es)
 renameExpTypeRefs renameMap (ExpVar Nothing n) =
   ExpVar
diff --git a/src/Solcore/Frontend/Parser/SolcoreParser.y b/src/Solcore/Frontend/Parser/SolcoreParser.y
index ac7449b14..c4b2d95c5 100644
--- a/src/Solcore/Frontend/Parser/SolcoreParser.y
+++ b/src/Solcore/Frontend/Parser/SolcoreParser.y
@@ -436,12 +436,20 @@ Expr : Name FunArgs                                {ExpName Nothing $1 $2}
      | '!' Expr                                    {ExpLNot $2 }
      | Conditional                                 {$1}
      | '@' Type                                    {ExpAt $2}
-     | Name '@{' TypeName '}' '(' ExprCommaList ')' { ExpNameAt Nothing $1 $3 $6 }
-     | Expr '.' Name '@{' TypeName '}' '(' ExprCommaList ')' { ExpNameAt (Just $1) $3 $5 $8 }
+     | Name '@{' ImplArgList '}' '(' ExprCommaList ')' { ExpNameAt Nothing $1 $3 $6 }
+     | Expr '.' Name '@{' ImplArgList '}' '(' ExprCommaList ')' { ExpNameAt (Just $1) $3 $5 $8 }
 
 Conditional :: { Exp }
 Conditional : 'if' Expr 'then' Expr 'else' Expr    {ExpCond $2 $4 $6}
 
+ImplArgList :: { [ImplArg] }
+ImplArgList : ImplArg                              {[$1]}
+            | ImplArg ',' ImplArgList              {$1 : $3}
+
+ImplArg :: { ImplArg }
+ImplArg : TypeName                                 {ImplArg Nothing $1}
+        | Name '=' TypeName                        {ImplArg (Just $1) $3}
+
 TupleArgs :: { [Exp] }
 TupleArgs : Expr ',' Expr                          {[$1, $3]}
           | Expr ',' TupleArgs                     {$1 : $3}
diff --git a/src/Solcore/Frontend/Pretty/SolcorePretty.hs b/src/Solcore/Frontend/Pretty/SolcorePretty.hs
index cd9678660..19c1a9b94 100644
--- a/src/Solcore/Frontend/Pretty/SolcorePretty.hs
+++ b/src/Solcore/Frontend/Pretty/SolcorePretty.hs
@@ -360,8 +360,8 @@ instance (Pretty a) => Pretty (Exp a) where
             then empty
             else (parens (nest 1 $ commaSep $ map ppr es))
   ppr (Lit l) = ppr l
-  ppr (Call e n lbl es) =
-    pprE e <> ppr n <> pprCallLabel lbl <> (parens (nest 1 $ commaSep $ map ppr es))
+  ppr (Call e n implArgs es) =
+    pprE e <> ppr n <> pprCallImplArgs implArgs <> (parens (nest 1 $ commaSep $ map ppr es))
   ppr (Lam args bd _) =
     text "lam"
       <+> pprParams args
@@ -380,9 +380,13 @@ pprE :: (Pretty a) => Maybe (Exp a) -> Doc
 pprE Nothing = ""
 pprE (Just e) = ppr e <> text "."
 
-pprCallLabel :: Maybe Name -> Doc
-pprCallLabel Nothing = empty
-pprCallLabel (Just lbl) = text "@{" <> ppr lbl <> text "}"
+pprCallImplArgs :: [ImplArg] -> Doc
+pprCallImplArgs [] = empty
+pprCallImplArgs implArgs = text "@{" <> commaSep (map ppr implArgs) <> text "}"
+
+instance Pretty ImplArg where
+  ppr (ImplArg Nothing implName) = ppr implName
+  ppr (ImplArg (Just slot) implName) = ppr slot <+> equals <+> ppr implName
 
 instance (Pretty a) => Pretty (Pat a) where
   ppr (PVar n) =
diff --git a/src/Solcore/Frontend/Pretty/TreePretty.hs b/src/Solcore/Frontend/Pretty/TreePretty.hs
index 08a798a0a..58734a16d 100644
--- a/src/Solcore/Frontend/Pretty/TreePretty.hs
+++ b/src/Solcore/Frontend/Pretty/TreePretty.hs
@@ -332,11 +332,11 @@ instance Pretty Exp where
       <> parensWhen
         (not $ null es)
         (commaSep (map ppr es))
-  ppr (ExpNameAt me n lbl es) =
+  ppr (ExpNameAt me n implArgs es) =
     maybe empty (\e -> ppr e <> char '.') me
       <> ppr n
       <> text "@{"
-      <> ppr lbl
+      <> commaSep (map ppr implArgs)
       <> char '}'
       <> parens (commaSep (map ppr es))
   ppr (ExpVar me v) =
@@ -398,6 +398,10 @@ instance Pretty Exp where
   ppr (ExpAt t) =
     text "@" <> ppr t
 
+instance Pretty ImplArg where
+  ppr (ImplArg Nothing implName) = ppr implName
+  ppr (ImplArg (Just slot) implName) = ppr slot <+> equals <+> ppr implName
+
 pprE :: Maybe Exp -> Doc
 pprE Nothing = ""
 pprE (Just e) = ppr e <> text "."
diff --git a/src/Solcore/Frontend/Syntax/NameResolution.hs b/src/Solcore/Frontend/Syntax/NameResolution.hs
index 5d282ef2e..2f04f52a2 100644
--- a/src/Solcore/Frontend/Syntax/NameResolution.hs
+++ b/src/Solcore/Frontend/Syntax/NameResolution.hs
@@ -591,7 +591,7 @@ instance Resolve S.Exp where
       case (me', dt) of
         -- normal function call
         (Nothing, Just TFunction) ->
-          pure (Call Nothing n Nothing es')
+          pure (Call Nothing n [] es')
         (Nothing, Just TTyCon) -> do
           sameName <- isSameNameConstructor n
           if sameName
@@ -611,7 +611,7 @@ instance Resolve S.Exp where
           let qn = QualName c (pretty n)
           qdt <- lookupName qn
           case qdt of
-            Just TFunction -> pure (Call Nothing qn Nothing es')
+            Just TFunction -> pure (Call Nothing qn [] es')
             Just TDataCon -> Con <$> resolveQualifiedConstructorName c n <*> pure es'
             _ -> undefinedName n
         -- class functions
@@ -620,11 +620,11 @@ instance Resolve S.Exp where
           let qn = QualName c (pretty n)
           case ct of
             Just TClass ->
-              pure (Call Nothing qn Nothing es')
+              pure (Call Nothing qn [] es')
             Just TModule -> do
               cf <- lookupName qn
               case cf of
-                Just TFunction -> pure (Call Nothing qn Nothing es')
+                Just TFunction -> pure (Call Nothing qn [] es')
                 Just TDataCon -> Con <$> resolveQualifiedConstructorName c n <*> pure es'
                 _ -> undefinedName n
             _ -> undefinedName c
@@ -634,9 +634,9 @@ instance Resolve S.Exp where
           cf <- lookupName qn
           case (ct, cf) of
             (Just TClass, Just TFunction) ->
-              pure (Call Nothing qn Nothing es')
+              pure (Call Nothing qn [] es')
             (_, Just TFunction) ->
-              pure (Call Nothing qn Nothing es')
+              pure (Call Nothing qn [] es')
             (_, Just TDataCon) ->
               Con <$> resolveQualifiedConstructorName c n <*> pure es'
             _ -> do
@@ -650,13 +650,13 @@ instance Resolve S.Exp where
           let qn = QualName c (pretty n)
           cf <- gets (Map.lookup qn . scopeEnv)
           case cf of
-            Just TFunction -> pure (Call Nothing qn Nothing es')
+            Just TFunction -> pure (Call Nothing qn [] es')
             _ -> undefinedName n
         -- variables
         (_, Just TLocalVar) ->
-          pure (Call Nothing n Nothing es')
+          pure (Call Nothing n [] es')
         (_, Just TParameter) ->
-          pure (Call Nothing n Nothing es')
+          pure (Call Nothing n [] es')
         -- error
         _ -> do
           sameName <- isSameNameConstructor n
@@ -672,31 +672,31 @@ instance Resolve S.Exp where
       e1' <- resolve e1 `wrapError` c
       e2' <- resolve e2 `wrapError` c
       let fun = QualName (Name "Add") "add"
-      pure $ Call Nothing fun Nothing [e1', e2']
+      pure $ Call Nothing fun [] [e1', e2']
   resolve c@(S.ExpMinus e1 e2) =
     do
       e1' <- resolve e1 `wrapError` c
       e2' <- resolve e2 `wrapError` c
       let fun = QualName (Name "Sub") "sub"
-      pure $ Call Nothing fun Nothing [e1', e2']
+      pure $ Call Nothing fun [] [e1', e2']
   resolve c@(S.ExpTimes e1 e2) =
     do
       e1' <- resolve e1 `wrapError` c
       e2' <- resolve e2 `wrapError` c
       let fun = QualName (Name "Mul") "mul"
-      pure $ Call Nothing fun Nothing [e1', e2']
+      pure $ Call Nothing fun [] [e1', e2']
   resolve c@(S.ExpDivide e1 e2) =
     do
       e1' <- resolve e1 `wrapError` c
       e2' <- resolve e2 `wrapError` c
       let fun = QualName (Name "Div") "div"
-      pure $ Call Nothing fun Nothing [e1', e2']
+      pure $ Call Nothing fun [] [e1', e2']
   resolve c@(S.ExpModulo e1 e2) =
     do
       e1' <- resolve e1 `wrapError` c
       e2' <- resolve e2 `wrapError` c
       let fun = QualName (Name "Mod") "mod"
-      pure $ Call Nothing fun Nothing [e1', e2']
+      pure $ Call Nothing fun [] [e1', e2']
   resolve c@(S.ExpIndexed array idx) = do
     arr' <- resolve array `wrapError` c
     idx' <- resolve idx `wrapError` c
@@ -704,40 +704,40 @@ instance Resolve S.Exp where
   resolve c@(S.ExpLT e1 e2) = do
     e1' <- resolve e1 `wrapError` c
     e2' <- resolve e2 `wrapError` c
-    pure $ Call Nothing (Name "lt") Nothing [e1', e2']
+    pure $ Call Nothing (Name "lt") [] [e1', e2']
   resolve c@(S.ExpGT e1 e2) = do
     e1' <- resolve e1 `wrapError` c
     e2' <- resolve e2 `wrapError` c
     let fun = QualName (Name "Ord") "gt"
-    pure $ Call Nothing fun Nothing [e1', e2']
+    pure $ Call Nothing fun [] [e1', e2']
   resolve c@(S.ExpLE e1 e2) = do
     e1' <- resolve e1 `wrapError` c
     e2' <- resolve e2 `wrapError` c
-    pure $ Call Nothing (Name "le") Nothing [e1', e2']
+    pure $ Call Nothing (Name "le") [] [e1', e2']
   resolve c@(S.ExpGE e1 e2) = do
     e1' <- resolve e1 `wrapError` c
     e2' <- resolve e2 `wrapError` c
-    pure $ Call Nothing (Name "ge") Nothing [e1', e2']
+    pure $ Call Nothing (Name "ge") [] [e1', e2']
   resolve c@(S.ExpEE e1 e2) = do
     e1' <- resolve e1 `wrapError` c
     e2' <- resolve e2 `wrapError` c
     let fun = QualName (Name "Eq") "eq"
-    pure $ Call Nothing fun Nothing [e1', e2']
+    pure $ Call Nothing fun [] [e1', e2']
   resolve c@(S.ExpNE e1 e2) = do
     e1' <- resolve e1 `wrapError` c
     e2' <- resolve e2 `wrapError` c
-    pure $ Call Nothing (Name "ne") Nothing [e1', e2']
+    pure $ Call Nothing (Name "ne") [] [e1', e2']
   resolve c@(S.ExpLAnd e1 e2) = do
     e1' <- resolve e1 `wrapError` c
     e2' <- resolve e2 `wrapError` c
-    pure $ Call Nothing (Name "and") Nothing [e1', e2']
+    pure $ Call Nothing (Name "and") [] [e1', e2']
   resolve c@(S.ExpLOr e1 e2) = do
     e1' <- resolve e1 `wrapError` c
     e2' <- resolve e2 `wrapError` c
-    pure $ Call Nothing (Name "or") Nothing [e1', e2']
+    pure $ Call Nothing (Name "or") [] [e1', e2']
   resolve c@(S.ExpLNot e) = do
     e' <- resolve e `wrapError` c
-    pure $ Call Nothing (Name "not") Nothing [e']
+    pure $ Call Nothing (Name "not") [] [e']
   resolve (S.ExpCond e1 e2 e3) =
     Cond <$> resolve e1 <*> resolve e2 <*> resolve e3
   resolve (S.ExpAt t) = do
@@ -747,9 +747,10 @@ instance Resolve S.Exp where
           (Con (Name "Proxy") [])
           (TyCon (Name "Proxy") [t'])
       )
-  resolve x@(S.ExpNameAt me n lbl es) = do
+  resolve x@(S.ExpNameAt me n implArgs es) = do
     me' <- resolve me `wrapError` x
     es' <- resolve es `wrapError` x
+    implArgs' <- mapM resolveImplArg implArgs `wrapError` x
     case me' of
       Just (Var c) -> do
         ct <- lookupName c
@@ -758,10 +759,10 @@ instance Resolve S.Exp where
             let qn = QualName c (pretty n)
             cf <- gets (Map.lookup qn . scopeEnv)
             case cf of
-              Just TFunction -> pure (Call Nothing qn (Just lbl) es')
+              Just TFunction -> pure (Call Nothing qn implArgs' es')
               _ -> undefinedName n
-          _ -> resolveNamedCall me' n lbl es'
-      _ -> resolveNamedCall me' n lbl es'
+          _ -> resolveNamedCall me' n implArgs' es'
+      _ -> resolveNamedCall me' n implArgs' es'
 
 instance Resolve S.Literal where
   type Result S.Literal = Literal
@@ -975,20 +976,22 @@ addQualifiedModules (QualName qualifier _) env =
   foldr addModuleName env (modulePrefixes qualifier)
 addQualifiedModules _ env = env
 
-resolveNamedCall :: Maybe (Exp Name) -> Name -> Name -> [Exp Name] -> ResolveM (Exp Name)
-resolveNamedCall me n lbl es = do
-  let args = maybe es (: es) me
-  dt <- lookupName lbl
+resolveImplArg :: S.ImplArg -> ResolveM ImplArg
+resolveImplArg (S.ImplArg slot implName) = do
+  dt <- lookupName implName
   case dt of
-    Just TNamedInstance -> pure (Call Nothing n (Just lbl) args)
+    Just TNamedInstance -> pure (ImplArg slot implName)
     _ ->
       throwError $
         "Unknown named instance '"
-          ++ pretty lbl
-          ++ "' for call '"
-          ++ pretty n
+          ++ pretty implName
           ++ "'"
 
+resolveNamedCall :: Maybe (Exp Name) -> Name -> [ImplArg] -> [Exp Name] -> ResolveM (Exp Name)
+resolveNamedCall me n implArgs es = do
+  let args = maybe es (: es) me
+  pure (Call Nothing n implArgs args)
+
 -- definition of a monad for name resolution
 
 type ResolveM a = StateT Env (ExceptT String IO) a
diff --git a/src/Solcore/Frontend/Syntax/Stmt.hs b/src/Solcore/Frontend/Syntax/Stmt.hs
index 660962557..ec4195eac 100644
--- a/src/Solcore/Frontend/Syntax/Stmt.hs
+++ b/src/Solcore/Frontend/Syntax/Stmt.hs
@@ -32,6 +32,13 @@ paramName :: Param a -> a
 paramName (Typed n _) = n
 paramName (Untyped n) = n
 
+data ImplArg
+  = ImplArg
+  { implArgSlot :: Maybe Name,
+    implArgName :: Name
+  }
+  deriving (Eq, Ord, Show, Data, Typeable)
+
 -- definition of the expression syntax
 
 data Exp a
@@ -39,7 +46,7 @@ data Exp a
   | Con a [Exp a] -- data type constructor
   | FieldAccess (Maybe (Exp a)) a -- field access
   | Lit Literal -- literal
-  | Call (Maybe (Exp a)) a (Maybe Name) [Exp a] -- function call (third arg = instance label)
+  | Call (Maybe (Exp a)) a [ImplArg] [Exp a] -- function call (third arg = explicit instance args)
   | Lam [Param a] (Body a) (Maybe Ty) -- lambda-abstraction
   | TyExp (Exp a) Ty -- type annotated expression
   | Cond (Exp a) (Exp a) (Exp a) -- conditional expression
diff --git a/src/Solcore/Frontend/Syntax/SyntaxTree.hs b/src/Solcore/Frontend/Syntax/SyntaxTree.hs
index 8b69e4f1a..8bc42a624 100644
--- a/src/Solcore/Frontend/Syntax/SyntaxTree.hs
+++ b/src/Solcore/Frontend/Syntax/SyntaxTree.hs
@@ -254,6 +254,13 @@ data Param
   | Untyped Name
   deriving (Eq, Ord, Show, Data, Typeable)
 
+data ImplArg
+  = ImplArg
+  { implArgSlot :: Maybe Name,
+    implArgName :: Name
+  }
+  deriving (Eq, Ord, Show, Data, Typeable)
+
 -- expression syntax
 
 data Exp
@@ -280,9 +287,9 @@ data Exp
   | ExpLNot Exp -- ! e
   | ExpCond Exp Exp Exp -- if e1 then e2 else e3
   | ExpAt Ty -- proxy sugar
-  | -- | ExpNameAt receiver methodName instanceLabel args
-    --   Represents receiver.method@{label}(args) or method@{label}(args)
-    ExpNameAt (Maybe Exp) Name Name [Exp]
+  | -- | ExpNameAt receiver methodName explicitInstanceArgs args
+    --   Represents receiver.method@{impl}(args) or method@{slot = impl}(args)
+    ExpNameAt (Maybe Exp) Name [ImplArg] [Exp]
   deriving (Eq, Ord, Show, Data, Typeable)
 
 -- pattern matching equations
diff --git a/src/Solcore/Frontend/TypeInference/InvokeGen.hs b/src/Solcore/Frontend/TypeInference/InvokeGen.hs
index 31842b701..afcfb6825 100644
--- a/src/Solcore/Frontend/TypeInference/InvokeGen.hs
+++ b/src/Solcore/Frontend/TypeInference/InvokeGen.hs
@@ -65,7 +65,7 @@ createInstance udt fd sch =
         discr = epair (Var sn) (Var an)
         fname = sigName (funSignature fd)
         ssargs = take (length args) (svs ++ sarg)
-        scall = Return (Call Nothing fname Nothing ssargs)
+        scall = Return (Call Nothing fname [] ssargs)
         bdy = Match [discr] [([foldr1 ppair (spvs : sargs)], [scall])]
         ifd = FunDef isig [bdy]
         vs' = bv qs `union` bv [tupleArgTy, returnTy, selfTy] `union` bv ifd
diff --git a/src/Solcore/Frontend/TypeInference/TcStmt.hs b/src/Solcore/Frontend/TypeInference/TcStmt.hs
index 1ce70fee1..65f34ac8e 100644
--- a/src/Solcore/Frontend/TypeInference/TcStmt.hs
+++ b/src/Solcore/Frontend/TypeInference/TcStmt.hs
@@ -4,6 +4,7 @@ import Common.Pretty
 import Control.Monad
 import Control.Monad.Except
 import Control.Monad.State
+import Data.Char (toLower)
 import Data.Generics hiding (Constr)
 import Data.List
 import Data.Map qualified as Map
@@ -317,10 +318,10 @@ tcExpWithExpected _ (FieldAccess (Just e) n) =
     s <- askField tn n
     (ps' :=> t') <- freshInst s
     withCurrentSubst (FieldAccess (Just e') (Id n t'), ps ++ ps', t')
-tcExpWithExpected _ ex@(Call me n Nothing args) =
+tcExpWithExpected _ ex@(Call me n [] args) =
   tcCall me n args `wrapError` ex
-tcExpWithExpected _ ex@(Call me n (Just lbl) args) =
-  tcCallNamed me n lbl args `wrapError` ex
+tcExpWithExpected _ ex@(Call me n implArgs args) =
+  tcCallNamed me n implArgs args `wrapError` ex
 tcExpWithExpected _ (Lam args bd _) =
   do
     (args', schs, ts') <- tcArgs args
@@ -1311,7 +1312,7 @@ tcBodyWithExpectedReturn mExpectedReturn (s : ss) =
 tcCall :: Maybe (Exp Name) -> Name -> [Exp Name] -> TcM (Exp Id, [Pred], Ty)
 tcCall Nothing n args =
   do
-    s <- askEnv n `wrapError` (Call Nothing n Nothing args)
+    s <- askEnv n `wrapError` (Call Nothing n [] args)
     (ps :=> t) <- freshInst s
     t' <- freshTyVar
     expectedArgTys <- mapM (const freshTyVar) args
@@ -1323,11 +1324,11 @@ tcCall Nothing n args =
     _ <- extSubst s1
     let ps' = foldr union [] (ps : pss')
         t1 = funtype ts' t'
-    withCurrentSubst (Call Nothing (Id n t1) Nothing es', ps', t')
+    withCurrentSubst (Call Nothing (Id n t1) [] es', ps', t')
 tcCall (Just e) n args =
   do
     (e', ps, _) <- tcExp e
-    s <- askEnv n `wrapError` (Call (Just e) n Nothing args)
+    s <- askEnv n `wrapError` (Call (Just e) n [] args)
     (ps1 :=> t) <- freshInst s
     t' <- freshTyVar
     expectedArgTys <- mapM (const freshTyVar) args
@@ -1338,80 +1339,100 @@ tcCall (Just e) n args =
     s' <- unify (foldr (:->) t' ts') t
     _ <- extSubst s'
     let ps' = foldr union [] ((ps ++ ps1) : pss')
-    withCurrentSubst (Call (Just e') (Id n t') Nothing es', ps', t')
-
-tcCallNamed :: Maybe (Exp Name) -> Name -> Name -> [Exp Name] -> TcM (Exp Id, [Pred], Ty)
-tcCallNamed me n lbl args =
-  do
-    let callExpr = Call me n (Just lbl) args
-    namedInst <-
-      askNamedInstance lbl >>= \mInst ->
-        case mInst of
-          Just inst -> pure inst
-          Nothing ->
+    withCurrentSubst (Call (Just e') (Id n t') [] es', ps', t')
+
+type ResolvedImplArg = (ImplArg, Instance Name)
+
+tcCallNamed :: Maybe (Exp Name) -> Name -> [ImplArg] -> [Exp Name] -> TcM (Exp Id, [Pred], Ty)
+tcCallNamed me n implArgs args =
+  do
+    let callExpr = Call me n implArgs args
+    resolvedImplArgs <- mapM resolveNamedImplArg implArgs
+    case resolvedImplArgs of
+      [(ImplArg _ lbl, namedInst)]
+        | hasNamedMethod n namedInst -> do
+          mrecv <- mapM tcExp me
+          (es', pss', ts') <- unzip3 <$> mapM tcExp args
+          let recvArgs = maybe [] (\(e', _, _) -> [e']) mrecv
+              recvPreds = maybe [] (\(_, ps0, _) -> ps0) mrecv
+              recvTys = maybe [] (\(_, _, ty0) -> [ty0]) mrecv
+              allArgs = recvArgs ++ es'
+              allTys = recvTys ++ ts'
+          matches <- matchesNamedCall callExpr n lbl allTys namedInst
+          unless matches $
             throwError $
-              "Unknown named instance: " ++ pretty lbl
-    if hasNamedMethod n namedInst
-      then do
-        mrecv <- mapM tcExp me
-        (es', pss', ts') <- unzip3 <$> mapM tcExp args
-        let recvArgs = maybe [] (\(e', _, _) -> [e']) mrecv
-            recvPreds = maybe [] (\(_, ps0, _) -> ps0) mrecv
-            recvTys = maybe [] (\(_, _, ty0) -> [ty0]) mrecv
-            allArgs = recvArgs ++ es'
-            allTys = recvTys ++ ts'
-        matches <- matchesNamedCall callExpr n lbl allTys namedInst
-        unless matches $
-          throwError $
-            unwords
-              [ "Named instance",
-                pretty lbl,
-                "does not match call to",
-                pretty n
-              ]
-        tcCallNamedWithInst callExpr n lbl recvPreds allArgs pss' allTys namedInst
-      else tcCallWithNamedEvidence callExpr me n lbl args namedInst
+              unwords
+                [ "Named instance",
+                  pretty lbl,
+                  "does not match call to",
+                  pretty n
+                ]
+          tcCallNamedWithInst callExpr n lbl recvPreds allArgs pss' allTys namedInst
+      _ -> tcCallWithNamedEvidence callExpr me n args resolvedImplArgs
+
+resolveNamedImplArg :: ImplArg -> TcM ResolvedImplArg
+resolveNamedImplArg implArg@(ImplArg _ implName) =
+  askNamedInstance implName >>= \mInst ->
+    case mInst of
+      Just inst -> pure (implArg, inst)
+      Nothing ->
+        throwError $
+          "Unknown named instance: " ++ pretty implName
 
 tcCallWithNamedEvidence ::
   Exp Name ->
   Maybe (Exp Name) ->
   Name ->
-  Name ->
   [Exp Name] ->
-  Instance Name ->
+  [ResolvedImplArg] ->
   TcM (Exp Id, [Pred], Ty)
-tcCallWithNamedEvidence callExpr me n lbl args inst =
+tcCallWithNamedEvidence callExpr me n args resolvedImplArgs =
   do
     (call, ps, ty) <- tcCall me n args
-    matching <- catMaybes <$> mapM (namedInstSolvesWanted inst) ps
-    case matching of
-      [(p, instPreds, evidenceSubst)] ->
-        case call of
-          Call me' i Nothing args' -> do
-            _ <- extSubst evidenceSubst
-            let ps' = apply evidenceSubst (instPreds ++ delete p ps)
-            withCurrentSubst (Call me' i (Just lbl) args', ps', ty)
-          _ ->
-            throwError $ "Internal error: expected a call while checking " ++ pretty callExpr
-      [] ->
-        throwError $
-          unwords
-            [ "Named instance",
-              pretty lbl,
-              "does not match any wanted constraint for",
-              pretty n
-            ]
+    (instPreds, evidenceSubst, remainingPs) <- solveNamedImplArgs n ps resolvedImplArgs
+    case call of
+      Call me' i [] args' -> do
+        _ <- extSubst evidenceSubst
+        let ps' = apply evidenceSubst (instPreds ++ remainingPs)
+        withCurrentSubst (Call me' i (map fst resolvedImplArgs) args', ps', ty)
       _ ->
-        throwError $
-          unlines
-            [ unwords
-                [ "Named instance",
-                  pretty lbl,
-                  "matches multiple wanted constraints for",
-                  pretty n
-                ],
-              "Use an explicit constraint slot to disambiguate."
-            ]
+        throwError $ "Internal error: expected a call while checking " ++ pretty callExpr
+
+solveNamedImplArgs :: Name -> [Pred] -> [ResolvedImplArg] -> TcM ([Pred], Subst, [Pred])
+solveNamedImplArgs _ ps [] = pure ([], mempty, ps)
+solveNamedImplArgs n ps ((implArg, inst) : rest) = do
+  matching <- catMaybes <$> mapM (namedImplArgSolvesWanted implArg inst) ps
+  case matching of
+    [(p, instPreds, evidenceSubst)] -> do
+      let psNext = apply evidenceSubst (delete p ps)
+      (restInstPreds, restSubst, remainingPs) <- solveNamedImplArgs n psNext rest
+      let combinedSubst = restSubst <> evidenceSubst
+      pure (apply restSubst instPreds ++ restInstPreds, combinedSubst, remainingPs)
+    [] ->
+      throwError $
+        unwords
+          [ "Named instance",
+            pretty (implArgName implArg),
+            "does not match any wanted constraint for",
+            pretty n
+          ]
+    _ ->
+      throwError $
+        unlines
+          [ unwords
+              [ "Named instance",
+                pretty (implArgName implArg),
+                "matches multiple wanted constraints for",
+                pretty n
+              ],
+            "Use an explicit constraint slot to disambiguate."
+          ]
+namedImplArgSolvesWanted :: ImplArg -> Instance Name -> Pred -> TcM (Maybe (Pred, [Pred], Subst))
+namedImplArgSolvesWanted implArg inst wanted
+  | Just slot <- implArgSlot implArg,
+    not (slotMatchesPred slot wanted) =
+      pure Nothing
+  | otherwise = namedInstSolvesWanted inst wanted
 
 namedInstSolvesWanted :: Instance Name -> Pred -> TcM (Maybe (Pred, [Pred], Subst))
 namedInstSolvesWanted inst wanted =
@@ -1434,6 +1455,24 @@ solveNamedInstPred (InCls c t ts) (InCls c' t' ts')
       mgu (t : ts) (t' : ts')
 solveNamedInstPred _ _ = throwError "Named instance does not solve wanted predicate"
 
+slotMatchesPred :: Name -> Pred -> Bool
+slotMatchesPred slot (InCls cls _ _) = slot `elem` classSlotNames cls
+slotMatchesPred _ _ = False
+
+classSlotNames :: Name -> [Name]
+classSlotNames cls =
+  nub [Name baseName, Name (lowerFirst baseName)]
+  where
+    baseName = nameLeaf cls
+
+nameLeaf :: Name -> String
+nameLeaf (Name s) = s
+nameLeaf (QualName _ s) = s
+
+lowerFirst :: String -> String
+lowerFirst [] = []
+lowerFirst (c : cs) = toLower c : cs
+
 hasNamedMethod :: Name -> Instance Name -> Bool
 hasNamedMethod n inst =
   let (mcls, meth) = splitNamedMethod n
@@ -1511,7 +1550,7 @@ tcCallNamedWithInst callExpr n lbl recvPreds allArgs pss' allTys inst =
     _ <- extSubst s'
     let ps' = foldr union [] (ps : recvPreds : pss')
         t1 = funtype allTys t'
-    withCurrentSubst (Call Nothing (Id n t1) (Just lbl) allArgs, ps', t')
+    withCurrentSubst (Call Nothing (Id n t1) [ImplArg Nothing lbl] allArgs, ps', t')
 
 tcParam :: Param Name -> TcM (Param Id)
 tcParam (Typed n t) =
diff --git a/test/Cases.hs b/test/Cases.hs
index 4cd3e4cec..84a0830a7 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -409,6 +409,7 @@ cases =
       runTestExpectingFailure "named-inst-shared-label-params.solc" caseFolder,
       runTestForFile "named-inst-receiver.solc" caseFolder,
       runTestExpectingFailure "named-inst-shared-label.solc" caseFolder,
+      runTestForFile "named-inst-slot-call.solc" caseFolder,
       runTestForFile "named-inst-two-instances.solc" caseFolder,
       runTestExpectingFailure "named-inst-unknown-label.solc" caseFolder,
       runTestExpectingFailure "named-inst-dup-label.solc" caseFolder,
diff --git a/test/examples/cases/named-inst-slot-call.solc b/test/examples/cases/named-inst-slot-call.solc
new file mode 100644
index 000000000..e155e9811
--- /dev/null
+++ b/test/examples/cases/named-inst-slot-call.solc
@@ -0,0 +1,33 @@
+// Slot syntax can pass multiple named instances to a constrained call.
+
+forall a . class a : Eq {
+  function same(x : a, y : a) -> word;
+}
+
+forall a . class a : Ord {
+  function cmp(x : a, y : a) -> word;
+}
+
+forall a . a : Eq, a : Ord => function choose(x : a, y : a) -> word {
+  let e : word = Eq.same(x, y);
+  let o : word = Ord.cmp(x, y);
+  return o;
+}
+
+instance [strictEq] word : Eq {
+  function same(x : word, y : word) -> word {
+    return primEqWord(x, y);
+  }
+}
+
+instance [fastOrd] word : Ord {
+  function cmp(x : word, y : word) -> word {
+    return x;
+  }
+}
+
+contract NamedInstSlotCall {
+  function main() -> word {
+    return choose@{eq = strictEq, ord = fastOrd}(1, 2);
+  }
+}

From c39620a10dc119b9671abdec9a85bee3f0930f4e Mon Sep 17 00:00:00 2001
From: Yoshitomo Nakanishi <yurayura.rounin.3@gmail.com>
Date: Sat, 2 May 2026 13:26:45 +0900
Subject: [PATCH 15/21] format

---
 src/Solcore/Frontend/TypeInference/TcStmt.hs | 35 ++++++++++----------
 1 file changed, 18 insertions(+), 17 deletions(-)

diff --git a/src/Solcore/Frontend/TypeInference/TcStmt.hs b/src/Solcore/Frontend/TypeInference/TcStmt.hs
index 65f34ac8e..a07d31dd8 100644
--- a/src/Solcore/Frontend/TypeInference/TcStmt.hs
+++ b/src/Solcore/Frontend/TypeInference/TcStmt.hs
@@ -1351,23 +1351,23 @@ tcCallNamed me n implArgs args =
     case resolvedImplArgs of
       [(ImplArg _ lbl, namedInst)]
         | hasNamedMethod n namedInst -> do
-          mrecv <- mapM tcExp me
-          (es', pss', ts') <- unzip3 <$> mapM tcExp args
-          let recvArgs = maybe [] (\(e', _, _) -> [e']) mrecv
-              recvPreds = maybe [] (\(_, ps0, _) -> ps0) mrecv
-              recvTys = maybe [] (\(_, _, ty0) -> [ty0]) mrecv
-              allArgs = recvArgs ++ es'
-              allTys = recvTys ++ ts'
-          matches <- matchesNamedCall callExpr n lbl allTys namedInst
-          unless matches $
-            throwError $
-              unwords
-                [ "Named instance",
-                  pretty lbl,
-                  "does not match call to",
-                  pretty n
-                ]
-          tcCallNamedWithInst callExpr n lbl recvPreds allArgs pss' allTys namedInst
+            mrecv <- mapM tcExp me
+            (es', pss', ts') <- unzip3 <$> mapM tcExp args
+            let recvArgs = maybe [] (\(e', _, _) -> [e']) mrecv
+                recvPreds = maybe [] (\(_, ps0, _) -> ps0) mrecv
+                recvTys = maybe [] (\(_, _, ty0) -> [ty0]) mrecv
+                allArgs = recvArgs ++ es'
+                allTys = recvTys ++ ts'
+            matches <- matchesNamedCall callExpr n lbl allTys namedInst
+            unless matches $
+              throwError $
+                unwords
+                  [ "Named instance",
+                    pretty lbl,
+                    "does not match call to",
+                    pretty n
+                  ]
+            tcCallNamedWithInst callExpr n lbl recvPreds allArgs pss' allTys namedInst
       _ -> tcCallWithNamedEvidence callExpr me n args resolvedImplArgs
 
 resolveNamedImplArg :: ImplArg -> TcM ResolvedImplArg
@@ -1427,6 +1427,7 @@ solveNamedImplArgs n ps ((implArg, inst) : rest) = do
               ],
             "Use an explicit constraint slot to disambiguate."
           ]
+
 namedImplArgSolvesWanted :: ImplArg -> Instance Name -> Pred -> TcM (Maybe (Pred, [Pred], Subst))
 namedImplArgSolvesWanted implArg inst wanted
   | Just slot <- implArgSlot implArg,

From d251860fb14d85869222ccf8a3f51bae5c1f69f0 Mon Sep 17 00:00:00 2001
From: Yoshitomo Nakanishi <yurayura.rounin.3@gmail.com>
Date: Sun, 3 May 2026 17:38:12 +0900
Subject: [PATCH 16/21] Fix dev shell evmone path on Darwin

---
 flake.nix | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/flake.nix b/flake.nix
index c7dd454bd..a240dac5e 100644
--- a/flake.nix
+++ b/flake.nix
@@ -34,6 +34,10 @@
           });
         texlive = pkgs.texlive.combine { inherit (pkgs.texlive) scheme-small thmtools pdfsync lkproof cm-super; };
         evmone-lib = pkgs.callPackage ./nix/evmone.nix { };
+        evmone-shared-lib =
+          if pkgs.stdenv.hostPlatform.isDarwin
+          then "${evmone-lib}/lib/libevmone.dylib"
+          else "${evmone-lib}/lib/libevmone.so";
 
         testrunner = pkgs.stdenv.mkDerivation {
           pname = "testrunner";
@@ -147,7 +151,7 @@
             (pkgs.callPackage ./nix/goevmlab.nix { src = inputs.goevmlab; })
             pkgs.mdbook
           ];
-          evmone="${evmone-lib}/lib/libevmone.so";
+          evmone = evmone-shared-lib;
         };
       }
     );

From 4a5338479c00975d2149de588df5c8f17fd48b1f Mon Sep 17 00:00:00 2001
From: Yoshitomo Nakanishi <yurayura.rounin.3@gmail.com>
Date: Mon, 4 May 2026 21:14:06 +0900
Subject: [PATCH 17/21] Qualify class stub type references

---
 src/Solcore/Frontend/Module/Loader.hs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Solcore/Frontend/Module/Loader.hs b/src/Solcore/Frontend/Module/Loader.hs
index 6c3cb7141..b3a2563a4 100644
--- a/src/Solcore/Frontend/Module/Loader.hs
+++ b/src/Solcore/Frontend/Module/Loader.hs
@@ -1417,11 +1417,12 @@ qualifiedNamedInstanceDecls qualifier cunit =
 
 qualifiedClassDecls :: Name -> CompUnit -> [TopDecl]
 qualifiedClassDecls qualifier cunit =
-  [ TClassDef (renameClassDeclClassRefs classRenameMap cls {className = renamedClassName (className cls)})
+  [ TClassDef (renameClassDeclClassRefs classRenameMap (renameClassTypeRefs typeRenameMap cls {className = renamedClassName (className cls)}))
     | TClassDef cls <- topDeclsFrom cunit
   ]
   where
     classRenameMap = localClassRenameMap qualifier (topDeclsFrom cunit)
+    typeRenameMap = localTypeRenameMap qualifier (topDeclsFrom cunit)
     renamedClassName n = Map.findWithDefault n n classRenameMap
 
 localClassRenameMap :: Name -> [TopDecl] -> Map Name Name

From 439c7680a01bdc4074c1bb078604de7cc466ceea Mon Sep 17 00:00:00 2001
From: Yoshitomo Nakanishi <yurayura.rounin.3@gmail.com>
Date: Tue, 5 May 2026 20:47:07 +0900
Subject: [PATCH 18/21] Prefer named evidence for constrained calls

---
 src/Solcore/Backend/Specialise.hs             | 12 +++-
 src/Solcore/Frontend/TypeInference/TcStmt.hs  | 58 +++++++++++++------
 test/Cases.hs                                 |  4 ++
 .../cases/named-inst-default-fail.solc        | 17 ++++++
 .../named-inst-function-method-collision.solc | 23 ++++++++
 .../cases/named-inst-not-implicit.solc        | 18 ++++++
 test/imports/namedinst_select_main.solc       |  7 +++
 7 files changed, 118 insertions(+), 21 deletions(-)
 create mode 100644 test/examples/cases/named-inst-default-fail.solc
 create mode 100644 test/examples/cases/named-inst-function-method-collision.solc
 create mode 100644 test/examples/cases/named-inst-not-implicit.solc
 create mode 100644 test/imports/namedinst_select_main.solc

diff --git a/src/Solcore/Backend/Specialise.hs b/src/Solcore/Backend/Specialise.hs
index 7191a5d24..26a275c91 100644
--- a/src/Solcore/Backend/Specialise.hs
+++ b/src/Solcore/Backend/Specialise.hs
@@ -12,7 +12,7 @@ import Control.Monad.State
 import Data.Generics
 import Data.List (find, intercalate, union, (\\))
 import Data.Map qualified as Map
-import Data.Maybe (fromMaybe)
+import Data.Maybe (fromMaybe, isJust)
 import Solcore.Backend.Mast
 import Solcore.Desugarer.IfDesugarer (desugaredBoolTy)
 import Solcore.Frontend.Pretty.ShortName
@@ -426,8 +426,9 @@ specExp (Call Nothing i [implArg] args) ty = do
   -- explicit evidence to a constrained function call.
   let lbl = implArgName implArg
   isNamedMethod <- namedEvidenceHasMethod lbl i
+  hasFunctionResolution <- callHasResolution i args ty
   (i'', args') <-
-    if isNamedMethod
+    if isNamedMethod && not hasFunctionResolution
       then do
         let i' = i {idName = QualName lbl (methodNameString (idName i))}
         specCall i' args ty
@@ -479,6 +480,13 @@ specConApp i@(Id _n conTy) args ty = do
 specCall :: Id -> [TcExp] -> Ty -> SM (Id, [TcExp])
 specCall = specCallWithEvidence []
 
+callHasResolution :: Id -> [TcExp] -> Ty -> SM Bool
+callHasResolution i args ty = do
+  i' <- atCurrentSubst i
+  ty' <- atCurrentSubst ty
+  argTypes' <- atCurrentSubst (map typeOfTcExp args)
+  isJust <$> lookupResolution (idName i') (foldr (:->) ty' argTypes')
+
 specCallWithEvidence :: [ImplArg] -> Id -> [TcExp] -> Ty -> SM (Id, [TcExp])
 specCallWithEvidence _ i@(Id (Name "revert") _) args _ = pure (i, args) -- FIXME
 specCallWithEvidence implArgs i args ty = do
diff --git a/src/Solcore/Frontend/TypeInference/TcStmt.hs b/src/Solcore/Frontend/TypeInference/TcStmt.hs
index a07d31dd8..72228086e 100644
--- a/src/Solcore/Frontend/TypeInference/TcStmt.hs
+++ b/src/Solcore/Frontend/TypeInference/TcStmt.hs
@@ -1349,27 +1349,47 @@ tcCallNamed me n implArgs args =
     let callExpr = Call me n implArgs args
     resolvedImplArgs <- mapM resolveNamedImplArg implArgs
     case resolvedImplArgs of
-      [(ImplArg _ lbl, namedInst)]
-        | hasNamedMethod n namedInst -> do
-            mrecv <- mapM tcExp me
-            (es', pss', ts') <- unzip3 <$> mapM tcExp args
-            let recvArgs = maybe [] (\(e', _, _) -> [e']) mrecv
-                recvPreds = maybe [] (\(_, ps0, _) -> ps0) mrecv
-                recvTys = maybe [] (\(_, _, ty0) -> [ty0]) mrecv
-                allArgs = recvArgs ++ es'
-                allTys = recvTys ++ ts'
-            matches <- matchesNamedCall callExpr n lbl allTys namedInst
-            unless matches $
-              throwError $
-                unwords
-                  [ "Named instance",
-                    pretty lbl,
-                    "does not match call to",
-                    pretty n
-                  ]
-            tcCallNamedWithInst callExpr n lbl recvPreds allArgs pss' allTys namedInst
+      [(implArg, namedInst)]
+        | isNothing me -> do
+            hasFunction <- isJust <$> maybeAskEnv n
+            if hasFunction
+              then tcCallWithNamedEvidence callExpr me n args resolvedImplArgs
+              else tcNamedMethodCall callExpr n implArg me args namedInst
+      [(implArg, namedInst)]
+        | hasNamedMethod n namedInst ->
+            tcNamedMethodCall callExpr n implArg me args namedInst
       _ -> tcCallWithNamedEvidence callExpr me n args resolvedImplArgs
 
+tcNamedMethodCall ::
+  Exp Name ->
+  Name ->
+  ImplArg ->
+  Maybe (Exp Name) ->
+  [Exp Name] ->
+  Instance Name ->
+  TcM (Exp Id, [Pred], Ty)
+tcNamedMethodCall callExpr n implArg@(ImplArg _ lbl) me args namedInst =
+  if hasNamedMethod n namedInst
+    then do
+      mrecv <- mapM tcExp me
+      (es', pss', ts') <- unzip3 <$> mapM tcExp args
+      let recvArgs = maybe [] (\(e', _, _) -> [e']) mrecv
+          recvPreds = maybe [] (\(_, ps0, _) -> ps0) mrecv
+          recvTys = maybe [] (\(_, _, ty0) -> [ty0]) mrecv
+          allArgs = recvArgs ++ es'
+          allTys = recvTys ++ ts'
+      matches <- matchesNamedCall callExpr n lbl allTys namedInst
+      unless matches $
+        throwError $
+          unwords
+            [ "Named instance",
+              pretty lbl,
+              "does not match call to",
+              pretty n
+            ]
+      tcCallNamedWithInst callExpr n lbl recvPreds allArgs pss' allTys namedInst
+    else tcCallWithNamedEvidence callExpr me n args [(implArg, namedInst)]
+
 resolveNamedImplArg :: ImplArg -> TcM ResolvedImplArg
 resolveNamedImplArg implArg@(ImplArg _ implName) =
   askNamedInstance implName >>= \mInst ->
diff --git a/test/Cases.hs b/test/Cases.hs
index 84a0830a7..fb346c3f1 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -146,6 +146,7 @@ imports =
       runImportSuccess "dupqual_module_main.solc",
       runImportSuccess "private_helper_main.solc",
       runImportSuccess "namedinst_qualified_main.solc",
+      runImportSuccess "namedinst_select_main.solc",
       runImportSuccess "module_qualified_constructor.solc",
       runImportSuccess "module_qualified_constructor_pattern.solc",
       runImportSuccess "module_qualified_constructor_alias.solc",
@@ -405,7 +406,10 @@ cases =
       runTestExpectingFailure "named-inst-ambiguous-unqualified.solc" caseFolder,
       runTestForFile "named-inst-class-qualified.solc" caseFolder,
       runTestForFile "named-inst-constrained-call.solc" caseFolder,
+      runTestExpectingFailure "named-inst-default-fail.solc" caseFolder,
+      runTestForFile "named-inst-function-method-collision.solc" caseFolder,
       runTestExpectingFailure "named-inst-no-matching-head.solc" caseFolder,
+      runTestExpectingFailure "named-inst-not-implicit.solc" caseFolder,
       runTestExpectingFailure "named-inst-shared-label-params.solc" caseFolder,
       runTestForFile "named-inst-receiver.solc" caseFolder,
       runTestExpectingFailure "named-inst-shared-label.solc" caseFolder,
diff --git a/test/examples/cases/named-inst-default-fail.solc b/test/examples/cases/named-inst-default-fail.solc
new file mode 100644
index 000000000..be9e7bf4e
--- /dev/null
+++ b/test/examples/cases/named-inst-default-fail.solc
@@ -0,0 +1,17 @@
+// Named instances and default instances are distinct mechanisms.
+
+forall a . class a : Score {
+  function score(x : a) -> word;
+}
+
+default instance [fastScore] word : Score {
+  function score(x : word) -> word {
+    return 7;
+  }
+}
+
+contract NamedInstDefaultFail {
+  function main() -> word {
+    return score@{fastScore}(3);
+  }
+}
diff --git a/test/examples/cases/named-inst-function-method-collision.solc b/test/examples/cases/named-inst-function-method-collision.solc
new file mode 100644
index 000000000..9b7f51a22
--- /dev/null
+++ b/test/examples/cases/named-inst-function-method-collision.solc
@@ -0,0 +1,23 @@
+// A constrained function can share its name with a class method. In that case,
+// @{...} should supply evidence to the function call, not eagerly dispatch to
+// the same-named method from the selected instance.
+
+forall a . class a : Score {
+  function score(x : a) -> word;
+}
+
+forall a . a : Score => function score(x : a, ignored : word) -> word {
+  return Score.score(x);
+}
+
+instance [fastScore] word : Score {
+  function score(x : word) -> word {
+    return 7;
+  }
+}
+
+contract NamedInstFunctionMethodCollision {
+  function main() -> word {
+    return score@{fastScore}(3, 5);
+  }
+}
diff --git a/test/examples/cases/named-inst-not-implicit.solc b/test/examples/cases/named-inst-not-implicit.solc
new file mode 100644
index 000000000..7b09995fa
--- /dev/null
+++ b/test/examples/cases/named-inst-not-implicit.solc
@@ -0,0 +1,18 @@
+// Named instances are explicit evidence and should not be used by ordinary
+// implicit instance search.
+
+forall a . class a : Score {
+  function score(x : a) -> word;
+}
+
+instance [fastScore] word : Score {
+  function score(x : word) -> word {
+    return 7;
+  }
+}
+
+contract NamedInstNotImplicit {
+  function main() -> word {
+    return Score.score(3);
+  }
+}
diff --git a/test/imports/namedinst_select_main.solc b/test/imports/namedinst_select_main.solc
new file mode 100644
index 000000000..422edd526
--- /dev/null
+++ b/test/imports/namedinst_select_main.solc
@@ -0,0 +1,7 @@
+import namedinst.a.{Score, byPriority};
+
+contract NamedInstSelectedImport {
+  function main() -> word {
+    return score@{byPriority}(1);
+  }
+}

From 0ac91e46104e46bb25ef9538e8035e6fc75bd08f Mon Sep 17 00:00:00 2001
From: Yoshitomo Nakanishi <yurayura.rounin.3@gmail.com>
Date: Fri, 8 May 2026 13:18:55 +0900
Subject: [PATCH 19/21] Update src/Solcore/Frontend/Parser/SolcoreParser.y

Co-authored-by: Marcin Benke <marcin.benke@argot.org>
---
 src/Solcore/Frontend/Parser/SolcoreParser.y | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Solcore/Frontend/Parser/SolcoreParser.y b/src/Solcore/Frontend/Parser/SolcoreParser.y
index c4b2d95c5..1b7a03da8 100644
--- a/src/Solcore/Frontend/Parser/SolcoreParser.y
+++ b/src/Solcore/Frontend/Parser/SolcoreParser.y
@@ -436,8 +436,9 @@ Expr : Name FunArgs                                {ExpName Nothing $1 $2}
      | '!' Expr                                    {ExpLNot $2 }
      | Conditional                                 {$1}
      | '@' Type                                    {ExpAt $2}
-     | Name '@{' ImplArgList '}' '(' ExprCommaList ')' { ExpNameAt Nothing $1 $3 $6 }
-     | Expr '.' Name '@{' ImplArgList '}' '(' ExprCommaList ')' { ExpNameAt (Just $1) $3 $5 $8 }
+     | Name '@{' ImplArgList '}' FunArgs { ExpNameAt Nothing $1 $3 $5 }
+     | Expr '.' Name '@{' ImplArgList '}' FunArgs { ExpNameAt (Just $1) $3 $5 $7 }
+
 
 Conditional :: { Exp }
 Conditional : 'if' Expr 'then' Expr 'else' Expr    {ExpCond $2 $4 $6}

From 097c1ee397ceff9770e29fa484149d7a3707b211 Mon Sep 17 00:00:00 2001
From: Yoshitomo Nakanishi <yurayura.rounin.3@gmail.com>
Date: Fri, 8 May 2026 11:32:30 +0900
Subject: [PATCH 20/21] Address named instance review feedback

---
 src/Solcore/Frontend/Syntax/NameResolution.hs | 69 ++++++++++++-------
 src/Solcore/Frontend/TypeInference/TcStmt.hs  | 31 ++++++---
 test/Cases.hs                                 |  3 +
 .../named-inst-function-label-clash.solc      | 16 +++++
 ...ed-inst-slot-capitalisation-ambiguous.solc | 32 +++++++++
 .../cases/named-inst-slot-capitalisation.solc | 32 +++++++++
 6 files changed, 151 insertions(+), 32 deletions(-)
 create mode 100644 test/examples/cases/named-inst-function-label-clash.solc
 create mode 100644 test/examples/cases/named-inst-slot-capitalisation-ambiguous.solc
 create mode 100644 test/examples/cases/named-inst-slot-capitalisation.solc

diff --git a/src/Solcore/Frontend/Syntax/NameResolution.hs b/src/Solcore/Frontend/Syntax/NameResolution.hs
index 2f04f52a2..56be67c96 100644
--- a/src/Solcore/Frontend/Syntax/NameResolution.hs
+++ b/src/Solcore/Frontend/Syntax/NameResolution.hs
@@ -515,8 +515,8 @@ instance Resolve S.Exp where
   resolve c@(S.ExpVar me n) =
     do
       me' <- resolve me `wrapError` c
-      dt <- lookupName n
-      case (me', dt) of
+      declType <- lookupName n
+      case (me', declType) of
         -- local variables
         (_, Just TLocalVar) -> pure (Var n)
         -- function parameters
@@ -525,7 +525,7 @@ instance Resolve S.Exp where
         (Nothing, Just TField) ->
           pure (FieldAccess Nothing n)
         -- function reference
-        (_, Just TFunction) -> do
+        (_, Just dt) | isFunctionDecl dt -> do
           dt1 <- gets (Map.lookup n . fieldEnv)
           case dt1 of
             Just TField -> pure (FieldAccess Nothing n)
@@ -544,7 +544,7 @@ instance Resolve S.Exp where
           let qn = QualName d (pretty n)
           qdt <- lookupName qn
           case qdt of
-            Just TFunction -> pure (Var qn)
+            Just dt | isFunctionDecl dt -> pure (Var qn)
             Just TDataCon -> Con <$> resolveQualifiedConstructorName d n <*> pure []
             Just TTyCon -> pure (Var qn)
             Just TModule -> pure (Var qn)
@@ -564,7 +564,7 @@ instance Resolve S.Exp where
           let qn = QualName d (pretty n)
           qdt <- lookupName qn
           case qdt of
-            Just TFunction -> pure (Var qn)
+            Just dt | isFunctionDecl dt -> pure (Var qn)
             Just TDataCon -> Con <$> resolveQualifiedConstructorName d n <*> pure []
             Just TTyCon -> pure (Var qn)
             Just TModule -> pure (Var qn)
@@ -587,11 +587,12 @@ instance Resolve S.Exp where
     do
       me' <- resolve me `wrapError` x
       es' <- resolve es `wrapError` x
-      dt <- lookupName n
-      case (me', dt) of
+      declType <- lookupName n
+      case (me', declType) of
         -- normal function call
-        (Nothing, Just TFunction) ->
-          pure (Call Nothing n [] es')
+        (Nothing, Just dt)
+          | isFunctionDecl dt ->
+              pure (Call Nothing n [] es')
         (Nothing, Just TTyCon) -> do
           sameName <- isSameNameConstructor n
           if sameName
@@ -611,11 +612,11 @@ instance Resolve S.Exp where
           let qn = QualName c (pretty n)
           qdt <- lookupName qn
           case qdt of
-            Just TFunction -> pure (Call Nothing qn [] es')
+            Just dt | isFunctionDecl dt -> pure (Call Nothing qn [] es')
             Just TDataCon -> Con <$> resolveQualifiedConstructorName c n <*> pure es'
             _ -> undefinedName n
         -- class functions
-        (Just (Var c), Just TFunction) -> do
+        (Just (Var c), Just dt) | isFunctionDecl dt -> do
           ct <- lookupName c
           let qn = QualName c (pretty n)
           case ct of
@@ -624,7 +625,7 @@ instance Resolve S.Exp where
             Just TModule -> do
               cf <- lookupName qn
               case cf of
-                Just TFunction -> pure (Call Nothing qn [] es')
+                Just dt' | isFunctionDecl dt' -> pure (Call Nothing qn [] es')
                 Just TDataCon -> Con <$> resolveQualifiedConstructorName c n <*> pure es'
                 _ -> undefinedName n
             _ -> undefinedName c
@@ -633,10 +634,12 @@ instance Resolve S.Exp where
           let qn = QualName c (pretty n)
           cf <- lookupName qn
           case (ct, cf) of
-            (Just TClass, Just TFunction) ->
-              pure (Call Nothing qn [] es')
-            (_, Just TFunction) ->
-              pure (Call Nothing qn [] es')
+            (Just TClass, Just dt)
+              | isFunctionDecl dt ->
+                  pure (Call Nothing qn [] es')
+            (_, Just dt)
+              | isFunctionDecl dt ->
+                  pure (Call Nothing qn [] es')
             (_, Just TDataCon) ->
               Con <$> resolveQualifiedConstructorName c n <*> pure es'
             _ -> do
@@ -650,7 +653,7 @@ instance Resolve S.Exp where
           let qn = QualName c (pretty n)
           cf <- gets (Map.lookup qn . scopeEnv)
           case cf of
-            Just TFunction -> pure (Call Nothing qn [] es')
+            Just dt | isFunctionDecl dt -> pure (Call Nothing qn [] es')
             _ -> undefinedName n
         -- variables
         (_, Just TLocalVar) ->
@@ -759,7 +762,7 @@ instance Resolve S.Exp where
             let qn = QualName c (pretty n)
             cf <- gets (Map.lookup qn . scopeEnv)
             case cf of
-              Just TFunction -> pure (Call Nothing qn implArgs' es')
+              Just dt | isFunctionDecl dt -> pure (Call Nothing qn implArgs' es')
               _ -> undefinedName n
           _ -> resolveNamedCall me' n implArgs' es'
       _ -> resolveNamedCall me' n implArgs' es'
@@ -833,6 +836,7 @@ instance Resolve S.Ty where
 data DeclType
   = TContract
   | TFunction
+  | TFunctionAndNamedInstance
   | TDataCon
   | TLocalVar
   | TParameter
@@ -845,6 +849,23 @@ data DeclType
   | TNamedInstance
   deriving (Eq, Show)
 
+isFunctionDecl :: DeclType -> Bool
+isFunctionDecl TFunction = True
+isFunctionDecl TFunctionAndNamedInstance = True
+isFunctionDecl _ = False
+
+isNamedInstanceDecl :: DeclType -> Bool
+isNamedInstanceDecl TNamedInstance = True
+isNamedInstanceDecl TFunctionAndNamedInstance = True
+isNamedInstanceDecl _ = False
+
+mergeScopeDecl :: DeclType -> DeclType -> DeclType
+mergeScopeDecl TFunction TNamedInstance = TFunctionAndNamedInstance
+mergeScopeDecl TNamedInstance TFunction = TFunctionAndNamedInstance
+mergeScopeDecl TFunctionAndNamedInstance _ = TFunctionAndNamedInstance
+mergeScopeDecl _ TFunctionAndNamedInstance = TFunctionAndNamedInstance
+mergeScopeDecl new _ = new
+
 data Env
   = Env
   { -- holds types and contracts. global visibility
@@ -922,7 +943,7 @@ addTopDecl (S.TContr (S.Contract n _ _)) env =
     env {typeEnv = Map.insert n TContract (typeEnv env)}
 addTopDecl (S.TFunDef (S.FunDef sig _)) env =
   addQualifiedModules (S.sigName sig) $
-    env {scopeEnv = Map.insert (S.sigName sig) TFunction (scopeEnv env)}
+    env {scopeEnv = Map.insertWith mergeScopeDecl (S.sigName sig) TFunction (scopeEnv env)}
 addTopDecl (S.TClassDef (S.Class _ _ n _ _ sigs)) env =
   let env' =
         foldr
@@ -956,7 +977,7 @@ addTopDecl (S.TExportDecl _) env = env
 addTopDecl (S.TInstDef (S.Instance _ (Just lbl) _ _ _ _ _ funs)) env =
   env
     { scopeEnv =
-        Map.insert lbl TNamedInstance $
+        Map.insertWith mergeScopeDecl lbl TNamedInstance $
           foldr
             ( \fd ac ->
                 let qn = QualName lbl (pretty (S.sigName (S.funSignature fd)))
@@ -979,9 +1000,9 @@ addQualifiedModules _ env = env
 resolveImplArg :: S.ImplArg -> ResolveM ImplArg
 resolveImplArg (S.ImplArg slot implName) = do
   dt <- lookupName implName
-  case dt of
-    Just TNamedInstance -> pure (ImplArg slot implName)
-    _ ->
+  if maybe False isNamedInstanceDecl dt
+    then pure (ImplArg slot implName)
+    else
       throwError $
         "Unknown named instance '"
           ++ pretty implName
@@ -1049,7 +1070,7 @@ addContractName n =
 
 addFunctionName :: Name -> ResolveM ()
 addFunctionName n =
-  modify (\env -> env {scopeEnv = Map.insert n TFunction (scopeEnv env)})
+  modify (\env -> env {scopeEnv = Map.insertWith mergeScopeDecl n TFunction (scopeEnv env)})
 
 addParameter :: Name -> ResolveM ()
 addParameter n =
diff --git a/src/Solcore/Frontend/TypeInference/TcStmt.hs b/src/Solcore/Frontend/TypeInference/TcStmt.hs
index 72228086e..157f777c4 100644
--- a/src/Solcore/Frontend/TypeInference/TcStmt.hs
+++ b/src/Solcore/Frontend/TypeInference/TcStmt.hs
@@ -1421,7 +1421,7 @@ tcCallWithNamedEvidence callExpr me n args resolvedImplArgs =
 solveNamedImplArgs :: Name -> [Pred] -> [ResolvedImplArg] -> TcM ([Pred], Subst, [Pred])
 solveNamedImplArgs _ ps [] = pure ([], mempty, ps)
 solveNamedImplArgs n ps ((implArg, inst) : rest) = do
-  matching <- catMaybes <$> mapM (namedImplArgSolvesWanted implArg inst) ps
+  matching <- namedImplArgSolvesWanteds n ps implArg inst
   case matching of
     [(p, instPreds, evidenceSubst)] -> do
       let psNext = apply evidenceSubst (delete p ps)
@@ -1448,12 +1448,26 @@ solveNamedImplArgs n ps ((implArg, inst) : rest) = do
             "Use an explicit constraint slot to disambiguate."
           ]
 
-namedImplArgSolvesWanted :: ImplArg -> Instance Name -> Pred -> TcM (Maybe (Pred, [Pred], Subst))
-namedImplArgSolvesWanted implArg inst wanted
-  | Just slot <- implArgSlot implArg,
-    not (slotMatchesPred slot wanted) =
-      pure Nothing
-  | otherwise = namedInstSolvesWanted inst wanted
+namedImplArgSolvesWanteds :: Name -> [Pred] -> ImplArg -> Instance Name -> TcM [(Pred, [Pred], Subst)]
+namedImplArgSolvesWanteds n ps implArg inst =
+  case implArgSlot implArg of
+    Nothing ->
+      catMaybes <$> mapM (namedInstSolvesWanted inst) ps
+    Just slot ->
+      case filter (slotMatchesPred slot) ps of
+        [] -> pure []
+        [wanted] -> maybeToList <$> namedInstSolvesWanted inst wanted
+        _ ->
+          throwError $
+            unlines
+              [ unwords
+                  [ "Constraint slot",
+                    pretty slot,
+                    "matches multiple wanted constraints for",
+                    pretty n
+                  ],
+                "Use a class name with exact capitalisation to disambiguate."
+              ]
 
 namedInstSolvesWanted :: Instance Name -> Pred -> TcM (Maybe (Pred, [Pred], Subst))
 namedInstSolvesWanted inst wanted =
@@ -1549,7 +1563,8 @@ matchesNamedCall callExpr n lbl allTys inst =
           pure True
         )
         `catchError` (\_ -> pure False)
-    put st
+    st' <- get
+    put st {nameSupply = nameSupply st', counter = counter st'}
     pure res
 
 tcCallNamedWithInst ::
diff --git a/test/Cases.hs b/test/Cases.hs
index fb346c3f1..7b4b3d98f 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -408,11 +408,14 @@ cases =
       runTestForFile "named-inst-constrained-call.solc" caseFolder,
       runTestExpectingFailure "named-inst-default-fail.solc" caseFolder,
       runTestForFile "named-inst-function-method-collision.solc" caseFolder,
+      runTestForFile "named-inst-function-label-clash.solc" caseFolder,
       runTestExpectingFailure "named-inst-no-matching-head.solc" caseFolder,
       runTestExpectingFailure "named-inst-not-implicit.solc" caseFolder,
       runTestExpectingFailure "named-inst-shared-label-params.solc" caseFolder,
       runTestForFile "named-inst-receiver.solc" caseFolder,
       runTestExpectingFailure "named-inst-shared-label.solc" caseFolder,
+      runTestForFile "named-inst-slot-capitalisation.solc" caseFolder,
+      runTestExpectingFailure "named-inst-slot-capitalisation-ambiguous.solc" caseFolder,
       runTestForFile "named-inst-slot-call.solc" caseFolder,
       runTestForFile "named-inst-two-instances.solc" caseFolder,
       runTestExpectingFailure "named-inst-unknown-label.solc" caseFolder,
diff --git a/test/examples/cases/named-inst-function-label-clash.solc b/test/examples/cases/named-inst-function-label-clash.solc
new file mode 100644
index 000000000..25d32bc8d
--- /dev/null
+++ b/test/examples/cases/named-inst-function-label-clash.solc
@@ -0,0 +1,16 @@
+// A named instance declaration may share its name with a term-level function.
+// The shared name should resolve as a function in ordinary calls.
+
+forall a . class a : C {}
+
+instance [foo] word : C {}
+
+function foo(x : word) -> word {
+  return 7;
+}
+
+contract NamedInstFunctionLabelClash {
+  function main() -> word {
+    return foo(1);
+  }
+}
diff --git a/test/examples/cases/named-inst-slot-capitalisation-ambiguous.solc b/test/examples/cases/named-inst-slot-capitalisation-ambiguous.solc
new file mode 100644
index 000000000..f6b415f37
--- /dev/null
+++ b/test/examples/cases/named-inst-slot-capitalisation-ambiguous.solc
@@ -0,0 +1,32 @@
+// The lowercase alias "eq" would identify both Eq and eq here, so it should
+// be rejected before using the selected instance head to pick one silently.
+
+forall a . class a : Eq {
+  function upperScore(x : a) -> word;
+}
+
+forall a . class a : eq {
+  function lowerScore(x : a) -> word;
+}
+
+forall a . a : Eq, a : eq => function useBoth(x : a) -> word {
+  return Eq.upperScore(x);
+}
+
+instance [upperEq] word : Eq {
+  function upperScore(x : word) -> word {
+    return 1;
+  }
+}
+
+instance [lowerEq] word : eq {
+  function lowerScore(x : word) -> word {
+    return 2;
+  }
+}
+
+contract NamedInstSlotCapitalisationAmbiguous {
+  function main() -> word {
+    return useBoth@{eq = upperEq}(1);
+  }
+}
diff --git a/test/examples/cases/named-inst-slot-capitalisation.solc b/test/examples/cases/named-inst-slot-capitalisation.solc
new file mode 100644
index 000000000..42da044e7
--- /dev/null
+++ b/test/examples/cases/named-inst-slot-capitalisation.solc
@@ -0,0 +1,32 @@
+// Lowercase slot aliases should not become ambiguous when two class names only
+// differ by capitalisation; exact class-name slots remain available.
+
+forall a . class a : Eq {
+  function upperScore(x : a) -> word;
+}
+
+forall a . class a : eq {
+  function lowerScore(x : a) -> word;
+}
+
+forall a . a : Eq, a : eq => function useBoth(x : a) -> word {
+  return Eq.upperScore(x);
+}
+
+instance [upperEq] word : Eq {
+  function upperScore(x : word) -> word {
+    return 1;
+  }
+}
+
+instance [lowerEq] word : eq {
+  function lowerScore(x : word) -> word {
+    return 2;
+  }
+}
+
+contract NamedInstSlotCapitalisation {
+  function main() -> word {
+    return useBoth@{Eq = upperEq, eq = lowerEq}(1);
+  }
+}

From 58b0b35c1dbecb7d22ecb25fc1d442481eae853d Mon Sep 17 00:00:00 2001
From: Yoshitomo Nakanishi <yurayura.rounin.3@gmail.com>
Date: Tue, 19 May 2026 10:45:11 +0900
Subject: [PATCH 21/21] Prefer exact named instance slot matches

---
 src/Solcore/Frontend/TypeInference/TcStmt.hs  | 31 ++++++++++++-----
 test/Cases.hs                                 |  1 +
 .../named-inst-slot-order-sensitivity.solc    | 33 +++++++++++++++++++
 3 files changed, 56 insertions(+), 9 deletions(-)
 create mode 100644 test/examples/cases/named-inst-slot-order-sensitivity.solc

diff --git a/src/Solcore/Frontend/TypeInference/TcStmt.hs b/src/Solcore/Frontend/TypeInference/TcStmt.hs
index 6579722e4..c756a4926 100644
--- a/src/Solcore/Frontend/TypeInference/TcStmt.hs
+++ b/src/Solcore/Frontend/TypeInference/TcStmt.hs
@@ -1458,7 +1458,7 @@ namedImplArgSolvesWanteds n ps implArg inst =
     Nothing ->
       catMaybes <$> mapM (namedInstSolvesWanted inst) ps
     Just slot ->
-      case filter (slotMatchesPred slot) ps of
+      case predsMatchingSlot slot ps of
         [] -> pure []
         [wanted] -> maybeToList <$> namedInstSolvesWanted inst wanted
         _ ->
@@ -1494,15 +1494,28 @@ solveNamedInstPred (InCls c t ts) (InCls c' t' ts')
       mgu (t : ts) (t' : ts')
 solveNamedInstPred _ _ = throwError "Named instance does not solve wanted predicate"
 
-slotMatchesPred :: Name -> Pred -> Bool
-slotMatchesPred slot (InCls cls _ _) = slot `elem` classSlotNames cls
-slotMatchesPred _ _ = False
+-- Exact class-name slots take precedence over lowercase aliases so Eq and eq
+-- can be disambiguated independently of named evidence argument order.
+predsMatchingSlot :: Name -> [Pred] -> [Pred]
+predsMatchingSlot slot ps =
+  let exactMatches = filter (slotMatchesExactClassName slot) ps
+   in if null exactMatches
+        then filter (slotMatchesLowerClassAlias slot) ps
+        else exactMatches
 
-classSlotNames :: Name -> [Name]
-classSlotNames cls =
-  nub [Name baseName, Name (lowerFirst baseName)]
-  where
-    baseName = nameLeaf cls
+slotMatchesExactClassName :: Name -> Pred -> Bool
+slotMatchesExactClassName slot (InCls cls _ _) = slot == classSlotName cls
+slotMatchesExactClassName _ _ = False
+
+slotMatchesLowerClassAlias :: Name -> Pred -> Bool
+slotMatchesLowerClassAlias slot (InCls cls _ _) = slot == lowerClassSlotAlias cls
+slotMatchesLowerClassAlias _ _ = False
+
+classSlotName :: Name -> Name
+classSlotName cls = Name (nameLeaf cls)
+
+lowerClassSlotAlias :: Name -> Name
+lowerClassSlotAlias cls = Name (lowerFirst (nameLeaf cls))
 
 nameLeaf :: Name -> String
 nameLeaf (Name s) = s
diff --git a/test/Cases.hs b/test/Cases.hs
index fae45fbef..75f9d54f7 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -421,6 +421,7 @@ cases =
       runTestForFile "named-inst-slot-capitalisation.solc" caseFolder,
       runTestExpectingFailure "named-inst-slot-capitalisation-ambiguous.solc" caseFolder,
       runTestForFile "named-inst-slot-call.solc" caseFolder,
+      runTestForFile "named-inst-slot-order-sensitivity.solc" caseFolder,
       runTestForFile "named-inst-two-instances.solc" caseFolder,
       runTestExpectingFailure "named-inst-unknown-label.solc" caseFolder,
       runTestExpectingFailure "named-inst-dup-label.solc" caseFolder,
diff --git a/test/examples/cases/named-inst-slot-order-sensitivity.solc b/test/examples/cases/named-inst-slot-order-sensitivity.solc
new file mode 100644
index 000000000..211b58ded
--- /dev/null
+++ b/test/examples/cases/named-inst-slot-order-sensitivity.solc
@@ -0,0 +1,33 @@
+// Exact class-name slots should disambiguate before lowercase aliases, so the
+// order of explicit named evidence does not matter when class names differ only
+// by capitalisation.
+
+forall a . class a : Eq {
+  function upperScore(x : a) -> word;
+}
+
+forall a . class a : eq {
+  function lowerScore(x : a) -> word;
+}
+
+forall a . a : Eq, a : eq => function useBoth(x : a) -> word {
+  return Eq.upperScore(x);
+}
+
+instance [upperEq] word : Eq {
+  function upperScore(x : word) -> word {
+    return 1;
+  }
+}
+
+instance [lowerEq] word : eq {
+  function lowerScore(x : word) -> word {
+    return 2;
+  }
+}
+
+contract NamedInstSlotOrderSensitivity {
+  function main() -> word {
+    return useBoth@{eq = lowerEq, Eq = upperEq}(1);
+  }
+}