Commit c955a514 authored by Richard Eisenberg's avatar Richard Eisenberg

Remove decideKindGeneralisationPlan

TypeInType came with a new function: decideKindGeneralisationPlan.
This type-level counterpart to the term-level decideGeneralisationPlan
chose whether or not a kind should be generalized. The thinking was
that if `let` should not be generalized, then kinds shouldn't either
(under the same circumstances around -XMonoLocalBinds).

However, this is too conservative -- the situation described in the
motivation for "let should be be generalized" does not occur in types.

This commit thus removes decideKindGeneralisationPlan, always
generalizing.

One consequence is that tc_hs_sig_type_and_gen no longer calls
solveEqualities, which reports all unsolved constraints, instead
relying on the solveLocalEqualities in tcImplicitTKBndrs. An effect
of this is that reporing kind errors gets delayed more frequently.
This seems to be a net benefit in error reporting; often, alongside
a kind error, the type error is now reported (and users might find
type errors easier to understand).

Some of these errors ended up at the top level, where it was
discovered that the GlobalRdrEnv containing the definitions in the
local module was not in the TcGblEnv, and thus errors were reported
with qualified names unnecessarily. This commit rejiggers some of
the logic around captureTopConstraints accordingly.

One error message (typecheck/should_fail/T1633)
is a regression, mentioning the name of a default method. However,
that problem is already reported as #10087, its solution is far from
clear, and so I'm not addressing it here.

This commit fixes #15141. As it's an internal refactor, there is
no concrete test case for it.

Along the way, we no longer need the hsib_closed field of
HsImplicitBndrs (it was used only in decideKindGeneralisationPlan)
and so it's been removed, simplifying the datatype structure.

Along the way, I removed code in the validity checker that looks
at coercions. This isn't related to this patch, really (though
it was, at one point), but it's an improvement, so I kept it.

This updates the haddock submodule.
parent c50574a8
......@@ -204,7 +204,7 @@ get_scoped_tvs (L _ signature)
-- Both implicit and explicit quantified variables
-- We need the implicit ones for f :: forall (a::k). blah
-- here 'k' scopes too
| HsIB { hsib_ext = HsIBRn { hsib_vars = implicit_vars }
| HsIB { hsib_ext = implicit_vars
, hsib_body = hs_ty } <- sig
, (explicit_vars, _) <- splitLHsForAllTy hs_ty
= implicit_vars ++ map hsLTyVarName explicit_vars
......@@ -544,7 +544,7 @@ repTyFamInstD decl@(TyFamInstDecl { tfid_eqn = eqn })
; repTySynInst tc eqn1 }
repTyFamEqn :: TyFamInstEqn GhcRn -> DsM (Core TH.TySynEqnQ)
repTyFamEqn (HsIB { hsib_ext = HsIBRn { hsib_vars = var_names }
repTyFamEqn (HsIB { hsib_ext = var_names
, hsib_body = FamEqn { feqn_pats = tys
, feqn_rhs = rhs }})
= do { let hs_tvs = HsQTvs { hsq_ext = HsQTvsRn
......@@ -561,7 +561,7 @@ repTyFamEqn (HsIB _ (XFamEqn _)) = panic "repTyFamEqn"
repDataFamInstD :: DataFamInstDecl GhcRn -> DsM (Core TH.DecQ)
repDataFamInstD (DataFamInstDecl { dfid_eqn =
(HsIB { hsib_ext = HsIBRn { hsib_vars = var_names }
(HsIB { hsib_ext = var_names
, hsib_body = FamEqn { feqn_tycon = tc_name
, feqn_pats = tys
, feqn_rhs = defn }})})
......@@ -651,7 +651,7 @@ repRuleD (L _ (XRuleDecl _)) = panic "repRuleD"
ruleBndrNames :: LRuleBndr GhcRn -> [Name]
ruleBndrNames (L _ (RuleBndr _ n)) = [unLoc n]
ruleBndrNames (L _ (RuleBndrSig _ n sig))
| HsWC { hswc_body = HsIB { hsib_ext = HsIBRn { hsib_vars = vars } }} <- sig
| HsWC { hswc_body = HsIB { hsib_ext = vars }} <- sig
= unLoc n : vars
ruleBndrNames (L _ (RuleBndrSig _ _ (HsWC _ (XHsImplicitBndrs _))))
= panic "ruleBndrNames"
......@@ -1042,7 +1042,7 @@ repContext ctxt = do preds <- repList typeQTyConName repLTy ctxt
repCtxt preds
repHsSigType :: LHsSigType GhcRn -> DsM (Core TH.TypeQ)
repHsSigType (HsIB { hsib_ext = HsIBRn { hsib_vars = implicit_tvs }
repHsSigType (HsIB { hsib_ext = implicit_tvs
, hsib_body = body })
| (explicit_tvs, ctxt, ty) <- splitLHsSigmaTy body
= addSimpleTyVarBinds implicit_tvs $
......
......@@ -20,7 +20,7 @@ module HsTypes (
HsType(..), NewHsTypeX(..), LHsType, HsKind, LHsKind,
HsTyVarBndr(..), LHsTyVarBndr,
LHsQTyVars(..), HsQTvsRn(..),
HsImplicitBndrs(..), HsIBRn(..),
HsImplicitBndrs(..),
HsWildCardBndrs(..),
LHsSigType, LHsSigWcType, LHsWcType,
HsTupleSort(..),
......@@ -332,23 +332,18 @@ isEmptyLHsQTvs _ = False
-- | Haskell Implicit Binders
data HsImplicitBndrs pass thing -- See Note [HsType binders]
= HsIB { hsib_ext :: XHsIB pass thing
= HsIB { hsib_ext :: XHsIB pass thing -- after renamer: [Name]
-- Implicitly-bound kind & type vars
-- Order is important; see
-- Note [Ordering of implicit variables]
, hsib_body :: thing -- Main payload (type or list of types)
}
| XHsImplicitBndrs (XXHsImplicitBndrs pass thing)
data HsIBRn
= HsIBRn { hsib_vars :: [Name] -- Implicitly-bound kind & type vars
-- Order is important; see
-- Note [Ordering of implicit variables]
, hsib_closed :: Bool -- Taking the hsib_vars into account,
-- is the payload closed? Used in
-- TcHsType.decideKindGeneralisationPlan
} deriving Data
type instance XHsIB GhcPs _ = NoExt
type instance XHsIB GhcRn _ = HsIBRn
type instance XHsIB GhcTc _ = HsIBRn
type instance XHsIB GhcRn _ = [Name]
type instance XHsIB GhcTc _ = [Name]
type instance XXHsImplicitBndrs (GhcPass _) _ = NoExt
......@@ -429,9 +424,7 @@ mkHsWildCardBndrs x = HsWC { hswc_body = x
-- Add empty binders. This is a bit suspicious; what if
-- the wrapped thing had free type variables?
mkEmptyImplicitBndrs :: thing -> HsImplicitBndrs GhcRn thing
mkEmptyImplicitBndrs x = HsIB { hsib_ext = HsIBRn
{ hsib_vars = []
, hsib_closed = False }
mkEmptyImplicitBndrs x = HsIB { hsib_ext = []
, hsib_body = x }
mkEmptyWildCardBndrs :: thing -> HsWildCardBndrs GhcRn thing
......@@ -928,7 +921,7 @@ hsWcScopedTvs :: LHsSigWcType GhcRn -> [Name]
-- because they scope in the same way
hsWcScopedTvs sig_ty
| HsWC { hswc_ext = nwcs, hswc_body = sig_ty1 } <- sig_ty
, HsIB { hsib_ext = HsIBRn { hsib_vars = vars}
, HsIB { hsib_ext = vars
, hsib_body = sig_ty2 } <- sig_ty1
= case sig_ty2 of
L _ (HsForAllTy { hst_bndrs = tvs }) -> vars ++ nwcs ++
......@@ -942,7 +935,7 @@ hsWcScopedTvs (XHsWildCardBndrs _) = panic "hsWcScopedTvs"
hsScopedTvs :: LHsSigType GhcRn -> [Name]
-- Same as hsWcScopedTvs, but for a LHsSigType
hsScopedTvs sig_ty
| HsIB { hsib_ext = HsIBRn { hsib_vars = vars }
| HsIB { hsib_ext = vars
, hsib_body = sig_ty2 } <- sig_ty
, L _ (HsForAllTy { hst_bndrs = tvs }) <- sig_ty2
= vars ++ map hsLTyVarName tvs
......@@ -1132,7 +1125,7 @@ splitLHsQualTy body = (noLoc [], body)
splitLHsInstDeclTy :: LHsSigType GhcRn
-> ([Name], LHsContext GhcRn, LHsType GhcRn)
-- Split up an instance decl type, returning the pieces
splitLHsInstDeclTy (HsIB { hsib_ext = HsIBRn { hsib_vars = itkvs }
splitLHsInstDeclTy (HsIB { hsib_ext = itkvs
, hsib_body = inst_ty })
| (tvs, cxt, body_ty) <- splitLHsSigmaTy inst_ty
= (itkvs ++ map hsLTyVarName tvs, cxt, body_ty)
......
......@@ -765,8 +765,7 @@ rnFamInstEqn doc mb_cls rhs_kvars
all_fvs = fvs `addOneFV` unLoc tycon'
-- type instance => use, hence addOneFV
; return (HsIB { hsib_ext = HsIBRn { hsib_vars = all_ibs
, hsib_closed = True }
; return (HsIB { hsib_ext = all_ibs
, hsib_body
= FamEqn { feqn_ext = noExt
, feqn_tycon = tycon'
......@@ -1691,7 +1690,7 @@ rnLDerivStrategy doc mds thing_inside
NewtypeStrategy -> boring_case (L loc NewtypeStrategy)
ViaStrategy via_ty ->
do (via_ty', fvs1) <- rnHsSigType doc via_ty
let HsIB { hsib_ext = HsIBRn { hsib_vars = via_imp_tvs }
let HsIB { hsib_ext = via_imp_tvs
, hsib_body = via_body } = via_ty'
(via_exp_tv_bndrs, _, _) = splitLHsSigmaTy via_body
via_exp_tvs = map hsLTyVarName via_exp_tv_bndrs
......
......@@ -127,7 +127,8 @@ rn_hs_sig_wc_type always_bind_free_tvs ctxt
; rnImplicitBndrs bind_free_tvs tv_rdrs $ \ vars ->
do { (wcs, hs_ty', fvs1) <- rnWcBody ctxt nwc_rdrs hs_ty
; let sig_ty' = HsWC { hswc_ext = wcs, hswc_body = ib_ty' }
ib_ty' = mk_implicit_bndrs vars hs_ty' fvs1
ib_ty' = HsIB { hsib_ext = vars
, hsib_body = hs_ty' }
; (res, fvs2) <- thing_inside sig_ty'
; return (res, fvs1 `plusFV` fvs2) } }
rn_hs_sig_wc_type _ _ (HsWC _ (XHsImplicitBndrs _)) _
......@@ -300,7 +301,9 @@ rnHsSigType ctx (HsIB { hsib_body = hs_ty })
; vars <- extractFilteredRdrTyVarsDups hs_ty
; rnImplicitBndrs (not (isLHsForAllTy hs_ty)) vars $ \ vars ->
do { (body', fvs) <- rnLHsType ctx hs_ty
; return ( mk_implicit_bndrs vars body' fvs, fvs ) } }
; return ( HsIB { hsib_ext = vars
, hsib_body = body' }
, fvs ) } }
rnHsSigType _ (XHsImplicitBndrs _) = panic "rnHsSigType"
rnImplicitBndrs :: Bool -- True <=> bring into scope any free type variables
......@@ -367,18 +370,6 @@ rnLHsInstType :: SDoc -> LHsSigType GhcPs -> RnM (LHsSigType GhcRn, FreeVars)
-- Do not try to decompose the inst_ty in case it is malformed
rnLHsInstType doc inst_ty = rnHsSigType (GenericCtx doc) inst_ty
mk_implicit_bndrs :: [Name] -- implicitly bound
-> a -- payload
-> FreeVars -- FreeVars of payload
-> HsImplicitBndrs GhcRn a
mk_implicit_bndrs vars body fvs
= HsIB { hsib_ext = HsIBRn
{ hsib_vars = vars
, hsib_closed = nameSetAll (not . isTyVarName) (vars `delFVs` fvs) }
, hsib_body = body }
{- ******************************************************
* *
LHsType and HsType
......
......@@ -713,17 +713,14 @@ tcStandaloneDerivInstType
:: UserTypeCtxt -> LHsSigWcType GhcRn
-> TcM ([TyVar], DerivContext, Class, [Type])
tcStandaloneDerivInstType ctxt
(HsWC { hswc_body = deriv_ty@(HsIB { hsib_ext = HsIBRn
{ hsib_vars = vars
, hsib_closed = closed }
(HsWC { hswc_body = deriv_ty@(HsIB { hsib_ext = vars
, hsib_body = deriv_ty_body })})
| (tvs, theta, rho) <- splitLHsSigmaTy deriv_ty_body
, L _ [wc_pred] <- theta
, L _ (HsWildCardTy (AnonWildCard (L wc_span _))) <- ignoreParens wc_pred
= do (deriv_tvs, _deriv_theta, deriv_cls, deriv_inst_tys)
<- tcHsClsInstType ctxt $
HsIB { hsib_ext = HsIBRn { hsib_vars = vars
, hsib_closed = closed }
HsIB { hsib_ext = vars
, hsib_body
= L (getLoc deriv_ty_body) $
HsForAllTy { hst_bndrs = tvs
......
......@@ -614,8 +614,10 @@ tcExtendLocalTypeEnv lcl_env@(TcLclEnv { tcl_env = lcl_type_env }) tc_ty_things
tvs
_other -> tvs `unionVarSet` id_tvs
where
id_tvs = tyCoVarsOfType (idType id)
is_closed_type = not (anyVarSet isTyVar id_tvs)
id_ty = idType id
id_tvs = tyCoVarsOfType id_ty
id_co_tvs = closeOverKinds (coVarsOfType id_ty)
is_closed_type = not (anyVarSet isTyVar (id_tvs `minusVarSet` id_co_tvs))
-- We only care about being closed wrt /type/ variables
-- E.g. a top-level binding might have a type like
-- foo :: t |> co
......
This diff is collapsed.
......@@ -588,9 +588,8 @@ tcDataFamInstDecl :: Maybe ClsInstInfo
-> LDataFamInstDecl GhcRn -> TcM (FamInst, Maybe DerivInfo)
-- "newtype instance" and "data instance"
tcDataFamInstDecl mb_clsinfo
(L loc decl@(DataFamInstDecl { dfid_eqn = HsIB { hsib_ext
= HsIBRn { hsib_vars = tv_names }
, hsib_body =
(L loc decl@(DataFamInstDecl { dfid_eqn = HsIB { hsib_ext = tv_names
, hsib_body =
FamEqn { feqn_pats = pats
, feqn_tycon = fam_tc_name
, feqn_fixity = fixity
......
......@@ -1307,6 +1307,8 @@ a \/\a in the final result but all the occurrences of a will be zonked to ()
-- variables free in anything (term-level or type-level) in scope. We thus
-- don't have to worry about clashes with things that are not in scope, because
-- if they are reachable, then they'll be returned here.
-- NB: This is closed over kinds, so it can return unification variables mentioned
-- in the kinds of in-scope tyvars.
tcGetGlobalTyCoVars :: TcM TcTyVarSet
tcGetGlobalTyCoVars
= do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
......
......@@ -391,14 +391,14 @@ tcRnSrcDecls :: Bool -- False => no 'module M(..) where' header at all
-> TcM TcGblEnv
tcRnSrcDecls explicit_mod_hdr decls
= do { -- Do all the declarations
; ((tcg_env, tcl_env), lie) <- captureTopConstraints $
do { (tcg_env, tcl_env) <- tc_rn_src_decls decls
; (tcg_env, tcl_env, lie) <- tc_rn_src_decls decls
-- Check for the 'main' declaration
-- Must do this inside the captureTopConstraints
; tcg_env <- setEnvs (tcg_env, tcl_env) $
checkMain explicit_mod_hdr
; return (tcg_env, tcl_env) }
-- Check for the 'main' declaration
-- Must do this inside the captureTopConstraints
; (tcg_env, lie_main) <- setEnvs (tcg_env, tcl_env) $
-- always set envs *before* captureTopConstraints
captureTopConstraints $
checkMain explicit_mod_hdr
; setEnvs (tcg_env, tcl_env) $ do {
......@@ -412,7 +412,7 @@ tcRnSrcDecls explicit_mod_hdr decls
-- * the local env exposes the local Ids to simplifyTop,
-- so that we get better error messages (monomorphism restriction)
; new_ev_binds <- {-# SCC "simplifyTop" #-}
simplifyTop lie
simplifyTop (lie `andWC` lie_main)
-- Emit Typeable bindings
; tcg_env <- mkTypeableBinds
......@@ -470,16 +470,17 @@ run_th_modfinalizers = do
then getEnvs
else do
writeTcRef th_modfinalizers_var []
(envs, lie) <- captureTopConstraints $ do
sequence_ th_modfinalizers
-- Finalizers can add top-level declarations with addTopDecls.
tc_rn_src_decls []
setEnvs envs $ do
(_, lie_th) <- captureTopConstraints $
sequence_ th_modfinalizers
-- Finalizers can add top-level declarations with addTopDecls, so
-- we have to run tc_rn_src_decls to get them
(tcg_env, tcl_env, lie_top_decls) <- tc_rn_src_decls []
setEnvs (tcg_env, tcl_env) $ do
-- Subsequent rounds of finalizers run after any new constraints are
-- simplified, or some types might not be complete when using reify
-- (see #12777).
new_ev_binds <- {-# SCC "simplifyTop2" #-}
simplifyTop lie
simplifyTop (lie_th `andWC` lie_top_decls)
updGblEnv (\tcg_env ->
tcg_env { tcg_ev_binds = tcg_ev_binds tcg_env `unionBags` new_ev_binds }
)
......@@ -487,9 +488,10 @@ run_th_modfinalizers = do
run_th_modfinalizers
tc_rn_src_decls :: [LHsDecl GhcPs]
-> TcM (TcGblEnv, TcLclEnv)
-> TcM (TcGblEnv, TcLclEnv, WantedConstraints)
-- Loops around dealing with each top level inter-splice group
-- in turn, until it's dealt with the entire module
-- Never emits constraints; calls captureTopConstraints internally
tc_rn_src_decls ds
= {-# SCC "tc_rn_src_decls" #-}
do { (first_group, group_tail) <- findSplice ds
......@@ -534,13 +536,17 @@ tc_rn_src_decls ds
}
-- Type check all declarations
; (tcg_env, tcl_env) <- setGblEnv tcg_env $
tcTopSrcDecls rn_decls
-- NB: set the env **before** captureTopConstraints so that error messages
-- get reported w.r.t. the right GlobalRdrEnv. It is for this reason that
-- the captureTopConstraints must go here, not in tcRnSrcDecls.
; ((tcg_env, tcl_env), lie1) <- setGblEnv tcg_env $
captureTopConstraints $
tcTopSrcDecls rn_decls
-- If there is no splice, we're nearly done
; setEnvs (tcg_env, tcl_env) $
case group_tail of
{ Nothing -> return (tcg_env, tcl_env)
{ Nothing -> return (tcg_env, tcl_env, lie1)
-- If there's a splice, we must carry on
; Just (SpliceDecl _ (L loc splice) _, rest_ds) ->
......@@ -551,8 +557,11 @@ tc_rn_src_decls ds
splice)
-- Glue them on the front of the remaining decls and loop
; setGblEnv (tcg_env `addTcgDUs` usesOnly splice_fvs) $
tc_rn_src_decls (spliced_decls ++ rest_ds)
; (tcg_env, tcl_env, lie2) <-
setGblEnv (tcg_env `addTcgDUs` usesOnly splice_fvs) $
tc_rn_src_decls (spliced_decls ++ rest_ds)
; return (tcg_env, tcl_env, lie1 `andWC` lie2)
}
; Just (XSpliceDecl _, _) -> panic "tc_rn_src_decls"
}
......@@ -583,8 +592,9 @@ tcRnHsBootDecls hsc_src decls
<- rnTopSrcDecls first_group
-- The empty list is for extra dependencies coming from .hs-boot files
-- See Note [Extra dependencies from .hs-boot files] in RnSource
; (gbl_env, lie) <- captureTopConstraints $ setGblEnv tcg_env $ do {
; (gbl_env, lie) <- setGblEnv tcg_env $ captureTopConstraints $ do {
-- NB: setGblEnv **before** captureTopConstraints so that
-- if the latter reports errors, it knows what's in scope
-- Check for illegal declarations
; case group_tail of
......
......@@ -303,12 +303,12 @@ tcPatSynSig :: Name -> LHsSigType GhcRn -> TcM TcPatSynInfo
-- See Note [Pattern synonym signatures]
-- See Note [Recipe for checking a signature] in TcHsType
tcPatSynSig name sig_ty
| HsIB { hsib_ext = HsIBRn { hsib_vars = implicit_hs_tvs }
| HsIB { hsib_ext = implicit_hs_tvs
, hsib_body = hs_ty } <- sig_ty
, (univ_hs_tvs, hs_req, hs_ty1) <- splitLHsSigmaTy hs_ty
, (ex_hs_tvs, hs_prov, hs_body_ty) <- splitLHsSigmaTy hs_ty1
= do { (implicit_tvs, (univ_tvs, (ex_tvs, (req, prov, body_ty))))
<- -- NB: tcImplicitTKBndrs calls solveEqualities
<- -- NB: tcImplicitTKBndrs calls solveLocalEqualities
tcImplicitTKBndrs skol_info implicit_hs_tvs $
tcExplicitTKBndrs skol_info univ_hs_tvs $
tcExplicitTKBndrs skol_info ex_hs_tvs $
......@@ -319,9 +319,8 @@ tcPatSynSig name sig_ty
-- e.g. pattern Zero <- 0# (Trac #12094)
; return (req, prov, body_ty) }
; ungen_patsyn_ty <- zonkPromoteType $
build_patsyn_type [] implicit_tvs univ_tvs req
ex_tvs prov body_ty
; let ungen_patsyn_ty = build_patsyn_type [] implicit_tvs univ_tvs req
ex_tvs prov body_ty
-- Kind generalisation
; kvs <- kindGeneralize ungen_patsyn_ty
......
......@@ -5,12 +5,14 @@ module TcSimplify(
growThetaTyVars,
simplifyAmbiguityCheck,
simplifyDefault,
simplifyTop, simplifyTopImplic, captureTopConstraints,
simplifyTop, simplifyTopImplic,
simplifyInteractive,
solveEqualities, solveLocalEqualities,
simplifyWantedsTcM,
tcCheckSatisfiability,
captureTopConstraints,
simpl_top,
promoteTyVar,
......@@ -76,6 +78,8 @@ captureTopConstraints :: TcM a -> TcM (a, WantedConstraints)
-- generates plus the constraints produced by static forms inside.
-- If it fails with an exception, it reports any insolubles
-- (out of scope variables) before doing so
-- NB: bring any environments into scope before calling this, so that
-- the reportUnsolved has access to the most complete GlobalRdrEnv
captureTopConstraints thing_inside
= do { static_wc_var <- TcM.newTcRef emptyWC ;
; (mb_res, lie) <- TcM.updGblEnv (\env -> env { tcg_static_wc = static_wc_var } ) $
......@@ -1027,7 +1031,7 @@ defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
= do { -- Promote any tyvars that we cannot generalise
-- See Note [Promote momomorphic tyvars]
; traceTc "decideMonoTyVars: promotion:" (ppr mono_tvs)
; prom <- promoteTyVarSet mono_tvs
; (prom, _) <- promoteTyVarSet mono_tvs
-- Default any kind/levity vars
; let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
......@@ -1909,10 +1913,11 @@ we'll get more Givens (a unification is like adding a Given) to
allow the implication to make progress.
-}
promoteTyVar :: TcTyVar -> TcM Bool
promoteTyVar :: TcTyVar -> TcM (Bool, TcTyVar)
-- When we float a constraint out of an implication we must restore
-- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in TcType
-- Return True <=> we did some promotion
-- Also returns either the original tyvar (no promotion) or the new one
-- See Note [Promoting unification variables]
promoteTyVar tv
= do { tclvl <- TcM.getTcLevel
......@@ -1920,14 +1925,16 @@ promoteTyVar tv
then do { cloned_tv <- TcM.cloneMetaTyVar tv
; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv)
; return True }
else return False }
; return (True, rhs_tv) }
else return (False, tv) }
-- Returns whether or not *any* tyvar is defaulted
promoteTyVarSet :: TcTyVarSet -> TcM Bool
promoteTyVarSet :: TcTyVarSet -> TcM (Bool, TcTyVarSet)
promoteTyVarSet tvs
= or <$> mapM promoteTyVar (nonDetEltsUniqSet tvs)
-- non-determinism is OK because order of promotion doesn't matter
= do { (bools, tyvars) <- mapAndUnzipM promoteTyVar (nonDetEltsUniqSet tvs)
-- non-determinism is OK because order of promotion doesn't matter
; return (or bools, mkVarSet tyvars) }
promoteTyVarTcS :: TcTyVar -> TcS ()
-- When we float a constraint out of an implication we must restore
......
......@@ -1180,7 +1180,7 @@ reifyInstances th_nm th_tys
do { (rn_ty, fvs) <- rnLHsType doc rdr_ty
; return ((tv_names, rn_ty), fvs) }
; (_tvs, ty)
<- solveEqualities $
<- failIfEmitsConstraints $ -- avoid error cascade if there are unsolved
tcImplicitTKBndrs ReifySkol tv_names $
fst <$> tcLHsType rn_ty
; ty <- zonkTcTypeToType emptyZonkEnv ty
......
......@@ -1399,7 +1399,7 @@ but it works.
-------------------------
kcTyFamInstEqn :: TcTyCon -> LTyFamInstEqn GhcRn -> TcM ()
kcTyFamInstEqn tc_fam_tc
(L loc (HsIB { hsib_ext = HsIBRn { hsib_vars = tv_names }
(L loc (HsIB { hsib_ext = tv_names
, hsib_body = FamEqn { feqn_tycon = L _ eqn_tc_name
, feqn_pats = pats
, feqn_rhs = hs_ty }}))
......@@ -1452,7 +1452,7 @@ tcTyFamInstEqn :: TcTyCon -> Maybe ClsInstInfo -> LTyFamInstEqn GhcRn
-- Needs to be here, not in TcInstDcls, because closed families
-- (typechecked here) have TyFamInstEqns
tcTyFamInstEqn fam_tc mb_clsinfo
(L loc (HsIB { hsib_ext = HsIBRn { hsib_vars = tv_names }
(L loc (HsIB { hsib_ext = tv_names
, hsib_body = FamEqn { feqn_tycon = L _ eqn_tc_name
, feqn_pats = pats
, feqn_rhs = hs_ty }}))
......@@ -1960,7 +1960,8 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
skol_info = DataConSkol name
; (imp_tvs, (exp_tvs, (ctxt, arg_tys, res_ty, field_lbls, stricts)))
<- solveEqualities $
<- failIfEmitsConstraints $ -- we won't get another crack, and we don't
-- want an error cascade
tcImplicitTKBndrs skol_info implicit_tkv_nms $
tcExplicitTKBndrs skol_info explicit_tkv_nms $
do { ctxt <- tcHsMbContext cxt
......
......@@ -2095,6 +2095,7 @@ checkValidTelescope tvbs user_tyvars extra
-}
-- Free variables of a type, retaining repetitions, and expanding synonyms
-- This ignores coercions, as coercions aren't user-written
fvType :: Type -> [TyCoVar]
fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
fvType (TyVarTy tv) = [tv]
......@@ -2105,42 +2106,12 @@ fvType (FunTy arg res) = fvType arg ++ fvType res
fvType (ForAllTy (TvBndr tv _) ty)
= fvType (tyVarKind tv) ++
filter (/= tv) (fvType ty)
fvType (CastTy ty co) = fvType ty ++ fvCo co
fvType (CoercionTy co) = fvCo co
fvType (CastTy ty _) = fvType ty
fvType (CoercionTy {}) = []
fvTypes :: [Type] -> [TyVar]
fvTypes tys = concat (map fvType tys)
fvMCo :: MCoercion -> [TyCoVar]
fvMCo MRefl = []
fvMCo (MCo co) = fvCo co
fvCo :: Coercion -> [TyCoVar]
fvCo (Refl ty) = fvType ty
fvCo (GRefl _ ty mco) = fvType ty ++ fvMCo mco
fvCo (TyConAppCo _ _ args) = concatMap fvCo args
fvCo (AppCo co arg) = fvCo co ++ fvCo arg
fvCo (ForAllCo tv h co) = filter (/= tv) (fvCo co) ++ fvCo h
fvCo (FunCo _ co1 co2) = fvCo co1 ++ fvCo co2
fvCo (CoVarCo v) = [v]
fvCo (AxiomInstCo _ _ args) = concatMap fvCo args
fvCo (UnivCo p _ t1 t2) = fvProv p ++ fvType t1 ++ fvType t2
fvCo (SymCo co) = fvCo co
fvCo (TransCo co1 co2) = fvCo co1 ++ fvCo co2
fvCo (NthCo _ _ co) = fvCo co
fvCo (LRCo _ co) = fvCo co
fvCo (InstCo co arg) = fvCo co ++ fvCo arg
fvCo (KindCo co) = fvCo co
fvCo (SubCo co) = fvCo co
fvCo (AxiomRuleCo _ cs) = concatMap fvCo cs
fvCo (HoleCo h) = pprPanic "fvCo falls into a hole" (ppr h)
fvProv :: UnivCoProvenance -> [TyCoVar]
fvProv UnsafeCoerceProv = []
fvProv (PhantomProv co) = fvCo co
fvProv (ProofIrrelProv co) = fvCo co
fvProv (PluginProv _) = []
sizeType :: Type -> Int
-- Size of a type: the number of variables and constructors
sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
......@@ -2151,7 +2122,7 @@ sizeType (AppTy fun arg) = sizeType fun + sizeType arg
sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
sizeType (ForAllTy _ ty) = sizeType ty
sizeType (CastTy ty _) = sizeType ty
sizeType (CoercionTy _) = 1
sizeType (CoercionTy _) = 0
sizeTypes :: [Type] -> Int
sizeTypes = foldr ((+) . sizeType) 0
......
......@@ -2247,6 +2247,34 @@ sym (ForAllCo tv h g)
==>
ForAllCo tv (sym h) (sym g[tv |-> tv |> sym h])
Note [Substituting in a coercion hole]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It seems highly suspicious to be substituting in a coercion that still
has coercion holes. Yet, this can happen in a situation like this:
f :: forall k. k :~: Type -> ()
f Refl = let x :: forall (a :: k). [a] -> ...
x = ...
When we check x's type signature, we require that k ~ Type. We indeed
know this due to the Refl pattern match, but the eager unifier can't
make use of givens. So, when we're done looking at x's type, a coercion
hole will remain. Then, when we're checking x's definition, we skolemise
x's type (in order to, e.g., bring the scoped type variable `a` into scope).
This requires performing a substitution for the fresh skolem variables.
This subsitution needs to affect the kind of the coercion hole, too --
otherwise, the kind will have an out-of-scope variable in it. More problematically
in practice (we won't actually notice the out-of-scope variable ever), skolems
in the kind might have too high a level, triggering a failure to uphold the
invariant that no free variables in a type have a higher level than the
ambient level in the type checker. In the event of having free variables in the
hole's kind, I'm pretty sure we'll always have an erroneous program, so we
don't need to worry what will happen when the hole gets filled in. After all,
a hole relating a locally-bound type variable will be unable to be solved. This
is why it's OK not to look through the IORef of a coercion hole during
substitution.
-}
-- | Type substitution, see 'zipTvSubst'
......@@ -2511,19 +2539,17 @@ subst_co subst co
go (SubCo co) = mkSubCo $! (go co)
go (AxiomRuleCo c cs) = let cs1 = map go cs
in cs1 `seqList` AxiomRuleCo c cs1
go (HoleCo h) = HoleCo h
-- NB: this last case is a little suspicious, but we need it. Originally,
-- there was a panic here, but it triggered from deeplySkolemise. Because
-- we only skolemise tyvars that are manually bound, this operation makes
-- sense, even over a coercion with holes. We don't need to substitute
-- in the type of the coHoleCoVar because it wouldn't makes sense to have
-- forall a. ....(ty |> {hole_cv::a})....
go (HoleCo h) = HoleCo $! go_hole h
go_prov UnsafeCoerceProv = UnsafeCoerceProv
go_prov (PhantomProv kco) = PhantomProv (go kco)
go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco)
go_prov p@(PluginProv _) = p
-- See Note [Substituting in a coercion hole]
go_hole h@(CoercionHole { ch_co_var = cv })
= h { ch_co_var = updateVarType go_ty cv }
substForAllCoBndr :: TCvSubst -> TyVar -> Coercion -> (TCvSubst, TyVar, Coercion)
substForAllCoBndr subst
= substForAllCoBndrUsing False (substCo subst) subst
......
......@@ -10559,49 +10559,6 @@ and :extension:`GADTs`. You can switch it off again with
:extension:`NoMonoLocalBinds <-XMonoLocalBinds>` but type inference becomes
less predictable if you do so. (Read the papers!)
.. _kind-generalisation:
Kind generalisation
-------------------
Just as :extension:`MonoLocalBinds` places limitations on when the *type* of a
*term* is generalised (see :ref:`mono-local-binds`), it also limits when the
*kind* of a *type signature* is generalised. Here is an example involving
:ref:`type signatures on instance declarations <instance-sigs>`: ::
data Proxy a = Proxy
newtype Tagged s b = Tagged b
class C b where
c :: forall (s :: k). Tagged s b
instance C (Proxy a) where
c :: forall s. Tagged s (Proxy a)
c = Tagged Proxy
With :extension:`MonoLocalBinds` enabled, this ``C (Proxy a)`` instance will
fail to typecheck. The reason is that the type signature for ``c`` captures
``a``, an outer-scoped type variable, which means the type signature is not
closed. Therefore, the inferred kind for ``s`` will *not* be generalised, and
as a result, it will fail to unify with the kind variable ``k`` which is
specified in the declaration of ``c``. This can be worked around by specifying
an explicit kind variable for ``s``, e.g., ::
instance C (Proxy a) where
c :: forall (s :: k). Tagged s (Proxy a)
c = Tagged Proxy
or, alternatively: ::
instance C (Proxy a) where
c :: forall k (s :: k). Tagged s (Proxy a)
c = Tagged Proxy
This declarations are equivalent using Haskell's implicit "add implicit
foralls" rules (see :ref:`implicit-quantification`). The implicit foralls rules
are purely syntactic and are quite separate from the kind generalisation
described here.
.. _visible-type-application:
Visible type application
......
......@@ -7,5 +7,5 @@ import Data.Proxy
f :: forall b. b -> (Proxy Int, Proxy Maybe)
f x = (fst y :: Proxy Int, fst y :: Proxy Maybe)
where
y :: (Proxy a, b) -- MonoLocalBinds means this won't generalize over the kind of a
y :: (Proxy a, b) -- this generalizes over the kind of a
y = (Proxy, x)
......@@ -53,3 +53,4 @@ test('T15264', normal, compile, [''])
test('DkNameRes', normal, compile, [''])
test('T15346', normal, compile, [''])
test('T15419', normal, compile, [''])
test('T14066h', normal, compile, [''])
......@@ -2,11 +2,25 @@
DepFail1.hs:7:6: error:
• Expecting one more argument to ‘Proxy Bool’
Expected a type, but ‘Proxy Bool’ has kind ‘Bool -> *’
• In the type signature:
z :: Proxy Bool
• In the type signature: z :: Proxy Bool
DepFail1.hs:8:5: error:
• Couldn't match expected type ‘Proxy Bool’
with actual type ‘Proxy k0 a1’
• In the expression: P
In an equation for ‘z’: z = P
DepFail1.hs:10:16: error:
• Expected kind ‘Int’, but ‘Bool’ has kind ‘*’
• In the second argument of ‘Proxy’, namely ‘Bool’