@@ -282,10 +282,12 @@ infer' v@(Constructor c) = do
282282 Just (_, _, ty, _) -> do (v', ty') <- sndM (introduceSkolemScope <=< replaceAllTypeSynonyms) <=< instantiatePolyTypeWithUnknowns v $ ty
283283 return $ TypedValue True v' ty'
284284infer' (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
286288 ret <- fresh
287− binders' <- checkBinders (map (\(TypedValue _ _ t) -> t) ts) ret binders
288− return $ TypedValue True (Case ts binders') ret
289+ binders' <- checkBinders ts ret binders
290+ return $ TypedValue True (Case vals' binders') ret
289291infer' (IfThenElse cond th el) = do
290292 cond' <- check cond tyBoolean
291293 v2@(TypedValue _ _ t2) <- infer th
@@ -376,7 +378,7 @@ inferBinder val (ConstructorBinder ctor binders) = do
376378 go [] ty' = case (val, ty') of
377379 (TypeConstructor _, TypeApp _ _) -> throwIncorrectArity
378380 _ -> do
379− _ <- subsumes Nothing val ty'
381+ _ <- val =?= ty'
380382 return M.empty
381383 go (binder : binders') (TypeApp (TypeApp t obj) ret) | t == tyFunction =
382384 M.union <$> inferBinder obj binder <*> go binders' ret
@@ -537,8 +539,9 @@ check' (TypedValue checkType val ty1) ty2 = do
537539 val''' <- if checkType then withScopedTypeVars moduleName args (check val ty2') else return val
538540 return $ TypedValue checkType val''' ty2'
539541check' (Case vals binders) ret = do
540− vals' <- mapM infer vals
541− let ts = map (\(TypedValue _ _ t) -> t) vals'
542+ (vals', ts) <- fmap unzip $ forM vals $ \val -> do
543+ TypedValue _ val' ty <- infer val
544+ instantiatePolyTypeWithUnknowns val' ty
542545 binders' <- checkBinders ts ret binders
543546 return $ TypedValue True (Case vals' binders') ret
544547check' (IfThenElse cond th el) ty = do
@@ -567,14 +570,16 @@ check' (Accessor prop val) ty = do
567570 rest <- fresh
568571 val' <- check val (TypeApp tyObject (RCons prop ty rest))
569572 return $ TypedValue True (Accessor prop val') ty
570−check' (Constructor c) ty = do
573+check' v@(Constructor c) ty = do
571574 env <- getEnv
572575 case M.lookup c (dataConstructors env) of
573576 Nothing -> throwError . errorMessage $ UnknownDataConstructor c Nothing
574577 Just (_, _, ty1, _) -> do
575578 repl <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1
576− _ <- subsumes Nothing repl ty
577− return $ TypedValue True (Constructor c) ty
579+ mv <- subsumes (Just v) repl ty
580+ case mv of
581+ Nothing -> throwError . errorMessage $ SubsumptionCheckFailed
582+ Just v' -> return $ TypedValue True v' ty
578583check' (Let ds val) ty = do
579584 (ds', val') <- inferLetBinding [] ds val (`check` ty)
580585 return $ TypedValue True (Let ds' val') ty