[Git][ghc/ghc][wip/T16762] Fixes from Simon

Simon Peyton Jones gitlab at gitlab.haskell.org
Mon Sep 21 14:37:00 UTC 2020



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


Commits:
60dd0659 by Simon Peyton Jones at 2020-09-21T15:35:30+01:00
Fixes from Simon

1. Comments in Hs.Type
2. Fix latent bug in emitFlatConstraints
3. Adopt Ryan's solution in tc_hs_sig_type, but with comments

- - - - -


3 changed files:

- compiler/GHC/Hs/Type.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Solver.hs


Changes:

=====================================
compiler/GHC/Hs/Type.hs
=====================================
@@ -357,7 +357,7 @@ data HsForAllTelescope pass
     { hsf_xvis      :: XHsForAllVis pass
     , hsf_vis_bndrs :: [LHsTyVarBndr () pass]
     }
-  | HsForAllInvis -- ^ An invisible @forall@ (e.g., @forall a {b} c -> {...}@),
+  | HsForAllInvis -- ^ An invisible @forall@ (e.g., @forall a {b} c. {...}@),
                   --   where each binder has a 'Specificity'.
     { hsf_xinvis       :: XHsForAllInvis pass
     , hsf_invis_bndrs  :: [LHsTyVarBndr Specificity pass]
@@ -416,6 +416,17 @@ emptyLHsQTvs = HsQTvs { hsq_ext = [], hsq_explicit = [] }
 -- Used to quantify the implicit binders of a type
 --    * Implicit binders of a type signature (LHsSigType/LHsSigWcType)
 --    * Patterns in a type/data family instance (HsTyPats)
+--
+-- We support two forms:
+--   HsOuterImplicit (implicit quantification, added by renamer)
+--         f :: a -> a     -- Short for f :: forall {a}. a->a
+--   HsOuterExplicit (explicit user quantifiation):
+--         f :: forall a. a->a
+--
+-- When the user writes /visible/ quanitification
+--         T :: forall k -> k -> Type
+-- we use use HsOuterImplicit, wrapped around a HsForAllTy
+-- for the visible quantification
 
 -- | TODO RGS: Docs
 data HsOuterTyVarBndrs flag pass


=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -349,6 +349,7 @@ tcHsSigType ctxt sig_ty
 
        -- Spit out the implication (and perhaps fail fast)
        -- See Note [Failure in local type signatures] in GHC.Tc.Solver
+       ; traceTc "tcHsSigType 2" (ppr implic)
        ; emitFlatConstraints (mkImplicWC (unitBag implic))
 
        ; ty <- zonkTcType ty
@@ -358,59 +359,6 @@ tcHsSigType ctxt sig_ty
   where
     skol_info = SigTypeSkol ctxt
 
-{-
--- TODO RGS: Delete this (only for testing purposes)
-tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn
-               -> ContextKind -> TcM (Implication, TcType)
--- Kind-checks/desugars an 'LHsSigType',
---   solve equalities,
---   and then kind-generalizes.
--- This will never emit constraints, as it uses solveEqualities internally.
--- No validity checking or zonking
--- Returns also an implication for the unsolved constraints
-tc_hs_sig_type skol_info hs_sig_type ctxt_kind
-  -- | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type
-  | L l (HsSig { sig_bndrs = outer_bndrs, sig_body = body_ty }) <- hs_sig_type
-  = do { let sig_vars = case outer_bndrs of
-                          HsOuterImplicit{hso_ximplicit = imp_vars} -> imp_vars
-                          HsOuterExplicit{}                         -> []
-             hs_ty = case outer_bndrs of
-                       HsOuterImplicit{} -> body_ty
-                       HsOuterExplicit{hso_bndrs = exp_bndrs} ->
-                         L l $ HsForAllTy { hst_xforall = noExtField
-                                          , hst_tele = HsForAllInvis { hsf_xinvis = noExtField
-                                                                     , hsf_invis_bndrs = exp_bndrs }
-                                          , hst_body = body_ty }
-       ; (tc_lvl, (wanted, (spec_tkvs, ty)))
-              <- pushTcLevelM                           $
-                 solveLocalEqualitiesX "tc_hs_sig_type" $
-                 -- See Note [Failure in local type signatures]
-                 bindImplicitTKBndrs_Skol sig_vars      $
-                 do { kind <- newExpectedKind ctxt_kind
-                    ; tcLHsType hs_ty kind }
-       -- Any remaining variables (unsolved in the solveLocalEqualities)
-       -- should be in the global tyvars, and therefore won't be quantified
-
-       ; spec_tkvs <- zonkAndScopedSort spec_tkvs
-       ; let ty1 = mkSpecForAllTys spec_tkvs ty
-
-       -- This bit is very much like decideMonoTyVars in GHC.Tc.Solver,
-       -- but constraints are so much simpler in kinds, it is much
-       -- easier here. (In particular, we never quantify over a
-       -- constraint in a type.)
-       ; constrained <- zonkTyCoVarsAndFV (tyCoVarsOfWC wanted)
-       ; let should_gen = not . (`elemVarSet` constrained)
-
-       ; kvs <- kindGeneralizeSome should_gen ty1
-
-       -- Build an implication for any as-yet-unsolved kind equalities
-       -- See Note [Skolem escape in type signatures]
-       ; implic <- buildTvImplication skol_info (kvs ++ spec_tkvs) tc_lvl wanted
-
-       ; return (implic, mkInfForAllTys kvs ty1) }
--}
-
--- TODO RGS: This is broken. Figure out why.
 tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn
                -> ContextKind -> TcM (Implication, TcType)
 -- Kind-checks/desugars an 'LHsSigType',
@@ -420,20 +368,49 @@ tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn
 -- No validity checking or zonking
 -- Returns also an implication for the unsolved constraints
 tc_hs_sig_type skol_info (L loc (HsSig { sig_bndrs = outer_bndrs
-                                        , sig_body = hs_ty })) ctxt_kind
+                                       , sig_body = hs_ty })) ctxt_kind
   = setSrcSpan loc $
-    do { (tc_lvl, (wanted, (imp_or_exp_tkvs, ty)))
-              <- pushTcLevelM                           $
-                 solveLocalEqualitiesX "tc_hs_sig_type" $
+    do { -- When there are /explicit/ user-written binders, e.g.
+         --      f :: forall a {k} (b::k). blah
+         -- treat it exactly like HsForAllTy; including its own,
+         -- individual implication constraint, so we get proper
+         -- telescope checking.
+         -- NB1: Do not be tempted to combine this implication constraint
+         --      with the one from kind generalisation. That messes up the
+         --      telescope error message, by mixing the inferred kind
+         --      quantifiers with the explicit ones.
+         -- NB2: There are no implicit binders (the forall-or-nothing rule),
+         --   hence implicit_bndrs = []
+         --
+         -- When there are only /implicit/ binders, added by the renamer, e.g.
+         --     f :: a -> t a -> t a
+         -- then bring those implicit binders into scope here.
+
+         let body_hs_ty     :: LHsType GhcRn
+             implicit_bndrs :: [Name]
+             (implicit_bndrs, body_hs_ty)
+                = case outer_bndrs of
+                    HsOuterExplicit { hso_bndrs = bndrs }
+                      -> ([], L loc $
+                              HsForAllTy { hst_xforall = noExtField
+                                         , hst_tele    = HsForAllInvis { hsf_xinvis = noExtField
+                                                                       , hsf_invis_bndrs = bndrs }
+                                         , hst_body    = hs_ty })
+                    HsOuterImplicit { hso_ximplicit = implicit_bndrs }
+                      -> (implicit_bndrs, hs_ty)
+
+       ; (tc_lvl, (wanted, (implicit_tkvs, ty)))
+              <- pushTcLevelM                            $
+                 solveLocalEqualitiesX "tc_hs_sig_type"  $
                  -- See Note [Failure in local type signatures]
-                 bindOuterSigTKBndrs_Skol outer_bndrs   $
+                 bindImplicitTKBndrs_Skol implicit_bndrs $
                  do { kind <- newExpectedKind ctxt_kind
-                    ; tcLHsType hs_ty kind }
+                    ; tcLHsType body_hs_ty kind }
        -- Any remaining variables (unsolved in the solveLocalEqualities)
        -- should be in the global tyvars, and therefore won't be quantified
 
-       ; imp_or_exp_tkvs <- bitraverse zonkAndScopedSort pure imp_or_exp_tkvs
-       ; let ty1 = either mkSpecForAllTys mkInvisForAllTys imp_or_exp_tkvs ty
+       ; implicit_tkvs <- zonkAndScopedSort implicit_tkvs
+       ; let ty1 = mkSpecForAllTys implicit_tkvs ty
 
        -- This bit is very much like decideMonoTyVars in GHC.Tc.Solver,
        -- but constraints are so much simpler in kinds, it is much
@@ -446,10 +423,7 @@ tc_hs_sig_type skol_info (L loc (HsSig { sig_bndrs = outer_bndrs
 
        -- Build an implication for any as-yet-unsolved kind equalities
        -- See Note [Skolem escape in type signatures]
-       ; implic <- buildTvImplication skol_info
-                     (kvs ++ either id binderVars imp_or_exp_tkvs) tc_lvl wanted
-         -- TODO RGS: The line above can put /visible/ foralls in a tyvar implication.
-         -- I'm not sure if that's kosher.
+       ; implic <- buildTvImplication skol_info (kvs ++ implicit_tkvs) tc_lvl wanted
 
        ; return (implic, mkInfForAllTys kvs ty1) }
 
@@ -1050,7 +1024,7 @@ tc_hs_type mode forall@(HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
             <- pushLevelAndCaptureConstraints      $
                bindExplicitTKTele_Skol_M mode tele $
                  -- The _M variant passes on the mode from the type, to
-                 -- any wildards in kind signatures on the forall'd variables
+                 -- any wildcards in kind signatures on the forall'd variables
                  -- e.g.      f :: _ -> Int -> forall (a :: _). blah
                tc_lhs_type mode ty exp_kind
                  -- Why exp_kind?  See Note [Body kind of HsForAllTy]


=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -163,21 +163,28 @@ simplifyTop wanteds
 solveLocalEqualities :: String -> TcM a -> TcM a
 -- Note [Failure in local type signatures]
 solveLocalEqualities callsite thing_inside
-  = do { (wanted, res) <- solveLocalEqualitiesX callsite thing_inside
+  = do { traceTc "solveLocalEqualities {" (vcat [ text "Called from" <+> text callsite ])
+       ; (res, wanted) <- captureConstraints thing_inside
        ; emitFlatConstraints wanted
+       ; traceTc "solveLocalEqualitie }" empty
        ; return res }
 
 emitFlatConstraints :: WantedConstraints -> TcM ()
 -- See Note [Failure in local type signatures]
 emitFlatConstraints wanted
-  = do { wanted <- TcM.zonkWC wanted
+  = do { -- Solve and zonk to esablish the
+         -- preconditions for floatKindEqualities
+         wanted <- runTcSEqualities (solveWanteds wanted)
+       ; wanted <- TcM.zonkWC wanted
+
+       ; traceTc "emitFlatConstraints {" (ppr wanted)
        ; case floatKindEqualities wanted of
-           Nothing -> do { traceTc "emitFlatConstraints: failing" (ppr wanted)
+           Nothing -> do { traceTc "emitFlatConstraints } failing" (ppr wanted)
                          ; emitConstraints wanted -- So they get reported!
                          ; failM }
            Just (simples, holes)
               -> do { _ <- promoteTyVarSet (tyCoVarsOfCts simples)
-                    ; traceTc "emitFlatConstraints:" $
+                    ; traceTc "emitFlatConstraints }" $
                       vcat [ text "simples:" <+> ppr simples
                            , text "holes:  " <+> ppr holes ]
                     ; emitHoles holes -- Holes don't need promotion
@@ -188,6 +195,11 @@ floatKindEqualities :: WantedConstraints -> Maybe (Bag Ct, Bag Hole)
 -- Return Nothing if any constraints can't be floated (captured
 -- by skolems), or if there is an insoluble constraint, or
 -- IC_Telescope telescope error
+-- Precondition 1: we have tried to solve the 'wanteds', both so that
+--    the ic_status field is set, and because solving can make constraints
+--    more floatable.
+-- Precondition 2: the 'wanteds' are zonked, since floatKindEqualities
+--    is not monadic
 floatKindEqualities wc = float_wc emptyVarSet wc
   where
     float_wc :: TcTyCoVarSet -> WantedConstraints -> Maybe (Bag Ct, Bag Hole)



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/60dd0659f5d42e1a2f7620f55a1e8e3befceffe2
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/20200921/3da1eae9/attachment-0001.html>


More information about the ghc-commits mailing list