fix: issues found in review

Qpf/Macro/Data.lean

@@ -541,7 +541,8 @@ def elabData : CommandElab := fun stx => do
   let modifiers ← elabModifiers stx[0]
   let decl := stx[1]
   /- Transforms binders into simple lambda types. -/
-  let view ← dataSyntaxToView modifiers decl >>= preProcessCtors
+  let view ← dataSyntaxToView modifiers decl 
+  let view ← preProcessCtors view /- same as >>= -/
 
   let (nonRecView, ⟨r, shape, _P, eff⟩) ← runTermElabM fun _ => do
     let (nonRecView, _rho) ← makeNonRecursive view;

Qpf/Macro/Data/Replace.lean

@@ -159,7 +159,9 @@ def getBinderNamesAndType : Syntax → m (Array Syntax × Syntax)
 def preProcessCtors (view : DataView) : m DataView := do
   let ctors ← view.ctors.mapM fun ctor => do
     let namedArgs ← ctor.binders.getArgs.mapM getBinderNamesAndType
-    let flatArgs: Array (TSyntax `term) := (namedArgs.map (fun (ids, ty) => ids.map (fun _ => ⟨ty⟩))).flatten.reverse
+    let flatArgs :=
+      (namedArgs.map (fun (ids, ty) => ids.map (fun _ => ⟨ty⟩)))
+      |>.flatten.reverse
 
     let ty := if let some x := ctor.type? then x else view.getExpectedType
 
@@ -191,7 +193,10 @@ Replace.run <| do
   let ctors := view.ctors
 
   let pairs ← ctors.mapM fun ctor => do
-    /- We do not need to check for binders as the preprocessort fixes this-/
+    /- We do not need to check for binders as the preprocessort fixes this.
+       We keep the test in case it goes wrong. -/
+    if !ctor.binders.isNone then
+      throwErrorAt ctor.binders "Constructor binders are not supported yet, please provide all arguments in the type"
 
     trace[Qpf.Data] "{ctor.declName}: {ctor.type?}"
 

Test.lean

@@ -7,5 +7,5 @@ import Test.List
 import Test.Misc
 import Test.Tree
 -- import Test.Variable
--- import Test.WithBindersInCtor
+import Test.WithBindersInCtor
 import Test.Wrap