Skip to content

Commit

Permalink
Typecheck: Do more substitution on reduced preds
Browse files Browse the repository at this point in the history
Add a test case that fails to typecheck without the substitution.
It's unclear if this is the most efficient fix -- for example, if the
substitution is just covering for an issue earlier where the
predicates are created -- but this doesn't seem to increase the run
time of the testsuite, so it's probably ok.
  • Loading branch information
quark17 committed Mar 3, 2024
1 parent e8aeb85 commit 2694b42
Show file tree
Hide file tree
Showing 7 changed files with 846 additions and 1 deletion.
8 changes: 7 additions & 1 deletion src/comp/TCMisc.hs
Original file line number Diff line number Diff line change
Expand Up @@ -423,8 +423,14 @@ satMany dvs es rs_accum bs s (p:ps) = do
-- We also accum the bindings to get from "p" to "needed".
-- we keep growing the substitution because anything we
-- have learned we can commit to
--
-- We apply the substitution to the "needed" preds because we
-- encounted an example where they were unsubstituted and that
-- prevented satisfying -- is this apSub just covering for an
-- issue elsewhere (that should not have returned unsubst'd preds)?
--
rtrace ("satMany Right: " ++ ppReadable needed) $
satMany dvs es (needed ++ rs_accum) (bs'++bs) (s' @@ s) ps
satMany dvs es ((apSub s' needed) ++ rs_accum) (bs'++bs) (s' @@ s) ps
([], bs', s') ->
-- If p is satisfied, we "drop" it, but add its binding and
-- substitution.
Expand Down
Loading

0 comments on commit 2694b42

Please sign in to comment.