refactor: remove the MvQPF.IsPolynomial class

Qpf/Macro/Comp.lean

@@ -49,7 +49,7 @@ def synthMvFunctor {n : Nat} (F : Q(TypeFun.{u,u} $n)) : MetaM Q(MvFunctor $F) :
     q(MvFunctor $F)
   synthInstanceQ inst_type
 
-def synthQPF {n : Nat} (F : Q(TypeFun.{u,u} $n)) (_ : Q(MvFunctor $F)) : MetaM Q(MvQPF $F) := do
+def synthQPF {n : Nat} (F : Q(TypeFun.{u,u} $n)) : MetaM Q(MvQPF $F) := do
   let inst_type : Q(Type (u+1)) :=
     q(MvQPF $F)
   synthInstanceQ inst_type
@@ -87,10 +87,9 @@ where
     try
       -- Only try to infer QPF if `F` contains no live variables
       if !F.hasAnyFVar isLiveVar then
-        let F : Q(TypeFun.{u,u} $depth)
-          := q(TypeFun.ofCurried $F)
-        let functor ← synthMvFunctor F
-        let _ ← synthQPF F functor
+        let F : Q(TypeFun.{u,u} $depth) :=
+          q(TypeFun.ofCurried $F)
+        let _ ← synthQPF F
         return ⟨depth, F, args⟩
       throwError "Smallest function subexpression still contains live variables:\n  {F}\ntry marking more variables as dead"
     catch e =>
@@ -106,8 +105,7 @@ where
       trace[QPF] "F := {F}\nargs := {args.toList}\ndepth := {depth}"
       let F : Q(TypeFun.{u,u} $depth)
         := q(TypeFun.ofCurried $F)
-      let functor ← synthMvFunctor F
-      let _ ← synthQPF F functor
+      let _ ← synthQPF F
       return ⟨depth, F, args⟩
 
 
@@ -213,7 +211,6 @@ partial def handleApp (vars : Vector FVarId arity) (target : Q(Type u)) : TermEl
   else
     let G ← args.mmap (elabQpf vars · none false)
 
-    let Ffunctor ← synthInstanceQ q(MvFunctor $F)
     let Fqpf ← synthInstanceQ q(@MvQPF _ $F)
 
     let G : Vec _ numArgs := fun i => G.get i.inv

Qpf/Macro/Data.lean

@@ -304,8 +304,8 @@ def mkQpf (shapeView : InductiveView) (ctorArgs : Array CtorArgs) (headT P : Ide
       map f x   := ($eqv).invFun <| ($P).map f <| ($eqv).toFun <| x
   )
   elabCommandAndTrace (header := "defining {q}") <|← `(
-    instance $q:ident : MvQPF.IsPolynomial (@TypeFun.ofCurried $(quote arity) $shape) :=
-      .ofEquiv $P $eqv
+    instance $q:ident : MvQPF (@TypeFun.ofCurried $(quote arity) $shape) :=
+      .ofEquiv (fun _ => $eqv)
   )
 
 /-! ## mkShape -/
@@ -382,33 +382,6 @@ def mkShape (view : DataView) : TermElabM MkShapeResult := do
     mkQpf view ctorArgs headTId PId r.expr.size
   ⟩
 
-open Elab.Term Parser.Term in
-/--
-  Checks whether the given term is a polynomial functor, i.e., whether there is an instance of
-  `IsPolynomial F`, and return that instance (if it exists).
--/
-def isPolynomial (view : DataView) (F: Term) : CommandElabM (Option Term) :=
-  withQPFTraceNode "isPolynomial" (tag := "isPolynomial") <|
-  runTermElabM fun _ => do
-  elabBinders view.deadBinders fun _deadVars => do
-    let inst_func ← `(MvFunctor $F:term)
-    let inst_func ← elabTerm inst_func none
-
-    trace[QPF] "F = {F}"
-    let inst_type ← `(MvQPF.IsPolynomial $F:term)
-    trace[QPF] "inst_type_stx: {inst_type}"
-    let inst_type ← elabTerm inst_type none
-    trace[QPF] "inst_type: {inst_type}"
-
-    try
-      let _ ← synthInstance inst_func
-      let inst ← synthInstance inst_type
-      return some <|<- delab inst
-    catch e =>
-      trace[QPF] "Failed to synthesize `IsPolynomial` instance.\
-        \n\n{e.toMessageData}"
-      return none
-
 /--
   Take either the fixpoint or cofixpoint of `base` to produce an `Internal` uncurried QPF,
   and define the desired type as the curried version of `Internal`

Qpf/PFunctor/Multivariate/Constructions/Prod.lean

@@ -6,7 +6,6 @@ import Mathlib.Data.QPF.Multivariate.Basic
 import Mathlib.Tactic.FinCases
 
 import Qpf.Util
-import Qpf.Qpf.Multivariate.Basic
 
 namespace MvQPF
 namespace Prod
@@ -20,16 +19,11 @@ def P : MvPFunctor 2
 abbrev QpfProd' := P.Obj
 abbrev QpfProd  := TypeFun.curried QpfProd'
 
-/--
-  An uncurried version of the root `Prod`
--/
-abbrev Prod' : TypeFun 2
-  := @TypeFun.ofCurried 2 Prod
-
+/-- An uncurried version of the root `Prod` -/
+def Prod' : TypeFun 2 :=
+  @TypeFun.ofCurried 2 Prod
 
-/--
-  Constructor for `QpfProd'`
--/
+/-- Constructor for `QpfProd'` -/
 def mk (a : Γ 1) (b : Γ 0) : QpfProd' Γ
   := ⟨
       (),
@@ -56,8 +50,9 @@ def equiv {Γ} : Prod' Γ ≃ QpfProd' Γ := {
 instance : MvFunctor Prod' where
   map f x   := equiv.invFun <| P.map f <| equiv.toFun <| x
 
-instance : MvQPF.IsPolynomial Prod' := .ofEquiv _ equiv
-
+instance : MvQPF Prod' := .ofEquiv (fun _ => equiv)
+instance : MvQPF (@TypeFun.ofCurried 2 Prod) :=
+  inferInstanceAs (MvQPF Prod')
 
 end Prod
 

Qpf/PFunctor/Multivariate/Constructions/Sum.lean

@@ -6,7 +6,6 @@ import Mathlib.Data.QPF.Multivariate.Basic
 import Mathlib.Tactic.FinCases
 
 import Qpf.Util
-import Qpf.Qpf.Multivariate.Basic
 
 namespace MvQPF
 namespace Sum
@@ -38,7 +37,7 @@ def inr {Γ : TypeVec 2} (b : Γ 0) : QpfSum' Γ
     ⟩
 
 
-abbrev Sum' := @TypeFun.ofCurried 2 Sum
+def Sum' := @TypeFun.ofCurried 2 Sum
 
 def box {Γ : TypeVec 2} : Sum' Γ → QpfSum' Γ
   | .inl a => inl a
@@ -70,8 +69,9 @@ def equiv {Γ} : Sum' Γ ≃ QpfSum' Γ :=
 instance : MvFunctor Sum' where
   map f x   := equiv.invFun <| SumPFunctor.map f <| equiv.toFun <| x
 
-instance : MvQPF.IsPolynomial Sum' :=
-  .ofEquiv _ equiv
+instance : MvQPF Sum' := .ofEquiv @equiv
+instance : MvQPF (@TypeFun.ofCurried 2 Sum) :=
+  inferInstanceAs (MvQPF Sum')
 
 end Sum
 

Qpf/Qpf.lean

@@ -1,6 +1,4 @@
 
-import Qpf.Qpf.Multivariate.Basic
-
 import Qpf.PFunctor.Multivariate.Basic
 import Qpf.PFunctor.Multivariate.Constructions.Arrow
 import Qpf.PFunctor.Multivariate.Constructions.Prod

Qpf/Qpf/Multivariate/Constructions/DeepThunk.lean

@@ -62,8 +62,8 @@ instance : MvFunctor DTSum.Uncurried where
   map f := equiv.invFun ∘ Sum.SumPFunctor.map f ∘ equiv.toFun
 
 open DTSum in
-instance : MvQPF.IsPolynomial DTSum.Uncurried :=
-  .ofEquiv _ equiv
+instance : MvQPF DTSum.Uncurried :=
+  .ofEquiv (fun _ => equiv)
 
 namespace DeepThunk