[Git][ghc/ghc][wip/T16762] Fixes from Simon
Simon Peyton Jones
gitlab at gitlab.haskell.org
Mon Sep 21 14:46:08 UTC 2020
Simon Peyton Jones pushed to branch wip/T16762 at Glasgow Haskell Compiler / GHC
Commits:
9004c100 by Simon Peyton Jones at 2020-09-21T15:45:13+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
- - - - -
4 changed files:
- compiler/GHC/Hs/Type.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Types/Constraint.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,50 @@ 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. See GHC.Tc.Types.Constraint
+ -- Note [Checking telescopes], in the "don't mix up" bullet.
+ -- 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 +424,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 +1025,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)
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -1235,7 +1235,7 @@ all at once, creating one implication constraint for the lot:
that binds existentials, where the type of the data constructor is
known to be valid (it in tcConPat), no need for the check.
- So the check is done if and only if ic_info is ForAllSkol
+ So the check is done /if and only if/ ic_info is ForAllSkol.
* If ic_info is (ForAllSkol dt dvs), the dvs::SDoc displays the
original, user-written type variables.
@@ -1245,6 +1245,18 @@ all at once, creating one implication constraint for the lot:
constraint solver a chance to make that bad-telescope test! Hence
the extra guard in emitResidualTvConstraint; see #16247
+* Don't mix up inferred and explicit variables in the same implication
+ constraint. E.g.
+ foo :: forall a kx (b :: kx). SameKind a b
+ We want an implication
+ Implic { ic_skol = [(a::kx), kx, (b::kx)], ... }
+ but GHC will attempt to quantify over kx, since it is free in (a::kx),
+ and it's hopelessly confusing to report an error about quantified
+ variables kx (a::kx) kx (b::kx).
+ Instead, the outer quantification over kx should be in a separate
+ implication. TL;DR: an explicit forall should generate an implication
+ quantified only over those explicitly quantified variables.
+
Note [Needed evidence variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Th ic_need_evs field holds the free vars of ic_binds, and all the
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9004c100c4ded5fe0894e957b857eed95bb07605
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9004c100c4ded5fe0894e957b857eed95bb07605
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/1e7f6e96/attachment-0001.html>
More information about the ghc-commits
mailing list