Migrate old named application syntax (#2876)

- Closes #2668

This pr migrates the old named application syntax to the new one. In
order to migrate a juvix file to the new syntax it suffices to run the
formatter.
After the next release, we should completely remove the support for the
old syntax.

## Other changes
I've improved Scope negative tests. Previously, when a negative test
failed, you could only see the title of the test and the message
"Incorrect Error", as well as the Haskell file and line where the test
is defined.
This is extremely incovenient because you have to go to the haskell test
file, go to the line where the error is defined, look at the name of the
file and then visit that file. Moreover, you need to manually run the
scoper on that file to see the error that was returned.
I've fixed that and it now shows all relevant information. Example:

![image](https://github.com/anoma/juvix/assets/5511599/f0b7ec60-55dc-4f38-9b51-1fbedbda63f4)
I've implemented this only using the `Generic` instance for the
`ScoperError` type, so doing something similar for the rest of negative
tests should be straightforward.

examples/demo/Package.juvix

@@ -3,5 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage
-    {name := "Demo"; version := mkVersion 0 1 0};
+  defaultPackage@?{
+    name := "Demo";
+    version := mkVersion 0 1 0
+  };

examples/midsquare/Package.juvix

@@ -3,5 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage
-    {name := "midsquare"; version := mkVersion 0 1 0};
+  defaultPackage@?{
+    name := "midsquare";
+    version := mkVersion 0 1 0
+  };

examples/milestone/Bank/Package.juvix

@@ -2,4 +2,7 @@ module Package;
 
 import PackageDescription.V2 open;
 
-package : Package := defaultPackage {name := "bank"};
+package : Package :=
+  defaultPackage@?{
+    name := "bank"
+  };

examples/milestone/Collatz/Package.juvix

@@ -3,7 +3,8 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage
-    {name := "Collatz";
+  defaultPackage@?{
+    name := "Collatz";
     version := mkVersion 0 1 0;
-     main := just "Collatz.juvix"};
+    main := just "Collatz.juvix"
+  };

examples/milestone/Fibonacci/Package.juvix

@@ -3,7 +3,8 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage
-    {name := "Fibonacci";
+  defaultPackage@?{
+    name := "Fibonacci";
     version := mkVersion 0 1 0;
-     main := just "Fibonacci.juvix"};
+    main := just "Fibonacci.juvix"
+  };

examples/milestone/Hanoi/Package.juvix

@@ -3,7 +3,8 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage
-    {name := "Hanoi";
+  defaultPackage@?{
+    name := "Hanoi";
     version := mkVersion 0 1 0;
-     main := just "Hanoi.juvix"};
+    main := just "Hanoi.juvix"
+  };

examples/milestone/HelloWorld/Package.juvix

@@ -3,7 +3,8 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage
-    {name := "HelloWorld";
+  defaultPackage@?{
+    name := "HelloWorld";
     version := mkVersion 0 1 0;
-     main := just "HelloWorld.juvix"};
+    main := just "HelloWorld.juvix"
+  };

examples/milestone/PascalsTriangle/Package.juvix

@@ -3,7 +3,8 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage
-    {name := "PascalsTriangle";
+  defaultPackage@?{
+    name := "PascalsTriangle";
     version := mkVersion 0 1 0;
-     main := just "PascalsTriangle.juvix"};
+    main := just "PascalsTriangle.juvix"
+  };

examples/milestone/TicTacToe/Package.juvix

@@ -3,7 +3,8 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage
-    {name := "TicTacToe";
+  defaultPackage@?{
+    name := "TicTacToe";
     version := mkVersion 0 1 0;
-     main := just "CLI/TicTacToe.juvix"};
+    main := just "CLI/TicTacToe.juvix"
+  };

examples/milestone/Tutorial/Package.juvix

@@ -3,5 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage
-    {name := "Tutorial"; version := mkVersion 0 1 0};
+  defaultPackage@?{
+    name := "Tutorial";
+    version := mkVersion 0 1 0
+  };

include/package/PackageDescription/V1.juvix

@@ -44,22 +44,28 @@ type Dependency :=
     defaultStdlib;
 
 --- Construct a ;Package; with useful default arguments.
-defaultPackage {name : String := "my-project"} {version : SemVer := defaultVersion} {dependencies : List
-  Dependency := [defaultStdlib]} {main : Maybe
-  String := nothing} {buildDir : Maybe String := nothing}
+defaultPackage
+  {name : String := "my-project"}
+  {version : SemVer := defaultVersion}
+  {dependencies : List Dependency := [defaultStdlib]}
+  {main : Maybe String := nothing}
+  {buildDir : Maybe String := nothing}
   : Package :=
   mkPackage name version dependencies main buildDir;
 
 --- Construct a ;SemVer; with useful default arguments.
-mkVersion (major minor patch : Nat) {release : Maybe
-  String := nothing} {meta : Maybe String := nothing}
+mkVersion
+  (major' minor' patch' : Nat)
+  {release' : Maybe String := nothing}
+  {meta' : Maybe String := nothing}
   : SemVer :=
-  mkSemVer
-    (major := major;
-    minor := minor;
-    patch := patch;
-    release := release;
-    meta := meta);
+  mkSemVer@?{
+    major := major';
+    minor := minor';
+    patch := patch';
+    release := release';
+    meta := meta'
+  };
 
 --- The default version used in `defaultPackage`.
 defaultVersion : SemVer := mkVersion 0 0 0;

include/package/PackageDescription/V2.juvix

@@ -44,22 +44,28 @@ type Dependency :=
     defaultStdlib;
 
 --- Construct a ;Package; with useful default arguments.
-defaultPackage {name : String := "my-project"} {version : SemVer := defaultVersion} {dependencies : List
-  Dependency := [defaultStdlib]} {main : Maybe
-  String := nothing} {buildDir : Maybe String := nothing}
+defaultPackage
+  {name : String := "my-project"}
+  {version : SemVer := defaultVersion}
+  {dependencies : List Dependency := [defaultStdlib]}
+  {main : Maybe String := nothing}
+  {buildDir : Maybe String := nothing}
   : Package :=
   mkPackage name version dependencies main buildDir;
 
 --- Construct a ;SemVer; with useful default arguments.
-mkVersion (major minor patch : Nat) {release : Maybe
-  String := nothing} {meta : Maybe String := nothing}
+mkVersion
+  (major' minor' patch' : Nat)
+  {release' : Maybe String := nothing}
+  {meta' : Maybe String := nothing}
   : SemVer :=
-  mkSemVer
-    (major := major;
-    minor := minor;
-    patch := patch;
-    release := release;
-    meta := meta);
+  mkSemVer@?{
+    major := major';
+    minor := minor';
+    patch := patch';
+    release := release';
+    meta := meta'
+  };
 
 --- The default version used in `defaultPackage`.
 defaultVersion : SemVer := mkVersion 0 0 0;

src/Juvix/Compiler/Concrete/Gen.hs

@@ -5,7 +5,7 @@ module Juvix.Compiler.Concrete.Gen
 where
 
 import Juvix.Compiler.Concrete.Keywords
-import Juvix.Compiler.Concrete.Language
+import Juvix.Compiler.Concrete.Language.Base
 import Juvix.Prelude
 
 kw :: (Members '[Reader Interval] r) => Keyword -> Sem r KeywordRef
@@ -18,6 +18,22 @@ kw k = do
         _keywordRefInterval = loc
       }
 
+simplestFunctionDef :: FunctionName s -> ExpressionType s -> FunctionDef s
+simplestFunctionDef funName funBody =
+  FunctionDef
+    { _signName = funName,
+      _signBody = SigBodyExpression funBody,
+      _signColonKw = Irrelevant Nothing,
+      _signArgs = [],
+      _signRetType = Nothing,
+      _signDoc = Nothing,
+      _signPragmas = Nothing,
+      _signBuiltin = Nothing,
+      _signTerminating = Nothing,
+      _signInstance = Nothing,
+      _signCoercion = Nothing
+    }
+
 smallUniverseExpression :: forall s r. (SingI s) => (Members '[Reader Interval] r) => Sem r (ExpressionType s)
 smallUniverseExpression = do
   loc <- ask @Interval
@@ -29,6 +45,16 @@ smallUniverseExpression = do
           _expressionAtoms = pure (AtomUniverse (smallUniverse loc))
         }
 
+isExhaustive :: (Member (Reader Interval) r) => Bool -> Sem r IsExhaustive
+isExhaustive _isExhaustive = do
+  _isExhaustiveKw <-
+    Irrelevant
+      <$> if
+          | _isExhaustive -> kw kwAt
+          | otherwise -> kw kwAtQuestion
+
+  return IsExhaustive {..}
+
 symbol :: (Member (Reader Interval) r) => Text -> Sem r Symbol
 symbol t = do
   l <- ask
@@ -39,12 +65,12 @@ expressionAtoms' _expressionAtoms = do
   _expressionAtomsLoc <- Irrelevant <$> ask
   return ExpressionAtoms {..}
 
-namedArgument :: (Member (Reader Interval) r) => Text -> NonEmpty (ExpressionAtom 'Parsed) -> Sem r (NamedArgument 'Parsed)
+namedArgument :: (Member (Reader Interval) r) => Text -> NonEmpty (ExpressionAtom 'Parsed) -> Sem r (NamedArgumentAssign 'Parsed)
 namedArgument n as = do
   _namedArgValue <- expressionAtoms' as
   _namedArgName <- symbol n
   _namedArgAssignKw <- Irrelevant <$> kw kwAssign
-  return NamedArgument {..}
+  return NamedArgumentAssign {..}
 
 literalString :: (Member (Reader Interval) r) => Text -> Sem r (ExpressionAtom s)
 literalString t = do
@@ -59,7 +85,7 @@ braced a = do
   l <- ask
   AtomBraces . WithLoc l <$> expressionAtoms' a
 
-argumentBlock :: (Member (Reader Interval) r) => IsImplicit -> NonEmpty (NamedArgument 'Parsed) -> Sem r (ArgumentBlock 'Parsed)
+argumentBlock :: (Member (Reader Interval) r) => IsImplicit -> NonEmpty (NamedArgumentAssign 'Parsed) -> Sem r (ArgumentBlock 'Parsed)
 argumentBlock i as = do
   parenL <- kw delimL
   parenR <- kw delimR
@@ -109,5 +135,8 @@ mkList as = do
           }
     )
 
-functionDefExpression :: (Member (Reader Interval) r) => NonEmpty (ExpressionAtom 'Parsed) -> Sem r (FunctionDefBody 'Parsed)
+functionDefExpression ::
+  (Member (Reader Interval) r) =>
+  NonEmpty (ExpressionAtom 'Parsed) ->
+  Sem r (FunctionDefBody 'Parsed)
 functionDefExpression exp = SigBodyExpression <$> expressionAtoms' exp

src/Juvix/Compiler/Concrete/Language/IsApeInstances.hs

@@ -0,0 +1,198 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Juvix.Compiler.Concrete.Language.IsApeInstances where
+
+import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
+import Juvix.Compiler.Concrete.Language.Base
+import Juvix.Compiler.Concrete.MigrateNamedApplication
+import Juvix.Data.Ape.Base as Ape
+import Juvix.Data.NameKind
+import Juvix.Parser.Lexer (isDelimiterStr)
+import Juvix.Prelude
+import Juvix.Prelude.Pretty (prettyText)
+
+instance IsApe PatternApp ApeLeaf where
+  toApe (PatternApp l r) =
+    ApeApp
+      Ape.App
+        { _appLeft = toApe l,
+          _appRight = toApe r
+        }
+
+instance IsApe Pattern ApeLeaf where
+  toApe = \case
+    PatternApplication a -> toApe a
+    PatternInfixApplication a -> toApe a
+    PatternPostfixApplication a -> toApe a
+    e ->
+      ApeLeaf
+        Leaf
+          { _leafAtomicity = atomicity e,
+            _leafExpr = ApeLeafPattern e
+          }
+
+instance IsApe PatternArg ApeLeaf where
+  toApe pa
+    | Atom == atomicity pa =
+        ApeLeaf
+          Leaf
+            { _leafAtomicity = Atom,
+              _leafExpr = ApeLeafPatternArg pa
+            }
+    | otherwise = toApe (pa ^. patternArgPattern)
+
+instance IsApe PatternPostfixApp ApeLeaf where
+  toApe p@(PatternPostfixApp l op) =
+    ApePostfix
+      Postfix
+        { _postfixFixity = getFixity p,
+          _postfixLeft = toApe l,
+          _postfixOp = ApeLeafPattern (PatternConstructor op)
+        }
+
+instance IsApe PatternInfixApp ApeLeaf where
+  toApe i@(PatternInfixApp l op r) =
+    ApeInfix
+      Infix
+        { _infixFixity = getFixity i,
+          _infixLeft = toApe l,
+          _infixRight = toApe r,
+          _infixIsDelimiter = isDelimiterStr (prettyText (op ^. scopedIdenSrcName . S.nameConcrete)),
+          _infixOp = ApeLeafPattern (PatternConstructor op)
+        }
+
+instance IsApe ScopedIden ApeLeaf where
+  toApe iden =
+    ApeLeaf
+      Leaf
+        { _leafAtomicity = Atom,
+          _leafExpr = ApeLeafExpression (ExpressionIdentifier iden)
+        }
+
+toApeIdentifierType :: forall s. (SingI s) => IdentifierType s -> Ape ApeLeaf
+toApeIdentifierType = case sing :: SStage s of
+  SParsed -> toApe
+  SScoped -> toApe
+
+instance IsApe Name ApeLeaf where
+  toApe n =
+    ApeLeaf
+      Leaf
+        { _leafAtomicity = atomicity n,
+          _leafExpr = ApeLeafAtom (sing :&: AtomIdentifier n)
+        }
+
+instance (SingI s) => IsApe (NamedApplication s) ApeLeaf where
+  toApe = toApe . migrateNamedApplication
+
+-- f = toApeIdentifierType _namedAppName
+
+instance (SingI s) => IsApe (NamedApplicationNew s) ApeLeaf where
+  toApe a =
+    ApeLeaf $
+      Leaf
+        { _leafAtomicity = atomicity a,
+          _leafExpr = ApeLeafAtom (sing :&: AtomNamedApplicationNew a)
+        }
+
+instance IsApe Application ApeLeaf where
+  toApe (Application l r) =
+    ApeApp
+      Ape.App
+        { _appLeft = toApe l,
+          _appRight = toApe r
+        }
+
+instance IsApe InfixApplication ApeLeaf where
+  toApe i@(InfixApplication l op r) =
+    ApeInfix
+      Infix
+        { _infixFixity = getFixity i,
+          _infixLeft = toApe l,
+          _infixRight = toApe r,
+          _infixIsDelimiter = isDelimiterStr (prettyText (op ^. scopedIdenSrcName . S.nameConcrete)),
+          _infixOp = ApeLeafExpression (ExpressionIdentifier op)
+        }
+
+instance IsApe PostfixApplication ApeLeaf where
+  toApe p@(PostfixApplication l op) =
+    ApePostfix
+      Postfix
+        { _postfixFixity = getFixity p,
+          _postfixLeft = toApe l,
+          _postfixOp = ApeLeafExpression (ExpressionIdentifier op)
+        }
+
+instance IsApe (Function 'Scoped) ApeLeaf where
+  toApe (Function ps kw ret) =
+    ApeInfix
+      Infix
+        { _infixFixity = funFixity,
+          _infixLeft = toApe ps,
+          _infixRight = toApe ret,
+          _infixIsDelimiter = False,
+          _infixOp = ApeLeafFunctionKw kw
+        }
+
+instance IsApe RecordUpdateApp ApeLeaf where
+  toApe :: RecordUpdateApp -> Ape ApeLeaf
+  toApe a =
+    ApePostfix
+      Postfix
+        { _postfixFixity = updateFixity,
+          _postfixOp = ApeLeafAtom (sing :&: AtomRecordUpdate (a ^. recordAppUpdate)),
+          _postfixLeft = toApe (a ^. recordAppExpression)
+        }
+
+instance IsApe Expression ApeLeaf where
+  toApe e = case e of
+    ExpressionApplication a -> toApe a
+    ExpressionInfixApplication a -> toApe a
+    ExpressionPostfixApplication a -> toApe a
+    ExpressionFunction a -> toApe a
+    ExpressionNamedApplication a -> toApe a
+    ExpressionNamedApplicationNew a -> toApe a
+    ExpressionRecordUpdate a -> toApe a
+    ExpressionParensRecordUpdate {} -> leaf
+    ExpressionParensIdentifier {} -> leaf
+    ExpressionIdentifier {} -> leaf
+    ExpressionList {} -> leaf
+    ExpressionCase {} -> leaf
+    ExpressionIf {} -> leaf
+    ExpressionLambda {} -> leaf
+    ExpressionLet {} -> leaf
+    ExpressionUniverse {} -> leaf
+    ExpressionHole {} -> leaf
+    ExpressionInstanceHole {} -> leaf
+    ExpressionLiteral {} -> leaf
+    ExpressionBraces {} -> leaf
+    ExpressionDoubleBraces {} -> leaf
+    ExpressionIterator {} -> leaf
+    where
+      leaf =
+        ApeLeaf
+          Leaf
+            { _leafAtomicity = atomicity e,
+              _leafExpr = ApeLeafExpression e
+            }
+
+instance IsApe (FunctionParameters 'Scoped) ApeLeaf where
+  toApe f
+    | atomicity f == Atom =
+        ApeLeaf
+          Leaf
+            { _leafAtomicity = Atom,
+              _leafExpr = ApeLeafFunctionParams f
+            }
+    | otherwise = toApe (f ^. paramType)
+
+instance HasAtomicity PatternArg where
+  atomicity p
+    | Implicit <- p ^. patternArgIsImplicit = Atom
+    | ImplicitInstance <- p ^. patternArgIsImplicit = Atom
+    | isJust (p ^. patternArgName) = Atom
+    | otherwise = atomicity (p ^. patternArgPattern)
+
+instance HasNameKind ScopedIden where
+  getNameKind = getNameKind . (^. scopedIdenFinal)
+  getNameKindPretty = getNameKindPretty . (^. scopedIdenFinal)

src/Juvix/Compiler/Concrete/MigrateNamedApplication.hs

@@ -0,0 +1,29 @@
+module Juvix.Compiler.Concrete.MigrateNamedApplication where
+
+import Juvix.Compiler.Concrete.Gen qualified as Gen
+import Juvix.Compiler.Concrete.Keywords
+import Juvix.Compiler.Concrete.Language.Base
+import Juvix.Prelude
+
+migrateNamedApplication :: forall s. (SingI s) => NamedApplication s -> NamedApplicationNew s
+migrateNamedApplication old@NamedApplication {..} = run . runReader (getLoc old) $ do
+  _namedApplicationNewAtKw <- Irrelevant <$> Gen.kw kwAt
+  _namedApplicationNewExhaustive <- Gen.isExhaustive False
+  return
+    NamedApplicationNew
+      { _namedApplicationNewName = _namedAppName,
+        _namedApplicationNewArguments = migrateNamedApplicationArguments (toList _namedAppArgs),
+        _namedApplicationNewExhaustive
+      }
+  where
+    migrateNamedApplicationArguments :: [ArgumentBlock s] -> [NamedArgumentNew s]
+    migrateNamedApplicationArguments = concatMap goBlock
+      where
+        goBlock :: ArgumentBlock s -> [NamedArgumentNew s]
+        goBlock ArgumentBlock {..} = map goArg (toList _argBlockArgs)
+          where
+            goArg :: NamedArgumentAssign s -> NamedArgumentNew s
+            goArg = NamedArgumentNewFunction . NamedArgumentFunctionDef . toFun
+
+            toFun :: NamedArgumentAssign s -> FunctionDef s
+            toFun NamedArgumentAssign {..} = Gen.simplestFunctionDef _namedArgName _namedArgValue

src/Juvix/Compiler/Concrete/Print/Base.hs

@@ -17,6 +17,7 @@ import Juvix.Compiler.Concrete.Gen qualified as Gen
 import Juvix.Compiler.Concrete.Keywords
 import Juvix.Compiler.Concrete.Keywords qualified as Kw
 import Juvix.Compiler.Concrete.Language
+import Juvix.Compiler.Concrete.MigrateNamedApplication
 import Juvix.Compiler.Concrete.Pretty.Options
 import Juvix.Compiler.Concrete.Translation.ImportScanner.Base
 import Juvix.Compiler.Pipeline.Loader.PathResolver.Data
@@ -294,9 +295,9 @@ instance (SingI s) => PrettyPrint (List s) where
         es = vcatPreSemicolon (map ppExpressionType _listItems)
     grouped (align (l <> spaceOrEmpty <> es <> lineOrEmpty <> r))
 
-instance (SingI s) => PrettyPrint (NamedArgument s) where
-  ppCode NamedArgument {..} = do
-    let s = ppCode _namedArgName
+instance (SingI s) => PrettyPrint (NamedArgumentAssign s) where
+  ppCode NamedArgumentAssign {..} = do
+    let s = ppSymbolType _namedArgName
         kwassign = ppCode _namedArgAssignKw
         val = ppExpressionType _namedArgValue
     s <+> kwassign <+> val
@@ -312,24 +313,30 @@ instance (SingI s) => PrettyPrint (ArgumentBlock s) where
       Irrelevant d = _argBlockDelims
 
 instance (SingI s) => PrettyPrint (NamedApplication s) where
-  ppCode = apeHelper
+  ppCode = ppCode . migrateNamedApplication
+
+instance PrettyPrint IsExhaustive where
+  ppCode IsExhaustive {..} = ppCode _isExhaustiveKw
 
 instance (SingI s) => PrettyPrint (NamedApplicationNew s) where
   ppCode NamedApplicationNew {..} = do
     let args'
           | null _namedApplicationNewArguments = mempty
           | otherwise =
-              blockIndent
-                ( sequenceWith
+              blockIndent $
+                sequenceWith
                   (semicolon >> line)
                   (ppCode <$> _namedApplicationNewArguments)
-                )
     ppIdentifierType _namedApplicationNewName
-      <> ppCode _namedApplicationNewAtKw
+      <> ppCode _namedApplicationNewExhaustive
       <> braces args'
 
+instance (SingI s) => PrettyPrint (NamedArgumentFunctionDef s) where
+  ppCode (NamedArgumentFunctionDef f) = ppCode f
+
 instance (SingI s) => PrettyPrint (NamedArgumentNew s) where
-  ppCode NamedArgumentNew {..} = ppCode _namedArgumentNewFunDef
+  ppCode = \case
+    NamedArgumentNewFunction f -> ppCode f
 
 instance (SingI s) => PrettyPrint (RecordStatement s) where
   ppCode = \case
@@ -668,7 +675,6 @@ instance PrettyPrint ApeLeaf where
     ApeLeafPattern r -> ppCode r
     ApeLeafPatternArg r -> ppCode r
     ApeLeafAtom r -> ppAnyStage r
-    ApeLeafArgumentBlock r -> ppAnyStage r
 
 annDef :: forall s r. (SingI s, Members '[ExactPrint] r) => SymbolType s -> Sem r () -> Sem r ()
 annDef nm = case sing :: SStage s of

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs

@@ -1099,6 +1099,7 @@ checkFunctionDef FunctionDef {..} = do
     checkBody = case _signBody of
       SigBodyExpression e -> SigBodyExpression <$> checkParseExpressionAtoms e
       SigBodyClauses cls -> SigBodyClauses <$> mapM checkClause cls
+
     checkClause :: FunctionClause 'Parsed -> Sem r (FunctionClause 'Scoped)
     checkClause FunctionClause {..} = do
       (patterns', body') <- withLocalScope $ do
@@ -2569,6 +2570,10 @@ checkExpressionAtom e = case e of
   AtomNamedApplicationNew i -> pure . AtomNamedApplicationNew <$> checkNamedApplicationNew i
   AtomRecordUpdate i -> pure . AtomRecordUpdate <$> checkRecordUpdate i
 
+reserveNamedArgumentName :: (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) => NamedArgumentNew 'Parsed -> Sem r ()
+reserveNamedArgumentName a = case a of
+  NamedArgumentNewFunction f -> void (reserveFunctionSymbol (f ^. namedArgumentFunctionDef))
+
 checkNamedApplicationNew :: forall r. (Members '[HighlightBuilder, Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => NamedApplicationNew 'Parsed -> Sem r (NamedApplicationNew 'Scoped)
 checkNamedApplicationNew napp = do
   let nargs = napp ^. namedApplicationNewArguments
@@ -2576,18 +2581,21 @@ checkNamedApplicationNew napp = do
   sig <- if null nargs then return $ NameSignature [] else getNameSignature aname
   let snames = HashSet.fromList (concatMap (HashMap.keys . (^. nameBlock)) (sig ^. nameSignatureArgs))
   args' <- withLocalScope . localBindings . ignoreSyntax $ do
-    mapM_ (reserveFunctionSymbol . (^. namedArgumentNewFunDef)) nargs
+    mapM_ reserveNamedArgumentName nargs
     mapM (checkNamedArgumentNew snames) nargs
-  let enames = HashSet.fromList (concatMap (HashMap.keys . (^. nameBlock)) (filter (not . isImplicitOrInstance . (^. nameImplicit)) (sig ^. nameSignatureArgs)))
-      sargs = HashSet.fromList (map (^. namedArgumentNewFunDef . signName . nameConcrete) (toList args'))
+  let enames =
+        HashSet.fromList
+          . concatMap (HashMap.keys . (^. nameBlock))
+          . filter (not . isImplicitOrInstance . (^. nameImplicit))
+          $ sig ^. nameSignatureArgs
+      sargs :: HashSet Symbol = hashSet (map (^. namedArgumentNewSymbol) nargs)
       missingArgs = HashSet.difference enames sargs
-  unless (null missingArgs || not (napp ^. namedApplicationNewExhaustive)) $
+  unless (null missingArgs || not (napp ^. namedApplicationNewExhaustive . isExhaustive)) $
     throw (ErrMissingArgs (MissingArgs (aname ^. scopedIdenFinal . nameConcrete) missingArgs))
   return
     NamedApplicationNew
       { _namedApplicationNewName = aname,
         _namedApplicationNewArguments = args',
-        _namedApplicationNewAtKw = napp ^. namedApplicationNewAtKw,
         _namedApplicationNewExhaustive = napp ^. namedApplicationNewExhaustive
       }
 
@@ -2596,14 +2604,22 @@ checkNamedArgumentNew ::
   HashSet Symbol ->
   NamedArgumentNew 'Parsed ->
   Sem r (NamedArgumentNew 'Scoped)
-checkNamedArgumentNew snames NamedArgumentNew {..} = do
-  def <- localBindings . ignoreSyntax $ checkFunctionDef _namedArgumentNewFunDef
+checkNamedArgumentNew snames = \case
+  NamedArgumentNewFunction f -> NamedArgumentNewFunction <$> checkNamedArgumentFunctionDef snames f
+
+checkNamedArgumentFunctionDef ::
+  (Members '[HighlightBuilder, Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) =>
+  HashSet Symbol ->
+  NamedArgumentFunctionDef 'Parsed ->
+  Sem r (NamedArgumentFunctionDef 'Scoped)
+checkNamedArgumentFunctionDef snames NamedArgumentFunctionDef {..} = do
+  def <- localBindings . ignoreSyntax $ checkFunctionDef _namedArgumentFunctionDef
   let fname = def ^. signName . nameConcrete
   unless (HashSet.member fname snames) $
     throw (ErrUnexpectedArgument (UnexpectedArgument fname))
   return
-    NamedArgumentNew
-      { _namedArgumentNewFunDef = def
+    NamedArgumentFunctionDef
+      { _namedArgumentFunctionDef = def
       }
 
 checkRecordUpdate :: forall r. (Members '[HighlightBuilder, Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => RecordUpdate 'Parsed -> Sem r (RecordUpdate 'Scoped)
@@ -2658,20 +2674,24 @@ checkNamedApplication napp = do
   _namedAppArgs <- mapM checkArgumentBlock (napp ^. namedAppArgs)
   return NamedApplication {..}
   where
-    checkNamedArg :: NamedArgument 'Parsed -> Sem r (NamedArgument 'Scoped)
-    checkNamedArg n = do
-      let _namedArgName = n ^. namedArgName
-          _namedArgAssignKw = n ^. namedArgAssignKw
-      _namedArgValue <- checkParseExpressionAtoms (n ^. namedArgValue)
-      return NamedArgument {..}
-
     checkArgumentBlock :: ArgumentBlock 'Parsed -> Sem r (ArgumentBlock 'Scoped)
     checkArgumentBlock b = do
       let _argBlockDelims = b ^. argBlockDelims
           _argBlockImplicit = b ^. argBlockImplicit
-      _argBlockArgs <- mapM checkNamedArg (b ^. argBlockArgs)
+      _argBlockArgs <- mapM checkNamedArgumentAssign (b ^. argBlockArgs)
       return ArgumentBlock {..}
 
+checkNamedArgumentAssign ::
+  forall r.
+  (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) =>
+  NamedArgumentAssign 'Parsed ->
+  Sem r (NamedArgumentAssign 'Scoped)
+checkNamedArgumentAssign n = do
+  _namedArgName <- withLocalScope (bindVariableSymbol (n ^. namedArgName))
+  let _namedArgAssignKw = n ^. namedArgAssignKw
+  _namedArgValue <- checkParseExpressionAtoms (n ^. namedArgValue)
+  return NamedArgumentAssign {..}
+
 getRecordInfo ::
   forall r.
   (Members '[State ScoperState, Error ScoperError] r) =>

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs

@@ -10,6 +10,7 @@ import Juvix.Compiler.Concrete.Data.NameSignature.Error
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Pretty
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Types
 import Juvix.Compiler.Internal.Translation.FromConcrete.NamedArguments.Error
+import Juvix.Prelude.Base.Foundation
 
 data ScoperError
   = ErrInfixParser InfixError
@@ -55,6 +56,7 @@ data ScoperError
   | ErrWrongDefaultValue WrongDefaultValue
   | ErrUnsupported Unsupported
   | ErrDefaultArgCycle DefaultArgCycle
+  deriving stock (Generic)
 
 instance ToGenericError ScoperError where
   genericError = \case

src/Juvix/Compiler/Concrete/Translation/FromSource.hs

@@ -869,10 +869,6 @@ pdoubleBracesExpression = do
             _expressionAtomsLoc = Irrelevant i
           }
 
---------------------------------------------------------------------------------
--- Iterators
---------------------------------------------------------------------------------
-
 iterator ::
   forall r.
   (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
@@ -967,36 +963,60 @@ iterator = do
       s <- P.try rangeStart
       rangeCont s
 
-    mkNamedArgument :: Int -> Initializer 'Parsed -> ParsecS r (NamedArgument 'Parsed)
+    mkNamedArgument :: Int -> Initializer 'Parsed -> ParsecS r (NamedArgumentAssign 'Parsed)
     mkNamedArgument off Initializer {..} = do
       let _namedArgAssignKw = _initializerAssignKw
           _namedArgValue = _initializerExpression
       _namedArgName <- case _initializerPattern ^. patternAtoms of
         PatternAtomIden (NameUnqualified n) :| [] -> return n
         _ -> parseFailure off "an iterator must have at least one range"
-      return NamedArgument {..}
+      return NamedArgumentAssign {..}
+
+pnamedArgumentFunctionDef ::
+  forall r.
+  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  ParsecS r (NamedArgumentFunctionDef 'Parsed)
+pnamedArgumentFunctionDef = do
+  fun <- functionDefinition True False Nothing
+  return
+    NamedArgumentFunctionDef
+      { _namedArgumentFunctionDef = fun
+      }
+
+namedArgumentNew ::
+  forall r.
+  (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
+  ParsecS r (NamedArgumentNew 'Parsed)
+namedArgumentNew = NamedArgumentNewFunction <$> pnamedArgumentFunctionDef
+
+pisExhaustive ::
+  forall r.
+  (Members '[ParserResultBuilder] r) =>
+  ParsecS r IsExhaustive
+pisExhaustive = do
+  (keyword, exh) <-
+    (,False) <$> kw kwAtQuestion
+      <|> (,True) <$> kw kwAt
+  return
+    IsExhaustive
+      { _isExhaustiveKw = Irrelevant keyword,
+        _isExhaustive = exh
+      }
 
 namedApplicationNew ::
   forall r.
   (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
   ParsecS r (NamedApplicationNew 'Parsed)
 namedApplicationNew = P.label "<named application>" $ do
-  (_namedApplicationNewName, _namedApplicationNewAtKw, _namedApplicationNewExhaustive) <- P.try $ do
+  (_namedApplicationNewName, _namedApplicationNewExhaustive) <- P.try $ do
     n <- name
-    (a, b) <- first Irrelevant <$> ((,False) <$> kw kwAtQuestion <|> (,True) <$> kw kwAt)
+    exhaustive <- pisExhaustive
     lbrace
-    return (n, a, b)
-  defs <- P.sepEndBy (functionDefinition True False Nothing) semicolon
+    return (n, exhaustive)
+  _namedApplicationNewArguments <- P.sepEndBy namedArgumentNew semicolon
   rbrace
-  let _namedApplicationNewArguments = fmap mkArg defs
-      _namedApplicationNewExtra = Irrelevant ()
+  let _namedApplicationNewExtra = Irrelevant ()
   return NamedApplicationNew {..}
-  where
-    mkArg :: FunctionDef 'Parsed -> NamedArgumentNew 'Parsed
-    mkArg f =
-      NamedArgumentNew
-        { _namedArgumentNewFunDef = f
-        }
 
 namedApplication ::
   forall r.
@@ -1013,15 +1033,15 @@ namedApplication = P.label "<named application>" $ do
       _namedAppSignature = Irrelevant ()
   return NamedApplication {..}
 
-namedArgument ::
+namedArgumentAssign ::
   forall r.
   (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) =>
-  ParsecS r (NamedArgument 'Parsed)
-namedArgument = do
+  ParsecS r (NamedArgumentAssign 'Parsed)
+namedArgumentAssign = do
   _namedArgName <- symbol
   _namedArgAssignKw <- Irrelevant <$> kw kwAssign
   _namedArgValue <- parseExpressionAtoms
-  return NamedArgument {..}
+  return NamedArgumentAssign {..}
 
 argumentBlockStart ::
   forall r.
@@ -1040,8 +1060,8 @@ argumentBlockCont ::
   ParsecS r (ArgumentBlock 'Parsed)
 argumentBlockCont (l, _argBlockImplicit, _namedArgName, _namedArgAssignKw) = do
   _namedArgValue <- parseExpressionAtoms
-  let arg = NamedArgument {..}
-  _argBlockArgs <- nonEmpty' . (arg :) <$> many (semicolon >> namedArgument)
+  let arg = NamedArgumentAssign {..}
+  _argBlockArgs <- nonEmpty' . (arg :) <$> many (semicolon >> namedArgumentAssign)
   r <- implicitClose _argBlockImplicit
   let _argBlockDelims = Irrelevant (Just (l, r))
   return ArgumentBlock {..}

src/Juvix/Compiler/Internal/Extra.hs

@@ -170,8 +170,8 @@ buildLetMutualBlocks ss = nonEmpty' . mapMaybe nameToPreStatement $ scomponents
           AcyclicSCC a -> AcyclicSCC <$> a
           CyclicSCC p -> CyclicSCC . toList <$> nonEmpty (catMaybes p)
 
-mkLetClauses :: NonEmpty PreLetStatement -> [LetClause]
-mkLetClauses pre = goSCC <$> (toList (buildLetMutualBlocks pre))
+mkLetClauses :: NonEmpty PreLetStatement -> NonEmpty LetClause
+mkLetClauses pre = goSCC <$> buildLetMutualBlocks pre
   where
     goSCC :: SCC PreLetStatement -> LetClause
     goSCC = \case

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -719,6 +719,49 @@ goListPattern l = do
   where
     loc = getLoc l
 
+createArgumentBlocks :: NonEmpty (NamedArgumentNew 'Scoped) -> [NameBlock 'Scoped] -> [ArgumentBlock 'Scoped]
+createArgumentBlocks appargs =
+  run
+    . execOutputList
+    . evalState args0
+    . mapM_ goBlock
+  where
+    args0 :: HashSet S.Symbol = hashSet ((^. namedArgumentNewSymbol) <$> appargs)
+    goBlock ::
+      forall r.
+      (Members '[State (HashSet S.Symbol), Output (ArgumentBlock 'Scoped)] r) =>
+      NameBlock 'Scoped ->
+      Sem r ()
+    goBlock NameBlock {..} = do
+      args <- get
+      let namesInBlock :: HashSet Symbol =
+            HashSet.intersection
+              (HashMap.keysSet _nameBlock)
+              (HashSet.map (^. S.nameConcrete) args)
+          argNames :: HashMap Symbol S.Symbol = hashMap . map (\n -> (n ^. S.nameConcrete, n)) $ toList args
+          getName sym = fromJust (argNames ^. at sym)
+      whenJust (nonEmpty namesInBlock) $ \(namesInBlock1 :: NonEmpty Symbol) -> do
+        let block' =
+              ArgumentBlock
+                { _argBlockDelims = Irrelevant Nothing,
+                  _argBlockImplicit = _nameImplicit,
+                  _argBlockArgs = goArg . getName <$> namesInBlock1
+                }
+        modify (HashSet.filter (not . flip HashSet.member namesInBlock . (^. S.nameConcrete)))
+        output block'
+      where
+        goArg :: S.Symbol -> NamedArgumentAssign 'Scoped
+        goArg sym =
+          NamedArgumentAssign
+            { _namedArgName = sym,
+              _namedArgAssignKw = Irrelevant dummyKw,
+              _namedArgValue = Concrete.ExpressionIdentifier (ScopedIden name Nothing)
+            }
+          where
+            name :: S.Name = over S.nameConcrete NameUnqualified sym
+            dummyKw = run (runReader dummyLoc (Gen.kw Gen.kwAssign))
+            dummyLoc = getLoc sym
+
 goExpression ::
   forall r.
   (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) =>
@@ -753,71 +796,41 @@ goExpression = \case
       s <- asks (^. S.infoNameSigs)
       runReader s (runNamedArguments w extraArgs) >>= goDesugaredNamedApplication
 
-    goNamedApplicationNew :: Concrete.NamedApplicationNew 'Scoped -> [Internal.ApplicationArg] -> Sem r Internal.Expression
+    goNamedApplicationNew ::
+      Concrete.NamedApplicationNew 'Scoped ->
+      [Internal.ApplicationArg] ->
+      Sem r Internal.Expression
     goNamedApplicationNew napp extraArgs = case nonEmpty (napp ^. namedApplicationNewArguments) of
       Nothing -> return (goIden (napp ^. namedApplicationNewName))
       Just appargs -> do
         let name = napp ^. namedApplicationNewName . scopedIdenFinal
         sig <- fromJust <$> asks (^. S.infoNameSigs . at (name ^. S.nameId))
-        cls <- goArgs appargs
-        let args :: [Internal.Name] = appargs ^.. each . namedArgumentNewFunDef . signName . to goSymbol
-            -- changes the kind from Variable to Function
-            updateKind :: Internal.Subs = Internal.subsKind args KNameFunction
-            napp' =
+        let napp' =
               Concrete.NamedApplication
                 { _namedAppName = napp ^. namedApplicationNewName,
-                  _namedAppArgs = nonEmpty' (createArgumentBlocks (sig ^. nameSignatureArgs))
+                  _namedAppArgs = nonEmpty' (createArgumentBlocks appargs (sig ^. nameSignatureArgs))
                 }
-        e <- goNamedApplication napp' extraArgs
+        compiledNameApp <- goNamedApplication napp' extraArgs
+        case nonEmpty (appargs ^.. each . _NamedArgumentNewFunction) of
+          Nothing -> return compiledNameApp
+          Just funs -> do
+            cls <- funDefsToClauses funs
+            let funsNames :: [Internal.Name] = funs ^.. each . namedArgumentFunctionDef . signName . to goSymbol
+                -- changes the kind from Variable to Function
+                updateKind :: Internal.Subs = Internal.subsKind funsNames KNameFunction
             let l =
                   Internal.Let
                     { _letClauses = cls,
-                  _letExpression = e
+                      _letExpression = compiledNameApp
                     }
-        expr <-
-          Internal.substitutionE updateKind l
-            >>= Internal.inlineLet
+            expr <- Internal.substitutionE updateKind l >>= Internal.inlineLet
             Internal.clone expr
             where
-          goArgs :: NonEmpty (NamedArgumentNew 'Scoped) -> Sem r (NonEmpty Internal.LetClause)
-          goArgs args = nonEmpty' . mkLetClauses <$> mapM goArg args
+              funDefsToClauses :: NonEmpty (NamedArgumentFunctionDef 'Scoped) -> Sem r (NonEmpty Internal.LetClause)
+              funDefsToClauses args = mkLetClauses <$> mapM goArg args
                 where
-              goArg :: NamedArgumentNew 'Scoped -> Sem r Internal.PreLetStatement
-              goArg = fmap Internal.PreLetFunctionDef . goFunctionDef . (^. namedArgumentNewFunDef)
-
-          createArgumentBlocks :: [NameBlock 'Scoped] -> [ArgumentBlock 'Scoped]
-          createArgumentBlocks = snd . foldr goBlock (args0, [])
-            where
-              args0 :: HashSet S.Symbol = HashSet.fromList $ fmap (^. namedArgumentNewFunDef . signName) (toList appargs)
-              goBlock :: NameBlock 'Scoped -> (HashSet S.Symbol, [ArgumentBlock 'Scoped]) -> (HashSet S.Symbol, [ArgumentBlock 'Scoped])
-              goBlock NameBlock {..} (args, blocks)
-                | null namesInBlock = (args', blocks)
-                | otherwise = (args', block' : blocks)
-                where
-                  namesInBlock =
-                    HashSet.intersection
-                      (HashSet.fromList (HashMap.keys _nameBlock))
-                      (HashSet.map (^. S.nameConcrete) args)
-                  argNames = HashMap.fromList . map (\n -> (n ^. S.nameConcrete, n)) $ toList args
-                  args' = HashSet.filter (not . flip HashSet.member namesInBlock . (^. S.nameConcrete)) args
-                  _argBlockArgs = nonEmpty' (map goArg (toList namesInBlock))
-                  block' =
-                    ArgumentBlock
-                      { _argBlockDelims = Irrelevant Nothing,
-                        _argBlockImplicit = _nameImplicit,
-                        _argBlockArgs
-                      }
-                  goArg :: Symbol -> NamedArgument 'Scoped
-                  goArg sym =
-                    NamedArgument
-                      { _namedArgName = sym,
-                        _namedArgAssignKw = Irrelevant dummyKw,
-                        _namedArgValue = Concrete.ExpressionIdentifier (ScopedIden name Nothing)
-                      }
-                    where
-                      name = over S.nameConcrete NameUnqualified $ fromJust $ HashMap.lookup sym argNames
-                      dummyKw = run (runReader dummyLoc (Gen.kw Gen.kwAssign))
-                      dummyLoc = getLoc sym
+                  goArg :: NamedArgumentFunctionDef 'Scoped -> Sem r Internal.PreLetStatement
+                  goArg = fmap Internal.PreLetFunctionDef . goFunctionDef . (^. namedArgumentFunctionDef)
 
     goDesugaredNamedApplication :: DesugaredNamedApplication -> Sem r Internal.Expression
     goDesugaredNamedApplication a = do
@@ -977,7 +990,7 @@ goExpression = \case
         Nothing -> _letExpression
 
     goLetFunDefs :: NonEmpty (LetStatement 'Scoped) -> Sem r [Internal.LetClause]
-    goLetFunDefs clauses = maybe [] mkLetClauses . nonEmpty <$> preLetStatements clauses
+    goLetFunDefs clauses = maybe [] (toList . mkLetClauses) . nonEmpty <$> preLetStatements clauses
       where
         preLetStatements :: NonEmpty (LetStatement 'Scoped) -> Sem r [Internal.PreLetStatement]
         preLetStatements cl = mapMaybeM preLetStatement (toList cl)

src/Juvix/Compiler/Internal/Translation/FromConcrete/NamedArguments.hs

@@ -137,7 +137,7 @@ helper loc = do
             (Implicit, Explicit) -> return mempty
             (ImplicitInstance, Explicit) -> return mempty
 
-    nextArgumentGroup :: Sem r (Maybe (IsImplicit, [NamedArgument 'Scoped], Bool))
+    nextArgumentGroup :: Sem r (Maybe (IsImplicit, [NamedArgumentAssign 'Scoped], Bool))
     nextArgumentGroup = do
       remb <- gets (^. stateRemainingArgs)
       case remb of
@@ -149,8 +149,8 @@ helper loc = do
           modify' (set stateRemainingArgs rem')
           return (Just (impl, concatMap (toList . (^. argBlockArgs)) (b : c), isLastBlock))
 
-    checkRepeated :: [NamedArgument 'Scoped] -> Sem r ()
-    checkRepeated args = whenJust (nonEmpty (findRepeated (map (^. namedArgName) args))) $ \reps ->
+    checkRepeated :: [NamedArgumentAssign 'Scoped] -> Sem r ()
+    checkRepeated args = whenJust (nonEmpty (findRepeated (map (^. namedArgName . S.nameConcrete) args))) $ \reps ->
       throw . ErrDuplicateArgument $ DuplicateArgument reps
 
     emitArgs :: IsImplicit -> Bool -> NamesByIndex -> [NameItem 'Scoped] -> IntMap Arg -> Sem r ()
@@ -231,8 +231,8 @@ helper loc = do
     scanGroup ::
       IsImplicit ->
       [NameItem 'Scoped] ->
-      [NamedArgument 'Scoped] ->
-      Sem r ([NamedArgument 'Scoped], ([NameItem 'Scoped], IntMap Arg))
+      [NamedArgumentAssign 'Scoped] ->
+      Sem r ([NamedArgumentAssign 'Scoped], ([NameItem 'Scoped], IntMap Arg))
     scanGroup impl names =
       fmap (second (first toList))
         . runOutputList
@@ -243,11 +243,11 @@ helper loc = do
         namesBySymbol :: HashMap Symbol (NameItem 'Scoped)
         namesBySymbol = HashMap.fromList [(symbolParsed (i ^. nameItemSymbol), i) | i <- names]
         go ::
-          (Members '[State (IntMap Arg), State (HashMap Symbol (NameItem 'Scoped)), State BuilderState, Output (NamedArgument 'Scoped), Error NamedArgumentsError] r') =>
-          NamedArgument 'Scoped ->
+          (Members '[State (IntMap Arg), State (HashMap Symbol (NameItem 'Scoped)), State BuilderState, Output (NamedArgumentAssign 'Scoped), Error NamedArgumentsError] r') =>
+          NamedArgumentAssign 'Scoped ->
           Sem r' ()
         go arg = do
-          let sym = arg ^. namedArgName
+          let sym = arg ^. namedArgName . S.nameConcrete
           midx :: Maybe (NameItem 'Scoped) <- gets @(HashMap Symbol (NameItem 'Scoped)) (^. at sym)
           case midx of
             Just idx -> do

src/Juvix/Compiler/Internal/Translation/FromConcrete/NamedArguments/Error.hs

@@ -39,7 +39,7 @@ instance ToGenericError DuplicateArgument where
     return GenericError {..}
 
 newtype UnexpectedArguments = UnexpectedArguments
-  { _unexpectedArguments :: NonEmpty (NamedArgument 'Scoped)
+  { _unexpectedArguments :: NonEmpty (NamedArgumentAssign 'Scoped)
   }
   deriving stock (Show)
 

src/Juvix/Compiler/Pipeline/Package/Loader/Versions.hs

@@ -110,7 +110,7 @@ v1v2FromPackage p = run . runReader l $ do
     defaultPackageNoArgs :: (Member (Reader Interval) r) => Sem r (NonEmpty (ExpressionAtom 'Parsed))
     defaultPackageNoArgs = NEL.singleton <$> identifier defaultPackageStr
 
-    defaultPackageWithArgs :: (Member (Reader Interval) r) => NonEmpty (NamedArgument 'Parsed) -> Sem r (NonEmpty (ExpressionAtom 'Parsed))
+    defaultPackageWithArgs :: (Member (Reader Interval) r) => NonEmpty (NamedArgumentAssign 'Parsed) -> Sem r (NonEmpty (ExpressionAtom 'Parsed))
     defaultPackageWithArgs as = do
       defaultPackageName' <- NameUnqualified <$> symbol defaultPackageStr
       argBlock <- argumentBlock Implicit as
@@ -120,18 +120,18 @@ v1v2FromPackage p = run . runReader l $ do
     l :: Interval
     l = singletonInterval (mkInitialLoc (p ^. packageFile))
 
-    mkNamedArgs :: forall r. (Member (Reader Interval) r) => Sem r [NamedArgument 'Parsed]
+    mkNamedArgs :: forall r. (Member (Reader Interval) r) => Sem r [NamedArgumentAssign 'Parsed]
     mkNamedArgs = do
       catMaybes <$> sequence [mkNameArg, mkVersionArg, mkDependenciesArg, mkMainArg, mkBuildDirArg]
       where
-        mkNameArg :: Sem r (Maybe (NamedArgument 'Parsed))
+        mkNameArg :: Sem r (Maybe (NamedArgumentAssign 'Parsed))
         mkNameArg
           | defaultPackageName == p ^. packageName = return Nothing
           | otherwise = do
               n <- literalString (p ^. packageName)
               Just <$> namedArgument "name" (n :| [])
 
-        mkDependenciesArg :: Sem r (Maybe (NamedArgument 'Parsed))
+        mkDependenciesArg :: Sem r (Maybe (NamedArgumentAssign 'Parsed))
         mkDependenciesArg = do
           let deps = p ^. packageDependencies
               dependenciesArg = Just <$> mkDependenciesArg' (p ^. packageDependencies)
@@ -142,7 +142,7 @@ v1v2FromPackage p = run . runReader l $ do
                   | otherwise -> dependenciesArg
             _ -> dependenciesArg
           where
-            mkDependenciesArg' :: [Dependency] -> Sem r (NamedArgument 'Parsed)
+            mkDependenciesArg' :: [Dependency] -> Sem r (NamedArgumentAssign 'Parsed)
             mkDependenciesArg' ds = do
               deps <- mkList =<< mapM mkDependencyArg ds
               namedArgument "dependencies" (deps :| [])
@@ -165,7 +165,7 @@ v1v2FromPackage p = run . runReader l $ do
                          )
                   )
 
-        mkMainArg :: Sem r (Maybe (NamedArgument 'Parsed))
+        mkMainArg :: Sem r (Maybe (NamedArgumentAssign 'Parsed))
         mkMainArg = do
           arg <- mapM mainArg (p ^. packageMain)
           mapM (namedArgument "main") arg
@@ -173,7 +173,7 @@ v1v2FromPackage p = run . runReader l $ do
             mainArg :: Prepath File -> Sem r (NonEmpty (ExpressionAtom 'Parsed))
             mainArg p' = mkJust =<< literalString (pack (unsafePrepathToFilePath p'))
 
-        mkBuildDirArg :: Sem r (Maybe (NamedArgument 'Parsed))
+        mkBuildDirArg :: Sem r (Maybe (NamedArgumentAssign 'Parsed))
         mkBuildDirArg = do
           arg <- mapM buildDirArg (p ^. packageBuildDir)
           mapM (namedArgument "buildDir") arg
@@ -181,12 +181,12 @@ v1v2FromPackage p = run . runReader l $ do
             buildDirArg :: SomeBase Dir -> Sem r (NonEmpty (ExpressionAtom 'Parsed))
             buildDirArg d = mkJust =<< literalString (pack (fromSomeDir d))
 
-        mkVersionArg :: Sem r (Maybe (NamedArgument 'Parsed))
+        mkVersionArg :: Sem r (Maybe (NamedArgumentAssign 'Parsed))
         mkVersionArg
           | p ^. packageVersion == defaultVersion = return Nothing
           | otherwise = Just <$> mkVersionArg'
           where
-            mkVersionArg' :: Sem r (NamedArgument 'Parsed)
+            mkVersionArg' :: Sem r (NamedArgumentAssign 'Parsed)
             mkVersionArg' = do
               mkVersionArgs <- liftM2 (++) explicitArgs implicitArgs
               mkVersionName <- identifier "mkVersion"

src/Juvix/Prelude.hs

@@ -2,6 +2,7 @@ module Juvix.Prelude
   ( module Juvix.Prelude.Base,
     module Juvix.Prelude.Lens,
     module Juvix.Prelude.Stream,
+    module Juvix.Prelude.Generic,
     module Juvix.Prelude.Trace,
     module Juvix.Prelude.Path,
     module Juvix.Prelude.Prepath,
@@ -11,6 +12,7 @@ where
 
 import Juvix.Data
 import Juvix.Prelude.Base
+import Juvix.Prelude.Generic
 import Juvix.Prelude.Lens
 import Juvix.Prelude.Path
 import Juvix.Prelude.Prepath

src/Juvix/Prelude/Generic.hs

@@ -0,0 +1,33 @@
+module Juvix.Prelude.Generic
+  ( genericConstructorName,
+    genericSameConstructor,
+    GenericHasConstructor,
+  )
+where
+
+import GHC.Generics qualified as G
+import Juvix.Prelude.Base.Foundation
+
+genericSameConstructor :: (Generic a, GenericHasConstructor (G.Rep a)) => a -> a -> Bool
+genericSameConstructor x y = genericConstructorName @String x == genericConstructorName y
+
+genericConstructorName ::
+  forall str a.
+  (GenericHasConstructor (G.Rep a), Generic a, IsString str) =>
+  a ->
+  str
+genericConstructorName = fromString . genericConstrName . G.from
+
+class GenericHasConstructor (f :: GHCType -> GHCType) where
+  genericConstrName :: f x -> String
+
+instance (GenericHasConstructor f) => GenericHasConstructor (G.D1 c f) where
+  genericConstrName (G.M1 x) = genericConstrName x
+
+instance (GenericHasConstructor x, GenericHasConstructor y) => GenericHasConstructor (x G.:+: y) where
+  genericConstrName = \case
+    G.L1 l -> genericConstrName l
+    G.R1 r -> genericConstrName r
+
+instance (G.Constructor c) => GenericHasConstructor (G.C1 c f) where
+  genericConstrName x = G.conName x

test/Base.hs

@@ -13,6 +13,7 @@ where
 import Control.Monad.Extra as Monad
 import Data.Algorithm.Diff
 import Data.Algorithm.DiffOutput
+import GHC.Generics qualified as GHC
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination
 import Juvix.Compiler.Pipeline.EntryPoint.IO
 import Juvix.Compiler.Pipeline.Loader.PathResolver
@@ -21,6 +22,7 @@ import Juvix.Data.Effect.TaggedLock
 import Juvix.Extra.Paths hiding (rootBuildDir)
 import Juvix.Prelude hiding (assert)
 import Juvix.Prelude.Env
+import Juvix.Prelude.Pretty (prettyString)
 import Parallel.ProgressLog
 import System.Process qualified as P
 import Test.Tasty
@@ -125,6 +127,28 @@ testRunIOEitherTermination entry =
 assertFailure :: (MonadIO m) => String -> m a
 assertFailure = liftIO . HUnit.assertFailure
 
+wantsError ::
+  forall err b.
+  (Generic err, GenericHasConstructor (GHC.Rep err)) =>
+  (b -> err) ->
+  Path Abs File ->
+  err ->
+  Maybe String
+wantsError wanted file actualErr
+  | genericSameConstructor wantedErr actualErr = Nothing
+  | otherwise =
+      Just
+        ( "In "
+            <> prettyString file
+            <> "\nExpected "
+            <> genericConstructorName wantedErr
+            <> "\nFound    "
+            <> genericConstructorName actualErr
+        )
+  where
+    wantedErr :: err
+    wantedErr = wanted impossible
+
 -- | The same as `P.readProcess` but instead of inheriting `stderr` redirects it
 -- to the child's `stdout`.
 readProcess :: FilePath -> [String] -> Text -> IO Text

test/Scope/Negative.hs

@@ -27,7 +27,7 @@ testDescr NegTest {..} =
             res <- testRunIOEitherTermination entryPoint upToInternal
             case mapLeft fromJuvixError res of
               Left (Just err) -> whenJust (_checkErr err) assertFailure
-              Left Nothing -> assertFailure "An error occurred but it was not in the scoper."
+              Left Nothing -> assertFailure ("An error occurred but it was not in the scoper.\nFile: " <> prettyString file')
               Right {} -> assertFailure "The scope checker did not find an error."
         }
 
@@ -38,352 +38,260 @@ allTests =
     ( map (mkTest . testDescr) scoperErrorTests
     )
 
-wrongError :: Maybe FailMsg
-wrongError = Just "Incorrect error"
+negTest ::
+  String ->
+  Path Rel Dir ->
+  Path Rel File ->
+  (Path Abs File -> ScoperError -> Maybe FailMsg) ->
+  NegTest ScoperError
+negTest tname rdir rfile chk =
+  NegTest
+    { _name = tname,
+      _relDir = rdir,
+      _file = rfile,
+      _checkErr = chk (root <//> rdir <//> rfile)
+    }
 
 scoperErrorTests :: [NegTest ScoperError]
 scoperErrorTests =
-  [ NegTest
+  [ negTest
       "Not in scope"
       $(mkRelDir ".")
       $(mkRelFile "NotInScope.juvix")
-      $ \case
-        ErrSymNotInScope {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrSymNotInScope,
+    negTest
       "Qualified not in scope"
       $(mkRelDir ".")
       $(mkRelFile "QualSymNotInScope.juvix")
-      $ \case
-        ErrQualSymNotInScope {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrQualSymNotInScope,
+    negTest
       "Multiple declarations"
       $(mkRelDir ".")
       $(mkRelFile "MultipleDeclarations.juvix")
-      $ \case
-        ErrMultipleDeclarations {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrMultipleDeclarations,
+    negTest
       "Import cycle"
       $(mkRelDir "ImportCycle")
       $(mkRelFile "A.juvix")
-      $ \case
-        ErrImportCycleNew {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrImportCycleNew,
+    negTest
       "Binding group conflict (function clause)"
       $(mkRelDir "BindGroupConflict")
       $(mkRelFile "Clause.juvix")
-      $ \case
-        ErrMultipleDeclarations {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrMultipleDeclarations,
+    negTest
       "Binding group conflict (lambda clause)"
       $(mkRelDir "BindGroupConflict")
       $(mkRelFile "Lambda.juvix")
-      $ \case
-        ErrMultipleDeclarations {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrMultipleDeclarations,
+    negTest
       "Infix error (expression)"
       $(mkRelDir ".")
       $(mkRelFile "InfixError.juvix")
-      $ \case
-        ErrInfixParser {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrInfixParser,
+    negTest
       "Infix error (pattern)"
       $(mkRelDir ".")
       $(mkRelFile "InfixErrorP.juvix")
-      $ \case
-        ErrInfixPattern {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrInfixPattern,
+    negTest
       "Duplicate operator declaration"
       $(mkRelDir ".")
       $(mkRelFile "DuplicateOperator.juvix")
-      $ \case
-        ErrDuplicateOperator {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrDuplicateOperator,
+    negTest
       "Multiple export conflict"
       $(mkRelDir ".")
       $(mkRelFile "MultipleExportConflict.juvix")
-      $ \case
-        ErrMultipleExport {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrMultipleExport,
+    negTest
       "Module not in scope"
       $(mkRelDir ".")
       $(mkRelFile "ModuleNotInScope.juvix")
-      $ \case
-        ErrModuleNotInScope {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrModuleNotInScope,
+    negTest
       "Unused operator syntax definition"
       $(mkRelDir ".")
       $(mkRelFile "UnusedOperatorDef.juvix")
-      $ \case
-        ErrUnusedOperatorDef {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrUnusedOperatorDef,
+    negTest
       "Ambiguous symbol"
       $(mkRelDir ".")
       $(mkRelFile "AmbiguousSymbol.juvix")
-      $ \case
-        ErrAmbiguousSym {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrAmbiguousSym,
+    negTest
       "Ambiguous export"
       $(mkRelDir ".")
       $(mkRelFile "AmbiguousExport.juvix")
-      $ \case
-        ErrMultipleExport {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrMultipleExport,
+    negTest
       "Ambiguous nested modules"
       $(mkRelDir ".")
       $(mkRelFile "AmbiguousModule.juvix")
-      $ \case
-        ErrAmbiguousModuleSym {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrAmbiguousModuleSym,
+    negTest
       "Ambiguous nested constructors"
       $(mkRelDir ".")
       $(mkRelFile "AmbiguousConstructor.juvix")
-      $ \case
-        ErrAmbiguousSym {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrAmbiguousSym,
+    negTest
       "Implicit argument on the left of an application"
       $(mkRelDir ".")
       $(mkRelFile "AppLeftImplicit.juvix")
-      $ \case
-        ErrAppLeftImplicit {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrAppLeftImplicit,
+    negTest
       "issue 230"
       $(mkRelDir "230")
       $(mkRelFile "Prod.juvix")
-      $ \case
-        ErrQualSymNotInScope {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrQualSymNotInScope,
+    negTest
       "Double braces in pattern"
       $(mkRelDir ".")
       $(mkRelFile "NestedPatternBraces.juvix")
-      $ \case
-        ErrDoubleBracesPattern {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrDoubleBracesPattern,
+    negTest
       "As-Pattern aliasing variable"
       $(mkRelDir ".")
       $(mkRelFile "AsPatternAlias.juvix")
-      $ \case
-        ErrAliasBinderPattern {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrAliasBinderPattern,
+    negTest
       "Nested As-Patterns"
       $(mkRelDir ".")
       $(mkRelFile "NestedAsPatterns.juvix")
-      $ \case
-        ErrDoubleBinderPattern {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrDoubleBinderPattern,
+    negTest
       "Pattern matching an implicit argument on the left of an application"
       $(mkRelDir ".")
       $(mkRelFile "ImplicitPatternLeftApplication.juvix")
-      $ \case
-        ErrImplicitPatternLeftApplication {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrImplicitPatternLeftApplication,
+    negTest
       "Constructor expected on the left of a pattern application"
       $(mkRelDir ".")
       $(mkRelFile "ConstructorExpectedLeftApplication.juvix")
-      $ \case
-        ErrConstructorExpectedLeftApplication {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrConstructorExpectedLeftApplication,
+    negTest
       "A type parameter name occurs twice when declaring an inductive type"
       $(mkRelDir ".")
       $(mkRelFile "DuplicateInductiveParameterName.juvix")
-      $ \case
-        ErrNameSignature (ErrDuplicateName DuplicateName {}) -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrNameSignature,
+    negTest
       "Using symbol that is not exported"
       $(mkRelDir "UsingHiding")
       $(mkRelFile "Main.juvix")
-      $ \case
-        ErrModuleDoesNotExportSymbol {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrModuleDoesNotExportSymbol,
+    negTest
       "Wrong number of iterator initializers"
       $(mkRelDir ".")
       $(mkRelFile "Iterators1.juvix")
-      $ \case
-        ErrIteratorInitializer {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrIteratorInitializer,
+    negTest
       "Wrong number of iterator ranges"
       $(mkRelDir ".")
       $(mkRelFile "Iterators2.juvix")
-      $ \case
-        ErrIteratorRange {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrIteratorRange,
+    negTest
       "Undeclared iterator"
       $(mkRelDir ".")
       $(mkRelFile "Iterators3.juvix")
-      $ \case
-        ErrIteratorUndefined {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrIteratorUndefined,
+    negTest
       "Duplicate iterator declaration"
       $(mkRelDir ".")
       $(mkRelFile "Iterators4.juvix")
-      $ \case
-        ErrDuplicateIterator {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrDuplicateIterator,
+    negTest
       "Unused iterator declaration"
       $(mkRelDir ".")
       $(mkRelFile "Iterators5.juvix")
-      $ \case
-        ErrUnusedIteratorDef {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrUnusedIteratorDef,
+    negTest
       "Repeated name in named application"
       $(mkRelDir ".")
       $(mkRelFile "DuplicateArgument.juvix")
-      $ \case
-        ErrNamedArgumentsError (ErrDuplicateArgument {}) -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrMultipleDeclarations,
+    negTest
       "Unexpected named argument after wildcard"
       $(mkRelDir ".")
       $(mkRelFile "UnexpectedArgumentWildcard.juvix")
-      $ \case
-        ErrNamedArgumentsError ErrUnexpectedArguments {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrUnexpectedArgument,
+    negTest
       "Unexpected named argument"
       $(mkRelDir ".")
       $(mkRelFile "UnexpectedArgument.juvix")
-      $ \case
-        ErrNamedArgumentsError ErrUnexpectedArguments {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrUnexpectedArgument,
+    negTest
       "Missing argument"
       $(mkRelDir ".")
       $(mkRelFile "MissingArgument.juvix")
-      $ \case
-        ErrNamedArgumentsError ErrMissingArguments {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrNamedArgumentsError,
+    negTest
       "Repeated name in name signature"
       $(mkRelDir ".")
       $(mkRelFile "RepeatedNameSignature.juvix")
-      $ \case
-        ErrNameSignature ErrDuplicateName {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrNameSignature,
+    negTest
       "No named arguments"
       $(mkRelDir ".")
       $(mkRelFile "NoNamedArguments.juvix")
-      $ \case
-        ErrNamedArgumentsError ErrUnexpectedArguments {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrNoNameSignature,
+    negTest
       "Not a record"
       $(mkRelDir ".")
       $(mkRelFile "NotARecord.juvix")
-      $ \case
-        ErrNotARecord NotARecord {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrNotARecord,
+    negTest
       "Unexpected field in record update"
       $(mkRelDir ".")
       $(mkRelFile "UnexpectedFieldUpdate.juvix")
-      $ \case
-        ErrUnexpectedField UnexpectedField {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrUnexpectedField,
+    negTest
       "Repeated field in record pattern"
       $(mkRelDir ".")
       $(mkRelFile "RepeatedFieldPattern.juvix")
-      $ \case
-        ErrRepeatedField RepeatedField {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrRepeatedField,
+    negTest
       "Missing fields in record creation"
       $(mkRelDir ".")
       $(mkRelFile "MissingFields.juvix")
-      $ \case
-        ErrMissingArgs {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrMissingArgs,
+    negTest
       "Unexpected argument"
       $(mkRelDir ".")
       $(mkRelFile "UnexpectedArgumentNew.juvix")
-      $ \case
-        ErrUnexpectedArgument UnexpectedArgument {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrUnexpectedArgument,
+    negTest
       "Incomparable precedences"
       $(mkRelDir ".")
       $(mkRelFile "IncomparablePrecedences.juvix")
-      $ \case
-        ErrIncomparablePrecedences {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrIncomparablePrecedences,
+    negTest
       "Precedence inconsistency"
       $(mkRelDir ".")
       $(mkRelFile "PrecedenceInconsistency.juvix")
-      $ \case
-        ErrPrecedenceInconsistency {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrPrecedenceInconsistency,
+    negTest
       "Alias cycle"
       $(mkRelDir ".")
       $(mkRelFile "AliasCycle.juvix")
-      $ \case
-        ErrAliasCycle {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrAliasCycle,
+    negTest
       "Invalid range number in iterator definition"
       $(mkRelDir ".")
       $(mkRelFile "InvalidRangeNumber.juvix")
-      $ \case
-        ErrInvalidRangeNumber {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrInvalidRangeNumber,
+    negTest
       "Dangling double brace"
       $(mkRelDir "Internal")
       $(mkRelFile "DanglingDoubleBrace.juvix")
-      $ \case
-        ErrDanglingDoubleBrace {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrDanglingDoubleBrace,
+    negTest
       "Nested let open shadowing"
       $(mkRelDir ".")
       $(mkRelFile "LetOpen.juvix")
-      $ \case
-        ErrAmbiguousSym {} -> Nothing
-        _ -> wrongError,
-    NegTest
+      $ wantsError ErrAmbiguousSym,
+    negTest
       "Invalid default"
       $(mkRelDir ".")
       $(mkRelFile "InvalidDefault.juvix")
-      $ \case
-        ErrWrongDefaultValue {} -> Nothing
-        _ -> wrongError,
-    NegTest
-      "Default argument cycle in FromConcrete"
-      $(mkRelDir ".")
-      $(mkRelFile "DefaultArgCycle.juvix")
-      $ \case
-        ErrDefaultArgCycle {} -> Nothing
-        _ -> wrongError
+      $ wantsError ErrWrongDefaultValue
   ]

tests/Anoma/Compilation/positive/Package.juvix

@@ -2,4 +2,7 @@ module Package;
 
 import PackageDescription.V2 open;
 
-package : Package := defaultPackage {name := "positive"};
+package : Package :=
+  defaultPackage@?{
+    name := "positive"
+  };

tests/Anoma/Compilation/positive/test067.juvix

@@ -5,4 +5,7 @@ import Stdlib.Data.Nat open;
 
 f {a : Nat := 2} {b : Nat := a + 1} {c : Nat} : Nat := a * b * c;
 
-main : Nat := f {c := 5};
+main : Nat :=
+  f@?{
+    c := 5
+  };

tests/Anoma/Compilation/positive/test069.juvix

@@ -20,10 +20,12 @@ mkOrdHelper
   (cmp : A -> A -> Ordering)
   {lt : A -> A -> Bool := λ {a b := isLT (cmp a b)}}
   {gt : A -> A -> Bool := λ {a b := isGT (cmp a b)}}
-  : Ord A :=
-  mkOrd cmp lt gt;
+  : Ord A := mkOrd cmp lt gt;
 
-ordNatNamed : Ord Nat := mkOrdHelper (cmp := Ord.compare);
+ordNatNamed : Ord Nat :=
+  mkOrdHelper@?{
+    cmp := Ord.compare
+  };
 
 instance
 ordNat : Ord Nat := mkOrdHelper Ord.compare;

tests/Anoma/Compilation/positive/test070.juvix

@@ -3,8 +3,16 @@ module test070;
 
 import Stdlib.Data.Nat open;
 
-fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1}
-  : Nat := a * b + c;
+fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1} : Nat := a * b + c;
 
 main : Nat :=
-  fun {a := fun; b := fun {b := 3} * fun {b := fun {2}}};
+  fun@?{
+    a := fun;
+    b :=
+      fun@?{
+          b := 3
+        }
+        * fun@?{
+          b := fun {2}
+        }
+  };

tests/Anoma/Compilation/positive/test072/Package.juvix

@@ -2,4 +2,7 @@ module Package;
 
 import PackageDescription.V2 open;
 
-package : Package := defaultPackage {name := "monads"};
+package : Package :=
+  defaultPackage@?{
+    name := "monads"
+  };

tests/Anoma/Compilation/positive/test073/Package.juvix

@@ -2,4 +2,7 @@ module Package;
 
 import PackageDescription.V2 open;
 
-package : Package := defaultPackage {name := "test073"};
+package : Package :=
+  defaultPackage@?{
+    name := "test073"
+  };

tests/Casm/Compilation/positive/test067.juvix

@@ -5,4 +5,7 @@ import Stdlib.Data.Nat open;
 
 f {a : Nat := 2} {b : Nat := a + 1} {c : Nat} : Nat := a * b * c;
 
-main : Nat := f {c := 5};
+main : Nat :=
+  f@?{
+    c := 5
+  };

tests/Casm/Compilation/positive/test069.juvix

@@ -20,10 +20,12 @@ mkOrdHelper
   (cmp : A -> A -> Ordering)
   {lt : A -> A -> Bool := λ {a b := isLT (cmp a b)}}
   {gt : A -> A -> Bool := λ {a b := isGT (cmp a b)}}
-  : Ord A :=
-  mkOrd cmp lt gt;
+  : Ord A := mkOrd cmp lt gt;
 
-ordNatNamed : Ord Nat := mkOrdHelper (cmp := Ord.compare);
+ordNatNamed : Ord Nat :=
+  mkOrdHelper@?{
+    cmp := Ord.compare
+  };
 
 instance
 ordNat : Ord Nat := mkOrdHelper Ord.compare;

tests/Casm/Compilation/positive/test070.juvix

@@ -3,8 +3,16 @@ module test070;
 
 import Stdlib.Data.Nat open;
 
-fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1}
-  : Nat := a * b + c;
+fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1} : Nat := a * b + c;
 
 main : Nat :=
-  fun {a := fun; b := fun {b := 3} * fun {b := fun {2}}};
+  fun@?{
+    a := fun;
+    b :=
+      fun@?{
+          b := 3
+        }
+        * fun@?{
+          b := fun {2}
+        }
+  };

tests/Casm/Compilation/positive/test072/Package.juvix

@@ -2,4 +2,7 @@ module Package;
 
 import PackageDescription.V2 open;
 
-package : Package := defaultPackage {name := "monads"};
+package : Package :=
+  defaultPackage@?{
+    name := "monads"
+  };

tests/Casm/Compilation/positive/test073/Package.juvix

@@ -2,4 +2,7 @@ module Package;
 
 import PackageDescription.V2 open;
 
-package : Package := defaultPackage {name := "test073"};
+package : Package :=
+  defaultPackage@?{
+    name := "test073"
+  };

tests/Compilation/positive/test006.juvix

@@ -8,6 +8,7 @@ loop : Nat := loop;
 
 main : IO :=
   printNatLn
-      (ite (3 > 0) 1 loop + ite (2 < 1) loop (ite (7 >= 8) loop 1))
+      (ite (3 > 0) 1 loop
+        + ite (2 < 1) loop (ite (7 >= 8) loop 1))
     >>> printBoolLn (2 > 0 || loop == 0)
     >>> printBoolLn (2 < 0 && loop == 0);

tests/Compilation/positive/test007.juvix

@@ -31,4 +31,5 @@ main : IO :=
     >>> printNatLn (head 0 (tail lst))
     >>> printNatListLn (map ((+) 1) lst)
     >>> printNatListLn (map' ((+) 1) lst)
-    >>> printNatListLn (runPartial (λ{{{_}} := map'' ((+) 1) lst}));
+    >>> printNatListLn
+      (runPartial λ {{{_}} := map'' ((+) 1) lst});

tests/Compilation/positive/test010.juvix

@@ -7,8 +7,7 @@ main : IO :=
   let
     x : Nat := 1;
   in let
-    x1 :
-      Nat :=
+       x1 : Nat :=
          x
            + let
                x2 : Nat := 2;

tests/Compilation/positive/test012.juvix

@@ -16,7 +16,8 @@ gen : Nat → Tree
     if
       | mod n 3 == 0 := node1 (gen (sub n 1))
       | mod n 3 == 1 := node2 (gen (sub n 1)) (gen (sub n 1))
-      | else := node3 (gen (sub n 1)) (gen (sub n 1)) (gen (sub n 1));
+      | else :=
+        node3 (gen (sub n 1)) (gen (sub n 1)) (gen (sub n 1));
 
 preorder : Tree → IO
   | leaf := printNat 0

tests/Compilation/positive/test018.juvix

@@ -13,4 +13,3 @@ u : Nat → Nat
   | x := f (h 4) + x;
 
 main : IO := printNatLn (u 2);
-

tests/Compilation/positive/test019.juvix

@@ -8,4 +8,3 @@ app : ({A : Type} → A → A) → {A : Type} → A → A
   | x := x x;
 
 main : IO := printNatLn (app id (3 + 4));
-

tests/Compilation/positive/test022.juvix

@@ -25,4 +25,3 @@ main : IO :=
     >>> printListNatLn (reverse (map (flip sub 1) (gen 10)))
     >>> printNatLn (sum 10000)
     >>> printNatLn (sum' 10000);
-

tests/Compilation/positive/test023.juvix

@@ -20,4 +20,3 @@ main : IO :=
   printNatLn (f 5)
     >>> printNatLn (f 10)
     >>> printNatLn (f 20);
-

tests/Compilation/positive/test027.juvix

@@ -1,33 +1,35 @@
--- Church numerals
+--- Church numerals
+--- This test is disabled until https://github.com/anoma/juvix/issues/1706 is fixed.
+--- It is convenient to comment it out so we can format all test files without a crash.
 module test027;
 
-import Stdlib.Prelude open hiding {toNat};
+-- import Stdlib.Prelude open hiding {toNat};
 
-Num : Type := {A : Type} → (A → A) → A → A;
+-- Num : Type := {A : Type} → (A → A) → A → A;
 
-czero : Num
-  | {_} f x := x;
+-- czero : Num
+--   | {_} f x := x;
 
-csuc : Num → Num
-  | n {_} f := f << n {_} f;
+-- csuc : Num → Num
+--   | n {_} f := f << n {_} f;
 
-num : Nat → Num
-  | zero := czero
-  | (suc n) := csuc (num n);
+-- num : Nat → Num
+--   | zero := czero
+--   | (suc n) := csuc (num n);
 
-add : Num → Num → Num
-  | n m {_} f := n {_} f << m {_} f;
+-- add : Num → Num → Num
+--   | n m {_} f := n {_} f << m {_} f;
 
-mul : Num → Num → Num
-  | n m {_} := n {_} << m {_};
+-- mul : Num → Num → Num
+--   | n m {_} := n {_} << m {_};
 
-isZero : Num → Bool
-  | n := n {_} (const false) true;
+-- isZero : Num → Bool
+--   | n := n {_} (const false) true;
 
-toNat : Num → Nat
-  | n := n {_} ((+) 1) 0;
+-- toNat : Num → Nat
+--   | n := n {_} ((+) 1) 0;
 
-main : IO :=
-  printNatLn (toNat (num 7))
-    >>> printNatLn (toNat (add (num 7) (num 3)))
-    >>> printNatLn (toNat (mul (num 7) (num 3)));
+-- main : IO :=
+--   printNatLn (toNat (num 7))
+--     >>> printNatLn (toNat (add (num 7) (num 3)))
+--     >>> printNatLn (toNat (mul (num 7) (num 3)));

tests/Compilation/positive/test030.juvix

@@ -25,4 +25,3 @@ main : IO :=
     >>> printNatLn (mult 3 7)
     >>> printNatLn (exp 3 7)
     >>> printNatLn (ackermann 3 7);
-

tests/Compilation/positive/test035.juvix

@@ -55,4 +55,3 @@ main : IO :=
     >>> printNatLn (f (gen 20))
     >>> printNatLn (h 5)
     >>> printNatLn (h 3);
-

tests/Compilation/positive/test036.juvix

@@ -21,4 +21,3 @@ j : Nat → Nat → Nat := g';
 k : Nat → Nat → Nat → Nat := expand j;
 
 main : IO := printNatLn (h 13 + j 2 3 + k 9 4 7);
-

tests/Compilation/positive/test037.juvix

@@ -10,12 +10,12 @@ f (l : List ((Nat → Nat) → Nat → Nat)) : Nat :=
   }
     (let
       y : Nat → Nat := id;
-    in (let
+    in let
          z : (Nat → Nat) → Nat → Nat := id;
-       in case l of
+       in case l of {
             | _ :: _ := id
-            | _ := id
-         z)
+            | _ := id z
+          }
       y)
     7;
 

tests/Compilation/positive/test040.juvix

@@ -4,11 +4,9 @@ module test040;
 import Stdlib.System.IO open;
 import Stdlib.Data.Bool open;
 
-type Unit :=
-  | unit : Unit;
+type Unit := unit : Unit;
 
-type Foo (A : Type) :=
-  | foo : Unit -> A -> Foo A;
+type Foo (A : Type) := foo : Unit -> A -> Foo A;
 
 f : {A : Type} -> Foo A -> A
   | (foo unit a) := a;

tests/Compilation/positive/test041.juvix

@@ -3,8 +3,7 @@ module test041;
 
 import Stdlib.Prelude open;
 
-type BoxedString :=
-  | boxed : String -> BoxedString;
+type BoxedString := boxed : String -> BoxedString;
 
 printBoxedString : BoxedString -> IO
   | (boxed s) := printStringLn s;

tests/Compilation/positive/test046.juvix

@@ -12,6 +12,7 @@ id' : Ty
 -- In PR https://github.com/anoma/juvix/pull/2545 we had to slightly modify
 -- the `fun` definition. The previous version is kept here as a comment.
 -- fun : {A : Type} → A → Ty := id λ {_ := id'};
-fun {A : Type} : A → Ty := id { _ -> {C : Type} → C → C } λ {_ := id'};
+fun {A : Type} : A → Ty :=
+  id {_ -> {C : Type} → C → C} λ {_ := id'};
 
 main : Nat := fun 5 {Nat} 7;

tests/Compilation/positive/test055.juvix

@@ -3,8 +3,7 @@ module test055;
 
 import Stdlib.Prelude open;
 
-type Pair' :=
-  | pair : Nat -> Nat -> Pair';
+type Pair' := pair : Nat -> Nat -> Pair';
 
 main : Pair (List (Pair Pair' Nat)) (List Pair') :=
   (pair 1 2, 3) :: (pair 2 3, 4) :: nil

tests/Compilation/positive/test060.juvix

@@ -36,8 +36,7 @@ main : Triple Nat Nat Nat :=
       mkPair@{
         fst := mkPair true nil;
         snd := 0 :: nil
-        } :=
-      (f p')
+      } := f p'
     | else :=
       mkTriple@{
         fst := 0;

tests/Compilation/positive/test061.juvix

@@ -7,10 +7,14 @@ trait
 type Show A := mkShow {show : A → String};
 
 Show' : Type -> Type := Show;
+
 Bool' : Type := Bool;
 
 instance
-showStringI : Show String := mkShow (show := id);
+showStringI : Show String :=
+  mkShow@?{
+    show := id
+  };
 
 instance
 showBoolI : Show' Bool' :=
@@ -19,7 +23,10 @@ showBoolI : Show' Bool' :=
   };
 
 instance
-showNatI : Show Nat := mkShow (show := natToString);
+showNatI : Show Nat :=
+  mkShow@?{
+    show := natToString
+  };
 
 g : {A : Type} → {{Show A}} → Nat := 5;
 
@@ -52,46 +59,49 @@ f'3 {A} {{M : Show A}} : A → String := Show.show {{M}};
 
 f'4 {A} {{_ : Show A}} : A → String := Show.show;
 
-f5 {A} {{Show' A}} (n : String) (a : A) : String :=
-  n ++str Show.show a;
+f5 {A} {{Show' A}} (n : String) (a : A) : String := n ++str Show.show a;
 
 instance
-showBoolFunI : Show (Bool → Bool) := mkShow@{
+showBoolFunI : Show (Bool → Bool) :=
+  mkShow@{
     show (f : Bool → Bool) : String :=
       let
         b1 : Bool := f true;
         b2 : Bool := f false;
-    in
-    "\\{ true := " ++str Show.show b1 ++str " | false := " ++str Show.show b2 ++str " }";
-};
+      in "\\{ true := " ++str Show.show b1 ++str " | false := " ++str Show.show b2 ++str " }"
+  };
 
 instance
 showPairI {A B} {{Show A}} {{Show' B}} : Show' (Pair A B) :=
   mkShow λ {(x, y) := Show.show x ++str ", " ++str Show.show y};
 
 trait
-type T A := mkT { a : A };
+type T A := mkT {a : A};
 
 instance
 tNatI : T Nat := mkT 0;
 
 instance
-tFunI {A} {{T A}} : T (A -> A) := mkT \ { a := a };
+tFunI {A} {{T A}} : T (A -> A) := mkT \ {a := a};
 
 main : IO :=
-  printStringLn (Show.show true) >>>
-  printStringLn (f false) >>>
-  printStringLn (Show.show 3) >>>
-  printStringLn (Show.show (g {Nat})) >>>
-  printStringLn (Show.show [true; false]) >>>
-  printStringLn (Show.show [1; 2; 3]) >>>
-  printStringLn (f' [1; 2]) >>>
-  printStringLn (f'' [true; false]) >>>
-  printStringLn (f'3 [just true; nothing; just false]) >>>
-  printStringLn (f'4 [just [1]; nothing; just [2; 3]]) >>>
-  printStringLn (f'3 "abba") >>>
-  printStringLn (f'3 {{M := mkShow (λ{x := x ++str "!"})}} "abba") >>>
-  printStringLn (f5 "abba" 3) >>>
-  printStringLn (Show.show {{_}} ["a"; "b"; "c"; "d"]) >>>
-  printStringLn (Show.show (λ{x := not x})) >>>
-  printStringLn (Show.show (3, [1; 2 + T.a 0]));
+  printStringLn (Show.show true)
+    >>> printStringLn (f false)
+    >>> printStringLn (Show.show 3)
+    >>> printStringLn (Show.show (g {Nat}))
+    >>> printStringLn (Show.show [true; false])
+    >>> printStringLn (Show.show [1; 2; 3])
+    >>> printStringLn (f' [1; 2])
+    >>> printStringLn (f'' [true; false])
+    >>> printStringLn (f'3 [just true; nothing; just false])
+    >>> printStringLn (f'4 [just [1]; nothing; just [2; 3]])
+    >>> printStringLn (f'3 "abba")
+    >>> printStringLn
+      (f'3@?{
+          M := mkShow λ {x := x ++str "!"}
+        }
+        "abba")
+    >>> printStringLn (f5 "abba" 3)
+    >>> printStringLn (Show.show {{_}} ["a"; "b"; "c"; "d"])
+    >>> printStringLn (Show.show λ {x := not x})
+    >>> printStringLn (Show.show (3, [1; 2 + T.a 0]));

tests/Compilation/positive/test064.juvix

@@ -36,6 +36,7 @@ even' : Nat -> Bool := even;
 
 main : Nat :=
   sum 3
-    + case even' 6 || g true || h true of
+    + case even' 6 || g true || h true of {
         | true := ite (g false) (f 1 2 + sum 7 + j 0) 0
-        | false := f (3 + 4) (f 0 8) + loop;
+        | false := f (3 + 4) (f 0 8) + loop
+      };

tests/Compilation/positive/test067.juvix

@@ -3,6 +3,10 @@ module test067;
 
 import Stdlib.Data.Nat open;
 
-f {a : Nat := 2} {b : Nat := a + 1} {c : Nat} : Nat := a * b * c;
+f {a : Nat := 2} {b : Nat := a + 1} {c : Nat} : Nat :=
+  a * b * c;
 
-main : Nat := f {c := 5};
+main : Nat :=
+  f@?{
+    c := 5
+  };

tests/Compilation/positive/test069.juvix

@@ -20,10 +20,12 @@ mkOrdHelper
   (cmp : A -> A -> Ordering)
   {lt : A -> A -> Bool := λ {a b := isLT (cmp a b)}}
   {gt : A -> A -> Bool := λ {a b := isGT (cmp a b)}}
-  : Ord A :=
-  mkOrd cmp lt gt;
+  : Ord A := mkOrd cmp lt gt;
 
-ordNatNamed : Ord Nat := mkOrdHelper (cmp := Ord.compare);
+ordNatNamed : Ord Nat :=
+  mkOrdHelper@?{
+    cmp := Ord.compare
+  };
 
 instance
 ordNat : Ord Nat := mkOrdHelper Ord.compare;

tests/Compilation/positive/test070.juvix

@@ -3,8 +3,16 @@ module test070;
 
 import Stdlib.Data.Nat open;
 
-fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1}
-  : Nat := a * b + c;
+fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1} : Nat := a * b + c;
 
 main : Nat :=
-  fun {a := fun; b := fun {b := 3} * fun {b := fun {2}}};
+  fun@?{
+    a := fun;
+    b :=
+      fun@?{
+          b := 3
+        }
+        * fun@?{
+          b := fun {2}
+        }
+  };

tests/Compilation/positive/test071.juvix

@@ -20,24 +20,49 @@ mkOrdHelper
   (cmp : A -> A -> Ordering)
   {lt : A -> A -> Bool := λ {a b := isLT (cmp a b)}}
   {gt : A -> A -> Bool := λ {a b := isGT (cmp a b)}}
-  : Ord A :=
-  mkOrd cmp lt gt;
+  : Ord A := mkOrd cmp lt gt;
 
 instance
-ordNat : Ord Nat := mkOrdHelper@{
+ordNat : Ord Nat :=
+  mkOrdHelper@{
     cmp (x y : Nat) : Ordering := Ord.compare x y
-};
+  };
 
-fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1}
+fun
+  {a : Nat := 1}
+  {b : Nat := a + 1}
+  {c : Nat := b + a + 1}
   : Nat := a * b + c;
 
-f {a : Nat := 2} {b : Nat := a + 1} {c : Nat} : Nat := a * b * c;
+f {a : Nat := 2} {b : Nat := a + 1} {c : Nat} : Nat :=
+  a * b * c;
 
-g {a : Nat := 2} {b : Nat := a + 1} (c : Nat) : Nat := a * b * c;
+g {a : Nat := 2} {b : Nat := a + 1} (c : Nat) : Nat :=
+  a * b * c;
 
-h {a : Nat := 2} (b c : Nat) {d : Nat := 3} : Nat := a * b + c * d;
+h {a : Nat := 2} (b c : Nat) {d : Nat := 3} : Nat :=
+  a * b + c * d;
 
 main : Nat :=
-  fun@{a := fun; b := fun@{b := 3} * fun@{b := fun {2}}} +
-  f@{c := 5} + g@?{b := 4} 3 + ite (Ord.lt 1 0) 1 0 +
-  h@?{b := 4} 1;
+  fun@{
+      a := fun;
+      b :=
+        fun@{
+            b := 3
+          }
+          * fun@{
+            b := fun {2}
+          }
+    }
+    + f@{
+      c := 5
+    }
+    + g@?{
+        b := 4
+      }
+      3
+    + ite (Ord.lt 1 0) 1 0
+    + h@?{
+        b := 4
+      }
+      1;

tests/Compilation/positive/test072/ExceptT.juvix

@@ -88,5 +88,8 @@ ExceptT-MonadError
       mkExceptT (MMonad.return (left err))
   };
 
-runExcept {Err A} {M : Type -> Type} : ExceptT Err M A -> M (Either Err A)
+runExcept
+  {Err A}
+  {M : Type -> Type}
+  : ExceptT Err M A -> M (Either Err A)
   | (mkExceptT x) := x;

tests/Compilation/positive/test072/Functor.juvix

@@ -9,5 +9,10 @@ type Functor (f : Type -> Type) :=
     <$> : {A B : Type} -> (A -> B) -> f A -> f B
   };
 
-fmap {f : Type -> Type} {{Functor f}} {A B : Type} (fun : A -> B) (x : f A) : f B :=
-  fun Functor.<$> x
+fmap
+  {f : Type -> Type}
+  {{Functor f}}
+  {A B : Type}
+  (fun : A -> B)
+  (x : f A)
+  : f B := fun Functor.<$> x;

tests/Compilation/positive/test072/Identity.juvix

@@ -19,7 +19,8 @@ Identity-Monad : Monad Identity :=
   mkMonad@{
     functor := Identity-Functor;
     return {A : Type} (a : A) : Identity A := mkIdentity a;
-    >>= {A B : Type}
+    >>=
+      {A B : Type}
       : Identity A -> (A -> Identity B) -> Identity B
       | (mkIdentity a) f := f a
   };

tests/Compilation/positive/test072/Monad.juvix

@@ -17,7 +17,13 @@ type Monad (f : Type -> Type) :=
 open Monad public;
 
 syntax operator >>> bind;
->>> {M : Type → Type} {A B : Type} {{Monad M}} (x : M
-  A) (y : M B) : M B := x >>= λ {_ := y};
+>>>
+  {M : Type → Type}
+  {A B : Type}
+  {{Monad M}}
+  (x : M A)
+  (y : M B)
+  : M B := x >>= λ {_ := y};
 
-getFunctor {M : Type -> Type} (_ : Monad M) : Functor M := Monad.functor;
+getFunctor {M : Type -> Type} (_ : Monad M) : Functor M :=
+  Monad.functor;

tests/Compilation/positive/test072/MonadError.juvix

@@ -7,7 +7,7 @@ trait
 type MonadError (Err : Type) (M : Type -> Type) :=
   mkMonadError {
     monad : Monad M;
-    throw : {A : Type} -> Err -> M A;
+    throw : {A : Type} -> Err -> M A
   };
 
 open MonadError public;

tests/Compilation/positive/test072/MonadState.juvix

@@ -13,6 +13,10 @@ type MonadState (S : Type) (M : Type -> Type) :=
 
 open MonadState public;
 
-modify {S : Type} {M : Type → Type} {{Monad M}} {{MonadState
-  S
-  M}} (f : S → S) : M Unit := get >>= λ {s := put (f s)};
+modify
+  {S : Type}
+  {M : Type → Type}
+  {{Monad M}}
+  {{MonadState S M}}
+  (f : S → S)
+  : M Unit := get >>= λ {s := put (f s)};

tests/Compilation/positive/test072/Package.juvix

@@ -2,4 +2,7 @@ module Package;
 
 import PackageDescription.V2 open;
 
-package : Package := defaultPackage {name := "monads"};
+package : Package :=
+  defaultPackage@?{
+    name := "monads"
+  };

tests/Compilation/positive/test072/Reader.juvix

@@ -19,7 +19,8 @@ Reader-Monad {R : Type} : Monad (Reader R) :=
     functor := Reader-Functor;
     return {A : Type} (a : A) : Reader R A :=
       mkReader (const a);
-    >>= {A B : Type}
+    >>=
+      {A B : Type}
       : Reader R A -> (A -> Reader R B) -> Reader R B
       | (mkReader ra) arb :=
         let

tests/Compilation/positive/test072/State.juvix

@@ -4,14 +4,15 @@ import Monad open;
 import Functor open;
 import Stdlib.Data.Pair open;
 
-type State (S A : Type) := mkState {runState : S -> Pair A S};
+type State (S A : Type) :=
+  mkState {runState : S -> Pair A S};
 
 instance
 State-Functor {S : Type} : Functor (State S) :=
   mkFunctor@{
     <$> {A B : Type} (f : A -> B) : State S A -> State S B
       | (mkState S→A×S) :=
-        mkState λ {s := case S→A×S s of {a, s := f a, s}}
+        mkState λ {s := case S→A×S s of a, s := f a, s}
   };
 
 instance
@@ -20,14 +21,13 @@ State-Monad {S : Type} : Monad (State S) :=
     functor := State-Functor;
     return {A : Type} (a : A) : State S A :=
       mkState λ {s := a, s};
-    >>= {A B : Type}
-      : State S A -> (A -> State S B) -> State S B
+    >>=
+      {A B : Type} : State S A -> (A -> State S B) -> State S B
       | (mkState s→s×a) a→Ss×b :=
         mkState
           λ {s :=
-            case s→s×a s of {
-              a, s1 := case a→Ss×b a of {mkState s→s×b := s→s×b s1}
-            }}
+            case s→s×a s of
+              a, s1 := case a→Ss×b a of mkState s→s×b := s→s×b s1}
   };
 
 import MonadState open;

tests/Compilation/positive/test072/StateT.juvix

@@ -9,18 +9,27 @@ import Stdlib.Data.Pair open;
 type StateT (S : Type) (M : Type → Type) (A : Type) :=
   mkStateT {runStateT : S → M (Pair A S)};
 
-runState {S A : Type} {M : Type → Type} (s : S) (m : StateT
-  S
-  M
-  A) : M (Pair A S) := StateT.runStateT m s;
+runState
+  {S A : Type}
+  {M : Type → Type}
+  (s : S)
+  (m : StateT S M A)
+  : M (Pair A S) := StateT.runStateT m s;
 
-evalState {S A : Type} {M : Type → Type} {{Functor
-  M}} (s : S) (m : StateT S M A) : M A :=
-  fst Functor.<$> runState s m;
+evalState
+  {S A : Type}
+  {M : Type → Type}
+  {{Functor M}}
+  (s : S)
+  (m : StateT S M A)
+  : M A := fst Functor.<$> runState s m;
 
 instance
-StateT-Functor {S : Type} {M : Type → Type} {{func : Functor
-  M}} : Functor (StateT S M) :=
+StateT-Functor
+  {S : Type}
+  {M : Type → Type}
+  {{func : Functor M}}
+  : Functor (StateT S M) :=
   mkFunctor@{
     <$> {A B : Type} (f : A → B) : StateT S M A → StateT S M B
       | (mkStateT S→M⟨A×S⟩) :=
@@ -31,7 +40,10 @@ StateT-Functor {S : Type} {M : Type → Type} {{func : Functor
   };
 
 instance
-StateT-Monad {S : Type} {M : Type → Type} {{mon : Monad M}}
+StateT-Monad
+  {S : Type}
+  {M : Type → Type}
+  {{mon : Monad M}}
   : Monad (StateT S M) :=
   mkMonad@{
     functor :=
@@ -40,7 +52,10 @@ StateT-Monad {S : Type} {M : Type → Type} {{mon : Monad M}}
       };
     return {A : Type} (a : A) : StateT S M A :=
       mkStateT λ {s := MMonad.return (a, s)};
-    >>= {A B : Type} (x : StateT S M A) (f : A → StateT S M B)
+    >>=
+      {A B : Type}
+      (x : StateT S M A)
+      (f : A → StateT S M B)
       : StateT S M B :=
       mkStateT
         λ {s :=
@@ -52,7 +67,10 @@ import MonadState open;
 import Stdlib.Data.Unit open;
 
 instance
-StateT-MonadState {S : Type} {M : Type → Type} {{Monad M}}
+StateT-MonadState
+  {S : Type}
+  {M : Type → Type}
+  {{Monad M}}
   : MonadState S (StateT S M) :=
   mkMonadState@{
     monad := StateT-Monad;

tests/Compilation/positive/test073/Package.juvix

@@ -2,4 +2,7 @@ module Package;
 
 import PackageDescription.V2 open;
 
-package : Package := defaultPackage {name := "test073"};
+package : Package :=
+  defaultPackage@?{
+    name := "test073"
+  };

tests/Internal/positive/Dependencies/Dep1/Conflict.juvix

@@ -1,3 +1 @@
 module Conflict;
-
-end;

tests/Internal/positive/Dependencies/Dep1/Dep1/Lib.juvix

@@ -1,3 +1 @@
 module Dep1.Lib;
-
-end;

tests/Internal/positive/Dependencies/Dep1/Package.juvix

@@ -3,4 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage {name := "dep1"; dependencies := []};
+  defaultPackage@?{
+    name := "dep1";
+    dependencies := []
+  };

tests/Internal/positive/Dependencies/Dep2/Conflict.juvix

@@ -1,3 +1 @@
 module Conflict;
-
-end;

tests/Internal/positive/Dependencies/Dep2/Dep2/Lib.juvix

@@ -1,3 +1 @@
 module Dep2.Lib;
-
-end;

tests/Internal/positive/Dependencies/Dep2/Package.juvix

@@ -3,4 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage {name := "dep2"; dependencies := []};
+  defaultPackage@?{
+    name := "dep2";
+    dependencies := []
+  };

tests/Rust/Compilation/positive/test067.juvix

@@ -5,4 +5,7 @@ import Stdlib.Data.Nat open;
 
 f {a : Nat := 2} {b : Nat := a + 1} {c : Nat} : Nat := a * b * c;
 
-main : Nat := f {c := 5};
+main : Nat :=
+  f@?{
+    c := 5
+  };

tests/Rust/Compilation/positive/test069.juvix

@@ -20,10 +20,12 @@ mkOrdHelper
   (cmp : A -> A -> Ordering)
   {lt : A -> A -> Bool := λ {a b := isLT (cmp a b)}}
   {gt : A -> A -> Bool := λ {a b := isGT (cmp a b)}}
-  : Ord A :=
-  mkOrd cmp lt gt;
+  : Ord A := mkOrd cmp lt gt;
 
-ordNatNamed : Ord Nat := mkOrdHelper (cmp := Ord.compare);
+ordNatNamed : Ord Nat :=
+  mkOrdHelper@?{
+    cmp := Ord.compare
+  };
 
 instance
 ordNat : Ord Nat := mkOrdHelper Ord.compare;

tests/Rust/Compilation/positive/test070.juvix

@@ -3,8 +3,16 @@ module test070;
 
 import Stdlib.Data.Nat open;
 
-fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1}
-  : Nat := a * b + c;
+fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1} : Nat := a * b + c;
 
 main : Nat :=
-  fun {a := fun; b := fun {b := 3} * fun {b := fun {2}}};
+  fun@?{
+    a := fun;
+    b :=
+      fun@?{
+          b := 3
+        }
+        * fun@?{
+          b := fun {2}
+        }
+  };

tests/Rust/Compilation/positive/test072/Package.juvix

@@ -2,4 +2,7 @@ module Package;
 
 import PackageDescription.V2 open;
 
-package : Package := defaultPackage {name := "monads"};
+package : Package :=
+  defaultPackage@?{
+    name := "monads"
+  };

tests/Rust/Compilation/positive/test073/Package.juvix

@@ -2,4 +2,7 @@ module Package;
 
 import PackageDescription.V2 open;
 
-package : Package := defaultPackage {name := "test073"};
+package : Package :=
+  defaultPackage@?{
+    name := "test073"
+  };

tests/negative/DefaultArgCycle.juvix

@@ -1,7 +0,0 @@
-module DefaultArgCycle;
-
-import Stdlib.Data.Nat open;
-
-fun {a : Nat := 1} {b : Nat := fun {c := 3}
-  + a
-  + 1} {c : Nat := b + a + 1} : Nat := a * b + c;

tests/negative/DuplicateArgument.juvix

@@ -4,4 +4,8 @@ type T := t : T;
 
 f (a : T) : T := t;
 
-x : T := f (a := t; a := t);
+x : T :=
+  f@?{
+    a := t;
+    a := t
+  };

tests/negative/Internal/AmbiguousCoercions.juvix

@@ -12,10 +12,16 @@ trait
 type T2 A := mkT2 {pp : A → A};
 
 instance
-unitT1 : T1 Unit := mkT1 (pp := λ {_ := unit});
+unitT1 : T1 Unit :=
+  mkT1@{
+    pp := λ {_ := unit}
+  };
 
 instance
-unitT2 : T2 Unit := mkT2 (pp := λ {_ := unit});
+unitT2 : T2 Unit :=
+  mkT2@{
+    pp := λ {_ := unit}
+  };
 
 coercion instance
 fromT1toT {A} {{T1 A}} : T A :=

tests/negative/Internal/AmbiguousInstances.juvix

@@ -8,15 +8,24 @@ trait
 type T A := mkT {pp : A → A};
 
 instance
-unitT : T Unit := mkT (pp := λ {_ := unit});
+unitT : T Unit :=
+  mkT@{
+    pp := λ {_ := unit}
+  };
 
 ppBox {A B} {{T A}} : Box A B → Box A B
   | (box x y) := box (T.pp x) y;
 
 instance
-boxT {A} {{T A}} : T (Box A Unit) := mkT (pp := ppBox);
+boxT {A} {{T A}} : T (Box A Unit) :=
+  mkT@{
+    pp := ppBox
+  };
 
 instance
-boxTUnit {B} : T (Box Unit B) := mkT (pp := λ {x := x});
+boxTUnit {B} : T (Box Unit B) :=
+  mkT@{
+    pp := λ {x := x}
+  };
 
 main : Box Unit Unit := T.pp (box unit unit);

tests/negative/Internal/ExplicitInstanceArgument.juvix

@@ -8,9 +8,15 @@ trait
 type T A := mkT {pp : A → A};
 
 instance
-unitT : T Unit := mkT (pp := λ {_ := unit});
+unitT : T Unit :=
+  mkT@{
+    pp := λ {_ := unit}
+  };
 
 instance
-boxT {A} (x : Box A) : T (Box A) := mkT (pp := \ {_ := x});
+boxT {A} (x : Box A) : T (Box A) :=
+  mkT@{
+    pp := \ {_ := x}
+  };
 
 main : Box Unit := T.pp (box unit);

tests/negative/Internal/SubsumedInstance.juvix

@@ -8,15 +8,24 @@ trait
 type T A := mkT {pp : A → A};
 
 instance
-unitT : T Unit := mkT (pp := λ {_ := unit});
+unitT : T Unit :=
+  mkT@{
+    pp := λ {_ := unit}
+  };
 
 ppBox {A} {{T A}} : Box A → Box A
   | (box x) := box (T.pp x);
 
 instance
-boxT {A} {{T A}} : T (Box A) := mkT (pp := ppBox);
+boxT {A} {{T A}} : T (Box A) :=
+  mkT@{
+    pp := ppBox
+  };
 
 instance
-boxTUnit : T (Box Unit) := mkT (pp := λ {x := x});
+boxTUnit : T (Box Unit) :=
+  mkT@{
+    pp := λ {x := x}
+  };
 
 main : Box Unit := T.pp (box unit);

tests/negative/MissingArgument.juvix

@@ -4,4 +4,7 @@ type T := t : T;
 
 f (a : T) (b : T) : T := t;
 
-x : T := f (b := t);
+x : T :=
+  f@?{
+    b := t
+  };

tests/negative/NoDependencies/Package.juvix

@@ -2,4 +2,7 @@ module Package;
 
 import PackageDescription.V2 open;
 
-package : Package := defaultPackage {dependencies := []};
+package : Package :=
+  defaultPackage@?{
+    dependencies := []
+  };

tests/negative/NoNamedArguments.juvix

@@ -2,4 +2,6 @@ module NoNamedArguments;
 
 axiom T : Type;
 
-axiom B : T (x := Type);
+axiom B : T@?{
+  x := Type
+};

tests/negative/Package/PackageJuvixDuplicateDependencies/Package.juvix

@@ -2,6 +2,6 @@ module Package;
 
 import PackageDescription.V2 open;
 
-package : Package := defaultPackage {name := "abc"; version := mkVersion 0 0 1 ; dependencies := [ github "org" "repo" "ref1" ; github "org" "repo" "ref2" ]};
+package : Package := defaultPackage@?{name := "abc"; version := mkVersion 0 0 1 ; dependencies := [ github "org" "repo" "ref1" ; github "org" "repo" "ref2" ]};
 
 main : Package := package;

tests/negative/UnexpectedArgument.juvix

@@ -4,4 +4,7 @@ type T := t : T;
 
 f (a : T) : T := t;
 
-x : T := f (x := t);
+x : T :=
+  f@?{
+    x := t
+  };

tests/negative/UnexpectedArgumentWildcard.juvix

@@ -5,4 +5,8 @@ type T := t : T;
 f (a : T) : {_ : Type} -> (b : T) -> T
   | b := t;
 
-x : T := f (a := t) (b := t);
+x : T :=
+  f@?{
+    a := t;
+    b := t
+  };

tests/negative/issue2771/Package.juvix

@@ -2,4 +2,7 @@ module Package;
 
 import PackageDescription.V2 open;
 
-package : Package := defaultPackage {name := "issue2771"};
+package : Package :=
+  defaultPackage@?{
+    name := "issue2771"
+  };