Type error, but all type error messages are suppressed: GHC 9.6.6, 9.8.2, 9.10.1

changed the description

I've reproduced this on HEAD as well

Diagnosis

-dcore-lint nails the problem in the output of the type checker

*** Core Lint errors : in result of Desugar (before optimization) ***
T25325.hs:13:5: warning:
    Out of scope: $dMonadState_a13S
                    :: MonadState (Buggy g_a13w[ssk:1] m_a13E[sk:3]) m_a13E[sk:3]
                  [LclId]
    In the RHS of $cdemo_a13A :: forall (f :: * -> *) (g :: * -> *)
                                        (m :: * -> *).
                                 (GhcBug f, GhcBug g, MonadState (Buggy (f :+: g) m) m) =>
                                 (:+:) f g (m Int) -> m Int
    In the body of lambda with binder f_a13v :: * -> *
    In the body of lambda with binder g_a13w :: * -> *
    In the body of lambda with binder $dGhcBug_a13x :: GhcBug f_a13v
    In the body of lambda with binder $dGhcBug_a13y :: GhcBug g_a13w
    In the body of lambda with binder m_a13E :: * -> *
    In the body of lambda with binder $dMonadState_a13F :: MonadState
                                                             (Buggy (f_a13v :+: g_a13w) m_a13E)
                                                             m_a13E
    In an occurrence of $dMonadState_a13S :: MonadState
                                               (Buggy g_a13w[ssk:1] m_a13E[sk:3]) m_a13E[sk:3]

The bit of code is this:

$cdemo_a13A
  = \ (@(f_a13v :: * -> *))
      (@(g_a13w :: * -> *))
      ($dGhcBug_a13x :: GhcBug f_a13v)
      ($dGhcBug_a13y :: GhcBug g_a13w)
      (@(m_a13E :: * -> *))
      ($dMonadState_a13F
         :: MonadState (Buggy (f_a13v :+: g_a13w) m_a13E) m_a13E) ->
      let {
        $dMonadState_a13L :: MonadState (Buggy f_a13v m_a13E) m_a13E
        [LclId]
        $dMonadState_a13L
          = $dMonadState_a13S
            `cast` (Sub (Sym (MonadState
                                (Buggy <* -> *>_N co_a144 <m_a13E>_N)_N <m_a13E>_N)_N)
                    :: MonadState (Buggy g_a13w[ssk:1] m_a13E) m_a13E
                       ~R# MonadState (Buggy f_a13v[ssk:1] m_a13E) m_a13E) } in
      let {
        $dGhcBug_a13Q :: GhcBug g_a13w
        [LclId]
        $dGhcBug_a13Q = $dGhcBug_a13y } in
      let {
        $dGhcBug_a13J :: GhcBug f_a13v
        [LclId]
        $dGhcBug_a13J = $dGhcBug_a13x } in
      let {
        $dMonad_a13Z :: Monad m_a13E
        [LclId]
        $dMonad_a13Z
          = $p1MonadState
              @(Buggy (f_a13v :+: g_a13w) m_a13E) @m_a13E $dMonadState_a13F } in
      let {
        $dApplicative_a140 :: Applicative m_a13E
        [LclId]
        $dApplicative_a140 = $p1Monad @m_a13E $dMonad_a13Z } in
      let {
        $dFunctor_a141 :: Functor m_a13E
        [LclId]
        $dFunctor_a141 = $p1Applicative @m_a13E $dApplicative_a140 } in
      let {
        $dFunctor_a14b :: Functor m_a13E
        [LclId]
        $dFunctor_a14b = $dFunctor_a141 } in
      let {
        $dApplicative_a14a :: Applicative m_a13E
        [LclId]
        $dApplicative_a14a = $dApplicative_a140 } in
      let {
        $dMonad_a149 :: Monad m_a13E
        [LclId]
        $dMonad_a149 = $dMonad_a13Z } in
      \ (ds_d14q :: (:+:) f_a13v g_a13w (m_a13E Int)) ->
        case ds_d14q of wild_00 {
          Inl l_az8 ->
            demo @f_a13v $dGhcBug_a13J @m_a13E $dMonadState_a13L l_az8;
          Inr r_az9 ->
            demo @g_a13w $dGhcBug_a13Q @m_a13E $dMonadState_a13S r_az9
        }

and sure enough, $dMonadState_a13S is never bound.

What is wrong? -ddump-tc-trace shows this, near the end:

reportUnsolved (after zonking):
  Free tyvars:
  Bound occs: [f, g, m]
  Tidy env: ([], [])
  Wanted: WC {wc_impl =
                Implic {
                  TcLevel = 1
                  Skolems = (f_a13v[ssk:1] :: * -> *) (g_a13w[ssk:1] :: * -> *)
                  Given-eqs = NoGivenEqs
                  Status = Insoluble
                  Given =
                    $dGhcBug_a13x :: GhcBug f_a13v[ssk:1]
                    $dGhcBug_a13y :: GhcBug g_a13w[ssk:1]
                  Wanted =
                    WC {wc_impl =
                          Implic {
                            TcLevel = 2
                            Skolems =
                            Given-eqs = NoGivenEqs
                            Status = Insoluble
                            Given =
                            Wanted =
                              WC {wc_impl =
                                    Implic {
                                      TcLevel = 3
                                      Skolems = (m_a13E[sk:3] :: * -> *)
                                      Given-eqs = NoGivenEqs
                                      Status = Insoluble
                                      Given =
                                        $dMonadState_a13F :: MonadState
                                                               (Buggy
                                                                  (f_a13v[ssk:1] :+: g_a13w[ssk:1])
                                                                  m_a13E[sk:3])
                                                               m_a13E[sk:3]
                                      Wanted =
                                        WC {wc_simple =
                                              [W] hole{co_a144} {0}:: f_a13v[ssk:1]
                                                                      GHC.Prim.~# g_a13w[ssk:1] (CNonCanonical)
                                              [W] hole{co_a147} {0;{{co_a144}}}:: g_a13w[ssk:1]
                                                                                  GHC.Prim.~# (g_a13w[ssk:1]
                                                                                               :+: g_a13w[ssk:1]) (CIrredCan{cteInsolubleOccurs})
                                              [W] hole{co_a148} {0;{{co_a144}}}:: g_a13w[ssk:1]
                                                                                  GHC.Prim.~# (g_a13w[ssk:1]
                                                                                               :+: g_a13w[ssk:1]) (CIrredCan{cteInsolubleOccurs})
                                              [W] hole{co_a14e} {0;{{co_a144}}}:: g_a13w[ssk:1]
                                                                                  GHC.Prim.~# (g_a13w[ssk:1]
                                                                                               :+: g_a13w[ssk:1]) (CIrredCan{cteInsolubleOccurs})
                                              [W] $dMonadState_a13S {0}:: MonadState
                                                                            (Buggy
                                                                               g_a13w[ssk:1]
                                                                               m_a13E[sk:3])
                                                                            m_a13E[sk:3] (CDictCan)}
                                      Binds = EvBindsVar<a13V>
                                      the type signature for:
                                        demo :: forall (m :: * -> *).
                                                MonadState
                                                  (Buggy (f_a13v[ssk:1] :+: g_a13w[ssk:1]) m) m =>
                                                (:+:) f_a13v[ssk:1] g_a13w[ssk:1] (m Int)
                                                -> m Int }}
                            Binds = EvBindsVar<a13W>
                            the instance declaration }}
                  Binds = EvBindsVar<a13z>
                  the instance declaration }}

Whoa! Five unsolved constraints! No wonder we don't bind that $dMonadState_a13S: it's the evidence variable for an unsolved constraint. So the error reporting machinery is failing to report an error, and the typechecker appears to complete with no errors.

Why does the error reporting machinery fail to report an error? Because:

If there is any definitely-insoluble constraint, we suppress reporting of all others.
Those three equality constraints co_a147, co_a148, co_a14e are all definitely insoluble, with an occurs check.
So we suppress reporting errors for co_a144 and $dMonadState_a13S
But alas we also suppress reporting any constraints that have unsolved rewriters; see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint
So we don't report those three either, because they have been rewritten with co_a144.

That is what is happening. Next: need to think about how to fix it. But we have a smoking gun.

changed title from lookupIdSubst Panic: GHC 9.6.6, 9.8.2, 9.10.1 to Type error, but all type error messages are suppressed: GHC 9.6.6, 9.8.2, 9.10.1

mentioned in commit eae1410c

mentioned in merge request !13371 (closed)

There is a fix in !13371 (closed)

Thank you @Rinzal for such a great repro case.

mentioned in commit 67eb3db8

added Tbug constraint solver error messages typechecker labels and removed needs triage label

added Pnormal label

assigned to @simonpj

mentioned in commit 47428444

closed with commit 083703a1

mentioned in commit 083703a1

Fixed by

commit 083703a12cd34369e7ed2f0efc4a5baee47aedab
Author: Simon Peyton Jones <simon.peytonjones@gmail.com>
Date:   Sun Oct 6 09:33:39 2024 +0100

    Consider Wanteds with rewriters as insoluble
    
    This MR fixes #25325
    
    See GHC.Tc.Types.Constraint, Note [Insoluble Wanteds], especially (IW2)
    
    There is a small change in the error message for T14172, but it looks
    entirely acceptable to me.

 compiler/GHC/Tc/Types/Constraint.hs                 | 82 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++-----------------------
 testsuite/tests/polykinds/T14172.stderr             | 21 ++++++++++-----------
 testsuite/tests/typecheck/should_fail/T25325.hs     | 14 ++++++++++++++
 testsuite/tests/typecheck/should_fail/T25325.stderr | 15 +++++++++++++++
 testsuite/tests/typecheck/should_fail/all.T         |  1 +
 5 files changed, 99 insertions(+), 34 deletions(-)

mentioned in commit abd0d124

mentioned in commit 7326051e

mentioned in commit a6fb8fc7

mentioned in commit cfc9f465

Type error, but all type error messages are suppressed: GHC 9.6.6, 9.8.2, 9.10.1

Summary

Steps to reproduce

Error messages

Expected behavior

Environment

Related issue

Child items ...

Activity

Diagnosis