PmCheck: More type-safe `GrdTree` variants that follow syntactic structure
In !3849 (closed), @simonpj pointed his finger at a few pain points with the untyped GrdTree
s as described in LYG:
- A lot of panics when "undesugaring" the
AnnotatedTree
back to[(Deltas, NonEmpty Delta)]
, corresponding toMatchGroup
structure - Relatedly, possibly failing matches for the GRHSs cases that call out to the MatchGroup version
- Related: !3849 (comment 293235) and !3849 (comment 293372)
Below follows an idea that turned out to be more complicated than necessary. See #18565 (comment 293600) for a better idea.
I think the proper solution here is to encode GrdTree
and AnnotatedTree
as GADTs, indexed by a "skeleton", which is rather like a regular expression describing the shape of the tree:
data GrdTreeSkeleton
= SkelRhs
| SkelBranches !GrdTreeSkeleton -- naming up for debate
| SkelRecordCoveredSet !GrdTreeSkeleton
data GrdTree (s :: GrdTreeSkeleton) where
= Rhs :: RhsInfo -> GrdTree SkelRhs
| Guard :: PmGrd -> GrdTree s -> GrdTree s
| Sequence :: [GrdTree s] -> GrdTree (SkelBranches s) -- Maybe even NonEmpty, then bring back `Empty :: GrdTree (SkelBranches s)`
| InsertCoveredSet :: GrdTree s -> GrdTree (SkelRecordCoveredSet s)
data AnnotatedTree (s :: GrdTreeSkeleton) where
= ARhs :: Deltas -> RhsInfo -> AnnotatedTree SkelRhs
| MayDiverge :: AnnotatedTree s -> AnnotatedTree s
| ASequence :: [AnnotatedTree s] -> AnnotatedTree (SkelBranches s)
| ACoveredSet :: Deltas -> AnnotatedTree s -> AnnotatedTree (SkelRecordCoveredSet s)
Now we can parameterise the whole coverage checking process over the skeleton of the source syntax, which corresponds to guard tree structure:
class LYGable syntax where
type Skeleton syntax :: GrdTreeSkeleton
lower :: ... -> syntax -> DsM (GrdTree (Skeleton syntax))
type family CoverageInfo :: GrdTreeSkeleton -> Type where
CoverageInfo SkelRhs = Deltas
CoverageInfo (SkelBranches s) = [CoverageInfo s] -- Or NonEmpty, see above
CoverageInfo (SkelRecordCoveredSet s) = (Deltas, CoverageInfo s) -- case in point!
-- This is now pretty much mechanical:
extractRhsDeltas :: AnnotatedTree s -> CoverageInfo s
extractRhsDeltas (ARhs deltas _) = deltas
extractRhsDeltas (MayDiverge t) = extractRhsDeltas t
extractRhsDeltas (ASequence ts) = map extractRhsDeltas ts
extractRhsDeltas (ACoveredSet ds t) = (ds, extractRhsDeltas t)
-- The whole pipeline:
lowerYourGuards :: ... -> syntax -> DsM (CoverageInfo (Skeleton syntax))
lowerYourGuards ... syntax = do
grds <- lower ... syntax -- D from the paper
init_deltas <- getPmDeltas
anns <- checkGrdTree deltas grds -- UA from the paper
dsPmWarn ... anns -- R from the paper
return (extractRhsDeltas anns) -- CoverageInfo for Long-distance info
What remains is the mostly trivial definition of LYGable
instances (if we consider the isntance for Pat
as a given):
instance (MatchGroup GhcTc (LHsExpr GhcTc) where
type instance Skeleton (MatchGroup ...) = SkelBranches (Skeleton (Match GhcTc (LHsExpr GhcTc))) -- or inline the defn of `Match`
lower ... mg = Sequence <$> traverse (lower @(Match ...) ...) (mg_alts mg)
instance (Match GhcTc (LHsExpr GhcTc) where
type instance Skeleton (Match ...) = SkelRecordCoveredSet (Skeleton (GRHSs GhcTc (LHsExpr GhcTc))) -- or inline the defn of `GRHSs`
lower ... match = do
pats_grds :: [PmGrd] <- traverse lowerPats (m_pats match)
grhss <- traverse (lower @(GRHs ...) ...) (m_grhss match)
return (foldr Guard (InserCoveredSet grhss) pats_grds)
instance (GRHSs GhcTc (LHsExpr GhcTc) where
type instance Skeleton (GRHSs ...) = SkelBranches (Skeleton (GRHS GhcTc (LHsExpr GhcTc))) -- or inline the defn of `GRHS`
lower ... grhss =
Sequence <$> traverse (lower @(GRHS ...) ...) (grhssGRHSs grhss)
instance (GRHS GhcTc (LHsExpr GhcTc) where
type instance Skeleton (GRHS ...) = SkelRhs
lower ... grhss =
Sequence <$> traverse (lower @(GRHS ...) ...) (grhssGRHSs grhss)
Quite nice, I think, but a bit more complicated.