
   0 | module Core.Coverage
   1 | 
   2 | import Core.Case.CaseTree
   3 | import Core.Case.Util
   4 | import Core.Context.Log
   5 | import Core.Env
   6 | import Core.Normalise
   7 | import Core.Value
   8 | 
   9 | import Data.Maybe
  10 | import Data.String
  11 | 
  12 | import Libraries.Data.NameMap
  13 | import Libraries.Data.NatSet
  14 | import Libraries.Data.String.Extra
  15 | import Libraries.Data.List.SizeOf
  16 | import Libraries.Text.PrettyPrint.Prettyprinter
  17 | 
  18 | %default covering
  19 | 
  20 | -- Return whether any of the name matches conflict
  21 | conflictMatch : List (Name, Term vars) -> Bool
  22 | conflictMatch [] = False
  23 | conflictMatch ((x, tm) :: ms) = conflictArgs x tm ms || conflictMatch ms
  24 |   where
  25 |     data ClashResult = Distinct | Same | Incomparable
  26 | 
  27 |     clash : Term vars -> Term vars -> ClashResult
  28 |     clash (Ref _ (DataCon t _) _) (Ref _ (DataCon t' _) _)
  29 |         = if t /= t' then Distinct else Same
  30 |     clash (Ref _ (TyCon _) n) (Ref _ (TyCon _) n')
  31 |         = if n /= n' then Distinct else Same
  32 |     clash (PrimVal _ c) (PrimVal _ c') = if c /= c' then Distinct else Same
  33 |     clash (Ref _ t _) (PrimVal {}) = if isJust (isCon t) then Distinct else Incomparable
  34 |     clash (PrimVal {}) (Ref _ t _) = if isJust (isCon t) then Distinct else Incomparable
  35 |     clash (Ref _ t _) (TType {})   = if isJust (isCon t) then Distinct else Incomparable
  36 |     clash (TType {}) (Ref _ t _)   = if isJust (isCon t) then Distinct else Incomparable
  37 |     clash (TType {}) (PrimVal {})  = Distinct
  38 |     clash (PrimVal {}) (TType {})  = Distinct
  39 |     clash _ _ = Incomparable
  40 | 
  41 |     findN : Nat -> Term vars -> Bool
  42 |     findN i (Local _ _ i' _) = i == i'
  43 |     findN i tm
  44 |         = let (Ref _ (DataCon {}) _, args) = getFnArgs tm
  45 |                    | _ => False in
  46 |               any (findN i) args
  47 | 
  48 |     -- Assuming in normal form. Look for: mismatched constructors, or
  49 |     -- a name appearing strong rigid in the other term
  50 |     conflictTm : Term vars -> Term vars -> Bool
  51 |     conflictTm (Local _ _ i _) tm
  52 |         = let (Ref _ (DataCon {}) _, args) = getFnArgs tm
  53 |                    | _ => False in
  54 |               any (findN i) args
  55 |     conflictTm tm (Local _ _ i _)
  56 |         = let (Ref _ (DataCon {}) _, args) = getFnArgs tm
  57 |                    | _ => False in
  58 |               any (findN i) args
  59 |     conflictTm tm tm'
  60 |         = let (f, args) = getFnArgs tm
  61 |               (f', args') = getFnArgs tm' in
  62 |           case clash f f' of
  63 |             Distinct => True
  64 |             Incomparable => False
  65 |             Same => (any (uncurry conflictTm) (zip args args'))
  66 | 
  67 |     conflictArgs : Name -> Term vars -> List (Name, Term vars) -> Bool
  68 |     conflictArgs n tm [] = False
  69 |     conflictArgs n tm ((x, tm') :: ms)
  70 |         = (n == x && conflictTm tm tm') || conflictArgs n tm ms
  71 | 
  72 | -- Return whether any part of the type conflicts in such a way that they
  73 | -- can't possibly be equal (i.e. mismatched constructor)
  74 | conflict : {vars : _} ->
  75 |            {auto c : Ref Ctxt Defs} ->
  76 |            Defs -> Env Term vars -> NF vars -> Name -> Core Bool
  77 | conflict defs env nfty n
  78 |     = do Just gdef <- lookupCtxtExact n (gamma defs)
  79 |               | Nothing => pure False
  80 |          case (definition gdef, type gdef) of
  81 |               (DCon t arity _, dty)
  82 |                   => do Nothing <- conflictNF 0 nfty !(nf defs Env.empty dty)
  83 |                             | Just ms => pure $ conflictMatch ms
  84 |                         pure True
  85 |               _ => pure False
  86 |   where
  87 |     mutual
  88 |       conflictArgs : Int -> List (Closure vars) -> List ClosedClosure ->
  89 |                      Core (Maybe (List (Name, Term vars)))
  90 |       conflictArgs _ [] [] = pure (Just [])
  91 |       conflictArgs i (c :: cs) (c' :: cs')
  92 |           = do cnf <- evalClosure defs c
  93 |                cnf' <- evalClosure defs c'
  94 |                Just ms <- conflictNF i cnf cnf'
  95 |                     | Nothing => pure Nothing
  96 |                Just ms' <- conflictArgs i cs cs'
  97 |                     | Nothing => pure Nothing
  98 |                pure (Just (ms ++ ms'))
  99 |       conflictArgs _ _ _ = pure (Just [])
 100 | 
 101 |       -- If the constructor type (the ClosedNF) matches the variable type,
 102 |       -- then there may be a way to construct it, so return the matches in
 103 |       -- the indices.
 104 |       -- If any of those matches clash, the constructor is not valid
 105 |       -- e.g, Eq x x matches Eq Z (S Z), with x = Z and x = S Z
 106 |       -- conflictNF returns the list of matches, for checking
 107 |       conflictNF : Int -> NF vars -> ClosedNF ->
 108 |                    Core (Maybe (List (Name, Term vars)))
 109 |       conflictNF i t (NBind fc x b sc)
 110 |           -- invent a fresh name, in case a user has bound the same name
 111 |           -- twice somehow both references appear in the result it's unlikely
 112 |           -- put possible
 113 |           = let x' = MN (show x) i in
 114 |                 conflictNF (i + 1) t
 115 |                        !(sc defs (toClosure defaultOpts Env.empty (Ref fc Bound x')))
 116 |       conflictNF i nf (NApp _ (NRef Bound n) [])
 117 |           = pure (Just [(n, !(quote defs env nf))])
 118 |       conflictNF i (NDCon _ n t a args) (NDCon _ n' t' a' args')
 119 |           = if t == t'
 120 |                then conflictArgs i (map snd args) (map snd args')
 121 |                else pure Nothing
 122 |       conflictNF i (NTCon _ n a args) (NTCon _ n' a' args')
 123 |           = if n == n'
 124 |                then conflictArgs i (map snd args) (map snd args')
 125 |                else pure Nothing
 126 |       conflictNF i (NPrimVal _ c) (NPrimVal _ c')
 127 |           = if c == c'
 128 |                then pure (Just [])
 129 |                else pure Nothing
 130 |       conflictNF _ _ _ = pure (Just [])
 131 | 
 132 | -- Return whether the given type is definitely empty (due to there being
 133 | -- no constructors which can possibly match it.)
 134 | export
 135 | isEmpty : {vars : _} ->
 136 |           {auto c : Ref Ctxt Defs} ->
 137 |           Defs -> Env Term vars -> NF vars -> Core Bool
 138 | isEmpty defs env (NTCon fc n a args)
 139 |   = do Just nty <- lookupDefExact n (gamma defs)
 140 |          | _ => pure False
 141 |        case nty of
 142 |             TCon _ _ _ flags _ Nothing _ => pure False
 143 |             TCon _ _ _ flags _ (Just cons) _
 144 |                  => if not (external flags)
 145 |                        then allM (conflict defs env (NTCon fc n a args)) cons
 146 |                        else pure False
 147 |             _ => pure False
 148 | isEmpty defs env _ = pure False
 149 | 
 150 | altMatch : CaseAlt vars -> CaseAlt vars -> Bool
 151 | altMatch _ (DefaultCase _) = True
 152 | altMatch (DelayCase _ _ t) (DelayCase _ _ t') = True
 153 | altMatch (ConCase n t _ _) (ConCase n' t' _ _) = t == t'
 154 | altMatch (ConstCase c _) (ConstCase c' _) = c == c'
 155 | altMatch _ _ = False
 156 | 
 157 | -- Given a type and a list of case alternatives, return the
 158 | -- well-typed alternatives which were *not* in the list
 159 | getMissingAlts : {auto c : Ref Ctxt Defs} ->
 160 |                  {vars : _} ->
 161 |                  FC -> Defs -> NF vars -> List (CaseAlt vars) ->
 162 |                  Core (List (CaseAlt vars))
 163 | -- If it's a primitive other than WorldVal, there's too many to reasonably
 164 | -- check, so require a catch all
 165 | getMissingAlts fc defs (NPrimVal _ $ PrT WorldType) alts
 166 |     = if isNil alts
 167 |          then pure [DefaultCase (Unmatched "Coverage check")]
 168 |          else pure []
 169 | getMissingAlts fc defs (NPrimVal _ c) alts
 170 |   = do log "coverage.missing" 50 $ "Looking for missing alts at type " ++ show c
 171 |        if any isDefault alts
 172 |          then do log "coverage.missing" 20 "Found default"
 173 |                  pure []
 174 |          else pure [DefaultCase (Unmatched "Coverage check")]
 175 | -- Similarly for types
 176 | getMissingAlts fc defs (NType {}) alts
 177 |     = do log "coverage.missing" 50 "Looking for missing alts at type Type"
 178 |          if any isDefault alts
 179 |            then do log "coverage.missing" 20 "Found default"
 180 |                    pure []
 181 |            else pure [DefaultCase (Unmatched "Coverage check")]
 182 | getMissingAlts fc defs nfty alts
 183 |     = do log "coverage.missing" 50 $ "Getting constructors for: " ++ show nfty
 184 |          logNF "coverage.missing" 20 "Getting constructors for" (mkEnv fc _) nfty
 185 |          allCons <- getCons defs nfty
 186 |          pure (filter (noneOf alts)
 187 |                  (map (mkAlt fc (Unmatched "Coverage check")) allCons))
 188 |   where
 189 |     -- Return whether the alternative c matches none of the given cases in alts
 190 |     noneOf : List (CaseAlt vars) -> CaseAlt vars -> Bool
 191 |     noneOf alts c = not $ any (altMatch c) alts
 192 | 
 193 | -- Mapping of variable to constructor tag already matched for it
 194 | KnownVars : Scope -> Type -> Type
 195 | KnownVars vars a = List (Var vars, a)
 196 | 
 197 | showK : {ns : _} ->
 198 |         Show a => KnownVars ns a -> String
 199 | showK {a} xs = show (map aString xs)
 200 |   where
 201 |     aString : {vars : Scope} ->
 202 |               (Var vars, a) -> (Name, a)
 203 |     aString (MkVar v, t) = (nameAt v, t)
 204 | 
 205 | -- TODO re-use `Thinnable`
 206 | weakenNs : SizeOf args -> KnownVars vars a -> KnownVars (args ++ vars) a
 207 | weakenNs args [] = []
 208 | weakenNs args ((v, t) :: xs)
 209 |   = (weakenNs args v, t) :: weakenNs args xs
 210 | 
 211 | findTag : {idx, vars : _} ->
 212 |           (0 p : IsVar n idx vars) -> KnownVars vars a -> Maybe a
 213 | findTag v [] = Nothing
 214 | findTag v ((v', t) :: xs)
 215 |     = if MkVar v == v'
 216 |          then Just t
 217 |          else findTag v xs
 218 | 
 219 | addNot : {idx, vars : _} ->
 220 |          (0 p : IsVar n idx vars) -> Int -> KnownVars vars (List Int) ->
 221 |          KnownVars vars (List Int)
 222 | addNot v t [] = [(MkVar v, [t])]
 223 | addNot v t ((v', ts) :: xs)
 224 |     = if MkVar v == v'
 225 |          then ((v', t :: ts) :: xs)
 226 |          else ((v', ts) :: addNot v t xs)
 227 | 
 228 | tagIsNot : List Int -> CaseAlt vars -> Bool
 229 | tagIsNot ts (ConCase _ t' _ _) = not (t' `elem` ts)
 230 | tagIsNot ts (ConstCase {}) = True
 231 | tagIsNot ts (DelayCase {}) = True
 232 | tagIsNot ts (DefaultCase _) = False
 233 | 
 234 | -- Replace a default case with explicit branches for the constructors.
 235 | -- This is easier than checking whether a default is needed when traversing
 236 | -- the tree (just one constructor lookup up front).
 237 | replaceDefaults : {auto c : Ref Ctxt Defs} ->
 238 |                   {vars : _} ->
 239 |                   FC -> Defs -> NF vars -> List (CaseAlt vars) ->
 240 |                   Core (List (CaseAlt vars))
 241 | -- Leave it alone if it's a primitive type though, since we need the catch
 242 | -- all case there
 243 | replaceDefaults fc defs (NPrimVal {}) cs = pure cs
 244 | replaceDefaults fc defs (NType {}) cs = pure cs
 245 | replaceDefaults fc defs nfty cs
 246 |     = do cs' <- traverse rep cs
 247 |          pure (dropRep (concat cs'))
 248 |   where
 249 |     rep : CaseAlt vars -> Core (List (CaseAlt vars))
 250 |     rep (DefaultCase sc)
 251 |         = do allCons <- getCons defs nfty
 252 |              pure (map (mkAlt fc sc) allCons)
 253 |     rep c = pure [c]
 254 | 
 255 |     dropRep : List (CaseAlt vars) -> List (CaseAlt vars)
 256 |     dropRep [] = []
 257 |     dropRep (c@(ConCase n t args sc) :: rest)
 258 |           -- assumption is that there's no defaultcase in 'rest' because
 259 |           -- we've just removed it
 260 |         = c :: dropRep (filter (not . tagIs t) rest)
 261 |     dropRep (c :: rest) = c :: dropRep rest
 262 | 
 263 | -- Traverse a case tree and refine the arguments while matching, so that
 264 | -- when we reach a leaf we know what patterns were used to get there,
 265 | -- and return those patterns.
 266 | -- The returned patterns are those arising from the *missing* cases
 267 | buildArgs : {auto c : Ref Ctxt Defs} ->
 268 |             {vars : _} ->
 269 |             FC -> Defs ->
 270 |             KnownVars vars Int -> -- Things which have definitely match
 271 |             KnownVars vars (List Int) -> -- Things an argument *can't* be
 272 |                                     -- (because a previous case matches)
 273 |             List ClosedTerm -> -- ^ arguments, with explicit names
 274 |             CaseTree vars -> Core (List (List ClosedTerm))
 275 | buildArgs fc defs known not ps cs@(Case {name = var} idx el ty altsIn)
 276 |   -- If we've already matched on 'el' in this branch, restrict the alternatives
 277 |   -- to the tag we already know. Otherwise, add missing cases and filter out
 278 |   -- the ones it can't possibly be (the 'not') because a previous case
 279 |   -- has matched.
 280 |     = do let fenv = mkEnv fc _
 281 |          nfty <- nf defs fenv ty
 282 |          alts <- replaceDefaults fc defs nfty altsIn
 283 |          let alts' = alts ++ !(getMissingAlts fc defs nfty alts)
 284 |          let altsK = maybe alts' (\t => filter (tagIs t) alts')
 285 |                               (findTag el known)
 286 |          let altsN = maybe altsK (\ts => filter (tagIsNot ts) altsK)
 287 |                               (findTag el not)
 288 |          buildArgsAlt not altsN
 289 |   where
 290 |     buildArgAlt : KnownVars vars (List Int) ->
 291 |                   CaseAlt vars -> Core (List (List ClosedTerm))
 292 |     buildArgAlt not' (ConCase n t args sc)
 293 |         = do let l = mkSizeOf args
 294 |              let con = Ref fc (DataCon t (size l)) n
 295 |              let ps' = map (substName var
 296 |                              (apply fc
 297 |                                     con (map (Ref fc Bound) args))) ps
 298 |              buildArgs fc defs (weakenNs l ((MkVar el, t) :: known))
 299 |                                (weakenNs l not') ps' sc
 300 |     buildArgAlt not' (DelayCase t a sc)
 301 |         = let l = mkSizeOf [t, a]
 302 |               ps' = map (substName var (TDelay fc LUnknown
 303 |                                              (Ref fc Bound t)
 304 |                                              (Ref fc Bound a))) ps in
 305 |               buildArgs fc defs (weakenNs l known) (weakenNs l not')
 306 |                                 ps' sc
 307 |     buildArgAlt not' (ConstCase c sc)
 308 |         = do let ps' = map (substName var (PrimVal fc c)) ps
 309 |              buildArgs fc defs known not' ps' sc
 310 |     buildArgAlt not' (DefaultCase sc)
 311 |         = buildArgs fc defs known not' ps sc
 312 | 
 313 |     buildArgsAlt : KnownVars vars (List Int) -> List (CaseAlt vars) ->
 314 |                    Core (List (List ClosedTerm))
 315 |     buildArgsAlt not' [] = pure []
 316 |     buildArgsAlt not' (c@(ConCase _ t _ _) :: cs)
 317 |         = pure $ !(buildArgAlt not' c) ++
 318 |                  !(buildArgsAlt (addNot el t not') cs)
 319 |     buildArgsAlt not' (c :: cs)
 320 |         = pure $ !(buildArgAlt not' c) ++ !(buildArgsAlt not' cs)
 321 | 
 322 | buildArgs fc defs known not ps (STerm _ vs)
 323 |     = pure [] -- matched, so return nothing
 324 | buildArgs fc defs known not ps (Unmatched msg)
 325 |     = pure [ps] -- unmatched, so return it
 326 | buildArgs fc defs known not ps Impossible
 327 |     = pure [] -- not a possible match, so return nothing
 328 | 
 329 | -- Traverse a case tree and return pattern clauses which are not
 330 | -- matched. These might still be invalid patterns, or patterns which are covered
 331 | -- elsewhere (turning up due to overlapping clauses) so the results should be
 332 | -- checked
 333 | export
 334 | getMissing : {vars : _} ->
 335 |              {auto c : Ref Ctxt Defs} ->
 336 |              FC -> Name -> ClosedTerm ->
 337 |              CaseTree vars ->
 338 |              Core (List ClosedTerm)
 339 | getMissing fc n ty ctree
 340 |    = do defs <- get Ctxt
 341 |         let psIn = map (Ref fc Bound) vars
 342 |         pats <- buildArgs fc defs [] [] psIn ctree
 343 |         pats <- for pats $ trimArgs defs [<] !(nf defs Env.empty ty)
 344 |         unless (null pats) $
 345 |           logC "coverage.missing" 20 $ map unlines $
 346 |             for pats $ map show . traverse toFullNames
 347 |         pure (map (apply fc (Ref fc Func n)) pats)
 348 |   where
 349 |     trimArgs : Defs ->
 350 |                SnocList ClosedTerm -> ClosedNF ->
 351 |                List ClosedTerm -> Core (List ClosedTerm)
 352 |     trimArgs defs acc (NBind _ n (Pi {}) sc) (x :: xs)
 353 |         = trimArgs defs (acc :< x) !(sc defs $ toClosure defaultOpts Env.empty x) xs
 354 |     trimArgs _ acc _ _ = pure $ toList acc
 355 | 
 356 | -- For the given name, get the names it refers to which are not themselves
 357 | -- covering.
 358 | -- Also need to go recursively into case blocks, since we only calculate
 359 | -- references for them at the top level clause
 360 | export
 361 | getNonCoveringRefs : {auto c : Ref Ctxt Defs} ->
 362 |                      FC -> Name -> Core (List Name)
 363 | getNonCoveringRefs fc n
 364 |    = do defs <- get Ctxt
 365 |         Just d <- lookupCtxtExact n (gamma defs)
 366 |            | Nothing => undefinedName fc n
 367 |         let ds = mapMaybe noAssert (toList (refersTo d))
 368 |         let cases = filter isCase !(traverse toFullNames ds)
 369 | 
 370 |         -- Case blocks aren't recursive, so we're safe!
 371 |         cbad <- traverse (getNonCoveringRefs fc) cases
 372 |         topbad <- filterM (notCovering defs) ds
 373 |         pure (topbad ++ concat cbad)
 374 |   where
 375 |     isCase : Name -> Bool
 376 |     isCase (NS _ n) = isCase n
 377 |     isCase (CaseBlock {}) = True
 378 |     isCase _ = False
 379 | 
 380 |     noAssert : (Name, Bool) -> Maybe Name
 381 |     noAssert (n, True) = Nothing
 382 |     noAssert (n, False) = Just n
 383 | 
 384 |     notCovering : Defs -> Name -> Core Bool
 385 |     notCovering defs n
 386 |         = case !(lookupCtxtExact n (gamma defs)) of
 387 |                Just def => case isCovering (totality def) of
 388 |                                 IsCovering => pure False
 389 |                                 _ => pure True
 390 |                _ => pure False
 391 | 
 392 | -- Does the second term match against the first?
 393 | -- 'Erased' matches against anything, we assume that's a Rig0 argument that
 394 | -- we don't care about
 395 | match : Term vs -> Term vs -> Bool
 396 | match (Local _ _ i _) _ = True
 397 | match (Ref _ Bound n) _ = True
 398 | match (Ref _ _ n) (Ref _ _ n') = n == n'
 399 | match (App _ f a) (App _ f' a') = match f f' && match a a'
 400 | match (As _ _ _ p) (As _ _ _ p') = match p p'
 401 | match (As _ _ _ p) p' = match p p'
 402 | match (TDelayed _ _ t) (TDelayed _ _ t') = match t t'
 403 | match (TDelay _ _ _ t) (TDelay _ _ _ t') = match t t'
 404 | match (TForce _ _ t) (TForce _ _ t') = match t t'
 405 | match (PrimVal _ c) (PrimVal _ c') = c == c'
 406 | match (Erased _ (Dotted t)) u = match t u
 407 | match t (Erased _ (Dotted u)) = match t u
 408 | match (Erased {}) _ = True
 409 | match _ (Erased {}) = True
 410 | match (TType {}) (TType {}) = True
 411 | match _ _ = False
 412 | 
 413 | -- Erase according to argument position
 414 | eraseApps : {auto c : Ref Ctxt Defs} ->
 415 |             Term vs -> Core (Term vs)
 416 | eraseApps {vs} tm
 417 |     = case getFnArgs tm of
 418 |            (Ref fc Bound n, args) =>
 419 |                 do args' <- traverse eraseApps args
 420 |                    pure (apply fc (Ref fc Bound n) args')
 421 |            (Ref fc nt n, args) =>
 422 |                 do defs <- get Ctxt
 423 |                    mgdef <- lookupCtxtExact n (gamma defs)
 424 |                    let eargs = maybe NatSet.empty eraseArgs mgdef
 425 |                    args' <- traverse eraseApps (NatSet.overwrite (Erased fc Placeholder) eargs args)
 426 |                    pure (apply fc (Ref fc nt n) args')
 427 |            (tm, args) =>
 428 |                 do args' <- traverse eraseApps args
 429 |                    pure (apply (getLoc tm) tm args')
 430 | 
 431 | -- if tm would be matched by trylhs, then it's not an impossible case
 432 | -- because we've already got it. Ignore anything in erased position.
 433 | clauseMatches : {vars : _} ->
 434 |                 {auto c : Ref Ctxt Defs} ->
 435 |                 (erase : Bool) -> Env Term vars -> Term vars ->
 436 |                 ClosedTerm -> Core Bool
 437 | clauseMatches erase env tm trylhs
 438 |     = do let lhs = close (getLoc tm) "cov" env tm
 439 |          lhs <- if erase
 440 |                    then eraseApps lhs
 441 |                    else pure lhs
 442 |          pure $ match !(toResolvedNames lhs) !(toResolvedNames trylhs)
 443 | 
 444 | export
 445 | checkMatched : {auto c : Ref Ctxt Defs} ->
 446 |                (erase : Bool) -> List Clause -> ClosedTerm -> Core (Maybe ClosedTerm)
 447 | checkMatched erase cs ulhs
 448 |     = do logTerm "coverage" 5 "Checking coverage for" ulhs
 449 |          logC "coverage" 10 $ pure $ "(raw term: " ++ show !(toFullNames ulhs) ++ ")"
 450 |          ulhs <- if erase
 451 |                     then do ulhs <- eraseApps ulhs
 452 |                             logTerm "coverage" 5 "Erased to" ulhs
 453 |                             pure ulhs
 454 |                     else pure ulhs
 455 |          logC "coverage" 5 $ do
 456 |             cs <- traverse toFullNames cs
 457 |             pure $ "Against clauses:\n" ++
 458 |                    (show $ indent 2 $ vcat $ map (pretty . show) cs)
 459 |          tryClauses cs ulhs
 460 |   where
 461 |     tryClauses : List Clause -> ClosedTerm -> Core (Maybe ClosedTerm)
 462 |     tryClauses [] ulhs
 463 |         = do logTermNF "coverage" 10 "Nothing matches" Env.empty ulhs
 464 |              pure $ Just ulhs
 465 |     tryClauses (MkClause env lhs _ :: cs) ulhs
 466 |         = if !(clauseMatches erase env lhs ulhs)
 467 |              then do logTermNF "coverage" 10 "Yes" env lhs
 468 |                      pure Nothing -- something matches, discared it
 469 |              else do logTermNF "coverage" 10 "No match" env lhs
 470 |                      tryClauses cs ulhs
 471 |