diff --git a/src/comp/CtxRed.hs b/src/comp/CtxRed.hs
index 13b0ea91e..5b35fd549 100644
--- a/src/comp/CtxRed.hs
+++ b/src/comp/CtxRed.hs
@@ -385,12 +385,16 @@ ctxRedCQType' isInstHead cqt = do
     -- (and do it here, after "convCQType", so that "expTFun" sees
     -- the qualified types)
     (qs, t) <- if isInstHead
-               then do -- XXX disable expanding of type synonyms until
-                       -- XXX failures with TLM instances are resolved
-                       -- XXX (vqs_extra, t1) <- expTFun t0 (expandSyn t0)
-                       (vqs_extra, t1) <- expTFun t0
+               then do (vqs_extra, t1) <- expTFun (expandSyn t0)
                        let qs_extra = map toPredWithPositions vqs_extra
-                       return (qs0 ++ qs_extra, t1)
+                       -- Use the expanded type t1 only if expTFun actually
+                       -- found something to expand (i.e. generated predicates).
+                       -- Otherwise keep the original t0.
+                       -- XXX we should probably be unconditionally expanding synonymns
+                       -- here and in tiField1, but there is existing code that relies on
+                       -- the current behavior, so changing this requires more thought.
+                       let t' = if null vqs_extra then t0 else t1
+                       return (qs0 ++ qs_extra, t')
                else return (qs0, t0)
 
     -- construct the predicates and try to reduce them
diff --git a/src/comp/MakeSymTab.hs b/src/comp/MakeSymTab.hs
index 4739d27be..7e047560c 100644
--- a/src/comp/MakeSymTab.hs
+++ b/src/comp/MakeSymTab.hs
@@ -464,10 +464,39 @@ checkNoTypeFunInHead errh r mi clsId args =
             | otherwise = []
         findTypeFun (TAp f a) = findTypeFun f ++ findTypeFun a
         findTypeFun _ = []
+        -- A type function can also be hidden behind a type synonym.
+        -- Expand each saturated synonym application and reject any type
+        -- function application in it that mentions a type variable (or
+        -- is not fully applied): such an application can neither be
+        -- reduced away nor used for instance matching.  Ground
+        -- applications are left alone; context reduction expands and
+        -- reduces them to a concrete type (Bug 1729, GitHub issue #311;
+        -- see ExpSizeOf_InstancesBaseSyn in the testsuite).  The error
+        -- is reported at the position of the synonym use.
+        synArity i | Just (TypeInfo { ti_sort = TItype n _ }) <- findType r i = Just n
+                   | otherwise = Nothing
+        findSynTypeFun t =
+            case splitTAp t of
+              (TCon (TyCon i _ _), as)
+                | Just n <- synArity i, toInteger (length as) >= n ->
+                    [ (getPosition i, tf)
+                    | tf <- varTypeFuns (expandSyn (updTypes r t)) ]
+              (_, as) -> concatMap findSynTypeFun as
+        varTypeFuns t =
+            case splitTAp t of
+              (TCon (TyCon i _ (TIatf { atf_param_idxs = pIdxs })), as)
+                | length as /= length pIdxs || not (null (tv as)) ->
+                    i : concatMap varTypeFuns as
+              (_, as) -> concatMap varTypeFuns as
         -- Only check non-determined positions
         nonDetArgs = [ arg | (idx, arg) <- zip [0..] args
                      , not (S.member idx determinedIdxs) ]
-        found = concatMap findTypeFun nonDetArgs
+        -- Report both the directly-written type functions and the ones
+        -- hidden behind synonyms, deduplicated (a directly-written type
+        -- function inside a synonym's argument can also appear in the
+        -- synonym's expansion).
+        checkArg a = nub (findTypeFun a ++ findSynTypeFun a)
+        found = concatMap checkArg nonDetArgs
     in if null found then ()
        else bsErrorUnsafe errh
                 [ (pos, EATFInInstanceHead (pfpString tfId))
diff --git a/src/comp/TCheck.hs b/src/comp/TCheck.hs
index e6d0cd09c..68e284a18 100644
--- a/src/comp/TCheck.hs
+++ b/src/comp/TCheck.hs
@@ -2394,7 +2394,14 @@ tiExpl''' as0 i sc alts me (oqt@(oqs :=> ot), vts) = do
 
     -- type functions like SizeOf could have crept into the predicates
     -- via unification, so we expand them out so that they can be satisfied
-    ps <- concatMapM (expTConPred . expandSynVPred) ps0
+    ps1 <- concatMapM (expTConPred . expandSynVPred) ps0
+
+    -- Expand type synonyms and type functions in the declared type to generate
+    -- implicit class predicates (e.g. SizeOf a generates Bits a n).
+    s_ot <- getSubst
+    let ot_expanded = expandSyn (apSub s_ot ot)
+    (ot_ps, _) <- expTFun ot_expanded
+    let ps = ps1 ++ ot_ps
 
     satTraceM ("tiExpl " ++ ppReadable i ++ " ps: " ++ ppReadable ps)
 
diff --git a/src/comp/Unify.hs b/src/comp/Unify.hs
index a121c88ac..0f71b8df7 100644
--- a/src/comp/Unify.hs
+++ b/src/comp/Unify.hs
@@ -1,8 +1,10 @@
 {-# LANGUAGE PatternGuards #-}
 module Unify(Unify(..), matchList) where
+import Data.Maybe(fromMaybe, isJust)
 import Type
 import Subst
 import CType
+import Pred(expandSyn)
 import ErrorUtil(internalError)
 import Util(fastNub)
 
@@ -24,8 +26,16 @@ class Unify t where
 instance Unify Type where
     -- an unreducable ATF application: identical types unify cleanly (reflexivity);
     -- different types generate a deferred equality constraint.
+    -- A type synonym is expanded when (and only when) that exposes an ATF
+    -- application, so that a synonym-hidden ATF unifies exactly like the
+    -- direct ATF application, instead of a variable being structurally
+    -- bound to the unexpanded synonym (which pins a fundep-determined
+    -- variable and makes derived-instance schemes spuriously mismatch).
     mgu bound_tyvars t1 t2
-        | isATFAp t1 || isATFAp t2 = atfUnify bound_tyvars t1 t2
+        | isJust m1 || isJust m2 =
+            atfUnify bound_tyvars (fromMaybe t1 m1) (fromMaybe t2 m2)
+      where m1 = asATFAp t1
+            m2 = asATFAp t2
     mgu bound_tyvars t1 t2
         | kind t1 == KNum =
       case kind t2 of
@@ -42,6 +52,27 @@ instance Unify Type where
     mgu bound_tyvars (TCon tc1) (TCon tc2) | tc1==tc2 = Just (nullSubst, [])
     mgu bound_tyvars _ _ = Nothing
 
+-- Return the type as a fully applied type-function (ATF) application,
+-- if it is one -- either directly, or behind a saturated type synonym.
+-- Synonyms are not expanded unconditionally, for three reasons:
+--  * unification is a hot path and expandSyn is a deep expansion, so
+--    only synonym-headed types should pay for it;
+--  * expandSyn fails on unsaturated synonym applications, so saturation
+--    must be checked first; and
+--  * a synonym whose expansion is not an ATF application must keep the
+--    existing structural unification of the unexpanded synonym, which
+--    existing code relies on (e.g. synonyms that drop some of their
+--    parameters; see GitHub issue #311).
+asATFAp :: Type -> Maybe Type
+asATFAp t
+    | isATFAp t = Just t
+    | isSynAp t, not (isUnSatSyn t), isATFAp t' = Just t'
+    | otherwise = Nothing
+  where t' = expandSyn t
+        isSynAp tt = case fst (splitTAp tt) of
+                       TCon (TyCon _ _ (TItype _ _)) -> True
+                       _ -> False
+
 atfUnify :: [TyVar] -> Type -> Type -> Maybe (Subst, [(Type, Type)])
 atfUnify bound_tyvars t1 t2
     | t1 == t2 = Just (nullSubst, [])
diff --git a/testsuite/bsc.typechecker/primtcons/CExtendATF.bsv b/testsuite/bsc.typechecker/primtcons/CExtendATF.bsv
new file mode 100644
index 000000000..e1c8fa619
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/CExtendATF.bsv
@@ -0,0 +1,64 @@
+// A variant of CExtendSynonym that puts a type function (here a user-defined
+// ATF, 'IdW') into the id-type synonyms, so that expanding the synonyms in the
+// instance head *does* reveal a type function.  That forces the conditional
+// synonym expansion in 'CtxRed.ctxRedCQType'' to fire (unlike CExtendSynonym,
+// where the plain synonyms are left unexpanded), which re-introduces the
+// dangling 'addr_size' parameter and makes typecheck fail with T0035.
+//
+// This is the case that is *still broken* -- see the XXX in ctxRedCQType' and
+// GitHub Issue #311 (and bsc-contrib PR 46, which worked around the analogous
+// AMBA_TLM failure by adding explicit method types).  CExtendATFExplicit.bsv
+// shows that adding explicit types makes it compile, which suggests the
+// problem is one of inference ordering rather than anything fundamental.
+// The same failure occurs with the builtin type function SizeOf in place of
+// the ATF 'IdW'.
+
+function Bit#(m) zExtend(Bit#(n) value)
+   provisos(Add#(n,m,k));
+   Bit#(k) out = zeroExtend(value);
+   if (valueOf(m) == 0)
+      return ?;
+   else
+      return out[valueOf(m) - 1:0];
+endfunction
+
+function a cExtend(b value)
+   provisos(Bits#(a, sa), Bits#(b, sb));
+   let out = unpack(zExtend(pack(value)));
+   return out;
+endfunction
+
+// A user-defined ATF: IdW#(Bit#(n)) = n (i.e. it plays the role of SizeOf).
+typeclass HasIdW#(type t, numeric type n) dependencies (t determines n);
+   type IdW#(type t) = n;
+endtypeclass
+
+instance HasIdW#(Bit#(n), n);
+endinstance
+
+`define TLM_PRM_DCL numeric type id_size,   \
+                    numeric type addr_size
+
+`define TLM_PRM    id_size,   \
+                   addr_size
+
+typedef Bit#(IdW#(Bit#(id_size)))  TLMId#(`TLM_PRM_DCL);
+typedef Bit#(IdW#(Bit#(id_size)))  AxiId#(`TLM_PRM_DCL);
+
+typedef struct {
+                AxiId#(`TLM_PRM)     id;
+                } AxiAddrCmd#(`TLM_PRM_DCL);
+
+function TLMId#(`TLM_PRM) fromAxiId(AxiId#(`TLM_PRM) id);
+   return cExtend(id);
+endfunction
+
+typeclass BusPayload#(type a, type b) dependencies(a determines b);
+   function b getId(a payload);
+endtypeclass
+
+instance BusPayload#(AxiAddrCmd#(`TLM_PRM), TLMId#(`TLM_PRM));
+   function getId(payload);
+      return fromAxiId(payload.id);
+   endfunction
+endinstance
diff --git a/testsuite/bsc.typechecker/primtcons/CExtendATFExplicit.bsv b/testsuite/bsc.typechecker/primtcons/CExtendATFExplicit.bsv
new file mode 100644
index 000000000..3229e2c69
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/CExtendATFExplicit.bsv
@@ -0,0 +1,55 @@
+// As CExtendATF.bsv, but with an explicit type on the 'getId' method.  With
+// the explicit type, typecheck succeeds despite the ATF-triggered synonym
+// expansion in the instance head.  This is the workaround used in bsc-contrib
+// PR 46, and it shows that the CExtendATF failure is not fundamental (see the
+// XXX in CtxRed.ctxRedCQType' and GitHub Issue #311).
+
+function Bit#(m) zExtend(Bit#(n) value)
+   provisos(Add#(n,m,k));
+   Bit#(k) out = zeroExtend(value);
+   if (valueOf(m) == 0)
+      return ?;
+   else
+      return out[valueOf(m) - 1:0];
+endfunction
+
+function a cExtend(b value)
+   provisos(Bits#(a, sa), Bits#(b, sb));
+   let out = unpack(zExtend(pack(value)));
+   return out;
+endfunction
+
+// A user-defined ATF: IdW#(Bit#(n)) = n (i.e. it plays the role of SizeOf).
+typeclass HasIdW#(type t, numeric type n) dependencies (t determines n);
+   type IdW#(type t) = n;
+endtypeclass
+
+instance HasIdW#(Bit#(n), n);
+endinstance
+
+`define TLM_PRM_DCL numeric type id_size,   \
+                    numeric type addr_size
+
+`define TLM_PRM    id_size,   \
+                   addr_size
+
+typedef Bit#(IdW#(Bit#(id_size)))  TLMId#(`TLM_PRM_DCL);
+typedef Bit#(IdW#(Bit#(id_size)))  AxiId#(`TLM_PRM_DCL);
+
+typedef struct {
+                AxiId#(`TLM_PRM)     id;
+                } AxiAddrCmd#(`TLM_PRM_DCL);
+
+function TLMId#(`TLM_PRM) fromAxiId(AxiId#(`TLM_PRM) id);
+   return cExtend(id);
+endfunction
+
+typeclass BusPayload#(type a, type b) dependencies(a determines b);
+   function b getId(a payload);
+endtypeclass
+
+instance BusPayload#(AxiAddrCmd#(`TLM_PRM), TLMId#(`TLM_PRM));
+   function TLMId#(`TLM_PRM) getId(AxiAddrCmd#(`TLM_PRM) payload);
+      return fromAxiId(payload.id);
+   endfunction
+endinstance
diff --git a/testsuite/bsc.typechecker/primtcons/CExtendSynonym.bsv b/testsuite/bsc.typechecker/primtcons/CExtendSynonym.bsv
new file mode 100644
index 000000000..4e47ea575
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/CExtendSynonym.bsv
@@ -0,0 +1,55 @@
+// Reduced version of the bsc-contrib AMBA_TLM library (see bsc-contrib PR 46).
+// Check that we can use type synonyms in instance heads.  The synonyms 'TLMId'
+// and 'AxiId' drop the 'addr_size' parameter; expanding them fully in the
+// instance head would leave 'addr_size' dangling and break unification.  This
+// exercises the (now conditional) synonym expansion in CtxRed.ctxRedCQType' --
+// see the XXX there and GitHub Issue #311.  Because these synonyms contain no
+// type function, the conditional expansion leaves them alone, so this compiles;
+// bsc-contrib PR 46 added explicit method types to work around the earlier
+// (unconditional-expansion) failure, and those are no longer needed here.
+// CExtendATF.bsv shows a variant that *does* still fail, because it puts a type
+// function in the synonyms and so triggers the expansion.
+
+function Bit#(m) zExtend(Bit#(n) value)
+   provisos(Add#(n,m,k));
+   Bit#(k) out = zeroExtend(value);
+   if (valueOf(m) == 0)
+      return ?;
+   else
+      return out[valueOf(m) - 1:0];
+endfunction
+
+function a cExtend(b value)
+   provisos(Bits#(a, sa), Bits#(b, sb));
+
+   let out = unpack(zExtend(pack(value)));
+
+   return out;
+endfunction
+
+`define TLM_PRM_DCL numeric type id_size,   \
+                    numeric type addr_size
+
+`define TLM_PRM    id_size,   \
+                   addr_size
+
+typedef Bit#(id_size)     TLMId#(`TLM_PRM_DCL);
+typedef Bit#(id_size)     AxiId#(`TLM_PRM_DCL);
+
+typedef struct {
+                AxiId#(`TLM_PRM)     id;
+                } AxiAddrCmd#(`TLM_PRM_DCL);
+
+function TLMId#(`TLM_PRM) fromAxiId(AxiId#(`TLM_PRM) id);
+   return cExtend(id);
+endfunction
+
+typeclass BusPayload#(type a, type b) dependencies(a determines b);
+   function b getId(a payload);
+endtypeclass
+
+instance BusPayload#(AxiAddrCmd#(`TLM_PRM), TLMId#(`TLM_PRM));
+   function getId(payload);
+      return fromAxiId(payload.id);
+   endfunction
+endinstance
diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_BS.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_BS.bs
new file mode 100644
index 000000000..87f0d453a
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_BS.bs
@@ -0,0 +1,20 @@
+package ExpSizeOf_FieldSyn_BS where
+
+-- Classic syntax version of ExpSizeOf_FieldSyn.
+-- A struct with a field whose type uses SizeOf through a synonym chain.
+
+type T t = UInt (S t)
+type S t = SizeOf t
+
+struct Node dataType =
+  dat    :: dataType
+  unused :: T dataType
+ deriving (Bits, Eq)
+
+{-# synthesize sysExpSizeOf_FieldSyn_BS #-}
+sysExpSizeOf_FieldSyn_BS :: Module Empty
+sysExpSizeOf_FieldSyn_BS = module
+  r_node :: Reg (Node (UInt 3)) <- mkRegU
+  r_data :: Reg (UInt 3)        <- mkRegU
+  rules
+    when True ==> r_data := r_node.dat
diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Minimal.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Minimal.bs
new file mode 100644
index 000000000..ae7c63d00
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Minimal.bs
@@ -0,0 +1,12 @@
+package ExpSizeOf_FieldSyn_Minimal where
+
+-- Minimal reproduction: a struct with a field type that uses SizeOf
+-- through a type synonym.  Without expanding synonyms in ctxRedCQType, the
+-- needed Bits context is not injected into the derived Generic instance, and
+-- that instance then fails to typecheck -- i.e. the failure is a compile
+-- error, so compile_pass is a sufficient regression guard here.
+
+type S t = SizeOf t
+
+struct Foo a =
+  x :: Bit (S a)
diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Unbound_NoCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Unbound_NoCtx.bs
new file mode 100644
index 000000000..9307d1c1f
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Unbound_NoCtx.bs
@@ -0,0 +1,15 @@
+package ExpSizeOf_FieldSyn_Unbound_NoCtx where
+
+-- A struct field whose type uses SizeOf through a synonym, where the type
+-- variable is *not* a parameter of the struct.  Because the variable is
+-- unbound in the struct type, the field's implicit Bits context cannot be
+-- satisfied by the struct itself, so the field must declare it explicitly.
+-- Here it does not, so typecheck reports the missing context (T0030).
+-- (GitHub Issues #890 and #310: the field's context requirement is not
+-- wrongly exempted here, despite the XXX in TCheck.tiField1.)
+
+type T t = UInt (S t)
+type S t = SizeOf t
+
+struct MyS =
+  sfield :: T dataType
diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Unbound_WithCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Unbound_WithCtx.bs
new file mode 100644
index 000000000..223ca6012
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Unbound_WithCtx.bs
@@ -0,0 +1,11 @@
+package ExpSizeOf_FieldSyn_Unbound_WithCtx where
+
+-- As ExpSizeOf_FieldSyn_Unbound_NoCtx, but the field declares the Bits
+-- context that its SizeOf-using type requires, so typecheck succeeds.
+-- (GitHub Issues #890 and #310)
+
+type T t = UInt (S t)
+type S t = SizeOf t
+
+struct MyS =
+  sfield :: (Bits dataType sz) => T dataType
diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_NoCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_NoCtx.bs
new file mode 100644
index 000000000..2b39de54f
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_NoCtx.bs
@@ -0,0 +1,19 @@
+package ExpSizeOf_FieldSyn_Use_NoCtx where
+
+-- Reading a struct field whose type uses SizeOf through a synonym chain
+-- requires a Bits context on the struct's type parameter.  The field type
+-- 'T a' expands to 'UInt (SizeOf a)', and reading the field during typecheck
+-- introduces the implicit 'Bits a' context.  Here it is not provided, so
+-- typecheck reports the missing context (T0030), confirming that the field's
+-- context requirement is handled during typecheck.  (GitHub Issue #890)
+
+type T t = UInt (S t)
+type S t = SizeOf t
+
+struct Node dataType =
+  dat  :: dataType
+  wide :: T dataType
+ deriving (Bits, Eq)
+
+fnNeedsCtx :: Node a -> Bool
+fnNeedsCtx n = n.wide == 0
diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_NoCtx.bs.bsc-out.expected b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_NoCtx.bs.bsc-out.expected
new file mode 100644
index 000000000..a854839a6
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_NoCtx.bs.bsc-out.expected
@@ -0,0 +1,12 @@
+checking package dependencies
+compiling ExpSizeOf_FieldSyn_Use_NoCtx.bs
+Error: "ExpSizeOf_FieldSyn_Use_NoCtx.bs", line 18, column 0: (T0030)
+  The contexts for this expression are too general.
+  Given type:
+    ExpSizeOf_FieldSyn_Use_NoCtx.Node a -> Prelude.Bool
+  The following contexts are needed:
+    Prelude.Bits a a__
+      Introduced at the following locations:
+	"ExpSizeOf_FieldSyn_Use_NoCtx.bs", line 15, column 10
+  The type variables are from the following positions:
+    "a__" at "ExpSizeOf_FieldSyn_Use_NoCtx.bs", line 15, column 10
diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_WithCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_WithCtx.bs
new file mode 100644
index 000000000..490091a50
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_FieldSyn_Use_WithCtx.bs
@@ -0,0 +1,15 @@
+package ExpSizeOf_FieldSyn_Use_WithCtx where
+
+-- As ExpSizeOf_FieldSyn_Use_NoCtx, but with the explicit Bits context that
+-- reading the field requires, so typecheck succeeds.  (GitHub Issue #890)
+
+type T t = UInt (S t)
+type S t = SizeOf t
+
+struct Node dataType =
+  dat  :: dataType
+  wide :: T dataType
+ deriving (Bits, Eq)
+
+fnNeedsCtx :: (Bits a sa) => Node a -> Bool
+fnNeedsCtx n = n.wide == 0
diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs
new file mode 100644
index 000000000..f746af2c4
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs
@@ -0,0 +1,12 @@
+package ExpSizeOf_Let_NoCtx where
+
+-- A let binding whose type annotation contains SizeOf requires a Bits
+-- context: expanding the SizeOf in the declared type introduces an implicit
+-- Bits context, which must be provided by an explicit context on the
+-- enclosing definition.  Here none is given, so typecheck reports the
+-- missing context (T0030).  (GitHub Issue #890)
+
+foo :: a -> String
+foo _ = let x :: Bit (SizeOf a)
+            x = _
+        in  printType $ typeOf $ x
diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs.bsc-out.expected b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs.bsc-out.expected
new file mode 100644
index 000000000..bacb7541a
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_Let_NoCtx.bs.bsc-out.expected
@@ -0,0 +1,12 @@
+checking package dependencies
+compiling ExpSizeOf_Let_NoCtx.bs
+Error: "ExpSizeOf_Let_NoCtx.bs", line 9, column 0: (T0030)
+  The contexts for this expression are too general.
+  Given type:
+    a -> Prelude.String
+  The following contexts are needed:
+    Prelude.Bits a a__
+      Introduced at the following locations:
+	"ExpSizeOf_Let_NoCtx.bs", line 10, column 22
+  The type variables are from the following positions:
+    "a__" at "ExpSizeOf_Let_NoCtx.bs", line 10, column 22
diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_NoCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_NoCtx.bs
new file mode 100644
index 000000000..3f09c2ff7
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_NoCtx.bs
@@ -0,0 +1,12 @@
+package ExpSizeOf_StringOf_NoCtx where
+
+data Thing = Thing (UInt 42) deriving (Bits)
+
+foo :: a -> String
+foo _ = stringOf (TNumToStr (SizeOf a))
+
+{-# synthesize main #-}
+main :: Module Empty
+main = module
+  rules
+    "asdf": when True ==> $display (foo $ Thing _)
diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_NoCtx.bs.bsc-out.expected b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_NoCtx.bs.bsc-out.expected
new file mode 100644
index 000000000..adfc6019e
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_NoCtx.bs.bsc-out.expected
@@ -0,0 +1,12 @@
+checking package dependencies
+compiling ExpSizeOf_StringOf_NoCtx.bs
+Error: "ExpSizeOf_StringOf_NoCtx.bs", line 5, column 0: (T0030)
+  The contexts for this expression are too general.
+  Given type:
+    a -> Prelude.String
+  The following contexts are needed:
+    Prelude.Bits a a__
+      Introduced at the following locations:
+	"ExpSizeOf_StringOf_NoCtx.bs", line 6, column 29
+  The type variables are from the following positions:
+    "a__" at "ExpSizeOf_StringOf_NoCtx.bs", line 6, column 29
diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_WithCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_WithCtx.bs
new file mode 100644
index 000000000..c3692d8a3
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_StringOf_WithCtx.bs
@@ -0,0 +1,12 @@
+package ExpSizeOf_StringOf_WithCtx where
+
+data Thing = Thing (UInt 42) deriving (Bits)
+
+foo :: (Bits a sz) => a -> String
+foo _ = stringOf (TNumToStr (SizeOf a))
+
+{-# synthesize main #-}
+main :: Module Empty
+main = module
+  rules
+    "asdf": when True ==> $display (foo $ Thing _)
diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_NoCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_NoCtx.bs
new file mode 100644
index 000000000..9536b37b0
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_NoCtx.bs
@@ -0,0 +1,9 @@
+package ExpSizeOf_TypedExpr_NoCtx where
+
+-- A type-annotated expression whose type mentions SizeOf introduces an
+-- implicit Bits context, the same way 'valueOf'/'stringOf' do (they are
+-- implemented using type-annotated expressions).  Here the context is not
+-- provided, so typecheck reports it (T0030).  (GitHub Issue #890)
+
+foo :: a -> String
+foo _ = printType $ typeOf (_ :: Bit (SizeOf a))
diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_NoCtx.bs.bsc-out.expected b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_NoCtx.bs.bsc-out.expected
new file mode 100644
index 000000000..1aa140360
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_NoCtx.bs.bsc-out.expected
@@ -0,0 +1,12 @@
+checking package dependencies
+compiling ExpSizeOf_TypedExpr_NoCtx.bs
+Error: "ExpSizeOf_TypedExpr_NoCtx.bs", line 8, column 0: (T0030)
+  The contexts for this expression are too general.
+  Given type:
+    a -> Prelude.String
+  The following contexts are needed:
+    Prelude.Bits a a__
+      Introduced at the following locations:
+	"ExpSizeOf_TypedExpr_NoCtx.bs", line 9, column 38
+  The type variables are from the following positions:
+    "a__" at "ExpSizeOf_TypedExpr_NoCtx.bs", line 9, column 38
diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_WithCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_WithCtx.bs
new file mode 100644
index 000000000..ce6dd6b4c
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_TypedExpr_WithCtx.bs
@@ -0,0 +1,7 @@
+package ExpSizeOf_TypedExpr_WithCtx where
+
+-- With an explicit Bits context, the SizeOf in a type-annotated expression
+-- can be reduced during typecheck.  (GitHub Issue #890)
+
+foo :: (Bits a sz) => a -> String
+foo _ = printType $ typeOf (_ :: Bit (SizeOf a))
diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_NoCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_NoCtx.bs
new file mode 100644
index 000000000..227418f74
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_NoCtx.bs
@@ -0,0 +1,12 @@
+package ExpSizeOf_ValueOf_NoCtx where
+
+data Thing = Thing (UInt 42) deriving (Bits)
+
+foo :: a -> Integer
+foo _ = valueOf (SizeOf a)
+
+{-# synthesize main #-}
+main :: Module Empty
+main = module
+  rules
+    "asdf": when True ==> $display (foo $ Thing _)
diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_NoCtx.bs.bsc-out.expected b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_NoCtx.bs.bsc-out.expected
new file mode 100644
index 000000000..38ff942da
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_NoCtx.bs.bsc-out.expected
@@ -0,0 +1,12 @@
+checking package dependencies
+compiling ExpSizeOf_ValueOf_NoCtx.bs
+Error: "ExpSizeOf_ValueOf_NoCtx.bs", line 5, column 0: (T0030)
+  The contexts for this expression are too general.
+  Given type:
+    a -> Prelude.Integer
+  The following contexts are needed:
+    Prelude.Bits a a__
+      Introduced at the following locations:
+	"ExpSizeOf_ValueOf_NoCtx.bs", line 6, column 17
+  The type variables are from the following positions:
+    "a__" at "ExpSizeOf_ValueOf_NoCtx.bs", line 6, column 17
diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_WithCtx.bs b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_WithCtx.bs
new file mode 100644
index 000000000..e1f08665d
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_ValueOf_WithCtx.bs
@@ -0,0 +1,12 @@
+package ExpSizeOf_ValueOf_WithCtx where
+
+data Thing = Thing (UInt 42) deriving (Bits)
+
+foo :: (Bits a sz) => a -> Integer
+foo _ = valueOf (SizeOf a)
+
+{-# synthesize main #-}
+main :: Module Empty
+main = module
+  rules
+    "asdf": when True ==> $display (foo $ Thing _)
diff --git a/testsuite/bsc.typechecker/primtcons/ExpSizeOf_VectorIfc.bsv b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_VectorIfc.bsv
new file mode 100644
index 000000000..03649e02c
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ExpSizeOf_VectorIfc.bsv
@@ -0,0 +1,27 @@
+// GitHub Issue #313 (Bluespec Inc Bug 1917): a SizeOf in the length parameter
+// of a Vector of subinterfaces confuses GenWrap's method-vs-subinterface
+// determination, which happens before typecheck and so cannot reduce
+// SizeOf#(Bit#(2)) to 2.  BSC therefore treats 'example' as a method and
+// requires its element type to be bitifiable.
+//
+// This is not fixed by the type-function expansion added in PR #916: the
+// example still typechecks fine (see the companion compile_pass), but fails when
+// synthesized (compile_verilog_fail_error, T0043).  The test documents the
+// current behavior; if #313 is fixed, this should become a compile_verilog_pass.
+
+import Vector::*;
+
+// Using 'SizeOf#(Bit#(2))' triggers the bug; 'typedef 2 Length' would not.
+typedef SizeOf#(Bit#(2)) Length;
+
+typedef Bit#(1) Data;
+
+interface Example;
+  interface Vector#(Length, WriteOnly#(Data)) example;
+endinterface
+
+(* synthesize *)
+module mkExample (Example);
+  Vector#(Length, Reg#(Data)) ex <- replicateM(mkRegU);
+  interface example = ?;
+endmodule
diff --git a/testsuite/bsc.typechecker/primtcons/ValueOf_KindMismatch_Arity.bs b/testsuite/bsc.typechecker/primtcons/ValueOf_KindMismatch_Arity.bs
new file mode 100644
index 000000000..a13e418c3
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ValueOf_KindMismatch_Arity.bs
@@ -0,0 +1,4 @@
+package ValueOf_KindMismatch_Arity where
+
+bar :: Integer
+bar = valueOf (SizeOf Int)
diff --git a/testsuite/bsc.typechecker/primtcons/ValueOf_KindMismatch_Res.bs b/testsuite/bsc.typechecker/primtcons/ValueOf_KindMismatch_Res.bs
new file mode 100644
index 000000000..aa14a1bd9
--- /dev/null
+++ b/testsuite/bsc.typechecker/primtcons/ValueOf_KindMismatch_Res.bs
@@ -0,0 +1,4 @@
+package ValueOf_KindMismatch_Res where
+
+baz :: Integer
+baz = valueOf Bool
diff --git a/testsuite/bsc.typechecker/primtcons/primtcons.exp b/testsuite/bsc.typechecker/primtcons/primtcons.exp
index 51712df07..f9295be37 100644
--- a/testsuite/bsc.typechecker/primtcons/primtcons.exp
+++ b/testsuite/bsc.typechecker/primtcons/primtcons.exp
@@ -18,8 +18,9 @@ compile_pass ExpSizeOf_Instances.bsv
 
 compile_pass ExpSizeOf_InstancesBase.bsv
 
-# Test that SizeOf is expanded even when it's buried in a type synonym
-compile_pass_bug ExpSizeOf_InstancesBaseSyn.bsv 1729
+# Test that SizeOf is expanded even when it's buried in a type synonym.
+# This was Bluespec Inc Bug 1729 (also GitHub Issue #311).
+compile_pass ExpSizeOf_InstancesBaseSyn.bsv
 
 # ---------------
 # Test that SizeOf introduced through the type of a field in a struct value
@@ -32,6 +33,82 @@ compile_verilog_pass ExpSizeOf_Field.bsv
 # but after adding the normtypes pass (later replaced by extra normalization in expanded),
 # it succeeds.
 compile_verilog_pass ExpSizeOf_FieldSyn.bsv
+compile_verilog_pass ExpSizeOf_FieldSyn_BS.bs
+
+# Minimal reproduction: without expanding the synonym in ctxRedCQType, the
+# derived Generic instance fails to typecheck (the needed Bits context is not
+# injected), so it fails to compile.  A plain compile_pass is therefore a
+# sufficient regression guard -- no intermediate dump is needed.
+compile_pass ExpSizeOf_FieldSyn_Minimal.bs
+
+# Using a struct field whose type uses SizeOf through a synonym requires a Bits
+# context on the struct's type parameter.  The requirement is introduced during
+# typecheck of the field access, so it must be provided (GitHub Issue #890).
+compile_fail_error ExpSizeOf_FieldSyn_Use_NoCtx.bs T0030
+compare_file [make_bsc_output_name ExpSizeOf_FieldSyn_Use_NoCtx.bs]
+compile_pass ExpSizeOf_FieldSyn_Use_WithCtx.bs
+
+# A struct field whose SizeOf-using type has a type variable that is not a
+# parameter of the struct is not exempted from the Bits requirement: the field
+# must declare the context explicitly (GitHub Issues #890 and #310).  BSC
+# currently reports two T0030 errors here (one of which lacks a source
+# position), so this uses an expected count of 2 rather than compare_file.
+compile_fail_error ExpSizeOf_FieldSyn_Unbound_NoCtx.bs T0030 2
+compile_pass ExpSizeOf_FieldSyn_Unbound_WithCtx.bs
+
+# ---------------
+# Test that type functions like SizeOf are expanded in explicitly-typed
+# expressions, introducing the implicit contexts they require and reporting an
+# error when those contexts are not provided (GitHub Issue #890).  This covers
+# 'valueOf', 'stringOf', type-annotated expressions, and explicitly-typed let
+# bindings (valueOf and stringOf are themselves implemented using type-annotated
+# expressions).
+
+# valueOf
+compile_fail_error ExpSizeOf_ValueOf_NoCtx.bs T0030
+compare_file [make_bsc_output_name ExpSizeOf_ValueOf_NoCtx.bs]
+compile_pass ExpSizeOf_ValueOf_WithCtx.bs
+
+# stringOf
+compile_fail_error ExpSizeOf_StringOf_NoCtx.bs T0030
+compare_file [make_bsc_output_name ExpSizeOf_StringOf_NoCtx.bs]
+compile_pass ExpSizeOf_StringOf_WithCtx.bs
+
+# type-annotated expression, e.g. '(_ :: Bit (SizeOf a))'
+compile_fail_error ExpSizeOf_TypedExpr_NoCtx.bs T0030
+compare_file [make_bsc_output_name ExpSizeOf_TypedExpr_NoCtx.bs]
+compile_pass ExpSizeOf_TypedExpr_WithCtx.bs
+
+# explicitly-typed let binding
+compile_fail_error ExpSizeOf_Let_NoCtx.bs T0030
+compare_file [make_bsc_output_name ExpSizeOf_Let_NoCtx.bs]
+
+# Kind errors in valueOf type argument
+compile_fail_error ValueOf_KindMismatch_Arity.bs T0025
+compile_fail_error ValueOf_KindMismatch_Res.bs T0026
+
+# ---------------
+# Type synonyms and type functions in instance heads
+# (GitHub Issue #311, bsc-contrib PR 46)
+
+# Plain type synonyms in an instance head are left unexpanded, so this compiles
+# without the explicit method types that bsc-contrib PR 46 previously needed.
+compile_pass CExtendSynonym.bsv
+
+# A type function (here a user-defined ATF) in the instance-head synonyms forces
+# the conditional expansion in ctxRedCQType', which re-introduces the dangling
+# parameter and still fails -- unless explicit method types are given.  This is
+# the case that remains broken (GitHub Issue #311).
+compile_fail_error CExtendATF.bsv T0035
+compile_pass CExtendATFExplicit.bsv
+
+# ---------------
+# SizeOf in the length of a Vector of subinterfaces (GitHub Issue #313,
+# Bluespec Inc Bug 1917).  This is not fixed by PR #916: the example typechecks,
+# but fails when synthesized, because GenWrap decides whether the field is a
+# method or a subinterface before typecheck and cannot reduce the SizeOf.
+compile_pass ExpSizeOf_VectorIfc.bsv
+compile_verilog_fail_error ExpSizeOf_VectorIfc.bsv T0043
 
 # ---------------
 
diff --git a/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyError.bs b/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyError.bs
new file mode 100644
index 000000000..440b5d381
--- /dev/null
+++ b/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyError.bs
@@ -0,0 +1,25 @@
+package ATFFieldUnifyError where
+
+-- Like ATFUnifyError, but the unification of a type function application with
+-- a concrete type is forced by reading a struct field.  Reading a field whose
+-- type is 'Elem f' and assigning it to Bool requires 'Container f Bool', which
+-- is not in scope, so typecheck reports the missing context (T0030).
+
+class Container f e | f -> e where
+  type Elem f = e
+  wrap   :: e -> f
+  unwrap :: f -> e
+
+data Box a = Box a
+
+instance Container (Box a) a where
+  wrap = Box
+  unwrap (Box x) = x
+
+-- Reading a struct field whose type is Elem f, and assigning to Bool,
+-- requires Container f Bool which is not in scope.
+struct Holder f =
+  val :: Elem f
+
+getBool :: Holder a -> Bool
+getBool h = h.val
diff --git a/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyError.bs.bsc-out.expected b/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyError.bs.bsc-out.expected
new file mode 100644
index 000000000..705fc1423
--- /dev/null
+++ b/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyError.bs.bsc-out.expected
@@ -0,0 +1,10 @@
+checking package dependencies
+compiling ATFFieldUnifyError.bs
+Error: "ATFFieldUnifyError.bs", line 24, column 0: (T0030)
+  The contexts for this expression are too general.
+  Given type:
+    ATFFieldUnifyError.Holder a -> Prelude.Bool
+  The following contexts are needed:
+    ATFFieldUnifyError.Container a Prelude.Bool
+      Introduced at the following locations:
+	"ATFFieldUnifyError.bs", line 25, column 12
diff --git a/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyHKError.bs b/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyHKError.bs
new file mode 100644
index 000000000..ed9bf01fa
--- /dev/null
+++ b/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyHKError.bs
@@ -0,0 +1,18 @@
+package ATFFieldUnifyHKError where
+
+-- Like ATFUnifyHKError, but the unification of a higher-kinded type function
+-- application with a concrete type constructor is forced by reading a struct
+-- field.  Reading a field whose type uses the higher-kinded ATF (Elem a), and
+-- assigning it to Foo Maybe, requires Container a Maybe which is not in scope,
+-- so typecheck reports the missing context (T0030).
+
+class (Container :: * -> (* -> *) -> *) a s | a -> s where
+  type Elem a = s
+
+data Foo f = Foo (f Bool)
+
+struct Holder a =
+  val :: Foo (Elem a)
+
+getMaybe :: Holder a -> Foo Maybe
+getMaybe h = h.val
diff --git a/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyHKError.bs.bsc-out.expected b/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyHKError.bs.bsc-out.expected
new file mode 100644
index 000000000..bed5d2fb7
--- /dev/null
+++ b/testsuite/bsc.typechecker/typeclasses/ATFFieldUnifyHKError.bs.bsc-out.expected
@@ -0,0 +1,10 @@
+checking package dependencies
+compiling ATFFieldUnifyHKError.bs
+Error: "ATFFieldUnifyHKError.bs", line 17, column 0: (T0030)
+  The contexts for this expression are too general.
+  Given type:
+    ATFFieldUnifyHKError.Holder a -> ATFFieldUnifyHKError.Foo Prelude.Maybe
+  The following contexts are needed:
+    ATFFieldUnifyHKError.Container a Prelude.Maybe
+      Introduced at the following locations:
+	"ATFFieldUnifyHKError.bs", line 18, column 13
diff --git a/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadDeterminedSynonym.bs b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadDeterminedSynonym.bs
new file mode 100644
index 000000000..2bba5307d
--- /dev/null
+++ b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadDeterminedSynonym.bs
@@ -0,0 +1,22 @@
+package ATFInInstHeadDeterminedSynonym where
+
+-- Like ATFInInstHeadDetermined, but the type function reaches the
+-- determined position through a type synonym.  Determined positions
+-- are never used for instance matching, so this must stay allowed,
+-- synonym or not.
+
+class Container f e | f -> e where
+  type Elem f = e
+  wrap :: e -> f
+
+type ElemSyn f = Elem f
+
+data Box a = Box a
+instance Container (Box a) a where
+  wrap = Box
+
+class Bar a b | a -> b where
+  bar :: a -> b
+
+instance Bar (Box a) (ElemSyn (Box a)) where
+  bar (Box x) = x
diff --git a/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonym.bs b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonym.bs
new file mode 100644
index 000000000..552956414
--- /dev/null
+++ b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonym.bs
@@ -0,0 +1,19 @@
+package ATFInInstHeadSynonym where
+
+-- Like ATFInInstHead, but the type function reaches the instance head
+-- through a type synonym, applied to a type variable.  The check must
+-- see through the synonym and reject this the same way it rejects the
+-- directly-written form: the application can neither be reduced away
+-- nor used for instance matching.
+
+class Container f e | f -> e where
+  type Elem f = e
+  wrap :: e -> f
+
+type ElemSyn f = Elem f
+
+class Foo a where
+  foo :: a -> Bool
+
+instance Foo (ElemSyn f) where
+  foo _ = True
diff --git a/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonym.bs.bsc-out.expected b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonym.bs.bsc-out.expected
new file mode 100644
index 000000000..e0bc4b615
--- /dev/null
+++ b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonym.bs.bsc-out.expected
@@ -0,0 +1,4 @@
+checking package dependencies
+compiling ATFInInstHeadSynonym.bs
+Error: "ATFInInstHeadSynonym.bs", line 18, column 14: (T0156)
+  Type function `ATFInInstHeadSynonym.Elem' cannot be used in an instance head
diff --git a/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymBoth.bs b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymBoth.bs
new file mode 100644
index 000000000..caeac07ca
--- /dev/null
+++ b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymBoth.bs
@@ -0,0 +1,19 @@
+package ATFInInstHeadSynonymBoth where
+
+-- Both a directly-written and a synonym-hidden type function in the
+-- same instance head: both must be reported (two T0156 errors), not
+-- just the directly-written one.
+
+class Container f e | f -> e where
+  type Elem f = e
+  wrap :: e -> f
+
+type ElemSyn f = Elem f
+
+data Pair a b = Pair a b
+
+class Foo a where
+  foo :: a -> Bool
+
+instance Foo (Pair (Elem f) (ElemSyn g)) where
+  foo _ = True
diff --git a/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymBoth.bs.bsc-out.expected b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymBoth.bs.bsc-out.expected
new file mode 100644
index 000000000..ceb5ab5ad
--- /dev/null
+++ b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymBoth.bs.bsc-out.expected
@@ -0,0 +1,7 @@
+checking package dependencies
+compiling ATFInInstHeadSynonymBoth.bs
+Error: "ATFInInstHeadSynonymBoth.bs", line 18, column 20: (T0156)
+  Type function `Elem' cannot be used in an instance head
+Error: "ATFInInstHeadSynonymBoth.bs", line 18, column 29: (T0156)
+  Type function `ATFInInstHeadSynonymBoth.Elem' cannot be used in an instance
+  head
diff --git a/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymElsewhere.bs b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymElsewhere.bs
new file mode 100644
index 000000000..11edf6574
--- /dev/null
+++ b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymElsewhere.bs
@@ -0,0 +1,21 @@
+package ATFInInstHeadSynonymElsewhere where
+
+-- Like ATFInInstHeadSynonym, but the type function's argument also
+-- appears elsewhere in the instance head.  Before the check saw
+-- through synonyms, this form was silently accepted (the head was
+-- rewritten by instance-head expansion), while the directly-written
+-- form was rejected with T0156.  Both must be rejected identically.
+
+class Container f e | f -> e where
+  type Elem f = e
+  wrap :: e -> f
+
+type ElemSyn f = Elem f
+
+data Pair a b = Pair a b
+
+class Foo a where
+  foo :: a -> Bool
+
+instance Foo (Pair f (ElemSyn f)) where
+  foo _ = True
diff --git a/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymElsewhere.bs.bsc-out.expected b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymElsewhere.bs.bsc-out.expected
new file mode 100644
index 000000000..cebea81ba
--- /dev/null
+++ b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymElsewhere.bs.bsc-out.expected
@@ -0,0 +1,5 @@
+checking package dependencies
+compiling ATFInInstHeadSynonymElsewhere.bs
+Error: "ATFInInstHeadSynonymElsewhere.bs", line 20, column 22: (T0156)
+  Type function `ATFInInstHeadSynonymElsewhere.Elem' cannot be used in an
+  instance head
diff --git a/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymGround.bs b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymGround.bs
new file mode 100644
index 000000000..d18641547
--- /dev/null
+++ b/testsuite/bsc.typechecker/typeclasses/ATFInInstHeadSynonymGround.bs
@@ -0,0 +1,24 @@
+package ATFInInstHeadSynonymGround where
+
+-- A type function hidden behind a type synonym in an instance head is
+-- allowed when its application is ground: context reduction expands
+-- and reduces it to a concrete type (here Elem (Box Integer) reduces
+-- to Integer).  Same behavior as ExpSizeOf_InstancesBaseSyn (Bug 1729,
+-- GitHub issue #311), with a user-defined ATF.
+
+class Container f e | f -> e where
+  type Elem f = e
+  wrap :: e -> f
+
+type ElemSyn f = Elem f
+
+data Box a = Box a
+
+instance Container (Box a) a where
+  wrap = Box
+
+class Foo a where
+  foo :: a -> Bool
+
+instance Foo (ElemSyn (Box Integer)) where
+  foo _ = True
diff --git a/testsuite/bsc.typechecker/typeclasses/ATFPolyDataWidth.bs b/testsuite/bsc.typechecker/typeclasses/ATFPolyDataWidth.bs
index 6e66f7c25..679fec40c 100644
--- a/testsuite/bsc.typechecker/typeclasses/ATFPolyDataWidth.bs
+++ b/testsuite/bsc.typechecker/typeclasses/ATFPolyDataWidth.bs
@@ -31,11 +31,12 @@ mkEncoded val =
   let raw = toBit val
   in Encoded raw (zeroExtend raw)
 
--- Polymorphic pattern match
-getRaw :: Encoded f -> Bit (Width f)
+-- Polymorphic pattern match: need HasWidth context because Width f
+-- in the return type generates an implicit HasWidth predicate.
+getRaw :: (HasWidth f n) => Encoded f -> Bit (Width f)
 getRaw (Encoded r _) = r
 
-getExtended :: Encoded f -> Bit (TAdd (Width f) 1)
+getExtended :: (HasWidth f n) => Encoded f -> Bit (TAdd (Width f) 1)
 getExtended (Encoded _ e) = e
 
 -- Concrete: Width Byte = 8, TAdd 8 1 = 9
diff --git a/testsuite/bsc.typechecker/typeclasses/ATFSynonymField.bs b/testsuite/bsc.typechecker/typeclasses/ATFSynonymField.bs
new file mode 100644
index 000000000..e79cae657
--- /dev/null
+++ b/testsuite/bsc.typechecker/typeclasses/ATFSynonymField.bs
@@ -0,0 +1,29 @@
+package ATFSynonymField where
+
+-- Test that a data/struct field whose type reaches an associated type
+-- function through a type synonym compiles.  The auto-derived Generic
+-- instance must not report a spurious "signature too general" (T0029)
+-- error: the given scheme (from the instance head, where synonyms are
+-- expanded and the type function is generalized to a fresh variable
+-- constrained by the class predicate) and the deduced scheme (where the
+-- field type keeps the unexpanded synonym) are equal up to the
+-- fundep-forced substitution.
+
+class Container f e | f -> e where
+  type Elem f = e
+  extract :: f -> e
+
+type ElemSyn f = Elem f
+
+data WrapSyn f =
+   WrapSyn (ElemSyn f)
+ | NoElem
+
+struct SBox f =
+  field :: ElemSyn f
+
+-- A field applying the type function directly (not via a synonym)
+-- already compiled; check that it stays working.
+data WrapDirect f =
+   WrapDirect (Elem f)
+ | NoElemDirect
diff --git a/testsuite/bsc.typechecker/typeclasses/ATFSynonymFieldUse.bs b/testsuite/bsc.typechecker/typeclasses/ATFSynonymFieldUse.bs
new file mode 100644
index 000000000..4a5ea49d4
--- /dev/null
+++ b/testsuite/bsc.typechecker/typeclasses/ATFSynonymFieldUse.bs
@@ -0,0 +1,48 @@
+package ATFSynonymFieldUse where
+
+-- Companion to ATFSynonymField: exercise data/struct fields whose types
+-- reach an ATF through a type synonym, all the way through elaboration.
+-- The derived Generic instances are used explicitly (via from/to) and
+-- the types are stored in registers, so the synonym-hidden ATF must
+-- survive typecheck, Bits derivation, and synthesis.
+
+class Container f e | f -> e where
+  type Elem f = e
+  extract :: f -> e
+
+type ElemSyn f = Elem f
+
+data Box a = Box a
+
+instance Container (Box a) a where
+  extract (Box x) = x
+
+data WrapSyn f =
+   WrapSyn (ElemSyn f)
+ | NoElem
+ deriving (Bits)
+
+struct SBox f =
+  field :: ElemSyn f
+ deriving (Bits)
+
+-- Round trip through the derived Generic representation.
+roundTrip :: (Generic a r) => a -> a
+roundTrip x = to (from x)
+
+sboxVal :: SBox (Box (UInt 8))
+sboxVal = SBox { field = 42 }
+
+wrapVal :: WrapSyn (Box (UInt 8))
+wrapVal = WrapSyn 42
+
+{-# synthesize sysATFSynonymFieldUse #-}
+sysATFSynonymFieldUse :: Module Empty
+sysATFSynonymFieldUse = module
+  r1 :: Reg (SBox (Box (UInt 8))) <- mkReg (roundTrip sboxVal)
+  r2 :: Reg (WrapSyn (Box (UInt 8))) <- mkReg (roundTrip wrapVal)
+
+  rules
+    when True ==> do
+      r1 := SBox { field = extract (Box (r1.field + 1)) }
+      r2 := roundTrip (WrapSyn r1.field)
diff --git a/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs b/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs
index eac7a1e73..d8a6f808c 100644
--- a/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs
+++ b/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs
@@ -1,7 +1,10 @@
 package ATFUnifyError where
 
--- Test that unification of two different type function applications fails
--- when they cannot be proven equal.
+-- Test that unifying a type function application (Elem a) with a concrete
+-- type (Bool) requires the corresponding class context (Container a Bool).
+-- Here it is missing, so typecheck reports it (T0030).  The unification is
+-- forced by giving 'id' the explicit type 'a -> Elem a -> Bool'.
+-- (See ATFFieldUnifyError for the same check via struct field access.)
 
 class Container f e | f -> e where
   type Elem f = e
diff --git a/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs.bsc-out.expected b/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs.bsc-out.expected
index 5fbec0d16..f23e0e286 100644
--- a/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs.bsc-out.expected
+++ b/testsuite/bsc.typechecker/typeclasses/ATFUnifyError.bs.bsc-out.expected
@@ -1,10 +1,11 @@
 checking package dependencies
 compiling ATFUnifyError.bs
-Error: "ATFUnifyError.bs", line 18, column 0: (T0030)
+Error: "ATFUnifyError.bs", line 21, column 0: (T0030)
   The contexts for this expression are too general.
   Given type:
     a -> ATFUnifyError.Elem a -> Prelude.Bool
   The following contexts are needed:
     ATFUnifyError.Container a Prelude.Bool
       Introduced at the following locations:
-	"ATFUnifyError.bs", line 19, column 9
+	"ATFUnifyError.bs", line 21, column 13
+	"ATFUnifyError.bs", line 22, column 9
diff --git a/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs b/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs
index ff3a22444..0bfcdb188 100644
--- a/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs
+++ b/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs
@@ -1,6 +1,11 @@
 package ATFUnifyHKError where
 
--- Test that higher-kinded type function constraints fail properly.
+-- Test that unifying a higher-kinded type function application (Elem a,
+-- of kind * -> *) with a concrete type constructor (Maybe) requires the
+-- corresponding class context (Container a Maybe).  Here it is missing, so
+-- typecheck reports it (T0030).  The unification is forced by giving 'id'
+-- the explicit type 'a -> Foo (Elem a) -> Foo Maybe'.
+-- (See ATFFieldUnifyHKError for the same check via struct field access.)
 
 class (Container :: * -> (* -> *) -> *) a s | a -> s where
   type Elem a = s
diff --git a/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs.bsc-out.expected b/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs.bsc-out.expected
index 83bf6d1a4..ac04359d7 100644
--- a/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs.bsc-out.expected
+++ b/testsuite/bsc.typechecker/typeclasses/ATFUnifyHKError.bs.bsc-out.expected
@@ -1,6 +1,6 @@
 checking package dependencies
 compiling ATFUnifyHKError.bs
-Error: "ATFUnifyHKError.bs", line 10, column 0: (T0030)
+Error: "ATFUnifyHKError.bs", line 15, column 0: (T0030)
   The contexts for this expression are too general.
   Given type:
     a -> ATFUnifyHKError.Foo (ATFUnifyHKError.Elem a) -> ATFUnifyHKError.Foo
@@ -8,4 +8,5 @@ Error: "ATFUnifyHKError.bs", line 10, column 0: (T0030)
   The following contexts are needed:
     ATFUnifyHKError.Container a Prelude.Maybe
       Introduced at the following locations:
-	"ATFUnifyHKError.bs", line 11, column 9
+	"ATFUnifyHKError.bs", line 15, column 18
+	"ATFUnifyHKError.bs", line 16, column 9
diff --git a/testsuite/bsc.typechecker/typeclasses/typeclasses.exp b/testsuite/bsc.typechecker/typeclasses/typeclasses.exp
index 709629a59..87cfe6ad1 100644
--- a/testsuite/bsc.typechecker/typeclasses/typeclasses.exp
+++ b/testsuite/bsc.typechecker/typeclasses/typeclasses.exp
@@ -86,10 +86,16 @@ compile_pass ATFImported.bs
 compile_pass ATFUnify.bs
 compile_pass ATFUnifyHK.bs
 compile_pass ATFInInstHeadDetermined.bs
+compile_pass ATFInInstHeadDeterminedSynonym.bs
+compile_pass ATFInInstHeadSynonymGround.bs
 compile_pass ATFInjective.bs
 compile_pass ATFFieldAccess.bs
 compile_pass ATFPartialApp.bs
+# A field type that reaches an ATF through a type synonym must not make
+# the auto-derived Generic instance fail with a spurious T0029
+compile_pass ATFSynonymField.bs
 
+compile_verilog_pass ATFSynonymFieldUse.bs
 compile_verilog_pass ATFSizeOf.bs
 compile_verilog_pass ATFPoly.bs
 compile_verilog_pass ATFSynthIfc.bs
@@ -128,12 +134,26 @@ compile_fail_error ATFInInstHead.bs T0156
 compare_file ATFInInstHead.bs.bsc-out
 compile_fail_error ATFInInstHeadBiDirectional.bs T0156
 compare_file ATFInInstHeadBiDirectional.bs.bsc-out
+# Same checks with the type function hidden behind a type synonym
+compile_fail_error ATFInInstHeadSynonym.bs T0156
+compare_file ATFInInstHeadSynonym.bs.bsc-out
+compile_fail_error ATFInInstHeadSynonymElsewhere.bs T0156
+compare_file ATFInInstHeadSynonymElsewhere.bs.bsc-out
+# A direct and a synonym-hidden type function in the same head: both reported
+compile_fail_error ATFInInstHeadSynonymBoth.bs T0156 2
+compare_file ATFInInstHeadSynonymBoth.bs.bsc-out
 compile_fail_error ATFResultNotDetermined.bs T0155
 compare_file ATFResultNotDetermined.bs.bsc-out
 compile_fail_error ATFUnifyError.bs T0030
 compare_file ATFUnifyError.bs.bsc-out
 compile_fail_error ATFUnifyHKError.bs T0030
 compare_file ATFUnifyHKError.bs.bsc-out
+# Same checks as ATFUnify{,HK}Error, but forcing the unification via struct
+# field access instead of via 'id'
+compile_fail_error ATFFieldUnifyError.bs T0030
+compare_file ATFFieldUnifyError.bs.bsc-out
+compile_fail_error ATFFieldUnifyHKError.bs T0030
+compare_file ATFFieldUnifyHKError.bs.bsc-out
 compile_fail_error ATFAmbig.bs T0079
 compare_file ATFAmbig.bs.bsc-out
 compile_fail_error ATFNameClashTwoClasses.bs T0011