Stop weakening the AST (#628)

waspc/src/Wasp/Analyzer/Evaluator.hs

@@ -26,7 +26,7 @@ evalStmts :: [AST.WithCtx AST.TypedStmt] -> Eval [Decl]
 evalStmts = traverse evalStmt
 
 evalStmt :: AST.WithCtx AST.TypedStmt -> Eval Decl
-evalStmt (AST.WithCtx _ctx (AST.Decl name param (Type.DeclType declTypeName))) = do
+evalStmt (AST.WithCtx _ctx (AST.Decl declName declBody (Type.DeclType declTypeName))) = do
   declType <-
     asks
       ( fromMaybe
@@ -35,9 +35,9 @@ evalStmt (AST.WithCtx _ctx (AST.Decl name param (Type.DeclType declTypeName))) =
       )
   typeDefs <- ask
   bindings <- get
-  case TD.dtEvaluate declType typeDefs bindings name param of
+  case TD.dtEvaluate declType typeDefs bindings declName declBody of
     Left err -> throwError err
-    Right decl -> modify (H.insert name decl) >> return decl
+    Right decl -> modify (H.insert declName decl) >> return decl
 evalStmt (AST.WithCtx _ AST.Decl {}) = error "impossible: Decl statement has non-Decl type after type checking"
 
 type Eval a = StateT Bindings (ReaderT TD.TypeDefinitions (Except EvaluationError)) a

waspc/src/Wasp/Analyzer/TypeChecker/Internal.hs

@@ -20,7 +20,8 @@
 --
 -- In this second phase, the types of the argument to each declaration are checked
 -- to ensure they are valid for the declaration type. The implementation of the
--- type inference rules is in "inferExprType", "unifyTypes", and "weaken".
+-- type inference rules is in "inferExprType", "unify", "unifyTypes", and
+-- "checkIsSubTypeOf".
 module Wasp.Analyzer.TypeChecker.Internal
   ( check,
     hoistDeclarations,
@@ -29,14 +30,14 @@ module Wasp.Analyzer.TypeChecker.Internal
     inferExprType,
     unify,
     unifyTypes,
-    weaken,
+    checkIsSubTypeOf,
   )
 where
 
 import Control.Arrow (left, second)
-import Control.Monad (foldM, void)
+import Control.Monad (foldM)
 import qualified Data.HashMap.Strict as M
-import Data.List.NonEmpty (NonEmpty ((:|)), nonEmpty, toList)
+import Data.List.NonEmpty (NonEmpty ((:|)), nonEmpty)
 import Data.Maybe (fromJust)
 import Wasp.Analyzer.Parser (AST)
 import qualified Wasp.Analyzer.Parser as P
@@ -66,10 +67,10 @@ checkStmt (P.WithCtx ctx (P.Decl typeName name expr)) =
     Nothing -> throw $ mkTypeError ctx $ NoDeclarationType typeName
     Just (TD.DeclType _ expectedType _) -> do
       -- Decides whether the argument to the declaration has the correct type
-      mTypedExpr <- weaken expectedType <$> inferExprType expr
-      case mTypedExpr of
-        Left e -> throw $ mkTypeError ctx $ WeakenError e
-        Right typedExpr -> return $ WithCtx ctx $ Decl name typedExpr (DeclType typeName)
+      typedExpr <- inferExprType expr
+      case typedExpr `checkIsSubTypeOf` expectedType of
+        Left e -> throw $ mkTypeError ctx $ CoercionError e
+        Right () -> return $ WithCtx ctx $ Decl name typedExpr (DeclType typeName)
 
 -- | Determine the type of an expression, following the inference rules described in
 -- the wasplang document. Some of these rules are referenced by name in the comments
@@ -100,8 +101,8 @@ inferExprType = P.withCtx $ \ctx -> \case
       -- Apply [EmptyList].
       Nothing -> return $ WithCtx ctx $ List [] EmptyListType
       Just (Left e) -> throw e
-      Just (Right (unifiedValues, unifiedType)) ->
-        return $ WithCtx ctx $ List (toList unifiedValues) (ListType unifiedType)
+      Just (Right unifiedType) ->
+        return $ WithCtx ctx $ List typedValues (ListType unifiedType)
   -- Apply [Dict], and also check that there are no duplicate keys in the dictionary.
   P.Dict entries -> do
     typedEntries <- mapM (\(key, expr) -> (key,) <$> inferExprType expr) entries
@@ -130,24 +131,17 @@ inferExprType = P.withCtx $ \ctx -> \case
       | key `M.member` m = throw $ mkTypeError ctx $ DictDuplicateField key
       | otherwise = return $ M.insert key value m
 
--- | Finds the strongest common type for all of the given expressions, "common" meaning
--- all the expressions can be typed with it and "strongest" meaning it is as specific
--- as possible. If such a type exists, it returns that type and all of the given expressions
--- typed with the new type. If no such type exists, it returns an error.
+-- | Finds the strongest common type for all of the given expressions, "common"
+-- meaning all the expressions can be typed with it and "strongest" meaning it
+-- is as specific as possible. If such a type exists, it returns that type. If
+-- no such type exists, it returns an error.
 --
--- The following property is gauranteed:
---
--- * IF   @unify ctx exprs == Right (exprs', commonType)@
---   THEN @all ((==commonType) . exprType . fromWithCtx) exprs'@
---
--- First argument, `Ctx`, is the context of the top level structure or smth that contains all these expressions.
-unify :: P.Ctx -> NonEmpty (WithCtx TypedExpr) -> Either TypeError (NonEmpty (WithCtx TypedExpr), Type)
-unify ctx texprs@((WithCtx _ texprFirst) :| texprsRest) = do
-  superType <-
-    left (mkTypeError ctx . UnificationError) $
-      foldM unifyTypes (exprType texprFirst) texprsRest
-  left (mkTypeError ctx . WeakenError) $
-    (,superType) <$> mapM (weaken superType) texprs
+-- First argument, `Ctx`, is the context of the top level structure or smth that
+-- contains all these expressions.
+unify :: P.Ctx -> NonEmpty (WithCtx TypedExpr) -> Either TypeError Type
+unify ctx ((WithCtx _ texprFirst) :| texprsRest) = left (mkTypeError ctx . UnificationError) superTypeOrError
+  where
+    superTypeOrError = foldM unifyTypes (exprType texprFirst) texprsRest
 
 -- | @unifyTypes t texpr@ finds the strongest type that both type @t@ and
 -- type of typed expression @texpr@ are a sub-type of.
@@ -201,58 +195,46 @@ unifyTypes t@(DictType dict1EntryTypes) texpr@(WithCtx _ (Dict dict2Entries (Dic
     annotateError key = left (TypeCoercionError texpr t . ReasonDictWrongKeyType key)
 unifyTypes t texpr = Left $ TypeCoercionError texpr t ReasonUncoercable
 
--- | Converts a typed expression from its current type to the given weaker type, "weaker"
--- meaning it is a super-type of the original type. If that is possible, it returns the
--- converted expression. If not, an error is returned.
---
--- The following property is guaranteed:
---
--- * If @weaken typ expr == Right expr'@ then @(exprType . fromWithCtx) expr' == typ@
---
--- When a @Left@ value is returned, then @expr@ can not be typed as @typ@.
-weaken :: Type -> WithCtx TypedExpr -> Either TypeCoercionError (WithCtx TypedExpr)
-weaken t texprwc@(WithCtx _ texpr)
-  | exprType texpr == t = Right texprwc
--- Apply [AnyList]: An empty list can be weakened to any list type
-weaken t@(ListType _) (WithCtx ctx (List [] EmptyListType)) = return $ WithCtx ctx $ List [] t
--- A non-empty list can be weakened to type @t@ if
+-- | Checks that a typed expression is a subtype of a given type. If it isn't,
+-- it returns an error.
+checkIsSubTypeOf :: WithCtx TypedExpr -> Type -> Either TypeCoercionError ()
+checkIsSubTypeOf (WithCtx _ texpr) t | exprType texpr == t = return ()
+-- Apply [AnyList]: An empty list is subtype of any list type
+checkIsSubTypeOf (WithCtx _ (List [] EmptyListType)) (ListType _) = return ()
+-- A non-empty list is subtype of type @t@ if
 -- - @t@ is of the form @ListType elemType@
--- - Every value in the list can be weakened to type @elemType@
-weaken t@(ListType elemType) texprwc@(WithCtx ctx ((List elems _))) = do
-  elems' <- annotateError $ mapM (weaken elemType) elems
-  return $ WithCtx ctx $ List elems' t
+-- - Every value in the list is subtype of type @elemType@
+checkIsSubTypeOf texprwc@(WithCtx _ ((List elems _))) (ListType elemType) =
+  -- To get more detailed error messages, instead of only comparing list types
+  -- directly, we recurisvely check the subtype relationship for each list
+  -- element.
+  annotateError $ mapM_ (`checkIsSubTypeOf` elemType) elems
   where
     annotateError = left (TypeCoercionError texprwc elemType . ReasonList)
-weaken t@(DictType entryTypes) texprwc@(WithCtx ctx (Dict entries _)) = do
-  entries' <- mapM weakenEntry entries
-  mapM_ ensureExprSatisifiesEntryType $ M.toList entryTypes
-  return $ WithCtx ctx $ Dict entries' t
+checkIsSubTypeOf texprwc@(WithCtx _ (Dict entries _)) t@(DictType expectedEntryTypes) = do
+  mapM_ checkEntryHasExpectedType entries
+  mapM_ checkEntryExistsIfRequired $ M.toList expectedEntryTypes
   where
-    -- Tries to apply [DictSome] and [DictNone] rules to the entries of the dict
-    weakenEntry :: (Identifier, WithCtx TypedExpr) -> Either TypeCoercionError (Identifier, WithCtx TypedExpr)
-    weakenEntry (key, value) = case M.lookup key entryTypes of
-      -- @key@ is missing from @typ'@ => extra keys are not allowed
+    checkEntryHasExpectedType :: (Identifier, WithCtx TypedExpr) -> Either TypeCoercionError ()
+    checkEntryHasExpectedType entry@(key, _) = getExpectedTypeOfEntry key >>= (entry `checkIsDictEntrySubtypeOf`)
+
+    getExpectedTypeOfEntry :: Identifier -> Either TypeCoercionError DictEntryType
+    getExpectedTypeOfEntry key = case M.lookup key expectedEntryTypes of
       Nothing -> Left $ TypeCoercionError texprwc t (ReasonDictExtraKey key)
-      -- @key@ is required and present => only need to weaken the value's type
-      Just (DictRequired valueTyp) -> (key,) <$> annotateKeyTypeError key (weaken valueTyp value)
-      -- @key@ is optional and present => weaken value's type + use [DictSome]
-      Just (DictOptional valueTyp) -> (key,) <$> annotateKeyTypeError key (weaken valueTyp value)
+      Just typ -> return typ
+
+    checkIsDictEntrySubtypeOf :: (Identifier, WithCtx TypedExpr) -> DictEntryType -> Either TypeCoercionError ()
+    checkIsDictEntrySubtypeOf (key, entryExpr) expectedEntryType =
+      annotateKeyTypeError key (entryExpr `checkIsSubTypeOf` dictEntryType expectedEntryType)
 
     -- Checks that all DictRequired entries in typ' exist in entries
-    ensureExprSatisifiesEntryType :: (Identifier, DictEntryType) -> Either TypeCoercionError ()
-    ensureExprSatisifiesEntryType (key, DictOptional typ) = case lookup key entries of
-      -- @key@ is optional and missing => use [DictNone]
-      Nothing -> Right ()
-      -- @key@ is optional and present => weaken the value's type + use [DictSome]
-      Just entryVal -> void $ annotateKeyTypeError key $ weaken typ entryVal
-    ensureExprSatisifiesEntryType (key, DictRequired typ) = case lookup key entries of
-      -- @key@ is required and missing => not allowed
+    checkEntryExistsIfRequired :: (Identifier, DictEntryType) -> Either TypeCoercionError ()
+    checkEntryExistsIfRequired (_, DictOptional _) = return ()
+    checkEntryExistsIfRequired (key, DictRequired _) = case lookup key entries of
       Nothing -> Left $ TypeCoercionError texprwc t (ReasonDictNoKey key)
-      -- @key@ is required and present => only need to weaken value's type
-      Just entryVal -> void $ annotateKeyTypeError key $ weaken typ entryVal
+      Just _ -> return ()
 
     -- Wraps a ReasonDictWrongKeyType error around a type error
     annotateKeyTypeError :: String -> Either TypeCoercionError a -> Either TypeCoercionError a
     annotateKeyTypeError key = left (TypeCoercionError texprwc t . ReasonDictWrongKeyType key)
--- All other cases can not be weakened
-weaken typ' expr = Left $ TypeCoercionError expr typ' ReasonUncoercable
+checkIsSubTypeOf expr typ' = Left $ TypeCoercionError expr typ' ReasonUncoercable

waspc/src/Wasp/Analyzer/TypeChecker/TypeError.hs

@@ -20,16 +20,18 @@ newtype TypeError = TypeError (WithCtx TypeError')
 
 {- ORMOLU_DISABLE -}
 data TypeError'
-  -- | Type coercion error that occurs when trying to "unify" the type T1 of typed expression with some other type T2.
-  -- If there is a super type that both T2 and T1 can be safely coerced to, "unify" will succeed, but if not,
+  -- | Type coercion error that occurs when trying to "unify" the type T1 of
+  -- typed expression with some other type T2.  If there is a super type that
+  -- both T2 and T1 can be safely coerced to, "unify" will succeed, but if not,
   -- we get this error.
-  -- We use "unify" in the TypeChecker when trying to infer the common type for typed expressions that we know
-  -- should be of the same type (e.g. for elements in the list).
+  -- We use "unify" in the TypeChecker when trying to infer the common type for
+  -- typed expressions that we know should be of the same type (e.g. for
+  -- elements in the list).
   = UnificationError    TypeCoercionError
-  -- | Type coercion error that occurs when trying to "weaken" the typed expression from its type T1 to some type T2.
-  -- If T2 is super type of T1 and T1 can be safely coerced to T2, "weaken" will succeed, but if not, we get this error.
-  -- We use "weaken" in the TypeChecker when trying to match inferred type of typed expression with some expected type.
-  | WeakenError         TypeCoercionError
+  -- | Type coercion error that occurs when trying to use the typed expression
+  -- of type T1 where T2 is expected.  If T2 is a super type of T1 and T1 can be
+  -- safely coerced to T2, no problem, but if not, we get this error.
+  | CoercionError       TypeCoercionError
   | NoDeclarationType   TypeName
   | UndefinedIdentifier Identifier
   | QuoterUnknownTag    QuoterTag
@@ -53,13 +55,13 @@ getErrorMessageAndCtx (TypeError (WithCtx ctx typeError)) = case typeError of
   (QuoterUnknownTag quoterTag) -> ("Unknown quoter tag: " ++ quoterTag, ctx)
   (DictDuplicateField dictFieldName) -> ("Duplicate dictionary field: " ++ dictFieldName, ctx)
   (UnificationError e) -> getUnificationErrorMessageAndCtx e
-  (WeakenError e) -> getWeakenErrorMessageAndCtx e
+  (CoercionError e) -> getCoercionErrorMessageAndCtx e
 
 -- TypeCoercionError <typed expression> <type which we tried to coerce the typed expression to/with> <reason>
 data TypeCoercionError = TypeCoercionError (WithCtx TypedExpr) Type (TypeCoercionErrorReason TypeCoercionError)
   deriving (Eq, Show)
 
--- | Describes a reason that a @UnificationError@ or @WeakenError@ happened
+-- | Describes a reason that a @UnificationError@ or @CoercionError@ happened
 data TypeCoercionErrorReason e
   = -- | A coercion involving a DeclType and a different type happened. For example,
     -- @unifyTypes (DeclType "foo") (DeclType "bar")@ and
@@ -90,8 +92,8 @@ getUnificationErrorMessageAndCtx = getTypeCoercionErrorMessageAndCtx $
         concatShortPrefixAndText " - " (show $ exprType texpr)
       ]
 
-getWeakenErrorMessageAndCtx :: TypeCoercionError -> (String, Ctx)
-getWeakenErrorMessageAndCtx = getTypeCoercionErrorMessageAndCtx $
+getCoercionErrorMessageAndCtx :: TypeCoercionError -> (String, Ctx)
+getCoercionErrorMessageAndCtx = getTypeCoercionErrorMessageAndCtx $
   \t texpr ->
     intercalate
       "\n"

waspc/src/Wasp/Analyzer/TypeDefinitions/Class/IsDeclType.hs

@@ -30,9 +30,9 @@ import qualified Wasp.AppSpec.Core.Decl as AppSpecDecl
 class (Typeable a, AppSpecDecl.IsDecl a) => IsDeclType a where
   declType :: DeclType
 
-  -- | Evaluates a given Wasp "TypedExpr" to a value of type @a@, assuming given
-  -- typed expression is of declaration type described by @dtBodyType . declType@
-  -- and @dtName . declType@ (otherwise throws an error).
+  -- | Evaluates a given Wasp "TypedExpr" to @a@, assuming given typed
+  -- expression is a subtype of declaration type described by @dtBodyType .
+  -- declType@ and @dtName . declType@ (otherwise throws an error).
   --
   -- For @declEvaluate typeDefs bindings declBodyExpr@:
   -- - "typeDefs" is the type definitions used in the Analyzer

waspc/src/Wasp/Analyzer/TypeDefinitions/TH/Common.hs

@@ -11,6 +11,6 @@ nameToLowerFirstStringLiteralExpr = litE . stringL . toLowerFirst . nameBase
 nameToStringLiteralExpr :: Name -> ExpQ
 nameToStringLiteralExpr = litE . stringL . nameBase
 
--- | @genFunc name expr@ writes a function like @name = expr@
-genFunc :: Name -> ExpQ -> DecQ
-genFunc name expr = funD name [clause [] (normalB expr) []]
+-- | @genVal name expr@ defines a value binding like @name = expr@
+genVal :: Name -> ExpQ -> DecQ
+genVal name expr = valD (varP name) (normalB expr) []

waspc/src/Wasp/Analyzer/TypeDefinitions/TH/Decl.hs

@@ -181,7 +181,7 @@ genIsDeclTypeInstanceDefinitionFromRecordDataConstructor typeName dataConstructo
 -- A helper function for 'genPrimDecl' and 'genRecDecl'.
 genIsDeclTypeInstanceDefinition :: Name -> Name -> ExpQ -> ExpQ -> [DecQ]
 genIsDeclTypeInstanceDefinition typeName dataConstructorName bodyTypeE evaluateE =
-  [ genFunc
+  [ genVal
       'declType
       [|
         DeclType
@@ -191,7 +191,7 @@ genIsDeclTypeInstanceDefinition typeName dataConstructorName bodyTypeE evaluateE
               makeDecl @ $(conT typeName) declName <$> declEvaluate typeDefs bindings declBodyExpr
           }
         |],
-    genFunc 'declEvaluate evaluateE
+    genVal 'declEvaluate evaluateE
   ]
 
 --------------- Kind, Wasp Type and Evaluation of a Haskell type ------------------

waspc/src/Wasp/Analyzer/TypeDefinitions/TH/Enum.hs

@@ -7,7 +7,7 @@ where
 
 import Language.Haskell.TH
 import Wasp.Analyzer.TypeDefinitions (EnumType (..), IsEnumType (..))
-import Wasp.Analyzer.TypeDefinitions.TH.Common
+import qualified Wasp.Analyzer.TypeDefinitions.TH.Common as THC
 
 -- | @makeEnumType ''Type@ writes an @IsEnumType@ instance for @Type@. A type
 -- error is raised if @Type@ does not fit the criteria described below.
@@ -47,31 +47,35 @@ makeEnumType typeName = do
       instanceDefinition = makeIsEnumTypeDefinition typeName dataConstructorNames
   sequence [instanceDeclaration]
 
+namesOfEnumDataConstructors :: [Con] -> Q [Name]
+namesOfEnumDataConstructors = mapM conName
+  where
+    conName (NormalC name []) = pure name
+    conName _ = fail "Enum variant should have only one value"
+
 makeIsEnumTypeDefinition :: Name -> [Name] -> Q [DecQ]
 makeIsEnumTypeDefinition typeName dataConstructorNames =
   pure
-    [ genFunc
-        'enumType
-        [|
-          EnumType
-            { etName = $(nameToLowerFirstStringLiteralExpr typeName),
-              etVariants = $(listE $ map nameToStringLiteralExpr dataConstructorNames)
-            }
-          |],
-      genEnumFromVariants dataConstructorNames
+    [ genEnumType typeName dataConstructorNames,
+      genEnumEvaluate dataConstructorNames
     ]
 
-genEnumFromVariants :: [Name] -> DecQ
-genEnumFromVariants dataConstructorNames = do
+genEnumType :: Name -> [Name] -> DecQ
+genEnumType typeName dataConstructorNames =
+  THC.genVal
+    'enumType
+    [|
+      EnumType
+        { etName = $(THC.nameToLowerFirstStringLiteralExpr typeName),
+          etVariants = $(listE $ map THC.nameToStringLiteralExpr dataConstructorNames)
+        }
+      |]
+
+genEnumEvaluate :: [Name] -> DecQ
+genEnumEvaluate dataConstructorNames = do
   let clauses = map genClause dataConstructorNames
   let invalidVariantClause = clause [[p|_|]] (normalB [|Nothing|]) []
   funD 'enumEvaluate (clauses ++ [invalidVariantClause])
   where
     genClause :: Name -> ClauseQ
     genClause name = clause [litP $ stringL $ nameBase name] (normalB [|Just $(conE name)|]) []
-
-namesOfEnumDataConstructors :: [Con] -> Q [Name]
-namesOfEnumDataConstructors = mapM conName
-  where
-    conName (NormalC name []) = pure name
-    conName _ = fail "Enum variant should have only one value"

waspc/test/Analyzer/TypeChecker/InternalTest.hs

@@ -1,6 +1,7 @@
 module Analyzer.TypeChecker.InternalTest where
 
 import Analyzer.TestUtil (ctx, fromWithCtx)
+import Data.Either (isLeft)
 import qualified Data.HashMap.Strict as H
 import Data.List.NonEmpty (NonEmpty ((:|)))
 import Test.Tasty.Hspec
@@ -67,35 +68,103 @@ spec_Internal = do
         wctx6 = WithCtx ctx6
         wctx7 = WithCtx ctx7
 
-    describe "unify" $ do
-      it "Doesn't affect 2 expressions of the same type" $ do
-        property $ \(a, b) ->
-          let initial = wctx2 (IntegerLiteral a) :| [wctx3 $ DoubleLiteral b]
-              actual = unify ctx1 initial
-           in actual == Right (initial, NumberType)
-      it "Unifies two same-typed dictionaries to their original type" $ do
-        let typ = DictType $ H.fromList [("a", DictRequired BoolType), ("b", DictOptional NumberType)]
-        let a = wctx2 $ Dict [("a", wctx3 $ BoolLiteral True), ("b", wctx4 $ IntegerLiteral 2)] typ
-        let b = wctx5 $ Dict [("a", wctx6 $ BoolLiteral True), ("b", wctx7 $ DoubleLiteral 3.14)] typ
-        let texprs = a :| [b]
-        unify ctx1 texprs
-          `shouldBe` Right (texprs, typ)
-      it "Unifies an empty dict and a dict with one property" $ do
-        let a = wctx2 $ Dict [] (DictType H.empty)
-        let b = wctx3 $ Dict [("a", wctx4 $ BoolLiteral True)] (DictType $ H.singleton "a" $ DictRequired BoolType)
-        let expectedType = DictType $ H.singleton "a" $ DictOptional BoolType
-        fmap (fmap (exprType . fromWithCtx) . fst) (unify ctx1 (a :| [b]))
-          `shouldBe` Right (expectedType :| [expectedType])
-      it "Is idempotent when unifying an empty dict and a singleton dict" $ do
-        let a = wctx2 $ Dict [] (DictType H.empty)
-        let b = wctx3 $ Dict [("a", wctx4 $ BoolLiteral True)] $ DictType $ H.singleton "a" $ DictRequired BoolType
-        unify ctx1 (a :| [b]) `shouldBe` (unify ctx1 (a :| [b]) >>= unify ctx1 . fst)
-      it "Unifies an empty list with any other list" $ do
-        let a = wctx2 $ List [] EmptyListType
-        let b = wctx3 $ List [wctx4 $ StringLiteral "a"] (ListType StringType)
-        let expected = ListType StringType
-        fmap (fmap (exprType . fromWithCtx) . fst) (unify ctx1 (a :| [b]))
-          `shouldBe` Right (expected :| [expected])
+    describe "check" $ do
+      describe "Correctly type checks an AST" $ do
+        it "When a declaration is used before its definition" $ do
+          let typeDefs =
+                TD.TypeDefinitions
+                  { TD.declTypes =
+                      H.fromList
+                        [ ("person", TD.DeclType "person" (DictType $ H.singleton "favoritePet" (DictRequired $ DeclType "pet")) undefined),
+                          ("pet", TD.DeclType "pet" (DictType H.empty) undefined)
+                        ],
+                    TD.enumTypes = H.empty
+                  }
+          let ast =
+                P.AST
+                  [ wctx1 $ P.Decl "person" "John" $ wctx2 $ P.Dict [("favoritePet", wctx3 $ P.Var "Riu")],
+                    wctx4 $ P.Decl "pet" "Riu" $ wctx5 $ P.Dict []
+                  ]
+          let actual = run typeDefs $ check ast
+          let expected =
+                Right $
+                  TypedAST
+                    [ wctx1 $
+                        Decl
+                          "John"
+                          ( wctx2 $
+                              Dict
+                                [("favoritePet", wctx3 $ Var "Riu" (DeclType "pet"))]
+                                (DictType $ H.singleton "favoritePet" (DictRequired $ DeclType "pet"))
+                          )
+                          (DeclType "person"),
+                      wctx4 $
+                        Decl
+                          "Riu"
+                          (wctx5 $ Dict [] (DictType H.empty))
+                          (DeclType "pet")
+                    ]
+
+          actual `shouldBe` expected
+
+    describe "checkStmt" $ do
+      it "Type checks existing declaration type with correct argument" $ do
+        let ast = wctx1 $ P.Decl "string" "App" $ wctx2 $ P.StringLiteral "Wasp"
+        let typeDefs =
+              TD.TypeDefinitions
+                { TD.declTypes = H.singleton "string" (TD.DeclType "string" StringType undefined),
+                  TD.enumTypes = H.empty
+                }
+        let actual = run typeDefs $ checkStmt ast
+        let expected = Right $ wctx1 $ Decl "App" (wctx2 $ StringLiteral "Wasp") (DeclType "string")
+        actual `shouldBe` expected
+      it "Fails to type check non-existant declaration type" $ do
+        let ast = wctx1 $ P.Decl "string" "App" $ wctx2 $ P.StringLiteral "Wasp"
+        let actual = run TD.empty $ checkStmt ast
+        actual `shouldBe` Left (mkTypeError ctx1 $ NoDeclarationType "string")
+      it "Fails to type check existing declaration type with incorrect argument" $ do
+        let ast = wctx1 $ P.Decl "string" "App" $ wctx2 $ P.IntegerLiteral 5
+        let typeDefs =
+              TD.TypeDefinitions
+                { TD.declTypes = H.singleton "string" (TD.DeclType "string" StringType undefined),
+                  TD.enumTypes = H.empty
+                }
+        let actual = run typeDefs $ checkStmt ast
+        let expectedError =
+              mkTypeError ctx1 $
+                CoercionError $
+                  TypeCoercionError
+                    (wctx2 $ IntegerLiteral 5)
+                    StringType
+                    ReasonUncoercable
+        actual `shouldBe` Left expectedError
+
+      describe "A declaration statement with a body of type T satisfies a declaration type definition with a body of type S, when T is subtype of S." $ do
+        it "When S is a dict with an optional field, and T is a dict with a required field" $ do
+          let ast = wctx1 $ P.Decl "typeWithOptional" "Foo" $ wctx2 $ P.Dict [("val", wctx3 $ P.StringLiteral "Bar")]
+          let typeDefs =
+                TD.TypeDefinitions
+                  { TD.declTypes =
+                      H.singleton "typeWithOptional" $
+                        TD.DeclType
+                          "typeWithOptional"
+                          (DictType $ H.singleton "val" (DictOptional StringType))
+                          undefined,
+                    TD.enumTypes = H.empty
+                  }
+          let actual = run typeDefs $ checkStmt ast
+          let expected =
+                Right $
+                  wctx1 $
+                    Decl
+                      "Foo"
+                      ( wctx2 $
+                          Dict
+                            [("val", wctx3 $ StringLiteral "Bar")]
+                            (DictType $ H.singleton "val" (DictRequired StringType))
+                      )
+                      (DeclType "typeWithOptional")
+          actual `shouldBe` expected
 
     describe "inferExprType" $ do
       testSuccess "Types string literals as StringType" (wctx1 $ P.StringLiteral "string") StringType
@@ -215,59 +284,95 @@ spec_Internal = do
           )
           (TupleType (NumberType, StringType, [NumberType]))
 
-    describe "checkStmt" $ do
-      it "Type checks existing declaration type with correct argument" $ do
-        let ast = wctx1 $ P.Decl "string" "App" $ wctx2 $ P.StringLiteral "Wasp"
-        let typeDefs =
-              TD.TypeDefinitions
-                { TD.declTypes = H.singleton "string" (TD.DeclType "string" StringType undefined),
-                  TD.enumTypes = H.empty
-                }
-        let actual = run typeDefs $ checkStmt ast
-        let expected = Right $ wctx1 $ Decl "App" (wctx2 $ StringLiteral "Wasp") (DeclType "string")
-        actual `shouldBe` expected
-      it "Fails to type check non-existant declaration type" $ do
-        let ast = wctx1 $ P.Decl "string" "App" $ wctx2 $ P.StringLiteral "Wasp"
-        let actual = run TD.empty $ checkStmt ast
-        actual `shouldBe` Left (mkTypeError ctx1 $ NoDeclarationType "string")
-      it "Fails to type check existing declaration type with incorrect argument" $ do
-        let ast = wctx1 $ P.Decl "string" "App" $ wctx2 $ P.IntegerLiteral 5
-        let typeDefs =
-              TD.TypeDefinitions
-                { TD.declTypes = H.singleton "string" (TD.DeclType "string" StringType undefined),
-                  TD.enumTypes = H.empty
-                }
-        let actual = run typeDefs $ checkStmt ast
-        let expectedError =
-              mkTypeError ctx1 $
-                WeakenError $
-                  TypeCoercionError
-                    (wctx2 $ IntegerLiteral 5)
-                    StringType
-                    ReasonUncoercable
-        actual `shouldBe` Left expectedError
-      it "Type checks declaration with dict type with an argument that unifies to the correct type" $ do
-        let ast = wctx1 $ P.Decl "maybeString" "App" $ wctx2 $ P.Dict [("val", wctx3 $ P.StringLiteral "Wasp")]
-        let typeDefs =
-              TD.TypeDefinitions
-                { TD.declTypes =
-                    H.singleton "maybeString" $
-                      TD.DeclType
-                        "maybeString"
-                        (DictType $ H.singleton "val" (DictOptional StringType))
-                        undefined,
-                  TD.enumTypes = H.empty
-                }
-        let actual = run typeDefs $ checkStmt ast
-        let expected =
-              Right $
-                wctx1 $
-                  Decl
-                    "App"
-                    ( wctx2 $
-                        Dict
-                          [("val", wctx3 $ StringLiteral "Wasp")]
-                          (DictType $ H.singleton "val" (DictOptional StringType))
-                    )
-                    (DeclType "maybeString")
-        actual `shouldBe` expected
+    describe "unify" $ do
+      it "Correctly unifies two expressions of the same type" $ do
+        property $ \(a, b) ->
+          let initial = wctx2 (IntegerLiteral a) :| [wctx3 $ DoubleLiteral b]
+              actual = unify ctx1 initial
+           in actual == Right NumberType
+      it "Correctly unifies two dictionaries of the same type" $ do
+        let typ = DictType $ H.fromList [("a", DictRequired BoolType), ("b", DictOptional NumberType)]
+        let a = wctx2 $ Dict [("a", wctx3 $ BoolLiteral True), ("b", wctx4 $ IntegerLiteral 2)] typ
+        let b = wctx5 $ Dict [("a", wctx6 $ BoolLiteral True), ("b", wctx7 $ DoubleLiteral 3.14)] typ
+        let texprs = a :| [b]
+        unify ctx1 texprs `shouldBe` Right typ
+      it "Unifies an empty dict and a dict with one property" $ do
+        let a = wctx2 $ Dict [] (DictType H.empty)
+        let b = wctx3 $ Dict [("a", wctx4 $ BoolLiteral True)] (DictType $ H.singleton "a" $ DictRequired BoolType)
+        let expectedType = DictType $ H.singleton "a" $ DictOptional BoolType
+        unify ctx1 (a :| [b]) `shouldBe` Right expectedType
+      it "Unifies an empty list with any other list" $ do
+        let a = wctx2 $ List [] EmptyListType
+        let b = wctx3 $ List [wctx4 $ StringLiteral "a"] (ListType StringType)
+        let expected = ListType StringType
+        unify ctx1 (a :| [b]) `shouldBe` Right expected
+
+    describe "checkIsSubTypeOf" $ do
+      describe "for lists" $ do
+        let emptyListExpr = wctx1 $ List [] EmptyListType
+        it "should confirm that an empty list is a subtype of any list" $ do
+          checkIsSubTypeOf emptyListExpr EmptyListType `shouldBe` Right ()
+          checkIsSubTypeOf emptyListExpr (ListType StringType) `shouldBe` Right ()
+          checkIsSubTypeOf emptyListExpr (ListType $ DictType H.empty) `shouldBe` Right ()
+        it "should confirm that an empty list is NOT a subtype of a non-list type" $ do
+          isLeft (checkIsSubTypeOf emptyListExpr NumberType) `shouldBe` True
+          isLeft (checkIsSubTypeOf emptyListExpr (DictType H.empty)) `shouldBe` True
+        it "should confirm that a non-empty list is NOT a subtype of an empty list" $ do
+          let integerListExpr = wctx1 $ List [wctx2 $ IntegerLiteral 5] (ListType NumberType)
+          isLeft (checkIsSubTypeOf integerListExpr EmptyListType) `shouldBe` True
+        it "should confirm that a list with elements of type T1 is a subtype of list with elements of type T2 when T1 is a subtype of T2" $ do
+          let listOfEmptyLists = wctx1 $ List [wctx2 $ List [] EmptyListType] (ListType EmptyListType)
+          checkIsSubTypeOf listOfEmptyLists (ListType $ ListType StringType) `shouldBe` Right ()
+
+      describe "for dictionaries" $ do
+        let d1Type = DictType $ H.fromList [("a", DictRequired BoolType), ("b", DictRequired NumberType)]
+        let d1Expr = wctx1 $ Dict [("a", wctx2 $ BoolLiteral True), ("b", wctx3 $ IntegerLiteral 2)] d1Type
+
+        describe "should confirm that a dict expr D1 is subtype of dict type D2 when" $ do
+          it "D2 is type of D1" $ do
+            checkIsSubTypeOf d1Expr d1Type `shouldBe` Right ()
+          it "D1 contains all fields specified by D2 (and only those), where D2 has some optional fields" $ do
+            let d2Type = DictType $ H.fromList [("a", DictRequired BoolType), ("b", DictOptional NumberType)]
+            checkIsSubTypeOf d1Expr d2Type `shouldBe` Right ()
+          it "D1 contains all required fields specified by D2 (and only those), where D2 has some optional fields" $ do
+            let d2Type =
+                  DictType $
+                    H.fromList
+                      [ ("a", DictRequired BoolType),
+                        ("b", DictRequired NumberType),
+                        ("c", DictOptional NumberType)
+                      ]
+            checkIsSubTypeOf d1Expr d2Type `shouldBe` Right ()
+          it "D2 has a field of type T1 and D1 has a field of type T2, where T1 is a subtype of T2" $ do
+            let d1Type' = DictType $ H.fromList [("a", DictRequired EmptyListType)]
+            let d1Expr' = wctx1 $ Dict [("a", wctx2 $ List [] EmptyListType)] d1Type'
+            let d2Type' = DictType $ H.fromList [("a", DictRequired $ ListType StringType)]
+            checkIsSubTypeOf d1Expr' d2Type' `shouldBe` Right ()
+
+        describe "should confirm that a dict expr D1 is NOT a subtype of dict type D2 when" $ do
+          it "D1 contains a field not specified by D2" $ do
+            let d2Type = DictType $ H.fromList [("a", DictRequired BoolType)]
+            isLeft (checkIsSubTypeOf d1Expr d2Type) `shouldBe` True
+          it "D1 does contain a field specified by D2 but has different type" $ do
+            let d2Type = DictType $ H.fromList [("a", DictRequired BoolType), ("b", DictOptional BoolType)]
+            isLeft (checkIsSubTypeOf d1Expr d2Type) `shouldBe` True
+          it "D1 does not contain a required field specified by D2" $ do
+            let d2Type =
+                  DictType $
+                    H.fromList
+                      [ ("a", DictRequired BoolType),
+                        ("b", DictOptional NumberType),
+                        ("c", DictRequired NumberType)
+                      ]
+            isLeft (checkIsSubTypeOf d1Expr d2Type) `shouldBe` True
+
+      it "should fail for non-related types" $ do
+        isLeft (checkIsSubTypeOf (wctx1 $ IntegerLiteral 5) StringType) `shouldBe` True
+        isLeft (checkIsSubTypeOf (wctx1 $ StringLiteral "a") EmptyListType) `shouldBe` True
+        isLeft (checkIsSubTypeOf (wctx1 $ List [wctx2 $ IntegerLiteral 5] (ListType NumberType)) BoolType) `shouldBe` True
+        isLeft
+          ( checkIsSubTypeOf
+              (wctx1 $ Dict [("a", wctx2 $ IntegerLiteral 5)] (DictType H.empty))
+              (ListType StringType)
+          )
+          `shouldBe` True

waspc/test/Analyzer/TypeCheckerTest.hs

@@ -62,7 +62,7 @@ spec_TypeChecker = do
         let actual = typeCheck typeDefs ast
         let expectedError =
               mkTypeError ctx1 $
-                WeakenError $
+                CoercionError $
                   TypeCoercionError (wctx2 $ IntegerLiteral 5) StringType ReasonUncoercable
         actual `shouldBe` Left expectedError
       it "Properly hoists declarations" $ do
@@ -105,6 +105,6 @@ spec_TypeChecker = do
         let expected =
               Right $
                 TypedAST
-                  [ wctx1 $ Decl "Bedrooms" (wctx2 $ List [] (ListType StringType)) (DeclType "rooms")
+                  [ wctx1 $ Decl "Bedrooms" (wctx2 $ List [] EmptyListType) (DeclType "rooms")
                   ]
         actual `shouldBe` expected