Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC

Commits:

17 changed files:

Changes:

  • compiler/GHC/Core/Coercion.hs
    ... ... @@ -41,7 +41,8 @@ module GHC.Core.Coercion (
    41 41 
             mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo,
    42 42 
             mkFunCo, mkFunCo2, mkFunCoNoFTF, mkFunResCo,
    43 43 
             mkNakedFunCo,
    44 
    -        mkNakedForAllCo, mkForAllCo, mkForAllVisCos, mkHomoForAllCos,
    44 
    +        mkNakedForAllCo, mkForAllCo, mkForAllVisCos,
    45 
    +        mkHomoForAllCo, mkHomoForAllCos,
    45 46 
             mkPhantomCo, mkAxiomCo,
    46 47 
             mkHoleCo, mkUnivCo, mkSubCo,
    47 48 
             mkProofIrrelCo,
    ... ... @@ -980,7 +981,7 @@ mkForAllCo v visL visR kind_co co
    980 981 
       = mkReflCo r (mkTyCoForAllTy v visL ty)
    981 982
    982 983 
       | otherwise
    983 
    -  = mkForAllCo_NoRefl v visL visR kind_co co
    984 
    +  = mk_forall_co v visL visR kind_co co
    984 985
    985 986 
     -- mkForAllVisCos [tv{vis}] constructs a cast
    986 987 
     --   forall tv. res  ~R#   forall tv{vis} res`.
    ... ... @@ -1000,14 +1001,26 @@ mkHomoForAllCos vs orig_co
    1000 1001 
       = foldr go orig_co vs
    1001 1002 
       where
    1002 1003 
         go :: ForAllTyBinder -> Coercion -> Coercion
    1003 
    -    go (Bndr var vis) = mkForAllCo_NoRefl var vis vis MRefl
    1004 
    -
    1005 
    --- | Like 'mkForAllCo', but there is no need to check that the inner coercion isn't Refl;
    1006 
    ---   the caller has done that. (For example, it is guaranteed in 'mkHomoForAllCos'.)
    1007 
    --- The kind of the tycovar should be the left-hand kind of the kind coercion.
    1008 
    -mkForAllCo_NoRefl :: TyCoVar -> ForAllTyFlag -> ForAllTyFlag
    1009 
    -                  -> KindMCoercion -> Coercion -> Coercion
    1010 
    -mkForAllCo_NoRefl tcv visL visR kind_co co
    1004 
    +    go (Bndr var vis) co = mk_forall_co var vis vis MRefl co
    1005 
    +
    1006 
    +mkHomoForAllCo :: TyVar -> Coercion -> Coercion
    1007 
    +-- Specialised for a single TyVar,
    1008 
    +--    and visibility of coreTyLamForAllTyFlag
    1009 
    +mkHomoForAllCo tv orig_co
    1010 
    +  | Just (ty, r) <- isReflCo_maybe orig_co
    1011 
    +  = mkReflCo r (mkForAllTy (Bndr tv vis) ty)
    1012 
    +  | otherwise
    1013 
    +  = mk_forall_co tv vis vis MRefl orig_co
    1014 
    +  where
    1015 
    +    vis  = coreTyLamForAllTyFlag
    1016 
    +
    1017 
    +-- | `mk_forall_co` just builds a ForAllCo.
    1018 
    +-- With debug on, it checks invariants (e.g. he kind of the tycovar should
    1019 
    +--   be the left-hand kind of the kind coercion).
    1020 
    +-- Callers should have done any isReflCo short-cutting.
    1021 
    +mk_forall_co :: TyCoVar -> ForAllTyFlag -> ForAllTyFlag
    1022 
    +             -> KindMCoercion -> Coercion -> Coercion
    1023 
    +mk_forall_co tcv visL visR kind_co co
    1011 1024 
       = assertGoodForAllCo tcv visL visR kind_co co $
    1012 1025 
         assertPpr (not (isReflCo co && isReflMCo kind_co && visL == visR)) (ppr co) $
    1013 1026 
         ForAllCo { fco_tcv = tcv, fco_visL = visL, fco_visR = visR
    ... ... @@ -1769,7 +1782,7 @@ mkPiCos r vs co = foldr (mkPiCo r) co vs
    1769 1782 
     -- | Make a forall 'Coercion', where both types related by the coercion
    1770 1783 
     -- are quantified over the same variable.
    1771 1784 
     mkPiCo  :: Role -> Var -> Coercion -> Coercion
    1772 
    -mkPiCo r v co | isTyVar v = mkHomoForAllCos [Bndr v coreTyLamForAllTyFlag] co
    1785 
    +mkPiCo r v co | isTyVar v = mkHomoForAllCo v co
    1773 1786 
                   | isCoVar v = assert (not (v `elemVarSet` tyCoVarsOfCo co)) $
    1774 1787 
                       -- We didn't call mkForAllCo here because if v does not appear
    1775 1788 
                       -- in co, the argument coercion will be nominal. But here we

  • compiler/GHC/Hs/Syn/Type.hs
    ... ... @@ -187,11 +187,13 @@ liftPRType :: (Type -> Type) -> PRType -> PRType
    187 187 
     liftPRType f pty = (f (prTypeType pty), [])
    188 188
    189 189 
     hsWrapperType :: HsWrapper -> Type -> Type
    190 
    +-- Return the type of (WrapExpr wrap e), given that e :: ty
    190 191 
     hsWrapperType wrap ty = prTypeType $ go wrap (ty,[])
    191 192 
       where
    192 193 
         go WpHole              = id
    194 
    +    go (WpSubType w)       = go w
    193 195 
         go (w1 `WpCompose` w2) = go w1 . go w2
    194 
    -    go (WpFun _ w2 (Scaled m exp_arg)) = liftPRType $ \t ->
    196 
    +    go (WpFun _ w2 (Scaled m exp_arg) _) = liftPRType $ \t ->
    195 197 
           let act_res = funResultTy t
    196 198 
               exp_res = hsWrapperType w2 act_res
    197 199 
           in mkFunctionType m exp_arg exp_res

  • compiler/GHC/HsToCore/Binds.hs
    ... ... @@ -1597,9 +1597,13 @@ dsHsWrapper hs_wrap thing_inside
    1597 1597 
     ds_hs_wrapper :: HsWrapper
    1598 1598 
                   -> ((CoreExpr -> CoreExpr) -> DsM a)
    1599 1599 
                   -> DsM a
    1600 
    -ds_hs_wrapper wrap = go wrap
    1600 
    +ds_hs_wrapper hs_wrap
    1601 
    +  = go hs_wrap
    1601 1602 
       where
    1602 1603 
         go WpHole            k = k $ \e -> e
    1604 
    +    go (WpSubType w)     k = go (optSubTypeHsWrapper w) k
    1605 
    +                             -- See (DSST3) in Note [Deep subsumption and WpSubType]
    1606 
    +                             --             in GHC.Tc.Types.Evidence
    1603 1607 
         go (WpTyApp ty)      k = k $ \e -> App e (Type ty)
    1604 1608 
         go (WpEvLam ev)      k = k $ Lam ev
    1605 1609 
         go (WpTyLam tv)      k = k $ Lam tv
    ... ... @@ -1612,13 +1616,13 @@ ds_hs_wrapper wrap = go wrap
    1612 1616 
         go (WpCompose c1 c2) k = go c1 $ \w1 ->
    1613 1617 
                                  go c2 $ \w2 ->
    1614 1618 
                                  k (w1 . w2)
    1615 
    -    go (WpFun c1 c2 st)  k = -- See Note [Desugaring WpFun]
    1616 
    -                             do { x <- newSysLocalDs st
    1617 
    -                                ; go c1 $ \w1 ->
    1618 
    -                                  go c2 $ \w2 ->
    1619 
    -                                  let app f a = mkCoreApp (text "dsHsWrapper") f a
    1620 
    -                                      arg     = w1 (Var x)
    1621 
    -                                  in k (\e -> (Lam x (w2 (app e arg)))) }
    1619 
    +    go (WpFun c1 c2 st _) k = -- See Note [Desugaring WpFun]
    1620 
    +                              do { x <- newSysLocalDs st
    1621 
    +                                 ; go c1 $ \w1 ->
    1622 
    +                                   go c2 $ \w2 ->
    1623 
    +                                   let app f a = mkCoreApp (text "dsHsWrapper") f a
    1624 
    +                                       arg     = w1 (Var x)
    1625 
    +                                   in k (\e -> (Lam x (w2 (app e arg)))) }
    1622 1626
    1623 1627 
     --------------------------------------
    1624 1628 
     dsTcEvBinds_s :: [TcEvBinds] -> ([CoreBind] -> DsM a) -> DsM a

  • compiler/GHC/HsToCore/Match.hs
    ... ... @@ -1240,7 +1240,7 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2
    1240 1240 
         --        equating different ways of writing a coercion)
    1241 1241 
         wrap WpHole WpHole = True
    1242 1242 
         wrap (WpCompose w1 w2) (WpCompose w1' w2') = wrap w1 w1' && wrap w2 w2'
    1243 
    -    wrap (WpFun w1 w2 _)   (WpFun w1' w2' _)   = wrap w1 w1' && wrap w2 w2'
    1243 
    +    wrap (WpFun w1 w2 _ _) (WpFun w1' w2' _ _) = wrap w1 w1' && wrap w2 w2'
    1244 1244 
         wrap (WpCast co)       (WpCast co')        = co `eqCoercion` co'
    1245 1245 
         wrap (WpEvApp et1)     (WpEvApp et2)       = et1 `ev_term` et2
    1246 1246 
         wrap (WpTyApp t)       (WpTyApp t')        = eqType t t'

  • compiler/GHC/Iface/Ext/Ast.hs
    ... ... @@ -696,7 +696,7 @@ instance ToHie (LocatedA HsWrapper) where
    696 696 
             (WpLet bs)      -> toHie $ EvBindContext (mkScope osp) (getRealSpanA osp) (L osp bs)
    697 697 
             (WpCompose a b) -> concatM $
    698 698 
               [toHie (L osp a), toHie (L osp b)]
    699 
    -        (WpFun a b _)   -> concatM $
    699 
    +        (WpFun a b _ _) -> concatM $
    700 700 
               [toHie (L osp a), toHie (L osp b)]
    701 701 
             (WpEvLam a) ->
    702 702 
               toHie $ C (EvidenceVarBind EvWrapperBind (mkScope osp) (getRealSpanA osp))

  • compiler/GHC/Tc/Errors/Hole.hs
    ... ... @@ -823,9 +823,11 @@ tcFilterHoleFits limit typed_hole ht@(hole_ty, _) candidates =
    823 823
    824 824 
         unfoldWrapper :: HsWrapper -> [Type]
    825 825 
         unfoldWrapper = reverse . unfWrp'
    826 
    -      where unfWrp' (WpTyApp ty) = [ty]
    827 
    -            unfWrp' (WpCompose w1 w2) = unfWrp' w1 ++ unfWrp' w2
    828 
    -            unfWrp' _ = []
    826 
    +      where
    827 
    +        unfWrp' (WpTyApp ty)      = [ty]
    828 
    +        unfWrp' (WpSubType w)     = unfWrp' w
    829 
    +        unfWrp' (WpCompose w1 w2) = unfWrp' w1 ++ unfWrp' w2
    830 
    +        unfWrp' _                  = []
    829 831
    830 832
    831 833 
         -- The real work happens here, where we invoke the type checker using

  • compiler/GHC/Tc/Gen/App.hs
    ... ... @@ -794,7 +794,7 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
    794 794 
           = do { let herald = case fun_ctxt of
    795 795 
                                  VAExpansion (OrigStmt{}) _ _ -> ExpectedFunTySyntaxOp DoOrigin tc_fun
    796 796 
                                  _ ->  ExpectedFunTyArg (HsExprTcThing tc_fun) (unLoc arg)
    797 
    -           ; (wrap, arg_ty, res_ty) <-
    797 
    +           ; (fun_co, arg_ty, res_ty) <-
    798 798 
                     -- NB: matchActualFunTy does the rep-poly check.
    799 799 
                     -- For example, suppose we have f :: forall r (a::TYPE r). a -> Int
    800 800 
                     -- In an application (f x), we need 'x' to have a fixed runtime
    ... ... @@ -805,7 +805,7 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
    805 805 
                       (n_val_args, fun_sigma) fun_ty
    806 806
    807 807 
                ; arg' <- quickLookArg do_ql ctxt arg arg_ty
    808 
    -           ; let acc' = arg' : addArgWrap wrap acc
    808 
    +           ; let acc' = arg' : addArgWrap (mkWpCastN fun_co) acc
    809 809 
                ; go (pos+1) acc' res_ty rest_args }
    810 810
    811 811 
         new_arg_ty :: LHsExpr GhcRn -> Int -> TcM (Scaled TcType)

  • compiler/GHC/Tc/Gen/Head.hs
    ... ... @@ -765,13 +765,13 @@ tcInferOverLit lit@(OverLit { ol_val = val
    765 765 
                thing    = NameThing from_name
    766 766 
                mb_thing = Just thing
    767 767 
                herald   = ExpectedFunTyArg thing (HsLit noExtField hs_lit)
    768 
    -       ; (wrap2, sarg_ty, res_ty) <- matchActualFunTy herald mb_thing (1, from_ty) from_ty
    768 
    +       ; (co2, sarg_ty, res_ty) <- matchActualFunTy herald mb_thing (1, from_ty) from_ty
    769 769
    770 770 
            ; co <- unifyType mb_thing (hsLitType hs_lit) (scaledThing sarg_ty)
    771 771 
            -- See Note [Source locations for implicit function calls] in GHC.Iface.Ext.Ast
    772 772 
            ; let lit_expr = L (l2l loc) $ mkHsWrapCo co $
    773 773 
                             HsLit noExtField hs_lit
    774 
    -             from_expr = mkHsWrap (wrap2 <.> wrap1) $
    774 
    +             from_expr = mkHsWrap (mkWpCastN co2 <.> wrap1) $
    775 775 
                              mkHsVar (L loc from_id)
    776 776 
                  witness = HsApp noExtField (L (l2l loc) from_expr) lit_expr
    777 777 
                  lit' = OverLit { ol_val = val

  • compiler/GHC/Tc/Gen/Pat.hs
    ... ... @@ -699,7 +699,7 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
    699 699
    700 700 
              -- Expression must be a function
    701 701 
             ; let herald = ExpectedFunTyViewPat $ unLoc expr
    702 
    -        ; (expr_wrap1, Scaled _mult inf_arg_ty, inf_res_sigma)
    702 
    +        ; (expr_co1, Scaled _mult inf_arg_ty, inf_res_sigma)
    703 703 
                 <- matchActualFunTy herald (Just . HsExprRnThing $ unLoc expr) (1,expr_rho) expr_rho
    704 704 
                    -- See Note [View patterns and polymorphism]
    705 705 
                    -- expr_wrap1 :: expr_rho "->" (inf_arg_ty -> inf_res_sigma)
    ... ... @@ -720,7 +720,7 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
    720 720 
                   -- NB: pat_ty comes from matchActualFunTy, so it has a
    721 721 
                   -- fixed RuntimeRep, as needed to call mkWpFun.
    722 722
    723 
    -              expr_wrap = expr_wrap2' <.> expr_wrap1
    723 
    +              expr_wrap = expr_wrap2' <.> mkWpCastN expr_co1
    724 724
    725 725 
             ; return $ (ViewPat pat_ty (mkLHsWrap expr_wrap expr') pat', res) }
    726 726

  • compiler/GHC/Tc/Types/Evidence.hs
    ... ... @@ -8,10 +8,11 @@ module GHC.Tc.Types.Evidence (
    8 8 
       -- * HsWrapper
    9 9 
       HsWrapper(..),
    10 10 
       (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpForAllCast,
    11 
    -  mkWpEvLams, mkWpLet, mkWpFun, mkWpCastN, mkWpCastR, mkWpEta,
    11 
    +  mkWpEvLams, mkWpLet, mkWpFun, mkWpCastN, mkWpCastR, mkWpEta, mkWpSubType,
    12 12 
       collectHsWrapBinders,
    13 13 
       idHsWrapper, isIdHsWrapper,
    14 14 
       pprHsWrapper, hsWrapDictBinders,
    15 
    +  optSubTypeHsWrapper,
    15 16
    16 17 
       -- * Evidence bindings
    17 18 
       TcEvBinds(..), EvBindsVar(..),
    ... ... @@ -73,7 +74,7 @@ import GHC.Types.Unique.DFM
    73 74 
     import GHC.Types.Unique.FM
    74 75 
     import GHC.Types.Name( isInternalName )
    75 76 
     import GHC.Types.Var
    76 
    -import GHC.Types.Id( idScaledType )
    77 
    +import GHC.Types.Id( idScaledType, idType )
    77 78 
     import GHC.Types.Var.Env
    78 79 
     import GHC.Types.Var.Set
    79 80 
     import GHC.Types.Basic
    ... ... @@ -134,35 +135,128 @@ maybeSymCo NotSwapped co = co
    134 135 
     ************************************************************************
    135 136 
     -}
    136 137
    137 
    --- We write    wrap :: t1 ~> t2
    138 
    --- if       wrap[ e::t1 ] :: t2
    138 
    +{- Note [Deep subsumption and WpSubType]
    139 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    140 
    +When making DeepSubsumption checks, we may end up with hard-to-spot identity wrappers.
    141 
    +For example (#26349) suppose we have
    142 
    +    (forall a. Eq a => a->a) -> Int  <=   (forall a. Eq a => a->a) -> Int
    143 
    +The two types are equal so we should certainly get an identity wrapper.  But we'll get
    144 
    +tihs wrapper from `tcSubType`:
    145 
    +    WpFun (WpTyLam a <.> WpEvLam dg <.> WpLet (dw=dg) <.> WpEvApp dw <.> WpTyApp a)
    146 
    +          WpHole
    147 
    +That elaborate wrapper is really just a no-op, but it's far from obvious.  If we just
    148 
    +desugar (HsWrap f wp) straightforwardly we'll get
    149 
    +   \(g:forall a. Eq a => a -> a).
    150 
    +       f (/\a. \(dg:Eq a). let dw=dg in g a dw)
    151 
    +
    152 
    +To recognise that as just `f`, we'd have to eta-reduce twice.  But eta-reduction
    153 
    +is not sound in general, so we'll end up retaining the lambdas.  Two bad results:
    154 
    +
    155 
    +* Adding DeepSubsumption gratuitiously makes programs less efficient.
    156 
    +
    157 
    +* When the subsumption is on the LHS of a rule, or in a SPECIALISE pragma, we
    158 
    +  may not be able to make a decent RULE at all, and will fail with "LHS of rule
    159 
    +  is too complicated to desugar" (#26255)
    160 
    +
    161 
    +It'd be ideal to solve the problem at the source, by never generating those
    162 
    +gruesome wrappers in the first place, but we can't do that because:
    163 
    +
    164 
    +* The WpTyLam and WpTyApp are introduced independently, not together, in `tcSubType`,
    165 
    +  so we can't easily cancel them out.   For example, even if we have
    166 
    +     forall a. t1  <=  forall a. t2
    167 
    +  there is no guarantee that these are the "same" a.  E.g.
    168 
    +     forall a b. a -> b -> b   <=   forall x y. y -> x -> x
    169 
    +  Similarly WpEvLam and WpEvApp
    170 
    +
    171 
    +* We have not yet done constraint solving so we don't know what evidence will
    172 
    +  end up in those WpLet bindings.
    173 
    +
    174 
    +TL;DR we must generate the wrapper and then optimise it way if it turns out
    175 
    +that it is a no-op.  Here's our solution:
    176 
    +
    177 
    +(DSST1) Tag the wrappers generated from a subtype check with WpSubType. In normal
    178 
    +  wrappers the binders of a WpTyLam or WpEvLam can scope over the "hole" of the
    179 
    +  wrapper -- that is how we introduce type-lambdas and dictionary-lambda into the
    180 
    +  terms!  But in /subtype/ wrappers, these type/dictionary lambdas only scope over
    181 
    +  the WpTyApp and WpEvApp nodes in the /same/ wrapper.  That is what justifies us
    182 
    +  eta-reducing the type/dictionary lambdas.
    183 
    +
    184 
    +  In short, (WpSubType wp) means the same as `wp`, but with the added promise that
    185 
    +  the binders in `wp` do not scope over the hole.
    186 
    +
    187 
    +(DSST2) Avoid creating a WpSubType in the common WpHole case, using `mkWpSubType`.
    188 
    +
    189 
    +(DSST3) When desugaring, try eta-reduction on the payload of a WpSubType.
    190 
    +  This is done in `GHC.HsToCore.Binds.dsHsWrapper` by the call to `optSubTypeHsWrapper`.
    191 
    +
    192 
    +  We don't attempt to optimise HsWrappers /other than/ subtype wrappers. Why not?
    193 
    +  Because there aren't any useful optimsations we can do.  (We could collapse
    194 
    +  adjacent `WpCast`s perhaps, but that'll happen later automatically via `mkCast`.)
    195 
    +
    196 
    +  TL;DR:
    197 
    +    * we /must/ optimise subtype-HsWrappers (that's the point of this Note!)
    198 
    +    * there is little point in attempting to optimise any other HsWrappers
    199 
    +
    200 
    +Note [WpFun-RR-INVARIANT]
    201 
    +~~~~~~~~~~~~~~~~~~~~~~~~~
    202 
    +Given
    203 
    +  wrap = WpFun wrap1 wrap2 sty1 ty2
    204 
    +  where:  wrap1 :: exp_arg ~~> act_arg
    205 
    +          wrap2 :: act_res ~~> exp_res
    206 
    +          wrap  :: (act_arg -> act_res) ~~> (exp_arg -> exp_res)
    207 
    +we have
    208 
    +  WpFun-RR-INVARIANT:
    209 
    +      the input (exp_arg) and output (act_arg) types of `wrap1`
    210 
    +      both have a fixed runtime-rep
    211 
    +
    212 
    +Reason: We desugar wrap[e] into
    213 
    +    \(x:exp_arg). wrap2[ e wrap1[x] ]
    214 
    +And then, because of Note [Representation polymorphism invariants], we need:
    215 
    +
    216 
    +  * `exp_arg` must have a fixed runtime rep,
    217 
    +    so that lambda obeys the the FRR rules
    218 
    +
    219 
    +  * `act_arg` must have a fixed runtime rep,
    220 
    +    so the that application (e wrap1[x]) obeys the FRR tules
    221 
    +
    222 
    +Hence WpFun-INVARIANT.
    223 
    +-}
    224 
    +
    139 225 
     data HsWrapper
    226 
    +  -- NOTATION (~~>):
    227 
    +  --    We write          wrap :: t1 ~~> t2
    228 
    +  --    if       wrap[ e::t1 ] :: t2
    140 229 
       = WpHole                      -- The identity coercion
    141 230
    231 
    +  | WpSubType HsWrapper
    232 
    +       -- (WpSubType wp) is the same as `wp`, but with extra invariants
    233 
    +       -- See Note [Deep subsumption and WpSubType] (DSST1)
    234 
    +
    142 235 
       | WpCompose HsWrapper HsWrapper
    143 236 
            -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]
    144 237 
            --
    145 238 
            -- Hence  (\a. []) `WpCompose` (\b. []) = (\a b. [])
    146 239 
            -- But    ([] a)   `WpCompose` ([] b)   = ([] b a)
    147 240 
            --
    148 
    -       -- If wrap1 :: t2 ~> t3
    149 
    -       --    wrap2 :: t1 ~> t2
    150 
    -       --- Then (wrap1 `WpCompose` wrap2) :: t1 ~> t3
    151 
    -
    152 
    -  | WpFun HsWrapper HsWrapper (Scaled TcTypeFRR)
    153 
    -       -- (WpFun wrap1 wrap2 (w, t1))[e] = \(x:_w exp_arg). wrap2[ e wrap1[x] ]
    154 
    -       -- So note that if  e     :: act_arg -> act_res
    155 
    -       --                  wrap1 :: exp_arg ~> act_arg
    156 
    -       --                  wrap2 :: act_res ~> exp_res
    157 
    -       --           then   WpFun wrap1 wrap2 : (act_arg -> arg_res) ~> (exp_arg -> exp_res)
    241 
    +       -- If wrap1 :: t2 ~~> t3
    242 
    +       --    wrap2 :: t1 ~~> t2
    243 
    +       --- Then (wrap1 `WpCompose` wrap2) :: t1 ~~> t3
    244 
    +
    245 
    +  | WpFun HsWrapper HsWrapper (Scaled TcTypeFRR) TcType
    246 
    +       -- (WpFun wrap1 wrap2 (w, t1) t2)[e] = \(x:_w exp_arg). wrap2[ e wrap1[x] ]
    247 
    +       --
    248 
    +       -- INVARIANT: both input and output types of `wrap1` have a fixed runtime-rep
    249 
    +       --            See Note [WpFun-RR-INVARIANT]
    250 
    +       --
    251 
    +       -- Typing rules:
    252 
    +       -- If    e     :: act_arg -> act_res
    253 
    +       --       wrap1 :: exp_arg ~~> act_arg
    254 
    +       --       wrap2 :: act_res ~~> exp_res
    255 
    +       -- then   WpFun wrap1 wrap2 :: (act_arg -> act_res) ~~> (exp_arg -> exp_res)
    158 256 
            -- This isn't the same as for mkFunCo, but it has to be this way
    159 257 
            -- because we can't use 'sym' to flip around these HsWrappers
    160 
    -       -- The TcType is the "from" type of the first wrapper;
    161 
    -       --     it always a Type, not a Constraint
    162 258 
            --
    163 
    -       -- NB: a WpFun is always for a (->) function arrow
    164 
    -       --
    165 
    -       -- Use 'mkWpFun' to construct such a wrapper.
    259 
    +       -- NB: a WpFun is always for a (->) function arrow, never (=>)
    166 260
    167 261 
       | WpCast TcCoercionR        -- A cast:  [] `cast` co
    168 262 
                                   -- Guaranteed not the identity coercion
    ... ... @@ -212,50 +306,48 @@ WpCast c1 <.> WpCast c2 = WpCast (c2 `mkTransCo` c1)
    212 306 
       --
    213 307 
       -- NB: <.> behaves like function composition:
    214 308 
       --
    215 
    -  --   WpCast c1 <.> WpCast c2 :: coercionLKind c2 ~> coercionRKind c1
    309 
    +  --   WpCast c1 <.> WpCast c2 :: coercionLKind c2 ~~> coercionRKind c1
    216 310 
       --
    217 311 
       -- This is thus the same as WpCast (c2 ; c1) and not WpCast (c1 ; c2).
    218 312 
     c1        <.> c2        = c1 `WpCompose` c2
    219 313
    220 
    --- | Smart constructor to create a 'WpFun' 'HsWrapper', which avoids introducing
    221 
    --- a lambda abstraction if the two supplied wrappers are either identities or
    222 
    --- casts.
    223 
    ---
    224 
    --- PRECONDITION: either:
    225 
    ---
    226 
    ---  1. both of the 'HsWrapper's are identities or casts, or
    227 
    ---  2. both the "from" and "to" types of the first wrapper have a syntactically
    228 
    ---     fixed RuntimeRep (see Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete).
    229 314 
     mkWpFun :: HsWrapper -> HsWrapper
    230 315 
             -> Scaled TcTypeFRR -- ^ the "from" type of the first wrapper
    231 316 
             -> TcType           -- ^ Either "from" type or "to" type of the second wrapper
    232 317 
                                 --   (used only when the second wrapper is the identity)
    233 318 
             -> HsWrapper
    234 
    -mkWpFun WpHole       WpHole       _             _  = WpHole
    235 
    -mkWpFun WpHole       (WpCast co2) (Scaled w t1) _  = WpCast (mk_wp_fun_co w (mkRepReflCo t1) co2)
    236 
    -mkWpFun (WpCast co1) WpHole       (Scaled w _)  t2 = WpCast (mk_wp_fun_co w (mkSymCo co1)    (mkRepReflCo t2))
    237 
    -mkWpFun (WpCast co1) (WpCast co2) (Scaled w _)  _  = WpCast (mk_wp_fun_co w (mkSymCo co1)    co2)
    238 
    -mkWpFun w_arg        w_res        t1            _  =
    239 
    -  -- In this case, we will desugar to a lambda
    240 
    -  --
    241 
    -  --   \x. w_res[ e w_arg[x] ]
    242 
    -  --
    243 
    -  -- To satisfy Note [Representation polymorphism invariants] in GHC.Core,
    244 
    -  -- it must be the case that both the lambda bound variable x and the function
    245 
    -  -- argument w_arg[x] have a fixed runtime representation, i.e. that both the
    246 
    -  -- "from" and "to" types of the first wrapper "w_arg" have a fixed runtime representation.
    247 
    -  --
    248 
    -  -- Unfortunately, we can't check this with an assertion here, because of
    249 
    -  -- [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
    250 
    -  WpFun w_arg w_res t1
    251 
    -
    252 
    -mkWpEta :: [Id] -> HsWrapper -> HsWrapper
    319 
    +-- ^ Smart constructor for `WpFun`
    320 
    +-- Just removes clutter and optimises some common cases.
    321 
    +--
    322 
    +-- PRECONDITION: same as Note [WpFun-RR-INVARIANT]
    323 
    +--
    324 
    +-- Unfortunately, we can't check PRECONDITION with an assertion here, because of
    325 
    +-- [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
    326 
    +mkWpFun w1 w2 st1@(Scaled m1 t1) t2
    327 
    +  = case (w1,w2) of
    328 
    +      (WpHole,     WpHole)     -> WpHole
    329 
    +      (WpHole,     WpCast co2) -> WpCast (mk_wp_fun_co m1 (mkRepReflCo t1) co2)
    330 
    +      (WpCast co1, WpHole)     -> WpCast (mk_wp_fun_co m1 (mkSymCo co1)    (mkRepReflCo t2))
    331 
    +      (WpCast co1, WpCast co2) -> WpCast (mk_wp_fun_co m1 (mkSymCo co1)    co2)
    332 
    +      (_,          _)          -> WpFun w1 w2 st1 t2
    333 
    +
    334 
    +mkWpSubType :: HsWrapper -> HsWrapper
    335 
    +-- See (DSST2) in Note [Deep subsumption and WpSubType]
    336 
    +mkWpSubType WpHole      = WpHole
    337 
    +mkWpSubType (WpCast co) = WpCast co
    338 
    +mkWpSubType w           = WpSubType w
    339 
    +
    340 
    +mkWpEta :: Type -> [Id] -> HsWrapper -> HsWrapper
    253 341 
     -- (mkWpEta [x1, x2] wrap) [e]
    254 342 
     --   = \x1. \x2.  wrap[e x1 x2]
    255 343 
     -- Just generates a bunch of WpFuns
    256 
    -mkWpEta xs wrap = foldr eta_one wrap xs
    344 
    +-- The incoming type is the type of the entire expression
    345 
    +mkWpEta orig_fun_ty xs wrap = go orig_fun_ty xs
    257 346 
       where
    258 
    -    eta_one x wrap = WpFun idHsWrapper wrap (idScaledType x)
    347 
    +    go _      []       = wrap
    348 
    +    go fun_ty (id:ids) = WpFun idHsWrapper (go res_ty ids) (idScaledType id) res_ty
    349 
    +                       where
    350 
    +                         res_ty = funResultTy fun_ty
    259 351
    260 352 
     mk_wp_fun_co :: Mult -> TcCoercionR -> TcCoercionR -> TcCoercionR
    261 353 
     mk_wp_fun_co mult arg_co res_co
    ... ... @@ -333,8 +425,9 @@ hsWrapDictBinders wrap = go wrap
    333 425 
      where
    334 426 
        go (WpEvLam dict_id)   = unitBag dict_id
    335 427 
        go (w1 `WpCompose` w2) = go w1 `unionBags` go w2
    336 
    -   go (WpFun _ w _)       = go w
    428 
    +   go (WpFun _ w _ _)     = go w
    337 429 
        go WpHole              = emptyBag
    430 
    +   go (WpSubType {})      = emptyBag  -- See Note [Deep subsumption and WpSubType]
    338 431 
        go (WpCast  {})        = emptyBag
    339 432 
        go (WpEvApp {})        = emptyBag
    340 433 
        go (WpTyLam {})        = emptyBag
    ... ... @@ -350,6 +443,7 @@ collectHsWrapBinders wrap = go wrap []
    350 443 
         go :: HsWrapper -> [HsWrapper] -> ([Var], HsWrapper)
    351 444 
         go (WpEvLam v)       wraps = add_lam v (gos wraps)
    352 445 
         go (WpTyLam v)       wraps = add_lam v (gos wraps)
    446 
    +    go (WpSubType w)     wraps = go w wraps
    353 447 
         go (WpCompose w1 w2) wraps = go w1 (w2:wraps)
    354 448 
         go wrap              wraps = ([], foldl' (<.>) wrap wraps)
    355 449
    ... ... @@ -358,6 +452,162 @@ collectHsWrapBinders wrap = go wrap []
    358 452
    359 453 
         add_lam v (vs,w) = (v:vs, w)
    360 454
    455 
    +
    456 
    +optSubTypeHsWrapper :: HsWrapper -> HsWrapper
    457 
    +-- This optimiser is used only on the payload of WpSubType
    458 
    +-- It finds cases where the entire wrapper is a no-op
    459 
    +-- See (DSST3) in Note [Deep subsumption and WpSubType]
    460 
    +optSubTypeHsWrapper wrap
    461 
    +  = opt wrap
    462 
    +  where
    463 
    +    opt :: HsWrapper -> HsWrapper
    464 
    +    opt w = foldr (<.>) WpHole (opt1 w [])
    465 
    +
    466 
    +    opt1 :: HsWrapper -> [HsWrapper] -> [HsWrapper]
    467 
    +    -- opt1 w ws = w <.> (foldr <.> WpHole ws)
    468 
    +    -- INVARIANT: ws::[HsWrapper] is optimised
    469 
    +    opt1 WpHole                 ws = ws
    470 
    +    opt1 (WpSubType w)          ws = opt1 w ws
    471 
    +    opt1 (w1 `WpCompose` w2)    ws = opt1 w1 (opt1 w2 ws)
    472 
    +    opt1 (WpCast co)            ws = opt_co co ws
    473 
    +    opt1 (WpEvLam ev)           ws = opt_ev_lam ev ws
    474 
    +    opt1 (WpTyLam tv)           ws = opt_ty_lam tv ws
    475 
    +    opt1 (WpLet binds)          ws = pushWpLet binds ws
    476 
    +    opt1 (WpFun w1 w2 sty1 ty2) ws = opt_fun w1 w2 sty1 ty2 ws
    477 
    +    opt1 w@(WpTyApp {})         ws = w : ws
    478 
    +    opt1 w@(WpEvApp {})         ws = w : ws
    479 
    +
    480 
    +    -----------------
    481 
    +    -- (WpTyLam a <.> WpTyApp a <.> w) = w
    482 
    +    -- i.e.   /\a. <hole> a   -->  <hole>
    483 
    +    -- This is only valid if whatever fills the hole does not mention 'a'
    484 
    +    -- But that's guaranteed in subtype-wrappers;
    485 
    +    -- see (DSST1) in Note [Deep subsumption and WpSubType]
    486 
    +    opt_ty_lam tv (WpTyApp ty : ws)
    487 
    +      | Just tv' <- getTyVar_maybe ty
    488 
    +      , tv==tv'
    489 
    +      , all (tv `not_in`) ws
    490 
    +      = ws
    491 
    +
    492 
    +    -- (WpTyLam a <.> WpCastCo co <.> w)
    493 
    +    --    = WpCast (ForAllCo a co) (WpTyLam <.> w)
    494 
    +    opt_ty_lam tv (WpCast co : ws)
    495 
    +      = opt_co (mkHomoForAllCo tv co) (opt_ty_lam tv ws)
    496 
    +
    497 
    +    opt_ty_lam tv ws
    498 
    +      = WpTyLam tv : ws
    499 
    +
    500 
    +    -----------------
    501 
    +    -- (WpEvLam ev <.> WpEvAp ev <.> w) = w
    502 
    +    -- Similar notes to WpTyLam
    503 
    +    opt_ev_lam ev (WpEvApp ev_tm : ws)
    504 
    +      | EvExpr (Var ev') <- ev_tm
    505 
    +      , ev == ev'
    506 
    +      , all (ev `not_in`) ws
    507 
    +      = ws
    508 
    +
    509 
    +    -- (WpEvLam ev <.> WpCast co <.> w)
    510 
    +    --    = WpCast (FunCo ev co) (WpEvLam <.> w)
    511 
    +    opt_ev_lam ev (WpCast co : ws)
    512 
    +      = opt_co fun_co (opt_ev_lam ev ws)
    513 
    +      where
    514 
    +        fun_co = mkFunCo Representational FTF_C_T
    515 
    +                        (mkNomReflCo ManyTy)
    516 
    +                        (mkRepReflCo (idType ev))
    517 
    +                        co
    518 
    +
    519 
    +    opt_ev_lam ev ws
    520 
    +      = WpEvLam ev : ws
    521 
    +
    522 
    +    -----------------
    523 
    +    -- WpCast co <.> WpCast co' <.> ws = WpCast (co;co') ws
    524 
    +    opt_co co (WpCast co' : ws)     = opt_co (co `mkTransCo` co') ws
    525 
    +    opt_co co ws | isReflexiveCo co = ws
    526 
    +                 | otherwise        = WpCast co : ws
    527 
    +
    528 
    +    ------------------
    529 
    +    opt_fun w1 w2 sty1 ty2 ws
    530 
    +      = case mkWpFun (opt w1) (opt w2) sty1 ty2 of
    531 
    +          WpHole    -> ws
    532 
    +          WpCast co -> opt_co co ws
    533 
    +          w         -> w : ws
    534 
    +
    535 
    +    ------------------
    536 
    +    -- Tiresome check that the lambda-bound type/evidence variable that we
    537 
    +    -- want to eta-reduce isn't free in the rest of the wrapper
    538 
    +    not_in :: TyVar -> HsWrapper -> Bool
    539 
    +    not_in _  WpHole                   = True
    540 
    +    not_in v (WpCast co)               = not (anyFreeVarsOfCo (== v) co)
    541 
    +    not_in v (WpTyApp ty)              = not (anyFreeVarsOfType (== v) ty)
    542 
    +    not_in v (WpFun w1 w2 _ _)         = not_in v w1 && not_in v w2
    543 
    +    not_in v (WpSubType w)             = not_in v w
    544 
    +    not_in v (WpCompose w1 w2)         = not_in v w1 && not_in v w2
    545 
    +    not_in v (WpEvApp (EvExpr e))      = not (v `elemVarSet` exprFreeVars e)
    546 
    +    not_in _ (WpEvApp (EvTypeable {})) = False  -- Giving up; conservative
    547 
    +    not_in _ (WpEvApp (EvFun {}))      = False  -- Giving up; conservative
    548 
    +    not_in _ (WpTyLam {}) = False    -- Give  up; conservative
    549 
    +    not_in _ (WpEvLam {}) = False    -- Ditto
    550 
    +    not_in _ (WpLet {})   = False    -- Ditto
    551 
    +
    552 
    +pushWpLet :: TcEvBinds -> [HsWrapper] -> [HsWrapper]
    553 
    +-- See if we can transform
    554 
    +--    WpLet binds <.> w1 <.> .. <.> wn   -->   w1' <.> .. <.> wn'
    555 
    +-- by substitution.
    556 
    +-- We do this just for the narrow case when
    557 
    +--   - the `binds` are all just v=w, variables only
    558 
    +--   - the wi are all WpTyApp, WpEvApp, or WpCast
    559 
    +-- This is just enough to get us the eta-reductions that we seek
    560 
    +pushWpLet tc_ev_binds ws
    561 
    +  = case tc_ev_binds of
    562 
    +      TcEvBinds {} -> pprPanic "pushWpLet" (ppr tc_ev_binds)
    563 
    +      EvBinds binds
    564 
    +        | isEmptyBag binds
    565 
    +        -> ws
    566 
    +        | Just env <- ev_bind_swizzle binds
    567 
    +        -> case go env ws of
    568 
    +              Just ws' -> ws'
    569 
    +              Nothing  -> bale_out
    570 
    +        | otherwise
    571 
    +        -> bale_out
    572 
    +  where
    573 
    +    bale_out = WpLet tc_ev_binds : ws
    574 
    +
    575 
    +    go :: IdEnv Id -> [HsWrapper] -> Maybe [HsWrapper]
    576 
    +    go env (WpCast co  : ws) = do { ws' <- go env ws
    577 
    +                                  ; return (WpCast co  : ws') }
    578 
    +    go env (WpTyApp ty : ws) = do { ws' <- go env ws
    579 
    +                                  ; return (WpTyApp ty : ws') }
    580 
    +    go env (WpEvApp (EvExpr (Var v)) : ws)
    581 
    +       = do { v'  <- swizzle_id env v
    582 
    +            ; ws' <- go env ws
    583 
    +            ; return (WpEvApp (EvExpr (Var v')) : ws') }
    584 
    +
    585 
    +    go _ ws = case ws of
    586 
    +                 []    -> Just []
    587 
    +                 (_:_) -> Nothing  -- Could not fully eliminate the WpLet
    588 
    +
    589 
    +    swizzle_id :: IdEnv Id -> Id -> Maybe Id
    590 
    +    -- Nothing <=> ran out of fuel
    591 
    +    -- This is just belt and braces; we should never build bottom evidence
    592 
    +    swizzle_id env v = go 100 v
    593 
    +      where
    594 
    +        go :: Int -> EvId -> Maybe EvId
    595 
    +        go fuel v
    596 
    +          | fuel == 0                     = Nothing
    597 
    +          | Just v' <- lookupVarEnv env v = go (fuel-1) v'
    598 
    +          | otherwise                     = Just v
    599 
    +
    600 
    +    ev_bind_swizzle :: Bag EvBind -> Maybe (IdEnv Id)
    601 
    +    -- Succeeds only if the bindings are all var-to-var bindings
    602 
    +    ev_bind_swizzle evbs = foldl' do_one (Just emptyVarEnv) evbs
    603 
    +      where
    604 
    +        do_one :: Maybe (IdEnv Id) -> EvBind -> Maybe (IdEnv Id)
    605 
    +        do_one Nothing _ = Nothing
    606 
    +        do_one (Just swizzle) (EvBind {eb_lhs = bndr, eb_rhs = rhs})
    607 
    +          = case rhs of
    608 
    +               EvExpr (Var v) -> Just (extendVarEnv swizzle bndr v)
    609 
    +               _              -> Nothing
    610 
    +
    361 611 
     {-
    362 612 
     ************************************************************************
    363 613 
     *                                                                      *
    ... ... @@ -1018,8 +1268,9 @@ pprHsWrapper wrap pp_thing_inside
    1018 1268 
         -- True  <=> appears in function application position
    1019 1269 
         -- False <=> appears as body of let or lambda
    1020 1270 
         help it WpHole             = it
    1021 
    -    help it (WpCompose f1 f2)  = help (help it f2) f1
    1022 
    -    help it (WpFun f1 f2 (Scaled w t1)) = add_parens $ text "\\(x" <> dcolon <> brackets (ppr w) <> ppr t1 <> text ")." <+>
    1271 
    +    help it (WpCompose w1 w2)  = help (help it w2) w1
    1272 
    +    help it (WpSubType w)      = no_parens $ text "subtype" <> braces (help it w False)
    1273 
    +    help it (WpFun f1 f2 (Scaled w t1) _) = add_parens $ text "\\(x" <> dcolon <> brackets (ppr w) <> ppr t1 <> text ")." <+>
    1023 1274 
                                                 help (\_ -> it True <+> help (\_ -> text "x") f1 True) f2 False
    1024 1275 
         help it (WpCast co)   = add_parens $ sep [it False, nest 2 (text "|>"
    1025 1276 
                                                   <+> pprParendCo co)]

  • compiler/GHC/Tc/Utils/Concrete.hs
    ... ... @@ -626,8 +626,12 @@ hasFixedRuntimeRep :: HasDebugCallStack
    626 626 
                             -- @ki@ is concrete, and @co :: ty ~# ty'@.
    627 627 
                             -- That is, @ty'@ has a syntactically fixed RuntimeRep
    628 628 
                             -- in the sense of Note [Fixed RuntimeRep].
    629 
    -hasFixedRuntimeRep frr_ctxt ty =
    630 
    -  checkFRR_with (fmap (fmap coToMCo) . unifyConcrete_kind (fsLit "cx") . ConcreteFRR) frr_ctxt ty
    629 
    +hasFixedRuntimeRep frr_ctxt ty
    630 
    +  = checkFRR_with unify_conc frr_ctxt ty
    631 
    +  where
    632 
    +    unify_conc frr_orig ki
    633 
    +      = do { co <- unifyConcrete_kind (fsLit "cx") (ConcreteFRR frr_orig) ki
    634 
    +           ; return (coToMCo co) }
    631 635
    632 636 
     -- | Like 'hasFixedRuntimeRep', but we perform an eager syntactic check.
    633 637 
     --

  • compiler/GHC/Tc/Utils/Unify.hs
    ... ... @@ -148,7 +148,7 @@ matchActualFunTy
    148 148 
           -- (Both are used only for error messages)
    149 149 
       -> TcRhoType
    150 150 
           -- ^ Type to analyse: a TcRhoType
    151 
    -  -> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType)
    151 
    +  -> TcM (TcCoercion, Scaled TcSigmaTypeFRR, TcSigmaType)
    152 152 
     -- This function takes in a type to analyse (a RhoType) and returns
    153 153 
     -- an argument type and a result type (splitting apart a function arrow).
    154 154 
     -- The returned argument type is a SigmaType with a fixed RuntimeRep;
    ... ... @@ -157,7 +157,7 @@ matchActualFunTy
    157 157 
     -- See Note [matchActualFunTy error handling] for the first three arguments
    158 158
    159 159 
     -- If   (wrap, arg_ty, res_ty) = matchActualFunTy ... fun_ty
    160 
    --- then wrap :: fun_ty ~> (arg_ty -> res_ty)
    160 
    +-- then wrap :: fun_ty ~~> (arg_ty -> res_ty)
    161 161 
     -- and NB: res_ty is an (uninstantiated) SigmaType
    162 162
    163 163 
     matchActualFunTy herald mb_thing err_info fun_ty
    ... ... @@ -172,13 +172,13 @@ matchActualFunTy herald mb_thing err_info fun_ty
    172 172 
         -- hide the forall inside a meta-variable
    173 173 
         go :: TcRhoType   -- The type we're processing, perhaps after
    174 174 
                           -- expanding type synonyms
    175 
    -       -> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType)
    175 
    +       -> TcM (TcCoercion, Scaled TcSigmaTypeFRR, TcSigmaType)
    176 176 
         go ty | Just ty' <- coreView ty = go ty'
    177 177
    178 178 
         go (FunTy { ft_af = af, ft_mult = w, ft_arg = arg_ty, ft_res = res_ty })
    179 179 
           = assert (isVisibleFunArg af) $
    180 180 
           do { hasFixedRuntimeRep_syntactic (FRRExpectedFunTy herald 1) arg_ty
    181 
    -         ; return (idHsWrapper, Scaled w arg_ty, res_ty) }
    181 
    +         ; return (mkNomReflCo fun_ty, Scaled w arg_ty, res_ty) }
    182 182
    183 183 
         go ty@(TyVarTy tv)
    184 184 
           | isMetaTyVar tv
    ... ... @@ -210,7 +210,7 @@ matchActualFunTy herald mb_thing err_info fun_ty
    210 210 
                ; res_ty <- newOpenFlexiTyVarTy
    211 211 
                ; let unif_fun_ty = mkScaledFunTys [arg_ty] res_ty
    212 212 
                ; co <- unifyType mb_thing fun_ty unif_fun_ty
    213 
    -           ; return (mkWpCastN co, arg_ty, res_ty) }
    213 
    +           ; return (co, arg_ty, res_ty) }
    214 214
    215 215 
         ------------
    216 216 
         mk_ctxt :: TcType -> TidyEnv -> ZonkM (TidyEnv, ErrCtxtMsg)
    ... ... @@ -249,8 +249,10 @@ matchActualFunTys :: ExpectedFunTyOrigin -- ^ See Note [Herald for matchExpected
    249 249 
                       -> Arity
    250 250 
                       -> TcSigmaType
    251 251 
                       -> TcM (HsWrapper, [Scaled TcSigmaTypeFRR], TcRhoType)
    252 
    --- If    matchActualFunTys n ty = (wrap, [t1,..,tn], res_ty)
    253 
    --- then  wrap : ty ~> (t1 -> ... -> tn -> res_ty)
    252 
    +-- NB: Called only from `tcSynArgA`, and hence scheduled for destruction
    253 
    +--
    254 
    +-- If    matchActualFunTys n fun_ty = (wrap, [t1,..,tn], res_ty)
    255 
    +-- then  wrap : fun_ty ~~>  (t1 -> ... -> tn -> res_ty)
    254 256 
     --       and res_ty is a RhoType
    255 257 
     -- NB: the returned type is top-instantiated; it's a RhoType
    256 258 
     matchActualFunTys herald ct_orig n_val_args_wanted top_ty
    ... ... @@ -265,15 +267,13 @@ matchActualFunTys herald ct_orig n_val_args_wanted top_ty
    265 267 
         go 0 _ fun_ty = return (idHsWrapper, [], fun_ty)
    266 268
    267 269 
         go n so_far fun_ty
    268 
    -      = do { (wrap_fun1, arg_ty1, res_ty1) <- matchActualFunTy
    269 
    -                                                 herald Nothing
    270 
    -                                                 (n_val_args_wanted, top_ty)
    271 
    -                                                 fun_ty
    272 
    -           ; (wrap_res, arg_tys, res_ty)   <- go (n-1) (arg_ty1:so_far) res_ty1
    270 
    +      = do { (co1, arg_ty1, res_ty1) <- matchActualFunTy herald Nothing
    271 
    +                                           (n_val_args_wanted, top_ty) fun_ty
    272 
    +           ; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1
    273 273 
                ; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty
    274 274 
                -- NB: arg_ty1 comes from matchActualFunTy, so it has
    275 
    -           -- a syntactically fixed RuntimeRep as needed to call mkWpFun.
    276 
    -           ; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) }
    275 
    +           -- a syntactically fixed RuntimeRep
    276 
    +           ; return (wrap_fun2 <.> mkWpCastN co1, arg_ty1:arg_tys, res_ty) }
    277 277
    278 278 
     {-
    279 279 
     ************************************************************************
    ... ... @@ -459,7 +459,7 @@ tcSkolemiseGeneral ds_flag ctxt top_ty expected_ty thing_inside
    459 459 
     tcSkolemiseCompleteSig :: TcCompleteSig
    460 460 
                            -> ([ExpPatType] -> TcRhoType -> TcM result)
    461 461 
                            -> TcM (HsWrapper, result)
    462 
    --- ^ The wrapper has type: spec_ty ~> expected_ty
    462 
    +-- ^ The wrapper has type: spec_ty ~~> expected_ty
    463 463 
     -- See Note [Skolemisation] for the differences between
    464 464 
     -- tcSkolemiseCompleteSig and tcTopSkolemise
    465 465
    ... ... @@ -790,7 +790,7 @@ matchExpectedFunTys :: forall a.
    790 790 
                         -> ([ExpPatType] -> ExpRhoType -> TcM a)
    791 791 
                         -> TcM (HsWrapper, a)
    792 792 
     -- If    matchExpectedFunTys n ty = (wrap, _)
    793 
    --- then  wrap : (t1 -> ... -> tn -> ty_r) ~> ty,
    793 
    +-- then  wrap : (t1 -> ... -> tn -> ty_r) ~~> ty,
    794 794 
     --   where [t1, ..., tn], ty_r are passed to the thing_inside
    795 795 
     --
    796 796 
     -- Unconditionally concludes by skolemising any trailing invisible
    ... ... @@ -865,12 +865,13 @@ matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside
    865 865 
                                        , ft_arg = arg_ty, ft_res = res_ty })
    866 866 
           = assert (isVisibleFunArg af) $
    867 867 
             do { let arg_pos = arity - n_req + 1   -- 1 for the first argument etc
    868 
    -           ; (arg_co, arg_ty) <- hasFixedRuntimeRep (FRRExpectedFunTy herald arg_pos) arg_ty
    868 
    +           ; (arg_co, arg_ty_frr) <- hasFixedRuntimeRep (FRRExpectedFunTy herald arg_pos) arg_ty
    869 
    +           ; let arg_sty_frr = Scaled mult arg_ty_frr
    869 870 
                ; (wrap_res, result) <- check (n_req - 1)
    870 
    -                                         (mkCheckExpFunPatTy (Scaled mult arg_ty) : rev_pat_tys)
    871 
    +                                         (mkCheckExpFunPatTy arg_sty_frr : rev_pat_tys)
    871 872 
                                              res_ty
    872 873 
                ; let wrap_arg = mkWpCastN arg_co
    873 
    -                 fun_wrap = mkWpFun wrap_arg wrap_res (Scaled mult arg_ty) res_ty
    874 
    +                 fun_wrap = mkWpFun wrap_arg wrap_res arg_sty_frr res_ty
    874 875 
                ; return (fun_wrap, result) }
    875 876
    876 877 
         ----------------------------
    ... ... @@ -1407,7 +1408,7 @@ tcSubTypePat :: CtOrigin -> UserTypeCtxt
    1407 1408 
     -- Used in patterns; polarity is backwards compared
    1408 1409 
     --   to tcSubType
    1409 1410 
     -- If wrap = tc_sub_type_et t1 t2
    1410 
    ---    => wrap :: t1 ~> t2
    1411 
    +--    => wrap :: t1 ~~> t2
    1411 1412 
     tcSubTypePat inst_orig ctxt (Check ty_actual) ty_expected
    1412 1413 
       = tc_sub_type unifyTypeET inst_orig ctxt ty_actual ty_expected
    1413 1414
    ... ... @@ -1427,11 +1428,12 @@ tcSubTypeDS :: HsExpr GhcRn
    1427 1428 
                                -- DeepSubsumption <=> when checking, this type
    1428 1429 
                                --                     is deeply skolemised
    1429 1430 
                 -> TcM HsWrapper
    1430 
    --- Only one call site, in GHC.Tc.Gen.App.tcApp
    1431 
    +-- Only one call site, in GHC.Tc.Gen.App.checkResultTy
    1431 1432 
     tcSubTypeDS rn_expr act_rho exp_rho
    1432 
    -  = tc_sub_type_deep Top (unifyExprType rn_expr) orig GenSigCtxt act_rho exp_rho
    1433 
    -  where
    1434 
    -    orig = exprCtOrigin rn_expr
    1433 
    +  = do { wrap <- tc_sub_type_deep Top (unifyExprType rn_expr)
    1434 
    +                                  (exprCtOrigin rn_expr)
    1435 
    +                                  GenSigCtxt act_rho exp_rho
    1436 
    +       ; return (mkWpSubType wrap) }
    1435 1437
    1436 1438 
     ---------------
    1437 1439
    ... ... @@ -1456,7 +1458,7 @@ tcSubTypeSigma :: CtOrigin -- where did the actual type arise / why are we
    1456 1458 
                    -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
    1457 1459 
     -- External entry point, but no ExpTypes on either side
    1458 1460 
     -- Checks that actual <= expected
    1459 
    --- Returns HsWrapper :: actual ~ expected
    1461 
    +-- Returns HsWrapper :: actual ~~> expected
    1460 1462 
     tcSubTypeSigma orig ctxt ty_actual ty_expected
    1461 1463 
       = tc_sub_type (unifyType Nothing) orig ctxt ty_actual ty_expected
    1462 1464
    ... ... @@ -1495,7 +1497,7 @@ tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify
    1495 1497 
                 -> TcM HsWrapper
    1496 1498 
     -- Checks that actual_ty is more polymorphic than expected_ty
    1497 1499 
     -- If wrap = tc_sub_type t1 t2
    1498 
    ---    => wrap :: t1 ~> t2
    1500 
    +--    => wrap :: t1 ~~> t2
    1499 1501 
     --
    1500 1502 
     -- The "how to unify argument" is always a call to `uType TypeLevel orig`,
    1501 1503 
     -- but with different ways of constructing the CtOrigin `orig` from
    ... ... @@ -1504,7 +1506,8 @@ tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify
    1504 1506 
     ----------------------
    1505 1507 
     tc_sub_type unify inst_orig ctxt ty_actual ty_expected
    1506 1508 
       = do { ds_flag <- getDeepSubsumptionFlag
    1507 
    -       ; tc_sub_type_ds Top ds_flag unify inst_orig ctxt ty_actual ty_expected }
    1509 
    +       ; wrap <- tc_sub_type_ds Top ds_flag unify inst_orig ctxt ty_actual ty_expected
    1510 
    +       ; return (mkWpSubType wrap) }
    1508 1511
    1509 1512 
     ----------------------
    1510 1513 
     tc_sub_type_ds :: Position p -- ^ position in the type (for error messages only)
    ... ... @@ -1753,59 +1756,59 @@ we deal with function arrows. Suppose we have:
    1753 1756 
       ty_actual   = act_arg -> act_res
    1754 1757 
       ty_expected = exp_arg -> exp_res
    1755 1758
    1756 
    -To produce fun_wrap :: (act_arg -> act_res) ~> (exp_arg -> exp_res), we use
    1759 
    +To produce fun_wrap :: (act_arg -> act_res) ~~> (exp_arg -> exp_res), we use
    1757 1760 
     the fact that the function arrow is contravariant in its argument type and
    1758 1761 
     covariant in its result type. Thus we recursively perform subtype checks
    1759 1762 
     on the argument types (with actual/expected switched) and the result types,
    1760 1763 
     to get:
    1761 1764
    1762 
    -  arg_wrap :: exp_arg ~> act_arg   -- NB: expected/actual have switched sides
    1763 
    -  res_wrap :: act_res ~> exp_res
    1765 
    +  arg_wrap :: exp_arg ~~> act_arg   -- NB: expected/actual have switched sides
    1766 
    +  res_wrap :: act_res ~~> exp_res
    1764 1767
    1765 1768 
     Then fun_wrap = mkWpFun arg_wrap res_wrap.
    1766 1769
    1767 
    -Wrinkle [Representation-polymorphism checking during subtyping]
    1770 
    +Note [Representation-polymorphism checking during subtyping]
    1771 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1772 
    +When doing deep subsumption in `tc_sub_type_deep`, looking under function arrows,
    1773 
    +we would usually build a `WpFun` HsWrapper.  When desugared, we get eta-expansion:
    1768 1774
    1769 
    -  Inserting a WpFun HsWrapper amounts to impedance matching in deep subsumption
    1770 
    -  via eta-expansion:
    1775 
    +  f  ==>  \(x :: exp_arg). res_wrap [ f (arg_wrap [x]) ]
    1771 1776
    1772 
    -    f  ==>  \ (x :: exp_arg) -> res_wrap [ f (arg_wrap [x]) ]
    1777 
    +Since we produce a lambda, we must enforce the representation polymorphism
    1778 
    +invariants described in Note [Representation polymorphism invariants] in GHC.Core.
    1779 
    +That is, we must ensure that both
    1780 
    +   - x (the lambda binder), and
    1781 
    +   - (arg_wrap [x]) (the function argument)
    1782 
    +have a fixed runtime representation.
    1773 1783
    1774 
    -  As we produce a lambda, we must enforce the representation polymorphism
    1775 
    -  invariants described in Note [Representation polymorphism invariants] in GHC.Core.
    1776 
    -  That is, we must ensure that both x (the lambda binder) and (arg_wrap [x]) (the function argument)
    1777 
    -  have a fixed runtime representation.
    1784 
    +But we don't /always/ need to produce a `WpFun`: if both argument and result wrappers
    1785 
    +are merely coercions, we can produce a `WpCast co` instead of a `WpFun`.  In that
    1786 
    +case there is no eta-expansion, and hence no need for FRR checks.
    1778 1787
    1779 
    -  Note however that desugaring mkWpFun does not always introduce a lambda: if
    1780 
    -  both the argument and result HsWrappers are casts, then a FunCo cast suffices,
    1781 
    -  in which case we should not perform representation-polymorphism checking.
    1788 
    +Here's a contrived example (there are undoubtedly more natural examples)
    1789 
    +(see testsuite/tests/rep-poly/NoEtaRequired):
    1782 1790
    1783 
    -  This means that, in the FunTy/FunTy case of tc_sub_type_deep, we can skip
    1784 
    -  the representation-polymorphism checks if the produced argument and result
    1785 
    -  wrappers are identities or casts.
    1786 
    -  It is important to do so, otherwise we reject valid programs.
    1791 
    +    type Id :: k -> k
    1792 
    +    type family Id a where
    1787 1793
    1788 
    -    Here's a contrived example (there are undoubtedly more natural examples)
    1789 
    -    (see testsuite/tests/rep-poly/NoEtaRequired):
    1794 
    +    type T :: TYPE r -> TYPE (Id r)
    1795 
    +    type family T a where
    1790 1796
    1791 
    -      type Id :: k -> k
    1792 
    -      type family Id a where
    1797 
    +    test :: forall r (a :: TYPE r). a :~~: T a -> ()
    1798 
    +    test HRefl =
    1799 
    +      let
    1800 
    +        f :: (a -> a) -> ()
    1801 
    +        f _ = ()
    1802 
    +        g :: T a -> T a
    1803 
    +        g = undefined
    1804 
    +      in f g
    1793 1805
    1794 
    -      type T :: TYPE r -> TYPE (Id r)
    1795 
    -      type family T a where
    1806 
    +We don't need to eta-expand `g` to make `f g` typecheck; a cast
    1807 
    +suffices.  Hence we should not perform representation-polymorphism
    1808 
    +checks; they would fail here.
    1796 1809
    1797 
    -      test :: forall r (a :: TYPE r). a :~~: T a -> ()
    1798 
    -      test HRefl =
    1799 
    -        let
    1800 
    -          f :: (a -> a) -> ()
    1801 
    -          f _ = ()
    1802 
    -          g :: T a -> T a
    1803 
    -          g = undefined
    1804 
    -        in f g
    1805 
    -
    1806 
    -    We don't need to eta-expand `g` to make `f g` typecheck; a cast suffices.
    1807 
    -    Hence we should not perform representation-polymorphism checks; they would
    1808 
    -    fail here.
    1810 
    +All this is done by `mkWpFun_FRR`, which checks for the cast/cast case and
    1811 
    +returns a `FunCo` if so.
    1809 1812
    1810 1813 
     Note [Setting the argument context]
    1811 1814 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    ... ... @@ -1947,7 +1950,7 @@ getDeepSubsumptionFlag = do { ds <- xoptM LangExt.DeepSubsumption
    1947 1950 
     -- | 'tc_sub_type_deep' is where the actual work happens for deep subsumption.
    1948 1951 
     --
    1949 1952 
     -- Given @ty_actual@ (a sigma-type) and @ty_expected@ (deeply skolemised, i.e.
    1953 
    +-- a deep rho type), it returns an 'HsWrapper' @wrap :: ty_actual ~~> ty_expected@.
    1950 1954 
     tc_sub_type_deep :: HasDebugCallStack
    1951 1955 
                      => Position p     -- ^ Position in the type (for error messages only)
    1952 1956 
                      -> (TcType -> TcType -> TcM TcCoercionN) -- ^ How to unify
    ... ... @@ -1958,7 +1961,7 @@ tc_sub_type_deep :: HasDebugCallStack
    1958 1961 
                      -> TcM HsWrapper
    1959 1962
    1960 1963 
     -- If wrap = tc_sub_type_deep t1 t2
    1961 
    ---    => wrap :: t1 ~> t2
    1964 
    +--    => wrap :: t1 ~~> t2
    1962 1965 
     -- Here is where the work actually happens!
    1963 1966 
     -- Precondition: ty_expected is deeply skolemised
    1964 1967
    ... ... @@ -2015,8 +2018,8 @@ tc_sub_type_deep pos unify inst_orig ctxt ty_actual ty_expected
    2015 2018 
                ; unify_wrap <- just_unify exp_funTy ty_e
    2016 2019 
                ; fun_wrap <- go_fun af1 act_mult act_arg act_res af1 exp_mult exp_arg exp_res
    2017 2020 
                ; return $ unify_wrap <.> fun_wrap
    2018 
    -             -- unify_wrap :: exp_funTy ~> ty_e
    2019 
    -             -- fun_wrap :: ty_a ~> exp_funTy
    2021 
    +             -- unify_wrap :: exp_funTy ~~> ty_e
    2022 
    +             -- fun_wrap :: ty_a ~~> exp_funTy
    2020 2023 
                }
    2021 2024 
         go1 ty_a (FunTy { ft_af = af2, ft_mult = exp_mult, ft_arg = exp_arg, ft_res = exp_res })
    2022 2025 
           | isVisibleFunArg af2
    ... ... @@ -2028,8 +2031,8 @@ tc_sub_type_deep pos unify inst_orig ctxt ty_actual ty_expected
    2028 2031 
                ; unify_wrap <- just_unify ty_a act_funTy
    2029 2032 
                ; fun_wrap <- go_fun af2 act_mult act_arg act_res af2 exp_mult exp_arg exp_res
    2030 2033 
                ; return $ fun_wrap <.> unify_wrap
    2031 
    -             -- unify_wrap :: ty_a ~> act_funTy
    2032 
    -             -- fun_wrap :: act_funTy ~> ty_e
    2034 
    +             -- unify_wrap :: ty_a ~~> act_funTy
    2035 
    +             -- fun_wrap :: act_funTy ~~> ty_e
    2033 2036 
                }
    2034 2037
    2035 2038 
         -- Otherwise, revert to unification.
    ... ... @@ -2064,17 +2067,28 @@ mkWpFun_FRR
    2064 2067 
       -> Position p
    2065 2068 
       -> FunTyFlag -> Type -> TcType -> Type --   actual FunTy
    2066 2069 
       -> FunTyFlag -> Type -> TcType -> Type -- expected FunTy
    2067 
    -  -> HsWrapper -- ^ exp_arg ~> act_arg
    2068 
    -  -> HsWrapper -- ^ act_res ~> exp_res
    2069 
    -  -> TcM HsWrapper -- ^ act_funTy ~> exp_funTy
    2070 
    +  -> HsWrapper -- ^ exp_arg ~~> act_arg
    2071 
    +  -> HsWrapper -- ^ act_res ~~> exp_res
    2072 
    +  -> TcM HsWrapper -- ^ (act_arg->act_res) ~~> (exp_arg->exp_res)
    2070 2073 
     mkWpFun_FRR unify pos act_af act_mult act_arg act_res exp_af exp_mult exp_arg exp_res arg_wrap res_wrap
    2071 
    -  = do { ((exp_arg_co, exp_arg_frr), (act_arg_co, _act_arg_frr)) <-
    2072 
    -            if needs_frr_checks
    2073 
    -              -- See Wrinkle [Representation-polymorphism checking during subtyping]
    2074 
    -            then do { exp_frr_wrap <- hasFixedRuntimeRep (frr_ctxt True ) exp_arg
    2075 
    -                    ; act_frr_wrap <- hasFixedRuntimeRep (frr_ctxt False) act_arg
    2076 
    -                    ; return (exp_frr_wrap, act_frr_wrap) }
    2077 
    -            else return ((mkNomReflCo exp_arg, exp_arg), (mkNomReflCo act_arg, act_arg))
    2074 
    +  | Just arg_co <- getWpCo_maybe arg_wrap act_arg   -- arg_co :: exp_arg ~R# act_arg
    2075 
    +  , Just res_co <- getWpCo_maybe res_wrap act_res   -- res_co :: act_res ~R# exp_res
    2076 
    +  = -- The argument and result wrappers are both hole or cast;
    2077 
    +    -- so we can make do with a FunCo
    2078 
    +    -- See Note [Representation-polymorphism checking during subtyping]
    2079 
    +    do { mult_co <- unify act_mult exp_mult
    2080 
    +       ; let the_co = mkFunCo2 Representational act_af exp_af mult_co (mkSymCo arg_co) res_co
    2081 
    +       ; return (mkWpCastR the_co) }
    2082 
    +
    2083 
    +  | otherwise
    2084 
    +  = -- We need a full WpFun, with the eta-expansion that it entails
    2085 
    +    -- And hence we must add fixed-runtime-rep checks so that the eta-expansion is OK
    2086 
    +    -- See Note [Representation-polymorphism checking during subtyping]
    2087 
    +    do { (exp_arg_co, exp_arg_frr)  <- hasFixedRuntimeRep (frr_ctxt True ) exp_arg
    2088 
    +       ; (act_arg_co, _act_arg_frr) <- hasFixedRuntimeRep (frr_ctxt False) act_arg
    2089 
    +       -- exp_arg_frr, act_arg_frr :: Type   have fixed runtime-reps
    2090 
    +       -- exp_arg_co :: exp_arg ~ exp_arg_frr      Usually Refl
    2091 
    +       -- act_arg_co :: act_arg ~ act_arg_frr      Usually Refl
    2078 2092
    2079 2093 
              -- Enforce equality of multiplicities (not the more natural sub-multiplicity).
    2080 2094 
              -- See Note [Multiplicity in deep subsumption]
    ... ... @@ -2083,46 +2097,36 @@ mkWpFun_FRR unify pos act_af act_mult act_arg act_res exp_af exp_mult exp_arg ex
    2083 2097 
                -- equality to be Refl, but it might well not be (#26332).
    2084 2098
    2085 2099 
            ; let
    2086 
    -            exp_arg_fun_co =
    2100 
    +            exp_arg_fun_co =  -- (exp_arg_frr -> exp_res) ~ (exp_arg -> exp_res)
    2087 2101 
                   mkFunCo Nominal exp_af
    2088 
    -                 (mkReflCo Nominal exp_mult)
    2102 
    +                 (mkNomReflCo exp_mult)
    2089 2103 
                      (mkSymCo exp_arg_co)
    2090 
    -                 (mkReflCo Nominal exp_res)
    2091 
    -            act_arg_fun_co =
    2104 
    +                 (mkNomReflCo exp_res)
    2105 
    +            act_arg_fun_co =  -- (act_arg -> act_res) ~ (act_arg_frr -> act_res)
    2092 2106 
                   mkFunCo Nominal act_af
    2093 2107 
                      act_arg_mult_co
    2094 2108 
                      act_arg_co
    2095 
    -                 (mkReflCo Nominal act_res)
    2096 
    -            arg_wrap_frr =
    2109 
    +                 (mkNomReflCo act_res)
    2110 
    +            arg_wrap_frr =    -- exp_arg_frr ~~> act_arg_frr
    2097 2111 
                   mkWpCastN (mkSymCo exp_arg_co) <.> arg_wrap <.> mkWpCastN act_arg_co
    2098 
    -               --  exp_arg_co :: exp_arg ~> exp_arg_frr
    2099 
    -               --  act_arg_co :: act_arg ~> act_arg_frr
    2100 
    -               --  arg_wrap :: exp_arg ~> act_arg
    2101 
    -               --  arg_wrap_frr :: exp_arg_frr ~> act_arg_frr
    2102 2112
    2103 
    -       ; return $
    2104 
    -            mkWpCastN exp_arg_fun_co
    2113 
    +       ; return $   -- Whole thing :: (act_arg->act_res) ~~> (exp_arg->exp_ress)
    2114 
    +            mkWpCastN exp_arg_fun_co   -- (exp_ar_frr->exp_res) ~~> (exp_arg->exp_res)
    2105 2115 
                   <.>
    2106 2116 
                 mkWpFun arg_wrap_frr res_wrap (Scaled exp_mult exp_arg_frr) exp_res
    2107 
    -              <.>
    2108 
    -            mkWpCastN act_arg_fun_co
    2117 
    +              <.>                       -- (act_arg_frr->act_res) ~~> (exp_arg_frr->exp_res)
    2118 
    +            mkWpCastN act_arg_fun_co    -- (act_arg->act_res) ~~> (act_arg_frr->act_res)
    2109 2119 
            }
    2110 2120 
       where
    2111 
    -    needs_frr_checks :: Bool
    2112 
    -    needs_frr_checks =
    2113 
    -      not (hole_or_cast arg_wrap)
    2114 
    -        ||
    2115 
    -      not (hole_or_cast res_wrap)
    2116 
    -    hole_or_cast :: HsWrapper -> Bool
    2117 
    -    hole_or_cast WpHole = True
    2118 
    -    hole_or_cast (WpCast {}) = True
    2119 
    -    hole_or_cast _ = False
    2121 
    +    getWpCo_maybe :: HsWrapper -> Type -> Maybe CoercionR
    2122 
    +    -- See if a HsWrapper is just a coercion
    2123 
    +    getWpCo_maybe WpHole      ty = Just (mkRepReflCo ty)
    2124 
    +    getWpCo_maybe (WpCast co) _  = Just co
    2125 
    +    getWpCo_maybe _           _  = Nothing
    2126 
    +
    2120 2127 
         frr_ctxt :: Bool -> FixedRuntimeRepContext
    2121 
    -    frr_ctxt is_exp_ty =
    2122 
    -      FRRDeepSubsumption
    2123 
    -        { frrDSExpected = is_exp_ty
    2124 
    -        , frrDSPosition = pos
    2125 
    -        }
    2128 
    +    frr_ctxt is_exp_ty = FRRDeepSubsumption { frrDSExpected = is_exp_ty
    2129 
    +                                            , frrDSPosition = pos }
    2126 2130
    2127 2131 
     -----------------------
    2128 2132 
     deeplySkolemise :: SkolemInfo -> TcSigmaType
    ... ... @@ -2146,9 +2150,9 @@ deeplySkolemise skol_info ty
    2146 2150 
                ; let tvs     = binderVars bndrs
    2147 2151 
                      tvs1    = binderVars bndrs1
    2148 2152 
                      tv_prs1 = map tyVarName tvs `zip` bndrs1
    2149 
    -           ; return ( mkWpEta ids1 (mkWpTyLams tvs1
    2150 
    -                                    <.> mkWpEvLams ev_vars1
    2151 
    -                                    <.> wrap)
    2153 
    +           ; return ( mkWpEta ty ids1 (mkWpTyLams tvs1
    2154 
    +                                      <.> mkWpEvLams ev_vars1
    2155 
    +                                      <.> wrap)
    2152 2156 
                         , tv_prs1  ++ tvs_prs2
    2153 2157 
                         , ev_vars1 ++ ev_vars2
    2154 2158 
                         , mkScaledFunTys arg_tys' rho ) }
    ... ... @@ -2182,7 +2186,7 @@ deeplyInstantiate orig ty
    2182 2186 
                ; ids1  <- newSysLocalIds (fsLit "di") arg_tys'
    2183 2187 
                ; wrap1 <- instCall orig (mkTyVarTys tvs') theta'
    2184 2188 
                ; (wrap2, rho2) <- go subst' rho
    2185 
    -           ; return (mkWpEta ids1 (wrap2 <.> wrap1),
    2189 
    +           ; return (mkWpEta ty ids1 (wrap2 <.> wrap1),
    2186 2190 
                          mkScaledFunTys arg_tys' rho2) }
    2187 2191
    2188 2192 
           | otherwise

  • compiler/GHC/Tc/Zonk/Type.hs
    ... ... @@ -1233,13 +1233,16 @@ zonk_cmd_top (HsCmdTop (CmdTopTc stack_tys ty ids) cmd)
    1233 1233 
     -------------------------------------------------------------------------
    1234 1234 
     zonkCoFn :: HsWrapper -> ZonkBndrTcM HsWrapper
    1235 1235 
     zonkCoFn WpHole   = return WpHole
    1236 
    +zonkCoFn (WpSubType w)     = do { w' <- zonkCoFn w
    1237 
    +                                ; return (WpSubType w') }
    1236 1238 
     zonkCoFn (WpCompose c1 c2) = do { c1' <- zonkCoFn c1
    1237 1239 
                                     ; c2' <- zonkCoFn c2
    1238 1240 
                                     ; return (WpCompose c1' c2') }
    1239 
    -zonkCoFn (WpFun c1 c2 t1)  = do { c1' <- zonkCoFn c1
    1240 
    -                                ; c2' <- zonkCoFn c2
    1241 
    -                                ; t1' <- noBinders $ zonkScaledTcTypeToTypeX t1
    1242 
    -                                ; return (WpFun c1' c2' t1') }
    1241 
    +zonkCoFn (WpFun c1 c2 t1 t2) = do { c1' <- zonkCoFn c1
    1242 
    +                                  ; c2' <- zonkCoFn c2
    1243 
    +                                  ; t1' <- noBinders $ zonkScaledTcTypeToTypeX t1
    1244 
    +                                  ; t2' <- noBinders $ zonkTcTypeToTypeX t2
    1245 
    +                                  ; return (WpFun c1' c2' t1' t2') }
    1243 1246 
     zonkCoFn (WpCast co)   = WpCast  <$> noBinders (zonkCoToCo co)
    1244 1247 
     zonkCoFn (WpEvLam ev)  = WpEvLam <$> zonkEvBndrX ev
    1245 1248 
     zonkCoFn (WpEvApp arg) = WpEvApp <$> noBinders (zonkEvTerm arg)

  • testsuite/tests/simplCore/should_compile/T26349.hs
    1 
    +{-# LANGUAGE DeepSubsumption, RankNTypes #-}
    2 
    +module T26349 where
    3 
    +
    4 
    +{-# SPECIALIZE INLINE mapTCMT :: (forall b. IO b -> IO b) -> IO a -> IO a #-}
    5 
    +mapTCMT :: (forall b. m b -> n b) -> m a -> n a
    6 
    +mapTCMT f m = f m
    7 
    +
    8 
    +{-
    9 
    + We'll check
    10 
    +    tcExpr (mapTCMT) (Check ((forall b. IO b -> IO b) -> IO a_sk -> IO a_sk))
    11 
    +-}

  • testsuite/tests/simplCore/should_compile/T26349.stderr
    1 
    +==================== Tidy Core rules ====================
    2 
    +"USPEC mapTCMT @(*) @IO @IO @_"
    3 
    +    forall (@a). mapTCMT @(*) @IO @IO @a = mapTCMT_$smapTCMT @a

  • testsuite/tests/simplCore/should_compile/all.T
    ... ... @@ -559,3 +559,4 @@ test('T26051', [ grep_errmsg(r'\$wspecMe')
    559 559 
     test('T26115', [grep_errmsg(r'DFun')], compile, ['-O -ddump-simpl -dsuppress-uniques'])
    560 560 
     test('T26116', normal, compile, ['-O -ddump-rules'])
    561 561 
     test('T26117', [grep_errmsg(r'==')], compile, ['-O -ddump-simpl -dsuppress-uniques'])
    562 
    +test('T26349',  normal, compile, ['-O -ddump-rules'])

  • testsuite/tests/simplCore/should_compile/rule2.stderr
    ... ... @@ -10,18 +10,15 @@
    10 10
    11 11
    12 12 
     ==================== Grand total simplifier statistics ====================
    13 
    -Total ticks:     13
    13 
    +Total ticks:     11
    14 14
    15 
    -2 PreInlineUnconditionally
    16 
    -  1 ds
    17 
    -  1 f
    15 
    +1 PreInlineUnconditionally 1 f
    18 16 
     2 UnfoldingDone
    19 17 
       1 GHC.Internal.Base.id
    20 18 
       1 Roman.bar
    21 19 
     1 RuleFired 1 foo/bar
    22 20 
     1 LetFloatFromLet 1
    23 
    -7 BetaReduction
    24 
    -  1 ds
    21 
    +6 BetaReduction
    25 22 
       1 f
    26 23 
       1 a
    27 24 
       1 m

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