From 8ef357beada6d7445d79adedc0f62524682ebb68 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?William=20S=C3=B8rensen?= <ws423@cam.ac.uk>
Date: Mon, 24 Jun 2024 14:23:49 +0100
Subject: [PATCH] feat: Fix binder issue

---
 Qpf/Macro/Data.lean         |  3 ++-
 Test/WithBindersInCtor.lean | 14 +++++++++++---
 2 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/Qpf/Macro/Data.lean b/Qpf/Macro/Data.lean
index 680b1aa..99757a1 100644
--- a/Qpf/Macro/Data.lean
+++ b/Qpf/Macro/Data.lean
@@ -540,7 +540,8 @@ open Macro Comp in
 def elabData : CommandElab := fun stx => do
   let modifiers ← elabModifiers stx[0]
   let decl := stx[1]
-  let view ← dataSyntaxToView modifiers decl
+  /- Transforms binders into simple lambda types. -/
+  let view ← dataSyntaxToView modifiers decl >>= preProcessCtors
 
   let (nonRecView, ⟨r, shape, _P, eff⟩) ← runTermElabM fun _ => do
     let (nonRecView, _rho) ← makeNonRecursive view;
diff --git a/Test/WithBindersInCtor.lean b/Test/WithBindersInCtor.lean
index af4fa54..4b56fce 100644
--- a/Test/WithBindersInCtor.lean
+++ b/Test/WithBindersInCtor.lean
@@ -1,5 +1,13 @@
-import Qpf
+import Qpf.Macro.Data
 
-data QpfListWithBinder α 
+data QpfListWithBinder α
+  | cons (h : α) (tl : QpfListWithBinder α)
   | nil
-  | cons (hd : α) (tl : QpfListWithBinder α)
\ No newline at end of file
+
+data Wrap α
+  | mk : α → Wrap α
+data Wrap₂ α
+  | mk (a : α) : Wrap₂ α
+data Wrap₃ α
+  | mk (a : α)
+