diff --git a/flake.nix b/flake.nix
index be1036c87..749f4f8a7 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/${if pkgs.stdenv.isDarwin then "libevmone.dylib" else "libevmone.so"}";
+          evmone = evmone-shared-lib;
         };
       }
     );
diff --git a/src/Solcore/Backend/Specialise.hs b/src/Solcore/Backend/Specialise.hs
index d7e5a69ed..29f2acd06 100644
--- a/src/Solcore/Backend/Specialise.hs
+++ b/src/Solcore/Backend/Specialise.hs
@@ -10,9 +10,9 @@ 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 Data.Maybe (fromMaybe, isJust)
 import Solcore.Backend.Mast
 import Solcore.Desugarer.IfDesugarer (desugaredBoolTy)
 import Solcore.Frontend.Pretty.ShortName
@@ -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, 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 :: [(ImplArg, 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,23 @@ extSpSubst subst = modify $ \s -> s {spSubst = spSubst s <> subst}
 atCurrentSubst :: (HasTV a) => a -> SM a
 atCurrentSubst a = flip applytv a <$> getSpSubst
 
+withNamedEvidence :: ImplArg -> SM a -> SM a
+withNamedEvidence implArg action = do
+  env <- gets spGlobalEnv
+  case Map.lookup (implArgName implArg) (namedInstEnv env) of
+    Nothing -> action
+    Just inst -> do
+      saved <- gets spNamedEvidence
+      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)})
 
@@ -218,7 +237,32 @@ 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
+      case instLabel inst of
+        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
+-- 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
@@ -300,14 +344,101 @@ 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 $ implArgName . fst <$> find (matchesNamedEvidence cls methName funType) evidences
+    Name _ -> pure Nothing
+
+matchesNamedEvidence :: Name -> Name -> Ty -> (ImplArg, 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 args) ty = do
+specExp (Call Nothing i [] 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'
+  mlbl <- explicitNamedEvidenceForCall i args ty
+  case mlbl of
+    Just lbl -> specExp (Call Nothing i [ImplArg Nothing lbl] args) ty
+    Nothing -> do
+      (i'', args') <- specCall i args ty
+      let e' = Call Nothing i'' [] args'
+      -- debug ["< specExp (Call): ", pretty e']
+      return e'
+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
+  hasFunctionResolution <- callHasResolution i args ty
+  (i'', args') <-
+    if isNamedMethod && not hasFunctionResolution
+      then do
+        let i' = i {idName = QualName lbl (methodNameString (idName i))}
+        specCall i' args ty
+      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
@@ -347,8 +478,18 @@ 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 []
+
+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
   i' <- atCurrentSubst i
   ty' <- atCurrentSubst ty
   -- debug ["> specCall: ", pretty i', show args, " : ", pretty ty']
@@ -372,21 +513,28 @@ specCall i args ty = do
             prettys (map snd varToVar),
             "\n  The intermediate type cannot be determined from this call site.",
             "\n  Expression: ",
-            pretty (Call Nothing i args),
+            pretty (Call Nothing i [] args),
             "\n  This often occurs when a polymorphic-return function (e.g. `require`)",
             "\n  is passed directly to a polymorphic-argument function (e.g. `void`)."
           ]
       extSpSubst phi
       subst <- getSpSubst
       let ty'' = applytv subst fty
-      ensureClosed ty'' (Call Nothing i args) subst
-      name' <- 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'')
     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`
@@ -587,7 +735,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
@@ -893,7 +1041,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 838e38d9d..f854baf46 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" [] (Just unit)) body
-    body = [StmtExp (Call Nothing (QualName "RunContract" "exec") [cdata])]
+    body = [StmtExp (Call Nothing (QualName "RunContract" "exec") [] [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"
+                []
                 [ 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" [] [])),
         -- , Match [Var "conargs"] ...
         Let "fun" Nothing (Just (Var initFunName)),
-        StmtExp $ Call Nothing "fun" [Var "conargs"],
+        StmtExp $ Call Nothing "fun" [] [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 7756ad3de..ca2b5bf19 100644
--- a/src/Solcore/Desugarer/DecisionTreeCompiler.hs
+++ b/src/Solcore/Desugarer/DecisionTreeCompiler.hs
@@ -275,8 +275,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) =
@@ -287,8 +287,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
@@ -656,7 +656,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 1aaf28f18..9f19b0a99 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",
@@ -188,7 +189,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 [] [lhs', rhs']
 transAssignment lhs rhs cenv =
   traces ["Other assignment:", pretty (lhs := rhs)] $
     (lhs := rhs')
@@ -212,7 +213,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 [] [lhs', rhs']
 
 transRhs :: (HasCallStack) => NmExp -> CEM NmExp
 transRhs expr@(FieldAccess Nothing x) cenv
@@ -229,7 +230,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
@@ -250,13 +251,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) [] [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) [] [arr', idx2']
 indexAccess _dir exp idx = notImplemented "indexAccess" (Indexed exp idx)
 
 lhsIndex, rhsIndex :: (HasCallStack) => NmExp -> NmExp -> CEM (Exp Name)
@@ -319,10 +320,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") [] [e]
 
 rhsAccess :: Exp Name -> Exp Name
-rhsAccess e = Call Nothing (QualName "RVA" "acc") [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/IfDesugarer.hs b/src/Solcore/Desugarer/IfDesugarer.hs
index a4a9f6b85..27a3863e6 100644
--- a/src/Solcore/Desugarer/IfDesugarer.hs
+++ b/src/Solcore/Desugarer/IfDesugarer.hs
@@ -37,8 +37,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 e2221c216..ab2701e63 100644
--- a/src/Solcore/Desugarer/IndirectCall.hs
+++ b/src/Solcore/Desugarer/IndirectCall.hs
@@ -98,18 +98,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 implArgs es) =
     do
       m' <- desugar m
       es' <- desugar es
       b <- isDirectCall n
       let qn = QualName invokableName "invoke"
           args' = [Var n, indirectArgs es']
-      if b
+      -- Explicit instance calls are always direct: no defunctionalization.
+      if b || not (null implArgs)
         then
-          pure $ Call m' n es'
+          pure $ Call m' n implArgs es'
         else
-          pure $ Call Nothing qn args'
+          pure $ Call Nothing qn [] args'
   desugar (Cond e1 e2 e3) =
     Cond <$> desugar e1 <*> desugar e2 <*> desugar e3
   desugar x = pure x
@@ -118,8 +119,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/Module/Loader.hs b/src/Solcore/Frontend/Module/Loader.hs
index a829123ff..5f71ea383 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,82 @@ 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 (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
+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)
@@ -1460,6 +1538,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 implArgs es) =
+  ExpNameAt me' n' implArgs 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 ->
@@ -1644,6 +1730,12 @@ renameExpTypeRefs renameMap (ExpName me n es) =
     (renameMemberQualifierTypeRefs renameMap <$> me)
     n
     (map (renameExpTypeRefs renameMap) es)
+renameExpTypeRefs renameMap (ExpNameAt me n implArgs es) =
+  ExpNameAt
+    (renameMemberQualifierTypeRefs renameMap <$> me)
+    n
+    implArgs
+    (map (renameExpTypeRefs renameMap) es)
 renameExpTypeRefs renameMap (ExpVar Nothing n) =
   ExpVar
     (sameNameConstructorQualifier renameMap n)
@@ -1751,9 +1843,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
@@ -1890,7 +1983,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
 
@@ -1921,7 +2014,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
@@ -1933,8 +2027,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
@@ -1960,6 +2053,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
@@ -1995,7 +2095,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
@@ -2262,6 +2365,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
@@ -2418,9 +2528,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]
@@ -2462,8 +2572,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 _) =
@@ -2503,7 +2614,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 4058cfaab..609c009c8 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}
@@ -446,10 +451,21 @@ Expr : Name FunArgs                                {ExpName Nothing $1 $2}
      | '!' Expr                                    {ExpLNot $2 }
      | Conditional                                 {$1}
      | '@' Type                                    {ExpAt $2}
+     | 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}
 
+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/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 1941854c7..d0466e3cc 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
 
@@ -375,8 +380,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 implArgs es) =
+    pprE e <> ppr n <> pprCallImplArgs implArgs <> (parens (nest 1 $ commaSep $ map ppr es))
   ppr (Lam args bd _) =
     text "lam"
       <+> pprParams args
@@ -395,6 +400,14 @@ pprE :: (Pretty a) => Maybe (Exp a) -> Doc
 pprE Nothing = ""
 pprE (Just e) = ppr e <> 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) =
     ppr n
diff --git a/src/Solcore/Frontend/Pretty/TreePretty.hs b/src/Solcore/Frontend/Pretty/TreePretty.hs
index c17a35bac..66575bdb3 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"
@@ -354,6 +354,13 @@ instance Pretty Exp where
       <> parensWhen
         (not $ null es)
         (commaSep (map ppr es))
+  ppr (ExpNameAt me n implArgs es) =
+    maybe empty (\e -> ppr e <> char '.') me
+      <> ppr n
+      <> text "@{"
+      <> commaSep (map ppr implArgs)
+      <> char '}'
+      <> parens (commaSep (map ppr es))
   ppr (ExpVar me v) =
     maybe empty (\e -> ppr e <> char '.') me
       <> ppr v
@@ -413,6 +420,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/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 23740204e..7ddbf3e2c 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
@@ -274,7 +281,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 +293,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
@@ -512,8 +519,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
@@ -522,7 +529,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)
@@ -541,7 +548,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)
@@ -561,7 +568,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)
@@ -584,11 +591,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
@@ -608,20 +616,20 @@ 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
             Just TClass ->
-              pure (Call Nothing qn es')
+              pure (Call Nothing qn [] es')
             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
@@ -630,10 +638,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
@@ -647,13 +657,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 dt | isFunctionDecl dt -> pure (Call Nothing qn [] es')
             _ -> undefinedName n
         -- variables
         (_, Just TLocalVar) ->
-          pure (Call Nothing n es')
+          pure (Call Nothing n [] es')
         (_, Just TParameter) ->
-          pure (Call Nothing n es')
+          pure (Call Nothing n [] es')
         -- error
         _ -> do
           sameName <- isSameNameConstructor n
@@ -669,31 +679,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 [] [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 [] [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 [] [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 [] [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 [] [e1', e2']
   resolve c@(S.ExpIndexed array idx) = do
     arr' <- resolve array `wrapError` c
     idx' <- resolve idx `wrapError` c
@@ -701,40 +711,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") [] [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 [] [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") [] [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") [] [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 [] [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") [] [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") [] [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") [] [e1', e2']
   resolve c@(S.ExpLNot e) = do
     e' <- resolve e `wrapError` c
-    pure $ Call Nothing (Name "not") [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
@@ -744,6 +754,22 @@ instance Resolve S.Exp where
           (Con (Name "Proxy") [])
           (TyCon (Name "Proxy") [t'])
       )
+  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
+        case ct of
+          Just TClass -> do
+            let qn = QualName c (pretty n)
+            cf <- gets (Map.lookup qn . scopeEnv)
+            case cf of
+              Just dt | isFunctionDecl dt -> pure (Call Nothing qn implArgs' es')
+              _ -> undefinedName n
+          _ -> resolveNamedCall me' n implArgs' es'
+      _ -> resolveNamedCall me' n implArgs' es'
 
 instance Resolve S.Literal where
   type Result S.Literal = Literal
@@ -814,6 +840,7 @@ instance Resolve S.Ty where
 data DeclType
   = TContract
   | TFunction
+  | TFunctionAndNamedInstance
   | TDataCon
   | TLocalVar
   | TParameter
@@ -823,8 +850,26 @@ data DeclType
   | TTyCon
   | TTyVar
   | TModule
+  | 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
@@ -902,7 +947,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
@@ -933,6 +978,18 @@ 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 =
+        Map.insertWith mergeScopeDecl 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
 
 addModuleName :: Name -> Env -> Env
@@ -944,6 +1001,22 @@ addQualifiedModules (QualName qualifier _) env =
   foldr addModuleName env (modulePrefixes qualifier)
 addQualifiedModules _ env = env
 
+resolveImplArg :: S.ImplArg -> ResolveM ImplArg
+resolveImplArg (S.ImplArg slot implName) = do
+  dt <- lookupName implName
+  if maybe False isNamedInstanceDecl dt
+    then pure (ImplArg slot implName)
+    else
+      throwError $
+        "Unknown named instance '"
+          ++ 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
@@ -1001,7 +1074,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/Syntax/Stmt.hs b/src/Solcore/Frontend/Syntax/Stmt.hs
index d5a5c1911..0f46b4140 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
@@ -33,6 +34,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
@@ -40,7 +48,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 [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 3104d6dce..f8ff83162 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,
@@ -255,6 +256,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
@@ -281,6 +289,9 @@ data Exp
   | ExpLNot Exp -- ! e
   | ExpCond Exp Exp Exp -- if e1 then e2 else e3
   | ExpAt Ty -- proxy sugar
+  | -- | 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/Erase.hs b/src/Solcore/Frontend/TypeInference/Erase.hs
index 170a38198..e4d3fda5b 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
@@ -71,8 +71,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..afcfb6825 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 [] 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 bdcf2def5..2ffde665b 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
@@ -212,7 +212,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 95e8bfcb8..c3d0c7fa2 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 declaration name)
     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..5a2c2c26b 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 d45a57330..39a245332 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
@@ -342,8 +343,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 [] args) =
   tcCall me n 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
@@ -878,14 +881,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) =
@@ -900,12 +903,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
@@ -915,10 +918,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
@@ -1065,7 +1068,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
@@ -1083,31 +1086,42 @@ 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
+        when d $
+          throwError $
+            "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
 maybeExpandSynonym (TyCon n ts) = do
@@ -1337,7 +1351,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 [] args)
     (ps :=> t) <- freshInst s
     t' <- freshTyVar
     expectedArgTys <- mapM (const freshTyVar) args
@@ -1349,11 +1363,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) [] 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 [] args)
     (ps1 :=> t) <- freshInst s
     t' <- freshTyVar
     expectedArgTys <- mapM (const freshTyVar) args
@@ -1364,7 +1378,267 @@ 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') [] 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, 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 ->
+    case mInst of
+      Just inst -> pure (implArg, inst)
+      Nothing ->
+        throwError $
+          "Unknown named instance: " ++ pretty implName
+
+tcCallWithNamedEvidence ::
+  Exp Name ->
+  Maybe (Exp Name) ->
+  Name ->
+  [Exp Name] ->
+  [ResolvedImplArg] ->
+  TcM (Exp Id, [Pred], Ty)
+tcCallWithNamedEvidence callExpr me n args resolvedImplArgs =
+  do
+    (call, ps, ty) <- tcCall me n args
+    (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 $ "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 <- namedImplArgSolvesWanteds n ps implArg inst
+  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."
+          ]
+
+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 predsMatchingSlot 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 =
+  (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"
+
+-- 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
+
+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
+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
+   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)
+
+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 $
+            unwords
+              ["Method", pretty n, "not found in named instance", pretty lbl]
+        )
+        pure
+        (findNamedMethod meth inst)
+    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)
+    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)
+    st' <- get
+    put st {nameSupply = nameSupply st', counter = counter 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
+    s' <- unify t (funtype allTys t') `wrapError` callExpr
+    _ <- extSubst s'
+    let ps' = foldr union [] (ps : recvPreds : pss')
+        t1 = funtype allTys t'
+    withCurrentSubst (Call Nothing (Id n t1) [ImplArg Nothing lbl] allArgs, ps', t')
 
 tcParam :: Param Name -> TcM (Param Id)
 tcParam (Typed n t) =
@@ -1697,8 +1971,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 0b610157a..4fb9624a7 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
diff --git a/test/Cases.hs b/test/Cases.hs
index 1d7d594c4..e9519b086 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -147,6 +147,8 @@ imports =
       runImportSuccess "dupqual_main.solc",
       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",
@@ -415,6 +417,25 @@ cases =
       runTestForFile "redundant-match.solc" caseFolder,
       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,
+      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-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,
       runTestForFile "invokable-issue.solc" caseFolder,
       runTestForFile "td.solc" caseFolder,
       runTestForFile "bar.solc" caseFolder,
diff --git a/test/MatchCompilerTests.hs b/test/MatchCompilerTests.hs
index 0f61b005b..4934ab2f6 100644
--- a/test/MatchCompilerTests.hs
+++ b/test/MatchCompilerTests.hs
@@ -541,8 +541,8 @@ test_compileMatch_bindsScrutineeOnce =
     let idZ = Id (Name "z") tyBool
         stmt =
           Match
-            [Call Nothing idF []]
-            [([PVar idZ], [Return (Call Nothing idG [Var idZ, Var idZ])])]
+            [Call Nothing idF [] []]
+            [([PVar idZ], [Return (Call Nothing idG [] [Var idZ, Var idZ])])]
     r <- runCompileStmt boolEnv stmt
     case r of
       Left err -> assertFailure ("unexpected error: " ++ err)
@@ -557,7 +557,7 @@ test_compileMatch_bindsScrutineeOnce =
       everything (+) (mkQ 0 countExp)
       where
         countExp :: Exp Id -> Int
-        countExp (Call Nothing i _) | idName i == target = 1
+        countExp (Call Nothing i _ _) | idName i == target = 1
         countExp _ = 0
 
 -- 14. Rows after a first all-var row are warned as unreachable even when they
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..acb06f0c6
--- /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 Bool.True;
+  }
+}
+
+instance [shared] word : Bar {
+  function run(x : word) -> Bool {
+    return Bool.False;
+  }
+}
+
+contract NamedInstAmbiguousUnqualified {
+  function main() -> Bool {
+    return run@{shared}(1);
+  }
+}
diff --git a/test/examples/cases/named-inst-basic.solc b/test/examples/cases/named-inst-basic.solc
new file mode 100644
index 000000000..0f236fdf4
--- /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 Bool.False;
+    | _ => return Bool.True;
+    }
+  }
+}
+
+instance [myEq] word : Eq {
+  function eq(x : word, y : word) -> Bool {
+    match primEqWord(x, y) {
+    | 0 => return Bool.False;
+    | _ => return Bool.True;
+    }
+  }
+}
+
+contract NamedInstBasic {
+  function main() -> Bool {
+    return eq@{myEq}(1, 1);
+  }
+}
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..ff4dcc6fc
--- /dev/null
+++ b/test/examples/cases/named-inst-class-qualified.solc
@@ -0,0 +1,31 @@
+// Class-qualified named calls should dispatch through the selected instance.
+
+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 [fooShared] word : Foo {
+  function run(x : word) -> Bool {
+    return Bool.True;
+  }
+}
+
+instance [barShared] word : Bar {
+  function run(x : word) -> Bool {
+    return Bool.False;
+  }
+}
+
+contract NamedInstClassQualified {
+  function main() -> Bool {
+    let x : Bool = Foo.run@{fooShared}(1);
+    let y : Bool = Bar.run@{barShared}(1);
+    return y;
+  }
+}
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);
+  }
+}
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-dup-label.solc b/test/examples/cases/named-inst-dup-label.solc
new file mode 100644
index 000000000..c52c1e74f
--- /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 Bool.True;
+  }
+}
+
+instance [dupLabel] word : Eq {
+  function eq(x : word, y : word) -> Bool {
+    return Bool.False;
+  }
+}
+
+contract NamedInstDupLabel {
+  function main() -> Bool {
+    return eq@{dupLabel}(1, 1);
+  }
+}
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-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-no-matching-head.solc b/test/examples/cases/named-inst-no-matching-head.solc
new file mode 100644
index 000000000..18058d49b
--- /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, Flag.F);
+  }
+}
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/examples/cases/named-inst-receiver.solc b/test/examples/cases/named-inst-receiver.solc
new file mode 100644
index 000000000..5e2dea80e
--- /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 Bool.False;
+    | _ => return Bool.True;
+    }
+  }
+}
+
+contract NamedInstReceiver {
+  function main() -> Bool {
+    return 1.eq@{myEq}(1);
+  }
+}
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..1d2ed1dc7
--- /dev/null
+++ b/test/examples/cases/named-inst-shared-label-params.solc
@@ -0,0 +1,28 @@
+// Reusing a named-instance declaration name in one module is rejected even
+// when the instance heads differ by weak parameters.
+
+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, Bool.True);
+    return y;
+  }
+}
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..332d3c1e5
--- /dev/null
+++ b/test/examples/cases/named-inst-shared-label.solc
@@ -0,0 +1,30 @@
+// Reusing the same named-instance declaration name in one module is rejected.
+
+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 Bool.True;
+  }
+}
+
+instance [shared] Bool : Eq {
+  function eq(x : Bool, y : Bool) -> Bool {
+    match x, y {
+    | Bool.True, Bool.True => return Bool.True;
+    | _, _ => return Bool.False;
+    }
+  }
+}
+
+contract NamedInstSharedLabel {
+  function main() -> Bool {
+    let x : Bool = eq@{shared}(1, 2);
+    let y : Bool = eq@{shared}(Bool.True, Bool.True);
+    return y;
+  }
+}
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);
+  }
+}
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);
+  }
+}
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);
+  }
+}
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..429fef761
--- /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 Bool.False;
+    | _ => return Bool.True;
+    }
+  }
+}
+
+// Named instance: always equal (trivial equality)
+instance [trivialEq] word : Eq {
+  function eq(x : word, y : word) -> Bool {
+    return Bool.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);
+  }
+}
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;
+  }
+}
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);
+  }
+}