Simon Peyton Jones pushed to branch wip/26543 at Glasgow Haskell Compiler / GHC

Commits:

2 changed files:

Changes:

  • compiler/GHC/Tc/Gen/App.hs
    ... ... @@ -385,8 +385,7 @@ tcApp rn_expr exp_res_ty
    385 385
    386 386 
            -- Step 3: Instantiate the function type (taking a quick look at args)
    387 387 
            ; do_ql <- wantQuickLook rn_fun
    388 
    -       ; (inst_args, app_res_rho)
    389 
    -              <- tcInstFun do_ql inst_final tc_head fun_sigma rn_args
    388 
    +       ; (inst_args, app_res_rho) <- tcInstFun do_ql inst_final tc_head fun_sigma rn_args
    390 389
    391 390 
            ; case do_ql of
    392 391 
                 NoQL -> do { traceTc "tcApp:NoQL" (ppr rn_fun $$ ppr app_res_rho)
    ... ... @@ -406,10 +405,11 @@ tcApp rn_expr exp_res_ty
    406 405
    407 406 
                              -- Step 5.1: Take a quick look at the result type
    408 407 
                            ; quickLookResultType app_res_rho exp_res_ty
    408 
    +                       ; inst_args' <- mapM quickLookArg inst_args
    409 409
    410 410 
                              -- Step 5.2: typecheck the arguments, and monomorphise
    411 411 
                              --           any un-unified instantiation variables
    412 
    -                       ; tc_args <- tcValArgs DoQL inst_args
    412 
    +                       ; tc_args <- tcValArgs DoQL inst_args'
    413 413
    414 414 
                              -- Step 5.3: zonk to expose the polymorphism hidden under
    415 415 
                              --           QuickLook instantiation variables in `app_res_rho`
    ... ... @@ -841,9 +841,11 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
    841 841 
                       (Just $ HsExprTcThing tc_fun)
    842 842 
                       (n_val_args, fun_sigma) fun_ty
    843 843
    844 
    -           ; ds_flag <- getDeepSubsumptionFlag_DataConHead tc_fun
    845 
    -           ; arg' <- quickLookArg ds_flag do_ql ctxt arg arg_ty
    846 
    -           ; let acc' = arg' : addArgWrap (mkWpCastN fun_co) acc
    844 
    +           ; let arg' = EValArg { ea_ctxt   = ctxt
    845 
    +                                , ea_arg    = arg
    846 
    +                                , ea_arg_ty = arg_ty }
    847 
    +                 acc' = arg' : addArgWrap (mkWpCastN fun_co) acc
    848 
    +
    847 849 
                ; go (pos+1) acc' res_ty rest_args }
    848 850
    849 851 
         new_arg_ty :: LHsExpr GhcRn -> Int -> TcM (Scaled TcType)
    ... ... @@ -1841,68 +1843,20 @@ This turned out to be more subtle than I expected. Wrinkles:
    1841 1843
    1842 1844 
     -}
    1843 1845
    1844 
    -quickLookArg :: DeepSubsumptionFlag
    1845 
    -             -> QLFlag -> AppCtxt
    1846 
    -             -> LHsExpr GhcRn          -- ^ Argument
    1847 
    -             -> Scaled TcSigmaTypeFRR  -- ^ Type expected by the function
    1846 
    +quickLookArg :: HsExprArg 'TcpInst
    1848 1847 
                  -> TcM (HsExprArg 'TcpInst)
    1848 
    +-- quickLookArg1 implements the "QL Argument" judgement in Fig 5 of the paper
    1849 1849 
     -- See Note [Quick Look at value arguments]
    1850 
    -quickLookArg _ NoQL ctxt larg orig_arg_ty
    1851 
    -  = skipQuickLook ctxt larg orig_arg_ty
    1852 
    -quickLookArg ds_flag DoQL ctxt larg orig_arg_ty
    1853 
    -  = do { is_rho <- tcIsDeepRho ds_flag (scaledThing orig_arg_ty)
    1850 
    +quickLookArg e_arg@(EValArg { ea_ctxt   = ctxt
    1851 
    +                            , ea_arg    = larg@(L _ arg)
    1852 
    +                            , ea_arg_ty = orig_arg_ty@(Scaled _ orig_arg_rho) })
    1853 
    +  = do { is_rho <- tcIsDeepRho orig_arg_rho
    1854 1854 
            ; traceTc "qla" (ppr orig_arg_ty $$ ppr is_rho)
    1855 1855 
            ; if not is_rho
    1856 
    -         then skipQuickLook ctxt larg orig_arg_ty
    1857 
    -         else quickLookArg1 ctxt larg orig_arg_ty }
    1858 
    -
    1859 
    -skipQuickLook :: AppCtxt -> LHsExpr GhcRn -> Scaled TcRhoType
    1860 
    -              -> TcM (HsExprArg 'TcpInst)
    1861 
    -skipQuickLook ctxt larg arg_ty
    1862 
    -  = return (EValArg { ea_ctxt   = ctxt
    1863 
    -                    , ea_arg    = larg
    1864 
    -                    , ea_arg_ty = arg_ty })
    1865 
    -
    1866 
    -whenQL :: QLFlag -> ZonkM () -> TcM ()
    1867 
    -whenQL DoQL thing_inside = liftZonkM thing_inside
    1868 
    -whenQL NoQL _            = return ()
    1869 
    -
    1870 
    -tcIsDeepRho :: DeepSubsumptionFlag -> TcType -> TcM Bool
    1871 
    --- This top-level zonk step, which is the reason we need a local 'go' loop,
    1872 
    --- is subtle. See Section 9 of the QL paper
    1873 
    -
    1874 
    -tcIsDeepRho ds_flag = go
    1875 
    -  where
    1876 
    -    go ty
    1877 
    -      | isSigmaTy ty
    1878 
    -      = return False
    1879 
    -
    1880 
    -      | Just kappa <- getTyVar_maybe ty
    1881 
    -      , isQLInstTyVar kappa
    1882 
    -      = do { info <- readMetaTyVar kappa
    1883 
    -           ; case info of
    1884 
    -               Indirect arg_ty' -> go arg_ty'
    1885 
    -               Flexi            -> return True }
    1886 
    -
    1887 
    -      | Deep {} <- ds_flag
    1888 
    -      , Just (_, res_ty) <- tcSplitFunTy_maybe ty
    1889 
    -      = go res_ty
    1890 
    -
    1891 
    -      | otherwise
    1892 
    -      = return True
    1856 
    +         then return e_arg
    1857 
    +         else
    1893 1858
    1894 
    -isGuardedTy :: TcType -> Bool
    1895 
    -isGuardedTy ty
    1896 
    -  | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
    1897 
    -  | Just {} <- tcSplitAppTy_maybe ty        = True
    1898 
    -  | otherwise                               = False
    1899 
    -
    1900 
    -quickLookArg1 :: AppCtxt -> LHsExpr GhcRn
    1901 
    -              -> Scaled TcRhoType  -- Deeply skolemised
    1902 
    -              -> TcM (HsExprArg 'TcpInst)
    1903 
    --- quickLookArg1 implements the "QL Argument" judgement in Fig 5 of the paper
    1904 
    -quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho)
    1905 
    -  = addArgCtxt ctxt larg $ -- Context needed for constraints
    1859 
    +    addArgCtxt ctxt larg $ -- Context needed for constraints
    1906 1860 
                                -- generated by calls in arg
    1907 1861 
         do { ((rn_fun, fun_ctxt), rn_args) <- splitHsApps arg
    1908 1862
    ... ... @@ -1920,7 +1874,7 @@ quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho)
    1920 1874 
                   , text "args:" <+> ppr rn_args ]
    1921 1875
    1922 1876 
            ; case mb_fun_ty of {
    1923 
    -           Nothing -> skipQuickLook ctxt larg sc_arg_ty ;    -- fun is too complicated
    1877 
    +           Nothing -> return e_arg ;  -- fun is too complicated
    1924 1878 
                Just (tc_fun, fun_sigma) ->
    1925 1879
    1926 1880 
            -- step 2: use |-inst to instantiate the head applied to the arguments
    ... ... @@ -1930,9 +1884,10 @@ quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho)
    1930 1884 
                  <- captureConstraints $
    1931 1885 
                     tcInstFun do_ql True tc_head fun_sigma rn_args
    1932 1886 
                     -- We must capture type-class and equality constraints here, but
    1933 
    -                -- not equality constraints.  See (QLA6) in Note [Quick Look at
    1887 
    +                -- not usage constraints.  See (QLA6) in Note [Quick Look at
    1934 1888 
                     -- value arguments]
    1935 1889
    1890 
    +{-
    1936 1891 
            ; traceTc "quickLookArg 2" $
    1937 1892 
              vcat [ text "arg:" <+> ppr arg
    1938 1893 
                   , text "orig_arg_rho:" <+> ppr orig_arg_rho
    ... ... @@ -1943,10 +1898,10 @@ quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho)
    1943 1898 
              --           or: (B) fiv(app_res_rho) = emptyset
    1944 1899 
            -- This tells us if the quick look at the argument yields information that
    1945 1900 
            -- influences the enclosing function call
    1946 
    -       -- NB: guardedness is computed based on the original,
    1947 
    -       -- unzonked orig_arg_rho, so that we deliberately do
    1948 
    -       -- not exploit guardedness that emerges a result of QL on earlier args
    1949 
    -       -- We must do the anyFreeKappa test /after/ tcInstFun; see (QLA3).
    1901 
    +       -- NB: `isGuardedTy` is computed based on the original,
    1902 
    +       --         unzonked orig_arg_rho, so that we deliberately do not exploit
    1903 
    +       --         guardedness that emerges a result of QL on earlier args
    1904 
    +       --     In contrast, we must do the `anyFreeKappa` test /after/ tcInstFun; see (QLA3).
    1950 1905 
            ; arg_influences_enclosing_call
    1951 1906 
                 <- if isGuardedTy orig_arg_rho
    1952 1907 
                    then return True
    ... ... @@ -1957,18 +1912,69 @@ quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho)
    1957 1912 
            -- NB: orig_arg_rho may not be zonked, but that's ok
    1958 1913 
            ; when arg_influences_enclosing_call $
    1959 1914 
              qlUnify app_res_rho orig_arg_rho
    1915 
    +-}
    1916 
    +
    1917 
    +       ; (arg_influences_call, inst_args')
    1918 
    +            <- if isGuardedTy orig_arg_rho
    1919 
    +               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
    1924 
    +                       ; if has_free_inst_vars
    1925 
    +                         then return (False, inst_args')
    1926 
    +                         else do { qlUnify app_res_rho orig_arg_rho
    1927 
    +                                 ; return (True, inst_args') } }
    1960 1928
    1961 1929 
            ; traceTc "quickLookArg done }" (ppr rn_fun)
    1962 1930
    1963 1931 
            ; return (EValArgQL { eaql_ctxt    = ctxt
    1964 
    -                           , eaql_arg_ty  = sc_arg_ty
    1932 
    +                           , eaql_arg_ty  = orig_arg_ty
    1965 1933 
                                , eaql_larg    = larg
    1966 1934 
                                , eaql_tc_fun  = tc_head
    1967 1935 
                                , eaql_fun_ue  = fun_ue
    1968 
    -                           , eaql_args    = inst_args
    1936 
    +                           , eaql_args    = inst_args'
    1969 1937 
                                , eaql_wanted  = wanted
    1970 
    -                           , eaql_encl    = arg_influences_enclosing_call
    1971 
    -                           , eaql_res_rho = app_res_rho }) }}}
    1938 
    +                           , eaql_encl    = arg_influences_call
    1939 
    +                           , eaql_res_rho = app_res_rho }) }}}}
    1940 
    +
    1941 
    +quickLookArg other_arg = return other_arg
    1942 
    +
    1943 
    +whenQL :: QLFlag -> ZonkM () -> TcM ()
    1944 
    +whenQL DoQL thing_inside = liftZonkM thing_inside
    1945 
    +whenQL NoQL _            = return ()
    1946 
    +
    1947 
    +tcIsDeepRho :: TcType -> TcM Bool
    1948 
    +-- This top-level zonk step, which is the reason we need a local 'go' loop,
    1949 
    +-- is subtle. See Section 9 of the QL paper
    1950 
    +
    1951 
    +tcIsDeepRho ty
    1952 
    +  = do { ds_flag <- getDeepSubsumptionFlag
    1953 
    +       ; go ds_flag ty }
    1954 
    +  where
    1955 
    +    go ds_flag ty
    1956 
    +      | isSigmaTy ty
    1957 
    +      = return False
    1958 
    +
    1959 
    +      | Just kappa <- getTyVar_maybe ty
    1960 
    +      , isQLInstTyVar kappa
    1961 
    +      = do { info <- readMetaTyVar kappa
    1962 
    +           ; case info of
    1963 
    +               Indirect arg_ty' -> go ds_flag arg_ty'
    1964 
    +               Flexi            -> return True }
    1965 
    +
    1966 
    +      | Deep {} <- ds_flag
    1967 
    +      , Just (_, res_ty) <- tcSplitFunTy_maybe ty
    1968 
    +      = go ds_flag res_ty
    1969 
    +
    1970 
    +      | otherwise
    1971 
    +      = return True
    1972 
    +
    1973 
    +isGuardedTy :: TcType -> Bool
    1974 
    +isGuardedTy ty
    1975 
    +  | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
    1976 
    +  | Just {} <- tcSplitAppTy_maybe ty        = True
    1977 
    +  | otherwise                               = False
    1972 1978
    1973 1979 
     {- *********************************************************************
    1974 1980 
     *                                                                      *
    ... ... @@ -2075,13 +2081,14 @@ We will instantiate Just with kappa, say, and then call
    2075 2081 
         quickLookArg1 False {kappa} (ids ++ ids) kappa
    2076 2082 
     The call to tcInstFun will return with app_res_rho = [forall a. a->a]
    2077 2083 
     which has no free instantiation variables, so we can QL-unify
    2078 
    -  kappa ~ [Forall a. a->a]
    2084 
    +  kappa ~ [forall a. a->a]
    2079 2085 
     -}
    2080 2086
    2081 2087 
     anyFreeKappa :: TcType -> TcM Bool
    2082 2088 
     -- True if there is a free instantiation variable
    2083 2089 
     -- in the argument type, after zonking
    2084 2090 
     -- See Note [The fiv test in quickLookArg]
    2091 
    +-- The function is monadic; it does not require a zonked type as input
    2085 2092 
     anyFreeKappa ty = unTcMBool (foldQLInstVars go_tv ty)
    2086 2093 
       where
    2087 2094 
         go_tv tv = TCMB $ do { info <- readMetaTyVar tv

  • compiler/GHC/Tc/Utils/Unify.hs
    ... ... @@ -3076,15 +3076,16 @@ lhsPriority tv
    3076 3076 
           RuntimeUnk  -> 0
    3077 3077 
           SkolemTv {} -> 0
    3078 3078 
           MetaTv { mtv_info = info, mtv_tclvl = lvl }
    3079 
    -        | QLInstVar <- lvl
    3080 
    -        -> 5  -- Eliminate instantiation variables first
    3081 
    -        | otherwise
    3082 3079 
             -> case info of
    3083 3080 
                  CycleBreakerTv -> 0
    3084 3081 
                  TyVarTv        -> 1
    3085 
    -             ConcreteTv {}  -> 2
    3086 
    -             TauTv          -> 3
    3087 
    -             RuntimeUnkTv   -> 4
    3082 
    +             ConcreteTv {}  -> qli 2  -- 2,3
    3083 
    +             TauTv          -> qli 4  -- 4,5
    3084 
    +             RuntimeUnkTv   -> 6
    3085 
    +        where
    3086 
    +          qli n = case lvl of
    3087 
    +                    QLInstVar -> n+1  -- Eliminate instantiation variables first
    3088 
    +                    _         -> n
    3088 3089
    3089 3090 
     {- Note [Unification preconditions]
    3090 3091 
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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