Skip to content

Commit

Permalink
fix(check): Avoid instantiating higher ranked types in function argum…
Browse files Browse the repository at this point in the history
…ents
  • Loading branch information
Marwes committed Nov 26, 2018
1 parent 796f006 commit f4fc545
Show file tree
Hide file tree
Showing 3 changed files with 184 additions and 35 deletions.
118 changes: 83 additions & 35 deletions check/src/typecheck.rs
Original file line number Diff line number Diff line change
Expand Up @@ -741,7 +741,7 @@ impl<'a> Typecheck<'a> {
fn typecheck_opt(
&mut self,
mut expr: &mut SpannedExpr<Symbol>,
expected_type: Option<&ArcType>,
mut expected_type: Option<&ArcType>,
) -> ArcType {
fn moving<T>(t: T) -> T {
t
Expand All @@ -750,8 +750,6 @@ impl<'a> Typecheck<'a> {
let mut scope_count = 0;
let returned_type;
loop {
let expected_type = expected_type.map(|t| self.skolemize(t));
let mut expected_type = expected_type.as_ref();
match self.typecheck_(expr, &mut expected_type) {
Ok(tailcall) => {
match tailcall {
Expand Down Expand Up @@ -1021,13 +1019,41 @@ impl<'a> Typecheck<'a> {
} => {
let level = self.subs.var_id();

let expected_type = expected_type.map(|expected_type| {
let expected_record_type = expected_type.and_then(|expected_type| {
let expected_type = self.subs.real(expected_type).clone();
let typ = resolve::remove_aliases_cow(&self.environment, &expected_type);
self.new_skolem_scope(&typ)
let typ = self.new_skolem_scope(&typ);
match *typ {
Type::Record(_) => Some(typ),
_ => None,
}
});

let expected_type = expected_type.as_ref();
let expected_type = match &expected_record_type {
Some(expected_record_type) => {
let mut expected_fields: FnvSet<_> = expected_record_type
.row_iter()
.map(|f| &f.name)
.chain(expected_record_type.type_field_iter().map(|f| &f.name))
.collect();

let expected_fields_matches = fields
.iter()
.map(|f| &f.name.value)
.chain(types.iter().map(|f| &f.name.value))
.all(|name| expected_fields.remove(&name))
&& expected_fields.is_empty();

if expected_fields_matches {
// No need to do subsumption checking against the expected type as all the
// fields will be matched against anyway
expected_type.take();
}

Some(expected_record_type)
}
None => None,
};

let mut base_record_types = FnvMap::default();
let mut base_record_fields = FnvMap::default();
Expand Down Expand Up @@ -1321,24 +1347,9 @@ impl<'a> Typecheck<'a> {

let mut prev_arg_end = implicit_args.last().map_or(span, |arg| arg.span).end();
for arg in args.map(|arg| arg.borrow_mut()) {
let arg_ty = self.subs.new_var();
let ret_ty = self.subs.new_var();
let f = self
.type_cache
.function(once(arg_ty.clone()), ret_ty.clone());

let level = self.subs.var_id();
let errors_before = self.errors.len();
self.subsumes_implicit(
span,
level,
ErrorOrder::ExpectedActual,
&f,
func_type.clone(),
&mut |implicit_arg| {
implicit_args.push(pos::spanned2(prev_arg_end, arg.span.start(), implicit_arg));
},
);
let (arg_ty, ret_ty) =
self.subsume_function(prev_arg_end, arg.span, func_type.clone(), implicit_args);

if errors_before != self.errors.len() {
self.errors.pop();
Expand Down Expand Up @@ -1385,15 +1396,14 @@ impl<'a> Typecheck<'a> {
Ok(TailCall::Type(func_type))
}

fn typecheck_lambda<'i>(
fn typecheck_lambda(
&mut self,
mut function_type: ArcType,
function_type: ArcType,
before_args_pos: BytePos,
args: &mut Vec<Argument<SpannedIdent<Symbol>>>,
body: &mut SpannedExpr<Symbol>,
) -> ArcType {
self.enter_scope();
function_type = self.skolemize(&function_type);
let mut arg_types = Vec::new();

let body_type = {
Expand All @@ -1403,15 +1413,7 @@ impl<'a> Typecheck<'a> {
let mut next_type_arg = iter1.next();

let make_new_arg = |tc: &mut Self, span: Span<BytePos>, typ: &mut ArcType| {
let arg = tc.subs.new_var();
let ret = tc.subs.new_var();
let f = tc.type_cache.function(Some(arg.clone()), ret.clone());
if let Err(err) = tc.unify(typ, f) {
tc.errors.push(Spanned {
span,
value: err.into(),
});
}
let (arg, ret) = tc.unify_function(span, typ.clone());
*typ = ret;
arg
};
Expand Down Expand Up @@ -2448,6 +2450,52 @@ impl<'a> Typecheck<'a> {
}
}

fn subsume_function(
&mut self,
prev_arg_end: BytePos,
span: Span<BytePos>,
actual: ArcType,
implicit_args: &mut Vec<SpannedExpr<Symbol>>,
) -> (ArcType, ArcType) {
let actual = self.remove_aliases(actual);
match actual.as_function_with_type() {
Some((ArgType::Explicit, arg, ret)) => return (arg.clone(), ret.clone()),
_ => (),
}

let arg_ty = self.subs.new_var();
let ret_ty = self.subs.new_var();
let f = self
.type_cache
.function(once(arg_ty.clone()), ret_ty.clone());

let level = self.subs.var_id();
self.subsumes_implicit(
span,
level,
ErrorOrder::ExpectedActual,
&f,
actual,
&mut |implicit_arg| {
implicit_args.push(pos::spanned2(prev_arg_end, span.start(), implicit_arg));
},
);
(arg_ty, ret_ty)
}

fn unify_function(&mut self, span: Span<BytePos>, actual: ArcType) -> (ArcType, ArcType) {
let actual = self.remove_aliases(actual);
match actual.as_function() {
Some((arg, ret)) => return (arg.clone(), ret.clone()),
None => (),
}
let arg = self.subs.new_var();
let ret = self.subs.new_var();
let f = self.type_cache.function(Some(arg.clone()), ret.clone());
self.unify_span(span, &f, actual);
(arg, ret)
}

fn unify_span(&mut self, span: Span<BytePos>, expected: &ArcType, actual: ArcType) -> ArcType {
match self.unify(expected, actual) {
Ok(typ) => typ,
Expand Down
17 changes: 17 additions & 0 deletions std/free.glu
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
let { List } = import! std.list

type Val = | Val

rec
type Free f a = | Free (FreeView f Val Val) (List (ExpF f))
type FreeView f a b = | Return a | Bind (f b) (b -> Free f a)
type ExpF f = Val -> Free f Val


let functor : Functor (Free f) = {
map = \f xs ->
match xs with
| Free
}

{ Free }
84 changes: 84 additions & 0 deletions test.glu
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
let option = import! std.option
let io @ { ? } = import! std.io

let { map } = import! std.functor
let { wrap } = import! std.applicative

let any x = any x

type VE w r = | Value w | Effect (r (VE w r))

type Eff r a = { run_effect : forall w . (a -> VE w r) -> VE w r }

let functor_eff : Functor (Eff r) = {
map = error ""
}

let applicative_eff : Applicative (Eff r) = {
functor = functor_eff,
apply = error "",
wrap = \x -> { run_effect = \k -> k x },
}

let monad_eff : Monad (Eff r) = {
applicative = applicative_eff,
flat_map = \f m -> { run_effect = \k -> m.run_effect (\v -> (f v).run_effect k) }
}


type Opt a r = [ option : Option | a ] r

let send f : forall a . (forall w . (a -> VE w r) -> r (VE w r)) -> Eff r a = { run_effect = \k -> Effect (f k) }
// let send2 t : r a -> Eff r a = { run_effect = \k -> Effect (r t) }
let admin eff : Eff r a -> VE a r = eff.run_effect Value

let inject : f a -> [f : f | r] (VE a [f : f | r]) = any ()
let option_eff : Option a -> [option : Option | r] (VE a [option : Option | r]) = any ()
let io_eff : IO a -> [io : IO | r] (VE a [io : IO | r]) = any ()
// let row : { option : Monad Option, io : Monad IO } = { option = option.monad, io = io.monad }
// let applicative_eff : Applicative (Eff _) = applicative_eff row
// let monad = monad_eff row

type Found f a r = | Found (f a) | NotFound ([| r] a)
let proj : forall f . [f : f | r] a -> (Found f a r) = any ()

let option_empty : Eff [option : Option | r] Int = send (\x -> option_eff None)

type Lift m v = forall a . { monad : (m a), cont : (a -> v) }
let lift_io io : IO a -> Eff [f : Lift IO | r] a = send (\x -> inject (let z : Lift IO a = { monad = io, cont = x } in z))

let io_effect : Eff [f : Lift IO | r] Int = lift_io (wrap 123)

// let handle_relay ret h m : (a -> Eff [| r] w) -> (forall v. [|r ] v -> Eff [| r] w) -> Eff [f : f | r] w -> Eff [| r] w =
// let loop x =
// match x with
// | Value v -> ret v
// | Effect e ->
// match proj e with
// | Found x -> { run_effect = \f -> (h x).run_effect (any ()) }
// | NotFound r -> { run_effect = \f -> Effect (f r) }
// loop m

let run_option eff : [Functor [| r]] -> Eff [f : Option | r] a -> Eff [| r] (Option a) =
let loop ve : VE a [f : Option | r] -> Eff [| r] (Option a) =
match ve with
| Value v -> wrap (Some v)
| Effect e ->
match proj e with
| Found x ->
match x with
| None -> wrap None
| Some y -> loop y
| NotFound rest ->
flat_map loop (send (\k -> map k rest))
loop (admin eff)


// let run_io eff : Eff [io : IO | r] a -> IO a =
// match admin eff with
// | IO x -> x
// | _ -> any ()

do x = option_empty
do y = io_effect
wrap (x #Int+ y)

0 comments on commit f4fc545

Please sign in to comment.