Re: [Caml-list] Why doesn't ocamlopt detect a missing ; afterfailwith statement?

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: Frederic van der Plancke <fvdp@decis.be>

> > The problem is rather that the technique I use, based on type
> > inference, is not foolproof (you can avoid the warning with a type
> > annotation for instance) and is wrong in presence of Obj.magic.
> > So the question is in which cases having a warning is worth the
> > inconvenience and the extra code in the compiler.
> 
> Why not create a special type "noreturn" or "empty" with special typing properties ? in most respect it would act like 'a; but the compiler would know the difference.
> * raise : exn -> noreturn   (and hence: failwith : string -> noreturn)
>   (similarly: [assert false : noreturn])
>   but Obj.magic keeps its type : 'a -> 'b
> * noreturn can be unified to any type t (including 'a), this yields type t
>    (so [function [] -> assert false | x::_ -> x] has type ['a list -> 'a])

This just looks like a much higher cost in terms of changes to the
compiler. And the danger of introducing bugs in unification, just for a
warning in some strange cases. (You should realize that what you are
proposing is not a new type, but a new kind of type variables.)
The generalization technique works well. It is not surprising that it
doesn't mix that well with Obj.magic, but then Obj.magic is clearly
unsound, so you know what to expect.

        Objective Caml version 3.09+dev9 (2004-11-29)

# fun () -> raise Exit print_int 3;;
                       ^^^^^^^^^
Warning X: this argument will not be received by the function.
# fun () -> raise Exit; "Hello";;
            ^^^^^^^^^^
Warning X: this statement never returns.
# fun f -> ((Obj.magic f) 3);;
                          ^
Warning X: this argument will not be received by the function.
# fun f -> ((Obj.magic f : _ -> _) 3);;
- : 'a -> 'b = <fun>

Jacques Garrigue