diff --git a/compiler/supercompile/Supercompile/Drive/MSG.hs b/compiler/supercompile/Supercompile/Drive/MSG.hs
index 6935b3404d5df6fe5926bb6303e1c1adb2c0f082..ee6adad551da644a25cbf1c84a1eb7ba191cf176 100644
--- a/compiler/supercompile/Supercompile/Drive/MSG.hs
+++ b/compiler/supercompile/Supercompile/Drive/MSG.hs
@@ -34,6 +34,7 @@ import Kind
 --import TysWiredIn (pairTyCon {- , tupleCon -})
 import TysPrim    (funTyCon)
 import TypeRep    (Type(..))
+import Type       (coreView)
 import TrieMap    (TrieMap(..), CoercionMap, TypeMap)
 import Rules      (mkSpecInfo, roughTopNames)
 import Unique     (mkUniqueGrimily)
@@ -879,8 +880,16 @@ msgType rn2 ty_l ty_r = case checkEqual (isKindTy ty_l) (isKindTy ty_r) of
 msgType' :: Bool -> RnEnv2 -> Type -> Type -> MSG Type
 msgType' _         rn2 (TyVarTy x_l)         (TyVarTy x_r)         = liftM TyVarTy $ msgVar rn2 x_l x_r -- NB: if this fails, one of the two sides is unfloatable, so don't try to generalise
 msgType' are_kinds rn2 (AppTy ty1_l ty2_l)   (AppTy ty1_r ty2_r)   = liftM2 mkAppTy (msgType' are_kinds rn2 ty1_l ty1_r) (msgType rn2 ty2_l ty2_r) -- NB: arguments not necessarily at same level, but type constructor must be
-msgType' _         _   (TyConApp tc_l [])    (TyConApp tc_r [])    | tc_l == tc_r = return (TyConApp tc_r [])
-msgType' are_kinds rn2 (TyConApp tc_l tys_l) (TyConApp tc_r tys_r) | not (null tys_l) || not (null tys_r) = msgType' are_kinds rn2 (foldl AppTy (TyConApp tc_l []) tys_l) (foldl AppTy (TyConApp tc_r []) tys_r)
+msgType' are_kinds rn2 (TyConApp tc_l tys_l) (TyConApp tc_r tys_r)
+  -- Special case so we can avoid splitting most type synonyms, also prevents loops in the case where we have (TyConApp tc []) on each side so breaking apart TyConApp would be a NOP
+  | tc_l == tc_r && length tys_l == length tys_r = liftM (TyConApp tc_r) (zipWithEqualM (msgType rn2) tys_l tys_r)
+msgType' are_kinds rn2 ty_l ty_r
+  -- MUST look through type synonyms because otherwise we might succeed in generalising when given (ShowsS `msgType` (a -> b)), which would be a disaster
+  | Just ty_l' <- coreView ty_l                  = msgType' are_kinds rn2 ty_l' ty_r
+  | Just ty_r' <- coreView ty_r                  = msgType' are_kinds rn2 ty_l ty_r'
+msgType' are_kinds rn2 (TyConApp tc_l tys_l) (TyConApp tc_r tys_r)
+  -- Must look through synonyms *before* we break apart TyConApps since coreView won't work any other way
+  | not (null tys_l) || not (null tys_r)         = msgType' are_kinds rn2 (foldl AppTy (TyConApp tc_l []) tys_l) (foldl AppTy (TyConApp tc_r []) tys_r)
 msgType' are_kinds rn2 (FunTy ty1_l ty2_l)   (FunTy ty1_r ty2_r)   = msgType' are_kinds rn2 ((TyConApp funTyCon [] `AppTy` ty1_l) `AppTy` ty2_l) ((TyConApp funTyCon [] `AppTy` ty1_r) `AppTy` ty2_r)
 msgType' are_kinds rn2 (ForAllTy a_l ty_l)   (ForAllTy a_r ty_r)   = msgTyVarBndr ForAllTy rn2 a_l a_r $ \rn2 -> msgType' are_kinds rn2 ty_l ty_r
 msgType' _         _   (LitTy l_l)           (LitTy l_r)           | l_l == l_r = return (LitTy l_r)
diff --git a/compiler/supercompile/Supercompile/Drive/Process.hs b/compiler/supercompile/Supercompile/Drive/Process.hs
index c7727b022e0797a89fbdfc914225f6931aaeb95d..e04073fa0e2bd05154b3ac0840fb28fe8aad23ea 100644
--- a/compiler/supercompile/Supercompile/Drive/Process.hs
+++ b/compiler/supercompile/Supercompile/Drive/Process.hs
@@ -889,7 +889,7 @@ reduceWithStats :: State -> (SCStats, State)
 reduceWithStats state = case reduce' state of (_, stats, state') -> (stats, state')
 
 reduce' :: State -> (Bool, SCStats, State)
-reduce' orig_state = go 0 False init_hist orig_state
+reduce' orig_state = go rEDUCE_STOP_LIMIT False init_hist orig_state
   where
     init_hist = mkLinearHistory rEDUCE_WQO
 
@@ -903,7 +903,7 @@ reduce' orig_state = go 0 False init_hist orig_state
            -> case terminate hist (gc state) of
                 Continue hist' -> go n True hist' state'
                 Stop old_state
-                  | n > 0      -> go (n - 1) True init_hist state' -- FIXME: huge hack
+                  | n > 1      -> go (n - 1) True init_hist state' -- FIXME: huge hack
                   | otherwise  -> pprTrace "reduce-stop" {--} (pPrintFullState quietStatePrettiness old_state $$ pPrintFullState quietStatePrettiness state) {--} -- empty
                                   -- let smmrse s@(_, _, _, qa) = pPrintFullState s $$ case annee qa of Question _ -> text "Question"; Answer _ -> text "Answer" in
                                   -- pprPreview2 "reduce-stop" (smmrse old_state) (smmrse state) $
diff --git a/compiler/supercompile/Supercompile/Drive/Process3.hs b/compiler/supercompile/Supercompile/Drive/Process3.hs
index 7ceef75a0f58fe2c59d06d01c4c7a63311910a2c..c6cdd140c4ab0e42a699cdc31beb743228dc2b15 100644
--- a/compiler/supercompile/Supercompile/Drive/Process3.hs
+++ b/compiler/supercompile/Supercompile/Drive/Process3.hs
@@ -291,8 +291,9 @@ sc' mb_h state = {- pprTrace "sc'" (trce1 state) $ -} {-# SCC "sc'" #-} case mb_
                terminateM h state rb
                  (speculateM (reduce state) $ \state -> my_split state)
                  (\shallow_h shallow_state shallow_rb -> trce shallow_h shallow_state $ do
-                                                           let (mb_shallow_gen, mb_gen) = zipPair mplus mplus (tryMSG sc shallow_state state)
-                                                                                                              (tryTaG sc shallow_state state)
+                                                           let (mb_shallow_gen, mb_gen) | not gENERALISATION = (Nothing, Nothing)
+                                                                                        | otherwise = zipPair mplus mplus (tryMSG sc shallow_state state)
+                                                                                                                          (tryTaG sc shallow_state state)
                                                            case mb_shallow_gen of
                                                              Just shallow_gen | sC_ROLLBACK           -> trace "sc-stop(rb,gen)"   $ shallow_rb shallow_gen
                                                              Nothing | sC_ROLLBACK, Nothing <- mb_gen -> trace "sc-stop(rb,split)" $ shallow_rb (split sc shallow_state)
@@ -323,7 +324,9 @@ tryTaG opt shallow_state state = bothWays (\_ -> generaliseSplit opt gen) shallo
   where gen = mK_GENERALISER shallow_state state
 
 -- NB: this cannot return (Just, Nothing)
-tryMSG opt shallow_state state = case msgMaybe mode shallow_state state of
+tryMSG opt shallow_state state
+  | not mSG_GENERALISATION = (Nothing, Nothing)
+  | otherwise = case msgMaybe mode shallow_state state of
     -- If we fail this way round, we should certainly fail the other way round too
     Nothing -> (Nothing, Nothing)
     Just msg_result@(Pair l r, _)
@@ -620,7 +623,9 @@ memo opt init_state = {-# SCC "memo'" #-} memo_opt init_state
                         -- NB: don't record a promise for type generalisation! This is OK for termination because all type gens
                         -- are non-trivial so we will eventually have to stop genning. Furthermore, it means that we can't end
                         -- up with a FIXME: continue
-                       RightGivesTypeGen rn_l s rn_r -> trace "typegen" $ (True, do { (deeds, e') <- memo_opt s
+                       RightGivesTypeGen rn_l s rn_r -> -- pprTrace "typegen" (pPrintFullState fullStatePrettiness state $$ pPrintFullState fullStatePrettiness s) $
+                                                        trace "typegen" $
+                                                                          (True, do { (deeds, e') <- memo_opt s
                                                                                     ; (_, e'_r) <- renameSCResult (case s of (_, Heap _ ids, _, _) -> ids) (rn_r, e')
                                                                                       -- OH MY GOD:
                                                                                       --  - If we do memo-rollback or sc-rollback then we CAN'T overwrite old fulfilments
@@ -662,9 +667,13 @@ memo opt init_state = {-# SCC "memo'" #-} memo_opt init_state
                         (promise -> Maybe Var)
                      -> [(promise, MSGMatchResult)]
                      -> [(Bool, (promise, MSGMatchResult))]
-            sortBest dumped ress = filter (\(_, (p, _)) -> case dumped p of Just fun -> pprTraceSC "tieback-to-dumped" (ppr fun) False; Nothing -> True) $
-                                          map ((,) True) best_ress ++ map ((,) False) (sortBy ((\x y -> if x `moreSpecific` y then LT else GT) `on` snd) other_ress)
-              where -- Stop early upon exact match (as an optimisation)
+            sortBest dumped ress = filter suitable $ map ((,) True) best_ress ++ map ((,) False) (sortBy ((\x y -> if x `moreSpecific` y then LT else GT) `on` snd) other_ress)
+              where suitable (_, (p, mr))
+                      | Just fun <- dumped p                     = pprTraceSC "tieback-to-dumped" (ppr fun) False
+                      | not tYPE_GEN, RightGivesTypeGen {} <- mr = False
+                      | otherwise                                = True
+
+                    -- Stop early upon exact match (as an optimisation)
                     (best_ress, other_ress) = partition (mostSpecific . snd) ress
 
                     mostSpecific :: MSGMatchResult -> Bool
diff --git a/compiler/supercompile/Supercompile/Drive/Split.hs b/compiler/supercompile/Supercompile/Drive/Split.hs
index 933cf393e02839f42d7204e19a01d0641edb38c6..fd35ef542d679e9f938162407b3207475fdcd0bd 100644
--- a/compiler/supercompile/Supercompile/Drive/Split.hs
+++ b/compiler/supercompile/Supercompile/Drive/Split.hs
@@ -201,7 +201,7 @@ generalise :: MonadStatics m
 generalise gen (deeds, Heap h ids, k, qa) = do
     let named_k = nameStack k
     
-    (gen_kfs, gen_xs') <- case gENERALISATION of
+    (gen_kfs, gen_xs') <- case sPLIT_GENERALISATION_TYPE of
         NoGeneralisation -> Nothing
         AllEligible -> guard (not (IS.null gen_kfs) || not (isEmptyVarSet gen_xs'')) >> return (gen_kfs, gen_xs'')
           where gen_kfs = IS.fromList [i   | (i, kf) <- trainCars named_k, generaliseStackFrame gen kf]
diff --git a/compiler/supercompile/Supercompile/Drive/Split2.hs b/compiler/supercompile/Supercompile/Drive/Split2.hs
index e529f22baa8160c07422e1b95f3b25edab7a0728..92fc3774c8ac6b853985745f38b18c9012504fcb 100644
--- a/compiler/supercompile/Supercompile/Drive/Split2.hs
+++ b/compiler/supercompile/Supercompile/Drive/Split2.hs
@@ -247,7 +247,7 @@ instanceSplit :: (Applicative m, Monad m)
 instanceSplit opt (deeds, heap, k, e) = recurse opt $ push (S.singleton FocusContext) (deeds, heap, k, OpaqueFocus e)
 
 applyGeneraliser :: Generaliser -> State -> Maybe (S.Set Context)
-applyGeneraliser gen (_deeds, Heap h _, k, qa) = fmap (\(gen_kfs, gen_xs) -> S.fromList $ map StackContext (IS.elems gen_kfs) ++ map HeapContext (varSetElems gen_xs)) $ case gENERALISATION of
+applyGeneraliser gen (_deeds, Heap h _, k, qa) = fmap (\(gen_kfs, gen_xs) -> S.fromList $ map StackContext (IS.elems gen_kfs) ++ map HeapContext (varSetElems gen_xs)) $ case sPLIT_GENERALISATION_TYPE of
     NoGeneralisation -> Nothing
     AllEligible -> guard (not (IS.null gen_kfs) || not (isEmptyVarSet gen_xs'')) >> return (gen_kfs, gen_xs'')
       where gen_kfs = IS.fromList [i   | (i, kf) <- named_k, generaliseStackFrame gen kf]
diff --git a/compiler/supercompile/Supercompile/Evaluator/Evaluate.hs b/compiler/supercompile/Supercompile/Evaluator/Evaluate.hs
index d3556bf02949a8c4a670da2db5df8fb9b99e2baf..2a833bbf107c6ce82f0e1a57da2b7f1e49e85601 100644
--- a/compiler/supercompile/Supercompile/Evaluator/Evaluate.hs
+++ b/compiler/supercompile/Supercompile/Evaluator/Evaluate.hs
@@ -560,7 +560,24 @@ shouldExposeUnfolding :: Id -> Either String Superinlinable
 shouldExposeUnfolding x = case inl_inline inl_prag of
     -- FIXME: God help my soul
     _ | Just mod <- nameModule_maybe (idName x)
-      , moduleName mod `elem` map mkModuleName ["Data.Complex", "GHC.List"]
+      , moduleName mod `elem` map mkModuleName [
+          "Data.Complex", "GHC.List",
+          "QSort", -- awards
+          "Checker", "Lisplikefns", "Rewritefns", "Rulebasetext", -- boyer2
+          "Auxil", "Interval", "Key", "Prog", -- cichelli
+          "MonadState", "MonadTrans", -- cryptarithm2
+          "StateMonad", -- cse
+          "Knowledge", "Result", "Search", "Table", "Match", -- expert
+          "Fourier", "Complex_Vectors", -- fft2
+          "RA", "RC", "RG", "RU", "Types", -- nucleic2
+          "ChessSetArray", "ChessSetList", "KnightHeuristic", "Queue", "Sort", -- knights
+          "Mandel", -- mandel
+          "Move", "Problem", "Solution", -- mate
+          "Board", "Game", "Prog", "Tree", "Wins", -- minimax
+          "CharSeq", "Pretty", -- pretty
+          "IntLib", "MyRandom", "Prime", -- primetest
+          "Digraph" -- scc
+        ]
       -> Right True
     -- These get wrappers generated for them: be very eager to inline the wrappers
       | isPrimOpId x || isDataConWorkId x
diff --git a/compiler/supercompile/Supercompile/GHC.hs b/compiler/supercompile/Supercompile/GHC.hs
index 0c0086459d4a7c3671ddc1279b9efeaea09338bb..63bc1dc3e59736631143f861b8bfa684be367194 100644
--- a/compiler/supercompile/Supercompile/GHC.hs
+++ b/compiler/supercompile/Supercompile/GHC.hs
@@ -55,7 +55,7 @@ desc = desc' . unI
 desc' :: S.TermF Identity -> Description
 desc' (S.Var x)            = Opaque (S.varString x)
 desc' (S.Value _)          = Opaque "value"
-desc' (S.TyApp e1 _)       = argOf (desc e1)
+desc' (S.TyApp e1 _)       = desc e1 -- NB: no argOf for type arguments because they don't get ANFed, so it's a bit redundant
 desc' (S.CoApp e1 _)       = argOf (desc e1)
 desc' (S.App e1 _)         = argOf (desc e1)
 desc' (S.PrimOp pop as es) = foldr (\() d -> argOf d) (Opaque (show pop)) (map (const ()) as ++ map (const ()) es)
diff --git a/compiler/supercompile/Supercompile/StaticFlags.hs b/compiler/supercompile/Supercompile/StaticFlags.hs
index d0256fabcc450f1577487a1219ffd82a8c1c2111..8ff8043a6f4725589e290601d7dc7c281aca0f57 100644
--- a/compiler/supercompile/Supercompile/StaticFlags.hs
+++ b/compiler/supercompile/Supercompile/StaticFlags.hs
@@ -56,6 +56,9 @@ dEPTH_LIIMT :: Maybe Int
 dEPTH_LIIMT = Just (lookup_def_int "-fsupercompiler-depth-limit" maxBound)
 --dEPTH_LIIMT = Just 10
 
+rEDUCE_STOP_LIMIT :: Int
+rEDUCE_STOP_LIMIT = lookup_def_int "-fsupercompiler-reduce-stop-limit" 1
+
 pOSITIVE_INFORMATION :: Bool
 pOSITIVE_INFORMATION = not $ lookUp $ fsLit "-fsupercompiler-no-positive-information"
 --pOSITIVE_INFORMATION = True
@@ -218,14 +221,20 @@ tAG_COLLECTION = parseEnum "-fsupercompiler-tag-collection" (TBT False) [("bags"
 
 data GeneralisationType = NoGeneralisation | AllEligible | DependencyOrder Bool | StackFirst
 
-gENERALISATION :: GeneralisationType
-gENERALISATION = parseEnum "-fsupercompiler-generalisation" StackFirst [("none", NoGeneralisation), ("all-eligible", AllEligible), ("first-reachable", DependencyOrder True), ("last-reachable", DependencyOrder False), ("stack-first", StackFirst)]
+sPLIT_GENERALISATION_TYPE :: GeneralisationType
+sPLIT_GENERALISATION_TYPE = parseEnum "-fsupercompiler-split-generalisation-type" StackFirst [("none", NoGeneralisation), ("all-eligible", AllEligible), ("first-reachable", DependencyOrder True), ("last-reachable", DependencyOrder False), ("stack-first", StackFirst)]
 
 oCCURRENCE_GENERALISATION :: Bool
 oCCURRENCE_GENERALISATION = not $ lookUp $ fsLit "-fsupercompiler-no-occurrence-generalisation"
 
+gENERALISATION :: Bool
+gENERALISATION = not $ lookUp $ fsLit "-fsupercompiler-no-generalisation"
+
+mSG_GENERALISATION :: Bool
+mSG_GENERALISATION = not $ lookUp $ fsLit "-fsupercompiler-no-msg-generalisation"
+
 tYPE_GEN :: Bool
-tYPE_GEN = True
+tYPE_GEN = not $ lookUp $ fsLit "-fsupercompiler-no-type-generalisation"
 
 eVALUATE_PRIMOPS :: Bool
 eVALUATE_PRIMOPS = not $ lookUp $ fsLit "-fsupercompiler-no-primops"