WIP: feat: allow limited type ascriptions in data/codata

Qpf/Macro/Comp.lean

@@ -267,6 +267,7 @@ partial def elabQpf {arity : Nat} (vars : Vector Q(Type u) arity) (target : Q(Ty
 
 
 structure QpfCompositionBodyView where
+  (ref : Syntax := .missing)
   (type?  : Option Syntax := none)
   (target : Term)
   (liveBinders deadBinders : Array Syntax)
@@ -288,7 +289,7 @@ def elabQpfCompositionBody (view: QpfCompositionBodyView) :
     liveBinders := {view.liveBinders}
     deadBinders := {view.deadBinders}
   "
-  runTermElabM fun _ => do
+  runTermElabM fun _ => withRef view.ref do
     let u : Level ←
       if let some typeStx := view.type? then
         let type ← elabTerm typeStx (some <| .sort <|<- mkFreshLevelMVar)

Qpf/Macro/Data.lean

@@ -332,7 +332,7 @@ structure MkShapeResult where
   (effects : CommandElabM Unit)
 
 open Parser in
-def mkShape (view: DataView) : TermElabM MkShapeResult := do
+def mkShape (view : DataView) : TermElabM MkShapeResult := do
   -- If the original declId was `MyType`, we want to register the shape type under `MyType.Shape`
   let (declName, declId, shortDeclName) ← addSuffixToDeclId view.declId "Shape"
 
@@ -399,7 +399,7 @@ open Elab.Term Parser.Term in
   `IsPolynomial F`, and return that instance (if it exists).
 -/
 def isPolynomial (view : DataView) (F: Term) : CommandElabM (Option Term) := do
-  runTermElabM fun _ => do
+  runTermElabM fun _ => withRef view.ref do
     elabBinders view.deadBinders fun _deadVars => do
       let inst_func ← `(MvFunctor $F:term)
       let inst_func ← elabTerm inst_func none
@@ -459,17 +459,20 @@ def mkType (view : DataView) (base : Term × Term × Term) : CommandElabM Unit :
     abbrev $baseIdent:ident $view.deadBinders:bracketedBinder* : TypeFun $(quote <| arity + 1) :=
       $base
 
+    -- instance foo : MvFunctor.{0,0} ($baseApplied) := $functor
+    instance foo : MvFunctor.{1,1} ($baseApplied) := $functor
     instance $baseFunctorIdent:ident : MvFunctor ($baseApplied) := $functor
     instance $baseQPFIdent:ident : MvQPF ($baseApplied) := $q
 
-    abbrev $uncurriedIdent:ident $view.deadBinders:bracketedBinder* : TypeFun $(quote arity) := $fix_or_cofix $base
+    abbrev $uncurriedIdent:ident $view.deadBinders:bracketedBinder* : TypeFun $(quote arity) :=
+      $fix_or_cofix $base
 
-    abbrev $(view.declId) $view.deadBinders:bracketedBinder*
-      := TypeFun.curried $uncurriedApplied
+    abbrev $(view.declId) $view.deadBinders:bracketedBinder* :=
+      TypeFun.curried $uncurriedApplied
   )
 
-  trace[QPF] "elabData.cmd = {cmd}"
-  elabCommand cmd
+  withRef view.ref <|
+    cmd.raw.getArgs.forM elabDeclaration
 
 
 
@@ -541,28 +544,29 @@ def elabData : CommandElab := fun stx => do
   let modifiers ← elabModifiers stx[0]
   let decl := stx[1]
   let view ← dataSyntaxToView modifiers decl
+  withRef view.ref do
+    let (nonRecView, ⟨r, shape, _P, eff⟩) ← runTermElabM fun _ => withRef view.ref do
+      let (nonRecView, _rho) ← makeNonRecursive view;
+      trace[QPF] "nonRecView: {nonRecView}"
+      pure (nonRecView, ←mkShape nonRecView)
+
+    /- Execute the `ComandElabM` side-effects prescribed by `mkShape` -/
+    let _ ← eff
+
+    /- Composition pipeline -/
+    let base ← elabQpfCompositionBody {
+      liveBinders := nonRecView.liveBinders,
+      deadBinders := nonRecView.deadBinders,
+      ref     := view.ref,
+      type?   := none,
+      target  := ←`(
+        $(mkIdent shape):ident $r.expr:term*
+      )
+    }
+    trace[QPF] "base = {base}"
 
-  let (nonRecView, ⟨r, shape, _P, eff⟩) ← runTermElabM fun _ => do
-    let (nonRecView, _rho) ← makeNonRecursive view;
-    trace[QPF] "nonRecView: {nonRecView}"
-    pure (nonRecView, ←mkShape nonRecView)
-
-  /- Execute the `ComandElabM` side-effects prescribed by `mkShape` -/
-  let _ ← eff
-
-  /- Composition pipeline -/
-  let base ← elabQpfCompositionBody {
-    liveBinders := nonRecView.liveBinders,
-    deadBinders := nonRecView.deadBinders,
-    type?   := none,
-    target  := ←`(
-      $(mkIdent shape):ident $r.expr:term*
-    )
-  }
-  trace[QPF] "base = {base}"
-
-  mkType view base
-  mkConstructors view shape
+    mkType view base
+    mkConstructors view shape
 
 
 end Data.Command

Qpf/Macro/Data/View.lean

@@ -2,7 +2,7 @@ import Lean
 import Qpf.Macro.Common
 
 open Lean
-open Meta Elab Elab.Command 
+open Meta Elab Elab.Command
 
 open Parser.Term (bracketedBinder)
 open Parser.Command (declId)
@@ -14,7 +14,7 @@ inductive DataCommand where
   | Codata
   deriving BEq, Inhabited
 
-namespace DataCommand 
+namespace DataCommand
 
 def fromSyntax : Syntax → CommandElabM DataCommand
   | Syntax.atom _ "data"   => pure .Data
@@ -62,13 +62,13 @@ def DataView.asInductive (view : DataView) : InductiveView
   := {
     ref             := view.ref
     declId          := view.declId
-    modifiers       := view.modifiers      
-    shortDeclName   := view.shortDeclName  
-    declName        := view.declName       
-    levelNames      := view.levelNames     
-    binders         := view.binders        
-    type?           := view.type?          
-    ctors           := view.ctors          
+    modifiers       := view.modifiers
+    shortDeclName   := view.shortDeclName
+    declName        := view.declName
+    levelNames      := view.levelNames
+    binders         := view.binders
+    type?           := view.type?
+    ctors           := view.ctors
     derivingClasses := view.derivingClasses
     -- TODO: find out what these computed fields are, add support for them in `data`/`codata`
     computedFields  := #[]
@@ -108,7 +108,7 @@ def DataView.addDeclNameSuffix (view : DataView) (suffix : String) : DataView
 def DataView.getExpectedType (view : DataView) : Term
   := Syntax.mkApp (mkIdent view.shortDeclName) (
     (Macro.getBinderIdents view.binders.getArgs false)
-  )  
+  )
 
 /-- Returns the fully applied, explicit (`@`) form of the type to be defined -/
 def DataView.getExplicitExpectedType (view : DataView) : CommandElabM Term
@@ -158,16 +158,17 @@ instance : ToString (DataView) := ⟨
 -/
 
 
+open Elab Term
 /--
   Raises (hopefully) more informative errors when `data` or `codata` are used with unsupported
   specifications
 -/
-def DataView.doSanityChecks (view : DataView) : CommandElabM Unit := do  
-  if view.liveBinders.isEmpty then    
+def DataView.doSanityChecks (view : DataView) : CommandElabM Unit := do
+  if view.liveBinders.isEmpty then
     if view.deadBinders.isEmpty then
       if view.command == .Codata then
         throwError "Due to a bug, codatatype without any parameters don't quite work yet. Please try adding parameters to your type"
-      else 
+      else
         throwError "Trying to define a datatype without variables, you probably want an `inductive` type instead"
     else
       throwErrorAt view.binders "You should mark some variables as live by removing the type ascription (they will be automatically inferred as `Type _`), or if you don't have variables of type `Type _`, you probably want an `inductive` type"
@@ -179,8 +180,15 @@ def DataView.doSanityChecks (view : DataView) : CommandElabM Unit := do
 
   -- TODO: make this more intelligent. In particular, allow types like `Type`, `Type 3`, or `Type u`
   --       and only throw an error if the user tries to define a family of types
+
   match view.type? with
-  | some t => throwErrorAt t "Unexpected type; type will be automatically inferred. Note that inductive families are not supported due to inherent limitations of QPFs"
+  | some t_stx =>
+    let t : Expr ← runTermElabM <| fun _ =>
+      elabTerm t_stx none
+    if t.isType then
+      pure ()
+    else
+      throwErrorAt t_stx "Unexpected type; type will be automatically inferred. Note that inductive families are not supported due to inherent limitations of QPFs"
   | none => pure ()
 
 
@@ -193,7 +201,7 @@ def dataSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM Data
 
   let (binders, type?) := expandOptDeclSig decl[2]
 
-  let declId  : TSyntax ``declId := ⟨decl[1]⟩ 
+  let declId  : TSyntax ``declId := ⟨decl[1]⟩
   let ⟨name, declName, levelNames⟩ ← expandDeclId declId modifiers
   addDeclarationRanges declName decl
   let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do

Test/Arrow.lean

@@ -1,16 +1,42 @@
 import Qpf
 
+universe u v w
+
 /-- info: MvQPF.Arrow ?α : CurriedTypeFun 1 -/
 #guard_msgs in
   #check MvQPF.Arrow ?α
 
-data Arrow (α : Type _) β
+data Arrow (α : Type) β : Type u
   | mk : (α → β) → Arrow α β
 
 /-- info: Arrow : Type → CurriedTypeFun 1 -/
 #guard_msgs in
   #check (Arrow : Type → Type → Type)
 
--- Types generated by `data` are not as polymorphic as they could/should be,
---   so the following does not yet work:
--- `#check (Arrow : Type 1 → Type 1 → Type 1)`
+/-- info: Arrow.Shape : Type u → Type v → Type w → Type w -/
+#guard_msgs in #check (Arrow.Shape : Type u → Type v → Type w → Type w)
+
+/-- info: Arrow.Base : Type → TypeFun 2 -/
+#guard_msgs in #check (Arrow.Base : Type → TypeFun.{u, u} 2)
+
+#synth MvFunctor (Arrow.Base.{0} _)
+-- ^^^ This works
+#synth MvFunctor (Arrow.Base.{1} _)
+-- ^^^ but this already does not, which explains the issues below
+-- If we add instance foo : MvFunctor.{1,1} ($baseApplied) := $functor to Qpf/Macro/Data.lean explicitely, 
+-- it seems to work but it produces a weird type error.
+
+-- #synth MvQPF (Arrow.Base _ : TypeFun.{0} 2)
+-- -- ^^^ We know that the `Base` is a QPF for universe 0
+--
+-- #synth MvQPF (Arrow.Base _ : TypeFun.{1} 2)
+-- -- ^^^ But, somehow we can't synthesize this fact for higher universes
+--
+-- #check (Arrow.Uncurried : Type → TypeFun.{1} 1)
+-- -- ^^^ Which, presumably, is why `Uncurried` is *not* polymorphic
+--
+--
+--
+-- /-- info: Arrow : Type → CurriedTypeFun 1 -/
+-- #guard_msgs in
+--   #check (Arrow : Type → Type u → Type u)