allow extra instance arguments for coercions

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs

@@ -405,6 +405,35 @@ checkDefType ty = checkIsType loc ty
   where
     loc = getLoc ty
 
+checkInstanceArg ::
+  forall r.
+  (Members '[Error TypeCheckerError, Reader InfoTable] r) =>
+  HashSet VarName ->
+  [InstanceParam] ->
+  FunctionParameter ->
+  Sem r ()
+checkInstanceArg metaVars params fp@FunctionParameter {..} = case _paramImplicit of
+  Implicit -> return ()
+  Explicit -> throw (ErrExplicitInstanceArgument (ExplicitInstanceArgument fp))
+  ImplicitInstance -> do
+    tab <- ask
+    case traitFromExpression metaVars _paramType of
+      Just app@InstanceApp {..}
+        | isTrait tab _instanceAppHead ->
+            checkTraitTermination app params
+      _ ->
+        throw (ErrNotATrait (NotATrait _paramType))
+
+checkInstanceArgs ::
+  forall r.
+  (Members '[Error TypeCheckerError, Reader InfoTable] r) =>
+  [FunctionParameter] ->
+  [InstanceParam] ->
+  Sem r ()
+checkInstanceArgs args params = do
+  let metaVars = HashSet.fromList $ mapMaybe (^. paramName) args
+  mapM_ (checkInstanceArg metaVars params) args
+
 checkInstanceType ::
   forall r.
   (Members '[Error TypeCheckerError, Reader InfoTable, Inference, NameIdGen, ResultBuilder] r) =>
@@ -427,22 +456,10 @@ checkInstanceType FunctionDef {..} = do
       is <- subsumingInstances itab ii
       unless (null is) $
         throw (ErrSubsumedInstance (SubsumedInstance ii is (getLoc _funDefName)))
-      let metaVars = HashSet.fromList $ mapMaybe (^. paramName) _instanceInfoArgs
-      mapM_ (checkArg tab metaVars ii) _instanceInfoArgs
+      checkInstanceArgs (ii ^. instanceInfoArgs) (ii ^. instanceInfoParams)
       addInstanceInfo ii
     Nothing ->
       throw (ErrInvalidInstanceType (InvalidInstanceType _funDefType))
-  where
-    checkArg :: InfoTable -> HashSet VarName -> InstanceInfo -> FunctionParameter -> Sem r ()
-    checkArg tab metaVars ii fp@FunctionParameter {..} = case _paramImplicit of
-      Implicit -> return ()
-      Explicit -> throw (ErrExplicitInstanceArgument (ExplicitInstanceArgument fp))
-      ImplicitInstance -> case traitFromExpression metaVars _paramType of
-        Just app@InstanceApp {..}
-          | isTrait tab _instanceAppHead ->
-              checkTraitTermination app ii
-        _ ->
-          throw (ErrNotATrait (NotATrait _paramType))
 
 checkInstanceParam ::
   (Member (Error TypeCheckerError) r) =>
@@ -476,17 +493,11 @@ checkCoercionType FunctionDef {..} = do
         throw (ErrTargetNotATrait (TargetNotATrait _funDefType))
       unless (isTrait tab (_coercionInfoTarget ^. instanceAppHead)) $
         throw (ErrInvalidCoercionType (InvalidCoercionType _funDefType))
-      mapM_ checkArg _coercionInfoArgs
+      checkInstanceArgs (ci ^. coercionInfoArgs) (ci ^. coercionInfoParams)
       addCoercionInfo (checkCoercionInfo ci)
       checkCoercionCycles
     Nothing ->
       throw (ErrInvalidCoercionType (InvalidCoercionType _funDefType))
-  where
-    checkArg :: FunctionParameter -> Sem r ()
-    checkArg fp@FunctionParameter {..} = case _paramImplicit of
-      Implicit -> return ()
-      Explicit -> throw (ErrWrongCoercionArgument (WrongCoercionArgument fp))
-      ImplicitInstance -> throw (ErrWrongCoercionArgument (WrongCoercionArgument fp))
 
 checkCaseBranchRhs ::
   forall r.

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs

@@ -26,7 +26,6 @@ data TypeCheckerError
   | ErrUnsupportedTypeFunction UnsupportedTypeFunction
   | ErrInvalidInstanceType InvalidInstanceType
   | ErrInvalidCoercionType InvalidCoercionType
-  | ErrWrongCoercionArgument WrongCoercionArgument
   | ErrCoercionCycles CoercionCycles
   | ErrTargetNotATrait TargetNotATrait
   | ErrNotATrait NotATrait
@@ -55,7 +54,6 @@ instance ToGenericError TypeCheckerError where
     ErrUnsupportedTypeFunction e -> genericError e
     ErrInvalidInstanceType e -> genericError e
     ErrInvalidCoercionType e -> genericError e
-    ErrWrongCoercionArgument e -> genericError e
     ErrCoercionCycles e -> genericError e
     ErrTargetNotATrait e -> genericError e
     ErrNotATrait e -> genericError e
@@ -84,7 +82,6 @@ instance Show TypeCheckerError where
     ErrUnsupportedTypeFunction {} -> "ErrUnsupportedTypeFunction"
     ErrInvalidInstanceType {} -> "ErrInvalidInstanceType"
     ErrInvalidCoercionType {} -> "ErrInvalidCoercionType"
-    ErrWrongCoercionArgument {} -> "ErrWrongCoercionArgument"
     ErrCoercionCycles {} -> "ErrCoercionCycles"
     ErrTargetNotATrait {} -> "ErrTargetNotATrait"
     ErrNotATrait {} -> "ErrNotATrait"

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs

@@ -383,7 +383,7 @@ instance ToGenericError InvalidCoercionType where
           "Invalid coercion type:"
             <+> ppCode opts _invalidCoercionTypeExpression
               <> line
-              <> "A coercion must have exactly one instance argument."
+              <> "A coercion must have a target instance argument."
     return
       GenericError
         { _genericErrorLoc = i,
@@ -394,29 +394,6 @@ instance ToGenericError InvalidCoercionType where
       i :: Interval
       i = getLoc _invalidCoercionTypeExpression
 
-newtype WrongCoercionArgument = WrongCoercionArgument
-  { _wrongCoercionArgumentParameter :: FunctionParameter
-  }
-
-makeLenses ''WrongCoercionArgument
-
-instance ToGenericError WrongCoercionArgument where
-  genericError e = generr
-    where
-      generr =
-        return
-          GenericError
-            { _genericErrorLoc = i,
-              _genericErrorMessage =
-                ppOutput $
-                  "Expected an implicit type argument."
-                    <> line
-                    <> "A coercion can have only implicit type arguments followed by exactly one instance argument.",
-              _genericErrorIntervals = [i]
-            }
-        where
-          i = getLoc (e ^. wrongCoercionArgumentParameter)
-
 newtype TargetNotATrait = TargetNotATrait
   { _targetNotATraitType :: Expression
   }

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Termination.hs

@@ -18,10 +18,10 @@ checkTraitTermination ::
   forall r.
   (Member (Error TypeCheckerError) r) =>
   InstanceApp ->
-  InstanceInfo ->
+  [InstanceParam] ->
   Sem r ()
-checkTraitTermination InstanceApp {..} InstanceInfo {..}
-  | checkMultisetOrdering _instanceAppArgs _instanceInfoParams =
+checkTraitTermination InstanceApp {..} params
+  | checkMultisetOrdering _instanceAppArgs params =
       return ()
   | otherwise =
       throw (ErrTraitNotTerminating (TraitNotTerminating _instanceAppExpression))

src/Juvix/Compiler/Store/Internal/Data/CoercionInfo.hs

@@ -11,11 +11,11 @@ data CoercionInfo = CoercionInfo
     _coercionInfoInductive :: Name,
     -- | The parameters of the coercion are the arguments of the trait on the right of `:`
     _coercionInfoParams :: [InstanceParam],
-    -- | The target is the instance argument of the coercion instance
+    -- | The target instance argument of the coercion instance
     _coercionInfoTarget :: InstanceApp,
     -- | The identifier of the coercion instance definition
     _coercionInfoResult :: Iden,
-    -- | Implicit type arguments of the coercion
+    -- | Remaining instance arguments (not including the target)
     _coercionInfoArgs :: [FunctionParameter],
     _coercionInfoDecreasing :: Bool
   }

test/Typecheck/Negative.hs

@@ -243,7 +243,7 @@ tests =
       $(mkRelDir "Internal")
       $(mkRelFile "WrongCoercionArgument.juvix")
       $ \case
-        ErrWrongCoercionArgument {} -> Nothing
+        ErrTraitNotTerminating {} -> Nothing
         _ -> wrongError,
     negTest
       "Ambiguous coercions"

tests/Compilation/positive/test091.juvix

@@ -88,7 +88,7 @@ StateT-State
       mkStateT λ{_ := Applicative.pure (unit, s)};
   };
 
--- coercion instance
+coercion instance
 StateT-State-trans
   {A B} {E : Type -> Type} {{Monad E}} {{State A E}} : State A (StateT B E) :=
   mkState@{
@@ -256,6 +256,25 @@ type MyNat := mkMyNat@{
   theNat : Nat;
 };
 
+getAndAdd {E : Type -> Type} {{Monad E}} {{State MyNat E}} {{State Nat E}} : E Nat :=
+  do {
+    s <- MyNat.theNat <$> State.get {MyNat};
+    modify ((+) s);
+    State.get
+  };
+
+addS (x y : Nat) : Nat :=
+  getAndAdd
+  |> evalState (mkMyNat y)
+  |> evalState x
+  |> run;
+
+addS' (x y : Nat) : Nat :=
+  getAndAdd
+  |> evalState x
+  |> evalState (mkMyNat y)
+  |> run;
+
 readAndAddMul {E : Type -> Type} {{Monad E}} {{Reader Nat E}} {{Reader MyNat E}} {{State Nat E}} : E Nat :=
   do {
     s <- MyNat.theNat <$> Reader.ask {MyNat};
@@ -272,5 +291,5 @@ addMul (x y z : Nat) : Nat :=
   |> run
   |> fst;
 
-main : Nat := add 1 2 + addMul 1 3 5 + add' 2 1;
+main : Nat := addS' (addS (add 1 2) (addMul 1 3 5)) (add' 2 1);
 -- result = 3 + 24 + 3 = 30