@@ -149,7 +149,7 @@ typeForBindingGroupElement (ident, val) dict untypedDict = do
150-- Check if a value contains a type annotation
150-- Check if a value contains a type annotation
152−isTyped :: (Ident, Expr) -> (Either (Ident, Expr) (Ident, (Expr, Type, Bool)))
152+isTyped :: (Ident, Expr) -> Either (Ident, Expr) (Ident, (Expr, Type, Bool))
153isTyped (name, TypedValue checkType value ty) = Right (name, (value, ty, checkType))
153isTyped (name, TypedValue checkType value ty) = Right (name, (value, ty, checkType))
154isTyped (name, value) = Left (name, value)
154isTyped (name, value) = Left (name, value)
@@ -177,6 +177,14 @@ replaceTypeClassDictionaries mn =
177 entails env mn dicts constraint trySuperclasses
177 entails env mn dicts constraint trySuperclasses
178 go other = return other
178 go other = return other
181+-- Check the kind of a type, failing if it is not of kind *.
183+checkTypeKind :: ModuleName -> Type -> UnifyT t Check ()
184+checkTypeKind moduleName ty = do
185+ kind <- liftCheck $ kindOf moduleName ty
186+ guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
181-- Remove any ForAlls and ConstrainedType constructors in a type by introducing new unknowns
189-- Remove any ForAlls and ConstrainedType constructors in a type by introducing new unknowns
182-- or TypeClassDictionary values.
190-- or TypeClassDictionary values.
@@ -282,8 +290,7 @@ infer' (SuperClassDictionary className tys) = do
282 return $ TypeClassDictionary False (className, tys) dicts
290 return $ TypeClassDictionary False (className, tys) dicts
283infer' (TypedValue checkType val ty) = do
291infer' (TypedValue checkType val ty) = do
284 Just moduleName <- checkCurrentModule <$> get
292 Just moduleName <- checkCurrentModule <$> get
285− kind <- liftCheck $ kindOf moduleName ty
293+ checkTypeKind moduleName ty
286− guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
287 ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
294 ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
288 val' <- if checkType then check val ty' else return val
295 val' <- if checkType then check val ty' else return val
289 return $ TypedValue True val' ty'
296 return $ TypedValue True val' ty'
@@ -294,8 +301,7 @@ inferLetBinding :: [Declaration] -> [Declaration] -> Expr -> (Expr -> UnifyT Typ
294inferLetBinding seen [] ret j = (,) seen <$> makeBindingGroupVisible (j ret)
301inferLetBinding seen [] ret j = (,) seen <$> makeBindingGroupVisible (j ret)
295inferLetBinding seen (ValueDeclaration ident nameKind [] (Right (tv@(TypedValue checkType val ty))) : rest) ret j = do
302inferLetBinding seen (ValueDeclaration ident nameKind [] (Right (tv@(TypedValue checkType val ty))) : rest) ret j = do
296 Just moduleName <- checkCurrentModule <$> get
303 Just moduleName <- checkCurrentModule <$> get
297− kind <- liftCheck $ kindOf moduleName ty
304+ checkTypeKind moduleName ty
298− guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
299 let dict = M.singleton (moduleName, ident) (ty, nameKind, Undefined)
305 let dict = M.singleton (moduleName, ident) (ty, nameKind, Undefined)
300 ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
306 ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
301 TypedValue _ val' ty'' <- if checkType then bindNames dict (check val ty') else return tv
307 TypedValue _ val' ty'' <- if checkType then bindNames dict (check val ty') else return tv
@@ -315,7 +321,7 @@ inferLetBinding seen (BindingGroupDeclaration ds : rest) ret j = do
315 let ds' = [(ident, LocalVariable, val') | (ident, (val', _)) <- ds1' ++ ds2']
321 let ds' = [(ident, LocalVariable, val') | (ident, (val', _)) <- ds1' ++ ds2']
316 makeBindingGroupVisible $ bindNames dict $ inferLetBinding (seen ++ [BindingGroupDeclaration ds']) rest ret j
322 makeBindingGroupVisible $ bindNames dict $ inferLetBinding (seen ++ [BindingGroupDeclaration ds']) rest ret j
317inferLetBinding seen (PositionedDeclaration pos d : ds) ret j = rethrowWithPosition pos $ do
323inferLetBinding seen (PositionedDeclaration pos d : ds) ret j = rethrowWithPosition pos $ do
318− ((d' : ds'), val') <- inferLetBinding seen (d : ds) ret j
324+ (d' : ds', val') <- inferLetBinding seen (d : ds) ret j
319 return (PositionedDeclaration pos d' : ds', val')
325 return (PositionedDeclaration pos d' : ds', val')
320inferLetBinding _ _ _ _ = error "Invalid argument to inferLetBinding"
326inferLetBinding _ _ _ _ = error "Invalid argument to inferLetBinding"
@@ -497,8 +503,7 @@ check' (SuperClassDictionary className tys) _ = do
497 return $ TypeClassDictionary False (className, tys) dicts
503 return $ TypeClassDictionary False (className, tys) dicts
498check' (TypedValue checkType val ty1) ty2 = do
504check' (TypedValue checkType val ty1) ty2 = do
499 Just moduleName <- checkCurrentModule <$> get
505 Just moduleName <- checkCurrentModule <$> get
500− kind <- liftCheck $ kindOf moduleName ty1
506+ checkTypeKind moduleName ty1
501− guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
502 ty1' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1
507 ty1' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1
503 ty2' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty2
508 ty2' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty2
504 val' <- subsumes (Just val) ty1' ty2'
509 val' <- subsumes (Just val) ty1' ty2'
@@ -547,7 +552,7 @@ check' (Constructor c) ty = do
547 _ <- subsumes Nothing repl ty
552 _ <- subsumes Nothing repl ty
548 return $ TypedValue True (Constructor c) ty
553 return $ TypedValue True (Constructor c) ty
549check' (Let ds val) ty = do
554check' (Let ds val) ty = do
550− (ds', val') <- inferLetBinding [] ds val (flip check ty)
555+ (ds', val') <- inferLetBinding [] ds val (`check` ty)
551 return $ TypedValue True (Let ds' val') ty
556 return $ TypedValue True (Let ds' val') ty
552check' val ty | containsTypeSynonyms ty = do
557check' val ty | containsTypeSynonyms ty = do
553 ty' <- introduceSkolemScope <=< expandAllTypeSynonyms $ ty
558 ty' <- introduceSkolemScope <=< expandAllTypeSynonyms $ ty
@@ -575,7 +580,7 @@ checkProperties ps row lax = let (ts, r') = rowToList row in go ps ts r' where
575 go [] [] REmpty = return []
580 go [] [] REmpty = return []
576 go [] [] u@(TUnknown _) = do u =?= REmpty
581 go [] [] u@(TUnknown _) = do u =?= REmpty
577 return []
582 return []
578− go [] [] (Skolem _ _ _) | lax = return []
583+ go [] [] Skolem{} | lax = return []
579 go [] ((p, _): _) _ | lax = return []
584 go [] ((p, _): _) _ | lax = return []
580 | otherwise = throwError $ mkErrorStack ("Object does not have property " ++ p) (Just (ExprError (ObjectLiteral ps)))
585 | otherwise = throwError $ mkErrorStack ("Object does not have property " ++ p) (Just (ExprError (ObjectLiteral ps)))
581 go ((p,_):_) [] REmpty = throwError $ mkErrorStack ("Property " ++ p ++ " is not present in closed object type " ++ prettyPrintRow row) (Just (ExprError (ObjectLiteral ps)))
586 go ((p,_):_) [] REmpty = throwError $ mkErrorStack ("Property " ++ p ++ " is not present in closed object type " ++ prettyPrintRow row) (Just (ExprError (ObjectLiteral ps)))
@@ -638,12 +643,12 @@ checkFunctionApplication' fn u@(TUnknown _) arg ret = do
638checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) arg ret = do
643checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) arg ret = do
639 ty <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs
644 ty <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs
640 checkFunctionApplication fn ty arg ret
645 checkFunctionApplication fn ty arg ret
641−checkFunctionApplication' fn (KindedType ty _) arg ret = do
646+checkFunctionApplication' fn (KindedType ty _) arg ret =
642 checkFunctionApplication fn ty arg ret
647 checkFunctionApplication fn ty arg ret
643checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg ret = do
648checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg ret = do
644 dicts <- getTypeClassDictionaries
649 dicts <- getTypeClassDictionaries
645 checkFunctionApplication' (foldl App fn (map (flip (TypeClassDictionary True) dicts) constraints)) fnTy arg ret
650 checkFunctionApplication' (foldl App fn (map (flip (TypeClassDictionary True) dicts) constraints)) fnTy arg ret
646−checkFunctionApplication' fn fnTy dict@(TypeClassDictionary _ _ _) _ =
651+checkFunctionApplication' fn fnTy dict@TypeClassDictionary{} _ =
647 return (fnTy, App fn dict)
652 return (fnTy, App fn dict)
648checkFunctionApplication' _ fnTy arg _ = throwError . strMsg $ "Cannot apply a function of type "
653checkFunctionApplication' _ fnTy arg _ = throwError . strMsg $ "Cannot apply a function of type "
649 ++ prettyPrintType fnTy
654 ++ prettyPrintType fnTy