Skip to content

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 GrdTrees as described in LYG:

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.

Edited by Sebastian Graf
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information