Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: ba210d98 by Simon Peyton Jones at 2025-09-08T16:26:36+01:00 Report solid equality errors before custom errors This MR fixes #26255 by * Reporting solid equality errors like Int ~ Bool before "custom type errors". See comments in `report1` in `reportWanteds` * Suppressing errors that arise from superclasses of Wanteds. See (SCE1) in Note [Suppressing confusing errors] More details in #26255. - - - - - 15 changed files: - compiler/GHC/Core/Type.hs - compiler/GHC/Core/Unify.hs - compiler/GHC/HsToCore/Pmc/Solver.hs - compiler/GHC/Tc/Errors.hs - compiler/GHC/Tc/Types/Constraint.hs - compiler/GHC/Tc/Utils/TcType.hs - testsuite/tests/typecheck/should_fail/T18851.hs - + testsuite/tests/typecheck/should_fail/T26255a.hs - + testsuite/tests/typecheck/should_fail/T26255a.stderr - + testsuite/tests/typecheck/should_fail/T26255b.hs - + testsuite/tests/typecheck/should_fail/T26255b.stderr - + testsuite/tests/typecheck/should_fail/T26255c.hs - + testsuite/tests/typecheck/should_fail/T26255c.stderr - testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr - testsuite/tests/typecheck/should_fail/all.T Changes: ===================================== compiler/GHC/Core/Type.hs ===================================== @@ -132,7 +132,7 @@ module GHC.Core.Type ( kindBoxedRepLevity_maybe, mightBeLiftedType, mightBeUnliftedType, definitelyLiftedType, definitelyUnliftedType, - isAlgType, isDataFamilyAppType, + isAlgType, isDataFamilyApp, isSatTyFamApp, isPrimitiveType, isStrictType, isTerminatingType, isLevityTy, isLevityVar, isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy, @@ -2292,6 +2292,21 @@ isFamFreeTy (ForAllTy _ ty) = isFamFreeTy ty isFamFreeTy (CastTy ty _) = isFamFreeTy ty isFamFreeTy (CoercionTy _) = False -- Not sure about this +-- | Check whether a type is a data family type +isDataFamilyApp :: Type -> Bool +isDataFamilyApp ty = case tyConAppTyCon_maybe ty of + Just tc -> isDataFamilyTyCon tc + _ -> False + +isSatTyFamApp :: Type -> Maybe (TyCon, [Type]) +-- Return the argument if we have a saturated type family application +-- Why saturated? See (ATF4) in Note [Apartness and type families] +isSatTyFamApp (TyConApp tc tys) + | isTypeFamilyTyCon tc + && not (tys `lengthExceeds` tyConArity tc) -- Not over-saturated + = Just (tc, tys) +isSatTyFamApp _ = Nothing + buildSynTyCon :: Name -> [KnotTied TyConBinder] -> Kind -- ^ /result/ kind -> [Role] -> KnotTied Type -> TyCon -- This function is here because here is where we have @@ -2459,12 +2474,6 @@ isAlgType ty isAlgTyCon tc _other -> False --- | Check whether a type is a data family type -isDataFamilyAppType :: Type -> Bool -isDataFamilyAppType ty = case tyConAppTyCon_maybe ty of - Just tc -> isDataFamilyTyCon tc - _ -> False - -- | Computes whether an argument (or let right hand side) should -- be computed strictly or lazily, based only on its type. -- Currently, it's just 'isUnliftedType'. ===================================== compiler/GHC/Core/Unify.hs ===================================== @@ -1741,8 +1741,8 @@ unify_ty env ty1 ty2 kco where mb_tc_app1 = splitTyConApp_maybe ty1 mb_tc_app2 = splitTyConApp_maybe ty2 - mb_sat_fam_app1 = isSatFamApp ty1 - mb_sat_fam_app2 = isSatFamApp ty2 + mb_sat_fam_app1 = isSatTyFamApp ty1 + mb_sat_fam_app2 = isSatTyFamApp ty2 unify_ty _ _ _ _ = surelyApart @@ -1801,16 +1801,6 @@ unify_tys env orig_xs orig_ys -- Possibly different saturations of a polykinded tycon -- See Note [Polykinded tycon applications] ---------------------------------- -isSatFamApp :: Type -> Maybe (TyCon, [Type]) --- Return the argument if we have a saturated type family application --- Why saturated? See (ATF4) in Note [Apartness and type families] -isSatFamApp (TyConApp tc tys) - | isTypeFamilyTyCon tc - && not (tys `lengthExceeds` tyConArity tc) -- Not over-saturated - = Just (tc, tys) -isSatFamApp _ = Nothing - --------------------------------- uVarOrFam :: UMEnv -> CanEqLHS -> InType -> OutCoercion -> UM () -- Invariants: (a) If ty1 is a TyFamLHS, then ty2 is NOT a TyVarTy @@ -1927,7 +1917,7 @@ uVarOrFam env ty1 ty2 kco | otherwise -> maybeApart MARTypeFamily -- Check for equality F tys1 ~ F tys2 - | Just (tc2, tys2) <- isSatFamApp ty2 + | Just (tc2, tys2) <- isSatTyFamApp ty2 , tc1 == tc2 = go_fam_fam substs tc1 tys1 tys2 kco ===================================== compiler/GHC/HsToCore/Pmc/Solver.hs ===================================== @@ -363,7 +363,7 @@ pmTopNormaliseType (TySt _ inert) typ = {-# SCC "pmTopNormaliseType" #-} do eq_src_ty ty tys = maybe ty id (find is_closed_or_data_family tys) is_closed_or_data_family :: Type -> Bool - is_closed_or_data_family ty = pmIsClosedType ty || isDataFamilyAppType ty + is_closed_or_data_family ty = pmIsClosedType ty || isDataFamilyApp ty -- For efficiency, represent both lists as difference lists. -- comb performs the concatenation, for both lists. ===================================== compiler/GHC/Tc/Errors.hs ===================================== @@ -439,10 +439,9 @@ reportBadTelescope _ _ skol_info skols -- See Note [Constraints to ignore]. ignoreConstraint :: Ct -> Bool ignoreConstraint ct - | AssocFamPatOrigin <- ctOrigin ct - = True - | otherwise - = False + = case ctOrigin ct of + AssocFamPatOrigin -> True -- See (CIG1) + _ -> False -- | Makes an error item from a constraint, calculating whether or not -- the item should be suppressed. See Note [Wanteds rewrite Wanteds] @@ -538,15 +537,15 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics ; when (null simples) $ reportMultiplicityCoercionErrs ctxt_for_insols mult_co_errs -- See Note [Suppressing confusing errors] - ; let (suppressed_items, items0) = partition suppress tidy_items + ; let (suppressed_items, reportable_items) = partition suppressItem tidy_items ; traceTc "reportWanteds suppressed:" (ppr suppressed_items) - ; (ctxt1, items1) <- tryReporters ctxt_for_insols report1 items0 + ; (ctxt1, items1) <- tryReporters ctxt_for_insols report1 reportable_items -- Now all the other constraints. We suppress errors here if -- any of the first batch failed, or if the enclosing context -- says to suppress ; let ctxt2 = ctxt1 { cec_suppress = cec_suppress ctxt || cec_suppress ctxt1 } - ; (ctxt3, leftovers) <- tryReporters ctxt2 report2 items1 + ; (_, leftovers) <- tryReporters ctxt2 report2 items1 ; massertPpr (null leftovers) (text "The following unsolved Wanted constraints \ \have not been reported to the user:" @@ -557,12 +556,16 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics -- wanted insoluble here; but do suppress inner insolubles -- if there's a *given* insoluble here (= inaccessible code) - -- Only now, if there are no errors, do we report suppressed ones - -- See Note [Suppressing confusing errors] - -- We don't need to update the context further because of the - -- whenNoErrs guard - ; whenNoErrs $ - do { (_, more_leftovers) <- tryReporters ctxt3 report3 suppressed_items + -- If there are no other errors to report, report suppressed errors. + -- See Note [Suppressing confusing errors]. NB: with -fdefer-type-errors + -- we might have reported warnings only from `reportable_items`, but we + -- still want to suppress the `suppressed_items`. + ; when (null reportable_items) $ + do { (_, more_leftovers) <- tryReporters ctxt_for_insols (report1++report2) + suppressed_items + -- ctxt_for_insols: the suppressed errors can be Int~Bool, which + -- will have made the incoming `ctxt` be True; don't make that + -- suppress the Int~Bool error! ; massertPpr (null more_leftovers) (ppr more_leftovers) } } where env = cec_tidy ctxt @@ -585,29 +588,42 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics DE_Multiplicity mult_co loc -> (es1, es2, es3, (mult_co, loc):es4) - -- See Note [Suppressing confusing errors] - suppress :: ErrorItem -> Bool - suppress item - | Wanted <- ei_flavour item - = is_ww_fundep_item item - | otherwise - = False - -- report1: ones that should *not* be suppressed by -- an insoluble somewhere else in the tree -- It's crucial that anything that is considered insoluble -- (see GHC.Tc.Utils.insolublWantedCt) is caught here, otherwise -- 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) + report1 = [ -- We put implicit lifting errors first, because are solid errors + -- See "Implicit lifting" in GHC.Tc.Gen.Splice + -- Note [Lifecycle of an untyped splice, and PendingRnSplice] + ("implicit lifting", is_implicit_lifting, True, mkImplicitLiftingReporter) - , ("implicit lifting", is_implicit_lifting, True, mkImplicitLiftingReporter) + -- Next, solid equality errors , given_eq_spec , ("insoluble2", utterly_wrong, True, mkGroupReporter mkEqErr) , ("skolem eq1", very_wrong, True, mkSkolReporter) , ("FixedRuntimeRep", is_FRR, True, mkGroupReporter mkFRRErr) , ("skolem eq2", skolem_eq, True, mkSkolReporter) + + -- Next, custom type errors + -- See Note [Custom type errors in constraints] in GHC.Tc.Types.Constraint + -- + -- Put custom type errors /after/ solid equality errors. In #26255 we + -- had a custom error (T <= F alpha) which was suppressing a far more + -- informative (K Int ~ [K alpha]). That mismatch between K and [] is + -- definitely wrong; and if it was fixed we'd know alpha:=Int, and hence + -- perhaps be able to solve T <= F alpha, by reducing F Int. + -- + -- But put custom type errors /before/ "non-tv eq", because if we have + -- () ~ TypeError blah + -- we want to report it as a custom error, /not/ as a mis-match + -- between TypeError and ()! Also see the Assert example + -- in Note [Custom type errors in constraints] + , ("custom_error", is_user_type_error, True, mkUserTypeErrorReporter) + -- (Handles TypeError and Unsatisfiable) + + -- "non-tv-eq": equalities (ty1 ~ ty2) where ty1 is not a tyvar , ("non-tv eq", non_tv_eq, True, mkSkolReporter) -- The only remaining equalities are alpha ~ ty, @@ -617,6 +633,7 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics -- See Note [Equalities with heterogeneous kinds] in GHC.Tc.Solver.Equality , ("Homo eqs", is_homo_equality, True, mkGroupReporter mkEqErr) , ("Other eqs", is_equality, True, mkGroupReporter mkEqErr) + ] -- report2: we suppress these if there are insolubles elsewhere in the tree @@ -625,11 +642,6 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics , ("Dicts", is_dict, False, mkGroupReporter mkDictErr) , ("Quantified", is_qc, False, mkGroupReporter mkQCErr) ] - -- report3: suppressed errors should be reported as categorized by either report1 - -- or report2. Keep this in sync with the suppress function above - report3 = [ ("wanted/wanted fundeps", is_ww_fundep, True, mkGroupReporter mkEqErr) - ] - -- rigid_nom_eq, rigid_nom_tv_eq, is_dict, is_equality, is_ip, is_FRR, is_irred :: ErrorItem -> Pred -> Bool @@ -690,10 +702,6 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics is_qc _ (ForAllPred {}) = True is_qc _ _ = False - -- See situation (1) of Note [Suppressing confusing errors] - is_ww_fundep item _ = is_ww_fundep_item item - is_ww_fundep_item = isWantedWantedFunDepOrigin . errorItemOrigin - given_eq_spec -- See Note [Given errors] | has_gadt_match_here = ("insoluble1a", is_given_eq, True, mkGivenErrorReporter) @@ -719,6 +727,16 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics = has_gadt_match implics --------------- +suppressItem :: ErrorItem -> Bool + -- See Note [Suppressing confusing errors] +suppressItem item + | Wanted <- ei_flavour item + , let orig = errorItemOrigin item + = isWantedSuperclassOrigin orig -- See (SCE1) + || isWantedWantedFunDepOrigin orig -- See (SCE2) + | otherwise + = False + isSkolemTy :: TcLevel -> Type -> Bool -- The type is a skolem tyvar isSkolemTy tc_lvl ty @@ -741,9 +759,25 @@ isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of Certain errors we might encounter are potentially confusing to users. If there are any other errors to report, at all, we want to suppress these. -Which errors (only 1 case right now): - -1) Errors which arise from the interaction of two Wanted fun-dep constraints. +Which errors are suppressed? + +(SCE1) Superclasses of Wanteds. These are generated only in case they trigger functional + dependencies. If such a constraint is unsolved, then its "parent" constraint must + also be unsolved, and is much more informative to the user. Example (#26255): + class (MinVersion <= F era) => Era era where { ... } + f :: forall era. EraFamily era -> IO () + f = ..blah... -- [W] Era era + Here we have simply omitted "Era era =>" from f's type. But we'll end up with + /two/ Wanted constraints: + [W] d1 : Era era + [W] d2 : MinVersion <= F era -- Superclass of d1 + We definitely want to report d1 and not d2! Happily it's easy to filter out those + superclass-Wanteds, becuase their Origin betrays them. + + See test T18851 for an example of how it is (just, barely) possible for the /only/ + errors to be superclass-of-Wanted constraints. + +(SCE2) Errors which arise from the interaction of two Wanted fun-dep constraints. Example: class C a b | a -> b where @@ -786,7 +820,7 @@ they will remain unfilled, and might have been used to rewrite another constrain Currently, the constraints to ignore are: -1) Constraints generated in order to unify associated type instance parameters +(CIG1) Constraints generated in order to unify associated type instance parameters with class parameters. Here are two illustrative examples: class C (a :: k) where @@ -814,6 +848,9 @@ Currently, the constraints to ignore are: If there is any trouble, checkValidFamInst bleats, aborting compilation. +(Note: Aug 25: this seems a rather tricky corner; + c.f. Note [Suppressing confusing errors]) + 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-un...). ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -903,75 +903,6 @@ isWantedCt = isWanted . ctEvidence isGivenCt :: Ct -> Bool isGivenCt = isGiven . ctEvidence -{- Note [Custom type errors in constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -When GHC reports a type-error about an unsolved-constraint, we check -to see if the constraint contains any custom-type errors, and if so -we report them. Here are some examples of constraints containing type -errors: - -TypeError msg -- The actual constraint is a type error - -TypError msg ~ Int -- Some type was supposed to be Int, but ended up - -- being a type error instead - -Eq (TypeError msg) -- A class constraint is stuck due to a type error - -F (TypeError msg) ~ a -- A type function failed to evaluate due to a type err - -It is also possible to have constraints where the type error is nested deeper, -for example see #11990, and also: - -Eq (F (TypeError msg)) -- Here the type error is nested under a type-function - -- call, which failed to evaluate because of it, - -- and so the `Eq` constraint was unsolved. - -- This may happen when one function calls another - -- and the called function produced a custom type error. --} - --- | 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 ErrorMsgType -getUserTypeErrorMsg pred = msum $ userTypeError_maybe pred - : map getUserTypeErrorMsg (subTys pred) - where - -- Richard thinks this function is very broken. What is subTys - -- supposed to be doing? Why are exactly-saturated tyconapps special? - -- What stops this from accidentally ripping apart a call to TypeError? - subTys t = case splitAppTys t of - (t,[]) -> - case splitTyConApp_maybe t of - Nothing -> [] - Just (_,ts) -> ts - (t,ts) -> t : ts - --- | 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 dict_ct) = isPendingScDictCt dict_ct isPendingScDict _ = False @@ -1413,6 +1344,93 @@ variable masquerading as expression holes IS treated as truly insoluble, so that it trumps other errors during error reporting. Yuk! +-} + +{- ********************************************************************* +* * + Custom type errors: Unsatisfiable and TypeError +* * +********************************************************************* -} + +{- Note [Custom type errors in constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When GHC reports a type-error about an unsolved-constraint, we check +to see if the constraint contains any custom-type errors, and if so +we report them. Here are some examples of constraints containing type +errors: + + TypeError msg -- The actual constraint is a type error + + TypError msg ~ Int -- Some type was supposed to be Int, but ended up + -- being a type error instead + + Eq (TypeError msg) -- A class constraint is stuck due to a type error + + F (TypeError msg) ~ a -- A type function failed to evaluate due to a type err + +It is also possible to have constraints where the type error is nested deeper, +for example see #11990, and also: + + Eq (F (TypeError msg)) -- Here the type error is nested under a type-function + -- call, which failed to evaluate because of it, + -- and so the `Eq` constraint was unsolved. + -- This may happen when one function calls another + -- and the called function produced a custom type error. + +A good use-case is described in "Detecting the undetectable" + https://blog.csongor.co.uk/report-stuck-families/ +which features + type family Assert (err :: Constraint) (break :: Type -> Type) (a :: k) :: k where + Assert _ Dummy _ = Any + Assert _ _ k = k +and an unsolved constraint like + Assert (TypeError ...) (F ty1) ty1 ~ ty2 +that reports that (F ty1) remains stuck. +-} + +-- | 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 ErrorMsgType +getUserTypeErrorMsg pred = msum $ userTypeError_maybe pred + : map getUserTypeErrorMsg (subTys pred) + where + -- Richard thinks this function is very broken. What is subTys + -- supposed to be doing? Why are exactly-saturated tyconapps special? + -- What stops this from accidentally ripping apart a call to TypeError? + subTys t = case splitAppTys t of + (t,[]) -> + case splitTyConApp_maybe t of + Nothing -> [] + Just (_,ts) -> ts + (t,ts) -> t : ts + +-- | 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 + +{- ************************************************************************ * * Implication constraints ===================================== compiler/GHC/Tc/Utils/TcType.hs ===================================== @@ -2090,6 +2090,7 @@ isRigidTy ty | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal | Just {} <- tcSplitAppTy_maybe ty = True | isForAllTy ty = True + | Just {} <- isLitTy ty = True | otherwise = False {- ===================================== testsuite/tests/typecheck/should_fail/T18851.hs ===================================== @@ -33,3 +33,14 @@ f = show (undefined :: c) -- blows up at run time once type checks g :: String g = f @A @B + +{- +[W] Show c, Num int, C int A, C int B, C int c +Superclasses + C_FD int ~ A + C_FD int ~ B + C_FD int ~ c +--> + C_FD int ~ B + B ~ A +-} ===================================== testsuite/tests/typecheck/should_fail/T26255a.hs ===================================== @@ -0,0 +1,47 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE UndecidableSuperClasses #-} + +module T26255a where + +import Data.Proxy +import GHC.TypeLits + +type MinVersion = 1 + +class + ( KnownNat (ProtVerLow era) + , MinVersion <= ProtVerLow era + , KnownSymbol (EraName era) + ) => + Era era + where + type EraName era = (r :: Symbol) | r -> era + + type ProtVerLow era :: Nat + + eraName :: Proxy era -> String + eraName _ = symbolVal (Proxy :: Proxy (EraName era)) + +data FooEra + +instance Era FooEra where + type EraName FooEra = "Foo" + type ProtVerLow FooEra = 1 + +data BarEra + +instance Era BarEra where + type EraName BarEra = "Bar" + type ProtVerLow BarEra = 2 + +fromEraName :: (Era era, EraName era ~ name) => Proxy (name :: Symbol) -> Proxy era +fromEraName _ = Proxy + +noCompileErrorMessage :: IO () +noCompileErrorMessage = putStrLn $ eraName $ fromEraName (Proxy :: Proxy "Bar") + +brokenCompileErrorMessage1 :: IO () +brokenCompileErrorMessage1 = putStrLn $ eraName $ fromEraName (Proxy :: Proxy "Blah") + ===================================== testsuite/tests/typecheck/should_fail/T26255a.stderr ===================================== @@ -0,0 +1,10 @@ +T26255a.hs:46:51: error: [GHC-18872] + • Couldn't match type ‘EraName era0’ with ‘"Blah"’ + arising from a use of ‘fromEraName’ + The type variable ‘era0’ is ambiguous + • In the second argument of ‘($)’, namely + ‘fromEraName (Proxy :: Proxy "Blah")’ + In the second argument of ‘($)’, namely + ‘eraName $ fromEraName (Proxy :: Proxy "Blah")’ + In the expression: + putStrLn $ eraName $ fromEraName (Proxy :: Proxy "Blah") ===================================== testsuite/tests/typecheck/should_fail/T26255b.hs ===================================== @@ -0,0 +1,46 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE UndecidableSuperClasses #-} + +module T26255b where + +import Data.Proxy +import GHC.TypeLits + +type MinVersion = 1 + +class + ( KnownNat (ProtVerLow era) + , MinVersion <= ProtVerLow era + , KnownSymbol (EraName era) + ) => + Era era + where + type EraName era = (r :: Symbol) | r -> era + + type ProtVerLow era :: Nat + + eraName :: Proxy era -> String + eraName _ = symbolVal (Proxy :: Proxy (EraName era)) + +data FooEra + +instance Era FooEra where + type EraName FooEra = "Foo" + type ProtVerLow FooEra = 1 + +data BarEra + +instance Era BarEra where + type EraName BarEra = "Bar" + type ProtVerLow BarEra = 2 + +fromEraName :: (Era era, EraName era ~ name) => Proxy (name :: Symbol) -> Proxy era +fromEraName _ = Proxy + +noCompileErrorMessage :: IO () +noCompileErrorMessage = putStrLn $ eraName $ fromEraName (Proxy :: Proxy "Bar") + +brokenCompileErrorMessage2 :: IO () +brokenCompileErrorMessage2 = putStrLn $ eraName $ head $ fromEraName (Proxy :: Proxy "Bar") ===================================== testsuite/tests/typecheck/should_fail/T26255b.stderr ===================================== @@ -0,0 +1,9 @@ +T26255b.hs:46:58: error: [GHC-83865] + • Couldn't match expected type: [Proxy era0] + with actual type: Proxy BarEra + • In the second argument of ‘($)’, namely + ‘fromEraName (Proxy :: Proxy "Bar")’ + In the second argument of ‘($)’, namely + ‘head $ fromEraName (Proxy :: Proxy "Bar")’ + In the second argument of ‘($)’, namely + ‘eraName $ head $ fromEraName (Proxy :: Proxy "Bar")’ ===================================== testsuite/tests/typecheck/should_fail/T26255c.hs ===================================== @@ -0,0 +1,30 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableSuperClasses #-} + +module T26255c where + +import Data.Kind +import Data.Proxy +import GHC.TypeLits + +type MinVersion = 1 + +class + ( KnownNat (ProtVerLow era) + , MinVersion <= ProtVerLow era + ) => + Era era + where + type ProtVerLow era :: Nat + +newtype EraFamily era = EraFamily Int + +class Era era => NewEra era where + eraFamilySize :: EraFamily era -> Int + +printEraFamilySize :: EraFamily era -> IO () +printEraFamilySize = print . eraFamilySize ===================================== testsuite/tests/typecheck/should_fail/T26255c.stderr ===================================== @@ -0,0 +1,11 @@ +T26255c.hs:30:30: error: [GHC-39999] + • No instance for ‘NewEra era’ + arising from a use of ‘eraFamilySize’ + Possible fix: + add (NewEra era) to the context of + the type signature for: + printEraFamilySize :: forall {k} (era :: k). EraFamily era -> IO () + • In the second argument of ‘(.)’, namely ‘eraFamilySize’ + In the expression: print . eraFamilySize + In an equation for ‘printEraFamilySize’: + printEraFamilySize = print . eraFamilySize ===================================== testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr ===================================== @@ -1,3 +1,7 @@ +UnliftedNewtypesFamilyKindFail2.hs:12:1: error: [GHC-83865] + • Expected a type, but ‘F 5’ has kind ‘5’ + • In the newtype family instance declaration for ‘F’ + UnliftedNewtypesFamilyKindFail2.hs:12:20: error: [GHC-83865] • Expected a type, but ‘5’ has kind ===================================== testsuite/tests/typecheck/should_fail/all.T ===================================== @@ -742,3 +742,5 @@ test('T25004', normal, compile_fail, ['']) test('T25004k', normal, compile_fail, ['']) test('T26004', normal, compile_fail, ['']) test('T26318', normal, compile_fail, ['']) +test('T26255a', normal, compile_fail, ['']) +test('T26255b', normal, compile_fail, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ba210d981b0812aea604f884d3c0aada... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ba210d981b0812aea604f884d3c0aada... You're receiving this email because of your account on gitlab.haskell.org.