| ... |
... |
@@ -290,10 +290,9 @@ Now we split into two cases: |
|
290
|
290
|
|
|
291
|
291
|
5. Case DoQL: use Quick Look
|
|
292
|
292
|
|
|
293
|
|
- 5.1 Use `quickLookResultType` to take a quick look at the result type,
|
|
294
|
|
- when in checking mode. This is the shaded part of APP-Downarrow
|
|
295
|
|
- in Fig 5. It also implements the key part of
|
|
296
|
|
- Note [Unify with expected type before typechecking arguments]
|
|
|
293
|
+ 5.1 Take a quick look at the result type, when in checking mode. This is the
|
|
|
294
|
+ shaded part of APP-Downarrow in Fig 5. It also implements the key part
|
|
|
295
|
+ of Note [Unify with expected type before typechecking arguments]
|
|
297
|
296
|
|
|
298
|
297
|
5.2 Check the arguments with `tcValArgs`. Importantly, this will monomorphise
|
|
299
|
298
|
all the instantiation variables of the call.
|
| ... |
... |
@@ -404,29 +403,28 @@ tcApp rn_expr exp_res_ty |
|
404
|
403
|
DoQL -> do { traceTc "tcApp:DoQL" (ppr rn_fun $$ ppr app_res_rho)
|
|
405
|
404
|
|
|
406
|
405
|
-- Step 5.1: Take a quick look at the result type
|
|
407
|
|
- ; quickLookResultType app_res_rho exp_res_ty
|
|
408
|
|
- ; inst_args' <- mapM quickLookArg inst_args
|
|
|
406
|
+ ; inst_args_with_guards <- case exp_res_ty of
|
|
|
407
|
+ Check exp_rho -> do { qlUnify app_res_rho exp_rho
|
|
|
408
|
+ ; mapM reGuardArg inst_args }
|
|
|
409
|
+ Infer {} -> return inst_args
|
|
409
|
410
|
|
|
410
|
|
- -- Step 5.2: typecheck the arguments, and monomorphise
|
|
411
|
|
- -- any un-unified instantiation variables
|
|
412
|
|
- ; tc_args <- tcValArgs DoQL inst_args'
|
|
|
411
|
+ ; inst_args_ql <- mapM quickLookArg inst_args_with_guards
|
|
413
|
412
|
|
|
414
|
413
|
-- Step 5.3: zonk to expose the polymorphism hidden under
|
|
415
|
414
|
-- QuickLook instantiation variables in `app_res_rho`
|
|
416
|
415
|
; app_res_rho <- liftZonkM $ zonkTcType app_res_rho
|
|
417
|
416
|
|
|
418
|
417
|
-- Step 5.4: subsumption check against the expected type
|
|
419
|
|
- ; res_wrap <- checkResultTy rn_expr tc_head inst_args
|
|
|
418
|
+ ; res_wrap <- checkResultTy rn_expr tc_head inst_args_ql
|
|
420
|
419
|
app_res_rho exp_res_ty
|
|
|
420
|
+
|
|
|
421
|
+ -- Step 5.2: typecheck the arguments, and monomorphise
|
|
|
422
|
+ -- any un-unified instantiation variables
|
|
|
423
|
+ ; tc_args <- tcValArgs DoQL inst_args_ql
|
|
|
424
|
+
|
|
421
|
425
|
-- Step 5.5: wrap up
|
|
422
|
426
|
; finishApp tc_head tc_args app_res_rho res_wrap } }
|
|
423
|
427
|
|
|
424
|
|
-quickLookResultType :: TcRhoType -> ExpRhoType -> TcM ()
|
|
425
|
|
--- This function implements the shaded bit of rule APP-Downarrow in
|
|
426
|
|
--- Fig 5 of the QL paper: "A quick look at impredicativity" (ICFP'20).
|
|
427
|
|
-quickLookResultType app_res_rho (Check exp_rho) = qlUnify app_res_rho exp_rho
|
|
428
|
|
-quickLookResultType _ _ = return ()
|
|
429
|
|
-
|
|
430
|
428
|
-- | Variant of 'getDeepSubsumptionFlag' which enables a top-level subsumption
|
|
431
|
429
|
-- in order to implement the plan of Note [Typechecking data constructors].
|
|
432
|
430
|
getDeepSubsumptionFlag_DataConHead :: HsExpr GhcTc -> TcM DeepSubsumptionFlag
|
| ... |
... |
@@ -458,7 +456,7 @@ finishApp tc_head@(tc_fun,_) tc_args app_res_rho res_wrap |
|
458
|
456
|
-- This is usually just a unification, but with deep subsumption there is more to do.
|
|
459
|
457
|
checkResultTy :: HsExpr GhcRn
|
|
460
|
458
|
-> (HsExpr GhcTc, AppCtxt) -- Head
|
|
461
|
|
- -> [HsExprArg p] -- Arguments, just error messages
|
|
|
459
|
+ -> [HsExprArg p] -- Arguments, just for error messages
|
|
462
|
460
|
-> TcRhoType -- Inferred type of the application; zonked to
|
|
463
|
461
|
-- expose foralls, but maybe not /deeply/ instantiated
|
|
464
|
462
|
-> ExpRhoType -- Expected type; this is deeply skolemised
|
| ... |
... |
@@ -1843,14 +1841,15 @@ This turned out to be more subtle than I expected. Wrinkles: |
|
1843
|
1841
|
|
|
1844
|
1842
|
-}
|
|
1845
|
1843
|
|
|
1846
|
|
-quickLookArg :: HsExprArg 'TcpInst
|
|
1847
|
|
- -> TcM (HsExprArg 'TcpInst)
|
|
|
1844
|
+quickLookArg :: HsExprArg 'TcpInst -> TcM (HsExprArg 'TcpInst)
|
|
1848
|
1845
|
-- quickLookArg1 implements the "QL Argument" judgement in Fig 5 of the paper
|
|
1849
|
1846
|
-- See Note [Quick Look at value arguments]
|
|
1850
|
1847
|
quickLookArg e_arg@(EValArg { ea_ctxt = ctxt
|
|
1851
|
1848
|
, ea_arg = larg@(L _ arg)
|
|
1852
|
|
- , ea_arg_ty = orig_arg_ty@(Scaled _ orig_arg_rho) })
|
|
1853
|
|
- = do { is_rho <- tcIsDeepRho orig_arg_rho
|
|
|
1849
|
+ , ea_arg_ty = orig_arg_ty })
|
|
|
1850
|
+ = do { let !(Scaled _ orig_arg_rho) = orig_arg_ty
|
|
|
1851
|
+ -- NB: orig_arg_rho may not be zonked, but that's ok
|
|
|
1852
|
+ ; is_rho <- tcIsDeepRho orig_arg_rho
|
|
1854
|
1853
|
; traceTc "qla" (ppr orig_arg_ty $$ ppr is_rho)
|
|
1855
|
1854
|
; if not is_rho
|
|
1856
|
1855
|
then return e_arg
|
| ... |
... |
@@ -1887,7 +1886,6 @@ quickLookArg e_arg@(EValArg { ea_ctxt = ctxt |
|
1887
|
1886
|
-- not usage constraints. See (QLA6) in Note [Quick Look at
|
|
1888
|
1887
|
-- value arguments]
|
|
1889
|
1888
|
|
|
1890
|
|
-{-
|
|
1891
|
1889
|
; traceTc "quickLookArg 2" $
|
|
1892
|
1890
|
vcat [ text "arg:" <+> ppr arg
|
|
1893
|
1891
|
, text "orig_arg_rho:" <+> ppr orig_arg_rho
|
| ... |
... |
@@ -1895,36 +1893,29 @@ quickLookArg e_arg@(EValArg { ea_ctxt = ctxt |
|
1895
|
1893
|
|
|
1896
|
1894
|
-- Step 3: Check the two other premises of APP-lightning-bolt (Fig 5 in the paper)
|
|
1897
|
1895
|
-- Namely: (A) is orig_arg_rho is guarded
|
|
1898
|
|
- -- or: (B) fiv(app_res_rho) = emptyset
|
|
|
1896
|
+ -- or: (B) fiv(app_res_rho) = emptyset
|
|
|
1897
|
+ -- then Step 4: do quick-look unification if either (A) or (B) hold
|
|
|
1898
|
+ --
|
|
|
1899
|
+ -- For (B) see Note [The fiv test in quickLookArg]
|
|
1899
|
1900
|
-- This tells us if the quick look at the argument yields information that
|
|
1900
|
1901
|
-- influences the enclosing function call
|
|
1901
|
1902
|
-- NB: `isGuardedTy` is computed based on the original,
|
|
1902
|
1903
|
-- unzonked orig_arg_rho, so that we deliberately do not exploit
|
|
1903
|
1904
|
-- guardedness that emerges a result of QL on earlier args
|
|
1904
|
1905
|
-- In contrast, we must do the `anyFreeKappa` test /after/ tcInstFun; see (QLA3).
|
|
1905
|
|
- ; arg_influences_enclosing_call
|
|
1906
|
|
- <- if isGuardedTy orig_arg_rho
|
|
1907
|
|
- then return True
|
|
1908
|
|
- else not <$> anyFreeKappa app_res_rho -- (B)
|
|
1909
|
|
- -- For (B) see Note [The fiv test in quickLookArg]
|
|
1910
|
|
-
|
|
1911
|
|
- -- Step 4: do quick-look unification if either (A) or (B) hold
|
|
1912
|
|
- -- NB: orig_arg_rho may not be zonked, but that's ok
|
|
1913
|
|
- ; when arg_influences_enclosing_call $
|
|
1914
|
|
- qlUnify app_res_rho orig_arg_rho
|
|
1915
|
|
--}
|
|
1916
|
1906
|
|
|
1917
|
|
- ; (arg_influences_call, inst_args')
|
|
1918
|
|
- <- if isGuardedTy orig_arg_rho
|
|
|
1907
|
+ ; (arg_influences_call, inst_args_ql)
|
|
|
1908
|
+ <- if isGuardedTy orig_arg_rho -- (A)
|
|
1919
|
1909
|
then do { qlUnify app_res_rho orig_arg_rho
|
|
1920
|
|
- ; inst_args' <- mapM quickLookArg inst_args
|
|
1921
|
|
- ; return (True, inst_args') }
|
|
1922
|
|
- else do { inst_args' <- mapM quickLookArg inst_args
|
|
1923
|
|
- ; has_free_inst_vars <- anyFreeKappa app_res_rho
|
|
|
1910
|
+ ; inst_args_with_guards <- mapM reGuardArg inst_args
|
|
|
1911
|
+ ; inst_args_ql <- mapM quickLookArg inst_args_with_guards
|
|
|
1912
|
+ ; return (True, inst_args_ql) }
|
|
|
1913
|
+ else do { inst_args_ql <- mapM quickLookArg inst_args
|
|
|
1914
|
+ ; has_free_inst_vars <- anyFreeKappa app_res_rho --(B)
|
|
1924
|
1915
|
; if has_free_inst_vars
|
|
1925
|
|
- then return (False, inst_args')
|
|
|
1916
|
+ then return (False, inst_args_ql)
|
|
1926
|
1917
|
else do { qlUnify app_res_rho orig_arg_rho
|
|
1927
|
|
- ; return (True, inst_args') } }
|
|
|
1918
|
+ ; return (True, inst_args_ql) } }
|
|
1928
|
1919
|
|
|
1929
|
1920
|
; traceTc "quickLookArg done }" (ppr rn_fun)
|
|
1930
|
1921
|
|
| ... |
... |
@@ -1933,7 +1924,7 @@ quickLookArg e_arg@(EValArg { ea_ctxt = ctxt |
|
1933
|
1924
|
, eaql_larg = larg
|
|
1934
|
1925
|
, eaql_tc_fun = tc_head
|
|
1935
|
1926
|
, eaql_fun_ue = fun_ue
|
|
1936
|
|
- , eaql_args = inst_args'
|
|
|
1927
|
+ , eaql_args = inst_args_ql
|
|
1937
|
1928
|
, eaql_wanted = wanted
|
|
1938
|
1929
|
, eaql_encl = arg_influences_call
|
|
1939
|
1930
|
, eaql_res_rho = app_res_rho }) }}}}
|
| ... |
... |
@@ -1970,6 +1961,15 @@ tcIsDeepRho ty |
|
1970
|
1961
|
| otherwise
|
|
1971
|
1962
|
= return True
|
|
1972
|
1963
|
|
|
|
1964
|
+reGuardArg :: HsExprArg 'TcpInst -> TcM (HsExprArg 'TcpInst)
|
|
|
1965
|
+-- Zonk the result type of an EValArg, so that a subseqent
|
|
|
1966
|
+-- call to isGuardedTy will see the unifications so far
|
|
|
1967
|
+reGuardArg arg@(EValArg { ea_arg_ty = arg_ty })
|
|
|
1968
|
+ = do { arg_ty' <- liftZonkM $ zonkScaledTcType arg_ty
|
|
|
1969
|
+ ; return (arg { ea_arg_ty = arg_ty' }) }
|
|
|
1970
|
+reGuardArg arg
|
|
|
1971
|
+ = return arg
|
|
|
1972
|
+
|
|
1973
|
1973
|
isGuardedTy :: TcType -> Bool
|
|
1974
|
1974
|
isGuardedTy ty
|
|
1975
|
1975
|
| Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
|