type alias is too hacky

[mimoo]

How do we generate type aliases?

We have a decl_type_alias! that can be used like this:

decl_type_alias!(w, env, "t" => SomeType<SomeConcreteType>);
decl_func!(w, env, thing);

it will then generate code like this:

type nonrec t = (Path.Of.some_concrete_type) Path.Of.some_type
external thing : unit -> (Path.Of.some_concrete_type) Path.Of.some_type = "thing"

The problem

as you can see, the return type of the function thing was not rewritten to simply point to t

Although it might work, this is probably not doing what you think it should do. Worse, it sometimes won't work.

Imagine that you are declaring the following:

decl_type!(w, env, SomeType<T1> => "t");

decl_module!(w, env, "A", {
  decl_type_alias!(w, env, "t" => SomeType<SomeConcreteType>);
  decl_func!(w, env, thing);
});

it will then generate code like this:

type 'a t = ...

module A = struct
  type nonrec t = (Path.Of.some_concrete_type) t
  external thing : unit -> (Path.Of.some_concrete_type) t = "thing"
end

This is obviously wrong, we have a type collision (talked about in https://github.com/o1-labs/proof-systems/issues/176 as well).

Solution?

What we want here is simple:

• we want to track the location of SomeType<SomeConcreteType> when we declare the type alias
• we want to first try to get that location when SomeType<SomeConcreteType> is used, and fallback on the location of SomeType<T1> (the generic type) otherwise

The problem is that we are tracking types and their location based on the generic type only (regardless of if the type parameters are concrete or not). I don't see how we could have our trait implementation be dependent on the type parameters:

/// OCamlDesc is the trait implemented by types to facilitate generation of their OCaml bindings.
/// It is usually derived automatically via the [Struct] macro,
/// or the [CustomType] macro for custom types.
pub trait OCamlDesc {
    /// describes the type in OCaml, given the current environment [Env]
    /// and the list of generic type parameters of the root type
    /// (the type that makes use of this type)
    fn ocaml_desc(env: &Env, generics: &[&str]) -> String;

    /// Returns a unique ID for the type. This ID will not change if concrete type parameters are used.
    fn unique_id() -> u128;
}

actually... since every type must implement this, we could just use the ocaml_desc to return the full string name of a type instead of using the unique_id. I think this could work, but we lose the benefit of having a unique_id.

We could always use the unique_id as a fallback though...

It'd be good to document what the unique_id really solves first. The idea was that we wanted to differentiate different types, even if they were named the same in Rust.

---

I found out here that using a mix of unique_id to distinguish between different instantiations of the same type wouldn't work: https://github.com/o1-labs/proof-systems/issues/172 but I'm not convinced anymore that this is true...

working on this in https://github.com/o1-labs/proof-systems/tree/mimoo/ocaml_custom

[mimoo]

cf https://github.com/o1-labs/proof-systems/pull/206 as well

[mimoo]

I've implemented a short-term solution, but it'll probably have some issues with aliases on different generics:

t1 := alias of Thing<T1>
t2 := alias of Thing<T2>

I think this will crash, although it might be worse and silently do something bad. The solution is probably to do what the previous comment is saying: calculte the unique id based on the XOR of the instantiated type parameters unique id + that generic type unique id

[mimoo]

it will crash if you do this, but there's another problem which is dangerous at the moment. If you do this:

t1 := alias of Thing<T1>

and you have a function that returns a Thing<T2>, the Thing<T2> will be renamed to t1.

[mimoo]

I think in general this type alias thing is a BAD IDEA, but we use it in Mina so I'll keep it around until we don't need it anymore