> From: Yaron Minsky <yminsky@gmail.com>
> 
> > Interesting.  I guess this is best understood as a limitation of the
> > type-checking algorithm.  Does anyone know if there are any plans to
> > remove this limitation?  Are there fundamental reasons why it would be
> > difficult to do so?
> 
> This is not a limitation of the type checking algorithm per se.
> Rather, the type checking algorithm prefers not to use
> exhaustiveness information when this can be avoided, to keep it
> predictable.
> (Exhaustiveness is only used for polymorphic variants, but for
> a deeper reason.)

Besides, the test for exhautiveness much relies on typing having been
performed. (Except for variants, which undergo a preliminary, specific kind
of exhautiveness checking before typing).

-- 
Luc Maranget