GitLab

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

Commits:

c97fd3f5
by Simon Peyton Jones at 2025-10-26T00:07:09+01:00
```
better
```

3 changed files:

compiler/GHC/HsToCore/Binds.hs
compiler/GHC/Tc/Errors/Hole.hs
compiler/GHC/Tc/Types/Evidence.hs

Changes:

@@ -1602,6 +1602,8 @@ ds_hs_wrapper hs_wrap
    where
      go WpHole            k = k $ \e -> e
      go (WpSubType w)     k = go (optSubTypeHsWrapper w) k
 +                             -- See (DSST3) in Note [Deep subsumption and WpSubType]
 +                             --             in GHC.Tc.Types.Evidence
      go (WpTyApp ty)      k = k $ \e -> App e (Type ty)
      go (WpEvLam ev)      k = k $ Lam ev
      go (WpTyLam tv)      k = k $ Lam tv

compiler/GHC/Tc/Errors/Hole.hs

@@ -823,9 +823,11 @@ tcFilterHoleFits limit typed_hole ht@(hole_ty, _) candidates =
      unfoldWrapper :: HsWrapper -> [Type]
      unfoldWrapper = reverse . unfWrp'
 -      where unfWrp' (WpTyApp ty) = [ty]
 -            unfWrp' (WpCompose w1 w2) = unfWrp' w1 ++ unfWrp' w2
 -            unfWrp' _ = []
 +      where
 +        unfWrp' (WpTyApp ty)      = [ty]
 +        unfWrp' (WpSubType w)     = unfWrp' w
 +        unfWrp' (WpCompose w1 w2) = unfWrp' w1 ++ unfWrp' w2
 +        unfWrp' _                  = []
      -- The real work happens here, where we invoke the type checker using

compiler/GHC/Tc/Types/Evidence.hs

@@ -138,7 +138,7 @@ maybeSymCo NotSwapped co = co
  {- Note [Deep subsumption and WpSubType]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  When making DeepSubsumption checks, we may end up with hard-to-spot identity wrappers.
 -For example (#26255) suppose we have
 +For example (#26349) suppose we have
      (forall a. Eq a => a->a) -> Int  <=   (forall a. Eq a => a->a) -> Int
  The two types are equal so we should certainly get an identity wrapper.  But we'll get
  tihs wrapper from `tcSubType`:
@@ -158,11 +158,11 @@ is not sound in general, so we'll end up retaining the lambdas.  Two bad results
    may not be able to make a decent RULE at all, and will fail with "LHS of rule
    is too complicated to desugar (#26255)
 -It'd be nicest to solve the problem at source, by never generating those
 +It'd be ideal to solve the problem at source, by never generating those
  gruesome wrappers in the first place, but we can't do that because
 -* The WpTyLam and WpTyApp are not introduced together in `tcSubType`, so we can't
 -  easily cancel them out.   Even if we have
 +* The WpTyLam and WpTyApp are introduced independently, not together, in `tcSubType`,
 +  so we can't easily cancel them out.   For example, even if we have
       forall a. t1  <=  forall a. t2
    there is no guarantee that these are the "same" a.  E.g.
       forall a b. a -> b -> b   <=   forall x y. y -> x - >x
@@ -171,17 +171,23 @@ gruesome wrappers in the first place, but we can't do that because
  * We have not yet done constraint solving so we don't know what evidence will
    end up in those WpLet bindings.
 -TL;DR we must generate
 -Here's our solution
 +TL;DR we must generate the wrapper and then optimise it way if it turns out
 +that it is a no-op.  Here's our solution
  (DSST1) Tag the wrappers generated from a subtype check with WpSubType. In normal
    wrappers the binders of a WpTyLam or WpEvLam can scope over the "hole" of the
    wrapper -- that is how we introduce type-lambdas and dictionary-lambda into the
    terms!  But in /subtype/ wrappers, these type/dictionary lambdas only scope over
 -  the WpTyApp and WpEvApp nodes in the /same/ wrapper.  That is w
 +  the WpTyApp and WpEvApp nodes in the /same/ wrapper.  That is what justifies us
 +  eta-reducing the type/dictionarly lambdas.
 -(WpSubType wp) means the same as `wp`, but with the added promise that
 -the binders in `wp` do not scope over the hole
 +  In short, (WpSubType wp) means the same as `wp`, but with the added promise that
 +  the binders in `wp` do not scope over the hole
++
 +(DSST2) Avoid creating a WpSubType in the common WpHole case, using `mkWpSubType`.
++
 +(DSST3) When desugaring, try eta-reduction on the payload of a WpSubType.
 +  This is done in `GHC.HsToCore.Binds.dsHsWrapper` by the call to `optSubTypeHsWrapper`.
  -}
  -- We write    wrap :: t1 ~> t2
@@ -190,7 +196,7 @@ data HsWrapper
    = WpHole                      -- The identity coercion
    | WpSubType HsWrapper   -- (WpSubType wp) Means the same as `wp`
 -                          -- But see Note [WpSubType]
 +                          -- See Note [Deep subsumption and WpSubType] (DSST1)
    | WpCompose HsWrapper HsWrapper
         -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]
@@ -299,6 +305,7 @@ mkWpFun w_arg  w_res  t1 t2 = WpFun w_arg w_res t1 t2
    -- [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
  mkWpSubType :: HsWrapper -> HsWrapper
 +-- See (DSST2) in Note [Deep subsumption and WpSubType]
  mkWpSubType WpHole      = WpHole
  mkWpSubType (WpCast co) = WpCast co
  mkWpSubType w           = WpSubType w
@@ -393,7 +400,7 @@ hsWrapDictBinders wrap = go wrap
     go (w1 `WpCompose` w2) = go w1 `unionBags` go w2
     go (WpFun _ w _ _)     = go w
     go WpHole              = emptyBag
 -   go (WpSubType {})      = emptyBag  -- See Note [WpSubType]
 +   go (WpSubType {})      = emptyBag  -- See Note [Deep subsumption and WpSubType]
     go (WpCast  {})        = emptyBag
     go (WpEvApp {})        = emptyBag
     go (WpTyLam {})        = emptyBag
@@ -420,9 +427,11 @@ collectHsWrapBinders wrap = go wrap []
  optSubTypeHsWrapper :: HsWrapper -> HsWrapper
 +-- This optimiser is used only on the payload of WpSubType
 +-- It finds cases where the entire wrapper is a no-op
 +-- See (DSST3) in Note [Deep subsumption and WpSubType]
  optSubTypeHsWrapper wrap
 -  = -- pprTrace "optHsWrapper" (vcat [ text "in:" <+> ppr wrap, text "out:" <+> ppr (opt wrap) ]) $
 -    opt wrap
 +  = opt wrap
    where
      opt :: HsWrapper -> HsWrapper
      opt w = foldr (<.>) WpHole (opt1 w [])
@@ -436,18 +445,17 @@ optSubTypeHsWrapper wrap
      opt1 (WpCast co)            ws = opt_co co ws
      opt1 (WpEvLam ev)           ws = opt_ev_lam ev ws
      opt1 (WpTyLam tv)           ws = opt_ty_lam tv ws
 -    opt1 (WpLet binds)          ws = opt_let binds ws
 +    opt1 (WpLet binds)          ws = pushWpLet binds ws
      opt1 (WpFun w1 w2 sty1 ty2) ws = mk_wp_fun (opt w1) (opt w2) sty1 ty2 ws
      opt1 w@(WpTyApp {})         ws = w : ws
      opt1 w@(WpEvApp {})         ws = w : ws
 -    ------------------
 -    opt_let b@(EvBinds bs) ws | isEmptyBag bs = ws
 -                              | otherwise     = WpLet b : ws
 -    opt_let (TcEvBinds {}) _  = pprPanic "optHsWrapper1" (ppr wrap)
+-
      -----------------
      -- (WpTyLam a <+> WpTyApp a <+> w) = w
 +    -- i.e.   /\a. <hole> a   -->  <hole>
 +    -- This is only valid if whatever fills the hole does not mention 'a'
 +    -- But that's guaranteed in subtype-wrappers;
 +    -- see (DSST1) in Note [Deep subsumption and WpSubType]
      opt_ty_lam tv (WpTyApp ty : ws)
        | Just tv' <- getTyVar_maybe ty
        , tv==tv'
@@ -458,15 +466,12 @@ optSubTypeHsWrapper wrap
      opt_ty_lam tv (WpCast co : ws)
        = opt_co (mkHomoForAllCo tv co) (opt_ty_lam tv ws)
 -    opt_ty_lam tv (WpLet bs : ws)
 -      | Just ws' <- pushWpLet bs ws
 -      = opt_ty_lam tv ws'
+-
      opt_ty_lam tv ws
        = WpTyLam tv : ws
      -----------------
      -- (WpEvLam ev <+> WpEvAp ev <+> w) = w
 +    -- Similar notes to WpTyLam
      opt_ev_lam ev (WpEvApp ev_tm : ws)
        | EvExpr (Var ev') <- ev_tm
        , ev == ev'
@@ -481,9 +486,6 @@ optSubTypeHsWrapper wrap
                          (mkNomReflCo ManyTy)
                          (mkRepReflCo (idType ev))
                          co
 -    opt_ev_lam ev (WpLet bs : ws)
 -      | Just ws' <- pushWpLet bs ws
 -      = opt_ev_lam ev ws'
      opt_ev_lam ev ws
        = WpEvLam ev : ws
@@ -505,48 +507,64 @@ optSubTypeHsWrapper wrap
        where
          co_ify co1 co2 = opt_co (mk_wp_fun_co w co1 co2) ws
 -pushWpLet :: TcEvBinds -> [HsWrapper] -> Maybe [HsWrapper]
 +pushWpLet :: TcEvBinds -> [HsWrapper] -> [HsWrapper]
 +-- See if we can transform
 +--    WpLet binds <.> w1 <.> .. <.> wn   -->   w1' <.> .. <.> wn'
 +-- by substitution.
 +-- We do this just for the narrow case when
 +--   - the `binds` are all just v=w, variables only
 +--   - the wi are all WpTyApp, WpEvApp, or WpCast
 +-- This is just enough to get us the eta-reductions that we seek
  pushWpLet tc_ev_binds ws
 -  | EvBinds binds <- tc_ev_binds
 -  , Just env <- evBindIdSwizzle binds
 -  = go env ws
 -  | otherwise
 -  = Nothing
 +  = case tc_ev_binds of
 +      TcEvBinds {} -> pprPanic "pushWpLet" (ppr tc_ev_binds)
 +      EvBinds binds
 +        | isEmptyBag binds
 +        -> ws
 +        | Just env <- ev_bind_swizzle binds
 +        -> case go env ws of
 +              Just ws' -> ws'
 +              Nothing  -> bale_out
 +        | otherwise
 +        -> bale_out
    where
 +    bale_out = WpLet tc_ev_binds : ws
++
      go :: IdEnv Id -> [HsWrapper] -> Maybe [HsWrapper]
      go env (WpCast co  : ws) = do { ws' <- go env ws
                                    ; return (WpCast co  : ws') }
      go env (WpTyApp ty : ws) = do { ws' <- go env ws
                                    ; return (WpTyApp ty : ws') }
      go env (WpEvApp (EvExpr (Var v)) : ws)
 -       = do { v'  <- swizzleId env v
 +       = do { v'  <- swizzle_id env v
              ; ws' <- go env ws
              ; return (WpEvApp (EvExpr (Var v')) : ws') }
      go _ ws = case ws of
                   []    -> Just []
 -                 (_:_) -> Nothing  -- Could not fully eliminate it
 +                 (_:_) -> Nothing  -- Could not fully eliminate the WpLet
 -swizzleId :: IdEnv Id -> Id -> Maybe Id
 --- Nothing <=> ran out of fuel
 --- Shoul
 -swizzleId env v = go 100 v
 -  where
 -    go :: Int -> EvId -> Maybe EvId
 -    go fuel v
 -      | fuel == 0                     = Nothing
 -      | Just v' <- lookupVarEnv env v = go (fuel-1) v'
 -      | otherwise                     = Just v
+-
 -evBindIdSwizzle :: Bag EvBind -> Maybe (IdEnv Id)
 -evBindIdSwizzle evbs = foldl' do_one (Just emptyVarEnv) evbs
 -  where
 -    do_one :: Maybe (IdEnv Id) -> EvBind -> Maybe (IdEnv Id)
 -    do_one Nothing _ = Nothing
 -    do_one (Just swizzle) (EvBind {eb_lhs = bndr, eb_rhs = rhs})
 -      = case rhs of
 -           EvExpr (Var v) -> Just (extendVarEnv swizzle bndr v)
 -           _              -> Nothing
 +    swizzle_id :: IdEnv Id -> Id -> Maybe Id
 +    -- Nothing <=> ran out of fuel
 +    -- This is just belt and braces; we should never build bottom evidence
 +    swizzle_id env v = go 100 v
 +      where
 +        go :: Int -> EvId -> Maybe EvId
 +        go fuel v
 +          | fuel == 0                     = Nothing
 +          | Just v' <- lookupVarEnv env v = go (fuel-1) v'
 +          | otherwise                     = Just v
++
 +    ev_bind_swizzle :: Bag EvBind -> Maybe (IdEnv Id)
 +    -- Succeeds only if the bindings are all var-to-var bindings
 +    ev_bind_swizzle evbs = foldl' do_one (Just emptyVarEnv) evbs
 +      where
 +        do_one :: Maybe (IdEnv Id) -> EvBind -> Maybe (IdEnv Id)
 +        do_one Nothing _ = Nothing
 +        do_one (Just swizzle) (EvBind {eb_lhs = bndr, eb_rhs = rhs})
 +          = case rhs of
 +               EvExpr (Var v) -> Just (extendVarEnv swizzle bndr v)
 +               _              -> Nothing
  {-
  ************************************************************************