@@ -95,11 +95,6 @@ unifyTypes t1 t2 = rethrow (\e -> "Error unifying type " ++ prettyPrintType t1 +
9595 sk <- skolemize ident ty1
9696 sk `unifyTypes` ty2
9797 unifyTypes' ty f@(ForAll _ _) = f `unifyTypes` ty
98− unifyTypes' Number Number = return ()
99− unifyTypes' String String = return ()
100− unifyTypes' Boolean Boolean = return ()
101− unifyTypes' Array Array = return ()
102− unifyTypes' Function Function = return ()
10398 unifyTypes' (Object row1) (Object row2) = row1 ?= row2
10499 unifyTypes' (TypeVar v1) (TypeVar v2) | v1 == v2 = return ()
105100 unifyTypes' (TypeConstructor c1) (TypeConstructor c2) = do
@@ -253,12 +248,7 @@ entails moduleName context goal@(className, ty) = do
253248-- and return a substitution from type variables to types which makes the type heads unify.
254249--
255250typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String, Type)]
256−typeHeadsAreEqual _ _ String String = Just []
257−typeHeadsAreEqual _ _ Number Number = Just []
258−typeHeadsAreEqual _ _ Boolean Boolean = Just []
259251typeHeadsAreEqual _ _ (Skolem s1) (Skolem s2) | s1 == s2 = Just []
260−typeHeadsAreEqual _ _ Array Array = Just []
261−typeHeadsAreEqual _ _ Function Function = Just []
262252typeHeadsAreEqual m e (TypeConstructor c1) (TypeConstructor c2) | typeConstructorsAreEqual e m c1 c2 = Just []
263253typeHeadsAreEqual m e (TypeApp h1 (TypeVar v)) (TypeApp h2 arg) = (:) (v, arg) <$> typeHeadsAreEqual m e h1 h2
264254typeHeadsAreEqual m e t1@(TypeApp _ _) t2@(TypeApp _ (TypeVar _)) = typeHeadsAreEqual m e t2 t1
@@ -390,13 +380,13 @@ infer val = rethrow (\e -> "Error inferring type of term " ++ prettyPrintValue v
390380-- Infer a type for a value
391381--
392382infer' :: Value -> UnifyT Check Value
393−infer' v@(NumericLiteral _) = return $ TypedValue True v Number
394−infer' v@(StringLiteral _) = return $ TypedValue True v String
395−infer' v@(BooleanLiteral _) = return $ TypedValue True v Boolean
383+infer' v@(NumericLiteral _) = return $ TypedValue True v tyNumber
384+infer' v@(StringLiteral _) = return $ TypedValue True v tyString
385+infer' v@(BooleanLiteral _) = return $ TypedValue True v tyBoolean
396386infer' (ArrayLiteral vals) = do
397387 ts <- mapM infer vals
398388 els <- fresh
399− forM_ ts $ \(TypedValue _ _ t) -> els ?= TypeApp Array t
389+ forM_ ts $ \(TypedValue _ _ t) -> els ?= TypeApp tyArray t
400390 return $ TypedValue True (ArrayLiteral ts) els
401391infer' (Unary op val) = do
402392 v <- infer val
@@ -421,9 +411,9 @@ infer' (ObjectUpdate o ps) = do
421411 return $ TypedValue True (ObjectUpdate o' newVals) $ Object $ rowFromList (newTys, row)
422412infer' (Indexer index val) = do
423413 el <- fresh
424− index' <- check index Number
425− val' <- check val (TypeApp Array el)
426− return $ TypedValue True (Indexer (TypedValue True index' Number) (TypedValue True val' (TypeApp Array el))) el
414+ index' <- check index tyNumber
415+ val' <- check val (TypeApp tyArray el)
416+ return $ TypedValue True (Indexer (TypedValue True index' tyNumber) (TypedValue True val' (TypeApp tyArray el))) el
427417infer' (Accessor prop val) = do
428418 typed@(TypedValue _ _ objTy) <- infer val
429419 propTy <- inferProperty objTy prop
@@ -473,7 +463,7 @@ infer' (Case vals binders) = do
473463 binders' <- checkBinders (map (\(TypedValue _ _ t) -> t) ts) ret binders
474464 return $ TypedValue True (Case ts binders') ret
475465infer' (IfThenElse cond th el) = do
476− cond' <- check cond Boolean
466+ cond' <- check cond tyBoolean
477467 v2@(TypedValue _ _ t2) <- infer th
478468 v3@(TypedValue _ _ t3) <- infer el
479469 t2 ?= t3
@@ -528,9 +518,9 @@ checkUnary op val res =
528518-- Built-in unary operators
529519--
530520unaryOps :: [(UnaryOperator, (Type, Type))]
531−unaryOps = [ (Negate, (Number, Number))
532− , (Not, (Boolean, Boolean))
533− , (BitwiseNot, (Number, Number))
521+unaryOps = [ (Negate, (tyNumber, tyNumber))
522+ , (Not, (tyBoolean, tyBoolean))
523+ , (BitwiseNot, (tyNumber, tyNumber))
534524 ]
535525
536526-- |
@@ -539,7 +529,7 @@ unaryOps = [ (Negate, (Number, Number))
539529inferBinary :: BinaryOperator -> Value -> Value -> UnifyT Check Value
540530inferBinary op left@(TypedValue _ _ leftTy) right@(TypedValue _ _ rightTy) | isEqualityTest op = do
541531 leftTy ?= rightTy
542− return $ TypedValue True (Binary op left right) Boolean
532+ return $ TypedValue True (Binary op left right) tyBoolean
543533inferBinary op left@(TypedValue _ _ leftTy) right@(TypedValue _ _ rightTy) =
544534 case fromMaybe (error "Invalid operator") $ lookup op binaryOps of
545535 (valTy, resTy) -> do
@@ -553,7 +543,7 @@ inferBinary _ _ _ = error "Invalid arguments to inferBinary"
553543--
554544checkBinary :: BinaryOperator -> Value -> Value -> Type -> UnifyT Check Value
555545checkBinary op left right res | isEqualityTest op = do
556− res ?= Boolean
546+ res ?= tyBoolean
557547 left'@(TypedValue _ _ t1) <- infer left
558548 right'@(TypedValue _ _ t2) <- infer right
559549 t1 ?= t2
@@ -578,24 +568,24 @@ isEqualityTest _ = False
578568-- Built-in binary operators
579569--
580570binaryOps :: [(BinaryOperator, (Type, Type))]
581−binaryOps = [ (Add, (Number, Number))
582− , (Subtract, (Number, Number))
583− , (Multiply, (Number, Number))
584− , (Divide, (Number, Number))
585− , (Modulus, (Number, Number))
586− , (BitwiseAnd, (Number, Number))
587− , (BitwiseOr, (Number, Number))
588− , (BitwiseXor, (Number, Number))
589− , (ShiftRight, (Number, Number))
590− , (ZeroFillShiftRight, (Number, Number))
591− , (And, (Boolean, Boolean))
592− , (Or, (Boolean, Boolean))
593− , (Concat, (String, String))
594− , (Modulus, (Number, Number))
595− , (LessThan, (Number, Boolean))
596− , (LessThanOrEqualTo, (Number, Boolean))
597− , (GreaterThan, (Number, Boolean))
598− , (GreaterThanOrEqualTo, (Number, Boolean))
571+binaryOps = [ (Add, (tyNumber, tyNumber))
572+ , (Subtract, (tyNumber, tyNumber))
573+ , (Multiply, (tyNumber, tyNumber))
574+ , (Divide, (tyNumber, tyNumber))
575+ , (Modulus, (tyNumber, tyNumber))
576+ , (BitwiseAnd, (tyNumber, tyNumber))
577+ , (BitwiseOr, (tyNumber, tyNumber))
578+ , (BitwiseXor, (tyNumber, tyNumber))
579+ , (ShiftRight, (tyNumber, tyNumber))
580+ , (ZeroFillShiftRight, (tyNumber, tyNumber))
581+ , (And, (tyBoolean, tyBoolean))
582+ , (Or, (tyBoolean, tyBoolean))
583+ , (Concat, (tyString, tyString))
584+ , (Modulus, (tyNumber, tyNumber))
585+ , (LessThan, (tyNumber, tyBoolean))
586+ , (LessThanOrEqualTo, (tyNumber, tyBoolean))
587+ , (GreaterThan, (tyNumber, tyBoolean))
588+ , (GreaterThanOrEqualTo, (tyNumber, tyBoolean))
599589 ]
600590
601591-- |
@@ -603,9 +593,9 @@ binaryOps = [ (Add, (Number, Number))
603593--
604594inferBinder :: Type -> Binder -> UnifyT Check (M.Map Ident Type)
605595inferBinder _ NullBinder = return M.empty
606−inferBinder val (StringBinder _) = val ?= String >> return M.empty
607−inferBinder val (NumberBinder _) = val ?= Number >> return M.empty
608−inferBinder val (BooleanBinder _) = val ?= Boolean >> return M.empty
596+inferBinder val (StringBinder _) = val ?= tyString >> return M.empty
597+inferBinder val (NumberBinder _) = val ?= tyNumber >> return M.empty
598+inferBinder val (BooleanBinder _) = val ?= tyBoolean >> return M.empty
609599inferBinder val (VarBinder name) = return $ M.singleton name val
610600inferBinder val (NullaryBinder ctor) = do
611601 env <- getEnv
@@ -622,7 +612,7 @@ inferBinder val (UnaryBinder ctor binder) = do
622612 Just (ty, _) -> do
623613 fn <- replaceAllVarsWithUnknowns ty
624614 case fn of
625− TypeApp (TypeApp Function obj) ret -> do
615+ TypeApp (TypeApp t obj) ret | t == tyFunction -> do
626616 _ <- subsumes Nothing val ret
627617 inferBinder obj binder
628618 _ -> throwError $ "Constructor " ++ show ctor ++ " is not a unary constructor"
@@ -644,13 +634,13 @@ inferBinder val (ObjectBinder props) = do
644634inferBinder val (ArrayBinder binders) = do
645635 el <- fresh
646636 m1 <- M.unions <$> mapM (inferBinder el) binders
647− val ?= TypeApp Array el
637+ val ?= TypeApp tyArray el
648638 return m1
649639inferBinder val (ConsBinder headBinder tailBinder) = do
650640 el <- fresh
651641 m1 <- inferBinder el headBinder
652642 m2 <- inferBinder val tailBinder
653− val ?= TypeApp Array el
643+ val ?= TypeApp tyArray el
654644 return $ m1 `M.union` m2
655645inferBinder val (NamedBinder name binder) = do
656646 m <- inferBinder val binder
@@ -669,7 +659,7 @@ checkBinders nvals ret ((binders, grd, val):bs) = do
669659 case grd of
670660 Nothing -> return (binders, Nothing, val')
671661 Just g -> do
672− g' <- check g Boolean
662+ g' <- check g tyBoolean
673663 return (binders, Just g', val')
674664 rs <- checkBinders nvals ret bs
675665 return $ r : rs
@@ -701,7 +691,7 @@ checkStatement mass _ (Assignment ident val) = do
701691 Just ty -> do t ?= ty
702692 return (False, mass, Assignment ident val')
703693checkStatement mass ret (While val inner) = do
704− val' <- check val Boolean
694+ val' <- check val tyBoolean
705695 (allCodePathsReturn, _, inner') <- checkBlock mass ret inner
706696 return (allCodePathsReturn, mass, While val' inner')
707697checkStatement mass ret (If ifst) = do
@@ -710,9 +700,9 @@ checkStatement mass ret (If ifst) = do
710700checkStatement mass ret (For ident start end inner) = do
711701 Just moduleName <- checkCurrentModule <$> get
712702 assignVariable ident
713− start' <- check start Number
714− end' <- check end Number
715− (allCodePathsReturn, _, inner') <- bindLocalVariables moduleName [(ident, Number)] $ checkBlock mass ret inner
703+ start' <- check start tyNumber
704+ end' <- check end tyNumber
705+ (allCodePathsReturn, _, inner') <- bindLocalVariables moduleName [(ident, tyNumber)] $ checkBlock mass ret inner
716706 return (allCodePathsReturn, mass, For ident start' end' inner')
717707checkStatement mass ret (Return val) = do
718708 val' <- check val ret
@@ -723,11 +713,11 @@ checkStatement mass ret (Return val) = do
723713--
724714checkIfStatement :: M.Map Ident Type -> Type -> IfStatement -> UnifyT Check (Bool, IfStatement)
725715checkIfStatement mass ret (IfStatement val thens Nothing) = do
726− val' <- check val Boolean
716+ val' <- check val tyBoolean
727717 (_, _, thens') <- checkBlock mass ret thens
728718 return (False, IfStatement val' thens' Nothing)
729719checkIfStatement mass ret (IfStatement val thens (Just elses)) = do
730− val' <- check val Boolean
720+ val' <- check val tyBoolean
731721 (allCodePathsReturn1, _, thens') <- checkBlock mass ret thens
732722 (allCodePathsReturn2, elses') <- checkElseStatement mass ret elses
733723 return (allCodePathsReturn1 && allCodePathsReturn2, IfStatement val' thens' (Just elses'))
@@ -802,17 +792,17 @@ check' val u@(TUnknown _) = do
802792 ty' <- replaceAllVarsWithUnknowns ty
803793 ty' ?= u
804794 return val'
805−check' v@(NumericLiteral _) Number = return v
806−check' v@(StringLiteral _) String = return v
807−check' v@(BooleanLiteral _) Boolean = return v
795+check' v@(NumericLiteral _) t | t == tyNumber = return v
796+check' v@(StringLiteral _) t | t == tyString = return v
797+check' v@(BooleanLiteral _) t | t == tyBoolean = return v
808798check' (Unary op val) ty = checkUnary op val ty
809799check' (Binary op left right) ty = checkBinary op left right ty
810−check' (ArrayLiteral vals) (TypeApp Array ty) = ArrayLiteral <$> forM vals (\val -> check val ty)
800+check' (ArrayLiteral vals) (TypeApp a ty) | a == tyArray = ArrayLiteral <$> forM vals (\val -> check val ty)
811801check' (Indexer index vals) ty = do
812− index' <- check index Number
813− vals' <- check vals (TypeApp Array ty)
802+ index' <- check index tyNumber
803+ vals' <- check vals (TypeApp tyArray ty)
814804 return $ Indexer index' vals'
815−check' (Abs arg ret) (TypeApp (TypeApp Function argTy) retTy) = do
805+check' (Abs arg ret) (TypeApp (TypeApp t argTy) retTy) | t == tyFunction = do
816806 Just moduleName <- checkCurrentModule <$> get
817807 ret' <- bindLocalVariables moduleName [(arg, argTy)] $ check ret retTy
818808 return $ Abs arg ret'
@@ -844,7 +834,7 @@ check' (Case vals binders) ret = do
844834 binders' <- checkBinders ts ret binders
845835 return $ Case vals' binders'
846836check' (IfThenElse cond th el) ty = do
847− cond' <- check cond Boolean
837+ cond' <- check cond tyBoolean
848838 th' <- check th ty
849839 el' <- check el ty
850840 return $ IfThenElse cond' th' el'
@@ -932,7 +922,7 @@ checkFunctionApplication fn fnTy arg ret = rethrow errorMessage $ checkFunctionA
932922-- Check the type of a function application
933923--
934924checkFunctionApplication' :: Value -> Type -> Value -> Type -> UnifyT Check Value
935−checkFunctionApplication' fn (TypeApp (TypeApp Function argTy) retTy) arg ret = do
925+checkFunctionApplication' fn (TypeApp (TypeApp t argTy) retTy) arg ret | t == tyFunction = do
936926 arg' <- check arg argTy
937927 _ <- subsumes Nothing retTy ret
938928 return $ App fn arg'
@@ -978,7 +968,7 @@ subsumes' :: Maybe Value -> Type -> Type -> UnifyT Check (Maybe Value)
978968subsumes' val (ForAll ident ty1) ty2 = do
979969 replaced <- replaceVarWithUnknown ident ty1
980970 subsumes val replaced ty2
981−subsumes' val (TypeApp (TypeApp Function arg1) ret1) (TypeApp (TypeApp Function arg2) ret2) = do
971+subsumes' val (TypeApp (TypeApp f1 arg1) ret1) (TypeApp (TypeApp f2 arg2) ret2) | f1 == tyFunction && f2 == tyFunction = do
982972 subsumes Nothing arg2 arg1
983973 subsumes Nothing ret1 ret2
984974 return val