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

Commits:

7 changed files:

Changes:

  • compiler/GHC/Tc/Solver/Default.hs
    ... ... @@ -395,7 +395,7 @@ tryConstraintDefaulting wc
    395 395 
       | isEmptyWC wc
    396 396 
       = return wc
    397 397 
       | otherwise
    398 
    -  = do { (unif_happened, better_wc) <- reportUnifications (go_wc wc)
    398 
    +  = do { (unif_happened, better_wc) <- reportCoarseGrainUnifications (go_wc wc)
    399 399 
              -- We may have done unifications; so solve again
    400 400 
            ; solveAgainIf unif_happened better_wc }
    401 401 
       where

  • compiler/GHC/Tc/Solver/Equality.hs
    ... ... @@ -543,9 +543,14 @@ can_eq_nc_forall ev eq_rel s1 s2
    543 543
    544 544 
           -- Generate the constraints that live in the body of the implication
    545 545 
           -- See (SF5) in Note [Solving forall equalities]
    546 
    -      ; (lvl, (all_co, wanteds)) <- pushLevelNoWorkList (ppr skol_info)   $
    547 
    -                                    wrapUnifier ev (eqRelRole eq_rel) $ \uenv ->
    548 
    -                                    go uenv skol_tvs init_subst2 bndrs1 bndrs2
    546 
    +      ; (unifs, (lvl, (all_co, wanteds)))
    547 
    +             <- reportFindGrainUnifications           $
    548 
    +                pushLevelNoWorkList (ppr skol_info)   $
    549 
    +                wrapUnifier ev (eqRelRole eq_rel) $ \uenv ->
    550 
    +                go uenv skol_tvs init_subst2 bndrs1 bndrs2
    551 
    +
    552 
    +      -- Kick out any inerts constraints that mention unified type variables
    553 
    +      ; kickOutAfterUnification unifs
    549 554
    550 555 
           -- Solve the implication right away, using `trySolveImplication`
    551 556 
           -- See (SF6) in Note [Solving forall equalities]
    ... ... @@ -1670,31 +1675,36 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2
    1670 1675 
                   ; finish emptyRewriterSet (givenCtEvCoercion kind_ev) }
    1671 1676
    1672 1677 
           CtWanted {}
    1673 
    -         -> do { (unifs, (kind_co, cts)) <- reportUnifications $
    1678 
    +         -> do { (unifs, (kind_co, eqs)) <- reportFineGrainUnifications $
    1674 1679 
                                                 wrapUnifier ev Nominal $ \uenv ->
    1675 1680 
                                                 let uenv' = updUEnvLoc uenv (mkKindEqLoc xi1 xi2)
    1676 1681 
                                                 in unSwap swapped (uType uenv') ki1 ki2
    1677 1682 
                           -- mkKindEqLoc: any new constraints, arising from the kind
    1678 1683 
                           -- unification, say they thay come from unifying xi1~xi2
    1684 
    +                      -- ...AndEmit: emit any unsolved equalities
    1679 1685
    1680 
    -               -- Emit any unsolved kind equalities
    1681 
    -               ; unless (isEmptyBag cts) $
    1682 
    -                 updWorkListTcS (extendWorkListChildEqs ev cts)
    1686 
    +               -- Kick out any inert constraints mentioning the unified variables
    1687 
    +               ; kickOutAfterUnification unifs
    1683 1688
    1684 
    -               ; if unifs
    1689 
    +               ; if not (isEmptyVarSet unifs)
    1685 1690 
                      then -- Unifications happened, so start again to do the zonking
    1686 1691 
                           -- Otherwise we might put something in the inert set that isn't inert
    1692 
    +                      -- Since we are starting again we can ignore `eqs`, because they will
    1693 
    +                      -- happen again next time round
    1687 1694 
                           startAgainWith (mkNonCanonical ev)
    1688 1695 
                      else
    1689 1696
    1690 
    -            assertPpr (not (isEmptyCts cts)) (ppr ev $$ ppr ki1 $$ ppr ki2) $
    1691 
    -              -- assert: the constraints won't be empty because the two kinds differ,
    1692 
    -              -- and there are no unifications, so we must have emitted one or
    1693 
    -              -- more constraints
    1694 
    -            finish (rewriterSetFromCts cts) kind_co }
    1695 
    -                    -- rewriterSetFromCts: record in the /type/ unification xi1~xi2 that
    1696 
    -                    -- it has been rewritten by any (unsolved) consraints in `cts`; that
    1697 
    -                    -- stops xi1~xi2 from unifying until `cts` are solved. See (EIK2).
    1697 
    +               -- Emit the deferred constraints
    1698 
    +            do { emitChildEqs eqs
    1699 
    +
    1700 
    +               ; assertPpr (not (isEmptyCts cts)) (ppr ev $$ ppr ki1 $$ ppr ki2) $
    1701 
    +                   -- assert: the constraints won't be empty because the two kinds differ,
    1702 
    +                   -- and there are no unifications, so we must have emitted one or
    1703 
    +                   -- more constraints
    1704 
    +                finish (rewriterSetFromCts cts) kind_co }}
    1705 
    +                         -- rewriterSetFromCts: record in the /type/ unification xi1~xi2 that
    1706 
    +                         -- it has been rewritten by any (unsolved) constraints in `cts`; that
    1707 
    +                         -- stops xi1~xi2 from unifying until `cts` are solved. See (EIK2).
    1698 1708 
       where
    1699 1709 
         xi1  = canEqLHSType lhs1
    1700 1710 
         role = eqRelRole eq_rel
    ... ... @@ -2019,6 +2029,9 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
    2019 2029 
              ; setEvBindIfWanted new_ev EvCanonical $
    2020 2030 
                evCoercion (mkNomReflCo final_rhs)
    2021 2031
    2032 
    +         -- Kick out any constraints that can now be rewritten
    2033 
    +         ; kickOutAfterUnification (unitVarSet tv)
    2034 
    +
    2022 2035 
              ; return (Stop new_ev (text "Solved by unification")) }
    2023 2036
    2024 2037 
     ---------------------------

  • compiler/GHC/Tc/Solver/FunDeps.hs
    ... ... @@ -198,7 +198,7 @@ The solution is super-simple:
    198 198
    199 199 
       * Better still, we solve the [FunDepEqns] with
    200 200 
           solveFunDeps :: CtEvidence -> [FunDepEqns] -> TcS Bool
    201 
    -    It uses `reportUnifications` to see if any unification happened at this
    201 
    +    It uses `reportFineGrainUnifications` to see if any unification happened at this
    202 202 
         level or outside -- that is, it does NOT report unifications to the fresh
    203 203 
         unification variables.  So `solveFunDeps` returns True only if it
    204 204 
         unifies a variable /other than/ the fresh ones.  Bingo.
    ... ... @@ -770,16 +770,20 @@ solveFunDeps work_ev fd_eqns
    770 770 
       = return False -- Common case no-op
    771 771
    772 772 
       | otherwise
    773 
    -  = do { (unif_happened, _res)
    774 
    -             <- reportUnifications $
    775 
    -                nestFunDepsTcS     $
    773 
    +  = do { (unifs, _res)
    774 
    +             <- reportFineGrainUnifications $
    775 
    +                nestFunDepsTcS              $
    776 776 
                     do { (_, eqs) <- wrapUnifier work_ev Nominal do_fundeps
    777 777 
                        ; solveSimpleWanteds eqs }
    778 778 
         -- Why solveSimpleWanteds?  Answer
    779 779 
         --     (a) We don't want to rely on the eager unifier being clever
    780 780 
         --     (b) F Int alpha ~ Maybe Int   where  type instance F Int x = Maybe x
    781 781
    782 
    -       ; return unif_happened }
    782 
    +       -- Kick out any inert constraints that mention variables
    783 
    +       -- that were unified by the fundep
    784 
    +       ; kickOutAfterUnification unifs
    785 
    +
    786 
    +       ; return (not (isEmptyVarSet unifs)) }
    783 787 
       where
    784 788 
         do_fundeps :: UnifyEnv -> TcM ()
    785 789 
         do_fundeps env = mapM_ (do_one env) fd_eqns

  • compiler/GHC/Tc/Solver/Monad.hs
    ... ... @@ -55,7 +55,7 @@ module GHC.Tc.Solver.Monad (
    55 55 
         newWanted,
    56 56 
         newWantedNC, newWantedEvVarNC,
    57 57 
         newBoundEvVarId,
    58 
    -    unifyTyVar, reportUnifications,
    58 
    +    unifyTyVar, reportFineGrainUnifications, reportCoarseGrainUnifications,
    59 59 
         setEvBind, setWantedEq,
    60 60 
         setWantedEvTerm, setEvBindIfWanted,
    61 61 
         newEvVar, newGivenEv, emitNewGivens,
    ... ... @@ -448,6 +448,17 @@ kickOutRewritable ko_spec new_fr
    448 448 
                              , text "kicked_out =" <+> ppr kicked_out
    449 449 
                              , text "Residual inerts =" <+> ppr ics' ]) } }
    450 450
    451 
    +kickOutAfterUnification :: TcTyVarSet -> TcS ()
    452 
    +kickOutAfterUnification tv_set
    453 
    +  | isEmptyVarSet tv_set
    454 
    +  = return ()
    455 
    +  | otherwise
    456 
    +  = do { n_kicked <- kickOutRewritable (KOAfterUnify tv_set) (Given, NomEq)
    457 
    +                     -- Given because the tv := xi is given; NomEq because
    458 
    +                     -- only nominal equalities are solved by unification
    459 
    +       ; traceTcS "kickOutAfterUnification" (ppr tvs $$ text "n_kicked =" <+> ppr n_kicked)
    460 
    +       ; return n_kicked }
    461 
    +
    451 462 
     kickOutAfterFillingCoercionHole :: CoercionHole -> TcS ()
    452 463 
     -- See Wrinkle (URW2) in Note [Unify only if the rewriter set is empty]
    453 464 
     -- in GHC.Tc.Solver.Equality
    ... ... @@ -1764,30 +1775,47 @@ unifyTyVar :: TcTyVar -> TcType -> TcS ()
    1764 1775 
     unifyTyVar tv ty
    1765 1776 
       = assertPpr (isMetaTyVar tv) (ppr tv) $
    1766 1777 
         do { liftZonkTcS (TcM.writeMetaTyVar tv ty)  -- Produces a trace message
    1767 
    -       ; uni_ref <- getWhatUnifications
    1768 
    -       ; wrapTcS $ recordUnification uni_ref tv }
    1778 
    +       ; what_uni <- getWhatUnifications
    1779 
    +       ; wrapTcS $ recordUnification what_uni tv }
    1780 
    +
    1781 
    +reportFineGrainUnifications :: TcS a -> TcS (TcTyVarSet, a)
    1782 
    +reportFineGrainUnifications (TcS thing_inside)
    1783 
    +  = TcS $ \ env@(TcSEnv { tcs_unif_lvl = outer_wu }) ->
    1784 
    +    do { (unif_tvs, res) <- report_fine_grain_unifs env thing_inside
    1785 
    +       ; recordUnifications outer_wu unif_tvs
    1786 
    +       ; return (unif_tvs, res) }
    1769 1787
    1770 
    -reportUnifications :: TcS a -> TcS (Bool, a)
    1788 
    +reportCoarseGrainUnifications :: TcS a -> TcS (Bool, a)
    1771 1789 
     -- Record whether any useful unifications are done by thing_inside
    1772 1790 
     -- Remember to propagate the information to the enclosing context
    1773 
    -reportUnifications (TcS thing_inside)
    1774 
    -  = TcS $ \ env@(TcSEnv { tcs_unif_lvl = outer_ul_var }) ->
    1775 
    -    do { inner_ul_var <- TcM.newTcRef NoUnificationsYet
    1776 
    -
    1777 
    -       ; res <- thing_inside (env { tcs_unif_lvl = inner_ul_var })
    1778 
    -
    1779 
    -       ; ambient_lvl  <- TcM.getTcLevel
    1780 
    -       ; mb_inner_lvl <- TcM.readTcRef inner_ul_var
    1781 
    -
    1782 
    -       ; case mb_inner_lvl of
    1783 
    -           UnificationsDone unif_lvl
    1784 
    -             | ambient_lvl `deeperThanOrSame` unif_lvl
    1785 
    -             -> -- Some useful unifications took place
    1786 
    -                do { recordUnificationLevel outer_ul_var unif_lvl
    1787 
    -                   ; return (True, res) }
    1788 
    -
    1789 
    -           _  -> -- No useful unifications
    1790 
    -                 return (False, res) }
    1791 
    +reportCoarseGrainUnifications (TcS thing_inside)
    1792 
    +  = TcS $ \ env@(TcSEnv { tcs_unif_lvl = outer_what }) ->
    1793 
    +    case outer_what of
    1794 
    +      WU_Coarse outer_ul_ref
    1795 
    +        -> do { inner_ul_ref <- TcM.newTcRef infiniteTcLevel
    1796 
    +              ; res <- thing_inside (env { tcs_unif_lvl = WU_Coarse inner_ul_ref })
    1797 
    +              ; ambient_lvl <- TcM.getTcLevel
    1798 
    +              ; outer_ul   <- TcM.readTcRef outer_ul_ref
    1799 
    +              ; inner_ul   <- TcM.readTcRef inner_ul_ref
    1800 
    +              ; unless (inner_ul `deeperThanOrSame` outer_ul) $
    1801 
    +                writeTcRef outer_ul_ref inner_ul
    1802 
    +              ; let unif_happened = ambient_lvl `deeperThanOrSame` inner_lvl
    1803 
    +              ; return (unif_happened, res) }
    1804 
    +      WU_Fine outer_tvs
    1805 
    +        -> do { (unif_tvs,res) <- report_fine_grain_unifs env thing_inside
    1806 
    +              ; return (not (isEmptyVarSet unif_tvs), res) }
    1807 
    +
    1808 
    +report_fine_grain_unifs :: TcSEnv -> (TcSEnv -> TcM a) -> TcM (TcTyVarSet, a)
    1809 
    +report_fine_grain_unifs env thing_inside
    1810 
    +  = do { unif_tvs_ref <- TcM.newTcRef emptyVarSet
    1811 
    +
    1812 
    +       ; res <- thing_inside (env { tcs_unif_lvl = WU_Fine unif_tvs_ref })
    1813 
    +
    1814 
    +       ; unif_tvs    <- TcM.readTcRef unif_tvs_ref
    1815 
    +       ; ambient_lvl <- TcM.getTcLevel
    1816 
    +       ; let interesting unif_tv = ambient_lvl `deeperThanOrSame` tcTyVarLevel tv
    1817 
    +             interesting_unifs = filterVarSet interesting unif_tvs
    1818 
    +       ; return (unif_tvs, res) }
    1791 1819
    1792 1820 
     getWhatUnifications :: TcS (TcRef WhatUnifications)
    1793 1821 
     getWhatUnifications
    ... ... @@ -1995,6 +2023,19 @@ emitNewWantedEq loc rewriters role ty1 ty2
    1995 2023 
            ; updWorkListTcS (extendWorkListEq rewriters (mkNonCanonical $ CtWanted wtd))
    1996 2024 
            ; return co }
    1997 2025
    2026 
    +emitChildEqs :: Cts -> TcS ()
    2027 
    +-- Emit a bunch of equalities into the work list
    2028 
    +-- See Note [Work-list ordering] in GHC.Tc.Solved.Equality
    2029 
    +--
    2030 
    +-- All the constraints in `cts` share the same rewriter set so,
    2031 
    +-- rather than looking at it one by one, we pass it to
    2032 
    +-- extendWorkListChildEqs; just a small optimisation.
    2033 
    +emitChildEqs eqs
    2034 
    +  | isEmptyBag eqs
    2035 
    +  = return ()
    2036 
    +  | otherwise
    2037 
    +  = updWorkListTcS (extendWorkListChildEqs ev cts)
    2038 
    +
    1998 2039 
     -- | Create a new Wanted constraint holding a coercion hole
    1999 2040 
     -- for an equality between the two types at the given 'Role'.
    2000 2041 
     newWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType
    ... ... @@ -2146,18 +2187,18 @@ uPairsTcM uenv eqns = mapM_ (\(Pair ty1 ty2) -> uType uenv ty1 ty2) eqns
    2146 2187 
     wrapUnifierAndEmit :: CtEvidence -> Role
    2147 2188 
                        -> (UnifyEnv -> TcM a)  -- Some calls to uType
    2148 2189 
                        -> TcS a
    2149 
    --- Like wrapUnifier, but emits any unsolved equalities into the work-list
    2190 
    +-- Like wrapUnifier, but
    2191 
    +--    emits any unsolved equalities into the work-list
    2192 
    +--    kicks out any inert constraints that mention unified variables
    2150 2193 
     wrapUnifierAndEmit ev role do_unifications
    2151 
    -  = do { (res, cts) <- wrapUnifier ev role do_unifications
    2194 
    +  = do { (unifs, (res, eqs)) <- reportFineGrainUnifications $
    2195 
    +                                wrapUnifier ev role do_unifications
    2152 2196
    2153 2197 
            -- Emit the deferred constraints
    2154 
    -       -- See Note [Work-list ordering] in GHC.Tc.Solved.Equality
    2155 
    -       --
    2156 
    -       -- All the constraints in `cts` share the same rewriter set so,
    2157 
    -       -- rather than looking at it one by one, we pass it to
    2158 
    -       -- extendWorkListChildEqs; just a small optimisation.
    2159 
    -       ; unless (isEmptyBag cts) $
    2160 
    -         updWorkListTcS (extendWorkListChildEqs ev cts)
    2198 
    +       ; emitChildEqs eqs
    2199 
    +
    2200 
    +       -- Kick out any inert constraints mentioning the unified variables
    2201 
    +       ; kickOutAfterUnification unifs
    2161 2202
    2162 2203 
            ; return res }
    2163 2204

  • compiler/GHC/Tc/Solver/Solve.hs
    ... ... @@ -119,7 +119,7 @@ simplify_loop n limit definitely_redo_implications
    119 119 
                                 , int (lengthBag simples) <+> text "simples to solve" ])
    120 120 
            ; traceTcS "simplify_loop: wc =" (ppr wc)
    121 121
    122 
    -       ; (unif_happened, wc1) <- reportUnifications $  -- See Note [Superclass iteration]
    122 
    +       ; (unif_happened, wc1) <- reportCoarseGrainUnifications $  -- See Note [Superclass iteration]
    123 123 
                                      solveSimpleWanteds simples
    124 124 
                     -- Any insoluble constraints are in 'simples' and so get rewritten
    125 125 
                     -- See Note [Rewrite insolubles] in GHC.Tc.Solver.InertSet
    ... ... @@ -1125,19 +1125,11 @@ solveSimpleWanteds simples
    1125 1125 
       where
    1126 1126 
         do_solve_and_plugins :: IntWithInf -> WantedConstraints -> TcS (Bool,WantedConstraints)
    1127 1127 
         do_solve_and_plugins max_iter wc
    1128 
    -      = do { wc1 <- run_simple_solver max_iter wc
    1128 
    +      = do { wc1 <- simple_solver wc
    1129 1129 
                ; (rerun_plugin, simples2) <- runTcPluginsWanted (wc_simple wc1)
    1130 1130 
                ; return (rerun_plugin, wc1 { wc_simple = simples2 }) }
    1131 1131
    1132 
    -    run_simple_solver :: IntWithInf -> WantedConstraints -> TcS WantedConstraints
    1133 
    -    -- Run `simple_solver` repeatedly until no more unifications happen
    1134 
    -    -- Try this repeatedly, until no unifications happen
    1135 
    -    -- This is potentially quadratic, because we might solve just one
    1136 
    -    -- constraint in each iteration but that seems inevitable
    1137 
    -    run_simple_solver max_iter
    1138 
    -       =  iterateToFixpoint (max_iter `mulWithInf` 10) simple_solver
    1139 
    -
    1140 
    -    simple_solver :: WantedConstraints -> TcS (Bool, WantedConstraints)
    1132 
    +    simple_solver :: WantedConstraints -> TcS WantedConstraints
    1141 1133 
         -- Try solving the wc_simple part of these constraints, once
    1142 1134 
         -- Affects the unification state (of course) but not the inert set
    1143 1135 
         -- The result is not necessarily zonked
    ... ... @@ -1145,8 +1137,7 @@ solveSimpleWanteds simples
    1145 1137 
           | isEmptyBag simples
    1146 1138 
           = return (False, wc)
    1147 1139 
           | otherwise
    1148 
    -      = reportUnifications $
    1149 
    -        nestTcS             $
    1140 
    +      = nestTcS $
    1150 1141 
             do { solveSimples simples
    1151 1142 
                ; simples1 <- getUnsolvedInerts
    1152 1143 
                    -- Now try to solve any Wanted quantified

  • compiler/GHC/Tc/Utils/TcType.hs
    ... ... @@ -45,6 +45,7 @@ module GHC.Tc.Utils.TcType (
    45 45 
       TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel,
    46 46 
       strictlyDeeperThan, deeperThanOrSame, sameDepthAs,
    47 47 
       tcTypeLevel, tcTyVarLevel, maxTcLevel, minTcLevel,
    48 
    +  infiniteTcLevel,
    48 49
    49 50 
       --------------------------------
    50 51 
       -- MetaDetails
    ... ... @@ -843,6 +844,12 @@ We can unify alpha:=b in the inner implication, because 'alpha' is
    843 844 
     touchable; but then 'b' has escaped its scope into the outer implication.
    844 845 
     -}
    845 846
    847 
    +infiniteTcLevel :: TcLevel
    848 
    +-- It is sometimes helpful to be able to say "infinitely deep"
    849 
    +-- Particularly as a unit for `minTcLevel`
    850 
    +-- Happily QLInstVar behaves like infinity :-)
    851 
    +infiniteTcLevel = QLInstVar
    852 
    +
    846 853 
     maxTcLevel :: TcLevel -> TcLevel -> TcLevel
    847 854 
     maxTcLevel (TcLevel a) (TcLevel b)
    848 855 
       | a > b      = TcLevel a

  • compiler/GHC/Tc/Utils/Unify.hs
    ... ... @@ -37,7 +37,7 @@ module GHC.Tc.Utils.Unify (
    37 37 
       makeTypeConcrete,
    38 38
    39 39 
       UnifyEnv(..), updUEnvLoc, setUEnvRole,
    40 
    -  WhatUnifications(..), recordUnification, recordUnificationLevel,
    40 
    +  WhatUnifications(..), recordUnification, recordUnifications, minTcTyVarSetLevel,
    41 41
    42 42 
       --------------------------------
    43 43 
       -- Holes
    ... ... @@ -2316,8 +2316,11 @@ unifyTypeAndEmit t_or_k orig ty1 ty2
    2316 2316 
     **********************************************************************-}
    2317 2317
    2318 2318 
     data WhatUnifications
    2319 
    -  = NoUnificationsYet
    2320 
    -  | UnificationsDone TcLevel
    2319 
    +  = WU_Coarse           -- Track unifications coarsely
    2320 
    +      (TcRef TcLevel)      -- infiniteTcLevel <=> no unifications yet
    2321 
    +
    2322 
    +  | WU_Fine                  -- Track each unification individually
    2323 
    +      (TcRef TcTyVarSet)
    2321 2324
    2322 2325 
     {- Note [WhatUnifications]
    2323 2326 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~
    ... ... @@ -2346,9 +2349,28 @@ Why do all this?
    2346 2349 
      * See Note [When to iterate the solver: unifications] in GHC.Tc.Solver.Solve
    2347 2350 
     -}
    2348 2351
    2349 
    -recordUnification :: TcRef WhatUnifications -> TcTyVar -> TcM ()
    2350 
    -recordUnification what_ref tv = recordUnificationLevel what_ref (tcTyVarLevel tv)
    2352 
    +minTcTyVarSetLevel :: TcTyVarSet -> TcLevel
    2353 
    +minTcTyVarSetLevel tvs
    2354 
    +  = nonDetStrictFoldVarSet (minTcLevel . tcTyVarLevel) infiniteTcLevel tvs
    2355 
    +
    2356 
    +recordUnification :: WhatUnifications -> TcTyVar -> TcM ()
    2357 
    +recordUnification what tv = recordUnifications what (unitVarSet tv)
    2358 
    +
    2359 
    +recordUnifications :: WhatUnifications -> TcTyVarSet -> TcM ()
    2360 
    +recordUnifications (WU_Coarse lvl_ref) tvs
    2361 
    +  = do { unif_lvl <- readTcRef lvl_ref
    2362 
    +       ; let tv_lvl = minTcTyVarSetLevel tvs
    2363 
    +       ; if tv_lvl `deeperThanOrSame` unif_lvl
    2364 
    +         then do { traceTc "set-uni-flag: no-op" $
    2365 
    +                   vcat [ text "lvl" <+> ppr tv_lvl, text "unif_lvl" <+> ppr unif_lvl ]
    2366 
    +                 ; return () }
    2367 
    +         else do { traceTc "set-uni-flag" (ppr tv_lvl)
    2368 
    +                 ; writeTcRef lvl_ref tv_lvl } }
    2369 
    +
    2370 
    +recordUnifications (WU_Fine tvs_ref) tvs
    2371 
    +  = updTcRef tvs_ref (`unionVarSet` tvs)
    2351 2372
    2373 
    +{-
    2352 2374 
     recordUnificationLevel :: TcRef WhatUnifications -> TcLevel -> TcM ()
    2353 2375 
     recordUnificationLevel what_ref tv_lvl
    2354 2376 
       = do { what <- readTcRef what_ref
    ... ... @@ -2360,11 +2382,7 @@ recordUnificationLevel what_ref tv_lvl
    2360 2382 
                        ; return () }
    2361 2383 
                _ -> do { traceTc "set-uni-flag" (ppr tv_lvl)
    2362 2384 
                        ; writeTcRef what_ref (UnificationsDone tv_lvl) } }
    2363 
    -
    2364 
    -
    2365 
    -instance Outputable WhatUnifications where
    2366 
    -   ppr NoUnificationsYet      = text "NoUniYet"
    2367 
    -   ppr (UnificationsDone lvl) = text "UniDone" <> braces (ppr lvl)
    2385 
    +-}
    2368 2386
    2369 2387 
     {-
    2370 2388 
     %************************************************************************
    ... ... @@ -2416,7 +2434,7 @@ data UnifyEnv
    2416 2434
    2417 2435 
              -- Which variables are unified;
    2418 2436 
              -- if Nothing, we don't care
    2419 
    -       , u_what :: Maybe (TcRef WhatUnifications)
    2437 
    +       , u_what :: Maybe WhatUnifications
    2420 2438 
         }
    2421 2439
    2422 2440 
     setUEnvRole :: UnifyEnv -> Role -> UnifyEnv
    ... ... @@ -2698,7 +2716,7 @@ Deferred unifications are of the form
    2698 2716 
     or              x ~ ...
    2699 2717 
     where F is a type function and x is a type variable.
    2700 2718 
     E.g.
    2701 
    -        id :: x ~ y => x -> y
    2719 
    +       id :: x ~ y => x -> y
    2702 2720 
             id e = e
    2703 2721
    2704 2722 
     involves the unification x = y. It is deferred until we bring into account the

    • —
    View it on GitLab.
    You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications · Help