@@ -282,10 +282,12 @@ infer' v@(Constructor c) = do
282 Just (_, _, ty, _) -> do (v', ty') <- sndM (introduceSkolemScope <=< replaceAllTypeSynonyms) <=< instantiatePolyTypeWithUnknowns v $ ty
282 Just (_, _, ty, _) -> do (v', ty') <- sndM (introduceSkolemScope <=< replaceAllTypeSynonyms) <=< instantiatePolyTypeWithUnknowns v $ ty
283 return $ TypedValue True v' ty'
283 return $ TypedValue True v' ty'
284infer' (Case vals binders) = do
284infer' (Case vals binders) = do
285− ts <- mapM infer vals
285+ (vals', ts) <- fmap unzip $ forM vals $ \val -> do
286+ TypedValue _ val' ty <- infer val
287+ instantiatePolyTypeWithUnknowns val' ty
286 ret <- fresh
288 ret <- fresh
287− binders' <- checkBinders (map (\(TypedValue _ _ t) -> t) ts) ret binders
289+ binders' <- checkBinders ts ret binders
288− return $ TypedValue True (Case ts binders') ret
290+ return $ TypedValue True (Case vals' binders') ret
289infer' (IfThenElse cond th el) = do
291infer' (IfThenElse cond th el) = do
290 cond' <- check cond tyBoolean
292 cond' <- check cond tyBoolean
291 v2@(TypedValue _ _ t2) <- infer th
293 v2@(TypedValue _ _ t2) <- infer th
@@ -376,7 +378,7 @@ inferBinder val (ConstructorBinder ctor binders) = do
376 go [] ty' = case (val, ty') of
378 go [] ty' = case (val, ty') of
377 (TypeConstructor _, TypeApp _ _) -> throwIncorrectArity
379 (TypeConstructor _, TypeApp _ _) -> throwIncorrectArity
379− _ <- subsumes Nothing val ty'
381+ _ <- val =?= ty'
380 return M.empty
382 return M.empty
381 go (binder : binders') (TypeApp (TypeApp t obj) ret) | t == tyFunction =
383 go (binder : binders') (TypeApp (TypeApp t obj) ret) | t == tyFunction =
382 M.union <$> inferBinder obj binder <*> go binders' ret
384 M.union <$> inferBinder obj binder <*> go binders' ret
@@ -537,8 +539,9 @@ check' (TypedValue checkType val ty1) ty2 = do
537 val''' <- if checkType then withScopedTypeVars moduleName args (check val ty2') else return val
539 val''' <- if checkType then withScopedTypeVars moduleName args (check val ty2') else return val
538 return $ TypedValue checkType val''' ty2'
540 return $ TypedValue checkType val''' ty2'
539check' (Case vals binders) ret = do
541check' (Case vals binders) ret = do
540− vals' <- mapM infer vals
542+ (vals', ts) <- fmap unzip $ forM vals $ \val -> do
541− let ts = map (\(TypedValue _ _ t) -> t) vals'
543+ TypedValue _ val' ty <- infer val
544+ instantiatePolyTypeWithUnknowns val' ty
542 binders' <- checkBinders ts ret binders
545 binders' <- checkBinders ts ret binders
543 return $ TypedValue True (Case vals' binders') ret
546 return $ TypedValue True (Case vals' binders') ret
544check' (IfThenElse cond th el) ty = do
547check' (IfThenElse cond th el) ty = do
@@ -567,14 +570,16 @@ check' (Accessor prop val) ty = do
567 rest <- fresh
570 rest <- fresh
568 val' <- check val (TypeApp tyObject (RCons prop ty rest))
571 val' <- check val (TypeApp tyObject (RCons prop ty rest))
569 return $ TypedValue True (Accessor prop val') ty
572 return $ TypedValue True (Accessor prop val') ty
570−check' (Constructor c) ty = do
573+check' v@(Constructor c) ty = do
571 env <- getEnv
574 env <- getEnv
572 case M.lookup c (dataConstructors env) of
575 case M.lookup c (dataConstructors env) of
573 Nothing -> throwError . errorMessage $ UnknownDataConstructor c Nothing
576 Nothing -> throwError . errorMessage $ UnknownDataConstructor c Nothing
574 Just (_, _, ty1, _) -> do
577 Just (_, _, ty1, _) -> do
575 repl <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1
578 repl <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1
576− _ <- subsumes Nothing repl ty
579+ mv <- subsumes (Just v) repl ty
581+ Nothing -> throwError . errorMessage $ SubsumptionCheckFailed
577− return $ TypedValue True (Constructor c) ty
582+ Just v' -> return $ TypedValue True v' ty
578check' (Let ds val) ty = do
583check' (Let ds val) ty = do
579 (ds', val') <- inferLetBinding [] ds val (`check` ty)
584 (ds', val') <- inferLetBinding [] ds val (`check` ty)
580 return $ TypedValue True (Let ds' val') ty
585 return $ TypedValue True (Let ds' val') ty