@@ -282,10 +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− ts <- mapM infer vals
285+ (vals', ts) <- instantiateForBinders vals binders
286286 ret <- fresh
287− binders' <- checkBinders (map (\(TypedValue _ _ t) -> t) ts) ret binders
288− return $ TypedValue True (Case ts binders') ret
287+ binders' <- checkBinders ts ret binders
288+ return $ TypedValue True (Case vals' binders') ret
289289infer' (IfThenElse cond th el) = do
290290 cond' <- check cond tyBoolean
291291 v2@(TypedValue _ _ t2) <- infer th
@@ -376,7 +376,7 @@ inferBinder val (ConstructorBinder ctor binders) = do
376376 go [] ty' = case (val, ty') of
377377 (TypeConstructor _, TypeApp _ _) -> throwIncorrectArity
378378 _ -> do
379− _ <- subsumes Nothing val ty'
379+ _ <- val =?= ty'
380380 return M.empty
381381 go (binder : binders') (TypeApp (TypeApp t obj) ret) | t == tyFunction =
382382 M.union <$> inferBinder obj binder <*> go binders' ret
@@ -408,6 +408,26 @@ inferBinder val (NamedBinder name binder) = do
408408inferBinder val (PositionedBinder pos _ binder) =
409409 warnAndRethrowWithPosition pos $ inferBinder val binder
410410
411+-- | Returns true if a binder requires its argument type to be a monotype.
412+-- | If this is the case, we need to instantiate any polymorphic types before checking binders.
413+binderRequiresMonotype :: Binder -> Bool
414+binderRequiresMonotype NullBinder = False
415+binderRequiresMonotype (VarBinder _) = False
416+binderRequiresMonotype (NamedBinder _ b) = binderRequiresMonotype b
417+binderRequiresMonotype (PositionedBinder _ _ b) = binderRequiresMonotype b
418+binderRequiresMonotype _ = True
419+
420+-- | Instantiate polytypes only when necessitated by a binder.
421+instantiateForBinders :: [Expr] -> [CaseAlternative] -> UnifyT Type Check ([Expr], [Type])
422+instantiateForBinders vals cas = fmap unzip $ zipWithM (\val inst -> do
423+ TypedValue _ val' ty <- infer val
424+ if inst
425+ then instantiatePolyTypeWithUnknowns val' ty
426+ else return (val', ty)) vals shouldInstantiate
427+ where
428+ shouldInstantiate :: [Bool]
429+ shouldInstantiate = map (any binderRequiresMonotype) . transpose . map caseAlternativeBinders $ cas
430+
411431-- |
412432-- Check the types of the return values in a set of binders in a case statement
413433--
@@ -537,8 +557,7 @@ check' (TypedValue checkType val ty1) ty2 = do
537557 val''' <- if checkType then withScopedTypeVars moduleName args (check val ty2') else return val
538558 return $ TypedValue checkType val''' ty2'
539559check' (Case vals binders) ret = do
540− vals' <- mapM infer vals
541− let ts = map (\(TypedValue _ _ t) -> t) vals'
560+ (vals', ts) <- instantiateForBinders vals binders
542561 binders' <- checkBinders ts ret binders
543562 return $ TypedValue True (Case vals' binders') ret
544563check' (IfThenElse cond th el) ty = do
@@ -567,14 +586,16 @@ check' (Accessor prop val) ty = do
567586 rest <- fresh
568587 val' <- check val (TypeApp tyObject (RCons prop ty rest))
569588 return $ TypedValue True (Accessor prop val') ty
570−check' (Constructor c) ty = do
589+check' v@(Constructor c) ty = do
571590 env <- getEnv
572591 case M.lookup c (dataConstructors env) of
573592 Nothing -> throwError . errorMessage $ UnknownDataConstructor c Nothing
574593 Just (_, _, ty1, _) -> do
575594 repl <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1
576− _ <- subsumes Nothing repl ty
577− return $ TypedValue True (Constructor c) ty
595+ mv <- subsumes (Just v) repl ty
596+ case mv of
597+ Nothing -> throwError . errorMessage $ SubsumptionCheckFailed
598+ Just v' -> return $ TypedValue True v' ty
578599check' (Let ds val) ty = do
579600 (ds', val') <- inferLetBinding [] ds val (`check` ty)
580601 return $ TypedValue True (Let ds' val') ty