Skip to content

Commit

Permalink
fix(check): Don't instantiate variables during unification inside ali…
Browse files Browse the repository at this point in the history 
…ases

The unification algorithm accidentally were to eager to instantiate
generic variables with fresh type variables which allowed programs to
pass typechecking even though they differed in the placement of
variables (see tests).

This fixes that by *ONLY* instantiating fresh typevariables during
subsumption (deduced from Purescript's implementation), otherwise we
only skolemize the variables (which ensures that different variables do
not unify with each other).

This would be enough to fix this, except the current way typechecking
proceeds throw a wrench into the mix. Consider the following example.

```f#
type Functor f = {
    map : forall a b . (a -> b) -> f a -> f b,
}

let functor : Functor List =
    let map = ...
    { map }
```

Since we want to preserve the alias during typechecking as long as
possible (both as an optimization as well as to present better error
messages), we do not immediately skolemize the inner `forall` binding.
Instead we only do this once unification forces us to look inside
`Functor List`. This is a problem if we end up skolemizing the same type
*twice* as the skolem constants from each time will not match.

```
{ map : (a@0 -> b@1) -> List a@0 -> List b@1 } <=>
{ map : (a@2 -> b@3) -> List a@2 -> List b@3 }

a@0 != a@2
```

I remedied this by moving the `merge_signature/subsumption` call that
was done on each `let` binding into the typechecking procedure itself
which has the effect of making this subsumption only happen once for
each part of the type.
  • Loading branch information
@Marwes
Marwes committed Dec 30, 2017
1 parent 0909139 commit 1326ca5
Show file tree
Hide file tree
Showing 6 changed files with 220 additions and 106 deletions.
10 changes: 6 additions & 4 deletions check/src/substitution.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -341,6 +341,11 @@ impl<T: Substitutable> Substitution<T> {
union.get_mut(other as usize).level = level;
}

pub fn set_level(&self, var: u32, level: u32) {
let mut union = self.union.borrow_mut();
union.get_mut(var as usize).level = level;
}

pub fn get_level(&self, mut var: u32) -> u32 {
if let Some(v) = self.find_type_for_var(var) {
var = v.get_var().map_or(var, |v| v.get_id());
Expand Down Expand Up @@ -552,10 +557,7 @@ impl<T: Substitutable + PartialEq + Clone> Substitution<T> {
typ.get_var().map(|x| x.get_id()),
resolved.get_var().map(|x| x.get_id()),
) {
(Some(x), Some(y)) if x > y => {
typ = Cow::Owned(resolved);
}
(_, None) => {
(Some(_), Some(_)) | (_, None) => {
typ = Cow::Owned(resolved);
}
_ => (),
Expand Down
114 changes: 75 additions & 39 deletions check/src/typecheck.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -348,8 +348,7 @@ impl<'a> Typecheck<'a> {
Ok(typ)
}
None => {
// Don't report global variables inserted by the `import!` macro as non-existing
// existing
// Don't report global variables inserted by the `import!` macro as undefined
// (if they don't exist the error will already have been reported by the macro)
if id.is_global() {
Ok(self.subs.new_var())
Expand Down Expand Up @@ -638,7 +637,8 @@ impl<'a> Typecheck<'a> {
let returned_type;
loop {
let expected_type = expected_type.map(|t| self.skolemize(t));
match self.typecheck_(expr, expected_type.as_ref()) {
let mut expected_type = expected_type.as_ref();
match self.typecheck_(expr, &mut expected_type) {
Ok(tailcall) => {
match tailcall {
TailCall::TailCall => {
Expand All @@ -655,7 +655,13 @@ impl<'a> Typecheck<'a> {
scope_count += 1;
}
TailCall::Type(typ) => {
returned_type = typ;
returned_type = match expected_type {
Some(expected_type) => {
let level = self.subs.var_id();
self.merge_signature(expr.span, level, &expected_type, typ)
}
None => typ,
};
break;
}
}
Expand All @@ -676,10 +682,12 @@ impl<'a> Typecheck<'a> {
returned_type
}

/// `expected_type` should be set to `None` if subsumption is done with it (to prevent us from
/// doing it twice)
fn typecheck_(
&mut self,
expr: &mut SpannedExpr<Symbol>,
expected_type: Option<&ArcType<Symbol>>,
expected_type: &mut Option<&ArcType<Symbol>>,
) -> Result<TailCall, TypeError<Symbol>> {
match expr.value {
Expr::Ident(ref mut id) => {
Expand All @@ -706,8 +714,8 @@ impl<'a> Typecheck<'a> {
self.unify_span(expr_check_span(pred), &bool_type, pred_type);

// Both branches must unify to the same type
let true_type = self.typecheck_opt(&mut **if_true, expected_type);
let false_type = self.typecheck_opt(&mut **if_false, expected_type);
let true_type = self.typecheck_opt(&mut **if_true, expected_type.clone());
let false_type = self.typecheck_opt(&mut **if_false, expected_type.take());

let true_type = self.instantiate_generics(&true_type);
let false_type = self.instantiate_generics(&false_type);
Expand Down Expand Up @@ -753,7 +761,7 @@ impl<'a> Typecheck<'a> {
} => {
*typ = match exprs.len() {
0 => Type::unit(),
1 => self.typecheck_opt(&mut exprs[0], expected_type),
1 => self.typecheck_opt(&mut exprs[0], expected_type.take()),
_ => {
let fields = exprs
.iter_mut()
Expand All @@ -775,6 +783,8 @@ impl<'a> Typecheck<'a> {
let typ = self.infer_expr(&mut **expr);
let mut expected_alt_type = expected_type.cloned();

let expected_type = expected_type.take();

for alt in alts.iter_mut() {
self.enter_scope();
self.typecheck_pattern(&mut alt.pattern, typ.clone());
Expand Down Expand Up @@ -855,10 +865,13 @@ impl<'a> Typecheck<'a> {
Expr::Lambda(ref mut lambda) => {
let loc = format!("{}.lambda:{}", self.symbols.module(), expr.span.start);
lambda.id.name = self.symbols.symbol(loc);
let level = self.subs.var_id();
let function_type = expected_type
.cloned()
.unwrap_or_else(|| self.subs.new_var());
let typ = self.typecheck_lambda(function_type, &mut lambda.args, &mut lambda.body);
let mut typ =
self.typecheck_lambda(function_type, &mut lambda.args, &mut lambda.body);
self.generalize_type(level, &mut typ);
lambda.id.typ = typ.clone();
Ok(TailCall::Type(typ))
}
Expand Down Expand Up @@ -896,23 +909,34 @@ impl<'a> Typecheck<'a> {
for field in fields {
let level = self.subs.var_id();

let name = &field.name.value;
let expected_field_type = expected_type
.and_then(|expected_type| {
expected_type
.row_iter()
.find(|expected_field| expected_field.name.name_eq(&name))
})
.map(|field| &field.typ);

let typ = match field.value {
Some(ref mut expr) => {
let name = &field.name.value;
let expected_type = expected_type
.and_then(|expected_type| {
expected_type
.row_iter()
.find(|expected_field| expected_field.name.name_eq(&name))
})
.map(|field| &field.typ);

let mut typ = self.typecheck_opt(expr, expected_type);
let mut typ = self.typecheck_opt(expr, expected_field_type);

self.generalize_type(level, &mut typ);
new_skolem_scope(&self.subs, &FnvMap::default(), &typ)
}
None => self.find(&field.name.value)?,
None => {
let typ = self.find(&field.name.value)?;
match expected_field_type {
Some(expected_field_type) => self.merge_signature(
field.name.span,
level,
&expected_field_type,
typ,
),
None => typ,
}
}
};
if self.error_on_duplicated_field(&mut duplicated_fields, field.name.clone()) {
new_fields.push(Field::new(field.name.value.clone(), typ));
Expand Down Expand Up @@ -970,7 +994,10 @@ impl<'a> Typecheck<'a> {
for expr in exprs {
self.infer_expr(expr);
}
Ok(TailCall::Type(self.typecheck_opt(last, expected_type)))
Ok(TailCall::Type(self.typecheck_opt(
last,
expected_type.take(),
)))
}
Expr::Do(Do {
ref mut id,
Expand Down Expand Up @@ -1037,6 +1064,7 @@ impl<'a> Typecheck<'a> {
where
I: IntoIterator<Item = &'e mut SpannedExpr<Symbol>>,
{
func_type = self.new_skolem_scope(&func_type);
for arg in args {
let f = self.type_cache
.function(once(self.subs.new_var()), self.subs.new_var());
Expand Down Expand Up @@ -1378,24 +1406,16 @@ impl<'a> Typecheck<'a> {
bind.resolved_type = typ;
}

bind.resolved_type = self.new_skolem_scope_signature(&bind.resolved_type);
self.typecheck(&mut bind.expr, &bind.resolved_type)
let typ = self.new_skolem_scope_signature(&bind.resolved_type);
self.typecheck(&mut bind.expr, &typ)
} else {
bind.resolved_type = self.new_skolem_scope_signature(&bind.resolved_type);
let function_type = self.instantiate_generics(&bind.resolved_type);
let typ = self.new_skolem_scope_signature(&bind.resolved_type);
let function_type = self.skolemize(&typ);
self.typecheck_lambda(function_type, &mut bind.args, &mut bind.expr)
};

debug!("let {:?} : {}", bind.name, typ);

let bind_span = Span::new(
bind.name.span.start,
bind.args
.last()
.map_or(bind.name.span.end, |last_arg| last_arg.span.end),
);
typ = self.merge_signature(bind_span, level, &bind.resolved_type, typ);

if !is_recursive {
// Merge the type declaration and the actual type
debug!("Generalize at {} = {}", level, bind.resolved_type);
Expand Down Expand Up @@ -1616,9 +1636,11 @@ impl<'a> Typecheck<'a> {
let typ = self.instantiate_generics(&typ);
let record_type = self.remove_alias(typ.clone());
with_pattern_types(fields, &record_type, |field_name, binding, field_type| {
let mut field_type = field_type.clone();
self.generalize_type(level, &mut field_type);
match *binding {
Some(ref mut pat) => {
self.finish_pattern(level, pat, field_type);
self.finish_pattern(level, pat, &field_type);
}
None => {
self.environment
Expand All @@ -1628,7 +1650,7 @@ impl<'a> Typecheck<'a> {
.typ = field_type.clone();
debug!("{}: {}", field_name, field_type);

self.intersect_type(level, field_name, field_type);
self.intersect_type(level, field_name, &field_type);
}
}
});
Expand All @@ -1642,7 +1664,9 @@ impl<'a> Typecheck<'a> {
let typ = self.top_skolem_scope(typ);
let typ = self.instantiate_generics(&typ);
for (elem, field) in elems.iter_mut().zip(typ.row_iter()) {
self.finish_pattern(level, elem, &field.typ);
let mut field_type = field.typ.clone();
self.generalize_type(level, &mut field_type);
self.finish_pattern(level, elem, &field_type);
}
}
Pattern::Constructor(ref id, ref mut args) => {
Expand Down Expand Up @@ -1670,8 +1694,8 @@ impl<'a> Typecheck<'a> {
// Only allow overloading for bindings whose types which do not contain type variables
// It might be possible to lift this restriction but currently it causes problems
// which I am not sure how to solve
debug!("Looking for intersection `{}`", symbol_type);
if existing_types.len() >= 2 {
debug!("Looking for intersection `{}`", symbol_type);
let existing_binding = &existing_types[existing_types.len() - 2];
debug!(
"Intersect `{}`\n{} ∩ {}",
Expand Down Expand Up @@ -1709,7 +1733,7 @@ impl<'a> Typecheck<'a> {
{
let constraints: FnvMap<_, _> = intersection_constraints
.into_iter()
.map(|((l, mut r), name)| {
.map(|((mut l, mut r), name)| {
let constraints = match *l {
Type::Generic(ref gen) => existing_binding.constraints.get(&gen.id),
Type::Skolem(ref skolem) => existing_binding.constraints.get(&skolem.name),
Expand All @@ -1728,6 +1752,7 @@ impl<'a> Typecheck<'a> {
_ => None,
};

self.generalize_type(level, &mut l);
self.generalize_type(level, &mut r);

(
Expand Down Expand Up @@ -1925,6 +1950,11 @@ impl<'a> Typecheck<'a> {
id: skolem.name.clone(),
kind: skolem.kind.clone(),
};

if self.type_variables.get(&generic.id).is_none() {
unbound_variables.insert(generic.id.clone(), generic.clone());
}

Some(Type::generic(generic))
}

Expand Down Expand Up @@ -2328,7 +2358,13 @@ impl<'a, 'b> Iterator for FunctionArgIter<'a, 'b> {
Some(typ) => (None, typ.clone()),
None => return None,
},
None => (Some(self.tc.subs.new_var()), self.tc.subs.new_var()),
None => {
let arg = self.tc.subs.new_var();
let ret = self.tc.subs.new_var();
let f = self.tc.type_cache.function(Some(arg.clone()), ret.clone());
self.tc.unify(&self.typ, f).unwrap();
(Some(arg), ret)
}
},
};
self.typ = new;
Expand Down
Loading

0 comments on commit 1326ca5

Please sign in to comment.