Skip to content

Commit

Permalink
fix(check): Don't generalize variables from an outer scope ...
Browse files Browse the repository at this point in the history
... when merging with a type signature

This commit tracks all type variables introduced in type signatures and uses this information to emit an error when a variable from a signature is matched to a variable from an outer scope.

Fixes gluon-lang#77
  • Loading branch information
Marwes committed Aug 5, 2016
1 parent 51b85f4 commit 6f15ab2
Show file tree
Hide file tree
Showing 5 changed files with 203 additions and 38 deletions.
91 changes: 58 additions & 33 deletions check/src/typecheck.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ use base::ast::{self, Typed, DisplayEnv, MutVisitor};
use base::types::{self, RcKind, Type, Generic, Kind};
use base::error::Errors;
use base::symbol::{Symbol, SymbolRef, SymbolModule, Symbols};
use base::types::{KindEnv, TypeEnv, PrimitiveEnv, TcIdent, Alias, AliasData, TcType};
use base::types::{KindEnv, TypeEnv, PrimitiveEnv, TcIdent, Alias, AliasData, TcType, TypeVariable};
use base::instantiate::{self, Instantiator};
use kindcheck::{self, KindCheck};
use substitution::Substitution;
Expand Down Expand Up @@ -209,7 +209,7 @@ pub struct Typecheck<'a> {
inst: Instantiator,
errors: Errors<ast::Spanned<TypeError<Symbol>>>,
/// Type variables `let test: a -> b` (`a` and `b`)
type_variables: ScopedMap<Symbol, u32>,
type_variables: ScopedMap<Symbol, TcType>,
}

/// Error returned when unsuccessfully typechecking an expression
Expand Down Expand Up @@ -846,16 +846,17 @@ impl<'a> Typecheck<'a> {
self.type_variables.enter_scope();
let level = self.subs.var_id();
let is_recursive = bindings.iter().all(|bind| !bind.arguments.is_empty());
// When the decfinitions are allowed to be mutually recursive
// When the definitions are allowed to be mutually recursive
if is_recursive {
for bind in bindings.iter_mut() {
let mut typ = self.subs.new_var();
if let Some(ref mut type_decl) = bind.typ {
*type_decl = self.refresh_symbols_in_type(type_decl.clone());
try!(self.kindcheck(type_decl));
let decl = self.instantiate(type_decl);
typ = self.unify_span(bind.name.span(), &decl, typ);
}
let typ = match bind.typ {
Some(ref mut type_decl) => {
*type_decl = self.refresh_symbols_in_type(type_decl.clone());
try!(self.kindcheck(type_decl));
self.instantiate_signature(type_decl)
}
None => self.subs.new_var(),
};
self.typecheck_pattern(&mut bind.name, typ);
if let ast::Expr::Lambda(ref mut lambda) = bind.expression.value {
if let ast::Pattern::Identifier(ref name) = bind.name.value {
Expand All @@ -872,17 +873,14 @@ impl<'a> Typecheck<'a> {
// recursive
let mut typ = if bind.arguments.is_empty() {
if let Some(ref mut type_decl) = bind.typ {
self.insert_type_variables(level, type_decl);
self.instantiate_signature(type_decl);
*type_decl = self.refresh_symbols_in_type(type_decl.clone());
try!(self.kindcheck(type_decl));
}
self.typecheck(&mut bind.expression)
} else {
let function_type = match bind.typ {
Some(ref type_decl) => {
self.insert_type_variables(level, type_decl);
self.instantiate(type_decl)
}
Some(ref type_decl) => self.instantiate(type_decl),
None => self.subs.new_var(),
};
self.typecheck_lambda(function_type, &mut bind.arguments, &mut bind.expression)
Expand All @@ -891,7 +889,7 @@ impl<'a> Typecheck<'a> {
bind.name,
types::display_type(&self.symbols, &typ));
if let Some(ref type_decl) = bind.typ {
typ = self.unify_span(bind.name.span(), type_decl, typ);
typ = self.merge_signature(bind.name.span(), level, type_decl, typ);
}
if !is_recursive {
// Merge the type declaration and the actual type
Expand Down Expand Up @@ -1069,7 +1067,11 @@ impl<'a> Typecheck<'a> {
s.push(c as char);
let symbol = self.symbols.symbol(&s[..]);
if self.type_variables.get(&symbol).is_none() {
self.type_variables.insert(symbol, level);
self.type_variables.insert(symbol,
Type::variable(TypeVariable {
id: level,
kind: Kind::typ(),
}));
return;
}
s.pop();
Expand Down Expand Up @@ -1152,14 +1154,16 @@ impl<'a> Typecheck<'a> {
visitor.visit(typ)
}

fn insert_type_variables(&mut self, level: u32, typ: &TcType) {
types::walk_type(typ, |typ| {
if let Type::Generic(ref generic) = **typ {
if self.type_variables.get(&generic.id).is_none() {
self.type_variables.insert(generic.id.clone(), level);
}
fn instantiate_signature(&mut self, typ: &TcType) -> TcType {
let typ = self.instantiate(typ);
// Put all new generic variable names into scope
let named_variables = self.inst.named_variables.borrow();
for (generic, variable) in &*named_variables {
if self.type_variables.get(generic).is_none() {
self.type_variables.insert(generic.clone(), variable.clone());
}
});
}
typ
}

fn refresh_symbols_in_type(&mut self, typ: TcType) -> TcType {
Expand Down Expand Up @@ -1221,6 +1225,35 @@ impl<'a> Typecheck<'a> {
types::walk_move_type(typ, &mut f)
}

fn merge_signature(&mut self,
span: ast::Span,
level: u32,
expected: &TcType,
mut actual: TcType)
-> TcType {
let state = unify_type::State::new(&self.environment);
match unify_type::merge_signature(&self.subs,
&mut self.type_variables,
level,
state,
expected,
&actual) {
Ok(typ) => self.subs.set_type(typ),
Err(errors) => {
let mut expected = expected.clone();
expected = self.subs.set_type(expected);
actual = self.subs.set_type(actual);
let err =
TypeError::Unification(expected, actual, apply_subs(&self.subs, errors.errors));
self.errors.error(ast::Spanned {
span: span,
value: err,
});
self.subs.new_var()
}
}
}

fn unify_span(&mut self, span: ast::Span, expected: &TcType, actual: TcType) -> TcType {
match self.unify(expected, actual) {
Ok(typ) => typ,
Expand Down Expand Up @@ -1306,15 +1339,7 @@ fn apply_subs(subs: &Substitution<TcType>,
TypeMismatch(subs.set_type(expected), subs.set_type(actual))
}
Occurs(var, typ) => Occurs(var, subs.set_type(typ)),
Other(unify_type::TypeError::UndefinedType(id)) => {
Other(unify_type::TypeError::UndefinedType(id))
}
Other(unify_type::TypeError::FieldMismatch(expected, actual)) => {
UnifyError::Other(unify_type::TypeError::FieldMismatch(expected, actual))
}
Other(unify_type::TypeError::SelfRecursive(t)) => {
UnifyError::Other(unify_type::TypeError::SelfRecursive(t))
}
Other(err) => Other(err),
}
})
.collect()
Expand Down
114 changes: 113 additions & 1 deletion check/src/unify_type.rs
Original file line number Diff line number Diff line change
@@ -1,13 +1,15 @@
use std::fmt;

use base::ast::AstType;
use base::error::Errors;
use base::types::{self, TcType, Type, TypeVariable, TypeEnv, merge};
use base::symbol::{Symbol, SymbolRef};
use base::instantiate;
use base::scoped_map::ScopedMap;

use unify;
use unify::{Error as UnifyError, Unifier, Unifiable};
use substitution::{Variable, Substitutable};
use substitution::{Variable, Substitutable, Substitution};

pub type Error<I> = UnifyError<AstType<I>, TypeError<I>>;

Expand All @@ -32,6 +34,7 @@ pub enum TypeError<I> {
UndefinedType(I),
FieldMismatch(I, I),
SelfRecursive(I),
UnableToGeneralize(I),
}

impl From<instantiate::Error> for Error<Symbol> {
Expand Down Expand Up @@ -60,6 +63,12 @@ impl<I> fmt::Display for TypeError<I>
"The use of self recursion in type `{}` could not be unified.",
id)
}
TypeError::UnableToGeneralize(ref id) => {
write!(f,
"Could not generalize the variable bound to `{}` as the variable was used \
outside its scope",
id)
}
}
}
}
Expand Down Expand Up @@ -375,6 +384,109 @@ fn walk_move_types2<'a, I, F, T>(mut types: I, replaced: bool, output: &mut Vec<
}
}

pub fn merge_signature(subs: &Substitution<TcType>,
variables: &mut ScopedMap<Symbol, TcType>,
level: u32,
state: State,
l: &TcType,
r: &TcType)
-> Result<TcType, Errors<Error<Symbol>>> {
let mut unifier = UnifierState {
state: state,
unifier: Merge {
subs: subs,
variables: variables,
errors: Errors::new(),
level: level,
},
};

let typ = unifier.try_match(l, r);
if unifier.unifier.errors.has_errors() {
Err(unifier.unifier.errors)
} else {
Ok(typ.unwrap_or_else(|| l.clone()))
}
}

struct Merge<'e> {
subs: &'e Substitution<TcType>,
variables: &'e ScopedMap<Symbol, TcType>,
errors: Errors<Error<Symbol>>,
level: u32,
}

impl<'a, 'e> Unifier<State<'a>, TcType> for Merge<'e> {
fn report_error(unifier: &mut UnifierState<Self>,
error: UnifyError<TcType, TypeError<Symbol>>) {
unifier.unifier.errors.error(error);
}

fn try_match(unifier: &mut UnifierState<Self>, l: &TcType, r: &TcType) -> Option<TcType> {
let subs = unifier.unifier.subs;
// Retrieve the 'real' types by resolving
let l = subs.real(l);
let r = subs.real(r);
// `l` and `r` must have the same type, if one is a variable that variable is
// unified with whatever the other type is
let result = match (&**l, &**r) {
(&Type::Variable(ref l), &Type::Variable(ref r)) if l.id == r.id => Ok(None),
(&Type::Generic(ref l_gen), &Type::Variable(ref r_var)) => {
let left = match unifier.unifier.variables.get(&l_gen.id) {
Some(generic_bound_var) => {
match **generic_bound_var {
// The generic variable is defined outside the current scope. Use the
// type variable instantiated from the generic and unify with that
Type::Variable(ref var) if var.id < unifier.unifier.level => {
generic_bound_var
}
// `r_var` is outside the scope of the generic variable.
Type::Variable(ref var) if var.id > r_var.id => {
let error = UnifyError::Other(TypeError::UnableToGeneralize(l_gen.id
.clone()));
unifier.unifier.errors.error(error);
return None;
}
_ => l,
}
}
None => l,
};
match subs.union(r_var, left) {
Ok(()) => Ok(None),
Err(()) => Err(UnifyError::Occurs(r_var.clone(), left.clone())),
}

}
(_, &Type::Variable(ref r)) => {
match subs.union(r, l) {
Ok(()) => Ok(None),
Err(()) => Err(UnifyError::Occurs(r.clone(), l.clone())),
}
}
(&Type::Variable(ref l), _) => {
match subs.union(l, r) {
Ok(()) => Ok(Some(r.clone())),
Err(()) => Err(UnifyError::Occurs(l.clone(), r.clone())),
}
}
_ => {
// Both sides are concrete types, the only way they can be equal is if
// the matcher finds their top level to be equal (and their sub-terms
// unify)
l.zip_match(r, unifier)
}
};
match result {
Ok(typ) => typ,
Err(error) => {
unifier.unifier.errors.error(error);
Some(subs.new_var())
}
}
}
}

#[cfg(test)]
mod tests {
use super::*;
Expand Down
14 changes: 14 additions & 0 deletions check/tests/fail.rs
Original file line number Diff line number Diff line change
Expand Up @@ -294,3 +294,17 @@ let g x: A a -> () = x

assert_unify_err!(result, Other(SelfRecursive(..)));
}

#[test]
fn declared_generic_variables_may_not_make_outer_bindings_more_general() {
let _ = ::env_logger::init();
let text = r#"
let make m =
let m2: m = m
m
make
"#;
let result = support::typecheck(text);
assert!(result.is_err());
}
20 changes: 17 additions & 3 deletions check/tests/pass.rs
Original file line number Diff line number Diff line change
Expand Up @@ -698,13 +698,12 @@ in \(<) ->
| Cons y ys -> if x < y
then Cons x xs
else Cons y (insert x ys)
let ret : { empty: SortedList a, insert: a -> SortedList a -> SortedList a }
= { empty, insert }
let ret = { empty, insert }
ret
";
let result = support::typecheck(text);

assert!(result.is_ok());
assert!(result.is_ok(), "{}", result.unwrap_err());
}

#[test]
Expand Down Expand Up @@ -827,3 +826,18 @@ in r1"#;

assert_eq!(result, expected);
}

#[test]
fn scoped_generic_variable() {
let _ = ::env_logger::init();
let text = r#"
let any x = any x
let make m: m -> { test: m, test2: m } =
let m2: m = any ()
{ test = m, test2 = m2 }
make
"#;
let result = support::typecheck(text);
assert!(result.is_ok(), "{}", result.unwrap_err());
}
2 changes: 1 addition & 1 deletion src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -389,7 +389,7 @@ impl Compiler {
let env = vm.get_env();
let name = Name::new(filename);
let name = NameBuf::from(name.module());
let symbols = SymbolModule::new(StdString::from(name.as_ref()), &mut self.symbols);
let symbols = SymbolModule::new(StdString::from(AsRef::<str>::as_ref(&name)), &mut self.symbols);
let mut compiler = Compiler::new(&*env, vm.global_env(), symbols);
compiler.compile_expr(&expr)
};
Expand Down

0 comments on commit 6f15ab2

Please sign in to comment.