Every implication should bump the TcLevel exactly once

Simon recently added an assertion that every implication bumps the TcLevel exactly once. However, this turns out not to be true, and thus caused quite a few failures in a DEBUG compiler. I commented the check out, but we really should investigate and fix any deviations from this plan.

Here is the suspect code in TcSimplify:

    -- Though sensible, this check causes lots of testsuite failures. It is
    -- remaining commented out for now.
    {-
    check_tc_level = do { cur_lvl <- TcS.getTcLevel
                        ; MASSERT2( tclvl == pushTcLevel cur_lvl
                                  , text "Cur lvl =" <+> ppr cur_lvl $$
                                    text "Imp lvl =" <+> ppr tclvl ) }
    -}

The goal is to uncomment this region without introducing failures.

Trac metadata

Trac field	Value
Version	8.5
Type	Task
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

mentioned in issue #15007 (closed)

mentioned in issue #15370 (closed)

changed milestone to %8.6.1

changed weight to 5

added Ttask Trac import labels

Which tests fail?

These do:

   gadt/T12468.run                                             T12468 [stderr mismatch] (normal)
   ghci/scripts/T8353.run                                      T8353 [bad stderr] (ghci)
   ghci/scripts/T10248.run                                     T10248 [bad stderr] (ghci)
   ghci/scripts/T10249.run                                     T10249 [bad stderr] (ghci)
   ghci/should_run/T15007.run                                  T15007 [bad stderr] (ghci)
   module/mod71.run                                            mod71 [stderr mismatch] (normal)
   partial-sigs/should_compile/T12531.run                      T12531 [exit code non-0] (normal)
   partial-sigs/should_fail/T14040a.run                        T14040a [stderr mismatch] (normal)
   quotes/T10384.run                                           T10384 [stderr mismatch] (normal)
   th/T10267.run                                               T10267 [stderr mismatch] (normal)
   th/T10267.run                                               T10267 [stderr mismatch] (ext-interp)
   typecheck/should_compile/holes2.run                         holes2 [exit code non-0] (normal)
   typecheck/should_compile/subsumption_sort_hole_fits.run     subsumption_sort_hole_fits [exit code non-0] (normal)
   typecheck/should_compile/valid_hole_fits_interactions.run   valid_hole_fits_interactions [exit code non-0] (normal)
   typecheck/should_compile/hole_constraints.run               hole_constraints [exit code non-0] (normal)
   typecheck/should_compile/abstract_refinement_hole_fits.run  abstract_refinement_hole_fits [exit code non-0] (normal)
   typecheck/should_compile/holes.run                          holes [exit code non-0] (normal)
   typecheck/should_compile/valid_hole_fits.run                valid_hole_fits [exit code non-0] (normal)
   typecheck/should_compile/free_monad_hole_fits.run           free_monad_hole_fits [exit code non-0] (normal)
   typecheck/should_compile/refinement_hole_fits.run           refinement_hole_fits [exit code non-0] (normal)
   typecheck/should_compile/hole_constraints_nested.run        hole_constraints_nested [exit code non-0] (normal)
   typecheck/should_compile/local_hole_fits.run                local_hole_fits [exit code non-0] (normal)
   typecheck/should_compile/constraint_hole_fits.run           constraint_hole_fits [exit code non-0] (normal)
   typecheck/should_compile/type_in_type_hole_fits.run         type_in_type_hole_fits [exit code non-0] (normal)
   typecheck/should_compile/holes3.run                         holes3 [stderr mismatch] (normal)
   typecheck/should_compile/T9497b.run                         T9497b [exit code non-0] (normal)
   typecheck/should_compile/T9497c.run                         T9497c [exit code non-0] (normal)
   typecheck/should_compile/T9497a.run                         T9497a [exit code non-0] (normal)
   typecheck/should_compile/T13050.run                         T13050 [exit code non-0] (normal)
   typecheck/should_compile/T14590.run                         T14590 [exit code non-0] (normal)
   typecheck/should_compile/T14273.run                         T14273 [exit code non-0] (normal)
   typecheck/should_fail/TcStaticPointersFail02.run            TcStaticPointersFail02 [stderr mismatch] (normal)
   typecheck/should_fail/T9497d.run                            T9497d [stderr mismatch] (normal)
   typecheck/should_fail/T11274.run                            T11274 [stderr mismatch] (normal)
   typecheck/should_fail/T12177.run                            T12177 [stderr mismatch] (normal)

Without the ASSERT in !TcSimplify, no test cases fail.

Tritlo, I see you've added yourself in cc. Yes, I think this is probably a bug in the valid-hole-fits code.

Could you look at it? If you get stuck, or think it's not your code, do get back to me.

Thanks!

Will do!

I've fixed the ones that were due to the hole fits setting the TcLevel incorrectly, and submitted a patch to Phabricator (https://phabricator.haskell.org/D4994). However, T10384, T14040a and TcStaticPointersFail02 still fail, and are unrelated to typed-holes.

Great. I've commented -- please commit after that. (Ben can help if need be.) Then let's look at the remaining 3.

mentioned in commit b202e7a4

changed milestone to %8.8.1

These won't be fixed for in GHC 8.6.

Also, I think #15007 (closed) and #15401 (closed) are other examples.

Trac metadata

Trac field	Value
Related	- → #15007 (closed), #15401 (closed)

changed milestone to %8.10.1

Bumping milestones of low-priority tickets.

mentioned in issue #15809 (closed)

added Pnormal label

changed milestone to %9.0.1

changed milestone to %9.2.1

mentioned in commit b6c3767b

mentioned in commit 7f10d5fc

removed milestone %9.2.1