@@ -282,12 +282,10 @@ 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− (vals', ts) <- fmap unzip $ forM vals $ \val -> do
286− TypedValue _ val' ty <- infer val
287− instantiatePolyTypeWithUnknowns val' ty
285+ ts <- mapM infer vals
288286 ret <- fresh
289− binders' <- checkBinders ts ret binders
290− return $ TypedValue True (Case vals' binders') ret
287+ binders' <- checkBinders (map (\(TypedValue _ _ t) -> t) ts) ret binders
288+ return $ TypedValue True (Case ts binders') ret
291289infer' (IfThenElse cond th el) = do
292290 cond' <- check cond tyBoolean
293291 v2@(TypedValue _ _ t2) <- infer th
@@ -378,7 +376,7 @@ inferBinder val (ConstructorBinder ctor binders) = do
378376 go [] ty' = case (val, ty') of
379377 (TypeConstructor _, TypeApp _ _) -> throwIncorrectArity
380378 _ -> do
381− _ <- val =?= ty'
379+ _ <- subsumes Nothing val ty'
382380 return M.empty
383381 go (binder : binders') (TypeApp (TypeApp t obj) ret) | t == tyFunction =
384382 M.union <$> inferBinder obj binder <*> go binders' ret
@@ -539,9 +537,8 @@ check' (TypedValue checkType val ty1) ty2 = do
539537 val''' <- if checkType then withScopedTypeVars moduleName args (check val ty2') else return val
540538 return $ TypedValue checkType val''' ty2'
541539check' (Case vals binders) ret = do
542− (vals', ts) <- fmap unzip $ forM vals $ \val -> do
543− TypedValue _ val' ty <- infer val
544− instantiatePolyTypeWithUnknowns val' ty
540+ vals' <- mapM infer vals
541+ let ts = map (\(TypedValue _ _ t) -> t) vals'
545542 binders' <- checkBinders ts ret binders
546543 return $ TypedValue True (Case vals' binders') ret
547544check' (IfThenElse cond th el) ty = do
@@ -570,16 +567,14 @@ check' (Accessor prop val) ty = do
570567 rest <- fresh
571568 val' <- check val (TypeApp tyObject (RCons prop ty rest))
572569 return $ TypedValue True (Accessor prop val') ty
573−check' v@(Constructor c) ty = do
570+check' (Constructor c) ty = do
574571 env <- getEnv
575572 case M.lookup c (dataConstructors env) of
576573 Nothing -> throwError . errorMessage $ UnknownDataConstructor c Nothing
577574 Just (_, _, ty1, _) -> do
578575 repl <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1
579− mv <- subsumes (Just v) repl ty
580− case mv of
581− Nothing -> throwError . errorMessage $ SubsumptionCheckFailed
582− Just v' -> return $ TypedValue True v' ty
576+ _ <- subsumes Nothing repl ty
577+ return $ TypedValue True (Constructor c) ty
583578check' (Let ds val) ty = do
584579 (ds', val') <- inferLetBinding [] ds val (`check` ty)
585580 return $ TypedValue True (Let ds' val') ty