Index: src/ResolvExpr/CandidateFinder.cpp
===================================================================
--- src/ResolvExpr/CandidateFinder.cpp	(revision fc134a48a40512fa2957765975077ee1bb642ba2)
+++ src/ResolvExpr/CandidateFinder.cpp	(revision 9e23b446e321a87bbf5f2439c8d555a808d5e53c)
@@ -1265,4 +1265,12 @@
 					newExpr, copy( tenv ), ast::OpenVarSet{}, ast::AssertionSet{}, Cost::zero,
 					cost );
+
+				if (newCand->expr->env) {
+					newCand->env.add(*newCand->expr->env);
+					auto mutExpr = newCand->expr.get_and_mutate();
+					mutExpr->env  = nullptr;
+					newCand->expr = mutExpr;
+				}
+
 				PRINT(
 					std::cerr << "decl is ";
Index: src/ResolvExpr/Resolver.cc
===================================================================
--- src/ResolvExpr/Resolver.cc	(revision fc134a48a40512fa2957765975077ee1bb642ba2)
+++ src/ResolvExpr/Resolver.cc	(revision 9e23b446e321a87bbf5f2439c8d555a808d5e53c)
@@ -1555,7 +1555,10 @@
 		if ( type->dimension ) {
 			ast::ptr< ast::Type > sizeType = context.global.sizeType;
+			ast::ptr< ast::Expr > dimension = findSingleExpression( type->dimension, sizeType, context );
+			assertf(dimension->env->empty(), "array dimension expr has nonempty env");
+			dimension.get_and_mutate()->env = nullptr;
 			ast::mutate_field(
 				type, &PtrType::dimension,
-				findSingleExpression( type->dimension, sizeType, context ) );
+				dimension);
 		}
 		return type;
@@ -2008,4 +2011,7 @@
 				tmp->accept( *visitor );
 			}
+			else if (expr->env && expr->env->empty()) {
+				expr = ast::mutate_field(expr.get(), &ast::Expr::env, nullptr);
+			}
 		}
 	}