diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index b2f9543b2d..c5d2fc0f79 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -403,26 +403,45 @@ def withCtorRef (views : Array InductiveView) (ctorName : Name) (k : TermElabM 
   k
 
 private def checkResultingUniverses (views : Array InductiveView) (numParams : Nat) (indTypes : List InductiveType) : TermElabM Unit := do
-  let u ← instantiateLevelMVars (← getResultingUniverse indTypes)
+  let u := (← instantiateLevelMVars (← getResultingUniverse indTypes)).normalize
   checkResultingUniverse u
   unless u.isZero do
     indTypes.forM fun indType => indType.ctors.forM fun ctor =>
-      forallTelescopeReducing ctor.type fun ctorArgs type =>
+      forallTelescopeReducing ctor.type fun ctorArgs type => do
         for ctorArg in ctorArgs[numParams:] do
           let type ← inferType ctorArg
-          let v ← instantiateLevelMVars (← getLevel type)
-          if v.hasMVar then
-            -- TODO
-            trace[Meta.debug] "checkCtorArgLevel, {v} <= {u}"
-          else unless u.geq v do
-            let mut msg := m!"invalid universe level in constructor '{ctor.name}', parameter"
-            let localDecl ← getFVarLocalDecl ctorArg
-            unless localDecl.userName.hasMacroScopes do
-              msg := msg ++ m!" '{ctorArg}'"
-            msg := msg ++ m!" has type{indentExpr type}"
-            msg := msg ++ m!"\nat universe level{indentD v}"
-            msg := msg ++ m!"\nit must be smaller than or equal to the inductive datatype universe level{indentD u}"
-            withCtorRef views ctor.name <| throwError msg
+          let v := (← instantiateLevelMVars (← getLevel type)).normalize
+          let rec check (v' : Level) (u' : Level) : TermElabM Unit :=
+            match v', u' with
+            | .succ v' _, .succ u' _ => check v' u'
+            | .mvar id _, .param ..  =>
+              /- Special case:
+                 The constructor parameter `v` is at unverse level `?v+k` and
+                 the resulting inductive universe level is `u'+k`, where `u'` is a parameter (or zero).
+                 Thus, `?v := u'` is the only choice for satisfying the universe contraint `?v+k <= u'+k`.
+                 Note that, we still generate an error for cases where there is more than one of satisfying the constraint.
+                 Examples:
+                 -----------------------------------------------------------
+                 | ctor universe level | inductive datatype universe level |
+                 -----------------------------------------------------------
+                 |   ?v                | max u w                           |
+                 -----------------------------------------------------------
+                 |   ?v                | u + 1                             |
+                 -----------------------------------------------------------
+              -/
+              assignLevelMVar id u'
+            | .mvar id _, .zero _    => assignLevelMVar id u' -- TODO: merge with previous case
+            | _, _ =>
+              unless u.geq v do
+                let mut msg := m!"invalid universe level in constructor '{ctor.name}', parameter"
+                let localDecl ← getFVarLocalDecl ctorArg
+                unless localDecl.userName.hasMacroScopes do
+                  msg := msg ++ m!" '{ctorArg}'"
+                msg := msg ++ m!" has type{indentExpr type}"
+                msg := msg ++ m!"\nat universe level{indentD v}"
+                msg := msg ++ m!"\nit must be smaller than or equal to the inductive datatype universe level{indentD u}"
+                withCtorRef views ctor.name <| throwError msg
+          check v u
 
 private def collectUsed (indTypes : List InductiveType) : StateRefT CollectFVars.State MetaM Unit := do
   indTypes.forM fun indType => do
diff --git a/tests/lean/ctorUnivTooBig.lean b/tests/lean/ctorUnivTooBig.lean
index 3be8e882c1..4e143ff0ba 100644
--- a/tests/lean/ctorUnivTooBig.lean
+++ b/tests/lean/ctorUnivTooBig.lean
@@ -1,17 +1,47 @@
 inductive Bla : Type u where
   | nil  : Bla
-  | cons : (α : Type u) → (a : α) → Bla → Bla
+  | cons : (α : Type u) → (a : α) → Bla → Bla -- Error
 
 inductive Foo : Type where
   | leaf
-  | mk (α : Type) (a : α)
+  | mk (α : Type) (a : α) -- Error
   | mk₂
 
 inductive Foo' : Type u where
   | leaf
-  | mk : Sort (max u v) → a → Foo'
+  | mk : Sort (max u v) → a → Foo' -- Error
   | mk₂
 
 inductive Boo : Type u where
   | nil  : Boo
   | cons : (α : Sort u) → (a : α) → Boo → Boo
+
+namespace Ex1
+inductive Member : α → List α → Type u
+  | head : Member a (a::as)
+  | tail : Member a bs → Member a (b::bs)
+end Ex1
+
+namespace Ex2
+inductive Member : α → List α → Type
+  | head : Member a (a::as)
+  | tail : Member a bs → Member a (b::bs)
+end Ex2
+
+namespace Ex3
+inductive Member : α → List α → Type (max u v)
+  | head : Member a (a::as) -- Error
+  | tail : Member a bs → Member a (b::bs)
+end Ex3
+
+namespace Ex4
+inductive Member : α → List α → Type (u+1)
+  | head : Member a (a::as) -- Error
+  | tail : Member a bs → Member a (b::bs)
+end Ex4
+
+namespace Ex5
+inductive Member : α → List α → Type 1
+  | head : Member a (a::as) -- Error
+  | tail : Member a bs → Member a (b::bs)
+end Ex5
diff --git a/tests/lean/ctorUnivTooBig.lean.expected.out b/tests/lean/ctorUnivTooBig.lean.expected.out
index 7d0b120183..3d0e3c5884 100644
--- a/tests/lean/ctorUnivTooBig.lean.expected.out
+++ b/tests/lean/ctorUnivTooBig.lean.expected.out
@@ -13,6 +13,24 @@ it must be smaller than or equal to the inductive datatype universe level
 ctorUnivTooBig.lean:12:2-12:34: error: invalid universe level in constructor 'Foo'.mk', parameter has type
   Sort (max u v)
 at universe level
-  (max u v)+1
+  max (u+1) (v+1)
 it must be smaller than or equal to the inductive datatype universe level
   u+1
+ctorUnivTooBig.lean:33:2-33:27: error: invalid universe level in constructor 'Ex3.Member.head', parameter 'a' has type
+  x✝
+at universe level
+  ?u+1
+it must be smaller than or equal to the inductive datatype universe level
+  max (u+1) (v+1)
+ctorUnivTooBig.lean:39:2-39:27: error: invalid universe level in constructor 'Ex4.Member.head', parameter 'a' has type
+  x✝
+at universe level
+  ?u+1
+it must be smaller than or equal to the inductive datatype universe level
+  u+2
+ctorUnivTooBig.lean:45:2-45:27: error: invalid universe level in constructor 'Ex5.Member.head', parameter 'a' has type
+  x✝
+at universe level
+  ?u+1
+it must be smaller than or equal to the inductive datatype universe level
+  2