More comments (related to Trac #10180)
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 24 Mar 2015 13:52:20 +0000 (13:52 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 24 Mar 2015 13:52:20 +0000 (13:52 +0000)
compiler/coreSyn/CoreLint.hs
compiler/coreSyn/CoreSyn.hs
compiler/coreSyn/CoreUtils.hs

index c0ca270..256a682 100644 (file)
@@ -718,24 +718,23 @@ applied in the type variables:
 
 Note [No alternatives lint check]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
 Case expressions with no alternatives are odd beasts, and worth looking at
-in the linter.
-
-Certainly, it would be terribly wrong if the scrutinee was already in head
-normal form. That is the first check.
-
-Furthermore, we should be able to see why GHC believes the scrutinee is
-diverging for sure. That is the second check. see #10180.
-
-In principle, the first check is redundant: exprIsBottom == True will always
-imply exprIsHNF == False.
-But the first check is reliable: If exprIsHNF == True, then there definitely is
-a problem (exprIsHNF errs on the right side).
-If the second check triggers then it may be the case that the compiler got
-smarter elsewhere, and the empty case is correct, but that exprIsBottom is
-unable to see it. Therefore, this check is not fully reliable, and we keep
-both around.
+in the linter (cf Trac #10180).  We check two things:
+
+* exprIsHNF is false: certainly, it would be terribly wrong if the
+  scrutinee was already in head normal form.
+
+* exprIsBottom is true: we should be able to see why GHC believes the
+  scrutinee is diverging for sure.
+
+In principle, the first check is redundant: exprIsBottom == True will
+always imply exprIsHNF == False.  But the first check is reliable: If
+exprIsHNF == True, then there definitely is a problem (exprIsHNF errs
+on the right side).  If the second check triggers then it may be the
+case that the compiler got smarter elsewhere, and the empty case is
+correct, but that exprIsBottom is unable to see it. In particular, the
+empty-type check in exprIsBottom is an approximation. Therefore, this
+check is not fully reliable, and we keep both around.
 
 ************************************************************************
 *                                                                      *
index b744ea2..e614c93 100644 (file)
@@ -379,25 +379,20 @@ See #type_let#
 
 Note [Empty case alternatives]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The alternatives of a case expression should be exhaustive.  A case expression
-can have empty alternatives if (and only if) the scrutinee is bound to raise
-an exception or diverge.  So:
-   Case (error Int "Hello") b Bool []
-is fine, and has type Bool.  This is one reason we need a type on
-the case expression: if the alternatives are empty we can't get the type
-from the alternatives!  I'll write this
-   case (error Int "Hello") of Bool {}
-with the return type just before the alternatives.
-
-Here's another example:
+The alternatives of a case expression should be exhaustive.
+
+A case expression can have empty alternatives if (and only if) the
+scrutinee is bound to raise an exception or diverge. When do we know
+this?  See Note [Bottoming expressions] in CoreUtils.
+
+The possiblity of empty alternatives is one reason we need a type on
+the case expression: if the alternatives are empty we can't get the
+type from the alternatives!
+
+In the case of empty types (see Note [Bottoming expressions]), say
   data T
-  f :: T -> Bool
-  f = \(x:t). case x of Bool {}
-Since T has no data constructors, the case alternatives are of course
-empty.  However note that 'x' is not bound to a visibly-bottom value;
-it's the *type* that tells us it's going to diverge.  Its a bit of a
-degnerate situation but we do NOT want to replace
-   case x of Bool {}   -->   error Bool "Inaccessible case"
+we do NOT want to replace
+   case (x::T) of Bool {}   -->   error Bool "Inaccessible case"
 because x might raise an exception, and *that*'s what we want to see!
 (Trac #6067 is an example.) To preserve semantics we'd have to say
    x `seq` error Bool "Inaccessible case"
index f400ebc..d7344e1 100644 (file)
@@ -694,11 +694,11 @@ expensive.
 -}
 
 exprIsBottom :: CoreExpr -> Bool
--- If the type only contains no elements besides bottom, then this expressions,
--- well, bottom.
-exprIsBottom e | isEmptyTy (exprType e) = True
--- Otherwise see if this is a bottoming id applied to enough arguments
+-- See Note [Bottoming expressions]
 exprIsBottom e
+  | isEmptyTy (exprType e)
+  = True
+  | otherwise
   = go 0 e
   where
     go n (Var v) = isBottomingId v &&  n >= idArity v
@@ -710,7 +710,36 @@ exprIsBottom e
     go n (Lam v e) | isTyVar v   = go n e
     go _ _                       = False
 
-{-
+{- Note [Bottoming expressions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A bottoming expression is guaranteed to diverge, or raise an
+exception.  We can test for it in two different ways, and exprIsBottom
+checks for both of these situations:
+
+* Visibly-bottom computations.  For example
+      (error Int "Hello")
+  is visibly bottom.  The strictness analyser also finds out if
+  a function diverges or raises an exception, and puts that info
+  in its strictness signature.
+
+* Empty types.  If a type is empty, its only inhabitant is bottom.
+  For example:
+      data T
+      f :: T -> Bool
+      f = \(x:t). case x of Bool {}
+  Since T has no data constructors, the case alternatives are of course
+  empty.  However note that 'x' is not bound to a visibly-bottom value;
+  it's the *type* that tells us it's going to diverge.
+
+A GADT may also be empty even though it has constructors:
+        data T a where
+          T1 :: a -> T Bool
+          T2 :: T Int
+        ...(case (x::T Char) of {})...
+Here (T Char) is uninhabited.  A more realistic case is (Int ~ Bool),
+which is likewise uninhabited.
+
+
 ************************************************************************
 *                                                                      *
              exprIsDupable
@@ -2114,8 +2143,9 @@ rhsIsStatic platform is_dynamic_name cvt_integer rhs = is_static False rhs
 
 -- | True if the type has no non-bottom elements, e.g. when it is an empty
 -- datatype, or a GADT with non-satisfiable type parameters, e.g. Int :~: Bool.
+-- See Note [Bottoming expressions]
 --
--- See Note [No alternatives lint check] for one use of this function.
+-- See Note [No alternatives lint check] for another use of this function.
 isEmptyTy :: Type -> Bool
 isEmptyTy ty
     -- Data types where, given the particular type parameters, no data