This Note describes the implementation of
GHC proposal 516 "Add warning for incomplete record selectors".
A **partial field** is a field that does not belong to every constructor of the
corresponding datatype.
A **partial selector occurrence** is a use of a record selector for a partial
field, either as a selector function in an expression, or as the solution to a
HasField constraint.
Partial selector occurrences desugar to case expressions which may crash at
runtime:
data T a where
T1 :: T Int
T2 {sel :: Int} :: T Bool
urgh :: T a -> Int
urgh x = sel x
===>
urgh x = case x of
T1 -> error "no record field sel"
T2 f -> f
As such, it makes sense to warn about such potential crashes.
We do so whenever -Wincomplete-record-selectors is present, and we utilise
the pattern-match coverage checker for precise results, because there are many
uses of selectors for partial fields which are in fact dynamically safe.
Pmc can detect two very common safe uses for which we will not warn:
(LDI) Ambient pattern-matches unleash Note [Long-distance information] that
render a naively flagged partial selector occurrence safe, as in
ldi :: T a -> Int
ldi T1 = 0
ldi arg = sel arg
We should not warn here, because `arg` cannot be `T1`.
(RES) Constraining the result type of a GADT such as T might render
naively flagged partial selector occurrences safe, as in
resTy :: T Bool -> Int
resTy = sel
Here, `T1 :: T Int` is ruled out because it has the wrong result type.
Additionally, we want to support incomplete -XOverloadedRecordDot access as
well, in either the (LDI) use case or the (RES) use case:
data Dot = No | Yes { sel2 :: Int }
dot d = d.sel2 -- should warn
ldiDot No = 0
ldiDot d = d.sel2 -- should not warn
resTyDot :: T Bool -> Int
resTyDot x = x.sel -- should not warn
From a user's point of view, function `ldiDot` looks very like example `ldi` and
`resTyDot` looks very like `resTy`. But from an /implementation/ point of view
they are very different: both `ldiDot` and `resTyDot` simply emit `HasField`
constraints, and it is those constraints that the implementation must use to
determine incompleteness.
Furthermore, HasField constraints allow to delay the completeness check from
the field access site to a caller, as in test cases TcIncompleteRecSel and T24891:
accessDot :: HasField "sel2" t Int => t -> Int
accessDot x = x.sel2 -- getField @Symbol @"sel2" @t @Int x
solveDot :: Dot -> Int
solveDot = accessDot
We should warn in `solveDot`, but not in `accessDot`.
Here is how we achieve all this in the implementation:
(IRS1) When renaming a record selector in `mkOneRecordSelector`,
we precompute the constructors the selector succeeds on.
That would be `T2` for `sel` because `sel (T2 42)` succeeds,
and `Yes` for `sel2` because `sel2 (Yes 13)` succeeds.
We store this information in the `sel_cons` field of `RecSelId`.
(Remember, the same field may occur in several constructors of the data
type; hence the selector may succeed on more than one constructor.)
We generate warnings for incomplete record selectors in two places:
* Mainly: in GHC.HsToCore.Expr.ds_app (see (IRS2-5) below)
* Plus: in GHC.Tc.Instance.Class.matchHassField (see (IRS6-7) below)
(IRS2) In function `ldi`, we have a record selector application `sel arg`.
This situation is detected `GHC.HsToCore.Expr.ds_app_rec_sel`, when the
record selector is applied to at least one argument. We call out to the
pattern-match checker to determine whether use of the selector is safe,
by calling GHC.HsToCore.Pmc.pmcRecSel, passing the `RecSelId` `sel` as
well as `arg`.
The pattern-match checker reduces the partial-selector-occurrence problem to
a complete-match problem by adding a negative constructor constraint such as
`arg /~ T2` for every constructor in the precomputed `rsi_def . sel_cons` of
`sel`. (Recall that these were exactly the constructors which define a field
`sel`.) `pmcRecSel` then tests
case arg of {}
for completeness. Any incomplete match, such as in the original `urgh`, must
reference a constructor that does not have field `sel`, such as `T1`.
In case of `urgh`, `T1` is indeed the case that we report as inexhaustive.
However, in function `ldi`, we have *both* the result type of
`arg::T a` (boring, but see (IRS3)) as well as Note [Long-distance information]
about `arg` from the ambient match, and the latter lists the constraint
`arg /~ T1`. Consequently, since `arg` is neither `T1` nor `T2` in the
reduced problem, the match is exhaustive and the use of the record selector
safe.
(IRS3) In function `resTy`, the record selector is unsaturated, but the result type
ensures a safe use of the selector.
This situation is also detected in `GHC.HsToCore.Expr.ds_app_rec_sel`.
THe selector is elaborated with its type arguments; we simply match on
desugared Core `sel @Bool :: T Bool -> Int` to learn the result type `T Bool`.
We again call `pmcRecSel`, but this time with a fresh dummy Id `ds::T Bool`.
(IRS4) In case of an unsaturated record selector that is *not* applied to any type
argument after elaboration (e.g. in `urgh2 = sel2 :: Dot -> Int`), we simply
produce a warning about all `sel_cons`; no need to call `pmcRecSel`.
This happens in `ds_app_rec_sel`
Finally, there are two more items addressing -XOverloadedRecordDot:
(IRS5) With -XOverloadedDot, all occurrences of (r.x), such as in `ldiDot` and
`accessDot` above, are warned about as follows. `r.x` is parsed as
`HsGetField` in `HsExpr`; which is then expanded (in `rnExpr`) to a call to
`getField`. For example, consider:
ldiDot No = 0
ldiDot x = x.sel2 -- should not warn
The `d.sel2` in the RHS generates
getField @GHC.Types.Symbol @"sel2" @Dot @Int
($dHasField :: HasField "sel2" Dot Int) x
where
$dHasField = sel2 |> (co :: Dot -> Int ~R# HasField "sel2" Dot Int)
We spot this `getField` application in `GHC.HsToCore.Expr.ds_app_var`,
and treat it exactly like (IRS2) and (IRS3).
Note carefully that doing this in the desugarer allows us to account for the
long-distance info about `x`; even though `sel2` is partial, we don't want
to warn about `x.sel2` in this example.
(IRS6) Finally we have
solveDot :: Dot -> Int
solveDot = accessDot
No field-accesses or selectors in sight! From the RHS we get the constraint
[W] HasField @"sel2" @Dot @Int`
The only time we can generate a warning is when we solve this constraint,
in `GHC.Tc.Instance.Class.matchHasField`, generating a call to the (partial)
selector. We have no hope of exploiting long-distance info here.
(IRS7) BUT, look back at `ldiDot`. Doesn't `matchHasField` /also/ generate a
warning for the `HasField` constraint arising from `x.sel2`? We don't
want that, because the desugarer will catch it: see (IRS5). So we suppress
the (IRS6) warning in the typechecker for a `HasField` constraint that
arises from a record-dot HsGetField occurrence. Happily, this is easy to do
by looking at its `CtOrigin`. Tested in T24891.