diff options
author | Griffin Smith <grfn@gws.fyi> | 2021-03-20T19·11-0400 |
---|---|---|
committer | glittershark <grfn@gws.fyi> | 2021-03-20T20·20+0000 |
commit | e7033bd8b066c8f4163a4f6aa618a39d8110dc6c (patch) | |
tree | db56bc1e6072cec5a0f09ae23b1b26399189d1f9 /users/glittershark/achilles/src | |
parent | e2a3aea4516425ddb2022a85a3d492c605f910d4 (diff) |
fix(gs/achilles): Get rid of universalization step r/2295
The step of "universalizing" function expressions was conflicting with top-level ascriptions for polymorphic function declarations: universalization generates universal type variables, and top-level polymorphic ascription *also* generates universal type variables, and the two were conflicting with each other when unifying. Let's just get rid of this now, and we can bring it back in a more principled manner once we do actual let-generalization (which there's still an ignored test case for) Change-Id: Idc08c8cb5ac92d1e6e1e63c9b8729176cab73f44 Reviewed-on: https://cl.tvl.fyi/c/depot/+/2616 Tested-by: BuildkiteCI Reviewed-by: glittershark <grfn@gws.fyi>
Diffstat (limited to 'users/glittershark/achilles/src')
-rw-r--r-- | users/glittershark/achilles/src/ast/hir.rs | 7 | ||||
-rw-r--r-- | users/glittershark/achilles/src/tc/mod.rs | 90 |
2 files changed, 67 insertions, 30 deletions
diff --git a/users/glittershark/achilles/src/ast/hir.rs b/users/glittershark/achilles/src/ast/hir.rs index 0212b3dbcdbb..691b9607e7e6 100644 --- a/users/glittershark/achilles/src/ast/hir.rs +++ b/users/glittershark/achilles/src/ast/hir.rs @@ -228,6 +228,13 @@ pub enum Decl<'a, T> { } impl<'a, T> Decl<'a, T> { + pub fn name(&self) -> &Ident<'a> { + match self { + Decl::Fun { name, .. } => name, + Decl::Extern { name, .. } => name, + } + } + pub fn type_(&self) -> Option<&T> { match self { Decl::Fun { type_, .. } => Some(type_), diff --git a/users/glittershark/achilles/src/tc/mod.rs b/users/glittershark/achilles/src/tc/mod.rs index 4bca52733bc8..f3cb40a8b010 100644 --- a/users/glittershark/achilles/src/tc/mod.rs +++ b/users/glittershark/achilles/src/tc/mod.rs @@ -262,10 +262,10 @@ impl<'ast> Typechecker<'ast> { let body = self.tc_expr(body)?; self.env.pop(); Ok(hir::Expr::Fun { - type_: self.universalize( - args.iter().map(|(_, ty)| ty.clone()).collect(), - body.type_().clone(), - ), + type_: Type::Fun { + args: args.iter().map(|(_, ty)| ty.clone()).collect(), + ret: Box::new(body.type_().clone()), + }, args, body: Box::new(body), }) @@ -319,9 +319,11 @@ impl<'ast> Typechecker<'ast> { }; } + self.env.push(); let body = self.tc_expr(expr)?; let type_ = body.type_().clone(); self.env.set(name.clone(), type_); + self.env.pop(); match body { hir::Expr::Fun { args, body, type_ } => Ok(Some(hir::Decl::Fun { name, @@ -365,27 +367,6 @@ impl<'ast> Typechecker<'ast> { Type::Univ(self.fresh_tv()) } - #[allow(clippy::redundant_closure)] // https://github.com/rust-lang/rust-clippy/issues/6903 - fn universalize(&mut self, args: Vec<Type>, ret: Type) -> Type { - let mut vars = HashMap::new(); - let mut universalize_type = move |ty| match ty { - Type::Exist(tv) if self.resolve_tv(tv).is_none() => vars - .entry(tv) - .or_insert_with(|| { - let ty = self.fresh_univ(); - self.ctx.insert(tv, ty.clone()); - ty - }) - .clone(), - _ => ty, - }; - - Type::Fun { - args: args.into_iter().map(|t| universalize_type(t)).collect(), - ret: Box::new(universalize_type(ret)), - } - } - fn unify(&mut self, ty1: &Type, ty2: &Type) -> Result<Type> { match (ty1, ty2) { (Type::Exist(tv), ty) | (ty, Type::Exist(tv)) => match self.resolve_tv(*tv) { @@ -462,10 +443,15 @@ impl<'ast> Typechecker<'ast> { } fn finalize_decl( - &self, + &mut self, decl: hir::Decl<'ast, Type>, ) -> Result<hir::Decl<'ast, ast::Type<'ast>>> { - decl.traverse_type(|ty| self.finalize_type(ty)) + let res = decl.traverse_type(|ty| self.finalize_type(ty))?; + if let Some(type_) = res.type_() { + let ty = self.type_from_ast_type(type_.clone()); + self.env.set(res.name().clone(), ty); + } + Ok(res) } fn finalize_type(&self, ty: Type) -> Result<ast::Type<'static>> { @@ -541,7 +527,12 @@ impl<'ast> Typechecker<'ast> { .get_by_right(&tv) .map(Ident::to_owned) .unwrap_or_else(|| { - let name = vars.1.make_name(); + let name = loop { + let name = vars.1.make_name(); + if !vars.0.contains_left(&name) { + break name; + } + }; vars.0.insert_no_overwrite(name.clone(), tv).unwrap(); name }) @@ -619,6 +610,26 @@ mod tests { $type ); }; + + (toplevel($program: expr), $($decl: ident => $type: expr),+ $(,)?) => {{ + use crate::parser::{toplevel, type_}; + let program = test_parse!(toplevel, $program); + let res = typecheck_toplevel(program).unwrap_or_else(|e| panic!("{}", e)); + $( + let parsed_type = test_parse!(type_, $type); + let ident = Ident::try_from(::std::stringify!($decl)).unwrap(); + let decl = res.iter().find(|decl| { + matches!(decl, crate::ast::hir::Decl::Fun { name, .. } if name == &ident) + }).unwrap_or_else(|| panic!("Could not find declaration for {}", ident)); + assert!( + decl.type_().unwrap().alpha_equiv(&parsed_type), + "inferred type {} for {}, but expected {}", + decl.type_().unwrap(), + ident, + $type + ); + )+ + }}; } macro_rules! assert_type_error { @@ -656,8 +667,27 @@ mod tests { } #[test] - fn generic_function() { - assert_type!("fn x = x", "fn x -> x"); + fn call_let_bound_generic() { + assert_type!("let id = fn x = x in id 1", "int"); + } + + #[test] + fn universal_ascripted_let() { + assert_type!("let id: fn a -> a = fn x = x in id 1", "int"); + } + + #[test] + fn call_generic_function_toplevel() { + assert_type!( + toplevel( + "ty id : fn a -> a + fn id x = x + + fn main = id 0" + ), + main => "fn -> int", + id => "fn a -> a", + ); } #[test] |