[Git][ghc/ghc][master] 3 commits: Fix two places that failed the substitution invariant
Marge Bot
gitlab at gitlab.haskell.org
Thu Jun 20 02:15:50 UTC 2019
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
3c9b57b0 by Simon Peyton Jones at 2019-06-20T02:15:39Z
Fix two places that failed the substitution invariant
The substition invariant relies on keeping the in-scope
set in sync, and we weren't always doing so, which means that
a DEBUG compiler crashes sometimes with an assertion failure
This patch fixes a couple more cases. Still not validate
clean (with -DEEBUG) but closer!
- - - - -
48fb3482 by Simon Peyton Jones at 2019-06-20T02:15:39Z
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.
- - - - -
3ae23992 by Simon Peyton Jones at 2019-06-20T02:15:39Z
Comments and tiny refactor
* Added Note [Quantified varaibles in partial type signatures]
in TcRnTypes
* Kill dVarSetElemsWellScoped; it was only called in
one function, quantifyTyVars. I inlined it because it
was only scopedSort . dVarSetElems
* Kill Type.tyCoVarsOfBindersWellScoped, never called.
- - - - -
21 changed files:
- compiler/rename/RnTypes.hs
- compiler/typecheck/Inst.hs
- compiler/typecheck/TcBinds.hs
- compiler/typecheck/TcCanonical.hs
- compiler/typecheck/TcExpr.hs
- compiler/typecheck/TcHsType.hs
- compiler/typecheck/TcMType.hs
- compiler/typecheck/TcRnDriver.hs
- compiler/typecheck/TcRnMonad.hs
- compiler/typecheck/TcRnTypes.hs
- compiler/typecheck/TcSigs.hs
- compiler/typecheck/TcType.hs
- compiler/types/Type.hs
- + testsuite/tests/partial-sigs/should_compile/T16728.hs
- + testsuite/tests/partial-sigs/should_compile/T16728.stderr
- + testsuite/tests/partial-sigs/should_compile/T16728a.hs
- + testsuite/tests/partial-sigs/should_compile/T16728a.stderr
- + testsuite/tests/partial-sigs/should_compile/T16728b.hs
- + testsuite/tests/partial-sigs/should_compile/T16728b.stderr
- testsuite/tests/partial-sigs/should_compile/all.T
- testsuite/tests/partial-sigs/should_fail/T14040a.stderr
Changes:
=====================================
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"
=====================================
compiler/typecheck/Inst.hs
=====================================
@@ -297,24 +297,23 @@ instTyVarsWith :: CtOrigin -> [TyVar] -> [TcType] -> TcM TCvSubst
-- If they don't match, emit a kind-equality to promise that they will
-- eventually do so, and thus make a kind-homongeneous substitution.
instTyVarsWith orig tvs tys
- = go empty_subst tvs tys
+ = go emptyTCvSubst tvs tys
where
- empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfTypes tys))
-
go subst [] []
= return subst
go subst (tv:tvs) (ty:tys)
| tv_kind `tcEqType` ty_kind
- = go (extendTCvSubst subst tv ty) tvs tys
+ = go (extendTvSubstAndInScope subst tv ty) tvs tys
| otherwise
= do { co <- emitWantedEq orig KindLevel Nominal ty_kind tv_kind
- ; go (extendTCvSubst subst tv (ty `mkCastTy` co)) tvs tys }
+ ; go (extendTvSubstAndInScope subst tv (ty `mkCastTy` co)) tvs tys }
where
tv_kind = substTy subst (tyVarKind tv)
ty_kind = tcTypeKind ty
go _ _ _ = pprPanic "instTysWith" (ppr tvs $$ ppr tys)
+
{-
************************************************************************
* *
=====================================
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)
=====================================
compiler/typecheck/TcCanonical.hs
=====================================
@@ -1007,8 +1007,10 @@ can_eq_nc_forall ev eq_rel s1 s2
= do { let tv2 = binderVar bndr2
; (kind_co, wanteds1) <- unify loc Nominal (tyVarKind skol_tv)
(substTy subst (tyVarKind tv2))
- ; let subst' = extendTvSubst subst 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 ) }
=====================================
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)
=====================================
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
+ at _ 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.
=====================================
compiler/typecheck/TcMType.hs
=====================================
@@ -1433,9 +1433,9 @@ quantifyTyVars gbl_tvs
-- NB: All variables in the kind of a covar must not be
-- quantified over, as we don't quantify over the covar.
- dep_kvs = dVarSetElemsWellScoped $
+ dep_kvs = scopedSort $ dVarSetElems $
dep_tkvs `dVarSetMinusVarSet` mono_tvs
- -- dVarSetElemsWellScoped: put the kind variables into
+ -- scopedSort: put the kind variables into
-- well-scoped order.
-- E.g. [k, (a::k)] not the other way roud
@@ -1453,7 +1453,7 @@ quantifyTyVars gbl_tvs
-- This block uses level numbers to decide what to quantify
-- and emits a warning if the two methods do not give the same answer
- ; let dep_kvs2 = dVarSetElemsWellScoped $
+ ; let dep_kvs2 = scopedSort $ dVarSetElems $
filterDVarSet (quantifiableTv outer_tclvl) dep_tkvs
nondep_tvs2 = filter (quantifiableTv outer_tclvl) $
dVarSetElems (nondep_tkvs `minusDVarSet` dep_tkvs)
=====================================
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]
=====================================
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
=====================================
compiler/typecheck/TcRnTypes.hs
=====================================
@@ -1542,6 +1542,10 @@ data TcIdSigInst
-- No need to keep track of whether they are truly lexically
-- scoped because the renamer has named them uniquely
-- See Note [Binding scoped type variables] in TcSigs
+ --
+ -- NB: The order of sig_inst_skols is irrelevant
+ -- for a CompleteSig, but for a PartialSig see
+ -- Note [Quantified varaibles in partial type signatures]
, sig_inst_theta :: TcThetaType
-- Instantiated theta. In the case of a
@@ -1553,15 +1557,15 @@ data TcIdSigInst
-- Relevant for partial signature only
, sig_inst_wcs :: [(Name, TcTyVar)]
- -- Like sig_inst_skols, but for wildcards. The named
- -- wildcards scope over the binding, and hence their
- -- Names may appear in type signatures in the binding
+ -- Like sig_inst_skols, but for /named/ wildcards (_a etc).
+ -- The named wildcards scope over the binding, and hence
+ -- their Names may appear in type signatures in the binding
, sig_inst_wcx :: Maybe TcType
-- 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]
@@ -1572,6 +1576,26 @@ if the original function had a signature like
But that's ok: tcMatchesFun (called by tcRhs) can deal with that
It happens, too! See Note [Polymorphic methods] in TcClassDcl.
+Note [Quantified varaibles in partial type signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ f :: forall a b. _ -> a -> _ -> b
+ f (x,y) p q = q
+
+Then we expect f's final type to be
+ f :: forall {x,y}. forall a b. (x,y) -> a -> b -> b
+
+Note that x,y are Inferred, and can't be use for visible type
+application (VTA). But a,b are Specified, and remain Specified
+in the final type, so we can use VTA for them. (Exception: if
+it turns out that a's kind mentions b we need to reorder them
+with scopedSort.)
+
+The sig_inst_skols of the TISI from a partial signature records
+that original order, and is used to get the variables of f's
+final type in the correct order.
+
+
Note [Wildcards in partial signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The wildcards in psig_wcs may stand for a type mentioning
=====================================
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 }
=====================================
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?
=====================================
compiler/types/Type.hs
=====================================
@@ -158,8 +158,8 @@ module Type (
typeSize, occCheckExpand,
-- * Well-scoped lists of variables
- dVarSetElemsWellScoped, scopedSort, tyCoVarsOfTypeWellScoped,
- tyCoVarsOfTypesWellScoped, tyCoVarsOfBindersWellScoped,
+ scopedSort, tyCoVarsOfTypeWellScoped,
+ tyCoVarsOfTypesWellScoped,
-- * Type comparison
eqType, eqTypeX, eqTypes, nonDetCmpType, nonDetCmpTypes, nonDetCmpTypeX,
@@ -250,7 +250,7 @@ import UniqSet
import Class
import TyCon
import TysPrim
-import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind, unitTy
+import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind
, typeSymbolKind, liftedTypeKind
, constraintKind )
import PrelNames
@@ -2199,15 +2199,6 @@ scopedSort = go [] []
-- lists not in correspondence
insert _ _ _ = panic "scopedSort"
--- | Extract a well-scoped list of variables from a deterministic set of
--- variables. The result is deterministic.
--- NB: There used to exist varSetElemsWellScoped :: VarSet -> [Var] which
--- took a non-deterministic set and produced a non-deterministic
--- well-scoped list. If you care about the list being well-scoped you also
--- most likely care about it being in deterministic order.
-dVarSetElemsWellScoped :: DVarSet -> [Var]
-dVarSetElemsWellScoped = scopedSort . dVarSetElems
-
-- | Get the free vars of a type in scoped order
tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList
@@ -2216,12 +2207,6 @@ tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList
tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList
--- | Given the suffix of a telescope, returns the prefix.
--- Ex: given [(k :: j), (a :: Proxy k)], returns [(j :: *)].
-tyCoVarsOfBindersWellScoped :: [TyVar] -> [TyVar]
-tyCoVarsOfBindersWellScoped tvs
- = tyCoVarsOfTypeWellScoped (mkInvForAllTys tvs unitTy)
-
------------- Closing over kinds -----------------
-- | Add the kind variables free in the kinds of the tyvars in the given set.
=====================================
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
=====================================
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 :: _)’
=====================================
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
+
=====================================
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 -> _
=====================================
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
+
=====================================
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 -> _
=====================================
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, [''])
=====================================
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)’
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/compare/39c758e1426c9e5b00de2207ad53bb4377c1e6a6...3ae23992786c7ea3211ab6f13e1d61a5edfe5952
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/compare/39c758e1426c9e5b00de2207ad53bb4377c1e6a6...3ae23992786c7ea3211ab6f13e1d61a5edfe5952
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/20190619/c7fb88bf/attachment-0001.html>
More information about the ghc-commits
mailing list