From 57277662989b97dbf5ddc034d6c41ce39ab674ab Mon Sep 17 00:00:00 2001 From: sheaf Date: Sat, 29 Apr 2023 18:59:10 +0200 Subject: Add the Unsatisfiable class This commit implements GHC proposal #433, adding the Unsatisfiable class to the GHC.TypeError module. This provides an alternative to TypeError for which error reporting is more predictable: we report it when we are reporting unsolved Wanted constraints. Fixes #14983 #16249 #16906 #18310 #20835 --- compiler/GHC/Builtin/Names.hs | 21 ++- compiler/GHC/Builtin/Types.hs | 2 +- compiler/GHC/Builtin/Types/Prim.hs | 4 +- compiler/GHC/Core/Type.hs | 11 +- compiler/GHC/Data/Bag.hs | 13 +- compiler/GHC/Tc/Errors.hs | 144 +++++++++++++++- compiler/GHC/Tc/Errors/Ppr.hs | 2 + compiler/GHC/Tc/Errors/Types.hs | 7 +- compiler/GHC/Tc/Instance/Class.hs | 23 +-- compiler/GHC/Tc/Instance/FunDeps.hs | 10 ++ compiler/GHC/Tc/Solver.hs | 183 +++++++++++++++++++-- compiler/GHC/Tc/Solver/Monad.hs | 36 ++-- compiler/GHC/Tc/Solver/Types.hs | 15 +- compiler/GHC/Tc/TyCl/Instance.hs | 40 ++++- compiler/GHC/Tc/Types/Constraint.hs | 54 ++++-- compiler/GHC/Tc/Utils/Env.hs | 2 +- compiler/GHC/Tc/Utils/TcType.hs | 1 + compiler/GHC/Tc/Validity.hs | 4 +- compiler/GHC/Types/Error/Codes.hs | 1 + docs/users_guide/9.8.1-notes.rst | 15 ++ libraries/base/GHC/TypeError.hs | 75 +++++++-- libraries/base/changelog.md | 4 + testsuite/tests/unsatisfiable/T11503_Unsat.hs | 52 ++++++ testsuite/tests/unsatisfiable/T14141_Unsat.hs | 41 +++++ testsuite/tests/unsatisfiable/T14141_Unsat.stderr | 8 + testsuite/tests/unsatisfiable/T14339_Unsat.hs | 25 +++ testsuite/tests/unsatisfiable/T14339_Unsat.stderr | 4 + testsuite/tests/unsatisfiable/T15232_Unsat.hs | 13 ++ testsuite/tests/unsatisfiable/T22696_Unsat.stderr | 4 + testsuite/tests/unsatisfiable/UnsatClassMethods.hs | 29 ++++ testsuite/tests/unsatisfiable/UnsatDefault.hs | 14 ++ testsuite/tests/unsatisfiable/UnsatDefault.stderr | 6 + testsuite/tests/unsatisfiable/UnsatDefer.hs | 23 +++ testsuite/tests/unsatisfiable/UnsatDefer.stderr | 5 + testsuite/tests/unsatisfiable/UnsatFunDeps.hs | 10 ++ testsuite/tests/unsatisfiable/UnsatInstance.hs | 7 + testsuite/tests/unsatisfiable/UnsatInstance.stderr | 4 + testsuite/tests/unsatisfiable/UnsatPMWarnings.hs | 20 +++ testsuite/tests/unsatisfiable/Unsatisfiable1.hs | 21 +++ testsuite/tests/unsatisfiable/Unsatisfiable2.hs | 22 +++ .../tests/unsatisfiable/UnsatisfiableFail1.hs | 12 ++ .../tests/unsatisfiable/UnsatisfiableFail1.stderr | 5 + .../tests/unsatisfiable/UnsatisfiableFail2.hs | 15 ++ .../tests/unsatisfiable/UnsatisfiableFail2.stderr | 5 + .../tests/unsatisfiable/UnsatisfiableFail3.hs | 43 +++++ .../tests/unsatisfiable/UnsatisfiableFail3.stderr | 21 +++ .../tests/unsatisfiable/UnsatisfiableFail4.hs | 20 +++ .../tests/unsatisfiable/UnsatisfiableFail4.stderr | 22 +++ testsuite/tests/unsatisfiable/all.T | 19 +++ 49 files changed, 1050 insertions(+), 87 deletions(-) create mode 100644 testsuite/tests/unsatisfiable/T11503_Unsat.hs create mode 100644 testsuite/tests/unsatisfiable/T14141_Unsat.hs create mode 100644 testsuite/tests/unsatisfiable/T14141_Unsat.stderr create mode 100644 testsuite/tests/unsatisfiable/T14339_Unsat.hs create mode 100644 testsuite/tests/unsatisfiable/T14339_Unsat.stderr create mode 100644 testsuite/tests/unsatisfiable/T15232_Unsat.hs create mode 100644 testsuite/tests/unsatisfiable/T22696_Unsat.stderr create mode 100644 testsuite/tests/unsatisfiable/UnsatClassMethods.hs create mode 100644 testsuite/tests/unsatisfiable/UnsatDefault.hs create mode 100644 testsuite/tests/unsatisfiable/UnsatDefault.stderr create mode 100644 testsuite/tests/unsatisfiable/UnsatDefer.hs create mode 100644 testsuite/tests/unsatisfiable/UnsatDefer.stderr create mode 100644 testsuite/tests/unsatisfiable/UnsatFunDeps.hs create mode 100644 testsuite/tests/unsatisfiable/UnsatInstance.hs create mode 100644 testsuite/tests/unsatisfiable/UnsatInstance.stderr create mode 100644 testsuite/tests/unsatisfiable/UnsatPMWarnings.hs create mode 100644 testsuite/tests/unsatisfiable/Unsatisfiable1.hs create mode 100644 testsuite/tests/unsatisfiable/Unsatisfiable2.hs create mode 100644 testsuite/tests/unsatisfiable/UnsatisfiableFail1.hs create mode 100644 testsuite/tests/unsatisfiable/UnsatisfiableFail1.stderr create mode 100644 testsuite/tests/unsatisfiable/UnsatisfiableFail2.hs create mode 100644 testsuite/tests/unsatisfiable/UnsatisfiableFail2.stderr create mode 100644 testsuite/tests/unsatisfiable/UnsatisfiableFail3.hs create mode 100644 testsuite/tests/unsatisfiable/UnsatisfiableFail3.stderr create mode 100644 testsuite/tests/unsatisfiable/UnsatisfiableFail4.hs create mode 100644 testsuite/tests/unsatisfiable/UnsatisfiableFail4.stderr create mode 100644 testsuite/tests/unsatisfiable/all.T diff --git a/compiler/GHC/Builtin/Names.hs b/compiler/GHC/Builtin/Names.hs index 8671b5521f..d72e911541 100644 --- a/compiler/GHC/Builtin/Names.hs +++ b/compiler/GHC/Builtin/Names.hs @@ -503,6 +503,10 @@ basicKnownKeyNames , typeErrorVAppendDataConName , typeErrorShowTypeDataConName + -- "Unsatisfiable" constraint + , unsatisfiableClassName + , unsatisfiableIdName + -- Unsafe coercion proofs , unsafeEqualityProofName , unsafeEqualityTyConName @@ -1452,6 +1456,13 @@ typeErrorVAppendDataConName = typeErrorShowTypeDataConName = dcQual gHC_TYPEERROR (fsLit "ShowType") typeErrorShowTypeDataConKey +-- "Unsatisfiable" constraint +unsatisfiableClassName, unsatisfiableIdName :: Name +unsatisfiableClassName = + clsQual gHC_TYPEERROR (fsLit "Unsatisfiable") unsatisfiableClassNameKey +unsatisfiableIdName = + varQual gHC_TYPEERROR (fsLit "unsatisfiable") unsatisfiableIdNameKey + -- Unsafe coercion proofs unsafeEqualityProofName, unsafeEqualityTyConName, unsafeCoercePrimName, unsafeReflDataConName :: Name @@ -1993,9 +2004,13 @@ uFloatTyConKey = mkPreludeTyConUnique 161 uIntTyConKey = mkPreludeTyConUnique 162 uWordTyConKey = mkPreludeTyConUnique 163 +-- "Unsatisfiable" constraint +unsatisfiableClassNameKey :: Unique +unsatisfiableClassNameKey = mkPreludeTyConUnique 170 + -- Custom user type-errors errorMessageTypeErrorFamKey :: Unique -errorMessageTypeErrorFamKey = mkPreludeTyConUnique 181 +errorMessageTypeErrorFamKey = mkPreludeTyConUnique 181 coercibleTyConKey :: Unique coercibleTyConKey = mkPreludeTyConUnique 183 @@ -2548,6 +2563,10 @@ getFieldClassOpKey, setFieldClassOpKey :: Unique getFieldClassOpKey = mkPreludeMiscIdUnique 572 setFieldClassOpKey = mkPreludeMiscIdUnique 573 +-- "Unsatisfiable" constraints +unsatisfiableIdNameKey :: Unique +unsatisfiableIdNameKey = mkPreludeMiscIdUnique 580 + ------------------------------------------------------ -- ghc-bignum uses 600-699 uniques ------------------------------------------------------ diff --git a/compiler/GHC/Builtin/Types.hs b/compiler/GHC/Builtin/Types.hs index 59970daa3c..7dceb6524e 100644 --- a/compiler/GHC/Builtin/Types.hs +++ b/compiler/GHC/Builtin/Types.hs @@ -1999,7 +1999,7 @@ data BoxingInfo b -- recall: data Int = I# Int# -- -- BI_Box { bi_data_con = MkInt8Box, bi_inst_con = MkInt8Box @ty - -- , bi_boxed_type = Int8Box ty }A + -- , bi_boxed_type = Int8Box ty } -- recall: data Int8Box (a :: TYPE Int8Rep) = MkIntBox a boxingDataCon :: Type -> BoxingInfo b diff --git a/compiler/GHC/Builtin/Types/Prim.hs b/compiler/GHC/Builtin/Types/Prim.hs index 0335e1cb11..74710077b2 100644 --- a/compiler/GHC/Builtin/Types/Prim.hs +++ b/compiler/GHC/Builtin/Types/Prim.hs @@ -759,7 +759,7 @@ Wrinkles (W2) We need two absent-error Ids, aBSENT_ERROR_ID for types of kind Type, and aBSENT_CONSTRAINT_ERROR_ID for vaues of kind Constraint. Ditto noInlineId - vs noInlieConstraintId in GHC.Types.Id.Make; see Note [inlineId magic]. + vs noInlineConstraintId in GHC.Types.Id.Make; see Note [inlineId magic]. (W3) We need a TypeOrConstraint flag in LitRubbish. @@ -802,7 +802,7 @@ irretrievably overlap with: Wrinkles -(W1) In GHC.Core.RoughMap.roughMtchTyConName we are careful to map +(W1) In GHC.Core.RoughMap.roughMatchTyConName we are careful to map TYPE and CONSTRAINT to the same rough-map key. Reason: If we insert (F @Constraint tys) into a FamInstEnv, and look up (F @Type tys'), we /must/ ensure that the (C @Constraint tys) diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs index 40fa1ea2df..86f483abca 100644 --- a/compiler/GHC/Core/Type.hs +++ b/compiler/GHC/Core/Type.hs @@ -76,6 +76,7 @@ module GHC.Core.Type ( mkCastTy, mkCoercionTy, splitCastTy_maybe, + ErrorMsgType, userTypeError_maybe, pprUserTypeErrorTy, coAxNthLHS, @@ -1229,9 +1230,12 @@ isLitTy ty | LitTy l <- coreFullView ty = Just l | otherwise = Nothing +-- | A type of kind 'ErrorMessage' (from the 'GHC.TypeError' module). +type ErrorMsgType = Type + -- | Is this type a custom user error? --- If so, give us the kind and the error message. -userTypeError_maybe :: Type -> Maybe Type +-- If so, give us the error message. +userTypeError_maybe :: Type -> Maybe ErrorMsgType userTypeError_maybe t = do { (tc, _kind : msg : _) <- splitTyConApp_maybe t -- There may be more than 2 arguments, if the type error is @@ -1241,7 +1245,7 @@ userTypeError_maybe t ; return msg } -- | Render a type corresponding to a user type error into a SDoc. -pprUserTypeErrorTy :: Type -> SDoc +pprUserTypeErrorTy :: ErrorMsgType -> SDoc pprUserTypeErrorTy ty = case splitTyConApp_maybe ty of @@ -1267,7 +1271,6 @@ pprUserTypeErrorTy ty = -- An unevaluated type function _ -> ppr ty - {- ********************************************************************* * * FunTy diff --git a/compiler/GHC/Data/Bag.hs b/compiler/GHC/Data/Bag.hs index a9b8a669de..14caf3d5b1 100644 --- a/compiler/GHC/Data/Bag.hs +++ b/compiler/GHC/Data/Bag.hs @@ -18,7 +18,7 @@ module GHC.Data.Bag ( concatBag, catBagMaybes, foldBag, isEmptyBag, isSingletonBag, consBag, snocBag, anyBag, allBag, listToBag, nonEmptyToBag, bagToList, headMaybe, mapAccumBagL, - concatMapBag, concatMapBagPair, mapMaybeBag, unzipBag, + concatMapBag, concatMapBagPair, mapMaybeBag, mapMaybeBagM, unzipBag, mapBagM, mapBagM_, lookupBag, flatMapBagM, flatMapBagPairM, mapAndUnzipBagM, mapAccumBagLM, @@ -232,6 +232,17 @@ mapMaybeBag f (UnitBag x) = case f x of mapMaybeBag f (TwoBags b1 b2) = unionBags (mapMaybeBag f b1) (mapMaybeBag f b2) mapMaybeBag f (ListBag xs) = listToBag $ mapMaybe f (toList xs) +mapMaybeBagM :: Monad m => (a -> m (Maybe b)) -> Bag a -> m (Bag b) +mapMaybeBagM _ EmptyBag = return EmptyBag +mapMaybeBagM f (UnitBag x) = do r <- f x + return $ case r of + Nothing -> EmptyBag + Just y -> UnitBag y +mapMaybeBagM f (TwoBags b1 b2) = do r1 <- mapMaybeBagM f b1 + r2 <- mapMaybeBagM f b2 + return $ unionBags r1 r2 +mapMaybeBagM f (ListBag xs) = listToBag <$> mapMaybeM f (toList xs) + mapBagM :: Monad m => (a -> m b) -> Bag a -> m (Bag b) mapBagM _ EmptyBag = return EmptyBag mapBagM f (UnitBag x) = do r <- f x diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs index cb23c835dc..ed102d9bb5 100644 --- a/compiler/GHC/Tc/Errors.hs +++ b/compiler/GHC/Tc/Errors.hs @@ -588,6 +588,7 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics -- we might suppress its error message, and proceed on past -- type checking to get a Lint error later report1 = [ ("custom_error", is_user_type_error, True, mkUserTypeErrorReporter) + -- (Handles TypeError and Unsatisfiable) , given_eq_spec , ("insoluble2", utterly_wrong, True, mkGroupReporter mkEqErr) @@ -643,7 +644,12 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics non_tv_eq _ (EqPred NomEq ty1 _) = not (isTyVarTy ty1) non_tv_eq _ _ = False - is_user_type_error item _ = isUserTypeError (errorItemPred item) + -- Catch TypeError and Unsatisfiable. + -- Here, we want any nested TypeErrors to bubble up, so we use + -- 'containsUserTypeError' and not 'isTopLevelUserTypeError'. + -- + -- See also Note [Implementation of Unsatisfiable constraints], point (F). + is_user_type_error item _ = containsUserTypeError (errorItemPred item) is_homo_equality _ (EqPred _ ty1 ty2) = typeKind ty1 `tcEqType` typeKind ty2 @@ -786,8 +792,129 @@ Currently, the constraints to ignore are: If there is any trouble, checkValidFamInst bleats, aborting compilation. --} +Note [Implementation of Unsatisfiable constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The Unsatisfiable constraint was introduced in GHC proposal #433 (https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0433-unsatisfiable.rst). +See Note [The Unsatisfiable constraint] in GHC.TypeError. + +Its implementation consists of the following: + + A. The definitions. + + The Unsatisfiable class is defined in GHC.TypeError, in base. + It consists of the following definitions: + + type Unsatisfiable :: ErrorMessage -> Constraint + class Unsatisfiable msg where + unsatisfiableLifted :: a + + unsatisfiable :: forall {rep} (msg :: ErrorMessage) (a :: TYPE rep). Unsatisfiable msg => a + unsatisfiable = unsatisfiableLifted @msg @((##) -> a) (##) + + The class TyCon as well as the unsatisfiable Id have known-key Names + in GHC; they are not wired-in. + + B. Unsatisfiable instances. + + The Unsatisfiable typeclass has no instances (see GHC.Tc.Instance.Class.matchGlobalInst). + + Users are prevented from writing instances in GHC.Tc.Validity.check_special_inst_head. + This is done using the same mechanism as for, say, Coercible or WithDict. + + C. Using [G] Unsatisfiable msg to solve any Wanted. + + In GHC.Tc.Solver.simplifyTopWanteds, after defaulting happens, when an + implication contains Givens of the form [G] Unsatisfiable msg, and the + implication supports term-level evidence (as per Note [Coercion evidence only] + in GHC.Tc.Types.Evidence), we use any such Given to solve all the Wanteds + in that implication. See GHC.Tc.Solver.useUnsatisfiableGivens. + + The way we construct the evidence terms is slightly complicated by + Type vs Constraint considerations; see Note [Evidence terms from Unsatisfiable Givens] + in GHC.Tc.Solver. + + The proposal explains why this happens after defaulting: if there are other + ways to solve the Wanteds, we would prefer to use that, as that will make + user programs "as defined as possible". + + Wrinkle [Ambiguity] + + We also use an Unsatisfiable Given to solve Wanteds when performing an + ambiguity check. See the call to "useUnsatisfiableGivens" in + GHC.Tc.Solver.simplifyAmbiguityCheck. + + This is, for example, required to typecheck the definition + of "unsatisfiable" itself: + + unsatisfiable :: forall {rep} (msg :: ErrorMessage) (a :: TYPE rep). Unsatisfiable msg => a + + The ambiguity check on this type signature will produce + + [G] Unsatisfiable msg1, [W] Unsatisfiable msg2 + + and we want to ensure the Given solves the Wanted, to accept the definition. + + NB: + + An alternative would be to add a functional dependency on Unsatisfiable: + class Unsatisfiable msg | -> msg + + Then we would unify msg1 and msg2 in the above constraint solving problem, + and would be able to solve the Wanted using the Given in the normal way. + However, adding such a functional dependency solely for this purpose + could have undesirable consequences. For example, one might have + + [W] Unsatisfiable (Text "msg1"), [W] Unsatisfiable (Text "msg2") + + and W-W fundep interaction would produce the insoluble constraint + + [W] "msg1" ~ "msg2" + + which we definitely wouldn't want to report to the user. + + D. Adding "meth = unsatisfiable @msg" method bindings. + + When a class instance has an "Unsatisfiable msg" constraint in its context, + and the user has omitted methods (which don't have any default implementations), + we add method bindings of the form "meth = unsatisfiable @msg". + See GHC.Tc.TyCl.Instance.tcMethods, in particular "tc_default". + + Example: + + class C a where { op :: a -> a } + instance Unsatisfiable Msg => C [a] where {} + + elaborates to + + instance Unsatisfiable Msg => C [a] where { op = unsatisfiable @Msg } + + due to the (Unsatisfiable Msg) constraint in the instance context. + + We also switch off the "missing methods" warning in this situation. + See "checkMinimalDefinition" in GHC.Tc.TyCl.Instance.tcMethods. + + E. Switching off functional dependency coverage checks when there is + an "Unsatisfiable msg" context. + + This is because we want to allow users to rule out certain instances with + an "unsatisfiable" error, even when that would violate a functional + dependency. For example: + + class C a b | a -> b + instance Unsatisfiable (Text "No") => C a b + + See GHC.Tc.Instance.FunDeps.checkInstCoverage. + + F. Error reporting of "Unsatisfiable msg" constraints. + + This is done in GHC.Tc.Errors.reportWanteds: we detect when a constraint + is of the form "Unsatisfiable msg" and just emit the custom message + as an error to the user. + + This is the only way that "Unsatisfiable msg" constraints are reported, + which makes their behaviour much more predictable than TypeError. +-} -------------------------------------------- @@ -922,10 +1049,15 @@ mkUserTypeErrorReporter ctxt ; addDeferredBinding ctxt err item } mkUserTypeError :: ErrorItem -> TcSolverReportMsg -mkUserTypeError item = - case getUserTypeErrorMsg (errorItemPred item) of - Just msg -> UserTypeError msg - Nothing -> pprPanic "mkUserTypeError" (ppr item) +mkUserTypeError item + | Just msg <- getUserTypeErrorMsg pty + = UserTypeError msg + | Just msg <- isUnsatisfiableCt_maybe pty + = UnsatisfiableError msg + | otherwise + = pprPanic "mkUserTypeError" (ppr item) + where + pty = errorItemPred item mkGivenErrorReporter :: Reporter -- See Note [Given errors] diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs index 33c67fee79..4152866492 100644 --- a/compiler/GHC/Tc/Errors/Ppr.hs +++ b/compiler/GHC/Tc/Errors/Ppr.hs @@ -3438,6 +3438,8 @@ pprTcSolverReportMsg _ (BadTelescope telescope skols) = sorted_tvs = scopedSort skols pprTcSolverReportMsg _ (UserTypeError ty) = pprUserTypeErrorTy ty +pprTcSolverReportMsg _ (UnsatisfiableError ty) = + pprUserTypeErrorTy ty pprTcSolverReportMsg ctxt (ReportHoleError hole err) = pprHoleError ctxt hole err pprTcSolverReportMsg ctxt diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs index e2a69e0ce2..8cdc5eb007 100644 --- a/compiler/GHC/Tc/Errors/Types.hs +++ b/compiler/GHC/Tc/Errors/Types.hs @@ -150,7 +150,7 @@ import GHC.Core.InstEnv (LookupInstanceErrReason, ClsInst) import GHC.Core.PatSyn (PatSyn) import GHC.Core.Predicate (EqRel, predTypeEqRel) import GHC.Core.TyCon (TyCon, Role) -import GHC.Core.Type (Kind, Type, ThetaType, PredType) +import GHC.Core.Type (Kind, Type, ThetaType, PredType, ErrorMsgType) import GHC.Driver.Backend (Backend) import GHC.Unit.State (UnitState) import GHC.Utils.Misc (capitalise, filterOut) @@ -4482,7 +4482,10 @@ data TcSolverReportMsg -- err = () -- -- Test cases: CustomTypeErrors0{1,2,3,4,5}, T12104. - | UserTypeError Type + | UserTypeError ErrorMsgType -- ^ the message to report + + -- | Report a Wanted constraint of the form "Unsatisfiable msg". + | UnsatisfiableError ErrorMsgType -- ^ the message to report -- | We want to report an out of scope variable or a typed hole. -- See 'HoleError'. diff --git a/compiler/GHC/Tc/Instance/Class.hs b/compiler/GHC/Tc/Instance/Class.hs index 00811459c4..349ea1e34c 100644 --- a/compiler/GHC/Tc/Instance/Class.hs +++ b/compiler/GHC/Tc/Instance/Class.hs @@ -121,17 +121,18 @@ matchGlobalInst :: DynFlags -- See Note [Shortcut solving: overlap] -> Class -> [Type] -> TcM ClsInstResult matchGlobalInst dflags short_cut clas tys - | cls_name == knownNatClassName = matchKnownNat dflags short_cut clas tys - | cls_name == knownSymbolClassName = matchKnownSymbol dflags short_cut clas tys - | cls_name == knownCharClassName = matchKnownChar dflags short_cut clas tys - | isCTupleClass clas = matchCTuple clas tys - | cls_name == typeableClassName = matchTypeable clas tys - | cls_name == withDictClassName = matchWithDict tys - | clas `hasKey` heqTyConKey = matchHeteroEquality tys - | clas `hasKey` eqTyConKey = matchHomoEquality tys - | clas `hasKey` coercibleTyConKey = matchCoercible tys - | cls_name == hasFieldClassName = matchHasField dflags short_cut clas tys - | otherwise = matchInstEnv dflags short_cut clas tys + | cls_name == knownNatClassName = matchKnownNat dflags short_cut clas tys + | cls_name == knownSymbolClassName = matchKnownSymbol dflags short_cut clas tys + | cls_name == knownCharClassName = matchKnownChar dflags short_cut clas tys + | isCTupleClass clas = matchCTuple clas tys + | cls_name == typeableClassName = matchTypeable clas tys + | cls_name == withDictClassName = matchWithDict tys + | clas `hasKey` heqTyConKey = matchHeteroEquality tys + | clas `hasKey` eqTyConKey = matchHomoEquality tys + | clas `hasKey` coercibleTyConKey = matchCoercible tys + | cls_name == hasFieldClassName = matchHasField dflags short_cut clas tys + | cls_name == unsatisfiableClassName = return NoInstance -- See (B) in Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors + | otherwise = matchInstEnv dflags short_cut clas tys where cls_name = className clas diff --git a/compiler/GHC/Tc/Instance/FunDeps.hs b/compiler/GHC/Tc/Instance/FunDeps.hs index 681fd5d9a2..3b4768fb99 100644 --- a/compiler/GHC/Tc/Instance/FunDeps.hs +++ b/compiler/GHC/Tc/Instance/FunDeps.hs @@ -37,6 +37,7 @@ import GHC.Core.TyCo.FVs import GHC.Core.TyCo.Compare( eqTypes, eqType ) import GHC.Core.TyCo.Ppr( pprWithExplicitKindsWhen ) +import GHC.Tc.Types.Constraint ( isUnsatisfiableCt_maybe ) import GHC.Tc.Utils.TcType( transSuperClasses ) import GHC.Types.Var.Set @@ -401,6 +402,15 @@ checkInstCoverage :: Bool -- Be liberal -- Just msg => coverage problem described by msg checkInstCoverage be_liberal clas theta inst_taus + | any (isJust . isUnsatisfiableCt_maybe) theta + -- As per [GHC proposal #433](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0433-unsatisfiable.rst), + -- we skip checking the coverage condition if there is an "Unsatisfiable" + -- constraint in the instance context. + -- + -- See Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors, + -- point (E). + = IsValid + | otherwise = allValid (map fundep_ok fds) where (tyvars, fds) = classTvsFds clas diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index d4dae8e31e..eaa62e44ea 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE MultiWayIf, RecursiveDo #-} +{-# LANGUAGE MultiWayIf, RecursiveDo, TupleSections #-} module GHC.Tc.Solver( InferMode(..), simplifyInfer, findInferredDiff, @@ -31,11 +31,15 @@ import GHC.Prelude import GHC.Data.Bag import GHC.Core.Class +import GHC.Core +import GHC.Core.DataCon +import GHC.Core.InstEnv ( Coherence(IsCoherent) ) +import GHC.Core.Make import GHC.Driver.Session -import GHC.Tc.Utils.Instantiate +import GHC.Data.FastString import GHC.Data.List.SetOps import GHC.Types.Name -import GHC.Types.Id( idType ) +import GHC.Types.Id import GHC.Utils.Outputable import GHC.Builtin.Utils import GHC.Builtin.Names @@ -58,22 +62,25 @@ import GHC.Tc.Utils.TcType import GHC.Core.Type import GHC.Core.Ppr import GHC.Core.TyCon ( TyConBinder, isTypeFamilyTyCon ) -import GHC.Builtin.Types ( liftedRepTy, liftedDataConTy ) +import GHC.Builtin.Types import GHC.Core.Unify ( tcMatchTyKi ) +import GHC.Unit.Module ( getModule ) import GHC.Utils.Misc import GHC.Utils.Panic import GHC.Types.Var import GHC.Types.Var.Set -import GHC.Types.Basic ( IntWithInf, intGtLimit - , DefaultingStrategy(..), NonStandardDefaultingStrategy(..) ) +import GHC.Types.Basic +import GHC.Types.Id.Make ( unboxedUnitExpr ) import GHC.Types.Error import qualified GHC.LanguageExtensions as LangExt import Control.Monad +import Control.Monad.Trans.Class ( lift ) +import Control.Monad.Trans.State.Strict ( StateT(runStateT), put ) import Data.Foldable ( toList ) import Data.List ( partition ) import Data.List.NonEmpty ( NonEmpty(..) ) -import GHC.Data.Maybe ( mapMaybe, isJust ) +import GHC.Data.Maybe ( mapMaybe ) {- ********************************************************************************* @@ -487,7 +494,11 @@ simplifyTopWanteds wanteds = do { wc_first_go <- nestTcS (solveWanteds wanteds) -- This is where the main work happens ; dflags <- getDynFlags - ; try_tyvar_defaulting dflags wc_first_go } + ; wc_defaulted <- try_tyvar_defaulting dflags wc_first_go + + -- See Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors, + -- point (C). + ; useUnsatisfiableGivens wc_defaulted } where try_tyvar_defaulting :: DynFlags -> WantedConstraints -> TcS WantedConstraints try_tyvar_defaulting dflags wc @@ -539,6 +550,149 @@ simplifyTopWanteds wanteds | otherwise = defaultCallStacks wc +-- | If an implication contains a Given of the form @Unsatisfiable msg@, use +-- it to solve all Wanteds within the implication. +-- +-- This does a complete walk over the implication tree. +-- +-- See point (C) in Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors. +useUnsatisfiableGivens :: WantedConstraints -> TcS WantedConstraints +useUnsatisfiableGivens wc = + do { (final_wc, did_work) <- (`runStateT` False) $ go_wc wc + ; if did_work + then nestTcS (solveWanteds final_wc) + else return final_wc } + where + go_wc (WC { wc_simple = wtds, wc_impl = impls, wc_errors = errs }) + = do impls' <- mapMaybeBagM go_impl impls + return $ WC { wc_simple = wtds, wc_impl = impls', wc_errors = errs } + go_impl impl + | isSolvedStatus (ic_status impl) + = return $ Just impl + -- Is there a Given with type "Unsatisfiable msg"? + -- If so, use it to solve all other Wanteds. + | unsat_given:_ <- mapMaybe unsatisfiableEv_maybe (ic_given impl) + = do { put True + ; lift $ solveImplicationUsingUnsatGiven unsat_given impl } + -- Otherwise, recurse. + | otherwise + = do { wcs' <- go_wc (ic_wanted impl) + ; lift $ setImplicationStatus $ impl { ic_wanted = wcs' } } + +-- | Is this evidence variable the evidence for an 'Unsatisfiable' constraint? +-- +-- If so, return the variable itself together with the error message type. +unsatisfiableEv_maybe :: EvVar -> Maybe (EvVar, Type) +unsatisfiableEv_maybe v = (v,) <$> isUnsatisfiableCt_maybe (idType v) + +-- | We have an implication with an 'Unsatisfiable' Given; use that Given to +-- solve all the other Wanted constraints, including those nested within +-- deeper implications. +solveImplicationUsingUnsatGiven :: (EvVar, Type) -> Implication -> TcS (Maybe Implication) +solveImplicationUsingUnsatGiven + unsat_given@(given_ev,_) + impl@(Implic { ic_wanted = wtd, ic_tclvl = tclvl, ic_binds = ev_binds_var, ic_need_inner = inner }) + | isCoEvBindsVar ev_binds_var + -- We can't use Unsatisfiable evidence in kinds. + -- See Note [Coercion evidence only] in GHC.Tc.Types.Evidence. + = return $ Just impl + | otherwise + = do { wcs <- nestImplicTcS ev_binds_var tclvl $ go_wc wtd + ; setImplicationStatus $ + impl { ic_wanted = wcs + , ic_need_inner = inner `extendVarSet` given_ev } } + where + go_wc :: WantedConstraints -> TcS WantedConstraints + go_wc wc@(WC { wc_simple = wtds, wc_impl = impls }) + = do { mapBagM_ go_simple wtds + ; impls <- mapMaybeBagM (solveImplicationUsingUnsatGiven unsat_given) impls + ; return $ wc { wc_simple = emptyBag, wc_impl = impls } } + go_simple :: Ct -> TcS () + go_simple ct = case ctEvidence ct of + CtWanted { ctev_pred = pty, ctev_dest = dst } + -> do { ev_expr <- unsatisfiableEvExpr unsat_given pty + ; setWantedEvTerm dst IsCoherent $ EvExpr ev_expr } + _ -> return () + +-- | Create an evidence expression for an arbitrary constraint using +-- evidence for an "Unsatisfiable" Given. +-- +-- See Note [Evidence terms from Unsatisfiable Givens] +unsatisfiableEvExpr :: (EvVar, ErrorMsgType) -> PredType -> TcS EvExpr +unsatisfiableEvExpr (unsat_ev, given_msg) wtd_ty + = do { mod <- getModule + -- If we're typechecking GHC.TypeError, return a bogus expression; + -- it's only used for the ambiguity check, which throws the evidence away anyway. + -- This avoids problems with circularity; where we are trying to look + -- up the "unsatisfiable" Id while we are in the middle of typechecking it. + ; if mod == gHC_TYPEERROR then return (Var unsat_ev) else + do { unsatisfiable_id <- tcLookupId unsatisfiableIdName + + -- See Note [Evidence terms from Unsatisfiable Givens] + -- for a description of what evidence term we are constructing here. + + ; let -- (##) -=> wtd_ty + fun_ty = mkFunTy visArgConstraintLike ManyTy unboxedUnitTy wtd_ty + mkDictBox = case boxingDataCon fun_ty of + BI_Box { bi_data_con = mkDictBox } -> mkDictBox + _ -> pprPanic "unsatisfiableEvExpr: no DictBox!" (ppr wtd_ty) + dictBox = dataConTyCon mkDictBox + ; ev_bndr <- mkSysLocalM (fsLit "ct") ManyTy fun_ty + -- Dict ((##) -=> wtd_ty) + ; let scrut_ty = mkTyConApp dictBox [fun_ty] + -- unsatisfiable @{LiftedRep} @given_msg @(Dict ((##) -=> wtd_ty)) unsat_ev + scrut = + mkCoreApps (Var unsatisfiable_id) + [ Type liftedRepTy + , Type given_msg + , Type scrut_ty + , Var unsat_ev ] + -- case scrut of { MkDictBox @((##) -=> wtd_ty)) ct -> ct (# #) } + ev_expr = + mkWildCase scrut (unrestricted $ scrut_ty) wtd_ty + [ Alt (DataAlt mkDictBox) [ev_bndr] $ + mkCoreApps (Var ev_bndr) [unboxedUnitExpr] + ] + ; return ev_expr } } + +{- Note [Evidence terms from Unsatisfiable Givens] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +An Unsatisfiable Given constraint, of the form [G] Unsatisfiable msg, should be +able to solve ANY Wanted constraint whatsoever. + +Recall that we have + + unsatisfiable :: forall {rep} (msg :: ErrorMessage) (a :: TYPE rep) + . Unsatisfiable msg => a + +We want to use this function, together with the evidence +[G] unsat_ev :: Unsatisfiable msg, to solve any other constraint [W] wtd_ty. + +We could naively think that a valid evidence term for the Wanted might be: + + wanted_ev = unsatisfiable @{rep} @msg @wtd_ty unsat_ev + +Unfortunately, this is a kind error: "wtd_ty :: CONSTRAINT rep", but +"unsatisfiable" expects the third type argument to be of kind "TYPE rep". + +Instead, we use a boxing data constructor to box the constraint into a type. +In the end, we construct the following evidence for the implication: + + [G] unsat_ev :: Unsatisfiable msg + ==> + [W] wtd_ev :: wtd_ty + + wtd_ev = + case unsatisfiable @{LiftedRep} @msg @(Dict ((##) -=> wtd_ty)) unsat_ev of + MkDictBox ct -> ct (# #) + +Note that we play the same trick with the function arrow -=> that we did +in order to define "unsatisfiable" in terms of "unsatisfiableLifted", as described +in Note [The Unsatisfiable representation-polymorphism trick] in base:GHC.TypeError. +This allows us to indirectly box constraints with different representations +(such as primitive equality constraints). +-} + -- | Default any remaining @CallStack@ constraints to empty @CallStack@s. defaultCallStacks :: WantedConstraints -> TcS WantedConstraints -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence @@ -845,8 +999,11 @@ last example above. simplifyAmbiguityCheck :: Type -> WantedConstraints -> TcM () simplifyAmbiguityCheck ty wanteds = do { traceTc "simplifyAmbiguityCheck {" (text "type = " <+> ppr ty $$ text "wanted = " <+> ppr wanteds) - ; (final_wc, _) <- runTcS $ solveWanteds wanteds + ; (final_wc, _) <- runTcS $ useUnsatisfiableGivens =<< solveWanteds wanteds -- NB: no defaulting! See Note [No defaulting in the ambiguity check] + -- Note: we do still use Unsatisfiable Givens to solve Wanteds, + -- see Wrinkle [Ambiguity] under point (C) of + -- Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors. ; traceTc "End simplifyAmbiguityCheck }" empty @@ -2785,9 +2942,9 @@ findUnnecessaryGivens info need_inner givens unused_givens = filterOut is_used givens - is_used given = is_type_error given - || (given `elemVarSet` need_inner) - || (in_instance_decl && is_improving (idType given)) + is_used given = is_type_error given + || given `elemVarSet` need_inner + || (in_instance_decl && is_improving (idType given)) minimal_givens = mkMinimalBySCs evVarPred givens is_minimal = (`elemVarSet` mkVarSet minimal_givens) @@ -2796,7 +2953,7 @@ findUnnecessaryGivens info need_inner givens | otherwise = filterOut is_minimal givens -- See #15232 - is_type_error = isJust . userTypeError_maybe . idType + is_type_error id = isTopLevelUserTypeError (idType id) is_improving pred -- (transSuperClasses p) does not include p = any isImprovementPred (pred : transSuperClasses pred) diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index 49699d865d..bd2e48682f 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -59,7 +59,8 @@ module GHC.Tc.Solver.Monad ( getTopEnv, getGblEnv, getLclEnv, setLclEnv, getTcEvBindsVar, getTcLevel, getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap, - tcLookupClass, tcLookupId, + tcLookupClass, tcLookupId, tcLookupTyCon, + -- Inerts updInertTcS, updInertCans, updInertDicts, updInertIrreds, @@ -134,7 +135,9 @@ import qualified GHC.Tc.Utils.Monad as TcM import qualified GHC.Tc.Utils.TcMType as TcM import qualified GHC.Tc.Instance.Class as TcM( matchGlobalInst, ClsInstResult(..) ) import qualified GHC.Tc.Utils.Env as TcM - ( checkWellStaged, tcGetDefaultTys, tcLookupClass, tcLookupId, topIdLvl + ( checkWellStaged, tcGetDefaultTys + , tcLookupClass, tcLookupId, tcLookupTyCon + , topIdLvl , tcInitTidyEnv ) import GHC.Driver.Session @@ -151,6 +154,8 @@ import GHC.Tc.Types.Origin import GHC.Tc.Types.Constraint import GHC.Tc.Utils.Unify +import GHC.Builtin.Names ( unsatisfiableClassNameKey ) + import GHC.Core.Type import GHC.Core.TyCo.Rep as Rep import GHC.Core.Coercion @@ -536,17 +541,25 @@ getInnermostGivenEqLevel :: TcS TcLevel getInnermostGivenEqLevel = do { inert <- getInertCans ; return (inert_given_eq_lvl inert) } -getInertInsols :: TcS Cts --- Returns insoluble equality constraints and TypeError constraints, --- specifically including Givens. +-- | Retrieves all insoluble constraints from the inert set, +-- specifically including Given constraints. -- --- Note that this function only inspects irreducible constraints; --- a DictCan constraint such as 'Eq (TypeError msg)' is not --- considered to be an insoluble constraint by this function. +-- This consists of: -- --- See Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver. +-- - insoluble equalities, such as @Int ~# Bool@; +-- - constraints that are top-level custom type errors, of the form +-- @TypeError msg@, but not constraints such as @Eq (TypeError msg)@ +-- in which the type error is nested; +-- - unsatisfiable constraints, of the form @Unsatisfiable msg@. +-- +-- The inclusion of Givens is important for pattern match warnings, as we +-- want to consider a pattern match that introduces insoluble Givens to be +-- redundant (see Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver). +getInertInsols :: TcS Cts getInertInsols = do { inert <- getInertCans - ; return $ filterBag insolubleCt (inert_irreds inert) } + ; let irreds = inert_irreds inert + unsats = findDictsByTyConKey (inert_dicts inert) unsatisfiableClassNameKey + ; return $ unsats `unionBags` filterBag insolubleCt irreds } getInertGivens :: TcS [Ct] -- Returns the Given constraints in the inert set @@ -1356,6 +1369,9 @@ tcLookupClass c = wrapTcS $ TcM.tcLookupClass c tcLookupId :: Name -> TcS Id tcLookupId n = wrapTcS $ TcM.tcLookupId n +tcLookupTyCon :: Name -> TcS TyCon +tcLookupTyCon n = wrapTcS $ TcM.tcLookupTyCon n + -- Any use of this function is a bit suspect, because it violates the -- pure veneer of TcS. But it's just about warnings around unused imports -- and local constructors (GHC will issue fewer warnings than it otherwise diff --git a/compiler/GHC/Tc/Solver/Types.hs b/compiler/GHC/Tc/Solver/Types.hs index 80ca1113a6..648f451eee 100644 --- a/compiler/GHC/Tc/Solver/Types.hs +++ b/compiler/GHC/Tc/Solver/Types.hs @@ -4,7 +4,8 @@ -- | Utility types used within the constraint solver module GHC.Tc.Solver.Types ( -- Inert CDictCans - DictMap, emptyDictMap, findDictsByClass, addDict, + DictMap, emptyDictMap, addDict, + findDictsByTyConKey, findDictsByClass, addDictsByClass, delDict, foldDicts, filterDicts, findDict, dictsToBag, partitionDicts, @@ -25,6 +26,9 @@ import GHC.Tc.Types.Constraint import GHC.Tc.Types.Origin import GHC.Tc.Utils.TcType +import GHC.Types.Unique +import GHC.Types.Unique.DFM + import GHC.Core.Class import GHC.Core.Map.Type import GHC.Core.Predicate @@ -140,9 +144,12 @@ findDict m loc cls tys = findTcApp m (classTyCon cls) tys findDictsByClass :: DictMap a -> Class -> Bag a -findDictsByClass m cls - | Just tm <- lookupDTyConEnv m (classTyCon cls) = foldTM consBag tm emptyBag - | otherwise = emptyBag +findDictsByClass m cls = findDictsByTyConKey m (getUnique $ classTyCon cls) + +findDictsByTyConKey :: DictMap a -> Unique -> Bag a +findDictsByTyConKey m tc + | Just tm <- lookupUDFM_Directly m tc = foldTM consBag tm emptyBag + | otherwise = emptyBag delDict :: DictMap a -> Class -> [Type] -> DictMap a delDict m cls tys = delTcApp m (classTyCon cls) tys diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs index caae46ce36..f0bfb8b4da 100644 --- a/compiler/GHC/Tc/TyCl/Instance.hs +++ b/compiler/GHC/Tc/TyCl/Instance.hs @@ -6,6 +6,8 @@ {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeFamilies #-} {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} @@ -48,6 +50,7 @@ import GHC.Tc.Deriv import GHC.Tc.Utils.Env import GHC.Tc.Gen.HsType import GHC.Tc.Utils.Unify +import GHC.Builtin.Names ( unsatisfiableIdName ) import GHC.Core ( Expr(..), mkApps, mkVarApps, mkLams ) import GHC.Core.Make ( nO_METHOD_BINDING_ERROR_ID ) import GHC.Core.Unfold.Make ( mkInlineUnfoldingWithArity, mkDFunUnfolding ) @@ -1785,6 +1788,9 @@ tcMethods skol_info dfun_id clas tyvars dfun_ev_vars inst_tys hs_sig_fn = mkHsSigFun sigs inst_loc = getSrcSpan dfun_id + unsat_thetas = + mapMaybe (\ id -> (id,) <$> isUnsatisfiableCt_maybe (idType id)) dfun_ev_vars + ---------------------- tc_item :: ClassOpItem -> TcM (Id, LHsBind GhcTc, Maybe Implication) tc_item (sel_id, dm_info) @@ -1813,8 +1819,29 @@ tcMethods skol_info dfun_id clas tyvars dfun_ev_vars inst_tys ; (meth_id, _) <- mkMethIds clas tyvars dfun_ev_vars inst_tys sel_id ; dflags <- getDynFlags - ; let meth_bind = mkVarBind meth_id $ - mkLHsWrap lam_wrapper (error_rhs dflags) + ; meth_rhs <- + if + -- If the instance has an "Unsatisfiable msg" context, + -- add method bindings that use "unsatisfiable". + -- + -- See Note [Implementation of Unsatisfiable constraints], + -- in GHC.Tc.Errors, point (D). + | (theta_id,unsat_msg):_ <- unsat_thetas + -> do { unsat_id <- tcLookupId unsatisfiableIdName + -- Recall that unsatisfiable :: forall {rep} (msg :: ErrorMessage) (a :: TYPE rep). Unsatisfiable msg => a + -- + -- So we need to instantiate the forall and pass the dictionary evidence. + ; return $ L inst_loc' $ + wrapId + ( mkWpEvApps [EvExpr $ Var theta_id] + <.> mkWpTyApps [getRuntimeRep meth_tau, unsat_msg, meth_tau]) + unsat_id } + + -- Otherwise, add bindings whose RHS is an error + -- "No explicit nor default method for class operation 'meth'". + | otherwise + -> return $ error_rhs dflags + ; let meth_bind = mkVarBind meth_id $ mkLHsWrap lam_wrapper meth_rhs ; return (meth_id, meth_bind, Nothing) } where inst_loc' = noAnnSrcSpan inst_loc @@ -1829,13 +1856,18 @@ tcMethods skol_info dfun_id clas tyvars dfun_ev_vars inst_tys (unsafeMkByteString (error_string dflags)))) meth_tau = classMethodInstTy sel_id inst_tys error_string dflags = showSDoc dflags - (hcat [ppr inst_loc, vbar, ppr sel_id ]) + (hcat [ppr inst_loc, vbar, quotes (ppr sel_id) ]) lam_wrapper = mkWpTyLams tyvars <.> mkWpEvLams dfun_ev_vars ---------------------- -- Check if one of the minimal complete definitions is satisfied checkMinimalDefinition - = whenIsJust (isUnsatisfied methodExists (classMinimalDef clas)) $ + = when (null unsat_thetas) $ + -- Don't warn if there is an "Unsatisfiable" constraint in the context. + -- + -- See Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors, + -- point (D). + whenIsJust (isUnsatisfied methodExists (classMinimalDef clas)) $ warnUnsatisfiedMinimalDefinition methodExists meth = isJust (findMethodBind meth binds prag_fn) diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index 6fc6b235c4..d99f9067df 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -16,7 +16,8 @@ module GHC.Tc.Types.Constraint ( isPendingScDict, pendingScDict_maybe, superClassesMightHelp, getPendingWantedScs, isWantedCt, isGivenCt, - isUserTypeError, getUserTypeErrorMsg, + isTopLevelUserTypeError, containsUserTypeError, getUserTypeErrorMsg, + isUnsatisfiableCt_maybe, ctEvidence, ctLoc, ctPred, ctFlavour, ctEqRel, ctOrigin, ctRewriters, ctEvId, wantedEvId_maybe, mkTcEqPredLikeEv, @@ -118,8 +119,8 @@ import GHC.Core.TyCo.Ppr import GHC.Utils.FV import GHC.Types.Var.Set import GHC.Driver.Session (DynFlags(reductionDepth)) +import GHC.Builtin.Names import GHC.Types.Basic -import GHC.Types.Unique import GHC.Types.Unique.Set import GHC.Utils.Outputable @@ -134,7 +135,7 @@ import Data.Coerce import Data.Monoid ( Endo(..) ) import qualified Data.Semigroup as S import Control.Monad ( msum, when ) -import Data.Maybe ( mapMaybe ) +import Data.Maybe ( mapMaybe, isJust ) import Data.List.NonEmpty ( NonEmpty ) -- these are for CheckTyEqResult @@ -957,7 +958,7 @@ Eq (F (TypeError msg)) -- Here the type error is nested under a type-function -- | A constraint is considered to be a custom type error, if it contains -- custom type errors anywhere in it. -- See Note [Custom type errors in constraints] -getUserTypeErrorMsg :: PredType -> Maybe Type +getUserTypeErrorMsg :: PredType -> Maybe ErrorMsgType getUserTypeErrorMsg pred = msum $ userTypeError_maybe pred : map getUserTypeErrorMsg (subTys pred) where @@ -971,10 +972,30 @@ getUserTypeErrorMsg pred = msum $ userTypeError_maybe pred Just (_,ts) -> ts (t,ts) -> t : ts -isUserTypeError :: PredType -> Bool -isUserTypeError pred = case getUserTypeErrorMsg pred of - Just _ -> True - _ -> False +-- | Is this an user error message type, i.e. either the form @TypeError err@ or +-- @Unsatisfiable err@? +isTopLevelUserTypeError :: PredType -> Bool +isTopLevelUserTypeError pred = + isJust (userTypeError_maybe pred) || isJust (isUnsatisfiableCt_maybe pred) + +-- | Does this constraint contain an user error message? +-- +-- That is, the type is either of the form @Unsatisfiable err@, or it contains +-- a type of the form @TypeError msg@, either at the top level or nested inside +-- the type. +containsUserTypeError :: PredType -> Bool +containsUserTypeError pred = + isJust (getUserTypeErrorMsg pred) || isJust (isUnsatisfiableCt_maybe pred) + +-- | Is this type an unsatisfiable constraint? +-- If so, return the error message. +isUnsatisfiableCt_maybe :: Type -> Maybe ErrorMsgType +isUnsatisfiableCt_maybe t + | Just (tc, [msg]) <- splitTyConApp_maybe t + , tc `hasKey` unsatisfiableClassNameKey + = Just msg + | otherwise + = Nothing isPendingScDict :: Ct -> Bool isPendingScDict (CDictCan { cc_pend_sc = f }) = pendingFuel f @@ -1297,22 +1318,23 @@ insolubleEqCt _ = False -- nested custom type errors: it only detects @TypeError msg :: Constraint@, -- and not e.g. @Eq (TypeError msg)@. insolubleCt :: Ct -> Bool -insolubleCt ct - | Just _ <- userTypeError_maybe (ctPred ct) - -- Don't use 'isUserTypeErrorCt' here, as that function is too eager: - -- the TypeError might appear inside a type family application - -- which might later reduce, but we only want to return 'True' +insolubleCt ct = isTopLevelUserTypeError (ctPred ct) || insolubleEqCt ct + where + -- NB: 'isTopLevelUserTypeError' detects constraints of the form "TypeError msg" + -- and "Unsatisfiable msg". It deliberately does not detect TypeError + -- nested in a type (e.g. it does not use "containsUserTypeError"), as that + -- would be too eager: the TypeError might appear inside a type family + -- application which might later reduce, but we only want to return 'True' -- for constraints that are definitely insoluble. -- + -- For example: Num (F Int (TypeError "msg")), where F is a type family. + -- -- Test case: T11503, with the 'Assert' type family: -- -- > type Assert :: Bool -> Constraint -> Constraint -- > type family Assert check errMsg where -- > Assert 'True _errMsg = () -- > Assert _check errMsg = errMsg - = True - | otherwise - = insolubleEqCt ct -- | Does this hole represent an "out of scope" error? -- See Note [Insoluble holes] diff --git a/compiler/GHC/Tc/Utils/Env.hs b/compiler/GHC/Tc/Utils/Env.hs index b8f9d83912..aa7230108c 100644 --- a/compiler/GHC/Tc/Utils/Env.hs +++ b/compiler/GHC/Tc/Utils/Env.hs @@ -462,7 +462,7 @@ tcLookup name = do local_env <- getLclTypeEnv case lookupNameEnv local_env name of Just thing -> return thing - Nothing -> (AGlobal <$> tcLookupGlobal name) + Nothing -> AGlobal <$> tcLookupGlobal name tcLookupTyVar :: Name -> TcM TcTyVar tcLookupTyVar name diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index e7d33c3a80..1a03cd1c4b 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -2542,6 +2542,7 @@ isTerminatingClass cls -- Typeable constraints are bigger than they appear due -- to kind polymorphism, but we can never get instance divergence this way || cls `hasKey` coercibleTyConKey + || cls `hasKey` unsatisfiableClassNameKey allDistinctTyVars :: TyVarSet -> [KindOrType] -> Bool -- (allDistinctTyVars tvs tys) returns True if tys are diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs index 250811b99e..da51f7245f 100644 --- a/compiler/GHC/Tc/Validity.hs +++ b/compiler/GHC/Tc/Validity.hs @@ -1503,7 +1503,9 @@ check_special_inst_head dflags is_boot is_sig ctxt clas cls_args -- instances for (~), (~~), or Coercible; -- but we DO want to allow them in quantified constraints: -- f :: (forall a b. Coercible a b => Coercible (m a) (m b)) => ...m... - | clas_nm `elem` [ heqTyConName, eqTyConName, coercibleTyConName, withDictClassName ] + | clas_nm `elem` + [ heqTyConName, eqTyConName, coercibleTyConName + , withDictClassName, unsatisfiableClassName ] , not quantified_constraint = failWithTc $ TcRnSpecialClassInst clas False diff --git a/compiler/GHC/Types/Error/Codes.hs b/compiler/GHC/Types/Error/Codes.hs index 9c2f7d1dc3..195f6e0608 100644 --- a/compiler/GHC/Types/Error/Codes.hs +++ b/compiler/GHC/Types/Error/Codes.hs @@ -300,6 +300,7 @@ type family GhcDiagnosticCode c = n | n -> c where -- Constraint solver diagnostic codes GhcDiagnosticCode "BadTelescope" = 97739 GhcDiagnosticCode "UserTypeError" = 64725 + GhcDiagnosticCode "UnsatisfiableError" = 22250 GhcDiagnosticCode "ReportHoleError" = 88464 GhcDiagnosticCode "UntouchableVariable" = 34699 GhcDiagnosticCode "FixedRuntimeRepError" = 55287 diff --git a/docs/users_guide/9.8.1-notes.rst b/docs/users_guide/9.8.1-notes.rst index 0f0848765f..9f2d51d329 100644 --- a/docs/users_guide/9.8.1-notes.rst +++ b/docs/users_guide/9.8.1-notes.rst @@ -93,6 +93,21 @@ Compiler with each other, communicating via the system semaphore specified by the flag argument. +- GHC Proposal `#433 + `_ + has been implemented. This adds the class ``Unsatisfiable :: ErrorMessage -> Constraint`` + to the ``GHC.TypeError`` module. Constraints of the form ``Unsatisfiable msg`` + provide a mechanism for custom type errors that reports the errors in a more + predictable behaviour than ``TypeError``, as these constraints are + handled purely during constraint solving. + + For example: :: + + instance Unsatisfiable (Text "There is no Eq instance for functions") => Eq (a -> b) where + (==) = unsatisfiable + + This allows errors to be reported when users use the instance, even when + type errors are being deferred. GHCi ~~~~ diff --git a/libraries/base/GHC/TypeError.hs b/libraries/base/GHC/TypeError.hs index 77df75854b..21f62afad5 100644 --- a/libraries/base/GHC/TypeError.hs +++ b/libraries/base/GHC/TypeError.hs @@ -1,16 +1,25 @@ {-# LANGUAGE Trustworthy #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE MagicHash #-} {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UnboxedTuples #-} {-# LANGUAGE NoImplicitPrelude #-} {-# OPTIONS_HADDOCK not-home #-} {-| -This module exports the TypeError family, which is used to provide custom type -errors, and the ErrorMessage kind used to define these custom error messages. -This is a type-level analogue to the term level error function. +This module exports: + + - The 'TypeError' type family, which is used to provide custom type + errors. This is a type-level analogue to the term level error function. + - The 'ErrorMessage' kind, used to define custom error messages. + - The 'Unsatisfiable' constraint, a more principled variant of 'TypeError' + which gives a more predictable way of reporting custom type errors. @since 4.17.0.0 -} @@ -19,15 +28,15 @@ module GHC.TypeError ( ErrorMessage (..) , TypeError , Assert + , Unsatisfiable, unsatisfiable ) where import Data.Bool import GHC.Num.Integer () -- See Note [Depend on GHC.Num.Integer] in GHC.Base -import GHC.Types (Constraint, Symbol) +import GHC.Types (TYPE, Constraint, Symbol) -{- -Note [Custom type errors] -~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Custom type errors] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ TypeError is used to provide custom type errors, similar to the term-level error function. TypeError is somewhat magical: when the constraint solver encounters a constraint where the RHS is TypeError, it reports the error to @@ -85,9 +94,8 @@ infixl 6 :<>: -- @since 4.9.0.0 type family TypeError (a :: ErrorMessage) :: b where -{- -Note [Getting good error messages from boolean comparisons] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Getting good error messages from boolean comparisons] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We want to write types like f :: forall (x :: Int) (y :: Int). (x <= y) => T x -> T y @@ -139,3 +147,50 @@ type family Assert check errMsg where Assert 'True _ = () Assert _ errMsg = errMsg -- See Note [Getting good error messages from boolean comparisons] + +{- Note [The Unsatisfiable constraint] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The class `Unsatisfiable :: ErrorMessage -> Constraint` provides a mechanism +for custom type errors that reports the errors in a more predictable behaviour +than `TypeError`, as these constraints are handled purely during constraint solving. + +The details are laid out in GHC Proposal #433 (https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0433-unsatisfiable.rst). + +See Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors for +details of the implementation in GHC. + +Note [The Unsatisfiable representation-polymorphism trick] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The class method `unsatisfiableLifted :: forall (a::Type). Unsatisfiable msg => a` +works only for lifted types `a`. What if we want an unsatisfiable value of type +`Int#`, say? The function `unsatisfiable` has a representation-polymoprhic type + unsatisfiable :: forall {rep} (msg :: ErrorMessage) (b :: TYPE rep). + Unsatisfiable msg => b +and yet is defined in terms of `unsatisfiableLifted`. How? By instantiating +`unsatisfiableLifted` at type `(##) -> b`, and applying the result to `(##)`. +Very cunning! +-} + +-- | An unsatisfiable constraint. Similar to 'TypeError' when used at the +-- 'Constraint' kind, but reports errors in a more predictable manner. +-- +-- See also the 'unsatisfiable' function. +-- +-- @since 4.19.0.0@. +type Unsatisfiable :: ErrorMessage -> Constraint +class Unsatisfiable msg where + unsatisfiableLifted :: a + +-- | Prove anything within a context with an 'Unsatisfiable' constraint. +-- +-- This is useful for filling in instance methods when there is an 'Unsatisfiable' +-- constraint in the instance head, e.g.: +-- +-- > instance Unsatisfiable (Text "No Eq instance for functions") => Eq (a -> b) where +-- (==) = unsatisfiable +-- +-- @since 4.19.0.0@. +unsatisfiable :: forall {rep} (msg :: ErrorMessage) (a :: TYPE rep). Unsatisfiable msg => a +unsatisfiable = unsatisfiableLifted @msg @((##) -> a) (##) + -- See Note [The Unsatisfiable representation-polymorphism trick] + diff --git a/libraries/base/changelog.md b/libraries/base/changelog.md index d25888e7fb..bc55cc4977 100644 --- a/libraries/base/changelog.md +++ b/libraries/base/changelog.md @@ -20,6 +20,10 @@ * Add `COMPLETE` pragmas to the `TypeRep`, `SSymbol`, `SChar`, and `SNat` pattern synonyms. ([CLC proposal #149](https://github.com/haskell/core-libraries-committee/issues/149)) * Make `($)` representation polymorphic ([CLC proposal #132](https://github.com/haskell/core-libraries-committee/issues/132)) + * Implemented [GHC Proposal #433](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0433-unsatisfiable.rst), + adding the class `Unsatisfiable :: ErrorMessage -> TypeError`` to `GHC.TypeError`, + which provides a mechanism for custom type errors that reports the errors in + a more predictable behaviour than ``TypeError``. ## 4.18.0.0 *March 2023* * Shipped with GHC 9.6.1 diff --git a/testsuite/tests/unsatisfiable/T11503_Unsat.hs b/testsuite/tests/unsatisfiable/T11503_Unsat.hs new file mode 100644 index 0000000000..a685daf066 --- /dev/null +++ b/testsuite/tests/unsatisfiable/T11503_Unsat.hs @@ -0,0 +1,52 @@ +{-# LANGUAGE Haskell2010 #-} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module T11503_Unsat where + +import GHC.TypeError + ( Unsatisfiable, ErrorMessage(..) ) +import GHC.TypeNats + ( Nat, type (+), type (<=?) ) +import Data.Kind + ( Constraint, Type ) + +-- Example 1: from #11503 + +type NotInt :: Type -> Constraint +type family NotInt a where + NotInt Int = Unsatisfiable (Text "That's Int, silly.") + NotInt _ = (() :: Constraint) + +data T a where + MkT1 :: a -> T a + MkT2 :: NotInt a => T a + +foo :: T Int -> Int +foo (MkT1 x) = x +-- Should not have any pattern match warnings for MkT2. + +-- Example 2: from #20180 + +type Assert :: Bool -> Constraint -> Constraint +type family Assert check errMsg where + Assert 'True _errMsg = () + Assert _check errMsg = errMsg + +type List :: Nat -> Type -> Type +data List n t where + Nil :: List 0 t + (:-) :: t -> List n t -> List (n+1) t + +type (<=) :: Nat -> Nat -> Constraint +type family x <= y where + x <= y = Assert (x <=? y) (Unsatisfiable (Text "Impossible!")) + +head' :: 1 <= n => List n t -> t +head' (x :- _) = x +-- Should not have any pattern match warnings for Nil. diff --git a/testsuite/tests/unsatisfiable/T14141_Unsat.hs b/testsuite/tests/unsatisfiable/T14141_Unsat.hs new file mode 100644 index 0000000000..8be3b41960 --- /dev/null +++ b/testsuite/tests/unsatisfiable/T14141_Unsat.hs @@ -0,0 +1,41 @@ +{-# LANGUAGE Haskell2010 #-} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module T14141_Unsat where + +import GHC.TypeError +import Data.Kind + ( Constraint, Type ) + +-- Example 1: from #14141 + +data D where + MkD :: C => D + +type C :: Constraint +type family C where + C = Unsatisfiable ('Text "error") + +f :: D -> () +f MkD = () + +-- Example 2: from #16377 + +type F :: Type -> Constraint +type family F a :: Constraint +type instance F Int = () +type instance F Char = Unsatisfiable ('Text "Nope") + +data T where + A :: F Int => T + B :: F Char => T + +exhaustive :: T -> () +exhaustive A = () +exhaustive B = () diff --git a/testsuite/tests/unsatisfiable/T14141_Unsat.stderr b/testsuite/tests/unsatisfiable/T14141_Unsat.stderr new file mode 100644 index 0000000000..d71928917f --- /dev/null +++ b/testsuite/tests/unsatisfiable/T14141_Unsat.stderr @@ -0,0 +1,8 @@ + +T14141_Unsat.hs:26:1: warning: [GHC-94210] [-Woverlapping-patterns (in -Wdefault)] + Pattern match has inaccessible right hand side + In an equation for ‘f’: f MkD = ... + +T14141_Unsat.hs:41:1: warning: [GHC-53633] [-Woverlapping-patterns (in -Wdefault)] + Pattern match is redundant + In an equation for ‘exhaustive’: exhaustive B = ... diff --git a/testsuite/tests/unsatisfiable/T14339_Unsat.hs b/testsuite/tests/unsatisfiable/T14339_Unsat.hs new file mode 100644 index 0000000000..ffa0c141ab --- /dev/null +++ b/testsuite/tests/unsatisfiable/T14339_Unsat.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UndecidableInstances #-} + +module T14339_Unsat where + +import GHC.TypeError + +newtype Foo = Foo Int + +class Bar a where + bar :: a + +instance (Unsatisfiable (Text "Boo")) => Bar Foo where + bar = undefined + +newtype Baz1 = Baz1 Foo + + +-- should be ok +deriving instance Unsatisfiable (Text "Shouldn't see this") => Bar Baz1 + +-- should emit the error "Boo" +newtype Baz2 = Baz2 Foo + deriving Bar diff --git a/testsuite/tests/unsatisfiable/T14339_Unsat.stderr b/testsuite/tests/unsatisfiable/T14339_Unsat.stderr new file mode 100644 index 0000000000..c24a421eb8 --- /dev/null +++ b/testsuite/tests/unsatisfiable/T14339_Unsat.stderr @@ -0,0 +1,4 @@ + +T14339_Unsat.hs:25:12: error: [GHC-22250] + • Boo + • When deriving the instance for (Bar Baz2) diff --git a/testsuite/tests/unsatisfiable/T15232_Unsat.hs b/testsuite/tests/unsatisfiable/T15232_Unsat.hs new file mode 100644 index 0000000000..c8a55e2be3 --- /dev/null +++ b/testsuite/tests/unsatisfiable/T15232_Unsat.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} + +module T15232_Unsat where + +import GHC.TypeError + +class C a where f :: a -> a +instance {-# OVERLAPPING #-} C Int where f _ = 42 +instance {-# OVERLAPPABLE #-} Unsatisfiable ( 'Text "Only Int is supported" ) => C a where f = undefined + +main :: IO () +main = print $ f (42::Int) diff --git a/testsuite/tests/unsatisfiable/T22696_Unsat.stderr b/testsuite/tests/unsatisfiable/T22696_Unsat.stderr new file mode 100644 index 0000000000..26b5362362 --- /dev/null +++ b/testsuite/tests/unsatisfiable/T22696_Unsat.stderr @@ -0,0 +1,4 @@ + +T22696_Unsat.hs:25:12: error: [GHC-22250] + • Boo + • When deriving the instance for (Bar Baz2) diff --git a/testsuite/tests/unsatisfiable/UnsatClassMethods.hs b/testsuite/tests/unsatisfiable/UnsatClassMethods.hs new file mode 100644 index 0000000000..f0543df7ab --- /dev/null +++ b/testsuite/tests/unsatisfiable/UnsatClassMethods.hs @@ -0,0 +1,29 @@ +{-# LANGUAGE DataKinds #-} + +module UnsatClassMethods where + +import GHC.TypeError + +-- Easy version + +class Cls a where + method :: a -> a -> a + +instance Unsatisfiable (Text "Not allowed for Bool") => (Cls Bool) + + +-- Trickier version + +class C a where + {-# MINIMAL (method1, method3, method4) | (method2, method3, method4) | (method1, method2, method4) #-} + method1 :: a -> a + method1 = method2 + method2 :: a -> a + method2 = method1 + method3 :: a -> a + method3 = method2 . method1 + + method4 :: a -> a -> a + +instance Unsatisfiable (Text "Not allowed for Int") => (C Int) where + method3 = error "not implemented" diff --git a/testsuite/tests/unsatisfiable/UnsatDefault.hs b/testsuite/tests/unsatisfiable/UnsatDefault.hs new file mode 100644 index 0000000000..5593fa092e --- /dev/null +++ b/testsuite/tests/unsatisfiable/UnsatDefault.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DefaultSignatures #-} + +module UnsatDefault where + +import GHC.TypeError + +class C a where + method :: a + default method :: Unsatisfiable (Text "Please define the method manually. You can try...") => a + method = unsatisfiable + + +instance C Int diff --git a/testsuite/tests/unsatisfiable/UnsatDefault.stderr b/testsuite/tests/unsatisfiable/UnsatDefault.stderr new file mode 100644 index 0000000000..b4db515840 --- /dev/null +++ b/testsuite/tests/unsatisfiable/UnsatDefault.stderr @@ -0,0 +1,6 @@ + +UnsatDefault.hs:14:10: error: [GHC-22250] + • Please define the method manually. You can try... + • In the expression: UnsatDefault.$dmmethod @(Int) + In an equation for ‘method’: method = UnsatDefault.$dmmethod @(Int) + In the instance declaration for ‘C Int’ diff --git a/testsuite/tests/unsatisfiable/UnsatDefer.hs b/testsuite/tests/unsatisfiable/UnsatDefer.hs new file mode 100644 index 0000000000..8169fc2483 --- /dev/null +++ b/testsuite/tests/unsatisfiable/UnsatDefer.hs @@ -0,0 +1,23 @@ +{-# LANGUAGE DataKinds #-} + +{-# OPTIONS_GHC -Wno-deferred-type-errors #-} + +module Main where + +import GHC.TypeError + +-- This test makes sure we don't end up with duplication of error messages +-- when adding Unsatisfiable contexts to classes with superclasses. + +-- Test 1: we add an Unsatisfiable context to both the class and its superclass. + +class ReflexiveEq a where + reflexiveEq :: a -> a -> Bool + +type DoubleMsg = Text "Equality is not reflexive on Double" +instance Unsatisfiable DoubleMsg => ReflexiveEq Double + +foo = reflexiveEq 0 (0 :: Double) + +main :: IO () +main = print foo diff --git a/testsuite/tests/unsatisfiable/UnsatDefer.stderr b/testsuite/tests/unsatisfiable/UnsatDefer.stderr new file mode 100644 index 0000000000..fa802c3b3d --- /dev/null +++ b/testsuite/tests/unsatisfiable/UnsatDefer.stderr @@ -0,0 +1,5 @@ +UnsatDefer.exe: UnsatDefer.hs:20:7: error: [GHC-22250] + • Equality is not reflexive on Double + • In the expression: reflexiveEq 0 (0 :: Double) + In an equation for ‘foo’: foo = reflexiveEq 0 (0 :: Double) +(deferred type error) diff --git a/testsuite/tests/unsatisfiable/UnsatFunDeps.hs b/testsuite/tests/unsatisfiable/UnsatFunDeps.hs new file mode 100644 index 0000000000..1abf8910af --- /dev/null +++ b/testsuite/tests/unsatisfiable/UnsatFunDeps.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE UndecidableInstances #-} + +module UnsatFunDeps where + +import GHC.TypeError + +class C a b | a -> b +instance Unsatisfiable (Text "No") => C a b diff --git a/testsuite/tests/unsatisfiable/UnsatInstance.hs b/testsuite/tests/unsatisfiable/UnsatInstance.hs new file mode 100644 index 0000000000..c95089cb17 --- /dev/null +++ b/testsuite/tests/unsatisfiable/UnsatInstance.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE DataKinds #-} + +module UnsatInstance where + +import GHC.TypeError + +instance Unsatisfiable (Text "hello") diff --git a/testsuite/tests/unsatisfiable/UnsatInstance.stderr b/testsuite/tests/unsatisfiable/UnsatInstance.stderr new file mode 100644 index 0000000000..d79574e73b --- /dev/null +++ b/testsuite/tests/unsatisfiable/UnsatInstance.stderr @@ -0,0 +1,4 @@ + +UnsatInstance.hs:7:10: error: [GHC-97044] + • Class ‘Unsatisfiable’ does not support user-specified instances. + • In the instance declaration for ‘Unsatisfiable (Text "hello")’ diff --git a/testsuite/tests/unsatisfiable/UnsatPMWarnings.hs b/testsuite/tests/unsatisfiable/UnsatPMWarnings.hs new file mode 100644 index 0000000000..13a6ee3e6e --- /dev/null +++ b/testsuite/tests/unsatisfiable/UnsatPMWarnings.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} + +module UnsatPMWarnings where + +import Data.Kind +import Data.Void +import GHC.TypeError + +data MyGADT a where + MyInt :: MyGADT Int + +type IsBool :: Type -> Constraint +type family IsBool a where + IsBool Bool = () + IsBool a = Unsatisfiable (Text "Must be Bool") + +foo :: IsBool a => MyGADT a -> Void +foo x = case x of {} diff --git a/testsuite/tests/unsatisfiable/Unsatisfiable1.hs b/testsuite/tests/unsatisfiable/Unsatisfiable1.hs new file mode 100644 index 0000000000..357cd296a1 --- /dev/null +++ b/testsuite/tests/unsatisfiable/Unsatisfiable1.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE DataKinds #-} + +module Unsatisfiable1 where + +import GHC.TypeError ( Unsatisfiable, unsatisfiable, ErrorMessage(Text) ) + +type Msg = Text "Cannot call 'uncallable'." + +uncallable :: Unsatisfiable Msg => () +uncallable = unsatisfiable @Msg + +uncallable' :: Unsatisfiable Msg => () +uncallable' = uncallable + +------------------------------------- + +unusual :: Unsatisfiable Msg => Char +unusual = 42 -- no error + +k :: Unsatisfiable (Text "No") => () +k = uncallable -- no error diff --git a/testsuite/tests/unsatisfiable/Unsatisfiable2.hs b/testsuite/tests/unsatisfiable/Unsatisfiable2.hs new file mode 100644 index 0000000000..88241a7e46 --- /dev/null +++ b/testsuite/tests/unsatisfiable/Unsatisfiable2.hs @@ -0,0 +1,22 @@ +{-# LANGUAGE DataKinds #-} + +module Unsatisfiable2 where + +import GHC.TypeError +import Data.Type.Bool ( If ) +import Data.Kind +import Data.Proxy + + +type ExpectTrue x = If x (() :: Constraint) (Unsatisfiable (Text "Input was False!")) + +h1 :: ExpectTrue x => proxy x -> () +h1 _ = () + +h2 :: If x (() :: Constraint) (Unsatisfiable (Text "Input was False!")) => proxy x -> () +h2 _ = () + +eg11 _ = h1 (Proxy @True) +eg12 p = h1 p +eg21 _ = h2 (Proxy @True) +eg22 p = h2 p diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail1.hs b/testsuite/tests/unsatisfiable/UnsatisfiableFail1.hs new file mode 100644 index 0000000000..70e2b78ac5 --- /dev/null +++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail1.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE DataKinds #-} + +module UnsatisfiableFail1 where + +import GHC.TypeError + +type Msg = Text "Cannot call 'uncallable'." + +uncallable :: Unsatisfiable Msg => () +uncallable = unsatisfiable @Msg + +rejected = uncallable diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail1.stderr b/testsuite/tests/unsatisfiable/UnsatisfiableFail1.stderr new file mode 100644 index 0000000000..9babaf7aea --- /dev/null +++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail1.stderr @@ -0,0 +1,5 @@ + +UnsatisfiableFail1.hs:12:12: error: [GHC-22250] + • Cannot call 'uncallable'. + • In the expression: uncallable + In an equation for ‘rejected’: rejected = uncallable diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail2.hs b/testsuite/tests/unsatisfiable/UnsatisfiableFail2.hs new file mode 100644 index 0000000000..07309c25a4 --- /dev/null +++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail2.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE DataKinds #-} + +module UnsatisfiableFail2 where + +import GHC.TypeError +import Data.Type.Bool ( If ) +import Data.Kind +import Data.Proxy + +type ExpectTrue x = If x (() :: Constraint) (Unsatisfiable (Text "Input was False!")) + +h :: ExpectTrue x => proxy x -> () +h _ = () + +eg3 _ = h (Proxy @False) -- error diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail2.stderr b/testsuite/tests/unsatisfiable/UnsatisfiableFail2.stderr new file mode 100644 index 0000000000..04c9574f49 --- /dev/null +++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail2.stderr @@ -0,0 +1,5 @@ + +UnsatisfiableFail2.hs:15:9: error: [GHC-22250] + • Input was False! + • In the expression: h (Proxy @False) + In an equation for ‘eg3’: eg3 _ = h (Proxy @False) diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail3.hs b/testsuite/tests/unsatisfiable/UnsatisfiableFail3.hs new file mode 100644 index 0000000000..90befcd5a9 --- /dev/null +++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail3.hs @@ -0,0 +1,43 @@ +{-# LANGUAGE DataKinds #-} + +module UnsatisfiableFail3 where + +import GHC.TypeError + + +-- This test makes sure we don't end up with duplication of error messages +-- when adding Unsatisfiable contexts to classes with superclasses. + +-- Test 1: we add an Unsatisfiable context to both the class and its superclass. + +class Eq a => ReflexiveEq a where + reflexiveEq :: a -> a -> Bool + reflexiveEq = (==) + +instance Unsatisfiable (Text "Can't compare functions with (==)") => Eq (a -> b) where + (==) = unsatisfiable + +instance Unsatisfiable (Text "Can't compare functions with reflexiveEq") => ReflexiveEq (a -> b) + +type DoubleMsg = Text "Equality is not reflexive on Double" +instance Unsatisfiable DoubleMsg => ReflexiveEq Double where + reflexiveEq = unsatisfiable @DoubleMsg + +foo = reflexiveEq 0 (0 :: Double) + +bar = reflexiveEq (\ (x :: Int) -> x + 1) + + +-- Test 2: we add an Unsatisfiable context to the class, but not the superclass. + +class Eq a => ReflexiveEq' a where + reflexiveEq' :: a -> a -> Bool + reflexiveEq' = (==) + +instance Unsatisfiable (Text "Can't compare functions with reflexiveEq'") => ReflexiveEq' (a -> b) +instance Unsatisfiable DoubleMsg => ReflexiveEq' Double where + reflexiveEq' = unsatisfiable @DoubleMsg + +foo' = reflexiveEq' 0 (0 :: Double) + +bar' = reflexiveEq' (\ (x :: Int) -> x + 1) diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail3.stderr b/testsuite/tests/unsatisfiable/UnsatisfiableFail3.stderr new file mode 100644 index 0000000000..5db0db1c04 --- /dev/null +++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail3.stderr @@ -0,0 +1,21 @@ + +UnsatisfiableFail3.hs:26:7: error: [GHC-22250] + • Equality is not reflexive on Double + • In the expression: reflexiveEq 0 (0 :: Double) + In an equation for ‘foo’: foo = reflexiveEq 0 (0 :: Double) + +UnsatisfiableFail3.hs:28:7: error: [GHC-22250] + • Can't compare functions with reflexiveEq + • In the expression: reflexiveEq (\ (x :: Int) -> x + 1) + In an equation for ‘bar’: bar = reflexiveEq (\ (x :: Int) -> x + 1) + +UnsatisfiableFail3.hs:41:8: error: [GHC-22250] + • Equality is not reflexive on Double + • In the expression: reflexiveEq' 0 (0 :: Double) + In an equation for ‘foo'’: foo' = reflexiveEq' 0 (0 :: Double) + +UnsatisfiableFail3.hs:43:8: error: [GHC-22250] + • Can't compare functions with reflexiveEq' + • In the expression: reflexiveEq' (\ (x :: Int) -> x + 1) + In an equation for ‘bar'’: + bar' = reflexiveEq' (\ (x :: Int) -> x + 1) diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail4.hs b/testsuite/tests/unsatisfiable/UnsatisfiableFail4.hs new file mode 100644 index 0000000000..070c621d4e --- /dev/null +++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail4.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE DataKinds, PartialTypeSignatures #-} + +module UnsatisfiableFail4 where + +import GHC.TypeError + +data D = MkD + +-- Check that we don't try to solve errors in kinds using Unsatisfiable. + +instance Unsatisfiable (Text "msg") => Eq D where + _ == _ = let y :: Maybe Maybe + y = unsatisfiable + in unsatisfiable + +instance Unsatisfiable (Text "msg") => Ord D where + compare _ _ + = let y :: _ => Maybe Maybe + y = unsatisfiable + in unsatisfiable diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail4.stderr b/testsuite/tests/unsatisfiable/UnsatisfiableFail4.stderr new file mode 100644 index 0000000000..5ce4735a42 --- /dev/null +++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail4.stderr @@ -0,0 +1,22 @@ + +UnsatisfiableFail4.hs:12:27: error: [GHC-83865] + • Expecting one more argument to ‘Maybe’ + Expected a type, but ‘Maybe’ has kind ‘* -> *’ + • In the first argument of ‘Maybe’, namely ‘Maybe’ + In the type signature: y :: Maybe Maybe + In the expression: + let + y :: Maybe Maybe + y = unsatisfiable + in unsatisfiable + +UnsatisfiableFail4.hs:18:27: error: [GHC-83865] + • Expecting one more argument to ‘Maybe’ + Expected a type, but ‘Maybe’ has kind ‘* -> *’ + • In the first argument of ‘Maybe’, namely ‘Maybe’ + In the type signature: y :: _ => Maybe Maybe + In the expression: + let + y :: _ => Maybe Maybe + y = unsatisfiable + in unsatisfiable diff --git a/testsuite/tests/unsatisfiable/all.T b/testsuite/tests/unsatisfiable/all.T new file mode 100644 index 0000000000..2358c7eabc --- /dev/null +++ b/testsuite/tests/unsatisfiable/all.T @@ -0,0 +1,19 @@ + +test('Unsatisfiable1', normal, compile, ['']) +test('Unsatisfiable2', normal, compile, ['']) +test('UnsatisfiableFail1', normal, compile_fail, ['']) +test('UnsatisfiableFail2', normal, compile_fail, ['']) +test('UnsatisfiableFail3', normal, compile_fail, ['']) +test('UnsatisfiableFail4', normal, compile_fail, ['']) + +test('UnsatClassMethods', normal, compile, ['-Werror=missing-methods']) +test('UnsatDefault', normal, compile_fail, ['']) +test('UnsatDefer', exit_code(1), compile_and_run, ['-fdefer-type-errors']) +test('UnsatFunDeps', normal, compile, ['']) +test('UnsatInstance', normal, compile_fail, ['']) +test('UnsatPMWarnings', normal, compile, ['-Woverlapping-patterns -Wincomplete-patterns']) + +test('T11503_Unsat', normal, compile, ['-Woverlapping-patterns -Wincomplete-patterns']) +test('T14141_Unsat', normal, compile, ['-Woverlapping-patterns -Wincomplete-patterns']) +test('T14339_Unsat', normal, compile_fail, ['']) +test('T15232_Unsat', normal, compile, ['-Wredundant-constraints']) -- cgit v1.2.1