diff --git a/src/compiler/simp_pr1_rec.cpp b/src/compiler/simp_pr1_rec.cpp
index e17c4f007c..7d367e8616 100644
--- a/src/compiler/simp_pr1_rec.cpp
+++ b/src/compiler/simp_pr1_rec.cpp
@@ -117,7 +117,7 @@ class simp_pr1_rec_fn : public compiler_step_visitor {
             // Step 1.
             for (unsigned k = 0; k < minor_ctx.size(); k++) {
                 if (minor_is_rec_arg[k]) {
-                    expr type = ctx().whnf(minor_ctx[k]);
+                    expr type = ctx().whnf(ctx().infer(minor_ctx[k]));
                     buffer<expr> type_args;
                     expr type_fn = get_app_args(type, type_args);
                     if (!is_constant(type_fn) || const_name(type_fn) != get_prod_name() || type_args.size() != 2)