Simon Peyton Jones pushed to branch wip/T25440 at Glasgow Haskell Compiler / GHC

Commits:

1 changed file:

Changes:

  • compiler/GHC/Tc/Solver/Equality.hs
    ... ... @@ -1604,7 +1604,7 @@ canEqCanLHSHetero :: CtEvidence -- :: (xi1 :: ki1) ~ (xi2 :: ki2)
    1604 1604 
                       -> TcType -> TcType   -- xi2
    1605 1605 
                       -> TcKind             -- ki2
    1606 1606 
                       -> TcS (StopOrContinue (Either IrredCt EqCt))
    1607 
    -canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 _ps_xi2 ki2
    1607 
    +canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2
    1608 1608 
     -- See Note [Equalities with incompatible kinds]
    1609 1609 
     -- See Note [Kind Equality Orientation]
    1610 1610
    ... ... @@ -1613,60 +1613,63 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 _ps_xi2 ki2
    1613 1613 
     --    NotSwapped:
    1614 1614 
     --        ev      :: (lhs1:ki1) ~r# (xi2:ki2)
    1615 1615 
     --        kind_co :: k11 ~# ki2               -- Same orientation as ev
    1616 
    ---        type_ev :: lhs1 ~r# (xi2 |> sym kind_co)
    1616 
    +--        new_ev  :: lhs1 ~r# (xi2 |> sym kind_co)
    1617 1617 
     --    Swapped
    1618 1618 
     --        ev      :: (xi2:ki2) ~r# (lhs1:ki1)
    1619 1619 
     --        kind_co :: ki2 ~# ki1               -- Same orientation as ev
    1620 
    ---        type_ev :: (xi2 |> kind_co) ~r# lhs1
    1620 
    +--        new_ev  :: (xi2 |> kind_co) ~r# lhs1
    1621 
    +-- Note that we need the `sym` when we are /not/ swapped; hence `mk_sym_co`
    1621 1622
    1622 
    -  = do { (kind_co, rewriters, unifs_happened) <- mk_kind_eq   -- :: ki1 ~N ki2
    1623 
    -       ; if unifs_happened
    1624 
    -              -- Unifications happened, so start again to do the zonking
    1625 
    -              -- Otherwise we might put something in the inert set that isn't inert
    1626 
    -         then startAgainWith (mkNonCanonical ev)
    1627 
    -         else
    1628 
    -    assertPpr (not (isEmptyRewriterSet rewriters)) (ppr ev) $
    1629 
    -      -- The rewriter set won't be empty because the two kinds differ, and there
    1630 
    -      -- are no unifications, so we must have emitted one or more constraints
    1631 
    -    do { let lhs_redn = mkReflRedn role ps_xi1
    1632 
    -             rhs_redn = mkGReflRightRedn role xi2 mb_sym_kind_co
    1633 
    -             mb_sym_kind_co = case swapped of
    1634 
    -                                NotSwapped -> mkSymCo kind_co
    1635 
    -                                IsSwapped  -> kind_co
    1636 
    -
    1637 
    -       ; traceTcS "Hetero equality gives rise to kind equality"
    1638 
    -           (ppr swapped $$
    1639 
    -            ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ])
    1640 
    -       ; type_ev <- rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn
    1641 
    -
    1642 
    -       -- The rewritten equality is non-canonical, so put it straight in the Irreds
    1643 
    -       ; finishCanWithIrred (NonCanonicalReason (cteProblem cteCoercionHole)) type_ev } }
    1644 
    -
    1645 
    ---       ; let new_xi2 = mkCastTy ps_xi2 mb_sym_kind_co
    1646 
    ---       ; canEqCanLHSHomo type_ev eq_rel NotSwapped lhs1 ps_xi1 new_xi2 new_xi2 }}
    1647 
    -
    1648 
    -  where
    1649 
    -    mk_kind_eq :: TcS (CoercionN, RewriterSet, Bool)
    1650 
    -    -- Returned kind_co has kind (k1 ~ k2) if NotSwapped, (k2 ~ k1) if Swapped
    1651 
    -    -- Returned Bool = True if unifications happened, so we should retry
    1652 
    -    mk_kind_eq = case ev of
    1623 
    +  = case ev of
    1653 1624 
           CtGiven (GivenCt { ctev_evar = evar, ctev_loc = loc })
    1654 1625 
             -> do { let kind_co  = mkKindCo (mkCoVarCo evar)
    1655 1626 
                         pred_ty  = unSwap swapped mkNomEqPred ki1 ki2
    1656 1627 
                         kind_loc = mkKindEqLoc xi1 xi2 loc
    1657 1628 
                   ; kind_ev <- newGivenEvVar kind_loc (pred_ty, evCoercion kind_co)
    1658 1629 
                   ; emitWorkNC [CtGiven kind_ev]
    1659 
    -              ; return (givenCtEvCoercion kind_ev, emptyRewriterSet, False) }
    1630 
    +              ; let kind_co = givenCtEvCoercion kind_ev
    1631 
    +                    new_xi2 = mkCastTy ps_xi2 (mk_sym_co kind_co)
    1632 
    +              ; new_ev <- do_rewrite emptyRewriterSet kind_co
    1633 
    +                -- In the Given case, `new_ev` is canonical, so carry on
    1634 
    +              ; canEqCanLHSHomo new_ev eq_rel NotSwapped lhs1 ps_xi1 new_xi2 new_xi2 }
    1660 1635
    1661 1636 
           CtWanted {}
    1662 
    -        -> do { (kind_co, cts, unifs) <- wrapUnifierTcS ev Nominal $ \uenv ->
    1663 
    -                                         let uenv' = updUEnvLoc uenv (mkKindEqLoc xi1 xi2)
    1664 
    -                                         in unSwap swapped (uType uenv') ki1 ki2
    1665 
    -              ; return (kind_co, rewriterSetFromCts cts, not (null unifs)) }
    1666 
    -
    1637 
    +         -> do { (kind_co, cts, unifs) <- wrapUnifierTcS ev Nominal $ \uenv ->
    1638 
    +                                          let uenv' = updUEnvLoc uenv (mkKindEqLoc xi1 xi2)
    1639 
    +                                          in unSwap swapped (uType uenv') ki1 ki2
    1640 
    +               ; if not (null unifs)
    1641 
    +                 then -- Unifications happened, so start again to do the zonking
    1642 
    +                      -- Otherwise we might put something in the inert set that isn't inert
    1643 
    +                      startAgainWith (mkNonCanonical ev)
    1644 
    +                 else
    1645 
    +
    1646 
    +            assertPpr (not (isEmptyCts cts)) (ppr ev $$ ppr ki1 $$ ppr ki2) $
    1647 
    +              -- The constraints won't be empty because the two kinds differ, and there
    1648 
    +              -- are no unifications, so we must have emitted one or more constraints
    1649 
    +            do { new_ev <- do_rewrite (rewriterSetFromCts cts) kind_co
    1650 
    +                 -- The rewritten equality `new_ev` is non-canonical,
    1651 
    +                 -- so put it straight in the Irreds
    1652 
    +               ; finishCanWithIrred (NonCanonicalReason (cteProblem cteCoercionHole)) new_ev } }
    1653 
    +  where
    1667 1654 
         xi1  = canEqLHSType lhs1
    1668 1655 
         role = eqRelRole eq_rel
    1669 1656
    1657 
    +    -- Apply mkSymCo when /not/ swapped
    1658 
    +    mk_sym_co co = case swapped of
    1659 
    +                      NotSwapped -> mkSymCo co
    1660 
    +                      IsSwapped  -> co
    1661 
    +
    1662 
    +    do_rewrite rewriters kind_co
    1663 
    +      = do { traceTcS "Hetero equality gives rise to kind equality"
    1664 
    +                 (ppr swapped $$
    1665 
    +                  ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ])
    1666 
    +           ; rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn }
    1667 
    +      where
    1668 
    +        -- kind_co :: ki1 ~N ki2
    1669 
    +        lhs_redn    = mkReflRedn role ps_xi1
    1670 
    +        rhs_redn    = mkGReflRightRedn role xi2 (mk_sym_co kind_co)
    1671 
    +
    1672 
    +
    1670 1673 
     canEqCanLHSHomo :: CtEvidence          -- lhs ~ rhs
    1671 1674 
                                            -- or, if swapped: rhs ~ lhs
    1672 1675 
                     -> EqRel -> SwapFlag

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