In this chapter, we describe the syntax and informal semantics of Haskell expressions, including their translations into the Haskell kernel, where appropriate. Except in the case of let expressions, these translations preserve both the static and dynamic semantics. Free variables and constructors used in these translations always refer to entities defined by the Prelude. For example, "concatMap" used in the translation of list comprehensions (Section 3.11) means the concatMap defined by the Prelude, regardless of whether or not the identifier "concatMap" is in scope where the list comprehension is used, and (if it is in scope) what it is bound to.
In the syntax that follows, there are some families of nonterminals indexed by precedence levels (written as a superscript). Similarly, the nonterminals op, varop, and conop may have a double index: a letter l, r, or n for left, right or nonassociativity and a precedence level. A precedencelevel variable i ranges from 0 to 9; an associativity variable a varies over {l, r, n}. For example
aexp  >  ( exp^{i+1} qop^{(a,i)} ) 
exp  >  exp^{0} :: [context =>] type  (expression type signature) 
  exp^{0}  
exp^{i}  >  exp^{i+1} [qop^{(n,i)} exp^{i+1}]  
  lexp^{i}  
  rexp^{i}  
lexp^{i}  >  (lexp^{i}  exp^{i+1}) qop^{(l,i)} exp^{i+1}  
lexp^{6}  >   exp^{7}  
rexp^{i}  >  exp^{i+1} qop^{(r,i)} (rexp^{i}  exp^{i+1})  
exp^{10}  >  \ apat_{1} ... apat_{n} > exp  (lambda abstraction, n>=1) 
  let decls in exp  (let expression)  
  if exp then exp else exp  (conditional)  
  case exp of { alts }  (case expression)  
  do { stmts }  (do expression)  
  fexp  
fexp  >  [fexp] aexp  (function application) 
aexp  >  qvar  (variable) 
  gcon  (general constructor)  
  literal  
  ( exp )  (parenthesized expression)  
  ( exp_{1} , ... , exp_{k} )  (tuple, k>=2)  
  [ exp_{1} , ... , exp_{k} ]  (list, k>=1)  
  [ exp_{1} [, exp_{2}] .. [exp_{3}] ]  (arithmetic sequence)  
  [ exp  qual_{1} , ... , qual_{n} ]  (list comprehension, n>=1)  
  ( exp^{i+1} qop^{(a,i)} )  (left section)  
  ( lexp^{i} qop^{(l,i)} )  (left section)  
  ( qop^{(a,i)}_{<>} exp^{i+1} )  (right section)  
  ( qop^{(r,i)}_{<>} rexp^{i} )  (right section)  
  qcon { fbind_{1} , ... , fbind_{n} }  (labeled construction, n>=0)  
  aexp_{<qcon>} { fbind_{1} , ... , fbind_{n} }  (labeled update, n >= 1) 
Expressions involving infix operators are disambiguated by the operator's fixity (see Section 4.4.2). Consecutive unparenthesized operators with the same precedence must both be either left or right associative to avoid a syntax error. Given an unparenthesized expression "x qop^{(a,i)} y qop^{(b,j)} z", parentheses must be added around either "x qop^{(a,i)} y" or "y qop^{(b,j)} z" when i=j unless a=b=l or a=b=r.
Negation is the only prefix operator in Haskell ; it has the same precedence as the infix  operator defined in the Prelude (see Section 4.4.2, Figure 4.1).
The grammar is ambiguous regarding the extent of lambda abstractions, let expressions, and conditionals. The ambiguity is resolved by the metarule that each of these constructs extends as far to the right as possible.
Sample parses are shown below.
This  Parses as 
f x + g y  (f x) + (g y) 
 f x + y  ( (f x)) + y 
let { ... } in x + y  let { ... } in (x + y) 
z + let { ... } in x + y  z + (let { ... } in (x + y)) 
f x y :: Int  (f x y) :: Int 
\ x > a+b :: Int  \ x > ((a+b) :: Int) 
A note about parsing. Expressions that involve the interaction
of fixities with the let/lambda metarule
may be hard to parse. For example, the expression
let x = True in x == x == True
cannot possibly mean
let x = True in (x == x == True)
because (==) is a nonassociative operator; so the expression must parse thus:
(let x = True in (x == x)) == True
However, implementations may well use a postparsing pass to deal with fixities,
so they may well incorrectly deliver the former parse. Programmers are advised
to avoid constructs whose parsing involves an interaction of (lack of) associativity
with the let/lambda metarule.
For the sake of clarity, the rest of this section shows the syntax of expressions without their precedences.
Translations of Haskell expressions use error and undefined to explicitly indicate where execution time errors may occur. The actual program behavior when an error occurs is up to the implementation. The messages passed to the error function in these translations are only suggestions; implementations may choose to display more or less information when an error occurs.
aexp  >  qvar  (variable) 
  gcon  (general constructor)  
  literal 
gcon  >  ()  
  []  
  (,{,})  
  qcon  
var  >  varid  ( varsym )  (variable) 
qvar  >  qvarid  ( qvarsym )  (qualified variable) 
con  >  conid  ( consym )  (constructor) 
qcon  >  qconid  ( gconsym )  (qualified constructor) 
varop  >  varsym  `varid `  (variable operator) 
qvarop  >  qvarsym  `qvarid `  (qualified variable operator) 
conop  >  consym  `conid `  (constructor operator) 
qconop  >  gconsym  `qconid `  (qualified constructor operator) 
op  >  varop  conop  (operator) 
qop  >  qvarop  qconop  (qualified operator) 
gconsym  >  :  qconsym 
Haskell provides special syntax to support infix notation. An operator is a function that can be applied using infix syntax (Section 3.4), or partially applied using a section (Section 3.5).
An operator is either an operator symbol, such as + or $$, or is an ordinary identifier enclosed in grave accents (backquotes), such as `op`. For example, instead of writing the prefix application op x y, one can write the infix application x `op` y. If no fixity declaration is given for `op` then it defaults to highest precedence and left associativity (see Section 4.4.2).
Dually, an operator symbol can be converted to an ordinary identifier by enclosing it in parentheses. For example, (+) x y is equivalent to x + y, and foldr (*) 1 xs is equivalent to foldr (\x y > x*y) 1 xs.
Special syntax is used to name some constructors for some of the builtin types, as found in the production for gcon and literal. These are described in Section 6.1.
An integer literal represents the application of the function fromInteger to the appropriate value of type Integer. Similarly, a floating point literal stands for an application of fromRational to a value of type Rational (that is, Ratio Integer).
Translation:The integer literal i is equivalent to fromInteger i, where fromInteger is a method in class Num (see Section 6.4.1).The floating point literal f is equivalent to fromRational (n Ratio.% d), where fromRational is a method in class Fractional and Ratio.% constructs a rational from two integers, as defined in the Ratio library. The integers n and d are chosen so that n/d = f. 
fexp  >  [fexp] aexp  (function application) 
exp  >  \ apat_{1} ... apat_{n} > exp  (lambda abstraction, n>=1) 
Function application is written e_{1} e_{2}. Application associates to the left, so the parentheses may be omitted in (f x) y. Because e_{1} could be a data constructor, partial applications of data constructors are allowed.
Lambda abstractions are written \ p_{1} ... p_{n} > e, where the p_{i} are patterns. An expression such as \x:xs>x is syntactically incorrect; it may legally be written as \(x:xs)>x.
The set of patterns must be linearno variable may appear more than once in the set.
Translation:The following identity holds:

exp  >  exp_{1} qop exp_{2}  
   exp  (prefix negation)  
qop  >  qvarop  qconop  (qualified operator) 
The form e_{1} qop e_{2} is the infix application of binary operator qop to expressions e_{1} and e_{2}.
The special form e denotes prefix negation, the only prefix operator in Haskell , and is syntax for negate (e). The binary  operator does not necessarily refer to the definition of  in the Prelude; it may be rebound by the module system. However, unary  will always refer to the negate function defined in the Prelude. There is no link between the local meaning of the  operator and unary negation.
Prefix negation has the same precedence as the infix operator  defined in the Prelude (see Table 4.1). Because e1e2 parses as an infix application of the binary operator , one must write e1(e2) for the alternative parsing. Similarly, () is syntax for (\ x y > xy), as with any infix operator, and does not denote (\ x > x)one must use negate for that.
Translation:The following identities hold:

aexp  >  ( exp^{i+1} qop^{(a,i)} )  (left section) 
  ( lexp^{i} qop^{(l,i)} )  (left section)  
  ( qop^{(a,i)}_{<>} exp^{i+1} )  (right section)  
  ( qop^{(r,i)}_{<>} rexp^{i} )  (right section) 
Sections are written as ( op e ) or ( e op ), where op is a binary operator and e is an expression. Sections are a convenient syntax for partial application of binary operators.
Syntactic precedence rules apply to sections as follows.
(op e) is legal if and only if (x op e) parses
in the same way as (x op (e));
and similarly for (e op).
For example, (*a+b) is syntactically invalid, but (+a*b) and
(*(a+b)) are valid. Because (+) is left associative, (a+b+) is syntactically correct,
but (+a+b) is not; the latter may legally be written as (+(a+b)).
As another example, the expression
(let n = 10 in n +)
is invalid because, by the let/lambda metarule (Section 3),
the expression
(let n = 10 in n + x)
parses as
(let n = 10 in (n + x))
rather than
((let n = 10 in n) + x)
Because  is treated specially in the grammar, ( exp) is not a section, but an application of prefix negation, as described in the preceding section. However, there is a subtract function defined in the Prelude such that (subtract exp) is equivalent to the disallowed section. The expression (+ ( exp)) can serve the same purpose.
Translation:The following identities hold:

exp  >  if exp_{1} then exp_{2} else exp_{3} 
A conditional expression has the form if e_{1} then e_{2} else e_{3} and returns the value of e_{2} if the value of e_{1} is True, e_{3} if e_{1} is False, and __ otherwise.
Translation:The following identity holds:

exp  >  exp_{1} qop exp_{2}  
aexp  >  [ exp_{1} , ... , exp_{k} ]  (k>=1) 
  gcon  
gcon  >  []  
  qcon  
qcon  >  ( gconsym )  
qop  >  qconop  
qconop  >  gconsym  
gconsym  >  : 
Lists are written [e_{1}, ..., e_{k}], where k>=1. The list constructor is :, and the empty list is denoted []. Standard operations on lists are given in the Prelude (see Section 6.1.3, and Chapter 8 notably Section 8.1).
Translation:The following identity holds:

aexp  >  ( exp_{1} , ... , exp_{k} )  (k>=2) 
  qcon  
qcon  >  (,{,}) 
Tuples are written (e_{1}, ..., e_{k}), and may be of arbitrary length k>=2. The constructor for an ntuple is denoted by (,...,), where there are n1 commas. Thus (a,b,c) and (,,) a b c denote the same value. Standard operations on tuples are given in the Prelude (see Section 6.1.4 and Chapter 8).
Translation:(e_{1}, ..., e_{k}) for k>=2 is an instance of a ktuple as defined in the Prelude, and requires no translation. If t_{1} through t_{k} are the types of e_{1} through e_{k}, respectively, then the type of the resulting tuple is (t_{1}, ..., t_{k}) (see Section 4.1.2). 
aexp  >  gcon 
  ( exp )  
gcon  >  () 
The form (e) is simply a parenthesized expression, and is equivalent to e. The unit expression () has type () (see Section 4.1.2). It is the only member of that type apart from __, and can be thought of as the "nullary tuple" (see Section 6.1.5).
Translation:(e) is equivalent to e. 
aexp  >  [ exp_{1} [, exp_{2}] .. [exp_{3}] ] 
The arithmetic sequence [e_{1}, e_{2} .. e_{3}] denotes a list of values of type t, where each of the e_{i} has type t, and t is an instance of class Enum.
Translation:Arithmetic sequences satisfy these identities:

The semantics of arithmetic sequences therefore depends entirely on the instance declaration for the type t. See Section 6.3.4 for more details of which Prelude types are in Enum and their semantics.
aexp  >  [ exp  qual_{1} , ... , qual_{n} ]  (list comprehension, n>=1) 
qual  >  pat < exp  (generator) 
  let decls  (local declaration)  
  exp  (guard) 
A list comprehension has the form [ e  q_{1}, ..., q_{n} ], n>=1, where the q_{i} qualifiers are either
Such a list comprehension returns the list of elements
produced by evaluating e in the successive environments
created by the nested, depthfirst evaluation of the generators in the
qualifier list. Binding of variables occurs according to the normal
pattern matching rules (see Section 3.17), and if a
match fails then that element of the list is simply skipped over. Thus:
[ x  xs < [ [(1,2),(3,4)], [(5,4),(3,2)] ],
(3,x) < xs ]
yields the list [4,2]. If a qualifier is a guard, it must evaluate
to True for the previous pattern match to succeed.
As usual, bindings in list comprehensions can shadow those in outer
scopes; for example:
[ x  x < x, x < x ]  =  [ z  y < x, z < y] 
Translation:List comprehensions satisfy these identities, which may be used as a translation into the kernel:

As indicated by the translation of list comprehensions, variables bound by let have fully polymorphic types while those defined by < are lambda bound and are thus monomorphic (see Section 4.5.4).
exp  >  let decls in exp 
Let expressions have the general form
let { d_{1} ; ... ; d_{n} } in e,
and introduce a
nested, lexicallyscoped,
mutuallyrecursive list of declarations (let is often called letrec in
other languages). The scope of the declarations is the expression e
and the right hand side of the declarations. Declarations are
described in Chapter 4. Pattern bindings are matched
lazily; an implicit ~ makes these patterns
irrefutable.
For example,
let (x,y) = undefined in e
does not cause an executiontime error until x or y is evaluated.
Translation:The dynamic semantics of the expression let { d_{1} ; ... ; d_{n} } in e_{0} are captured by this translation: After removing all type signatures, each declaration d_{i} is translated into an equation of the form p_{i} = e_{i}, where p_{i} and e_{i} are patterns and expressions respectively, using the translation in Section 4.4.3. Once done, these identities hold, which may be used as a translation into the kernel:

exp  >  case exp of { alts }  
alts  >  alt_{1} ; ... ; alt_{n}  (n>=1) 
alt  >  pat > exp [where decls]  
  pat gdpat [where decls]  
  (empty alternative)  
gdpat  >  gd > exp [ gdpat ]  
gd  >   exp^{0} 
A case expression has the general form
case e of { p_{1} match_{1} ; ... ; p_{n} match_{n} }
where each match_{i} is of the general form
 g_{i1}  > e_{i1}  
...  
 g_{imi}  > e_{imi}  
where decls_{i} 
(Notice that in the syntax rule for gd, the "" is a terminal symbol, not the syntactic metasymbol for alternation.) Each alternative p_{i} match_{i} consists of a pattern p_{i} and its matches, match_{i}. Each match in turn consists of a sequence of pairs of guards g_{ij} and bodies e_{ij} (expressions), followed by optional bindings (decls_{i}) that scope over all of the guards and expressions of the alternative. An alternative of the form
pat > exp where decls
is treated as shorthand for:
pat  True  > exp  
where decls 
A case expression must have at least one alternative and each alternative must have at least one body. Each body must have the same type, and the type of the whole expression is that type.
A case expression is evaluated by pattern matching the expression e against the individual alternatives. The alternatives are tried sequentially, from top to bottom. If e matches the pattern in the alternative, the guards for that alternative are tried sequentially from top to bottom, in the environment of the case expression extended first by the bindings created during the matching of the pattern, and then by the decls_{i} in the where clause associated with that alternative. If one of the guards evaluates to True, the corresponding righthand side is evaluated in the same environment as the guard. If all the guards evaluate to False, matching continues with the next alternative. If no match succeeds, the result is __. Pattern matching is described in Section 3.17, with the formal semantics of case expressions in Section 3.17.3.
A note about parsing. The expression
case x of { (a,_)  let b = not a in b :: Bool > a }
is tricky to parse correctly. It has a single unambiguous parse, namely
case x of { (a,_)  (let b = not a in b :: Bool) > a }
However, the phrase Bool > a is syntactically valid as a type, and
parsers with limited lookahead may incorrectly commit to this choice, and hence
reject the program. Programmers are advised, therefore, to avoid guards that
end with a type signature  indeed that is why a gd contains
an exp^{0} not an exp.
exp  >  do { stmts }  (do expression) 
stmts  >  stmt_{1} ... stmt_{n} exp [;]  (n>=0) 
stmt  >  exp ;  
  pat < exp ;  
  let decls ;  
  ;  (empty statement) 
A do expression provides a more conventional syntax for monadic programming.
It allows an expression such as
putStr "x: " >>
getLine >>= \l >
return (words l)
to be written in a more traditional way as:
do putStr "x: "
l < getLine
return (words l)
Translation:Do expressions satisfy these identities, which may be used as a translation into the kernel, after eliminating empty stmts:

Different datatypes cannot share common field labels in the same scope.
A field label can be used at most once in a constructor.
Within a datatype, however, a field label can be used in more
than one constructor provided the field has the same typing in all
constructors. To illustrate the last point, consider:
data S = S1 { x :: Int }  S2 { x :: Int }  OK
data T = T1 { y :: Int }  T2 { y :: Bool }  BAD
Here S is legal but T is not, because y is given
inconsistent typings in the latter.
aexp  >  qvar 
Field labels are used as selector functions. When used as a variable, a field label serves as a function that extracts the field from an object. Selectors are top level bindings and so they may be shadowed by local variables but cannot conflict with other top level bindings of the same name. This shadowing only affects selector functions; in record construction (Section 3.15.2) and update (Section 3.15.3), field labels cannot be confused with ordinary variables.
Translation:A field label f introduces a selector function defined as:

aexp  >  qcon { fbind_{1} , ... , fbind_{n} }  (labeled construction, n>=0) 
fbind  >  qvar = exp 
A constructor with labeled fields may be used to construct a value in which the components are specified by name rather than by position. Unlike the braces used in declaration lists, these are not subject to layout; the { and } characters must be explicit. (This is also true of field updates and field patterns.) Construction using field labels is subject to the following constraints:
Translation:In the binding f = v, the field f labels v.
The auxiliary function pick^{C}_{i} bs d is defined as follows: If the ith component of a constructor C has the field label f, and if f=v appears in the binding list bs, then pick^{C}_{i} bs d is v. Otherwise, pick^{C}_{i} bs d is the default value d. 
aexp  >  aexp_{<qcon>} { fbind_{1} , ... , fbind_{n} }  (labeled update, n>=1) 
Values belonging to a datatype with field labels may be nondestructively updated. This creates a new value in which the specified field values replace those in the existing value. Updates are restricted in the following ways:
Translation:Using the prior definition of pick,

Expression  Translation 
C1 {f1 = 3}  C1 3 undefined 
C2 {f1 = 1, f4 = 'A', f3 = 'B'}  C2 1 'B' 'A' 
x {f1 = 1}  case x of C1 _ f2 > C1 1 f2 
C2 _ f3 f4 > C2 1 f3 f4 
The field f1 is common to both constructors in T. This example translates expressions using constructors in fieldlabel notation into equivalent expressions using the same constructors without field labels. A compiletime error will result if no single constructor defines the set of field labels used in an update, such as x {f2 = 1, f3 = 'x'}.
exp  >  exp :: [context =>] type 
Expression typesignatures have the form e :: t, where e is an expression and t is a type (Section 4.1.2); they are used to type an expression explicitly and may be used to resolve ambiguous typings due to overloading (see Section 4.3.4). The value of the expression is just that of exp. As with normal type signatures (see Section 4.4.1), the declared type may be more specific than the principal type derivable from exp, but it is an error to give a type that is more general than, or not comparable to, the principal type.
Translation:

Patterns appear in lambda abstractions, function definitions, pattern bindings, list comprehensions, do expressions, and case expressions. However, the first five of these ultimately translate into case expressions, so defining the semantics of pattern matching for case expressions is sufficient.
Patterns have this syntax:
pat  >  var + integer  (successor pattern) 
  pat^{0}  
pat^{i}  >  pat^{i+1} [qconop^{(n,i)} pat^{i+1}]  
  lpat^{i}  
  rpat^{i}  
lpat^{i}  >  (lpat^{i}  pat^{i+1}) qconop^{(l,i)} pat^{i+1}  
lpat^{6}  >   (integer  float)  (negative literal) 
rpat^{i}  >  pat^{i+1} qconop^{(r,i)} (rpat^{i}  pat^{i+1})  
pat^{10}  >  apat  
  gcon apat_{1} ... apat_{k}  (arity gcon = k, k>=1)  
apat  >  var [@ apat]  (as pattern) 
  gcon  (arity gcon = 0)  
  qcon { fpat_{1} , ... , fpat_{k} }  (labeled pattern, k>=0)  
  literal  
  _  (wildcard)  
  ( pat )  (parenthesized pattern)  
  ( pat_{1} , ... , pat_{k} )  (tuple pattern, k>=2)  
  [ pat_{1} , ... , pat_{k} ]  (list pattern, k>=1)  
  ~ apat  (irrefutable pattern)  
fpat  >  qvar = pat 
The arity of a constructor must match the number of subpatterns associated with it; one cannot match against a partiallyapplied constructor.
All patterns must be linear
no variable may appear more than once. For
example, this definition is illegal:
f (x,x) = x  ILLEGAL; x used twice in pattern
Patterns of the form var@pat are called aspatterns,
and allow one to use var
as a name for the value being matched by pat. For example,
case e of { xs@(x:rest) > if x==0 then rest else xs }
is equivalent to:
let { xs = e } in
case xs of { (x:rest) > if x==0 then rest else xs }
Patterns of the form _ are
wildcards and are useful when some part of a pattern
is not referenced on the righthandside. It is as if an
identifier not used elsewhere were put in its place. For example,
case e of { [x,_,_] > if x==0 then True else False }
is equivalent to:
case e of { [x,y,z] > if x==0 then True else False }
Patterns are matched against values. Attempting to match a pattern can have one of three results: it may fail; it may succeed, returning a binding for each variable in the pattern; or it may diverge (i.e. return __). Pattern matching proceeds from left to right, and outside to inside, according to the following rules:
Operationally, this means that no matching is done on a ~apat pattern until one of the variables in apat is used. At that point the entire pattern is matched against the value, and if the match fails or diverges, so does the overall computation.
The interpretation of numeric literals is exactly as described in Section 3.2; that is, the overloaded function fromInteger or fromRational is applied to an Integer or Rational literal (resp) to convert it to the appropriate type.
The interpretation of the literal k is the same as in numeric literal patterns, except that only integer literals are allowed.
Aside from the obvious static type constraints (for example, it is a static error to match a character against a boolean), the following static class constraints hold:
Many people feel that n+k patterns should not be used. These patterns may be removed or changed in future versions of Haskell .
It is sometimes helpful to distinguish two kinds of patterns. Matching an irrefutable pattern is nonstrict: the pattern matches even if the value to be matched is __. Matching a refutable pattern is strict: if the value to be matched is __ the match diverges. The irrefutable patterns are as follows: a variable, a wildcard, N apat where N is a constructor defined by newtype and apat is irrefutable (see Section 4.2.3), var@apat where apat is irrefutable, or of the form ~apat (whether or not apat is irrefutable). All other patterns are refutable.
Here are some examples:
Top level patterns in case expressions and the set of top level patterns in function or pattern bindings may have zero or more associated guards. A guard is a boolean expression that is evaluated only after all of the arguments have been successfully matched, and it must be true for the overall pattern match to succeed. The environment of the guard is the same as the righthandside of the caseexpression alternative, function definition, or pattern binding to which it is attached.
The guard semantics have an obvious influence on the
strictness characteristics of a function or case expression. In
particular, an otherwise irrefutable pattern
may be evaluated because of a guard. For example, in
f :: (Int,Int,Int) > [Int] > Int
f ~(x,y,z) [a]  (a == y) = 1
both a and y will be evaluated by == in the guard.
The semantics of all pattern matching constructs other than case expressions are defined by giving identities that relate those constructs to case expressions. The semantics of case expressions themselves are in turn given as a series of identities, in Figures 3.13.2. Any implementation should behave so that these identities hold; it is not expected that it will use them directly, since that would generate rather inefficient code.
Figure 4Semantics of Case Expressions, Part 2 
In Figures 3.13.2: e, e' and e_{i} are expressions; g and g_{i} are booleanvalued expressions; p and p_{i} are patterns; v, x, and x_{i} are variables; K and K' are algebraic datatype (data) constructors (including tuple constructors); and N is a newtype constructor.
Rule (b) matches a general sourcelanguage case expression, regardless of whether it actually includes guardsif no guards are written, then True is substituted for the guards g_{i,j} in the match_{i} forms. Subsequent identities manipulate the resulting case expression into simpler and simpler forms.
Rule (h) in Figure 3.2 involves the overloaded operator ==; it is this rule that defines the meaning of pattern matching against overloaded constants.
These identities all preserve the static semantics. Rules (d), (e), (j), (q), and (s) use a lambda rather than a let; this indicates that variables bound by case are monomorphically typed (Section 4.1.4).