Skip to content

Commit

Permalink
fix(check): Subsume implicit functions with forall correctly
Browse files Browse the repository at this point in the history
The previous, naive subsume_implicit function did not traverse the
functions simultaneously so the implicit arguments would be lost if the
left side had a `forall` at the top.

Fixes an issue found in #686

cc @Etherian
  • Loading branch information
Marwes committed Feb 13, 2019
1 parent 7552e64 commit 6de5c25
Show file tree
Hide file tree
Showing 3 changed files with 161 additions and 61 deletions.
108 changes: 48 additions & 60 deletions check/src/typecheck.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2400,75 +2400,63 @@ impl<'a> Typecheck<'a> {
span: Span<BytePos>,
error_order: ErrorOrder,
expected: &RcType,
mut actual: RcType,
actual: RcType,
receiver: &mut FnMut(Expr<Symbol>),
) -> RcType {
debug!("Subsume expr {} <=> {}", expected, actual);

self.environment.type_variables.enter_scope();

// Act as the implicit arguments of `actual` has been supplied (unless `expected` is
// specified to have implicit arguments)
loop {
actual = self.instantiate_generics(&actual);
actual = match *actual {
Type::Function(ArgType::Implicit, ref arg_type, ref r_ret) => {
match **self.subs.real(expected) {
Type::Variable(_) | Type::Function(ArgType::Implicit, _, _) => break,
_ => {
let name = self.implicit_resolver.make_implicit_ident(arg_type);

receiver(Expr::Ident(TypedIdent {
name,
typ: self.subs.bind_arc(&arg_type),
}));

r_ret.clone()
}
}
}
_ => break,
};
}
let original_expected = expected;
let mut expected = expected.clone();
let mut resolved_implicit = false;

let mut skolem_scope = FnvMap::default();
loop {
expected = expected.skolemize(&mut &self.subs, &mut skolem_scope);
self.environment.type_variables.extend(skolem_scope.drain());

expected = match *expected {
Type::Function(ArgType::Implicit, ref arg_type, ref r_ret) => {
match **self.subs.real(&actual) {
Type::Variable(_) | Type::Function(ArgType::Implicit, _, _) => break,
_ => {
resolved_implicit = true;

let name = self.implicit_resolver.make_implicit_ident(arg_type);
let state = unify_type::State::new(&self.environment, &self.subs);

receiver(Expr::Ident(TypedIdent {
name,
typ: self.subs.bind_arc(&arg_type),
}));
let implicit_resolver = &mut self.implicit_resolver;
let mut receiver = |implicit_type: &RcType| {
let name = implicit_resolver.make_implicit_ident(implicit_type);

r_ret.clone()
receiver(Expr::Ident(TypedIdent {
name,
typ: implicit_type.clone(),
}));
};
let typ = match unify_type::subsumes_implicit(
&self.subs,
state,
&expected,
&actual,
&mut receiver,
) {
Ok(typ) => typ,
Err((typ, mut errors)) => {
let expected = expected.clone();
debug!(
"Error '{}' between:\n>> {}\n>> {}",
errors, expected, actual
);
let err = match error_order {
ErrorOrder::ExpectedActual => {
TypeError::Unification(expected, actual, errors.into())
}
ErrorOrder::ActualExpected => {
for err in &mut errors {
match err {
unify::Error::TypeMismatch(l, r) => mem::swap(l, r),
unify::Error::Other(unify_type::TypeError::FieldMismatch(l, r)) => {
mem::swap(l, r)
}
_ => (),
}
}
TypeError::Unification(actual, expected, errors.into())
}
}
_ => break,
};
}

// HACK Need to move elaboration/implicit argument insertion into the normal subsumption so
// variables get correctly subsumed with forall
if !resolved_implicit {
expected = original_expected.clone();
}

let new_type = self.subsumes(span, error_order, &expected, actual);
let typ = self.with_forall(original_expected, new_type);
};
self.errors.push(Spanned {
span: span,
// TODO Help what caused this unification failure
value: err.into(),
});
typ
}
};

self.environment.type_variables.exit_scope();

Expand All @@ -2489,7 +2477,7 @@ impl<'a> Typecheck<'a> {
Err((typ, mut errors)) => {
let expected = expected.clone();
debug!(
"Error '{:?}' between:\n>> {}\n>> {}",
"Error '{}' between:\n>> {}\n>> {}",
errors, expected, actual
);
let err = match error_order {
Expand Down
89 changes: 88 additions & 1 deletion check/src/unify_type.rs
Original file line number Diff line number Diff line change
Expand Up @@ -634,7 +634,7 @@ where

match (&lhs_base, &rhs_base) {
(&None, &None) => {
debug!("Unify error: {:?} <=> {:?}", expected, actual);
debug!("Unify error: {} <=> {}", expected, actual);
Err(UnifyError::TypeMismatch(expected.clone(), actual.clone()))
}
(_, _) => {
Expand Down Expand Up @@ -1100,6 +1100,31 @@ pub fn subsumes(
}
}

pub fn subsumes_implicit(
subs: &Substitution<RcType>,
state: State,
l: &RcType,
r: &RcType,
receiver: &mut FnMut(&RcType),
) -> Result<RcType, (RcType, Errors<Error<Symbol>>)> {
debug!("Subsume {} <=> {}", l, r);
let mut unifier = UnifierState {
state: state,
unifier: Subsume {
subs: subs,
errors: Errors::new(),
allow_returned_type_replacement: true,
},
};

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

pub fn subsumes_no_subst(
state: State,
l: &RcType,
Expand Down Expand Up @@ -1130,6 +1155,68 @@ struct Subsume<'e> {
}

impl<'a, 'e> UnifierState<'a, Subsume<'e>> {
fn subsumes_implicit(
&mut self,
l: &RcType,
r: &RcType,
receiver: &mut FnMut(&RcType),
) -> Option<RcType> {
debug!("Subsume implicit {} <=> {}", l, r);

// Act as the implicit arguments of `actual` has been supplied (unless `expected` is
// specified to have implicit arguments)

let l_orig = &l;
let mut map = FnvMap::default();

let r = r.instantiate_generics(&mut self.unifier.subs, &mut FnvMap::default());
let typ = match *r {
Type::Function(ArgType::Implicit, ref arg_type, ref r_ret) => {
let l = l.skolemize(&mut self.unifier.subs, &mut map);

match **self.unifier.subs.real(&l) {
Type::Variable(_) | Type::Function(ArgType::Implicit, _, _) => {
self.subsume_check(&l, &r)
}

_ => {
receiver(&arg_type);

self.subsumes_implicit(&l, r_ret, receiver);
None
}
}
}
_ => self.try_match(&l, &r),
};

// If a skolem variable we just created somehow appears in the original type it has been
// unified with a type variable outside of this skolem scope meaning it has escaped
//
// Unifying:
// forall s . Test s 2 <=> Test 1 1
// ^ skolemize
// ==> 1 <=> s@3
// ==> 1 <=> 2
// ==> s@3 <=> 2
//
// `l_orig` is still `forall s . Test s 2` so we can detect `s@2` escaping in the
// variable `2`
if !map.is_empty() {
self.skolem_escape_check(&map, l_orig);
}

typ.or(if l_orig.forall_params().next().is_some() {
Some(l.clone())
} else {
None
})
.map(|typ| {
self.unifier.allow_returned_type_replacement = false;
self.unifier.subs.with_forall(typ, l_orig)
})
}

fn subsume_check(&mut self, l: &RcType, r: &RcType) -> Option<RcType> {
let l_orig = &l;
let mut map = FnvMap::default();
Expand Down
25 changes: 25 additions & 0 deletions check/tests/implicits.rs
Original file line number Diff line number Diff line change
Expand Up @@ -974,3 +974,28 @@ let show_Test : Show (Test a) =
"#,
"()"
}

test_check! {
field_with_implicit_parameter,
r#"
#[implicit]
type Monad m = { wrap : a -> m a }
type StateT s m a = s -> m { value : a, state : s }
let any x = any x
#[implicit]
type Transformer t = {
wrap_monad : forall a m . [Monad m] -> m a -> t m a
}
let transformer : Transformer (StateT s) =
let wrap_monad : [Monad m] -> m a -> StateT s m a = any ()
{ wrap_monad }
()
"#,
"()"
}

0 comments on commit 6de5c25

Please sign in to comment.