[commit: ghc] master: More comments (related to Trac #10180) (33cfa5f)
git at git.haskell.org
git at git.haskell.org
Tue Mar 24 13:52:28 UTC 2015
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/33cfa5ff9db4e7886b3e7c2eed5ac1c75436bc4c/ghc
>---------------------------------------------------------------
commit 33cfa5ff9db4e7886b3e7c2eed5ac1c75436bc4c
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Tue Mar 24 13:52:20 2015 +0000
More comments (related to Trac #10180)
>---------------------------------------------------------------
33cfa5ff9db4e7886b3e7c2eed5ac1c75436bc4c
compiler/coreSyn/CoreLint.hs | 33 ++++++++++++++++-----------------
compiler/coreSyn/CoreSyn.hs | 31 +++++++++++++------------------
compiler/coreSyn/CoreUtils.hs | 42 ++++++++++++++++++++++++++++++++++++------
3 files changed, 65 insertions(+), 41 deletions(-)
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index c0ca270..256a682 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -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.
************************************************************************
* *
diff --git a/compiler/coreSyn/CoreSyn.hs b/compiler/coreSyn/CoreSyn.hs
index b744ea2..e614c93 100644
--- a/compiler/coreSyn/CoreSyn.hs
+++ b/compiler/coreSyn/CoreSyn.hs
@@ -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"
diff --git a/compiler/coreSyn/CoreUtils.hs b/compiler/coreSyn/CoreUtils.hs
index f400ebc..d7344e1 100644
--- a/compiler/coreSyn/CoreUtils.hs
+++ b/compiler/coreSyn/CoreUtils.hs
@@ -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
More information about the ghc-commits
mailing list