Comment author: @garrigue

This is nothing about Obj.magic, but just about the relaxed value restriction.
Basically, the relaxed value restriction says that a type variable appearing only in covariant positions can be generalized, even if the subject is not a value.

(* Accepted. *)
module M : sig
val id : 'a -> 'a
end = struct
let id (x : int) = x
let id = Obj.magic id
end

Here id is first typed as 'a, which is generalizable, and 'a -> 'a is an instance of it.

(* Rejected. *)
module M : sig
val id : 'a -> 'a
end = struct
let id (x : int) = x
let id : 'a . 'a -> 'a = Obj.magic id
end

Here the type annotation is propagated to the expression, and Obj.magic id is typed as 'a -> 'a, which is not generalizable.
If you want to make it generalizable, you have to work in two steps, just as for the typing of modules.

let id2 = Obj.magic id (* generalized as 'a covariant )
let id3 : 'a. 'a -> 'a = id2 ( generalizable since this is a value *)

One could argue that we should not propagate the constraint inside, but in other cases this propagation is actually needed...

Comment author: @fpottier

Thanks Jacques.

I knew about the relaxed value restriction, but did not realize that it does not commute with the propagation of type annotations. Interesting.

What about my suggestion of always viewing "Obj.magic v" as a value?

Francois.

Comment author: @garrigue

You suggest adding a new rule for Obj.magic?
Something saying that Obj.magic applied to a value is a value?

This could of course be done, but as I have shown, you can already obtain the same effect by doing the binding in two steps. So is it really worth extending the specification of the type system just for one function?

If we do that, we would probably want to do that for all the primitives which have no side-effects.

Comment author: @fpottier

Yes, I suggest Obj.magic applied to a value should be a value.
Doing the same thing for other primitives as well would make sense.

It's just that binding in two steps is painful (and is a trick
which only an expert can know about...).

Comment author: @alainfrisch

It's just that binding in two steps is painful (and is a trick
which only an expert can know about...).

I'm not convinced that adding code to the type-checker only to simplify the use of Obj.magic by non-expert users is relevant.

Doing the same thing for other primitives as well would make sense.

What would be the typical examples of other polymorphic primitives where the variable appear on the result type, and without side effects?

Comment author: @garrigue

The trivial example is Obj.obj (which is just a variant of Obj.magic).
More interesting examples are fst and snd, which are primitives, but must meet the value restriction.
I'm not very enthusiastic either. But I get asked repeatedly about this trick; maybe putting it in a FAQ would be enough.