Skip to content

Commit

Permalink
fix: Handle forall before variant constructors
Browse files Browse the repository at this point in the history
  • Loading branch information
Marwes committed Nov 26, 2018
1 parent f4fc545 commit 7e472ab
Show file tree
Hide file tree
Showing 3 changed files with 96 additions and 35 deletions.
64 changes: 49 additions & 15 deletions check/src/typecheck.rs
Original file line number Diff line number Diff line change
Expand Up @@ -478,23 +478,49 @@ impl<'a> Typecheck<'a> {
// Some ""
// ```
let aliased_type = alias.typ();
let canonical_alias = resolve::canonical_alias(&self.environment, &aliased_type, |alias| {
match **alias.unresolved_type().remove_forall() {
Type::Variant(_) => true,
_ => false,
let canonical_alias_type =
resolve::canonical_alias(&self.environment, &aliased_type, |alias| {
match **alias.unresolved_type().remove_forall() {
Type::Variant(_) => true,
_ => false,
}
});

fn unpack_canonical_alias<'a>(
alias: &'a Alias<Symbol, ArcType>,
canonical_alias_type: &'a ArcType,
) -> (
Cow<'a, [Generic<Symbol>]>,
&'a AliasRef<Symbol, ArcType>,
Cow<'a, ArcType>,
) {
match **canonical_alias_type {
Type::App(ref func, _) => match **func {
Type::Alias(ref alias) => (Cow::Borrowed(&[]), alias, alias.typ()),
_ => (Cow::Borrowed(&[]), &**alias, Cow::Borrowed(func)),
},
Type::Alias(ref alias) => (Cow::Borrowed(&[]), alias, alias.typ()),
Type::Forall(ref params, ref typ, None) => {
let mut params = Cow::Borrowed(&params[..]);
let (more_params, canonical_alias, inner_type) =
unpack_canonical_alias(alias, typ);
if !more_params.is_empty() {
params.to_mut().extend(more_params.iter().cloned());
}
(params, canonical_alias, inner_type)
}
_ => (
Cow::Borrowed(&[]),
&**alias,
Cow::Borrowed(canonical_alias_type),
),
}
});
}

let canonical_alias = match **canonical_alias.remove_forall() {
Type::App(ref func, _) => match **func {
Type::Alias(ref alias) => alias.typ(),
_ => Cow::Borrowed(func),
},
Type::Alias(ref alias) => alias.typ(),
_ => Cow::Borrowed(canonical_alias.remove_forall()),
};
let (outer_params, canonical_alias, inner_type) =
unpack_canonical_alias(alias, &canonical_alias_type);

if let Type::Variant(ref variants) = **canonical_alias {
if let Type::Variant(ref variants) = **inner_type {
for field in variants.row_iter().cloned() {
let ctor_type = self.type_cache.function(
field
Expand All @@ -513,7 +539,15 @@ impl<'a> Typecheck<'a> {
);
self.stack_var(
field.name,
Type::forall(alias.params().to_owned(), ctor_type),
Type::forall(
canonical_alias
.params()
.iter()
.chain(outer_params.iter())
.cloned()
.collect(),
ctor_type,
),
);
}
}
Expand Down
18 changes: 18 additions & 0 deletions check/tests/forall.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1115,3 +1115,21 @@ let foo : (forall i . Proxy i -> ()) -> Proxy i -> () =

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

#[test]
fn forall_in_alias() {
let _ = ::env_logger::try_init();

let text = r#"
type IO a = | IO a
type Lift m v = forall a . (| Lift (m a))
let z io : IO a -> Lift IO _ = Lift io
()
"#;
let result = support::typecheck(text);

assert!(result.is_ok(), "{}", result.unwrap_err());
}
49 changes: 29 additions & 20 deletions test.glu
Original file line number Diff line number Diff line change
Expand Up @@ -10,42 +10,39 @@ 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) = {
let functor : Functor (Eff r) = {
map = error ""
}

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

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


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

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 inject : f a -> [f : f | r] a = any ()
let option_eff : Option a -> Opt 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))
type Lift m v = forall a . (| Lift (m a) (a -> v))
let lift_io io : IO a -> Eff [f : Lift IO | r] a = send (\x -> inject (Lift io x))

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

Expand Down Expand Up @@ -73,12 +70,24 @@ let run_option eff : [Functor [| r]] -> Eff [f : Option | r] a -> Eff [| r] (Opt
flat_map loop (send (\k -> map k rest))
loop (admin eff)

let run_lift eff : [Monad m] -> Eff [f : Lift m] a -> m a =
let loop ve : VE a [f : Lift m] -> m a =
match ve with
| Value v -> wrap v
| Effect e ->
match proj e with
| Found x ->
match x with
| Lift m f ->
do a = m
loop (f a)
| NotFound _ -> error "unreachable"
loop (admin eff)

// let run_io eff : Eff [io : IO | r] a -> IO a =
// match admin eff with
// | IO x -> x
// | _ -> any ()
let effect =
do x = option_empty
do y = io_effect
wrap (x #Int+ y)

do x = option_empty
do y = io_effect
wrap (x #Int+ y)
let final : IO (Option Int) = run_lift (run_option effect)
final

0 comments on commit 7e472ab

Please sign in to comment.