From 8735820b496b23e857513a35d4997495a37cdc9d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 16 Oct 2020 07:58:47 -0700
Subject: [PATCH] fix: anonymous constructor too restrictive

We should support (recursive) inductive datatypes that have only one
constructor. We use this feature in the current `src/Lean` code base.
---
 src/Lean/Elab/BuiltinNotation.lean | 15 ++++++++-------
 tests/lean/run/anonymousCtor.lean  |  7 +++++++
 2 files changed, 15 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/run/anonymousCtor.lean

diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 9649752ced..98d43bcbd1 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -36,14 +36,15 @@ fun stx expectedType? => match_syntax stx with
   tryPostponeIfNoneOrMVar expectedType?
   match expectedType? with
   | some expectedType =>
-    let expectedType ← instantiateMVars expectedType
-    let expectedType := expectedType.consumeMData
     let expectedType ← whnf expectedType
-    matchConstStruct expectedType.getAppFn
-      (fun _ => throwError! "invalid constructor ⟨...⟩, expected type must be a structure {indentExpr expectedType}")
-      (fun val _ ctor => do
-        let newStx ← `($(mkCIdentFrom stx ctor.name) $(args.getSepElems)*)
-        withMacroExpansion stx newStx $ elabTerm newStx expectedType?)
+    matchConstInduct expectedType.getAppFn
+      (fun _ => throwError! "invalid constructor ⟨...⟩, expected type must be an inductive type {indentExpr expectedType}")
+      (fun ival us => do
+        match ival.ctors with
+        | [ctor] =>
+          let newStx ← `($(mkCIdentFrom stx ctor) $(args.getSepElems)*)
+          withMacroExpansion stx newStx $ elabTerm newStx expectedType?
+        | _ => throwError! "invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor {indentExpr expectedType}")
   | none => throwError "invalid constructor ⟨...⟩, expected type must be known"
 | _ => throwUnsupportedSyntax
 
diff --git a/tests/lean/run/anonymousCtor.lean b/tests/lean/run/anonymousCtor.lean
new file mode 100644
index 0000000000..d9f8427c86
--- /dev/null
+++ b/tests/lean/run/anonymousCtor.lean
@@ -0,0 +1,7 @@
+#lang lean4
+
+inductive S
+| mk : List S → String → S
+
+def f (s : String) : S :=
+⟨[], s⟩