From 445a7a2b8bd56c9342dc671af2b2f40601a708be Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?William=20S=C3=B8rensen?= <ws423@cam.ac.uk>
Date: Wed, 26 Jun 2024 11:30:38 +0100
Subject: [PATCH 1/7] refactor: replace.lean

---
 Qpf/Macro/Data/Replace.lean | 49 +++++++++++++++++--------------------
 1 file changed, 22 insertions(+), 27 deletions(-)

diff --git a/Qpf/Macro/Data/Replace.lean b/Qpf/Macro/Data/Replace.lean
index 9120cee..30f7c45 100644
--- a/Qpf/Macro/Data/Replace.lean
+++ b/Qpf/Macro/Data/Replace.lean
@@ -19,10 +19,11 @@ structure CtorArgs where
 
 /- TODO(@William): make these correspond by combining expr and vars into a product -/
 structure Replace where
-  (expr: Array Term)
-  (vars: Array Name)
+  (vals: Array (Name × Term))
   (ctor: CtorArgs)
 
+def Replace.vars (r : Replace): Array Name := r.vals.map Prod.fst
+def Replace.expr (r : Replace): Array Term := r.vals.map Prod.snd
 
 variable (m) [Monad m] [MonadQuotation m] [MonadError m] [MonadTrace m] [MonadOptions m]
               [AddMessageContext m] [MonadLiftT IO m]
@@ -32,13 +33,13 @@ private abbrev ReplaceM := StateT Replace m
 variable {m}
 
 private def Replace.new : m Replace := 
-  do pure ⟨#[], #[], ⟨#[], #[]⟩⟩
+  do pure ⟨#[], ⟨#[], #[]⟩⟩
 
 private def CtorArgs.reset : ReplaceM m Unit := do
   let r ← StateT.get
   let n := r.vars.size
   let ctor: CtorArgs := ⟨#[], (Array.range n).map fun _ => #[]⟩
-  StateT.set ⟨r.expr, r.vars, ctor⟩
+  StateT.set { r with ctor }
 
 private def CtorArgs.get : ReplaceM m CtorArgs := do
   pure (←StateT.get).ctor
@@ -47,7 +48,7 @@ private def CtorArgs.get : ReplaceM m CtorArgs := do
   The arity of the shape type created *after* replacing, i.e., the size of `r.expr`
 -/
 def Replace.arity (r : Replace) : Nat :=
-  r.expr.size
+  r.vals.size
 
 def Replace.getBinderIdents (r : Replace) : Array Ident :=
   r.vars.map mkIdent
@@ -68,19 +69,19 @@ private def ReplaceM.identFor (stx : Term) : ReplaceM m Ident := do
   let r ← StateT.get
   let ctor := r.ctor
   let argName ← mkFreshBinderName
-  let ctor_args := ctor.args.push argName
+  let args := ctor.args.push argName
   -- dbg_trace "\nstx := {stx}\nr.expr := {r.expr}"
 
   let name ← match r.expr.indexOf? stx with
-  | some id => do      
-      let ctor_per_type := ctor.per_type.set! id $ (ctor.per_type.get! id).push argName
-      let ctor := ⟨ctor_args, ctor_per_type⟩
-      StateT.set ⟨r.expr, r.vars, ctor⟩
+  | some id => do
+      let per_type := ctor.per_type.set! id $ (ctor.per_type.get! id).push argName
+      let ctor := { args, per_type }
+      StateT.set { r with ctor }
       pure $ r.vars.get! id
   | none       => do
-      let ctor_per_type := ctor.per_type.push #[argName]
+      let per_type := ctor.per_type.push #[argName]
       let name ← mkFreshBinderName
-      StateT.set ⟨r.expr.push stx, r.vars.push name, ⟨ctor_args, ctor_per_type⟩⟩
+      StateT.set { vals := r.vals.push (name, stx), ctor := { args, per_type } }
       pure name
 
   return mkIdent name
@@ -118,11 +119,6 @@ private partial def setResultingType (res_type : Syntax) : Syntax → ReplaceM m
   | _ => 
       pure res_type
 
--- TODO: this should be deprecated in favour of {v with ...} syntax
-def CtorView.withType? (ctor : CtorView) (type? : Option Syntax) : CtorView := {
-  ctor with type?
-}
-
 /-
   TODO: currently these functions ignore dead variables, everything is replaced.
   This is OK, we can supply a "dead" value to a live variable, but we lose the ability to have
@@ -216,8 +212,8 @@ Replace.run <| do
 
       -- HACK: It seems that `Array.append` causes a stack overflow, so we go through `List` for now
       -- TODO: fix this after updating to newer Lean version
-      let per_type := per_type.appendList $ (List.range diff).map (fun _ => (#[] : Array Name));
-      ⟨ctorArgs.args, per_type⟩
+      let per_type := per_type.appendList $ List.replicate diff (#[] : Array Name)
+      { ctorArgs with per_type }
 
   -- Now that we know how many free variables were introduced, we can fix up the resulting type
   -- of each constructor to be `Shape α_0 α_1 ... α_n`
@@ -226,7 +222,7 @@ Replace.run <| do
 
   let ctors ← ctors.mapM fun ctor => do
     let type? ← ctor.type?.mapM (setResultingType res) 
-    pure $ CtorView.withType? ctor type?
+    pure { ctor with type? }
 
   pure (ctors, ctorArgs)
 
@@ -234,12 +230,11 @@ Replace.run <| do
 
 
 /-- Replace syntax in *all* subexpressions -/
-partial def Replace.replaceAllStx (find replace : Syntax) : Syntax → Syntax := 
-  fun stx =>
-    if stx == find then
-      replace
-    else
-      stx.setArgs (stx.getArgs.map (replaceAllStx find replace))
+partial def Replace.replaceAllStx (find replace stx : Syntax) : Syntax := 
+  if stx == find then
+    replace
+  else
+    stx.setArgs (stx.getArgs.map (replaceAllStx find replace))
 
 
 
@@ -292,7 +287,7 @@ def makeNonRecursive (view : DataView) : MetaM (DataView × Name) := do
 
   let ctors ← view.ctors.mapM fun ctor => do
     let type? ← ctor.type?.mapM (Replace.replaceStx expected recId <| TSyntax.mk ·)
-    return CtorView.withType? ctor type?
+    pure { ctor with type? }
 
   let view := view.setCtors ctors
   pure (view, rec)

From 33b6353260004d827e7d9a2133ca47054e546f49 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?William=20S=C3=B8rensen?= <ws423@cam.ac.uk>
Date: Wed, 26 Jun 2024 11:33:08 +0100
Subject: [PATCH 2/7] fix: typo in refactor

---
 Qpf/Macro/Data/Replace.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Qpf/Macro/Data/Replace.lean b/Qpf/Macro/Data/Replace.lean
index 30f7c45..89de3bb 100644
--- a/Qpf/Macro/Data/Replace.lean
+++ b/Qpf/Macro/Data/Replace.lean
@@ -201,7 +201,7 @@ Replace.run <| do
 
     let type? ← ctor.type?.mapM $ shapeOf'
 
-    pure $ (CtorView.withType? ctor type?, ←CtorArgs.get)
+    pure ({ ctor with type? }, ←CtorArgs.get)
 
   let r ← StateT.get
   let ctors := pairs.map Prod.fst;

From e46d8e0a256704b20c3adf52acc3e4d4cfb566be Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 26 Jun 2024 16:50:52 +0100
Subject: [PATCH 3/7] Revert "refactor: replace.lean"

---
 Qpf/Macro/Data/Replace.lean | 51 ++++++++++++++++++++-----------------
 1 file changed, 28 insertions(+), 23 deletions(-)

diff --git a/Qpf/Macro/Data/Replace.lean b/Qpf/Macro/Data/Replace.lean
index 89de3bb..9120cee 100644
--- a/Qpf/Macro/Data/Replace.lean
+++ b/Qpf/Macro/Data/Replace.lean
@@ -19,11 +19,10 @@ structure CtorArgs where
 
 /- TODO(@William): make these correspond by combining expr and vars into a product -/
 structure Replace where
-  (vals: Array (Name × Term))
+  (expr: Array Term)
+  (vars: Array Name)
   (ctor: CtorArgs)
 
-def Replace.vars (r : Replace): Array Name := r.vals.map Prod.fst
-def Replace.expr (r : Replace): Array Term := r.vals.map Prod.snd
 
 variable (m) [Monad m] [MonadQuotation m] [MonadError m] [MonadTrace m] [MonadOptions m]
               [AddMessageContext m] [MonadLiftT IO m]
@@ -33,13 +32,13 @@ private abbrev ReplaceM := StateT Replace m
 variable {m}
 
 private def Replace.new : m Replace := 
-  do pure ⟨#[], ⟨#[], #[]⟩⟩
+  do pure ⟨#[], #[], ⟨#[], #[]⟩⟩
 
 private def CtorArgs.reset : ReplaceM m Unit := do
   let r ← StateT.get
   let n := r.vars.size
   let ctor: CtorArgs := ⟨#[], (Array.range n).map fun _ => #[]⟩
-  StateT.set { r with ctor }
+  StateT.set ⟨r.expr, r.vars, ctor⟩
 
 private def CtorArgs.get : ReplaceM m CtorArgs := do
   pure (←StateT.get).ctor
@@ -48,7 +47,7 @@ private def CtorArgs.get : ReplaceM m CtorArgs := do
   The arity of the shape type created *after* replacing, i.e., the size of `r.expr`
 -/
 def Replace.arity (r : Replace) : Nat :=
-  r.vals.size
+  r.expr.size
 
 def Replace.getBinderIdents (r : Replace) : Array Ident :=
   r.vars.map mkIdent
@@ -69,19 +68,19 @@ private def ReplaceM.identFor (stx : Term) : ReplaceM m Ident := do
   let r ← StateT.get
   let ctor := r.ctor
   let argName ← mkFreshBinderName
-  let args := ctor.args.push argName
+  let ctor_args := ctor.args.push argName
   -- dbg_trace "\nstx := {stx}\nr.expr := {r.expr}"
 
   let name ← match r.expr.indexOf? stx with
-  | some id => do
-      let per_type := ctor.per_type.set! id $ (ctor.per_type.get! id).push argName
-      let ctor := { args, per_type }
-      StateT.set { r with ctor }
+  | some id => do      
+      let ctor_per_type := ctor.per_type.set! id $ (ctor.per_type.get! id).push argName
+      let ctor := ⟨ctor_args, ctor_per_type⟩
+      StateT.set ⟨r.expr, r.vars, ctor⟩
       pure $ r.vars.get! id
   | none       => do
-      let per_type := ctor.per_type.push #[argName]
+      let ctor_per_type := ctor.per_type.push #[argName]
       let name ← mkFreshBinderName
-      StateT.set { vals := r.vals.push (name, stx), ctor := { args, per_type } }
+      StateT.set ⟨r.expr.push stx, r.vars.push name, ⟨ctor_args, ctor_per_type⟩⟩
       pure name
 
   return mkIdent name
@@ -119,6 +118,11 @@ private partial def setResultingType (res_type : Syntax) : Syntax → ReplaceM m
   | _ => 
       pure res_type
 
+-- TODO: this should be deprecated in favour of {v with ...} syntax
+def CtorView.withType? (ctor : CtorView) (type? : Option Syntax) : CtorView := {
+  ctor with type?
+}
+
 /-
   TODO: currently these functions ignore dead variables, everything is replaced.
   This is OK, we can supply a "dead" value to a live variable, but we lose the ability to have
@@ -201,7 +205,7 @@ Replace.run <| do
 
     let type? ← ctor.type?.mapM $ shapeOf'
 
-    pure ({ ctor with type? }, ←CtorArgs.get)
+    pure $ (CtorView.withType? ctor type?, ←CtorArgs.get)
 
   let r ← StateT.get
   let ctors := pairs.map Prod.fst;
@@ -212,8 +216,8 @@ Replace.run <| do
 
       -- HACK: It seems that `Array.append` causes a stack overflow, so we go through `List` for now
       -- TODO: fix this after updating to newer Lean version
-      let per_type := per_type.appendList $ List.replicate diff (#[] : Array Name)
-      { ctorArgs with per_type }
+      let per_type := per_type.appendList $ (List.range diff).map (fun _ => (#[] : Array Name));
+      ⟨ctorArgs.args, per_type⟩
 
   -- Now that we know how many free variables were introduced, we can fix up the resulting type
   -- of each constructor to be `Shape α_0 α_1 ... α_n`
@@ -222,7 +226,7 @@ Replace.run <| do
 
   let ctors ← ctors.mapM fun ctor => do
     let type? ← ctor.type?.mapM (setResultingType res) 
-    pure { ctor with type? }
+    pure $ CtorView.withType? ctor type?
 
   pure (ctors, ctorArgs)
 
@@ -230,11 +234,12 @@ Replace.run <| do
 
 
 /-- Replace syntax in *all* subexpressions -/
-partial def Replace.replaceAllStx (find replace stx : Syntax) : Syntax := 
-  if stx == find then
-    replace
-  else
-    stx.setArgs (stx.getArgs.map (replaceAllStx find replace))
+partial def Replace.replaceAllStx (find replace : Syntax) : Syntax → Syntax := 
+  fun stx =>
+    if stx == find then
+      replace
+    else
+      stx.setArgs (stx.getArgs.map (replaceAllStx find replace))
 
 
 
@@ -287,7 +292,7 @@ def makeNonRecursive (view : DataView) : MetaM (DataView × Name) := do
 
   let ctors ← view.ctors.mapM fun ctor => do
     let type? ← ctor.type?.mapM (Replace.replaceStx expected recId <| TSyntax.mk ·)
-    pure { ctor with type? }
+    return CtorView.withType? ctor type?
 
   let view := view.setCtors ctors
   pure (view, rec)

From d9cc5228839614b9bdcccbeeab27557398c88468 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 26 Jun 2024 17:03:32 +0100
Subject: [PATCH 4/7] style

---
 Qpf/Macro/Data/Replace.lean | 49 +++++++++++++++++--------------------
 1 file changed, 23 insertions(+), 26 deletions(-)

diff --git a/Qpf/Macro/Data/Replace.lean b/Qpf/Macro/Data/Replace.lean
index 89de3bb..6587589 100644
--- a/Qpf/Macro/Data/Replace.lean
+++ b/Qpf/Macro/Data/Replace.lean
@@ -17,13 +17,12 @@ structure CtorArgs where
   (args : Array Name)
   (per_type : Array (Array Name))
 
-/- TODO(@William): make these correspond by combining expr and vars into a product -/
 structure Replace where
-  (vals: Array (Name × Term))
+  (newParameters : Array (Name × Term))
   (ctor: CtorArgs)
 
-def Replace.vars (r : Replace): Array Name := r.vals.map Prod.fst
-def Replace.expr (r : Replace): Array Term := r.vals.map Prod.snd
+def Replace.vars (r : Replace) : Array Name := r.newParameters.map Prod.fst
+def Replace.expr (r : Replace) : Array Term := r.newParameters.map Prod.snd
 
 variable (m) [Monad m] [MonadQuotation m] [MonadError m] [MonadTrace m] [MonadOptions m]
               [AddMessageContext m] [MonadLiftT IO m]
@@ -32,7 +31,7 @@ private abbrev ReplaceM := StateT Replace m
 
 variable {m}
 
-private def Replace.new : m Replace := 
+private def Replace.new : m Replace :=
   do pure ⟨#[], ⟨#[], #[]⟩⟩
 
 private def CtorArgs.reset : ReplaceM m Unit := do
@@ -44,11 +43,9 @@ private def CtorArgs.reset : ReplaceM m Unit := do
 private def CtorArgs.get : ReplaceM m CtorArgs := do
   pure (←StateT.get).ctor
 
-/--
-  The arity of the shape type created *after* replacing, i.e., the size of `r.expr`
--/
+/-- The arity of the shape type created *after* replacing, i.e., the size of `r.newParameters` -/
 def Replace.arity (r : Replace) : Nat :=
-  r.vals.size
+  r.newParameters.size
 
 def Replace.getBinderIdents (r : Replace) : Array Ident :=
   r.vars.map mkIdent
@@ -81,11 +78,11 @@ private def ReplaceM.identFor (stx : Term) : ReplaceM m Ident := do
   | none       => do
       let per_type := ctor.per_type.push #[argName]
       let name ← mkFreshBinderName
-      StateT.set { vals := r.vals.push (name, stx), ctor := { args, per_type } }
+      StateT.set { newParameters := r.newParameters.push (name, stx), ctor := { args, per_type } }
       pure name
 
   return mkIdent name
-  
+
 
 
 
@@ -97,13 +94,13 @@ open Lean.Parser in
 -/
 private partial def shapeOf' : Syntax → ReplaceM m Syntax
   | Syntax.node _ ``Term.arrow #[arg, arrow, tail] => do
-    let ctor_arg ← ReplaceM.identFor ⟨arg⟩ 
+    let ctor_arg ← ReplaceM.identFor ⟨arg⟩
     let ctor_tail ← shapeOf' tail
 
-    -- dbg_trace ">> {arg} ==> {ctor_arg}"    
+    -- dbg_trace ">> {arg} ==> {ctor_arg}"
     pure $ mkNode ``Term.arrow #[ctor_arg, arrow, ctor_tail]
 
-  | ctor_type => 
+  | ctor_type =>
       pure ctor_type
 
 
@@ -116,7 +113,7 @@ private partial def setResultingType (res_type : Syntax) : Syntax → ReplaceM m
   | Syntax.node _ ``Term.arrow #[arg, arrow, tail] => do
     let tail ← setResultingType res_type tail
     pure $ mkNode ``Term.arrow #[arg, arrow, tail]
-  | _ => 
+  | _ =>
       pure res_type
 
 /-
@@ -127,7 +124,7 @@ private partial def setResultingType (res_type : Syntax) : Syntax → ReplaceM m
 
   We should instead detect which expressions are dead, and NOT introduce fresh variables for them.
   Instead, have the shape functor also take the same dead binders as the original.
-  This does mean that we should check for collisions between the original dead binders, and the 
+  This does mean that we should check for collisions between the original dead binders, and the
   fresh variables.
 -/
 
@@ -135,8 +132,8 @@ private partial def setResultingType (res_type : Syntax) : Syntax → ReplaceM m
 
 
 /-- Runs the given action with a fresh instance of `Replace` -/
-def Replace.run : ReplaceM m α → m (α × Replace) := 
-  fun x => do 
+def Replace.run : ReplaceM m α → m (α × Replace) :=
+  fun x => do
     let r ← Replace.new
     StateT.run x r
 
@@ -174,9 +171,9 @@ def preProcessCtors (view : DataView) : m DataView := do
   of the same type map to a single variable, where "same" refers to a very simple notion of
   syntactic equality. E.g., it does not realize `Nat` and `ℕ` are the same.
 -/
-def Replace.shapeOfCtors (view : DataView) 
-                          (shapeIdent : Syntax) 
-    : m ((Array CtorView × Array CtorArgs) × Replace) := 
+def Replace.shapeOfCtors (view : DataView)
+                          (shapeIdent : Syntax)
+    : m ((Array CtorView × Array CtorArgs) × Replace) :=
 Replace.run <| do
   for var in view.liveBinders do
     let varIdent : Ident := ⟨if var.raw.getKind == ``Parser.Term.binderIdent then
@@ -221,7 +218,7 @@ Replace.run <| do
   let res := Syntax.mkApp (TSyntax.mk shapeIdent) r.getBinderIdents
 
   let ctors ← ctors.mapM fun ctor => do
-    let type? ← ctor.type?.mapM (setResultingType res) 
+    let type? ← ctor.type?.mapM (setResultingType res)
     pure { ctor with type? }
 
   pure (ctors, ctorArgs)
@@ -230,7 +227,7 @@ Replace.run <| do
 
 
 /-- Replace syntax in *all* subexpressions -/
-partial def Replace.replaceAllStx (find replace stx : Syntax) : Syntax := 
+partial def Replace.replaceAllStx (find replace stx : Syntax) : Syntax :=
   if stx == find then
     replace
   else
@@ -250,7 +247,7 @@ partial def Replace.replaceStx (recType newParam : Term) : Term → MetaM Term
         pure <| TSyntax.mk <| stx.setArgs #[
           replaceAllStx recType newParam arg,
           arrow,
-          ←replaceStx recType newParam ⟨tail⟩ 
+          ←replaceStx recType newParam ⟨tail⟩
         ]
 
     | stx@(Syntax.node _ ``Term.arrow _) =>
@@ -259,11 +256,11 @@ partial def Replace.replaceStx (recType newParam : Term) : Term → MetaM Term
     | stx@(Syntax.node _ ``Term.depArrow _) =>
         throwErrorAt stx "Dependent arrows are not supported, please only use plain arrow types"
 
-    | ctor_type => 
+    | ctor_type =>
         if ctor_type != recType then
           throwErrorAt ctor_type m!"Unexpected constructor resulting type; expected {recType}, found {ctor_type}"
         else
-          pure ⟨ctor_type⟩ 
+          pure ⟨ctor_type⟩
 
 
 

From abff4611ee943cb4a47fef6516d6ae9cdd4e9cfa Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 26 Jun 2024 17:17:05 +0100
Subject: [PATCH 5/7] fix build

---
 Qpf/Macro/Data/Replace.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Qpf/Macro/Data/Replace.lean b/Qpf/Macro/Data/Replace.lean
index 355aad1..05800ca 100644
--- a/Qpf/Macro/Data/Replace.lean
+++ b/Qpf/Macro/Data/Replace.lean
@@ -38,7 +38,7 @@ private def CtorArgs.reset : ReplaceM m Unit := do
   let r ← StateT.get
   let n := r.vars.size
   let ctor: CtorArgs := ⟨#[], (Array.range n).map fun _ => #[]⟩
-  StateT.set ⟨r.expr, r.vars, ctor⟩
+  StateT.set { r with ctor }
 
 private def CtorArgs.get : ReplaceM m CtorArgs := do
   pure (←StateT.get).ctor
@@ -66,17 +66,17 @@ private def ReplaceM.identFor (stx : Term) : ReplaceM m Ident := do
   let r ← StateT.get
   let ctor := r.ctor
   let argName ← mkFreshBinderName
-  let ctor_args := ctor.args.push argName
+  let args := ctor.args.push argName
   -- dbg_trace "\nstx := {stx}\nr.expr := {r.expr}"
 
   let name ← match r.expr.indexOf? stx with
   | some id => do
-      let ctor_per_type := ctor.per_type.set! id $ (ctor.per_type.get! id).push argName
-      let ctor := ⟨ctor_args, ctor_per_type⟩
-      StateT.set ⟨r.expr, r.vars, ctor⟩
+      let per_type := ctor.per_type.set! id $ (ctor.per_type.get! id).push argName
+      let ctor := { args, per_type }
+      StateT.set { r with ctor }
       pure $ r.vars.get! id
   | none       => do
-      let ctor_per_type := ctor.per_type.push #[argName]
+      let per_type := ctor.per_type.push #[argName]
       let name ← mkFreshBinderName
       StateT.set { newParameters := r.newParameters.push (name, stx), ctor := { args, per_type } }
       pure name

From b3c22704a1b7c777df420a2c47be96dfb7c60b9f Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 26 Jun 2024 17:32:31 +0100
Subject: [PATCH 6/7] chore: minor style changes

---
 Qpf/Macro/Comp.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/Qpf/Macro/Comp.lean b/Qpf/Macro/Comp.lean
index 8d10d00..8dcf5fa 100644
--- a/Qpf/Macro/Comp.lean
+++ b/Qpf/Macro/Comp.lean
@@ -42,13 +42,13 @@ open Qq
   open TSyntax.Compat
 
 def synthMvFunctor {n : Nat} (F : Q(TypeFun.{u,u} $n)) : MetaM Q(MvFunctor $F) := do
-  let inst_type : Q(Type (u+1))
-    := q(MvFunctor $F)
+  let inst_type : Q(Type (u+1)) :=
+    q(MvFunctor $F)
   synthInstanceQ inst_type
 
 def synthQPF {n : Nat} (F : Q(TypeFun.{u,u} $n)) (_ : Q(MvFunctor $F)) : MetaM Q(MvQPF $F) := do
-  let inst_type : Q(Type (u+1))
-    := q(MvQPF $F)
+  let inst_type : Q(Type (u+1)) :=
+    q(MvQPF $F)
   synthInstanceQ inst_type
 
 
@@ -242,7 +242,7 @@ partial def handleApp (vars : Vector Q(Type u) arity) (target : Q(Type u))  : Te
       pure ⟨comp, functor, qpf⟩
 
 
-partial def handleArrow (vars : Vector Q(Type u) arity) (target : Q(Type u)) (targetStx : Option Term := none) (normalized := false) : TermElabM (ElabQpfResult u arity) := do 
+partial def handleArrow (vars : Vector Q(Type u) arity) (target : Q(Type u)) (targetStx : Option Term := none) (normalized := false) : TermElabM (ElabQpfResult u arity) := do
   match target with
   | Expr.forallE _ e₁ e₂ .. =>
     let newTarget ← mkAppM ``MvQPF.Arrow.Arrow #[e₁, e₂]

From 76af185c57b88b3c0af43c2ea092a32a1cec3367 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?William=20S=C3=B8rensen?=
 <47296141+Equilibris@users.noreply.github.com>
Date: Fri, 28 Jun 2024 17:48:39 +0200
Subject: [PATCH 7/7] Apply suggestions from code review

Fix whitespace
---
 Qpf/Macro/Comp.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Qpf/Macro/Comp.lean b/Qpf/Macro/Comp.lean
index 68aa414..35a2a4a 100644
--- a/Qpf/Macro/Comp.lean
+++ b/Qpf/Macro/Comp.lean
@@ -154,7 +154,7 @@ def DVec.toExpr {n : Nat} {αs : Q(Fin2 $n → Type u)} (xs : DVec (fun (i : Fin
 
 
 structure ElabQpfResult (u : Level) (arity : Nat) where
-  F : Q(TypeFun.{u,u} $arity)       := by exact q(by infer_instance)
+  F : Q(TypeFun.{u,u} $arity)
   functor : Q(MvFunctor $F)         := by exact q(by infer_instance)
   qpf     : Q(@MvQPF _ $F $functor) := by exact q(by infer_instance)
 deriving Inhabited
@@ -183,7 +183,7 @@ partial def handleConst (target : Q(Type u))  : TermElabM (ElabQpfResult u arity
   pure { F := const, functor := q(Const.MvFunctor), qpf := q(Const.mvqpf)}
 
 
-partial def handleApp (vars : Vector FVarId arity) (target : Q(Type u))  : TermElabM (ElabQpfResult u arity) := do
+partial def handleApp (vars : Vector FVarId arity) (target : Q(Type u)) : TermElabM (ElabQpfResult u arity) := do
   let vars' := vars.toList
 
   let ⟨numArgs, F, args⟩ ← (Comp.parseApp (isLiveVar vars) target)
@@ -236,7 +236,7 @@ partial def handleApp (vars : Vector FVarId arity) (target : Q(Type u))  : TermE
     return { F := comp, functor, qpf }
 
 
-partial def handleArrow (binderType body : Expr) (vars : Vector FVarId arity) (targetStx : Option Term := none) (normalized := false): TermElabM (ElabQpfResult u arity) := do
+partial def handleArrow (binderType body : Expr) (vars : Vector FVarId arity) (targetStx : Option Term := none) (normalized := false) : TermElabM (ElabQpfResult u arity) := do
   let newTarget ← mkAppM ``MvQPF.Arrow.Arrow #[binderType, body]
   elabQpf vars newTarget targetStx normalized
 /--