cannot infer an appropriate lifetime

[brendanzab]

I'm experimenting with making a type checker using eff. Eventually I want to try implementing "An Algebraic Approach to Typechecking and Elaboration" using it.

use eff::{eff, Effect};

#[derive(Debug)]
pub struct Report(pub String);

impl Effect for Report {
    type Output = ();
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Type {
    Base,
    Fun(Box<Type>, Box<Type>),
    Error,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Term {
    Var(usize),
    FunIntro(Box<Type>, Box<Term>),
    FunElim(Box<Term>, Box<Term>),
}

#[eff(Report)]
pub fn ty_check(context: &mut Vec<Type>, term: &Term) -> Type {
    match term {
        Term::Var(index) => match context.get(*index) {
            Some(ty) => ty.clone(),
            None => {
                eff::perform!(Report("unknown variable".to_owned()));
                Type::Error
            }
        },
        Term::FunIntro(ty, body) => {
            context.push((**ty).clone());
            let body_ty = eff::perform_from!(ty_check(context, body));
            context.pop();
            body_ty
        }
        Term::FunElim(fun, arg) => match eff::perform_from!(ty_check(context, fun)) {
            Type::Fun(param_ty, body_ty) => match eff::perform_from!(ty_check(context, arg)) {
                Type::Error => Type::Error,
                arg_ty if arg_ty == *param_ty => (*body_ty).clone(),
                _ => {
                    eff::perform!(Report("mismatched parameter".to_owned()));
                    Type::Error
                }
            },
            _ => Type::Error,
        },
    }
}

Sadly I get the following error:

error: cannot infer an appropriate lifetime
  --> src/lam1_eff.rs:24:1
   |
24 | #[eff(Report)]
   | ^^^^^^^^^^^^^^
   | |
   | this return type evaluates to the `'static` lifetime...
   | ...but this borrow...
   |
note: ...can't outlive the anonymous lifetime #2 defined on the function body at 24:14
  --> src/lam1_eff.rs:24:14
   |
24 | #[eff(Report)]
   |              ^
help: you can add a constraint to the return type to make it last less than `'static` and match the anonymous lifetime #2 defined on the function body at 24:14
   |
24 | #[eff(Report)] + '_
   |

error: cannot infer an appropriate lifetime
  --> src/lam1_eff.rs:24:1
   |
24 | #[eff(Report)]
   | ^^^^^^^^^^^^^^
   | |
   | this return type evaluates to the `'static` lifetime...
   | ...but this borrow...
   |
note: ...can't outlive the anonymous lifetime #1 defined on the function body at 24:14
  --> src/lam1_eff.rs:24:14
   |
24 | #[eff(Report)]
   |              ^
help: you can add a constraint to the return type to make it last less than `'static` and match the anonymous lifetime #1 defined on the function body at 24:14
   |
24 | #[eff(Report)] + '_
   |

error: aborting due to 2 previous errors

Any thoughts on what might be causing this?

In addition, it was a bit of a challenge to figure out how to call an effectful function recusively, seeing as there's no example of this! I had to find it in the state test! Might be handy to make it more prominent in the docs if you have a chance! :)

[pandaman64]

Hi! Thank you for your feedback. I found my first user 😄

The root cause of your compile error is that the computation returned by ty_check captures both of context and term. Therefore, the computation must be outlived by both lifetimes, but expressing it in Rust is a little bit tricky.
One way to do that is introducing another lifetime shorter than both, though you need to write the real signature of your function by yourself instead of using eff macro.
For example:

pub fn ty_check<'c, 'a: 'c, 'b: 'c>(context: &'a mut Vec<Type>, term: &'b Term) -> impl Effectful<Output = Type, Effect = Coproduct![Report]> + 'c {
    effectful!{ // macro for creating an effectful computation block
        match term {
            Term::Var(index) => match context.get(*index) {
                Some(ty) => ty.clone(),
                None => {
                    eff::perform!(Report("unknown variable".to_owned()));
                    Type::Error
                }
            },
            Term::FunIntro(ty, body) => {
                context.push((**ty).clone());
                let comp = ty_check(context, body).boxed();  // boxing recursive call
                let body_ty = eff::perform_from!(comp);
                context.pop();
                body_ty
            }
            Term::FunElim(fun, arg) => {
                let comp = ty_check(context, fun).boxed();
                match eff::perform_from!(comp) {
                    Type::Fun(param_ty, body_ty) => {
                        let comp = ty_check(context, arg).boxed();
                        match eff::perform_from!(comp) {
                            Type::Error => Type::Error,
                            ref arg_ty if *arg_ty == *param_ty => (*body_ty).clone(),
                            _ => {
                                eff::perform!(Report("mismatched parameter".to_owned()));
                                Type::Error
                            }
                        }
                    },
                    _ => Type::Error,
                }
            },
        }
    }
}

You also need to box your recursive call since it wll create an infinite type otherwise. This is as same as you cannot make recursive async fn.

[brendanzab]

Oh, right! I see - I guess it's a bit much for the attribute to handle... the fun of wrangling Rust!

[brendanzab]

Yeah, it might be helpful to have some docs showing what the eff attribute expands to! It's nice to see that here - I might have been able to debug it a bit better from there 😅

[pandaman64]

you can try cargo-expand 👍
It’s basically wrapping the function body in a generator and some type puzzles.