diff --git a/sol-core.cabal b/sol-core.cabal
index 1f4565cc0..cbc3df7d9 100644
--- a/sol-core.cabal
+++ b/sol-core.cabal
@@ -64,6 +64,7 @@ library
       Solcore.Backend.MastEval
       Solcore.Backend.Specialise
       Solcore.Desugarer.DecisionTreeCompiler
+      Solcore.Desugarer.DeriveGeneric
       Solcore.Desugarer.FieldAccess
       Solcore.Desugarer.IfDesugarer
       Solcore.Desugarer.IndirectCall
diff --git a/src/Solcore/Desugarer/DeriveGeneric.hs b/src/Solcore/Desugarer/DeriveGeneric.hs
new file mode 100644
index 000000000..d97372306
--- /dev/null
+++ b/src/Solcore/Desugarer/DeriveGeneric.hs
@@ -0,0 +1,199 @@
+module Solcore.Desugarer.DeriveGeneric where
+
+import Data.List (nub)
+import Data.List.NonEmpty (toList)
+import Solcore.Frontend.Syntax
+
+-- Generate Generic instances for data types
+
+deriveGenericTopDecls :: [DataTy] -> [TopDecl Name] -> Either String [TopDecl Name]
+deriveGenericTopDecls localData allDecls
+  | not (genericClassVisible allDecls) = Right allDecls
+  | (n : _) <- conflicts = Left (conflictError n)
+  | otherwise = Right (allDecls ++ newInsts)
+  where
+    excluded = pragmaExcluded allDecls
+    hasInst = existingGenericTypes allDecls
+    conflicts =
+      [ dataName dt
+        | dt <- localData,
+          dataName dt `elem` hasInst,
+          dataName dt `notElem` excluded
+      ]
+    newInsts =
+      [ TInstDef (buildInstance dt)
+        | dt <- localData,
+          not (null (dataConstrs dt)),
+          dataName dt `notElem` excluded,
+          dataName dt `notElem` hasInst
+      ]
+    conflictError n =
+      "type '"
+        ++ show n
+        ++ "' has a manual Generic instance "
+        ++ "but no 'pragma no-generic-instance-for "
+        ++ show n
+        ++ "'; "
+        ++ "add the pragma to suppress auto-derivation"
+
+genericClassVisible :: [TopDecl Name] -> Bool
+genericClassVisible = any isGenericClass
+  where
+    isGenericClass (TClassDef cls) = className cls == Name "Generic"
+    isGenericClass _ = False
+
+collectDataDefs :: [TopDecl Name] -> [DataTy]
+collectDataDefs = concatMap go
+  where
+    go (TDataDef dt) = [dt]
+    go (TContr (Contract _ _ ds)) = [dt | CDataDecl dt <- ds]
+    go _ = []
+
+existingGenericTypes :: [TopDecl Name] -> [Name]
+existingGenericTypes = concatMap go
+  where
+    go (TInstDef inst)
+      | instName inst == Name "Generic" = [tyConName (mainTy inst)]
+    go _ = []
+    tyConName (TyCon n _) = n
+    tyConName _ = Name ""
+
+pragmaExcluded :: [TopDecl Name] -> [Name]
+pragmaExcluded = nub . concatMap go
+  where
+    go (TPragmaDecl (Pragma NoGenericInstanceFor (DisableFor names))) =
+      toList names
+    go _ = []
+
+-- SOP representation type
+
+unitTy :: Ty
+unitTy = TyCon (Name "()") []
+
+mkProdOf :: [Ty] -> Ty
+mkProdOf [] = unitTy
+mkProdOf [t] = t
+mkProdOf (t : ts) = TyCon (Name "pair") [t, mkProdOf ts]
+
+mkSumOf :: [Ty] -> Ty
+mkSumOf [] = unitTy
+mkSumOf [t] = t
+mkSumOf (t : ts) = TyCon (Name "sum") [t, mkSumOf ts]
+
+constrRep :: Constr -> Ty
+constrRep (Constr _ []) = unitTy
+constrRep (Constr _ [t]) = t
+constrRep (Constr _ ts) = mkProdOf ts
+
+sopRep :: DataTy -> Ty
+sopRep dt = mkSumOf (map constrRep (dataConstrs dt))
+
+-- Expression helpers
+
+mkProdExp :: [Exp Name] -> Exp Name
+mkProdExp [] = Con (Name "()") []
+mkProdExp [e] = e
+mkProdExp (e : es) = Con (Name "pair") [e, mkProdExp es]
+
+applyInr :: Int -> Exp Name -> Exp Name
+applyInr 0 e = e
+applyInr n e = Con (Name "inr") [applyInr (n - 1) e]
+
+wrapSumExp :: Int -> Int -> Exp Name -> Exp Name
+wrapSumExp _ 1 inner = inner
+wrapSumExp idx total inner
+  | idx == total - 1 = applyInr (total - 1) inner
+  | otherwise = applyInr idx (Con (Name "inl") [inner])
+
+pairPat :: Pat Name -> Pat Name -> Pat Name
+pairPat p1 p2 = PCon (Name "pair") [p1, p2]
+
+mkProdPat :: [Name] -> Pat Name
+mkProdPat [] = PCon (Name "()") []
+mkProdPat [v] = PVar v
+mkProdPat vs = foldr1 pairPat (map PVar vs)
+
+applyPInr :: Int -> Pat Name -> Pat Name
+applyPInr 0 p = p
+applyPInr n p = PCon (Name "inr") [applyPInr (n - 1) p]
+
+wrapSumPat :: Int -> Int -> Pat Name -> Pat Name
+wrapSumPat _ 1 inner = inner
+wrapSumPat idx total inner
+  | idx == total - 1 = applyPInr (total - 1) inner
+  | otherwise = applyPInr idx (PCon (Name "inl") [inner])
+
+freshVarNames :: Int -> [Name]
+freshVarNames n = [Name ("_gv" ++ show i) | i <- [0 .. n - 1]]
+
+fromClause :: Int -> Int -> Constr -> Equation Name
+fromClause idx total (Constr cname tys) =
+  let vars = freshVarNames (length tys)
+      pat = PCon cname (map PVar vars)
+      prodExp = mkProdExp (map Var vars)
+      sumExp = wrapSumExp idx total prodExp
+   in ([pat], [Return sumExp])
+
+fromBody :: DataTy -> Body Name
+fromBody dt =
+  let constrs = dataConstrs dt
+      total = length constrs
+   in [Match [Var (Name "_x")] (zipWith (\i c -> fromClause i total c) [0 ..] constrs)]
+
+toClause :: Int -> Int -> Constr -> Equation Name
+toClause idx total (Constr cname tys) =
+  let vars = freshVarNames (length tys)
+      prodPat = mkProdPat vars
+      sumPat = wrapSumPat idx total prodPat
+      conExp = Con cname (map Var vars)
+   in ([sumPat], [Return conExp])
+
+toBody :: DataTy -> Body Name
+toBody dt =
+  let constrs = dataConstrs dt
+      total = length constrs
+   in [Match [Var (Name "_r")] (zipWith (\i c -> toClause i total c) [0 ..] constrs)]
+
+buildFrom :: DataTy -> FunDef Name
+buildFrom dt = FunDef False sig (fromBody dt)
+  where
+    mainT = TyCon (dataName dt) (map TyVar (dataParams dt))
+    repT = sopRep dt
+    sig =
+      Signature
+        { sigVars = [],
+          sigContext = [],
+          sigName = Name "from",
+          sigParams = [Typed False (Name "_x") mainT],
+          sigRetComptime = False,
+          sigReturn = Just repT,
+          sigPayable = False
+        }
+
+buildTo :: DataTy -> FunDef Name
+buildTo dt = FunDef False sig (toBody dt)
+  where
+    mainT = TyCon (dataName dt) (map TyVar (dataParams dt))
+    repT = sopRep dt
+    sig =
+      Signature
+        { sigVars = [],
+          sigContext = [],
+          sigName = Name "to",
+          sigParams = [Typed False (Name "_r") repT],
+          sigRetComptime = False,
+          sigReturn = Just mainT,
+          sigPayable = False
+        }
+
+buildInstance :: DataTy -> Instance Name
+buildInstance dt =
+  Instance
+    { instDefault = False,
+      instVars = dataParams dt,
+      instContext = [],
+      instName = Name "Generic",
+      paramsTy = [sopRep dt],
+      mainTy = TyCon (dataName dt) (map TyVar (dataParams dt)),
+      instFunctions = [buildFrom dt, buildTo dt]
+    }
diff --git a/src/Solcore/Frontend/Parser/Decl.hs b/src/Solcore/Frontend/Parser/Decl.hs
index a38c34776..93f47478d 100644
--- a/src/Solcore/Frontend/Parser/Decl.hs
+++ b/src/Solcore/Frontend/Parser/Decl.hs
@@ -183,7 +183,7 @@ pragmaP :: Parser Pragma
 pragmaP = do
   keyword "pragma"
   ty <- pragmaTypeP
-  st <- pragmaStatusP
+  st <- pragmaStatusForP ty
   _ <- semicolon
   return (Pragma ty st)
 
@@ -195,9 +195,17 @@ pragmaTypeP =
     <$ keyword "no-patterson-condition"
       <|> NoBoundVariableCondition
     <$ keyword "no-bounded-variable-condition"
-
-pragmaStatusP :: Parser PragmaStatus
-pragmaStatusP = option DisableAll $ do
+      <|> NoGenericInstanceFor
+    <$ keyword "no-generic-instance-for"
+
+-- | Parse the pragma status.  For 'NoGenericInstanceFor' a non-empty list of
+-- type names is mandatory; for all other pragma types the list is optional and
+-- defaults to 'DisableAll'.
+pragmaStatusForP :: PragmaType -> Parser PragmaStatus
+pragmaStatusForP NoGenericInstanceFor = do
+  names <- (Name <$> identifier) `sepBy1` comma
+  return (DisableFor (NE.fromList names))
+pragmaStatusForP _ = option DisableAll $ do
   names <- (Name <$> identifier) `sepBy1` comma
   return (DisableFor (NE.fromList names))
 
diff --git a/src/Solcore/Frontend/Pretty/SolcorePretty.hs b/src/Solcore/Frontend/Pretty/SolcorePretty.hs
index aa4803762..6bef0cf53 100644
--- a/src/Solcore/Frontend/Pretty/SolcorePretty.hs
+++ b/src/Solcore/Frontend/Pretty/SolcorePretty.hs
@@ -132,6 +132,7 @@ instance Pretty PragmaType where
   ppr NoBoundVariableCondition = text "no-bounded-variable-condition"
   ppr NoCoverageCondition = text "no-coverage-condition"
   ppr NoPattersonCondition = text "no-patterson-condition"
+  ppr NoGenericInstanceFor = text "no-generic-instance-for"
 
 instance Pretty PragmaStatus where
   ppr (DisableFor ns) =
diff --git a/src/Solcore/Frontend/Pretty/TreePretty.hs b/src/Solcore/Frontend/Pretty/TreePretty.hs
index 0d10ed6ec..792f38eb5 100644
--- a/src/Solcore/Frontend/Pretty/TreePretty.hs
+++ b/src/Solcore/Frontend/Pretty/TreePretty.hs
@@ -110,6 +110,7 @@ instance Pretty PragmaType where
   ppr NoBoundVariableCondition = text "no-bounded-variable-condition"
   ppr NoCoverageCondition = text "no-coverage-condition"
   ppr NoPattersonCondition = text "no-patterson-condition"
+  ppr NoGenericInstanceFor = text "no-generic-instance-for"
 
 instance Pretty PragmaStatus where
   ppr (DisableFor ns) =
diff --git a/src/Solcore/Frontend/Syntax/Contract.hs b/src/Solcore/Frontend/Syntax/Contract.hs
index 0a49a425e..683ea2198 100644
--- a/src/Solcore/Frontend/Syntax/Contract.hs
+++ b/src/Solcore/Frontend/Syntax/Contract.hs
@@ -33,6 +33,7 @@ data PragmaType
   = NoCoverageCondition
   | NoPattersonCondition
   | NoBoundVariableCondition
+  | NoGenericInstanceFor
   deriving (Eq, Ord, Show, Data, Typeable)
 
 data PragmaStatus
diff --git a/src/Solcore/Frontend/Syntax/NameResolution.hs b/src/Solcore/Frontend/Syntax/NameResolution.hs
index 7d76dc9e3..4d2b6d9d0 100644
--- a/src/Solcore/Frontend/Syntax/NameResolution.hs
+++ b/src/Solcore/Frontend/Syntax/NameResolution.hs
@@ -327,6 +327,8 @@ instance Resolve S.PragmaType where
     pure NoPattersonCondition
   resolve S.NoBoundVariableCondition =
     pure NoBoundVariableCondition
+  resolve S.NoGenericInstanceFor =
+    pure NoGenericInstanceFor
 
 instance Resolve S.PragmaStatus where
   type Result S.PragmaStatus = PragmaStatus
diff --git a/src/Solcore/Frontend/Syntax/SyntaxTree.hs b/src/Solcore/Frontend/Syntax/SyntaxTree.hs
index 2e892a02a..22a7acb04 100644
--- a/src/Solcore/Frontend/Syntax/SyntaxTree.hs
+++ b/src/Solcore/Frontend/Syntax/SyntaxTree.hs
@@ -32,6 +32,7 @@ data PragmaType
   = NoCoverageCondition
   | NoPattersonCondition
   | NoBoundVariableCondition
+  | NoGenericInstanceFor
   deriving (Eq, Ord, Show, Data, Typeable)
 
 data PragmaStatus
diff --git a/src/Solcore/Pipeline/SolcorePipeline.hs b/src/Solcore/Pipeline/SolcorePipeline.hs
index 933ed6451..e07175460 100644
--- a/src/Solcore/Pipeline/SolcorePipeline.hs
+++ b/src/Solcore/Pipeline/SolcorePipeline.hs
@@ -18,6 +18,7 @@ import Solcore.Backend.MastEval (defaultFuel, eliminateDeadCode, evalCompUnit)
 import Solcore.Backend.Specialise (specialiseCompUnit)
 import Solcore.Desugarer.ContractDispatch (contractDispatchTopDecls)
 import Solcore.Desugarer.DecisionTreeCompiler (matchCompiler, showWarning)
+import Solcore.Desugarer.DeriveGeneric (deriveGenericTopDecls)
 import Solcore.Desugarer.FieldAccess (fieldDesugarTopDecls)
 import Solcore.Desugarer.IfDesugarer (ifDesugarer)
 import Solcore.Desugarer.IndirectCall (indirectCallTopDecls)
@@ -301,12 +302,23 @@ prepareInferenceDeclsForTypeInference opts emitOutput imps inferenceDecls = do
     putStrLn "> Dispatch:"
     putStrLn $ prettyInferenceDecls dispatched
 
+  -- Generic instance derivation (only for locally-defined data types)
+  let localData = [dt | ModuleInferenceDecl ModuleLocalDecl (TDataDef dt) <- dispatched]
+  derived <-
+    ExceptT $
+      runExceptT $
+        traverseModuleInferenceTopDecls (ExceptT . pure . deriveGenericTopDecls localData) dispatched
+
+  liftIO $ when verbose $ do
+    putStrLn "> Generic instance derivation:"
+    putStrLn $ prettyInferenceDecls derived
+
   -- SCC analysis
   connected <-
     ExceptT $
       timeItNamed "SCC           " $
         runExceptT $
-          traverseModuleInferenceTopDecls (ExceptT . sccAnalysisTopDecls) dispatched
+          traverseModuleInferenceTopDecls (ExceptT . sccAnalysisTopDecls) derived
 
   liftIO $ when verbose $ do
     putStrLn "> SCC Analysis:"
diff --git a/std/ABIGeneric.solc b/std/ABIGeneric.solc
index 02b6c0ef0..ad87ac70f 100644
--- a/std/ABIGeneric.solc
+++ b/std/ABIGeneric.solc
@@ -10,19 +10,110 @@ export {
 import std.{*};
 import std.Generic.{*};
 
-// Top-level generic ABI encode.
+function maxWord(a : word, b : word) -> word {
+    match gtWord(a, b) {
+    | true  => return a;
+    | false => return b;
+    }
+}
+
+// ─── ABIAttribs for the primitive sum(f, g) type ─────────────────────────
+// headSize = 32 (tag word) + max(headSize(f), headSize(g))
+
+forall f g . f:ABIAttribs, g:ABIAttribs =>
+instance sum(f, g) : ABIAttribs {
+    function headSize(ty : Proxy(sum(f, g))) -> word {
+        let pf : Proxy(f);
+        let pg : Proxy(g);
+        return 32 + maxWord(ABIAttribs.headSize(pf), ABIAttribs.headSize(pg));
+    }
+    function isStatic(ty : Proxy(sum(f, g))) -> bool {
+        let pf : Proxy(f);
+        let pg : Proxy(g);
+        return and(ABIAttribs.isStatic(pf), ABIAttribs.isStatic(pg));
+    }
+}
+
+// ─── ABIEncode for sum(f, g) ─────────────────────────────────────────────
+// Wire layout (static sums only):
+//   [offset +  0 .. offset + 31] : tag word (0 = inl, 1 = inr)
+//   [offset + 32 ..             ] : encoded branch payload
+
+forall f g . f:ABIAttribs, f:ABIEncode, g:ABIAttribs, g:ABIEncode =>
+instance sum(f, g) : ABIEncode {
+    function encodeInto(x : sum(f, g), basePtr : word, offset : word, tail : word) -> word {
+        match x {
+        | inl(v) =>
+            mstore(basePtr + offset, 0);
+            return ABIEncode.encodeInto(v, basePtr, offset + 32, tail);
+        | inr(v) =>
+            mstore(basePtr + offset, 1);
+            return ABIEncode.encodeInto(v, basePtr, offset + 32, tail);
+        }
+    }
+}
+
+// ─── ABIDecode for sum(f, g) ─────────────────────────────────────────────
+// Reads the tag word at headOffset; dispatches to f or g decoder at headOffset + 32.
+
+forall f g reader .
+    reader : WordReader,
+    f : ABIAttribs,
+    ABIDecoder(f, reader) : ABIDecode(f),
+    ABIDecoder(g, reader) : ABIDecode(g) =>
+instance ABIDecoder(sum(f, g), reader) : ABIDecode(sum(f, g)) {
+    function decode(ptr : ABIDecoder(sum(f, g), reader), headOffset : word) -> sum(f, g) {
+        match ptr {
+        | ABIDecoder(rdr) =>
+            let tag = WordReader.read(WordReader.advance(rdr, headOffset));
+            match tag {
+            | 0 =>
+                let dec_f : ABIDecoder(f, reader) = ABIDecoder(rdr);
+                return inl(ABIDecode.decode(dec_f, headOffset + 32));
+            | _ =>
+                let dec_g : ABIDecoder(g, reader) = ABIDecoder(rdr);
+                return inr(ABIDecode.decode(dec_g, headOffset + 32));
+            }
+        }
+    }
+}
+
+// ─── Default bridges: ABIAttribs and ABIEncode via Generic ───────────────
+// Any type 'a' with Generic(rep) inherits its ABI layout from rep.
+
+forall a rep . a:Generic(rep), rep:ABIAttribs =>
+default instance a : ABIAttribs {
+    function headSize(ty : Proxy(a)) -> word {
+        let prx : Proxy(rep);
+        return ABIAttribs.headSize(prx);
+    }
+    function isStatic(ty : Proxy(a)) -> bool {
+        let prx : Proxy(rep);
+        return ABIAttribs.isStatic(prx);
+    }
+}
+
+forall a rep . a:Generic(rep), rep:ABIAttribs, rep:ABIEncode =>
+default instance a : ABIEncode {
+    function encodeInto(x : a, basePtr : word, offset : word, tail : word) -> word {
+        return ABIEncode.encodeInto(Generic.from(x), basePtr, offset, tail);
+    }
+}
+
+// ─── Top-level generic encode function ───────────────────────────────────
 // Serialises any 'a' that has a Generic(rep) instance.
-// ABIEncode for 'a' is resolved via the default instance bridge in std.Generic.
+// Only the Generic instance is required — ABIEncode is resolved via the bridge.
+
 forall a rep . a:Generic(rep), rep:ABIAttribs, rep:ABIEncode =>
 function encode(x : a, basePtr : word, offset : word, tail : word) -> word {
     let xrep : rep = Generic.from(x);
     return ABIEncode.encodeInto(xrep, basePtr, offset, tail);
 }
 
-// Top-level generic ABI decode.
-// Deserialises any 'a' whose representation type 'rep' is decodable.
-// The caller supplies ABIDecoder(a, reader); the function wraps it in
-// ABIDecoder(rep, reader), decodes the rep, then converts via Generic.to.
+// ─── Top-level generic decode function ───────────────────────────────────
+// Deserialises any 'a' that has a Generic(rep) instance.
+// Only the Generic instance is required — ABIDecode is resolved via the bridge.
+
 forall a rep reader .
     a : Generic(rep),
     reader : WordReader,
diff --git a/std/Generic.solc b/std/Generic.solc
index 18b180bc3..ba30049d1 100644
--- a/std/Generic.solc
+++ b/std/Generic.solc
@@ -1,120 +1,17 @@
-pragma no-patterson-condition ABIAttribs, ABIEncode;
-pragma no-bounded-variable-condition ABIAttribs, ABIEncode;
+pragma no-patterson-condition;
+pragma no-bounded-variable-condition;
 
-export {
-    Sum(*),
-    Generic
-};
+export { Generic };
 
 import std.{*};
 
-// Binary tagged union: the only new representation type.
-// Native () and (f, g) are reused as Unit and Prod respectively;
-// they already have full ABIAttribs / ABIEncode / ABIDecode support in std.solc.
-data Sum(f, g) = Inl(f) | Inr(g);
-
 // MPTC: isomorphism between a user type and its SOP representation.
-// Pattern mirrors Typedef(rep) in std.solc.
+// The representation 'rep' is built from primitive Solcore types:
+//   sum(f, g)  with constructors inl / inr
+//   (f, g)     pair (product)
+//   ()         unit
 forall a rep.
 class a : Generic(rep) {
     function from(x : a) -> rep;
     function to(x : rep) -> a;
 }
-
-// Maximum of two words, used for Sum headSize.
-function maxWord(a : word, b : word) -> word {
-    match gtWord(a, b) {
-    | true  => return a;
-    | false => return b;
-    }
-}
-
-// ABIAttribs for Sum:
-// headSize = 32 (tag word) + max(headSize(f), headSize(g))
-forall f g . f:ABIAttribs, g:ABIAttribs =>
-instance Sum(f, g) : ABIAttribs {
-    function headSize(ty : Proxy(Sum(f, g))) -> word {
-        let pf : Proxy(f);
-        let pg : Proxy(g);
-        return 32 + maxWord(ABIAttribs.headSize(pf), ABIAttribs.headSize(pg));
-    }
-    function isStatic(ty : Proxy(Sum(f, g))) -> bool {
-        let pf : Proxy(f);
-        let pg : Proxy(g);
-        return and(ABIAttribs.isStatic(pf), ABIAttribs.isStatic(pg));
-    }
-}
-
-// ABIEncode for Sum.
-// Wire layout (static sums only):
-//   [offset + 0  .. offset + 31] : tag word (0 = Inl, 1 = Inr)
-//   [offset + 32 ..             ] : encoded branch payload
-// For uniform sums (headSize(f) == headSize(g)) no bytes are left uninitialised.
-forall f g . f:ABIAttribs, f:ABIEncode, g:ABIAttribs, g:ABIEncode =>
-instance Sum(f, g) : ABIEncode {
-    function encodeInto(x : Sum(f, g), basePtr : word, offset : word, tail : word) -> word {
-        match x {
-        | Sum.Inl(v) =>
-            mstore(basePtr + offset, 0);
-            return ABIEncode.encodeInto(v, basePtr, offset + 32, tail);
-        | Sum.Inr(v) =>
-            mstore(basePtr + offset, 1);
-            return ABIEncode.encodeInto(v, basePtr, offset + 32, tail);
-        }
-    }
-}
-
-// ABIDecode for Sum.
-// Reads the tag word at headOffset; dispatches to the f or g decoder at headOffset + 32.
-forall f g reader .
-    reader:WordReader,
-    f:ABIAttribs,
-    ABIDecoder(f, reader) : ABIDecode(f),
-    ABIDecoder(g, reader) : ABIDecode(g) =>
-instance ABIDecoder(Sum(f, g), reader) : ABIDecode(Sum(f, g)) {
-    function decode(ptr : ABIDecoder(Sum(f, g), reader), headOffset : word) -> Sum(f, g) {
-        match ptr {
-        | ABIDecoder(rdr) =>
-            let tag = WordReader.read(WordReader.advance(rdr, headOffset));
-            match tag {
-            | 0 =>
-                let dec_f : ABIDecoder(f, reader) = ABIDecoder(rdr);
-                return Sum.Inl(ABIDecode.decode(dec_f, headOffset + 32));
-            | _ =>
-                let dec_g : ABIDecoder(g, reader) = ABIDecoder(rdr);
-                return Sum.Inr(ABIDecode.decode(dec_g, headOffset + 32));
-            }
-        }
-    }
-}
-
-// Bridge: any type with a Generic(rep) instance gains ABIAttribs automatically.
-forall a rep . a:Generic(rep), rep:ABIAttribs =>
-default instance a : ABIAttribs {
-    function headSize(ty : Proxy(a)) -> word {
-        let prx : Proxy(rep);
-        return ABIAttribs.headSize(prx);
-    }
-    function isStatic(ty : Proxy(a)) -> bool {
-        let prx : Proxy(rep);
-        return ABIAttribs.isStatic(prx);
-    }
-}
-
-// Bridge: any type with a Generic(rep) instance gains ABIEncode automatically.
-forall a rep . a:Generic(rep), rep:ABIAttribs, rep:ABIEncode =>
-default instance a : ABIEncode {
-    function encodeInto(x : a, basePtr : word, offset : word, tail : word) -> word {
-        let r : rep = Generic.from(x);
-        return ABIEncode.encodeInto(r, basePtr, offset, tail);
-    }
-}
-
-// Note: ABIDecode bridge omitted.  The class head ABIDecoder(a, reader) is a type
-// application, not a plain variable, so Solcore's "default instance" restriction
-// makes automatic derivation impossible.  To decode a Generic type, create an
-// ABIDecoder for the representation type and call Generic.to on the result:
-//
-//   let dec : ABIDecoder(Rep, MemoryWordReader) = ABIDecoder.ABIDecoder(reader);
-//   let rep : Rep = ABIDecode.decode(dec, offset);
-//   let val : MyType = Generic.to(rep);
diff --git a/test/Cases.hs b/test/Cases.hs
index cc7d6f787..0a394e60e 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -300,6 +300,11 @@ cases =
       runTestExpectingFailure "default-inst.solc" caseFolder,
       runTestExpectingFailure "default-instance-missing.solc" caseFolder,
       runTestExpectingFailure "default-instance-weak.solc" caseFolder,
+      runTestForFile "derive-generic-sum.solc" caseFolder,
+      runTestForFile "derive-generic-excluded.solc" caseFolder,
+      runTestExpectingFailure "generic-manual-no-pragma.solc" caseFolder,
+      runTestExpectingFailure "generic-sum-no-pragma.solc" caseFolder,
+      runTestExpectingFailure "generic-product-no-pragma.solc" caseFolder,
       runTestForFile "dot-expression-constructor.solc" caseFolder,
       runTestForFile "dot-expression-call-arg-context.solc" caseFolder,
       runTestForFile "dot-expression-match-return.solc" caseFolder,
diff --git a/test/examples/cases/derive-generic-excluded.solc b/test/examples/cases/derive-generic-excluded.solc
new file mode 100644
index 000000000..784f244ce
--- /dev/null
+++ b/test/examples/cases/derive-generic-excluded.solc
@@ -0,0 +1,39 @@
+// Test: pragma no-generic-instance-for suppresses auto-derivation for the
+// listed types.  Pair has its instance suppressed and provided manually;
+// Box gets its instance generated automatically.
+
+import std.{*};
+import std.Generic.{*};
+
+pragma no-patterson-condition;
+pragma no-bounded-variable-condition;
+pragma no-generic-instance-for Pair;
+
+data Pair(a, b) = MkPair(a, b);
+
+data Box(a) = MkBox(a);
+
+// Manual instance for Pair (suppressed from auto-derivation).
+forall a b.
+instance Pair(a, b) : Generic((a, b)) {
+    function from(p : Pair(a, b)) -> (a, b) {
+        match p {
+        | Pair.MkPair(x, y) => return (x, y);
+        }
+    }
+    function to(t : (a, b)) -> Pair(a, b) {
+        match t {
+        | (x, y) => return Pair.MkPair(x, y);
+        }
+    }
+}
+
+// Box gets its Generic instance auto-derived (not excluded).
+function boxRoundtrip(v : word) -> bool {
+    let b : Box(word) = Box.MkBox(v);
+    let r : word = Generic.from(b);
+    let b2 : Box(word) = Generic.to(r);
+    match b2 {
+    | Box.MkBox(v2) => return eqWord(v, v2);
+    }
+}
diff --git a/test/examples/cases/derive-generic-sum.solc b/test/examples/cases/derive-generic-sum.solc
new file mode 100644
index 000000000..aa93b5607
--- /dev/null
+++ b/test/examples/cases/derive-generic-sum.solc
@@ -0,0 +1,34 @@
+// Test: Generic instances are auto-derived for sum types.
+// Neither Option nor Tree has an explicit Generic instance; both should be
+// generated automatically by DeriveGeneric.
+
+import std.{*};
+import std.Generic.{*};
+
+pragma no-patterson-condition;
+pragma no-bounded-variable-condition;
+
+data Option(a) = None | Some(a);
+
+data Tree(a) = Leaf | Node(Tree(a), a, Tree(a));
+
+// Use the auto-derived instances to check that from/to round-trip.
+function roundtripNone() -> bool {
+    let x : Option(word) = Option.None;
+    let r : sum((), word) = Generic.from(x);
+    let x2 : Option(word) = Generic.to(r);
+    match x2 {
+    | Option.None    => return true;
+    | Option.Some(_) => return false;
+    }
+}
+
+function roundtripSome(v : word) -> bool {
+    let x : Option(word) = Option.Some(v);
+    let r : sum((), word) = Generic.from(x);
+    let x2 : Option(word) = Generic.to(r);
+    match x2 {
+    | Option.None     => return false;
+    | Option.Some(v2) => return eqWord(v, v2);
+    }
+}
diff --git a/test/examples/cases/generic-manual-no-pragma.solc b/test/examples/cases/generic-manual-no-pragma.solc
new file mode 100644
index 000000000..6551643c5
--- /dev/null
+++ b/test/examples/cases/generic-manual-no-pragma.solc
@@ -0,0 +1,18 @@
+// Error case: manual Generic instance without pragma no-generic-instance-for.
+// The compiler must reject this with a conflict error.
+
+import std.Generic.{*};
+
+pragma no-patterson-condition;
+pragma no-bounded-variable-condition;
+
+data Foo = MkFoo(word);
+
+instance Foo : Generic(word) {
+    function from(x : Foo) -> word {
+        match x { | Foo.MkFoo(v) => return v; }
+    }
+    function to(v : word) -> Foo {
+        return Foo.MkFoo(v);
+    }
+}
diff --git a/test/examples/cases/generic-product-no-pragma.solc b/test/examples/cases/generic-product-no-pragma.solc
new file mode 100644
index 000000000..bb2fb4db8
--- /dev/null
+++ b/test/examples/cases/generic-product-no-pragma.solc
@@ -0,0 +1,21 @@
+import std.{*};
+import std.dispatch.{*};
+import std.Generic.{*};
+import std.ABIGeneric.{*};
+
+pragma no-patterson-condition;
+pragma no-coverage-condition;
+pragma no-bounded-variable-condition;
+
+data Point = Point(uint256, uint256);
+
+// Manual Generic instance without pragma no-generic-instance-for Point.
+// The compiler must reject this with a conflict error.
+instance Point : Generic((uint256, uint256)) {
+    function from(p : Point) -> (uint256, uint256) {
+        match p { | Point(x, y) => return (x, y); }
+    }
+    function to(t : (uint256, uint256)) -> Point {
+        match t { | (x, y) => return Point(x, y); }
+    }
+}
diff --git a/test/examples/cases/generic-sum-no-pragma.solc b/test/examples/cases/generic-sum-no-pragma.solc
new file mode 100644
index 000000000..49923afb7
--- /dev/null
+++ b/test/examples/cases/generic-sum-no-pragma.solc
@@ -0,0 +1,27 @@
+import std.{*};
+import std.dispatch.{*};
+import std.Generic.{*};
+import std.ABIGeneric.{*};
+
+pragma no-patterson-condition;
+pragma no-coverage-condition;
+pragma no-bounded-variable-condition;
+
+data Option(a) = None | Some(a);
+
+// Manual Generic instance without pragma no-generic-instance-for Option.
+// The compiler must reject this with a conflict error.
+instance Option(uint256) : Generic(sum((), uint256)) {
+    function from(x : Option(uint256)) -> sum((), uint256) {
+        match x {
+        | Option.None    => return inl(());
+        | Option.Some(v) => return inr(v);
+        }
+    }
+    function to(r : sum((), uint256)) -> Option(uint256) {
+        match r {
+        | inl(_) => return Option.None;
+        | inr(v) => return Option.Some(v);
+        }
+    }
+}
diff --git a/test/examples/cases/user-op-lambda.solc b/test/examples/cases/user-op-lambda.solc
new file mode 100644
index 000000000..ec2d8cd53
--- /dev/null
+++ b/test/examples/cases/user-op-lambda.solc
@@ -0,0 +1,20 @@
+import std.{*};
+pragma no-patterson-condition ;
+pragma no-coverage-condition ;
+pragma no-bounded-variable-condition ;
+
+infixl 70 (^^) => pow;
+
+function pow(b : word, e : word) -> word {
+  let r : word;
+  assembly { r := exp(b, e) }
+  return r;
+}
+
+contract UserOpLambda {
+  function main() -> word {
+    // operator (^^) used inside a lambda body
+    let f = lam(x : word) -> word { return x ^^ 3; };
+    return f(2);
+  }
+}
diff --git a/test/examples/dispatch/generic_product.solc b/test/examples/dispatch/generic_product.solc
index bae06dc26..162f9a054 100644
--- a/test/examples/dispatch/generic_product.solc
+++ b/test/examples/dispatch/generic_product.solc
@@ -6,6 +6,7 @@ import std.ABIGeneric.{*};
 pragma no-patterson-condition;
 pragma no-coverage-condition;
 pragma no-bounded-variable-condition;
+pragma no-generic-instance-for Point;
 
 data Point = Point(uint256, uint256);
 
diff --git a/test/examples/dispatch/generic_sum.solc b/test/examples/dispatch/generic_sum.solc
index abbf11ce0..5a2630225 100644
--- a/test/examples/dispatch/generic_sum.solc
+++ b/test/examples/dispatch/generic_sum.solc
@@ -6,22 +6,23 @@ import std.ABIGeneric.{*};
 pragma no-patterson-condition;
 pragma no-coverage-condition;
 pragma no-bounded-variable-condition;
+pragma no-generic-instance-for Option;
 
 data Option(a) = None | Some(a);
 
-// Generic instance using the Sum ADT from std.Generic as the representation.
-// Sum((), uint256): Sum.Inl(()) = None, Sum.Inr(v) = Some(v)
-instance Option(uint256) : Generic(Sum((), uint256)) {
-    function from(x : Option(uint256)) -> Sum((), uint256) {
+// Only requirement: Generic instance using the primitive sum type.
+// rep = sum((), uint256): inl(()) = None, inr(v) = Some(v)
+instance Option(uint256) : Generic(sum((), uint256)) {
+    function from(x : Option(uint256)) -> sum((), uint256) {
         match x {
-        | Option.None    => return Sum.Inl(());
-        | Option.Some(v) => return Sum.Inr(v);
+        | Option.None    => return inl(());
+        | Option.Some(v) => return inr(v);
         }
     }
-    function to(r : Sum((), uint256)) -> Option(uint256) {
+    function to(r : sum((), uint256)) -> Option(uint256) {
         match r {
-        | Sum.Inl(_) => return Option.None;
-        | Sum.Inr(v) => return Option.Some(v);
+        | inl(_) => return Option.None;
+        | inr(v) => return Option.Some(v);
         }
     }
 }
@@ -29,8 +30,8 @@ instance Option(uint256) : Generic(Sum((), uint256)) {
 contract GenericSum {
     constructor() {}
 
-    // Calls encode; returns the tag word at offset 0.
-    // None -> 0 (Sum.Inl)
+    // Calls encode; returns the tag word (first 32 bytes).
+    // None → 0
     public function encodeNone() -> uint256 {
         let x : Option(uint256) = Option.None;
         let buf = allocate_zeroed_memory(64);
@@ -38,8 +39,8 @@ contract GenericSum {
         return Typedef.abs(mload(buf));
     }
 
-    // Calls encode; returns the tag word at offset 0.
-    // Some(n) -> 1 (Sum.Inr)
+    // Calls encode; returns the tag word (first 32 bytes).
+    // Some(n) → 1
     public function encodeSomeTag(n : uint256) -> uint256 {
         let x : Option(uint256) = Option.Some(n);
         let buf = allocate_zeroed_memory(64);
@@ -47,7 +48,7 @@ contract GenericSum {
         return Typedef.abs(mload(buf));
     }
 
-    // Calls encode; returns the payload word at offset 32.
+    // Calls encode; returns the payload word (bytes 32-63).
     public function encodePayload(n : uint256) -> uint256 {
         let x : Option(uint256) = Option.Some(n);
         let buf = allocate_zeroed_memory(64);