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