| ... |
... |
@@ -188,11 +188,12 @@ tcExprSigma :: Bool -> HsExpr GhcRn -> TcM (HsExpr GhcTc, TcSigmaType) |
|
188
|
188
|
tcExprSigma inst rn_expr
|
|
189
|
189
|
= do { (fun@(rn_fun,fun_lspan), rn_args) <- splitHsApps rn_expr
|
|
190
|
190
|
; (tc_fun, fun_sigma) <- tcInferAppHead fun
|
|
|
191
|
+ ; ds_flag <- getDeepSubsumptionFlag_DataConHead tc_fun
|
|
191
|
192
|
; fun_orig <- mk_origin fun_lspan rn_fun rn_fun
|
|
192
|
|
-
|
|
193
|
193
|
; traceTc "tcExprSigma" (vcat [ text "rn_expr:" <+> ppr rn_expr
|
|
194
|
194
|
, text "tc_fun" <+> ppr tc_fun ])
|
|
195
|
|
- ; (inst_args, app_res_sigma) <- tcInstFun DoQL inst (fun_orig, rn_fun, fun_lspan) tc_fun fun_sigma rn_args
|
|
|
195
|
+ ; (inst_args, app_res_sigma) <- tcInstFun DoQL inst ds_flag (fun_orig, rn_fun, fun_lspan)
|
|
|
196
|
+ tc_fun fun_sigma rn_args
|
|
196
|
197
|
; tc_args <- tcValArgs DoQL (rn_fun, fun_lspan) inst_args
|
|
197
|
198
|
; let tc_expr = rebuildHsApps (tc_fun, fun_lspan) tc_args
|
|
198
|
199
|
; return (tc_expr, app_res_sigma) }
|
| ... |
... |
@@ -412,6 +413,7 @@ tcApp rn_expr exp_res_ty |
|
412
|
413
|
IIF_ShallowRho -> True
|
|
413
|
414
|
IIF_DeepRho -> True
|
|
414
|
415
|
IIF_Sigma -> False
|
|
|
416
|
+ ; ds_flag <- getDeepSubsumptionFlag_DataConHead tc_fun
|
|
415
|
417
|
|
|
416
|
418
|
-- Step 3.1: Instantiate the function type (taking a quick look at args)
|
|
417
|
419
|
; do_ql <- wantQuickLook rn_fun
|
| ... |
... |
@@ -431,11 +433,10 @@ tcApp rn_expr exp_res_ty |
|
431
|
433
|
, text "fun_origin" <+> ppr fun_orig
|
|
432
|
434
|
, text "do_ql:" <+> ppr do_ql]
|
|
433
|
435
|
; (inst_args, app_res_rho)
|
|
434
|
|
- <- tcInstFun do_ql inst_final (fun_orig, rn_fun, fun_lspan) tc_fun fun_sigma rn_args
|
|
|
436
|
+ <- tcInstFun do_ql inst_final ds_flag (fun_orig, rn_fun, fun_lspan) tc_fun fun_sigma rn_args
|
|
435
|
437
|
-- See (TCAPP1) and (TCAPP2) in
|
|
436
|
438
|
-- Note [tcApp: typechecking applications]
|
|
437
|
439
|
|
|
438
|
|
- ; ds_flag <- getDeepSubsumptionFlag_DataConHead tc_fun
|
|
439
|
440
|
; case do_ql of
|
|
440
|
441
|
NoQL -> do { traceTc "tcApp:NoQL" (ppr rn_fun $$ ppr app_res_rho)
|
|
441
|
442
|
|
| ... |
... |
@@ -652,6 +653,7 @@ tcValArg _ pos (fun, fun_lspan) (EValArgQL { |
|
652
|
653
|
, eaql_arg_ty = sc_arg_ty
|
|
653
|
654
|
, eaql_larg = larg@(L arg_loc rn_expr)
|
|
654
|
655
|
, eaql_tc_fun = tc_head
|
|
|
656
|
+ , eaql_ds_flag = ds_flag
|
|
655
|
657
|
, eaql_rn_fun = rn_fun
|
|
656
|
658
|
, eaql_fun_ue = head_ue
|
|
657
|
659
|
, eaql_args = inst_args
|
| ... |
... |
@@ -670,7 +672,6 @@ tcValArg _ pos (fun, fun_lspan) (EValArgQL { |
|
670
|
672
|
, text "head_lspan" <+> ppr fun_lspan
|
|
671
|
673
|
, text "tc_head" <+> ppr tc_head])
|
|
672
|
674
|
|
|
673
|
|
- ; ds_flag <- getDeepSubsumptionFlag_DataConHead (fst tc_head)
|
|
674
|
675
|
; (wrap, arg')
|
|
675
|
676
|
<- tcScalingUsage mult $
|
|
676
|
677
|
tcSkolemise ds_flag GenSigCtxt exp_arg_ty $ \ exp_arg_rho ->
|
| ... |
... |
@@ -728,15 +729,16 @@ tcInstFun :: QLFlag |
|
728
|
729
|
-- always return a rho-type (but not a deep-rho type)
|
|
729
|
730
|
-- Generally speaking we pass in True; in Fig 5 of the paper
|
|
730
|
731
|
-- |-inst returns a rho-type
|
|
|
732
|
+ -> DeepSubsumptionFlag
|
|
731
|
733
|
-> (CtOrigin, HsExpr GhcRn, SrcSpan)
|
|
732
|
|
- -> HsExpr GhcTc -- ANI: TODO, move HsExpr GhcRn, SrcSpan to CtOrigin
|
|
|
734
|
+ -> HsExpr GhcTc
|
|
733
|
735
|
-> TcSigmaType -> [HsExprArg 'TcpRn]
|
|
734
|
736
|
-> TcM ( [HsExprArg 'TcpInst]
|
|
735
|
737
|
, TcSigmaType ) -- Does not instantiate trailing invisible foralls
|
|
736
|
738
|
-- This crucial function implements the |-inst judgement in Fig 4, plus the
|
|
737
|
739
|
-- modification in Fig 5, of the QL paper:
|
|
738
|
740
|
-- "A quick look at impredicativity" (ICFP'20).
|
|
739
|
|
-tcInstFun do_ql inst_final (fun_orig, rn_fun, fun_lspan) tc_fun fun_sigma rn_args
|
|
|
741
|
+tcInstFun do_ql inst_final ds_flag (fun_orig, rn_fun, fun_lspan) tc_fun fun_sigma rn_args
|
|
740
|
742
|
= do { traceTc "tcInstFun" (vcat [ text "origin" <+> ppr fun_orig
|
|
741
|
743
|
, text "tc_fun" <+> ppr tc_fun
|
|
742
|
744
|
, text "fun_sigma" <+> ppr fun_sigma
|
| ... |
... |
@@ -935,7 +937,7 @@ tcInstFun do_ql inst_final (fun_orig, rn_fun, fun_lspan) tc_fun fun_sigma rn_arg |
|
935
|
937
|
(Just $ HsExprTcThing tc_fun)
|
|
936
|
938
|
(n_val_args, fun_sigma) fun_ty
|
|
937
|
939
|
|
|
938
|
|
- ; ds_flag <- getDeepSubsumptionFlag_DataConHead tc_fun
|
|
|
940
|
+ -- ; ds_flag <- getDeepSubsumptionFlag_DataConHead tc_fun
|
|
939
|
941
|
; arg' <- quickLookArg ds_flag do_ql pos ctxt (rn_fun, fun_lspan) arg arg_ty
|
|
940
|
942
|
; let acc' = arg' : addArgWrap (mkWpCastN fun_co) acc
|
|
941
|
943
|
; go (pos+1) acc' res_ty rest_args }
|
| ... |
... |
@@ -2022,10 +2024,10 @@ quickLookArg1 pos app_lspan (fun, fun_lspan) larg@(L _ arg) sc_arg_ty@(Scaled _ |
|
2022
|
2024
|
; do_ql <- wantQuickLook rn_fun_arg
|
|
2023
|
2025
|
|
|
2024
|
2026
|
; arg_orig <- mk_origin fun_lspan_arg rn_fun_arg fun
|
|
2025
|
|
-
|
|
|
2027
|
+ ; ds_flag_arg <- getDeepSubsumptionFlag_DataConHead tc_fun_arg_head
|
|
2026
|
2028
|
; ((inst_args, app_res_rho), wanted)
|
|
2027
|
2029
|
<- captureConstraints $
|
|
2028
|
|
- tcInstFun do_ql True (arg_orig, rn_fun_arg, fun_lspan_arg) tc_fun_arg_head fun_sigma_arg_head rn_args
|
|
|
2030
|
+ tcInstFun do_ql True ds_flag_arg (arg_orig, rn_fun_arg, fun_lspan_arg) tc_fun_arg_head fun_sigma_arg_head rn_args
|
|
2029
|
2031
|
-- We must capture type-class and equality constraints here, but
|
|
2030
|
2032
|
-- not equality constraints. See (QLA6) in Note [Quick Look at
|
|
2031
|
2033
|
-- value arguments]
|
| ... |
... |
@@ -2062,6 +2064,7 @@ quickLookArg1 pos app_lspan (fun, fun_lspan) larg@(L _ arg) sc_arg_ty@(Scaled _ |
|
2062
|
2064
|
, eaql_larg = larg
|
|
2063
|
2065
|
, eaql_tc_fun = arg_tc_head
|
|
2064
|
2066
|
, eaql_rn_fun = rn_fun_arg
|
|
|
2067
|
+ , eaql_ds_flag = ds_flag_arg
|
|
2065
|
2068
|
, eaql_fun_ue = fun_ue
|
|
2066
|
2069
|
, eaql_args = inst_args
|
|
2067
|
2070
|
, eaql_wanted = wanted
|