| ... |
... |
@@ -864,12 +864,13 @@ matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside |
|
864
|
864
|
, ft_arg = arg_ty, ft_res = res_ty })
|
|
865
|
865
|
= assert (isVisibleFunArg af) $
|
|
866
|
866
|
do { let arg_pos = arity - n_req + 1 -- 1 for the first argument etc
|
|
867
|
|
- ; (arg_co, arg_ty) <- hasFixedRuntimeRep (FRRExpectedFunTy herald arg_pos) arg_ty
|
|
|
867
|
+ ; (arg_co, arg_ty_frr) <- hasFixedRuntimeRep (FRRExpectedFunTy herald arg_pos) arg_ty
|
|
|
868
|
+ ; let arg_sty_frr = Scaled mult arg_ty_frr
|
|
868
|
869
|
; (wrap_res, result) <- check (n_req - 1)
|
|
869
|
|
- (mkCheckExpFunPatTy (Scaled mult arg_ty) : rev_pat_tys)
|
|
|
870
|
+ (mkCheckExpFunPatTy arg_sty_frr : rev_pat_tys)
|
|
870
|
871
|
res_ty
|
|
871
|
872
|
; let wrap_arg = mkWpCastN arg_co
|
|
872
|
|
- fun_wrap = mkWpFun wrap_arg wrap_res (Scaled mult arg_ty) res_ty
|
|
|
873
|
+ fun_wrap = mkWpFun wrap_arg wrap_res arg_sty_frr res_ty
|
|
873
|
874
|
-- mkWpFun: see Note [Smart contructor for WpFun] in GHC.Tc.Types.Evidence
|
|
874
|
875
|
; return (fun_wrap, result) }
|
|
875
|
876
|
|
| ... |
... |
@@ -1457,7 +1458,7 @@ tcSubTypeSigma :: CtOrigin -- where did the actual type arise / why are we |
|
1457
|
1458
|
-> TcSigmaType -> TcSigmaType -> TcM HsWrapper
|
|
1458
|
1459
|
-- External entry point, but no ExpTypes on either side
|
|
1459
|
1460
|
-- Checks that actual <= expected
|
|
1460
|
|
--- Returns HsWrapper :: actual ~ expected
|
|
|
1461
|
+-- Returns HsWrapper :: actual ~> expected
|
|
1461
|
1462
|
tcSubTypeSigma orig ctxt ty_actual ty_expected
|
|
1462
|
1463
|
= tc_sub_type (unifyType Nothing) orig ctxt ty_actual ty_expected
|
|
1463
|
1464
|
|
| ... |
... |
@@ -2068,15 +2069,20 @@ mkWpFun_FRR |
|
2068
|
2069
|
-> FunTyFlag -> Type -> TcType -> Type -- expected FunTy
|
|
2069
|
2070
|
-> HsWrapper -- ^ exp_arg ~> act_arg
|
|
2070
|
2071
|
-> HsWrapper -- ^ act_res ~> exp_res
|
|
2071
|
|
- -> TcM HsWrapper -- ^ act_funTy ~> exp_funTy
|
|
|
2072
|
+ -> TcM HsWrapper -- ^ (act_arg->act_res) ~> (exp_arg->exp_res)
|
|
2072
|
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
|
|
2073
|
|
- = do { ((exp_arg_co, exp_arg_frr), (act_arg_co, _act_arg_frr)) <-
|
|
2074
|
|
- if needs_frr_checks
|
|
2075
|
|
- -- See Wrinkle [Representation-polymorphism checking during subtyping]
|
|
2076
|
|
- then do { exp_frr_wrap <- hasFixedRuntimeRep (frr_ctxt True ) exp_arg
|
|
2077
|
|
- ; act_frr_wrap <- hasFixedRuntimeRep (frr_ctxt False) act_arg
|
|
2078
|
|
- ; return (exp_frr_wrap, act_frr_wrap) }
|
|
2079
|
|
- 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
|
+ = do { mult_co <- unify act_mult exp_mult
|
|
|
2077
|
+ ; let the_co = mkFunCo2 Representational act_af exp_af mult_co (mkSymCo arg_co) res_co
|
|
|
2078
|
+ ; return (mkWpCastR the_co) }
|
|
|
2079
|
+
|
|
|
2080
|
+ | otherwise -- See Wrinkle [Representation-polymorphism checking during subtyping]
|
|
|
2081
|
+ = do { (exp_arg_co, exp_arg_frr) <- hasFixedRuntimeRep (frr_ctxt True ) exp_arg
|
|
|
2082
|
+ ; (act_arg_co, _act_arg_frr) <- hasFixedRuntimeRep (frr_ctxt False) act_arg
|
|
|
2083
|
+ -- exp_arg_frr, act_arg_frr :: Type have fixed runtime-reps
|
|
|
2084
|
+ -- exp_arg_co :: exp_arg ~ exp_arg_frr Usually Refl
|
|
|
2085
|
+ -- act_arg_co :: act_arg ~ act_arg_frr Usually Refl
|
|
2080
|
2086
|
|
|
2081
|
2087
|
-- Enforce equality of multiplicities (not the more natural sub-multiplicity).
|
|
2082
|
2088
|
-- See Note [Multiplicity in deep subsumption]
|
| ... |
... |
@@ -2085,46 +2091,36 @@ mkWpFun_FRR unify pos act_af act_mult act_arg act_res exp_af exp_mult exp_arg ex |
|
2085
|
2091
|
-- equality to be Refl, but it might well not be (#26332).
|
|
2086
|
2092
|
|
|
2087
|
2093
|
; let
|
|
2088
|
|
- exp_arg_fun_co =
|
|
|
2094
|
+ exp_arg_fun_co = -- (exp_arg_frr -> exp_res) ~ (exp_arg -> exp_res)
|
|
2089
|
2095
|
mkFunCo Nominal exp_af
|
|
2090
|
2096
|
(mkReflCo Nominal exp_mult)
|
|
2091
|
2097
|
(mkSymCo exp_arg_co)
|
|
2092
|
2098
|
(mkReflCo Nominal exp_res)
|
|
2093
|
|
- act_arg_fun_co =
|
|
|
2099
|
+ act_arg_fun_co = -- (act_arg -> act_res) ~ (act_arg_frr -> act_res)
|
|
2094
|
2100
|
mkFunCo Nominal act_af
|
|
2095
|
2101
|
act_arg_mult_co
|
|
2096
|
2102
|
act_arg_co
|
|
2097
|
2103
|
(mkReflCo Nominal act_res)
|
|
2098
|
|
- arg_wrap_frr =
|
|
|
2104
|
+ arg_wrap_frr = -- exp_arg_frr ~> act_arg_frr
|
|
2099
|
2105
|
mkWpCastN (mkSymCo exp_arg_co) <.> arg_wrap <.> mkWpCastN act_arg_co
|
|
2100
|
|
- -- exp_arg_co :: exp_arg ~> exp_arg_frr
|
|
2101
|
|
- -- act_arg_co :: act_arg ~> act_arg_frr
|
|
2102
|
|
- -- arg_wrap :: exp_arg ~> act_arg
|
|
2103
|
|
- -- arg_wrap_frr :: exp_arg_frr ~> act_arg_frr
|
|
2104
|
2106
|
|
|
2105
|
|
- ; return $
|
|
2106
|
|
- mkWpCastN exp_arg_fun_co
|
|
|
2107
|
+ ; return $ -- Whole thing :: (act_arg->act_res) ~> (exp_arg->exp_ress)
|
|
|
2108
|
+ mkWpCastN exp_arg_fun_co -- (exp_ar_frr->exp_res) ~> (exp_arg->exp_res)
|
|
2107
|
2109
|
<.>
|
|
2108
|
2110
|
mkWpFun arg_wrap_frr res_wrap (Scaled exp_mult exp_arg_frr) exp_res
|
|
2109
|
|
- <.>
|
|
2110
|
|
- mkWpCastN act_arg_fun_co
|
|
|
2111
|
+ <.> -- (act_arg_frr->act_res) ~> (exp_arg_frr->exp_res)
|
|
|
2112
|
+ mkWpCastN act_arg_fun_co -- (act_arg->act_res) ~> (act_arg_frr->act_res)
|
|
2111
|
2113
|
}
|
|
2112
|
2114
|
where
|
|
2113
|
|
- needs_frr_checks :: Bool
|
|
2114
|
|
- needs_frr_checks =
|
|
2115
|
|
- not (hole_or_cast arg_wrap)
|
|
2116
|
|
- ||
|
|
2117
|
|
- not (hole_or_cast res_wrap)
|
|
2118
|
|
- hole_or_cast :: HsWrapper -> Bool
|
|
2119
|
|
- hole_or_cast WpHole = True
|
|
2120
|
|
- hole_or_cast (WpCast {}) = True
|
|
2121
|
|
- hole_or_cast _ = False
|
|
|
2115
|
+ getWpCo_maybe :: HsWrapper -> Type -> Maybe CoercionR
|
|
|
2116
|
+ -- See if a HsWrapper is just a coercion
|
|
|
2117
|
+ getWpCo_maybe WpHole ty = Just (mkRepReflCo ty)
|
|
|
2118
|
+ getWpCo_maybe (WpCast co) _ = Just co
|
|
|
2119
|
+ getWpCo_maybe _ _ = Nothing
|
|
|
2120
|
+
|
|
2122
|
2121
|
frr_ctxt :: Bool -> FixedRuntimeRepContext
|
|
2123
|
|
- frr_ctxt is_exp_ty =
|
|
2124
|
|
- FRRDeepSubsumption
|
|
2125
|
|
- { frrDSExpected = is_exp_ty
|
|
2126
|
|
- , frrDSPosition = pos
|
|
2127
|
|
- }
|
|
|
2122
|
+ frr_ctxt is_exp_ty = FRRDeepSubsumption { frrDSExpected = is_exp_ty
|
|
|
2123
|
+ , frrDSPosition = pos }
|
|
2128
|
2124
|
|
|
2129
|
2125
|
-----------------------
|
|
2130
|
2126
|
deeplySkolemise :: SkolemInfo -> TcSigmaType
|