@@ -655,8 +655,8 @@ infer' (IfThenElse cond th el) = do
655655 cond' <- check cond tyBoolean
656656 v2@(TypedValue _ _ t2) <- infer th
657657 v3@(TypedValue _ _ t3) <- infer el
658− t2 =?= t3
659− return $ TypedValue True (IfThenElse cond' v2 v3) t2
658+ (v2', v3', t) <- meet v2 v3 t2 t3
659+ return $ TypedValue True (IfThenElse cond' v2' v3') t
660660infer' (Let ds val) = do
661661 (ds', val'@(TypedValue _ _ valTy)) <- inferLetBinding [] ds val infer
662662 return $ TypedValue True (Let ds' val') valTy
@@ -1119,6 +1119,18 @@ subsumes' val ty1 ty2 = do
11191119 ty1 =?= ty2
11201120 return val
11211121
1122+-- |
1123+-- Compute the meet of two types, i.e. the most general type which both types subsume.
1124+-- TODO: handle constrained types
1125+--
1126+meet :: Expr -> Expr -> Type -> Type -> UnifyT Type Check (Expr, Expr, Type)
1127+meet e1 e2 t1@(ForAll _ _ _) t2 = meet e1 e2 t1 t2
1128+meet e1 e2 t1 (ForAll ident t2 _) = do
1129+ t2' <- replaceVarWithUnknown ident t2
1130+ meet e1 e2 t1 t2'
1131+meet e1 e2 t1 t2 = do
1132+ t1 =?= t2
1133+ return (e1, e2, t1)
11221134
11231135
11241136