Fix Concretification/Unification Issue in app

src/Covenant/ASG.hs

@@ -240,7 +240,7 @@ import Covenant.Internal.Unification
     reconcile,
     runUnifyM,
     substitute,
-    unify,
+    unify, concretifyFT,
   )
 import Covenant.Prim
   ( OneArgFunc,
@@ -757,6 +757,13 @@ err = refTo AnError
 -- * \'Use this type variable in our scope\', specified as 'Data.Wedge.Here'.
 -- * \'Use this concrete type\', specified as 'Data.Wedge.There'.
 --
+-- *** IMPORTANT ***
+-- The *only* purpose of explicit type application arguments is to instantiate a tyvar in the result which is
+-- not determined by any argument. These variables are instantiated after every other argument has been concretified.
+--
+-- For example, if you have a function
+--   `f :: forall a b c. (a -> b) -> (b -> a) -> b -> Either a c`
+-- Then you will need to supply *ONE* explicit type application to concretify `c`.
 -- @since wip
 app ::
   forall (m :: Type -> Type).
@@ -780,7 +787,7 @@ app fId argRefs instTys = do
           then throwError $ WrongNumInstantiationsInApp renamedFT numVars numInstantiations
           else do
             renamedArgs <- traverse renameArg argRefs
-            concretifiedFT <- concretifyFT renamedFT renamedArgs
+            let concretifiedFT = concretifyFT renamedFT renamedArgs
             instantiatedFT <- instantiate subs concretifiedFT
             tyDict <- asks (view #datatypeInfo)
             result <- either (throwError . UnificationError) pure $ checkApp tyDict instantiatedFT (Vector.toList renamedArgs)
@@ -797,22 +804,6 @@ app fId argRefs instTys = do
         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`).
     --
@@ -830,7 +821,6 @@ app fId argRefs instTys = do
         []
 
     instantiate :: [(Index "tyvar", ValT Renamed)] -> CompT Renamed -> m (CompT Renamed)
-    instantiate [] fn = pure fn
     instantiate subs fn = do
       instantiated <- liftUnifyM . fixUp $ foldr (\(i, t) f -> substitute i t f) (ThunkT fn) subs
       case instantiated of

src/Covenant/Internal/Unification.hs

@@ -11,14 +11,15 @@ module Covenant.Internal.Unification
     fixUp,
     reconcile,
     lookupDatatypeInfo,
+    concretifyFT
   )
 where
 
 import Control.Monad (foldM, unless, when)
 import Data.Ord (comparing)
-#if __GLASGOW_HASKELL__==908
+
 import Data.Foldable (foldl')
-#endif
+
 import Control.Monad.Except (MonadError, catchError, throwError)
 import Control.Monad.Reader (MonadReader, ReaderT (runReaderT), ask)
 import Covenant.Data (DatatypeInfo)
@@ -48,6 +49,9 @@ import Data.Vector.NonEmpty (NonEmptyVector)
 import Data.Vector.NonEmpty qualified as NonEmpty
 import Data.Word (Word64)
 import Optics.Core (ix, preview, view)
+import Covenant.Type (CompT(CompN), CompTBody (ArgsAndResult))
+import qualified Data.Map as M
+import Control.Applicative (Alternative((<|>)))
 
 -- | Possible errors resulting from applications of arguments to functions.
 --
@@ -149,7 +153,7 @@ checkApp' ::
   CompT Renamed ->
   [Maybe (ValT Renamed)] ->
   UnifyM (ValT Renamed)
-checkApp' f@(CompT _ (CompTBody xs)) ys = do
+checkApp' f@(CompT _ (CompTBody xs)) ys =  do
   let (curr, rest) = NonEmpty.uncons xs
       numArgsExpected = NonEmpty.length xs - 1
       numArgsActual = length ys
@@ -268,7 +272,7 @@ unify ::
   ValT Renamed ->
   ValT Renamed ->
   UnifyM (Map (Index "tyvar") (ValT Renamed))
-unify expected actual =
+unify expected actual = 
   catchError
     ( case expected of
         Abstraction t1 -> case t1 of
@@ -404,3 +408,62 @@ reconcile =
           _ -> case new of
             Abstraction (Unifiable _) -> pure old
             _ -> throwError $ CouldNotReconcile i old new
+
+
+----- Extra stuff
+
+concretifyFT :: CompT Renamed
+             -> Vector (Maybe (ValT Renamed))
+             -> CompT Renamed
+concretifyFT (CompN cnt (ArgsAndResult fromFn res)) fromArgs =  unfixedResult
+   where
+    -- NOTE/REVIEW: I am not sure if we should fix this up here. I think we shouldn't, b/c we need the unifiables to
+    --              conform with the what the instantiations expect from the explicit type applications, but I
+    --              could very easily be wrong. 
+    unfixedResult :: CompT Renamed
+    unfixedResult = CompN cnt (ArgsAndResult subbedArgs subbedRes)
+
+    subbedArgs = substMany allSubstitutions <$> fromFn
+    subbedRes  = substMany allSubstitutions res
+
+    substMany :: [(Index "tyvar", ValT Renamed)] -> ValT Renamed -> ValT Renamed
+    substMany subs val = foldl' (\acc (tv,ty) -> substitute tv ty acc) val subs
+
+    allUnifiables =  Set.toList $ Vector.foldMap collectUnifiables fromFn
+
+    allSubstitutions = M.toList $ getInstantiations allUnifiables (Vector.toList fromFn) (Vector.toList fromArgs)
+
+getInstantiations :: [Index "tyvar"] -> [ValT Renamed] -> [Maybe (ValT Renamed)] -> Map (Index "tyvar") (ValT Renamed)
+getInstantiations [] _ _ =  M.empty
+getInstantiations _ [] _ =  M.empty
+getInstantiations _ _ [] =  M.empty
+getInstantiations vs (_: fEs) (Nothing : aEs) = getInstantiations vs fEs aEs
+getInstantiations (var : vars) fs@(fE : fEs) as@(aE' : aEs) =
+  -- somewhat subjective but I think doing it w/ fromJust makes the logic easier to follow here 
+  let aE = fromJust aE'
+  in case instantiates (Unifiable var) aE fE of
+        Nothing -> getInstantiations [var] fEs aEs <> getInstantiations vars fs as
+        Just t -> M.insert var t $ getInstantiations vars fs as
+
+instantiates ::
+    Renamed ->
+    ValT Renamed -> -- the "more concrete type", usually the actual argument from 'app'
+    ValT Renamed -> -- the "more polymorphic type', usually from the fn definition
+    Maybe (ValT Renamed)
+instantiates var concrete abstract = case (concrete, abstract) of
+    (x, Abstraction a) -> if var == a then Just x else  Nothing -- N.b. we need to be sure we only run this w/ unifiables as the first arg
+    (ThunkT (CompN _ concreteFn), ThunkT (CompN _ abstractFn)) ->
+        let concreteFn' = Vector.toList $ compTBodyToVec concreteFn
+            abstractFn' = Vector.toList $ compTBodyToVec abstractFn
+         in go concreteFn' abstractFn'
+    (Datatype tnC argsC, Datatype tnA argsA)
+        | tnC == tnA -> go (Vector.toList argsC) (Vector.toList argsA)
+    _ -> Nothing
+  where
+    go :: [ValT Renamed] -> [ValT Renamed] -> Maybe (ValT Renamed)
+    go [] _ =  Nothing
+    go _ [] =  Nothing
+    go (c : cs) (a : as) =  instantiates var c a <|> go cs as
+
+compTBodyToVec :: forall a. CompTBody a -> Vector (ValT a)
+compTBodyToVec (ArgsAndResult args res) = Vector.snoc args res