[Git][ghc/ghc][wip/T24810] Cast visibilities correctly

[Simon Peyton Jones (@simonpj)]

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


Commits:
f5627b7c by Simon Peyton Jones at 2024-05-17T17:32:29+01:00
Cast visibilities correctly

- - - - -


5 changed files:

- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/Utils.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Utils/Instantiate.hs
- compiler/GHC/Types/Var.hs


Changes:

=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -1195,6 +1195,21 @@ among branches, but that doesn't quite concern us here.)
 The Int in the AxiomInstCo constructor is the 0-indexed number
 of the chosen branch.
 
+Note [Required foralls in Core]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the CoreExpr (Lam a e) where `a` is a TyVar, and (e::e_ty).
+It has type
+   forall a{Specified}. e_ty
+Note the Specified visibility;
+the Core type just isn't able to express more than one visiblity, and we pick `Specified`.
+See `exprType` and `mkLamType` in GHC.Core.Utils, and `GHC.Type.Var.coreLamForAllTyFlag`.
+
+So how can we ever get a term of type (forall a -> e_ty)?  Answer: /only/ via a
+cast built with ForAllCo.  See `GHC.Tc.Types.Evidence.mkWpForAllCast`.  This does
+not seem very satisfying, but it does the job.
+
+See also Note [ForAllTy and type equality] in GHC.Core.TyCo.Compare.
+
 Note [ForAllCo]
 ~~~~~~~~~~~~~~~
 See also Note [ForAllTy and type equality] in GHC.Core.TyCo.Compare.
@@ -1255,6 +1270,7 @@ Several things to note here
   flag `GHC.Type.Var.coreTyLamForAllTyFlag`, not (forall a -> ty).
   See `GHC.Type.Var.coreTyLamForAllTyFlag` and `GHC.Core.Utils.mkLamType`.
   The only way to get a term of type (forall a -> ty) is to cast a lambda.
+  See Note [Required foralls in Core].
 
 (FC5) In a /type/, in (ForAllTy cv ty) where cv is a CoVar, we insist that
   `cv` must appear free in `ty`; see Note [Unused coercion variable in ForAllTy]


=====================================
compiler/GHC/Core/Utils.hs
=====================================
@@ -170,7 +170,7 @@ mkLamTypes :: [Var] -> Type -> Type
 mkLamType v body_ty
    | isTyVar v
    = mkForAllTy (Bndr v coreTyLamForAllTyFlag) body_ty
-     -- coreTyLamForAllTyFlag: see (FC4) in Note [ForAllCo]
+     -- coreTyLamForAllTyFlag: see Note [Required foralls in Core]
      --                        in GHC.Core.TyCo.Rep
 
    | isCoVar v


=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -7,7 +7,7 @@ module GHC.Tc.Types.Evidence (
 
   -- * HsWrapper
   HsWrapper(..),
-  (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpVisTyLam,
+  (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpForAllCast,
   mkWpEvLams, mkWpLet, mkWpFun, mkWpCastN, mkWpCastR, mkWpEta,
   collectHsWrapBinders,
   idHsWrapper, isIdHsWrapper,
@@ -258,20 +258,20 @@ mkWpEvVarApps vs = mk_co_app_fn WpEvApp (map (EvExpr . evId) vs)
 mkWpTyLams :: [TyVar] -> HsWrapper
 mkWpTyLams ids = mk_co_lam_fn WpTyLam ids
 
--- Construct a type lambda and cast its type
--- from `forall tv. res` to `forall tv -> res`.
+-- mkWpForAllCast [tv{vis}] constructs a cast
+--   forall tv. res  ~R#   forall tv{vis} res`.
+-- See Note [Required foralls in Core]
 --
--- (\ @tv -> e )
---    `cast` (forall (tv[spec]~[req] :: <*>_N). <res>_R       -- ForAllCo is the evidence that...
---              :: (forall tv. res) ~R# (forall tv -> res))   -- invisible and visible foralls are representationally equal
---
-mkWpVisTyLam :: TyVar -> Type -> HsWrapper
-mkWpVisTyLam tv res =
-  WpCast (mkForAllCo tv coreTyLamForAllTyFlag Required kind_co body_co)
-  <.> WpTyLam tv
+-- It's a no-op if all binders are invisible;
+-- but in that case we refrain from calling it.
+mkWpForAllCast :: [ForAllTyBinder] -> Type -> HsWrapper
+mkWpForAllCast bndrs res_ty
+  = mkWpCastR (go bndrs)
   where
-    kind_co = mkNomReflCo (varType tv)
-    body_co = mkRepReflCo res
+    go []                 = mkRepReflCo res_ty
+    go (Bndr tv vis : bs) = mkForAllCo tv coreTyLamForAllTyFlag vis kind_co (go bs)
+      where
+        kind_co = mkNomReflCo (varType tv)
 
 mkWpEvLams :: [Var] -> HsWrapper
 mkWpEvLams ids = mk_co_lam_fn WpEvLam ids


=====================================
compiler/GHC/Tc/Utils/Instantiate.hs
=====================================
@@ -247,8 +247,13 @@ skolemiseRequired skolem_info n_req sigma
       , not (null bndrs)
       = do { (subst', bndrs1) <- tcInstSkolTyVarBndrsX skolem_info subst bndrs
            ; let tvs1 = binderVars bndrs1
+                 -- fix_up_vis: see Note [Required foralls in Core]
+                 fix_up_vis | n_req == n_req'
+                            = idHsWrapper
+                            | otherwise
+                            = mkWpForAllCast bndrs1 (substTy subst' inner_ty)
            ; go n_req' subst'
-                (wrap <.> mkWpTyLams tvs1)
+                (wrap <.> fix_up_vis <.> mkWpTyLams tvs1)
                 (acc_nms   ++ map (tyVarName . binderVar) bndrs)
                 (acc_bndrs ++ bndrs1)
                 ev_vars


=====================================
compiler/GHC/Types/Var.hs
=====================================
@@ -503,7 +503,7 @@ isSpecifiedForAllTyFlag _                         = False
 coreTyLamForAllTyFlag :: ForAllTyFlag
 -- ^ The ForAllTyFlag on a (Lam a e) term, where `a` is a type variable.
 -- If you want other ForAllTyFlag, use a cast.
--- See Note [ForAllCo] in GHC.Core.TyCo.Rep
+-- See Note [Required foralls in Core] in GHC.Core.TyCo.Rep
 coreTyLamForAllTyFlag = Specified
 
 instance Outputable ForAllTyFlag where



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f5627b7c846aa6a8776323e3cbc3a8e59b650741
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/20240517/f36545af/attachment-0001.html>