diff options
| author | sheaf <sam.derbyshire@gmail.com> | 2022-03-02 00:12:17 +0100 |
|---|---|---|
| committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2022-03-02 14:08:36 -0500 |
| commit | b27b2af3fab48e21aabcc9441967c4dd7a6a75ea (patch) | |
| tree | ca2919f3d98c35b6a22b08118ca32f4dae04a40d /compiler | |
| parent | aeea6bd588060108dea88996c19f48b9e50adad2 (diff) | |
| download | haskell-b27b2af3fab48e21aabcc9441967c4dd7a6a75ea.tar.gz | |
Introduce ConcreteTv metavariables
This patch introduces a new kind of metavariable, by adding the
constructor `ConcreteTv` to `MetaInfo`. A metavariable with
`ConcreteTv` `MetaInfo`, henceforth a concrete metavariable, can only
be unified with a type that is concrete (that is, a type that answers
`True` to `GHC.Core.Type.isConcrete`).
This solves the problem of dangling metavariables in `Concrete#`
constraints: instead of emitting `Concrete# ty`, which contains a
secret existential metavariable, we simply emit a primitive equality
constraint `ty ~# concrete_tv` where `concrete_tv` is a fresh concrete
metavariable.
This means we can avoid all the complexity of canonicalising
`Concrete#` constraints, as we can just re-use the existing machinery
for `~#`.
To finish things up, this patch then removes the `Concrete#` special
predicate, and instead introduces the special predicate `IsRefl#`
which enforces that a coercion is reflexive.
Such a constraint is needed because the canonicaliser is quite happy
to rewrite an equality constraint such as `ty ~# concrete_tv`, but
such a rewriting is not handled by the rest of the compiler currently,
as we need to make use of the resulting coercion, as outlined in the
FixedRuntimeRep plan.
The big upside of this approach (on top of simplifying the code)
is that we can now selectively implement PHASE 2 of FixedRuntimeRep,
by changing individual calls of `hasFixedRuntimeRep_MustBeRefl` to
`hasFixedRuntimeRep` and making use of the obtained coercion.
Diffstat (limited to 'compiler')
29 files changed, 696 insertions, 790 deletions
diff --git a/compiler/GHC/Builtin/Names.hs b/compiler/GHC/Builtin/Names.hs index 905fb6c8dc..9b1c9bad01 100644 --- a/compiler/GHC/Builtin/Names.hs +++ b/compiler/GHC/Builtin/Names.hs @@ -1835,7 +1835,7 @@ statePrimTyConKey, stableNamePrimTyConKey, stableNameTyConKey, funPtrTyConKey, tVarPrimTyConKey, eqPrimTyConKey, eqReprPrimTyConKey, eqPhantPrimTyConKey, compactPrimTyConKey, stackSnapshotPrimTyConKey, - concretePrimTyConKey :: Unique + isReflPrimTyConKey :: Unique statePrimTyConKey = mkPreludeTyConUnique 50 stableNamePrimTyConKey = mkPreludeTyConUnique 51 stableNameTyConKey = mkPreludeTyConUnique 52 @@ -1864,7 +1864,7 @@ funPtrTyConKey = mkPreludeTyConUnique 78 tVarPrimTyConKey = mkPreludeTyConUnique 79 compactPrimTyConKey = mkPreludeTyConUnique 80 stackSnapshotPrimTyConKey = mkPreludeTyConUnique 81 -concretePrimTyConKey = mkPreludeTyConUnique 82 +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 6570867898..f5ff25523a 100644 --- a/compiler/GHC/Builtin/Types/Prim.hs +++ b/compiler/GHC/Builtin/Types/Prim.hs @@ -100,7 +100,7 @@ module GHC.Builtin.Types.Prim( eqPhantPrimTyCon, -- ty1 ~P# ty2 (at role Phantom) equalityTyCon, - concretePrimTyCon, + isReflPrimTyCon, -- * SIMD #include "primop-vector-tys-exports.hs-incl" @@ -165,7 +165,7 @@ unexposedPrimTyCons = [ eqPrimTyCon , eqReprPrimTyCon , eqPhantPrimTyCon - , concretePrimTyCon + , isReflPrimTyCon ] -- | Primitive 'TyCon's that are defined in, and exported from, GHC.Prim. @@ -239,7 +239,7 @@ charPrimTyConName, intPrimTyConName, int8PrimTyConName, int16PrimTyConName, int3 weakPrimTyConName, threadIdPrimTyConName, eqPrimTyConName, eqReprPrimTyConName, eqPhantPrimTyConName, stackSnapshotPrimTyConName, - concretePrimTyConName :: Name + isReflPrimTyConName :: Name charPrimTyConName = mkPrimTc (fsLit "Char#") charPrimTyConKey charPrimTyCon intPrimTyConName = mkPrimTc (fsLit "Int#") intPrimTyConKey intPrimTyCon int8PrimTyConName = mkPrimTc (fsLit "Int8#") int8PrimTyConKey int8PrimTyCon @@ -277,7 +277,7 @@ stackSnapshotPrimTyConName = mkPrimTc (fsLit "StackSnapshot#") stackSnapshotP bcoPrimTyConName = mkPrimTc (fsLit "BCO") bcoPrimTyConKey bcoPrimTyCon weakPrimTyConName = mkPrimTc (fsLit "Weak#") weakPrimTyConKey weakPrimTyCon threadIdPrimTyConName = mkPrimTc (fsLit "ThreadId#") threadIdPrimTyConKey threadIdPrimTyCon -concretePrimTyConName = mkPrimTc (fsLit "Concrete#") concretePrimTyConKey concretePrimTyCon +isReflPrimTyConName = mkPrimTc (fsLit "IsRefl#") isReflPrimTyConKey isReflPrimTyCon {- ************************************************************************ @@ -1070,22 +1070,23 @@ equalityTyCon Phantom = eqPhantPrimTyCon {- ********************************************************************* * * - The Concrete mechanism + IsRefl# * * ********************************************************************* -} --- See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete. - --- type Concrete# :: forall k. k -> TYPE (TupleRep '[]) - -concretePrimTyCon :: TyCon -concretePrimTyCon = - mkPrimTyCon concretePrimTyConName binders res_kind roles +-- | 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 -> TYPE (TupleRep '[]) - binders = mkTemplateTyConBinders [liftedTypeKind] (\[k] -> [k]) + -- Kind :: forall k. k -> k-> TYPE (TupleRep '[]) + binders = mkTemplateTyConBinders [liftedTypeKind] (\[k] -> [k, k]) res_kind = unboxedTupleKind [] - roles = [Nominal, Nominal] + roles = [Nominal, Nominal, Nominal] {- ********************************************************************* * * diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs index 22f3c32201..a5f2f34221 100644 --- a/compiler/GHC/Core/Coercion.hs +++ b/compiler/GHC/Core/Coercion.hs @@ -20,7 +20,8 @@ module GHC.Core.Coercion ( Role(..), ltRole, -- ** Functions over coercions - coVarTypes, coVarKind, coVarKindsTypesRole, coVarRole, + coVarRType, coVarLType, coVarTypes, + coVarKind, coVarKindsTypesRole, coVarRole, coercionType, mkCoercionType, coercionKind, coercionLKind, coercionRKind,coercionKinds, coercionRole, coercionKindRole, diff --git a/compiler/GHC/Core/Predicate.hs b/compiler/GHC/Core/Predicate.hs index 3de166364b..c3994c2366 100644 --- a/compiler/GHC/Core/Predicate.hs +++ b/compiler/GHC/Core/Predicate.hs @@ -19,7 +19,7 @@ module GHC.Core.Predicate ( mkHeteroPrimEqPred, mkHeteroReprPrimEqPred, -- Special predicates - SpecialPred(..), specialPredTyCon, + SpecialPred(..), mkIsReflPrimPred, isIsReflPrimPred, -- Class predicates mkClassPred, isDictTy, @@ -34,12 +34,14 @@ module GHC.Core.Predicate ( -- Evidence variables DictId, isEvVar, isDictId + ) where 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 @@ -47,7 +49,7 @@ import GHC.Core.Coercion import GHC.Core.Multiplicity ( scaledThing ) import GHC.Builtin.Names -import GHC.Builtin.Types.Prim ( concretePrimTyCon ) +import GHC.Builtin.Types.Prim ( isReflPrimTyCon ) import GHC.Utils.Outputable import GHC.Utils.Misc @@ -77,13 +79,8 @@ data Pred -- | A special predicate, used internally in GHC. -- - -- The meaning of the type argument is dictated by the 'SpecialPred' - -- specified in the first agument; see the documentation of 'SpecialPred' for more info. - -- - -- Example: @Concrete# rep@, used for representation-polymorphism checks - -- within GHC. See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete. - -- (This is the only example currently. More to come: see GHC ticket #20000.) - | SpecialPred SpecialPred Type + -- See #20000. + | SpecialPred SpecialPred -- NB: There is no TuplePred case -- Tuple predicates like (Eq a, Ord b) are just treated @@ -96,9 +93,9 @@ 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, ty]) - | tc `hasKey` concretePrimTyConKey - -> SpecialPred ConcretePrimPred ty + Just (tc, [_ki, lhs, rhs]) + | tc `hasKey` isReflPrimTyConKey + -> SpecialPred (IsReflPrimPred lhs rhs) Just (tc, tys) | Just clas <- tyConClass_maybe tc @@ -203,25 +200,19 @@ predTypeEqRel ty -- (such as `KnownNat`, `Typeable`, `Coercible`, ...), as special predicates -- can't be expressed as typeclasses, as they hold evidence of a different kind. data SpecialPred - -- | A @Concrete#@ predicate, to check for representation polymorphism. - -- - -- When the first argument to the 'SpecialPred' data constructor of 'Pred' - -- is 'ConcretePrimPred', the second argument is the type we are inspecting - -- to decide whether it is concrete. That is, it refers to the - -- second argument of the 'Concrete#' 'TyCon'. Recall that this 'TyCon' has kind - -- - -- > forall k. k -> TupleRep '[] - -- - -- See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete for further details. - = ConcretePrimPred - deriving stock Eq + -- | 'IsRefl#'. + = IsReflPrimPred Type Type instance Outputable SpecialPred where - ppr ConcretePrimPred = text "Concrete#" + ppr (IsReflPrimPred l r) = + text "IsRefl#" <+> pprParendType l <+> pprParendType r + +mkIsReflPrimPred :: Type -> Type -> PredType +mkIsReflPrimPred lhs rhs = mkTyConApp isReflPrimTyCon [typeKind lhs, lhs, rhs] --- | Obtain the 'TyCon' associated with a special predicate. -specialPredTyCon :: SpecialPred -> TyCon -specialPredTyCon ConcretePrimPred = concretePrimTyCon +isIsReflPrimPred :: Pred -> Bool +isIsReflPrimPred (SpecialPred (IsReflPrimPred {})) = True +isIsReflPrimPred _ = False {------------------------------------------- Predicates on PredType diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs index df8bf09fa0..cc1b712eec 100644 --- a/compiler/GHC/Core/TyCon.hs +++ b/compiler/GHC/Core/TyCon.hs @@ -2495,8 +2495,8 @@ isConcreteTyConFlavour = \case SumFlavour -> True DataTypeFlavour -> True NewtypeFlavour -> True - AbstractTypeFlavour -> True -- See (3) in Note [Solving Concrete# constraints] in GHC.Tc.Utils.Concrete - DataFamilyFlavour {} -> False -- See + AbstractTypeFlavour -> True -- See Note [Concrete types] in GHC.Tc.Utils.Concrete + DataFamilyFlavour {} -> False OpenTypeFamilyFlavour {} -> False ClosedTypeFamilyFlavour -> False TypeSynonymFlavour -> False diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs index 1b5a21b733..e05acf1881 100644 --- a/compiler/GHC/Core/Type.hs +++ b/compiler/GHC/Core/Type.hs @@ -279,6 +279,7 @@ import {-# SOURCE #-} GHC.Core.Coercion , isReflexiveCo, seqCo , topNormaliseNewType_maybe ) +import {-# SOURCE #-} GHC.Tc.Utils.TcType ( isConcreteTyVar ) -- others import GHC.Utils.Misc @@ -3549,11 +3550,8 @@ distinct uniques, they are treated as equal at all times except during type inference. -} --- | Tests whether the given kind is a constructor tree --- (that is, constructors at every node). --- --- E.g. @False@ for @TYPE k@, @TYPE (F Int)@ --- @True@ for @TYPE 'LiftedRep@ +-- | Checks that a kind of the form 'Type', 'Constraint' +-- or @'TYPE r@ is concrete. See 'isConcrete'. -- -- __Precondition:__ The type has kind @('TYPE' blah)@. isFixedRuntimeRepKind :: HasDebugCallStack => Kind -> Bool @@ -3564,19 +3562,24 @@ isFixedRuntimeRepKind k where _is_type = classifiesTypeWithValues k --- | Tests whether the given type is a constructor tree, --- consisting only of concrete type constructors and applications. +-- | Tests whether the given type is concrete, i.e. it +-- whether it consists only of concrete type constructors, +-- concrete type variables, and applications. +-- +-- See Note [Concrete types] in GHC.Tc.Utils.Concrete. isConcrete :: Type -> Bool isConcrete = go where go ty | Just ty' <- coreView ty = go ty' - go TyVarTy{} = False - go AppTy{} = False -- it can't be a TyConApp + go (TyVarTy tv) = isConcreteTyVar tv + go (AppTy ty1 ty2) = go ty1 && go ty2 go (TyConApp tc tys) | 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 LitTy{} = True go CastTy{} = False go CoercionTy{} = False diff --git a/compiler/GHC/Data/Bag.hs b/compiler/GHC/Data/Bag.hs index a5f4a48375..0dcdef55a5 100644 --- a/compiler/GHC/Data/Bag.hs +++ b/compiler/GHC/Data/Bag.hs @@ -146,7 +146,7 @@ catBagMaybes bs = foldr add emptyBag bs add Nothing rs = rs add (Just x) rs = x `consBag` rs -partitionBag :: (a -> Bool) -> Bag a -> (Bag a {- Satisfy predictate -}, +partitionBag :: (a -> Bool) -> Bag a -> (Bag a {- Satisfy predicate -}, Bag a {- Don't -}) partitionBag _ EmptyBag = (EmptyBag, EmptyBag) partitionBag pred b@(UnitBag val) diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs index 596271b065..1262dac062 100644 --- a/compiler/GHC/Tc/Errors.hs +++ b/compiler/GHC/Tc/Errors.hs @@ -82,7 +82,6 @@ import qualified GHC.Data.Strict as Strict import Control.Monad ( unless, when, foldM, forM_ ) import Data.Foldable ( toList ) -import Data.Functor ( (<&>) ) import Data.Function ( on ) import Data.List ( partition, sort, sortBy ) import Data.List.NonEmpty ( NonEmpty(..), (<|) ) @@ -638,11 +637,23 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics is_user_type_error item _ = isUserTypeError (errorItemPred item) - is_homo_equality _ (EqPred _ ty1 ty2) = tcTypeKind ty1 `tcEqType` tcTypeKind ty2 - is_homo_equality _ _ = False + is_homo_equality item (EqPred _ ty1 ty2) + | FixedRuntimeRepOrigin {} <- errorItemOrigin item + -- Constraints with FixedRuntimeRep origin must be reported using mkFRRErr. + = False + | otherwise + = tcTypeKind ty1 `tcEqType` tcTypeKind ty2 + is_homo_equality _ _ + = False - is_equality _ (EqPred {}) = True - is_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_dict _ (ClassPred {}) = True is_dict _ _ = False @@ -650,7 +661,7 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics is_ip _ (ClassPred cls _) = isIPClass cls is_ip _ _ = False - is_FRR item (SpecialPred ConcretePrimPred _) + is_FRR item _ | FixedRuntimeRepOrigin {} <- errorItemOrigin item = True is_FRR _ _ @@ -1040,7 +1051,9 @@ 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) }} + ; fillCoercionHole hole (mkTcCoVarCo co_var) } + NoDest + -> return () } addDeferredBinding _ _ _ = return () -- Do not set any evidence for Given mkErrorTerm :: SolverReportErrCtxt -> CtLoc -> Type -- of the error term @@ -1426,32 +1439,39 @@ mkIPErr ctxt items ---------------- --- | Create a user-facing error message for unsolved @'Concrete#' ki@ --- Wanted constraints arising from representation-polymorphism checks. +-- | Report a representation-polymorphism error to the user: `ty` should have +-- a fixed runtime representation, but doesn't. -- -- See Note [Reporting representation-polymorphism errors] in GHC.Tc.Types.Origin. mkFRRErr :: SolverReportErrCtxt -> [ErrorItem] -> TcM SolverReport mkFRRErr ctxt items - = do { -- Zonking/tidying. - ; origs <- - -- Zonk/tidy the 'CtOrigin's. + = 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. - (nubOrdBy (nonDetCmpType `on` (snd . frr_orig_and_type)) . snd) - -- Obtain all the errors we want to report (constraints with FixedRuntimeRep origin), - -- with the corresponding types: - -- ty1 :: TYPE rep1, ty2 :: TYPE rep2, ... - ; let origs_and_tys = map frr_orig_and_type origs - - ; return $ important ctxt $ FixedRuntimeRepError origs_and_tys } + -- 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) + ; return $ important ctxt $ FixedRuntimeRepError frr_infos } where - frr_orig_and_type :: CtOrigin -> (FRROrigin, Type) - frr_orig_and_type (FixedRuntimeRepOrigin ty frr_orig) = (frr_orig, ty) - frr_orig_and_type orig - = pprPanic "mkFRRErr: not a FixedRuntimeRep origin" - (text "origin =" <+> ppr orig) + 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 ] {- Note [Constraints include ...] diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs index 2e535338e6..84eea92b01 100644 --- a/compiler/GHC/Tc/Errors/Ppr.hs +++ b/compiler/GHC/Tc/Errors/Ppr.hs @@ -1722,21 +1722,44 @@ pprTcSolverReportMsg ctxt maybe_num_args_msg = num_args_msg `orElse` empty count_args ty = count isVisibleBinder $ fst $ splitPiTys ty -pprTcSolverReportMsg _ (FixedRuntimeRepError origs_and_tys) = - let +pprTcSolverReportMsg _ (FixedRuntimeRepError frr_infos) = + vcat (map make_msg frr_infos) $$ mustBeRefl_msg + where -- Assemble the error message: pair up each origin with the corresponding type, e.g. -- • FixedRuntimeRep origin msg 1 ... -- a :: TYPE r1 -- • FixedRuntimeRep origin msg 2 ... -- b :: TYPE r2 - combine_origin_ty :: FRROrigin -> Type -> SDoc - combine_origin_ty frr_orig ty = - -- Add bullet points if there is more than one error. - (if length origs_and_tys > 1 then (bullet <+>) else id) $ - vcat [pprFRROrigin frr_orig <> colon - ,nest 2 $ ppr ty <+> dcolon <+> pprWithTYPE (typeKind ty)] - in - vcat $ map (uncurry combine_origin_ty) origs_and_tys + 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." ] + , 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 + pprTcSolverReportMsg _ (SkolemEscape item implic esc_skols) = let esc_doc = sep [ text "because" <+> what <+> text "variable" <> plural esc_skols diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs index d6004c7b96..ca835a4ae9 100644 --- a/compiler/GHC/Tc/Errors/Types.hs +++ b/compiler/GHC/Tc/Errors/Types.hs @@ -46,6 +46,7 @@ module GHC.Tc.Errors.Types ( , SolverReportErrCtxt(..) , getUserGivens, discardProvCtxtGivens , TcSolverReportMsg(..), TcSolverReportInfo(..) + , FixedRuntimeRepErrorInfo(..) , CND_Extra(..) , mkTcReportWithInfo , FitsMbSuppressed(..) @@ -2239,7 +2240,7 @@ data TcSolverReportMsg -- i.e. an unsolved `Concrete# ty` constraint. -- -- See 'FRROrigin' for more information. - | FixedRuntimeRepError [(FRROrigin, Type)] + | FixedRuntimeRepError [FixedRuntimeRepErrorInfo] -- | A skolem type variable escapes its scope. -- @@ -2346,6 +2347,20 @@ 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 diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs index 659e4f64d5..a6e505db96 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 ) +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_MustBeRefl ) import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst_maybe ) import GHC.Tc.Gen.HsType import GHC.Tc.Utils.TcMType @@ -587,7 +587,7 @@ hasFixedRuntimeRep_remainingValArgs applied_args app_res_rho = \case InvisArg -> go i_visval (i_val + 1) tys VisArg -> do - _concrete_ev <- hasFixedRuntimeRep (mk_frr_orig i_visval) arg_ty + hasFixedRuntimeRep_MustBeRefl (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 @@ -678,10 +678,10 @@ tcEValArg :: AppCtxt -> EValArg 'TcpInst -> TcSigmaType -> TcM (LHsExpr GhcTc) tcEValArg ctxt (ValArg larg@(L arg_loc arg)) exp_arg_sigma = addArgCtxt ctxt larg $ do { arg' <- tcPolyExpr arg (mkCheckExpType exp_arg_sigma) - ; _concrete_ev <- hasFixedRuntimeRep (FRRApp arg) exp_arg_sigma + ; hasFixedRuntimeRep_MustBeRefl (FRRApp arg') exp_arg_sigma ; return (L arg_loc arg') } -tcEValArg ctxt (ValArgQL { va_expr = larg@(L arg_loc arg) +tcEValArg ctxt (ValArgQL { va_expr = larg@(L arg_loc _) , va_fun = (inner_fun, fun_ctxt) , va_args = inner_args , va_ty = app_res_rho }) exp_arg_sigma @@ -689,10 +689,10 @@ tcEValArg ctxt (ValArgQL { va_expr = larg@(L arg_loc arg) do { traceTc "tcEValArgQL {" (vcat [ ppr inner_fun <+> ppr inner_args ]) ; tc_args <- tcValArgs True inner_args ; co <- unifyType Nothing app_res_rho exp_arg_sigma - ; _concrete_ev <- hasFixedRuntimeRep (FRRApp arg) exp_arg_sigma - ; traceTc "tcEValArg }" empty - ; return (L arg_loc $ mkHsWrapCo co $ - rebuildHsApps inner_fun fun_ctxt tc_args) } + ; let arg' = mkHsWrapCo co $ rebuildHsApps inner_fun fun_ctxt tc_args + ; hasFixedRuntimeRep_MustBeRefl (FRRApp arg') exp_arg_sigma + ; traceTc "tcEValArgQL }" empty + ; return (L arg_loc arg') } {- ********************************************************************* * * diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs index 0f0abcd71d..dd3d19dfab 100644 --- a/compiler/GHC/Tc/Gen/Arrow.hs +++ b/compiler/GHC/Tc/Gen/Arrow.hs @@ -22,7 +22,7 @@ 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 ) +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_MustBeRefl ) import GHC.Tc.Utils.TcType import GHC.Tc.Utils.TcMType import GHC.Tc.Gen.Bind @@ -146,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 - ; _concrete_ev <- hasFixedRuntimeRep (FRRArrow $ ArrowCmdResTy cmd) res_ty + ; hasFixedRuntimeRep_MustBeRefl (FRRArrow $ ArrowCmdResTy cmd) res_ty ; return (L loc cmd') } tc_cmd :: CmdEnv -> HsCmd GhcRn -> CmdType -> TcM (HsCmd GhcTc) @@ -223,9 +223,9 @@ tc_cmd env cmd@(HsCmdArrApp _ fun arg ho_app lr) (_, res_ty) ; arg' <- tcCheckMonoExpr arg arg_ty - ; _concrete_ev <- hasFixedRuntimeRep - (FRRArrow $ ArrowCmdArrApp (unLoc fun) (unLoc arg) ho_app) - fun_ty + ; hasFixedRuntimeRep_MustBeRefl + (FRRArrow $ ArrowCmdArrApp (unLoc fun) (unLoc arg) ho_app) + fun_ty ; return (HsCmdArrApp fun_ty fun' arg' ho_app lr) } where @@ -251,9 +251,9 @@ 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 - ; _concrete_ev <- hasFixedRuntimeRep - (FRRArrow $ ArrowCmdApp (unLoc fun) (unLoc arg)) - arg_ty + ; hasFixedRuntimeRep_MustBeRefl + (FRRArrow $ ArrowCmdApp (unLoc fun) (unLoc arg)) + arg_ty ; return (HsCmdApp x fun' arg') } ------------------------------------------- @@ -283,12 +283,11 @@ tc_cmd env , m_grhss = grhss' }) arg_tys = map (unrestricted . hsLPatType) pats' - ; _concrete_evs <- - zipWithM - (\ (Scaled _ arg_ty) i -> - hasFixedRuntimeRep (FRRArrow $ ArrowCmdLam i) arg_ty) - arg_tys - [1..] + ; zipWithM_ + (\ (Scaled _ arg_ty) i -> + hasFixedRuntimeRep_MustBeRefl (FRRArrow $ ArrowCmdLam i) arg_ty) + arg_tys + [1..] ; let cmd' = HsCmdLam x (MG { mg_alts = L l [match'] diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs index 193292c797..404a5a55d2 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 ) +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_MustBeRefl ) import GHC.Tc.Utils.Monad import GHC.Tc.Types.Origin import GHC.Tc.Utils.Env @@ -508,10 +508,9 @@ tcPolyBinds sig_fn prag_fn rec_group rec_tc closed bind_list InferGen mn -> tcPolyInfer rec_tc prag_fn sig_fn mn bind_list CheckGen lbind sig -> tcPolyCheck prag_fn sig lbind - ; _concrete_evs <- - mapM (\ poly_id -> - hasFixedRuntimeRep (FRRBinder $ idName poly_id) (idType poly_id)) - poly_ids + ; mapM_ (\ poly_id -> + hasFixedRuntimeRep_MustBeRefl (FRRBinder $ idName poly_id) (idType poly_id)) + poly_ids ; traceTc "} End of bindings for" (vcat [ ppr binder_names, ppr rec_group , vcat [ppr id <+> ppr (idType id) | id <- poly_ids] diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs index 46775235df..189eb989c5 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, mkWpFun ) +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_MustBeRefl, mkWpFun ) import GHC.Tc.Utils.Instantiate import GHC.Tc.Gen.App import GHC.Tc.Gen.Head @@ -353,7 +353,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. - ; _concrete_ev <- hasFixedRuntimeRep FRRUnboxedSum res_ty + ; hasFixedRuntimeRep_MustBeRefl FRRUnboxedSum res_ty ; return $ mkHsWrapCo coi (ExplicitSum arg_tys' alt arity expr' ) } @@ -954,11 +954,11 @@ tcTupArgs args tys go :: Int -> HsTupArg GhcRn -> TcType -> TcM (HsTupArg GhcTc) go i (Missing {}) arg_ty = do { mult <- newFlexiTyVarTy multiplicityTy - ; _concrete_ev <- hasFixedRuntimeRep (FRRTupleSection i) arg_ty + ; hasFixedRuntimeRep_MustBeRefl (FRRTupleSection i) arg_ty ; return (Missing (Scaled mult arg_ty)) } go i (Present x expr) arg_ty = do { expr' <- tcCheckPolyExpr expr arg_ty - ; _concrete_ev <- hasFixedRuntimeRep (FRRTupleArg i) arg_ty + ; hasFixedRuntimeRep_MustBeRefl (FRRTupleArg i) arg_ty ; return (Present x expr') } --------------------------- @@ -1386,9 +1386,8 @@ 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 - ; _concrete_ev <- - hasFixedRuntimeRep (FRRRecordUpdate (unLoc lbl) (unLoc rhs)) - field_ty + ; hasFixedRuntimeRep_MustBeRefl (FRRRecordUpdate (unLoc lbl) (unLoc rhs')) + field_ty ; let field_id = mkUserLocal (nameOccName sel_name) (nameUnique sel_name) Many field_ty (locA loc) diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs index 1b2ebf797a..a4f24dbb1b 100644 --- a/compiler/GHC/Tc/Gen/Match.hs +++ b/compiler/GHC/Tc/Gen/Match.hs @@ -49,7 +49,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 ) +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_MustBeRefl ) import GHC.Tc.Utils.Unify import GHC.Tc.Types.Origin import GHC.Tc.Types.Evidence @@ -227,10 +227,10 @@ tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches = do { tcEmitBindingUsage bottomUE ; pat_tys <- mapM scaledExpTypeToType pat_tys ; rhs_ty <- expTypeToType rhs_ty - ; _concrete_evs <- zipWithM - (\ i (Scaled _ pat_ty) -> - hasFixedRuntimeRep (FRRMatch (mc_what ctxt) i) pat_ty) - [1..] pat_tys + ; zipWithM_ + (\ i (Scaled _ pat_ty) -> + hasFixedRuntimeRep_MustBeRefl (FRRMatch (mc_what ctxt) i) pat_ty) + [1..] pat_tys ; return (MG { mg_alts = L l [] , mg_ext = MatchGroupTc pat_tys rhs_ty , mg_origin = origin }) } @@ -241,10 +241,10 @@ tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches ; tcEmitBindingUsage $ supUEs usages ; pat_tys <- mapM readScaledExpType pat_tys ; rhs_ty <- readExpType rhs_ty - ; _concrete_evs <- zipWithM - (\ i (Scaled _ pat_ty) -> - hasFixedRuntimeRep (FRRMatch (mc_what ctxt) i) pat_ty) - [1..] pat_tys + ; zipWithM_ + (\ i (Scaled _ pat_ty) -> + hasFixedRuntimeRep_MustBeRefl (FRRMatch (mc_what ctxt) i) pat_ty) + [1..] pat_tys ; return (MG { mg_alts = L l matches' , mg_ext = MatchGroupTc pat_tys rhs_ty , mg_origin = origin }) } @@ -440,7 +440,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 - ; _concrete_ev <- hasFixedRuntimeRep FRRBindStmtGuard rhs_ty + ; hasFixedRuntimeRep_MustBeRefl FRRBindStmtGuard rhs_ty ; (pat', thing) <- tcCheckPat_O (StmtCtxt ctxt) (lexprCtOrigin rhs) pat (unrestricted rhs_ty) $ thing_inside res_ty @@ -602,7 +602,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) } - ; _concrete_ev <- hasFixedRuntimeRep (FRRBindStmt MonadComprehension) rhs_ty + ; hasFixedRuntimeRep_MustBeRefl (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 -> @@ -638,9 +638,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') } - ; _evTerm1 <- hasFixedRuntimeRep FRRBodyStmtGuard test_ty - ; _evTerm2 <- hasFixedRuntimeRep (FRRBodyStmt MonadComprehension 1) rhs_ty - ; _evTerm3 <- hasFixedRuntimeRep (FRRBodyStmt MonadComprehension 2) new_res_ty + ; hasFixedRuntimeRep_MustBeRefl FRRBodyStmtGuard test_ty + ; hasFixedRuntimeRep_MustBeRefl (FRRBodyStmt MonadComprehension 1) rhs_ty + ; hasFixedRuntimeRep_MustBeRefl (FRRBodyStmt MonadComprehension 2) new_res_ty ; return (BodyStmt rhs_ty rhs' then_op' guard_op', thing) } @@ -876,7 +876,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) } - ; _concrete_ev <- hasFixedRuntimeRep (FRRBindStmt DoNotation) rhs_ty + ; hasFixedRuntimeRep_MustBeRefl (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 -> @@ -910,8 +910,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) } - ; _evTerm1 <- hasFixedRuntimeRep (FRRBodyStmt DoNotation 1) rhs_ty - ; _evTerm2 <- hasFixedRuntimeRep (FRRBodyStmt DoNotation 2) new_res_ty + ; hasFixedRuntimeRep_MustBeRefl (FRRBodyStmt DoNotation 1) rhs_ty + ; hasFixedRuntimeRep_MustBeRefl (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/Rule.hs b/compiler/GHC/Tc/Gen/Rule.hs index 0d2c5bcc8b..912068a0cb 100644 --- a/compiler/GHC/Tc/Gen/Rule.hs +++ b/compiler/GHC/Tc/Gen/Rule.hs @@ -397,24 +397,21 @@ simplifyRule :: RuleName -- NB: This consumes all simple constraints on the LHS, but not -- any LHS implication constraints. simplifyRule name tc_lvl lhs_wanted rhs_wanted - = do { setTcLevel tc_lvl $ - do { -- Note [The SimplifyRule Plan] step 1 - -- First solve the LHS and *then* solve the RHS - -- Crucially, this performs unifications - -- Why clone? See Note [Simplify cloned constraints] - -- This must be in the bumped TcLevel because cloneWC creates - -- metavariables for Concrete# constraints. See Note [The Concrete mechanism] - -- in GHC.Tc.Utils.Concrete - ; lhs_clone <- cloneWC lhs_wanted - ; rhs_clone <- cloneWC rhs_wanted - ; discardResult $ - runTcS $ - do { - ; _ <- solveWanteds lhs_clone - ; _ <- solveWanteds rhs_clone - -- Why do them separately? - -- See Note [Solve order for RULES] - ; return () }} + = do { + -- Note [The SimplifyRule Plan] step 1 + -- First solve the LHS and *then* solve the RHS + -- Crucially, this performs unifications + -- Why clone? See Note [Simplify cloned constraints] + ; lhs_clone <- cloneWC lhs_wanted + ; rhs_clone <- cloneWC rhs_wanted + ; setTcLevel tc_lvl $ + discardResult $ + runTcS $ + do { _ <- solveWanteds lhs_clone + ; _ <- solveWanteds rhs_clone + -- Why do them separately? + -- See Note [Solve order for RULES] + ; return () } -- Note [The SimplifyRule Plan] step 2 ; lhs_wanted <- zonkWC lhs_wanted @@ -443,6 +440,7 @@ 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) @@ -489,10 +487,8 @@ getRuleQuantCts wc | not (ok_eq t1 t2) -> False -- Note [RULE quantification over equalities] SpecialPred {} - -- RULES must never quantify over special predicates, as that - -- would leak internal GHC implementation details to the user. - -- - -- Tests (for Concrete# predicates): RepPolyRule{1,2,3}. + -- Rules should not quantify over special predicates, as these + -- are a GHC implementation detail. -> False _ -> tyCoVarsOfCt ct `disjointVarSet` skol_tvs diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index 78f0f18fb7..7d0c10f924 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -1193,7 +1193,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds -------------------- emitResidualConstraints :: TcLevel -> EvBindsVar -> [(Name, TcTauType)] - -> VarSet -> [TcTyVar] -> [EvVar] + -> CoVarSet -> [TcTyVar] -> [EvVar] -> WantedConstraints -> TcM () -- Emit the remaining constraints from the RHS. emitResidualConstraints rhs_tclvl ev_binds_var @@ -1204,7 +1204,11 @@ emitResidualConstraints rhs_tclvl ev_binds_var | otherwise = do { wanted_simple <- TcM.zonkSimples (wc_simple wanteds) ; let (outer_simple, inner_simple) = partitionBag is_mono wanted_simple - is_mono ct = isWantedCt ct && ctEvId ct `elemVarSet` co_vars + is_mono ct + | Just ct_ev_id <- wantedEvId_maybe ct + = ct_ev_id `elemVarSet` co_vars + | otherwise + = False -- Reason for the partition: -- see Note [Emitting the residual implication in simplifyInfer] @@ -1561,7 +1565,7 @@ decideQuantification -> [PredType] -- Candidate theta; already zonked -> TcM ( [TcTyVar] -- Quantify over these (skolems) , [PredType] -- and this context (fully zonked) - , VarSet) + , CoVarSet) -- See Note [Deciding quantification] decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates = do { -- Step 1: find the mono_tvs @@ -1810,11 +1814,9 @@ defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates simplify_cand [] = return [] -- see Note [Unconditionally resimplify constraints when quantifying] simplify_cand candidates - = do { WC { wc_simple = simples } <- setTcLevel rhs_tclvl $ - do { wanteds <- newWanteds DefaultOrigin candidates - -- build wanteds at bumped level because newConcreteHole - -- whips up fresh metavariables - ; simplifyWantedsTcM wanteds } + = do { clone_wanteds <- newWanteds DefaultOrigin candidates + ; WC { wc_simple = simples } <- setTcLevel rhs_tclvl $ + simplifyWantedsTcM clone_wanteds -- Discard evidence; simples is fully zonked ; let new_candidates = ctsPreds simples diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index f38c5de866..e1baaba7c0 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -15,7 +15,6 @@ import GHC.Prelude import GHC.Tc.Types.Constraint import GHC.Core.Predicate import GHC.Tc.Types.Origin -import GHC.Tc.Utils.Concrete ( newConcretePrimWanted ) import GHC.Tc.Utils.Unify import GHC.Tc.Utils.TcType import GHC.Core.Type @@ -43,7 +42,6 @@ import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Utils.Panic.Plain import GHC.Builtin.Types ( anyTypeOfKind ) -import GHC.Builtin.Types.Prim ( concretePrimTyCon ) import GHC.Types.Name.Set import GHC.Types.Name.Reader import GHC.Hs.Type( HsIPName(..) ) @@ -62,7 +60,6 @@ import GHC.Types.Basic import qualified Data.Semigroup as S import Data.Bifunctor ( bimap ) import Data.Foldable ( traverse_ ) -import GHC.Tc.Utils.Monad (setTcLevel) {- ************************************************************************ @@ -104,9 +101,6 @@ canonicalize (CNonCanonical { cc_ev = ev }) canonicalize (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc })) = canForAll ev pend_sc -canonicalize (CSpecialCan { cc_ev = ev, cc_special_pred = special_pred, cc_xi = xi }) - = canSpecial ev special_pred xi - canonicalize (CIrredCan { cc_ev = ev }) = canNC ev -- Instead of rewriting the evidence before classifying, it's possible we @@ -130,6 +124,9 @@ 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 @@ -141,8 +138,9 @@ canNC ev = canIrred ev ForAllPred tvs th p -> do traceTcS "canEvNC:forall" (ppr pred) canForAllNC ev tvs th p - SpecialPred tc ty -> do traceTcS "canEvNC:special" (ppr pred) - canSpecial ev tc ty + SpecialPred spec -> do traceTcS "canEvNC:special" (ppr pred) + canSpecial ev spec + where pred = ctEvPred ev @@ -750,10 +748,9 @@ canIrred ev -- in with a polytype. This is #18987. do traceTcS "canEvNC:forall" (ppr pred) canForAllNC ev tvs th p - SpecialPred tc tys -> -- IrredPreds have kind Constraint, so cannot + SpecialPred {} -> -- IrredPreds have kind Constraint, so cannot -- become SpecialPreds - pprPanic "canIrred: SpecialPred" - (ppr ev $$ ppr tc $$ ppr tys) + pprPanic "canIrred: SpecialPred" (ppr ev) IrredPred {} -> continueWith $ mkIrredCt IrredShapeReason new_ev } } @@ -932,213 +929,39 @@ we'll find a match in the InstEnv. ********************************************************************* -} -- | Canonicalise a 'SpecialPred' constraint. -canSpecial :: CtEvidence -> SpecialPred -> TcType -> TcS (StopOrContinue Ct) -canSpecial ev special_pred ty - = do { -- Special constraints should never appear in Givens. - ; massertPpr (not $ isGivenOrigin $ ctEvOrigin ev) - (text "canSpecial: Given Special constraint" $$ ppr ev) - ; case special_pred of - { ConcretePrimPred -> canConcretePrim ev ty } } - -{- Note [Canonical Concrete# constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -A 'Concrete#' constraint can be decomposed precisely when -it is an application, possibly nullary, of a concrete 'TyCon'. - -A canonical 'Concrete#' constraint is one that cannot be decomposed. - -To illustrate, when we come across a constraint of the form `Concrete# (f a_1 ... a_n)`, -to canonicalise it, we decompose it into the collection of constraints -`Concrete# a_1`, ..., `Concrete# a_n`, whenever `f` is a concrete type constructor -(that is, it is not a type variable, nor a type-family, nor an abstract 'TyCon' -as declared in a Backpack signature file). - -Writing NC for a non-canonical constraint and C for a canonical one, -here are some examples: - - (1) - NC: Concrete# IntRep - ==> nullary decomposition, by observing that `IntRep = TyConApp intRepTyCon []` - - (2) - NC: Concrete# (TYPE (TupleRep '[Rep, rr])) -- where 'Rep' is an abstract type and 'rr' is a type variable - ==> decompose once, noting that 'TYPE' is a concrete 'TyCon' - NC: Concrete# (TupleRep '[Rep, rr]) - ==> decompose again in the same way but with 'TupleRep' - NC: Concrete# ((:) @RuntimeRep Rep ((:) @RuntimeRep rr [])) - ==> handle (:) and its type-level argument 'RuntimeRep' (which is concrete) - C: Concrete# Rep, NC: Concrete# ((:) @RuntimeRep rr [])) - ==> the second constraint can be decomposed again; 'RuntimeRep' and '[]' are concrete, so we get - C: Concrete# Rep, C: Concrete# rr - -Note [Solving Concrete constraints requires simplifyArgsWorker] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We have - [W] co :: Concrete# [LiftedRep, IntRep] -and wish to canonicalise it so that we can solve it. Of course, that's really - [W] co :: Concrete# ((:) @RuntimeRep LiftedRep ((:) @RuntimeRep IntRep ('[] @RuntimeRep))) - -We can decompose to - [W] co1 :: Concrete# RuntimeRep - [W] co2 :: Concrete# LiftedRep - [W] co3 :: Concrete# ((:) @RuntimeRep IntRep ('[] @RuntimeRep)) - -Recall (Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete) that the evidence for -a Concrete# ty constraint is a coercion of type ty ~# alpha, where we require a concrete -type (one that responds True to GHC.Core.Type.isConcrete) to fill in alpha when solving -the constraint. Accordingly, when we create these new Concrete# constraints, we create -new metavariables alpha1 :: Type, alpha2 :: RuntimeRep, alpha3 :: [RuntimeRep], with: - - co1 :: RuntimeRep ~# alpha1 - co2 :: LiftedRep ~# alpha2 - co3 :: '[IntRep] ~# alpha3 - -and we already have - - co :: [LiftedRep, IntRep] ~# alpha0 - -We are now solving co. What do we fill in alpha0 with? The naive answer is to say - - alpha0 := (:) alpha1 alpha2 alpha3 - -but this would be ill-kinded! The first problem is that `(:) alpha1` expects its next -argument to have kind alpha1. (The next argument -- alpha3 -- is problematic, too.) The -second problem is that alpha0 :: [RuntimeRep], but the right-hand side above has kind -[alpha1]. Happily, we have a solution close to hand: simplifyArgsWorker, which deals -with precisely this scenario, of replacing all the arguments to a function (in this case, (:)), -with new arguments but making sure the kinds line up. All we have to do is bundle the information -we have in a form simplifyArgsWorker likes, and then do the reverse from its result. - --} - --- | Canonicalise a 'Concrete#' 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 [Canonical Concrete# constraints] for details. -canConcretePrim :: CtEvidence -> TcType -> TcS (StopOrContinue Ct) -canConcretePrim ev ty - = do { - -- As per Note [The Concrete mechanism] in GHC.Tc.Instance.Class, - -- in PHASE 1, we don't allow a 'Concrete#' constraint to be rewritten. - -- We still need to zonk, otherwise we can end up stuck with a constraint - -- such as `Concrete# rep` for a unification variable `rep`, - -- which we can't make progress on. - ; ty <- zonkTcType ty - ; traceTcS "canConcretePrim" $ - vcat [text "ev =" <+> ppr ev, text "ty =" <+> ppr ty] - - ; decomposeConcretePrim ev ty } - --- | Try to decompose a 'Concrete#' constraint: --- --- - calls 'canDecomposableConcretePrim' if the constraint can be decomposed; --- - calls 'canNonDecomposableConcretePrim' otherwise. -decomposeConcretePrim :: CtEvidence -> Type -> TcS (StopOrContinue Ct) -decomposeConcretePrim ev ty - -- Handle applications of concrete 'TyCon's. - -- See examples (1,2) in Note [Canonical Concrete# constraints]. - | (f,args) <- tcSplitAppTys ty - , Just f_tc <- tyConAppTyCon_maybe f - , isConcreteTyCon f_tc - = canDecomposableConcretePrim ev f_tc args - - -- Couldn't decompose the constraint: keep it as-is. - | otherwise - = canNonDecomposableConcretePrim ev ty - --- | Decompose a constraint of the form @'Concrete#' (f t_1 ... t_n)@, --- for a concrete `TyCon' `f`. --- --- This function will emit new Wanted @Concrete# t_i@ constraints, one for --- each of the arguments of `f`. +-- See Note [IsRefl#] in GHC.Tc.Utils.Concrete. -- --- See Note [Canonical Concrete# constraints]. -canDecomposableConcretePrim :: CtEvidence - -> TyCon - -> [TcType] - -> TcS (StopOrContinue Ct) -canDecomposableConcretePrim ev f_tc args - = do { traceTcS "canDecomposableConcretePrim" $ - vcat [text "args =" <+> ppr args, text "ev =" <+> ppr ev] - ; let ev_lvl - | CtWanted { ctev_dest = HoleDest hole } <- ev - , (_, _, _, conc_rhs_ty, Nominal) <- coVarKindsTypesRole (coHoleCoVar hole) - , Just conc_rhs_tv <- getTyVar_maybe conc_rhs_ty - , Just lvl <- metaTyVarTcLevel_maybe conc_rhs_tv - = lvl - - | otherwise - = pprPanic "canDecomposableConcretePrim" (ppr ev) - - ; (arg_cos, rhs_args) - <- mapAndUnzipM (emit_new_concretePrim_wanted ev_lvl (ctEvLoc ev)) args - - -- See Note [Solving Concrete constraints requires simplifyArgsWorker] - ; let (tc_binders, tc_res_kind) = splitPiTys (tyConKind f_tc) - fvs_args = tyCoVarsOfTypes rhs_args - ArgsReductions reductions final_co - = simplifyArgsWorker tc_binders tc_res_kind fvs_args - (repeat Nominal) (zipWith mkReduction arg_cos rhs_args) - Reduction concrete_co uncasted_concrete_rhs = mkTyConAppRedn Nominal f_tc reductions - concrete_rhs = uncasted_concrete_rhs `mkCastTyMCo` mkSymMCo final_co - - ; solveConcretePrimWanted ev concrete_co concrete_rhs - ; stopWith ev "Decomposed Concrete#" } - --- | Canonicalise a non-decomposable 'Concrete#' constraint. -canNonDecomposableConcretePrim :: CtEvidence -> TcType -> TcS (StopOrContinue Ct) -canNonDecomposableConcretePrim ev ty - = do { -- Update the evidence to account for the zonk to `ty`. - let ki = typeKind ty - new_ev = setCtEvPredType ev (mkTyConApp concretePrimTyCon [ki, ty]) - new_ct = - CSpecialCan { cc_ev = new_ev - , cc_special_pred = ConcretePrimPred - , cc_xi = ty } - ; traceTcS "canNonDecomposableConcretePrim" $ - vcat [ text "ty =" <+> ppr ty, text "new_ev =" <+> ppr new_ev ] - ; continueWith new_ct } - --- | Create a new 'Concrete#' Wanted constraint and immediately add it --- to the work list. Returns the evidence (a coercion hole) used for the --- constraint, and the right-hand type (a metavariable) of that coercion -emit_new_concretePrim_wanted :: TcLevel -> CtLoc -> Type -> TcS (Coercion, TcType) -emit_new_concretePrim_wanted ev_lvl loc ty - = do { (hole, rhs_ty, wanted) <- wrapTcS $ setTcLevel ev_lvl $ newConcretePrimWanted loc ty - ; emitWorkNC [wanted] - ; return (mkHoleCo hole, rhs_ty) } - --- | Solve a Wanted 'Concrete#' constraint. --- --- Recall that, when we create a Wanted constraint of the form @Concrete# ty@, --- we create a metavariable @concrete_tau@ and a coercion hole of type --- @ty ~# concrete_tau@. --- --- When we want to solve this constraint, because we have found that --- @ty@ is indeed equal to a concrete type @rhs@, we thus need to do --- two things: --- --- 1. fill the metavariable @concrete_tau := rhs@, --- 2. fill the coercion hole with the evidence for the equality @ty ~# rhs@. -solveConcretePrimWanted :: HasDebugCallStack - => CtEvidence -- ^ always a [W] Concrete# ty - -> Coercion -- ^ @co :: ty ~ rhs@ - -> TcType -- ^ @rhs@, which must be concrete - -> TcS () -solveConcretePrimWanted (CtWanted { ctev_dest = dest@(HoleDest hole) }) co rhs - = do { let Pair _ty concrete_tau = coVarTypes $ coHoleCoVar hole - tau_tv = getTyVar "solveConcretePrimWanted" concrete_tau - ; unifyTyVar tau_tv rhs - ; setWantedEq dest co } - -solveConcretePrimWanted ev co rhs - = pprPanic "solveConcretePrimWanted: no coercion hole to fill" $ - vcat [ text "ev =" <+> ppr ev <> semi <+> text "dest =" <+> case ev of - CtWanted { ctev_dest = EvVarDest var } -> text "var" <+> ppr var - _ -> text "XXX NOT EVEN A WANTED XXX" - , text "co =" <+> ppr co - , text "rhs =" <+> ppr rhs ] - -{- ********************************************************************** +-- 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/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs index b753a3c902..75a117798e 100644 --- a/compiler/GHC/Tc/Solver/Interact.hs +++ b/compiler/GHC/Tc/Solver/Interact.hs @@ -429,7 +429,9 @@ interactWithInertsStage wi CEqCan {} -> interactEq ics wi CIrredCan {} -> interactIrred ics wi CDictCan {} -> interactDict ics wi - CSpecialCan {} -> continueWith wi -- cannot have Special Givens, so nothing to interact with + 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 @@ -1891,13 +1893,14 @@ topReactionsStage work_item CEqCan {} -> doTopReactEq work_item - CSpecialCan {} -> - -- No top-level interactions for special constraints. - continueWith 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 9f75491dd0..34f4751f1d 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -168,7 +168,6 @@ import GHC.Tc.Types.Constraint import GHC.Tc.Utils.Unify import GHC.Core.Predicate import GHC.Types.Unique.Set (nonDetEltsUniqSet) -import GHC.Utils.Panic.Plain import Control.Monad import GHC.Utils.Monad @@ -735,7 +734,7 @@ removeInertCt is ct = CQuantCan {} -> panic "removeInertCt: CQuantCan" CIrredCan {} -> panic "removeInertCt: CIrredEvCan" CNonCanonical {} -> panic "removeInertCt: CNonCanonical" - CSpecialCan _ special_pred _ -> + CSpecialCan { cc_special_pred = special_pred } -> pprPanic "removeInertCt" (ppr "CSpecialCan" <+> parens (ppr special_pred)) -- | Looks up a family application in the inerts. @@ -1690,7 +1689,8 @@ setWantedEq :: HasDebugCallStack => TcEvDest -> Coercion -> TcS () setWantedEq (HoleDest hole) co = do { useVars (coVarsOfCo co) ; fillCoercionHole hole co } -setWantedEq (EvVarDest ev) _ = pprPanic "setWantedEq" (ppr ev) +setWantedEq (EvVarDest ev) _ = pprPanic "setWantedEq: EvVarDest" (ppr ev) +setWantedEq NoDest _ = panic "setWantedEq: NoDest" -- | Good for both equalities and non-equalities setWantedEvTerm :: TcEvDest -> EvTerm -> TcS () @@ -1706,6 +1706,8 @@ 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] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1773,7 +1775,8 @@ emitNewWantedEq loc rewriters role ty1 ty2 ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev)) ; return co } --- | Make a new equality CtEvidence +-- | Create a new Wanted constraint holding a coercion hole +-- for an equality between the two types at the given 'Role'. newWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS (CtEvidence, Coercion) newWantedEq loc rewriters role ty1 ty2 @@ -1787,7 +1790,9 @@ newWantedEq loc rewriters role ty1 ty2 where pty = mkPrimEqPredRole role ty1 ty2 --- no equalities here. Use newWantedEq instead +-- | Create a new Wanted constraint holding an evidence variable. +-- +-- Don't use this for equality constraints: use 'newWantedEq' instead. newWantedEvVarNC :: CtLoc -> RewriterSet -> TcPredType -> TcS CtEvidence -- Don't look up in the solved/inerts; we know it's not there @@ -1800,11 +1805,19 @@ newWantedEvVarNC loc rewriters pty , ctev_loc = loc , ctev_rewriters = rewriters })} +-- | Like 'newWantedEvVarNC', except it might look up in the inert set +-- to see if an inert already exists, and uses that instead of creating +-- a new Wanted constraint. +-- +-- Don't use this for equality constraints: this function is only for +-- constraints with 'EvVarDest'. newWantedEvVar :: CtLoc -> RewriterSet -> TcPredType -> TcS MaybeNew -- For anything except ClassPred, this is the same as newWantedEvVarNC newWantedEvVar loc rewriters pty - = assert (not (isHoleDestPred pty)) $ + = assertPpr (not (isEqPrimPred pty)) + (vcat [ text "newWantedEvVar: HoleDestPred" + , text "pty:" <+> ppr pty ]) $ do { mb_ct <- lookupInInerts loc pty ; case mb_ct of Just ctev @@ -1813,16 +1826,24 @@ newWantedEvVar loc rewriters pty _ -> do { ctev <- newWantedEvVarNC loc rewriters pty ; return (Fresh ctev) } } +-- | Create a new Wanted constraint, potentially looking up +-- non-equality constraints in the cache instead of creating +-- a new one from scratch. +-- +-- Deals with both equality and non-equality constraints. newWanted :: CtLoc -> RewriterSet -> PredType -> TcS MaybeNew --- Deals with both equalities and non equalities. Tries to look --- up non-equalities in the cache newWanted loc rewriters pty | Just (role, ty1, ty2) <- getEqPredTys_maybe pty = Fresh . fst <$> newWantedEq loc rewriters role ty1 ty2 | otherwise = newWantedEvVar loc rewriters pty --- deals with both equalities and non equalities. Doesn't do any cache lookups. +-- | Create a new Wanted constraint. +-- +-- Deals with both equality and non-equality constraints. +-- +-- Does not attempt to re-use non-equality constraints that already +-- exist in the inert set. newWantedNC :: CtLoc -> RewriterSet -> PredType -> TcS CtEvidence newWantedNC loc rewriters pty | Just (role, ty1, ty2) <- getEqPredTys_maybe pty diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index 8bd29b7bd5..2db40c7f7c 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -21,7 +21,7 @@ module GHC.Tc.Types.Constraint ( isUserTypeError, getUserTypeErrorMsg, ctEvidence, ctLoc, ctPred, ctFlavour, ctEqRel, ctOrigin, ctRewriters, - ctEvId, mkTcEqPredLikeEv, + ctEvId, wantedEvId_maybe, mkTcEqPredLikeEv, mkNonCanonical, mkNonCanonicalCt, mkGivens, mkIrredCt, ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel, @@ -69,7 +69,6 @@ module GHC.Tc.Types.Constraint ( ctEvRole, setCtEvPredType, setCtEvLoc, arisesFromGivens, tyCoVarsOfCtEvList, tyCoVarsOfCtEv, tyCoVarsOfCtEvsList, ctEvUnique, tcEvDestUnique, - isHoleDestPred, RewriterSet(..), emptyRewriterSet, isEmptyRewriterSet, -- exported concretely only for anyUnfilledCoercionHoles @@ -255,17 +254,13 @@ data Ct -- look like this, with the payload in an -- auxiliary type - -- | A special canonical constraint. + -- | A special canonical constraint: + -- a constraint that is used internally by GHC's typechecker. -- - -- When the 'SpecialPred' is 'ConcretePrimPred': - -- - -- - `cc_ev` is Wanted, - -- - `cc_xi = ty`, where `ty` cannot be decomposed any further. - -- See Note [Canonical Concrete# constraints] in GHC.Tc.Solver.Canonical. + -- See #20000. | CSpecialCan { cc_ev :: CtEvidence, - cc_special_pred :: SpecialPred, - cc_xi :: Xi + cc_special_pred :: SpecialPred } ------------ @@ -585,10 +580,26 @@ ctPred ct = ctEvPred (ctEvidence ct) ctRewriters :: Ct -> RewriterSet ctRewriters = ctEvRewriters . ctEvidence -ctEvId :: Ct -> EvVar +ctEvId :: HasDebugCallStack => Ct -> EvVar -- The evidence Id for this Ct 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'). +-- +-- Returns 'Nothing' otherwise. +wantedEvId_maybe :: Ct -> Maybe EvVar +wantedEvId_maybe ct + = case ctEvidence ct of + ctev@(CtWanted { ctev_dest = dst }) + | NoDest <- dst + -> Nothing + | otherwise + -> Just $ ctEvEvId ctev + CtGiven {} + -> Nothing + -- | Makes a new equality predicate with the same role as the given -- evidence. mkTcEqPredLikeEv :: CtEvidence -> TcType -> TcType -> TcType @@ -1647,9 +1658,8 @@ wrapType ty skols givens = mkSpecForAllTys skols $ mkPhiTy givens ty Note [CtEvidence invariants] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The `ctev_pred` field of a `CtEvidence` is a just a cache for the type -of the evidence. More precisely: +of the evidence. More precisely: -More precisely: * For Givens, `ctev_pred` = `varType ctev_evar` * For Wanteds, `ctev_pred` = `evDestType ctev_dest` @@ -1706,8 +1716,10 @@ 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 are always HoleDest; other wanteds are always --- EvVarDest. +-- +-- - Wanted equalities use HoleDest, +-- - IsRefl# constraints use NoDest, +-- - other Wanteds use EvVarDest. data TcEvDest = EvVarDest EvVar -- ^ bind this var to the evidence -- EvVarDest is always used for non-type-equalities @@ -1717,6 +1729,9 @@ 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] @@ -1759,7 +1774,7 @@ ctEvRewriters :: CtEvidence -> RewriterSet ctEvRewriters (CtWanted { ctev_rewriters = rewriters }) = rewriters ctEvRewriters _other = emptyRewriterSet -ctEvExpr :: CtEvidence -> EvExpr +ctEvExpr :: HasDebugCallStack => CtEvidence -> EvExpr ctEvExpr ev@(CtWanted { ctev_dest = HoleDest _ }) = Coercion $ ctEvCoercion ev ctEvExpr ev = evId (ctEvEvId ev) @@ -1775,10 +1790,12 @@ ctEvCoercion (CtWanted { ctev_dest = dest }) ctEvCoercion ev = pprPanic "ctEvCoercion" (ppr ev) -ctEvEvId :: CtEvidence -> EvVar +ctEvEvId :: HasDebugCallStack => 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 @@ -1787,6 +1804,7 @@ 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 } @@ -1798,12 +1816,13 @@ arisesFromGivens ct = isGivenCt ct || isGivenLoc (ctLoc ct) -- -- This function ensures that the invariants on 'CtEvidence' hold, by updating -- the evidence and the ctev_pred in sync with each other. --- See Note [CtEvidence invariants] -setCtEvPredType :: CtEvidence -> PredType -> CtEvidence -setCtEvPredType old_ctev new_pred = case old_ctev of +-- See Note [CtEvidence invariants]. +setCtEvPredType :: HasDebugCallStack => CtEvidence -> Type -> CtEvidence +setCtEvPredType old_ctev new_pred + = case old_ctev of CtGiven { ctev_evar = ev, ctev_loc = loc } -> CtGiven { ctev_pred = new_pred - , ctev_evar = setVarType ev new_var_type + , ctev_evar = setVarType ev new_pred , ctev_loc = loc } CtWanted { ctev_dest = dest, ctev_loc = loc, ctev_rewriters = rewriters } -> @@ -1814,33 +1833,14 @@ setCtEvPredType old_ctev new_pred = case old_ctev of } where new_dest = case dest of - EvVarDest ev -> EvVarDest (setVarType ev new_var_type) - HoleDest h -> HoleDest (setCoHoleType h new_var_type) - where - new_var_type - -- Gotcha: Concrete# constraints have evidence of a different type - -- than the predicate type - | SpecialPred ConcretePrimPred new_concrete_ty <- classifyPredType new_pred - = mkHeteroPrimEqPred (typeKind new_concrete_ty) k2 new_concrete_ty t2 - - | otherwise - = new_pred - - where - -- This is gross. But it will be short-lived, once we re-design - -- Concrete# constraints. - old_var = case old_ctev of - CtGiven { ctev_evar = evar } -> evar - CtWanted { ctev_dest = HoleDest h } -> coHoleCoVar h - CtWanted { ctev_dest = EvVarDest {} } -> - pprPanic "setCtEvPredType" (ppr old_ctev $$ ppr new_pred) - - (_k1, k2, _t1, t2, _role) = coVarKindsTypesRole old_var - + 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) @@ -1864,16 +1864,6 @@ isGiven :: CtEvidence -> Bool isGiven (CtGiven {}) = True isGiven _ = False --- | When creating a constraint for the given predicate, should --- it get a 'HoleDest'? True for equalities and Concrete# constraints --- only. See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete -isHoleDestPred :: PredType -> Bool -isHoleDestPred pty = case classifyPredType pty of - EqPred {} -> True - SpecialPred ConcretePrimPred _ -> True - _ -> False - - {- ************************************************************************ * * diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs index 2733ddd5ba..38345d82aa 100644 --- a/compiler/GHC/Tc/Types/Origin.hs +++ b/compiler/GHC/Tc/Types/Origin.hs @@ -941,7 +941,7 @@ callStackOriginFS orig = mkFastString (showSDocUnsafe (pprCtO orig Note [Reporting representation-polymorphism errors] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When we emit a 'Concrete#' Wanted constraint using GHC.Tc.Utils.Concrete.hasFixedRuntimeRep, +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, @@ -949,8 +949,8 @@ which keeps track of two things: a function application, a record update, ... If the constraint goes unsolved, we report it as follows: - - we detect that the unsolved Wanted is a Concrete# constraint in - GHC.Tc.Errors.reportWanteds using is_FRR, + - 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 @@ -958,11 +958,10 @@ 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 Concrete# wanted constraints, namely -'Concrete# r1' and 'Concrete# r2', and their 'CtOrigin's will be: +we will get two unsolved Wanted constraints, namely - FixedRuntimeRepOrigin a (FRRVarPattern x) - FixedRuntimeRepOrigin b (FRRVarPattern y) + 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: @@ -976,19 +975,18 @@ producing an error message of the form: b :: TYPE r2 -} --- | Where are we checking that a type has a fixed runtime representation? --- Equivalently: what is the origin of an emitted 'Concrete#' constraint? +-- | In what context are we checking that a type has a fixed runtime representation? data FRROrigin -- | Function arguments must have a fixed runtime representation. -- -- Test case: RepPolyApp. - = FRRApp !(HsExpr GhcRn) + = FRRApp !(HsExpr GhcTc) -- | Record fields in record updates must have a fixed runtime representation. -- -- Test case: RepPolyRecordUpdate. - | FRRRecordUpdate !RdrName !(HsExpr GhcRn) + | FRRRecordUpdate !RdrName !(HsExpr GhcTc) -- | Variable binders must have a fixed runtime representation. -- @@ -1074,23 +1072,18 @@ data FRROrigin -- which is not fixed. That information is added by 'GHC.Tc.Errors.mkFRRErr'. pprFRROrigin :: FRROrigin -> SDoc pprFRROrigin (FRRApp arg) - = sep [ text "The function argument" - , nest 2 $ quotes (ppr arg) - , text "does not have a fixed runtime representation"] + = vcat [ text "The function argument" + , nest 2 $ quotes (ppr arg) ] pprFRROrigin (FRRRecordUpdate lbl _arg) = hsep [ text "The record update at field" - , quotes (ppr lbl) - , text "does not have a fixed runtime representation"] + , quotes (ppr lbl) ] pprFRROrigin (FRRBinder binder) = hsep [ text "The binder" - , quotes (ppr binder) - , text "does not have a fixed runtime representation"] + , quotes (ppr binder) ] pprFRROrigin (FRRMatch matchCtxt i) - = vcat [ text "The type of the" <+> speakNth i <+> text "pattern in the" <+> pprMatchContextNoun matchCtxt - , text "does not have a fixed runtime representation"] + = text "The" <+> speakNth i <+> text "pattern in the" <+> pprMatchContextNoun matchCtxt pprFRROrigin (FRRDataConArg con i) - = sep [ text "The" <+> what - , text "does not have a fixed runtime representation"] + = text "The" <+> what where what :: SDoc what @@ -1100,36 +1093,29 @@ pprFRROrigin (FRRDataConArg con i) = text "data constructor argument in" <+> speakNth i <+> text "position" pprFRROrigin (FRRNoBindingResArg fn i) = vcat [ text "Unsaturated use of a representation-polymorphic primitive function." - , text "The" <+> speakNth i <+> text "argument of" <+> quotes (ppr $ getName fn) - , text "does not have a fixed runtime representation" ] + , text "The" <+> speakNth i <+> text "argument of" <+> quotes (ppr $ getName fn) ] pprFRROrigin (FRRTupleArg i) - = hsep [ text "The tuple argument in" <+> speakNth i <+> text "position" - , text "does not have a fixed runtime representation"] + = text "The tuple argument in" <+> speakNth i <+> text "position" pprFRROrigin (FRRTupleSection i) - = hsep [ text "The tuple section does not have a fixed runtime representation" - , text "in the" <+> speakNth i <+> text "position" ] + = text "The" <+> speakNth i <+> text "component of the tuple section" pprFRROrigin FRRUnboxedSum - = hsep [ text "The unboxed sum result type" - , text "does not have a fixed runtime representation"] + = text "The unboxed sum" pprFRROrigin (FRRBodyStmt stmtOrig i) = vcat [ text "The" <+> speakNth i <+> text "argument to (>>)" <> comma - , text "arising from the" <+> ppr stmtOrig <> comma - , text "does not have a fixed runtime representation" ] + , text "arising from the" <+> ppr stmtOrig <> comma ] pprFRROrigin FRRBodyStmtGuard = vcat [ text "The argument to" <+> quotes (text "guard") <> comma - , text "arising from the" <+> ppr MonadComprehension <> comma - , text "does not have a fixed runtime representation" ] + , text "arising from the" <+> ppr MonadComprehension <> comma ] pprFRROrigin (FRRBindStmt stmtOrig) = vcat [ text "The first argument to (>>=)" <> comma - , text "arising from the" <+> ppr stmtOrig <> comma - , text "does not have a fixed runtime representation" ] + , text "arising from the" <+> ppr stmtOrig <> comma ] pprFRROrigin FRRBindStmtGuard - = hsep [ text "The return type of the bind statement" - , text "does not have a fixed runtime representation" ] + = hsep [ text "The body of the bind statement" ] pprFRROrigin (FRRArrow arrowOrig) = pprFRRArrowOrigin arrowOrig pprFRROrigin (FRRWpFun wpFunOrig) - = pprWpFunOrigin wpFunOrig + = hsep [ text "The function argument" + , pprWpFunOrigin wpFunOrig ] instance Outputable FRROrigin where ppr = pprFRROrigin @@ -1188,27 +1174,22 @@ data FRRArrowOrigin pprFRRArrowOrigin :: FRRArrowOrigin -> SDoc pprFRRArrowOrigin (ArrowCmdResTy cmd) - = vcat [ hang (text "The arrow command") 2 (quotes (ppr cmd)) - , text "does not have a fixed runtime representation" ] + = vcat [ hang (text "The arrow command") 2 (quotes (ppr cmd)) ] pprFRRArrowOrigin (ArrowCmdApp fun arg) - = vcat [ text "In the arrow command application of" + = vcat [ text "The argument in the arrow command application of" , nest 2 (quotes (ppr fun)) , text "to" - , nest 2 (quotes (ppr arg)) <> comma - , text "the argument does not have a fixed runtime representation" ] + , nest 2 (quotes (ppr arg)) ] pprFRRArrowOrigin (ArrowCmdArrApp fun arg ho_app) - = vcat [ text "In the" <+> pprHsArrType ho_app <+> text "of" + = vcat [ text "The function un the" <+> pprHsArrType ho_app <+> text "of" , nest 2 (quotes (ppr fun)) , text "to" - , nest 2 (quotes (ppr arg)) <> comma - , text "the function does not have a fixed runtime representation" ] + , nest 2 (quotes (ppr arg)) ] pprFRRArrowOrigin (ArrowCmdLam i) - = vcat [ text "The" <+> speakNth i <+> text "pattern of the arrow command abstraction" - , text "does not have a fixed runtime representation" ] + = vcat [ text "The" <+> speakNth i <+> text "pattern of the arrow command abstraction" ] pprFRRArrowOrigin (ArrowFun fun) = vcat [ text "The return type of the arrow function" - , nest 2 (quotes (ppr fun)) - , text "does not have a fixed runtime representation" ] + , nest 2 (quotes (ppr fun)) ] instance Outputable FRRArrowOrigin where ppr = pprFRRArrowOrigin @@ -1231,16 +1212,16 @@ data WpFunOrigin pprWpFunOrigin :: WpFunOrigin -> SDoc pprWpFunOrigin (WpFunSyntaxOp orig) - = vcat [ text "When checking a rebindable syntax operator arising from" + = vcat [ text "of a rebindable syntax operator arising from" , nest 2 (ppr orig) ] pprWpFunOrigin (WpFunViewPat expr) - = vcat [ text "When checking the view pattern function:" + = vcat [ text "of the view pattern function" , nest 2 (ppr expr) ] pprWpFunOrigin (WpFunFunTy fun_ty) - = vcat [ text "When inferring the argument type of a function with type" + = vcat [ text "of the inferred argument type of a function with type" , nest 2 (ppr fun_ty) ] pprWpFunOrigin (WpFunFunExpTy fun_ty) - = vcat [ text "When inferring the argument type of a function with expected type" + = vcat [ text "of the inferred argument type of a function with expected type" , nest 2 (ppr fun_ty) ] instance Outputable WpFunOrigin where diff --git a/compiler/GHC/Tc/Utils/Concrete.hs b/compiler/GHC/Tc/Utils/Concrete.hs index 8ae32e5a78..dbf379479d 100644 --- a/compiler/GHC/Tc/Utils/Concrete.hs +++ b/compiler/GHC/Tc/Utils/Concrete.hs @@ -1,9 +1,13 @@ {-# LANGUAGE MultiWayIf #-} +-- | Checking for representation-polymorphism using the Concrete mechanism. +-- +-- This module contains the logic for enforcing the representation-polymorphism +-- invariants by way of emitting constraints. module GHC.Tc.Utils.Concrete - ( -- * Creating/emitting 'Concrete#' constraints + ( -- * Ensuring that a type has a fixed runtime representation hasFixedRuntimeRep - , newConcretePrimWanted + , hasFixedRuntimeRep_MustBeRefl -- * HsWrapper: checking for representation-polymorphism , mkWpFun ) @@ -11,28 +15,38 @@ module GHC.Tc.Utils.Concrete import GHC.Prelude -import GHC.Core.Coercion ( multToCo ) -import GHC.Core.Type ( isConcrete, typeKind ) -import GHC.Core.TyCo.Rep - -import GHC.Tc.Utils.Monad -import GHC.Tc.Utils.TcType ( mkTyConApp ) -import GHC.Tc.Utils.TcMType -import GHC.Tc.Types.Constraint -import GHC.Tc.Types.Evidence -import GHC.Tc.Types.Origin ( CtOrigin(..), FRROrigin(..), WpFunOrigin(..) ) +import GHC.Builtin.Types ( unliftedTypeKindTyCon, liftedTypeKindTyCon ) -import GHC.Builtin.Types ( unliftedTypeKindTyCon, liftedTypeKindTyCon ) -import GHC.Builtin.Types.Prim ( concretePrimTyCon ) +import GHC.Core.Coercion ( Role(..), multToCo ) +import GHC.Core.Predicate ( mkIsReflPrimPred ) +import GHC.Core.TyCo.Rep ( Type(TyConApp), Scaled(..) + , mkTyVarTy, scaledThing ) +import GHC.Core.Type ( isConcrete, typeKind ) -import GHC.Types.Basic ( TypeOrKind(KindLevel) ) +import GHC.Tc.Types ( TcM, ThStage(Brack), PendingStuff(TcPending) ) +import GHC.Tc.Types.Constraint ( mkNonCanonical ) +import GHC.Tc.Types.Evidence ( TcCoercion, HsWrapper(..) + , mkTcFunCo, mkTcRepReflCo, mkTcSymCo ) +import GHC.Tc.Types.Origin ( CtOrigin(..), FRROrigin(..), WpFunOrigin(..) ) +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.Types.Basic ( TypeOrKind(..) ) +import GHC.Utils.Misc ( HasDebugCallStack ) +import GHC.Utils.Outputable +import GHC.Utils.Panic ( assertPpr ) {- Note [Concrete overview] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Special predicates of the form `Concrete# ty` are used -to check, in the typechecker, that certain types have a fixed runtime representation. +GHC ensures that certain types have a fixed runtime representation in the +typechecker, by emitting certain constraints. +Emitting constraints to be solved later allows us to accept more programs: +if we directly inspected the type (using e.g. `typePrimRep`), we might not +have enough information available (e.g. if the type has kind `TYPE r` for +a metavariable `r` which has not yet been filled in.) + We give here an overview of the various moving parts, to serve as a central point of reference for this topic. @@ -50,20 +64,26 @@ as a central point of reference for this topic. So, instead of checking immediately, we emit a constraint. * What does it mean for a type to be concrete? - Note [Concrete types] + Note [Concrete types] explains what it means for a type to be concrete. + + To compute which representation to use for a type, `typePrimRep` expects + its kind to be concrete: something specific like `BoxedRep Lifted` or + `IntRep`; certainly not a type involving type variables or type families. + + * What constraints do we emit? Note [The Concrete mechanism] - The predicate 'Concrete# ty' is satisfied when we can produce - a coercion + Instead of simply checking that a type `ty` is concrete (i.e. computing + 'isConcrete`), we emit an equality constraint: - co :: ty ~ concrete_ty + co :: ty ~# concrete_ty - where 'concrete_ty' consists only of concrete types (no type variables, - no type families). + where 'concrete_ty' is a concrete metavariable: a metavariable whose 'MetaInfo' + is 'ConcreteTv', signifying that it can only be unified with a concrete type. - The first note explains more precisely what it means for a type to be concrete. - The second note explains how this relates to the `Concrete#` predicate, - and explains that the implementation is happening in two phases (PHASE 1 and PHASE 2). + The Note explains that this allows us to accept more programs. The Note + also explains that the implementation is happening in two phases + (PHASE 1 and PHASE 2). In PHASE 1 (the current implementation) we only allow trivial evidence of the form `co = Refl`. @@ -72,42 +92,29 @@ as a central point of reference for this topic. We currently enforce the representation-polymorphism invariants by checking that binders and function arguments have a "fixed RuntimeRep". - That is, `ty :: ki` has a "fixed RuntimeRep" if we can solve `Concrete# ki`. This is slightly less general than we might like, as this rules out types with kind `TYPE (BoxedRep l)`: we know that this will be represented by a pointer, which should be enough to go on in many situations. - * When do we emit 'Concrete#' constraints? + * When do we emit these constraints? Note [hasFixedRuntimeRep] - We introduce 'Concrete#' constraints to satisfy the representation-polymorphism + We introduce constraints to satisfy the representation-polymorphism invariants outlined in Note [Representation polymorphism invariants] in GHC.Core, which mostly amounts to the following two cases: - checking that a binder has a fixed runtime representation, - checking that a function argument has a fixed runtime representation. - The note explains precisely how we emit these 'Concrete#' constraints. - - * How do we solve Concrete# constraints? - Note [Solving Concrete# constraints] in GHC.Tc.Instance.Class + The Note explains precisely how and where these constraints are emitted. - Concrete# constraints are solved through two mechanisms, - which are both explained further in the note: - - - by decomposing them, e.g. `Concrete# (TYPE r)` is turned - into `Concrete# r` (canonicalisation of `Concrete#` constraints), - - by using 'Concrete' instances (top-level interactions). - The note explains that the evidence we get from using such 'Concrete' - instances can only ever be Refl, even in PHASE 2. - - * Reporting unsolved Concrete# constraints + * Reporting unsolved constraints Note [Reporting representation-polymorphism errors] in GHC.Tc.Types.Origin - When we emit a 'Concrete#' constraint, 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 an unsolved Wanted 'Concrete#' constraint. + 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. Note [Representation polymorphism checking] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -157,17 +164,12 @@ has a fixed runtime representation, both in the typechecker: See Note [Concrete overview] in GHC.Tc.Utils.Concrete for an overview of the various moving parts. - The idea is that, to guarantee that a type (rr :: RuntimeRep) is - representation-monomorphic, we emit a 'Concrete# rr' Wanted constraint. - If GHC can solve this constraint, it means 'rr' is monomorphic, and we - are OK to proceed. Otherwise, we report this unsolved Wanted in the form - of a representation-polymorphism error. The different contexts in which - such constraints arise are enumerated in 'FRROrigin'. - Note [Concrete types] ~~~~~~~~~~~~~~~~~~~~~ -Definition: a type is /concrete/ - iff it consists of a tree of concrete type constructors +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 Definition: a /concrete type constructor/ is defined by @@ -182,69 +184,57 @@ Definition: a /concrete type constructor/ is defined by Examples of concrete types: Lifted, BoxedRep Lifted, TYPE (BoxedRep Lifted) are all concrete Examples of non-concrete types - F Int, TYPE (F Int), TYPE r, a Int + F Int, TYPE (F Int), TYPE r, a[sk] NB: (F Int) is not concrete because F is a type function -Note [The Concrete mechanism] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -As explained in (2) in Note [Representation polymorphism checking], -to check (ty :: ki) has a fixed runtime representation, -we emit a `Concrete# ki` constraint, where +The recursive definition of concreteness entails the following property: - Concrete# :: forall k. k -> TupleRep '[] +Concrete Congruence Property (CCP) + All sub-trees of a concrete type tree are concrete. -Such constraints get solved by decomposition, as per - Note [Canonical Concrete# constraints] in GHC.Tc.Solver.Canonical. -When unsolved Wanted `Concrete#` constraints remain after typechecking, -we report them as representation-polymorphism errors, using `GHC.Tc.Types.Origin.FRROrigin` -to inform the user of the context in which a fixed-runtime-rep check arose. +The following property also holds due to the invariant that the kind of a +concrete metavariable is itself concrete (see Note [ConcreteTv]): --------------- --- EVIDENCE -- --------------- +Concrete Kinds Property (CKP) + The kind of a concrete type is concrete. -The evidence for a 'Concrete# ty' constraint is a nominal coercion +The CCP and the CKP taken together mean that we never have to inspect +in kinds to check concreteness. - co :: ty ~# concrete_ty +Note [ConcreteTv] +~~~~~~~~~~~~~~~~~ +A concrete metavariable is a metavariable whose 'MetaInfo' is 'ConcreteTv'. +Similar to 'TyVarTv's which are type variables which can only be unified with +other type variables, a 'ConcreteTv' type variable is a type variable which can +only be unified with a concrete type (in the sense of Note [Concrete types]). -where 'concrete_ty' consists only of (non-synonym) type constructors and applications -(after expanding any vanilla type synonyms). +INVARIANT: the kind of a concrete metavariable is concrete. - OK: +This invariant is upheld at the time of creation of a new concrete metavariable. - TYPE FloatRep - TYPE (BoxedRep Lifted) - Type - TYPE (TupleRep '[ FloatRep, SumRep '[ IntRep, IntRep ] ]) +Concrete metavariables are useful for representation-polymorphism checks: +they allow us to refer to a type whose representation is not yet known but will +be figured out by the typechecker (see Note [The Concrete mechanism]). - Not OK: - - Type variables: - - ty - TYPE r - TYPE (BoxedRep l) - - Type family applications: - - TYPE (Id FloatRep) - -This is so that we can compute the 'PrimRep's needed to represent the type -using 'runtimeRepPrimRep', which expects to be able to read off the 'RuntimeRep', -as per Note [Getting from RuntimeRep to PrimRep] in GHC.Types.RepType. +Note [The Concrete mechanism] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +To check (ty :: ki) has a fixed runtime representation, we proceed as follows: -Note that the evidence for a `Concrete#` constraint isn't a typeclass dictionary: -like with `(~#)`, the evidence is an (unlifted) nominal coercion, which justifies defining + - Create a new concrete metavariable `concrete_tv`, i.e. a metavariable + with 'ConcreteTv' 'MetaInfo' (see Note [ConcreteTv]). - Concrete# :: forall k. k -> TYPE (TupleRep '[]) + - Emit an equality constraint: -We still need a constraint that users can write in their own programs, -so much like `(~#)` and `(~)` we also define: + ki ~# concrete_tv - Concrete :: forall k. k -> Constraint + 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. -The need for user-facing 'Concrete' constraints is detailed in - Note [Concrete and Concrete#] in GHC.Builtin.Types. +To solve `ki ~# concrete_ki`, we must unify `concrete_tv := concrete_ki`, +where `concrete_ki` is some concrete type. We can then compute `kindPrimRep` +on `concrete_ki` to compute the representation: this means `ty` indeed +has a fixed runtime representation. ------------------------- -- PHASE 1 and PHASE 2 -- @@ -252,15 +242,20 @@ The need for user-facing 'Concrete' constraints is detailed in The Concrete mechanism is being implemented in two separate phases. -In PHASE 1 (currently implemented), we never allow a 'Concrete#' constraint -to be rewritten (see e.g. GHC.Tc.Solver.Canonical.canConcretePrim). -The only allowable evidence term is Refl, which forbids any program -that requires type family evaluation in order to determine that a 'RuntimeRep' is fixed. -N.B.: we do not currently check that this invariant is upheld: as we are discarding the -evidence in PHASE 1, we no longer have access to the coercion after constraint solving -(which is the point at which we would want to check that the filled in evidence is Refl). - -In PHASE 2 (future work), we lift this restriction. To illustrate what this entails, +In PHASE 1 (currently implemented), 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. + +In PHASE 2, we lift this restriction. This means we replace a call to +`hasFixedRuntimeRep_MustBeRefl` 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. As a result, we must insert additional casts in Core to ensure that no type family @@ -275,7 +270,7 @@ explicitly visible: f = /\ ( a :: F Int ). \ ( x :: ( a |> kco ) ). some_expression -where 'kco' is the evidence for `Concrete# (F Int)`, for example if `F Int = TYPE Int#` +where 'kco' is the appropriate coercion; for example if `F Int = TYPE Int#` this would be: kco :: F Int ~# TYPE Int# @@ -289,12 +284,9 @@ Note [Fixed RuntimeRep] ~~~~~~~~~~~~~~~~~~~~~~~ Definition: a type `ty :: ki` has a /fixed RuntimeRep/ - iff we can solve `Concrete# ki` - -In PHASE 1 (see Note [The Concrete mechanism]), this is equivalent to: - - a type `ty :: ki` has a /fixed RuntimeRep/ - iff `ki` is a concrete type (in the sense of Note [Concrete types]). + <=> + there exists a concrete type `concrete_ty` (in the sense of Note [Concrete types]) + such that we can solve `ki ~# concrete_ty`. This definition is crafted to be useful to satisfy the invariants of Core; see Note [Representation polymorphism invariants] in GHC.Core. @@ -312,10 +304,11 @@ Kinds are Calling Conventions [ICFP'20], but this suffices for now. Note [hasFixedRuntimeRep] ~~~~~~~~~~~~~~~~~~~~~~~~~ The 'hasFixedRuntimeRep' function is responsible for taking a type 'ty' -and emitting a 'Concrete#' constraint to ensure that 'ty' has a fixed `RuntimeRep`, +and emitting a constraint to ensure that 'ty' has a fixed `RuntimeRep`, as outlined in Note [The Concrete mechanism]. -To do so, we compute the kind 'ki' of 'ty' and emit a 'Concrete# ki' constraint, +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. [Wrinkle: Typed Template Haskell] @@ -350,136 +343,134 @@ which will only be solved if we can prove that 'ty' indeed has a fixed RuntimeRe Test case: rep-poly/T18170a. -Note [Solving Concrete# constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The representation polymorphism checks emit 'Concrete# ty' constraints, -as explained in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete. - -The main mechanism through which a `Concrete# ty` constraint is solved -is to directly inspect 'ty' to check that it is a concrete type -such as 'TYPE IntRep' or `TYPE (TupleRep '[ TupleRep '[], FloatRep ])`, -and not, e.g., a skolem type variable. - -There are, however, some interactions to take into account: - - 1. Decomposition. - - The solving of `Concrete#` constraints works recursively. - For example, to solve a Wanted `Concrete# (TYPE r)` constraint, - we decompose it, emitting a new `Concrete# @RuntimeRep r` Wanted constraint, - and use it to solve the original `Concrete# (TYPE r)` constraint. - This happens in the canonicaliser -- see GHC.Tc.Solver.Canonical.canDecomposableConcretePrim. - - Note that Decomposition fully solves `Concrete# ty` whenever `ty` is a - concrete type. For example: +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). - Concrete# (TYPE (BoxedRep Lifted)) - ==> (decompose) - Concrete# (BoxedRep Lifted) - ==> (decompose) - Concrete# Lifted - ==> (decompose) - <nothing, since Lifted is nullary> +That is, if we have a type family `F` with `F Int` reducing to `Int`, we __cannot__ solve +`IsRefl# (F Int) Int`. - 2. Rewriting. +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 - In PHASE 1 (as per Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete), - we don't have to worry about a 'Concrete#' constraint being rewritten. - We only need to zonk: if e.g. a metavariable, `alpha`, gets unified with `IntRep`, - we should be able to solve `Concrete# alpha`. + {co_hole} :: ki ~# concrete_tv - In PHASE 2, we will need to proceed as in GHC.Tc.Solver.Canonical.canClass: - if we have a constraint `Concrete# (F ty1)` and a coercion witnessing the reduction of - `F`, say `co :: F ty1 ~# ty2`, then we will solve `Concrete# (F ty1)` in terms of `Concrete# ty2`, - by rewriting the evidence for `Concrete# ty2` using `co` (see GHC.Tc.Solver.Canonical.rewriteEvidence). - - 3. Backpack - - Abstract 'TyCon's in Backpack signature files are always considered to be concrete. - This is because of the strong restrictions around how abstract types are allowed - to be implemented, as laid out in Note [Synonyms implement abstract data] in GHC.Tc.Module. - In particular, no variables or type family applications are allowed. - - Examples: backpack/should_run/T13955.bkp, rep-poly/RepPolyBackpack2. +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. -} --- | Evidence for a `Concrete#` constraint: --- essentially a 'ConcreteHole' (a coercion hole) that will be filled later, --- except: +-- | Like 'hasFixedRuntimeRep', but we insist that the obtained coercion must be 'Refl'. -- --- - we might already have the evidence now; no point in creating a coercion hole --- in that case; --- - we sometimes skip the check entirely, e.g. in Typed Template Haskell --- (see [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep]). -data ConcreteEvidence - = ConcreteReflEvidence - -- ^ We have evidence right now: don't bother creating a 'ConcreteHole'. - | ConcreteTypedTHNoEvidence - -- ^ We don't emit 'Concrete#' constraints in Typed Template Haskell. - -- See [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep]. - | ConcreteHoleEvidence ConcreteHole - -- ^ The general form of evidence: a 'ConcreteHole' that should be - -- filled in later by the constraint solver, as per - -- Note [Solving Concrete# constraints]. - --- | Check that the kind of the provided type is of the form --- @TYPE rep@ for a __fixed__ 'RuntimeRep' @rep@. +-- 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#]. -- --- If this isn't immediately obvious, for instance if the 'RuntimeRep' --- is hidden under a type-family application such as +-- 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@. -- --- > ty :: TYPE (F x) --- --- this function will emit a new Wanted 'Concrete#' constraint. -hasFixedRuntimeRep :: FRROrigin -> Type -> TcM ConcreteEvidence -hasFixedRuntimeRep frrOrig ty - - -- Shortcut: check for 'Type' and 'UnliftedType' type synonyms. - | TyConApp tc [] <- ki - , tc == liftedTypeKindTyCon || tc == unliftedTypeKindTyCon - = return ConcreteReflEvidence - - | otherwise +-- 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 = do { th_stage <- getStage ; if - -- We have evidence for 'Concrete# ty' right now: - -- no need to emit a constraint/create an evidence hole. - | isConcrete ki - -> return ConcreteReflEvidence + -- Shortcut: check for 'Type' and 'UnliftedType' type synonyms. + | TyConApp tc [] <- ki + , tc == liftedTypeKindTyCon || tc == unliftedTypeKindTyCon + -> return Nothing -- See [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep]. | Brack _ (TcPending {}) <- th_stage - -> return ConcreteTypedTHNoEvidence + -> return Nothing - -- Create a new Wanted 'Concrete#' constraint and emit it. | otherwise - -> do { loc <- getCtLocM (FixedRuntimeRepOrigin ty frrOrig) (Just KindLevel) - ; (hole, _, ct_ev) <- newConcretePrimWanted loc ki - ; emitSimple $ mkNonCanonical ct_ev - ; return $ ConcreteHoleEvidence hole } } + -- 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. + } where - ki :: Kind + ki :: TcKind ki = typeKind ty + orig :: CtOrigin + orig = FixedRuntimeRepOrigin ty frr_orig --- | Create a new 'Concrete#' constraint. --- Returns the evidence, a metavariable which will be filled in with a --- guaranteed-concrete type, and a Wanted CtEvidence -newConcretePrimWanted :: CtLoc -> Type -> TcM (ConcreteHole, TcType, CtEvidence) -newConcretePrimWanted loc ty - = do { let - ki :: Kind - ki = typeKind ty - ; (hole, concrete_ty) <- newConcreteHole ki ty - ; let - wantedCtEv :: CtEvidence - wantedCtEv = - CtWanted - { ctev_dest = HoleDest hole - , ctev_pred = mkTyConApp concretePrimTyCon [ki, ty] - , ctev_rewriters = emptyRewriterSet - , ctev_loc = loc - } - ; return (hole, concrete_ty, wantedCtEv) } +-- | 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 => 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'. +-- +-- 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'. +-- +-- 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) } + where + ki :: TcKind + ki = typeKind ty {-*********************************************************************** * * @@ -489,9 +480,9 @@ newConcretePrimWanted loc ty -- | Smart constructor to create a 'WpFun' 'HsWrapper'. -- --- Might emit a 'Concrete#' constraint, to check for --- representation polymorphism. This is necessary, as 'WpFun' will desugar to --- a lambda abstraction, whose binder must have a fixed runtime representation. +-- Might emit new Wanted constraints to check for representation polymorphism. +-- This is necessary, as 'WpFun' will desugar to a lambda abstraction, +-- whose binder must have a fixed runtime representation. mkWpFun :: HsWrapper -> HsWrapper -> Scaled TcType -- ^ the "from" type of the first wrapper -> TcType -- ^ either type of the second wrapper (used only when the @@ -503,5 +494,8 @@ mkWpFun WpHole (WpCast co2) (Scaled w t1) _ _ = return $ WpCast (mkTcFunC mkWpFun (WpCast co1) WpHole (Scaled w _) t2 _ = return $ WpCast (mkTcFunCo Representational (multToCo w) (mkTcSymCo co1) (mkTcRepReflCo t2)) mkWpFun (WpCast co1) (WpCast co2) (Scaled w _) _ _ = return $ WpCast (mkTcFunCo Representational (multToCo w) (mkTcSymCo co1) co2) mkWpFun co1 co2 t1 _ wpFunOrig - = do { _concrete_ev <- hasFixedRuntimeRep (FRRWpFun wpFunOrig) (scaledThing t1) + = do { hasFixedRuntimeRep_MustBeRefl (FRRWpFun wpFunOrig) (scaledThing t1) ; return $ WpFun co1 co2 t1 } + + -- NB: feel free to move this function elsewhere if you find a better place + -- for it (which doesn't create any cyclic imports). diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs index 4193514665..78c7ad4c12 100644 --- a/compiler/GHC/Tc/Utils/Instantiate.hs +++ b/compiler/GHC/Tc/Utils/Instantiate.hs @@ -97,7 +97,7 @@ import GHC.Unit.External import Data.List ( mapAccumL ) import qualified Data.List.NonEmpty as NE -import Control.Monad( when, unless, void ) +import Control.Monad( when, unless ) import Data.Function ( on ) {- @@ -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 void $ hasFixedRuntimeRep (FRRArrow $ ArrowFun user_expr) res_ty + in hasFixedRuntimeRep_MustBeRefl (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/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index cbbdcdfb47..8c59e30d95 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -197,12 +197,14 @@ newEvVar ty = do { name <- newSysName (predTypeOccName ty) -- | Create a new Wanted constraint with the given 'CtLoc'. newWantedWithLoc :: CtLoc -> PredType -> TcM CtEvidence newWantedWithLoc loc pty - = do d <- case classifyPredType pty of - EqPred {} -> HoleDest <$> newCoercionHole pty - SpecialPred ConcretePrimPred ty -> - HoleDest <$> (fst <$> newConcreteHole (typeKind ty) ty) - _ -> EvVarDest <$> newEvVar pty - return $ CtWanted { ctev_dest = d + = do dst <- case classifyPredType pty of + EqPred {} + -> HoleDest <$> newCoercionHole pty + SpecialPred s + -> case s of + IsReflPrimPred {} -> return NoDest + _ -> EvVarDest <$> newEvVar pty + return $ CtWanted { ctev_dest = dst , ctev_pred = pty , ctev_loc = loc , ctev_rewriters = emptyRewriterSet } @@ -229,9 +231,6 @@ cloneWantedCtEv ctev@(CtWanted { ctev_pred = pty, ctev_dest = HoleDest _ }) | isEqPrimPred pty = do { co_hole <- newCoercionHole pty ; return (ctev { ctev_dest = HoleDest co_hole }) } - | SpecialPred ConcretePrimPred ty <- classifyPredType pty - = do { (co_hole, _) <- newConcreteHole (typeKind ty) ty - ; return (ctev { ctev_dest = HoleDest co_hole }) } | otherwise = pprPanic "cloneWantedCtEv" (ppr pty) cloneWantedCtEv ctev = return ctev @@ -333,9 +332,9 @@ predTypeOccName ty = case classifyPredType ty of EqPred {} -> mkVarOccFS (fsLit "co") IrredPred {} -> mkVarOccFS (fsLit "irred") ForAllPred {} -> mkVarOccFS (fsLit "df") - SpecialPred special_pred _ -> - case special_pred of - ConcretePrimPred -> mkVarOccFS (fsLit "concr") + 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 @@ -865,6 +864,7 @@ metaInfoToTyVarName meta_info = TyVarTv -> fsLit "a" RuntimeUnkTv -> fsLit "r" CycleBreakerTv -> fsLit "b" + ConcreteTv -> fsLit "c" newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar newAnonMetaTyVar mi = newNamedAnonMetaTyVar (metaInfoToTyVarName mi) mi @@ -2712,9 +2712,10 @@ tidyEvVar env var = updateIdTypeAndMult (tidyType env) var -- If it isn't, throw a representation-polymorphism error appropriate -- for the context (as specified by the 'FixedRuntimeRepProvenance'). -- --- Unlike the other representation polymorphism checks, which emit --- 'Concrete#' constraints, this function does not emit any constraints, --- as it has enough information to immediately make a decision. +-- Unlike the other representation polymorphism checks, which can emit +-- new Wanted constraints to be solved by the constraint solver, this function +-- does not emit any constraints: it has enough information to immediately +-- make a decision. -- -- See (1) in Note [Representation polymorphism checking] in GHC.Tc.Utils.Concrete checkTypeHasFixedRuntimeRep :: FixedRuntimeRepProvenance -> Type -> TcM () diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index 807ad0ab56..b01f72b185 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -41,6 +41,7 @@ module GHC.Tc.Utils.TcType ( MetaDetails(Flexi, Indirect), MetaInfo(..), skolemSkolInfo, isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy, tcIsTcTyVar, isTyVarTyVar, isOverlappableTyVar, isTyConableTyVar, + isConcreteTyVar, isAmbiguousTyVar, isCycleBreakerTyVar, metaTyVarRef, metaTyVarInfo, isFlexi, isIndirect, isRuntimeUnkSkol, metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe, @@ -566,21 +567,27 @@ data MetaDetails | Indirect TcType data MetaInfo - = TauTv -- This MetaTv is an ordinary unification variable + = TauTv -- ^ This MetaTv is an ordinary unification variable -- A TauTv is always filled in with a tau-type, which -- never contains any ForAlls. - | TyVarTv -- A variant of TauTv, except that it should not be + | TyVarTv -- ^ A variant of TauTv, except that it should not be -- unified with a type, only with a type variable -- See Note [TyVarTv] in GHC.Tc.Utils.TcMType - | RuntimeUnkTv -- A unification variable used in the GHCi debugger. + | RuntimeUnkTv -- ^ A unification variable used in the GHCi debugger. -- It /is/ allowed to unify with a polytype, unlike TauTv | CycleBreakerTv -- Used to fix occurs-check problems in Givens -- See Note [Type variable cycles] in -- GHC.Tc.Solver.Canonical + | ConcreteTv + -- ^ 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. + instance Outputable MetaDetails where ppr Flexi = text "Flexi" ppr (Indirect ty) = text "Indirect" <+> ppr ty @@ -590,6 +597,7 @@ instance Outputable MetaInfo where ppr TyVarTv = text "tyv" ppr RuntimeUnkTv = text "rutv" ppr CycleBreakerTv = text "cbv" + ppr ConcreteTv = text "conc" {- ********************************************************************* * * @@ -1081,6 +1089,18 @@ isCycleBreakerTyVar tv | otherwise = False +-- | 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 + | isTcTyVar tv + , MetaTv { mtv_info = ConcreteTv } <- tcTyVarDetails tv + = True + | otherwise + = False + isMetaTyVarTy :: TcType -> Bool isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv isMetaTyVarTy _ = False @@ -1892,7 +1912,9 @@ isImprovementPred ty ClassPred cls _ -> classHasFds cls IrredPred {} -> True -- Might have equalities after reduction? ForAllPred {} -> False - SpecialPred {} -> False + SpecialPred s -> + case s of + IsReflPrimPred {} -> False {- Note [Expanding superclasses] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/GHC/Tc/Utils/TcType.hs-boot b/compiler/GHC/Tc/Utils/TcType.hs-boot index 08602fa5ac..4d09c1e7e1 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs-boot +++ b/compiler/GHC/Tc/Utils/TcType.hs-boot @@ -13,6 +13,7 @@ pprTcTyVarDetails :: TcTyVarDetails -> SDoc vanillaSkolemTvUnk :: HasCallStack => TcTyVarDetails isMetaTyVar :: TcTyVar -> Bool isTyConableTyVar :: TcTyVar -> Bool +isConcreteTyVar :: TcTyVar -> Bool tcEqType :: HasDebugCallStack => Type -> Type -> Bool diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index 4a5ef151b7..7bd489dc50 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -1479,9 +1479,9 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2 --- | Checks (TYVAR-TV) and (COERCION-HOLE) of Note [Unification preconditions]; --- returns True if these conditions are satisfied. But see the Note for other --- preconditions, too. +-- | 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 @@ -1490,15 +1490,18 @@ canSolveByUnification _ xi canSolveByUnification info xi = case info of CycleBreakerTv -> False - TyVarTv -> case tcGetTyVar_maybe xi of - Nothing -> False - Just tv -> case tcTyVarDetails tv of -- (TYVAR-TV) wrinkle - MetaTv { mtv_info = info } - -> case info of - TyVarTv -> True - _ -> False - SkolemTv {} -> True - RuntimeUnk -> True + ConcreteTv -> isConcrete xi -- (CONCRETE) check + TyVarTv -> + case tcGetTyVar_maybe xi of + Nothing -> False + Just tv -> + case tcTyVarDetails tv of -- (TYVAR-TV) wrinkle + SkolemTv {} -> True + RuntimeUnk -> True + MetaTv { mtv_info = info } -> + case info of + TyVarTv -> True + _ -> False _ -> True swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool @@ -1541,8 +1544,9 @@ lhsPriority tv MetaTv { mtv_info = info } -> case info of CycleBreakerTv -> 0 TyVarTv -> 1 - TauTv -> 2 - RuntimeUnkTv -> 3 + ConcreteTv -> 2 + TauTv -> 3 + RuntimeUnkTv -> 4 {- Note [Unification preconditions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1552,7 +1556,7 @@ unify alpha := ty? This note only applied to /homogeneous/ equalities, in which both sides have the same kind. -There are four reasons not to unify: +There are five reasons not to unify: 1. (SKOL-ESC) Skolem-escape Consider the constraint @@ -1590,7 +1594,16 @@ There are four reasons not to unify: * CycleBreakerTv: never unified, except by restoreTyVarCycles. -4. (COERCION-HOLE) Confusing coercion holes +4. (CONCRETE) A ConcreteTv can only unify with a concrete type, + by definition. + + That is, if we have `rr[conc] ~ F Int`, we can't unify + `rr` with `F Int`, so we hold off on unifying. + Note however that the equality might get rewritten; for instance + 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`. + +5. (COERCION-HOLE) Confusing coercion holes Suppose our equality is (alpha :: k) ~ (Int |> {co}) where co :: Type ~ k is an unsolved wanted. Note that this @@ -1605,6 +1618,7 @@ There are four reasons not to unify: This is expanded as Wrinkle (2) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical. + Needless to say, all there are wrinkles: * (SKOL-ESC) Promotion. Given alpha[n] ~ ty, what if beta[k] is free @@ -1678,12 +1692,16 @@ So we look for a positive reason to swap, using a three-step test: a TyVarTv with a TauTv, because then the TyVarTv could (transitively) get a non-tyvar type. So give these a low priority: 1. + - ConcreteTv: These are like TauTv, except they can only unify with + a concrete type. So we want to be able to write to them, but not quite + as much as TauTvs: 2. + - TauTv: This is the common case; we want these on the left so that they - can be written to: 2. + can be written to: 3. - RuntimeUnkTv: These aren't really meta-variables used in type inference, but just a convenience in the implementation of the GHCi debugger. - Eagerly write to these: 3. See Note [RuntimeUnkTv] in + Eagerly write to these: 4. See Note [RuntimeUnkTv] in GHC.Runtime.Heap.Inspect. * Names. If the level and priority comparisons are all diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs index 18474d41b1..1a5f2f6a41 100644 --- a/compiler/GHC/Tc/Validity.hs +++ b/compiler/GHC/Tc/Validity.hs @@ -1788,7 +1788,6 @@ checkInstTermination theta head_pred check foralld_tvs pred = case classifyPredType pred of EqPred {} -> return () -- See #4200. - SpecialPred {} -> return () IrredPred {} -> check2 foralld_tvs pred (sizeType pred) ClassPred cls tys | isTerminatingClass cls @@ -1807,6 +1806,10 @@ 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 $ |