Commit 33cfa5ff authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

More comments (related to Trac #10180)

parent 8eaa70a6
......@@ -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.
************************************************************************
* *
......
......@@ -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"
......
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment