Jacques Garrigue wrote:
> 
> From: Damien Doligez <damien.doligez@inria.fr>
> > > I believe the problem with failwith is solvable, albeit rather
> > > complicated. The idea is that you want to be warned when you apply a
> > > function of type (\forall 'a. 'a) to something, because no such
> > > function may exist, so that this application will never actually take
> > > place.
> >
> > More generally, you want to output a warning whenever the computation
> > of such a value is not immediately followed by a join in the control
> > flow graph, because at that point you know you're compiling dead code.
> >
> > Then you would also get a warning for things like this:
> >
> >    failwith "foo";
> >    print_string "hello world"
> >
> > or
> >
> >    f (a, b, failwith "foo", c, d)
> >
> > etc.
> >
> > Don't ask me to implement it, though.
> 
> This is not specially hard to implement case by case.
> 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])
* a warning would be issued
   - for an "apply" node when any input term has type noreturn
   - for a ";" node when the first term has type noreturn
   - etc
* problem: one could write [Obj.magic 123 : noreturn]
  (or similarly in other cases like marshalling where a lone 'a *can*
   correspond to a value) and defeat the system.
  possible solution: forbid or restrict explicit casts (er, type annotations,
  sorry ;-) to noreturn. (i.e. since 'a annotates "a value of any type" and
  noreturn annotates "no value", there's no reason to allow "casting" 'a as
  noreturn.)

Frédéric vdP