From 48fb3482f8cbc8a4b37161021e846105f980eed4 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Wed, 5 Jun 2019 08:55:17 +0100
Subject: [PATCH] Fix typechecking of partial type signatures
Partial type sigs had grown hair. tcHsParialSigType was
doing lots of unnecessary work, and tcInstSig was cloning it
unnecessarily -- and the result didn't even work: #16728.
This patch cleans it all up, described by TcHsType
Note [Checking parital type signatures]
I basically just deleted code... but very carefully!
Some refactoring along the way
* Distinguish more explicintly between "anonymous" wildcards "_"
and "named" wildcards "_a". I changed the names of a number
of functions to make this distinction much more apparent.
The patch also revealed that the code in `TcExpr`
that implements the special typing rule for `($)` was wrong.
It called `getRuntimeRep` in a situation where where was no
particular reason to suppose that the thing had kind `TYPE r`.
This caused a crash in typecheck/should_run/T10846.
The fix was easy, and actually simplifies the code in `TcExpr`
quite a bit. Hooray.
---
compiler/rename/RnTypes.hs | 7 +-
compiler/typecheck/TcBinds.hs | 2 +-
compiler/typecheck/TcCanonical.hs | 2 +
compiler/typecheck/TcExpr.hs | 31 ++--
compiler/typecheck/TcHsType.hs | 161 ++++++++++--------
compiler/typecheck/TcRnDriver.hs | 4 +-
compiler/typecheck/TcRnMonad.hs | 17 +-
compiler/typecheck/TcRnTypes.hs | 2 +-
compiler/typecheck/TcSigs.hs | 21 +--
compiler/typecheck/TcType.hs | 13 +-
.../partial-sigs/should_compile/T16728.hs | 9 +
.../partial-sigs/should_compile/T16728.stderr | 9 +
.../partial-sigs/should_compile/T16728a.hs | 8 +
.../should_compile/T16728a.stderr | 20 +++
.../partial-sigs/should_compile/T16728b.hs | 9 +
.../should_compile/T16728b.stderr | 13 ++
.../tests/partial-sigs/should_compile/all.T | 3 +
.../partial-sigs/should_fail/T14040a.stderr | 8 +-
18 files changed, 215 insertions(+), 124 deletions(-)
create mode 100644 testsuite/tests/partial-sigs/should_compile/T16728.hs
create mode 100644 testsuite/tests/partial-sigs/should_compile/T16728.stderr
create mode 100644 testsuite/tests/partial-sigs/should_compile/T16728a.hs
create mode 100644 testsuite/tests/partial-sigs/should_compile/T16728a.stderr
create mode 100644 testsuite/tests/partial-sigs/should_compile/T16728b.hs
create mode 100644 testsuite/tests/partial-sigs/should_compile/T16728b.stderr
diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs
index 755ed206f0f5..4b4d519324cd 100644
--- a/compiler/rename/RnTypes.hs
+++ b/compiler/rename/RnTypes.hs
@@ -693,8 +693,8 @@ checkAnonWildCard env
| otherwise
= case rtke_what env of
RnTypeBody -> Nothing
- RnConstraint -> Just constraint_msg
RnTopConstraint -> Just constraint_msg
+ RnConstraint -> Just constraint_msg
constraint_msg = hang
(notAllowed pprAnonWildCard <+> text "in a constraint")
@@ -714,7 +714,10 @@ checkNamedWildCard env name
| otherwise
= case rtke_what env of
RnTypeBody -> Nothing -- Allowed
- RnTopConstraint -> Nothing -- Allowed
+ RnTopConstraint -> Nothing -- Allowed; e.g.
+ -- f :: (Eq _a) => _a -> Int
+ -- g :: (_a, _b) => T _a _b -> Int
+ -- The named tyvars get filled in from elsewhere
RnConstraint -> Just constraint_msg
constraint_msg = notAllowed (ppr name) <+> text "in a constraint"
diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index c8c1bc06bd00..72748ac76f77 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -1020,7 +1020,7 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
; case tcGetCastedTyVar_maybe wc_var_ty of
-- We know that wc_co must have type kind(wc_var) ~ Constraint, as it
- -- comes from the checkExpectedKind in TcHsType.tcWildCardOcc. So, to
+ -- comes from the checkExpectedKind in TcHsType.tcAnonWildCardOcc. So, to
-- make the kinds work out, we reverse the cast here.
Just (wc_var, wc_co) -> writeMetaTyVar wc_var (ctuple `mkCastTy` mkTcSymCo wc_co)
Nothing -> pprPanic "chooseInferredQuantifiers 1" (ppr wc_var_ty)
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index c296a9eee393..31c9ad9a8968 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1009,6 +1009,8 @@ can_eq_nc_forall ev eq_rel s1 s2
(substTy subst (tyVarKind tv2))
; let subst' = extendTvSubstAndInScope subst tv2
(mkCastTy (mkTyVarTy skol_tv) kind_co)
+ -- skol_tv is already in the in-scope set, but the
+ -- free vars of kind_co are not; hence "...AndInScope"
; (co, wanteds2) <- go skol_tvs subst' bndrs2
; return ( mkTcForAllCo skol_tv kind_co co
, wanteds1 `unionBags` wanteds2 ) }
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index adaea907670f..891f3ad8c3c5 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -378,42 +378,35 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty
-- So: arg1_ty = arg2_ty -> op_res_ty
-- where arg2_sigma maybe polymorphic; that's the point
- ; arg2' <- tcArg op arg2 arg2_sigma 2
+ ; arg2' <- tcArg op arg2 arg2_sigma 2
-- Make sure that the argument type has kind '*'
-- ($) :: forall (r:RuntimeRep) (a:*) (b:TYPE r). (a->b) -> a -> b
-- Eg we do not want to allow (D# $ 4.0#) #5570
-- (which gives a seg fault)
- --
- -- The *result* type can have any kind (#8739),
- -- so we don't need to check anything for that
; _ <- unifyKind (Just (XHsType $ NHsCoreTy arg2_sigma))
(tcTypeKind arg2_sigma) liftedTypeKind
- -- ignore the evidence. arg2_sigma must have type * or #,
- -- because we know arg2_sigma -> or_res_ty is well-kinded
+ -- Ignore the evidence. arg2_sigma must have type * or #,
+ -- because we know (arg2_sigma -> op_res_ty) is well-kinded
-- (because otherwise matchActualFunTys would fail)
- -- There's no possibility here of, say, a kind family reducing to *.
+ -- So this 'unifyKind' will either succeed with Refl, or will
+ -- produce an insoluble constraint * ~ #, which we'll report later.
- ; wrap_res <- tcSubTypeHR orig1 (Just expr) op_res_ty res_ty
- -- op_res -> res
+ -- NB: unlike the argument type, the *result* type, op_res_ty can
+ -- have any kind (#8739), so we don't need to check anything for that
; op_id <- tcLookupId op_name
- ; res_ty <- readExpType res_ty
- ; let op' = L loc (mkHsWrap (mkWpTyApps [ getRuntimeRep res_ty
+ ; let op' = L loc (mkHsWrap (mkWpTyApps [ getRuntimeRep op_res_ty
, arg2_sigma
- , res_ty])
+ , op_res_ty])
(HsVar noExt (L lv op_id)))
-- arg1' :: arg1_ty
-- wrap_arg1 :: arg1_ty "->" (arg2_sigma -> op_res_ty)
- -- wrap_res :: op_res_ty "->" res_ty
- -- op' :: (a2_ty -> res_ty) -> a2_ty -> res_ty
+ -- op' :: (a2_ty -> op_res_ty) -> a2_ty -> op_res_ty
- -- wrap1 :: arg1_ty "->" (arg2_sigma -> res_ty)
- wrap1 = mkWpFun idHsWrapper wrap_res arg2_sigma res_ty doc
- <.> wrap_arg1
- doc = text "When looking at the argument to ($)"
+ expr' = OpApp fix (mkLHsWrap wrap_arg1 arg1') op' arg2'
- ; return (OpApp fix (mkLHsWrap wrap1 arg1') op' arg2') }
+ ; tcWrapResult expr expr' op_res_ty res_ty }
| (L loc (HsRecFld _ (Ambiguous _ lbl))) <- op
, Just sig_ty <- obviousSig (unLoc arg1)
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index f2a795045018..adc25f5ff886 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -36,7 +36,7 @@ module TcHsType (
-- Kind-checking types
-- No kind generalisation, no checkValidType
kcLHsQTyVars,
- tcWildCardBinders,
+ tcNamedWildCardBinders,
tcHsLiftedType, tcHsOpenType,
tcHsLiftedTypeNC, tcHsOpenTypeNC,
tcLHsType, tcLHsTypeUnsaturated, tcCheckLHsType,
@@ -387,7 +387,7 @@ tcHsTypeApp wc_ty kind
unsetWOptM Opt_WarnPartialTypeSignatures $
setXOptM LangExt.PartialTypeSignatures $
-- See Note [Wildcards in visible type application]
- tcWildCardBinders sig_wcs $ \ _ ->
+ tcNamedWildCardBinders sig_wcs $ \ _ ->
tcCheckLHsType hs_ty kind
-- We must promote here. Ex:
-- f :: forall a. a
@@ -402,18 +402,19 @@ tcHsTypeApp (XHsWildCardBndrs _) _ = panic "tcHsTypeApp"
{- Note [Wildcards in visible type application]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-A HsWildCardBndrs's hswc_ext now only includes named wildcards, so any unnamed
-wildcards stay unchanged in hswc_body and when called in tcHsTypeApp, tcCheckLHsType
-will call emitWildCardHoleConstraints on them. However, this would trigger
-error/warning when an unnamed wildcard is passed in as a visible type argument,
-which we do not want because users should be able to write @_ to skip a instantiating
-a type variable variable without fuss. The solution is to switch the
-PartialTypeSignatures flags here to let the typechecker know that it's checking
-a '@_' and do not emit hole constraints on it.
-See related Note [Wildcards in visible kind application]
-and Note [The wildcard story for types] in HsTypes.hs
-
+A HsWildCardBndrs's hswc_ext now only includes /named/ wildcards, so
+any unnamed wildcards stay unchanged in hswc_body. When called in
+tcHsTypeApp, tcCheckLHsType will call emitAnonWildCardHoleConstraint
+on these anonymous wildcards. However, this would trigger
+error/warning when an anonymous wildcard is passed in as a visible type
+argument, which we do not want because users should be able to write
+@_ to skip a instantiating a type variable variable without fuss. The
+solution is to switch the PartialTypeSignatures flags here to let the
+typechecker know that it's checking a '@_' and do not emit hole
+constraints on it. See related Note [Wildcards in visible kind
+application] and Note [The wildcard story for types] in HsTypes.hs
+
+Ugh!
-}
{-
@@ -829,7 +830,7 @@ tc_hs_type mode ty@(HsAppKindTy{}) ek = tc_infer_hs_type_ek mode ty ek
tc_hs_type mode ty@(HsOpTy {}) ek = tc_infer_hs_type_ek mode ty ek
tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek
tc_hs_type mode ty@(XHsType (NHsCoreTy{})) ek = tc_infer_hs_type_ek mode ty ek
-tc_hs_type _ wc@(HsWildCardTy _) ek = tcWildCardOcc wc ek
+tc_hs_type _ wc@(HsWildCardTy _) ek = tcAnonWildCardOcc wc ek
------------------------------------------
tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> TcKind
@@ -849,18 +850,18 @@ tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
liftedTypeKind exp_kind }
---------------------------
-tcWildCardOcc :: HsType GhcRn -> Kind -> TcM TcType
-tcWildCardOcc wc exp_kind
- = do { wc_tv <- newWildTyVar
- -- The wildcard's kind should be an un-filled-in meta tyvar
- ; loc <- getSrcSpanM
- ; uniq <- newUnique
- ; let name = mkInternalName uniq (mkTyVarOcc "_") loc
+tcAnonWildCardOcc :: HsType GhcRn -> Kind -> TcM TcType
+tcAnonWildCardOcc wc exp_kind
+ = do { wc_tv <- newWildTyVar -- The wildcard's kind will be an un-filled-in meta tyvar
+
; part_tysig <- xoptM LangExt.PartialTypeSignatures
; warning <- woptM Opt_WarnPartialTypeSignatures
- -- See Note [Wildcards in visible kind application]
- ; unless (part_tysig && not warning)
- (emitWildCardHoleConstraints [(name,wc_tv)])
+
+ ; unless (part_tysig && not warning) $
+ emitAnonWildCardHoleConstraint wc_tv
+ -- Why the 'unless' guard?
+ -- See Note [Wildcards in visible kind application]
+
; checkExpectedKind wc (mkTyVarTy wc_tv)
(tyVarKind wc_tv) exp_kind }
@@ -877,11 +878,11 @@ x = MkT
So we should allow '@_' without emitting any hole constraints, and
regardless of whether PartialTypeSignatures is enabled or not. But how would
the typechecker know which '_' is being used in VKA and which is not when it
-calls emitWildCardHoleConstraints in tcHsPartialSigType on all HsWildCardBndrs?
+calls emitNamedWildCardHoleConstraints in tcHsPartialSigType on all HsWildCardBndrs?
The solution then is to neither rename nor include unnamed wildcards in HsWildCardBndrs,
-but instead give every unnamed wildcard a fresh wild tyvar in tcWildCardOcc.
+but instead give every anonymous wildcard a fresh wild tyvar in tcAnonWildCardOcc.
And whenever we see a '@', we automatically turn on PartialTypeSignatures and
-turn off hole constraint warnings, and never call emitWildCardHoleConstraints
+turn off hole constraint warnings, and do not call emitAnonWildCardHoleConstraint
under these conditions.
See related Note [Wildcards in visible type application] here and
Note [The wildcard story for types] in HsTypes.hs
@@ -1722,23 +1723,26 @@ To avoid the double-zonk, we do two things:
gathers free variables. So this way effectively sidesteps step 3.
-}
-tcWildCardBinders :: [Name]
- -> ([(Name, TcTyVar)] -> TcM a)
- -> TcM a
-tcWildCardBinders wc_names thing_inside
+tcNamedWildCardBinders :: [Name]
+ -> ([(Name, TcTyVar)] -> TcM a)
+ -> TcM a
+-- Bring into scope the /named/ wildcard binders. Remember that
+-- plain wildcards _ are anonymous and dealt with by HsWildCardTy
+-- Soe Note [The wildcard story for types] in HsTypes
+tcNamedWildCardBinders wc_names thing_inside
= do { wcs <- mapM (const newWildTyVar) wc_names
; let wc_prs = wc_names `zip` wcs
; tcExtendNameTyVarEnv wc_prs $
thing_inside wc_prs }
newWildTyVar :: TcM TcTyVar
--- ^ New unification variable for a wildcard
+-- ^ New unification variable '_' for a wildcard
newWildTyVar
= do { kind <- newMetaKindVar
; uniq <- newUnique
; details <- newMetaDetails TauTv
- ; let name = mkSysTvName uniq (fsLit "_")
- tyvar = (mkTcTyVar name kind details)
+ ; let name = mkSysTvName uniq (fsLit "_")
+ tyvar = mkTcTyVar name kind details
; traceTc "newWildTyVar" (ppr tyvar)
; return tyvar }
@@ -2490,11 +2494,11 @@ tcHsPartialSigType
-> LHsSigWcType GhcRn -- The type signature
-> TcM ( [(Name, TcTyVar)] -- Wildcards
, Maybe TcType -- Extra-constraints wildcard
- , [Name] -- Original tyvar names, in correspondence with ...
- , [TcTyVar] -- ... Implicitly and explicitly bound type variables
+ , [(Name,TcTyVar)] -- Original tyvar names, in correspondence with
+ -- the implicitly and explicitly bound type variables
, TcThetaType -- Theta part
, TcType ) -- Tau part
--- See Note [Recipe for checking a signature]
+-- See Note [Checking partial type signatures]
tcHsPartialSigType ctxt sig_ty
| HsWC { hswc_ext = sig_wcs, hswc_body = ib_ty } <- sig_ty
, HsIB { hsib_ext = implicit_hs_tvs
@@ -2502,8 +2506,11 @@ tcHsPartialSigType ctxt sig_ty
, (explicit_hs_tvs, L _ hs_ctxt, hs_tau) <- splitLHsSigmaTy hs_ty
= addSigCtxt ctxt hs_ty $
do { (implicit_tvs, (explicit_tvs, (wcs, wcx, theta, tau)))
- <- solveLocalEqualities "tcHsPatSigTypes" $
- tcWildCardBinders sig_wcs $ \ wcs ->
+ <- solveLocalEqualities "tcHsPartialSigType" $
+ -- This solveLocalEqualiltes fails fast if there are
+ -- insoluble equalities. See TcSimplify
+ -- Note [Fail fast if there are insoluble kind equalities]
+ tcNamedWildCardBinders sig_wcs $ \ wcs ->
bindImplicitTKBndrs_Tv implicit_hs_tvs $
bindExplicitTKBndrs_Tv explicit_hs_tvs $
do { -- Instantiate the type-class context; but if there
@@ -2514,38 +2521,23 @@ tcHsPartialSigType ctxt sig_ty
; return (wcs, wcx, theta, tau) }
- -- We must return these separately, because all the zonking below
- -- might change the name of a TyVarTv. This, in turn, causes trouble
- -- in partial type signatures that bind scoped type variables, as
- -- we bring the wrong name into scope in the function body.
- -- Test case: partial-sigs/should_compile/LocalDefinitionBug
- ; let tv_names = implicit_hs_tvs ++ hsLTyVarNames explicit_hs_tvs
-
-- Spit out the wildcards (including the extra-constraints one)
-- as "hole" constraints, so that they'll be reported if necessary
-- See Note [Extra-constraint holes in partial type signatures]
- ; emitWildCardHoleConstraints wcs
+ ; emitNamedWildCardHoleConstraints wcs
- -- The TyVarTvs created above will sometimes have too high a TcLevel
- -- (note that they are generated *after* bumping the level in
- -- the tc{Im,Ex}plicitTKBndrsSig functions. Bumping the level
- -- is still important here, because the kinds of these variables
- -- do indeed need to have the higher level, so they can unify
- -- with other local type variables. But, now that we've type-checked
- -- everything (and solved equalities in the tcImplicit call)
- -- we need to promote the TyVarTvs so we don't violate the TcLevel
- -- invariant
- ; implicit_tvs <- zonkAndScopedSort implicit_tvs
- ; explicit_tvs <- mapM zonkAndSkolemise explicit_tvs
- ; theta <- mapM zonkTcType theta
- ; tau <- zonkTcType tau
-
- ; let all_tvs = implicit_tvs ++ explicit_tvs
+ -- 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
+ ; let tv_prs = (implicit_hs_tvs `zip` implicit_tvs)
+ ++ (hsLTyVarNames explicit_hs_tvs `zip` explicit_tvs)
- ; checkValidType ctxt (mkSpecForAllTys all_tvs $ mkPhiTy theta tau)
+ -- 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
- ; traceTc "tcHsPartialSigType" (ppr all_tvs)
- ; return (wcs, wcx, tv_names, all_tvs, theta, tau) }
+ ; traceTc "tcHsPartialSigType" (ppr tv_prs)
+ ; return (wcs, wcx, tv_prs, theta, tau) }
tcHsPartialSigType _ (HsWC _ (XHsImplicitBndrs _)) = panic "tcHsPartialSigType"
tcHsPartialSigType _ (XHsWildCardBndrs _) = panic "tcHsPartialSigType"
@@ -2555,14 +2547,43 @@ tcPartialContext hs_theta
| Just (hs_theta1, hs_ctxt_last) <- snocView hs_theta
, L wc_loc wc@(HsWildCardTy _) <- ignoreParens hs_ctxt_last
= do { wc_tv_ty <- setSrcSpan wc_loc $
- tcWildCardOcc wc constraintKind
+ tcAnonWildCardOcc wc constraintKind
; theta <- mapM tcLHsPredType hs_theta1
; return (theta, Just wc_tv_ty) }
| otherwise
= do { theta <- mapM tcLHsPredType hs_theta
; return (theta, Nothing) }
-{- Note [Extra-constraint holes in partial type signatures]
+{- Note [Checking partial type signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See also Note [Recipe for checking a signature]
+
+When we have a parital signature like
+ f,g :: forall a. a -> _
+we do the following
+
+* In TcSigs.tcUserSigType we return a PartialSig, which (unlike
+ the companion CompleteSig) contains the original, as-yet-unchecked
+ source-code LHsSigWcType
+
+* Then, for f and g /separately/, we call tcInstSig, which in turn
+ call tchsPartialSig (defined near this Note). It kind-checks the
+ LHsSigWcType, creating fresh unification variables for each "_"
+ wildcard. It's important that the wildcards for f and g are distinct
+ becase they migh get instantiated completely differently. E.g.
+ f,g :: forall a. a -> _
+ f x = a
+ 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.
+
+Note [Extra-constraint holes in partial type signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
f :: (_) => a -> a
@@ -2631,12 +2652,12 @@ tcHsPatSigType ctxt sig_ty
-- Always solve local equalities if possible,
-- else casts get in the way of deep skolemisation
-- (#16033)
- tcWildCardBinders sig_wcs $ \ wcs ->
+ tcNamedWildCardBinders sig_wcs $ \ wcs ->
tcExtendNameTyVarEnv sig_tkv_prs $
do { sig_ty <- tcHsOpenType hs_ty
; return (wcs, sig_ty) }
- ; emitWildCardHoleConstraints wcs
+ ; emitNamedWildCardHoleConstraints wcs
-- sig_ty might have tyvars that are at a higher TcLevel (if hs_ty
-- contains a forall). Promote these.
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index d13abf4e0314..3ffc5df61e98 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -2438,8 +2438,8 @@ tcRnType hsc_env flexi normalise rdr_type
-- must push level to satisfy level precondition of
-- kindGeneralize, below
solveEqualities $
- tcWildCardBinders wcs $ \ wcs' ->
- do { emitWildCardHoleConstraints wcs'
+ tcNamedWildCardBinders wcs $ \ wcs' ->
+ do { emitNamedWildCardHoleConstraints wcs'
; tcLHsTypeUnsaturated rn_type }
-- Do kind generalisation; see Note [Kind-generalise in tcRnType]
diff --git a/compiler/typecheck/TcRnMonad.hs b/compiler/typecheck/TcRnMonad.hs
index 25cf04f1532b..9a76e9ced8df 100644
--- a/compiler/typecheck/TcRnMonad.hs
+++ b/compiler/typecheck/TcRnMonad.hs
@@ -103,7 +103,8 @@ module TcRnMonad(
pushTcLevelM_, pushTcLevelM, pushTcLevelsM,
getTcLevel, setTcLevel, isTouchableTcM,
getLclTypeEnv, setLclTypeEnv,
- traceTcConstraints, emitWildCardHoleConstraints,
+ traceTcConstraints,
+ emitNamedWildCardHoleConstraints, emitAnonWildCardHoleConstraint,
-- * Template Haskell context
recordThUse, recordThSpliceUse, recordTopLevelSpliceLoc,
@@ -1676,8 +1677,16 @@ traceTcConstraints msg
hang (text (msg ++ ": LIE:")) 2 (ppr lie)
}
-emitWildCardHoleConstraints :: [(Name, TcTyVar)] -> TcM ()
-emitWildCardHoleConstraints wcs
+emitAnonWildCardHoleConstraint :: TcTyVar -> TcM ()
+emitAnonWildCardHoleConstraint tv
+ = do { ct_loc <- getCtLocM HoleOrigin Nothing
+ ; emitInsolubles $ unitBag $
+ CHoleCan { cc_ev = CtDerived { ctev_pred = mkTyVarTy tv
+ , ctev_loc = ct_loc }
+ , cc_hole = TypeHole (mkTyVarOcc "_") } }
+
+emitNamedWildCardHoleConstraints :: [(Name, TcTyVar)] -> TcM ()
+emitNamedWildCardHoleConstraints wcs
= do { ct_loc <- getCtLocM HoleOrigin Nothing
; emitInsolubles $ listToBag $
map (do_one ct_loc) wcs }
@@ -1690,7 +1699,7 @@ emitWildCardHoleConstraints wcs
where
real_span = case nameSrcSpan name of
RealSrcSpan span -> span
- UnhelpfulSpan str -> pprPanic "emitWildCardHoleConstraints"
+ UnhelpfulSpan str -> pprPanic "emitNamedWildCardHoleConstraints"
(ppr name <+> quotes (ftext str))
-- Wildcards are defined locally, and so have RealSrcSpans
ct_loc' = setCtLocSpan ct_loc real_span
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 221d9cea8c5d..3c6b8ca68590 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -1561,7 +1561,7 @@ data TcIdSigInst
-- Extra-constraints wildcard to fill in, if any
-- If this exists, it is surely of the form (meta_tv |> co)
-- (where the co might be reflexive). This is filled in
- -- only from the return value of TcHsType.tcWildCardOcc
+ -- only from the return value of TcHsType.tcAnonWildCardOcc
}
{- Note [sig_inst_tau may be polymorphic]
diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs
index 5bcb0eee9c2a..da18065b93b9 100644
--- a/compiler/typecheck/TcSigs.hs
+++ b/compiler/typecheck/TcSigs.hs
@@ -498,25 +498,14 @@ tcInstSig hs_sig@(PartialSig { psig_hs_ty = hs_ty
, sig_loc = loc })
= setSrcSpan loc $ -- Set the binding site of the tyvars
do { traceTc "Staring partial sig {" (ppr hs_sig)
- ; (wcs, wcx, tv_names, tvs, theta, tau) <- tcHsPartialSigType ctxt hs_ty
-
- -- Clone the quantified tyvars
- -- Reason: we might have f, g :: forall a. a -> _ -> a
- -- and we want it to behave exactly as if there were
- -- two separate signatures. Cloning here seems like
- -- the easiest way to do so, and is very similar to
- -- the tcInstType in the CompleteSig case
- -- See #14643
- ; (subst, tvs') <- newMetaTyVarTyVars tvs
- -- Why newMetaTyVarTyVars? See TcBinds
- -- Note [Quantified variables in partial type signatures]
- ; let tv_prs = tv_names `zip` tvs'
- inst_sig = TISI { sig_inst_sig = hs_sig
+ ; (wcs, wcx, tv_prs, theta, tau) <- tcHsPartialSigType ctxt hs_ty
+ -- See Note [Checking partial type signatures] in TcHsType
+ ; let inst_sig = TISI { sig_inst_sig = hs_sig
, sig_inst_skols = tv_prs
, sig_inst_wcs = wcs
, sig_inst_wcx = wcx
- , sig_inst_theta = substTysUnchecked subst theta
- , sig_inst_tau = substTyUnchecked subst tau }
+ , sig_inst_theta = theta
+ , sig_inst_tau = tau }
; traceTc "End partial sig }" (ppr inst_sig)
; return inst_sig }
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 55427d509ab3..55cb50113991 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -1795,11 +1795,14 @@ hasTyVarHead ty -- Haskell 98 allows predicates of form
Nothing -> False
evVarPred :: EvVar -> PredType
-evVarPred var
- = ASSERT2( isEvVarType var_ty, ppr var <+> dcolon <+> ppr var_ty )
- var_ty
- where
- var_ty = varType var
+evVarPred var = varType var
+ -- Historical note: I used to have an ASSERT here,
+ -- checking (isEvVarType (varType var)). But with something like
+ -- f :: c => _ -> _
+ -- we end up with (c :: kappa), and (kappa ~ Constraint). Until
+ -- we solve and zonk (which there is no particular reason to do for
+ -- partial signatures, (isEvVarType kappa) will return False. But
+ -- nothing is wrong. So I just removed the ASSERT.
------------------
-- | When inferring types, should we quantify over a given predicate?
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728.hs b/testsuite/tests/partial-sigs/should_compile/T16728.hs
new file mode 100644
index 000000000000..f54f17ef560d
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16728.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module Bug where
+
+import Data.Proxy
+
+f :: forall k (x :: k). Proxy (x :: _)
+f = Proxy
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728.stderr b/testsuite/tests/partial-sigs/should_compile/T16728.stderr
new file mode 100644
index 000000000000..6efdae343ee4
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16728.stderr
@@ -0,0 +1,9 @@
+
+T16728.hs:8:37: warning: [-Wpartial-type-signatures (in -Wdefault)]
+ • Found type wildcard ‘_’ standing for ‘k’
+ Where: ‘k’ is a rigid type variable bound by
+ the inferred type of f :: Proxy x
+ at T16728.hs:9:1-9
+ • In the kind ‘_’
+ In the first argument of ‘Proxy’, namely ‘(x :: _)’
+ In the type ‘Proxy (x :: _)’
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728a.hs b/testsuite/tests/partial-sigs/should_compile/T16728a.hs
new file mode 100644
index 000000000000..96d693a192cb
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16728a.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE ExplicitForAll, PartialTypeSignatures #-}
+module Bug where
+
+g,h:: forall a. a -> _
+g x = h x
+
+h x = g x
+
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728a.stderr b/testsuite/tests/partial-sigs/should_compile/T16728a.stderr
new file mode 100644
index 000000000000..50785ebc1ce2
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16728a.stderr
@@ -0,0 +1,20 @@
+
+T16728a.hs:4:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
+ • Found type wildcard ‘_’ standing for ‘_’
+ Where: ‘_’ is a rigid type variable bound by
+ the inferred types of
+ g :: a -> _
+ h :: a -> _
+ at T16728a.hs:(5,1)-(7,9)
+ • In the type ‘a -> _’
+ In the type signature: g :: forall a. a -> _
+
+T16728a.hs:4:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
+ • Found type wildcard ‘_’ standing for ‘_’
+ Where: ‘_’ is a rigid type variable bound by
+ the inferred types of
+ g :: a -> _
+ h :: a -> _
+ at T16728a.hs:(5,1)-(7,9)
+ • In the type ‘a -> _’
+ In the type signature: h :: forall a. a -> _
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728b.hs b/testsuite/tests/partial-sigs/should_compile/T16728b.hs
new file mode 100644
index 000000000000..db1e564a1416
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16728b.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE ExplicitForAll, PartialTypeSignatures #-}
+module Bug where
+
+g,h:: forall a. a -> _
+
+g x = x -- Instantiates the wildcard to 'a'
+
+h x = True -- Instantiates the wildcard to Bool
+
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728b.stderr b/testsuite/tests/partial-sigs/should_compile/T16728b.stderr
new file mode 100644
index 000000000000..712acfe0b931
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16728b.stderr
@@ -0,0 +1,13 @@
+
+T16728b.hs:4:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
+ • Found type wildcard ‘_’ standing for ‘Bool’
+ • In the type ‘a -> _’
+ In the type signature: h :: forall a. a -> _
+
+T16728b.hs:4:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
+ • Found type wildcard ‘_’ standing for ‘a’
+ Where: ‘a’ is a rigid type variable bound by
+ the inferred type of g :: a -> a
+ at T16728b.hs:6:1-7
+ • In the type ‘a -> _’
+ In the type signature: g :: forall a. a -> _
diff --git a/testsuite/tests/partial-sigs/should_compile/all.T b/testsuite/tests/partial-sigs/should_compile/all.T
index 56d821eca001..4cb12ed14437 100644
--- a/testsuite/tests/partial-sigs/should_compile/all.T
+++ b/testsuite/tests/partial-sigs/should_compile/all.T
@@ -92,3 +92,6 @@ test('T15039c', normal, compile, ['-fprint-equality-relations'])
test('T15039d', normal, compile,
['-fprint-explicit-kinds -fprint-equality-relations'])
test('T16334', normal, compile, [''])
+test('T16728', normal, compile, [''])
+test('T16728a', normal, compile, [''])
+test('T16728b', normal, compile, [''])
diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
index 0a07f0590d18..24782235ba78 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
@@ -1,10 +1,10 @@
T14040a.hs:34:8: error:
- • Cannot apply expression of type ‘Sing wl0
- -> (forall y. p0 _0 'WeirdNil)
+ • Cannot apply expression of type ‘Sing wl
+ -> (forall y. p _2 'WeirdNil)
-> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
- Sing x -> Sing xs -> p0 _1 xs -> p0 _2 ('WeirdCons x xs))
- -> p0 _3 wl0’
+ Sing x -> Sing xs -> p _0 xs -> p _1 ('WeirdCons x xs))
+ -> p _2 wl’
to a visible type argument ‘(WeirdList z)’
• In the sixth argument of ‘pWeirdCons’, namely
‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
--
GitLab