[Git][ghc/ghc][master] Add a missing zonk in tcHsPartialType
Marge Bot
gitlab at gitlab.haskell.org
Sat Apr 18 17:20:39 UTC 2020
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
84cc8394 by Simon Peyton Jones at 2020-04-18T13:20:29-04:00
Add a missing zonk in tcHsPartialType
I omitted a vital zonk when refactoring tcHsPartialType in
commit 48fb3482f8cbc8a4b37161021e846105f980eed4
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Wed Jun 5 08:55:17 2019 +0100
Fix typechecking of partial type signatures
This patch fixes it and adds commentary to explain why.
Fixes #18008
- - - - -
4 changed files:
- compiler/GHC/Tc/Gen/HsType.hs
- + testsuite/tests/partial-sigs/should_compile/T18008.hs
- + testsuite/tests/partial-sigs/should_compile/T18008.stderr
- testsuite/tests/partial-sigs/should_compile/all.T
Changes:
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -732,6 +732,7 @@ tc_hs_type mode forall@(HsForAllTy { hst_fvf = fvf, hst_bndrs = hs_tvs
m_telescope = Just (sep (map ppr hs_tvs))
; emitResidualTvConstraint skol_info m_telescope tvs' tclvl wanted
+ -- See Note [Skolem escape and forall-types]
; return (mkForAllTys bndrs ty') }
@@ -920,6 +921,26 @@ under these conditions.
See related Note [Wildcards in visible type application] here and
Note [The wildcard story for types] in GHC.Hs.Types
+Note [Skolem escape and forall-types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ f :: forall a. (forall kb (b :: kb). Proxy '[a, b]) -> ()
+
+The Proxy '[a,b] forces a and b to have the same kind. But a's
+kind must be bound outside the 'forall a', and hence escapes.
+We discover this by building an implication constraint for
+each forall. So the inner implication constraint will look like
+ forall kb (b::kb). kb ~ ka
+where ka is a's kind. We can't unify these two, /even/ if ka is
+unification variable, because it would be untouchable inside
+this inner implication.
+
+That's what the pushLevelAndCaptureConstraints, plus subsequent
+emitResidualTvConstraint is all about, when kind-checking
+HsForAllTy.
+
+Note that we don't need to /simplify/ the constraints here
+because we aren't generalising. We just capture them.
-}
{- *********************************************************************
@@ -2819,10 +2840,13 @@ kindGeneralizeAll ty = do { traceTc "kindGeneralizeAll" empty
; kindGeneralizeSome (const True) ty }
-- | Specialized version of 'kindGeneralizeSome', but where no variables
--- can be generalized. Use this variant when it is unknowable whether metavariables
--- might later be constrained.
--- See Note [Recipe for checking a signature] for why and where this
--- function is needed.
+-- can be generalized, but perhaps some may neeed to be promoted.
+-- Use this variant when it is unknowable whether metavariables might
+-- later be constrained.
+--
+-- To see why this promotion is needed, see
+-- Note [Recipe for checking a signature], and especially
+-- Note [Promotion in signatures].
kindGeneralizeNone :: TcType -- needn't be zonked
-> TcM ()
kindGeneralizeNone ty
@@ -3160,7 +3184,7 @@ tcHsPartialSigType ctxt sig_ty
; return (wcs, wcx, theta, tau) }
- -- No kind-generalization here:
+ -- No kind-generalization here, but perhaps some promotion
; kindGeneralizeNone (mkSpecForAllTys implicit_tvs $
mkSpecForAllTys explicit_tvs $
mkPhiTy theta $
@@ -3171,6 +3195,14 @@ tcHsPartialSigType ctxt sig_ty
-- See Note [Extra-constraint holes in partial type signatures]
; emitNamedWildCardHoleConstraints wcs
+ -- Zonk, so that any nested foralls can "see" their occurrences
+ -- See Note [Checking partial type signatures], in
+ -- the bullet on Nested foralls.
+ ; implicit_tvs <- mapM zonkTcTyVarToTyVar implicit_tvs
+ ; explicit_tvs <- mapM zonkTcTyVarToTyVar explicit_tvs
+ ; theta <- mapM zonkTcType theta
+ ; tau <- zonkTcType tau
+
-- We return a proper (Name,TyVar) environment, to be sure that
-- we bring the right name into scope in the function body.
-- Test case: partial-sigs/should_compile/LocalDefinitionBug
@@ -3179,7 +3211,7 @@ tcHsPartialSigType ctxt sig_ty
-- NB: checkValidType on the final inferred type will be
-- done later by checkInferredPolyId. We can't do it
- -- here because we don't have a complete tuype to check
+ -- here because we don't have a complete type to check
; traceTc "tcHsPartialSigType" (ppr tv_prs)
; return (wcs, wcx, tv_prs, theta, tau) }
@@ -3198,12 +3230,31 @@ tcPartialContext hs_theta
{- Note [Checking partial type signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-See also Note [Recipe for checking a signature]
+This Note is about tcHsPartialSigType. See also
+Note [Recipe for checking a signature]
When we have a partial signature like
- f,g :: forall a. a -> _
+ f :: forall a. a -> _
we do the following
+* tcHsPartialSigType does not make quantified type (forall a. blah)
+ and then instantiate it -- it makes no sense to instantiate a type
+ with wildcards in it. Rather, tcHsPartialSigType just returns the
+ 'a' and the 'blah' separately.
+
+ Nor, for the same reason, do we push a level in tcHsPartialSigType.
+
+* We instantiate 'a' to a unification variable, a TyVarTv, and /not/
+ a skolem; hence the "_Tv" in bindExplicitTKBndrs_Tv. Consider
+ f :: forall a. a -> _
+ g :: forall b. _ -> b
+ f = g
+ g = f
+ They are typechecked as a recursive group, with monomorphic types,
+ so 'a' and 'b' will get unified together. Very like kind inference
+ for mutually recursive data types (sans CUSKs or SAKS); see
+ Note [Cloning for tyvar binders] in GHC.Tc.Gen.HsType
+
* In GHC.Tc.Gen.Sig.tcUserSigType we return a PartialSig, which (unlike
the companion CompleteSig) contains the original, as-yet-unchecked
source-code LHsSigWcType
@@ -3218,12 +3269,28 @@ we do the following
g x = True
It's really as if we'd written two distinct signatures.
-* Note that we don't make quantified type (forall a. blah) and then
- instantiate it -- it makes no sense to instantiate a type with
- wildcards in it. Rather, tcHsPartialSigType just returns the
- 'a' and the 'blah' separately.
-
- Nor, for the same reason, do we push a level in tcHsPartialSigType.
+* Nested foralls. Consider
+ f :: forall b. (forall a. a -> _) -> b
+ We do /not/ allow the "_" to be instantiated to 'a'; but we do
+ (as before) allow it to be instantiated to the (top level) 'b'.
+ Why not? Because suppose
+ f x = (x True, x 'c')
+ We must instantiate that (forall a. a -> _) when typechecking
+ f's body, so we must know precisely where all the a's are; they
+ must not be hidden under (filled-in) unification variables!
+
+ We achieve this in the usual way: we push a level at a forall,
+ so now the unification variable for the "_" can't unify with
+ 'a'.
+
+* Just as for ordinary signatures, we must zonk the type after
+ kind-checking it, to ensure that all the nested forall binders can
+ see their occurrenceds
+
+ Just as for ordinary signatures, this zonk also gets any Refl casts
+ out of the way of instantiation. Example: #18008 had
+ foo :: (forall a. (Show a => blah) |> Refl) -> _
+ and that Refl cast messed things up. See #18062.
Note [Extra-constraint holes in partial type signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
testsuite/tests/partial-sigs/should_compile/T18008.hs
=====================================
@@ -0,0 +1,7 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+module Bug where
+
+f :: (forall a. Show a => a -> String) -> _
+f s = s ()
+
=====================================
testsuite/tests/partial-sigs/should_compile/T18008.stderr
=====================================
@@ -0,0 +1,5 @@
+
+T18008.hs:5:43: warning: [-Wpartial-type-signatures (in -Wdefault)]
+ • Found type wildcard ‘_’ standing for ‘String’
+ • In the type ‘(forall a. Show a => a -> String) -> _’
+ In the type signature: f :: (forall a. Show a => a -> String) -> _
=====================================
testsuite/tests/partial-sigs/should_compile/all.T
=====================================
@@ -95,3 +95,4 @@ test('T16334', normal, compile, [''])
test('T16728', normal, compile, [''])
test('T16728a', normal, compile, [''])
test('T16728b', normal, compile, [''])
+test('T18008', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/84cc8394d075cea236faa0bcd9ef0a84de89ee8c
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/84cc8394d075cea236faa0bcd9ef0a84de89ee8c
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/20200418/3aa34675/attachment-0001.html>
More information about the ghc-commits
mailing list