GitLab

Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC

Commits:

d6fac0a4

by Simon Peyton Jones at 2025-08-08T11:37:43+01:00

More wibbles

Need to remove the unification-count stuff entirely
and do more tidying up -- this commit is mainly for CI

4 changed files:

compiler/GHC/Tc/Solver/FunDeps.hs
compiler/GHC/Tc/Solver/Monad.hs
compiler/GHC/Tc/Solver/Solve.hs
compiler/GHC/Tc/Utils/Unify.hs

Changes:

compiler/GHC/Tc/Solver/FunDeps.hs

@@ -323,9 +323,11 @@ doDictFunDepImprovementLocal dict_ct@(DictCt { di_cls = cls, di_ev = work_ev })
    = Stage $
      do { inerts <- getInertCans
 +       ; traceTcS "doDictFunDepImprovementLocal {" (ppr dict_ct)
         ; imp <- solveFunDeps $
                  foldM do_interaction emptyCts $
                  findDictsByClass (inert_dicts inerts) cls
 +       ; traceTcS "doDictFunDepImprovementLocal }" (text "imp =" <+> ppr imp)
         ; if imp then startAgainWith (CDictCan dict_ct)
                  else continueWith () }
@@ -344,15 +346,13 @@ doDictFunDepImprovementLocal dict_ct@(DictCt { di_cls = cls, di_ev = work_ev })
        = return new_eqs1
        | otherwise
 -      = do { traceTcS "doLocalFunDepImprovement" $
 -             vcat [ ppr work_ev
 -                  , pprCtLoc work_loc, ppr (isGivenLoc work_loc)
 -                  , pprCtLoc inert_loc, ppr (isGivenLoc inert_loc)
 -                  , pprCtLoc deriv_loc, ppr (isGivenLoc deriv_loc) ]
+-
 -           ; new_eqs2 <- unifyFunDepWanteds_new work_ev $
 +      = do { new_eqs2 <- unifyFunDepWanteds_new work_ev $
                           improveFromAnother (deriv_loc, inert_rewriters)
                                              inert_pred work_pred
++
 +           ; traceTcS "doDictFunDepImprovementLocal item" $
 +             vcat [ ppr work_ev, ppr new_eqs2 ]
++
             ; return (new_eqs1 `unionBags` new_eqs2) }
        where
          inert_pred  = ctEvPred inert_ev
@@ -374,10 +374,12 @@ doDictFunDepImprovementTop dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys =
    = Stage $
      do { inst_envs <- getInstEnvs
 +       ; traceTcS "doDictFunDepImprovementTop {" (ppr dict_ct)
         ; let eqns :: [FunDepEqn (CtLoc, RewriterSet)]
               eqns = improveFromInstEnv inst_envs mk_ct_loc cls xis
         ; imp <- solveFunDeps $
                  unifyFunDepWanteds_new ev eqns
 +       ; traceTcS "doDictFunDepImprovementTop }" (text "imp =" <+> ppr imp)
         ; if imp then startAgainWith (CDictCan dict_ct)
                  else continueWith () }

compiler/GHC/Tc/Solver/Monad.hs

@@ -44,7 +44,7 @@ module GHC.Tc.Solver.Monad (
      panicTcS, traceTcS, tryEarlyAbortTcS,
      traceFireTcS, bumpStepCountTcS, csTraceTcS,
      wrapErrTcS, wrapWarnTcS,
 -    getUnificationFlag,
 +    getUnificationFlag, traceUnificationFlag,
      -- Evidence creation and transformation
      MaybeNew(..), freshGoals, isFresh, getEvExpr,
@@ -454,7 +454,8 @@ kickOutAfterUnification :: [TcTyVar] -> TcS ()
  kickOutAfterUnification tv_list
    = case nonEmpty tv_list of
        Nothing  -> return ()
 -      Just tvs -> setUnificationFlagTo min_tv_lvl
 +      Just tvs -> do { traceTcS "kickOutAfterUnification" (ppr min_tv_lvl $$ ppr tv_list)
 +                     ; setUnificationFlagTo min_tv_lvl }
           where
             min_tv_lvl = foldr1 minTcLevel (NE.map tcTyVarLevel tvs)
@@ -1833,16 +1834,31 @@ reportUnifications (TcS thing_inside)
               | ambient_lvl `deeperThanOrSame` unif_lvl
               -> -- Some useful unifications took place
                  do { mb_outer_lvl <- TcM.readTcRef outer_ul_var
 +                   ; TcM.traceTc "reportUnifications" $
 +                     vcat [ text "ambient =" <+> ppr ambient_lvl
 +                          , text "unif_lvl =" <+> ppr unif_lvl
 +                          , text "mb_outer =" <+> ppr mb_outer_lvl ]
                     ; case mb_outer_lvl of
 -                       Just outer_unif_lvl | outer_unif_lvl `strictlyDeeperThan` unif_lvl
 -                         -> -- Update, because outer_unif_lv > unif_lvl
 +                       Just outer_unif_lvl | unif_lvl `deeperThanOrSame` outer_unif_lvl
 +                         -> -- No need to update: outer_unif_lvl is already shallower
 +                            return ()
 +                       _ -> -- Update the outer level
                              TcM.writeTcRef outer_ul_var (Just unif_lvl)
 -                       _ -> return ()
                     ; return (True, res) }
             _  -> -- No useful unifications
                   return (False, res) }
 +traceUnificationFlag :: String -> TcS ()
 +traceUnificationFlag str
 +  = TcS $ \env ->
 +    do { ambient_lvl <- TcM.getTcLevel
 +       ; mb_lvl <- TcM.readTcRef (tcs_unif_lvl env)
 +       ; TcM.traceTc ("trace-uni-flag: " ++ str) $
 +         vcat [ text "ambient =" <+> ppr ambient_lvl
 +              , text "mb_lvl =" <+> ppr mb_lvl ]
 +       ; return () }
++
  getUnificationFlag :: TcS Bool
  -- We are at ambient level i
  -- If the unification flag = Just i, reset it to Nothing and return True
@@ -1872,8 +1888,11 @@ setUnificationFlagTo lvl
         ; mb_lvl <- TcM.readTcRef ref
         ; case mb_lvl of
             Just unif_lvl | lvl `deeperThanOrSame` unif_lvl
 -                         -> return ()
 -           _ -> TcM.writeTcRef ref (Just lvl) }
 +                         -> do { TcM.traceTc "set-uni-flag skip" $
 +                                 vcat [ text "lvl" <+> ppr lvl, text "unif_lvl" <+> ppr unif_lvl ]
 +                               ; return () }
 +           _ -> do { TcM.traceTc "set-uni-flag" (ppr lvl)
 +                   ; TcM.writeTcRef ref (Just lvl) } }
  {- *********************************************************************
@@ -2263,14 +2282,16 @@ wrapUnifierX :: CtEvidence -> Role
               -> TcS (a, Bag Ct, [TcTyVar])
  wrapUnifierX ev role do_unifications
    = do { unif_count_ref <- getUnifiedRef
 +       ; given_eq_lvl <- getInnermostGivenEqLevel
         ; wrapTcS $
           do { defer_ref   <- TcM.newTcRef emptyBag
              ; unified_ref <- TcM.newTcRef []
 -            ; let env = UE { u_role      = role
 -                           , u_rewriters = ctEvRewriters ev
 -                           , u_loc       = ctEvLoc ev
 -                           , u_defer     = defer_ref
 -                           , u_unified   = Just unified_ref}
 +            ; let env = UE { u_role         = role
 +                           , u_given_eq_lvl = given_eq_lvl
 +                           , u_rewriters    = ctEvRewriters ev
 +                           , u_loc          = ctEvLoc ev
 +                           , u_defer        = defer_ref
 +                           , u_unified      = Just unified_ref}
                -- u_rewriters: the rewriter set and location from
                -- the parent constraint `ev` are inherited in any
                -- new constraints spat out by the unifier

compiler/GHC/Tc/Solver/Solve.hs

@@ -1063,8 +1063,10 @@ solveSimpleWanteds simples
                           simples limit (emptyWC { wc_simple = wc })
        | otherwise
        = do { -- Solve
 -             (unif_happened, wc1) <- reportUnifications $
 +             traceUnificationFlag "solveSimpleWanteds1"
 +           ; (unif_happened, wc1) <- reportUnifications $
                                       solve_simple_wanteds wc
 +           ; traceUnificationFlag "solveSimpleWanteds2"
               -- Run plugins
               -- NB: runTcPluginsWanted has a fast path for empty wc1,

compiler/GHC/Tc/Utils/Unify.hs

@@ -2063,7 +2063,12 @@ unifyTypeAndEmit :: TypeOrKind -> CtOrigin -> TcType -> TcType -> TcM CoercionN
  unifyTypeAndEmit t_or_k orig ty1 ty2
    = do { ref <- newTcRef emptyBag
         ; loc <- getCtLocM orig (Just t_or_k)
 +       ; cur_lvl <- getTcLevel
 +           -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles
 +           -- Here we don't know about given equalities; so we treat
 +           -- /any/ level outside this one as untouchable.  Hence cur_lvl.
         ; let env = UE { u_loc = loc, u_role = Nominal
 +                      , u_given_eq_lvl = cur_lvl
                        , u_rewriters = emptyRewriterSet  -- ToDo: check this
                        , u_defer = ref, u_unified = Nothing }
@@ -2112,11 +2117,14 @@ A job for the future.
  -}
  data UnifyEnv
 -  = UE { u_role      :: Role
 -       , u_loc       :: CtLoc
 -       , u_rewriters :: RewriterSet
+-
 -         -- Deferred constraints
 +  = UE { u_role         :: Role
 +       , u_loc          :: CtLoc
 +       , u_rewriters    :: RewriterSet
 +       , u_given_eq_lvl :: TcLevel  -- Just like the inert_given_eq_lvl field
 +                                    -- of GHC.Tc.Solver.InertSet.InertCans
++
 +         -- Deferred constraints; ones that could not be
 +         -- solved by "on the fly" unification
         , u_defer     :: TcRef (Bag Ct)
           -- Which variables are unified;
@@ -2483,15 +2491,22 @@ uUnfilledVar2 :: UnifyEnv       -- Precondition: u_role==Nominal
                                  --    definitely not a /filled/ meta-tyvar
                -> TcTauType      -- Type 2, zonked
                -> TcM CoercionN
 -uUnfilledVar2 env@(UE { u_defer = def_eq_ref }) swapped tv1 ty2
 -  = do { cur_lvl <- getTcLevel
 -           -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles
 -           -- Here we don't know about given equalities; so we treat
 -           -- /any/ level outside this one as untouchable.  Hence cur_lvl.
 -       ; if simpleUnifyCheck UC_OnTheFly cur_lvl tv1 ty2 /= SUC_CanUnify
 -         then not_ok_so_defer cur_lvl
 -         else
 -    do { def_eqs <- readTcRef def_eq_ref  -- Capture current state of def_eqs
 +uUnfilledVar2 env@(UE { u_defer = def_eq_ref, u_given_eq_lvl = given_eq_lvl })
 +              swapped tv1 ty2
 +  | simpleUnifyCheck UC_OnTheFly given_eq_lvl tv1 ty2 /= SUC_CanUnify
 +  = -- Simple unification check fails, so defer
 +    do { traceTc "uUnfilledVar2 not ok" $
 +             vcat [ text "tv1:" <+> ppr tv1
 +                  , text "ty2:" <+> ppr ty2
 +                  , text "simple-unify-chk:" <+> ppr (simpleUnifyCheck UC_OnTheFly given_eq_lvl tv1 ty2)
 +                  ]
 +               -- Occurs check or an untouchable: just defer
 +               -- NB: occurs check isn't necessarily fatal:
 +               --     eg tv1 occurred in type family parameter
 +       ; defer }
++
 +  | otherwise
 +  = do { def_eqs <- readTcRef def_eq_ref  -- Capture current state of def_eqs
         -- Attempt to unify kinds
         -- When doing so, be careful to preserve orientation;
@@ -2524,22 +2539,11 @@ uUnfilledVar2 env@(UE { u_defer = def_eq_ref }) swapped tv1 ty2
                       -- Do this dicarding by simply restoring the previous state
                       -- of def_eqs; a bit imperative/yukky but works fine.
                   ; defer }
 -         }}
 +         }
    where
      ty1 = mkTyVarTy tv1
      defer = unSwap swapped (uType_defer env) ty1 ty2
 -    not_ok_so_defer cur_lvl =
 -      do { traceTc "uUnfilledVar2 not ok" $
 -             vcat [ text "tv1:" <+> ppr tv1
 -                  , text "ty2:" <+> ppr ty2
 -                  , text "simple-unify-chk:" <+> ppr (simpleUnifyCheck UC_OnTheFly cur_lvl tv1 ty2)
 -                  ]
 -               -- Occurs check or an untouchable: just defer
 -               -- NB: occurs check isn't necessarily fatal:
 -               --     eg tv1 occurred in type family parameter
 -          ; defer }
+-
  swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool
  swapOverTyVars is_given tv1 tv2
    -- See Note [Unification variables on the left]