[ test ] Fix test

OwO.cabal

@@ -114,6 +114,7 @@ Test-Suite tests
   main-is:          Main.hs
   build-depends:    OwO
                   , base >= 4.8 && < 5
+                  , containers >= 0.5.10 && < 0.7
                   , hspec
                   , process
                   , mtl >= 2.2.1 && < 2.3

src/full/OwO/TypeChecking.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE ConstraintKinds  #-}
 {-# LANGUAGE CPP              #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE LambdaCase       #-}
@@ -36,14 +37,7 @@ import           OwO.TypeChecking.Reduce
 literalType :: LiteralInfo -> Type
 literalType _ = Var __TODO__
 
---checkDecl ::
-
-typeCheckFile
-  :: ( MonadState TCState m
-     , MonadError TCError m
-     )
-  => PsiFile
-  -> m ()
+typeCheckFile :: TCM m => PsiFile -> m ()
 typeCheckFile file = do
   let decls       = declarations file
       moduleName  = topLevelModuleName file

src/full/OwO/TypeChecking/Desugar.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE ConstraintKinds  #-}
 {-# LANGUAGE CPP              #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE LambdaCase       #-}
@@ -50,26 +51,22 @@ data DesugarError
   -- ^ Invalid syntax, but allowed by parser, disallowed by desugarer
   deriving (Eq, Show)
 
+type DesugarMonad m = (MonadState AstContext m, MonadError DesugarError m)
+
 concreteToAbstractDecl
-  :: ( MonadState AstContext   m
-     , MonadError DesugarError m
-     )
+  :: DesugarMonad m
   => [PsiDeclaration]
   -> m [DesugarError]
 concreteToAbstractDecl = concreteToAbstractDecl' []
 
 concreteToAbstractTerm
-  :: ( MonadState AstContext   m
-     , MonadError DesugarError m
-     )
+  :: DesugarMonad m
   => PsiTerm
   -> m AstTerm
 concreteToAbstractTerm = concreteToAbstractTerm' []
 
 concreteToAbstractDecl'
-  :: ( MonadState AstContext   m
-     , MonadError DesugarError m
-     )
+  :: DesugarMonad m
   => [TypeSignature]
   -- Unimplemented declarations
   -> [PsiDeclaration]
@@ -121,9 +118,7 @@ concreteToAbstractDecl' sigs (d : ds) =
     checkTerm = concreteToAbstractTerm' []
 
 concreteToAbstractTerm'
-  :: ( MonadState AstContext   m
-     , MonadError DesugarError m
-     )
+  :: DesugarMonad m
   => [AstBinderInfo]
   -- Local variables
   -> PsiTerm

src/full/OwO/TypeChecking/Monad.hs

@@ -1,10 +1,15 @@
+{-# LANGUAGE ConstraintKinds       #-}
 {-# LANGUAGE CPP                   #-}
 {-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE FlexibleContexts      #-}
 
 -- | OwO's type checking state is a state monad transformer.
 --   We call it TypeCheckingMonad, in short TCM, as Agda does.
 module OwO.TypeChecking.Monad where
 
+import           Control.Monad.Except     (MonadError (..))
+import           Control.Monad.State      (MonadState (..))
+
 import qualified Data.Text                as T
 
 import           OwO.Options
@@ -48,3 +53,5 @@ data TCError
   = DesugarErr DesugarError
   | OtherErr String
   deriving (Eq, Show)
+
+type TCM m = (MonadState TCState m, MonadError TCError m)

src/test/Main.hs

@@ -1,15 +1,20 @@
+{-# LANGUAGE FlexibleContexts #-}
 module Main where
 
 -- import           Control.Monad.IO.Class        (liftIO)
+import           Control.Monad.Except          (runExceptT)
 import           Control.Monad.State           (runStateT)
+import           Control.Monad.Identity        (runIdentity)
 import           Data.Either                   (isLeft, isRight)
 import qualified Data.Text                     as T
+import qualified Data.Map                      as Map
 
 import           Test.Hspec
 
 import           System.Exit                   (ExitCode (..), exitWith)
 
 import           OwO.Syntax.Concrete
+import           OwO.Syntax.Context            (emptyCtx)
 import           OwO.Syntax.Module
 import           OwO.Syntax.Parser             (parseNaiveWith)
 import           OwO.Syntax.Parser.NaiveParser as NP
@@ -23,73 +28,75 @@ checkExit n           = exitWith n
 main :: IO ()
 main = hspec $ do
 
-  describe "Simple reference resolving" $ do
-    let pre = parseNaiveWith $ snd <$> NP.declarationsP []
-        p   = (concreteToAbstractDecl <$>) . pre
+  describe "simple reference resolving" $ do
+    let p str = do
+          decls <- flip parseNaiveWith str $ snd <$> NP.declarationsP []
+          let tcm = concreteToAbstractDecl decls
+          runExceptT $ runStateT tcm emptyCtx
 
     let ok (Right (Right _)) = True
         ok _ = False
 
-    it "Should resolve built-in definitions" $ do
+    it "should resolve built-in definitions" $ do
       p "{ a = Type }" `shouldSatisfy` ok
       p "{ id = Type -> Type }" `shouldSatisfy` ok
       p "{ id = Type1 -> Type2 }" `shouldSatisfy` ok
       p "{ id = TypeInf -> Type0 }" `shouldSatisfy` ok
 
-    it "Should resolve contextual definitions" $ do
+    it "should resolve contextual definitions" $ do
       p "{ a = Type; b = a }" `shouldSatisfy` ok
       p "{ postulate { a : Type } ; id = a -> a }" `shouldSatisfy` ok
       p "{ id = \\x -> x }" `shouldSatisfy` ok
 
-    it "Should give unresolved-reference" $ do
+    it "should give unresolved-reference" $ do
       let notOk (Right (Left (UnresolvedReferenceError _))) = True
           notOk _ = False
       p "{ a = b }" `shouldSatisfy` notOk
       p "{ a : b }" `shouldSatisfy` notOk
       p "{ id = \\x -> y }" `shouldSatisfy` notOk
 
-    it "Should give unimplemented errors" $ do
-      let notOk (Right (Left (NoImplementationError _))) = True
+    it "should give unimplemented errors" $ do
+      let notOk (Right (Right (NoImplementationError _ : _, _))) = True
           notOk _ = False
       p "{ a : Type }" `shouldSatisfy` notOk
       p "{ id : Type -> Type }" `shouldSatisfy` notOk
 
   describe "Infix declaration parsing" $ do
 
-    it "Should not parse incorrect infix declarations" $ do
+    it "should not parse incorrect infix declarations" $ do
       let p = parseNaiveWith NP.fixityP
       p "infixl 1 233"  `shouldSatisfy` isLeft
       p "infixr +"      `shouldSatisfy` isLeft
       p "infix 1"       `shouldSatisfy` isLeft
 
-    it "Should parse simple infix declarations" $ do
+    it "should parse simple infix declarations" $ do
       let p = parseNaiveWith NP.fixityP
       p "infixl 1 +"  `shouldSatisfy` isRight
       p "infixr 2 -"  `shouldSatisfy` isRight
       p "infix 3 <|>" `shouldSatisfy` isRight
 
   describe "Type signature parsing" $ do
 
-    it "Should not parse errored files" $ do
+    it "should not parse errored files" $ do
       let p = parseNaiveSimple
       p "module A where\na :" `shouldSatisfy` isLeft
       p "module B where\n: b" `shouldSatisfy` isLeft
 
-    it "Should parse simple type signatures" $ do
+    it "should parse simple type signatures" $ do
       let p = parseNaiveSimple
       p "module A where\na : b" `shouldSatisfy` isRight
       p "module A where\na:b"   `shouldSatisfy` isRight
 
   describe "Module name parsing" $ do
 
-    it "Should not work for errored files" $ do
+    it "should not work for errored files" $ do
       let p = parseNaiveSimple
       p ""             `shouldSatisfy` isLeft
       p "module"       `shouldSatisfy` isLeft
       p "module where" `shouldSatisfy` isLeft
       p "where"        `shouldSatisfy` isLeft
 
-    it "Should parse module name" $ do
+    it "should parse module name" $ do
       let p s = moduleNameList . topLevelModuleName <$> parseNaiveSimple s
       p "module A where\n"     `shouldBe` Right [T.pack "A"]
       p "module A.B where\n"   `shouldBe` Right (T.pack <$> ["A", "B"])