diff --git a/src/library/tactic/intros_tactic.cpp b/src/library/tactic/intros_tactic.cpp
index 325cfd588..49b676d0c 100644
--- a/src/library/tactic/intros_tactic.cpp
+++ b/src/library/tactic/intros_tactic.cpp
@@ -33,6 +33,7 @@ tactic intros_tactic(list<name> _ns, bool relax_main_opaque) {
                         expr new_t = tc->whnf(t).first;
                         if (!is_pi(new_t))
                             break;
+                        t = new_t;
                     }
                 }
                 name new_name;
diff --git a/tests/lean/run/366.lean b/tests/lean/run/366.lean
new file mode 100644
index 000000000..897344e54
--- /dev/null
+++ b/tests/lean/run/366.lean
@@ -0,0 +1,8 @@
+import hott.path
+open path
+definition foo (A : Type) : Type := Π (a : A), a ≈ a
+definition thm : Π (A : Type), foo A :=
+begin
+  intros,
+  apply idp
+end