> N'ayant pas entrevu de message a ce propos je me permet
> de poser la question suivante : 
> 
> Soit le code suivant (stupide soit mais pas pour le typage)
> 
> # fun x -> x
> #   | x -> 1 + x
> #;;
> 
> La reponse est la suivante :
> 
> Toplevel input:
> >  | x -> 1 + x
> >    ^
> Warning: this matching case is unused.
> - : int -> int = <fun>
> 
> Ma question est la suivante : pourquoi prendre en compte
> cette branche lors du typage, qui de ce fait instancie le
> type de 'x' par 'int' ? 

1) Parceque la de'tection du ``cas inutile'' n'est pas de la
responsabilite' du contro^leur de type, c'est le compilateur qui en
fait l'analyse, apre`s le passage du typeur.

2) C'est une proprie'te' se'mantique du programme qui n'est pas du ressort
de conside'rations de typage. De la me^me manie`re

(function x -> if true then x else 1)

aura le type int -> int, quand il est clair que cette fonction est
e'quivalente a` (function x -> x) qui a le type 'a -> 'a.

Conclusion: le contro^leur de types traite votre programme, tout votre
programme, rien que votre programme. Il de'tectera une erreur me^me
s'il existe un programme simplifie' e'quivalent au vo^tre qui pourrait
e^tre correctement type'. (L'analyseur syntaxique fait de me^me et
conside`re if false then + - * else 1 comme syntaxiquement incorrect,
alors qu'il pourrait jetter la branche then sans changer la
se'mantique du programme.)

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://pauillac.inria.fr/~weis/