From 29c907de13cc84e4cbdfcebf044d73e5f523085d Mon Sep 17 00:00:00 2001
From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
Date: Wed, 13 Jan 2016 15:14:15 +0900
Subject: [PATCH] add description of refutation cases

---
 manual/manual/refman/exten.etex | 43 +++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)

diff --git a/manual/manual/refman/exten.etex b/manual/manual/refman/exten.etex
index a38a53c1f..501291987 100644
--- a/manual/manual/refman/exten.etex
+++ b/manual/manual/refman/exten.etex
@@ -1211,6 +1211,49 @@ exhaustive (the "Add" case cannot happen).
           | App(_,_) -> 0
 \end{verbatim}
 
+
+\paragraph{Refutation cases and redundancy} (Introduced in 4.03)
+
+Usually, the exhaustiveness check only tries to check whether the
+cases omitted from the pattern matching are typable or not.
+However, you can force it to try harder by adding {\em refutation cases}:
+\begin{syntax}
+matching-case:
+     pattern ['when' expr] '->' expr
+   | pattern '->' '.'
+\end{syntax}
+In presence of a refutation case, the exhaustiveness check will first
+compute the intersection of the pattern with the complement of the
+cases preceding it. It then checks whether the resulting patterns can
+really match any concrete values by trying to type-check them.
+Wild cards in the generated patterns are handled in a special way: if
+their type is a variant type with only GADT constructors, then the
+pattern is split into the different constructors, in order to check whether
+any of them is possible (this splitting is not done for arguments of these
+constructors, to avoid non-termination.) We also split tuples and
+variant types with only one case, since they may contain GADTs inside.
+For instance, the following code is deemed exhaustive:
+
+\begin{verbatim}
+        type _ t =
+          | Int : int t
+          | Bool : bool t
+
+        let deep : (char t * int) option -> char = function
+          | None -> 'c'
+          | _ -> .
+\end{verbatim}
+
+Namely, the inferred remaining case is "Some _", which is split into
+"Some (Int, _)" and "Some (Bool, _)", which are both untypable.
+Note that the refutation case could be omitted here, because it is
+automatically added when there is only one case in the pattern
+matching.
+
+Another addition is that the redundancy check is now aware of GADTs: a
+case will be detected as redundant if it could be replaced by a
+refutation case using the same pattern.
+
 \paragraph{Advanced examples}
 The "term" type we have defined above is an {\em indexed} type, where
 a type parameter reflects a property of the value contents.