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

Commits:

5 changed files:

Changes:

  • compiler/GHC/Tc/Solver/Dict.hs
    ... ... @@ -648,69 +648,6 @@ on whether we apply this optimization when IncoherentInstances is in effect:
    648 648 
     The output of `main` if we avoid the optimization under the effect of
    649 649 
     IncoherentInstances is `1`. If we were to do the optimization, the output of
    650 650 
     `main` would be `2`.
    651 
    -
    652 
    -
    653 
    -Note [No Given/Given fundeps]
    654 
    -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    655 
    -We do not create constraints from:
    656 
    -* Given/Given interactions via functional dependencies or type family
    657 
    -  injectivity annotations.
    658 
    -* Given/instance fundep interactions via functional dependencies or
    659 
    -  type family injectivity annotations.
    660 
    -
    661 
    -In this Note, all these interactions are called just "fundeps".
    662 
    -
    663 
    -We ingore such fundeps for several reasons:
    664 
    -
    665 
    -1. These fundeps will never serve a purpose in accepting more
    666 
    -   programs: Given constraints do not contain metavariables that could
    667 
    -   be unified via exploring fundeps. They *could* be useful in
    668 
    -   discovering inaccessible code. However, the constraints will be
    669 
    -   Wanteds, and as such will cause errors (not just warnings) if they
    670 
    -   go unsolved. Maybe there is a clever way to get the right
    671 
    -   inaccessible code warnings, but the path forward is far from
    672 
    -   clear. #12466 has further commentary.
    673 
    -
    674 
    -2. Furthermore, here is a case where a Given/instance interaction is actively
    675 
    -   harmful (from dependent/should_compile/RaeJobTalk):
    676 
    -
    677 
    -       type family a == b :: Bool
    678 
    -       type family Not a = r | r -> a where
    679 
    -         Not False = True
    680 
    -         Not True  = False
    681 
    -
    682 
    -       [G] Not (a == b) ~ True
    683 
    -
    684 
    -   Reacting this Given with the equations for Not produces
    685 
    -
    686 
    -      [W] a == b ~ False
    687 
    -
    688 
    -   This is indeed a true consequence, and would make sense as a fresh Given.
    689 
    -   But we don't have a way to produce evidence for fundeps, as a Wanted it
    690 
    -   is /harmful/: we can't prove it, and so we'll report an error and reject
    691 
    -   the program. (Previously fundeps gave rise to Deriveds, which
    692 
    -   carried no evidence, so it didn't matter that they could not be proved.)
    693 
    -
    694 
    -3. #20922 showed a subtle different problem with Given/instance fundeps.
    695 
    -      type family ZipCons (as :: [k]) (bssx :: [[k]]) = (r :: [[k]]) | r -> as bssx where
    696 
    -        ZipCons (a ': as) (bs ': bss) = (a ': bs) ': ZipCons as bss
    697 
    -        ...
    698 
    -
    699 
    -      tclevel = 4
    700 
    -      [G] ZipCons is1 iss ~ (i : is2) : jss
    701 
    -
    702 
    -   (The tclevel=4 means that this Given is at level 4.)  The fundep tells us that
    703 
    -   'iss' must be of form (is2 : beta[4]) where beta[4] is a fresh unification
    704 
    -   variable; we don't know what type it stands for. So we would emit
    705 
    -      [W] iss ~ is2 : beta
    706 
    -
    707 
    -   Again we can't prove that equality; and worse we'll rewrite iss to
    708 
    -   (is2:beta) in deeply nested constraints inside this implication,
    709 
    -   where beta is untouchable (under other equality constraints), leading
    710 
    -   to other insoluble constraints.
    711 
    -
    712 
    -The bottom line: since we have no evidence for them, we should ignore Given/Given
    713 
    -and Given/instance fundeps entirely.
    714 651 
     -}
    715 652
    716 653 
     tryInertDicts :: DictCt -> SolverStage ()

  • compiler/GHC/Tc/Solver/FunDeps.hs
    ... ... @@ -313,7 +313,13 @@ doDictFunDepImprovement dict_ct
    313 313 
     doDictFunDepImprovementLocal :: DictCt -> SolverStage ()
    314 314 
     -- Using functional dependencies, interact the DictCt with the
    315 315 
     -- inert Givens and Wanteds, to produce new equalities
    316 
    -doDictFunDepImprovementLocal dict_ct@(DictCt { di_cls = cls, di_ev = wanted_ev })
    316 
    +doDictFunDepImprovementLocal dict_ct@(DictCt { di_cls = cls, di_ev = work_ev })
    317 
    +  | isGiven work_ev
    318 
    +  = -- If work_ev is Given, there could in principle be some inert Wanteds
    319 
    +    -- but in practice there never are because we solve Givens first
    320 
    +    nopStage ()
    321 
    +
    322 
    +  | otherwise
    317 323 
       = Stage $
    318 324 
         do { inerts <- getInertCans
    319 325
    ... ... @@ -324,35 +330,44 @@ doDictFunDepImprovementLocal dict_ct@(DictCt { di_cls = cls, di_ev = wanted_ev }
    324 330 
            ; if imp then startAgainWith (CDictCan dict_ct)
    325 331 
                     else continueWith () }
    326 332 
       where
    327 
    -    wanted_pred = ctEvPred wanted_ev
    328 
    -    wanted_loc  = ctEvLoc  wanted_ev
    333 
    +    work_pred     = ctEvPred work_ev
    334 
    +    work_loc      = ctEvLoc  work_ev
    335 
    +    work_is_given = isGiven work_ev
    329 336
    330 337 
         do_interaction :: Cts -> DictCt -> TcS Cts
    331 
    -    do_interaction new_eqs1 (DictCt { di_ev = all_ev }) -- This can be Given or Wanted
    338 
    +    do_interaction new_eqs1 (DictCt { di_ev = inert_ev }) -- This can be Given or Wanted
    339 
    +      | work_is_given && isGiven inert_ev
    340 
    +        -- Do not create FDs from Given/Given interactions
    341 
    +        -- See Note [No Given/Given fundeps]
    342 
    +        -- It is possible for work_ev to be Given when inert_ev is Wanted:
    343 
    +        -- this can happen if a Given is kicked out by a unification
    344 
    +      = return new_eqs1
    345 
    +
    346 
    +      | otherwise
    332 347 
           = do { traceTcS "doLocalFunDepImprovement" $
    333 
    -             vcat [ ppr wanted_ev
    334 
    -                  , pprCtLoc wanted_loc, ppr (isGivenLoc wanted_loc)
    335 
    -                  , pprCtLoc all_loc, ppr (isGivenLoc all_loc)
    348 
    +             vcat [ ppr work_ev
    349 
    +                  , pprCtLoc work_loc, ppr (isGivenLoc work_loc)
    350 
    +                  , pprCtLoc inert_loc, ppr (isGivenLoc inert_loc)
    336 351 
                       , pprCtLoc deriv_loc, ppr (isGivenLoc deriv_loc) ]
    337 352
    338 
    -           ; new_eqs2 <- unifyFunDepWanteds_new wanted_ev $
    339 
    -                         improveFromAnother (deriv_loc, all_rewriters)
    340 
    -                                            all_pred wanted_pred
    353 
    +           ; new_eqs2 <- unifyFunDepWanteds_new work_ev $
    354 
    +                         improveFromAnother (deriv_loc, inert_rewriters)
    355 
    +                                            inert_pred work_pred
    341 356 
                ; return (new_eqs1 `unionBags` new_eqs2) }
    342 357 
           where
    343 
    -        all_pred  = ctEvPred all_ev
    344 
    -        all_loc   = ctEvLoc all_ev
    345 
    -        all_rewriters = ctEvRewriters all_ev
    346 
    -        deriv_loc = wanted_loc { ctl_depth  = deriv_depth
    358 
    +        inert_pred  = ctEvPred inert_ev
    359 
    +        inert_loc   = ctEvLoc inert_ev
    360 
    +        inert_rewriters = ctEvRewriters inert_ev
    361 
    +        deriv_loc = work_loc { ctl_depth  = deriv_depth
    347 362 
                                    , ctl_origin = deriv_origin }
    348 
    -        deriv_depth = ctl_depth wanted_loc `maxSubGoalDepth`
    349 
    -                      ctl_depth all_loc
    350 
    -        deriv_origin = FunDepOrigin1 wanted_pred
    351 
    -                                     (ctLocOrigin wanted_loc)
    352 
    -                                     (ctLocSpan wanted_loc)
    353 
    -                                     all_pred
    354 
    -                                     (ctLocOrigin all_loc)
    355 
    -                                     (ctLocSpan all_loc)
    363 
    +        deriv_depth = ctl_depth work_loc `maxSubGoalDepth`
    364 
    +                      ctl_depth inert_loc
    365 
    +        deriv_origin = FunDepOrigin1 work_pred
    366 
    +                                     (ctLocOrigin work_loc)
    367 
    +                                     (ctLocSpan work_loc)
    368 
    +                                     inert_pred
    369 
    +                                     (ctLocOrigin inert_loc)
    370 
    +                                     (ctLocSpan inert_loc)
    356 371
    357 372 
     doDictFunDepImprovementTop :: DictCt -> SolverStage ()
    358 373 
     doDictFunDepImprovementTop dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = xis })
    ... ... @@ -389,6 +404,69 @@ solveFunDeps generate_eqs
    389 404 
         do { eqs <- generate_eqs
    390 405 
            ; solveSimpleWanteds eqs }
    391 406
    407 
    +{- Note [No Given/Given fundeps]
    408 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    409 
    +We do not create constraints from:
    410 
    +* Given/Given interactions via functional dependencies or type family
    411 
    +  injectivity annotations.
    412 
    +* Given/instance fundep interactions via functional dependencies or
    413 
    +  type family injectivity annotations.
    414 
    +
    415 
    +In this Note, all these interactions are called just "fundeps".
    416 
    +
    417 
    +We ingore such fundeps for several reasons:
    418 
    +
    419 
    +1. These fundeps will never serve a purpose in accepting more
    420 
    +   programs: Given constraints do not contain metavariables that could
    421 
    +   be unified via exploring fundeps. They *could* be useful in
    422 
    +   discovering inaccessible code. However, the constraints will be
    423 
    +   Wanteds, and as such will cause errors (not just warnings) if they
    424 
    +   go unsolved. Maybe there is a clever way to get the right
    425 
    +   inaccessible code warnings, but the path forward is far from
    426 
    +   clear. #12466 has further commentary.
    427 
    +
    428 
    +2. Furthermore, here is a case where a Given/instance interaction is actively
    429 
    +   harmful (from dependent/should_compile/RaeJobTalk):
    430 
    +
    431 
    +       type family a == b :: Bool
    432 
    +       type family Not a = r | r -> a where
    433 
    +         Not False = True
    434 
    +         Not True  = False
    435 
    +
    436 
    +       [G] Not (a == b) ~ True
    437 
    +
    438 
    +   Reacting this Given with the equations for Not produces
    439 
    +
    440 
    +      [W] a == b ~ False
    441 
    +
    442 
    +   This is indeed a true consequence, and would make sense as a fresh Given.
    443 
    +   But we don't have a way to produce evidence for fundeps, as a Wanted it
    444 
    +   is /harmful/: we can't prove it, and so we'll report an error and reject
    445 
    +   the program. (Previously fundeps gave rise to Deriveds, which
    446 
    +   carried no evidence, so it didn't matter that they could not be proved.)
    447 
    +
    448 
    +3. #20922 showed a subtle different problem with Given/instance fundeps.
    449 
    +      type family ZipCons (as :: [k]) (bssx :: [[k]]) = (r :: [[k]]) | r -> as bssx where
    450 
    +        ZipCons (a ': as) (bs ': bss) = (a ': bs) ': ZipCons as bss
    451 
    +        ...
    452 
    +
    453 
    +      tclevel = 4
    454 
    +      [G] ZipCons is1 iss ~ (i : is2) : jss
    455 
    +
    456 
    +   (The tclevel=4 means that this Given is at level 4.)  The fundep tells us that
    457 
    +   'iss' must be of form (is2 : beta[4]) where beta[4] is a fresh unification
    458 
    +   variable; we don't know what type it stands for. So we would emit
    459 
    +      [W] iss ~ is2 : beta
    460 
    +
    461 
    +   Again we can't prove that equality; and worse we'll rewrite iss to
    462 
    +   (is2:beta) in deeply nested constraints inside this implication,
    463 
    +   where beta is untouchable (under other equality constraints), leading
    464 
    +   to other insoluble constraints.
    465 
    +
    466 
    +The bottom line: since we have no evidence for them, we should ignore Given/Given
    467 
    +and Given/instance fundeps entirely.
    468 
    +-}
    469 
    +
    392 470 
     {-
    393 471 
     ************************************************************************
    394 472 
     *                                                                      *

  • compiler/GHC/Tc/Solver/Monad.hs
    ... ... @@ -1298,21 +1298,25 @@ nestFunDepsTcS (TcS thing_inside)
    1298 1298 
                                 , tcs_worklist = new_wl_var
    1299 1299 
                                 , tcs_unif_lvl = new_unif_lvl_var }
    1300 1300
    1301 
    +       ; TcM.traceTc "nestFunDepsTcS {" empty
    1301 1302 
            ; (inner_lvl, _res) <- TcM.pushTcLevelM $
    1302 1303 
                                   thing_inside nest_env
    1304 
    +           -- Increase the level so that unification variables allocated by
    1305 
    +           -- the fundep-creation itself don't count as useful unifications
    1306 
    +       ; TcM.traceTc "nestFunDepsTcS }" empty
    1303 1307
    1304 1308 
            -- Figure out whether the fundeps did any useful unifications,
    1305 1309 
            -- and if so update the tcs_unif_lvl
    1306 1310 
            ; mb_new_lvl <- TcM.readTcRef new_unif_lvl_var
    1307 1311 
            ; case mb_new_lvl of
    1308 
    -           Just new_lvl
    1309 
    -             | inner_lvl `deeperThanOrSame` new_lvl
    1312 
    +           Just unif_lvl
    1313 
    +             | inner_lvl `deeperThanOrSame` unif_lvl
    1310 1314 
                  -> -- Some useful unifications took place
    1311 1315 
                     do { mb_old_lvl <- TcM.readTcRef unif_lvl_var
    1312 1316 
                        ; case mb_old_lvl of
    1313 
    -                       Just old_lvl | new_lvl `deeperThanOrSame` old_lvl
    1317 
    +                       Just old_lvl | unif_lvl `deeperThanOrSame` old_lvl
    1314 1318 
                                         -> return ()
    1315 
    -                       _ -> TcM.writeTcRef unif_lvl_var (Just new_lvl)
    1319 
    +                       _ -> TcM.writeTcRef unif_lvl_var (Just unif_lvl)
    1316 1320 
                        ; return True }
    1317 1321
    1318 1322 
                _  -> return False   -- No unifications (except of vars

  • compiler/GHC/Tc/Solver/Solve.hs
    ... ... @@ -126,7 +126,7 @@ simplify_loop n limit definitely_redo_implications
    126 126 
                     -- See Note [Rewrite insolubles] in GHC.Tc.Solver.InertSet
    127 127
    128 128 
            ; wc2 <- if not definitely_redo_implications  -- See Note [Superclass iteration]
    129 
    -                   && n_unifs1 == 0                    -- for this conditional
    129 
    +                   && n_unifs1 == 0                  -- for this conditional
    130 130 
                     then return (wc { wc_simple = simples1 })  -- Short cut
    131 131 
                     else do { implics1 <- solveNestedImplications implics
    132 132 
                             ; return (wc { wc_simple = simples1

  • testsuite/tests/typecheck/should_fail/tcfail143.stderr
    1 
    -
    2 
    -tcfail143.hs:30:9: error: [GHC-18872]
    3 
    -    • Couldn't match type ‘S Z’ with ‘Z’
    4 
    -        arising from a functional dependency between:
    5 
    -          constraint ‘MinMax (S Z) Z Z Z’ arising from a use of ‘extend’
    6 
    -          instance ‘MinMax a Z Z a’ at tcfail143.hs:12:10-23
    1 
    +tcfail143.hs:30:9: error: [GHC-39999]
    2 
    +    • No instance for ‘MinMax (S Z) Z Z Z’
    3 
    +        arising from a use of ‘extend’
    7 4 
         • In the expression: n1 `extend` n0
    8 5 
           In an equation for ‘t2’: t2 = n1 `extend` n0
    6 
    +

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