GitLab

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

Commits:

ce4975ed
by Simon Peyton Jones at 2025-10-25T12:51:24+01:00
```
Better now

Added WpSubType
```

5 changed files:

compiler/GHC/Hs/Syn/Type.hs
compiler/GHC/HsToCore/Binds.hs
compiler/GHC/Tc/Types/Evidence.hs
compiler/GHC/Tc/Utils/Unify.hs
compiler/GHC/Tc/Zonk/Type.hs

Changes:

@@ -191,6 +191,7 @@ hsWrapperType :: HsWrapper -> Type -> Type
  hsWrapperType wrap ty = prTypeType $ go wrap (ty,[])
    where
      go WpHole              = id
 +    go (WpSubType w)       = go w
      go (w1 `WpCompose` w2) = go w1 . go w2
      go (WpFun _ w2 (Scaled m exp_arg) _) = liftPRType $ \t ->
        let act_res = funResultTy t

compiler/GHC/HsToCore/Binds.hs

@@ -1598,9 +1598,10 @@ ds_hs_wrapper :: HsWrapper
                -> ((CoreExpr -> CoreExpr) -> DsM a)
                -> DsM a
  ds_hs_wrapper hs_wrap
 -  = go (optHsWrapper hs_wrap)
 +  = go hs_wrap
    where
      go WpHole            k = k $ \e -> e
 +    go (WpSubType w)     k = go (optSubTypeHsWrapper w) k
      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/Types/Evidence.hs

@@ -8,11 +8,11 @@ module GHC.Tc.Types.Evidence (
    -- * HsWrapper
    HsWrapper(..),
    (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpForAllCast,
 -  mkWpEvLams, mkWpLet, mkWpFun, mkWpCastN, mkWpCastR, mkWpEta,
 +  mkWpEvLams, mkWpLet, mkWpFun, mkWpCastN, mkWpCastR, mkWpEta, mkWpSubType,
    collectHsWrapBinders,
    idHsWrapper, isIdHsWrapper,
    pprHsWrapper, hsWrapDictBinders,
 -  optHsWrapper,
 +  optSubTypeHsWrapper,
    -- * Evidence bindings
    TcEvBinds(..), EvBindsVar(..),
@@ -135,11 +135,20 @@ maybeSymCo NotSwapped co = co
  ************************************************************************
  -}
 +{- Note [WpSubType]
 +~~~~~~~~~~~~~~~~~~~
 +(WpSubType wp) means the same as `wp`, but with the added promise that
 +the binders in `wp` do not scope over the hole
 +-}
++
  -- We write    wrap :: t1 ~> t2
  -- if       wrap[ e::t1 ] :: t2
  data HsWrapper
    = WpHole                      -- The identity coercion
 +  | WpSubType HsWrapper   -- (WpSubType wp) Means the same as `wp`
 +                          -- But see Note [WpSubType]
++
    | WpCompose HsWrapper HsWrapper
         -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]
         --
@@ -246,6 +255,11 @@ mkWpFun w_arg  w_res  t1 t2 = WpFun w_arg w_res t1 t2
    -- Unfortunately, we can't check this with an assertion here, because of
    -- [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
 +mkWpSubType :: HsWrapper -> HsWrapper
 +mkWpSubType WpHole      = WpHole
 +mkWpSubType (WpCast co) = WpCast co
 +mkWpSubType w           = WpSubType w
++
  mkWpEta :: Type -> [Id] -> HsWrapper -> HsWrapper
  -- (mkWpEta [x1, x2] wrap) [e]
  --   = \x1. \x2.  wrap[e x1 x2]
@@ -336,6 +350,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 (WpCast  {})        = emptyBag
     go (WpEvApp {})        = emptyBag
     go (WpTyLam {})        = emptyBag
@@ -351,6 +366,7 @@ collectHsWrapBinders wrap = go wrap []
      go :: HsWrapper -> [HsWrapper] -> ([Var], HsWrapper)
      go (WpEvLam v)       wraps = add_lam v (gos wraps)
      go (WpTyLam v)       wraps = add_lam v (gos wraps)
 +    go (WpSubType w)     wraps = go w wraps
      go (WpCompose w1 w2) wraps = go w1 (w2:wraps)
      go wrap              wraps = ([], foldl' (<.>) wrap wraps)
@@ -360,124 +376,113 @@ collectHsWrapBinders wrap = go wrap []
      add_lam v (vs,w) = (v:vs, w)
 -optHsWrapper :: HsWrapper -> HsWrapper
 -optHsWrapper wrap
 -  = foldr (<.>) WpHole (norm wrap [])
 -    -- let wrap' = foldr (<.>) WpHole (norm wrap [])
 -    -- in pprTrace "optHsWrapper" (vcat [ text "in:" <+> ppr wrap, text "out:" <+> ppr wrap' ]) $
 -    --    wrap'
 +optSubTypeHsWrapper :: HsWrapper -> HsWrapper
 +optSubTypeHsWrapper wrap
 +  = pprTrace "optHsWrapper" (vcat [ text "in:" <+> ppr wrap, text "out:" <+> ppr (opt wrap) ]) $
 +    opt wrap
    where
 -    norm :: HsWrapper -> [HsWrapper] -> [HsWrapper]
 -    -- norm w ws = w <.> (foldr <.> WpHole ws)
 -    -- INVARIANT: ws:[HsWrapper] is normalised
 -    norm WpHole                 ws = ws
 -    norm (w1 `WpCompose` w2)    ws = norm w1 (norm w2 ws)
 -    norm (WpCast co)            ws = norm_co co ws
 -    norm (WpEvLam ev)           ws = norm_ev_lam ev ws
 -    norm (WpTyLam tv)           ws = norm_ty_lam tv ws
 -    norm (WpLet binds)          ws = norm_let binds ws
 -    norm (WpFun w1 w2 sty1 ty2) ws = norm_fun w1 w2 sty1 ty2 ws
 -    norm w@(WpTyApp {})         ws = w : ws
 -    norm w@(WpEvApp {})         ws = w : ws
 +    opt :: HsWrapper -> HsWrapper
 +    opt w = foldr (<.>) WpHole (opt1 w [])
++
 +    opt1 :: HsWrapper -> [HsWrapper] -> [HsWrapper]
 +    -- opt1 w ws = w <.> (foldr <.> WpHole ws)
 +    -- INVARIANT: ws:[HsWrapper] is optimised
 +    opt1 WpHole                 ws = ws
 +    opt1 (WpSubType w)          ws = opt1 w ws
 +    opt1 (w1 `WpCompose` w2)    ws = opt1 w1 (opt1 w2 ws)
 +    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 (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
      ------------------
 -    norm_let b@(EvBinds bs) ws | isEmptyBag bs = ws
 -                               | otherwise     = WpLet b : ws
 -    norm_let (TcEvBinds {}) _  = pprPanic "optHsWrapper1" (ppr wrap)
 +    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
 -    norm_ty_lam tv (WpTyApp ty : ws)
 +    opt_ty_lam tv (WpTyApp ty : ws)
        | Just tv' <- getTyVar_maybe ty
        , tv==tv'
        = ws
      -- (WpTyLam a <+> WpCastCo co <+> w)
      --    = WpCast (ForAllCo a co) (WpTyLam <.> w)
 -    norm_ty_lam tv (WpCast co : ws)
 -      = norm_co (mkHomoForAllCo tv co) (norm_ty_lam tv ws)
 +    opt_ty_lam tv (WpCast co : ws)
 +      = opt_co (mkHomoForAllCo tv co) (opt_ty_lam tv ws)
 -    norm_ty_lam tv (WpLet bs : ws)
 +    opt_ty_lam tv (WpLet bs : ws)
        | Just ws' <- pushWpLet bs ws
 -      = norm_ty_lam tv ws'
 +      = opt_ty_lam tv ws'
 -    norm_ty_lam tv ws
 +    opt_ty_lam tv ws
        = WpTyLam tv : ws
      -----------------
      -- (WpEvLam ev <+> WpEvAp ev <+> w) = w
 -    norm_ev_lam ev (WpEvApp ev_tm : ws)
 +    opt_ev_lam ev (WpEvApp ev_tm : ws)
        | EvExpr (Var ev') <- ev_tm
        , ev == ev'
        = ws
      -- (WpEvLam ev <.> WpCast co <.> w)
      --    = WpCast (FunCo ev co) (WpEvLam <.> w)
 -    norm_ev_lam ev (WpCast co : ws)
 -      = norm_co fun_co (norm_ev_lam ev ws)
 +    opt_ev_lam ev (WpCast co : ws)
 +      = opt_co fun_co (opt_ev_lam ev ws)
        where
          fun_co = mkFunCo Representational FTF_C_T
                          (mkNomReflCo ManyTy)
                          (mkRepReflCo (idType ev))
                          co
 -    norm_ev_lam ev (WpLet bs : ws)
 +    opt_ev_lam ev (WpLet bs : ws)
        | Just ws' <- pushWpLet bs ws
 -      = norm_ev_lam ev ws'
 +      = opt_ev_lam ev ws'
 -    norm_ev_lam ev ws
 +    opt_ev_lam ev ws
        = WpEvLam ev : ws
      -----------------
      -- WpCast co <.> WpCast co' <+> ws = WpCast (co;co') ws
 -    norm_co co (WpCast co' : ws)     = norm_co (co `mkTransCo` co') ws
 -    norm_co co ws | isReflexiveCo co = ws
 -                  | otherwise        = WpCast co : ws
 +    opt_co co (WpCast co' : ws)     = opt_co (co `mkTransCo` co') ws
 +    opt_co co ws | isReflexiveCo co = ws
 +                 | otherwise        = WpCast co : ws
      ------------------
 -    norm_fun w1 w2 (Scaled w t1) t2 ws
 -      = case (optHsWrapper w1, optHsWrapper w2) of
 +    mk_wp_fun w1 w2 sty1@(Scaled w t1) ty2 ws
 +      = case (w1, w2) of
            (WpHole,     WpHole)     -> ws
 -          (WpLet {},   WpHole)     -> ws
            (WpHole,     WpCast co2) -> co_ify (mkRepReflCo t1) co2
 -          (WpCast co1, WpHole)     -> co_ify (mkSymCo co1)    (mkRepReflCo t2)
 +          (WpCast co1, WpHole)     -> co_ify (mkSymCo co1)    (mkRepReflCo ty2)
            (WpCast co1, WpCast co2) -> co_ify (mkSymCo co1)    co2
 -          (w1',        w2')        -> WpFun w1' w2' (Scaled w t1) t2 : ws
 +          (w1',        w2')        -> WpFun w1' w2' sty1 ty2 : ws
        where
 -        co_ify co1 co2 = norm_co (mk_wp_fun_co w co1 co2) ws
 +        co_ify co1 co2 = opt_co (mk_wp_fun_co w co1 co2) ws
  pushWpLet :: TcEvBinds -> [HsWrapper] -> Maybe [HsWrapper]
  pushWpLet tc_ev_binds ws
    | EvBinds binds <- tc_ev_binds
    , Just env <- evBindIdSwizzle binds
 -  = case go env ws of
 -         WpLet {} : _  -> Nothing
 -         ws'           -> Just ws'
 +  = go env ws
    | otherwise
    = Nothing
    where
 -    go :: IdEnv Id -> [HsWrapper] -> [HsWrapper]
 -    go env (WpTyApp ty : ws') = WpTyApp ty : go env ws'
 -    go env (WpCast co  : ws') = WpCast co  : go env ws'
 -    go env (WpTyLam tv : ws')
 -       | not (tv_captures env tv)
 -       = WpTyLam tv : go env ws'
+-
 -    go env (WpEvLam ev : ws')
 -       | not (ev `elemVarEnv` env)   -- `ev` must not be in the domain
 -       , not (anyVarEnv (== ev) env) --      or range of `env`
 -       = WpEvLam ev : go env ws'
+-
 -    go env (WpEvApp (EvExpr (Var v)) : ws')
 -       | Just v' <- swizzleId env v
 -       = WpEvApp (EvExpr (Var v')) : go env ws'
+-
 -    go _ ws = WpLet tc_ev_binds : ws
+-
 -    tv_captures :: IdEnv Id -> TyVar -> Bool
 -    tv_captures env tv = anyVarEnv bad env
 -        where
 -          bad id = anyFreeVarsOfType (== tv) (idType id)
+-
 +    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
 +            ; ws' <- go env ws
 +            ; return (WpEvApp (EvExpr (Var v')) : ws') }
++
 +    go _ ws = case ws of
 +                 []    -> Just []
 +                 (_:_) -> Nothing  -- Could not fully eliminate it
  swizzleId :: IdEnv Id -> Id -> Maybe Id
  -- Nothing <=> ran out of fuel
@@ -1158,7 +1163,8 @@ pprHsWrapper wrap pp_thing_inside
      -- True  <=> appears in function application position
      -- False <=> appears as body of let or lambda
      help it WpHole             = it
 -    help it (WpCompose f1 f2)  = help (help it f2) f1
 +    help it (WpCompose w1 w2)  = help (help it w2) w1
 +    help it (WpSubType w)      = no_parens $ text "subtype" <> braces (help it w False)
      help it (WpFun f1 f2 (Scaled w t1) _) = add_parens $ text "\\(x" <> dcolon <> brackets (ppr w) <> ppr t1 <> text ")." <+>
                                              help (\_ -> it True <+> help (\_ -> text "x") f1 True) f2 False
      help it (WpCast co)   = add_parens $ sep [it False, nest 2 (text "|>"

compiler/GHC/Tc/Utils/Unify.hs

@@ -1426,11 +1426,12 @@ tcSubTypeDS :: HsExpr GhcRn
                             -- DeepSubsumption <=> when checking, this type
                             --                     is deeply skolemised
              -> TcM HsWrapper
 --- Only one call site, in GHC.Tc.Gen.App.tcApp
 +-- Only one call site, in GHC.Tc.Gen.App.checkResultTy
  tcSubTypeDS rn_expr act_rho exp_rho
 -  = tc_sub_type_deep Top (unifyExprType rn_expr) orig GenSigCtxt act_rho exp_rho
 -  where
 -    orig = exprCtOrigin rn_expr
 +  = do { wrap <- tc_sub_type_deep Top (unifyExprType rn_expr)
 +                                  (exprCtOrigin rn_expr)
 +                                  GenSigCtxt act_rho exp_rho
 +       ; return (mkWpSubType wrap) }
  ---------------
@@ -1503,7 +1504,8 @@ tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN)  -- How to unify
  ----------------------
  tc_sub_type unify inst_orig ctxt ty_actual ty_expected
    = do { ds_flag <- getDeepSubsumptionFlag
 -       ; tc_sub_type_ds Top ds_flag unify inst_orig ctxt ty_actual ty_expected }
 +       ; wrap <- tc_sub_type_ds Top ds_flag unify inst_orig ctxt ty_actual ty_expected
 +       ; return (mkWpSubType wrap) }
  ----------------------
  tc_sub_type_ds :: Position p -- ^ position in the type (for error messages only)

compiler/GHC/Tc/Zonk/Type.hs

@@ -1231,6 +1231,8 @@ zonk_cmd_top (HsCmdTop (CmdTopTc stack_tys ty ids) cmd)
  -------------------------------------------------------------------------
  zonkCoFn :: HsWrapper -> ZonkBndrTcM HsWrapper
  zonkCoFn WpHole   = return WpHole
 +zonkCoFn (WpSubType w)     = do { w' <- zonkCoFn w
 +                                ; return (WpSubType w') }
  zonkCoFn (WpCompose c1 c2) = do { c1' <- zonkCoFn c1
                                  ; c2' <- zonkCoFn c2
                                  ; return (WpCompose c1' c2') }