From c5cd5f2e5b7de8f9eddaa574d7ebfaaf1c9d099c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 1 Sep 2020 17:20:06 -0700
Subject: [PATCH] feat: check kinds

---
 src/Lean/Elab/MutualDef.lean            |  8 ++++++++
 tests/lean/mutualdef1.lean              | 24 ++++++++++++++++++++++++
 tests/lean/mutualdef1.lean.expected.out |  2 ++
 3 files changed, 34 insertions(+)

diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 99c4a0cf5d..2ca186011d 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -34,6 +34,13 @@ unless (m₁.isPartial == m₂.isPartial) $
   throwError "cannot mix partial and non-partial definitions";
 pure ()
 
+def checkKinds (k₁ k₂ : DefKind) : TermElabM Unit := do
+unless (k₁.isExample == k₂.isExample) $
+  throwError "cannot mix examples and definitions"; -- Reason: we should discard examples
+unless (k₁.isTheorem == k₂.isTheorem) $
+  throwError "cannot mix theorems and definitions"; -- Reason: we will eventually elaborate theorems in `Task`s.
+pure ()
+
 def elabHeaders (views : Array DefView) : TermElabM (Array DefViewElabHeader) :=
 views.foldlM
   (fun (headers : Array DefViewElabHeader) (view : DefView) => withRef view.ref do
@@ -60,6 +67,7 @@ views.foldlM
             unless (levelNames == firstHeader.levelNames) $
               throwError "universe parameters mismatch in mutual definition";
             checkModifiers view.modifiers firstHeader.modifiers;
+            checkKinds view.kind firstHeader.kind;
             forallTelescopeCompatible type firstHeader.type xs.size fun _ _ _ => pure ())
           (fun ex => match ex with
             | Exception.error ref msg => throw (Exception.error ref ("invalid mutually recursive definitions, " ++ msg))
diff --git a/tests/lean/mutualdef1.lean b/tests/lean/mutualdef1.lean
index 33d0ff9f6c..d9b18c52f4 100644
--- a/tests/lean/mutualdef1.lean
+++ b/tests/lean/mutualdef1.lean
@@ -61,3 +61,27 @@ def g (x : Nat) : Nat → Nat -- universe parameter mistmatch
 | x+1 => f x
 
 end
+
+
+mutual
+
+def f (x : Nat) : Nat → Nat
+| 0   => 1
+| x+1 => g x
+
+theorem g (x : Nat) : Nat → Nat -- cannot mix theorems and definitions
+| 0   => 2
+| x+1 => f x
+
+end
+
+mutual
+
+def f  : Nat → Nat
+| 0   => 1
+| x+1 => g x
+
+example : Nat := -- cannot mix examples and definitions
+g 10
+
+end
diff --git a/tests/lean/mutualdef1.lean.expected.out b/tests/lean/mutualdef1.lean.expected.out
index 5651630087..c777109012 100644
--- a/tests/lean/mutualdef1.lean.expected.out
+++ b/tests/lean/mutualdef1.lean.expected.out
@@ -6,3 +6,5 @@ mutualdef1.lean:22:0: error: invalid mutually recursive definitions, parameter n
 mutualdef1.lean:35:0: error: invalid mutually recursive definitions, binder annotation mismatch at parameter 'x'
 mutualdef1.lean:47:0: error: invalid mutually recursive definitions, number of parameters mismatch
 mutualdef1.lean:59:0: error: invalid mutually recursive definitions, universe parameters mismatch in mutual definition
+mutualdef1.lean:72:0: error: invalid mutually recursive definitions, cannot mix theorems and definitions
+mutualdef1.lean:84:0: error: invalid mutually recursive definitions, cannot mix examples and definitions