diff --git a/fco2/GenerateC.hs b/fco2/GenerateC.hs
index 1335de2..f8d770f 100644
--- a/fco2/GenerateC.hs
+++ b/fco2/GenerateC.hs
@@ -896,7 +896,7 @@ introduceSpec (A.Specification _ n (A.Proc _ fs p))
           tell ["}\n"]
 introduceSpec (A.Specification _ n (A.Retypes _ am t v))
     =  do origT <- typeOfVariable v
-          let (rhs, rhsSizes) = abbrevVariable am origT v
+          let (rhs, rhsSizes) = abbrevVariable A.Abbrev origT v
           genDecl am t n
           tell [" = ("]
           genDeclType am t
diff --git a/fco2/SimplifyExprs.hs b/fco2/SimplifyExprs.hs
index 5b56fd5..89814ae 100644
--- a/fco2/SimplifyExprs.hs
+++ b/fco2/SimplifyExprs.hs
@@ -105,7 +105,8 @@ pullUp = doGeneric `extM` doStructured `extM` doProcess `extM` doSpecification `
               popPullContext
               return p''
 
-    -- | *Don't* pull anything that's already an abbreviation.
+    -- | *Don't* pull anything that's already an abbreviation -- but do convert
+    -- RetypesExpr into Retypes (of a variable).
     doSpecification :: A.Specification -> PassM A.Specification
     doSpecification (A.Specification m n (A.Is m' am t v))
         =  do v' <- doGeneric v    -- note doGeneric rather than pullUp
@@ -113,6 +114,12 @@ pullUp = doGeneric `extM` doStructured `extM` doProcess `extM` doSpecification `
     doSpecification (A.Specification m n (A.IsExpr m' am t e))
         =  do e' <- doGeneric e    -- note doGeneric rather than pullUp
               return $ A.Specification m n (A.IsExpr m' am t e')
+    doSpecification (A.Specification m n (A.RetypesExpr m' am toT e))
+        =  do e' <- doExpression e
+              fromT <- typeOfExpression e'
+              spec@(A.Specification _ n' _) <- makeNonceIsExpr "retypes_expr" m' fromT e'
+              addPulled $ A.Spec m' spec
+              return $ A.Specification m n (A.Retypes m' am toT (A.Variable m' n'))
     doSpecification s = doGeneric s
 
     -- | Pull array expressions that aren't already non-subscripted variables.
diff --git a/fco2/TODO b/fco2/TODO
index d13abd4..9bef7ad 100644
--- a/fco2/TODO
+++ b/fco2/TODO
@@ -71,6 +71,8 @@ time.
 
 Real-to-integer conversions don't work correctly.
 
+Slice checks should not be generated if the slice is known to be safe.
+
 ## Long-term
 
 If we have constant folding, we're three-quarters of the way towards having an