typechecker is compatible with one extra addition to the spec

Grammar.cf

@@ -46,12 +46,13 @@ Data. Data ::= "data" Indexed "where" "{" [Constructor] "}" ;
 -------------------------------------------------------------------------------
 
 EAnn.   Exp5 ::= "(" Exp ":" Type ")" ;
-EId.    Exp4 ::= Ident ;
+EVar.   Exp4 ::= LIdent ;
+ECons.  Exp4 ::= UIdent ;
 ELit.   Exp4 ::= Lit ;
 EApp.   Exp3 ::= Exp3 Exp4 ;
 EAdd.   Exp1 ::= Exp1 "+" Exp2 ;
 ELet.   Exp  ::= "let" LIdent "=" Exp "in" Exp ; 
-EAbs.   Exp  ::= "\\" Ident "." Exp ;
+EAbs.   Exp  ::= "\\" LIdent "." Exp ;
 ECase.  Exp  ::= "case" Exp "of" "{" [Inj] "}";
 
 -------------------------------------------------------------------------------

language.cabal

@@ -47,6 +47,8 @@ executable language
       , either
       , extra
       , array
+      , hspec
+      , QuickCheck
 
     default-language: GHC2021
 

sample-programs/basic-1

@@ -1,2 +1,2 @@
 f : Int -> Int ;
-f = \x. x+1 ;
+f x = x ;

sample-programs/basic-8

@@ -1,6 +1,6 @@
 data Maybe (a) where {
     Nothing : Maybe (a)
-    Just : forall a. a -> Maybe (a)
+    Just : a -> Maybe (a)
 };
 
 fromJust : Maybe (a) -> a ;

src/Renamer/Renamer.hs

@@ -16,12 +16,12 @@ import Control.Monad.State (
     gets,
     modify,
  )
+import Data.Coerce (coerce)
 import Data.Function (on)
 import Data.Map (Map)
 import Data.Map qualified as Map
 import Data.Maybe (fromMaybe)
 import Data.Tuple.Extra (dupe)
-import Data.Coerce (coerce)
 import Grammar.Abs
 
 -- | Rename all variables and local binds
@@ -91,11 +91,12 @@ newtype Rn a = Rn {runRn :: StateT Cxt (ExceptT String Identity) a}
     deriving (Functor, Applicative, Monad, MonadState Cxt)
 
 -- | Maps old to new name
-type Names = Map Ident Ident
+type Names = Map LIdent LIdent
 
 renameExp :: Names -> Exp -> Rn (Names, Exp)
 renameExp old_names = \case
-    EId n -> pure (coerce old_names, EId . fromMaybe n $ Map.lookup n (coerce old_names))
+    EVar n -> pure (coerce old_names, EVar . fromMaybe n $ Map.lookup n old_names)
+    ECons n -> pure (old_names, ECons n)
     ELit lit -> pure (old_names, ELit lit)
     EApp e1 e2 -> do
         (env1, e1') <- renameExp old_names e1
@@ -170,20 +171,20 @@ substitute tvar1 tvar2 typ = case typ of
     substitute' = substitute tvar1 tvar2
 
 -- | Create a new name and add it to name environment.
-newName :: Names -> Ident -> Rn (Names, Ident)
+newName :: Names -> LIdent -> Rn (Names, LIdent)
 newName env old_name = do
     new_name <- makeName old_name
     pure (Map.insert old_name new_name env, new_name)
 
 -- | Create multiple names and add them to the name environment
-newNames :: Names -> [Ident] -> Rn (Names, [Ident])
+newNames :: Names -> [LIdent] -> Rn (Names, [LIdent])
 newNames = mapAccumM newName
 
 -- | Annotate name with number and increment the number @prefix ⇒ prefix_number@.
-makeName :: Ident -> Rn Ident
+makeName :: LIdent -> Rn LIdent
-makeName (Ident prefix) = do
+makeName (LIdent prefix) = do
     i <- gets var_counter
-    let name = Ident $ prefix ++ "_" ++ show i
+    let name = LIdent $ prefix ++ "_" ++ show i
     modify $ \cxt -> cxt{var_counter = succ cxt.var_counter}
     pure name
 

src/TypeChecker/TypeChecker.hs

@@ -134,6 +134,7 @@ isMoreSpecificOrEq a b = a == b
 
 isPoly :: Type -> Bool
 isPoly (TAll _ _) = True
+isPoly (TVar _) = True
 isPoly _ = False
 
 inferExp :: Exp -> Infer T.ExpT
@@ -193,21 +194,20 @@ algoW = \case
     -- \| ----------------------
     -- \|     Γ ⊢ x : τ, ∅
 
-    EId i -> do
+    EVar i -> do
         var <- asks vars
-        case M.lookup i var of
+        case M.lookup (coerce i) var of
-            Just t -> inst t >>= \(x) -> return (nullSubst, (T.EId (i, x), x))
+            Just t -> inst t >>= \x -> return (nullSubst, (T.EId (coerce i, x), x))
             Nothing -> do
                 sig <- gets sigs
-                case M.lookup i sig of
+                case M.lookup (coerce i) sig of
-                    Just t -> return (nullSubst, (T.EId (i, t), t))
+                    Just t -> return (nullSubst, (T.EId (coerce i, t), t))
-                    Nothing -> do
+                    Nothing -> throwError $ "Unbound variable: " ++ show i
+    ECons i -> do
         constr <- gets constructors
-                        case M.lookup i constr of
+        case M.lookup (coerce i) constr of
-                            Just t -> return (nullSubst, (T.EId (i, t), t))
+            Just t -> return (nullSubst, (T.EId (coerce i, t), t))
-                            Nothing ->
+            Nothing -> throwError $ "Constructor: '" ++ printTree i ++ "' is not defined"
-                                throwError $
-                                    "Unbound variable: " ++ show i
 
     -- \| τ = newvar   Γ, x : τ ⊢ e : τ', S
     -- \| ---------------------------------
@@ -219,7 +219,7 @@ algoW = \case
             (s1, (e', t')) <- algoW e
             let varType = apply s1 fr
             let newArr = T.TFun varType t'
-            return (s1, apply s1 $ (T.EAbs (coerce name, varType) (e', newArr), newArr))
+            return (s1, apply s1 (T.EAbs (coerce name, varType) (e', newArr), newArr))
 
     -- \| Γ ⊢ e₀ : τ₀, S₀    S₀Γ ⊢ e₁ : τ₁, S₁
     -- \| s₂ = mgu(s₁τ₀, Int)    s₃ = mgu(s₂τ₁, Int)
@@ -237,7 +237,7 @@ algoW = \case
             let comp = s4 `compose` s3 `compose` s2 `compose` s1
             return
                 ( comp
-                , apply comp $ (T.EAdd (e0', t0) (e1', t1), int)
+                , apply comp (T.EAdd (e0', t0) (e1', t1), int)
                 )
 
     -- \| Γ ⊢ e₀ : τ₀, S₀    S₀Γ ⊢ e₁ : τ₁, S1
@@ -384,7 +384,7 @@ class FreeVars t where
 instance FreeVars T.Type where
     free :: T.Type -> Set Ident
     free (T.TVar (T.MkTVar a)) = S.singleton a
-    free (T.TAll (T.MkTVar bound) t) = (S.singleton bound) `S.intersection` free t
+    free (T.TAll (T.MkTVar bound) t) = S.singleton bound `S.intersection` free t
     free (T.TLit _) = mempty
     free (T.TFun a b) = free a `S.union` free b
     -- \| Not guaranteed to be correct
@@ -398,7 +398,9 @@ instance FreeVars T.Type where
             T.TVar (T.MkTVar a) -> case M.lookup a sub of
                 Nothing -> T.TVar (T.MkTVar $ coerce a)
                 Just t -> t
-            T.TAll bound t -> undefined
+            T.TAll (T.MkTVar i) t -> case M.lookup i sub of
+                Nothing -> T.TAll (T.MkTVar i) (apply sub t)
+                Just _ -> apply sub t
             T.TFun a b -> T.TFun (apply sub a) (apply sub b)
             T.TIndexed (T.Indexed name a) -> T.TIndexed (T.Indexed name (map (apply sub) a))
 
@@ -416,10 +418,10 @@ instance FreeVars T.ExpT where
         (T.EId (i, innerT), outerT) -> (T.EId (i, apply s innerT), apply s outerT)
         (T.ELit lit, t) -> (T.ELit lit, apply s t)
         (T.ELet (T.Bind (ident, t1) args e1) e2, t2) -> (T.ELet (T.Bind (ident, apply s t1) args (apply s e1)) (apply s e2), apply s t2)
-        (T.EApp e1 e2, t) -> (T.EApp (apply s e1) (apply s e2), (apply s t))
+        (T.EApp e1 e2, t) -> (T.EApp (apply s e1) (apply s e2), apply s t)
-        (T.EAdd e1 e2, t) -> (T.EAdd (apply s e1) (apply s e2), (apply s t))
+        (T.EAdd e1 e2, t) -> (T.EAdd (apply s e1) (apply s e2), apply s t)
-        (T.EAbs (ident, t2) e, t1) -> (T.EAbs (ident, apply s t2) (apply s e), (apply s t1))
+        (T.EAbs (ident, t2) e, t1) -> (T.EAbs (ident, apply s t2) (apply s e), apply s t1)
-        (T.ECase e injs, t) -> (T.ECase (apply s e) (apply s injs), (apply s t))
+        (T.ECase e injs, t) -> (T.ECase (apply s e) (apply s injs), apply s t)
 
 instance FreeVars T.Inj where
     free :: T.Inj -> Set Ident

tests/Tests.hs

@@ -28,75 +28,66 @@ main = hspec $ do
     infer_eann
     infer_eid
     infer_eabs
-    infer_eapp
     test_id_function
 
 infer_elit = describe "algoW used on ELit" $ do
     it "infers the type mono Int" $ do
-        getType (ELit (LInt 0)) `shouldBe` Right (TMono "Int")
+        getType (ELit (LInt 0)) `shouldBe` Right (T.TLit "Int")
 
     it "infers the type mono Int" $ do
-        getType (ELit (LInt 9999)) `shouldBe` Right (TMono "Int")
+        getType (ELit (LInt 9999)) `shouldBe` Right (T.TLit "Int")
 
 infer_eann = describe "algoW used on EAnn" $ do
     it "infers the type and checks if the annotated type matches" $ do
-        getType (EAnn (ELit $ LInt 0) (TMono "Int")) `shouldBe` Right (TMono "Int")
+        getType (EAnn (ELit $ LInt 0) (TLit "Int")) `shouldBe` Right (T.TLit "Int")
 
     it "fails if the annotated type does not match with the inferred type" $ do
-        getType (EAnn (ELit $ LInt 0) (TPol "a")) `shouldSatisfy` isLeft
+        getType (EAnn (ELit $ LInt 0) (TVar $ MkTVar "a")) `shouldSatisfy` isLeft
 
     it "should be possible to annotate with a more specific type" $ do
-        let annotated_lambda = EAnn (EAbs "x" (EId "x")) (TArr (TMono "Int") (TMono "Int"))
+        let annotated_lambda = EAnn (EAbs "x" (EVar "x")) (TFun (TLit "Int") (TLit "Int"))
-         in getType annotated_lambda `shouldBe` Right (TArr (TMono "Int") (TMono "Int"))
+         in getType annotated_lambda `shouldBe` Right (T.TFun (T.TLit "Int") (T.TLit "Int"))
 
     it "should fail if the annotated type is more general than the inferred type" $ do
-        getType (EAnn (ELit (LInt 0)) (TPol "a")) `shouldSatisfy` isLeft
+        getType (EAnn (ELit (LInt 0)) (TVar $ MkTVar "a")) `shouldSatisfy` isLeft
 
     it "should fail if the annotated type is an arrow but the annotated type is not" $ do
-        getType (EAnn (EAbs "x" (EId "x")) (TPol "a")) `shouldSatisfy` isLeft
+        getType (EAnn (EAbs "x" (EVar "x")) (TVar $ MkTVar "a")) `shouldSatisfy` isLeft
 
-infer_eid = describe "algoW used on EId" $ do
+infer_eid = describe "algoW used on EVar" $ do
     it "should fail if the variable is not added to the environment" $ do
-        property $ \x -> getType (EId (Ident (x :: String))) `shouldSatisfy` isLeft
+        property $ \x -> getType (EVar (LIdent (x :: String))) `shouldSatisfy` isLeft
 
     it "should succeed if the type exist in the environment" $ do
         property $ \x -> do
             let env = Env 0 mempty mempty
-            let t = Forall [] (TPol "a")
+            let t = T.TVar $ T.MkTVar "a"
             let ctx = Ctx (M.singleton (Ident (x :: String)) t)
-            getTypeC env ctx (EId (Ident x)) `shouldBe` Right (TPol "a")
+            getTypeC env ctx (EVar (LIdent x)) `shouldBe` Right (T.TVar $ T.MkTVar "a")
 
 infer_eabs = describe "algoW used on EAbs" $ do
     it "should infer the argument type as int if the variable is used as an int" $ do
-        let lambda = EAbs "x" (EAdd (EId "x") (ELit (LInt 0)))
+        let lambda = EAbs "x" (EAdd (EVar "x") (ELit (LInt 0)))
-        getType lambda `shouldBe` Right (TArr (TMono "Int") (TMono "Int"))
+        getType lambda `shouldBe` Right (T.TFun (T.TLit "Int") (T.TLit "Int"))
 
     it "should infer the argument type as polymorphic if it is not used in the lambda" $ do
         let lambda = EAbs "x" (ELit (LInt 0))
         getType lambda `shouldSatisfy` isArrowPolyToMono
 
     it "should infer a variable as function if used as one" $ do
-        let lambda = EAbs "f" (EAbs "x" (EApp (EId "f") (EId "x")))
+        let lambda = EAbs "f" (EAbs "x" (EApp (EVar "f") (EVar "x")))
-        let isOk (Right (TArr (TArr (TPol _) (TPol _)) (TArr (TPol _) (TPol _)))) = True
+        let isOk (Right (T.TFun (T.TFun (T.TVar _) (T.TVar _)) (T.TFun (T.TVar _) (T.TVar _)))) = True
             isOk _ = False
         getType lambda `shouldSatisfy` isOk
 
-infer_eapp = describe "algoW used on EApp" $ do
-    it "should fail if a variable is applied to itself (occurs check)" $ do
-        property $ \x -> do
-            let env = Env 0 mempty mempty
-            let t = Forall [] (TPol "a")
-            let ctx = Ctx (M.singleton (Ident (x :: String)) t)
-            getTypeC env ctx (EApp (EId (Ident x)) (EId (Ident x))) `shouldSatisfy` isLeft
-
 churf_id :: Bind
-churf_id = Bind "id" (TArr (TPol "a") (TPol "a")) "id" ["x"] (EId "x")
+churf_id = Bind "id" ["x"] (EVar "x")
 
 churf_add :: Bind
-churf_add = Bind "add" (TArr (TMono "Int") (TArr (TMono "Int") (TMono "Int"))) "add" ["x", "y"] (EAdd (EId "x") (EId "y"))
+churf_add = Bind "add" ["x", "y"] (EAdd (EVar "x") (EVar "y"))
 
 churf_main :: Bind
-churf_main = Bind "main" (TArr (TMono "Int") (TMono "Int")) "main" [] (EApp (EApp (EId "id") (EId "add")) (ELit (LInt 0)))
+churf_main = Bind "main" [] (EApp (EApp (EVar "id") (EVar "add")) (ELit (LInt 0)))
 
 prg = Program [DBind churf_main, DBind churf_add, DBind churf_id]
 
@@ -106,14 +97,14 @@ test_id_function =
         it "should succeed to find the correct type" $ do
             typecheck prg `shouldSatisfy` isRight
 
-isArrowPolyToMono :: Either Error Type -> Bool
+isArrowPolyToMono :: Either Error T.Type -> Bool
-isArrowPolyToMono (Right (TArr (TPol _) (TMono _))) = True
+isArrowPolyToMono (Right (T.TFun (T.TVar _) (T.TLit _))) = True
 isArrowPolyToMono _ = False
 
 -- | Empty environment
-getType :: Exp -> Either Error Type
+getType :: Exp -> Either Error T.Type
-getType e = pure fst <*> run (inferExp e)
+getType e = pure snd <*> run (inferExp e)
 
 -- | Custom environment
-getTypeC :: Env -> Ctx -> Exp -> Either Error Type
+getTypeC :: Env -> Ctx -> Exp -> Either Error T.Type
-getTypeC env ctx e = pure fst <*> runC env ctx (inferExp e)
+getTypeC env ctx e = pure snd <*> runC env ctx (inferExp e)