From 3bab89662d8981bdc6589339693efa61f367e91b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20=C3=85gren=20Thun=C3=A9?= Date: Thu, 9 Nov 2023 17:12:24 +0100 Subject: [PATCH] Fix inconsistency in handling of Unknown in let annotations --- stdlib/mexpr/type-check.mc | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/stdlib/mexpr/type-check.mc b/stdlib/mexpr/type-check.mc index 5eaf19957..36878ff2c 100644 --- a/stdlib/mexpr/type-check.mc +++ b/stdlib/mexpr/type-check.mc @@ -526,7 +526,7 @@ lang LetTypeCheck = match stripTyAll tyBody with (vars, stripped) in let newTyVars = foldr (lam v. mapInsert v.0 newLvl) env.tyVarEnv vars in let newEnv = {env with currentLvl = newLvl, tyVarEnv = newTyVars} in - let body = typeCheckExpr newEnv (propagateTyAnnot (t.body, stripped)) in + let body = typeCheckExpr newEnv (propagateTyAnnot (t.body, tyAnnot)) in -- Unify the annotated type with the inferred one and generalize unify newEnv [infoTy t.tyAnnot, infoTm body] stripped (tyTm body); (if env.disableRecordPolymorphism then @@ -548,6 +548,7 @@ lang LetTypeCheck = ty = tyTm inexpr} sem propagateTyAnnot = + | (tm, TyAll a) -> propagateTyAnnot (tm, a.ty) | (TmLam l, TyArrow a) -> let body = propagateTyAnnot (l.body, a.to) in let ty = optionGetOr a.from (sremoveUnknown l.tyAnnot) in @@ -580,7 +581,7 @@ lang RecLetsTypeCheck = TypeCheck + RecLetsAst + LetTypeCheck + MetaVarDisableGe if isValue (GVal ()) b.body then let newEnv = {recLetEnv with currentLvl = newLvl, tyVarEnv = newTyVarEnv} in match stripTyAll b.tyBody with (_, stripped) in - let body = typeCheckExpr newEnv (propagateTyAnnot (b.body, stripped)) in + let body = typeCheckExpr newEnv (propagateTyAnnot (b.body, b.tyAnnot)) in -- Unify the inferred type of the body with the annotated one unify newEnv [infoTy b.tyAnnot, infoTm body] stripped (tyTm body); body