diff --git a/src/Init/Lean/Meta/InferType.lean b/src/Init/Lean/Meta/InferType.lean
index a52932ec4d..00d1147c4a 100644
--- a/src/Init/Lean/Meta/InferType.lean
+++ b/src/Init/Lean/Meta/InferType.lean
@@ -327,5 +327,22 @@ match r with
   | Expr.sort _ _ => pure true
   | _             => pure false
 
+partial def isTypeFormerAux : Expr → MetaM Bool
+| type => do
+  type ← whnfD type;
+  match type with
+  | Expr.sort _ _ => pure true
+  | Expr.forallE n d b c =>
+    withLocalDecl n d c.binderInfo $ fun fvar =>
+    isTypeFormerAux (b.instantiate1 fvar)
+  | _ => pure false
+
+/--
+  Return true iff `e : Sort _` or `e : (forall As, Sort _)`.
+  Remark: it subsumes `isType` -/
+def isTypeFormer (e : Expr) : MetaM Bool := do
+type ← inferType e;
+isTypeFormerAux type
+
 end Meta
 end Lean