Type disambiguation and PPX

[bobot]

A PPX could break type disambiguation of constructors in the sense that the code compile before the ppx and not after. For example landmark wrap function in a way comparable to the second version of the function.

module M = struct
type t = A

end

let f x : M.t = A

let f x : M.t =
  let r = A in Landmark.exit (); r

The first function types but not the second one because the typer doesn't know that the type of r is the type of the whole expression.

A ppx could add type variables for simplifying the link to the OCaml typer:

let f x : M.t =
  (let r = (A:landmark') in Landmark.exit (); r : landmark')

The typer would need to look at the type annotation before typing the term, which it seems not to do currently (surely for a good reason).

[nojb]

cc @mlasson

[lthls]

Does the following alternate approach look realistic ?

(* Before instrumentation *)
(fun x y : t -> body)
(* With current Landmark *)
(fun x y : t -> let r = body in Landmark.exit (); r)
(* Alternative *)
(fun x y -> let[@local always] orig = (fun x y : t -> body) in let r = orig x y in Landmark.exit (); r)

With the local functions optimisation, that should give you the same code in the end, but the type-checker would still see the type annotations in the right place.

[mlasson]

@lthls, yes it does !

I think should be able to use this trick to solve LexiFi/landmarks#31 without any modification to the compiler.

[gasche]

It looks like currently the typing of (e : ty) is careful to not unify ty with the expected type before e is itself type-checked. I'm not sure what is the reason for this (@garrigue would know); I think it may come from older versions where the logic of (x : t) and (x : t :> u) was shared in the code. If I read things correctly, the pattern-side construct (p : ty) does unify the expected type with the annotation before checking the pattern, so maybe that would also be a reasonable approach for expressions.

Personally I think it would be nice if expert metaprogramming users could control propagation of type information through type variables as proposed by François (using (... : 'a) to capture the expected type 'a to be used in ...). The translation proposed by Vincent is less local, as it assumes that we know we are inside an annotated-function construct, and it is more complex.

[lpw25]

I think that using variables like that in a principal way would require a different notion of type variable, with different scoping and behaviour. It's not enough to change the order of unification in constraints -- that will work without -principal but it will still fail with it.

How often do people really need to move some user code from a checking position to an inference position? Adding some cleanup code, as in this example, is an obvious case, but that might be better served by just adding a simple try ... finally ... construct instead.

[bobot]

@lthls it does not always works. The case is simplified, in the real case f is a method and the type of the expression is obtained from inheritance. So t can't be copied.

However it could still be an improvement for landmark in other cases.

EDIT: In fact the type variable trick works already! If it is put before the equal at the place of an absent t as shown in the issue pointed LexiFi/landmarks#31 by @mlasson

[gasche]

How often do people really need to move some user code from a checking position to an inference position? Adding some cleanup code, as in this example, is an obvious case, but that might be better served by just adding a simple try ... finally ... construct instead.

And try ... finally%lwt ..., etc. I suspect that in general there may be a family of control-capture abstractions (for example in resourceful monads) needing this approach, where a more general solution would be required. I wonder about having expected-type-propagating function types for example; for example (unit -> -'a) -> (exn -> -'a) -> +'a, imitating Prolog mode declarations.

[gasche]

@bobot regarding the type variable, fun x : 'a -> ... and fun x : (t as 'a) -> ... work, but fun x : t -> (... : 'a) does not, and the former requires non-local reasoning so it is a less general approach.

[garrigue]

It looks like currently the typing of (e : ty) is careful to not unify ty with the expected type before e is itself type-checked. I'm not sure what is the reason for this (@garrigue would know); I think it may come from older versions where the logic of (x : t) and (x : t :> u) was shared in the code. If I read things correctly, the pattern-side construct (p : ty) does unify the expected type with the annotation before checking the pattern, so maybe that would also be a reasonable approach for expressions.

Indeed, it would be possible to propagate the expected type to the expression, combining it with the type annotation. This must be done with care, so that we really add information. I believe I just assumed that if you give a type annotation it would be precise enough that you don't need to propagate the expected type through it.

Personally I think it would be nice if expert metaprogramming users could control propagation of type information through type variables as proposed by François (using (... : 'a) to capture the expected type 'a to be used in ...). The translation proposed by Vincent is less local, as it assumes that we know we are inside an annotated-function construct, and it is more complex.

As @lpw25 explained, type variables can be used as constraints, but they cannot be used to propagate explicit type information, because the algorithm will always see them as implicit in principal mode.

If you want to use local abbreviations, you can do something like this, but I don't know if this is very practical:

module M = struct type t = A end
type (_,_) eq = Refl : ('a,'a) eq
let f (type a) (w : (a, M.t) eq) = let Refl = w in (A : a)

[gasche]

I don't understand your proposed translation. How would you transform

let f x : M.t =
  let r = A in Landmark.exit (); r

to ensure that the expected type of let r = A in exit (); r is also known by the type-checker to be the expected type of r ?

[lpw25]

And try ... finally%lwt ..., etc.

To be clear, I wasn't proposing that try ... finally ... would be used by the user instead of a ppx -- although I'm sure it would be useful -- I was proposing that ppxes like landmark could generate try ... finally ... when they wanted to add side-effects after a user expression without changing the flow of expected type information to that expression.

[github-actions]

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.