diff options
| author | sheaf <sam.derbyshire@gmail.com> | 2022-04-26 16:19:53 +0200 |
|---|---|---|
| committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2022-04-28 18:56:37 -0400 |
| commit | a8c993910ea79264775105a09ad6c80fb52400db (patch) | |
| tree | 7d31e51d42c631ce14a68f8fc1b5480df02b046e | |
| parent | 6130518409cd44de620489a2981fd3075dfb94a1 (diff) | |
| download | haskell-a8c993910ea79264775105a09ad6c80fb52400db.tar.gz | |
Fix unification of ConcreteTvs, removing IsRefl#
This patch fixes the unification of concrete type variables.
The subtlety was that unifying concrete metavariables is more subtle
than other metavariables, as decomposition is possible. See the Note
[Unifying concrete metavariables], which explains how we unify a
concrete type variable with a type 'ty' by concretising 'ty', using
the function 'GHC.Tc.Utils.Concrete.concretise'.
This can be used to perform an eager syntactic check for concreteness,
allowing us to remove the IsRefl# special predicate. Instead of emitting
two constraints `rr ~# concrete_tv` and `IsRefl# rr concrete_tv`, we
instead concretise 'rr'. If this succeeds we can fill 'concrete_tv',
and otherwise we directly emit an error message to the typechecker
environment instead of deferring. We still need the error message
to be passed on (instead of directly thrown), as we might benefit from
further unification in which case we will need to zonk the stored types.
To achieve this, we change the 'wc_holes' field of 'WantedConstraints'
to 'wc_errors', which stores general delayed errors. For the moement,
a delayed error is either a hole, or a syntactic equality error.
hasFixedRuntimeRep_MustBeRefl is now hasFixedRuntimeRep_syntactic, and
hasFixedRuntimeRep has been refactored to directly return the most
useful coercion for PHASE 2 of FixedRuntimeRep.
This patch also adds a field ir_frr to the InferResult datatype,
holding a value of type Maybe FRROrigin. When this value is not
Nothing, this means that we must fill the ir_ref field with a type
which has a fixed RuntimeRep.
When it comes time to fill such an ExpType, we ensure that the type
has a fixed RuntimeRep by performing a representation-polymorphism
check with the given FRROrigin
This is similar to what we already do to ensure we fill an Infer
ExpType with a type of the correct TcLevel.
This allows us to properly perform representation-polymorphism checks
on 'Infer' 'ExpTypes'.
The fillInferResult function had to be moved to GHC.Tc.Utils.Unify
to avoid a cyclic import now that it calls hasFixedRuntimeRep.
This patch also changes the code in matchExpectedFunTys to make use
of the coercions, which is now possible thanks to the previous change.
This implements PHASE 2 of FixedRuntimeRep in some situations.
For example, the test cases T13105 and T17536b are now both accepted.
Fixes #21239 and #21325
-------------------------
Metric Decrease:
T18223
T5631
-------------------------
87 files changed, 1847 insertions, 1206 deletions
diff --git a/compiler/GHC/Builtin/Names.hs b/compiler/GHC/Builtin/Names.hs index 176685bbf9..62511b3cfc 100644 --- a/compiler/GHC/Builtin/Names.hs +++ b/compiler/GHC/Builtin/Names.hs @@ -1841,8 +1841,7 @@ statePrimTyConKey, stableNamePrimTyConKey, stableNameTyConKey, typeConKey, threadIdPrimTyConKey, bcoPrimTyConKey, ptrTyConKey, funPtrTyConKey, tVarPrimTyConKey, eqPrimTyConKey, eqReprPrimTyConKey, eqPhantPrimTyConKey, - compactPrimTyConKey, stackSnapshotPrimTyConKey, - isReflPrimTyConKey :: Unique + compactPrimTyConKey, stackSnapshotPrimTyConKey :: Unique statePrimTyConKey = mkPreludeTyConUnique 50 stableNamePrimTyConKey = mkPreludeTyConUnique 51 stableNameTyConKey = mkPreludeTyConUnique 52 @@ -1871,7 +1870,6 @@ funPtrTyConKey = mkPreludeTyConUnique 78 tVarPrimTyConKey = mkPreludeTyConUnique 79 compactPrimTyConKey = mkPreludeTyConUnique 80 stackSnapshotPrimTyConKey = mkPreludeTyConUnique 81 -isReflPrimTyConKey = mkPreludeTyConUnique 82 eitherTyConKey :: Unique eitherTyConKey = mkPreludeTyConUnique 84 diff --git a/compiler/GHC/Builtin/Types/Prim.hs b/compiler/GHC/Builtin/Types/Prim.hs index bf33710e4d..aa867cc6ed 100644 --- a/compiler/GHC/Builtin/Types/Prim.hs +++ b/compiler/GHC/Builtin/Types/Prim.hs @@ -100,8 +100,6 @@ module GHC.Builtin.Types.Prim( eqPhantPrimTyCon, -- ty1 ~P# ty2 (at role Phantom) equalityTyCon, - isReflPrimTyCon, - -- * SIMD #include "primop-vector-tys-exports.hs-incl" ) where @@ -163,7 +161,6 @@ unexposedPrimTyCons = [ eqPrimTyCon , eqReprPrimTyCon , eqPhantPrimTyCon - , isReflPrimTyCon ] -- | Primitive 'TyCon's that are defined in, and exported from, GHC.Prim. @@ -236,8 +233,7 @@ charPrimTyConName, intPrimTyConName, int8PrimTyConName, int16PrimTyConName, int3 stableNamePrimTyConName, compactPrimTyConName, bcoPrimTyConName, weakPrimTyConName, threadIdPrimTyConName, eqPrimTyConName, eqReprPrimTyConName, eqPhantPrimTyConName, - stackSnapshotPrimTyConName, - isReflPrimTyConName :: Name + stackSnapshotPrimTyConName :: Name charPrimTyConName = mkPrimTc (fsLit "Char#") charPrimTyConKey charPrimTyCon intPrimTyConName = mkPrimTc (fsLit "Int#") intPrimTyConKey intPrimTyCon int8PrimTyConName = mkPrimTc (fsLit "Int8#") int8PrimTyConKey int8PrimTyCon @@ -275,7 +271,6 @@ stackSnapshotPrimTyConName = mkPrimTc (fsLit "StackSnapshot#") stackSnapshotP bcoPrimTyConName = mkPrimTc (fsLit "BCO") bcoPrimTyConKey bcoPrimTyCon weakPrimTyConName = mkPrimTc (fsLit "Weak#") weakPrimTyConKey weakPrimTyCon threadIdPrimTyConName = mkPrimTc (fsLit "ThreadId#") threadIdPrimTyConKey threadIdPrimTyCon -isReflPrimTyConName = mkPrimTc (fsLit "IsRefl#") isReflPrimTyConKey isReflPrimTyCon {- ************************************************************************ @@ -991,26 +986,6 @@ equalityTyCon Phantom = eqPhantPrimTyCon {- ********************************************************************* * * - IsRefl# -* * -********************************************************************* -} - --- | The 'TyCon' for the 'IsRefl#' constraint. --- --- @type IsRefl# :: forall k. k -> k -> TYPE (TupleRep '[])@ --- --- See Note [IsRefl#] in GHC.Tc.Utils.Concrete. -isReflPrimTyCon :: TyCon -isReflPrimTyCon = - mkPrimTyCon isReflPrimTyConName binders res_kind roles - where - -- Kind :: forall k. k -> k-> TYPE (TupleRep '[]) - binders = mkTemplateTyConBinders [liftedTypeKind] (\[k] -> [k, k]) - res_kind = unboxedTupleKind [] - roles = [Nominal, Nominal, Nominal] - -{- ********************************************************************* -* * The primitive array types * * ********************************************************************* -} diff --git a/compiler/GHC/Core/PatSyn.hs b/compiler/GHC/Core/PatSyn.hs index 39cafc46e2..c63981bc71 100644 --- a/compiler/GHC/Core/PatSyn.hs +++ b/compiler/GHC/Core/PatSyn.hs @@ -59,9 +59,7 @@ data PatSyn psName :: Name, psUnique :: Unique, -- Cached from Name - psArgs :: [Type], -- ^ Argument types. - -- These always have a fixed RuntimeRep as per - -- Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. + psArgs :: [FRRType], -- ^ Argument types psArity :: Arity, -- == length psArgs psInfix :: Bool, -- True <=> declared infix psFieldLabels :: [FieldLabel], -- List of fields for a @@ -382,9 +380,7 @@ mkPatSyn :: Name -- variables and required dicts -> ([InvisTVBinder], ThetaType) -- ^ Existentially-quantified type -- variables and provided dicts - -> [Type] -- ^ Original arguments - -- These must have a fixed RuntimeRep as per - -- Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. + -> [FRRType] -- ^ Original arguments -> Type -- ^ Original result type -> PatSynMatcher -- ^ Matcher -> PatSynBuilder -- ^ Builder diff --git a/compiler/GHC/Core/Predicate.hs b/compiler/GHC/Core/Predicate.hs index c3994c2366..9dd1a7b815 100644 --- a/compiler/GHC/Core/Predicate.hs +++ b/compiler/GHC/Core/Predicate.hs @@ -18,9 +18,6 @@ module GHC.Core.Predicate ( mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole, mkHeteroPrimEqPred, mkHeteroReprPrimEqPred, - -- Special predicates - SpecialPred(..), mkIsReflPrimPred, isIsReflPrimPred, - -- Class predicates mkClassPred, isDictTy, isClassPred, isEqPredClass, isCTupleClass, @@ -41,7 +38,6 @@ import GHC.Prelude import GHC.Core.Type import GHC.Core.Class -import GHC.Core.TyCo.Ppr ( pprParendType ) import GHC.Core.TyCon import GHC.Core.TyCon.RecWalk import GHC.Types.Var @@ -49,7 +45,6 @@ import GHC.Core.Coercion import GHC.Core.Multiplicity ( scaledThing ) import GHC.Builtin.Names -import GHC.Builtin.Types.Prim ( isReflPrimTyCon ) import GHC.Utils.Outputable import GHC.Utils.Misc @@ -58,7 +53,6 @@ import GHC.Data.FastString import Control.Monad ( guard ) - -- | A predicate in the solver. The solver tries to prove Wanted predicates -- from Given ones. data Pred @@ -77,11 +71,6 @@ data Pred -- See Note [Quantified constraints] in GHC.Tc.Solver.Canonical | ForAllPred [TyVar] [PredType] PredType - -- | A special predicate, used internally in GHC. - -- - -- See #20000. - | SpecialPred SpecialPred - -- NB: There is no TuplePred case -- Tuple predicates like (Eq a, Ord b) are just treated -- as ClassPred, as if we had a tuple class with two superclasses @@ -93,10 +82,6 @@ classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of | tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2 | tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2 - Just (tc, [_ki, lhs, rhs]) - | tc `hasKey` isReflPrimTyConKey - -> SpecialPred (IsReflPrimPred lhs rhs) - Just (tc, tys) | Just clas <- tyConClass_maybe tc -> ClassPred clas tys @@ -191,29 +176,6 @@ predTypeEqRel ty | otherwise = NomEq --- --------------------- Special predicates ---------------------------------- - --- | 'SpecialPred' describes all the special predicates --- that are currently used in GHC. --- --- These are different from the special typeclasses --- (such as `KnownNat`, `Typeable`, `Coercible`, ...), as special predicates --- can't be expressed as typeclasses, as they hold evidence of a different kind. -data SpecialPred - -- | 'IsRefl#'. - = IsReflPrimPred Type Type - -instance Outputable SpecialPred where - ppr (IsReflPrimPred l r) = - text "IsRefl#" <+> pprParendType l <+> pprParendType r - -mkIsReflPrimPred :: Type -> Type -> PredType -mkIsReflPrimPred lhs rhs = mkTyConApp isReflPrimTyCon [typeKind lhs, lhs, rhs] - -isIsReflPrimPred :: Pred -> Bool -isIsReflPrimPred (SpecialPred (IsReflPrimPred {})) = True -isIsReflPrimPred _ = False - {------------------------------------------- Predicates on PredType --------------------------------------------} diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs index 391543190d..84f4428a41 100644 --- a/compiler/GHC/Core/TyCo/Rep.hs +++ b/compiler/GHC/Core/TyCo/Rep.hs @@ -32,7 +32,7 @@ module GHC.Core.TyCo.Rep ( KindOrType, Kind, RuntimeRepType, KnotTied, - PredType, ThetaType, -- Synonyms + PredType, ThetaType, FRRType, -- Synonyms ArgFlag(..), AnonArgFlag(..), -- * Coercions @@ -116,6 +116,10 @@ type Kind = Type -- | Type synonym used for types of kind RuntimeRep. type RuntimeRepType = Type +-- A type with a syntactically fixed RuntimeRep, in the sense +-- of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. +type FRRType = Type + -- If you edit this type, you may need to update the GHC formalism -- See Note [GHC Formalism] in GHC.Core.Lint data Type diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs index cc1b712eec..48da8e8275 100644 --- a/compiler/GHC/Core/TyCon.hs +++ b/compiler/GHC/Core/TyCon.hs @@ -1033,7 +1033,7 @@ Note [Representation-polymorphic TyCons] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ To check for representation-polymorphism directly in the typechecker, e.g. when using GHC.Tc.Utils.TcMType.checkTypeHasFixedRuntimeRep, -we need to compute whether a type has a fixed RuntimeRep, +we need to compute whether a type has a syntactically fixed RuntimeRep, as per Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. It's useful to have a quick way to check whether a saturated application @@ -2444,7 +2444,7 @@ setTcTyConKind tc@(TcTyCon {}) kind = let tc' = tc { tyConKind = kind in tc' setTcTyConKind tc _ = pprPanic "setTcTyConKind" (ppr tc) --- | Does this 'TyCon' have a fixed RuntimeRep when fully applied, +-- | Does this 'TyCon' have a syntactically fixed RuntimeRep when fully applied, -- as per Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete? -- -- False is safe. True means we're sure. diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs index fbe499ee79..d6ae874d15 100644 --- a/compiler/GHC/Core/Type.hs +++ b/compiler/GHC/Core/Type.hs @@ -17,7 +17,7 @@ module GHC.Core.Type ( -- $representation_types Type, ArgFlag(..), AnonArgFlag(..), Specificity(..), - KindOrType, PredType, ThetaType, + KindOrType, PredType, ThetaType, FRRType, Var, TyVar, isTyVar, TyCoVar, TyCoBinder, TyCoVarBinder, TyVarBinder, Mult, Scaled, KnotTied, @@ -3177,7 +3177,7 @@ typeLiteralKind (NumTyLit {}) = naturalTy typeLiteralKind (StrTyLit {}) = typeSymbolKind typeLiteralKind (CharTyLit {}) = charTy --- | Returns True if a type has a fixed runtime rep, +-- | Returns True if a type has a syntactically fixed runtime rep, -- as per Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. -- -- This function is equivalent to @('isFixedRuntimeRepKind' . 'typeKind')@, @@ -3558,9 +3558,9 @@ isConcrete = go | isConcreteTyCon tc = all go tys | otherwise = False go ForAllTy{} = False - go (FunTy _ w t1 t2) = go w && go t1 && go t2 - -- NB: no need to check the kinds of 't1' and 't2'. - -- See Note [Concrete types] in GHC.Tc.Utils.Concrete. + go (FunTy _ w t1 t2) = go w + && go (typeKind t1) && go t1 + && go (typeKind t2) && go t2 go LitTy{} = True go CastTy{} = False go CoercionTy{} = False diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs index bbdda9c731..8c46285ad4 100644 --- a/compiler/GHC/Tc/Errors.hs +++ b/compiler/GHC/Tc/Errors.hs @@ -507,7 +507,7 @@ mkErrorItem ct ---------------------------------------------------------------- reportWanteds :: SolverReportErrCtxt -> TcLevel -> WantedConstraints -> TcM () reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics - , wc_holes = holes }) + , wc_errors = errs }) | isEmptyWC wc = traceTc "reportWanteds empty WC" empty | otherwise = do { tidy_items <- mapMaybeM mkErrorItem tidy_cts @@ -515,7 +515,7 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics , text "Suppress =" <+> ppr (cec_suppress ctxt) , text "tidy_cts =" <+> ppr tidy_cts , text "tidy_items =" <+> ppr tidy_items - , text "tidy_holes =" <+> ppr tidy_holes ]) + , text "tidy_errs =" <+> ppr tidy_errs ]) -- This check makes sure that we aren't suppressing the only error that will -- actually stop compilation @@ -530,7 +530,7 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics (vcat [text "reportWanteds is suppressing all errors"]) -- First, deal with any out-of-scope errors: - ; let (out_of_scope, other_holes) = partition isOutOfScopeHole tidy_holes + ; let (out_of_scope, other_holes, not_conc_errs) = partition_errors tidy_errs -- don't suppress out-of-scope errors ctxt_for_scope_errs = ctxt { cec_suppress = False } ; (_, no_out_of_scope) <- askNoErrs $ @@ -545,6 +545,8 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics ; reportHoles tidy_items ctxt_for_insols other_holes -- holes never suppress + ; reportNotConcreteErrs ctxt_for_insols not_conc_errs + -- See Note [Suppressing confusing errors] ; let (suppressed_items, items0) = partition suppress tidy_items ; traceTc "reportWanteds suppressed:" (ppr suppressed_items) @@ -573,9 +575,25 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics do { (_, more_leftovers) <- tryReporters ctxt3 report3 suppressed_items ; massertPpr (null more_leftovers) (ppr more_leftovers) } } where - env = cec_tidy ctxt - tidy_cts = bagToList (mapBag (tidyCt env) simples) - tidy_holes = bagToList (mapBag (tidyHole env) holes) + env = cec_tidy ctxt + tidy_cts = bagToList (mapBag (tidyCt env) simples) + tidy_errs = bagToList (mapBag (tidyDelayedError env) errs) + + partition_errors :: [DelayedError] -> ([Hole], [Hole], [NotConcreteError]) + partition_errors = go [] [] [] + where + go out_of_scope other_holes syn_eqs [] + = (out_of_scope, other_holes, syn_eqs) + go es1 es2 es3 (err:errs) + | (es1, es2, es3) <- go es1 es2 es3 errs + = case err of + DE_Hole hole + | isOutOfScopeHole hole + -> (hole : es1, es2, es3) + | otherwise + -> (es1, hole : es2, es3) + DE_NotConcrete err + -> (es1, es2, err : es3) -- See Note [Suppressing confusing errors] suppress :: ErrorItem -> Bool @@ -594,10 +612,11 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics report1 = [ ("custom_error", is_user_type_error, True, mkUserTypeErrorReporter) , given_eq_spec - , ("insoluble2", utterly_wrong, True, mkGroupReporter mkEqErr) - , ("skolem eq1", very_wrong, True, mkSkolReporter) - , ("skolem eq2", skolem_eq, True, mkSkolReporter) - , ("non-tv eq", non_tv_eq, True, mkSkolReporter) + , ("insoluble2", utterly_wrong, True, mkGroupReporter mkEqErr) + , ("skolem eq1", very_wrong, True, mkSkolReporter) + , ("FixedRuntimeRep", is_FRR, True, mkGroupReporter mkFRRErr) + , ("skolem eq2", skolem_eq, True, mkSkolReporter) + , ("non-tv eq", non_tv_eq, True, mkSkolReporter) -- The only remaining equalities are alpha ~ ty, -- where alpha is untouchable; and representational equalities @@ -611,7 +630,6 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics -- report2: we suppress these if there are insolubles elsewhere in the tree report2 = [ ("Implicit params", is_ip, False, mkGroupReporter mkIPErr) , ("Irreds", is_irred, False, mkGroupReporter mkIrredErr) - , ("FixedRuntimeRep", is_FRR, False, mkGroupReporter mkFRRErr) , ("Dicts", is_dict, False, mkGroupReporter mkDictErr) ] -- report3: suppressed errors should be reported as categorized by either report1 @@ -636,6 +654,9 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics very_wrong _ (EqPred NomEq ty1 ty2) = isSkolemTy tc_lvl ty1 && isRigidTy ty2 very_wrong _ _ = False + -- Representation-polymorphism errors, to be reported using mkFRRErr. + is_FRR item _ = isJust $ fixedRuntimeRepOrigin_maybe item + -- Things like (a ~N b) or (a ~N F Bool) skolem_eq _ (EqPred NomEq ty1 _) = isSkolemTy tc_lvl ty1 skolem_eq _ _ = False @@ -646,23 +667,13 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics is_user_type_error item _ = isUserTypeError (errorItemPred item) - is_homo_equality item (EqPred _ ty1 ty2) - | FixedRuntimeRepOrigin {} <- errorItemOrigin item - -- Constraints with FixedRuntimeRep origin must be reported using mkFRRErr. - = False - | otherwise + is_homo_equality _ (EqPred _ ty1 ty2) = tcTypeKind ty1 `tcEqType` tcTypeKind ty2 is_homo_equality _ _ = False - is_equality item (EqPred {}) - | FixedRuntimeRepOrigin {} <- errorItemOrigin item - -- Constraints with FixedRuntimeRep origin must be reported using mkFRRErr. - = False - | otherwise - = True - is_equality _ _ - = False + is_equality _(EqPred {}) = True + is_equality _ _ = False is_dict _ (ClassPred {}) = True is_dict _ _ = False @@ -670,12 +681,6 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics is_ip _ (ClassPred cls _) = isIPClass cls is_ip _ _ = False - is_FRR item _ - | FixedRuntimeRepOrigin {} <- errorItemOrigin item - = True - is_FRR _ _ - = False - is_irred _ (IrredPred {}) = True is_irred _ _ = False @@ -890,6 +895,35 @@ zonkTidyTcLclEnvs tidy_env lcls = foldM go (tidy_env, emptyNameEnv) (concatMap t (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env ty return (tidy_env', extendNameEnv name_env name tidy_ty) +reportNotConcreteErrs :: SolverReportErrCtxt -> [NotConcreteError] -> TcM () +reportNotConcreteErrs _ [] = return () +reportNotConcreteErrs ctxt errs@(err0:_) + = do { msg <- mkErrorReport (ctLocEnv (nce_loc err0)) diag (Just ctxt) [] + ; reportDiagnostic msg } + + where + + frr_origins = acc_errors errs + diag = TcRnSolverReport + [SolverReportWithCtxt ctxt (FixedRuntimeRepError frr_origins)] + ErrorWithoutFlag noHints + + -- Accumulate the different kind of errors arising from syntactic equality. + -- (Only SynEq_FRR origin for the moment.) + acc_errors = go [] + where + go frr_errs [] = frr_errs + go frr_errs (err:errs) + | frr_errs <- go frr_errs errs + = case err of + NCE_FRR + { nce_frr_origin = frr_orig + , nce_reasons = _not_conc } -> + FRR_Info + { frr_info_origin = frr_orig + , frr_info_not_concrete = Nothing } + : frr_errs + {- Note [Skip type holes rapidly] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have module with a /lot/ of partial type signatures, and we @@ -1019,10 +1053,10 @@ reportGroup mk_err ctxt items -- See Note [No deferring for multiplicity errors] nonDeferrableOrigin :: CtOrigin -> Bool -nonDeferrableOrigin NonLinearPatternOrigin = True -nonDeferrableOrigin (UsageEnvironmentOf {}) = True -nonDeferrableOrigin (FixedRuntimeRepOrigin {}) = True -nonDeferrableOrigin _ = False +nonDeferrableOrigin NonLinearPatternOrigin = True +nonDeferrableOrigin (UsageEnvironmentOf {}) = True +nonDeferrableOrigin (FRROrigin {}) = True +nonDeferrableOrigin _ = False maybeReportError :: SolverReportErrCtxt -> [ErrorItem] -- items covered by the Report @@ -1060,9 +1094,7 @@ addDeferredBinding ctxt err (EI { ei_evdest = Just dest, ei_pred = item_ty -> do { -- See Note [Deferred errors for coercion holes] let co_var = coHoleCoVar hole ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var err_tm - ; fillCoercionHole hole (mkTcCoVarCo co_var) } - NoDest - -> return () } + ; fillCoercionHole hole (mkTcCoVarCo co_var) } } addDeferredBinding _ _ _ = return () -- Do not set any evidence for Given mkErrorTerm :: SolverReportErrCtxt -> CtLoc -> Type -- of the error term @@ -1448,39 +1480,35 @@ mkIPErr ctxt items ---------------- --- | Report a representation-polymorphism error to the user: `ty` should have --- a fixed runtime representation, but doesn't. +-- | Report a representation-polymorphism error to the user: +-- a type is required to havehave a fixed runtime representation, +-- but doesn't. -- -- See Note [Reporting representation-polymorphism errors] in GHC.Tc.Types.Origin. -mkFRRErr :: SolverReportErrCtxt -> [ErrorItem] -> TcM SolverReport +mkFRRErr :: HasDebugCallStack => SolverReportErrCtxt -> [ErrorItem] -> TcM SolverReport mkFRRErr ctxt items - = do { -- Zonk and tidy the error items. - ; (_tidy_env, tidied_origins) <- - zonkTidyOrigins (cec_tidy ctxt) (map errorItemOrigin items) - -- Then remove duplicates: only retain one 'CtOrigin' per representation-polymorphic type. - ; let frr_infos = - nubOrdBy (nonDetCmpType `on` frrInfo_type) $ - zipWith frr_info tidied_origins (map errorItemPred items) + = do { -- Process the error items. + ; (_tidy_env, frr_infos) <- + zonkTidyFRRInfos (cec_tidy ctxt) $ + -- Zonk/tidy to show useful variable names. + nubOrdBy (nonDetCmpType `on` (frr_type . frr_info_origin)) $ + -- Remove duplicates: only one representation-polymorphism error per type. + map (expectJust "mkFRRErr" . fixedRuntimeRepOrigin_maybe) + items ; return $ important ctxt $ FixedRuntimeRepError frr_infos } - where - frr_info :: CtOrigin -> PredType -> FixedRuntimeRepErrorInfo - frr_info orig pty - | FixedRuntimeRepOrigin ty frr_orig <- orig - = FixedRuntimeRepErrorInfo - { frrInfo_origin = frr_orig - , frrInfo_type = ty - , frrInfo_isReflPrim = isIsReflPrimPred (classifyPredType pty) - -- NB: it's useful to categorise the error messages depending on - -- whether they were triggered by an 'IsRefl#' constraint or not, - -- so that we can print an extra explanatory message to the user. - -- - -- See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete. - } - | otherwise - = pprPanic "mkFRRErr: not a FixedRuntimeRep origin" $ - vcat [ text "origin:" <+> ppr orig - , text "pty:" <+> ppr pty ] +-- | Whether to report something using the @FixedRuntimeRep@ mechanism. +fixedRuntimeRepOrigin_maybe :: HasDebugCallStack => ErrorItem -> Maybe FixedRuntimeRepErrorInfo +fixedRuntimeRepOrigin_maybe item + -- An error that arose directly from a representation-polymorphism check. + | FRROrigin frr_orig <- errorItemOrigin item + = Just $ FRR_Info { frr_info_origin = frr_orig + , frr_info_not_concrete = Nothing } + -- Unsolved nominal equalities involving a concrete type variable, + -- such as @alpha[conc] ~# rr[sk]@ or @beta[conc] ~# RR@ for a + -- type family application @RR@, are handled by 'mkTyVarEqErr''. + | otherwise + = Nothing {- Note [Constraints include ...] @@ -1621,10 +1649,10 @@ mkEqErr_help :: SolverReportErrCtxt -> ErrorItem -> TcType -> TcType -> TcM (AccReportMsgs, [GhcHint]) mkEqErr_help ctxt item ty1 ty2 - | Just (tv1, _) <- tcGetCastedTyVar_maybe ty1 - = mkTyVarEqErr ctxt item tv1 ty2 - | Just (tv2, _) <- tcGetCastedTyVar_maybe ty2 - = mkTyVarEqErr ctxt item tv2 ty1 + | Just casted_tv1 <- tcGetCastedTyVar_maybe ty1 + = mkTyVarEqErr ctxt item casted_tv1 ty2 + | Just casted_tv2 <- tcGetCastedTyVar_maybe ty2 + = mkTyVarEqErr ctxt item casted_tv2 ty1 | otherwise = return (reportEqErr ctxt item ty1 ty2 :| [], []) @@ -1638,29 +1666,39 @@ reportEqErr ctxt item ty1 ty2 eqInfos = eqInfoMsgs ty1 ty2 mkTyVarEqErr :: SolverReportErrCtxt -> ErrorItem - -> TcTyVar -> TcType -> TcM (AccReportMsgs, [GhcHint]) + -> (TcTyVar, TcCoercionN) -> TcType -> TcM (AccReportMsgs, [GhcHint]) -- tv1 and ty2 are already tidied -mkTyVarEqErr ctxt item tv1 ty2 - = do { traceTc "mkTyVarEqErr" (ppr item $$ ppr tv1 $$ ppr ty2) - ; mkTyVarEqErr' ctxt item tv1 ty2 } +mkTyVarEqErr ctxt item casted_tv1 ty2 + = do { traceTc "mkTyVarEqErr" (ppr item $$ ppr casted_tv1 $$ ppr ty2) + ; mkTyVarEqErr' ctxt item casted_tv1 ty2 } mkTyVarEqErr' :: SolverReportErrCtxt -> ErrorItem - -> TcTyVar -> TcType -> TcM (AccReportMsgs, [GhcHint]) -mkTyVarEqErr' ctxt item tv1 ty2 - -- impredicativity is a simple error to understand; try it first - | check_eq_result `cterHasProblem` cteImpredicative = do - tyvar_eq_info <- extraTyVarEqInfo tv1 ty2 - let - poly_msg = CannotUnifyWithPolytype item tv1 ty2 - poly_msg_with_info - | isSkolemTyVar tv1 - = mkTcReportWithInfo poly_msg tyvar_eq_info - | otherwise - = poly_msg - -- Unlike the other reports, this discards the old 'report_important' - -- instead of augmenting it. This is because the details are not likely - -- to be helpful since this is just an unimplemented feature. - return (poly_msg_with_info <| headline_msg :| [], []) + -> (TcTyVar, TcCoercionN) -> TcType -> TcM (AccReportMsgs, [GhcHint]) +mkTyVarEqErr' ctxt item (tv1, co1) ty2 + + -- Is this a representation-polymorphism error, e.g. + -- alpha[conc] ~# rr[sk] ? If so, handle that first. + | Just frr_info <- mb_concrete_reason + = do + (_, infos) <- zonkTidyFRRInfos (cec_tidy ctxt) [frr_info] + return (FixedRuntimeRepError infos :| [], []) + + -- Impredicativity is a simple error to understand; try it before + -- anything more complicated. + | check_eq_result `cterHasProblem` cteImpredicative + = do + tyvar_eq_info <- extraTyVarEqInfo tv1 ty2 + let + poly_msg = CannotUnifyWithPolytype item tv1 ty2 + poly_msg_with_info + | isSkolemTyVar tv1 + = mkTcReportWithInfo poly_msg tyvar_eq_info + | otherwise + = poly_msg + -- Unlike the other reports, this discards the old 'report_important' + -- instead of augmenting it. This is because the details are not likely + -- to be helpful since this is just an unimplemented feature. + return (poly_msg_with_info <| headline_msg :| [], []) | isSkolemTyVar tv1 -- ty2 won't be a meta-tyvar; we would have -- swapped in Solver.Canonical.canEqTyVarHomo @@ -1690,7 +1728,7 @@ mkTyVarEqErr' ctxt item tv1 ty2 -- This is wrinkle (4) in Note [Equalities with incompatible kinds] in -- GHC.Tc.Solver.Canonical - | hasCoercionHoleTy ty2 + | hasCoercionHoleCo co1 || hasCoercionHoleTy ty2 = return (mkBlockedEqErr item :| [], []) -- If the immediately-enclosing implication has 'tv' a skolem, and @@ -1734,6 +1772,25 @@ mkTyVarEqErr' ctxt item tv1 ty2 mismatch_msg = mkMismatchMsg item ty1 ty2 add_sig = maybeToList $ suggestAddSig ctxt ty1 ty2 + -- The following doesn't use the cterHasProblem mechanism because + -- we need to retrieve the ConcreteTvOrigin. Just knowing whether + -- there is an error is not sufficient. See #21430. + mb_concrete_reason + | Just frr_orig <- isConcreteTyVar_maybe tv1 + , not (isConcrete ty2) + = Just $ frr_reason frr_orig tv1 ty2 + | Just (tv2, frr_orig) <- isConcreteTyVarTy_maybe ty2 + , not (isConcreteTyVar tv1) + = Just $ frr_reason frr_orig tv2 ty1 + -- NB: if it's an unsolved equality in which both sides are concrete + -- (e.g. a concrete type variable on both sides), then it's not a + -- representation-polymorphism problem. + | otherwise + = Nothing + frr_reason (ConcreteFRR frr_orig) conc_tv not_conc + = FRR_Info { frr_info_origin = frr_orig + , frr_info_not_concrete = Just (conc_tv, not_conc) } + ty1 = mkTyVarTy tv1 check_eq_result = case ei_m_reason item of diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs index 5778050413..dee1a99775 100644 --- a/compiler/GHC/Tc/Errors/Ppr.hs +++ b/compiler/GHC/Tc/Errors/Ppr.hs @@ -1877,8 +1877,8 @@ pprTcSolverReportMsg ctxt maybe_num_args_msg = num_args_msg `orElse` empty count_args ty = count isVisibleBinder $ fst $ splitPiTys ty -pprTcSolverReportMsg _ (FixedRuntimeRepError frr_infos) = - vcat (map make_msg frr_infos) $$ mustBeRefl_msg +pprTcSolverReportMsg _ (FixedRuntimeRepError frr_origs) = + vcat (map make_msg frr_origs) where -- Assemble the error message: pair up each origin with the corresponding type, e.g. -- • FixedRuntimeRep origin msg 1 ... @@ -1886,16 +1886,21 @@ pprTcSolverReportMsg _ (FixedRuntimeRepError frr_infos) = -- • FixedRuntimeRep origin msg 2 ... -- b :: TYPE r2 make_msg :: FixedRuntimeRepErrorInfo -> SDoc - make_msg - (FixedRuntimeRepErrorInfo - { frrInfo_origin = frr_orig - , frrInfo_type = ty }) - = - -- Add bullet points if there is more than one error. - (if length frr_infos > 1 then (bullet <+>) else id) $ - vcat [ sep [ pprFRROrigin frr_orig - , text "does not have a fixed runtime representation." ] - , type_printout ty ] + make_msg (FRR_Info { frr_info_origin = + FixedRuntimeRepOrigin + { frr_type = ty + , frr_context = frr_ctxt } + , frr_info_not_concrete = + mb_not_conc }) = + -- Add bullet points if there is more than one error. + (if length frr_origs > 1 then (bullet <+>) else id) $ + vcat [ sep [ pprFixedRuntimeRepContext frr_ctxt + , text "does not have a fixed runtime representation." ] + , type_printout ty + , case mb_not_conc of + Nothing -> empty + Just (conc_tv, not_conc) -> + unsolved_concrete_eq_explanation conc_tv not_conc ] -- Don't print out the type (only the kind), if the type includes -- a confusing cast, unless the user passed -fprint-explicit-coercions. @@ -1926,29 +1931,28 @@ pprTcSolverReportMsg _ (FixedRuntimeRepError frr_infos) = type_printout :: Type -> SDoc type_printout ty = sdocOption sdocPrintExplicitCoercions $ \ show_coercions -> - if confusing_cast ty && not show_coercions + if confusing_cast ty && not show_coercions then vcat [ text "Its kind is:" , nest 2 $ pprWithTYPE (typeKind ty) , text "(Use -fprint-explicit-coercions to see the full type.)" ] else vcat [ text "Its type is:" , nest 2 $ ppr ty <+> dcolon <+> pprWithTYPE (typeKind ty) ] - -- In PHASE 1 of FixedRuntimeRep, we don't allow rewriting in hasFixedRuntimeRep, - -- so we add a special message to explain this to the user. - -- - -- See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete. - give_mustBeRefl_msg :: Bool - give_mustBeRefl_msg = all frrInfo_isReflPrim frr_infos - - mustBeRefl_msg :: SDoc - mustBeRefl_msg - | give_mustBeRefl_msg - = vcat - [ text "NB: GHC does not (yet) support rewriting in runtime representations." - , text "Please comment on GHC ticket #13105 if this is causing you trouble." - , text "<https://gitlab.haskell.org/ghc/ghc/-/issues/13105>" ] - | otherwise - = empty + unsolved_concrete_eq_explanation :: TcTyVar -> Type -> SDoc + unsolved_concrete_eq_explanation tv not_conc = + text "Cannot unify" <+> quotes (ppr not_conc) + <+> text "with the type variable" <+> quotes (ppr tv) + $$ text "because it is not a concrete" <+> what <> dot + where + ki = tyVarKind tv + what :: SDoc + what + | isRuntimeRepTy ki + = quotes (text "RuntimeRep") + | isLevityTy ki + = quotes (text "Levity") + | otherwise + = text "type" pprTcSolverReportMsg _ (SkolemEscape item implic esc_skols) = let diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs index 3c67bcb507..30780d9d0e 100644 --- a/compiler/GHC/Tc/Errors/Types.hs +++ b/compiler/GHC/Tc/Errors/Types.hs @@ -37,6 +37,7 @@ module GHC.Tc.Errors.Types ( , MissingSignature(..) , Exported(..) , HsDocContext(..) + , FixedRuntimeRepErrorInfo(..) , ErrorItem(..), errorItemOrigin, errorItemEqRel, errorItemPred, errorItemCtLoc @@ -45,7 +46,6 @@ module GHC.Tc.Errors.Types ( , SolverReportErrCtxt(..) , getUserGivens, discardProvCtxtGivens , TcSolverReportMsg(..), TcSolverReportInfo(..) - , FixedRuntimeRepErrorInfo(..) , CND_Extra(..) , mkTcReportWithInfo , FitsMbSuppressed(..) @@ -69,7 +69,9 @@ import {-# SOURCE #-} GHC.Tc.Types (TcIdSigInfo) import {-# SOURCE #-} GHC.Tc.Errors.Hole.FitTypes (HoleFit) import GHC.Tc.Types.Constraint import GHC.Tc.Types.Evidence (EvBindsVar) -import GHC.Tc.Types.Origin (CtOrigin (ProvCtxtOrigin), SkolemInfoAnon (SigSkol), UserTypeCtxt (PatSynCtxt), TyVarBndrs, TypedThing, FRROrigin) +import GHC.Tc.Types.Origin ( CtOrigin (ProvCtxtOrigin), SkolemInfoAnon (SigSkol) + , UserTypeCtxt (PatSynCtxt), TyVarBndrs, TypedThing + , FixedRuntimeRepOrigin(..) ) import GHC.Tc.Types.Rank (Rank) import GHC.Tc.Utils.TcType (IllegalForeignTypeReason, TcType) import GHC.Types.Error @@ -2380,10 +2382,9 @@ data TcSolverReportMsg } -- TODO: combine 'Mismatch' and 'TypeEqMismatch' messages. - -- | A violation of the representation-polymorphism invariants, - -- i.e. an unsolved `Concrete# ty` constraint. + -- | A violation of the representation-polymorphism invariants. -- - -- See 'FRROrigin' for more information. + -- See 'FixedRuntimeRepErrorInfo' and 'FixedRuntimeRepContext' for more information. | FixedRuntimeRepError [FixedRuntimeRepErrorInfo] -- | A skolem type variable escapes its scope. @@ -2491,20 +2492,6 @@ data TcSolverReportMsg , unsafeOverlap_matches :: [ClsInst] , unsafeOverlapped :: [ClsInst] } --- | Stores the information we have when performing a --- representation-polymorphism check. -data FixedRuntimeRepErrorInfo - = FixedRuntimeRepErrorInfo - { frrInfo_origin :: !FRROrigin - -- ^ Context for the representation-polymorphism check. - , frrInfo_type :: !Type - -- ^ The type which we are insisting must have a fixed runtime representation. - , frrInfo_isReflPrim :: !Bool } - -- ^ Was this check due to 'IsRefl#', i.e. it's a PHASE 1 check? - -- - -- See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete. - - -- | Additional information to be given in a 'CouldNotDeduce' message, -- which is then passed on to 'mk_supplementary_ea_msg'. data CND_Extra = CND_Extra TypeOrKind Type Type @@ -2723,6 +2710,18 @@ discardMsg :: SDoc discardMsg = text "(Some bindings suppressed;" <+> text "use -fmax-relevant-binds=N or -fno-max-relevant-binds)" +-- | Stores the information to be reported in a representation-polymorphism +-- error message. +data FixedRuntimeRepErrorInfo + = FRR_Info + { frr_info_origin :: FixedRuntimeRepOrigin + -- ^ What is the original type we checked for + -- representation-polymorphism, and what specific + -- check did we perform? + , frr_info_not_concrete :: Maybe (TcTyVar, TcType) + -- ^ Which non-concrete type did we try to + -- unify this concrete type variable with? + } {- ************************************************************************ diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs index 05d4a25dc2..e72e3ed194 100644 --- a/compiler/GHC/Tc/Gen/App.hs +++ b/compiler/GHC/Tc/Gen/App.hs @@ -36,7 +36,7 @@ import GHC.Tc.Errors.Types import GHC.Tc.Utils.Monad import GHC.Tc.Utils.Unify import GHC.Tc.Utils.Instantiate -import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_MustBeRefl ) +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_syntactic ) import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst_maybe ) import GHC.Tc.Gen.HsType import GHC.Tc.Utils.TcMType @@ -403,7 +403,7 @@ Note [Checking for representation-polymorphic built-ins] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We cannot have representation-polymorphic or levity-polymorphic function arguments. See Note [Representation polymorphism invariants] -in GHC.Core. That is checked by the calls to `hasFixedRuntimeRep ` in +in GHC.Core. That is checked by the calls to `hasFixedRuntimeRep` in `tcEValArg`. But some /built-in/ functions have representation-polymorphic argument @@ -567,7 +567,11 @@ hasFixedRuntimeRep_remainingValArgs applied_args app_res_rho = \case -- in the (possibly instantiated) inferred type of the function will -- be at least the arity of the function. - check_thing :: Outputable thing => thing -> Arity -> (Int -> FRROrigin) -> TcM () + check_thing :: Outputable thing + => thing + -> Arity + -> (Int -> FixedRuntimeRepContext) + -> TcM () check_thing thing arity mk_frr_orig = do traceTc "tcApp remainingValArgs check_thing" (debug_msg thing arity) go (nb_applied_vis_val_args + 1) (nb_applied_val_args + 1) arg_tys @@ -590,7 +594,7 @@ hasFixedRuntimeRep_remainingValArgs applied_args app_res_rho = \case InvisArg -> go i_visval (i_val + 1) tys VisArg -> do - hasFixedRuntimeRep_MustBeRefl (mk_frr_orig i_visval) arg_ty + hasFixedRuntimeRep_syntactic (mk_frr_orig i_visval) arg_ty go (i_visval + 1) (i_val + 1) tys -- A message containing all the relevant info, in case this functions diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs index d3035b5cf2..b404a00b1a 100644 --- a/compiler/GHC/Tc/Gen/Arrow.hs +++ b/compiler/GHC/Tc/Gen/Arrow.hs @@ -19,11 +19,10 @@ import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckMonoExpr, tcInferRho, tcSyntaxOp , tcCheckPolyExpr ) import GHC.Hs -import GHC.Hs.Syn.Type import GHC.Tc.Errors.Types import GHC.Tc.Gen.Match import GHC.Tc.Gen.Head( tcCheckId ) -import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_MustBeRefl ) +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_syntactic ) import GHC.Tc.Utils.TcType import GHC.Tc.Utils.TcMType import GHC.Tc.Gen.Bind @@ -46,8 +45,6 @@ import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Utils.Misc -import qualified GHC.Data.Strict as Strict - import Control.Monad {- @@ -149,7 +146,7 @@ tcCmd :: CmdEnv -> LHsCmd GhcRn -> CmdType -> TcM (LHsCmd GhcTc) tcCmd env (L loc cmd) cmd_ty@(_, res_ty) = setSrcSpan (locA loc) $ do { cmd' <- tc_cmd env cmd cmd_ty - ; hasFixedRuntimeRep_MustBeRefl (FRRArrow $ ArrowCmdResTy cmd) res_ty + ; hasFixedRuntimeRep_syntactic (FRRArrow $ ArrowCmdResTy cmd) res_ty ; return (L loc cmd') } tc_cmd :: CmdEnv -> HsCmd GhcRn -> CmdType -> TcM (HsCmd GhcTc) @@ -166,7 +163,7 @@ tc_cmd env (HsCmdLet x tkLet binds tkIn (L body_loc body)) res_ty tc_cmd env in_cmd@(HsCmdCase x scrut matches) (stk, res_ty) = addErrCtxt (cmdCtxt in_cmd) $ do (scrut', scrut_ty) <- tcInferRho scrut - hasFixedRuntimeRep_MustBeRefl + hasFixedRuntimeRep_syntactic (FRRArrow $ ArrowCmdCase) scrut_ty matches' <- tcCmdMatches env scrut_ty matches (stk, res_ty) @@ -177,11 +174,8 @@ tc_cmd env cmd@(HsCmdLamCase x lc_variant match) cmd_ty do { let match_ctxt = ArrowLamCaseAlt lc_variant ; checkPatCounts (ArrowMatchCtxt match_ctxt) match ; (wrap, match') <- - tcCmdMatchLambda env match_ctxt mk_origin match cmd_ty + tcCmdMatchLambda env match_ctxt match cmd_ty ; return (mkHsCmdWrap wrap (HsCmdLamCase x lc_variant match')) } - where mk_origin = ArrowCmdLamCase . case lc_variant of - LamCase -> const Strict.Nothing - LamCases -> Strict.Just tc_cmd env (HsCmdIf x NoSyntaxExprRn pred b1 b2) res_ty -- Ordinary 'if' = do { pred' <- tcCheckMonoExpr pred boolTy @@ -234,7 +228,7 @@ tc_cmd env cmd@(HsCmdArrApp _ fun arg ho_app lr) (_, res_ty) ; arg' <- tcCheckMonoExpr arg arg_ty - ; hasFixedRuntimeRep_MustBeRefl + ; hasFixedRuntimeRep_syntactic (FRRArrow $ ArrowCmdArrApp (unLoc fun) (unLoc arg) ho_app) fun_ty @@ -262,7 +256,7 @@ tc_cmd env cmd@(HsCmdApp x fun arg) (cmd_stk, res_ty) do { arg_ty <- newOpenFlexiTyVarTy ; fun' <- tcCmd env fun (mkPairTy arg_ty cmd_stk, res_ty) ; arg' <- tcCheckMonoExpr arg arg_ty - ; hasFixedRuntimeRep_MustBeRefl + ; hasFixedRuntimeRep_syntactic (FRRArrow $ ArrowCmdApp (unLoc fun) (unLoc arg)) arg_ty ; return (HsCmdApp x fun' arg') } @@ -275,7 +269,7 @@ tc_cmd env cmd@(HsCmdApp x fun arg) (cmd_stk, res_ty) -- D;G |-a (\x.cmd) : (t,stk) --> res tc_cmd env (HsCmdLam x match) cmd_ty - = do { (wrap, match') <- tcCmdMatchLambda env KappaExpr ArrowCmdLam match cmd_ty + = do { (wrap, match') <- tcCmdMatchLambda env KappaExpr match cmd_ty ; return (mkHsCmdWrap wrap (HsCmdLam x match')) } ------------------------------------------- @@ -325,9 +319,7 @@ tc_cmd env cmd@(HsCmdArrForm x expr f fixity cmd_args) (cmd_stk, res_ty) -- | Typechecking for case command alternatives. Used for 'HsCmdCase'. tcCmdMatches :: CmdEnv - -> TcType -- ^ Type of the scrutinee. - -- Must have a fixed RuntimeRep as per - -- Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete + -> TcTypeFRR -- ^ Type of the scrutinee. -> MatchGroup GhcRn (LHsCmd GhcRn) -- ^ case alternatives -> CmdType -> TcM (MatchGroup GhcTc (LHsCmd GhcTc)) @@ -342,14 +334,11 @@ tcCmdMatches env scrut_ty matches (stk, res_ty) -- | Typechecking for 'HsCmdLam' and 'HsCmdLamCase'. tcCmdMatchLambda :: CmdEnv -> HsArrowMatchContext - -> (Int -> FRRArrowOrigin) -- ^ Function that creates an origin - -- given the index of a pattern -> MatchGroup GhcRn (LHsCmd GhcRn) -> CmdType -> TcM (HsWrapper, MatchGroup GhcTc (LHsCmd GhcTc)) tcCmdMatchLambda env ctxt - mk_origin mg@MG { mg_alts = L l matches } (cmd_stk, res_ty) = do { (co, arg_tys, cmd_stk') <- matchExpectedCmdArgs n_pats cmd_stk @@ -373,20 +362,11 @@ tcCmdMatchLambda env tcPats match_ctxt pats arg_tys $ tc_grhss grhss cmd_stk' (mkCheckExpType res_ty) - ; let arg_tys' = map (unrestricted . hsLPatType) pats' - - ; zipWithM_ - (\ (Scaled _ arg_ty) i -> - hasFixedRuntimeRep_MustBeRefl (FRRArrow $ mk_origin i) arg_ty) - arg_tys' - [1..] - ; return $ L mtch_loc (Match { m_ext = noAnn , m_ctxt = match_ctxt , m_pats = pats' , m_grhss = grhss' }) } - match_ctxt = ArrowMatchCtxt ctxt pg_ctxt = PatGuard match_ctxt @@ -401,7 +381,7 @@ tcCmdMatchLambda env (stk_ty, checkingExpType "tc_grhs" res_ty) ; return (GRHS x guards' rhs') } -matchExpectedCmdArgs :: Arity -> TcType -> TcM (TcCoercionN, [TcType], TcType) +matchExpectedCmdArgs :: Arity -> TcType -> TcM (TcCoercionN, [TcTypeFRR], TcType) matchExpectedCmdArgs 0 ty = return (mkTcNomReflCo ty, [], ty) matchExpectedCmdArgs n ty diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs index 3adbb1b0d6..04ff88f7b9 100644 --- a/compiler/GHC/Tc/Gen/Bind.hs +++ b/compiler/GHC/Tc/Gen/Bind.hs @@ -34,7 +34,7 @@ import GHC.Data.FastString import GHC.Hs import GHC.Tc.Errors.Types import GHC.Tc.Gen.Sig -import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_MustBeRefl ) +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_syntactic ) import GHC.Tc.Utils.Monad import GHC.Tc.Types.Origin import GHC.Tc.Utils.Env @@ -509,7 +509,7 @@ tcPolyBinds top_lvl sig_fn prag_fn rec_group rec_tc closed bind_list CheckGen lbind sig -> tcPolyCheck prag_fn sig lbind ; mapM_ (\ poly_id -> - hasFixedRuntimeRep_MustBeRefl (FRRBinder $ idName poly_id) (idType poly_id)) + hasFixedRuntimeRep_syntactic (FRRBinder $ idName poly_id) (idType poly_id)) poly_ids ; traceTc "} End of bindings for" (vcat [ ppr binder_names, ppr rec_group @@ -1384,7 +1384,7 @@ tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss }) -- See Note [Existentials in pattern bindings] ; ((pat', nosig_mbis), pat_ty) <- addErrCtxt (patMonoBindsCtxt pat grhss) $ - tcInfer $ \ exp_ty -> + tcInferFRR FRRPatBind $ \ exp_ty -> tcLetPat inst_sig_fun no_gen pat (unrestricted exp_ty) $ -- The above inferred type get an unrestricted multiplicity. It may be -- worth it to try and find a finer-grained multiplicity here diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs index c9e4421a7d..f85cf4ade5 100644 --- a/compiler/GHC/Tc/Gen/Expr.hs +++ b/compiler/GHC/Tc/Gen/Expr.hs @@ -40,7 +40,7 @@ import GHC.Types.Error import GHC.Core.Multiplicity import GHC.Core.UsageEnv import GHC.Tc.Errors.Types -import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_MustBeRefl ) +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_syntactic ) import GHC.Tc.Utils.Instantiate import GHC.Tc.Gen.App import GHC.Tc.Gen.Head @@ -344,7 +344,7 @@ tcExpr (ExplicitSum _ alt arity expr) res_ty -- This should cause an error, even though (17# :: Int#) -- is not representation-polymorphic: we don't know how -- wide the concrete representation of the sum type will be. - ; hasFixedRuntimeRep_MustBeRefl FRRUnboxedSum res_ty + ; hasFixedRuntimeRep_syntactic FRRUnboxedSum res_ty ; return $ mkHsWrapCo coi (ExplicitSum arg_tys' alt arity expr' ) } @@ -382,7 +382,7 @@ tcExpr (HsCase x scrut matches) res_ty ; (scrut', scrut_ty) <- tcScalingUsage mult $ tcInferRho scrut ; traceTc "HsCase" (ppr scrut_ty) - ; hasFixedRuntimeRep_MustBeRefl FRRCase scrut_ty + ; hasFixedRuntimeRep_syntactic FRRCase scrut_ty ; matches' <- tcMatchesCase match_ctxt (Scaled mult scrut_ty) matches res_ty ; return (HsCase x scrut' matches') } where @@ -950,11 +950,11 @@ tcTupArgs args tys go :: Int -> HsTupArg GhcRn -> TcType -> TcM (HsTupArg GhcTc) go i (Missing {}) arg_ty = do { mult <- newFlexiTyVarTy multiplicityTy - ; hasFixedRuntimeRep_MustBeRefl (FRRTupleSection i) arg_ty + ; hasFixedRuntimeRep_syntactic (FRRTupleSection i) arg_ty ; return (Missing (Scaled mult arg_ty)) } go i (Present x expr) arg_ty = do { expr' <- tcCheckPolyExpr expr arg_ty - ; hasFixedRuntimeRep_MustBeRefl (FRRTupleArg i) arg_ty + ; hasFixedRuntimeRep_syntactic (FRRTupleArg i) arg_ty ; return (Present x expr') } --------------------------- @@ -1386,7 +1386,7 @@ tcRecordField con_like flds_w_tys (L loc (FieldOcc sel_name lbl)) rhs | Just field_ty <- assocMaybe flds_w_tys sel_name = addErrCtxt (fieldCtxt field_lbl) $ do { rhs' <- tcCheckPolyExprNC rhs field_ty - ; hasFixedRuntimeRep_MustBeRefl (FRRRecordUpdate (unLoc lbl) (unLoc rhs')) + ; hasFixedRuntimeRep_syntactic (FRRRecordUpdate (unLoc lbl) (unLoc rhs')) field_ty ; let field_id = mkUserLocal (nameOccName sel_name) (nameUnique sel_name) diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs index 0763ad2679..05d95bf6d2 100644 --- a/compiler/GHC/Tc/Gen/Match.hs +++ b/compiler/GHC/Tc/Gen/Match.hs @@ -50,7 +50,7 @@ import GHC.Tc.Gen.Head( tcCheckId ) import GHC.Tc.Utils.TcMType import GHC.Tc.Utils.TcType import GHC.Tc.Gen.Bind -import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_MustBeRefl ) +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_syntactic ) import GHC.Tc.Utils.Unify import GHC.Tc.Types.Origin import GHC.Tc.Types.Evidence @@ -436,7 +436,7 @@ tcGuardStmt ctxt (BindStmt _ pat rhs) res_ty thing_inside -- two multiplicity to still be the same. (rhs', rhs_ty) <- tcScalingUsage Many $ tcInferRhoNC rhs -- Stmt has a context already - ; hasFixedRuntimeRep_MustBeRefl FRRBindStmtGuard rhs_ty + ; hasFixedRuntimeRep_syntactic FRRBindStmtGuard rhs_ty ; (pat', thing) <- tcCheckPat_O (StmtCtxt ctxt) (lexprCtOrigin rhs) pat (unrestricted rhs_ty) $ thing_inside res_ty @@ -598,7 +598,7 @@ tcMcStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside thing_inside (mkCheckExpType new_res_ty) ; return (rhs_ty, rhs', pat_mult, pat', thing, new_res_ty) } - ; hasFixedRuntimeRep_MustBeRefl (FRRBindStmt MonadComprehension) rhs_ty + ; hasFixedRuntimeRep_syntactic (FRRBindStmt MonadComprehension) rhs_ty -- If (but only if) the pattern can fail, typecheck the 'fail' operator ; fail_op' <- fmap join . forM (xbsrn_failOp xbsrn) $ \fail -> @@ -634,9 +634,9 @@ tcMcStmt _ (BodyStmt _ rhs then_op guard_op) res_ty thing_inside ; thing <- tcScalingUsage fun_mult $ thing_inside (mkCheckExpType new_res_ty) ; return (thing, rhs', rhs_ty, new_res_ty, test_ty, guard_op') } - ; hasFixedRuntimeRep_MustBeRefl FRRBodyStmtGuard test_ty - ; hasFixedRuntimeRep_MustBeRefl (FRRBodyStmt MonadComprehension 1) rhs_ty - ; hasFixedRuntimeRep_MustBeRefl (FRRBodyStmt MonadComprehension 2) new_res_ty + ; hasFixedRuntimeRep_syntactic FRRBodyStmtGuard test_ty + ; hasFixedRuntimeRep_syntactic (FRRBodyStmt MonadComprehension 1) rhs_ty + ; hasFixedRuntimeRep_syntactic (FRRBodyStmt MonadComprehension 2) new_res_ty ; return (BodyStmt rhs_ty rhs' then_op' guard_op', thing) } @@ -872,7 +872,7 @@ tcDoStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside thing_inside (mkCheckExpType new_res_ty) ; return (rhs_ty, rhs', pat_mult, pat', new_res_ty, thing) } - ; hasFixedRuntimeRep_MustBeRefl (FRRBindStmt DoNotation) rhs_ty + ; hasFixedRuntimeRep_syntactic (FRRBindStmt DoNotation) rhs_ty -- If (but only if) the pattern can fail, typecheck the 'fail' operator ; fail_op' <- fmap join . forM (xbsrn_failOp xbsrn) $ \fail -> @@ -906,8 +906,8 @@ tcDoStmt _ (BodyStmt _ rhs then_op _) res_ty thing_inside do { rhs' <- tcScalingUsage rhs_mult $ tcCheckMonoExprNC rhs rhs_ty ; thing <- tcScalingUsage fun_mult $ thing_inside (mkCheckExpType new_res_ty) ; return (rhs', rhs_ty, new_res_ty, thing) } - ; hasFixedRuntimeRep_MustBeRefl (FRRBodyStmt DoNotation 1) rhs_ty - ; hasFixedRuntimeRep_MustBeRefl (FRRBodyStmt DoNotation 2) new_res_ty + ; hasFixedRuntimeRep_syntactic (FRRBodyStmt DoNotation 1) rhs_ty + ; hasFixedRuntimeRep_syntactic (FRRBodyStmt DoNotation 2) new_res_ty ; return (BodyStmt rhs_ty rhs' then_op' noSyntaxExpr, thing) } tcDoStmt ctxt (RecStmt { recS_stmts = L l stmts, recS_later_ids = later_names diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs index fb629e8826..487b1512ab 100644 --- a/compiler/GHC/Tc/Gen/Pat.hs +++ b/compiler/GHC/Tc/Gen/Pat.hs @@ -43,7 +43,7 @@ import GHC.Types.Var import GHC.Types.Name import GHC.Types.Name.Reader import GHC.Core.Multiplicity -import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_MustBeRefl ) +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_syntactic ) import GHC.Tc.Utils.Env import GHC.Tc.Utils.TcMType import GHC.Tc.Validity( arityErr ) @@ -120,11 +120,13 @@ tcPats ctxt pats pat_tys thing_inside where penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin } -tcInferPat :: HsMatchContext GhcTc -> LPat GhcRn +tcInferPat :: FixedRuntimeRepContext + -> HsMatchContext GhcTc + -> LPat GhcRn -> TcM a - -> TcM ((LPat GhcTc, a), TcSigmaType) -tcInferPat ctxt pat thing_inside - = tcInfer $ \ exp_ty -> + -> TcM ((LPat GhcTc, a), TcSigmaTypeFRR) +tcInferPat frr_orig ctxt pat thing_inside + = tcInferFRR frr_orig $ \ exp_ty -> tc_lpat (unrestricted exp_ty) penv pat thing_inside where penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin } @@ -471,7 +473,7 @@ arrow type (t1 -> t2); hence using (tcInferRho expr). Then, when taking that arrow apart we want to get a *sigma* type (forall b. b->(Int,b)), because that's what we want to bind 'x' to. -Fortunately that's what matchExpectedFunTySigma returns anyway. +Fortunately that's what matchActualFunTySigma returns anyway. -} -- Type signatures in patterns @@ -932,7 +934,7 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled -- See test case T20363. ; zipWithM_ ( \ i arg_sty -> - hasFixedRuntimeRep_MustBeRefl + hasFixedRuntimeRep_syntactic (FRRDataConArg Pattern data_con i) (scaledThing arg_sty) ) @@ -1044,7 +1046,8 @@ tcPatSynPat penv (L con_span con_name) pat_syn pat_ty arg_pats thing_inside ; traceTc "instCall" (ppr req_wrap) -- Pattern synonyms can never have representation-polymorphic argument types, - -- as checked in 'GHC.Tc.Gen.Sig.tcPatSynSig' (see use of 'FixedRuntimeRepPatSynSigArg'). + -- as checked in 'GHC.Tc.Gen.Sig.tcPatSynSig' (see use of 'FixedRuntimeRepPatSynSigArg') + -- and 'GHC.Tc.TyCl.PatSyn.tcInferPatSynDecl'. -- (If you want to lift this restriction, use 'hasFixedRuntimeRep' here, to match -- 'tcDataConPat'.) ; let diff --git a/compiler/GHC/Tc/Gen/Rule.hs b/compiler/GHC/Tc/Gen/Rule.hs index 912068a0cb..1aae9a5ece 100644 --- a/compiler/GHC/Tc/Gen/Rule.hs +++ b/compiler/GHC/Tc/Gen/Rule.hs @@ -152,13 +152,20 @@ tcRule (HsRule { rd_ext = ext -- See Note [Re-quantify type variables in rules] ; forall_tkvs <- candidateQTyVarsOfTypes (rule_ty : map idType tpl_ids) - ; qtkvs <- quantifyTyVars skol_info DefaultNonStandardTyVars forall_tkvs + ; let don't_default = nonDefaultableTyVarsOfWC residual_lhs_wanted + ; let weed_out = (`dVarSetMinusVarSet` don't_default) + quant_cands = forall_tkvs { dv_kvs = weed_out (dv_kvs forall_tkvs) + , dv_tvs = weed_out (dv_tvs forall_tkvs) } + ; qtkvs <- quantifyTyVars skol_info DefaultNonStandardTyVars quant_cands ; traceTc "tcRule" (vcat [ pprFullRuleName rname - , ppr forall_tkvs - , ppr qtkvs - , ppr rule_ty - , ppr ty_bndrs - , ppr (qtkvs ++ tpl_ids) + , text "forall_tkvs:" <+> ppr forall_tkvs + , text "quant_cands:" <+> ppr quant_cands + , text "don't_default:" <+> ppr don't_default + , text "residual_lhs_wanted:" <+> ppr residual_lhs_wanted + , text "qtkvs:" <+> ppr qtkvs + , text "rule_ty:" <+> ppr rule_ty + , text "ty_bndrs:" <+> ppr ty_bndrs + , text "qtkvs ++ tpl_ids:" <+> ppr (qtkvs ++ tpl_ids) , vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ] ]) @@ -440,7 +447,6 @@ simplifyRule name tc_lvl lhs_wanted rhs_wanted do { ev_id <- newEvVar pred ; fillCoercionHole hole (mkTcCoVarCo ev_id) ; return ev_id } - NoDest -> pprPanic "mk_quant_ev: NoDest" (ppr ct) mk_quant_ev ct = pprPanic "mk_quant_ev" (ppr ct) @@ -466,9 +472,9 @@ getRuleQuantCts wc = float_wc emptyVarSet wc where float_wc :: TcTyCoVarSet -> WantedConstraints -> (Cts, WantedConstraints) - float_wc skol_tvs (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes }) + float_wc skol_tvs (WC { wc_simple = simples, wc_impl = implics, wc_errors = errs }) = ( simple_yes `andCts` implic_yes - , emptyWC { wc_simple = simple_no, wc_impl = implics_no, wc_holes = holes }) + , emptyWC { wc_simple = simple_no, wc_impl = implics_no, wc_errors = errs }) where (simple_yes, simple_no) = partitionBag (rule_quant_ct skol_tvs) simples (implic_yes, implics_no) = mapAccumBagL (float_implic skol_tvs) @@ -486,10 +492,6 @@ getRuleQuantCts wc EqPred _ t1 t2 | not (ok_eq t1 t2) -> False -- Note [RULE quantification over equalities] - SpecialPred {} - -- Rules should not quantify over special predicates, as these - -- are a GHC implementation detail. - -> False _ -> tyCoVarsOfCt ct `disjointVarSet` skol_tvs ok_eq t1 t2 diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index 31e2f7ed93..3ae3836624 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -235,15 +235,16 @@ simplifyAndEmitFlatConstraints wanted -- any skolem variables here | Note [Wrapping failing kind equalities] ; emitImplication implic ; failM } - Just (simples, holes) + Just (simples, errs) -> do { _ <- promoteTyVarSet (tyCoVarsOfCts simples) ; traceTc "emitFlatConstraints }" $ vcat [ text "simples:" <+> ppr simples - , text "holes: " <+> ppr holes ] - ; emitHoles holes -- Holes don't need promotion + , text "errs: " <+> ppr errs ] + -- Holes and other delayed errors don't need promotion + ; emitDelayedErrors errs ; emitSimples simples } } -floatKindEqualities :: WantedConstraints -> Maybe (Bag Ct, Bag Hole) +floatKindEqualities :: WantedConstraints -> Maybe (Bag Ct, Bag DelayedError) -- Float out all the constraints from the WantedConstraints, -- Return Nothing if any constraints can't be floated (captured -- by skolems), or if there is an insoluble constraint, or @@ -256,15 +257,15 @@ floatKindEqualities :: WantedConstraints -> Maybe (Bag Ct, Bag Hole) -- See Note [floatKindEqualities vs approximateWC] floatKindEqualities wc = float_wc emptyVarSet wc where - float_wc :: TcTyCoVarSet -> WantedConstraints -> Maybe (Bag Ct, Bag Hole) + float_wc :: TcTyCoVarSet -> WantedConstraints -> Maybe (Bag Ct, Bag DelayedError) float_wc trapping_tvs (WC { wc_simple = simples , wc_impl = implics - , wc_holes = holes }) + , wc_errors = errs }) | all is_floatable simples - = do { (inner_simples, inner_holes) + = do { (inner_simples, inner_errs) <- flatMapBagPairM (float_implic trapping_tvs) implics ; return ( simples `unionBags` inner_simples - , holes `unionBags` inner_holes) } + , errs `unionBags` inner_errs) } | otherwise = Nothing where @@ -272,7 +273,7 @@ floatKindEqualities wc = float_wc emptyVarSet wc | insolubleEqCt ct = False | otherwise = tyCoVarsOfCt ct `disjointVarSet` trapping_tvs - float_implic :: TcTyCoVarSet -> Implication -> Maybe (Bag Ct, Bag Hole) + float_implic :: TcTyCoVarSet -> Implication -> Maybe (Bag Ct, Bag DelayedError) float_implic trapping_tvs (Implic { ic_wanted = wanted, ic_given_eqs = given_eqs , ic_skols = skols, ic_status = status }) | isInsolubleStatus status @@ -496,14 +497,22 @@ simplifyTopWanteds wanteds , gopt Opt_PrintExplicitRuntimeReps dflags -- See Note [Defaulting insolubles] = try_class_defaulting wc | otherwise - = do { free_tvs <- TcS.zonkTyCoVarsAndFVList (tyCoVarsOfWCList wc) - ; let meta_tvs = filter (isTyVar <&&> isMetaTyVar) free_tvs - -- zonkTyCoVarsAndFV: the wc_first_go is not yet zonked - -- filter isMetaTyVar: we might have runtime-skolems in GHCi, - -- and we definitely don't want to try to assign to those! - -- The isTyVar is needed to weed out coercion variables - - ; defaulted <- mapM defaultTyVarTcS meta_tvs -- Has unification side effects + = do { -- Need to zonk first, as the WantedConstraints are not yet zonked. + ; free_tvs <- TcS.zonkTyCoVarsAndFVList (tyCoVarsOfWCList wc) + ; let defaultable_tvs = filter can_default free_tvs + can_default tv + = isTyVar tv + -- Weed out coercion variables. + + && isMetaTyVar tv + -- Weed out runtime-skolems in GHCi, which we definitely + -- shouldn't try to default. + + && not (tv `elemVarSet` nonDefaultableTyVarsOfWC wc) + -- Weed out variables for which defaulting would be unhelpful, + -- e.g. alpha appearing in [W] alpha[conc] ~# rr[sk]. + + ; defaulted <- mapM defaultTyVarTcS defaultable_tvs -- Has unification side effects ; if or defaulted then do { wc_residual <- nestTcS (solveWanteds wc) -- See Note [Must simplify after defaulting] @@ -513,7 +522,7 @@ simplifyTopWanteds wanteds try_class_defaulting :: WantedConstraints -> TcS WantedConstraints try_class_defaulting wc | isEmptyWC wc || insolubleWC wc -- See Note [Defaulting insolubles] - = return wc + = try_callstack_defaulting wc | otherwise -- See Note [When to do type-class defaulting] = do { something_happened <- applyDefaultingRules wc -- See Note [Top-level Defaulting Plan] @@ -594,6 +603,20 @@ Another potential alternative would be to suppress *all* non-insoluble errors if there are *any* insoluble errors, anywhere, but that seems too drastic. +Note [Don't default in syntactic equalities] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When there are unsolved syntactic equalities such as + + rr[sk] ~S# alpha[conc] + +we should not default alpha, lest we obtain a poor error message such as + + Couldn't match kind `rr' with `LiftedRep' + +We would rather preserve the original syntactic equality to be +reported to the user, especially as the concrete metavariable alpha +might store an informative origin for the user. + Note [Must simplify after defaulting] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We may have a deeply buried constraint @@ -797,9 +820,25 @@ If we default RuntimeRep-vars, we get which is just plain wrong. -Conclusion: we should do RuntimeRep-defaulting on insolubles only when the user does not -want to hear about RuntimeRep stuff -- that is, when -fprint-explicit-runtime-reps -is not set. +Another situation in which we don't want to default involves concrete metavariables. + +In equalities such as alpha[conc] ~# rr[sk] , alpha[conc] ~# RR beta[tau] +for a type family RR (all at kind RuntimeRep), we would prefer to report a +representation-polymorphism error rather than default alpha and get error: + + Could not unify `rr` with `Lifted` / Could not unify `RR b0` with `Lifted` + +which is very confusing. For this reason, we weed out the concrete +metavariables participating in such equalities in nonDefaultableTyVarsOfWC. +Just looking at insolublity is not enough, as `alpha[conc] ~# RR beta[tau]` could +become soluble after defaulting beta (see also #21430). + +Conclusion: we should do RuntimeRep-defaulting on insolubles only when the +user does not want to hear about RuntimeRep stuff -- that is, when +-fprint-explicit-runtime-reps is not set. +However, we must still take care not to default concrete type variables +participating in an equality with a non-concrete type, as seen in the +last example above. -} ------------------ @@ -2216,7 +2255,7 @@ simplifyWantedsTcM wanted ; return result } solveWanteds :: WantedConstraints -> TcS WantedConstraints -solveWanteds wc@(WC { wc_holes = holes }) +solveWanteds wc@(WC { wc_errors = errs }) = do { cur_lvl <- TcS.getTcLevel ; traceTcS "solveWanteds {" $ vcat [ text "Level =" <+> ppr cur_lvl @@ -2225,8 +2264,8 @@ solveWanteds wc@(WC { wc_holes = holes }) ; dflags <- getDynFlags ; solved_wc <- simplify_loop 0 (solverIterations dflags) True wc - ; holes' <- simplifyHoles holes - ; let final_wc = solved_wc { wc_holes = holes' } + ; errs' <- simplifyDelayedErrors errs + ; let final_wc = solved_wc { wc_errors = errs' } ; ev_binds_var <- getTcEvBindsVar ; bb <- TcS.getTcEvBindsMap ev_binds_var @@ -2268,6 +2307,7 @@ simplify_loop n limit definitely_redo_implications , wc_impl = implics2 }) } ; unif_happened <- resetUnificationFlag + ; csTraceTcS $ text "unif_happened" <+> ppr unif_happened -- Note [The Unification Level Flag] in GHC.Tc.Solver.Monad ; maybe_simplify_again (n+1) limit unif_happened wc2 } @@ -2483,12 +2523,12 @@ setImplicationStatus implic@(Implic { ic_status = status then Nothing else Just final_implic } where - WC { wc_simple = simples, wc_impl = implics, wc_holes = holes } = wc + WC { wc_simple = simples, wc_impl = implics, wc_errors = errs } = wc pruned_implics = filterBag keep_me implics pruned_wc = WC { wc_simple = simples , wc_impl = pruned_implics - , wc_holes = holes } -- do not prune holes; these should be reported + , wc_errors = errs } -- do not prune holes; these should be reported keep_me :: Implication -> Bool keep_me ic @@ -2602,9 +2642,13 @@ neededEvVars implic@(Implic { ic_given = givens | otherwise = evVarsOfTerm rhs `unionVarSet` needs ------------------------------------------------- -simplifyHoles :: Bag Hole -> TcS (Bag Hole) -simplifyHoles = mapBagM simpl_hole +simplifyDelayedErrors :: Bag DelayedError -> TcS (Bag DelayedError) +simplifyDelayedErrors = mapBagM simpl_err where + simpl_err :: DelayedError -> TcS DelayedError + simpl_err (DE_Hole hole) = DE_Hole <$> simpl_hole hole + simpl_err err@(DE_NotConcrete {}) = return err + simpl_hole :: Hole -> TcS Hole -- See Note [Do not simplify ConstraintHoles] @@ -2836,23 +2880,20 @@ ridiculous, but I (Richard E) don't see a good fix. -- | Like 'defaultTyVar', but in the TcS monad. defaultTyVarTcS :: TcTyVar -> TcS Bool defaultTyVarTcS the_tv - | isRuntimeRepVar the_tv - , not (isTyVarTyVar the_tv) + | isTyVarTyVar the_tv -- TyVarTvs should only be unified with a tyvar -- never with a type; c.f. GHC.Tc.Utils.TcMType.defaultTyVar -- and Note [Inferring kinds for type declarations] in GHC.Tc.TyCl + = return False + | isRuntimeRepVar the_tv = do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv) ; unifyTyVar the_tv liftedRepTy ; return True } | isLevityVar the_tv - , not (isTyVarTyVar the_tv) = do { traceTcS "defaultTyVarTcS Levity" (ppr the_tv) ; unifyTyVar the_tv liftedDataConTy ; return True } | isMultiplicityVar the_tv - , not (isTyVarTyVar the_tv) -- TyVarTvs should only be unified with a tyvar - -- never with a type; c.f. TcMType.defaultTyVar - -- See Note [Kind generalisation and SigTvs] = do { traceTcS "defaultTyVarTcS Multiplicity" (ppr the_tv) ; unifyTyVar the_tv manyDataConTy ; return True } diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index 222a665eaa..f63cb5c030 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -124,9 +124,6 @@ canonicalize (CEqCan { cc_ev = ev = {-# SCC "canEqLeafTyVarEq" #-} canEqNC ev eq_rel (canEqLHSType lhs) rhs -canonicalize (CSpecialCan { cc_ev = ev, cc_special_pred = special_pred }) - = canSpecial ev special_pred - canNC :: CtEvidence -> TcS (StopOrContinue Ct) canNC ev = case classifyPredType pred of @@ -138,8 +135,6 @@ canNC ev = canIrred ev ForAllPred tvs th p -> do traceTcS "canEvNC:forall" (ppr pred) canForAllNC ev tvs th p - SpecialPred spec -> do traceTcS "canEvNC:special" (ppr pred) - canSpecial ev spec where pred = ctEvPred ev @@ -750,9 +745,6 @@ canIrred ev -- in with a polytype. This is #18987. do traceTcS "canEvNC:forall" (ppr pred) canForAllNC ev tvs th p - SpecialPred {} -> -- IrredPreds have kind Constraint, so cannot - -- become SpecialPreds - pprPanic "canIrred: SpecialPred" (ppr ev) IrredPred {} -> continueWith $ mkIrredCt IrredShapeReason new_ev } } @@ -923,48 +915,8 @@ we just add it to TcS's local InstEnv of known instances, via addInertForall. Then, if we look up (C x Int Bool), say, we'll find a match in the InstEnv. - ************************************************************************ * * -* Special predicates -* * -********************************************************************* -} - --- | Canonicalise a 'SpecialPred' constraint. -canSpecial :: CtEvidence -> SpecialPred -> TcS (StopOrContinue Ct) -canSpecial ev special_pred = - case special_pred of - IsReflPrimPred lhs rhs -> - canIsReflPrim ev lhs rhs - --- | Canonicalise a 'IsRefl#' constraint: zonk the lhs and rhs, --- and solve it if they are equal. --- --- See Note [IsRefl#] in GHC.Tc.Utils.Concrete. --- --- Important: we never rewrite the arguments to an 'IsRefl#' constraint --- (we only zonk them), as rewriting would defeat the whole purpose of the constraint! -canIsReflPrim :: CtEvidence -> TcType -> TcType -> TcS (StopOrContinue Ct) -canIsReflPrim ev lhs rhs - = do { -- IsRefl# constraints should never appear in Givens. - ; massertPpr (not $ isGivenOrigin $ ctEvOrigin ev) - (text "canIsReflPrim: Given IsRefl# constraint" $$ ppr ev) - ; lhs <- zonkTcType lhs - ; rhs <- zonkTcType rhs - ; if lhs `tcEqType` rhs - then stopWith ev "Solved IsRefl#" - else - do { let new_pty = mkIsReflPrimPred lhs rhs - new_ev = setCtEvPredType ev new_pty - new_ct = CSpecialCan { cc_ev = new_ev - , cc_special_pred = IsReflPrimPred lhs rhs } - ; traceTcS "canIsReflPrim continueWith" $ - vcat [ text "new_ev =" <+> ppr new_ev - , text "lhs =" <+> ppr lhs, text "rhs =" <+> ppr rhs ] - ; continueWith new_ct }} - -{-********************************************************************** -* * * Equalities * * ************************************************************************ diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs index cc2afc1b0e..f7d0eb0701 100644 --- a/compiler/GHC/Tc/Solver/InertSet.hs +++ b/compiler/GHC/Tc/Solver/InertSet.hs @@ -1263,9 +1263,6 @@ addInertItem tc_lvl ics@(IC { inert_irreds = irreds }) item@(CIrredCan {}) addInertItem _ ics item@(CDictCan { cc_class = cls, cc_tyargs = tys }) = ics { inert_dicts = addDict (inert_dicts ics) cls tys item } -addInertItem _ ics@( IC { inert_irreds = irreds }) item@(CSpecialCan {}) - = ics { inert_irreds = irreds `snocBag` item } - addInertItem _ _ item = pprPanic "upd_inert set: can't happen! Inserting " $ ppr item -- Can't be CNonCanonical because they only land in inert_irreds @@ -1621,7 +1618,7 @@ mightEqualLater inert_set given_pred given_loc wanted_pred wanted_loc | otherwise = False - -- like canSolveByUnification, but allows cbv variables to unify + -- like startSolvingByUnification, but allows cbv variables to unify can_unify :: TcTyVar -> MetaInfo -> Type -> Bool can_unify _lhs_tv TyVarTv rhs_ty -- see Example 3 from the Note | Just rhs_tv <- tcGetTyVar_maybe rhs_ty diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs index 5c4b18621f..0a246939c6 100644 --- a/compiler/GHC/Tc/Solver/Interact.hs +++ b/compiler/GHC/Tc/Solver/Interact.hs @@ -140,13 +140,13 @@ solve_simple_wanteds :: WantedConstraints -> TcS WantedConstraints -- Try solving these constraints -- Affects the unification state (of course) but not the inert set -- The result is not necessarily zonked -solve_simple_wanteds (WC { wc_simple = simples1, wc_impl = implics1, wc_holes = holes }) +solve_simple_wanteds (WC { wc_simple = simples1, wc_impl = implics1, wc_errors = errs }) = nestTcS $ do { solveSimples simples1 ; (implics2, unsolved) <- getUnsolvedInerts ; return (WC { wc_simple = unsolved , wc_impl = implics1 `unionBags` implics2 - , wc_holes = holes }) } + , wc_errors = errs }) } {- Note [The solveSimpleWanteds loop] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -429,9 +429,6 @@ interactWithInertsStage wi CEqCan {} -> interactEq ics wi CIrredCan {} -> interactIrred ics wi CDictCan {} -> interactDict ics wi - CSpecialCan { cc_special_pred = spec } -> - case spec of - IsReflPrimPred {} -> continueWith wi -- cannot have IsRefl# Givens, so nothing to interact with _ -> pprPanic "interactWithInerts" (ppr wi) } -- CNonCanonical have been canonicalised @@ -1896,11 +1893,6 @@ topReactionsStage work_item CIrredCan {} -> doTopReactOther work_item - CSpecialCan { cc_special_pred = spec } -> - case spec of - IsReflPrimPred {} -> continueWith work_item - -- No top-level interactions for IsRefl# constraints. - -- Any other work item does not react with any top-level equations _ -> continueWith work_item } diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index a039630887..764f1eb454 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -648,8 +648,6 @@ removeInertCt is ct = CQuantCan {} -> panic "removeInertCt: CQuantCan" CIrredCan {} -> panic "removeInertCt: CIrredEvCan" CNonCanonical {} -> panic "removeInertCt: CNonCanonical" - CSpecialCan { cc_special_pred = special_pred } -> - pprPanic "removeInertCt" (ppr "CSpecialCan" <+> parens (ppr special_pred)) -- | Looks up a family application in the inerts. lookupFamAppInert :: (CtFlavourRole -> Bool) -- can it rewrite the target? @@ -1253,8 +1251,11 @@ touchabilityTest :: CtFlavour -> TcTyVar -> TcType -> TcS TouchabilityTestResult touchabilityTest flav tv1 rhs | flav /= Given -- See Note [Do not unify Givens] , MetaTv { mtv_tclvl = tv_lvl, mtv_info = info } <- tcTyVarDetails tv1 - , canSolveByUnification info rhs - = do { ambient_lvl <- getTcLevel + = do { can_continue_solving <- wrapTcS $ startSolvingByUnification info rhs + ; if not can_continue_solving + then return Untouchable + else + do { ambient_lvl <- getTcLevel ; given_eq_lvl <- getInnermostGivenEqLevel ; if | tv_lvl `sameDepthAs` ambient_lvl @@ -1265,7 +1266,7 @@ touchabilityTest flav tv1 rhs -> return (TouchableOuterLevel free_metas tv_lvl) | otherwise - -> return Untouchable } + -> return Untouchable } } | otherwise = return Untouchable where @@ -1605,7 +1606,6 @@ setWantedEq (HoleDest hole) co = do { useVars (coVarsOfCo co) ; fillCoercionHole hole co } setWantedEq (EvVarDest ev) _ = pprPanic "setWantedEq: EvVarDest" (ppr ev) -setWantedEq NoDest _ = panic "setWantedEq: NoDest" -- | Good for both equalities and non-equalities setWantedEvTerm :: TcEvDest -> EvTerm -> TcS () @@ -1621,8 +1621,6 @@ setWantedEvTerm (HoleDest hole) tm setWantedEvTerm (EvVarDest ev_id) tm = setEvBind (mkWantedEvBind ev_id tm) -setWantedEvTerm NoDest tm - = pprPanic "setWantedEvTerm: NoDest" (ppr tm) {- Note [Yukky eq_sel for a HoleDest] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/GHC/Tc/TyCl/Build.hs b/compiler/GHC/Tc/TyCl/Build.hs index 9f508491dc..19d79bc0a7 100644 --- a/compiler/GHC/Tc/TyCl/Build.hs +++ b/compiler/GHC/Tc/TyCl/Build.hs @@ -210,9 +210,7 @@ buildPatSyn :: Name -> Bool -> PatSynMatcher -> PatSynBuilder -> ([InvisTVBinder], ThetaType) -- ^ Univ and req -> ([InvisTVBinder], ThetaType) -- ^ Ex and prov - -> [Type] -- ^ Argument types - -- These must have a fixed RuntimeRep as per - -- Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. + -> [FRRType] -- ^ Argument types -> Type -- ^ Result type -> [FieldLabel] -- ^ Field labels for -- a record pattern synonym diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs index 46691958a6..ce3025bafa 100644 --- a/compiler/GHC/Tc/TyCl/PatSyn.hs +++ b/compiler/GHC/Tc/TyCl/PatSyn.hs @@ -150,8 +150,8 @@ tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details ; let (arg_names, is_infix) = collectPatSynArgInfo details ; (tclvl, wanted, ((lpat', args), pat_ty)) - <- pushLevelAndCaptureConstraints $ - tcInferPat PatSyn lpat $ + <- pushLevelAndCaptureConstraints $ + tcInferPat FRRPatSynArg PatSyn lpat $ mapM tcLookupId arg_names ; let (ex_tvs, prov_dicts) = tcCollectEx lpat' @@ -669,9 +669,9 @@ tc_patsyn_finish :: LocatedN Name -- ^ PatSyn Name -> TcPragEnv -> ([TcInvisTVBinder], [PredType], TcEvBinds, [EvVar]) -> ([TcInvisTVBinder], [TcType], [PredType], [EvTerm]) - -> ([LHsExpr GhcTc], [TcType]) + -> ([LHsExpr GhcTc], [TcTypeFRR]) -- ^ Pattern arguments and types. - -- These must have a fixed RuntimeRep as per + -- These must have a syntactically fixed RuntimeRep as per -- Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. -> TcType -- ^ Pattern type -> [FieldLabel] -- ^ Selector names diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index f5a1c6ab17..ed05f8a1de 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -35,6 +35,7 @@ module GHC.Tc.Types.Constraint ( CheckTyEqResult, CheckTyEqProblem, cteProblem, cterClearOccursCheck, cteOK, cteImpredicative, cteTypeFamily, cteInsolubleOccurs, cteSolubleOccurs, cterSetOccursCheckSoluble, + cterHasNoProblem, cterHasProblem, cterHasOnlyProblem, cterRemoveProblem, cterHasOccursCheck, cterFromKind, @@ -42,13 +43,16 @@ module GHC.Tc.Types.Constraint ( eqCanEqLHS, Hole(..), HoleSort(..), isOutOfScopeHole, + DelayedError(..), NotConcreteError(..), + NotConcreteReason(..), WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC, isSolvedWC, andWC, unionsWC, mkSimpleWC, mkImplicWC, addInsols, dropMisleading, addSimples, addImplics, addHoles, + addNotConcreteError, addDelayedErrors, tyCoVarsOfWC, tyCoVarsOfWCList, insolubleWantedCt, insolubleEqCt, insolubleCt, - insolubleImplic, + insolubleImplic, nonDefaultableTyVarsOfWC, Implication(..), implicationPrototype, checkTelescopeSkol, ImplicStatus(..), isInsolubleStatus, isSolvedStatus, @@ -127,6 +131,7 @@ import Data.Monoid ( Endo(..) ) import qualified Data.Semigroup as S import Control.Monad ( msum, when ) import Data.Maybe ( mapMaybe ) +import Data.List.NonEmpty ( NonEmpty ) -- these are for CheckTyEqResult import Data.Word ( Word8 ) @@ -134,6 +139,7 @@ import Data.List ( intersperse ) + {- ************************************************************************ * * @@ -253,15 +259,6 @@ data Ct -- look like this, with the payload in an -- auxiliary type - -- | A special canonical constraint: - -- a constraint that is used internally by GHC's typechecker. - -- - -- See #20000. - | CSpecialCan { - cc_ev :: CtEvidence, - cc_special_pred :: SpecialPred - } - ------------ -- | A 'CanEqLHS' is a type that can appear on the left of a canonical -- equality: a type variable or exactly-saturated type family application. @@ -288,7 +285,28 @@ data QCInst -- A much simplified version of ClsInst instance Outputable QCInst where ppr (QCI { qci_ev = ev }) = ppr ev ------------- +------------------------------------------------------------------------------ +-- +-- Holes and other delayed errors +-- +------------------------------------------------------------------------------ + +-- | A delayed error, to be reported after constraint solving, in order to benefit +-- from deferred unifications. +data DelayedError + = DE_Hole Hole + -- ^ A hole (in a type or in a term). + -- + -- See Note [Holes]. + | DE_NotConcrete NotConcreteError + -- ^ A type could not be ensured to be concrete. + -- + -- See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete. + +instance Outputable DelayedError where + ppr (DE_Hole hole) = ppr hole + ppr (DE_NotConcrete err) = ppr err + -- | A hole stores the information needed to report diagnostics -- about holes in terms (unbound identifiers or underscores) or -- in types (also called wildcards, as used in partial type @@ -336,6 +354,45 @@ instance Outputable HoleSort where ppr TypeHole = text "TypeHole" ppr ConstraintHole = text "ConstraintHole" +-- | Why did we require that a certain type be concrete? +data NotConcreteError + -- | Concreteness was required by a representation-polymorphism + -- check. + -- + -- See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete. + = NCE_FRR + { nce_loc :: CtLoc + -- ^ Where did this check take place? + , nce_frr_origin :: FixedRuntimeRepOrigin + -- ^ Which representation-polymorphism check did we perform? + , nce_reasons :: NonEmpty NotConcreteReason + -- ^ Why did the check fail? + } + +-- | Why did we decide that a type was not concrete? +data NotConcreteReason + -- | The type contains a 'TyConApp' of a non-concrete 'TyCon'. + -- + -- See Note [Concrete types] in GHC.Tc.Utils.Concrete. + = NonConcreteTyCon TyCon [TcType] + + -- | The type contains a type variable that could not be made + -- concrete (e.g. a skolem type variable). + | NonConcretisableTyVar TyVar + + -- | The type contains a cast. + | ContainsCast TcType TcCoercionN + + -- | The type contains a forall. + | ContainsForall TyCoVarBinder TcType + + -- | The type contains a 'CoercionTy'. + | ContainsCoercionTy TcCoercion + +instance Outputable NotConcreteError where + ppr (NCE_FRR { nce_frr_origin = frr_orig }) + = text "NCE_FRR" <+> parens (ppr (frr_type frr_orig)) + ------------ -- | Used to indicate extra information about why a CIrredCan is irreducible data CtIrredReason @@ -584,16 +641,13 @@ ctEvId :: HasDebugCallStack => Ct -> EvVar ctEvId ct = ctEvEvId (ctEvidence ct) -- | Returns the evidence 'Id' for the argument 'Ct' --- when this 'Ct' is a 'Wanted' which can hold evidence --- (i.e. doesn't have 'NoDest' 'TcEvDest'). +-- when this 'Ct' is a 'Wanted'. -- -- Returns 'Nothing' otherwise. wantedEvId_maybe :: Ct -> Maybe EvVar wantedEvId_maybe ct = case ctEvidence ct of - ctev@(CtWanted { ctev_dest = dst }) - | NoDest <- dst - -> Nothing + ctev@(CtWanted {}) | otherwise -> Just $ ctEvEvId ctev CtGiven {} @@ -632,8 +686,6 @@ instance Outputable Ct where CQuantCan (QCI { qci_pend_sc = pend_sc }) | pend_sc -> text "CQuantCan(psc)" | otherwise -> text "CQuantCan" - CSpecialCan { cc_special_pred = special_pred } -> - text "CSpecialCan" <> parens (ppr special_pred) ----------------------------------- -- | Is a type a canonical LHS? That is, is it a tyvar or an exactly-saturated @@ -751,10 +803,10 @@ tyCoVarsOfWCList = fvVarList . tyCoFVsOfWC -- computation. See Note [Deterministic FV] in "GHC.Utils.FV". tyCoFVsOfWC :: WantedConstraints -> FV -- Only called on *zonked* things -tyCoFVsOfWC (WC { wc_simple = simple, wc_impl = implic, wc_holes = holes }) +tyCoFVsOfWC (WC { wc_simple = simple, wc_impl = implic, wc_errors = errors }) = tyCoFVsOfCts simple `unionFV` tyCoFVsOfBag tyCoFVsOfImplic implic `unionFV` - tyCoFVsOfBag tyCoFVsOfHole holes + tyCoFVsOfBag tyCoFVsOfDelayedError errors -- | Returns free variables of Implication as a composable FV computation. -- See Note [Deterministic FV] in "GHC.Utils.FV". @@ -770,6 +822,10 @@ tyCoFVsOfImplic (Implic { ic_skols = skols tyCoFVsVarBndrs givens $ tyCoFVsOfWC wanted +tyCoFVsOfDelayedError :: DelayedError -> FV +tyCoFVsOfDelayedError (DE_Hole hole) = tyCoFVsOfHole hole +tyCoFVsOfDelayedError (DE_NotConcrete {}) = emptyFV + tyCoFVsOfHole :: Hole -> FV tyCoFVsOfHole (Hole { hole_ty = ty }) = tyCoFVsOfType ty @@ -963,13 +1019,13 @@ pprCts cts = vcat (map ppr (bagToList cts)) data WantedConstraints = WC { wc_simple :: Cts -- Unsolved constraints, all wanted , wc_impl :: Bag Implication - , wc_holes :: Bag Hole + , wc_errors :: Bag DelayedError } emptyWC :: WantedConstraints emptyWC = WC { wc_simple = emptyBag , wc_impl = emptyBag - , wc_holes = emptyBag } + , wc_errors = emptyBag } mkSimpleWC :: [CtEvidence] -> WantedConstraints mkSimpleWC cts @@ -980,22 +1036,22 @@ mkImplicWC implic = emptyWC { wc_impl = implic } isEmptyWC :: WantedConstraints -> Bool -isEmptyWC (WC { wc_simple = f, wc_impl = i, wc_holes = holes }) - = isEmptyBag f && isEmptyBag i && isEmptyBag holes +isEmptyWC (WC { wc_simple = f, wc_impl = i, wc_errors = errors }) + = isEmptyBag f && isEmptyBag i && isEmptyBag errors -- | Checks whether a the given wanted constraints are solved, i.e. -- that there are no simple constraints left and all the implications -- are solved. isSolvedWC :: WantedConstraints -> Bool -isSolvedWC WC {wc_simple = wc_simple, wc_impl = wc_impl, wc_holes = holes} = - isEmptyBag wc_simple && allBag (isSolvedStatus . ic_status) wc_impl && isEmptyBag holes +isSolvedWC WC {wc_simple = wc_simple, wc_impl = wc_impl, wc_errors = errors} = + isEmptyBag wc_simple && allBag (isSolvedStatus . ic_status) wc_impl && isEmptyBag errors andWC :: WantedConstraints -> WantedConstraints -> WantedConstraints -andWC (WC { wc_simple = f1, wc_impl = i1, wc_holes = h1 }) - (WC { wc_simple = f2, wc_impl = i2, wc_holes = h2 }) +andWC (WC { wc_simple = f1, wc_impl = i1, wc_errors = e1 }) + (WC { wc_simple = f2, wc_impl = i2, wc_errors = e2 }) = WC { wc_simple = f1 `unionBags` f2 , wc_impl = i1 `unionBags` i2 - , wc_holes = h1 `unionBags` h2 } + , wc_errors = e1 `unionBags` e2 } unionsWC :: [WantedConstraints] -> WantedConstraints unionsWC = foldr andWC emptyWC @@ -1014,29 +1070,40 @@ addInsols wc cts addHoles :: WantedConstraints -> Bag Hole -> WantedConstraints addHoles wc holes - = wc { wc_holes = holes `unionBags` wc_holes wc } + = wc { wc_errors = mapBag DE_Hole holes `unionBags` wc_errors wc } + +addNotConcreteError :: WantedConstraints -> NotConcreteError -> WantedConstraints +addNotConcreteError wc err + = wc { wc_errors = unitBag (DE_NotConcrete err) `unionBags` wc_errors wc } + +addDelayedErrors :: WantedConstraints -> Bag DelayedError -> WantedConstraints +addDelayedErrors wc errs + = wc { wc_errors = errs `unionBags` wc_errors wc } dropMisleading :: WantedConstraints -> WantedConstraints -- Drop misleading constraints; really just class constraints -- See Note [Constraints and errors] in GHC.Tc.Utils.Monad -- for why this function is so strange, treating the 'simples' -- and the implications differently. Sigh. -dropMisleading (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes }) +dropMisleading (WC { wc_simple = simples, wc_impl = implics, wc_errors = errors }) = WC { wc_simple = filterBag insolubleWantedCt simples , wc_impl = mapBag drop_implic implics - , wc_holes = filterBag isOutOfScopeHole holes } + , wc_errors = filterBag keep_delayed_error errors } where drop_implic implic = implic { ic_wanted = drop_wanted (ic_wanted implic) } - drop_wanted (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes }) + drop_wanted (WC { wc_simple = simples, wc_impl = implics, wc_errors = errors }) = WC { wc_simple = filterBag keep_ct simples , wc_impl = mapBag drop_implic implics - , wc_holes = filterBag isOutOfScopeHole holes } + , wc_errors = filterBag keep_delayed_error errors } keep_ct ct = case classifyPredType (ctPred ct) of ClassPred {} -> False _ -> True + keep_delayed_error (DE_Hole hole) = isOutOfScopeHole hole + keep_delayed_error (DE_NotConcrete {}) = True + isSolvedStatus :: ImplicStatus -> Bool isSolvedStatus (IC_Solved {}) = True isSolvedStatus _ = False @@ -1049,11 +1116,62 @@ isInsolubleStatus _ = False insolubleImplic :: Implication -> Bool insolubleImplic ic = isInsolubleStatus (ic_status ic) +-- | Gather all the type variables from 'WantedConstraints' +-- that it would be unhelpful to default. For the moment, +-- these are only 'ConcreteTv' metavariables participating +-- in a nominal equality whose other side is not concrete; +-- it's usually better to report those as errors instead of +-- defaulting. +nonDefaultableTyVarsOfWC :: WantedConstraints -> TyCoVarSet +-- Currently used in simplifyTop and in tcRule. +-- TODO: should we also use this in decideQuantifiedTyVars, kindGeneralize{All,Some}? +nonDefaultableTyVarsOfWC (WC { wc_simple = simples, wc_impl = implics, wc_errors = errs }) + = concatMapBag non_defaultable_tvs_of_ct simples + `unionVarSet` concatMapBag (nonDefaultableTyVarsOfWC . ic_wanted) implics + `unionVarSet` concatMapBag non_defaultable_tvs_of_err errs + where + + concatMapBag :: (a -> TyVarSet) -> Bag a -> TyCoVarSet + concatMapBag f = foldr (\ r acc -> f r `unionVarSet` acc) emptyVarSet + + -- Don't default ConcreteTv metavariables involved + -- in an equality with something non-concrete: it's usually + -- better to report the unsolved Wanted. + -- + -- Example: alpha[conc] ~# rr[sk]. + non_defaultable_tvs_of_ct :: Ct -> TyCoVarSet + non_defaultable_tvs_of_ct ct = + -- NB: using classifyPredType instead of inspecting the Ct + -- so that we deal uniformly with CNonCanonical (which come up in tcRule), + -- CEqCan (unsolved but potentially soluble, e.g. @alpha[conc] ~# RR@) + -- and CIrredCan. + case classifyPredType $ ctPred ct of + EqPred NomEq lhs rhs + | Just tv <- getTyVar_maybe lhs + , isConcreteTyVar tv + , not (isConcrete rhs) + -> unitVarSet tv + | Just tv <- getTyVar_maybe rhs + , isConcreteTyVar tv + , not (isConcrete lhs) + -> unitVarSet tv + _ -> emptyVarSet + + -- Make sure to apply the same logic as above to delayed errors. + non_defaultable_tvs_of_err (DE_NotConcrete err) + = case err of + NCE_FRR { nce_frr_origin = frr } -> tyCoVarsOfType (frr_type frr) + non_defaultable_tvs_of_err (DE_Hole {}) = emptyVarSet + insolubleWC :: WantedConstraints -> Bool -insolubleWC (WC { wc_impl = implics, wc_simple = simples, wc_holes = holes }) +insolubleWC (WC { wc_impl = implics, wc_simple = simples, wc_errors = errors }) = anyBag insolubleWantedCt simples || anyBag insolubleImplic implics - || anyBag isOutOfScopeHole holes -- See Note [Insoluble holes] + || anyBag is_insoluble errors + + where + is_insoluble (DE_Hole hole) = isOutOfScopeHole hole -- See Note [Insoluble holes] + is_insoluble (DE_NotConcrete {}) = True insolubleWantedCt :: Ct -> Bool -- Definitely insoluble, in particular /excluding/ type-hole constraints @@ -1120,11 +1238,11 @@ isOutOfScopeHole :: Hole -> Bool isOutOfScopeHole (Hole { hole_occ = occ }) = not (startsWithUnderscore occ) instance Outputable WantedConstraints where - ppr (WC {wc_simple = s, wc_impl = i, wc_holes = h}) + ppr (WC {wc_simple = s, wc_impl = i, wc_errors = e}) = text "WC" <+> braces (vcat [ ppr_bag (text "wc_simple") s , ppr_bag (text "wc_impl") i - , ppr_bag (text "wc_holes") h ]) + , ppr_bag (text "wc_errors") e ]) ppr_bag :: Outputable a => SDoc -> Bag a -> SDoc ppr_bag doc bag @@ -1715,7 +1833,6 @@ So a Given has EvVar inside it rather than (as previously) an EvTerm. -- | A place for type-checking evidence to go after it is generated. -- -- - Wanted equalities use HoleDest, --- - IsRefl# constraints use NoDest, -- - other Wanteds use EvVarDest. data TcEvDest = EvVarDest EvVar -- ^ bind this var to the evidence @@ -1726,9 +1843,6 @@ data TcEvDest -- HoleDest is always used for type-equalities -- See Note [Coercion holes] in GHC.Core.TyCo.Rep - | NoDest -- ^ we don't need to record any evidence. - -- This is used for 'IsRefl#' constraints. - data CtEvidence = CtGiven -- Truly given, not depending on subgoals { ctev_pred :: TcPredType -- See Note [Ct/evidence invariant] @@ -1787,12 +1901,10 @@ ctEvCoercion (CtWanted { ctev_dest = dest }) ctEvCoercion ev = pprPanic "ctEvCoercion" (ppr ev) -ctEvEvId :: HasDebugCallStack => CtEvidence -> EvVar +ctEvEvId :: CtEvidence -> EvVar ctEvEvId (CtWanted { ctev_dest = EvVarDest ev }) = ev ctEvEvId (CtWanted { ctev_dest = HoleDest h }) = coHoleCoVar h ctEvEvId (CtGiven { ctev_evar = ev }) = ev -ctEvEvId wt@(CtWanted { ctev_dest = NoDest }) - = pprPanic "ctEvEvId: NoDest" (ppr wt) ctEvUnique :: CtEvidence -> Unique ctEvUnique (CtGiven { ctev_evar = ev }) = varUnique ev @@ -1801,7 +1913,6 @@ ctEvUnique (CtWanted { ctev_dest = dest }) = tcEvDestUnique dest tcEvDestUnique :: TcEvDest -> Unique tcEvDestUnique (EvVarDest ev_var) = varUnique ev_var tcEvDestUnique (HoleDest co_hole) = varUnique (coHoleCoVar co_hole) -tcEvDestUnique NoDest = panic "tcEvDestUnique: NoDest" setCtEvLoc :: CtEvidence -> CtLoc -> CtEvidence setCtEvLoc ctev loc = ctev { ctev_loc = loc } @@ -1832,12 +1943,10 @@ setCtEvPredType old_ctev new_pred new_dest = case dest of EvVarDest ev -> EvVarDest (setVarType ev new_pred) HoleDest h -> HoleDest (setCoHoleType h new_pred) - NoDest -> NoDest instance Outputable TcEvDest where ppr (HoleDest h) = text "hole" <> ppr h ppr (EvVarDest ev) = ppr ev - ppr NoDest = text "NoDest" instance Outputable CtEvidence where ppr ev = ppr (ctEvFlavour ev) diff --git a/compiler/GHC/Tc/Types/Evidence.hs b/compiler/GHC/Tc/Types/Evidence.hs index 74240b1f94..c6c0c7b0ca 100644 --- a/compiler/GHC/Tc/Types/Evidence.hs +++ b/compiler/GHC/Tc/Types/Evidence.hs @@ -8,7 +8,8 @@ module GHC.Tc.Types.Evidence ( -- * HsWrapper HsWrapper(..), (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, - mkWpLams, mkWpLet, mkWpFun, mkWpCastN, mkWpCastR, collectHsWrapBinders, + mkWpLams, mkWpLet, mkWpFun, mkWpCastN, mkWpCastR, + collectHsWrapBinders, idHsWrapper, isIdHsWrapper, pprHsWrapper, hsWrapDictBinders, @@ -43,7 +44,9 @@ module GHC.Tc.Types.Evidence ( mkTcReflCo, mkTcNomReflCo, mkTcRepReflCo, mkTcTyConAppCo, mkTcAppCo, mkTcFunCo, mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos, - mkTcSymCo, mkTcSymMCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcSubCo, maybeTcSymCo, + mkTcSymCo, mkTcSymMCo, + mkTcTransCo, + mkTcNthCo, mkTcLRCo, mkTcSubCo, maybeTcSymCo, maybeTcSubCo, tcDowngradeRole, mkTcAxiomRuleCo, mkTcGReflRightCo, mkTcGReflRightMCo, mkTcGReflLeftCo, mkTcGReflLeftMCo, mkTcPhantomCo, @@ -225,7 +228,7 @@ data HsWrapper -- Hence (\a. []) `WpCompose` (\b. []) = (\a b. []) -- But ([] a) `WpCompose` ([] b) = ([] b a) - | WpFun HsWrapper HsWrapper (Scaled TcType) + | WpFun HsWrapper HsWrapper (Scaled TcTypeFRR) -- (WpFun wrap1 wrap2 (w, t1))[e] = \(x:_w t1). wrap2[ e wrap1[x] ] -- So note that if wrap1 :: exp_arg <= act_arg -- wrap2 :: act_res <= exp_res @@ -283,16 +286,17 @@ c1 <.> c2 = c1 `WpCompose` c2 -- | Smart constructor to create a 'WpFun' 'HsWrapper'. -- --- PRECONDITION: the "from" type of the first wrapper must have a +-- PRECONDITION: the "from" type of the first wrapper must have a syntactically -- fixed RuntimeRep (see Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete). mkWpFun :: HsWrapper -> HsWrapper - -> Scaled TcType -- ^ the "from" type of the first wrapper - -- MUST have a fixed RuntimeRep - -> TcType -- ^ either type of the second wrapper (used only when the - -- second wrapper is the identity) + -> Scaled TcTypeFRR -- ^ the "from" type of the first wrapper + -- MUST have a fixed RuntimeRep + -> TcType -- ^ either type of the second wrapper (used only when the + -- second wrapper is the identity) -> HsWrapper - -- NB: can't check that the argument type has a fixed RuntimeRep with an assertion, - -- as we will only be able to know that after typechecking. + -- NB: we can't check that the argument type has a fixed RuntimeRep with an assertion, + -- because of [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep] + -- in GHC.Tc.Utils.Concrete. mkWpFun WpHole WpHole _ _ = WpHole mkWpFun WpHole (WpCast co2) (Scaled w t1) _ = WpCast (mkTcFunCo Representational (multToCo w) (mkTcRepReflCo t1) co2) mkWpFun (WpCast co1) WpHole (Scaled w _) t2 = WpCast (mkTcFunCo Representational (multToCo w) (mkTcSymCo co1) (mkTcRepReflCo t2)) diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs index 54a0f2127e..d088762270 100644 --- a/compiler/GHC/Tc/Types/Origin.hs +++ b/compiler/GHC/Tc/Types/Origin.hs @@ -29,12 +29,12 @@ module GHC.Tc.Types.Origin ( -- * CtOrigin and CallStack isPushCallStackOrigin, callStackOriginFS, -- * FixedRuntimeRep origin - FRROrigin(..), pprFRROrigin, + FixedRuntimeRepOrigin(..), FixedRuntimeRepContext(..), + pprFixedRuntimeRepContext, StmtOrigin(..), -- * Arrow command origin - FRRArrowOrigin(..), pprFRRArrowOrigin, - -- * ExpectedFunTy origin + FRRArrowContext(..), pprFRRArrowContext, ExpectedFunTyOrigin(..), pprExpectedFunTyOrigin, pprExpectedFunTyHerald, ) where @@ -60,7 +60,6 @@ import GHC.Types.Basic import GHC.Types.SrcLoc import GHC.Data.FastString -import qualified GHC.Data.Strict as Strict import GHC.Utils.Outputable import GHC.Utils.Panic @@ -607,10 +606,8 @@ data CtOrigin | CycleBreakerOrigin CtOrigin -- origin of the original constraint -- See Detail (7) of Note [Type variable cycles] in GHC.Tc.Solver.Canonical - | FixedRuntimeRepOrigin - !Type -- ^ The type being checked for representation polymorphism. - -- We record it here for access in 'GHC.Tc.Errors.mkFRRErr'. - !FRROrigin + | FRROrigin + FixedRuntimeRepOrigin | WantedSuperclassOrigin PredType CtOrigin -- From expanding out the superclasses of a Wanted; the PredType @@ -820,11 +817,8 @@ pprCtOrigin (InstProvidedOrigin mod cls_inst) pprCtOrigin (CycleBreakerOrigin orig) = pprCtOrigin orig -pprCtOrigin (FixedRuntimeRepOrigin _ frrOrig) - -- We ignore the type argument, as we would prefer - -- to report all types that don't have a fixed runtime representation at once, - -- in 'GHC.Tc.Errors.mkFRRErr'. - = pprFRROrigin frrOrig +pprCtOrigin (FRROrigin {}) + = ctoHerald <+> text "a representation-polymorphism check" pprCtOrigin (WantedSuperclassOrigin subclass_pred subclass_orig) = sep [ ctoHerald <+> text "a superclass required to satisfy" <+> quotes (ppr subclass_pred) <> comma @@ -906,7 +900,7 @@ pprCtO (Shouldn'tHappenOrigin note) = text note pprCtO (ProvCtxtOrigin {}) = text "a provided constraint" pprCtO (InstProvidedOrigin {}) = text "a provided constraint" pprCtO (CycleBreakerOrigin orig) = pprCtO orig -pprCtO (FixedRuntimeRepOrigin {}) = text "a representation polymorphism check" +pprCtO (FRROrigin {}) = text "a representation-polymorphism check" pprCtO GhcBug20076 = text "GHC Bug #20076" pprCtO (WantedSuperclassOrigin {}) = text "a superclass constraint" pprCtO (InstanceSigOrigin {}) = text "a type signature in an instance" @@ -942,42 +936,59 @@ callStackOriginFS orig = mkFastString (showSDocUnsafe (pprCtO orig Note [Reporting representation-polymorphism errors] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When we emit new Wanted constraints using GHC.Tc.Utils.Concrete.hasFixedRuntimeRep, -we provide a 'CtOrigin' using the 'FixedRuntimeRepOrigin' constructor of, -which keeps track of two things: - - the type which we want to ensure has a fixed runtime representation, - - the 'FRROrigin' explaining the nature of the check, e.g. a pattern, - a function application, a record update, ... - -If the constraint goes unsolved, we report it as follows: - - we detect that the unsolved Wanted has an 'FRROrigin' 'CtOrigin' - in GHC.Tc.Errors.reportWanteds using is_FRR, - - we assemble an error message in GHC.Tc.Errors.mkFRRErr. - -For example, if we try to write the program - - foo :: forall r1 r2 (a :: TYPE r1) (b :: TYPE r2). a -> b -> () - foo x y = () - -we will get two unsolved Wanted constraints, namely - - r1 ~# concrete_tv1, with 'CtOrigin' FixedRuntimeRepOrigin a (FRRVarPattern x) - r2 ~# concrete_tv2, with 'CtOrigin' FixedRuntimeRepOrigin b (FRRVarPattern y) - -These constraints will be processed in tandem by mkFRRErr, -producing an error message of the form: - - Representation-polymorphic types are not allowed here. - * The variable 'x' bound by the pattern - does not have a fixed runtime representation: - a :: TYPE r1 - * The variable 'y' bound by the pattern - does not have a fixed runtime representation: - b :: TYPE r2 +As explained in Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete, +to check that (ty :: ki) has a fixed runtime representation, we emit +an equality constraint of the form + + ki ~# concrete_tv + +where concrete_tv is a concrete metavariable. In this situation, we attach +a 'FixedRuntimeRepOrigin' to both the equality and the concrete type variable. +The 'FixedRuntimeRepOrigin' consists of two pieces of information: + + - the type 'ty' on which we performed the representation-polymorphism check, + - a 'FixedRuntimeRepContext' which explains why we needed to perform a check + (e.g. because 'ty' was the kind of a function argument, or of a bound variable + in a lambda abstraction, ...). + +This information gets passed along as we make progress on solving the constraint, +and if we end up with an unsolved constraint we can report an informative error +message to the user using the 'FixedRuntimeRepOrigin'. + +The error reporting goes through two different paths: + + - constraints whose 'CtOrigin' contains a 'FixedRuntimeRepOrigin' are reported + using 'mkFRRErr' in 'reportWanteds', + - equality constraints in which one side is a concrete metavariable and the + other side is not concrete are reported using 'mkTyVarEqErr'. In this case, + we pass on the type variable and the non-concrete type for error reporting, + using the 'frr_info_not_concrete' field. + +This is why we have the 'FixedRuntimeRepErrorInfo' datatype: so that we can optionally +include this extra message about an unsolved equality between a concrete type variable +and a non-concrete type. -} --- | In what context are we checking that a type has a fixed runtime representation? -data FRROrigin +-- | The context for a representation-polymorphism check. +-- +-- For example, when typechecking @ \ (a :: k) -> ...@, +-- we are checking the type @a@ because it's the type of +-- a term variable bound in a lambda, so we use 'FRRBinder'. +data FixedRuntimeRepOrigin + = FixedRuntimeRepOrigin + { frr_type :: Type + -- ^ What type are we checking? + -- For example, `a[tau]` in `a[tau] :: TYPE rr[tau]`. + + , frr_context :: FixedRuntimeRepContext + -- ^ What context requires a fixed runtime representation? + } + +-- | The context in which a representation-polymorphism check was performed. +-- +-- Does not include the type on which the check was performed; see +-- 'FixedRuntimeRepOrigin' for that. +data FixedRuntimeRepContext -- | Record fields in record updates must have a fixed runtime representation. -- @@ -989,6 +1000,16 @@ data FRROrigin -- Test cases: LevPolyLet, RepPolyPatBind. | FRRBinder !Name + -- | Pattern binds must have a fixed runtime representation. + -- + -- Test case: RepPolyInferPatBind. + | FRRPatBind + + -- | Pattern synonym arguments must have a fixed runtime representation. + -- + -- Test case: RepPolyInferPatSyn. + | FRRPatSynArg + -- | The type of the scrutinee in a case statement must have a -- fixed runtime representation. -- @@ -1051,8 +1072,8 @@ data FRROrigin -- | A representation-polymorphism check arising from arrow notation. -- - -- See 'FRRArrowOrigin' for more details. - | FRRArrow !FRRArrowOrigin + -- See 'FRRArrowContext' for more details. + | FRRArrow !FRRArrowContext -- | A representation-polymorphic check arising from a call -- to 'matchExpectedFunTys' or 'matchActualFunTySigma'. @@ -1061,22 +1082,27 @@ data FRROrigin | FRRExpectedFunTy !ExpectedFunTyOrigin !Int - -- ^ argument position (0-indexed) + -- ^ argument position (1-indexed) -- | Print the context for a @FixedRuntimeRep@ representation-polymorphism check. -- -- Note that this function does not include the specific 'RuntimeRep' --- which is not fixed. That information is added by 'GHC.Tc.Errors.mkFRRErr'. -pprFRROrigin :: FRROrigin -> SDoc -pprFRROrigin (FRRRecordUpdate lbl _arg) +-- which is not fixed. That information is stored in 'FixedRuntimeRepOrigin' +-- and is reported separately. +pprFixedRuntimeRepContext :: FixedRuntimeRepContext -> SDoc +pprFixedRuntimeRepContext (FRRRecordUpdate lbl _arg) = sep [ text "The record update at field" , quotes (ppr lbl) ] -pprFRROrigin (FRRBinder binder) +pprFixedRuntimeRepContext (FRRBinder binder) = sep [ text "The binder" , quotes (ppr binder) ] -pprFRROrigin FRRCase +pprFixedRuntimeRepContext FRRPatBind + = text "The pattern binding" +pprFixedRuntimeRepContext FRRPatSynArg + = text "The pattern synonym argument pattern" +pprFixedRuntimeRepContext FRRCase = text "The scrutinee of the case statement" -pprFRROrigin (FRRDataConArg expr_or_pat con i) +pprFixedRuntimeRepContext (FRRDataConArg expr_or_pat con i) = text "The" <+> what where arg, what :: SDoc @@ -1088,33 +1114,33 @@ pprFRROrigin (FRRDataConArg expr_or_pat con i) = text "newtype constructor" <+> arg | otherwise = text "data constructor" <+> arg <+> text "in" <+> speakNth i <+> text "position" -pprFRROrigin (FRRNoBindingResArg fn i) +pprFixedRuntimeRepContext (FRRNoBindingResArg fn i) = vcat [ text "Unsaturated use of a representation-polymorphic primitive function." , text "The" <+> speakNth i <+> text "argument of" <+> quotes (ppr $ getName fn) ] -pprFRROrigin (FRRTupleArg i) +pprFixedRuntimeRepContext (FRRTupleArg i) = text "The tuple argument in" <+> speakNth i <+> text "position" -pprFRROrigin (FRRTupleSection i) +pprFixedRuntimeRepContext (FRRTupleSection i) = text "The" <+> speakNth i <+> text "component of the tuple section" -pprFRROrigin FRRUnboxedSum +pprFixedRuntimeRepContext FRRUnboxedSum = text "The unboxed sum" -pprFRROrigin (FRRBodyStmt stmtOrig i) +pprFixedRuntimeRepContext (FRRBodyStmt stmtOrig i) = vcat [ text "The" <+> speakNth i <+> text "argument to (>>)" <> comma , text "arising from the" <+> ppr stmtOrig <> comma ] -pprFRROrigin FRRBodyStmtGuard +pprFixedRuntimeRepContext FRRBodyStmtGuard = vcat [ text "The argument to" <+> quotes (text "guard") <> comma , text "arising from the" <+> ppr MonadComprehension <> comma ] -pprFRROrigin (FRRBindStmt stmtOrig) +pprFixedRuntimeRepContext (FRRBindStmt stmtOrig) = vcat [ text "The first argument to (>>=)" <> comma , text "arising from the" <+> ppr stmtOrig <> comma ] -pprFRROrigin FRRBindStmtGuard +pprFixedRuntimeRepContext FRRBindStmtGuard = sep [ text "The body of the bind statement" ] -pprFRROrigin (FRRArrow arrowOrig) - = pprFRRArrowOrigin arrowOrig -pprFRROrigin (FRRExpectedFunTy funTyOrig zero_indexed_arg) - = pprExpectedFunTyOrigin funTyOrig (zero_indexed_arg + 1) +pprFixedRuntimeRepContext (FRRArrow arrowContext) + = pprFRRArrowContext arrowContext +pprFixedRuntimeRepContext (FRRExpectedFunTy funTyOrig arg_pos) + = pprExpectedFunTyOrigin funTyOrig arg_pos -instance Outputable FRROrigin where - ppr = pprFRROrigin +instance Outputable FixedRuntimeRepContext where + ppr = pprFixedRuntimeRepContext -- | Are we in a @do@ expression or a monad comprehension? -- @@ -1136,8 +1162,9 @@ instance Outputable StmtOrigin where -- | While typechecking arrow notation, in which context -- did a representation polymorphism check arise? -- --- See 'FRROrigin' for more general origins of representation polymorphism checks. -data FRRArrowOrigin +-- See 'FixedRuntimeRepContext' for more general origins of +-- representation polymorphism checks. +data FRRArrowContext -- | The result of an arrow command does not have a fixed runtime representation. -- @@ -1156,60 +1183,39 @@ data FRRArrowOrigin -- Test cases: none. | ArrowCmdArrApp !(HsExpr GhcRn) !(HsExpr GhcRn) !HsArrAppType - -- | A pattern in an arrow command abstraction does not have - -- a fixed runtime representation. - -- - -- Test cases: none. - | ArrowCmdLam !Int - -- | The scrutinee type in an arrow command case statement does not have a -- fixed runtime representation. -- -- Test cases: none. | ArrowCmdCase - -- | A pattern in an arrow command \cases statement does not - -- have a fixed runtime representation. - -- - -- Test cases: none. - | ArrowCmdLamCase !(Strict.Maybe Int) - -- ^ @Nothing@ for @\case@, @Just@ the index of the pattern for @\cases@ - -- (starting from 1) - -- | The overall type of an arrow proc expression does not have -- a fixed runtime representation. -- -- Test case: RepPolyArrowFun. | ArrowFun !(HsExpr GhcRn) -pprFRRArrowOrigin :: FRRArrowOrigin -> SDoc -pprFRRArrowOrigin (ArrowCmdResTy cmd) +pprFRRArrowContext :: FRRArrowContext -> SDoc +pprFRRArrowContext (ArrowCmdResTy cmd) = vcat [ hang (text "The arrow command") 2 (quotes (ppr cmd)) ] -pprFRRArrowOrigin (ArrowCmdApp fun arg) +pprFRRArrowContext (ArrowCmdApp fun arg) = vcat [ text "The argument in the arrow command application of" , nest 2 (quotes (ppr fun)) , text "to" , nest 2 (quotes (ppr arg)) ] -pprFRRArrowOrigin (ArrowCmdArrApp fun arg ho_app) +pprFRRArrowContext (ArrowCmdArrApp fun arg ho_app) = vcat [ text "The function in the" <+> pprHsArrType ho_app <+> text "of" , nest 2 (quotes (ppr fun)) , text "to" , nest 2 (quotes (ppr arg)) ] -pprFRRArrowOrigin (ArrowCmdLam i) - = vcat [ text "The" <+> speakNth i <+> text "pattern of the arrow command abstraction" ] -pprFRRArrowOrigin ArrowCmdCase +pprFRRArrowContext ArrowCmdCase = text "The scrutinee of the arrow case command" -pprFRRArrowOrigin (ArrowCmdLamCase Strict.Nothing) - = text "The scrutinee of the arrow \\case command" -pprFRRArrowOrigin (ArrowCmdLamCase (Strict.Just i)) - = text "The" <+> speakNth i - <+> text "scrutinee of the arrow \\cases command" -pprFRRArrowOrigin (ArrowFun fun) +pprFRRArrowContext (ArrowFun fun) = vcat [ text "The return type of the arrow function" , nest 2 (quotes (ppr fun)) ] -instance Outputable FRRArrowOrigin where - ppr = pprFRRArrowOrigin +instance Outputable FRRArrowContext where + ppr = pprFRRArrowContext {- ********************************************************************* * * @@ -1231,7 +1237,8 @@ instance Outputable FRRArrowOrigin where -- doesn't have a fixed RuntimeRep as per Note [Fixed RuntimeRep] -- in GHC.Tc.Utils.Concrete. -- Uses 'pprExpectedFunTyOrigin'. --- See 'FRROrigin' for more general origins of representation polymorphism checks. +-- See 'FixedRuntimeRepContext' for the situations in which +-- representation-polymorphism checks are performed. data ExpectedFunTyOrigin -- | A rebindable syntax operator is expected to have a function type. diff --git a/compiler/GHC/Tc/Types/Origin.hs-boot b/compiler/GHC/Tc/Types/Origin.hs-boot index 1110cc0967..eecb8cb490 100644 --- a/compiler/GHC/Tc/Types/Origin.hs-boot +++ b/compiler/GHC/Tc/Types/Origin.hs-boot @@ -4,5 +4,7 @@ import GHC.Stack ( HasCallStack ) data SkolemInfoAnon data SkolemInfo +data FixedRuntimeRepContext +data FixedRuntimeRepOrigin unkSkol :: HasCallStack => SkolemInfo diff --git a/compiler/GHC/Tc/Utils/Concrete.hs b/compiler/GHC/Tc/Utils/Concrete.hs index 22ba6b45e3..da9efb7ef3 100644 --- a/compiler/GHC/Tc/Utils/Concrete.hs +++ b/compiler/GHC/Tc/Utils/Concrete.hs @@ -7,32 +7,45 @@ module GHC.Tc.Utils.Concrete ( -- * Ensuring that a type has a fixed runtime representation hasFixedRuntimeRep - , hasFixedRuntimeRep_MustBeRefl + , hasFixedRuntimeRep_syntactic + + -- * Making a type concrete + , makeTypeConcrete ) where import GHC.Prelude -import GHC.Builtin.Types ( unliftedTypeKindTyCon, liftedTypeKindTyCon ) - -import GHC.Core.Coercion ( Role(..) ) -import GHC.Core.Predicate ( mkIsReflPrimPred ) -import GHC.Core.TyCo.Rep ( Type(TyConApp), mkTyVarTy ) -import GHC.Core.Type ( isConcrete, typeKind ) - -import GHC.Tc.Types ( TcM, ThStage(Brack), PendingStuff(TcPending) ) -import GHC.Tc.Types.Constraint ( mkNonCanonical ) -import GHC.Tc.Types.Evidence ( TcCoercion ) -import GHC.Tc.Types.Origin ( CtOrigin(..), FRROrigin(..) ) -import GHC.Tc.Utils.Monad ( emitSimple, getStage ) -import GHC.Tc.Utils.TcType ( TcType, TcKind, TcTyVar, MetaInfo(ConcreteTv) ) -import GHC.Tc.Utils.TcMType ( newAnonMetaTyVar, newWanted, emitWantedEq ) +import GHC.Builtin.Types ( liftedTypeKindTyCon, unliftedTypeKindTyCon ) + +import GHC.Core.Coercion ( coToMCo, mkCastTyMCo ) +import GHC.Core.TyCo.Rep ( Type(..), MCoercion(..) ) +import GHC.Core.TyCon ( isConcreteTyCon ) +import GHC.Core.Type ( isConcrete, typeKind, tyVarKind, tcView + , mkTyVarTy, mkTyConApp, mkFunTy, mkAppTy ) + +import GHC.Tc.Types ( TcM, ThStage(..), PendingStuff(..) ) +import GHC.Tc.Types.Constraint ( NotConcreteError(..), NotConcreteReason(..) ) +import GHC.Tc.Types.Evidence ( Role(..), TcCoercionN, TcMCoercionN + , mkTcGReflRightMCo, mkTcNomReflCo ) +import GHC.Tc.Types.Origin ( CtOrigin(..), FixedRuntimeRepContext, FixedRuntimeRepOrigin(..) ) +import GHC.Tc.Utils.Monad ( emitNotConcreteError, setTcLevel, getCtLocM, getStage, traceTc ) +import GHC.Tc.Utils.TcType ( TcType, TcKind, TcTypeFRR + , MetaInfo(..), ConcreteTvOrigin(..) + , isMetaTyVar, metaTyVarInfo, tcTyVarLevel ) +import GHC.Tc.Utils.TcMType ( newConcreteTyVar, isFilledMetaTyVar_maybe, writeMetaTyVar + , emitWantedEq ) import GHC.Types.Basic ( TypeOrKind(..) ) - import GHC.Utils.Misc ( HasDebugCallStack ) import GHC.Utils.Outputable -import GHC.Utils.Panic ( assertPpr ) + +import Control.Monad ( void ) +import Data.Functor ( ($>) ) +import Data.List.NonEmpty ( NonEmpty((:|)) ) + +import Control.Monad.Trans.Class ( lift ) +import Control.Monad.Trans.Writer.CPS ( WriterT, runWriterT, tell ) {- Note [Concrete overview] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -109,8 +122,8 @@ as a central point of reference for this topic. Note [Reporting representation-polymorphism errors] in GHC.Tc.Types.Origin When we emit a constraint to enforce a fixed representation, we also provide - a 'FRROrigin' which gives context about the check being done. This origin gets - reported to the user if we end up with such an an unsolved Wanted constraint. + a 'FixedRuntimeRepOrigin' which gives context about the check being done. + This origin gets reported to the user if we end up with such an an unsolved Wanted constraint. Note [Representation polymorphism checking] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -166,7 +179,7 @@ Definition: a type is /concrete/ iff it is: - a concrete type constructor (as defined below), or - a concrete type variable (see Note [ConcreteTv] below), or - an application of a concrete type to another concrete type - See GHC.Core.Type.isConcrete +GHC.Core.Type.isConcrete checks whether a type meets this definition. Definition: a /concrete type constructor/ is defined by - a promoted data constructor @@ -175,7 +188,7 @@ Definition: a /concrete type constructor/ is defined by - an abstract type as defined in a Backpack signature file (see Note [Synonyms implement abstract data] in GHC.Tc.Module) In particular, type and data families are not concrete. - See GHC.Core.TyCon.isConcreteTyCon. +GHC.Core.TyCon.isConcreteTyCon checks whether a TyCon meets this definition. Examples of concrete types: Lifted, BoxedRep Lifted, TYPE (BoxedRep Lifted) are all concrete @@ -194,9 +207,6 @@ concrete metavariable is itself concrete (see Note [ConcreteTv]): Concrete Kinds Property (CKP) The kind of a concrete type is concrete. -The CCP and the CKP taken together mean that we never have to inspect -in kinds to check concreteness. - Note [ConcreteTv] ~~~~~~~~~~~~~~~~~ A concrete metavariable is a metavariable whose 'MetaInfo' is 'ConcreteTv'. @@ -224,8 +234,9 @@ To check (ty :: ki) has a fixed runtime representation, we proceed as follows: ki ~# concrete_tv The origin for such an equality constraint uses - `GHC.Tc.Types.Origin.FRROrigin`, so that we can report the appropriate - representation-polymorphism error if any such constraint goes unsolved. + `GHC.Tc.Types.Origin.FixedRuntimeRepOrigin`, so that we can report the + appropriate representation-polymorphism error if any such constraint + goes unsolved. To solve `ki ~# concrete_ki`, we must unify `concrete_tv := concrete_ki`, where `concrete_ki` is some concrete type. We can then compute `kindPrimRep` @@ -238,19 +249,16 @@ has a fixed runtime representation. The Concrete mechanism is being implemented in two separate phases. -In PHASE 1 (currently implemented), we enforce that we only solve the emitted -constraints `co :: ki ~# concrete_tv` with `Refl`. This forbids any program +In PHASE 1, we enforce that we only solve the emitted constraints +`co :: ki ~# concrete_tv` with `Refl`. This forbids any program which requires type family evaluation in order to determine that a 'RuntimeRep' -is fixed. We do this using the `IsRefl#` special predicate (see Note [IsRefl#]); -we only solve `IsRefl# a b` if `a` and `b` are equal (after zonking, but not rewriting). -This means that it is safe to not use the coercion `co` anywhere in the program. -PHASE 1 corresponds to calls to `hasFixedRuntimeRep_MustBeRefl` in the code: on top -of emitting a constraint of the form `ki ~# concrete_tv`, we also emit -`IsRefl# ki concrete_tv` to ensure we only solve the equality constraint using -reflexivity. +is fixed. +To achieve this, instead of creating a new concrete metavariable, we directly +ensure that 'ki' is concrete, using 'makeTypeConcrete'. If it fails, then +we report an error (even though rewriting might have allowed us to proceed). In PHASE 2, we lift this restriction. This means we replace a call to -`hasFixedRuntimeRep_MustBeRefl` with a call to `hasFixedRuntimeRep`, and insert the +`hasFixedRuntimeRep_syntactic` with a call to `hasFixedRuntimeRep`, and insert the obtained coercion in the typechecked result. To illustrate what this entails, recall that the code generator needs to be able to compute 'PrimRep's, so that it can put function arguments in the correct registers, etc. @@ -274,17 +282,37 @@ this would be: As `( a |> kco ) :: TYPE Int#`, the code generator knows to use a machine-sized integer register for `x`, and all is good again. +Because we can convert calls from hasFixedRuntimeRep_syntactic to +hasFixedRuntimeRep one at a time, we can migrate from PHASE 1 to PHASE 2 +incrementally. + Example test cases that require PHASE 2: T13105, T17021, T20363b. Note [Fixed RuntimeRep] ~~~~~~~~~~~~~~~~~~~~~~~ -Definition: - a type `ty :: ki` has a /fixed RuntimeRep/ - <=> - there exists a concrete type `concrete_ty` (in the sense of Note [Concrete types]) - such that we can solve `ki ~# concrete_ty`. +Definitions: -This definition is crafted to be useful to satisfy the invariants of + FRR. + + The type `ty :: ki` has a /syntactically fixed RuntimeRep/ + (we also say that `ty` is an `FRRType`) + <=> + the kind `ki` is concrete (in the sense of Note [Concrete types]) + <=> + `typePrimRep ty` (= `kindPrimRep ki`) does not crash + (assuming that typechecking succeeded, so that all metavariables + in `ty` have been filled) + + Fixed RuntimeRep. + + The type `ty :: ki` has a /fixed RuntimeRep/ + <=> + there exists an FRR type `ty'` with `ty ~# ty'` + <=> + there exists a concrete type `concrete_ki` such that + `ki ~ concrete_ki` + +These definitions are crafted to be useful to satisfy the invariants of Core; see Note [Representation polymorphism invariants] in GHC.Core. Notice that "fixed RuntimeRep" means (for now anyway) that @@ -307,6 +335,16 @@ To do so, we compute the kind 'ki' of 'ty', create a new concrete metavariable `concrete_tv` of kind `ki`, and emit a constraint `ki ~# concrete_tv`, which will only be solved if we can prove that 'ty' indeed has a fixed RuntimeRep. +If we can solve the equality constraint, i.e. produce a coercion +`kco :: ki ~# concrete_tv`, then 'hasFixedRuntimeRep' returns the coercion + + co = GRefl ty kco :: ty ~# ty |> kco + +The RHS of the coercion `co` is `ty |> kco`. The kind of this type is +concrete (by construction), which means that `ty |> kco` is an FRRType +in the sense of Note [Fixed RuntimeRep], so that we can directely compute +its runtime representation using `typePrimRep`. + [Wrinkle: Typed Template Haskell] We don't perform any checks when type-checking a typed Template Haskell quote: we want to allow representation polymorphic quotes, as long as they are @@ -338,132 +376,309 @@ which will only be solved if we can prove that 'ty' indeed has a fixed RuntimeRe this shouldn't cause any problems in practice. See ticket #18170. Test case: rep-poly/T18170a. - -Note [IsRefl#] -~~~~~~~~~~~~~~ -`IsRefl# :: forall k. k -> k -> TYPE (TupleRep '[])` is a constraint with no -evidence. `IsRefl# a b' can be solved precisely when `a` and `b` are equal (up to zonking, -but __without__ any rewriting). - -That is, if we have a type family `F` with `F Int` reducing to `Int`, we __cannot__ solve -`IsRefl# (F Int) Int`. - -What is the point of such a constraint? As outlined in Note [The Concrete mechanism], -to check `ty :: ki` has a fixed RuntimeRep we create a concrete metavariable `concrete_tv` -and emit a Wanted equality constraint - - {co_hole} :: ki ~# concrete_tv - -Then, when we fill in the coercion hole with a coercion `co`, we must make use of it -(as that Note explains). If we don't, then we can only safely discard it if it is -reflexive. Therefore, whenever we perform a representation polymorphism check but also -discard the resulting coercion, we also emit a special constraint `IsRefl# ki concrete_tv`. -See 'hasFixedRuntimeRep_MustBeRefl', which calls 'hasFixedRuntimeRep', and thenemits -an 'IsRefl#' constraint to ensure that discarding the coercion is safe. -} --- | Like 'hasFixedRuntimeRep', but we insist that the obtained coercion must be 'Refl'. +-- | Given a type @ty :: ki@, this function ensures that @ty@ +-- has a __fixed__ 'RuntimeRep', by emitting a new equality constraint +-- @ki ~ concrete_tv@ for a concrete metavariable @concrete_tv@. +-- +-- Returns a coercion @co :: ty ~# concrete_ty@ as evidence. +-- If @ty@ obviously has a fixed 'RuntimeRep', e.g @ki = IntRep@, +-- then this function immediately returns 'MRefl', +-- without emitting any constraints. +hasFixedRuntimeRep :: HasDebugCallStack + => FixedRuntimeRepContext + -- ^ Context to be reported to the user + -- if the type ends up not having a fixed + -- 'RuntimeRep'. + -> TcType + -- ^ The type to check (we only look at its kind). + -> TcM (TcCoercionN, TcTypeFRR) + -- ^ @(co, ty')@ where @ty' :: ki'@, + -- @ki@ is concrete, and @co :: ty ~# ty'@. + -- That is, @ty'@ has a syntactically fixed RuntimeRep + -- in the sense of Note [Fixed RuntimeRep]. +hasFixedRuntimeRep frr_ctxt ty = checkFRR_with unifyConcrete frr_ctxt ty + +-- | Like 'hasFixedRuntimeRep', but we perform an eager syntactic check. +-- +-- Throws an error in the 'TcM' monad if the check fails. -- -- This is useful if we are not actually going to use the coercion returned -- from 'hasFixedRuntimeRep'; it would generally be unsound to allow a non-reflexive --- coercion but not actually make use of it in a cast. See Note [IsRefl#]. +-- coercion but not actually make use of it in a cast. -- -- The goal is to eliminate all uses of this function and replace them with --- 'hasFixedRuntimeRep', making use of the returned coercion. -hasFixedRuntimeRep_MustBeRefl :: FRROrigin -> TcType -> TcM () -hasFixedRuntimeRep_MustBeRefl frr_orig ty - = do { -- STEP 1: check that the type has a fixed 'RuntimeRep'. - mb_co <- hasFixedRuntimeRep frr_orig ty - -- STEP 2: ensure that we only solve using a reflexive coercion. - ; case mb_co of - -- If the coercion is immediately reflexive: we're OK. - { Nothing -> return () - -- Otherwise: emit an @IsRefl#@ constraint. - -- This means we are free to discard the coercion. - ; Just (ki, _co, concrete_kv) -> - do { isRefl_ctev <- newWanted (FixedRuntimeRepOrigin ty frr_orig) - (Just KindLevel) $ - mkIsReflPrimPred ki (mkTyVarTy concrete_kv) - ; emitSimple $ mkNonCanonical isRefl_ctev } } } - --- | Given a type @ty :: ki@, this function ensures that @ty@ --- has a __fixed__ 'RuntimeRep', by emitting a new equality constraint --- @ki ~ concrete_tv@ for a concrete metavariable @concrete_tv@. +-- 'hasFixedRuntimeRep', making use of the returned coercion. This is what +-- is meant by going from PHASE 1 to PHASE 2, in Note [The Concrete mechanism]. +hasFixedRuntimeRep_syntactic :: HasDebugCallStack + => FixedRuntimeRepContext + -- ^ Context to be reported to the user + -- if the type does not have a syntactically + -- fixed 'RuntimeRep'. + -> TcType + -- ^ The type to check (we only look at its kind). + -> TcM () +hasFixedRuntimeRep_syntactic frr_ctxt ty + = void $ checkFRR_with ensure_conc frr_ctxt ty + where + ensure_conc :: FixedRuntimeRepOrigin -> TcKind -> TcM TcMCoercionN + ensure_conc frr_orig ki = ensureConcrete frr_orig ki $> MRefl + +-- | Internal function to check whether the given type has a fixed 'RuntimeRep'. -- --- Returns a coercion @co :: ki ~# concrete_tv@ as evidence. --- If @ty@ obviously has a fixed 'RuntimeRep', e.g @ki = IntRep@, --- then this function immediately returns 'Nothing' --- instead of emitting a new constraint. -hasFixedRuntimeRep :: FRROrigin -- ^ Context to be reported to the user - -- if the type ends up not having a fixed - -- 'RuntimeRep' (unsolved Wanted constraint). - -> TcType -- ^ The type to check (we only look at its kind). - -> TcM (Maybe (TcType, TcCoercion, TcTyVar) ) - -- ^ @Just ( ki, co, concrete_tv )@ - -- where @co :: ki ~# concrete_ty@ is evidence that - -- the type @ty :: ki@ has a fixed 'RuntimeRep', - -- or 'Nothing' if 'ki' responds 'True' to 'isConcrete', - -- (i.e. we can take @co = Refl@). -hasFixedRuntimeRep frr_orig ty +-- Use 'hasFixedRuntimeRep' to allow rewriting, or 'hasFixedRuntimeRep_syntactic' +-- to perform a syntactic check. +checkFRR_with :: HasDebugCallStack + => (FixedRuntimeRepOrigin -> TcKind -> TcM TcMCoercionN) + -- ^ The check to perform on the kind. + -> FixedRuntimeRepContext + -- ^ The context which required a fixed 'RuntimeRep', + -- e.g. an application, a lambda abstraction, ... + -> TcType + -- ^ The type @ty@ to check (the check itself only looks at its kind). + -> TcM (TcCoercionN, TcTypeFRR) + -- ^ Returns @(co, frr_ty)@ with @co :: ty ~# frr_ty@ + -- and @frr_@ty has a fixed 'RuntimeRep'. +checkFRR_with check_kind frr_ctxt ty = do { th_stage <- getStage ; if -- Shortcut: check for 'Type' and 'UnliftedType' type synonyms. | TyConApp tc [] <- ki , tc == liftedTypeKindTyCon || tc == unliftedTypeKindTyCon - -> return Nothing + -> return refl -- See [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep]. | Brack _ (TcPending {}) <- th_stage - -> return Nothing + -> return refl + -- Otherwise: ensure that the kind 'ki' of 'ty' is concrete. | otherwise - -- Ensure that the kind 'ki' of 'ty' is concrete. - -> emitNewConcreteWantedEq_maybe orig ki - -- NB: the kind of 'ki' is 'Data.Kind.Type', which is concrete. - -- This means that the invariant required to call - -- 'newConcreteTyVar' is satisfied. - } + -> do { kco <- check_kind frr_orig ki + ; return ( mkTcGReflRightMCo Nominal ty kco + , mkCastTyMCo ty kco ) } } + where + refl :: (TcCoercionN, TcType) + refl = (mkTcNomReflCo ty, ty) ki :: TcKind ki = typeKind ty - orig :: CtOrigin - orig = FixedRuntimeRepOrigin ty frr_orig + frr_orig :: FixedRuntimeRepOrigin + frr_orig = FixedRuntimeRepOrigin { frr_type = ty, frr_context = frr_ctxt } --- | Create a new metavariable, of the given kind, which can only be unified --- with a concrete type. +-- | Ensure that the given type @ty@ can unify with a concrete type, +-- in the sense of Note [Concrete types]. -- --- Invariant: the kind must be concrete, as per Note [ConcreteTv]. --- This is checked with an assertion. -newConcreteTyVar :: HasDebugCallStack => TcKind -> TcM TcTyVar -newConcreteTyVar kind = - assertPpr (isConcrete kind) - (text "newConcreteTyVar: non-concrete kind" <+> ppr kind) - $ newAnonMetaTyVar ConcreteTv kind - --- | Create a new concrete metavariable @concrete_tv@ and emit a new non-canonical Wanted --- equality constraint @ty ~# concrete_tv@ with the given 'CtOrigin'. +-- Returns a coercion @co :: ty ~# conc_ty@, where @conc_ty@ is +-- concrete. -- --- Short-cut: if the type responds 'True' to 'isConcrete', then --- we already know it is concrete, so don't emit any new constraints, --- and return 'Nothing'. +-- If the type is already syntactically concrete, this +-- immediately returns a reflexive coercion. Otherwise, +-- it creates a new concrete metavariable @concrete_tv@ +-- and emits an equality constraint @ty ~# concrete_tv@, +-- to be handled by the constraint solver. -- -- Invariant: the kind of the supplied type must be concrete. -- --- We also assume the provided type is already at the kind-level. ---(This only matters for error messages.) -emitNewConcreteWantedEq_maybe :: CtOrigin -> TcType -> TcM (Maybe (TcType, TcCoercion, TcTyVar)) -emitNewConcreteWantedEq_maybe orig ty - -- The input type is already concrete: no need to do anything. - -- Return 'Nothing', indicating that reflexivity is valid evidence. - | isConcrete ty - = return Nothing - -- Otherwise: create a new concrete metavariable and emit a new Wanted equality constraint. - | otherwise - = do { concrete_tv <- newConcreteTyVar ki - ; co <- emitWantedEq orig KindLevel Nominal ty (mkTyVarTy concrete_tv) - -- ^^^^^^^^^ we assume 'ty' is at the kind level. - -- (For representation polymorphism checks, we are always checking a kind.) - ; return $ Just (ty, co, concrete_tv) } +-- We assume the provided type is already at the kind-level +-- (this only matters for error messages). +unifyConcrete :: HasDebugCallStack + => FixedRuntimeRepOrigin -> TcType -> TcM TcMCoercionN +unifyConcrete frr_orig ty + = do { (ty, errs) <- makeTypeConcrete (ConcreteFRR frr_orig) ty + ; case errs of + -- We were able to make the type fully concrete. + { [] -> return MRefl + -- The type could not be made concrete; perhaps it contains + -- a skolem type variable, a type family application, ... + -- + -- Create a new ConcreteTv metavariable @concrete_tv@ + -- and unify @ty ~# concrete_tv@. + ; _ -> + do { conc_tv <- newConcreteTyVar (ConcreteFRR frr_orig) ki + -- NB: newConcreteTyVar asserts that 'ki' is concrete. + ; coToMCo <$> emitWantedEq orig KindLevel Nominal ty (mkTyVarTy conc_tv) } } } where ki :: TcKind ki = typeKind ty + orig :: CtOrigin + orig = FRROrigin frr_orig + +-- | Ensure that the given type is concrete. +-- +-- This is an eager syntactic check, and never defers +-- any work to the constraint solver. +-- +-- Invariant: the kind of the supplied type must be concrete. +-- Invariant: the output type is equal to the input type, +-- up to zonking. +-- +-- We assume the provided type is already at the kind-level +-- (this only matters for error messages). +ensureConcrete :: HasDebugCallStack + => FixedRuntimeRepOrigin + -> TcType + -> TcM TcType +ensureConcrete frr_orig ty + = do { (ty', errs) <- makeTypeConcrete conc_orig ty + ; case errs of + { err:errs -> + do { traceTc "ensureConcrete } failure" $ + vcat [ text "ty:" <+> ppr ty + , text "ty':" <+> ppr ty' ] + ; loc <- getCtLocM (FRROrigin frr_orig) (Just KindLevel) + ; emitNotConcreteError $ + NCE_FRR + { nce_loc = loc + , nce_frr_origin = frr_orig + , nce_reasons = err :| errs } + } + ; [] -> + traceTc "ensureConcrete } success" $ + vcat [ text "ty: " <+> ppr ty + , text "ty':" <+> ppr ty' ] } + ; return ty' } + where + conc_orig :: ConcreteTvOrigin + conc_orig = ConcreteFRR frr_orig + +{-*********************************************************************** +%* * + Making a type concrete +%* * +%************************************************************************ + +Note [Unifying concrete metavariables] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Unifying concrete metavariables (as defined in Note [ConcreteTv]) is not +an all-or-nothing affair as it is for other sorts of metavariables. + +Consider the following unification problem in which all metavariables +are unfilled (and ignoring any TcLevel considerations): + + alpha[conc] ~# TYPE (TupleRep '[ beta[conc], IntRep, gamma[tau] ]) + +We can't immediately unify `alpha` with the RHS, because the RHS is not +a concrete type (in the sense of Note [Concrete types]). Instead, we +proceed as follows: + + - create a fresh concrete metavariable variable `gamma'[conc]`, + - write gamma[tau] := gamma'[conc], + - write alpha[conc] := TYPE (TupleRep '[ beta[conc], IntRep, gamma'[conc] ]). + +Thus, in general, to unify `alpha[conc] ~# rhs`, we first try to turn +`rhs` into a concrete type (see the 'makeTypeConcrete' function). +If this succeeds, resulting in a concrete type `rhs'`, we simply fill +`alpha[conc] := rhs'`. If it fails, then syntactic unification fails. + +Example 1: + + alpha[conc] ~# TYPE (TupleRep '[ beta[conc], IntRep, gamma[tau] ]) + + We proceed by filling metavariables: + + gamma[tau] := gamma[conc] + alpha[conc] := TYPE (TupleRep '[ beta[conc], IntRep, gamma[conc] ]) + + This successfully unifies alpha. + +Example 2: + + For a type family `F :: Type -> Type`: + + delta[conc] ~# TYPE (SumRep '[ zeta[tau], a[sk], F omega[tau] ]) + + We write zeta[tau] := zeta[conc], and then fail, providing the following + two reasons: + + - `a[sk]` is not a concrete type variable, so the overall type + cannot be concrete + - `F` is not a concrete type constructor, in the sense of + Note [Concrete types]. So we keep it as is; in particular, + we /should not/ try to make its argument `omega[tau]` into + a ConcreteTv. + + Note that making zeta concrete allows us to propagate information. + For example, after more typechecking, we might try to unify + `zeta ~# rr[sk]`. If we made zeta a ConcreteTv, we will report + this unsolved equality using the 'ConcreteTvOrigin' stored in zeta[conc]. + This allows us to report ALL the problems in a representation-polymorphism + check (instead of only a non-empty subset). +-} + +-- | Try to turn the provided type into a concrete type, by ensuring +-- unfilled metavariables are appropriately marked as concrete. +-- +-- Returns a zonked type which is "as concrete as possible", and +-- a list of problems encountered when trying to make it concrete. +-- +-- INVARIANT: the returned type is equal to the input type, up to zonking. +-- INVARIANT: if this function returns an empty list of 'NotConcreteReasons', +-- then the returned type is concrete, in the sense of Note [Concrete types]. +makeTypeConcrete :: ConcreteTvOrigin -> TcType -> TcM (TcType, [NotConcreteReason]) +-- TODO: it could be worthwhile to return enough information to continue solving. +-- Consider unifying `alpha[conc] ~# TupleRep '[ beta[tau], F Int ]` for +-- a type family 'F'. +-- This function will concretise `beta[tau] := beta[conc]` and return +-- that `TupleRep '[ beta[conc], F Int ]` is not concrete because of the +-- type family application `F Int`. But we could decompose by setting +-- alpha := TupleRep '[ beta, gamma[conc] ] and emitting `[W] gamma[conc] ~ F Int`. +-- +-- This would be useful in startSolvingByUnification. +makeTypeConcrete conc_orig ty = + do { res@(ty', _) <- runWriterT $ go ty + ; traceTc "makeTypeConcrete" $ + vcat [ text "ty:" <+> ppr ty + , text "ty':" <+> ppr ty' ] + ; return res } + where + go :: TcType -> WriterT [NotConcreteReason] TcM TcType + go ty + | Just ty <- tcView ty + = go ty + | isConcrete ty + = pure ty + go ty@(TyVarTy tv) -- not a ConcreteTv (already handled above) + = do { mb_filled <- lift $ isFilledMetaTyVar_maybe tv + ; case mb_filled of + { Just ty -> go ty + ; Nothing + | isMetaTyVar tv + , TauTv <- metaTyVarInfo tv + -> -- Change the MetaInfo to ConcreteTv, but retain the TcLevel + do { kind <- go (tyVarKind tv) + ; lift $ + do { conc_tv <- setTcLevel (tcTyVarLevel tv) $ + newConcreteTyVar conc_orig kind + ; let conc_ty = mkTyVarTy conc_tv + ; writeMetaTyVar tv conc_ty + ; return conc_ty } } + | otherwise + -- Don't attempt to make other type variables concrete + -- (e.g. SkolemTv, TyVarTv, CycleBreakerTv, RuntimeUnkTv). + -> bale_out ty (NonConcretisableTyVar tv) } } + go ty@(TyConApp tc tys) + | isConcreteTyCon tc + = mkTyConApp tc <$> mapM go tys + | otherwise + = bale_out ty (NonConcreteTyCon tc tys) + go (FunTy af w ty1 ty2) + = do { w <- go w + ; ty1 <- go ty1 + ; ty2 <- go ty2 + ; return $ mkFunTy af w ty1 ty2 } + go (AppTy ty1 ty2) + = do { ty1 <- go ty1 + ; ty2 <- go ty2 + ; return $ mkAppTy ty1 ty2 } + go ty@(LitTy {}) + = return ty + go ty@(CastTy cast_ty kco) + = bale_out ty (ContainsCast cast_ty kco) + go ty@(ForAllTy tcv body) + = bale_out ty (ContainsForall tcv body) + go ty@(CoercionTy co) + = bale_out ty (ContainsCoercionTy co) + + bale_out :: TcType -> NotConcreteReason -> WriterT [NotConcreteReason] TcM TcType + bale_out ty reason = do { tell [reason]; return ty } diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs index 78c7ad4c12..4284b35d5e 100644 --- a/compiler/GHC/Tc/Utils/Instantiate.hs +++ b/compiler/GHC/Tc/Utils/Instantiate.hs @@ -70,7 +70,7 @@ import GHC.Tc.Types.Origin import GHC.Tc.Utils.Env import GHC.Tc.Types.Evidence import GHC.Tc.Instance.FunDeps -import GHC.Tc.Utils.Concrete +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_syntactic ) import GHC.Tc.Utils.TcMType import GHC.Tc.Utils.TcType import GHC.Tc.Errors.Types @@ -825,7 +825,7 @@ hasFixedRuntimeRepRes std_nm user_expr ty = mapM_ do_check mb_arity do_check :: Arity -> TcM () do_check arity = let res_ty = nTimes arity (snd . splitPiTy) ty - in hasFixedRuntimeRep_MustBeRefl (FRRArrow $ ArrowFun user_expr) res_ty + in hasFixedRuntimeRep_syntactic (FRRArrow $ ArrowFun user_expr) res_ty mb_arity :: Maybe Arity mb_arity -- arity of the arrow operation, counting type-level arguments | std_nm == arrAName -- result used as an argument in, e.g., do_premap diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs index dada2c8041..571e02c7cf 100644 --- a/compiler/GHC/Tc/Utils/Monad.hs +++ b/compiler/GHC/Tc/Utils/Monad.hs @@ -106,7 +106,7 @@ module GHC.Tc.Utils.Monad( getConstraintVar, setConstraintVar, emitConstraints, emitStaticConstraints, emitSimple, emitSimples, emitImplication, emitImplications, emitInsoluble, - emitHole, emitHoles, + emitDelayedErrors, emitHole, emitHoles, emitNotConcreteError, discardConstraints, captureConstraints, tryCaptureConstraints, pushLevelAndCaptureConstraints, pushTcLevelM_, pushTcLevelM, @@ -1816,6 +1816,12 @@ emitInsoluble ct ; lie_var <- getConstraintVar ; updTcRef lie_var (`addInsols` unitBag ct) } +emitDelayedErrors :: Bag DelayedError -> TcM () +emitDelayedErrors errs + = do { traceTc "emitDelayedErrors" (ppr errs) + ; lie_var <- getConstraintVar + ; updTcRef lie_var (`addDelayedErrors` errs)} + emitHole :: Hole -> TcM () emitHole hole = do { traceTc "emitHole" (ppr hole) @@ -1828,6 +1834,12 @@ emitHoles holes ; lie_var <- getConstraintVar ; updTcRef lie_var (`addHoles` holes) } +emitNotConcreteError :: NotConcreteError -> TcM () +emitNotConcreteError err + = do { traceTc "emitNotConcreteError" (ppr err) + ; lie_var <- getConstraintVar + ; updTcRef lie_var (`addNotConcreteError` err) } + -- | Throw out any constraints emitted by the thing_inside discardConstraints :: TcM a -> TcM a discardConstraints thing_inside = fst <$> captureConstraints thing_inside diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index 8c59e30d95..1206b95da7 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -25,7 +25,7 @@ module GHC.Tc.Utils.TcMType ( newOpenFlexiTyVar, newOpenFlexiTyVarTy, newOpenTypeKind, newOpenBoxedTypeKind, newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel, - newAnonMetaTyVar, cloneMetaTyVar, + newAnonMetaTyVar, newConcreteTyVar, cloneMetaTyVar, newCycleBreakerTyVar, newMultiplicityVar, @@ -60,16 +60,18 @@ module GHC.Tc.Utils.TcMType ( -------------------------------- -- Expected types ExpType(..), ExpSigmaType, ExpRhoType, - mkCheckExpType, newInferExpType, tcInfer, + mkCheckExpType, newInferExpType, newInferExpTypeFRR, + tcInfer, tcInferFRR, readExpType, readExpType_maybe, readScaledExpType, expTypeToType, scaledExpTypeToType, checkingExpType_maybe, checkingExpType, - inferResultToType, fillInferResult, promoteTcType, + inferResultToType, ensureMonoType, promoteTcType, -------------------------------- -- Zonking and tidying zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin, zonkTidyOrigins, - tidyEvVar, tidyCt, tidyHole, + zonkTidyFRRInfos, + tidyEvVar, tidyCt, tidyHole, tidyDelayedError, zonkTcTyVar, zonkTcTyVars, zonkTcTyVarToTcTyVar, zonkTcTyVarsToTcTyVars, zonkInvisTVBinder, @@ -113,7 +115,6 @@ import GHC.Tc.Types.Origin import GHC.Tc.Utils.Monad -- TcType, amongst others import GHC.Tc.Types.Constraint import GHC.Tc.Types.Evidence -import {-# SOURCE #-} GHC.Tc.Utils.Unify( unifyType {- , unifyKind -} ) import GHC.Tc.Utils.TcType import GHC.Tc.Errors.Types import GHC.Tc.Errors.Ppr @@ -198,12 +199,8 @@ newEvVar ty = do { name <- newSysName (predTypeOccName ty) newWantedWithLoc :: CtLoc -> PredType -> TcM CtEvidence newWantedWithLoc loc pty = do dst <- case classifyPredType pty of - EqPred {} - -> HoleDest <$> newCoercionHole pty - SpecialPred s - -> case s of - IsReflPrimPred {} -> return NoDest - _ -> EvVarDest <$> newEvVar pty + EqPred {} -> HoleDest <$> newCoercionHole pty + _ -> EvVarDest <$> newEvVar pty return $ CtWanted { ctev_dest = dst , ctev_pred = pty , ctev_loc = loc @@ -332,9 +329,6 @@ predTypeOccName ty = case classifyPredType ty of EqPred {} -> mkVarOccFS (fsLit "co") IrredPred {} -> mkVarOccFS (fsLit "irred") ForAllPred {} -> mkVarOccFS (fsLit "df") - SpecialPred s -> - case s of - IsReflPrimPred {} -> mkVarOccFS (fsLit "rfl") -- | Create a new 'Implication' with as many sensible defaults for its fields -- as possible. Note that the 'ic_tclvl', 'ic_binds', and 'ic_info' fields do @@ -482,18 +476,42 @@ the ExpType with a tau-tv at the low TcLevel, hopefully to be worked out later by some means -- see fillInferResult, and Note [fillInferResult] This behaviour triggered in test gadt/gadt-escape1. + +Note [FixedRuntimeRep context in ExpType] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Sometimes, we want to be sure that we fill an ExpType with a type +that has a syntactically fixed RuntimeRep (in the sense of +Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete). + +Example: + + pattern S a = (a :: (T :: TYPE R)) + +We have to infer a type for `a` which has a syntactically fixed RuntimeRep. +When it comes time to filling in the inferred type, we do the appropriate +representation-polymorphism check, much like we do a level check +as explained in Note [TcLevel of ExpType]. + +See test case T21325. -} -- actual data definition is in GHC.Tc.Utils.TcType newInferExpType :: TcM ExpType -newInferExpType +newInferExpType = new_inferExpType Nothing + +newInferExpTypeFRR :: FixedRuntimeRepContext -> TcM ExpTypeFRR +newInferExpTypeFRR frr_orig = new_inferExpType (Just frr_orig) + +new_inferExpType :: Maybe FixedRuntimeRepContext -> TcM ExpType +new_inferExpType mb_frr_orig = do { u <- newUnique ; tclvl <- getTcLevel ; traceTc "newInferExpType" (ppr u <+> ppr tclvl) ; ref <- newMutVar Nothing ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl - , ir_ref = ref })) } + , ir_ref = ref + , ir_frr = mb_frr_orig })) } -- | Extract a type out of an ExpType, if one exists. But one should always -- exist. Unless you're quite sure you know what you're doing. @@ -563,119 +581,30 @@ order-independence we check for mono-type-ness even if it *is* filled in already. See also Note [TcLevel of ExpType] above, and -Note [fillInferResult]. +Note [fillInferResult] in GHC.Tc.Utils.Unify. -} -- | Infer a type using a fresh ExpType -- See also Note [ExpType] in "GHC.Tc.Utils.TcMType" +-- +-- Use 'tcInferFRR' if you require the type to have a fixed +-- runtime representation. tcInfer :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) -tcInfer tc_check - = do { res_ty <- newInferExpType +tcInfer = tc_infer Nothing + +-- | Like 'tcInfer', except it ensures that the resulting type +-- has a syntactically fixed RuntimeRep as per Note [Fixed RuntimeRep] in +-- GHC.Tc.Utils.Concrete. +tcInferFRR :: FixedRuntimeRepContext -> (ExpSigmaTypeFRR -> TcM a) -> TcM (a, TcSigmaTypeFRR) +tcInferFRR frr_orig = tc_infer (Just frr_orig) + +tc_infer :: Maybe FixedRuntimeRepContext -> (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) +tc_infer mb_frr tc_check + = do { res_ty <- new_inferExpType mb_frr ; result <- tc_check res_ty ; res_ty <- readExpType res_ty ; return (result, res_ty) } -fillInferResult :: TcType -> InferResult -> TcM TcCoercionN --- If co = fillInferResult t1 t2 --- => co :: t1 ~ t2 --- See Note [fillInferResult] -fillInferResult act_res_ty (IR { ir_uniq = u, ir_lvl = res_lvl - , ir_ref = ref }) - = do { mb_exp_res_ty <- readTcRef ref - ; case mb_exp_res_ty of - Just exp_res_ty - -> do { traceTc "Joining inferred ExpType" $ - ppr u <> colon <+> ppr act_res_ty <+> char '~' <+> ppr exp_res_ty - ; cur_lvl <- getTcLevel - ; unless (cur_lvl `sameDepthAs` res_lvl) $ - ensureMonoType act_res_ty - ; unifyType Nothing act_res_ty exp_res_ty } - Nothing - -> do { traceTc "Filling inferred ExpType" $ - ppr u <+> text ":=" <+> ppr act_res_ty - ; (prom_co, act_res_ty) <- promoteTcType res_lvl act_res_ty - ; writeTcRef ref (Just act_res_ty) - ; return prom_co } - } - - -{- Note [fillInferResult] -~~~~~~~~~~~~~~~~~~~~~~~~~ -When inferring, we use fillInferResult to "fill in" the hole in InferResult - data InferResult = IR { ir_uniq :: Unique - , ir_lvl :: TcLevel - , ir_ref :: IORef (Maybe TcType) } - -There are two things to worry about: - -1. What if it is under a GADT or existential pattern match? - - GADTs: a unification variable (and Infer's hole is similar) is untouchable - - Existentials: be careful about skolem-escape - -2. What if it is filled in more than once? E.g. multiple branches of a case - case e of - T1 -> e1 - T2 -> e2 - -Our typing rules are: - -* The RHS of a existential or GADT alternative must always be a - monotype, regardless of the number of alternatives. - -* Multiple non-existential/GADT branches can have (the same) - higher rank type (#18412). E.g. this is OK: - case e of - True -> hr - False -> hr - where hr:: (forall a. a->a) -> Int - c.f. Section 7.1 of "Practical type inference for arbitrary-rank types" - We use choice (2) in that Section. - (GHC 8.10 and earlier used choice (1).) - - But note that - case e of - True -> hr - False -> \x -> hr x - will fail, because we still /infer/ both branches, so the \x will get - a (monotype) unification variable, which will fail to unify with - (forall a. a->a) - -For (1) we can detect the GADT/existential situation by seeing that -the current TcLevel is greater than that stored in ir_lvl of the Infer -ExpType. We bump the level whenever we go past a GADT/existential match. - -Then, before filling the hole use promoteTcType to promote the type -to the outer ir_lvl. promoteTcType does this - - create a fresh unification variable alpha at level ir_lvl - - emits an equality alpha[ir_lvl] ~ ty - - fills the hole with alpha -That forces the type to be a monotype (since unification variables can -only unify with monotypes); and catches skolem-escapes because the -alpha is untouchable until the equality floats out. - -For (2), we simply look to see if the hole is filled already. - - if not, we promote (as above) and fill the hole - - if it is filled, we simply unify with the type that is - already there - -There is one wrinkle. Suppose we have - case e of - T1 -> e1 :: (forall a. a->a) -> Int - G2 -> e2 -where T1 is not GADT or existential, but G2 is a GADT. Then supppose the -T1 alternative fills the hole with (forall a. a->a) -> Int, which is fine. -But now the G2 alternative must not *just* unify with that else we'd risk -allowing through (e2 :: (forall a. a->a) -> Int). If we'd checked G2 first -we'd have filled the hole with a unification variable, which enforces a -monotype. - -So if we check G2 second, we still want to emit a constraint that restricts -the RHS to be a monotype. This is done by ensureMonoType, and it works -by simply generating a constraint (alpha ~ ty), where alpha is a fresh -unification variable. We discard the evidence. - --} - {- ********************************************************************* * * Promoting types @@ -864,7 +793,7 @@ metaInfoToTyVarName meta_info = TyVarTv -> fsLit "a" RuntimeUnkTv -> fsLit "r" CycleBreakerTv -> fsLit "b" - ConcreteTv -> fsLit "c" + ConcreteTv {} -> fsLit "c" newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar newAnonMetaTyVar mi = newNamedAnonMetaTyVar (metaInfoToTyVarName mi) mi @@ -909,6 +838,17 @@ cloneTyVarTyVar name kind ; traceTc "cloneTyVarTyVar" (ppr tyvar) ; return tyvar } +-- | Create a new metavariable, of the given kind, which can only be unified +-- with a concrete type. +-- +-- Invariant: the kind must be concrete, as per Note [ConcreteTv]. +-- This is checked with an assertion. +newConcreteTyVar :: HasDebugCallStack => ConcreteTvOrigin -> TcKind -> TcM TcTyVar +newConcreteTyVar reason kind = + assertPpr (isConcrete kind) + (text "newConcreteTyVar: non-concrete kind" <+> ppr kind) + $ newAnonMetaTyVar (ConcreteTv reason) kind + newPatSigTyVar :: Name -> Kind -> TcM TcTyVar newPatSigTyVar name kind = do { details <- newMetaDetails TauTv @@ -1863,9 +1803,7 @@ defaultTyVar :: DefaultingStrategy -> TcM Bool -- True <=> defaulted away altogether defaultTyVar def_strat tv | not (isMetaTyVar tv) - = return False - - | isTyVarTyVar tv + || isTyVarTyVar tv -- Do not default TyVarTvs. Doing so would violate the invariants -- on TyVarTvs; see Note [TyVarTv] in GHC.Tc.Utils.TcMType. -- #13343 is an example; #14555 is another @@ -1874,8 +1812,6 @@ defaultTyVar def_strat tv | isRuntimeRepVar tv , default_ns_vars - -- Do not quantify over a RuntimeRep var - -- unless it is a TyVarTv, handled earlier = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv) ; writeMetaTyVar tv liftedRepTy ; return True } @@ -2414,22 +2350,38 @@ zonkWC :: WantedConstraints -> TcM WantedConstraints zonkWC wc = zonkWCRec wc zonkWCRec :: WantedConstraints -> TcM WantedConstraints -zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_holes = holes }) +zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_errors = errs }) = do { simple' <- zonkSimples simple ; implic' <- mapBagM zonkImplication implic - ; holes' <- mapBagM zonkHole holes - ; return (WC { wc_simple = simple', wc_impl = implic', wc_holes = holes' }) } + ; errs' <- mapBagM zonkDelayedError errs + ; return (WC { wc_simple = simple', wc_impl = implic', wc_errors = errs' }) } zonkSimples :: Cts -> TcM Cts zonkSimples cts = do { cts' <- mapBagM zonkCt cts ; traceTc "zonkSimples done:" (ppr cts') ; return cts' } +zonkDelayedError :: DelayedError -> TcM DelayedError +zonkDelayedError (DE_Hole hole) + = DE_Hole <$> zonkHole hole +zonkDelayedError (DE_NotConcrete err) + = DE_NotConcrete <$> zonkNotConcreteError err + zonkHole :: Hole -> TcM Hole zonkHole hole@(Hole { hole_ty = ty }) = do { ty' <- zonkTcType ty ; return (hole { hole_ty = ty' }) } +zonkNotConcreteError :: NotConcreteError -> TcM NotConcreteError +zonkNotConcreteError err@(NCE_FRR { nce_frr_origin = frr_orig }) + = do { frr_orig <- zonkFRROrigin frr_orig + ; return $ err { nce_frr_origin = frr_orig } } + +zonkFRROrigin :: FixedRuntimeRepOrigin -> TcM FixedRuntimeRepOrigin +zonkFRROrigin (FixedRuntimeRepOrigin ty orig) + = do { ty' <- zonkTcType ty + ; return $ FixedRuntimeRepOrigin ty' orig } + {- Note [zonkCt behaviour] ~~~~~~~~~~~~~~~~~~~~~~~~~~ zonkCt tries to maintain the canonical form of a Ct. For example, @@ -2667,9 +2619,6 @@ zonkTidyOrigin env (CycleBreakerOrigin orig) zonkTidyOrigin env (InstProvidedOrigin mod cls_inst) = do { (env1, is_tys') <- mapAccumLM zonkTidyTcType env (is_tys cls_inst) ; return (env1, InstProvidedOrigin mod (cls_inst {is_tys = is_tys'})) } -zonkTidyOrigin env (FixedRuntimeRepOrigin ty frr_orig) - = do { (env1, ty') <- zonkTidyTcType env ty - ; return (env1, FixedRuntimeRepOrigin ty' frr_orig)} zonkTidyOrigin env (WantedSuperclassOrigin pty orig) = do { (env1, pty') <- zonkTidyTcType env pty ; (env2, orig') <- zonkTidyOrigin env1 orig @@ -2679,6 +2628,26 @@ zonkTidyOrigin env orig = return (env, orig) zonkTidyOrigins :: TidyEnv -> [CtOrigin] -> TcM (TidyEnv, [CtOrigin]) zonkTidyOrigins = mapAccumLM zonkTidyOrigin +zonkTidyFRRInfos :: TidyEnv + -> [FixedRuntimeRepErrorInfo] + -> TcM (TidyEnv, [FixedRuntimeRepErrorInfo]) +zonkTidyFRRInfos = go [] + where + go zs env [] = return (env, reverse zs) + go zs env (FRR_Info { frr_info_origin = FixedRuntimeRepOrigin ty orig + , frr_info_not_concrete = mb_not_conc } : tys) + = do { (env, ty) <- zonkTidyTcType env ty + ; (env, mb_not_conc) <- go_mb_not_conc env mb_not_conc + ; let info = FRR_Info { frr_info_origin = FixedRuntimeRepOrigin ty orig + , frr_info_not_concrete = mb_not_conc } + ; go (info:zs) env tys } + + go_mb_not_conc env Nothing = return (env, Nothing) + go_mb_not_conc env (Just (tv, ty)) + = do { (env, tv) <- return $ tidyOpenTyCoVar env tv + ; (env, ty) <- zonkTidyTcType env ty + ; return (env, Just (tv, ty)) } + ---------------- tidyCt :: TidyEnv -> Ct -> Ct -- Used only in error reporting @@ -2694,6 +2663,20 @@ tidyCtEvidence env ctev = ctev { ctev_pred = tidyType env ty } tidyHole :: TidyEnv -> Hole -> Hole tidyHole env h@(Hole { hole_ty = ty }) = h { hole_ty = tidyType env ty } +tidyDelayedError :: TidyEnv -> DelayedError -> DelayedError +tidyDelayedError env (DE_Hole hole) + = DE_Hole $ tidyHole env hole +tidyDelayedError env (DE_NotConcrete err) + = DE_NotConcrete $ tidyConcreteError env err + +tidyConcreteError :: TidyEnv -> NotConcreteError -> NotConcreteError +tidyConcreteError env err@(NCE_FRR { nce_frr_origin = frr_orig }) + = err { nce_frr_origin = tidyFRROrigin env frr_orig } + +tidyFRROrigin :: TidyEnv -> FixedRuntimeRepOrigin -> FixedRuntimeRepOrigin +tidyFRROrigin env (FixedRuntimeRepOrigin ty orig) + = FixedRuntimeRepOrigin (tidyType env ty) orig + ---------------- tidyEvVar :: TidyEnv -> EvVar -> EvVar tidyEvVar env var = updateIdTypeAndMult (tidyType env) var diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index 57f2dcd358..9caf6c9f5b 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -1,6 +1,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} @@ -22,14 +23,14 @@ module GHC.Tc.Utils.TcType ( -------------------------------- -- Types - TcType, TcSigmaType, TcSigmaTypeFRR, + TcType, TcSigmaType, TcTypeFRR, TcSigmaTypeFRR, TcRhoType, TcTauType, TcPredType, TcThetaType, TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet, TcKind, TcCoVar, TcTyCoVar, TcTyVarBinder, TcInvisTVBinder, TcReqTVBinder, TcTyCon, MonoTcTyCon, PolyTcTyCon, TcTyConBinder, KnotTied, ExpType(..), InferResult(..), - ExpSigmaType, ExpSigmaTypeFRR, + ExpTypeFRR, ExpSigmaType, ExpSigmaTypeFRR, ExpRhoType, mkCheckExpType, @@ -45,7 +46,8 @@ module GHC.Tc.Utils.TcType ( MetaDetails(Flexi, Indirect), MetaInfo(..), skolemSkolInfo, isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy, tcIsTcTyVar, isTyVarTyVar, isOverlappableTyVar, isTyConableTyVar, - isConcreteTyVar, + ConcreteTvOrigin(..), isConcreteTyVar_maybe, isConcreteTyVar, + isConcreteTyVarTy, isConcreteTyVarTy_maybe, isAmbiguousTyVar, isCycleBreakerTyVar, metaTyVarRef, metaTyVarInfo, isFlexi, isIndirect, isRuntimeUnkSkol, metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe, @@ -216,6 +218,10 @@ import GHC.Core.Predicate import GHC.Types.RepType import GHC.Core.TyCon +import {-# SOURCE #-} GHC.Tc.Types.Origin + ( SkolemInfo, unkSkol + , FixedRuntimeRepOrigin, FixedRuntimeRepContext ) + -- others: import GHC.Driver.Session import GHC.Core.FVs @@ -240,7 +246,6 @@ import qualified GHC.LanguageExtensions as LangExt import Data.IORef import Data.List.NonEmpty( NonEmpty(..) ) import Data.List ( partition ) -import {-# SOURCE #-} GHC.Tc.Types.Origin ( unkSkol, SkolemInfo ) {- @@ -346,6 +351,11 @@ type TcCoVar = CoVar -- Used only during type inference type TcType = Type -- A TcType can have mutable type variables type TcTyCoVar = Var -- Either a TcTyVar or a CoVar +-- | A type which has a syntactically fixed RuntimeRep as per +-- Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. +type TcTypeFRR = TcType + -- TODO: consider making this a newtype. + type TcTyVarBinder = TyVarBinder type TcInvisTVBinder = InvisTVBinder type TcReqTVBinder = ReqTVBinder @@ -361,8 +371,9 @@ type TcPredType = PredType type TcThetaType = ThetaType type TcSigmaType = TcType --- | A 'TcSigmaTypeFRR' is a 'TcSigmaType' which has a fixed 'RuntimeRep' --- in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. +-- | A 'TcSigmaTypeFRR' is a 'TcSigmaType' which has a syntactically +-- fixed 'RuntimeRep' in the sense of Note [Fixed RuntimeRep] +-- in GHC.Tc.Utils.Concrete. -- -- In particular, this means that: -- @@ -373,6 +384,8 @@ type TcSigmaType = TcType -- we want to provide argument types which have a known runtime representation. -- See Note [Return arguments with a fixed RuntimeRep. type TcSigmaTypeFRR = TcSigmaType + -- TODO: consider making this a newtype. + type TcRhoType = TcType -- Note [TcRhoType] type TcTauType = TcType type TcKind = Kind @@ -438,17 +451,38 @@ data ExpType = Check TcType | Infer !InferResult data InferResult - = IR { ir_uniq :: Unique -- For debugging only + = IR { ir_uniq :: Unique + -- ^ This 'Unique' is for debugging only - , ir_lvl :: TcLevel -- See Note [TcLevel of ExpType] in GHC.Tc.Utils.TcMType + , ir_lvl :: TcLevel + -- ^ See Note [TcLevel of ExpType] in GHC.Tc.Utils.TcMType + + , ir_frr :: Maybe FixedRuntimeRepContext + -- ^ See Note [FixedRuntimeRep context in ExpType] in GHC.Tc.Utils.TcMType , ir_ref :: IORef (Maybe TcType) } - -- The type that fills in this hole should be a Type, - -- that is, its kind should be (TYPE rr) for some rr + -- ^ The type that fills in this hole should be a @Type@, + -- that is, its kind should be @TYPE rr@ for some @rr :: RuntimeRep@. + -- + -- Additionally, if the 'ir_frr' field is @Just frr_orig@ then + -- @rr@ must be concrete, in the sense of Note [Concrete types] + -- in GHC.Tc.Utils.Concrete. type ExpSigmaType = ExpType + +-- | An 'ExpType' which has a fixed RuntimeRep. +-- +-- For a 'Check' 'ExpType', the stored 'TcType' must have +-- a fixed RuntimeRep. For an 'Infer' 'ExpType', the 'ir_frr' +-- field must be of the form @Just frr_orig@. +type ExpTypeFRR = ExpType + -- | Like 'TcSigmaTypeFRR', but for an expected type. -type ExpSigmaTypeFRR = ExpType +-- +-- See 'ExpTypeFRR'. +type ExpSigmaTypeFRR = ExpTypeFRR + -- TODO: consider making this a newtype. + type ExpRhoType = ExpType instance Outputable ExpType where @@ -456,8 +490,12 @@ instance Outputable ExpType where ppr (Infer ir) = ppr ir instance Outputable InferResult where - ppr (IR { ir_uniq = u, ir_lvl = lvl }) - = text "Infer" <> braces (ppr u <> comma <> ppr lvl) + ppr (IR { ir_uniq = u, ir_lvl = lvl, ir_frr = mb_frr }) + = text "Infer" <> mb_frr_text <> braces (ppr u <> comma <> ppr lvl) + where + mb_frr_text = case mb_frr of + Just _ -> text "FRR" + Nothing -> empty -- | Make an 'ExpType' suitable for checking. mkCheckExpType :: TcType -> ExpType @@ -587,6 +625,8 @@ data MetaDetails = Flexi -- Flexi type variables unify to become Indirects | Indirect TcType +-- | What restrictions are on this metavariable around unification? +-- These are checked in GHC.Tc.Utils.Unify.startSolvingByUnification. data MetaInfo = TauTv -- ^ This MetaTv is an ordinary unification variable -- A TauTv is always filled in with a tau-type, which @@ -603,22 +643,32 @@ data MetaInfo -- See Note [Type variable cycles] in -- GHC.Tc.Solver.Canonical - | ConcreteTv + | ConcreteTv ConcreteTvOrigin -- ^ A unification variable that can only be unified -- with a concrete type, in the sense of -- Note [Concrete types] in GHC.Tc.Utils.Concrete. -- See Note [ConcreteTv] in GHC.Tc.Utils.Concrete. + -- See also Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete + -- for an overview of how this works in context. instance Outputable MetaDetails where ppr Flexi = text "Flexi" ppr (Indirect ty) = text "Indirect" <+> ppr ty instance Outputable MetaInfo where - ppr TauTv = text "tau" - ppr TyVarTv = text "tyv" - ppr RuntimeUnkTv = text "rutv" - ppr CycleBreakerTv = text "cbv" - ppr ConcreteTv = text "conc" + ppr TauTv = text "tau" + ppr TyVarTv = text "tyv" + ppr RuntimeUnkTv = text "rutv" + ppr CycleBreakerTv = text "cbv" + ppr (ConcreteTv {}) = text "conc" + +-- | What caused us to create a 'ConcreteTv' metavariable? +-- See Note [ConcreteTv] in GHC.Tc.Utils.Concrete. +data ConcreteTvOrigin + -- | A 'ConcreteTv' used to enforce the representation-polymorphism invariants. + -- + -- See 'FixedRuntimeRepOrigin' for more information. + = ConcreteFRR FixedRuntimeRepOrigin {- ********************************************************************* * * @@ -1091,7 +1141,7 @@ isMetaTyVar tv -- isAmbiguousTyVar is used only when reporting type errors -- It picks out variables that are unbound, namely meta --- type variables and the RuntimUnk variables created by +-- type variables and the RuntimeUnk variables created by -- GHC.Runtime.Heap.Inspect.zonkRTTIType. These are "ambiguous" in -- the sense that they stand for an as-yet-unknown type isAmbiguousTyVar tv @@ -1113,14 +1163,31 @@ isCycleBreakerTyVar tv -- | Is this type variable a concrete type variable, i.e. -- it is a metavariable with 'ConcreteTv' 'MetaInfo'? -- --- Works with both 'TyVar' and 'TcTyVar'. -isConcreteTyVar :: TcTyVar -> Bool -isConcreteTyVar tv +-- Returns the 'ConcreteTvOrigin' stored in the type variable +-- if so, or 'Nothing' otherwise. +isConcreteTyVar_maybe :: TcTyVar -> Maybe ConcreteTvOrigin +isConcreteTyVar_maybe tv | isTcTyVar tv - , MetaTv { mtv_info = ConcreteTv } <- tcTyVarDetails tv - = True + , MetaTv { mtv_info = ConcreteTv conc_orig } <- tcTyVarDetails tv + = Just conc_orig | otherwise - = False + = Nothing + +-- | Is this type variable a concrete type variable, i.e. +-- it is a metavariable with 'ConcreteTv' 'MetaInfo'? +isConcreteTyVar :: TcTyVar -> Bool +isConcreteTyVar = isJust . isConcreteTyVar_maybe + +-- | Is this type concrete type variable, i.e. +-- a metavariable with 'ConcreteTv' 'MetaInfo'? +isConcreteTyVarTy :: TcType -> Bool +isConcreteTyVarTy = isJust . isConcreteTyVarTy_maybe + +-- | Is this type a concrete type variable? If so, return +-- the associated 'TcTyVar' and 'ConcreteTvOrigin'. +isConcreteTyVarTy_maybe :: TcType -> Maybe (TcTyVar, ConcreteTvOrigin) +isConcreteTyVarTy_maybe (TyVarTy tv) = (tv, ) <$> isConcreteTyVar_maybe tv +isConcreteTyVarTy_maybe _ = Nothing isMetaTyVarTy :: TcType -> Bool isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv @@ -1933,9 +2000,6 @@ isImprovementPred ty ClassPred cls _ -> classHasFds cls IrredPred {} -> True -- Might have equalities after reduction? ForAllPred {} -> False - SpecialPred s -> - case s of - IsReflPrimPred {} -> False {- Note [Expanding superclasses] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2077,7 +2141,6 @@ isRigidTy ty | isForAllTy ty = True | otherwise = False - {- ************************************************************************ * * diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index c19b592765..8ffbfb959b 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -1,6 +1,6 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} -{-# LANGUAGE RecursiveDo #-} +{-# LANGUAGE RecursiveDo #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} @@ -23,7 +23,7 @@ module GHC.Tc.Utils.Unify ( -- Various unifications unifyType, unifyKind, unifyExpectedType, uType, promoteTcType, - swapOverTyVars, canSolveByUnification, + swapOverTyVars, startSolvingByUnification, -------------------------------- -- Holes @@ -44,7 +44,7 @@ import GHC.Prelude import GHC.Hs import GHC.Core.TyCo.Rep import GHC.Core.TyCo.Ppr( debugPprType ) -import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_MustBeRefl ) +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep, makeTypeConcrete, hasFixedRuntimeRep_syntactic ) import GHC.Tc.Utils.Env import GHC.Tc.Utils.Instantiate import GHC.Tc.Utils.Monad @@ -88,8 +88,10 @@ import qualified Data.Semigroup as S ( (<>) ) -- | 'matchActualFunTySigma' looks for just one function arrow, -- returning an uninstantiated sigma-type. -- --- Invariant: the returned argument type has a fixed RuntimeRep --- as per Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. +-- Invariant: the returned argument type has a syntactically fixed +-- RuntimeRep in the sense of Note [Fixed RuntimeRep] +-- in GHC.Tc.Utils.Concrete. +-- -- See Note [Return arguments with a fixed RuntimeRep]. matchActualFunTySigma :: ExpectedFunTyOrigin @@ -100,7 +102,7 @@ matchActualFunTySigma -- ^ Total number of value args in the call, and -- types of values args to which function has -- been applied already (reversed) - -- Both are used only for error messages) + -- (Both are used only for error messages) -> TcRhoType -- ^ Type to analyse: a TcRhoType -> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType) @@ -126,13 +128,13 @@ matchActualFunTySigma herald mb_thing err_info fun_ty -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd -- hide the forall inside a meta-variable go :: TcRhoType -- The type we're processing, perhaps after - -- expanding any type synonym + -- expanding type synonyms -> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType) go ty | Just ty' <- tcView ty = go ty' go (FunTy { ft_af = af, ft_mult = w, ft_arg = arg_ty, ft_res = res_ty }) = assert (af == VisArg) $ - do { hasFixedRuntimeRep_MustBeRefl (FRRExpectedFunTy herald 0) arg_ty + do { hasFixedRuntimeRep_syntactic (FRRExpectedFunTy herald 1) arg_ty ; return (idHsWrapper, Scaled w arg_ty, res_ty) } go ty@(TyVarTy tv) @@ -166,7 +168,7 @@ matchActualFunTySigma herald mb_thing err_info fun_ty ; mult <- newFlexiTyVarTy multiplicityTy ; let unif_fun_ty = mkVisFunTy mult arg_ty res_ty ; co <- unifyType mb_thing fun_ty unif_fun_ty - ; hasFixedRuntimeRep_MustBeRefl (FRRExpectedFunTy herald 0) arg_ty + ; hasFixedRuntimeRep_syntactic (FRRExpectedFunTy herald 1) arg_ty ; return (mkWpCastN co, Scaled mult arg_ty, res_ty) } ------------ @@ -201,7 +203,7 @@ Ugh! -- | Like 'matchExpectedFunTys', but used when you have an "actual" type, -- for example in function application. -- --- INVARIANT: the returned arguemnt types all have a fixed RuntimeRep +-- INVARIANT: the returned arguemnt types all have a syntactically fixed RuntimeRep -- in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. -- See Note [Return arguments with a fixed RuntimeRep]. matchActualFunTysRho :: ExpectedFunTyOrigin -- ^ See Note [Herald for matchExpectedFunTys] @@ -233,7 +235,7 @@ matchActualFunTysRho herald ct_orig mb_thing n_val_args_wanted fun_ty ; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1 ; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty -- NB: arg_ty1 comes from matchActualFunTySigma, so it has - -- a fixed RuntimeRep as neede to call mkWpFun. + -- a syntactically fixed RuntimeRep as needed to call mkWpFun. ; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) } {- @@ -313,7 +315,7 @@ of the representation-polymorphism invariants of Note [Representation polymorphism invariants] in GHC.Core. This is why all these functions have an additional invariant, -that the argument types they return all have a fixed RuntimeRep, +that the argument types they return all have a syntactically fixed RuntimeRep, in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. Example: @@ -356,7 +358,7 @@ Example: -- This function skolemises at each polytype. -- -- Invariant: this function only applies the provided function --- to a list of argument types which all have a fixed RuntimeRep +-- to a list of argument types which all have a syntactically fixed RuntimeRep -- in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. -- See Note [Return arguments with a fixed RuntimeRep]. matchExpectedFunTys :: forall a. @@ -366,7 +368,7 @@ matchExpectedFunTys :: forall a. -> ExpRhoType -- Skolemised -> ([Scaled ExpSigmaTypeFRR] -> ExpRhoType -> TcM a) -> TcM (HsWrapper, a) --- If matchExpectedFunTys n ty = (_, wrap) +-- If matchExpectedFunTys n ty = (wrap, _) -- then wrap : (t1 -> ... -> tn -> ty_r) ~> ty, -- where [t1, ..., tn], ty_r are passed to the thing_inside matchExpectedFunTys herald ctx arity orig_ty thing_inside @@ -394,14 +396,13 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside go acc_arg_tys n (FunTy { ft_mult = mult, ft_af = af, ft_arg = arg_ty, ft_res = res_ty }) = assert (af == VisArg) $ - do { let arg_pos = length acc_arg_tys -- for error messages only - ; hasFixedRuntimeRep_MustBeRefl (FRRExpectedFunTy herald arg_pos) arg_ty + do { let arg_pos = 1 + length acc_arg_tys -- for error messages only + ; (arg_co, arg_ty) <- hasFixedRuntimeRep (FRRExpectedFunTy herald arg_pos) arg_ty ; (wrap_res, result) <- go ((Scaled mult $ mkCheckExpType arg_ty) : acc_arg_tys) (n-1) res_ty - ; let fun_wrap = mkWpFun idHsWrapper wrap_res (Scaled mult arg_ty) res_ty - -- NB: we are ensuring that arg_ty has a fixed RuntimeRep, - -- so we satisfy the precondition that mkWpFun requires. - ; return ( fun_wrap, result ) } + ; let wrap_arg = mkWpCastN arg_co + fun_wrap = mkWpFun wrap_arg wrap_res (Scaled mult arg_ty) res_ty + ; return (fun_wrap, result) } go acc_arg_tys n ty@(TyVarTy tv) | isMetaTyVar tv @@ -431,21 +432,22 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside ------------ defer :: [Scaled ExpSigmaTypeFRR] -> Arity -> ExpRhoType -> TcM (HsWrapper, a) defer acc_arg_tys n fun_ty - = do { more_arg_tys <- replicateM n (mkScaled <$> newFlexiTyVarTy multiplicityTy <*> newInferExpType) + = do { let last_acc_arg_pos = length acc_arg_tys + ; more_arg_tys <- mapM new_exp_arg_ty [last_acc_arg_pos + 1 .. last_acc_arg_pos + n] ; res_ty <- newInferExpType ; result <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty ; more_arg_tys <- mapM (\(Scaled m t) -> Scaled m <$> readExpType t) more_arg_tys - ; zipWithM_ - ( \ i (Scaled _ arg_ty) -> - hasFixedRuntimeRep_MustBeRefl (FRRExpectedFunTy herald i) arg_ty ) - [0..] - more_arg_tys ; res_ty <- readExpType res_ty ; let unif_fun_ty = mkVisFunTys more_arg_tys res_ty ; wrap <- tcSubType AppOrigin ctx unif_fun_ty fun_ty -- Not a good origin at all :-( ; return (wrap, result) } + new_exp_arg_ty :: Int -> TcM (Scaled ExpSigmaTypeFRR) + new_exp_arg_ty arg_pos -- position for error messages only + = mkScaled <$> newFlexiTyVarTy multiplicityTy + <*> newInferExpTypeFRR (FRRExpectedFunTy herald arg_pos) + ------------ mk_ctxt :: [Scaled ExpSigmaTypeFRR] -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc) mk_ctxt arg_tys res_ty env @@ -572,6 +574,167 @@ matchExpectedAppTy orig_ty kind2 = liftedTypeKind -- m :: * -> k -- arg type :: * +{- ********************************************************************** +* + fillInferResult +* +********************************************************************** -} + +{- Note [inferResultToType] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +expTypeToType and inferResultType convert an InferResult to a monotype. +It must be a monotype because if the InferResult isn't already filled in, +we fill it in with a unification variable (hence monotype). So to preserve +order-independence we check for mono-type-ness even if it *is* filled in +already. + +See also Note [TcLevel of ExpType] in GHC.Tc.Utils.TcType, and +Note [fillInferResult]. +-} + +-- | Fill an 'InferResult' with the given type. +-- +-- If @co = fillInferResult t1 infer_res@, then @co :: t1 ~# t2@, +-- where @t2@ is the type stored in the 'ir_ref' field of @infer_res@. +-- +-- This function enforces the following invariants: +-- +-- - Level invariant. +-- The stored type @t2@ is at the same level as given by the +-- 'ir_lvl' field. +-- - FRR invariant. +-- Whenever the 'ir_frr' field is not @Nothing@, @t2@ is guaranteed +-- to have a syntactically fixed RuntimeRep, in the sense of +-- Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. +fillInferResult :: TcType -> InferResult -> TcM TcCoercionN +fillInferResult act_res_ty (IR { ir_uniq = u + , ir_lvl = res_lvl + , ir_frr = mb_frr + , ir_ref = ref }) + = do { mb_exp_res_ty <- readTcRef ref + ; case mb_exp_res_ty of + Just exp_res_ty + -- We progressively refine the type stored in 'ref', + -- for example when inferring types across multiple equations. + -- + -- Example: + -- + -- \ x -> case y of { True -> x ; False -> 3 :: Int } + -- + -- When inferring the return type of this function, we will create + -- an 'Infer' 'ExpType', which will first be filled by the type of 'x' + -- after typechecking the first equation, and then filled again with + -- the type 'Int', at which point we want to ensure that we unify + -- the type of 'x' with 'Int'. This is what is happening below when + -- we are "joining" several inferred 'ExpType's. + -> do { traceTc "Joining inferred ExpType" $ + ppr u <> colon <+> ppr act_res_ty <+> char '~' <+> ppr exp_res_ty + ; cur_lvl <- getTcLevel + ; unless (cur_lvl `sameDepthAs` res_lvl) $ + ensureMonoType act_res_ty + ; unifyType Nothing act_res_ty exp_res_ty } + Nothing + -> do { traceTc "Filling inferred ExpType" $ + ppr u <+> text ":=" <+> ppr act_res_ty + + -- Enforce the level invariant: ensure the TcLevel of + -- the type we are writing to 'ref' matches 'ir_lvl'. + ; (prom_co, act_res_ty) <- promoteTcType res_lvl act_res_ty + + -- Enforce the FRR invariant: ensure the type has a syntactically + -- fixed RuntimeRep (if necessary, i.e. 'mb_frr' is not 'Nothing'). + ; (frr_co, act_res_ty) <- + case mb_frr of + Nothing -> return (mkNomReflCo act_res_ty, act_res_ty) + Just frr_orig -> hasFixedRuntimeRep frr_orig act_res_ty + + -- Compose the two coercions. + ; let final_co = prom_co `mkTcTransCo` frr_co + + ; writeTcRef ref (Just act_res_ty) + + ; return final_co } + } + +{- Note [fillInferResult] +~~~~~~~~~~~~~~~~~~~~~~~~~ +When inferring, we use fillInferResult to "fill in" the hole in InferResult + data InferResult = IR { ir_uniq :: Unique + , ir_lvl :: TcLevel + , ir_ref :: IORef (Maybe TcType) } + +There are two things to worry about: + +1. What if it is under a GADT or existential pattern match? + - GADTs: a unification variable (and Infer's hole is similar) is untouchable + - Existentials: be careful about skolem-escape + +2. What if it is filled in more than once? E.g. multiple branches of a case + case e of + T1 -> e1 + T2 -> e2 + +Our typing rules are: + +* The RHS of a existential or GADT alternative must always be a + monotype, regardless of the number of alternatives. + +* Multiple non-existential/GADT branches can have (the same) + higher rank type (#18412). E.g. this is OK: + case e of + True -> hr + False -> hr + where hr:: (forall a. a->a) -> Int + c.f. Section 7.1 of "Practical type inference for arbitrary-rank types" + We use choice (2) in that Section. + (GHC 8.10 and earlier used choice (1).) + + But note that + case e of + True -> hr + False -> \x -> hr x + will fail, because we still /infer/ both branches, so the \x will get + a (monotype) unification variable, which will fail to unify with + (forall a. a->a) + +For (1) we can detect the GADT/existential situation by seeing that +the current TcLevel is greater than that stored in ir_lvl of the Infer +ExpType. We bump the level whenever we go past a GADT/existential match. + +Then, before filling the hole use promoteTcType to promote the type +to the outer ir_lvl. promoteTcType does this + - create a fresh unification variable alpha at level ir_lvl + - emits an equality alpha[ir_lvl] ~ ty + - fills the hole with alpha +That forces the type to be a monotype (since unification variables can +only unify with monotypes); and catches skolem-escapes because the +alpha is untouchable until the equality floats out. + +For (2), we simply look to see if the hole is filled already. + - if not, we promote (as above) and fill the hole + - if it is filled, we simply unify with the type that is + already there + +There is one wrinkle. Suppose we have + case e of + T1 -> e1 :: (forall a. a->a) -> Int + G2 -> e2 +where T1 is not GADT or existential, but G2 is a GADT. Then supppose the +T1 alternative fills the hole with (forall a. a->a) -> Int, which is fine. +But now the G2 alternative must not *just* unify with that else we'd risk +allowing through (e2 :: (forall a. a->a) -> Int). If we'd checked G2 first +we'd have filled the hole with a unification variable, which enforces a +monotype. + +So if we check G2 second, we still want to emit a constraint that restricts +the RHS to be a monotype. This is done by ensureMonoType, and it works +by simply generating a constraint (alpha ~ ty), where alpha is a fresh +unification variable. We discard the evidence. + +-} + + + {- ************************************************************************ * * @@ -1451,7 +1614,6 @@ If available, we defer original types (rather than those where closed type synonyms have already been expanded via tcCoreView). This is, as usual, to improve error messages. - ************************************************************************ * * uUnfilledVar and friends @@ -1533,10 +1695,13 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 go cur_lvl | isTouchableMetaTyVar cur_lvl tv1 -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles - , canSolveByUnification (metaTyVarInfo tv1) ty2 , cterHasNoProblem (checkTyVarEq tv1 ty2) -- See Note [Prevent unification with type families] - = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2) (tyVarKind tv1) + = do { can_continue_solving <- startSolvingByUnification (metaTyVarInfo tv1) ty2 + ; if not can_continue_solving + then not_ok_so_defer + else + do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2) (tyVarKind tv1) ; traceTc "uUnfilledVar2 ok" $ vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) , ppr ty2 <+> dcolon <+> ppr (tcTypeKind ty2) @@ -1549,46 +1714,61 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 then do { writeMetaTyVar tv1 ty2 ; return (mkTcNomReflCo ty2) } - else defer } -- This cannot be solved now. See GHC.Tc.Solver.Canonical - -- Note [Equalities with incompatible kinds] for how - -- this will be dealt with in the solver + else defer }} -- This cannot be solved now. See GHC.Tc.Solver.Canonical + -- Note [Equalities with incompatible kinds] for how + -- this will be dealt with in the solver | otherwise - = do { traceTc "uUnfilledVar2 not ok" (ppr tv1 $$ ppr ty2) - -- Occurs check or an untouchable: just defer - -- NB: occurs check isn't necessarily fatal: - -- eg tv1 occurred in type family parameter - ; defer } + = not_ok_so_defer ty1 = mkTyVarTy tv1 kind_origin = KindEqOrigin ty1 ty2 origin (Just t_or_k) defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2 + not_ok_so_defer = + do { traceTc "uUnfilledVar2 not ok" (ppr tv1 $$ ppr ty2) + -- Occurs check or an untouchable: just defer + -- NB: occurs check isn't necessarily fatal: + -- eg tv1 occurred in type family parameter + ; defer } + -- | Checks (TYVAR-TV), (COERCION-HOLE) and (CONCRETE) of -- Note [Unification preconditions]; returns True if these conditions -- are satisfied. But see the Note for other preconditions, too. -canSolveByUnification :: MetaInfo -> TcType -- zonked - -> Bool -canSolveByUnification _ xi - | hasCoercionHoleTy xi -- (COERCION-HOLE) check - = False -canSolveByUnification info xi +startSolvingByUnification :: MetaInfo -> TcType -- zonked + -> TcM Bool +startSolvingByUnification _ xi + | hasCoercionHoleTy xi -- (COERCION-HOLE) check + = return False +startSolvingByUnification info xi = case info of - CycleBreakerTv -> False - ConcreteTv -> isConcrete xi -- (CONCRETE) check + CycleBreakerTv -> return False + ConcreteTv conc_orig -> + do { (_, not_conc_reasons) <- makeTypeConcrete conc_orig xi + -- NB: makeTypeConcrete has the side-effect of turning + -- some TauTvs into ConcreteTvs, e.g. + -- alpha[conc] ~# TYPE (TupleRep '[ beta[tau], IntRep ]) + -- will write `beta[tau] := beta[conc]`. + -- + -- We don't need to track these unifications for the purposes + -- of constraint solving (e.g. updating tcs_unified or tcs_unif_lvl), + -- as they don't unlock any further progress. + ; case not_conc_reasons of + [] -> return True + _ -> return False } TyVarTv -> case tcGetTyVar_maybe xi of - Nothing -> False + Nothing -> return False Just tv -> case tcTyVarDetails tv of -- (TYVAR-TV) wrinkle - SkolemTv {} -> True - RuntimeUnk -> True + SkolemTv {} -> return True + RuntimeUnk -> return True MetaTv { mtv_info = info } -> case info of - TyVarTv -> True - _ -> False - _ -> True + TyVarTv -> return True + _ -> return False + _ -> return True swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool swapOverTyVars is_given tv1 tv2 @@ -1630,7 +1810,7 @@ lhsPriority tv MetaTv { mtv_info = info } -> case info of CycleBreakerTv -> 0 TyVarTv -> 1 - ConcreteTv -> 2 + ConcreteTv {} -> 2 TauTv -> 3 RuntimeUnkTv -> 4 @@ -1689,6 +1869,14 @@ There are five reasons not to unify: if we can rewrite `F Int` to a concrete type, say `FloatRep`, then we will have `rr[conc] ~ FloatRep` and we can unify `rr ~ FloatRep`. + Note that we can still make progress on unification even if + we can't fully solve an equality, e.g. + + alpha[conc] ~# TupleRep '[ beta[tau], F gamma[tau] ] + + we can fill beta[tau] := beta[conc]. This is why we call + 'makeTypeConcrete' in startSolvingByUnification. + 5. (COERCION-HOLE) Confusing coercion holes Suppose our equality is (alpha :: k) ~ (Int |> {co}) @@ -2071,10 +2259,10 @@ checkTypeEq :: CanEqLHS -> TcType -> CheckTyEqResult checkTypeEq lhs ty = go ty where - impredicative = cteProblem cteImpredicative - type_family = cteProblem cteTypeFamily - insoluble_occurs = cteProblem cteInsolubleOccurs - soluble_occurs = cteProblem cteSolubleOccurs + impredicative = cteProblem cteImpredicative + type_family = cteProblem cteTypeFamily + insoluble_occurs = cteProblem cteInsolubleOccurs + soluble_occurs = cteProblem cteSolubleOccurs -- The GHCi runtime debugger does its type-matching with -- unification variables that can unify with a polytype diff --git a/compiler/GHC/Tc/Utils/Unify.hs-boot b/compiler/GHC/Tc/Utils/Unify.hs-boot index dc8bcce6e8..8afdbcd5ed 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs-boot +++ b/compiler/GHC/Tc/Utils/Unify.hs-boot @@ -1,15 +1,15 @@ module GHC.Tc.Utils.Unify where import GHC.Prelude +import GHC.Core.Type ( Mult ) import GHC.Tc.Utils.TcType ( TcTauType ) import GHC.Tc.Types ( TcM ) import GHC.Tc.Types.Evidence ( TcCoercion, HsWrapper ) -import GHC.Tc.Types.Origin ( CtOrigin, TypedThing ) -import GHC.Hs.Type ( Mult ) +import GHC.Tc.Types.Origin ( CtOrigin, TypedThing ) -- This boot file exists only to tie the knot between --- GHC.Tc.Utils.Unify and Inst +-- GHC.Tc.Utils.Unify and GHC.Tc.Utils.Instantiate unifyType :: Maybe TypedThing -> TcTauType -> TcTauType -> TcM TcCoercion unifyKind :: Maybe TypedThing -> TcTauType -> TcTauType -> TcM TcCoercion diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs index 6046c60dbc..9010c43d46 100644 --- a/compiler/GHC/Tc/Validity.hs +++ b/compiler/GHC/Tc/Validity.hs @@ -1677,7 +1677,6 @@ validDerivPred tv_set pred IrredPred {} -> True -- Accept (f a) EqPred {} -> False -- Reject equality constraints ForAllPred {} -> False -- Rejects quantified predicates - SpecialPred {} -> False -- Rejects special predicates {- ************************************************************************ @@ -1814,10 +1813,6 @@ checkInstTermination theta head_pred -> check (foralld_tvs `extendVarSetList` tvs) head_pred' -- Termination of the quantified predicate itself is checked -- when the predicates are individually checked for validity - SpecialPred {} -> - pprPanic "checkInstTermination: unexpected special constraint" $ - vcat [ text "pred:" <+> ppr pred - , text "theta:" <+> ppr theta ] check2 foralld_tvs pred pred_size | not (null bad_tvs) = failWithTc $ TcRnUnknownMessage $ mkPlainError noHints $ diff --git a/compiler/GHC/Types/Basic.hs b/compiler/GHC/Types/Basic.hs index 3843e2c880..a843250de7 100644 --- a/compiler/GHC/Types/Basic.hs +++ b/compiler/GHC/Types/Basic.hs @@ -1936,7 +1936,7 @@ mightBeUnlifted _ = True -- | Are we dealing with an expression or a pattern? -- -- Used only for the textual output of certain error messages; --- see the 'FRRDataConArg' constructor of 'FRROrigin'. +-- see the 'FRRDataConArg' constructor of 'FixedRuntimeRepContext'. data ExprOrPat = Expression | Pattern diff --git a/testsuite/tests/linters/notes.stdout b/testsuite/tests/linters/notes.stdout index 224fade77a..16fd6a02ac 100644 --- a/testsuite/tests/linters/notes.stdout +++ b/testsuite/tests/linters/notes.stdout @@ -83,7 +83,6 @@ ref compiler/GHC/Tc/Instance/Family.hs:515:35: Note [Constrained family i ref compiler/GHC/Tc/Module.hs:698:15: Note [Extra dependencies from .hs-boot files] ref compiler/GHC/Tc/Module.hs:1904:19: Note [Root-main id] ref compiler/GHC/Tc/Module.hs:1974:6: Note [Root-main id] -ref compiler/GHC/Tc/Solver.hs:2541:36: Note [Kind generalisation and SigTvs] ref compiler/GHC/Tc/Solver/Canonical.hs:1229:33: Note [Canonical LHS] ref compiler/GHC/Tc/Solver/Interact.hs:1638:9: Note [No touchables as FunEq RHS] ref compiler/GHC/Tc/Solver/Interact.hs:2292:12: Note [The equality class story] diff --git a/testsuite/tests/rep-poly/RepPolyArgument.hs b/testsuite/tests/rep-poly/RepPolyArgument.hs new file mode 100644 index 0000000000..4f72e89e32 --- /dev/null +++ b/testsuite/tests/rep-poly/RepPolyArgument.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE ExplicitForAll, PolyKinds, StandaloneKindSignatures, TypeApplications, TypeFamilies #-} + +module RepPolyArgument where + +import GHC.Exts + +type R :: forall k. k +data family R + +foo = undefined (undefined @(R @RuntimeRep)) diff --git a/testsuite/tests/rep-poly/RepPolyArgument.stderr b/testsuite/tests/rep-poly/RepPolyArgument.stderr new file mode 100644 index 0000000000..b5050fc6a5 --- /dev/null +++ b/testsuite/tests/rep-poly/RepPolyArgument.stderr @@ -0,0 +1,13 @@ + +RepPolyArgument.hs:10:18: error: + • The argument ‘(undefined @(R @RuntimeRep))’ of ‘undefined’ + does not have a fixed runtime representation. + Its type is: + t0 :: TYPE c0 + Cannot unify ‘R’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. + • In the first argument of ‘undefined’, namely + ‘(undefined @(R @RuntimeRep))’ + In the expression: undefined (undefined @(R @RuntimeRep)) + In an equation for ‘foo’: + foo = undefined (undefined @(R @RuntimeRep)) diff --git a/testsuite/tests/rep-poly/RepPolyArrowFun.stderr b/testsuite/tests/rep-poly/RepPolyArrowFun.stderr index db14b272f3..a79570822a 100644 --- a/testsuite/tests/rep-poly/RepPolyArrowFun.stderr +++ b/testsuite/tests/rep-poly/RepPolyArrowFun.stderr @@ -1,34 +1,27 @@ -RepPolyArrowFun.hs:29:9: error: - • • The return type of the arrow function - ‘arr’ +RepPolyArrowFun.hs:29:19: error: + • • The function in the first order arrow application of + ‘undefined’ + to + ‘x’ does not have a fixed runtime representation. Its type is: - arr b c :: TYPE r + arr a a :: TYPE r + • The return type of the arrow function + ‘first’ + does not have a fixed runtime representation. + Its type is: + arr (b, d) (c, d) :: TYPE r • The return type of the arrow function ‘(>>>)’ does not have a fixed runtime representation. Its type is: - arr a1 c4 :: TYPE r + arr a c :: TYPE r • The return type of the arrow function - ‘first’ + ‘arr’ does not have a fixed runtime representation. Its type is: - arr (b1, d) (c5, d) :: TYPE r - • When checking that ‘arr’ (needed by a syntactic construct) - has the required type: forall b c. (b -> c) -> arr b c - arising from a proc expression at RepPolyArrowFun.hs:29:9-32 - In the expression: proc x -> undefined -< x - In an equation for ‘foo’: foo _ = proc x -> undefined -< x - -RepPolyArrowFun.hs:29:19: error: - • The function in the first order arrow application of - ‘undefined’ - to - ‘x’ - does not have a fixed runtime representation. - Its type is: - arr a a :: TYPE r + arr b c :: TYPE r • In the command: undefined -< x In the expression: proc x -> undefined -< x In an equation for ‘foo’: foo _ = proc x -> undefined -< x diff --git a/testsuite/tests/rep-poly/RepPolyBackpack1.stderr b/testsuite/tests/rep-poly/RepPolyBackpack1.stderr index f521ada91c..e4a128ea4d 100644 --- a/testsuite/tests/rep-poly/RepPolyBackpack1.stderr +++ b/testsuite/tests/rep-poly/RepPolyBackpack1.stderr @@ -3,24 +3,7 @@ [2 of 2] Compiling NumberStuff ( number-unknown\NumberStuff.hs, nothing ) RepPolyBackpack1.bkp:17:5: error: - The first pattern in the equation for ‘funcA’ + The second pattern in the equation for ‘funcA’ does not have a fixed runtime representation. Its type is: Number l :: TYPE (Rep l) - -RepPolyBackpack1.bkp:17:17: error: - • The argument ‘x’ of ‘plus’ - does not have a fixed runtime representation. - Its type is: - Number l :: TYPE (Rep l) - • In the expression: plus x (multiply x y) - In an equation for ‘funcA’: funcA x y = plus x (multiply x y) - -RepPolyBackpack1.bkp:17:25: error: - • The argument ‘x’ of ‘multiply’ - does not have a fixed runtime representation. - Its type is: - Number l :: TYPE (Rep l) - • In the second argument of ‘plus’, namely ‘(multiply x y)’ - In the expression: plus x (multiply x y) - In an equation for ‘funcA’: funcA x y = plus x (multiply x y) diff --git a/testsuite/tests/rep-poly/RepPolyBinder.stderr b/testsuite/tests/rep-poly/RepPolyBinder.stderr index 33802a0621..177a4865e6 100644 --- a/testsuite/tests/rep-poly/RepPolyBinder.stderr +++ b/testsuite/tests/rep-poly/RepPolyBinder.stderr @@ -8,12 +8,3 @@ RepPolyBinder.hs:11:1: error: does not have a fixed runtime representation. Its type is: b :: TYPE rep2 - -RepPolyBinder.hs:11:17: error: - • The first argument of the view pattern - myId - does not have a fixed runtime representation. - Its type is: - b :: TYPE rep2 - • In the pattern: myId -> bndr_b - In an equation for ‘foo’: foo bndr_a pat@(myId -> bndr_b) = () diff --git a/testsuite/tests/rep-poly/RepPolyCase2.stderr b/testsuite/tests/rep-poly/RepPolyCase2.stderr index f1f59116c9..e84b8db2ed 100644 --- a/testsuite/tests/rep-poly/RepPolyCase2.stderr +++ b/testsuite/tests/rep-poly/RepPolyCase2.stderr @@ -4,8 +4,5 @@ RepPolyCase2.hs:33:7: error: does not have a fixed runtime representation. Its type is: Unbox Int :: TYPE (Rep Int) - NB: GHC does not (yet) support rewriting in runtime representations. - Please comment on GHC ticket #13105 if this is causing you trouble. - <https://gitlab.haskell.org/ghc/ghc/-/issues/13105> • In the expression: case unbox (3 :: Int) of _ -> () In an equation for ‘x’: x _ = case unbox (3 :: Int) of _ -> () diff --git a/testsuite/tests/rep-poly/RepPolyDoBind.stderr b/testsuite/tests/rep-poly/RepPolyDoBind.stderr index b3541dc5d5..bc3bd34465 100644 --- a/testsuite/tests/rep-poly/RepPolyDoBind.stderr +++ b/testsuite/tests/rep-poly/RepPolyDoBind.stderr @@ -4,7 +4,9 @@ RepPolyDoBind.hs:26:3: error: arising from a do statement does not have a fixed runtime representation. Its type is: - ma0 :: TYPE rep + ma0 :: TYPE c0 + Cannot unify ‘rep’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. • In a stmt of a 'do' block: a <- undefined In the expression: do a <- undefined @@ -13,3 +15,5 @@ RepPolyDoBind.hs:26:3: error: foo _ = do a <- undefined return () + • Relevant bindings include + foo :: () -> ma (bound at RepPolyDoBind.hs:25:1) diff --git a/testsuite/tests/rep-poly/RepPolyDoBody1.stderr b/testsuite/tests/rep-poly/RepPolyDoBody1.stderr index f71deeb24b..e31d97891e 100644 --- a/testsuite/tests/rep-poly/RepPolyDoBody1.stderr +++ b/testsuite/tests/rep-poly/RepPolyDoBody1.stderr @@ -1,15 +1,12 @@ RepPolyDoBody1.hs:24:3: error: - • • The first argument of the rebindable syntax operator ‘(>>)’ - arising from a do statement - does not have a fixed runtime representation. - Its type is: - ma :: TYPE rep - • The first argument of the rebindable syntax operator ‘(>>)’ - arising from a do statement - does not have a fixed runtime representation. - Its type is: - mb0 :: TYPE rep + • The first argument of the rebindable syntax operator ‘(>>)’ + arising from a do statement + does not have a fixed runtime representation. + Its type is: + ma0 :: TYPE c0 + Cannot unify ‘rep’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. • In a stmt of a 'do' block: undefined :: ma In the expression: do undefined :: ma @@ -18,3 +15,5 @@ RepPolyDoBody1.hs:24:3: error: foo _ = do undefined :: ma return () + • Relevant bindings include + foo :: () -> ma (bound at RepPolyDoBody1.hs:23:1) diff --git a/testsuite/tests/rep-poly/RepPolyDoBody2.stderr b/testsuite/tests/rep-poly/RepPolyDoBody2.stderr index 1d28c20d26..40a033a33d 100644 --- a/testsuite/tests/rep-poly/RepPolyDoBody2.stderr +++ b/testsuite/tests/rep-poly/RepPolyDoBody2.stderr @@ -4,7 +4,9 @@ RepPolyDoBody2.hs:23:3: error: arising from a do statement does not have a fixed runtime representation. Its type is: - mb0 :: TYPE rep + mb0 :: TYPE c0 + Cannot unify ‘rep’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. • In a stmt of a 'do' block: undefined :: () In the expression: do undefined :: () @@ -13,3 +15,5 @@ RepPolyDoBody2.hs:23:3: error: foo _ = do undefined :: () return () + • Relevant bindings include + foo :: () -> ma (bound at RepPolyDoBody2.hs:22:1) diff --git a/testsuite/tests/rep-poly/RepPolyInferPatBind.hs b/testsuite/tests/rep-poly/RepPolyInferPatBind.hs new file mode 100644 index 0000000000..ebf161ad60 --- /dev/null +++ b/testsuite/tests/rep-poly/RepPolyInferPatBind.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE Haskell2010 #-} + +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UnboxedTuples #-} + +module RepPolyInferPatBind where + +import Data.Kind +import GHC.Exts + +type R :: RuntimeRep +type family R where {} + +type T :: TYPE R +type family T where {} + +(x :: T) = x diff --git a/testsuite/tests/rep-poly/RepPolyInferPatBind.stderr b/testsuite/tests/rep-poly/RepPolyInferPatBind.stderr new file mode 100644 index 0000000000..8e9f7fb032 --- /dev/null +++ b/testsuite/tests/rep-poly/RepPolyInferPatBind.stderr @@ -0,0 +1,14 @@ + +RepPolyInferPatBind.hs:21:1: error: + The binder ‘x’ does not have a fixed runtime representation. + Its type is: + T :: TYPE R + +RepPolyInferPatBind.hs:21:2: error: + • The pattern binding does not have a fixed runtime representation. + Its type is: + T :: TYPE R + • When checking that the pattern signature: T + fits the type of its context: T + In the pattern: x :: T + In a pattern binding: (x :: T) = x diff --git a/testsuite/tests/rep-poly/RepPolyInferPatSyn.hs b/testsuite/tests/rep-poly/RepPolyInferPatSyn.hs new file mode 100644 index 0000000000..27ed7bfc25 --- /dev/null +++ b/testsuite/tests/rep-poly/RepPolyInferPatSyn.hs @@ -0,0 +1,22 @@ +{-# LANGUAGE Haskell2010 #-} + +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UnboxedTuples #-} + +module RepPolyInferPatSyn where + +import Data.Kind +import GHC.Exts + +type R :: RuntimeRep +type family R where {} + +type T :: TYPE R +type family T where {} + +pattern P a = (a :: T) diff --git a/testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr b/testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr new file mode 100644 index 0000000000..7e07ea88ca --- /dev/null +++ b/testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr @@ -0,0 +1,10 @@ + +RepPolyInferPatSyn.hs:22:16: error: + • The pattern synonym argument pattern + does not have a fixed runtime representation. + Its type is: + T :: TYPE R + • When checking that the pattern signature: T + fits the type of its context: T + In the pattern: a :: T + In the declaration for pattern synonym ‘P’ diff --git a/testsuite/tests/rep-poly/RepPolyLeftSection2.stderr b/testsuite/tests/rep-poly/RepPolyLeftSection2.stderr index fd9dbb31b1..b273475650 100644 --- a/testsuite/tests/rep-poly/RepPolyLeftSection2.stderr +++ b/testsuite/tests/rep-poly/RepPolyLeftSection2.stderr @@ -3,6 +3,10 @@ RepPolyLeftSection2.hs:14:11: error: • The argument ‘undefined’ of ‘f’ does not have a fixed runtime representation. Its type is: - a :: TYPE r + a0 :: TYPE c0 + Cannot unify ‘r’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. • In the expression: undefined `f` In an equation for ‘test1’: test1 = (undefined `f`) + • Relevant bindings include + test1 :: a -> a (bound at RepPolyLeftSection2.hs:14:1) diff --git a/testsuite/tests/rep-poly/RepPolyMagic.stderr b/testsuite/tests/rep-poly/RepPolyMagic.stderr index 47e7ba81d3..f99d0c740a 100644 --- a/testsuite/tests/rep-poly/RepPolyMagic.stderr +++ b/testsuite/tests/rep-poly/RepPolyMagic.stderr @@ -4,15 +4,23 @@ RepPolyMagic.hs:12:7: error: The second argument of ‘seq’ does not have a fixed runtime representation. Its type is: - b :: TYPE r + b0 :: TYPE c1 + Cannot unify ‘r’ with the type variable ‘c1’ + because it is not a concrete ‘RuntimeRep’. • In the expression: seq In an equation for ‘foo’: foo = seq + • Relevant bindings include + foo :: a -> b -> b (bound at RepPolyMagic.hs:12:1) RepPolyMagic.hs:15:7: error: • Unsaturated use of a representation-polymorphic primitive function. The second argument of ‘oneShot’ does not have a fixed runtime representation. Its type is: - a :: TYPE r + a0 :: TYPE c0 + Cannot unify ‘r’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. • In the expression: oneShot In an equation for ‘bar’: bar = oneShot + • Relevant bindings include + bar :: (a -> a) -> a -> a (bound at RepPolyMagic.hs:15:1) diff --git a/testsuite/tests/rep-poly/RepPolyMcBind.stderr b/testsuite/tests/rep-poly/RepPolyMcBind.stderr index 647a8d625d..676bb543ac 100644 --- a/testsuite/tests/rep-poly/RepPolyMcBind.stderr +++ b/testsuite/tests/rep-poly/RepPolyMcBind.stderr @@ -4,7 +4,11 @@ RepPolyMcBind.hs:26:16: error: arising from a statement in a monad comprehension does not have a fixed runtime representation. Its type is: - ma :: TYPE rep + ma0 :: TYPE c0 + Cannot unify ‘rep’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. • In a stmt of a monad comprehension: x <- undefined :: ma In the expression: [() | x <- undefined :: ma] In an equation for ‘foo’: foo _ = [() | x <- undefined :: ma] + • Relevant bindings include + foo :: () -> ma (bound at RepPolyMcBind.hs:26:1) diff --git a/testsuite/tests/rep-poly/RepPolyMcBody.stderr b/testsuite/tests/rep-poly/RepPolyMcBody.stderr index de9848d4c6..93aca381ce 100644 --- a/testsuite/tests/rep-poly/RepPolyMcBody.stderr +++ b/testsuite/tests/rep-poly/RepPolyMcBody.stderr @@ -4,7 +4,11 @@ RepPolyMcBody.hs:30:16: error: arising from a statement in a monad comprehension does not have a fixed runtime representation. Its type is: - ma0 :: TYPE rep + ma0 :: TYPE c0 + Cannot unify ‘rep’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. • In a stmt of a monad comprehension: True In the expression: [() | True] In an equation for ‘foo’: foo _ = [() | True] + • Relevant bindings include + foo :: () -> ma (bound at RepPolyMcBody.hs:30:1) diff --git a/testsuite/tests/rep-poly/RepPolyMcGuard.stderr b/testsuite/tests/rep-poly/RepPolyMcGuard.stderr index a1a32f7a3a..a545b53c6c 100644 --- a/testsuite/tests/rep-poly/RepPolyMcGuard.stderr +++ b/testsuite/tests/rep-poly/RepPolyMcGuard.stderr @@ -1,15 +1,14 @@ RepPolyMcGuard.hs:30:16: error: - • • The first argument of the rebindable syntax operator ‘(>>)’ - arising from a statement in a monad comprehension - does not have a fixed runtime representation. - Its type is: - ma0 :: TYPE rep - • The first argument of the rebindable syntax operator ‘guard’ - arising from a statement in a monad comprehension - does not have a fixed runtime representation. - Its type is: - a0 :: TYPE rep + • The first argument of the rebindable syntax operator ‘guard’ + arising from a statement in a monad comprehension + does not have a fixed runtime representation. + Its type is: + a0 :: TYPE c0 + Cannot unify ‘rep’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. • In a stmt of a monad comprehension: undefined In the expression: [() | undefined] In an equation for ‘foo’: foo _ = [() | undefined] + • Relevant bindings include + foo :: () -> ma (bound at RepPolyMcGuard.hs:30:1) diff --git a/testsuite/tests/rep-poly/RepPolyNPlusK.stderr b/testsuite/tests/rep-poly/RepPolyNPlusK.stderr index c5e5f84662..80672387db 100644 --- a/testsuite/tests/rep-poly/RepPolyNPlusK.stderr +++ b/testsuite/tests/rep-poly/RepPolyNPlusK.stderr @@ -4,12 +4,3 @@ RepPolyNPlusK.hs:22:1: error: does not have a fixed runtime representation. Its type is: a :: TYPE rep1 - -RepPolyNPlusK.hs:22:6: error: - • The first argument of the rebindable syntax operator ‘(>=)’ - arising from the literal ‘2’ - does not have a fixed runtime representation. - Its type is: - a :: TYPE rep1 - • In the pattern: bndr_a+2 - In an equation for ‘foo’: foo (bndr_a+2) = () diff --git a/testsuite/tests/rep-poly/RepPolyPatBind.stderr b/testsuite/tests/rep-poly/RepPolyPatBind.stderr index 3914ea8e30..976e84e81e 100644 --- a/testsuite/tests/rep-poly/RepPolyPatBind.stderr +++ b/testsuite/tests/rep-poly/RepPolyPatBind.stderr @@ -1,8 +1,11 @@ RepPolyPatBind.hs:18:5: error: - • The binder ‘x’ does not have a fixed runtime representation. - Its type is: - a :: TYPE rep + • • The binder ‘y’ does not have a fixed runtime representation. + Its type is: + a :: TYPE rep + • The binder ‘x’ does not have a fixed runtime representation. + Its type is: + a :: TYPE rep • In the expression: let x, y :: a diff --git a/testsuite/tests/rep-poly/RepPolyRecordPattern.stderr b/testsuite/tests/rep-poly/RepPolyRecordPattern.stderr index 085e2da393..11602f0285 100644 --- a/testsuite/tests/rep-poly/RepPolyRecordPattern.stderr +++ b/testsuite/tests/rep-poly/RepPolyRecordPattern.stderr @@ -4,10 +4,14 @@ RepPolyRecordPattern.hs:7:35: error: does not have a fixed runtime representation. Its type is: a :: TYPE rep - • The first pattern in the equation for ‘fld’ - does not have a fixed runtime representation. - Its type is: - X a :: TYPE rep + • In the pattern: MkX {fld = fld} + In an equation for ‘fld’: fld MkX {fld = fld} = fld + +RepPolyRecordPattern.hs:7:35: error: + The first pattern in the equation for ‘fld’ + does not have a fixed runtime representation. + Its type is: + X a :: TYPE rep RepPolyRecordPattern.hs:13:1: error: The first pattern in the equation for ‘upd’ diff --git a/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr b/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr index 5cdc9205f0..157c0403bc 100644 --- a/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr +++ b/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr @@ -4,16 +4,23 @@ RepPolyRecordUpdate.hs:7:35: error: does not have a fixed runtime representation. Its type is: a :: TYPE rep - • The first pattern in the equation for ‘fld’ - does not have a fixed runtime representation. - Its type is: - X a :: TYPE rep + • In the pattern: MkX {fld = fld} + In an equation for ‘fld’: fld MkX {fld = fld} = fld + +RepPolyRecordUpdate.hs:7:35: error: + The first pattern in the equation for ‘fld’ + does not have a fixed runtime representation. + Its type is: + X a :: TYPE rep RepPolyRecordUpdate.hs:13:9: error: • The record update at field ‘fld’ does not have a fixed runtime representation. Its type is: - a :: TYPE rep - • In the ‘fld’ field of a record - In the expression: x {fld = meth ()} + a0 :: TYPE c1 + Cannot unify ‘rep’ with the type variable ‘c1’ + because it is not a concrete ‘RuntimeRep’. + • In the expression: x {fld = meth ()} In an equation for ‘upd’: upd x = x {fld = meth ()} + • Relevant bindings include + upd :: X b -> X a (bound at RepPolyRecordUpdate.hs:13:1) diff --git a/testsuite/tests/rep-poly/RepPolyRightSection.stderr b/testsuite/tests/rep-poly/RepPolyRightSection.stderr index 62c0bdcd8d..fdc7a399fa 100644 --- a/testsuite/tests/rep-poly/RepPolyRightSection.stderr +++ b/testsuite/tests/rep-poly/RepPolyRightSection.stderr @@ -4,6 +4,10 @@ RepPolyRightSection.hs:14:11: error: The third argument of ‘rightSection’ does not have a fixed runtime representation. Its type is: - a :: TYPE r + a :: TYPE c0 + Cannot unify ‘r’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. • In the expression: `g` undefined In an equation for ‘test2’: test2 = (`g` undefined) + • Relevant bindings include + test2 :: a -> a (bound at RepPolyRightSection.hs:14:1) diff --git a/testsuite/tests/rep-poly/RepPolyRule1.stderr b/testsuite/tests/rep-poly/RepPolyRule1.stderr index f2fcb378da..6250ddb098 100644 --- a/testsuite/tests/rep-poly/RepPolyRule1.stderr +++ b/testsuite/tests/rep-poly/RepPolyRule1.stderr @@ -1,8 +1,25 @@ -RepPolyRule1.hs:11:49: error: +RepPolyRule1.hs:11:51: error: • The argument ‘x’ of ‘f’ does not have a fixed runtime representation. Its type is: - a :: TYPE rep - • In the expression: f x + a1 :: TYPE c0 + Cannot unify ‘rep’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. + • In the first argument of ‘f’, namely ‘x’ + In the expression: f x When checking the rewrite rule "f_id" + • Relevant bindings include + x :: a2 (bound at RepPolyRule1.hs:11:26) + +RepPolyRule1.hs:11:55: error: + • The argument ‘x’ of ‘f’ + does not have a fixed runtime representation. + Its type is: + a1 :: TYPE c0 + Cannot unify ‘rep’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. + • In the expression: x + When checking the rewrite rule "f_id" + • Relevant bindings include + x :: a2 (bound at RepPolyRule1.hs:11:26) diff --git a/testsuite/tests/rep-poly/RepPolyRule3.stderr b/testsuite/tests/rep-poly/RepPolyRule3.stderr index cdbfcdb66b..695a4985bf 100644 --- a/testsuite/tests/rep-poly/RepPolyRule3.stderr +++ b/testsuite/tests/rep-poly/RepPolyRule3.stderr @@ -5,9 +5,6 @@ RepPolyRule3.hs:17:57: error: Its kind is: TYPE (F 'WordRep) (Use -fprint-explicit-coercions to see the full type.) - NB: GHC does not (yet) support rewriting in runtime representations. - Please comment on GHC ticket #13105 if this is causing you trouble. - <https://gitlab.haskell.org/ghc/ghc/-/issues/13105> • In the expression: g x When checking the rewrite rule "g_id" @@ -17,8 +14,5 @@ RepPolyRule3.hs:23:52: error: Its kind is: TYPE (F 'WordRep) (Use -fprint-explicit-coercions to see the full type.) - NB: GHC does not (yet) support rewriting in runtime representations. - Please comment on GHC ticket #13105 if this is causing you trouble. - <https://gitlab.haskell.org/ghc/ghc/-/issues/13105> • In the expression: h x When checking the rewrite rule "h_id" diff --git a/testsuite/tests/rep-poly/RepPolyTuple.stderr b/testsuite/tests/rep-poly/RepPolyTuple.stderr index e651dca0fd..f9c1275976 100644 --- a/testsuite/tests/rep-poly/RepPolyTuple.stderr +++ b/testsuite/tests/rep-poly/RepPolyTuple.stderr @@ -1,9 +1,17 @@ RepPolyTuple.hs:11:9: error: - • The tuple argument in first position - does not have a fixed runtime representation. - Its type is: - a :: TYPE r + • • The tuple argument in third position + does not have a fixed runtime representation. + Its type is: + a :: TYPE r + • The tuple argument in second position + does not have a fixed runtime representation. + Its type is: + a :: TYPE r + • The tuple argument in first position + does not have a fixed runtime representation. + Its type is: + a :: TYPE r • In the expression: (# bar (), bar (), bar () #) In an equation for ‘foo’: foo _ diff --git a/testsuite/tests/rep-poly/RepPolyTupleSection.stderr b/testsuite/tests/rep-poly/RepPolyTupleSection.stderr index b2569ecfd6..fa2ddf93cb 100644 --- a/testsuite/tests/rep-poly/RepPolyTupleSection.stderr +++ b/testsuite/tests/rep-poly/RepPolyTupleSection.stderr @@ -3,6 +3,10 @@ RepPolyTupleSection.hs:11:7: error: • The second component of the tuple section does not have a fixed runtime representation. Its type is: - a :: TYPE r + t0 :: TYPE c0 + Cannot unify ‘r’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. • In the expression: (# 3#, #) In an equation for ‘foo’: foo = (# 3#, #) + • Relevant bindings include + foo :: a -> (# Int#, a #) (bound at RepPolyTupleSection.hs:11:1) diff --git a/testsuite/tests/rep-poly/T11473.stderr b/testsuite/tests/rep-poly/T11473.stderr index 411e074c0e..8e7b81f3e9 100644 --- a/testsuite/tests/rep-poly/T11473.stderr +++ b/testsuite/tests/rep-poly/T11473.stderr @@ -4,11 +4,3 @@ T11473.hs:19:1: error: does not have a fixed runtime representation. Its type is: a :: TYPE r - -T11473.hs:19:11: error: - • The argument ‘x’ of ‘boxed’ - does not have a fixed runtime representation. - Its type is: - a :: TYPE r - • In the expression: boxed x - In an equation for ‘hello’: hello x = boxed x diff --git a/testsuite/tests/rep-poly/T12709.stderr b/testsuite/tests/rep-poly/T12709.stderr index 782f995942..d96ec57896 100644 --- a/testsuite/tests/rep-poly/T12709.stderr +++ b/testsuite/tests/rep-poly/T12709.stderr @@ -1,9 +1,11 @@ T12709.hs:28:13: error: - • The argument ‘1 + 2 + 3’ of ‘(+)’ + • The argument ‘1’ of ‘(+)’ does not have a fixed runtime representation. Its type is: - a :: TYPE rep + a0 :: TYPE c0 + Cannot unify ‘rep’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. • In the expression: 1 + 2 + 3 + 4 In an equation for ‘u’: u = 1 + 2 + 3 + 4 In the expression: @@ -11,3 +13,4 @@ T12709.hs:28:13: error: u :: Num (a :: TYPE rep) => a u = 1 + 2 + 3 + 4 in BUB u u + • Relevant bindings include u :: a (bound at T12709.hs:28:9) diff --git a/testsuite/tests/rep-poly/T12973.stderr b/testsuite/tests/rep-poly/T12973.stderr index 7a70b92859..b328176c1d 100644 --- a/testsuite/tests/rep-poly/T12973.stderr +++ b/testsuite/tests/rep-poly/T12973.stderr @@ -3,6 +3,9 @@ T12973.hs:13:7: error: • The argument ‘3’ of ‘(+)’ does not have a fixed runtime representation. Its type is: - a :: TYPE r + a0 :: TYPE c0 + Cannot unify ‘r’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. • In the expression: 3 + 4 In an equation for ‘foo’: foo = 3 + 4 + • Relevant bindings include foo :: a (bound at T12973.hs:13:1) diff --git a/testsuite/tests/rep-poly/T13105.stderr b/testsuite/tests/rep-poly/T13105.stderr deleted file mode 100644 index e5eaafa03a..0000000000 --- a/testsuite/tests/rep-poly/T13105.stderr +++ /dev/null @@ -1,10 +0,0 @@ - -T13105.hs:22:3: error: - • The first pattern in the equation for ‘abst’ - does not have a fixed runtime representation. - Its type is: - Rep Int :: TYPE (RepRep Int) - NB: GHC does not (yet) support rewriting in runtime representations. - Please comment on GHC ticket #13105 if this is causing you trouble. - <https://gitlab.haskell.org/ghc/ghc/-/issues/13105> - • In the instance declaration for ‘HasRep Int’ diff --git a/testsuite/tests/rep-poly/T13233.stderr b/testsuite/tests/rep-poly/T13233.stderr index 614aa7b796..5b083ea6c7 100644 --- a/testsuite/tests/rep-poly/T13233.stderr +++ b/testsuite/tests/rep-poly/T13233.stderr @@ -1,22 +1,24 @@ T13233.hs:14:11: error: - • The data constructor argument in first position + • The data constructor argument in second position does not have a fixed runtime representation. Its type is: - a :: TYPE rep + b1 :: TYPE c3 + Cannot unify ‘rep’ with the type variable ‘c3’ + because it is not a concrete ‘RuntimeRep’. • In the first argument of ‘bar’, namely ‘(#,#)’ In the expression: bar (#,#) In an equation for ‘baz’: baz = bar (#,#) + • Relevant bindings include + baz :: a -> a -> (# a, a #) (bound at T13233.hs:14:1) T13233.hs:22:16: error: - • • The data constructor argument in first position - does not have a fixed runtime representation. - Its type is: - a :: TYPE rep1 - • The data constructor argument in second position - does not have a fixed runtime representation. - Its type is: - b :: TYPE rep2 + • The data constructor argument in second position + does not have a fixed runtime representation. + Its type is: + b0 :: TYPE c1 + Cannot unify ‘rep2’ with the type variable ‘c1’ + because it is not a concrete ‘RuntimeRep’. • In the first argument of ‘obscure’, namely ‘(#,#)’ In the expression: obscure (#,#) In an equation for ‘quux’: quux = obscure (#,#) diff --git a/testsuite/tests/rep-poly/T13929.stderr b/testsuite/tests/rep-poly/T13929.stderr index 23f0005172..5365f7d6b0 100644 --- a/testsuite/tests/rep-poly/T13929.stderr +++ b/testsuite/tests/rep-poly/T13929.stderr @@ -1,32 +1,28 @@ T13929.hs:29:24: error: - • • The tuple argument in first position - does not have a fixed runtime representation. - Its type is: - GUnboxed f rf :: TYPE rf - • The tuple argument in second position - does not have a fixed runtime representation. - Its type is: - GUnboxed g rg :: TYPE rg + • The tuple argument in first position + does not have a fixed runtime representation. + Its type is: + a0 :: TYPE c1 + Cannot unify ‘rf’ with the type variable ‘c1’ + because it is not a concrete ‘RuntimeRep’. • In the expression: (# gunbox x, gunbox y #) In an equation for ‘gunbox’: gunbox (x :*: y) = (# gunbox x, gunbox y #) In the instance declaration for ‘GUnbox (f :*: g) ('TupleRep '[rf, rg])’ - -T13929.hs:33:21: error: - • The unboxed sum does not have a fixed runtime representation. - Its type is: - GUnboxed (f :+: g) ('SumRep '[rf, rg]) :: TYPE ('SumRep '[rf, rg]) - • In the expression: (# gunbox l | #) - In an equation for ‘gunbox’: gunbox (L1 l) = (# gunbox l | #) - In the instance declaration for - ‘GUnbox (f :+: g) ('SumRep '[rf, rg])’ + • Relevant bindings include + x :: f p (bound at T13929.hs:29:13) + gunbox :: (:*:) f g p -> GUnboxed (f :*: g) ('TupleRep '[rf, rg]) + (bound at T13929.hs:29:5) T13929.hs:34:21: error: - • The unboxed sum does not have a fixed runtime representation. - Its type is: - GUnboxed (f :+: g) ('SumRep '[rf, rg]) :: TYPE ('SumRep '[rf, rg]) + • • The unboxed sum does not have a fixed runtime representation. + Its type is: + GUnboxed (f :+: g) ('SumRep '[rf, rg]) :: TYPE ('SumRep '[rf, rg]) + • The unboxed sum does not have a fixed runtime representation. + Its type is: + GUnboxed (f :+: g) ('SumRep '[rf, rg]) :: TYPE ('SumRep '[rf, rg]) • In the expression: (# | gunbox r #) In an equation for ‘gunbox’: gunbox (R1 r) = (# | gunbox r #) In the instance declaration for diff --git a/testsuite/tests/rep-poly/T14561.stderr b/testsuite/tests/rep-poly/T14561.stderr index 3c372e689c..8f102143eb 100644 --- a/testsuite/tests/rep-poly/T14561.stderr +++ b/testsuite/tests/rep-poly/T14561.stderr @@ -4,6 +4,10 @@ T14561.hs:12:9: error: The first argument of ‘unsafeCoerce#’ does not have a fixed runtime representation. Its type is: - a :: TYPE r + a0 :: TYPE c0 + Cannot unify ‘r’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. • In the expression: unsafeCoerce# In an equation for ‘badId’: badId = unsafeCoerce# + • Relevant bindings include + badId :: a -> a (bound at T14561.hs:12:1) diff --git a/testsuite/tests/rep-poly/T14561b.stderr b/testsuite/tests/rep-poly/T14561b.stderr index 7af3b05511..bbc72d01d8 100644 --- a/testsuite/tests/rep-poly/T14561b.stderr +++ b/testsuite/tests/rep-poly/T14561b.stderr @@ -4,6 +4,10 @@ T14561b.hs:12:9: error: The first argument of ‘coerce’ does not have a fixed runtime representation. Its type is: - a :: TYPE r + a0 :: TYPE c0 + Cannot unify ‘r’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. • In the expression: coerce In an equation for ‘badId’: badId = coerce + • Relevant bindings include + badId :: a -> a (bound at T14561b.hs:12:1) diff --git a/testsuite/tests/rep-poly/T17021.stderr b/testsuite/tests/rep-poly/T17021.stderr index 0521ed1259..39f907b40c 100644 --- a/testsuite/tests/rep-poly/T17021.stderr +++ b/testsuite/tests/rep-poly/T17021.stderr @@ -5,8 +5,5 @@ T17021.hs:18:5: error: Its kind is: TYPE (Id LiftedRep) (Use -fprint-explicit-coercions to see the full type.) - NB: GHC does not (yet) support rewriting in runtime representations. - Please comment on GHC ticket #13105 if this is causing you trouble. - <https://gitlab.haskell.org/ghc/ghc/-/issues/13105> • In the expression: MkT 42 In an equation for ‘f’: f = MkT 42 diff --git a/testsuite/tests/rep-poly/T17536b.stderr b/testsuite/tests/rep-poly/T17536b.stderr deleted file mode 100644 index a2d161038a..0000000000 --- a/testsuite/tests/rep-poly/T17536b.stderr +++ /dev/null @@ -1,22 +0,0 @@ - -T17536b.hs:19:7: error: - • The binder of the lambda expression - does not have a fixed runtime representation. - Its type is: - a :: TYPE r - NB: GHC does not (yet) support rewriting in runtime representations. - Please comment on GHC ticket #13105 if this is causing you trouble. - <https://gitlab.haskell.org/ghc/ghc/-/issues/13105> - • In the expression: \ _ -> 0 - In an equation for ‘g’: g L = \ _ -> 0 - -T17536b.hs:20:7: error: - • The binder of the lambda expression - does not have a fixed runtime representation. - Its type is: - a :: TYPE r - NB: GHC does not (yet) support rewriting in runtime representations. - Please comment on GHC ticket #13105 if this is causing you trouble. - <https://gitlab.haskell.org/ghc/ghc/-/issues/13105> - • In the expression: \ _ -> 3# - In an equation for ‘g’: g U = \ _ -> 3# diff --git a/testsuite/tests/rep-poly/T17817.stderr b/testsuite/tests/rep-poly/T17817.stderr index 7acdec120a..4fb45622bc 100644 --- a/testsuite/tests/rep-poly/T17817.stderr +++ b/testsuite/tests/rep-poly/T17817.stderr @@ -4,6 +4,15 @@ T17817.hs:16:10: error: The first argument of ‘mkWeak#’ does not have a fixed runtime representation. Its type is: - a :: TYPE ('BoxedRep l) + a0 :: TYPE ('BoxedRep c0) + Cannot unify ‘l’ with the type variable ‘c0’ + because it is not a concrete ‘Levity’. • In the expression: mkWeak# In an equation for ‘primop’: primop = mkWeak# + • Relevant bindings include + primop :: a + -> b + -> (State# RealWorld -> (# State# RealWorld, c #)) + -> State# RealWorld + -> (# State# RealWorld, Weak# b #) + (bound at T17817.hs:16:1) diff --git a/testsuite/tests/rep-poly/T19615.stderr b/testsuite/tests/rep-poly/T19615.stderr index 873b3816f9..f0d3d8297d 100644 --- a/testsuite/tests/rep-poly/T19615.stderr +++ b/testsuite/tests/rep-poly/T19615.stderr @@ -1,9 +1,14 @@ -T19615.hs:17:14: error: +T19615.hs:17:21: error: • The argument ‘(f x)’ of ‘lift'’ does not have a fixed runtime representation. Its type is: - b :: TYPE r' - • In the expression: lift' (f x) id + a0 :: TYPE c0 + Cannot unify ‘r'’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. + • In the first argument of ‘lift'’, namely ‘(f x)’ + In the expression: lift' (f x) id In an equation for ‘mapF’: mapF f x = lift' (f x) id - In the instance declaration for ‘Call LiftedRep’ + • Relevant bindings include + f :: a -> b (bound at T19615.hs:17:8) + mapF :: (a -> b) -> Lev a -> Lev b (bound at T19615.hs:17:3) diff --git a/testsuite/tests/rep-poly/T19709b.stderr b/testsuite/tests/rep-poly/T19709b.stderr index 6592f2d67f..a236ea99e2 100644 --- a/testsuite/tests/rep-poly/T19709b.stderr +++ b/testsuite/tests/rep-poly/T19709b.stderr @@ -1,13 +1,11 @@ -T19709b.hs:11:7: error: +T19709b.hs:11:15: error: • The argument ‘(error @Any "e2")’ of ‘levfun’ does not have a fixed runtime representation. Its type is: - a0 :: TYPE Any - • In the first argument of ‘seq’, namely ‘levfun (error @Any "e2")’ + a1 :: TYPE c0 + Cannot unify ‘Any’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. + • In the first argument of ‘levfun’, namely ‘(error @Any "e2")’ + In the first argument of ‘seq’, namely ‘levfun (error @Any "e2")’ In the expression: levfun (error @Any "e2") `seq` return [] - In the expression: - let - levfun :: forall (r :: RuntimeRep) (a :: TYPE r). a -> () - levfun = error "e1" - in levfun (error @Any "e2") `seq` return [] diff --git a/testsuite/tests/rep-poly/T20113.stderr b/testsuite/tests/rep-poly/T20113.stderr index 2e51b23d85..a941c709de 100644 --- a/testsuite/tests/rep-poly/T20113.stderr +++ b/testsuite/tests/rep-poly/T20113.stderr @@ -4,7 +4,12 @@ T20113.hs:7:35: error: does not have a fixed runtime representation. Its type is: a :: TYPE rep - • The first pattern in the equation for ‘$sel:y_fld:MkY’ - does not have a fixed runtime representation. - Its type is: - Y a :: TYPE rep + • In the pattern: MkY {y_fld = $sel:y_fld:MkY} + In an equation for ‘T20113.$sel:y_fld:MkY’: + T20113.$sel:y_fld:MkY MkY {y_fld = $sel:y_fld:MkY} = $sel:y_fld:MkY + +T20113.hs:7:35: error: + The first pattern in the equation for ‘$sel:y_fld:MkY’ + does not have a fixed runtime representation. + Its type is: + Y a :: TYPE rep diff --git a/testsuite/tests/rep-poly/T20363.stderr b/testsuite/tests/rep-poly/T20363.stderr index fdc6f94db6..cf719e3176 100644 --- a/testsuite/tests/rep-poly/T20363.stderr +++ b/testsuite/tests/rep-poly/T20363.stderr @@ -5,8 +5,5 @@ T20363.hs:23:10: error: Its kind is: TYPE NilRep (Use -fprint-explicit-coercions to see the full type.) - NB: GHC does not (yet) support rewriting in runtime representations. - Please comment on GHC ticket #13105 if this is causing you trouble. - <https://gitlab.haskell.org/ghc/ghc/-/issues/13105> • In the pattern: MkNT (##) In an equation for ‘test1b’: test1b (MkNT (##)) = 0 diff --git a/testsuite/tests/rep-poly/T20363_show_co.stderr b/testsuite/tests/rep-poly/T20363_show_co.stderr index 6b18496208..69fa078718 100644 --- a/testsuite/tests/rep-poly/T20363_show_co.stderr +++ b/testsuite/tests/rep-poly/T20363_show_co.stderr @@ -5,8 +5,5 @@ T20363_show_co.hs:23:10: error: Its type is: ((# #) |> (TYPE (Sym (T20363_show_co.D:R:NilRep[0])))_N) :: TYPE NilRep - NB: GHC does not (yet) support rewriting in runtime representations. - Please comment on GHC ticket #13105 if this is causing you trouble. - <https://gitlab.haskell.org/ghc/ghc/-/issues/13105> • In the pattern: MkNT (##) In an equation for ‘test1b’: test1b (MkNT (##)) = 0 diff --git a/testsuite/tests/rep-poly/T20363b.stderr b/testsuite/tests/rep-poly/T20363b.stderr index 8d2251390f..7651077162 100644 --- a/testsuite/tests/rep-poly/T20363b.stderr +++ b/testsuite/tests/rep-poly/T20363b.stderr @@ -1,50 +1,22 @@ -T20363b.hs:45:10: error: - • The newtype constructor pattern - does not have a fixed runtime representation. - Its type is: - NestedTuple 'Zero Addr# :: TYPE (NestedTupleRep 'Zero 'AddrRep) - NB: GHC does not (yet) support rewriting in runtime representations. - Please comment on GHC ticket #13105 if this is causing you trouble. - <https://gitlab.haskell.org/ghc/ghc/-/issues/13105> - • In the pattern: MkNT (##) - In an equation for ‘test1b’: test1b (MkNT (##)) = 0 - T20363b.hs:48:10: error: - • The newtype constructor pattern - does not have a fixed runtime representation. - Its type is: - NestedTuple ('Suc 'Zero) Addr# :: TYPE - (NestedTupleRep ('Suc 'Zero) 'AddrRep) - NB: GHC does not (yet) support rewriting in runtime representations. - Please comment on GHC ticket #13105 if this is causing you trouble. - <https://gitlab.haskell.org/ghc/ghc/-/issues/13105> + • • The newtype constructor pattern + does not have a fixed runtime representation. + Its type is: + NestedTuple ('Suc 'Zero) Addr# :: TYPE + (NestedTupleRep ('Suc 'Zero) 'AddrRep) + • The argument ‘(# nullAddr#, (##) #)’ of ‘MkNT’ + does not have a fixed runtime representation. + Its type is: + NestedTuple ('Suc 'Zero) Addr# :: TYPE + (NestedTupleRep ('Suc 'Zero) 'AddrRep) + • The newtype constructor pattern + does not have a fixed runtime representation. + Its type is: + NestedTuple 'Zero Addr# :: TYPE (NestedTupleRep 'Zero 'AddrRep) + • The argument ‘(##)’ of ‘MkNT’ + does not have a fixed runtime representation. + Its type is: + NestedTuple 'Zero Addr# :: TYPE (NestedTupleRep 'Zero 'AddrRep) • In the pattern: MkNT (# i, (##) #) In an equation for ‘test2b’: test2b (MkNT (# i, (##) #)) = i - -T20363b.hs:51:19: error: - • The argument ‘(##)’ of ‘MkNT’ - does not have a fixed runtime representation. - Its type is: - NestedTuple 'Zero Addr# :: TYPE (NestedTupleRep 'Zero 'AddrRep) - NB: GHC does not (yet) support rewriting in runtime representations. - Please comment on GHC ticket #13105 if this is causing you trouble. - <https://gitlab.haskell.org/ghc/ghc/-/issues/13105> - • In the first argument of ‘test1b’, namely ‘(MkNT (##))’ - In the expression: test1b (MkNT (##)) - In an equation for ‘test1c’: test1c = test1b (MkNT (##)) - -T20363b.hs:54:21: error: - • The argument ‘(# nullAddr#, (##) #)’ of ‘MkNT’ - does not have a fixed runtime representation. - Its type is: - NestedTuple ('Suc 'Zero) Addr# :: TYPE - (NestedTupleRep ('Suc 'Zero) 'AddrRep) - NB: GHC does not (yet) support rewriting in runtime representations. - Please comment on GHC ticket #13105 if this is causing you trouble. - <https://gitlab.haskell.org/ghc/ghc/-/issues/13105> - • In the first argument of ‘test2b’, namely - ‘(MkNT (# nullAddr#, (##) #))’ - In the expression: test2b (MkNT (# nullAddr#, (##) #)) - In an equation for ‘test2c’: - test2c _ = test2b (MkNT (# nullAddr#, (##) #)) diff --git a/testsuite/tests/rep-poly/T21239.hs b/testsuite/tests/rep-poly/T21239.hs new file mode 100644 index 0000000000..9ca1961114 --- /dev/null +++ b/testsuite/tests/rep-poly/T21239.hs @@ -0,0 +1,19 @@ + +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE UnboxedTuples #-} + +module T21239 where + +import GHC.Exts + +-- This test goes wrong if we don't properly decompose +-- when unifying ConcreteTv metavariables. + +atomicModifyMutVar# + :: MutVar# s a + -> (a -> b) + -> State# s + -> (# State# s, c #) +atomicModifyMutVar# mv f s = + case unsafeCoerce# (atomicModifyMutVar2# mv f s) of + (# s', _, ~(_, res) #) -> (# s', res #) diff --git a/testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.stderr b/testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.stderr index ba92961bcb..db08ac81d8 100644 --- a/testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.stderr +++ b/testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.stderr @@ -4,6 +4,10 @@ UnliftedNewtypesCoerceFail.hs:15:8: error: The first argument of ‘coerce’ does not have a fixed runtime representation. Its type is: - x :: TYPE rep + a0 :: TYPE c0 + Cannot unify ‘rep’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. • In the expression: coerce In an equation for ‘goof’: goof = coerce + • Relevant bindings include + goof :: x -> y (bound at UnliftedNewtypesCoerceFail.hs:15:1) diff --git a/testsuite/tests/rep-poly/UnliftedNewtypesLevityBinder.stderr b/testsuite/tests/rep-poly/UnliftedNewtypesLevityBinder.stderr index f4e7c62b46..41dbd44d3f 100644 --- a/testsuite/tests/rep-poly/UnliftedNewtypesLevityBinder.stderr +++ b/testsuite/tests/rep-poly/UnliftedNewtypesLevityBinder.stderr @@ -3,6 +3,10 @@ UnliftedNewtypesLevityBinder.hs:16:7: error: • The newtype constructor argument does not have a fixed runtime representation. Its type is: - a :: TYPE r + a0 :: TYPE c0 + Cannot unify ‘r’ with the type variable ‘c0’ + because it is not a concrete ‘RuntimeRep’. • In the expression: IdentC In an equation for ‘bad’: bad = IdentC + • Relevant bindings include + bad :: a -> Ident a (bound at UnliftedNewtypesLevityBinder.hs:16:1) diff --git a/testsuite/tests/rep-poly/all.T b/testsuite/tests/rep-poly/all.T index 140076e598..c7f4859272 100644 --- a/testsuite/tests/rep-poly/all.T +++ b/testsuite/tests/rep-poly/all.T @@ -27,10 +27,12 @@ test('T20330b', normal, compile, ['']) test('T20423', normal, compile_fail, ['']) test('T20423b', normal, compile_fail, ['']) test('T20426', normal, compile_fail, ['']) +test('T21239', normal, compile, ['']) test('LevPolyLet', normal, compile_fail, ['']) test('PandocArrowCmd', normal, compile, ['']) test('RepPolyApp', normal, compile_fail, ['']) +test('RepPolyArgument', normal, compile_fail, ['']) test('RepPolyArrowCmd', normal, compile_fail, ['']) test('RepPolyArrowFun', normal, compile_fail, ['']) test('RepPolyBackpack1', normal, backpack_compile_fail, ['']) @@ -48,6 +50,8 @@ test('RepPolyDoBody2', normal, compile_fail, ['']) test('RepPolyDoReturn', normal, compile, ['']) test('RepPolyFFI', normal, compile, ['']) test('RepPolyLambda', normal, compile_fail, ['']) +test('RepPolyInferPatBind', normal, compile_fail, ['']) +test('RepPolyInferPatSyn', normal, compile_fail, ['']) test('RepPolyLeftSection1', normal, compile, ['']) test('RepPolyLeftSection2', normal, compile_fail, ['']) test('RepPolyMagic', normal, compile_fail, ['']) @@ -83,12 +87,17 @@ test('UnliftedNewtypesLevityBinder', normal, compile_fail, ['']) ## The following tests require rewriting in RuntimeReps, ## ## i.e. PHASE 2 of the FixedRuntimeRep plan. ## ## ## +## These tests work! ## + ## +test('T13105', normal, compile, ['']) ## +test('T17536b', normal, compile, ['']) ## + ## +## These don't! ## ## For the moment, we check that we get the expected error message, ## ## as we want to reject these in the typechecker instead of getting ## ## a compiler crash. ## -test('T13105', normal, compile_fail, ['']) ## + ## test('T17021', normal, compile_fail, ['']) ## -test('T17536b', normal, compile_fail, ['']) ## test('T20363', normal, compile_fail, ['']) ## test('T20363_show_co', normal, compile_fail ## , ['-fprint-explicit-coercions']) ## diff --git a/testsuite/tests/typecheck/should_fail/T7869.stderr b/testsuite/tests/typecheck/should_fail/T7869.stderr index 15e9cc4658..c599b276d9 100644 --- a/testsuite/tests/typecheck/should_fail/T7869.stderr +++ b/testsuite/tests/typecheck/should_fail/T7869.stderr @@ -1,16 +1,18 @@ T7869.hs:3:12: error: - • Couldn't match type ‘b1’ with ‘b’ + • Couldn't match type ‘a1’ with ‘a’ Expected: [a1] -> b1 Actual: [a] -> b - ‘b1’ is a rigid type variable bound by + ‘a1’ 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 + ‘a’ is a rigid type variable bound by the inferred type of f :: [a] -> b at T7869.hs:3:1-27 • In the expression: f x In the expression: (\ x -> f x) :: [a] -> b In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b - • Relevant bindings include f :: [a] -> b (bound at T7869.hs:3:1) + • Relevant bindings include + x :: [a1] (bound at T7869.hs:3:7) + f :: [a] -> b (bound at T7869.hs:3:1) |