From 3fed9c9df7d391fe79bedac03491981f60469fd1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 28 Sep 2021 21:01:37 -0700
Subject: [PATCH] feat: reject `partial` when if constant is not a function

fixes #697
---
 src/Lean/Elab/PreDefinition/Main.lean     |  3 ++
 src/Lean/Meta/Tactic/Simp/Main.lean       |  9 +++---
 tests/lean/697.lean                       | 38 +++++++++++++++++++++++
 tests/lean/697.lean.expected.out          |  2 ++
 tests/lean/sanitychecks.lean              |  2 ++
 tests/lean/sanitychecks.lean.expected.out |  8 +++--
 6 files changed, 55 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/697.lean
 create mode 100644 tests/lean/697.lean.expected.out

diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index 059503f0e9..b707ce1873 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -74,6 +74,9 @@ def addPreDefinitions (preDefs : Array PreDefinition) (terminationBy? : Option S
     else if preDefs.any (·.modifiers.isUnsafe) then
       addAndCompileUnsafe preDefs
     else if preDefs.any (·.modifiers.isPartial) then
+      for preDef in preDefs do
+        if preDef.modifiers.isPartial && !(← whnfD preDef.type).isForall then
+          withRef preDef.ref <| throwError "invalid use of 'partial', '{preDef.declName}' is not a function{indentExpr preDef.type}"
       addAndCompilePartial preDefs
     else if let some wfStx := terminationBy.find? (preDefs.map (·.declName)) then
       terminationBy := terminationBy.erase (preDefs.map (·.declName))
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 7f1b7bd3be..16b106701b 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -399,7 +399,7 @@ mutual
       return none
     else
       withReader (fun ctx => { ctx with dischargeDepth := ctx.dischargeDepth + 1 }) do
-        let r ← simp e methods
+        let r ← simp e { pre := pre, post := post, discharge? := discharge? }
         if r.expr.isConstOf ``True then
           try
             return some (← mkOfEqTrue (← r.getProof))
@@ -413,10 +413,11 @@ mutual
 
   partial def post (e : Expr) : SimpM Step :=
     postDefault e discharge?
-
-  partial def methods : Methods :=
-    { pre := pre, post := post, discharge? := discharge? }
 end
+
+def methods : Methods :=
+  { pre := pre, post := post, discharge? := discharge? }
+
 end DefaultMethods
 
 end Simp
diff --git a/tests/lean/697.lean b/tests/lean/697.lean
new file mode 100644
index 0000000000..e9d5927b52
--- /dev/null
+++ b/tests/lean/697.lean
@@ -0,0 +1,38 @@
+inductive Maybe (a : Type) : Type where
+| ok: a -> Maybe a
+| err: Maybe a
+
+structure P (a: Type) where
+   runP: String -> Maybe (String × a)
+
+def ppure {a: Type} (v: a): P a := { runP :=  λ s => Maybe.ok (s, v) }
+
+def pbind {a b: Type} (pa: P a) (a2pb : a -> P b): P b :=
+   { runP := λs => match pa.runP s with
+            | Maybe.ok (s', a) => (a2pb a).runP  s'
+            | Maybe.err => Maybe.err
+   }
+
+instance : Monad P := { pure := ppure, bind := pbind }
+
+def pfail : P a := { runP := λ _  => Maybe.err }
+
+instance : Inhabited (P a) where default := pfail
+
+
+mutual
+partial def pregion : P Unit :=  do
+  pblock
+
+partial def pop : P Unit := do
+  pregion
+
+partial def pblock : P Unit := do
+   pop
+end
+
+-- partial def foo : Unit :=
+--  foo
+
+def main: IO Unit := do
+  return ()
diff --git a/tests/lean/697.lean.expected.out b/tests/lean/697.lean.expected.out
new file mode 100644
index 0000000000..2b6c3aabe6
--- /dev/null
+++ b/tests/lean/697.lean.expected.out
@@ -0,0 +1,2 @@
+697.lean:24:12-24:19: error: invalid use of 'partial', 'pregion' is not a function
+  P Unit
diff --git a/tests/lean/sanitychecks.lean b/tests/lean/sanitychecks.lean
index 8919ea76c5..cedde21e58 100644
--- a/tests/lean/sanitychecks.lean
+++ b/tests/lean/sanitychecks.lean
@@ -17,6 +17,8 @@ unsafe def unsound2 : False := unsound  -- OK
 
 partial def unsound3 : False := unsound3  -- Error
 
+partial def unsound4 (x : Unit) : False := unsound4 ()  -- Error
+
 partial def badcast1 (x : Nat) : Bool :=
   unsafeCast x -- Error: partial cannot use unsafe constant
 
diff --git a/tests/lean/sanitychecks.lean.expected.out b/tests/lean/sanitychecks.lean.expected.out
index 858a9b738e..dd1a753ec4 100644
--- a/tests/lean/sanitychecks.lean.expected.out
+++ b/tests/lean/sanitychecks.lean.expected.out
@@ -8,6 +8,8 @@ sanitychecks.lean:4:8-5:9: error: 'partial' theorems are not allowed, 'partial'
 sanitychecks.lean:7:7-8:9: error: 'unsafe' theorems are not allowed
 sanitychecks.lean:10:0-10:24: error: failed to synthesize instance
   Inhabited False
-sanitychecks.lean:18:0-18:40: error: failed to compile partial definition 'unsound3', failed to show that type is inhabited
-sanitychecks.lean:20:12-20:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'
-sanitychecks.lean:23:12-23:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'
+sanitychecks.lean:18:12-18:20: error: invalid use of 'partial', 'unsound3' is not a function
+  False
+sanitychecks.lean:20:0-20:54: error: failed to compile partial definition 'unsound4', failed to show that type is inhabited
+sanitychecks.lean:22:12-22:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'
+sanitychecks.lean:25:12-25:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'