Unify toplevel codefinition and local comatch.

[BinderDavid]

Currently we have toplevel codefinitions:

codef CountUp(n: Nat): Stream(Nat) {
    head(_) => n,
    tail(_) => CountUp(S(n)),
}

and local comatches

comatch {
    head(_) => n,
    tail(_) => CountUp(S(n)),
}

Morally, the codef construct is just syntactic sugar for:

let CountUp(n : Nat): Stream(Nat) {
    comatch {
      head(_) => n,
      tail(_) => CountUp(S(n)),
    }
}

But in the implementation we don't make that explicit:

#[derive(Debug, Clone)]
pub struct Codef {
    pub span: Option<Span>,
    pub doc: Option<DocComment>,
    pub name: Ident,
    pub attr: Attribute,
    pub params: Telescope,
    pub typ: TypCtor,
    pub body: Match,
}

So I propose to make it explicit by changing the definition to something like:

#[derive(Debug, Clone)]
pub struct Codef {
    pub span: Option<Span>,
    pub doc: Option<DocComment>,
    pub name: Ident,
    pub attr: Attribute,
    pub params: Telescope,
    pub typ: TypCtor,
    pub body: LocalComatch,
}

We can do a similar thing for Def/LocalMatch, but there they don't behave similarly enough yet due to the different handling of self parameters.

[BinderDavid]

I think this means that we also have to add a returns clause for local comatches, which makes sense. Currently we cannot infer the type of a comatch:

impl CheckInfer for LocalComatch {
    fn check(&self, prg: &Prg, ctx: &mut Ctx, t: Rc<Exp>) -> Result<Self, TypeError> {
      ...
    }

    fn infer(&self, _prg: &Prg, _ctx: &mut Ctx) -> Result<Self, TypeError> {
        Err(TypeError::CannotInferComatch { span: self.span().to_miette() })
    }
}

but we can add specialized syntax for the expected return type, i.e:

comatch : Stream(Nat) {
    head(_) => n,
    tail(_) => CountUp(S(n)),
}

Then we would desugar the codefinition from above to:

let CountUp(n : Nat): Stream(Nat) {
    comatch : Stream(Nat) {
      head(_) => n,
      tail(_) => CountUp(S(n)),
    }