add a fn-def type and adjust type of fn constants

racket-src/body/type-of.rkt

@@ -125,14 +125,40 @@
    (type-of/Constant Γ false (user-ty bool))]
 
   [; function
-   (where/error (fn _ KindedVarIds (Ty_arg ...) -> Ty_ret _ _ _) (find-fn Γ FnId))
-   (where/error (KindedVarId_subst ..._n KindedVarId_other ...) KindedVarIds)
-   (where/error Substitution (create-substitution (KindedVarId_subst ...) (Parameter ...)))
-   (where/error (Ty_argsubst ...) ((apply-substitution Substitution Ty_arg) ...))
-   (where/error Ty_retsubst (apply-substitution Substitution Ty_ret))
-   (where/error number_args ,(length (term (Ty_arg ...))))
-   (where/error Ty_fnptr (rigid-ty (fn-ptr "Rust" number_args) (Ty_argsubst ... Ty_retsubst)))
-   (where/error Ty (∀ (KindedVarId_other ...) Ty_fnptr))
+   ;
+   ; Subtle: functions in Rust today have early/late-bound parameters,
+   ; but we include both in the FnDef type (unlike rustc). The current assumption
+   ; is that the first N parameters (however many are supplied) are early-bound,
+   ; and the remainder are late. Therefore, the constant
+   ;
+   ;     (fn-ptr foo [P_1 … P_n])
+   ;
+   ; referring to a function foo with the formal variables V_1, …, V_m gets the type
+   ;
+   ;     (∀ [V_n+1 … V_m] (implies Biformulas (rigid-ty (fn-def foo) [P_1 … P_n V_n+1 … V_m])))
+   ;
+   (where/error (fn _ KindedVarIds _ -> _ where Biformulas _) (find-fn Γ FnId))
+
+   ; Split the generics from the function into early/late
+   (where/error (KindedVarId_early ..._n (ParameterKind_late VarId_late) ...) KindedVarIds)
+
+   ; Create a substitution from early-bound parameters to the values from user
+   (where/error Substitution_early (create-substitution (KindedVarId_early ...) (Parameter ...)))
+   (where/error Biformulas_early (apply-substitution Substitution_early Biformulas))
+
+   ; Apply that substitution
+   (where/error Ty_fn (rigid-ty (fn-def FnId) (Parameter ... VarId_late ...)))
+
+   ; Construct the final type
+   ;
+   ;   Note that it has implications to assert that the where-clauses hold.
+   ;   Is this quite right? We want them for at least the biformulas that relate
+   ;   to the late-bound lifetimes, and it seems wrong to do anything fancy, so
+   ;   I think we want them all.
+   ;
+   ;   The idea is that, when we apply the call, we'll have to discharge all those
+   ;   implications, and the same will be true to cast to a final type.
+   (where/error Ty (∀ ((ParameterKind_late VarId_late) ...) (implies Biformulas_early Ty_fn)))
    ------------------------------------------
    (type-of/Constant Γ (fn-ptr FnId (Parameter ..._n)) Ty)]
 

racket-src/decl/env.rkt

@@ -69,6 +69,8 @@
               (term (decl:categorize-goal ,goal)))
             (lambda (adt-id)
               (term (generics-for-adt-id CrateDecls ,adt-id)))
+            (lambda (fn-id)
+              (term (generics-for-fn-id CrateDecls ,fn-id)))
             ))
 
    (where/error (CrateDecls CrateId) DeclProgram)
@@ -86,4 +88,17 @@
    (((VarId (ParameterKind =)) ...) Biformulas) ; for now we hardcode `=` (invariance) as the variance
    (where/error (AdtKind AdtId ((ParameterKind VarId) ...) Biformulas AdtVariants) (adt-with-id CrateDecls AdtId))
    ]
+  )
+
+(define-metafunction formality-decl
+  ;; Part of the "hook" for a formality-decl program:
+  ;;
+  ;; Create the clauses for solving a given predicate
+  ;; (right now the predicate is not used).
+  generics-for-fn-id : CrateDecls FnId -> Generics
+
+  [(generics-for-fn-id CrateDecls FnId)
+   (((VarId (ParameterKind =)) ...) Biformulas) ; for now we hardcode `=` (invariance) as the variance
+   (where/error (fn FnId [(ParameterKind VarId) ...] _ -> _ where Biformulas _) (fn-with-id CrateDecls FnId))
+   ]
   )

racket-src/decl/grammar.rkt

@@ -115,8 +115,7 @@
     StaticId
     VariantId
     FeatureId
-    FieldId
-    FnId) variable-not-otherwise-mentioned)
+    FieldId) variable-not-otherwise-mentioned)
 
   #:binding-forms
   (AdtKind AdtKind

racket-src/ty/grammar.rkt

@@ -113,6 +113,7 @@
              (ref MaybeMut)  ; `&mut` or `&`, expects a lifetime + type parameter
              (tuple number)  ; tuple of given arity
              (fn-ptr Abi number) ; fn types
+             (fn-def FnId)       ; the zero-sized type derived from a type definition
              )
 
   ;; AliasTy -- an *alias* type is basically a *type lambda*. You can either *normalize* it
@@ -190,7 +191,7 @@
 
   ;; Identifiers -- these are all equivalent, but we give them fresh names to help
   ;; clarify their purpose
-  (AdtId AliasId TraitId AssociatedTyId AliasTyId ::=
+  (AdtId AliasId TraitId AssociatedTyId AliasTyId FnId ::=
          variable-not-otherwise-mentioned)
 
   ;; Signature

racket-src/ty/hook.rkt

@@ -12,7 +12,9 @@
 ;; Extends the core logic hook with the ability to query variance:
 ;;
 ;; adt-generics : AdtId -> Generics
+;; fn-generics : FnId -> Generics
 (struct formality-ty-hook formality-logic-hook (adt-generics
+                                                fn-generics
                                                 ))
 
 (define-metafunction formality-ty
@@ -25,6 +27,16 @@
    ]
   )
 
+(define-metafunction formality-ty
+  ;; Returns the variance for each of the parameters to an function
+  env-fn-generics : Env FnId -> Generics
+
+  [(env-fn-generics Env FnId)
+   ,((formality-ty-hook-fn-generics (term any)) (term FnId))
+   (where/error (Hook: any) (env-hook Env))
+   ]
+  )
+
 (define-metafunction formality-ty
   ty:categorize-goal : Goal -> Goal/Categorization
 

racket-src/ty/parameters.rkt

@@ -37,11 +37,26 @@
   ;; a `RigidName`.
   generics-for : Env RigidName -> Generics
 
-  [(generics-for Env AdtId) (env-adt-generics Env AdtId)]
-  [(generics-for Env ScalarId) (() ())]
-  [(generics-for Env (ref ())) (((TheLt (lifetime +)) (TheTy (type +)))
+  [; For an ADT like `Vec`, consult its definition to see what generic parameters it has.
+   (generics-for Env AdtId) (env-adt-generics Env AdtId)]
+
+  [; For a fn, consult its definition to see what generic parameters it has.
+   (generics-for Env (fn-def FnId)) (env-fn-generics Env FnId)]
+
+  [; Scalars like u32 have no generic parameters.
+   ;
+   ; Effectively they are modeled as `struct u32`.
+   (generics-for Env ScalarId) (() ())]
+
+  [; We model `&'a T` as a type with two parameters, `'a` and `T`,
+   ; where `T: 'a`.
+   ;
+   ; Kind of like `struct Ref<'a, T> where T: 'a`
+   (generics-for Env (ref ())) (((TheLt (lifetime +)) (TheTy (type +)))
                                 [(TheTy -outlives- TheLt)])]
-  [(generics-for Env (ref mut)) (((TheLt (lifetime +)) (TheTy (type =)))
+
+  [; We model `&'a mut T` the same way.
+   (generics-for Env (ref mut)) (((TheLt (lifetime +)) (TheTy (type =)))
                                  [(TheTy -outlives- TheLt)])]
 
   [; tuples are covariant in their elements P1...Pn

racket-src/ty/test/hook.rkt

@@ -35,6 +35,7 @@
                              (lambda (predicate1) (term (ty:debone-predicate ,predicate1)))
                              (lambda (goal) (term (ty:categorize-goal ,goal)))
                              (lambda (adt-id) (term (find-adt-generics ,adt-id ((AdtId Generics) ...))))
+                             (lambda (fn-id) (term NotDefined))
                              ))))
    ]
   )

src/gen/ty.rs

@@ -93,7 +93,6 @@ impl<'tcx> FormalityGen<'tcx> {
                     rustc_hir::Mutability::Mut => format!("(&mut {lifetime_str} {ty_str})"),
                 }
             }
-            ty::TyKind::FnDef(_, _) => todo!(),
             ty::TyKind::FnPtr(fn_sig) => {
                 let inputs = fn_sig
                     .skip_binder()
@@ -182,11 +181,21 @@ impl<'tcx> FormalityGen<'tcx> {
     }
 
     pub fn emit_ty(&self, ty: ty::Ty<'tcx>) -> String {
-        if let ty::TyKind::Param(param_ty) = ty.kind() {
-            format!("{}", param_ty.name)
-        } else {
-            // convert UserTy to Ty by calling the user-ty metafunction
-            format!("(mf-apply user-ty {})", self.emit_user_ty(ty))
+        match ty.kind() {
+            ty::TyKind::FnDef(def_id, substs) => {
+                let fn_id = self.emit_def_path(*def_id);
+                let params = substs
+                    .iter()
+                    .map(|arg| self.emit_param(arg))
+                    .intersperse(" ".to_string())
+                    .collect::<String>();
+                format!("(rigid-ty (fn-def {fn_id}) [{params}])")
+            }
+            ty::TyKind::Param(param_ty) => format!("{}", param_ty.name),
+            _ => {
+                // convert UserTy to Ty by calling the user-ty metafunction
+                format!("(mf-apply user-ty {})", self.emit_user_ty(ty))
+            }
         }
     }