diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2018-05-18 08:43:11 +0100 |
|---|---|---|
| committer | Simon Peyton Jones <simonpj@microsoft.com> | 2018-05-18 17:16:17 +0100 |
| commit | 2bbdd00c6d70bdc31ff78e2a42b26159c8717856 (patch) | |
| tree | 60701b6613e1822f3007d87e8d4f0bbc707ea4bf | |
| parent | efe405447b9fa88cebce718a6329091755deb9ad (diff) | |
| download | haskell-2bbdd00c6d70bdc31ff78e2a42b26159c8717856.tar.gz | |
Orient TyVar/TyVar equalities with deepest on the left
Trac #15009 showed that, for Given TyVar/TyVar equalities, we really
want to orient them with the deepest-bound skolem on the left. As it
happens, we also want to do the same for Wanteds, but for a different
reason (more likely to be touchable). Either way, deepest wins:
see TcUnify Note [Deeper level on the left].
This observation led me to some significant changes:
* A SkolemTv already had a TcLevel, but the level wasn't really being
used. Now it is!
* I updated added invariant (SkolInf) to TcType
Note [TcLevel and untouchable type variables], documenting that
the level number of all the ic_skols should be the same as the
ic_tclvl of the implication
* FlatSkolTvs and FlatMetaTvs previously had a dummy level-number of
zero, which messed the scheme up. Now they get a level number the
same way as all other TcTyVars, instead of being a special case.
* To make sure that FlatSkolTvs and FlatMetaTvs are untouchable (which
was previously done via their magic zero level) isTouchableMetaTyVar
just tests for those two cases.
* TcUnify.swapOverTyVars is the crucial orientation function; see the
new Note [TyVar/TyVar orientation]. I completely rewrote this function,
and it's now much much easier to understand.
I ended up doing some related refactoring, of course
* I noticed that tcImplicitTKBndrsX and tcExplicitTKBndrsX were doing
a lot of useless work in the case where there are no skolems; I
added a fast-patch
* Elminate the un-used tcExplicitTKBndrsSig; and thereby get rid of
the higher-order parameter to tcExpliciTKBndrsX.
* Replace TcHsType.emitTvImplication with TcUnify.checkTvConstraints,
by analogy with TcUnify.checkConstraints.
* Inline TcUnify.buildImplication into its only call-site in
TcUnify.checkConstraints
* TcS.buildImplication becomes TcS.CheckConstraintsTcS, with a
simpler API
* Now that we have NoEvBindsVar we have no need of termEvidenceAllowed;
nuke the latter, adding Note [No evidence bindings] to TcEvidence.
39 files changed, 531 insertions, 427 deletions
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index dc85fe237c..dfebb87813 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -747,14 +747,9 @@ can_eq_nc_forall ev eq_rel s1 s2 empty_subst2 = mkEmptyTCvSubst (getTCvInScope subst1) - ; (implic, _ev_binds, all_co) <- buildImplication skol_info skol_tvs [] $ - go skol_tvs empty_subst2 bndrs2 - -- We have nowhere to put these bindings - -- but TcSimplify.setImplicationStatus - -- checks that we don't actually use them - -- when skol_info = UnifyForAllSkol - - ; updWorkListTcS (extendWorkListImplic implic) + ; all_co <- checkConstraintsTcS skol_info skol_tvs $ + go skol_tvs empty_subst2 bndrs2 + ; setWantedEq orig_dest all_co ; stopWith ev "Deferred polytype equality" } } @@ -1757,24 +1752,6 @@ canEqTyVarTyVar, are these substituted out Note [Elminate flat-skols] fsk ~ a -Note [Eliminate flat-skols] -~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we have [G] Num (F [a]) -then we flatten to - [G] Num fsk - [G] F [a] ~ fsk -where fsk is a flatten-skolem (FlatSkolTv). Suppose we have - type instance F [a] = a -then we'll reduce the second constraint to - [G] a ~ fsk -and then replace all uses of 'a' with fsk. That's bad because -in error messages intead of saying 'a' we'll say (F [a]). In all -places, including those where the programmer wrote 'a' in the first -place. Very confusing! See Trac #7862. - -Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate -the fsk. - Note [Equalities with incompatible kinds] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ What do we do when we have an equality diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index 7a681b53a8..1172c0ab53 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -413,10 +413,9 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_telescope = m_telescope , ic_given = map (tidyEvVar env1) given , ic_info = info' } ctxt1 | NoEvBindsVar{} <- evb = noDeferredBindings ctxt - | termEvidenceAllowed info = ctxt - | otherwise = noDeferredBindings ctxt + | otherwise = ctxt -- If we go inside an implication that has no term - -- evidence (i.e. unifying under a forall), we can't defer + -- evidence (e.g. unifying under a forall), we can't defer -- type errors. You could imagine using the /enclosing/ -- bindings (in cec_binds), but that may not have enough stuff -- in scope for the bindings to be well typed. So we just diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs index 1065a15b88..2aa2f161b6 100644 --- a/compiler/typecheck/TcEvidence.hs +++ b/compiler/typecheck/TcEvidence.hs @@ -401,10 +401,9 @@ data EvBindsVar -- See Note [Tracking redundant constraints] in TcSimplify } - | NoEvBindsVar { -- used when we're solving only for equalities, - -- which don't have bindings + | NoEvBindsVar { -- See Note [No evidence bindings] - -- see above for comments + -- See above for comments on ebv_uniq, evb_tcvs ebv_uniq :: Unique, ebv_tcvs :: IORef CoVarSet } @@ -415,6 +414,21 @@ instance Data.Data TcEvBinds where gunfold _ _ = error "gunfold" dataTypeOf _ = Data.mkNoRepType "TcEvBinds" +{- Note [No evidence bindings] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Class constraints etc give rise to /term/ bindings for evidence, and +we have nowhere to put term bindings in /types/. So in some places we +use NoEvBindsVar (see newNoTcEvBinds) to signal that no term-level +evidence bindings are allowed. Notebly (): + + - Places in types where we are solving kind constraints (all of which + are equalities); see solveEqualities, solveLocalEqualities, + checkTvConstraints + + - When unifying forall-types +-} + ----------------- newtype EvBindMap = EvBindMap { diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 3bee41f878..125891fff0 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -18,8 +18,8 @@ module TcHsType ( tcHsDeriv, tcHsVectInst, tcHsTypeApp, UserTypeCtxt(..), - tcImplicitTKBndrs, tcImplicitTKBndrsX, tcImplicitTKBndrsSig, - tcExplicitTKBndrs, tcExplicitTKBndrsX, tcExplicitTKBndrsSig, + tcImplicitTKBndrs, tcImplicitTKBndrsX, + tcExplicitTKBndrs, kcExplicitTKBndrs, kcImplicitTKBndrs, -- Type checking type and class decls @@ -247,11 +247,12 @@ tc_hs_sig_type_and_gen skol_info (HsIB { hsib_ext -- kind variables floating about, immediately prior to -- kind generalisation - -- We use "InKnot", because this is called on class method sigs - -- in the knot + -- We use the "InKnot" zonker, because this is called + -- on class method sigs in the knot ; ty1 <- zonkPromoteTypeInKnot $ mkSpecForAllTys tkvs ty ; kvs <- kindGeneralize ty1 ; zonkSigType (mkInvForAllTys kvs ty1) } + tc_hs_sig_type_and_gen _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type_and_gen" tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn -> Kind -> TcM Type @@ -267,6 +268,7 @@ tc_hs_sig_type skol_info (HsIB { hsib_ext = HsIBRn { hsib_vars = sig_vars } -- need to promote any remaining metavariables; test case: -- dependent/should_fail/T14066e. ; zonkPromoteType (mkSpecForAllTys tkvs ty) } + tc_hs_sig_type _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type" ----------------- @@ -395,7 +397,7 @@ Answer: we use the same rule as for value bindings: * Additionally, we attempt to generalise if we have NoMonoLocalBinds Trac #13337 shows the problem if we kind-generalise an open type (i.e. -one that mentions in-scope tpe variable +one that mentions in-scope type variable foo :: forall k (a :: k) proxy. (Typeable k, Typeable a) => proxy a -> String foo _ = case eqT :: Maybe (k :~: Type) of @@ -407,7 +409,7 @@ but (Int :: Type). Since (:~:) is kind-homogeneous, this requires k ~ *, which is true in the Refl branch of the outer case. That equality will be solved if we allow it to float out to the -implication constraint for the Refl match, bnot not if we aggressively +implication constraint for the Refl match, but not not if we aggressively attempt to solve all equalities the moment they occur; that is, when checking (Maybe (a :~: Int)). (NB: solveEqualities fails unless it solves all the kind equalities, which is the right thing at top level.) @@ -1766,24 +1768,31 @@ tcImplicitTKBndrsX :: (Name -> Kind -> TcM TcTyVar) -- new_tv function -> [Name] -> TcM a -> TcM ([TcTyVar], a) -- these tyvars are dependency-ordered --- Returned TcTyVars have the supplied HsTyVarBndrs, --- but may be in different order to the original [Name] +-- * Guarantees to call solveLocalEqualities to unify +-- all constraints from thing_inside. +-- +-- * Returned TcTyVars have the supplied HsTyVarBndrs, +-- but may be in different order to the original [Name] -- (because of sorting to respect dependency) --- Returned TcTyVars have zonked kinds --- See Note [Keeping scoped variables in order: Implicit] +-- +-- * Returned TcTyVars have zonked kinds +-- See Note [Keeping scoped variables in order: Implicit] tcImplicitTKBndrsX new_tv m_kind skol_info tv_names thing_inside + | null tv_names -- Short cut for the common case where there + -- are no implicit type variables to bind + = do { result <- solveLocalEqualities thing_inside + ; return ([], result) } + + | otherwise = do { (skol_tvs, result) <- solveLocalEqualities $ - do { (inner_tclvl, wanted, (skol_tvs, result)) - <- pushLevelAndCaptureConstraints $ - do { tv_pairs <- mapM (tcHsTyVarName new_tv m_kind) tv_names - ; let must_scope_tvs = [ tv | (tv, False) <- tv_pairs ] - ; result <- tcExtendTyVarEnv must_scope_tvs $ - thing_inside - ; return (map fst tv_pairs, result) } + checkTvConstraints skol_info Nothing $ + do { tv_pairs <- mapM (tcHsTyVarName new_tv m_kind) tv_names + ; let must_scope_tvs = [ tv | (tv, False) <- tv_pairs ] + ; result <- tcExtendTyVarEnv must_scope_tvs $ + thing_inside + ; return (map fst tv_pairs, result) } - ; emitTvImplication inner_tclvl skol_tvs Nothing wanted skol_info - ; return (skol_tvs, result) } ; skol_tvs <- mapM zonkTcTyCoVarBndr skol_tvs -- use zonkTcTyCoVarBndr because a skol_tv might be a SigTv @@ -1812,24 +1821,8 @@ tcExplicitTKBndrs :: SkolemInfo -> [LHsTyVarBndr GhcRn] -> TcM a -> TcM ([TcTyVar], a) --- No cloning: returned TyVars have the same Name as the incoming LHsTyVarBndrs -tcExplicitTKBndrs = tcExplicitTKBndrsX newSkolemTyVar - --- | This brings a bunch of tyvars into scope as SigTvs, where they can unify --- with other type *variables* only. -tcExplicitTKBndrsSig :: SkolemInfo - -> [LHsTyVarBndr GhcRn] - -> TcM a - -> TcM ([TcTyVar], a) -tcExplicitTKBndrsSig = tcExplicitTKBndrsX newSigTyVar - -tcExplicitTKBndrsX :: (Name -> Kind -> TcM TyVar) - -> SkolemInfo - -> [LHsTyVarBndr GhcRn] - -> TcM a - -> TcM ([TcTyVar], a) -- See also Note [Associated type tyvar names] in Class -tcExplicitTKBndrsX new_tv skol_info hs_tvs thing_inside +tcExplicitTKBndrs skol_info hs_tvs thing_inside -- This function brings into scope a telescope of binders as written by -- the user. At first blush, it would then seem that we should bring -- them into scope one at a time, bumping the TcLevel each time. @@ -1840,11 +1833,16 @@ tcExplicitTKBndrsX new_tv skol_info hs_tvs thing_inside -- notice that the telescope is out of order. That's what we do here, -- following the logic of tcImplicitTKBndrsX. -- See also Note [Keeping scoped variables in order: Explicit] - = do { (inner_tclvl, wanted, (skol_tvs, result)) - <- pushLevelAndCaptureConstraints $ - bind_tvbs hs_tvs +-- +-- No cloning: returned TyVars have the same Name as the incoming LHsTyVarBndrs + | null hs_tvs -- Short cut that avoids creating an implication + -- constraint in the common case where none is needed + = do { result <- thing_inside + ; return ([], result) } - ; emitTvImplication inner_tclvl skol_tvs (Just doc) wanted skol_info + | otherwise + = do { (skol_tvs, result) <- checkTvConstraints skol_info (Just doc) $ + bind_tvbs hs_tvs ; traceTc "tcExplicitTKBndrs" $ vcat [ text "Hs vars:" <+> ppr hs_tvs @@ -1856,7 +1854,7 @@ tcExplicitTKBndrsX new_tv skol_info hs_tvs thing_inside bind_tvbs [] = do { result <- thing_inside ; return ([], result) } bind_tvbs (L _ tvb : tvbs) - = do { (tv, in_scope) <- tcHsTyVarBndr new_tv tvb + = do { (tv, in_scope) <- tcHsTyVarBndr newSkolemTyVar tvb ; (if in_scope then id else tcExtendTyVarEnv [tv]) $ do { (tvs, result) <- bind_tvbs tvbs ; return (tv : tvs, result) }} @@ -1874,28 +1872,6 @@ kcExplicitTKBndrs (L _ hs_tv : hs_tvs) thing_inside ; tcExtendTyVarEnv [tv] $ kcExplicitTKBndrs hs_tvs thing_inside } --- | Build and emit an Implication appropriate for type-checking a type. --- This assumes all constraints will be equality constraints, and --- so does not create an EvBindsVar -emitTvImplication :: TcLevel -- of the constraints - -> [TcTyVar] -- skolems - -> Maybe SDoc -- user-written telescope, if present - -> WantedConstraints - -> SkolemInfo - -> TcM () -emitTvImplication inner_tclvl skol_tvs m_telescope wanted skol_info - = do { tc_lcl_env <- getLclEnv - ; ev_binds <- newNoTcEvBinds - ; let implic = newImplication { ic_tclvl = inner_tclvl - , ic_skols = skol_tvs - , ic_telescope = m_telescope - , ic_no_eqs = True - , ic_wanted = wanted - , ic_binds = ev_binds - , ic_info = skol_info - , ic_env = tc_lcl_env } - ; emitImplication implic } - tcHsTyVarBndr :: (Name -> Kind -> TcM TyVar) -> HsTyVarBndr GhcRn -> TcM (TcTyVar, Bool) -- Return a TcTyVar, built using the provided function diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index b1bc1d0b23..398d345ea1 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -512,13 +512,24 @@ tcInstSkolTyVars' overlappable subst tvs ; instSkolTyCoVarsX (mkTcSkolTyVar lvl loc overlappable) subst tvs } mkTcSkolTyVar :: TcLevel -> SrcSpan -> Bool -> TcTyCoVarMaker gbl lcl -mkTcSkolTyVar lvl loc overlappable old_name kind +-- Allocates skolems whose level is ONE GREATER THAN the passed-in tc_lvl +-- See Note [Skolem level allocation] +mkTcSkolTyVar tc_lvl loc overlappable old_name kind = do { uniq <- newUnique ; let name = mkInternalName uniq (getOccName old_name) loc ; return (mkTcTyVar name kind details) } where - details = SkolemTv (pushTcLevel lvl) overlappable - -- NB: skolems bump the level + details = SkolemTv (pushTcLevel tc_lvl) overlappable + -- pushTcLevel: see Note [Skolem level allocation] + +{- Note [Skolem level allocation] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We generally allocate skolems /before/ calling pushLevelAndCaptureConstraints. +So we want their level to the level of the soon-to-be-created implication, +which has a level one higher than the current level. Hence the pushTcLevel. +It feels like a slight hack. Applies also to vanillaSkolemTv. + +-} ------------------ freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar]) @@ -569,9 +580,10 @@ newFskTyVar :: TcType -> TcM TcTyVar newFskTyVar fam_ty = do { uniq <- newUnique ; ref <- newMutVar Flexi + ; tclvl <- getTcLevel ; let details = MetaTv { mtv_info = FlatSkolTv , mtv_ref = ref - , mtv_tclvl = fmvTcLevel } + , mtv_tclvl = tclvl } name = mkMetaTyVarName uniq (fsLit "fsk") ; return (mkTcTyVar name (typeKind fam_ty) details) } @@ -624,9 +636,10 @@ newFmvTyVar :: TcType -> TcM TcTyVar newFmvTyVar fam_ty = do { uniq <- newUnique ; ref <- newMutVar Flexi + ; tclvl <- getTcLevel ; let details = MetaTv { mtv_info = FlatMetaTv , mtv_ref = ref - , mtv_tclvl = fmvTcLevel } + , mtv_tclvl = tclvl } name = mkMetaTyVarName uniq (fsLit "s") ; return (mkTcTyVar name (typeKind fam_ty) details) } diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs index d3f5c6822a..f39ce52917 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -636,9 +636,9 @@ tcPatSynMatcher (L loc name) lpat (args, arg_tys) pat_ty = do { rr_name <- newNameAt (mkTyVarOcc "rep") loc ; tv_name <- newNameAt (mkTyVarOcc "r") loc - ; let rr_tv = mkTcTyVar rr_name runtimeRepTy vanillaSkolemTv + ; let rr_tv = mkTyVar rr_name runtimeRepTy rr = mkTyVarTy rr_tv - res_tv = mkTcTyVar tv_name (tYPE rr) vanillaSkolemTv + res_tv = mkTyVar tv_name (tYPE rr) res_ty = mkTyVarTy res_tv is_unlifted = null args && null prov_dicts (cont_args, cont_arg_tys) @@ -686,7 +686,7 @@ tcPatSynMatcher (L loc name) lpat } match = mkMatch (mkPrefixFunRhs (L loc name)) [] (mkHsLams (rr_tv:res_tv:univ_tvs) - req_dicts body') + req_dicts body') (noLoc (EmptyLocalBinds noExt)) mg :: MatchGroup GhcTc (LHsExpr GhcTc) mg = MG{ mg_alts = L (getLoc match) [match] diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index 968330da8b..cc5c7ec508 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -106,7 +106,6 @@ module TcRnTypes( SkolemInfo(..), pprSigSkolInfo, pprSkolInfo, - termEvidenceAllowed, CtEvidence(..), TcEvDest(..), mkKindLoc, toKindLoc, mkGivenLoc, @@ -3228,14 +3227,6 @@ data SkolemInfo instance Outputable SkolemInfo where ppr = pprSkolInfo -termEvidenceAllowed :: SkolemInfo -> Bool --- Whether an implication constraint with this SkolemInfo --- is permitted to have term-level evidence. There is --- only one that is not, associated with unifiying --- forall-types -termEvidenceAllowed (UnifyForAllSkol {}) = False -termEvidenceAllowed _ = True - pprSkolInfo :: SkolemInfo -> SDoc -- Complete the sentence "is a rigid type variable bound by..." pprSkolInfo (SigSkol cx ty _) = pprSigSkolInfo cx ty diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index b1da40c18b..150f9be671 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -16,7 +16,7 @@ module TcSMonad ( TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds, failTcS, warnTcS, addErrTcS, runTcSEqualities, - nestTcS, nestImplicTcS, setEvBindsTcS, buildImplication, + nestTcS, nestImplicTcS, setEvBindsTcS, checkConstraintsTcS, runTcPluginTcS, addUsedGRE, addUsedGREs, @@ -1950,8 +1950,12 @@ getNoGivenEqs tclvl skol_tvs -- outer context but were refined to an insoluble by -- a local equality; so do /not/ add ct_given_here. - ; traceTcS "getNoGivenEqs" (vcat [ ppr has_given_eqs, ppr inerts - , ppr insols]) + ; traceTcS "getNoGivenEqs" $ + vcat [ if has_given_eqs then text "May have given equalities" + else text "No given equalities" + , text "Skols:" <+> ppr skol_tvs + , text "Inerts:" <+> ppr inerts + , text "Insols:" <+> ppr insols] ; return (not has_given_eqs, insols) } where eqs_given_here :: EqualCtList -> Bool @@ -2094,6 +2098,10 @@ b) 'a' will have been completely substituted out in the inert set, returned as part of 'fsks' For an example, see Trac #9211. + +See also TcUnify Note [Deeper level on the left] for how we ensure +that the right variable is on the left of the equality when both are +tyvars. -} removeInertCts :: [Ct] -> InertCans -> InertCans @@ -2704,40 +2712,40 @@ nestTcS (TcS thing_inside) ; return res } -buildImplication :: SkolemInfo - -> [TcTyVar] -- Skolems - -> [EvVar] -- Givens - -> TcS result - -> TcS (Bag Implication, TcEvBinds, result) --- Just like TcUnify.buildImplication, but in the TcS monnad, +checkConstraintsTcS :: SkolemInfo + -> [TcTyVar] -- Skolems + -> TcS result + -> TcS result +-- Just like TcUnify.checkTvConstraints, but in the TcS monnad, -- using the work-list to gather the constraints -buildImplication skol_info skol_tvs givens (TcS thing_inside) - = TcS $ \ env -> +checkConstraintsTcS skol_info skol_tvs (TcS thing_inside) + = TcS $ \ tcs_env -> do { new_wl_var <- TcM.newTcRef emptyWorkList - ; tc_lvl <- TcM.getTcLevel - ; let new_tclvl = pushTcLevel tc_lvl + ; let new_tcs_env = tcs_env { tcs_worklist = new_wl_var } - ; res <- TcM.setTcLevel new_tclvl $ - thing_inside (env { tcs_worklist = new_wl_var }) + ; (res, new_tclvl) <- TcM.pushTcLevelM $ + thing_inside new_tcs_env ; wl@WL { wl_eqs = eqs } <- TcM.readTcRef new_wl_var - ; if null eqs - then return (emptyBag, emptyTcEvBinds, res) - else - do { env <- TcM.getLclEnv - ; ev_binds_var <- TcM.newTcEvBinds - ; let wc = ASSERT2( null (wl_funeqs wl) && null (wl_rest wl) && - null (wl_implics wl), ppr wl ) - WC { wc_simple = listToCts eqs - , wc_impl = emptyBag } - imp = newImplication { ic_tclvl = new_tclvl - , ic_skols = skol_tvs - , ic_given = givens - , ic_wanted = wc - , ic_binds = ev_binds_var - , ic_env = env - , ic_info = skol_info } - ; return (unitBag imp, TcEvBinds ev_binds_var, res) } } + ; ASSERT2( null (wl_funeqs wl) && null (wl_rest wl) && + null (wl_implics wl), ppr wl ) + unless (null eqs) $ + do { tcl_env <- TcM.getLclEnv + ; ev_binds_var <- TcM.newNoTcEvBinds + ; let wc = WC { wc_simple = listToCts eqs + , wc_impl = emptyBag } + imp = newImplication { ic_tclvl = new_tclvl + , ic_skols = skol_tvs + , ic_wanted = wc + , ic_binds = ev_binds_var + , ic_env = tcl_env + , ic_info = skol_info } + + -- Add the implication to the work-list + ; TcM.updTcRef (tcs_worklist tcs_env) + (extendWorkListImplic (unitBag imp)) } + + ; return res } {- Note [Propagate the solved dictionaries] @@ -2778,9 +2786,7 @@ getWorkListImplics updWorkListTcS :: (WorkList -> WorkList) -> TcS () updWorkListTcS f = do { wl_var <- getTcSWorkListRef - ; wl_curr <- wrapTcS (TcM.readTcRef wl_var) - ; let new_work = f wl_curr - ; wrapTcS (TcM.writeTcRef wl_var new_work) } + ; wrapTcS (TcM.updTcRef wl_var f)} emitWorkNC :: [CtEvidence] -> TcS () emitWorkNC evs diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index ccb7ef5056..136e60ae37 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -1725,19 +1725,13 @@ neededEvVars :: Implication -> TcS Implication -- - From the 'needed' set, delete ev_bndrs, the binders of the -- evidence bindings, to give the final needed variables -- -neededEvVars implic@(Implic { ic_info = info - , ic_given = givens +neededEvVars implic@(Implic { ic_given = givens , ic_binds = ev_binds_var , ic_wanted = WC { wc_impl = implics } , ic_need_inner = old_needs }) = do { ev_binds <- TcS.getTcEvBindsMap ev_binds_var ; tcvs <- TcS.getTcEvTyCoVars ev_binds_var - -- Check that there are no term-level evidence bindings - -- in the cases where we have no place to put them - ; MASSERT2( termEvidenceAllowed info || isEmptyEvBindMap ev_binds - , ppr info $$ ppr ev_binds ) - ; let seeds1 = foldrBag add_implic_seeds old_needs implics seeds2 = foldEvBindMap add_wanted seeds1 ev_binds seeds3 = seeds2 `unionVarSet` tcvs diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 8295c5731d..9abd264949 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -30,7 +30,7 @@ module TcType ( -- TcLevel TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel, - strictlyDeeperThan, sameDepthAs, fmvTcLevel, + strictlyDeeperThan, sameDepthAs, tcTypeLevel, tcTyVarLevel, maxTcLevel, promoteSkolem, promoteSkolemX, promoteSkolemsX, -------------------------------- @@ -44,7 +44,7 @@ module TcType ( isAmbiguousTyVar, metaTyVarRef, metaTyVarInfo, isFlexi, isIndirect, isRuntimeUnkSkol, metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe, - isTouchableMetaTyVar, isTouchableOrFmv, + isTouchableMetaTyVar, isFloatedTouchableMetaTyVar, findDupSigTvs, mkTyVarNamePairs, @@ -282,8 +282,6 @@ However, the type checker and constraint solver can encounter type variables that use the 'TyVar' variant of Var.Var, for a couple of reasons: - - When unifying or flattening under (forall a. ty) - - When typechecking a class decl, say class C (a :: k) where foo :: T a -> Int @@ -295,7 +293,10 @@ reasons: See calls to tcExtendTyVarEnv for other places that ordinary TyVars are bought into scope, and hence may show up in the types - and inds generated by TcHsType. + and kinds generated by TcHsType. + + - The pattern-match overlap checker calls the constraint solver, + long afer TcTyVars have been zonked away It's convenient to simply treat these TyVars as skolem constants, which of course they are. So @@ -503,6 +504,8 @@ we would need to enforce the separation. data TcTyVarDetails = SkolemTv -- A skolem TcLevel -- Level of the implication that binds it + -- See TcUnify Note [Deeper level on the left] for + -- how this level number is used Bool -- True <=> this skolem type variable can be overlapped -- when looking up instances -- See Note [Binding when looking up instances] in InstEnv @@ -516,8 +519,10 @@ data TcTyVarDetails vanillaSkolemTv, superSkolemTv :: TcTyVarDetails -- See Note [Binding when looking up instances] in InstEnv -vanillaSkolemTv = SkolemTv (pushTcLevel topTcLevel) False -- Might be instantiated -superSkolemTv = SkolemTv (pushTcLevel topTcLevel) True -- Treat this as a completely distinct type +vanillaSkolemTv = SkolemTv topTcLevel False -- Might be instantiated +superSkolemTv = SkolemTv topTcLevel True -- Treat this as a completely distinct type + -- The choice of level number here is a bit dodgy, but + -- topTcLevel works in the places that vanillaSkolemTv is used ----------------------------- data MetaDetails @@ -689,9 +694,13 @@ Note [TcLevel and untouchable type variables] (ImplicInv) The level number (ic_tclvl) of an Implication is STRICTLY GREATER THAN that of its parent - (GivenInv) The level number of a unification variable appearing - in the 'ic_given' of an implication I should be - STRICTLY LESS THAN the ic_tclvl of I + (SkolInv) The level number of the skolems (ic_skols) of an + Implication is equal to the level of the implication + itself (ic_tclvl) + + (GivenInv) The level number of a unification variable appearing + in the 'ic_given' of an implication I should be + STRICTLY LESS THAN the ic_tclvl of I (WantedInv) The level number of a unification variable appearing in the 'ic_wanted' of an implication I should be @@ -699,7 +708,8 @@ Note [TcLevel and untouchable type variables] See Note [WantedInv] * A unification variable is *touchable* if its level number - is EQUAL TO that of its immediate parent implication. + is EQUAL TO that of its immediate parent implication, + and it is a TauTv or SigTv (but /not/ FlatMetaTv or FlatSkolTv Note [WantedInv] ~~~~~~~~~~~~~~~~ @@ -749,28 +759,21 @@ Note [TcLevel assignment] ~~~~~~~~~~~~~~~~~~~~~~~~~ We arrange the TcLevels like this - 0 Level for all flatten meta-vars - 1 Top level - 2 First-level implication constraints - 3 Second-level implication constraints + 0 Top level + 1 First-level implication constraints + 2 Second-level implication constraints ...etc... - -The flatten meta-vars are all at level 0, just to make them untouchable. -} maxTcLevel :: TcLevel -> TcLevel -> TcLevel maxTcLevel (TcLevel a) (TcLevel b) = TcLevel (a `max` b) -fmvTcLevel :: TcLevel --- See Note [TcLevel assignment] -fmvTcLevel = TcLevel 0 - topTcLevel :: TcLevel -- See Note [TcLevel assignment] -topTcLevel = TcLevel 1 -- 1 = outermost level +topTcLevel = TcLevel 0 -- 0 = outermost level isTopTcLevel :: TcLevel -> Bool -isTopTcLevel (TcLevel 1) = True +isTopTcLevel (TcLevel 0) = True isTopTcLevel _ = False pushTcLevel :: TcLevel -> TcLevel @@ -1172,37 +1175,25 @@ tcIsTcTyVar :: TcTyVar -> Bool -- See Note [TcTyVars in the typechecker] tcIsTcTyVar tv = isTyVar tv -isTouchableOrFmv :: TcLevel -> TcTyVar -> Bool -isTouchableOrFmv ctxt_tclvl tv - = ASSERT2( tcIsTcTyVar tv, ppr tv ) - case tcTyVarDetails tv of - MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info } - -> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl, - ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl ) - case info of - FlatMetaTv -> True - _ -> tv_tclvl `sameDepthAs` ctxt_tclvl - _ -> False - isTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool isTouchableMetaTyVar ctxt_tclvl tv | isTyVar tv -- See Note [Coercion variables in free variable lists] - = ASSERT2( tcIsTcTyVar tv, ppr tv ) - case tcTyVarDetails tv of - MetaTv { mtv_tclvl = tv_tclvl } - -> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl, - ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl ) - tv_tclvl `sameDepthAs` ctxt_tclvl - _ -> False + , MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info } <- tcTyVarDetails tv + , not (isFlattenInfo info) + = ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl, + ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl ) + tv_tclvl `sameDepthAs` ctxt_tclvl + | otherwise = False isFloatedTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool isFloatedTouchableMetaTyVar ctxt_tclvl tv | isTyVar tv -- See Note [Coercion variables in free variable lists] + , MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info } <- tcTyVarDetails tv + , not (isFlattenInfo info) = ASSERT2( tcIsTcTyVar tv, ppr tv ) - case tcTyVarDetails tv of - MetaTv { mtv_tclvl = tv_tclvl } -> tv_tclvl `strictlyDeeperThan` ctxt_tclvl - _ -> False + tv_tclvl `strictlyDeeperThan` ctxt_tclvl + | otherwise = False isImmutableTyVar :: TyVar -> Bool @@ -1237,7 +1228,10 @@ isFskTyVar tv -- | True of both given and wanted flatten-skolems (fak and usk) isFlattenTyVar tv - = isFmvTyVar tv || isFskTyVar tv + = ASSERT2( tcIsTcTyVar tv, ppr tv ) + case tcTyVarDetails tv of + MetaTv { mtv_info = info } -> isFlattenInfo info + _ -> False isSkolemTyVar tv = ASSERT2( tcIsTcTyVar tv, ppr tv ) @@ -1284,6 +1278,11 @@ metaTyVarInfo tv MetaTv { mtv_info = info } -> info _ -> pprPanic "metaTyVarInfo" (ppr tv) +isFlattenInfo :: MetaInfo -> Bool +isFlattenInfo FlatMetaTv = True +isFlattenInfo FlatSkolTv = True +isFlattenInfo _ = False + metaTyVarTcLevel :: TcTyVar -> TcLevel metaTyVarTcLevel tv = case tcTyVarDetails tv of diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index a61b06101a..4343c32bf4 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -13,7 +13,8 @@ module TcUnify ( tcWrapResult, tcWrapResultO, tcSkolemise, tcSkolemiseET, tcSubTypeHR, tcSubTypeO, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_NC_O, tcSubTypeET, - checkConstraints, buildImplicationFor, + checkConstraints, checkTvConstraints, + buildImplicationFor, -- Various unifications unifyType, unifyTheta, unifyKind, @@ -1124,29 +1125,45 @@ checkConstraints :: SkolemInfo -> TcM (TcEvBinds, result) checkConstraints skol_info skol_tvs given thing_inside - = do { (implics, ev_binds, result) - <- buildImplication skol_info skol_tvs given thing_inside - ; emitImplications implics - ; return (ev_binds, result) } - -buildImplication :: SkolemInfo - -> [TcTyVar] -- Skolems - -> [EvVar] -- Given - -> TcM result - -> TcM (Bag Implication, TcEvBinds, result) -buildImplication skol_info skol_tvs given thing_inside = do { implication_needed <- implicationNeeded skol_tvs given ; if implication_needed then do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted - ; return (implics, ev_binds, result) } + ; traceTc "checkConstraints" (ppr tclvl $$ ppr skol_tvs) + ; emitImplications implics + ; return (ev_binds, result) } else -- Fast path. We check every function argument with -- tcPolyExpr, which uses tcSkolemise and hence checkConstraints. -- So this fast path is well-exercised do { res <- thing_inside - ; return (emptyBag, emptyTcEvBinds, res) } } + ; return (emptyTcEvBinds, res) } } + +checkTvConstraints :: SkolemInfo + -> Maybe SDoc -- User-written telescope, if present + -> TcM ([TcTyVar], result) + -> TcM ([TcTyVar], result) + +checkTvConstraints skol_info m_telescope thing_inside + = do { (tclvl, wanted, (skol_tvs, result)) + <- pushLevelAndCaptureConstraints thing_inside + + ; if isEmptyWC wanted + then return () + else do { tc_lcl_env <- getLclEnv + ; ev_binds <- newNoTcEvBinds + ; emitImplication $ + newImplication { ic_tclvl = tclvl + , ic_skols = skol_tvs + , ic_no_eqs = True + , ic_telescope = m_telescope + , ic_wanted = wanted + , ic_binds = ev_binds + , ic_info = skol_info + , ic_env = tc_lcl_env } } + ; return (skol_tvs, result) } + implicationNeeded :: [TcTyVar] -> [EvVar] -> TcM Bool -- With the solver producing unlifted equalities, we need @@ -1585,72 +1602,113 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 swapOverTyVars :: TcTyVar -> TcTyVar -> Bool swapOverTyVars tv1 tv2 - | isFmvTyVar tv1 = False -- See Note [Fmv Orientation Invariant] - | isFmvTyVar tv2 = True - - | Just lvl1 <- metaTyVarTcLevel_maybe tv1 - -- If tv1 is touchable, swap only if tv2 is also - -- touchable and it's strictly better to update the latter - -- But see Note [Avoid unnecessary swaps] - = case metaTyVarTcLevel_maybe tv2 of - Nothing -> False - Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True - | lvl1 `strictlyDeeperThan` lvl2 -> False - | otherwise -> nicer_to_update_tv2 - - -- So tv1 is not a meta tyvar - -- If only one is a meta tyvar, put it on the left - -- This is not because it'll be solved; but because - -- the floating step looks for meta tyvars on the left - | isMetaTyVar tv2 = True - - -- So neither is a meta tyvar (including FlatMetaTv) - - -- If only one is a flatten skolem, put it on the left - -- See Note [Eliminate flat-skols] - | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True + -- Level comparison: see Note [TyVar/TyVar orientation] + | lvl1 `strictlyDeeperThan` lvl2 = False + | lvl2 `strictlyDeeperThan` lvl1 = True + + -- Priority: see Note [TyVar/TyVar orientation] + | pri1 > pri2 = False + | pri2 > pri1 = True + + -- Names: see Note [TyVar/TyVar orientation] + | isSystemName tv2_name, not (isSystemName tv1_name) = True | otherwise = False where + lvl1 = tcTyVarLevel tv1 + lvl2 = tcTyVarLevel tv2 + pri1 = lhsPriority tv1 + pri2 = lhsPriority tv2 tv1_name = Var.varName tv1 tv2_name = Var.varName tv2 - nicer_to_update_tv2 - | isSigTyVar tv1, not (isSigTyVar tv2) = True - | isSystemName tv2_name, not (isSystemName tv1_name) = True --- | nameUnique tv1_name `ltUnique` nameUnique tv2_name = True --- -- See Note [Eliminate younger unification variables] --- (which also explains why it's commented out) - | otherwise = False +lhsPriority :: TcTyVar -> Int +-- Higher => more important to be on the LHS +-- See Note [TyVar/TyVar orientation] +lhsPriority tv + = ASSERT2( isTyVar tv, ppr tv) + case tcTyVarDetails tv of + RuntimeUnk -> 0 + SkolemTv {} -> 0 + MetaTv { mtv_info = info } -> case info of + FlatSkolTv -> 1 + SigTv -> 2 + TauTv -> 3 + FlatMetaTv -> 4 +{- Note [TyVar/TyVar orientation] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Given (a ~ b), should we orient the CTyEqCan as (a~b) or (b~a)? +This is a surprisingly tricky question! --- @trySpontaneousSolve wi@ solves equalities where one side is a --- touchable unification variable. --- Returns True <=> spontaneous solve happened -canSolveByUnification :: TcLevel -> TcTyVar -> TcType -> Bool -canSolveByUnification tclvl tv xi - | isTouchableMetaTyVar tclvl tv - = case metaTyVarInfo tv of - SigTv -> is_tyvar xi - _ -> True +First note: only swap if you have to! + See Note [Avoid unnecessary swaps] - | otherwise -- Untouchable - = False - where - is_tyvar xi - = case tcGetTyVar_maybe xi of - Nothing -> False - Just tv -> case tcTyVarDetails tv of - MetaTv { mtv_info = info } - -> case info of - SigTv -> True - _ -> False - SkolemTv {} -> True - RuntimeUnk -> True +So we look for a positive reason to swap, using a three-step test: -{- Note [Fmv Orientation Invariant] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +* Level comparison. If 'a' has deeper level than 'b', + put 'a' on the left. See Note [Deeper level on the left] + +* Priority. If the levels are the same, look at what kind of + type variable it is, using 'lhsPriority' + + - FlatMetaTv: Always put on the left. + See Note [Fmv Orientation Invariant] + NB: FlatMetaTvs always have the current level, never an + outer one. So nothing can be deeper than a FlatMetaTv + + + - SigTv/TauTv: if we have sig_tv ~ tau_tv, put tau_tv + on the left because there are fewer + restrictions on updating TauTvs + + - SigTv/TauTv: put on the left eitehr + a) Because it's touchable and can be unified, or + b) Even if it's not touchable, TcSimplify.floatEqualities + looks for meta tyvars on the left + + - FlatSkolTv: Put on the left in preference to a SkolemTv + See Note [Eliminate flat-skols] + +* Names. If the level and priority comparisons are all + equal, try to eliminate a TyVars with a System Name in + favour of ones with a Name derived from a user type signature + +* Age. At one point in the past we tried to break any remaining + ties by eliminating the younger type variable, based on their + Uniques. See Note [Eliminate younger unification variables] + (which also explains why we don't do this any more) + +Note [Deeper level on the left] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The most important thing is that we want to put tyvars with +the deepest level on the left. The reason to do so differs for +Wanteds and Givens, but either way, deepest wins! Simple. + +* Wanteds. Putting the deepest variable on the left maximise the + chances that it's a touchable meta-tyvar which can be solved. + +* Givens. Suppose we have something like + forall a[2]. b[1] ~ a[2] => beta[1] ~ a[2] + + If we orient the Given a[2] on the left, we'll rewrite the Wanted to + (beta[1] ~ b[1]), and that can float out of the implication. + Otherwise it can't. By putting the deepest variable on the left + we maximise our changes of elminating skolem capture. + + See also TcSMonad Note [Let-bound skolems] for another reason + to orient with the deepest skolem on the left. + + IMPORTANT NOTE: this test does a level-number comparison on + skolems, so it's important that skolems have (accurate) level + numbers. + +See Trac #15009 for an further analysis of why "deepest on the left" +is a good plan. + +Note [Fmv Orientation Invariant] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * We always orient a constraint fmv ~ alpha with fmv on the left, even if alpha is @@ -1683,12 +1741,30 @@ T10226, T10009.) [WD] F fmv ~ fmv, [WD] fmv ~ a And now we are stuck. -So instead the Fmv Orientation Invariant puts te fmv on the +So instead the Fmv Orientation Invariant puts the fmv on the left, giving [WD] fmv ~ alpha, [WD] F alpha ~ fmv, [WD] alpha ~ a Now we get alpha:=a, and everything works out +Note [Eliminate flat-skols] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have [G] Num (F [a]) +then we flatten to + [G] Num fsk + [G] F [a] ~ fsk +where fsk is a flatten-skolem (FlatSkolTv). Suppose we have + type instance F [a] = a +then we'll reduce the second constraint to + [G] a ~ fsk +and then replace all uses of 'a' with fsk. That's bad because +in error messages intead of saying 'a' we'll say (F [a]). In all +places, including those where the programmer wrote 'a' in the first +place. Very confusing! See Trac #7862. + +Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate +the fsk. + Note [Avoid unnecessary swaps] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ If we swap without actually improving matters, we can get an infinite loop. @@ -1719,10 +1795,34 @@ But, to my surprise, it didn't seem to make any significant difference to the compiler's performance, so I didn't take it any further. Still it seemed to too nice to discard altogether, so I'm leaving these notes. SLPJ Jan 18. +-} +-- @trySpontaneousSolve wi@ solves equalities where one side is a +-- touchable unification variable. +-- Returns True <=> spontaneous solve happened +canSolveByUnification :: TcLevel -> TcTyVar -> TcType -> Bool +canSolveByUnification tclvl tv xi + | isTouchableMetaTyVar tclvl tv + = case metaTyVarInfo tv of + SigTv -> is_tyvar xi + _ -> True -Note [Prevent unification with type families] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + | otherwise -- Untouchable + = False + where + is_tyvar xi + = case tcGetTyVar_maybe xi of + Nothing -> False + Just tv -> case tcTyVarDetails tv of + MetaTv { mtv_info = info } + -> case info of + SigTv -> True + _ -> False + SkolemTv {} -> True + RuntimeUnk -> True + +{- Note [Prevent unification with type families] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We prevent unification with type families because of an uneasy compromise. It's perfectly sound to unify with type families, and it even improves the error messages in the testsuite. It also modestly improves performance, at @@ -1849,7 +1949,7 @@ lookupTcTyVar tyvar Note [Unifying untouchables] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We treat an untouchable type variable as if it was a skolem. That -ensures it won't unify with anything. It's a slight had, because +ensures it won't unify with anything. It's a slight hack, because we return a made-up TcTyVarDetails, but I think it works smoothly. -} diff --git a/testsuite/tests/ado/T13242a.stderr b/testsuite/tests/ado/T13242a.stderr index c3dbbba970..e03f471e8b 100644 --- a/testsuite/tests/ado/T13242a.stderr +++ b/testsuite/tests/ado/T13242a.stderr @@ -1,8 +1,7 @@ T13242a.hs:10:5: error: • Couldn't match expected type ‘a0’ with actual type ‘a’ - because type variable ‘a’ would escape its scope - This (rigid, skolem) type variable is bound by + ‘a’ is a rigid type variable bound by a pattern with constructor: A :: forall a. Eq a => a -> T, in a pattern binding in 'do' block @@ -28,7 +27,7 @@ T13242a.hs:13:11: error: These potential instances exist: instance Eq Ordering -- Defined in ‘GHC.Classes’ instance Eq Integer - -- Defined in ‘integer-gmp-1.0.1.0:GHC.Integer.Type’ + -- Defined in ‘integer-gmp-1.0.2.0:GHC.Integer.Type’ instance Eq a => Eq (Maybe a) -- Defined in ‘GHC.Base’ ...plus 22 others ...plus six instances involving out-of-scope types diff --git a/testsuite/tests/dependent/should_fail/T14066d.stderr b/testsuite/tests/dependent/should_fail/T14066d.stderr index 3a8b90edce..3f5eb9825a 100644 --- a/testsuite/tests/dependent/should_fail/T14066d.stderr +++ b/testsuite/tests/dependent/should_fail/T14066d.stderr @@ -1,14 +1,14 @@ T14066d.hs:11:35: error: - • Couldn't match type ‘b’ with ‘b1’ - ‘b’ is a rigid type variable bound by - the type signature for: - f :: forall b. b -> (Proxy Maybe, ()) - at T14066d.hs:10:1-37 + • Couldn't match type ‘b1’ with ‘b’ ‘b1’ is a rigid type variable bound by a type expected by the context: forall c b1 (a :: c). (Proxy a, Proxy c, b1) at T14066d.hs:11:33-35 + ‘b’ is a rigid type variable bound by + the type signature for: + f :: forall b. b -> (Proxy Maybe, ()) + at T14066d.hs:10:1-37 Expected type: (Proxy a, Proxy c, b1) Actual type: (Proxy a, Proxy c, b) • In the first argument of ‘g’, namely ‘y’ diff --git a/testsuite/tests/deriving/should_compile/T14578.stderr b/testsuite/tests/deriving/should_compile/T14578.stderr index 63375aeae0..bdb6ca5296 100644 --- a/testsuite/tests/deriving/should_compile/T14578.stderr +++ b/testsuite/tests/deriving/should_compile/T14578.stderr @@ -108,15 +108,15 @@ Derived type family instances: ==================== Filling in method body ==================== -GHC.Base.Semigroup [T14578.App f[ssk:2] a[ssk:2]] +GHC.Base.Semigroup [T14578.App f[ssk:1] a[ssk:1]] GHC.Base.sconcat = GHC.Base.$dmsconcat - @(T14578.App f[ssk:2] a[ssk:2]) + @(T14578.App f[ssk:1] a[ssk:1]) ==================== Filling in method body ==================== -GHC.Base.Semigroup [T14578.App f[ssk:2] a[ssk:2]] +GHC.Base.Semigroup [T14578.App f[ssk:1] a[ssk:1]] GHC.Base.stimes = GHC.Base.$dmstimes - @(T14578.App f[ssk:2] a[ssk:2]) + @(T14578.App f[ssk:1] a[ssk:1]) diff --git a/testsuite/tests/gadt/T15009.hs b/testsuite/tests/gadt/T15009.hs new file mode 100644 index 0000000000..58e17af864 --- /dev/null +++ b/testsuite/tests/gadt/T15009.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE GADTs #-} + +module T15009 where + +-- T2 is an ordinary H98 data type, +-- and f2 should typecheck with no problem +data T2 a where + MkT2 :: a -> T2 a + +f2 (MkT2 x) = not x + +-- T1 is a GADT, but the equality is really just a 'let' +-- so f1 should also typecheck no problem +data T1 a where + MkT1 :: b ~ a => b -> T1 a + +f1 (MkT1 x) = not x + + + diff --git a/testsuite/tests/gadt/all.T b/testsuite/tests/gadt/all.T index 4c8eb806a7..321d67e9e8 100644 --- a/testsuite/tests/gadt/all.T +++ b/testsuite/tests/gadt/all.T @@ -117,3 +117,4 @@ test('T12468', normal, compile_fail, ['']) test('T14320', normal, compile, ['']) test('T14719', normal, compile_fail, ['-fdiagnostics-show-caret']) test('T14808', normal, compile, ['']) +test('T15009', normal, compile, ['']) diff --git a/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr b/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr index fa19be483c..5b6863c740 100644 --- a/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr +++ b/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.stderr @@ -1,11 +1,17 @@ PushedInAsGivens.hs:10:31: error: - • Couldn't match expected type ‘a1’ with actual type ‘a’ - because type variable ‘a1’ would escape its scope - This (rigid, skolem) type variable is bound by + • Could not deduce: a1 ~ a + from the context: F Int ~ [a1] + bound by the type signature for: + foo :: forall a1. (F Int ~ [a1]) => a1 -> Int + at PushedInAsGivens.hs:9:13-44 + ‘a1’ is a rigid type variable bound by the type signature for: foo :: forall a1. (F Int ~ [a1]) => a1 -> Int at PushedInAsGivens.hs:9:13-44 + ‘a’ is a rigid type variable bound by + the inferred type of bar :: a -> (a, Int) + at PushedInAsGivens.hs:(9,1)-(11,20) • In the expression: y In the first argument of ‘length’, namely ‘[x, y]’ In the expression: length [x, y] diff --git a/testsuite/tests/indexed-types/should_fail/T13784.stderr b/testsuite/tests/indexed-types/should_fail/T13784.stderr index 79007badb3..ee4ec20b63 100644 --- a/testsuite/tests/indexed-types/should_fail/T13784.stderr +++ b/testsuite/tests/indexed-types/should_fail/T13784.stderr @@ -1,44 +1,38 @@ T13784.hs:28:28: error: - • Could not deduce: as1 ~ (a1 : Divide a1 as1) - from the context: (a : as) ~ (a1 : as1) - bound by a pattern with constructor: - :* :: forall a (as :: [*]). a -> Product as -> Product (a : as), - in an equation for ‘divide’ - at T13784.hs:28:13-19 - ‘as1’ is a rigid type variable bound by - a pattern with constructor: - :* :: forall a (as :: [*]). a -> Product as -> Product (a : as), - in an equation for ‘divide’ - at T13784.hs:28:13-19 + • Couldn't match type ‘as’ with ‘a : Divide a as’ + ‘as’ is a rigid type variable bound by + the instance declaration + at T13784.hs:24:10-30 Expected type: Product (Divide a (a : as)) Actual type: Product as1 • In the expression: as In the expression: (a, as) In an equation for ‘divide’: divide (a :* as) = (a, as) • Relevant bindings include - as :: Product as1 (bound at T13784.hs:28:18) - a :: a1 (bound at T13784.hs:28:13) + divide :: Product (a : as) -> (a, Product (Divide a (a : as))) + (bound at T13784.hs:28:5) T13784.hs:32:24: error: - • Couldn't match type ‘Product (a1 : as0)’ - with ‘(b, Product (Divide b (a1 : as1)))’ + • Couldn't match type ‘Product (a : as0)’ + with ‘(b, Product (Divide b (a : as)))’ Expected type: (b, Product (Divide b (a : as))) Actual type: Product (a1 : as0) • In the expression: a :* divide as In an equation for ‘divide’: divide (a :* as) = a :* divide as In the instance declaration for ‘Divideable b (a : as)’ • Relevant bindings include - as :: Product as1 (bound at T13784.hs:32:18) - a :: a1 (bound at T13784.hs:32:13) divide :: Product (a : as) -> (b, Product (Divide b (a : as))) (bound at T13784.hs:32:5) T13784.hs:32:29: error: - • Couldn't match expected type ‘Product as0’ - with actual type ‘(a0, Product (Divide a0 as1))’ + • Couldn't match type ‘(a0, Product (Divide a0 as))’ + with ‘Product as0’ + Expected type: Product as0 + Actual type: (a0, Product (Divide a0 as1)) • In the second argument of ‘(:*)’, namely ‘divide as’ In the expression: a :* divide as In an equation for ‘divide’: divide (a :* as) = a :* divide as • Relevant bindings include - as :: Product as1 (bound at T13784.hs:32:18) + divide :: Product (a : as) -> (b, Product (Divide b (a : as))) + (bound at T13784.hs:32:5) diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr index cc0d0ca708..c0e0664a06 100644 --- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr +++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr @@ -1,27 +1,29 @@ T14040a.hs:21:18: error: - • Couldn't match type ‘k0’ with ‘a’ - because type variable ‘a’ would escape its scope - This (rigid, skolem) type variable is bound by + • Couldn't match type ‘a’ with ‘k0’ + ‘a’ is a rigid type variable bound by the type signature for: elimWeirdList :: forall a1 (wl :: WeirdList a1) (p :: forall x. x -> WeirdList x -> *). Sing wl -> (forall y. p k0 w0 'WeirdNil) -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)). - Sing x -> Sing xs -> p k1 w1 xs -> p k2 w2 ('WeirdCons x xs)) - -> p k3 w3 wl + Sing x + -> Sing xs -> p (WeirdList k1) w1 xs -> p k1 w2 ('WeirdCons x xs)) + -> p k2 w3 wl at T14040a.hs:(21,18)-(28,23) Expected type: Sing wl -> (forall y. p k1 w0 'WeirdNil) -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)). - Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2 ('WeirdCons x xs)) - -> p k3 w3 wl + Sing x + -> Sing xs -> p (WeirdList k0) w1 xs -> p k0 w2 ('WeirdCons x xs)) + -> p k2 w3 wl Actual type: Sing wl -> (forall y. p k1 w0 'WeirdNil) -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)). - Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2 ('WeirdCons x xs)) - -> p k3 w3 wl + Sing x + -> Sing xs -> p (WeirdList k0) w1 xs -> p k0 w2 ('WeirdCons x xs)) + -> p k2 w3 wl • In the ambiguity check for ‘elimWeirdList’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature: @@ -39,8 +41,10 @@ T14040a.hs:34:8: error: -> (forall y. p k0 w0 'WeirdNil) -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)). Sing x - -> Sing xs -> p k1 w1 xs -> p k2 w2 ('WeirdCons x xs)) - -> p k3 w3 wl’ + -> Sing xs + -> p (WeirdList k1) w1 xs + -> p k1 w2 ('WeirdCons x xs)) + -> p k2 w3 wl’ to a visible type argument ‘(WeirdList z)’ • In the sixth argument of ‘pWeirdCons’, namely ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’ diff --git a/testsuite/tests/polykinds/T13555.stderr b/testsuite/tests/polykinds/T13555.stderr index e822f6e596..3d2492e23d 100644 --- a/testsuite/tests/polykinds/T13555.stderr +++ b/testsuite/tests/polykinds/T13555.stderr @@ -1,8 +1,7 @@ T13555.hs:25:14: error: - • Couldn't match type ‘k0’ with ‘k2’ - because type variable ‘k2’ would escape its scope - This (rigid, skolem) type variable is bound by + • Couldn't match type ‘k2’ with ‘k0’ + ‘k2’ is a rigid type variable bound by the type signature for: crtInfo :: forall k2 (m :: k2). Reflects m Int => diff --git a/testsuite/tests/polykinds/T14846.hs b/testsuite/tests/polykinds/T14846.hs index ad17841daa..7b96e942f3 100644 --- a/testsuite/tests/polykinds/T14846.hs +++ b/testsuite/tests/polykinds/T14846.hs @@ -34,6 +34,6 @@ data Hom :: Cat k -> Cat (Struct cls) where class Category (cat::Cat ob) where i :: StructI xx a => ríki a a -instance Category ríki => Category (Hom ríki :: Cat (Struct cls)) where - i :: forall xx a. StructI xx a => Hom ríki a a +instance Category riki => Category (Hom riki :: Cat (Struct cls)) where + i :: forall xx a. StructI xx a => Hom riki a a i = case struct :: AStruct (Structured a cls) of diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr index 828ddf6374..1bfa94218c 100644 --- a/testsuite/tests/polykinds/T14846.stderr +++ b/testsuite/tests/polykinds/T14846.stderr @@ -1,24 +1,24 @@ T14846.hs:38:8: error: - • Couldn't match type ‘ríki1’ with ‘Hom ríki’ - ‘ríki1’ is a rigid type variable bound by + • Couldn't match type ‘ríki’ with ‘Hom riki’ + ‘ríki’ is a rigid type variable bound by the type signature for: i :: forall k5 (cls1 :: k5 - -> Constraint) k6 (xx :: k6) (a :: Struct cls1) (ríki1 :: Struct - cls1 - -> Struct - cls1 - -> *). + -> Constraint) k6 (xx :: k6) (a :: Struct cls1) (ríki :: Struct + cls1 + -> Struct + cls1 + -> *). StructI xx a => - ríki1 a a + ríki a a at T14846.hs:38:8-48 - Expected type: ríki1 a a - Actual type: Hom ríki a0 a0 + Expected type: ríki a a + Actual type: Hom riki a0 a0 • When checking that instance signature for ‘i’ is more general than its signature in the class Instance sig: forall (xx :: k0) (a :: Struct cls0). StructI xx a => - Hom ríki a a + Hom riki a a Class sig: forall k1 (cls :: k1 -> Constraint) k2 (xx :: k2) (a :: Struct cls) (ríki :: Struct @@ -28,32 +28,7 @@ T14846.hs:38:8: error: -> *). StructI xx a => ríki a a - In the instance declaration for ‘Category (Hom ríki)’ - -T14846.hs:39:12: error: - • Could not deduce (StructI xx1 (Structured a cls)) - arising from a use of ‘struct’ - from the context: Category ríki - bound by the instance declaration at T14846.hs:37:10-65 - or from: StructI xx a - bound by the type signature for: - i :: forall (xx :: k0) (a :: Struct cls0). - StructI xx a => - Hom ríki a a - at T14846.hs:38:8-48 - The type variable ‘xx1’ is ambiguous - Relevant bindings include - i :: Hom ríki a a (bound at T14846.hs:39:3) - These potential instance exist: - instance forall k (xx :: k) (cls :: k - -> Constraint) (structured :: Struct cls). - (Structured xx cls ~ structured, cls xx) => - StructI xx structured - -- Defined at T14846.hs:28:10 - • In the expression: struct :: AStruct (Structured a cls) - In the expression: case struct :: AStruct (Structured a cls) of - In an equation for ‘i’: - i = case struct :: AStruct (Structured a cls) of + In the instance declaration for ‘Category (Hom riki)’ T14846.hs:39:44: error: • Expected kind ‘Struct cls0 -> Constraint’, @@ -62,4 +37,4 @@ T14846.hs:39:44: error: In the first argument of ‘AStruct’, namely ‘(Structured a cls)’ In an expression type signature: AStruct (Structured a cls) • Relevant bindings include - i :: Hom ríki a a (bound at T14846.hs:39:3) + i :: Hom riki a a (bound at T14846.hs:39:3) diff --git a/testsuite/tests/polykinds/T7230.stderr b/testsuite/tests/polykinds/T7230.stderr index 53b8bcd8c3..48781e8f7f 100644 --- a/testsuite/tests/polykinds/T7230.stderr +++ b/testsuite/tests/polykinds/T7230.stderr @@ -9,13 +9,13 @@ T7230.hs:48:32: error: at T7230.hs:47:1-68 or from: xs ~ (x : xs1) bound by a pattern with constructor: - SCons :: forall k (x :: k) (xs :: [k]). + SCons :: forall a (x :: a) (xs :: [a]). Sing x -> Sing xs -> Sing (x : xs), in an equation for ‘crash’ at T7230.hs:48:8-27 or from: xs1 ~ (x1 : xs2) bound by a pattern with constructor: - SCons :: forall k (x :: k) (xs :: [k]). + SCons :: forall a (x :: a) (xs :: [a]). Sing x -> Sing xs -> Sing (x : xs), in an equation for ‘crash’ at T7230.hs:48:17-26 diff --git a/testsuite/tests/polykinds/T8566.stderr b/testsuite/tests/polykinds/T8566.stderr index 52a4b21490..d368d055f0 100644 --- a/testsuite/tests/polykinds/T8566.stderr +++ b/testsuite/tests/polykinds/T8566.stderr @@ -1,12 +1,12 @@ T8566.hs:32:9: error: - • Could not deduce (C ('AA (t1 (I a ps)) as) ps fs0) + • Could not deduce (C ('AA (t (I a ps)) as) ps fs0) arising from a use of ‘c’ from the context: C ('AA (t (I a ps)) as) ps fs bound by the instance declaration at T8566.hs:30:10-67 or from: 'AA t (a : as) ~ 'AA t1 as1 bound by a pattern with constructor: - A :: forall k (t :: k) (as :: [U *]) (r :: [*]). I ('AA t as) r, + A :: forall v (t :: v) (as :: [U *]) (r :: [*]). I ('AA t as) r, in an equation for ‘c’ at T8566.hs:32:5 The type variable ‘fs0’ is ambiguous diff --git a/testsuite/tests/polykinds/T9222.stderr b/testsuite/tests/polykinds/T9222.stderr index a019b9e117..604cc1b7ec 100644 --- a/testsuite/tests/polykinds/T9222.stderr +++ b/testsuite/tests/polykinds/T9222.stderr @@ -8,7 +8,7 @@ T9222.hs:13:3: error: at T9222.hs:13:3-43 ‘c’ is a rigid type variable bound by the type of the constructor ‘Want’: - forall k2 k3 (a :: (k2, k3)) (b :: k2) (c :: k3). + forall i1 j1 (a :: (i1, j1)) (b :: i1) (c :: j1). ((a ~ '(b, c)) => Proxy b) -> Want a at T9222.hs:13:3-43 • In the ambiguity check for ‘Want’ diff --git a/testsuite/tests/typecheck/should_compile/ExPatFail.stderr b/testsuite/tests/typecheck/should_compile/ExPatFail.stderr index 6cc24fcaf6..e38c32b595 100644 --- a/testsuite/tests/typecheck/should_compile/ExPatFail.stderr +++ b/testsuite/tests/typecheck/should_compile/ExPatFail.stderr @@ -1,12 +1,14 @@ ExPatFail.hs:12:15: error: • Couldn't match expected type ‘p’ with actual type ‘a’ - because type variable ‘a’ would escape its scope - This (rigid, skolem) type variable is bound by + ‘a’ is a rigid type variable bound by a pattern with constructor: MkT :: forall a. Integral a => a -> Int -> T, in a pattern binding at ExPatFail.hs:12:11-17 + ‘p’ is a rigid type variable bound by + the inferred type of f :: T -> p + at ExPatFail.hs:(12,1)-(13,10) • In the pattern: MkT y _ In a pattern binding: MkT y _ = x In the expression: let MkT y _ = x in y diff --git a/testsuite/tests/typecheck/should_compile/T9834.stderr b/testsuite/tests/typecheck/should_compile/T9834.stderr index 01b003fa3a..52f207d511 100644 --- a/testsuite/tests/typecheck/should_compile/T9834.stderr +++ b/testsuite/tests/typecheck/should_compile/T9834.stderr @@ -19,17 +19,17 @@ T9834.hs:23:10: warning: [-Wdeferred-type-errors (in -Wdefault)] (bound at T9834.hs:23:3) T9834.hs:23:10: warning: [-Wdeferred-type-errors (in -Wdefault)] - • Couldn't match type ‘a’ with ‘a1’ + • Couldn't match type ‘a1’ with ‘a’ + ‘a1’ is a rigid type variable bound by + a type expected by the context: + forall (q :: * -> *). Applicative q => Nat (Comp p q) (Comp p q) + at T9834.hs:23:10-19 ‘a’ is a rigid type variable bound by the type signature for: afix :: forall a. (forall (q :: * -> *). Applicative q => Comp p q a -> Comp p q a) -> p a at T9834.hs:22:11-74 - ‘a1’ is a rigid type variable bound by - a type expected by the context: - forall (q :: * -> *). Applicative q => Nat (Comp p q) (Comp p q) - at T9834.hs:23:10-19 Expected type: Comp p q a1 -> Comp p q a1 Actual type: Comp p q a -> Comp p q a • In the expression: wrapIdComp diff --git a/testsuite/tests/typecheck/should_compile/tc141.stderr b/testsuite/tests/typecheck/should_compile/tc141.stderr index 9c13f1791d..b2fe9abb4b 100644 --- a/testsuite/tests/typecheck/should_compile/tc141.stderr +++ b/testsuite/tests/typecheck/should_compile/tc141.stderr @@ -8,11 +8,13 @@ tc141.hs:11:12: error: tc141.hs:11:31: error: • Couldn't match expected type ‘a2’ with actual type ‘a’ - because type variable ‘a2’ would escape its scope - This (rigid, skolem) type variable is bound by + ‘a2’ is a rigid type variable bound by an expression type signature: forall a2. a2 at tc141.hs:11:34 + ‘a’ is a rigid type variable bound by + the inferred type of f :: (a, a) -> (a1, a) + at tc141.hs:11:1-37 • In the expression: q :: a In the expression: (q :: a, p) In the expression: let (p :: a, q :: a) = x in (q :: a, p) @@ -36,11 +38,13 @@ tc141.hs:13:13: error: tc141.hs:15:18: error: • Couldn't match expected type ‘a2’ with actual type ‘p’ - because type variable ‘a2’ would escape its scope - This (rigid, skolem) type variable is bound by + ‘a2’ is a rigid type variable bound by the type signature for: v :: forall a2. a2 at tc141.hs:14:14-19 + ‘p’ is a rigid type variable bound by + the inferred type of g :: a -> p -> a1 + at tc141.hs:(13,1)-(16,13) • In the expression: b In an equation for ‘v’: v = b In the expression: diff --git a/testsuite/tests/typecheck/should_fail/T14607.hs b/testsuite/tests/typecheck/should_fail/T14607.hs index c05df0be25..86c738dc19 100644 --- a/testsuite/tests/typecheck/should_fail/T14607.hs +++ b/testsuite/tests/typecheck/should_fail/T14607.hs @@ -25,3 +25,10 @@ instance Mk a where -- At some point, this program was accepted. That's fine. But right now, -- it's rejected with a kind error, and we can't generally defer kind -- errors, so I'm saying that behavior is OK. + +-- Later (May 18) the kind error ended up being in an term-level +-- implication constraint, which /does/ have an evidence binding +-- So now the kind error can be deferred. +-- Consequence of a fast-path for tcImplicitTKBndrsX I think. + + diff --git a/testsuite/tests/typecheck/should_fail/T14607.stderr b/testsuite/tests/typecheck/should_fail/T14607.stderr index 0a63e53030..740f89a0d4 100644 --- a/testsuite/tests/typecheck/should_fail/T14607.stderr +++ b/testsuite/tests/typecheck/should_fail/T14607.stderr @@ -1,12 +1,21 @@ -T14607.hs:22:9: error: +T14607.hs:22:9: warning: [-Wdeferred-type-errors (in -Wdefault)] • Expecting one more argument to ‘LamCons a '()’ Expected a type, but ‘LamCons a '()’ has kind ‘() -> *’ • In the type signature: mk :: LamCons a '() In the instance declaration for ‘Mk a’ -T14607.hs:22:19: error: +T14607.hs:22:19: warning: [-Wdeferred-type-errors (in -Wdefault)] • Expected a type, but ‘ '()’ has kind ‘()’ • In the second argument of ‘LamCons’, namely ‘ '()’ In the type signature: mk :: LamCons a '() In the instance declaration for ‘Mk a’ + +T14607.hs:23:8: warning: [-Wdeferred-type-errors (in -Wdefault)] + • Couldn't match expected type ‘LamCons a '()’ + with actual type ‘LamCons a0 a0 '()’ + • In the expression: mk + In an equation for ‘mk’: mk = mk + In the instance declaration for ‘Mk a’ + • Relevant bindings include + mk :: LamCons a '() (bound at T14607.hs:23:3) diff --git a/testsuite/tests/typecheck/should_fail/T7453.stderr b/testsuite/tests/typecheck/should_fail/T7453.stderr index 77348c357a..d72b6d9a7a 100644 --- a/testsuite/tests/typecheck/should_fail/T7453.stderr +++ b/testsuite/tests/typecheck/should_fail/T7453.stderr @@ -1,11 +1,13 @@ T7453.hs:10:30: error: • Couldn't match expected type ‘t’ with actual type ‘p’ - because type variable ‘t’ would escape its scope - This (rigid, skolem) type variable is bound by + ‘t’ is a rigid type variable bound by the type signature for: z :: forall t. Id t at T7453.hs:8:11-19 + ‘p’ is a rigid type variable bound by + the inferred type of cast1 :: p -> a + at T7453.hs:(7,1)-(10,30) • In the first argument of ‘Id’, namely ‘v’ In the expression: Id v In an equation for ‘aux’: aux = Id v @@ -17,11 +19,13 @@ T7453.hs:10:30: error: T7453.hs:16:33: error: • Couldn't match expected type ‘t1’ with actual type ‘p’ - because type variable ‘t1’ would escape its scope - This (rigid, skolem) type variable is bound by + ‘t1’ is a rigid type variable bound by the type signature for: z :: forall t1. () -> t1 at T7453.hs:14:11-22 + ‘p’ is a rigid type variable bound by + the inferred type of cast2 :: p -> t + at T7453.hs:(13,1)-(16,33) • In the first argument of ‘const’, namely ‘v’ In the expression: const v In an equation for ‘aux’: aux = const v @@ -33,11 +37,13 @@ T7453.hs:16:33: error: T7453.hs:21:15: error: • Couldn't match expected type ‘t1’ with actual type ‘p’ - because type variable ‘t1’ would escape its scope - This (rigid, skolem) type variable is bound by + ‘t1’ is a rigid type variable bound by the type signature for: z :: forall t1. t1 at T7453.hs:20:11-16 + ‘p’ is a rigid type variable bound by + the inferred type of cast3 :: p -> t + at T7453.hs:(19,1)-(22,33) • In the expression: v In an equation for ‘z’: z = v diff --git a/testsuite/tests/typecheck/should_fail/T7869.stderr b/testsuite/tests/typecheck/should_fail/T7869.stderr index 4cf1cfaf67..7e01868526 100644 --- a/testsuite/tests/typecheck/should_fail/T7869.stderr +++ b/testsuite/tests/typecheck/should_fail/T7869.stderr @@ -1,11 +1,13 @@ T7869.hs:3:12: error: - • Couldn't match type ‘b’ with ‘b1’ - because type variable ‘b1’ would escape its scope - This (rigid, skolem) type variable is bound by + • Couldn't match type ‘b1’ with ‘b’ + ‘b1’ is a rigid type variable bound by an expression type signature: forall a1 b1. [a1] -> b1 at T7869.hs:3:20-27 + ‘b’ is a rigid type variable bound by + the inferred type of f :: [a] -> b + at T7869.hs:3:1-27 Expected type: [a1] -> b1 Actual type: [a] -> b • In the expression: f x diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index 5a3e73313f..86099ea026 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -1,4 +1,4 @@ - +4607 test('tcfail001', normal, compile_fail, ['']) test('tcfail002', normal, compile_fail, ['']) test('tcfail003', normal, compile_fail, ['']) @@ -467,7 +467,7 @@ test('T14350', normal, compile_fail, ['']) test('T14390', normal, compile_fail, ['']) test('MissingExportList03', normal, compile_fail, ['']) test('T14618', normal, compile_fail, ['']) -test('T14607', normal, compile_fail, ['']) +test('T14607', normal, compile, ['']) test('T14605', normal, compile_fail, ['']) test('T14761a', normal, compile_fail, ['']) test('T14761b', normal, compile_fail, ['']) diff --git a/testsuite/tests/typecheck/should_fail/tcfail068.stderr b/testsuite/tests/typecheck/should_fail/tcfail068.stderr index bb3f9ddb53..4318021213 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail068.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail068.stderr @@ -23,48 +23,48 @@ tcfail068.hs:14:9: error: (bound at tcfail068.hs:12:1) tcfail068.hs:19:9: error: - • Couldn't match type ‘s’ with ‘s1’ + • Couldn't match type ‘s1’ with ‘s’ + ‘s1’ is a rigid type variable bound by + a type expected by the context: + forall s1. GHC.ST.ST s1 (IndTree s a) + at tcfail068.hs:(18,9)-(21,19) ‘s’ is a rigid type variable bound by the type signature for: itiap :: forall a s. Constructed a => (Int, Int) -> (a -> a) -> IndTree s a -> IndTree s a at tcfail068.hs:16:1-75 - ‘s1’ is a rigid type variable bound by - a type expected by the context: - forall s1. GHC.ST.ST s1 (IndTree s a) - at tcfail068.hs:(18,9)-(21,19) Expected type: GHC.ST.ST s1 (IndTree s a) Actual type: GHC.ST.ST s (IndTree s a) • In the first argument of ‘runST’, namely ‘(readSTArray arr i - >>= \ val -> writeSTArray arr i (f val) >> return arr)’ + >>= \ val -> writeSTArray arr i (f val) >> return arr)’ In the expression: runST (readSTArray arr i - >>= \ val -> writeSTArray arr i (f val) >> return arr) + >>= \ val -> writeSTArray arr i (f val) >> return arr) In an equation for ‘itiap’: itiap i f arr = runST (readSTArray arr i - >>= \ val -> writeSTArray arr i (f val) >> return arr) + >>= \ val -> writeSTArray arr i (f val) >> return arr) • Relevant bindings include arr :: IndTree s a (bound at tcfail068.hs:17:11) itiap :: (Int, Int) -> (a -> a) -> IndTree s a -> IndTree s a (bound at tcfail068.hs:17:1) tcfail068.hs:24:36: error: - • Couldn't match type ‘s’ with ‘s1’ + • Couldn't match type ‘s1’ with ‘s’ + ‘s1’ is a rigid type variable bound by + a type expected by the context: + forall s1. GHC.ST.ST s1 (IndTree s a) + at tcfail068.hs:24:29-46 ‘s’ is a rigid type variable bound by the type signature for: itrap :: forall a s. Constructed a => ((Int, Int), (Int, Int)) -> (a -> a) -> IndTree s a -> IndTree s a at tcfail068.hs:23:1-87 - ‘s1’ is a rigid type variable bound by - a type expected by the context: - forall s1. GHC.ST.ST s1 (IndTree s a) - at tcfail068.hs:24:29-46 Expected type: GHC.ST.ST s1 (IndTree s a) Actual type: GHC.ST.ST s (IndTree s a) • In the first argument of ‘runST’, namely ‘(itrap' i k)’ @@ -91,7 +91,11 @@ tcfail068.hs:24:36: error: (bound at tcfail068.hs:24:1) tcfail068.hs:36:46: error: - • Couldn't match type ‘s’ with ‘s1’ + • Couldn't match type ‘s1’ with ‘s’ + ‘s1’ is a rigid type variable bound by + a type expected by the context: + forall s1. GHC.ST.ST s1 (c, IndTree s b) + at tcfail068.hs:36:40-63 ‘s’ is a rigid type variable bound by the type signature for: itrapstate :: forall b a c s. @@ -104,10 +108,6 @@ tcfail068.hs:36:46: error: -> IndTree s b -> (c, IndTree s b) at tcfail068.hs:(34,1)-(35,62) - ‘s1’ is a rigid type variable bound by - a type expected by the context: - forall s1. GHC.ST.ST s1 (c, IndTree s b) - at tcfail068.hs:36:40-63 Expected type: GHC.ST.ST s1 (c, IndTree s b) Actual type: GHC.ST.ST s (c, IndTree s b) • In the first argument of ‘runST’, namely ‘(itrapstate' i k s)’ diff --git a/testsuite/tests/typecheck/should_fail/tcfail076.stderr b/testsuite/tests/typecheck/should_fail/tcfail076.stderr index 546715aa4a..d4368a4cf5 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail076.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail076.stderr @@ -1,14 +1,14 @@ tcfail076.hs:18:82: error: - • Couldn't match type ‘res’ with ‘res1’ - ‘res’ is a rigid type variable bound by - a type expected by the context: - forall res. (a -> m res) -> m res - at tcfail076.hs:18:28-96 + • Couldn't match type ‘res1’ with ‘res’ ‘res1’ is a rigid type variable bound by a type expected by the context: forall res1. (b -> m res1) -> m res1 at tcfail076.hs:18:64-88 + ‘res’ is a rigid type variable bound by + a type expected by the context: + forall res. (a -> m res) -> m res + at tcfail076.hs:18:28-96 Expected type: m res1 Actual type: m res • In the expression: cont a diff --git a/testsuite/tests/typecheck/should_fail/tcfail099.stderr b/testsuite/tests/typecheck/should_fail/tcfail099.stderr index bc30866ec2..a04920fb39 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail099.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail099.stderr @@ -1,11 +1,13 @@ tcfail099.hs:9:20: error: • Couldn't match expected type ‘a’ with actual type ‘p’ - because type variable ‘a’ would escape its scope - This (rigid, skolem) type variable is bound by + ‘a’ is a rigid type variable bound by a pattern with constructor: C :: forall a. (a -> Int) -> DS, in an equation for ‘call’ at tcfail099.hs:9:7-9 + ‘p’ is a rigid type variable bound by + the inferred type of call :: DS -> p -> Int + at tcfail099.hs:9:1-22 • In the first argument of ‘f’, namely ‘arg’ In the expression: f arg In an equation for ‘call’: call (C f) arg = f arg diff --git a/testsuite/tests/typecheck/should_fail/tcfail103.stderr b/testsuite/tests/typecheck/should_fail/tcfail103.stderr index ba0694b117..2192d8a7f6 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail103.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail103.stderr @@ -1,14 +1,14 @@ tcfail103.hs:15:13: error: - • Couldn't match type ‘t’ with ‘s’ - ‘t’ is a rigid type variable bound by - the type signature for: - f :: forall t. ST t Int - at tcfail103.hs:10:1-12 + • Couldn't match type ‘s’ with ‘t’ ‘s’ is a rigid type variable bound by the type signature for: g :: forall s. ST s Int at tcfail103.hs:13:9-21 + ‘t’ is a rigid type variable bound by + the type signature for: + f :: forall t. ST t Int + at tcfail103.hs:10:1-12 Expected type: ST s Int Actual type: ST t Int • In the expression: readSTRef v diff --git a/testsuite/tests/typecheck/should_fail/tcfail174.stderr b/testsuite/tests/typecheck/should_fail/tcfail174.stderr index e8073887ac..724535145c 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail174.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail174.stderr @@ -7,11 +7,13 @@ tcfail174.hs:9:5: error: In an equation for ‘g’: g = Base id tcfail174.hs:16:14: error: - • Couldn't match type ‘a’ with ‘a1’ - because type variable ‘a1’ would escape its scope - This (rigid, skolem) type variable is bound by + • Couldn't match type ‘a1’ with ‘a’ + ‘a1’ is a rigid type variable bound by the type a -> a at tcfail174.hs:16:1-14 + ‘a’ is a rigid type variable bound by + the inferred type of h1 :: Capture a + at tcfail174.hs:16:1-14 Expected type: Capture (forall x. x -> a) Actual type: Capture (forall a. a -> a) • In the first argument of ‘Capture’, namely ‘g’ @@ -23,7 +25,8 @@ tcfail174.hs:16:14: error: tcfail174.hs:19:14: error: • Couldn't match type ‘a’ with ‘b’ ‘a’ is a rigid type variable bound by - the type a -> a at tcfail174.hs:1:1 + the type a -> a + at tcfail174.hs:1:1 ‘b’ is a rigid type variable bound by the type signature for: h2 :: forall b. Capture b diff --git a/testsuite/tests/typecheck/should_fail/tcfail198.stderr b/testsuite/tests/typecheck/should_fail/tcfail198.stderr index e8c3852b1c..66c8438dc4 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail198.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail198.stderr @@ -1,11 +1,13 @@ tcfail198.hs:6:36: error: • Couldn't match expected type ‘a1’ with actual type ‘a’ - because type variable ‘a1’ would escape its scope - This (rigid, skolem) type variable is bound by + ‘a1’ is a rigid type variable bound by an expression type signature: forall a1. a1 at tcfail198.hs:6:41 + ‘a’ is a rigid type variable bound by + the inferred type of f3 :: [a] -> [a] + at tcfail198.hs:6:1-44 • In the expression: x :: a In the second argument of ‘(++)’, namely ‘[x :: a]’ In the expression: xs ++ [x :: a] |