feat: reject partial when if constant is not a function

fixes #697

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))

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

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 ()

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

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
 

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'