Fix #2510 (#2512)

- Close #2510 
- Close #2518 
- Progress for #2520

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

@@ -66,7 +66,7 @@ mkPackageInfo mpackageEntry _packageRoot pkg = do
     juvixAccum cd _ files acc = return (newJuvixFiles <> acc, RecurseFilter (\hasJuvixPackage d -> not hasJuvixPackage && not (isHiddenDirectory d)))
       where
         newJuvixFiles :: [Path Abs File]
-        newJuvixFiles = [cd <//> f | f <- files, isJuvixFile f]
+        newJuvixFiles = [cd <//> f | f <- files, isJuvixFile f || isJuvixMarkdownFile f]
 
     pkgFile :: Path Abs File
     pkgFile = pkg ^. packageFile
@@ -282,12 +282,22 @@ resolvePath' :: (Members '[Files, State ResolverState, Reader ResolverEnv] r) =>
 resolvePath' mp = do
   z <- gets (^. resolverFiles)
   curPkg <- currentPackage
-  let rel = topModulePathToRelativePath' mp
-      packagesWithModule = z ^. at rel
+  let exts = [FileExtJuvix, FileExtJuvixMarkdown]
+  let rpaths = map (`topModulePathToRelativePathByExt` mp) exts
+
+      packagesWithModule :: [(PackageInfo, Path Rel File)]
+      packagesWithModule =
+        [ (pkg, p)
+          | p <- rpaths,
+            pkgs <- toList (HashMap.lookup p z),
+            pkg <- toList pkgs,
+            visible pkg
+        ]
+
       visible :: PackageInfo -> Bool
-      visible p = HashSet.member (p ^. packageRoot) (curPkg ^. packageAvailableRoots)
-  return $ case filter visible (maybe [] toList packagesWithModule) of
-    [r] -> Right (r ^. packageRoot, rel)
+      visible pkg = HashSet.member (pkg ^. packageRoot) (curPkg ^. packageAvailableRoots)
+  return $ case packagesWithModule of
+    [(r, relPath)] -> Right (r ^. packageRoot, relPath)
     [] ->
       Left
         ( ErrMissingModule
@@ -296,22 +306,46 @@ resolvePath' mp = do
                 _missingModule = mp
               }
         )
-    (r : rs) ->
+    ((r, _) : rs) ->
       Left
         ( ErrDependencyConflict
             DependencyConflict
-              { _conflictPackages = r :| rs,
+              { _conflictPackages = r :| map fst rs,
                 _conflictPath = mp
               }
         )
 
-expectedPath' :: (Members '[Reader ResolverEnv] r) => Path Abs File -> TopModulePath -> Sem r (Maybe (Path Abs File))
-expectedPath' actualPath m = do
-  root <- asks (^. envRoot)
-  msingle <- asks (^. envSingleFile)
-  if
-      | msingle == Just actualPath -> return Nothing
-      | otherwise -> return (Just (root <//> topModulePathToRelativePath' m))
+isModuleOrphan ::
+  (Members '[Files] r) =>
+  TopModulePath ->
+  Sem r Bool
+isModuleOrphan topJuvixPath = do
+  let actualPath = getLoc topJuvixPath ^. intervalFile
+
+      possiblePaths :: Path Abs Dir -> [Path Abs Dir]
+      possiblePaths p = p : toList (parents p)
+
+  packageFileExists <- findFile' (possiblePaths (parent actualPath)) packageFilePath
+
+  yamlFileExists <- findFile' (possiblePaths (parent actualPath)) juvixYamlFile
+
+  pathPackageDescription <- globalPackageDescriptionRoot
+
+  return $ isNothing (packageFileExists <|> yamlFileExists) && not (pathPackageDescription `isProperPrefixOf` actualPath)
+
+expectedPath' ::
+  (Members '[Reader ResolverEnv, Files] r) =>
+  TopModulePath ->
+  Sem r PathInfoTopModule
+expectedPath' m = do
+  let _pathInfoTopModule = m
+  _rootInfoPath <- asks (^. envRoot)
+  isOrphan <- isModuleOrphan m
+  let _rootInfoKind
+        | isOrphan = RootKindSingleFile
+        | otherwise = RootKindPackage
+      _pathInfoRootInfo = RootInfo {..}
+  return PathInfoTopModule {..}
 
 re ::
   forall r a.
@@ -326,7 +360,7 @@ re = reinterpret2H helper
       Tactical PathResolver (Sem rInitial) (Reader ResolverEnv ': (State ResolverState ': r)) x
     helper = \case
       RegisterDependencies forceUpdateLockfile -> registerDependencies' forceUpdateLockfile >>= pureT
-      ExpectedModulePath a m -> expectedPath' a m >>= pureT
+      ExpectedPathInfoTopModule m -> expectedPath' m >>= pureT
       WithPath m a -> do
         x :: Either PathResolverError (Path Abs Dir, Path Rel File) <- resolvePath' m
         oldroot <- asks (^. envRoot)

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/PathResolver/Base.hs

@@ -9,14 +9,33 @@ import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.PathResolver.Depe
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.PathResolver.Error
 import Juvix.Prelude
 
+data RootKind
+  = RootKindPackage
+  | RootKindSingleFile
+  deriving stock (Show)
+
+data RootInfo = RootInfo
+  { _rootInfoPath :: Path Abs Dir,
+    _rootInfoKind :: RootKind
+  }
+  deriving stock (Show)
+
+data PathInfoTopModule = PathInfoTopModule
+  { _pathInfoTopModule :: TopModulePath,
+    _pathInfoRootInfo :: RootInfo
+  }
+  deriving stock (Show)
+
 data PathResolver m a where
   RegisterDependencies :: DependenciesConfig -> PathResolver m ()
-  ExpectedModulePath :: Path Abs File -> TopModulePath -> PathResolver m (Maybe (Path Abs File))
+  ExpectedPathInfoTopModule :: TopModulePath -> PathResolver m PathInfoTopModule
   WithPath ::
     TopModulePath ->
     (Either PathResolverError (Path Abs Dir, Path Rel File) -> m x) ->
     PathResolver m x
 
+makeLenses ''RootInfo
+makeLenses ''PathInfoTopModule
 makeSem ''PathResolver
 
 withPathFile :: (Members '[PathResolver] r) => TopModulePath -> (Either PathResolverError (Path Abs File) -> Sem r a) -> Sem r a

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/PathResolver/Paths.hs

@@ -1,11 +1,18 @@
 module Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.PathResolver.Paths where
 
+import Data.Text qualified as Text
 import Juvix.Compiler.Concrete.Data.Name
 import Juvix.Prelude
 
 topModulePathToRelativePath' :: TopModulePath -> Path Rel File
-topModulePathToRelativePath' =
-  topModulePathToRelativePath (show FileExtJuvix) "" (</>)
+topModulePathToRelativePath' m =
+  let absPath :: Path Abs File = getLoc m ^. intervalFile
+      ext = fileExtension' absPath
+   in topModulePathToRelativePath ext "" (</>) m
+
+topModulePathToRelativePathByExt :: FileExt -> TopModulePath -> Path Rel File
+topModulePathToRelativePathByExt ext m =
+  topModulePathToRelativePath (Text.unpack $ fileExtToText ext) "" (</>) m
 
 topModulePathToRelativePath :: String -> String -> (FilePath -> FilePath -> FilePath) -> TopModulePath -> Path Rel File
 topModulePathToRelativePath ext suffix joinpath mp = relFile relFilePath

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

@@ -23,6 +23,7 @@ import Juvix.Compiler.Concrete.Extra qualified as P
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.PathResolver.Base
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.PathResolver.Error
+import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.PathResolver.Paths
 import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context
 import Juvix.Compiler.Concrete.Translation.FromSource.Lexer hiding
   ( symbol,
@@ -299,25 +300,40 @@ topModuleDefStdin = do
   optional_ stashJudoc
   top moduleDef
 
--- FIX: https://github.com/anoma/juvix/pull/251
-checkPath ::
-  (Members '[PathResolver, Error ParserError] s) =>
-  Maybe (Path Abs File) ->
-  TopModulePath ->
+checkModulePath ::
+  (Members '[PathResolver, Files, Error ParserError] s) =>
+  Module 'Parsed 'ModuleTop ->
   Sem s ()
-checkPath maybePath path = do
-  let actualPath = fromMaybe (getLoc path ^. intervalFile) maybePath
-  mexpectedPath <- expectedModulePath actualPath path
-  whenJust mexpectedPath $ \expectedPath ->
-    unlessM (equalPaths expectedPath actualPath) $
-      throw
-        ( ErrWrongTopModuleName
-            WrongTopModuleName
-              { _wrongTopModuleNameActualName = path,
-                _wrongTopModuleNameExpectedPath = expectedPath,
-                _wrongTopModuleNameActualPath = actualPath
-              }
-        )
+checkModulePath m = do
+  let topJuvixPath :: TopModulePath = m ^. modulePath
+  pathInfo :: PathInfoTopModule <- expectedPathInfoTopModule topJuvixPath
+  let expectedRootInfo = pathInfo ^. pathInfoRootInfo
+  let actualPath = getLoc topJuvixPath ^. intervalFile
+  case expectedRootInfo ^. rootInfoKind of
+    RootKindSingleFile -> do
+      let expectedName = Text.pack . toFilePath . removeExtensions . filename $ actualPath
+          actualName = topModulePathToDottedPath topJuvixPath
+
+      unless (expectedName == actualName) $
+        throw
+          ( ErrWrongTopModuleNameOrphan
+              WrongTopModuleNameOrphan
+                { _wrongTopModuleNameOrpahnExpectedName = expectedName,
+                  _wrongTopModuleNameOrpahnActualName = topJuvixPath
+                }
+          )
+    RootKindPackage -> do
+      let relPath = topModulePathToRelativePath' topJuvixPath
+          expectedAbsPath = (expectedRootInfo ^. rootInfoPath) <//> relPath
+      unlessM (equalPaths actualPath expectedAbsPath) $
+        throw
+          ( ErrWrongTopModuleName
+              WrongTopModuleName
+                { _wrongTopModuleNameActualName = topJuvixPath,
+                  _wrongTopModuleNameExpectedPath = expectedAbsPath,
+                  _wrongTopModuleNameActualPath = actualPath
+                }
+          )
 
 topModuleDef ::
   (Members '[Error ParserError, Files, PathResolver, InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) =>
@@ -326,7 +342,7 @@ topModuleDef = do
   space >> optional_ stashJudoc
   optional_ stashPragmas
   m <- top moduleDef
-  P.lift (checkPath Nothing (m ^. modulePath))
+  P.lift . checkModulePath $ m
   return m
 
 juvixCodeBlockParser ::

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

@@ -21,27 +21,46 @@ runPackagePathResolver rootPath sem = do
   runReader globalStdlib updateStdlib
   runReader globalPackageDir updatePackageFiles
   packageFiles' <- relFiles globalPackageDir
-  let mkPackageRoot' = mkPackageRoot packageFiles' globalPackageDir globalStdlib
+  let mkRootInfo' = mkRootInfo packageFiles' globalPackageDir globalStdlib
   ( interpretH $ \case
       RegisterDependencies {} -> pureT ()
-      ExpectedModulePath _ m -> do
-        let relPath = topModulePathToRelativePath' m
-        pureT ((<//> relPath) <$> (mkPackageRoot' relPath))
+      ExpectedPathInfoTopModule m -> do
+        let _pathInfoTopModule = m
+            _pathInfoRootInfo =
+              --  A Package file is a member of a package by definition.
+              fromMaybe (error "runPackagePathResolver: expected root info") $
+                mkRootInfo' (topModulePathToRelativePath' m)
+        pureT PathInfoTopModule {..}
       WithPath m a -> do
         let relPath = topModulePathToRelativePath' m
             x :: Either PathResolverError (Path Abs Dir, Path Rel File)
-            x = case mkPackageRoot' relPath of
-              Just p -> Right (p, relPath)
+            x = case mkRootInfo' relPath of
+              Just p -> Right (p ^. rootInfoPath, relPath)
               Nothing -> Left (ErrPackageInvalidImport PackageInvalidImport {_packageInvalidImport = m})
         runTSimple (return x) >>= bindTSimple a
     )
     sem
   where
-    mkPackageRoot :: HashSet (Path Rel File) -> Path Abs Dir -> Path Abs Dir -> Path Rel File -> Maybe (Path Abs Dir)
-    mkPackageRoot pkgFiles globalPackageDir globalStdlib relPath
-      | parent preludePath `isProperPrefixOf` relPath = Just globalStdlib
-      | relPath `HashSet.member` pkgFiles = Just globalPackageDir
-      | relPath == packageFilePath = Just rootPath
+    mkRootInfo :: HashSet (Path Rel File) -> Path Abs Dir -> Path Abs Dir -> Path Rel File -> Maybe RootInfo
+    mkRootInfo pkgFiles globalPackageDir globalStdlib relPath
+      | parent preludePath `isProperPrefixOf` relPath =
+          Just $
+            RootInfo
+              { _rootInfoPath = globalStdlib,
+                _rootInfoKind = RootKindPackage
+              }
+      | relPath `HashSet.member` pkgFiles =
+          Just $
+            RootInfo
+              { _rootInfoPath = globalPackageDir,
+                _rootInfoKind = RootKindPackage
+              }
+      | relPath == packageFilePath =
+          Just $
+            RootInfo
+              { _rootInfoPath = rootPath,
+                _rootInfoKind = RootKindPackage
+              }
       | otherwise = Nothing
 
 runPackagePathResolver' :: (Members '[TaggedLock, Files] r) => Path Abs Dir -> Sem (PathResolver ': r) a -> Sem r (ResolverState, a)

src/Juvix/Data/Effect/Files/Base.hs

@@ -45,5 +45,6 @@ data Files m a where
   CanonicalDir :: Path Abs Dir -> Prepath Dir -> Files m (Path Abs Dir)
   NormalizeDir :: Path b Dir -> Files m (Path Abs Dir)
   NormalizeFile :: Path b File -> Files m (Path Abs File)
+  FindFile' :: [Path b Dir] -> Path Rel File -> Files m (Maybe (Path Abs File))
 
 makeSem ''Files

src/Juvix/Data/Effect/Files/IO.hs

@@ -51,6 +51,7 @@ runFilesIO = interpret helper
       CanonicalDir root d -> prepathToAbsDir root d
       NormalizeDir p -> canonicalizePath p
       NormalizeFile b -> canonicalizePath b
+      FindFile' possiblePaths f -> Path.findFile possiblePaths f
 
 juvixConfigDirIO :: IO (Path Abs Dir)
 juvixConfigDirIO = (<//> versionDir) . absDir <$> getUserConfigDir "juvix"

src/Juvix/Data/Effect/Files/Pure.hs

@@ -87,6 +87,7 @@ re cwd = reinterpret $ \case
   CanonicalDir root d -> return (canonicalDirPure root d)
   NormalizeDir p -> return (absDir (cwd' </> toFilePath p))
   NormalizeFile p -> return (absFile (cwd' </> toFilePath p))
+  FindFile' ps f -> lookupFileDirs cwd ps f
   where
     cwd' :: FilePath
     cwd' = toFilePath cwd
@@ -221,3 +222,12 @@ lookupFile' p =
   fromMaybeM err (lookupFile p)
   where
     err = missingErr (toFilePath p)
+
+lookupFileDirs :: (Members '[State FS] r) => Path Abs Dir -> [Path a Dir] -> Path Rel File -> Sem r (Maybe (Path Abs File))
+lookupFileDirs cwd ps f =
+  asum <$> mapM helper ps
+  where
+    helper p = do
+      let rpath = absDir (toFilePath cwd </> toFilePath p)
+      let p' :: Path Abs File = rpath <//> f
+      fmap (const p') <$> (lookupFile p')

src/Juvix/Data/FileExt.hs

@@ -149,3 +149,26 @@ isHtmlFile = (== Just htmlFileExt) . fileExtension
 
 isCssFile :: Path b File -> Bool
 isCssFile = (== Just cssFileExt) . fileExtension
+
+toFileExt :: Path b File -> Maybe FileExt
+toFileExt p
+  | isJuvixFile p = Just FileExtJuvix
+  | isJuvixMarkdownFile p = Just FileExtJuvixMarkdown
+  | isJuvixGebFile p = Just FileExtJuvixGeb
+  | isJuvixCoreFile p = Just FileExtJuvixCore
+  | isJuvixAsmFile p = Just FileExtJuvixAsm
+  | isVampIRFile p = Just FileExtVampIR
+  | isVampIRParamsFile p = Just FileExtVampIRParams
+  | isPlonkFile p = Just FileExtPlonk
+  | isHaloFile p = Just FileExtHalo
+  | isLispFile p = Just FileExtLisp
+  | isCFile p = Just FileExtC
+  | isMarkdownFile p = Just FileExtMarkdown
+  | isHtmlFile p = Just FileExtHtml
+  | isCssFile p = Just FileExtCss
+  | otherwise = Nothing
+
+fileExtension' :: Path b File -> String
+fileExtension' p = case toFileExt p of
+  Just ext -> Text.unpack $ fileExtToText ext
+  Nothing -> mconcat $ fileExtension p

src/Juvix/Parser/Error.hs

@@ -18,6 +18,7 @@ data ParserError
   | ErrCommonmark CommonmarkError
   | ErrTopModulePath TopModulePathError
   | ErrWrongTopModuleName WrongTopModuleName
+  | ErrWrongTopModuleNameOrphan WrongTopModuleNameOrphan
   | ErrStdinOrFile StdinOrFileError
   | ErrDanglingJudoc DanglingJudoc
   | ErrMarkdownBackend MarkdownBackendError
@@ -29,6 +30,7 @@ instance ToGenericError ParserError where
     ErrCommonmark e -> genericError e
     ErrTopModulePath e -> genericError e
     ErrWrongTopModuleName e -> genericError e
+    ErrWrongTopModuleNameOrphan e -> genericError e
     ErrStdinOrFile e -> genericError e
     ErrDanglingJudoc e -> genericError e
     ErrMarkdownBackend e -> genericError e
@@ -150,6 +152,34 @@ instance ToGenericError WrongTopModuleName where
                 <> line
                 <> pretty _wrongTopModuleNameExpectedPath
 
+data WrongTopModuleNameOrphan = WrongTopModuleNameOrphan
+  { _wrongTopModuleNameOrpahnExpectedName :: Text,
+    _wrongTopModuleNameOrpahnActualName :: TopModulePath
+  }
+  deriving stock (Show)
+
+instance ToGenericError WrongTopModuleNameOrphan where
+  genericError WrongTopModuleNameOrphan {..} = ask >>= generr
+    where
+      generr opts =
+        return
+          GenericError
+            { _genericErrorLoc = i,
+              _genericErrorMessage = prettyError msg,
+              _genericErrorIntervals = [i]
+            }
+        where
+          opts' = fromGenericOptions opts
+          i = getLoc _wrongTopModuleNameOrpahnActualName
+          msg =
+            "This is a standalone module, but it's name is not the same as the file name."
+              <> line
+              <> "Expected module name:"
+              <+> pcode _wrongTopModuleNameOrpahnExpectedName
+                <> line
+                <> "Actual module name:"
+              <+> ppCode opts' _wrongTopModuleNameOrpahnActualName
+
 data StdinOrFileError = StdinOrFileError
   deriving stock (Show)
 

test/Parsing/Negative.hs

@@ -43,14 +43,16 @@ wrongError :: Maybe FailMsg
 wrongError = Just "Incorrect error"
 
 negTest :: String -> Path Rel Dir -> Path Rel File -> (ParserError -> Maybe FailMsg) -> NegTest
-negTest _name d f _checkErr =
-  let _dir = root <//> d
-   in NegTest
-        { _file = _dir <//> f,
-          _dir,
-          _name,
-          _checkErr
-        }
+negTest _name d f _checkErr = negTestAbsDir _name (root <//> d) f _checkErr
+
+negTestAbsDir :: String -> Path Abs Dir -> Path Rel File -> (ParserError -> Maybe FailMsg) -> NegTest
+negTestAbsDir _name _dir f _checkErr =
+  NegTest
+    { _file = _dir <//> f,
+      _dir,
+      _name,
+      _checkErr
+    }
 
 parserErrorTests :: [NegTest]
 parserErrorTests =
@@ -108,6 +110,13 @@ filesErrorTests =
       $ \case
         ErrWrongTopModuleName {} -> Nothing
         _ -> wrongError,
+    negTestAbsDir
+      "Incorrect top module path of an orphan file."
+      (relToProject $(mkRelDir "tests/WithoutPackageFile"))
+      $(mkRelFile "NoGood.juvix")
+      $ \case
+        ErrWrongTopModuleNameOrphan {} -> Nothing
+        _ -> wrongError,
     negTest
       "Import a module that doesn't exist"
       $(mkRelDir "NoDependencies")

test/Typecheck/Positive.hs

@@ -17,10 +17,15 @@ root :: Path Abs Dir
 root = relToProject $(mkRelDir "tests/positive")
 
 posTest :: String -> Path Rel Dir -> Path Rel File -> PosTest
-posTest _name rdir rfile =
-  let _dir = root <//> rdir
-      _file = _dir <//> rfile
-   in PosTest {..}
+posTest _name rdir rfile = posTestAbsDir _name (root <//> rdir) rfile
+
+posTestAbsDir :: String -> Path Abs Dir -> Path Rel File -> PosTest
+posTestAbsDir _name _dir f =
+  PosTest
+    { _file = _dir <//> f,
+      _dir,
+      _name
+    }
 
 testDescr :: PosTest -> TestDescr
 testDescr PosTest {..} =
@@ -302,7 +307,19 @@ tests =
     posTest
       "Markdown"
       $(mkRelDir "Markdown")
-      $(mkRelFile "Test.juvix.md")
+      $(mkRelFile "Test.juvix.md"),
+    posTest
+      "Import a .juvix.md module in a .juvix file"
+      $(mkRelDir "MarkdownImport")
+      $(mkRelFile "A.juvix"),
+    posTest
+      "Import a .juvix.md module in a .juvix.md file"
+      $(mkRelDir "MarkdownImport")
+      $(mkRelFile "C.juvix.md"),
+    posTestAbsDir
+      "Typecheck orphan file"
+      (relToProject $(mkRelDir "tests/WithoutPackageFile"))
+      $(mkRelFile "Good.juvix")
   ]
     <> [ compilationTest t | t <- Compilation.tests
        ]

tests/WithoutPackageFile/Good.juvix

@@ -0,0 +1,3 @@
+module Good;
+
+axiom A : Type;

tests/WithoutPackageFile/NoGood.juvix

@@ -0,0 +1,3 @@
+module B.C;
+
+end;

tests/positive/Markdown/Test.juvix.md

@@ -9,6 +9,7 @@ module Test;
 
 Certain blocks can be hidden from the output by adding the `hide` attribute, as shown below.
 
+
 ```juvix hide
 import Stdlib.Prelude open;
 ```

tests/positive/MarkdownImport/A.juvix

@@ -0,0 +1,5 @@
+module A;
+
+import B open;
+
+axiom a : D;

tests/positive/MarkdownImport/B.juvix.md

@@ -0,0 +1,5 @@
+```juvix
+module B;
+
+axiom D : Type; 
+```

tests/positive/MarkdownImport/C.juvix.md

@@ -0,0 +1,15 @@
+# This is a Juvix code block
+
+```juvix
+module C;
+
+import B open;
+
+axiom aa : D;
+```
+
+Text in between code blocks
+
+```juvix
+axiom b : D;
+```

tests/positive/MarkdownImport/Package.juvix

@@ -0,0 +1,6 @@
+module Package;
+
+import PackageDescription.V1 open;
+
+package : Package :=
+  defaultPackage {name := "MarkdownImport"};

tests/positive/Monads/Identity.juvix

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

tests/positive/Monads/MonadReader.juvix

@@ -8,5 +8,5 @@ type MonadReader (S : Type) (M : Type -> Type) :=
   mkMonadReader {
     monad : Monad M;
     ask : M S;
-    reader : {A : Type} → (S → A) → M A;
+    reader : {A : Type} → (S → A) → M A
   };

tests/positive/Monads/MonadState.juvix

@@ -4,9 +4,9 @@ import Monad open;
 import Stdlib.Data.Unit open;
 
 trait
-type MonadState  (S : Type) (M : Type -> Type) :=
+type MonadState (S : Type) (M : Type -> Type) :=
   mkMonadState {
     monad : Monad M;
     get : M S;
-    put : S -> M Unit;
+    put : S -> M Unit
   };

tests/positive/Monads/Package.juvix

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

tests/positive/Monads/ReaderT.juvix

@@ -49,7 +49,8 @@ ReaderT-MonadReader {S : Type} {M : Type → Type} {{Monad M}}
   mkMonadReader@{
     monad := ReaderT-Monad;
     ask : ReaderT S M S := mkReaderT λ {s := MMonad.return s};
-    reader {A : Type} (f : S → A) : ReaderT S M A := mkReaderT (MMonad.return ∘ f);
+    reader {A : Type} (f : S → A) : ReaderT S M A :=
+      mkReaderT (MMonad.return ∘ f)
   };
 
 import MonadState open;
@@ -59,8 +60,10 @@ import Stdlib.Data.Product open;
 liftReaderT {R A : Type} {M : Type → Type} (m : M A)
   : ReaderT R M A := mkReaderT (const m);
 
-liftStateT {S A : Type} {M : Type → Type} {{Monad M}} (m : M A)
-  : StateT S M A := mkStateT λ {s := m MMonad.>>= λ {a := MMonad.return (a, s)}};
+liftStateT {S A : Type} {M : Type → Type} {{Monad M}} (m : M
+  A) : StateT S M A :=
+  mkStateT
+    λ {s := m MMonad.>>= λ {a := MMonad.return (a, s)}};
 
 -- FIXME fails instance termination
 -- instance

tests/positive/Monads/StateT.juvix

@@ -43,9 +43,12 @@ import MonadState open;
 import Stdlib.Data.Unit open;
 
 instance
-StateT-MonadState {S : Type} {M : Type → Type} {{Monad M}} : MonadState S (StateT S M) :=
+StateT-MonadState {S : Type} {M : Type → Type} {{Monad M}}
+  : MonadState S (StateT S M) :=
   mkMonadState@{
     monad := StateT-Monad;
-    get : StateT S M S := mkStateT λ {s := MMonad.return (s, s)};
-    put (s : S) : StateT S M Unit := mkStateT λ {_ := MMonad.return (unit, s)};
+    get : StateT S M S :=
+      mkStateT λ {s := MMonad.return (s, s)};
+    put (s : S) : StateT S M Unit :=
+      mkStateT λ {_ := MMonad.return (unit, s)}
   };

tests/positive/Traits2.juvix

@@ -89,7 +89,8 @@ instance
 
 type Reader (r a : Type) := mkReader {runReader : r -> a};
 
-Reader-fmap {R A B : Type} (f : A -> B) : Reader R A -> Reader R B
+Reader-fmap {R A B : Type} (f : A -> B)
+  : Reader R A -> Reader R B
   | (mkReader ra) := mkReader (f ∘ ra);
 
 Reader-Functor-NoNamed {R : Type} : Functor (Reader R) :=