| ... |
... |
@@ -354,6 +354,44 @@ Unify result type /before/ typechecking the args |
|
354
|
354
|
• In the first argument of ‘Pair’, namely ‘"yes"’
|
|
355
|
355
|
|
|
356
|
356
|
The latter is much better. That is why we call checkResultType before tcValArgs.
|
|
|
357
|
+
|
|
|
358
|
+Note [QuickLook: arguments before result]
|
|
|
359
|
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
|
360
|
+Generally we try to push the expected result type into the call;
|
|
|
361
|
+see Note [Unify with expected type before typechecking arguments].
|
|
|
362
|
+But surprisingly we can't do that for QuickLook. (#26599 was a failed
|
|
|
363
|
+attempt to suggest this.) Consider
|
|
|
364
|
+ h :: (Int->Int) -> Int ids :: [forall a. a->a]
|
|
|
365
|
+and the call
|
|
|
366
|
+ h (head ids)
|
|
|
367
|
+Let's say we instantiate `head :: [a] -> a` with `a:=kappa`.
|
|
|
368
|
+We QuickLook at the argument with expected type (Int->Int). We must NOT
|
|
|
369
|
+unify kappa:=(Int->Int), because kappa:=forall a. a->a is the only
|
|
|
370
|
+solution, and one that we will find if we look at the argument first.
|
|
|
371
|
+
|
|
|
372
|
+TL;DR: we must do `quickLookArg` on all arguments before doing `quickLookResultType`
|
|
|
373
|
+on the result type.
|
|
|
374
|
+
|
|
|
375
|
+Remember: `quickLookResultType` is really anticipating a /subsumption/ test, not
|
|
|
376
|
+an equality test. Doing `qlUnify` on the result type (always a rho-type) is
|
|
|
377
|
+in general wrong if there is an un-guarded kappa in the result type. It's wrong
|
|
|
378
|
+UNLESS we have already gotten all the info about `kappa` (from the
|
|
|
379
|
+arguments) that we are going to get. That's why we QuickLook the arguments first.
|
|
|
380
|
+
|
|
|
381
|
+This is a bit sad, as #26599 shows. Consider
|
|
|
382
|
+
|
|
|
383
|
+ woo :: (x, [forall a. a->a])
|
|
|
384
|
+ bar1 = snd woo
|
|
|
385
|
+ bar2 = snd (id woo)
|
|
|
386
|
+
|
|
|
387
|
+For `bar1` we instantiate `snd` at [a:=k1,b:=k2]. Then we QL on the argument `woo`
|
|
|
388
|
+(instantiating with `x:=k3`. Since the result type is guarded we qlUnify
|
|
|
389
|
+ (k3,forall a.a->a) ~ (k1,k2)
|
|
|
390
|
+and thus succeed in discovering k2:=forall a.a->a, as desired.
|
|
|
391
|
+
|
|
|
392
|
+But for `bar2` we fail. When quick-looking (id woo) we instantiate `id` with [a:=k],
|
|
|
393
|
+and quick-look the argument `woo` with expected type `k`. That's not guarded,
|
|
|
394
|
+so we get no information. Adding the `id` call makes it un-typeable. Boo.
|
|
357
|
395
|
-}
|
|
358
|
396
|
|
|
359
|
397
|
tcApp :: HsExpr GhcRn
|
| ... |
... |
@@ -403,24 +441,23 @@ tcApp rn_expr exp_res_ty |
|
403
|
441
|
DoQL -> do { traceTc "tcApp:DoQL" (ppr rn_fun $$ ppr app_res_rho)
|
|
404
|
442
|
|
|
405
|
443
|
-- Step 5.1: Take a quick look at the result type
|
|
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
|
|
410
|
|
-
|
|
411
|
|
- ; inst_args_ql <- mapM quickLookArg inst_args_with_guards
|
|
|
444
|
+ -- See Note [QuickLook: arguments before result]
|
|
|
445
|
+ ; case exp_res_ty of
|
|
|
446
|
+ Check exp_rho -> quickLookResultType app_res_rho exp_rho
|
|
|
447
|
+ Infer {} -> return ()
|
|
412
|
448
|
|
|
413
|
449
|
-- Step 5.3: zonk to expose the polymorphism hidden under
|
|
414
|
450
|
-- QuickLook instantiation variables in `app_res_rho`
|
|
415
|
451
|
; app_res_rho <- liftZonkM $ zonkTcType app_res_rho
|
|
416
|
452
|
|
|
417
|
453
|
-- Step 5.4: subsumption check against the expected type
|
|
418
|
|
- ; res_wrap <- checkResultTy rn_expr tc_head inst_args_ql
|
|
419
|
|
- app_res_rho exp_res_ty
|
|
|
454
|
+ -- See Note [Unify with expected type before typechecking arguments]
|
|
|
455
|
+ ; res_wrap <- checkResultTy rn_expr tc_head inst_args
|
|
|
456
|
+ app_res_rho exp_res_ty
|
|
420
|
457
|
|
|
421
|
458
|
-- Step 5.2: typecheck the arguments, and monomorphise
|
|
422
|
459
|
-- any un-unified instantiation variables
|
|
423
|
|
- ; tc_args <- tcValArgs DoQL inst_args_ql
|
|
|
460
|
+ ; tc_args <- tcValArgs DoQL inst_args
|
|
424
|
461
|
|
|
425
|
462
|
-- Step 5.5: wrap up
|
|
426
|
463
|
; finishApp tc_head tc_args app_res_rho res_wrap } }
|
| ... |
... |
@@ -589,13 +626,13 @@ tcValArg _ (EValArgQL { eaql_wanted = wanted |
|
589
|
626
|
|
|
590
|
627
|
-- Unify with context if we have not already done so
|
|
591
|
628
|
-- See (QLA4) in Note [Quick Look at value arguments]
|
|
592
|
|
- ; unless arg_influences_enclosing_call $ -- Don't repeat
|
|
593
|
|
- qlUnify app_res_rho exp_arg_rho -- the qlUnify
|
|
|
629
|
+ ; unless arg_influences_enclosing_call $ -- Don't repeat
|
|
|
630
|
+ quickLookResultType app_res_rho exp_arg_rho -- the qlUnify
|
|
594
|
631
|
|
|
595
|
|
- ; tc_args <- tcValArgs DoQL inst_args
|
|
596
|
632
|
; app_res_rho <- liftZonkM $ zonkTcType app_res_rho
|
|
597
|
633
|
; res_wrap <- checkResultTy rn_expr tc_head inst_args
|
|
598
|
634
|
app_res_rho (mkCheckExpType exp_arg_rho)
|
|
|
635
|
+ ; tc_args <- tcValArgs DoQL inst_args
|
|
599
|
636
|
; finishApp tc_head tc_args app_res_rho res_wrap }
|
|
600
|
637
|
|
|
601
|
638
|
; traceTc "tcEValArgQL }" $
|
| ... |
... |
@@ -607,6 +644,10 @@ tcValArg _ (EValArgQL { eaql_wanted = wanted |
|
607
|
644
|
|
|
608
|
645
|
|
|
609
|
646
|
--------------------
|
|
|
647
|
+whenQL :: QLFlag -> ZonkM () -> TcM ()
|
|
|
648
|
+whenQL DoQL thing_inside = liftZonkM thing_inside
|
|
|
649
|
+whenQL NoQL _ = return ()
|
|
|
650
|
+
|
|
610
|
651
|
wantQuickLook :: HsExpr GhcRn -> TcM QLFlag
|
|
611
|
652
|
wantQuickLook (HsVar _ (L _ (WithUserRdr _ f)))
|
|
612
|
653
|
| getUnique f `elem` quickLookKeys = return DoQL
|
| ... |
... |
@@ -839,11 +880,8 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args |
|
839
|
880
|
(Just $ HsExprTcThing tc_fun)
|
|
840
|
881
|
(n_val_args, fun_sigma) fun_ty
|
|
841
|
882
|
|
|
842
|
|
- ; let arg' = EValArg { ea_ctxt = ctxt
|
|
843
|
|
- , ea_arg = arg
|
|
844
|
|
- , ea_arg_ty = arg_ty }
|
|
845
|
|
- acc' = arg' : addArgWrap (mkWpCastN fun_co) acc
|
|
846
|
|
-
|
|
|
883
|
+ ; arg' <- quickLookArg do_ql ctxt arg arg_ty
|
|
|
884
|
+ ; let acc' = arg' : addArgWrap (mkWpCastN fun_co) acc
|
|
847
|
885
|
; go (pos+1) acc' res_ty rest_args }
|
|
848
|
886
|
|
|
849
|
887
|
new_arg_ty :: LHsExpr GhcRn -> Int -> TcM (Scaled TcType)
|
| ... |
... |
@@ -1841,21 +1879,28 @@ This turned out to be more subtle than I expected. Wrinkles: |
|
1841
|
1879
|
|
|
1842
|
1880
|
-}
|
|
1843
|
1881
|
|
|
1844
|
|
-quickLookArg :: HsExprArg 'TcpInst -> TcM (HsExprArg 'TcpInst)
|
|
|
1882
|
+quickLookArg :: QLFlag -> AppCtxt
|
|
|
1883
|
+ -> LHsExpr GhcRn -- ^ Argument
|
|
|
1884
|
+ -> Scaled TcSigmaTypeFRR -- ^ Type expected by the function
|
|
|
1885
|
+ -> TcM (HsExprArg 'TcpInst)
|
|
1845
|
1886
|
-- quickLookArg1 implements the "QL Argument" judgement in Fig 5 of the paper
|
|
1846
|
1887
|
-- See Note [Quick Look at value arguments]
|
|
1847
|
|
-quickLookArg e_arg@(EValArg { ea_ctxt = ctxt
|
|
1848
|
|
- , ea_arg = larg@(L _ arg)
|
|
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
|
|
|
1888
|
+quickLookArg NoQL ctxt larg orig_arg_ty
|
|
|
1889
|
+ = skipQuickLook ctxt larg orig_arg_ty
|
|
|
1890
|
+quickLookArg DoQL ctxt larg orig_arg_ty
|
|
|
1891
|
+ = do { is_rho <- tcIsDeepRho (scaledThing orig_arg_ty)
|
|
1853
|
1892
|
; traceTc "qla" (ppr orig_arg_ty $$ ppr is_rho)
|
|
1854
|
1893
|
; if not is_rho
|
|
1855
|
|
- then return e_arg
|
|
1856
|
|
- else
|
|
|
1894
|
+ then skipQuickLook ctxt larg orig_arg_ty
|
|
|
1895
|
+ else quickLookArg1 ctxt larg orig_arg_ty }
|
|
1857
|
1896
|
|
|
1858
|
|
- addArgCtxt ctxt larg $ -- Context needed for constraints
|
|
|
1897
|
+quickLookArg1 :: AppCtxt -> LHsExpr GhcRn
|
|
|
1898
|
+ -> Scaled TcRhoType -- Deeply skolemised
|
|
|
1899
|
+ -> TcM (HsExprArg 'TcpInst)
|
|
|
1900
|
+-- quickLookArg1 implements the "QL Argument" judgement in Fig 5 of the paper
|
|
|
1901
|
+quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho)
|
|
|
1902
|
+ -- NB: orig_arg_rho may not be zonked, but that's ok
|
|
|
1903
|
+ = addArgCtxt ctxt larg $ -- Context needed for constraints
|
|
1859
|
1904
|
-- generated by calls in arg
|
|
1860
|
1905
|
do { ((rn_fun, fun_ctxt), rn_args) <- splitHsApps arg
|
|
1861
|
1906
|
|
| ... |
... |
@@ -1873,7 +1918,7 @@ quickLookArg e_arg@(EValArg { ea_ctxt = ctxt |
|
1873
|
1918
|
, text "args:" <+> ppr rn_args ]
|
|
1874
|
1919
|
|
|
1875
|
1920
|
; case mb_fun_ty of {
|
|
1876
|
|
- Nothing -> return e_arg ; -- fun is too complicated
|
|
|
1921
|
+ Nothing -> skipQuickLook ctxt larg sc_arg_ty ; -- fun is too complicated
|
|
1877
|
1922
|
Just (tc_fun, fun_sigma) ->
|
|
1878
|
1923
|
|
|
1879
|
1924
|
-- step 2: use |-inst to instantiate the head applied to the arguments
|
| ... |
... |
@@ -1903,37 +1948,40 @@ quickLookArg e_arg@(EValArg { ea_ctxt = ctxt |
|
1903
|
1948
|
-- unzonked orig_arg_rho, so that we deliberately do not exploit
|
|
1904
|
1949
|
-- guardedness that emerges a result of QL on earlier args
|
|
1905
|
1950
|
-- In contrast, we must do the `anyFreeKappa` test /after/ tcInstFun; see (QLA3).
|
|
|
1951
|
+ ; arg_influences_enclosing_call
|
|
|
1952
|
+ <- if isGuardedTy orig_arg_rho
|
|
|
1953
|
+ then return True
|
|
|
1954
|
+ else not <$> anyFreeKappa app_res_rho -- (B)
|
|
|
1955
|
+ -- For (B) see Note [The fiv test in quickLookArg]
|
|
1906
|
1956
|
|
|
1907
|
|
- ; (arg_influences_call, inst_args_ql)
|
|
1908
|
|
- <- if isGuardedTy orig_arg_rho -- (A)
|
|
1909
|
|
- then do { qlUnify app_res_rho orig_arg_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)
|
|
1915
|
|
- ; if has_free_inst_vars
|
|
1916
|
|
- then return (False, inst_args_ql)
|
|
1917
|
|
- else do { qlUnify app_res_rho orig_arg_rho
|
|
1918
|
|
- ; return (True, inst_args_ql) } }
|
|
|
1957
|
+ -- Step 4: do quick-look unification if either (A) or (B) hold
|
|
|
1958
|
+ -- NB: orig_arg_rho may not be zonked, but that's ok
|
|
|
1959
|
+ ; when arg_influences_enclosing_call $
|
|
|
1960
|
+ quickLookResultType app_res_rho orig_arg_rho
|
|
1919
|
1961
|
|
|
1920
|
1962
|
; traceTc "quickLookArg done }" (ppr rn_fun)
|
|
1921
|
1963
|
|
|
1922
|
1964
|
; return (EValArgQL { eaql_ctxt = ctxt
|
|
1923
|
|
- , eaql_arg_ty = orig_arg_ty
|
|
|
1965
|
+ , eaql_arg_ty = sc_arg_ty
|
|
1924
|
1966
|
, eaql_larg = larg
|
|
1925
|
1967
|
, eaql_tc_fun = tc_head
|
|
1926
|
1968
|
, eaql_fun_ue = fun_ue
|
|
1927
|
|
- , eaql_args = inst_args_ql
|
|
|
1969
|
+ , eaql_args = inst_args
|
|
1928
|
1970
|
, eaql_wanted = wanted
|
|
1929
|
|
- , eaql_encl = arg_influences_call
|
|
1930
|
|
- , eaql_res_rho = app_res_rho }) }}}}
|
|
|
1971
|
+ , eaql_encl = arg_influences_enclosing_call
|
|
|
1972
|
+ , eaql_res_rho = app_res_rho }) }}}
|
|
1931
|
1973
|
|
|
1932
|
|
-quickLookArg other_arg = return other_arg
|
|
|
1974
|
+quickLookResultType :: TcRhoType -> TcRhoType -> TcM ()
|
|
|
1975
|
+-- See Note [QuickLook: arguments before result]
|
|
|
1976
|
+quickLookResultType app_rest_rho exp_res_rho
|
|
|
1977
|
+ = qlUnify app_rest_rho exp_res_rho
|
|
1933
|
1978
|
|
|
1934
|
|
-whenQL :: QLFlag -> ZonkM () -> TcM ()
|
|
1935
|
|
-whenQL DoQL thing_inside = liftZonkM thing_inside
|
|
1936
|
|
-whenQL NoQL _ = return ()
|
|
|
1979
|
+skipQuickLook :: AppCtxt -> LHsExpr GhcRn -> Scaled TcRhoType
|
|
|
1980
|
+ -> TcM (HsExprArg 'TcpInst)
|
|
|
1981
|
+skipQuickLook ctxt larg arg_ty
|
|
|
1982
|
+ = return (EValArg { ea_ctxt = ctxt
|
|
|
1983
|
+ , ea_arg = larg
|
|
|
1984
|
+ , ea_arg_ty = arg_ty })
|
|
1937
|
1985
|
|
|
1938
|
1986
|
tcIsDeepRho :: TcType -> TcM Bool
|
|
1939
|
1987
|
-- This top-level zonk step, which is the reason we need a local 'go' loop,
|
| ... |
... |
@@ -1961,15 +2009,6 @@ tcIsDeepRho ty |
|
1961
|
2009
|
| otherwise
|
|
1962
|
2010
|
= return True
|
|
1963
|
2011
|
|
|
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
|
2012
|
isGuardedTy :: TcType -> Bool
|
|
1974
|
2013
|
isGuardedTy ty
|
|
1975
|
2014
|
| Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
|