fix(gs/achilles): Get rid of universalization step

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>
This commit is contained in:
Griffin Smith 2021-03-20 15:11:06 -04:00 committed by glittershark
parent e2a3aea451
commit e7033bd8b0
2 changed files with 67 additions and 30 deletions

View file

@ -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_),

View file

@ -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]