Concrete Function Type in App Nodes

CHANGELOG.md

@@ -10,6 +10,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
   respectively from `Covenant.Test`
 * Add read-only synonyms `Id` and `Arg` for the two data types with the same
   name in `Covenant.ASG`
+* Modify `App` to contain the calculated fully-concrete function type of the fn being applied
 
 ## 1.3.0 -- 2025-10-07
 

src/Covenant/ASG.hs

@@ -254,7 +254,7 @@ import Covenant.Prim
   )
 import Covenant.Type
   ( CompT (Comp0),
-    CompTBody (ReturnT),
+    CompTBody (ArgsAndResult, ReturnT),
     Constructor,
     ConstructorName,
     DataDeclaration (OpaqueData),
@@ -477,13 +477,15 @@ pattern Lit c <- LitInternal c
 -- or
 -- * 'Data.Wedge.There', meaning \'a concrete type\'.
 --
--- @since 1.3.0
+-- The final CompT is the concretified function type, which is necessary for codegen.
+-- @since wip
 pattern App ::
   Id ->
   Vector Ref ->
   Vector (Wedge BoundTyVar (ValT Void)) ->
+  CompT AbstractTy ->
   ValNodeInfo
-pattern App f args instTys <- AppInternal f args instTys
+pattern App f args instTys concreteFnTy <- AppInternal f args instTys concreteFnTy
 
 -- | Wrap a computation into a value (essentially delaying it).
 --
@@ -755,7 +757,7 @@ err = refTo AnError
 -- * \'Use this type variable in our scope\', specified as 'Data.Wedge.Here'.
 -- * \'Use this concrete type\', specified as 'Data.Wedge.There'.
 --
--- @since 1.2.0
+-- @since wip
 app ::
   forall (m :: Type -> Type).
   (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
@@ -777,16 +779,43 @@ app fId argRefs instTys = do
         if numInstantiations /= numVars
           then throwError $ WrongNumInstantiationsInApp renamedFT numVars numInstantiations
           else do
-            instantiatedFT <- instantiate subs renamedFT
             renamedArgs <- traverse renameArg argRefs
+            concretifiedFT <- concretifyFT renamedFT renamedArgs
+            instantiatedFT <- instantiate subs concretifiedFT
             tyDict <- asks (view #datatypeInfo)
             result <- either (throwError . UnificationError) pure $ checkApp tyDict instantiatedFT (Vector.toList renamedArgs)
             restored <- undoRenameM result
+            unRenamedFnTy <- undoRenameCompT instantiatedFT
             checkEncodingWithInfo tyDict restored
-            refTo . AValNode restored $ AppInternal fId argRefs instTys
+            refTo . AValNode restored $ AppInternal fId argRefs instTys unRenamedFnTy
     ValNodeType t -> throwError . ApplyToValType $ t
     ErrorNodeType -> throwError ApplyToError
   where
+    renameSubs :: [(Index "tyvar", ValT AbstractTy)] -> m [(Index "tyvar", ValT Renamed)]
+    renameSubs subs =
+      askScope >>= \scope -> case traverse (traverse (runRenameM scope . renameValT)) subs of
+        Left err' -> throwError $ FailedToRenameInstantiation err'
+        Right res -> pure res
+
+    concretifyFT :: CompT Renamed -> Vector (Maybe (ValT Renamed)) -> m (CompT Renamed)
+    concretifyFT fn@(CompT _ body) argValTypes = do
+      argSubs <- getArgSubs body argValTypes
+      instantiate (Map.toList argSubs) fn
+
+    getArgSubs :: CompTBody Renamed -> Vector (Maybe (ValT Renamed)) -> m (Map (Index "tyvar") (ValT Renamed))
+    getArgSubs (ArgsAndResult args _) argValTypes =
+      liftUnifyM
+        . fmap (Vector.foldMap id)
+        $ Vector.zipWithM argSubHelper args argValTypes
+      where
+        argSubHelper :: ValT Renamed -> Maybe (ValT Renamed) -> UnifyM (Map (Index "tyvar") (ValT Renamed))
+        argSubHelper fromFn = \case
+          Nothing -> pure Map.empty
+          Just fromArg -> unify fromFn fromArg
+
+    -- NOTE: The helper function below only concerns instantiations that result from
+    --       explicit type applications (via the third argument to `app`).
+    --
     mkSubstitutions :: Vector (Wedge BoundTyVar (ValT Void)) -> [(Index "tyvar", ValT AbstractTy)]
     mkSubstitutions =
       Vector.ifoldl'
@@ -800,12 +829,6 @@ app fId argRefs instTys = do
         )
         []
 
-    renameSubs :: [(Index "tyvar", ValT AbstractTy)] -> m [(Index "tyvar", ValT Renamed)]
-    renameSubs subs =
-      askScope >>= \scope -> case traverse (traverse (runRenameM scope . renameValT)) subs of
-        Left err' -> throwError $ FailedToRenameInstantiation err'
-        Right res -> pure res
-
     instantiate :: [(Index "tyvar", ValT Renamed)] -> CompT Renamed -> m (CompT Renamed)
     instantiate [] fn = pure fn
     instantiate subs fn = do
@@ -1345,6 +1368,17 @@ undoRenameM val = do
     Left err' -> throwError $ UndoRenameFailure err'
     Right renamed -> pure renamed
 
+undoRenameCompT ::
+  forall (m :: Type -> Type).
+  (MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
+  CompT Renamed ->
+  m (CompT AbstractTy)
+undoRenameCompT comp =
+  undoRenameM (ThunkT comp) >>= \case
+    ThunkT res -> pure res
+    -- This really should be impossible, not just unlikely.
+    _other -> error "Undoing renaming on a CompT resulting in something other than a thunk, which should be totally impossible"
+
 askScope ::
   forall (m :: Type -> Type).
   (MonadReader ASGEnv m) =>

src/Covenant/Data.hs

@@ -122,6 +122,8 @@ data BBFError
 data DatatypeInfo (var :: Type)
   = DatatypeInfo
   { _originalDecl :: DataDeclaration var,
+    -- The second element of the tuple here is the BB form of the Base functor
+    -- (this is what we actually care about most of the time)
     _baseFunctorStuff :: Maybe (DataDeclaration var, ValT var),
     -- NOTE: The ONLY type that won't have a BB form is `Void` (or something isomorphic to it)
     _bbForm :: Maybe (ValT var),

src/Covenant/Internal/Term.hs

@@ -416,8 +416,9 @@ data CompNodeInfo
 -- @since 1.0.0
 data ValNodeInfo
   = LitInternal AConstant
-  | -- | @since 1.3.0
-    AppInternal Id (Vector Ref) (Vector (Wedge BoundTyVar (ValT Void)))
+  | -- | @since wip
+    -- The CompT is the "fully concretified" function type
+    AppInternal Id (Vector Ref) (Vector (Wedge BoundTyVar (ValT Void))) (CompT AbstractTy)
   | ThunkInternal Id
   | -- | @since 1.1.0
     CataInternal Ref Ref

src/Covenant/JSON.hs

@@ -407,7 +407,7 @@ validateCompilationUnit' (CompilationUnit datatypes asg _) = do
         ForceInternal ref -> checkNode "force" $ force ref
       AValNode _ valInfo -> case valInfo of
         LitInternal aConstant -> checkNode "Lit" (lit aConstant)
-        AppInternal fId argRefs instTys -> checkNode "App" (app fId argRefs instTys)
+        AppInternal fId argRefs instTys _ -> checkNode "App" (app fId argRefs instTys)
         ThunkInternal i -> checkNode "Thunk" (thunk i)
         CataInternal r1 r2 -> checkNode "Cata" (cata r1 r2)
         DataConstructorInternal tn cn args -> checkNode "DataConstructor" (dataConstructor tn cn args)
@@ -838,7 +838,7 @@ decodeAConstant =
    Serializes as a sum type without named fields:
 
    {tag: "Lit", fields: [a]}
-   | {tag: "App", fields: [a,b]}
+   | {tag: "App", fields: [a,b,c,d]}
    | {tag: "Thunk",fields: [a]}
    | {tag: "Cata", fields: [a,b]}
    | {tag: "DataConstructor", fields: [a,b,c]}
@@ -850,12 +850,13 @@ decodeAConstant =
 encodeValNodeInfo :: ValNodeInfo -> Encoding
 encodeValNodeInfo = \case
   LitInternal aconst -> taggedFields "Lit" [encodeAConstant aconst]
-  AppInternal f args instTys ->
+  AppInternal f args instTys fTy ->
     taggedFields
       "App"
       [ encodeId f,
         list encodeRef . toList $ args,
-        list encodeInstTy . toList $ instTys
+        list encodeInstTy . toList $ instTys,
+        encodeCompT encodeAbstractTy fTy
       ]
   ThunkInternal f -> taggedFields "Thunk" [encodeId f]
   CataInternal r1 r2 -> taggedFields "Cata" [encodeRef r1, encodeRef r2]
@@ -880,7 +881,8 @@ decodeValNodeInfo =
           f <- withIndex 0 decodeId fieldsArr
           args <- withIndex 1 (withArray "App args" (traverse decodeRef)) fieldsArr
           instTys <- withIndex 2 (withArray "App instTys" (traverse decodeInstTy)) fieldsArr
-          pure $ AppInternal f args instTys,
+          fTy <- withIndex 3 (decodeCompT decodeAbstractTy) fieldsArr
+          pure $ AppInternal f args instTys fTy,
       "Thunk" :=> withField0 (fmap ThunkInternal . decodeId),
       "Cata"
         :=> withFields

src/Covenant/Zipper.hs

@@ -226,7 +226,7 @@ downStep zs@(ZipperState walkedOff g parentLevels currentLevel) =
                         Force r -> next . Tape [] r $ []
                         _ -> miss
                       AValNode _ info -> case info of
-                        App f args _ -> next . Tape [] (AnId f) . toList $ args
+                        App f args _ _ -> next . Tape [] (AnId f) . toList $ args
                         Thunk f -> next . Tape [] (AnId f) $ []
                         Cata alg x -> next . Tape [] alg $ [x]
                         DataConstructor _ _ args -> case args of