[Git][ghc/ghc][wip/T24676] More wibbles

Simon Peyton Jones (@simonpj) gitlab at gitlab.haskell.org
Tue May 28 22:44:37 UTC 2024



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


Commits:
af68929f by Simon Peyton Jones at 2024-05-28T23:43:50+01:00
More wibbles

- - - - -


4 changed files:

- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs


Changes:

=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -342,31 +342,43 @@ tcApp rn_expr exp_res_ty
 
        -- Instantiate
        ; do_ql <- wantQuickLook rn_fun
-       ; (inst_args, app_res_rho, res_wrap)
+       ; (inst_args, app_res_rho)
               <- setQLInstLevel do_ql $
-                 do { (inst_args, app_res_rho) <- tcInstFun do_ql True fun_ctxt tc_fun fun_sigma rn_args
-                    ; res_wrap <- unifyResTy rn_expr fun_ctxt tc_fun inst_args app_res_rho exp_res_ty
-                    ; return (inst_args, app_res_rho, res_wrap) }
+                 tcInstFun do_ql True fun_ctxt tc_fun fun_sigma rn_args
 
        -- Monomorphise any leftover instantiation variables
-       ; case do_ql of
-           DoQL -> monomorphiseQLInstVars inst_args app_res_rho
-           NoQL -> return ()
+       ; res_wrap <- case do_ql of
+           NoQL -> case exp_res_ty of
+                     Check res_ty ->
+                       unifyResTy rn_expr fun_ctxt tc_fun inst_args app_res_rho res_ty
+                     Infer inf_res ->
+                       do { co <- fillInferResult app_res_rho inf_res
+                          ; return (mkWpCastN co) }
+
+           DoQL -> case exp_res_ty of
+                     Check res_ty ->
+                       do { res_wrap <- unifyResTy rn_expr fun_ctxt tc_fun inst_args app_res_rho res_ty
+                          ; monomorphiseQLInstVars inst_args app_res_rho
+                          ; return res_wrap }
+                     Infer inf_res ->
+                       do { monomorphiseQLInstVars inst_args app_res_rho
+                          ; co <- fillInferResult app_res_rho inf_res
+                          ; return (mkWpCastN co) }
 
        -- Typecheck the arguments
-       ; tc_app <- finishApp do_ql fun_ctxt tc_fun inst_args app_res_rho
+       ; tc_app <- finishApp fun_ctxt tc_fun inst_args app_res_rho
        ; return (mkHsWrap res_wrap tc_app) }
 
 setQLInstLevel :: QLFlag -> TcM a -> TcM a
 setQLInstLevel DoQL thing_inside = setTcLevel QLInstVar thing_inside
 setQLInstLevel NoQL thing_inside = thing_inside
 
-finishApp :: QLFlag -> AppCtxt
+finishApp :: AppCtxt
           -> HsExpr GhcTc -> [HsExprArg 'TcpInst]
           -> TcRhoType
           -> TcM (HsExpr GhcTc)
 -- At this point there are no more instantiation variables
-finishApp do_ql fun_ctxt tc_fun inst_args app_res_rho
+finishApp fun_ctxt tc_fun inst_args app_res_rho
   = do { -- Typecheck the value arguments
        ; tc_args <- tcValArgs inst_args
 
@@ -381,7 +393,6 @@ finishApp do_ql fun_ctxt tc_fun inst_args app_res_rho
        ; whenDOptM Opt_D_dump_tc_trace $
          do { inst_args <- liftZonkM $ mapM zonkArg inst_args  -- Only when tracing
             ; traceTc "tcApp }" (vcat [ text "inst_args"    <+> brackets (pprWithCommas pprHsExprArgTc inst_args)
-                                      , text "do_ql:  "     <+> ppr do_ql
                                       , text "app_res_rho:" <+> ppr app_res_rho
                                       , text "tc_fun:"      <+> ppr tc_fun
                                       , text "tc_args:"     <+> ppr tc_args
@@ -392,31 +403,38 @@ finishApp do_ql fun_ctxt tc_fun inst_args app_res_rho
 
 unifyResTy :: HsExpr GhcRn -> AppCtxt -> HsExpr GhcTc
            -> [HsExprArg p]
-           -> TcType -> ExpRhoType
+           -> TcType -> TcRhoType
            -> TcM HsWrapper
-unifyResTy rn_expr fun_ctxt tc_fun inst_args app_res_rho exp_res_ty
+unifyResTy rn_expr fun_ctxt tc_fun inst_args app_res_rho res_ty
 -- Unify with expected type from the context
 -- See Note [Unify with expected type before typechecking arguments]
 --
 -- Match up app_res_rho: the result type of rn_expr
---     with exp_res_ty:  the expected result type
+--     with res_ty:  the expected result type
  = perhaps_add_res_ty_ctxt $
-   do { ds_flag <- getDeepSubsumptionFlag
+   do { traceTc "unifyResTy {" $
+          vcat [ text "tc_fun:" <+> ppr tc_fun
+               , text "app_res_rho:" <+> ppr app_res_rho
+               , text "res_ty:"  <+> ppr res_ty ]
+      ; ds_flag <- getDeepSubsumptionFlag
       ; case ds_flag of
           Shallow -> -- No deep subsumption
-             -- app_res_rho and exp_res_ty are both rho-types,
+             -- app_res_rho and res_ty are both rho-types,
              -- so with simple subsumption we can just unify them
              -- No need to zonk; the unifier does that
-             do { co <- unifyExpectedType rn_expr app_res_rho exp_res_ty
+             do { co <- unifyExprType rn_expr app_res_rho res_ty
+                ; traceTc "unifyResTy 1 }" (ppr co)
                 ; return (mkWpCastN co) }
 
           Deep ->   -- Deep subsumption
-             -- Even though both app_res_rho and exp_res_ty are rho-types,
+             -- Even though both app_res_rho and res_ty are rho-types,
              -- they may have nested polymorphism, so if deep subsumption
              -- is on we must call tcSubType.
              -- No need to zonk app_res_rho first; although QL may have instantiated some
              -- delta variables to polytypes, tcSubType can cope with that
-              tcSubTypeDS rn_expr app_res_rho exp_res_ty }
+              do { wrap <- tcSubTypeDS rn_expr app_res_rho res_ty
+                 ; traceTc "unifyResTy 2 }" (ppr wrap)
+                 ; return wrap } }
   where
     -- perhaps_add_res_ty_ctxt: Inside an expansion, the addFunResCtxt stuff is
     -- more confusing than helpful because the function at the head isn't in
@@ -426,7 +444,7 @@ unifyResTy rn_expr fun_ctxt tc_fun inst_args app_res_rho exp_res_ty
       | insideExpansion fun_ctxt
       = addHeadCtxt fun_ctxt thing_inside
       | otherwise
-      = addFunResCtxt tc_fun inst_args app_res_rho exp_res_ty $
+      = addFunResCtxt tc_fun inst_args app_res_rho (mkCheckExpType res_ty) $
         thing_inside
 
 
@@ -506,7 +524,7 @@ tcValArg (EValArgQL { eaql_status  = ql_status
     tcScalingUsage mult  $
     case ql_status of
       QLUnified res_wrap
-        -> do { tc_app <- finishApp DoQL ctxt tc_fun inst_args res_rho
+        -> do { tc_app <- finishApp ctxt tc_fun inst_args res_rho
               ; return (EValArg { ea_ctxt   = ctxt
                                 , ea_arg    = L arg_loc (mkHsWrap res_wrap tc_app)
                                 , ea_arg_ty = noExtField }) }
@@ -525,9 +543,9 @@ tcValArg (EValArgQL { eaql_status  = ql_status
               ; (wrap, arg')
                    <- tcSkolemise ds_flag GenSigCtxt arg_ty $ \ arg_rho ->
                       do { emitConstraints wc
-                         ; res_wrap <- unifyResTy rn_expr ctxt tc_fun inst_args res_rho (mkCheckExpType arg_rho)
+                         ; res_wrap <- unifyResTy rn_expr ctxt tc_fun inst_args res_rho arg_rho
                          ; monomorphiseQLInstVars inst_args res_rho
-                         ; tc_app <- finishApp DoQL ctxt tc_fun inst_args res_rho
+                         ; tc_app <- finishApp ctxt tc_fun inst_args res_rho
                          ; return (mkHsWrap res_wrap tc_app) }
 
               ; traceTc "tcEValArgQL }" $
@@ -1743,8 +1761,7 @@ quickLookArg1 ctxt larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_rho)
               -- No skolemisation of orig_arg_ty needed here:
               --   tcIsDeepRho checked that there are no foralls to skolemise
               do { emitConstraints wanted
-                 ; res_wrap <- unifyResTy arg fun_ctxt tc_fun inst_args app_res_rho
-                                          (mkCheckExpType orig_arg_rho)
+                 ; res_wrap <- unifyResTy arg fun_ctxt tc_fun inst_args app_res_rho orig_arg_rho
                  ; traceTc "quickLookArg unify" (ppr rn_fun)
                  ; return (mk_ql_arg (QLUnified res_wrap)) }
 


=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -1821,6 +1821,9 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
               , text "lhs:" <+> ppr lhs
               , text "rhs:" <+> ppr rhs ]
 
+         -- Assertion: no QL instantiation tyvars
+--       ; massertPpr (not (ql_inst_tv lhs)) (ppr lhs)
+
          -- Assertion: (TyEq:K) is already satisfied
        ; massert (canEqLHSKind lhs `eqType` typeKind rhs)
 
@@ -1832,6 +1835,9 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
        ; canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs }
 
   where
+    ql_inst_tv (TyVarLHS tv) = isQLInstTyVar tv
+    ql_inst_tv (TyFamLHS {}) = False
+
     -- This is about (TyEq:N): check that we don't have a saturated application
     -- of a newtype TyCon at the top level of the RHS, if the constructor
     -- of the newtype is in scope.


=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -55,7 +55,8 @@ module GHC.Tc.Utils.TcType (
   isConcreteTyVarTy, isConcreteTyVarTy_maybe, isConcreteInfo,
   ConcreteTyVars, noConcreteTyVars,
   isAmbiguousTyVar, isCycleBreakerTyVar, metaTyVarRef, metaTyVarInfo,
-  isFlexi, isIndirect, isRuntimeUnkSkol, isQLInstTyVar,
+  isFlexi, isIndirect, isRuntimeUnkSkol,
+  isQLInstTyVar, isRuntimeUnkTyVar,
   metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe,
   isTouchableMetaTyVar, isPromotableMetaTyVar,
   findDupTyVarTvs, mkTyVarNamePairs,
@@ -1201,6 +1202,12 @@ isQLInstTyVar tv
       MetaTv { mtv_tclvl = QLInstVar } -> True
       _                                -> False
 
+isRuntimeUnkTyVar :: TcTyVar -> Bool
+isRuntimeUnkTyVar tv
+  = case tcTyVarDetails tv of
+      MetaTv { mtv_info = RuntimeUnkTv } -> True
+      _                                  -> False
+
 isCycleBreakerTyVar tv
   | isTyVar tv -- See Note [Coercion variables in free variable lists]
   , MetaTv { mtv_info = CycleBreakerTv } <- tcTyVarDetails tv


=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -24,7 +24,7 @@ module GHC.Tc.Utils.Unify (
 
   -- Various unifications
   unifyType, unifyKind, unifyInvisibleType, unifyExpectedType,
-  unifyTypeAndEmit, promoteTcType,
+  unifyExprType, unifyTypeAndEmit, promoteTcType,
   swapOverTyVars, touchabilityAndShapeTest,
   UnifyEnv(..), updUEnvLoc, setUEnvRole,
   uType,
@@ -1326,22 +1326,16 @@ tcSubType orig ctxt ty_actual ty_expected
 ---------------
 tcSubTypeDS :: HsExpr GhcRn
             -> TcRhoType   -- Actual type -- a rho-type not a sigma-type
-            -> ExpRhoType  -- Expected type
+            -> TcRhoType   -- Expected type
                            -- DeepSubsumption <=> when checking, this type
                            --                     is deeply skolemised
             -> TcM HsWrapper
 -- Similar signature to unifyExpectedType; does deep subsumption
 -- Only one call site, in GHC.Tc.Gen.App.tcApp
-tcSubTypeDS rn_expr act_rho res_ty
-  = case res_ty of
-      Check exp_rho -> tc_sub_type_deep (unifyType m_thing) orig
-                                        GenSigCtxt act_rho exp_rho
-
-      Infer inf_res -> do { co <- fillInferResult act_rho inf_res
-                          ; return (mkWpCastN co) }
+tcSubTypeDS rn_expr act_rho exp_rho
+  = tc_sub_type_deep (unifyExprType rn_expr) orig GenSigCtxt act_rho exp_rho
   where
-    orig    = exprCtOrigin rn_expr
-    m_thing = Just (HsExprRnThing rn_expr)
+    orig = exprCtOrigin rn_expr
 
 ---------------
 tcSubTypeNC :: CtOrigin          -- ^ Used when instantiating
@@ -1972,6 +1966,10 @@ The exported functions are all defined as versions of some
 non-exported generic functions.
 -}
 
+unifyExprType :: HsExpr GhcRn -> TcType -> TcType -> TcM TcCoercionN
+unifyExprType rn_expr ty1 ty2
+  = unifyType (Just (HsExprRnThing rn_expr)) ty1 ty2
+
 unifyType :: Maybe TypedThing  -- ^ If present, the thing that has type ty1
           -> TcTauType -> TcTauType    -- ty1 (actual), ty2 (expected)
           -> TcM TcCoercionN           -- :: ty1 ~# ty2
@@ -2448,7 +2446,7 @@ uUnfilledVar2 env@(UE { u_defer = def_eq_ref }) swapped tv1 ty2
            -- /any/ level outside this one as untouchable.  Hence cur_lvl.
        ; if not (touchabilityAndShapeTest cur_lvl tv1 ty2
                  && simpleUnifyCheck False tv1 ty2)
-         then not_ok_so_defer
+         then not_ok_so_defer cur_lvl
          else
     do { def_eqs <- readTcRef def_eq_ref  -- Capture current state of def_eqs
 
@@ -2481,8 +2479,12 @@ uUnfilledVar2 env@(UE { u_defer = def_eq_ref }) swapped tv1 ty2
     ty1 = mkTyVarTy tv1
     defer = unSwap swapped (uType_defer env) ty1 ty2
 
-    not_ok_so_defer =
-      do { traceTc "uUnfilledVar2 not ok" (ppr tv1 $$ ppr ty2)
+    not_ok_so_defer cur_lvl =
+      do { traceTc "uUnfilledVar2 not ok" $
+             vcat [ text "tv1:" <+> ppr tv1
+                  , text "ty2:" <+> ppr ty2
+                  , text "simple-unify-chk:" <+> ppr (simpleUnifyCheck False tv1 ty2)
+                  , text "touchability:" <+> ppr (touchabilityAndShapeTest cur_lvl tv1 ty2)]
                -- Occurs check or an untouchable: just defer
                -- NB: occurs check isn't necessarily fatal:
                --     eg tv1 occurred in type family parameter
@@ -2870,45 +2872,48 @@ matchExpectedFunKind hs_ty n k = go n k
 *                                                                      *
 ********************************************************************* -}
 
-simpleUnifyCheck :: Bool -> TcTyVar -> TcType -> Bool
+simpleUnifyCheck :: Bool   -- True  <=> called from constraint solver
+                           -- False <=> called from on-the-fly unifier
+                 -> TcTyVar -> TcType -> Bool
 -- A fast check: True <=> unification is OK
 -- If it says 'False' then unification might still be OK, but
 -- it'll take more work to do -- use the full checkTypeEq
 --
--- * Always rejects foralls unless lhs_tv is RuntimeUnk
---   (used by GHCi debugger)
+-- * Rejects foralls unless
+--      lhs_tv is RuntimeUnk (used by GHCi debugger)
+--          or is a QL instantiation variable
 -- * Rejects a non-concrete type if lhs_tv is concrete
 -- * Rejects type families unless fam_ok=True
 -- * Does a level-check for type variables
 --
 -- This function is pretty heavily used, so it's optimised not to allocate
-simpleUnifyCheck fam_ok lhs_tv rhs
+simpleUnifyCheck called_from_solver lhs_tv rhs
   = go rhs
   where
+    fam_ok = called_from_solver || is_ql_inst_tv
+
     !(occ_in_ty, occ_in_co) = mkOccFolders lhs_tv
 
     lhs_tv_lvl         = tcTyVarLevel lhs_tv
     lhs_tv_is_concrete = isConcreteTyVar lhs_tv
-    forall_ok          = case tcTyVarDetails lhs_tv of
-                            MetaTv { mtv_info = RuntimeUnkTv } -> True
-                            MetaTv { mtv_tclvl = QLInstVar }   -> True
-                            _                                  -> False
+    is_ql_inst_tv      = isQLInstTyVar lhs_tv
+    forall_ok          = is_ql_inst_tv || isRuntimeUnkTyVar lhs_tv
 
     go (TyVarTy tv)
-      | lhs_tv == tv                                 = False
-      | tcTyVarLevel tv > lhs_tv_lvl                 = False
-      | lhs_tv_is_concrete, not (isConcreteTyVar tv) = False
-      | occ_in_ty $! (tyVarKind tv)                  = False
-      | otherwise                                    = True
+      | lhs_tv == tv                                    = False
+      | tcTyVarLevel tv `strictlyDeeperThan` lhs_tv_lvl = False
+      | lhs_tv_is_concrete, not (isConcreteTyVar tv)    = False
+      | occ_in_ty $! (tyVarKind tv)                     = False
+      | otherwise                                       = True
 
     go (FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r})
-      | isInvisibleFunArg af, not forall_ok = False
+      | not forall_ok, isInvisibleFunArg af = False
       | otherwise                           = go w && go a && go r
 
     go (TyConApp tc tys)
       | lhs_tv_is_concrete, not (isConcreteTyCon tc) = False
-      | not (isTauTyCon tc)                          = False
-      | not fam_ok, not (isFamFreeTyCon tc)          = False
+      | not forall_ok, not (isTauTyCon tc)           = False
+      | not fam_ok,    not (isFamFreeTyCon tc)       = False
       | otherwise                                    = all go tys
 
     go (ForAllTy (Bndr tv _) ty)



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/af68929f22b6fd62c06e2fd4cc1d979f5d9ba9ea

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/af68929f22b6fd62c06e2fd4cc1d979f5d9ba9ea
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20240528/6e8232ce/attachment-0001.html>


More information about the ghc-commits mailing list