diff --git a/src/Solcore/Backend/Specialise.hs b/src/Solcore/Backend/Specialise.hs
index d7e5a69ed..e3e08f5fa 100644
--- a/src/Solcore/Backend/Specialise.hs
+++ b/src/Solcore/Backend/Specialise.hs
@@ -355,8 +355,6 @@ specCall i args ty = do
   let name = idName i'
   let argTypes = map typeOfTcExp args
   argTypes' <- atCurrentSubst argTypes
-  let typedArgs = zip args argTypes'
-  args' <- forM typedArgs (uncurry specExp)
   let funType = foldr (:->) ty' argTypes'
   debug ["> specCall: ", show name, " : ", pretty funType]
   mres <- lookupResolution name funType
@@ -376,6 +374,9 @@ specCall i args ty = do
             "\n  This often occurs when a polymorphic-return function (e.g. `require`)",
             "\n  is passed directly to a polymorphic-argument function (e.g. `void`)."
           ]
+      let argTypesForArgs = map (applytv phi) argTypes'
+      let typedArgs = zip args argTypesForArgs
+      args' <- forM typedArgs (uncurry specExp)
       extSpSubst phi
       subst <- getSpSubst
       let ty'' = applytv subst fty
@@ -385,6 +386,8 @@ specCall i args ty = do
       args'' <- atCurrentSubst args'
       return (Id name' ty'', args'')
     Nothing -> do
+      let typedArgs = zip args argTypes'
+      args' <- forM typedArgs (uncurry specExp)
       void $ panics ["! specCall: no resolution found for ", show name, " : ", pretty funType]
       return (i, args')
 
@@ -498,11 +501,19 @@ specStmt stmt@(Let i mty mexp) = do
   debug ["> specStmt (Let): ", pretty i, " : ", pretty (idType i), " @ ", pretty subst]
   i' <- atCurrentSubst i
   let ty' = idType i'
-  ensureClosed ty' stmt subst
   mty' <- atCurrentSubst mty
   case mexp of
-    Nothing -> return $ Let i' mty' Nothing
-    Just e -> Let i' mty' . Just <$> specExp e ty'
+    Nothing -> do
+      ensureClosed ty' stmt subst
+      return $ Let i' mty' Nothing
+    Just e -> do
+      e' <- specExp e ty'
+      i'' <- atCurrentSubst i'
+      let ty'' = idType i''
+      subst' <- getSpSubst
+      ensureClosed ty'' stmt subst'
+      mty'' <- atCurrentSubst mty'
+      return $ Let i'' mty'' (Just e')
 specStmt (Block body) =
   Block <$> specBody body
 specStmt (StmtExp e) = do
diff --git a/src/Solcore/Frontend/Module/Loader.hs b/src/Solcore/Frontend/Module/Loader.hs
index 78706f6c3..4dd19ba23 100644
--- a/src/Solcore/Frontend/Module/Loader.hs
+++ b/src/Solcore/Frontend/Module/Loader.hs
@@ -1592,8 +1592,10 @@ toValidationImportStub (TFunDef (FunDef sig _)) =
   Just (TFunDef (stubFunction (sigName sig)))
 toValidationImportStub (TSym (TySym n _ _)) =
   Just (TSym (stubType n))
-toValidationImportStub d@(TClassDef _) =
-  Just d
+toValidationImportStub (TClassDef (Class bvs _ n pvs mv sigs)) =
+  Just (TClassDef (Class bvs [] n pvs mv (map stripSigContext sigs)))
+  where
+    stripSigContext (Signature vs _ sn ps ret) = Signature vs [] sn ps ret
 toValidationImportStub (TContr (Contract n _ _)) =
   Just (TContr (Contract n [] []))
 toValidationImportStub (TDataDef (DataTy n _ cs)) =
diff --git a/src/Solcore/Frontend/TypeInference/TcEnv.hs b/src/Solcore/Frontend/TypeInference/TcEnv.hs
index 95e8bfcb8..7ad96858b 100644
--- a/src/Solcore/Frontend/TypeInference/TcEnv.hs
+++ b/src/Solcore/Frontend/TypeInference/TcEnv.hs
@@ -163,6 +163,8 @@ primCtx =
       primUnit,
       primTrue,
       primFalse,
+      primInl,
+      primInr,
       primInvoke
     ]
 
diff --git a/src/Solcore/Frontend/TypeInference/TcSimplify.hs b/src/Solcore/Frontend/TypeInference/TcSimplify.hs
index 768f78faa..7ce3d63d6 100644
--- a/src/Solcore/Frontend/TypeInference/TcSimplify.hs
+++ b/src/Solcore/Frontend/TypeInference/TcSimplify.hs
@@ -193,10 +193,11 @@ toHnf depth p@(InCls c _ _)
               Nothing -> do
                 info [">>>> No default instance found for:", pretty p]
                 pure [p]
-              Just (_, s) -> do
+              Just (ps', s) -> do
                 info [">>>> Default instance for:", pretty p, " found! (Solved), \n>>> Subst: ", pretty s]
                 _ <- extSubst s
-                pure []
+                ps0 <- withCurrentSubst ps'
+                toHnfs (depth - 1) ps0
   | depth <= 0 = notEnoughFuel [p]
   | otherwise =
       do
@@ -207,16 +208,15 @@ toHnf depth p@(InCls c _ _)
             insts' <- mapM fromANF insts
             info [">>> No matching instance for:", pretty p, " trying a default instance.Defined instances:\n", unlines (map pretty insts')]
             denv <- getDefaultInstEnv
-            -- does c have a default instance?
             case proveDefaulting denv insts p of
               Nothing -> do
                 info [">>>> No default instance found for:", pretty p]
                 pure [p]
-              Just (_, s) -> do
+              Just (ps', s) -> do
                 info [">>>> Default instance for:", pretty p, " found! (Solved), \n>>> Subst: ", pretty s]
-                -- default instances should not have any additional contraints.
                 _ <- extSubst s
-                pure []
+                ps0 <- withCurrentSubst ps'
+                toHnfs (depth - 1) ps0
           Just (ps', s, i) -> do
             info [">>> Found instance for:", pretty p, "\n>>> Instance:", pretty i, "\n>>> Subst:", pretty s]
             _ <- extSubst s
diff --git a/std/Bits.solc b/std/Bits.solc
new file mode 100644
index 000000000..8594b1334
--- /dev/null
+++ b/std/Bits.solc
@@ -0,0 +1,65 @@
+export { * };
+
+// Bitwise word operations using EVM assembly.
+
+function band(a : word, b : word) -> word {
+    let res : word;
+    assembly { res := and(a, b) }
+    return res;
+}
+
+function bor(a : word, b : word) -> word {
+    let res : word;
+    assembly { res := or(a, b) }
+    return res;
+}
+
+function bxor(a : word, b : word) -> word {
+    let res : word;
+    assembly { res := xor(a, b) }
+    return res;
+}
+
+function bnot(a : word) -> word {
+    let res : word;
+    assembly { res := not(a) }
+    return res;
+}
+
+// shl(n, x): shift x left by n bits
+function shl_(n : word, x : word) -> word {
+    let res : word;
+    assembly { res := shl(n, x) }
+    return res;
+}
+
+// shr(n, x): logical shift x right by n bits
+function shr_(n : word, x : word) -> word {
+    let res : word;
+    assembly { res := shr(n, x) }
+    return res;
+}
+
+// mask(n): n-bit mask in the least significant positions (bits 0..n-1 set to 1)
+function mask(n : word) -> word {
+    let res : word;
+    assembly { res := sub(shl(n, 1), 1) }
+    return res;
+}
+
+// maxWord(a, b): returns the larger of the two words
+function maxWord(a : word, b : word) -> word {
+    let cond : word;
+    assembly { cond := gt(a, b) }
+    match cond {
+    | 0 => return b;
+    | _ => return a;
+    }
+}
+
+// addWord(a, b): wrapping 256-bit addition
+function addWord(a : word, b : word) -> word {
+    let res : word;
+    assembly { res := add(a, b) }
+    return res;
+}
diff --git a/std/Generic.solc b/std/Generic.solc
new file mode 100644
index 000000000..adc6779fe
--- /dev/null
+++ b/std/Generic.solc
@@ -0,0 +1,15 @@
+export { * };
+
+// Generic isomorphism class (sum-of-products representation).
+//
+// `a : Generic(rep)` witnesses that type `a` is isomorphic to `rep`,
+// where `rep` is a nested combination of `pair`, `sum`, `()`, `bool`,
+// and `word` — the sum-of-products normal form.
+//
+// Users write exactly one instance per data type; all generic operations
+// (Packable, Storable, ...) follow automatically via the bridge instances.
+
+forall a rep. class a : Generic(rep) {
+    function from(x : a) -> rep;
+    function to(x : rep) -> a;
+}
diff --git a/std/Packable.solc b/std/Packable.solc
new file mode 100644
index 000000000..9dc1d224c
--- /dev/null
+++ b/std/Packable.solc
@@ -0,0 +1,113 @@
+import Bits.{*};
+import Generic.{Generic};
+
+export { * };
+
+// Packable: types that fit in a 256-bit word with a dense bit layout.
+//
+// Invariant: pack(x) uses only the least significant bitWidth(x) bits.
+// bitWidth takes a value so the bridge instance can call Generic.from(x)
+// to resolve the rep type variable before any let-binding needs it.
+
+forall a. class a : Packable {
+    function bitWidth(x : a) -> word;
+    function pack(x : a) -> word;
+    function unpack(w : word) -> a;
+}
+
+instance () : Packable {
+    function bitWidth(x : ()) -> word { return 0; }
+    function pack(x : ()) -> word { return 0; }
+    function unpack(w : word) -> () { return (); }
+}
+
+instance bool : Packable {
+    function bitWidth(x : bool) -> word { return 1; }
+    function pack(x : bool) -> word {
+        match x {
+        | true  => return 1;
+        | false => return 0;
+        }
+    }
+    function unpack(w : word) -> bool {
+        match band(w, 1) {
+        | 0 => return false;
+        | _ => return true;
+        }
+    }
+}
+
+instance word : Packable {
+    function bitWidth(x : word) -> word { return 256; }
+    function pack(x : word) -> word { return x; }
+    function unpack(w : word) -> word { return w; }
+}
+
+// pair: low field a packed in bits 0..bitWidth(a)-1,
+//       high field b packed in bits bitWidth(a)..bitWidth(a)+bitWidth(b)-1
+forall a b. a : Packable, b : Packable =>
+instance pair(a, b) : Packable {
+    function bitWidth(x : pair(a, b)) -> word {
+        match x {
+        | (l, r) => return addWord(Packable.bitWidth(l), Packable.bitWidth(r));
+        }
+    }
+    function pack(x : pair(a, b)) -> word {
+        match x {
+        | (l, r) =>
+            let bw : word = Packable.bitWidth(l);
+            return bor(Packable.pack(l), shl_(bw, Packable.pack(r)));
+        }
+    }
+    function unpack(w : word) -> pair(a, b) {
+        let lo_dummy : a = Packable.unpack(0);
+        let bw : word = Packable.bitWidth(lo_dummy);
+        let lo : a = Packable.unpack(band(w, mask(bw)));
+        let hi : b = Packable.unpack(shr_(bw, w));
+        return (lo, hi);
+    }
+}
+
+// sum: bit 0 is the tag (0 = inl, 1 = inr); payload in the upper bits
+forall a b. a : Packable, b : Packable =>
+instance sum(a, b) : Packable {
+    function bitWidth(x : sum(a, b)) -> word {
+        let la : a = Packable.unpack(0);
+        let lb : b = Packable.unpack(0);
+        return addWord(1, maxWord(Packable.bitWidth(la), Packable.bitWidth(lb)));
+    }
+    function pack(x : sum(a, b)) -> word {
+        match x {
+        | inl(l) => return shl_(1, Packable.pack(l));
+        | inr(r) => return bor(shl_(1, Packable.pack(r)), 1);
+        }
+    }
+    function unpack(w : word) -> sum(a, b) {
+        match band(w, 1) {
+        | 0 => return inl(Packable.unpack(shr_(1, w)):a);
+        | _ => return inr(Packable.unpack(shr_(1, w)):b);
+        }
+    }
+}
+
+// --- Bridge instance ---
+// Any type with a Generic instance is automatically Packable.
+// bitWidth calls Generic.from(x) first so that the rep type variable
+// is resolved into the specialiser substitution before it is needed.
+
+pragma no-patterson-condition Packable;
+pragma no-bounded-variable-condition Packable;
+forall a rep. a : Generic(rep), rep : Packable =>
+default instance a : Packable {
+    function bitWidth(x : a) -> word {
+        let r : rep = Generic.from(x);
+        return Packable.bitWidth(r);
+    }
+    function pack(x : a) -> word {
+        let r : rep = Generic.from(x);
+        return Packable.pack(r);
+    }
+    function unpack(w : word) -> a {
+        return Generic.to(Packable.unpack(w):rep);
+    }
+}
diff --git a/std/Storage.solc b/std/Storage.solc
new file mode 100644
index 000000000..7d662cb08
--- /dev/null
+++ b/std/Storage.solc
@@ -0,0 +1,30 @@
+import Packable.{Packable};
+
+export { * };
+
+// Storable: EVM storage read/write derived from Packable.
+//
+// The default instance reads/writes the packed word representation.
+// For types with bitWidth > 256 the user must provide a specialised instance
+// that distributes the value across multiple storage slots.
+
+forall a. a : Packable =>
+class a : Storable {
+    function sload(slot : word) -> a;
+    function sstore(slot : word, v : a) -> ();
+}
+
+pragma no-patterson-condition Storable;
+pragma no-bounded-variable-condition Storable;
+forall a. a : Packable =>
+default instance a : Storable {
+    function sload(slot : word) -> a {
+        let raw : word;
+        assembly { raw := sload(slot) }
+        return Packable.unpack(raw);
+    }
+    function sstore(slot : word, v : a) -> () {
+        let w : word = Packable.pack(v);
+        assembly { sstore(slot, w) }
+    }
+}
diff --git a/std/Uint.solc b/std/Uint.solc
new file mode 100644
index 000000000..4adbc1324
--- /dev/null
+++ b/std/Uint.solc
@@ -0,0 +1,77 @@
+import Packable.{Packable};
+import Bits.{band, mask};
+
+export {
+    Uint8(*), Uint16(*), Uint32(*), Uint64(*), Uint128(*), Address(*)
+};
+
+// Fixed-width unsigned integer newtypes with Packable instances.
+// Each wraps a word and masks off the relevant bits.
+
+data Uint8 = MkUint8(word);
+data Uint16 = MkUint16(word);
+data Uint32 = MkUint32(word);
+data Uint64 = MkUint64(word);
+data Uint128 = MkUint128(word);
+data Address = MkAddress(word);
+
+instance Uint8 : Packable {
+    function bitWidth(x : Uint8) -> word { return 8; }
+    function pack(x : Uint8) -> word {
+        match x { | Uint8.MkUint8(w) => return band(w, mask(8)); }
+    }
+    function unpack(w : word) -> Uint8 {
+        return Uint8.MkUint8(band(w, mask(8)));
+    }
+}
+
+instance Uint16 : Packable {
+    function bitWidth(x : Uint16) -> word { return 16; }
+    function pack(x : Uint16) -> word {
+        match x { | Uint16.MkUint16(w) => return band(w, mask(16)); }
+    }
+    function unpack(w : word) -> Uint16 {
+        return Uint16.MkUint16(band(w, mask(16)));
+    }
+}
+
+instance Uint32 : Packable {
+    function bitWidth(x : Uint32) -> word { return 32; }
+    function pack(x : Uint32) -> word {
+        match x { | Uint32.MkUint32(w) => return band(w, mask(32)); }
+    }
+    function unpack(w : word) -> Uint32 {
+        return Uint32.MkUint32(band(w, mask(32)));
+    }
+}
+
+instance Uint64 : Packable {
+    function bitWidth(x : Uint64) -> word { return 64; }
+    function pack(x : Uint64) -> word {
+        match x { | Uint64.MkUint64(w) => return band(w, mask(64)); }
+    }
+    function unpack(w : word) -> Uint64 {
+        return Uint64.MkUint64(band(w, mask(64)));
+    }
+}
+
+instance Uint128 : Packable {
+    function bitWidth(x : Uint128) -> word { return 128; }
+    function pack(x : Uint128) -> word {
+        match x { | Uint128.MkUint128(w) => return band(w, mask(128)); }
+    }
+    function unpack(w : word) -> Uint128 {
+        return Uint128.MkUint128(band(w, mask(128)));
+    }
+}
+
+// Address: 160 bits (Ethereum address)
+instance Address : Packable {
+    function bitWidth(x : Address) -> word { return 160; }
+    function pack(x : Address) -> word {
+        match x { | Address.MkAddress(w) => return band(w, mask(160)); }
+    }
+    function unpack(w : word) -> Address {
+        return Address.MkAddress(band(w, mask(160)));
+    }
+}
diff --git a/std/std.solc b/std/std.solc
index b97115e88..108a573ef 100644
--- a/std/std.solc
+++ b/std/std.solc
@@ -493,6 +493,7 @@ function hash2(x: word, y: word) -> word {
   return result;
 }
 
+
 // --- Value Types ---
 
 forall t. t:Typedef(word) =>
diff --git a/test/Cases.hs b/test/Cases.hs
index f2b847556..54965baec 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -317,6 +317,8 @@ cases =
       runTestForFile "option2.solc" caseFolder,
       runTestExpectingFailure "overlapping-heads.solc" caseFolder,
       runTestForFile "Pair.solc" caseFolder,
+      runTestForFile "packed-token.solc" caseFolder,
+      runTestForFile "packed-direction.solc" caseFolder,
       runTestExpectingFailure "PairMatch1.solc" caseFolder,
       runTestExpectingFailure "PairMatch2.solc" caseFolder,
       -- failing due to missing assign constraint
diff --git a/test/examples/cases/packed-direction.solc b/test/examples/cases/packed-direction.solc
new file mode 100644
index 000000000..78e7f35cb
--- /dev/null
+++ b/test/examples/cases/packed-direction.solc
@@ -0,0 +1,52 @@
+import std.Generic.{*};
+import std.Storage.{*};
+
+// Direction = North | South | East | West
+// Rep: sum((), sum((), sum((), ())))
+// bitWidth = 1 + max(0, 1 + max(0, 1 + max(0, 0)))
+//          = 1 + max(0, 1 + max(0, 1))
+//          = 1 + max(0, 1 + 1)
+//          = 1 + 2 = 3 bits
+
+data Direction = North | South | East | West;
+
+instance Direction : Generic(sum((), sum((), sum((), ())))) {
+    function from(x : Direction) -> sum((), sum((), sum((), ()))) {
+        match x {
+        | Direction.North => return inl(());
+        | Direction.South => return inr(inl(()));
+        | Direction.East  => return inr(inr(inl(())));
+        | Direction.West  => return inr(inr(inr(())));
+        }
+    }
+    function to(x : sum((), sum((), sum((), ())))) -> Direction {
+        match x {
+        | inl(_)            => return Direction.North;
+        | inr(inl(_))       => return Direction.South;
+        | inr(inr(inl(_)))  => return Direction.East;
+        | inr(inr(inr(_)))  => return Direction.West;
+        }
+    }
+}
+
+contract PackedDirection {
+    // Store West (tag=inr(inr(inr(())))) in slot 0, then load and return its pack value.
+    // pack(West) = pack(inr(inr(inr(())))) = bor(shl(1, pack(inr(inr(())))), 1)
+    //   inner pack(inr(inr(()))) = bor(shl(1, pack(inr(()))), 1)
+    //     innermost pack(inr(())) = bor(shl(1, pack(())), 1) = bor(0, 1) = 1
+    //   = bor(shl(1, 1), 1) = bor(2, 1) = 3
+    // = bor(shl(1, 3), 1) = bor(6, 1) = 7
+    // So main() should return 7.
+    function main() -> word {
+        let slot : word = 0;
+        let d : Direction = Direction.West;
+        Storable.sstore(slot, d);
+        let d2 : Direction = Storable.sload(slot);
+        match d2 {
+        | Direction.North => return 0;
+        | Direction.South => return 1;
+        | Direction.East  => return 2;
+        | Direction.West  => return 3;
+        }
+    }
+}
diff --git a/test/examples/cases/packed-token.solc b/test/examples/cases/packed-token.solc
new file mode 100644
index 000000000..2317aae4e
--- /dev/null
+++ b/test/examples/cases/packed-token.solc
@@ -0,0 +1,35 @@
+import std.Generic.{*};
+import std.Uint.{*};
+import std.Storage.{*};
+
+// Token = (owner: Address, amount: Uint32, locked: bool)
+// bitWidth = 160 + 32 + 1 = 193 bits, fits in one EVM slot.
+
+data Token = MkToken(Address, Uint32, bool);
+
+instance Token : Generic(pair(Address, pair(Uint32, bool))) {
+    function from(x : Token) -> pair(Address, pair(Uint32, bool)) {
+        match x {
+        | Token.MkToken(a, b, c) => return (a, (b, c));
+        }
+    }
+    function to(x : pair(Address, pair(Uint32, bool))) -> Token {
+        match x {
+        | (a, (b, c)) => return Token.MkToken(a, b, c);
+        }
+    }
+}
+
+contract PackedToken {
+    function main() -> word {
+        let slot : word = 0;
+        let owner : Address = Address.MkAddress(0xdeadbeef);
+        let amount : Uint32 = Uint32.MkUint32(42);
+        let t : Token = Token.MkToken(owner, amount, false);
+        Storable.sstore(slot, t);
+        let t2 : Token = Storable.sload(slot);
+        match t2 {
+        | Token.MkToken(_, Uint32.MkUint32(v), _) => return v;
+        }
+    }
+}