August 2026 - ghc-commits

[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 4 commits: Better handling of serialisation of wired-in names
by Marge Bot (＠marge-bot) 23 Aug '26

23 Aug '26

Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC Commits: d2bc32aa by Simon Peyton Jones at 2026-08-21T12:59:26-04:00 Better handling of serialisation of wired-in names Fixes #27501 - - - - - d2795ffc by Alan Zimmerman at 2026-08-21T13:00:05-04:00 EPA: Remove NoEpTok/NoEpUniTok, using an unhelpful SrcSpan instead Also introduce helper functions noEpTok and noEpUniTok to serve as simple replacements in code inserting an token annotation without location information. - - - - - 27b5c6e7 by Andreas Klebinger at 2026-08-23T08:52:40-04:00 rts linker: Fix pointer arithmetic issue in flushInstructionCacheRISCV64 We accidentally operated over `uint64_t*` when we should use `uint8_t`. Fixes #27569 - - - - - 57b559a9 by Alan Zimmerman at 2026-08-23T08:52:41-04:00 EPA: Uses Parsers.parseModule for exactprint tests Parsers.parseModule is the advertised way to parse for use for exact printing in the ghc-exactprint library. This commit updates the GHC exact print testing to use it. This requires moving the comment balancing that was occurring only in the test path into the advertising parser path, so it moves from Transforms.hs to Utils.hs. Also update the comment adding to honour trailing annotations - - - - - 39 changed files: - compiler/GHC/Builtin.hs - compiler/GHC/Hs.hs - compiler/GHC/Hs/Dump.hs - compiler/GHC/Hs/Utils.hs - compiler/GHC/Iface/Binary.hs - compiler/GHC/Parser.y - compiler/GHC/Parser/Annotation.hs - compiler/GHC/Parser/PostProcess.hs - rts/linker/elf_reloc_riscv64.c - testsuite/tests/ghc-api/exactprint/T22919.stderr - testsuite/tests/ghc-api/exactprint/Test20239.stderr - testsuite/tests/ghc-api/exactprint/ZeroWidthSemi.stderr - testsuite/tests/haddock/should_compile_flag_haddock/T17544.stderr - testsuite/tests/haddock/should_compile_flag_haddock/T17544_kw.stderr - testsuite/tests/haddock/should_compile_flag_haddock/T24221.stderr - testsuite/tests/module/mod185.stderr - testsuite/tests/parser/should_compile/DumpParsedAst.stderr - testsuite/tests/parser/should_compile/DumpParsedAstComments.stderr - testsuite/tests/parser/should_compile/DumpRenamedAst.stderr - testsuite/tests/parser/should_compile/DumpSemis.stderr - testsuite/tests/parser/should_compile/DumpTypecheckedAst.stderr - testsuite/tests/parser/should_compile/KindSigs.stderr - testsuite/tests/parser/should_compile/T14189.stderr - testsuite/tests/parser/should_compile/T15323.stderr - testsuite/tests/parser/should_compile/T20452.stderr - testsuite/tests/parser/should_compile/T20718.stderr - testsuite/tests/parser/should_compile/T20718b.stderr - testsuite/tests/parser/should_compile/T20846.stderr - testsuite/tests/parser/should_compile/T23315/T23315.stderr - testsuite/tests/printer/AnnotationNoListTuplePuns.stdout - testsuite/tests/printer/T18791.stderr - testsuite/tests/printer/Test20297.stdout - testsuite/tests/printer/Test24533.stdout - utils/check-exact/ExactPrint.hs - utils/check-exact/Main.hs - utils/check-exact/Parsers.hs - utils/check-exact/Transform.hs - utils/check-exact/Utils.hs - utils/haddock/haddock-api/src/Haddock/Types.hs The diff was not included because it is too large. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f2adf12c140164ea6e31d39f485935… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f2adf12c140164ea6e31d39f485935… You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0

[Git][ghc/ghc][wip/sjakobi/T16836-implicit-field-strictness] Add -Wimplicit-field-strictness (#16836)
by Simon Jakobi (＠sjakobi) 23 Aug '26

23 Aug '26

Simon Jakobi pushed to branch wip/sjakobi/T16836-implicit-field-strictness at Glasgow Haskell Compiler / GHC Commits: d156d887 by Simon Jakobi at 2026-08-23T13:54:10+02:00 Add -Wimplicit-field-strictness (#16836) This opt-in warning fires when a data constructor field lacks an explicit strictness annotation (`!` or `~`). It complements the LazyFieldAnnotations extension (4762a8bf30f) from GHC proposal 752, which makes `~` annotations available for this purpose. Deciding which fields to report requires their levity, so the check runs after typechecking. To keep the noise down, the diagnostic is emitted once per data declaration, grouped by constructor. Closes #16836. Assisted-by: Claude Fable 5 - - - - - 20 changed files: - + changelog.d/implicit-field-strictness-warning - changelog.d/lazy-field-annotations - compiler/GHC/Driver/Flags.hs - compiler/GHC/Driver/Session.hs - compiler/GHC/Tc/Errors/Ppr.hs - compiler/GHC/Tc/Errors/Types.hs - compiler/GHC/Tc/TyCl.hs - compiler/GHC/Types/Error/Codes.hs - compiler/GHC/Types/Hint.hs - compiler/GHC/Types/Hint/Ppr.hs - docs/users_guide/exts/strict.rst - docs/users_guide/using-warnings.rst - + testsuite/tests/warnings/should_compile/T16836a.hs - + testsuite/tests/warnings/should_compile/T16836a.stderr - + testsuite/tests/warnings/should_compile/T16836b.hs - + testsuite/tests/warnings/should_compile/T16836c.hs - + testsuite/tests/warnings/should_compile/T16836c.stderr - + testsuite/tests/warnings/should_compile/T16836d.hs - + testsuite/tests/warnings/should_compile/T16836d.stderr - testsuite/tests/warnings/should_compile/all.T Changes: ===================================== changelog.d/implicit-field-strictness-warning ===================================== @@ -0,0 +1,10 @@ +section: compiler +synopsis: Add `-Wimplicit-field-strictness` +issues: #16836 +mrs: !16555 + +description: { + The new opt-in warning :ghc-flag:`-Wimplicit-field-strictness` reports + data constructor fields that lack an explicit strictness annotation + (``!`` or ``~``). +} ===================================== changelog.d/lazy-field-annotations ===================================== @@ -11,4 +11,7 @@ description: { continues to control the default strictness of unannotated fields. See `GHC Proposal #752 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0752-l…>`_. + + Also note the new opt-in :ghc-flag:`-Wimplicit-field-strictness` warning, which + reports fields lacking an explicit annotation. } ===================================== compiler/GHC/Driver/Flags.hs ===================================== @@ -1142,6 +1142,7 @@ data WarningFlag = | Opt_WarnUnrecognisedModifiers -- ^ @since 10.0 | Opt_WarnSemaphoreOpenFailure -- Since 10.0.1 | Opt_WarnDefaultedCallStack -- ^ @since 10.2 + | Opt_WarnImplicitFieldStrictness -- ^ @since 10.2 deriving (Eq, Ord, Show, Enum, Bounded) -- | Return the names of a WarningFlag @@ -1251,6 +1252,7 @@ warnFlagNames wflag = case wflag of Opt_WarnTypeEqualityRequiresOperators -> "type-equality-requires-operators" :| [] Opt_WarnMissingRoleAnnotations -> "missing-role-annotations" :| [] Opt_WarnImplicitRhsQuantification -> "implicit-rhs-quantification" :| [] + Opt_WarnImplicitFieldStrictness -> "implicit-field-strictness" :| [] Opt_WarnIncompleteExportWarnings -> "incomplete-export-warnings" :| [] Opt_WarnIncompleteRecordSelectors -> "incomplete-record-selectors" :| [] Opt_WarnBadlyLevelledTypes -> "badly-levelled-types" :| [] ===================================== compiler/GHC/Driver/Session.hs ===================================== @@ -2449,6 +2449,7 @@ wWarningFlagsDeps = [minBound..maxBound] >>= \x -> case x of Opt_WarnUnrecognisedModifiers -> warnSpec x Opt_WarnSemaphoreOpenFailure -> warnSpec x Opt_WarnDefaultedCallStack -> warnSpec x + Opt_WarnImplicitFieldStrictness -> warnSpec x warningGroupsDeps :: [(Deprecation, FlagSpec WarningGroup)] warningGroupsDeps = map mk warningGroups ===================================== compiler/GHC/Tc/Errors/Ppr.hs ===================================== @@ -1384,6 +1384,21 @@ instance Diagnostic TcRnMessage where hang (text "Missing role annotation" <> colon) 2 (text "type role" <+> ppr name <+> hsep (map ppr roles)) + TcRnImplicitFieldStrictness _lazy_anns cons -> mkSimpleDecorated $ + hang (text "These constructor fields lack an explicit strictness annotation" <> colon) + 2 (vcat (map ppr_con (NE.toList cons))) + where + ppr_con (con, fields) = + bullet <+> text "In" <+> quotes (ppr con) <> colon <+> ppr_fields (NE.toList fields) + ppr_fields fields + | let names = [n | ImplicitStrictnessRecField n <- fields] + , not (null names) + = text "field" <> plural names <+> quotedListWithAnd (map ppr names) + | otherwise + = let poss = [i | ImplicitStrictnessPosField i <- fields] + in text "field" <> plural poss + <+> unquotedListWith (text "and") (map int poss) + TcRnIllformedTypePattern p -> mkSimpleDecorated $ hang (text "Ill-formed type pattern:") 2 (ppr p) @@ -2693,6 +2708,8 @@ instance Diagnostic TcRnMessage where -> ErrorWithoutFlag TcRnMissingRoleAnnotation{} -> WarningWithFlag Opt_WarnMissingRoleAnnotations + TcRnImplicitFieldStrictness{} + -> WarningWithFlag Opt_WarnImplicitFieldStrictness TcRnIllegalInvisTyVarBndr{} -> ErrorWithoutFlag TcRnIllegalWildcardTyVarBndr{} @@ -3428,6 +3445,12 @@ instance Diagnostic TcRnMessage where -> noHints TcRnMissingRoleAnnotation{} -> noHints + TcRnImplicitFieldStrictness lazy_anns _ + -> SuggestExplicitFieldStrictness + : [ useExtensionInOrderTo + (text "to allow" <+> quotes (char '~') <+> text "annotations") + LangExt.LazyFieldAnnotations + | not lazy_anns ] TcRnIllegalInvisTyVarBndr{} -> [suggestExtension LangExt.TypeAbstractions] TcRnIllegalWildcardTyVarBndr{} ===================================== compiler/GHC/Tc/Errors/Types.hs ===================================== @@ -123,6 +123,7 @@ module GHC.Tc.Errors.Types ( , TypeSyntax(..) , typeSyntaxExtension , SuggestLinear(..) + , ImplicitStrictnessField(..) -- * Errors for hs-boot and signature files , BadBootDecls(..) @@ -4235,6 +4236,23 @@ data TcRnMessage where -} TcRnMissingRoleAnnotation :: Name -> [Role] -> TcRnMessage + + {-| TcRnImplicitFieldStrictness is a warning that occurs when a data + constructor field lacks an explicit strictness annotation (@!@ or @~@) + + Controlled by flags: + - Wimplicit-field-strictness + + Test cases: + T16836a, T16836b, T16836c, T16836d + + -} + TcRnImplicitFieldStrictness + :: Bool -- ^ whether @LazyFieldAnnotations@ is enabled + -> NonEmpty (Name, NonEmpty ImplicitStrictnessField) + -- ^ per data constructor, the fields lacking annotations + -> TcRnMessage + {-| TcRnPatersonCondFailure is an error that occurs when an instance declaration fails to conform to the Paterson conditions. Which particular condition fails depends on the constructor of PatersonCondFailure @@ -6399,6 +6417,14 @@ data PatSynInvalidRhsReason | PatSynUnboundVar !Name deriving (Generic) +-- | A constructor field lacking an explicit strictness annotation, as +-- reported by 'TcRnImplicitFieldStrictness'. +data ImplicitStrictnessField + -- | A record field + = ImplicitStrictnessRecField FieldLabelString + -- | A positional argument (1-based index) + | ImplicitStrictnessPosField Int + data BadFieldAnnotationReason where {-| A lazy data type field annotation (~) was used without enabling the extension LazyFieldAnnotations. ===================================== compiler/GHC/Tc/TyCl.hs ===================================== @@ -5022,6 +5022,16 @@ checkValidTyCon tc ; mapM_ (checkValidDataCon dflags ex_ok tc) data_cons ; mapM_ (checkPartialRecordField data_cons) (tyConFieldLabels tc) + ; warn_implicit_strictness <- woptM Opt_WarnImplicitFieldStrictness + ; when (warn_implicit_strictness + && not (isNewTyCon tc) + && not (isTypeDataTyCon tc)) $ + whenIsJust (NE.nonEmpty (mapMaybe conImplicitStrictnessFields data_cons)) $ + \offenders -> + do { lazy_anns <- xoptM LangExt.LazyFieldAnnotations + ; addDiagnosticTc $ + TcRnImplicitFieldStrictness lazy_anns offenders } + -- Check that fields with the same name share a type ; mapM_ check_fields groups }} where @@ -5072,6 +5082,29 @@ checkValidTyCon tc res2 = dataConOrigResTy con2 fty2 = dataConFieldType con2 lbl +-- | For a given data constructor, collect the fields to report for +-- @-Wimplicit-field-strictness@. +-- +-- Only fields whose type is known to be lifted are collected: unlifted +-- fields are unconditionally strict, and annotating one with @!@ or +-- @~@ would trigger @-Wredundant-strictness-flags@. +conImplicitStrictnessFields :: DataCon -> Maybe (Name, NonEmpty ImplicitStrictnessField) +conImplicitStrictnessFields con + | Just ne_fields <- NE.nonEmpty fields + = Just (dataConName con, ne_fields) + | otherwise + = Nothing + where + fld_refs = case dataConFieldLabels con of + [] -> map ImplicitStrictnessPosField [1..] + lbls -> map (ImplicitStrictnessRecField . flLabel) lbls + fields = [ ref + | (ref, arg_ty, HsSrcBang _ _ NoSrcStrict) + <- zip3 fld_refs + (map scaledThing (dataConOrigArgTys con)) + (dataConSrcBangs con) + , typeLevity_maybe arg_ty == Just Lifted ] + checkPartialRecordField :: [DataCon] -> FieldLabel -> TcM () -- Checks the partial record field selector, and warns. -- See Note [Checking partial record field] ===================================== compiler/GHC/Types/Error/Codes.hs ===================================== @@ -542,6 +542,7 @@ type family GhcDiagnosticCode c = n | n -> c where GhcDiagnosticCode "TcRnNegativeNumTypeLiteral" = 93632 GhcDiagnosticCode "TcRnUnusedQuantifiedTypeVar" = 54180 GhcDiagnosticCode "TcRnMissingRoleAnnotation" = 65490 + GhcDiagnosticCode "TcRnImplicitFieldStrictness" = 47032 GhcDiagnosticCode "TcRnUntickedPromotedThing" = 49957 GhcDiagnosticCode "TcRnIllegalBuiltinSyntax" = 39716 ===================================== compiler/GHC/Types/Hint.hs ===================================== @@ -343,6 +343,14 @@ data GhcHint -} | SuggestAddStandaloneKindSignature Name + {-| Suggests to annotate each constructor field with explicit strictness + (@!@ or @~@). + + Triggered by: 'GHC.Tc.Errors.Types.TcRnImplicitFieldStrictness' + Test case(s): warnings/should_compile/T16836a + -} + | SuggestExplicitFieldStrictness + {-| Suggests the user to fill in the wildcard constraint to disambiguate which constraint that is. ===================================== compiler/GHC/Types/Hint/Ppr.hs ===================================== @@ -185,6 +185,9 @@ instance Outputable GhcHint where -> text "Use a standalone deriving declaration instead" SuggestAddStandaloneKindSignature name -> text "Add a standalone kind signature for" <+> quotes (ppr name) + SuggestExplicitFieldStrictness + -> text "Annotate each field with" <+> quotes (char '!') + <+> text "(strict) or" <+> quotes (char '~') <+> text "(lazy)" SuggestFillInWildcardConstraint -> text "Fill in the wildcard constraint yourself" SuggestAppropriateTHTick ns ===================================== docs/users_guide/exts/strict.rst ===================================== @@ -194,6 +194,9 @@ The ``~`` annotation must be written in prefix form:: See `GHC Proposal #229 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0229-w…>`__ for the precise rules. +See also :ghc-flag:`-Wimplicit-field-strictness`, which warns about +fields lacking an explicit annotation. + .. _strict-data: Strict-by-default data types ===================================== docs/users_guide/using-warnings.rst ===================================== @@ -2505,6 +2505,21 @@ of ``-W(no-)*``. In other words the type-class role cannot be accidentally left representational or phantom, which could affected the code correctness. +.. ghc-flag:: -Wimplicit-field-strictness + :shortdesc: warn when constructor fields lack explicit strictness annotations + :type: dynamic + :reverse: -Wno-implicit-field-strictness + :category: + + :since: 10.2.1 + :default: off + + .. index:: + single: strictness annotations, missing + + This warning reports data constructor fields that lack an explicit + strictness annotation (``!`` or ``~``). + .. ghc-flag:: -Wimplicit-rhs-quantification :shortdesc: warn when type variables on the RHS of a type synonym are implicitly quantified :type: dynamic ===================================== testsuite/tests/warnings/should_compile/T16836a.hs ===================================== @@ -0,0 +1,37 @@ +{-# OPTIONS_GHC -Wimplicit-field-strictness #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +module T16836a where + +-- plain multi-constructor data +-- warns for both constructors +data T a = MkT a Bool + | MkT2 !Int a + +-- record with a shared field group +-- warns for x, y and z; not for b +data R = MkR { x, y :: Int, z :: Char, b :: !Bool } + +-- infix constructor +-- warns for the first argument +data I = Int :+: !Bool + +-- GADT syntax +-- warns for the first argument +data G a where + MkG :: Int -> !Bool -> G a + +-- GADT record syntax +-- warns for gx +data GR a where + MkGR :: { gx :: Int, gy :: !Bool } -> GR a + +-- data family instance +-- warns +data family F a +data instance F Int = MkF Char + +-- fully annotated +-- doesn't warn +data S = MkS !Int !Bool ===================================== testsuite/tests/warnings/should_compile/T16836a.stderr ===================================== @@ -0,0 +1,55 @@ +T16836a.hs:9:1: warning: [GHC-47032] [-Wimplicit-field-strictness] + • These constructor fields lack an explicit strictness annotation: + • In ‘MkT’: fields 1 and 2 + • In ‘MkT2’: field 2 + • In the data type declaration for ‘T’ + Suggested fixes: + • Annotate each field with ‘!’ (strict) or ‘~’ (lazy) + • Use the ‘LazyFieldAnnotations’ extension (implied by ‘StrictData’) + to allow ‘~’ annotations + +T16836a.hs:14:1: warning: [GHC-47032] [-Wimplicit-field-strictness] + • These constructor fields lack an explicit strictness annotation: + • In ‘MkR’: fields ‘x’, ‘y’ and ‘z’ + • In the data type declaration for ‘R’ + Suggested fixes: + • Annotate each field with ‘!’ (strict) or ‘~’ (lazy) + • Use the ‘LazyFieldAnnotations’ extension (implied by ‘StrictData’) + to allow ‘~’ annotations + +T16836a.hs:18:1: warning: [GHC-47032] [-Wimplicit-field-strictness] + • These constructor fields lack an explicit strictness annotation: + • In ‘:+:’: field 1 + • In the data type declaration for ‘I’ + Suggested fixes: + • Annotate each field with ‘!’ (strict) or ‘~’ (lazy) + • Use the ‘LazyFieldAnnotations’ extension (implied by ‘StrictData’) + to allow ‘~’ annotations + +T16836a.hs:22:1: warning: [GHC-47032] [-Wimplicit-field-strictness] + • These constructor fields lack an explicit strictness annotation: + • In ‘MkG’: field 1 + • In the data type declaration for ‘G’ + Suggested fixes: + • Annotate each field with ‘!’ (strict) or ‘~’ (lazy) + • Use the ‘LazyFieldAnnotations’ extension (implied by ‘StrictData’) + to allow ‘~’ annotations + +T16836a.hs:27:1: warning: [GHC-47032] [-Wimplicit-field-strictness] + • These constructor fields lack an explicit strictness annotation: + • In ‘MkGR’: field ‘gx’ + • In the data type declaration for ‘GR’ + Suggested fixes: + • Annotate each field with ‘!’ (strict) or ‘~’ (lazy) + • Use the ‘LazyFieldAnnotations’ extension (implied by ‘StrictData’) + to allow ‘~’ annotations + +T16836a.hs:33:1: warning: [GHC-47032] [-Wimplicit-field-strictness] + • These constructor fields lack an explicit strictness annotation: + • In ‘MkF’: field 1 + • In the data family instance declaration for ‘F’ + Suggested fixes: + • Annotate each field with ‘!’ (strict) or ‘~’ (lazy) + • Use the ‘LazyFieldAnnotations’ extension (implied by ‘StrictData’) + to allow ‘~’ annotations + ===================================== testsuite/tests/warnings/should_compile/T16836b.hs ===================================== @@ -0,0 +1,25 @@ +{-# OPTIONS_GHC -Wimplicit-field-strictness #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeData #-} +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE LazyFieldAnnotations #-} +module T16836b where + +-- fully annotated declarations don't warn +data T a = MkT ~a !Bool +data R = MkR { x, y :: !Int, z :: ~Char } +data G a where + MkG :: !Int -> ~Bool -> G a +data family F a +data instance F Int = MkF !Char + +-- newtypes can't have annotations; exempt +newtype N = MkN Int + +-- 'type data' can't have annotations; exempt +type data TD = MkTD Bool + +-- no fields, nothing to annotate +data E +data Nullary = A | B ===================================== testsuite/tests/warnings/should_compile/T16836c.hs ===================================== @@ -0,0 +1,6 @@ +{-# OPTIONS_GHC -Wimplicit-field-strictness #-} +{-# LANGUAGE StrictData #-} +module T16836c where + +-- unannotated fields warn under StrictData too +data T a = MkT a !Bool ~Char ===================================== testsuite/tests/warnings/should_compile/T16836c.stderr ===================================== @@ -0,0 +1,6 @@ +T16836c.hs:6:1: warning: [GHC-47032] [-Wimplicit-field-strictness] + • These constructor fields lack an explicit strictness annotation: + • In ‘MkT’: field 1 + • In the data type declaration for ‘T’ + Suggested fix: Annotate each field with ‘!’ (strict) or ‘~’ (lazy) + ===================================== testsuite/tests/warnings/should_compile/T16836d.hs ===================================== @@ -0,0 +1,20 @@ +{-# OPTIONS_GHC -Wimplicit-field-strictness #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE UnboxedTuples #-} +{-# LANGUAGE UnliftedDatatypes #-} +module T16836d where + +import GHC.Exts + +-- unlifted fields can't be usefully annotated; exempt +data P = MkP Int# (# Int, Int #) + +type UD :: UnliftedType +data UD = MkUD + +-- a field of an unlifted data type is exempt too +data Q = MkQ UD + +-- mixed constructor +-- warns only for the lifted field 2 +data M = MkM Int# Int ===================================== testsuite/tests/warnings/should_compile/T16836d.stderr ===================================== @@ -0,0 +1,9 @@ +T16836d.hs:20:1: warning: [GHC-47032] [-Wimplicit-field-strictness] + • These constructor fields lack an explicit strictness annotation: + • In ‘MkM’: field 2 + • In the data type declaration for ‘M’ + Suggested fixes: + • Annotate each field with ‘!’ (strict) or ‘~’ (lazy) + • Use the ‘LazyFieldAnnotations’ extension (implied by ‘StrictData’) + to allow ‘~’ annotations + ===================================== testsuite/tests/warnings/should_compile/all.T ===================================== @@ -91,3 +91,7 @@ test('T25901_imp_unused_3', [extra_files(['T25901_helper_3.hs'])], multimod_comp test('T25901_imp_unused_4', normal, compile, ['-Wunused-imports']) test('T25901_imp_dodgy_1', [extra_files(['T25901_helper_1.hs'])], multimod_compile, ['T25901_imp_dodgy_1', '-v0 -Wdodgy-imports']) test('T25901_imp_dodgy_2', [extra_files(['T25901_helper_2.hs'])], multimod_compile, ['T25901_imp_dodgy_2', '-v0 -Wdodgy-imports']) +test('T16836a', normal, compile, ['']) +test('T16836b', normal, compile, ['']) +test('T16836c', normal, compile, ['']) +test('T16836d', normal, compile, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d156d88713ac123db0f63307291064f… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d156d88713ac123db0f63307291064f… You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0

[Git][ghc/ghc][wip/T27731] Simplify the error-suppression mechanism in GHC.Tc.Errors
by Simon Peyton Jones (＠simonpj) 23 Aug '26

23 Aug '26

Simon Peyton Jones pushed to branch wip/T27731 at Glasgow Haskell Compiler / GHC Commits: 4088ec5b by Simon Peyton Jones at 2026-08-23T10:58:16+01:00 Simplify the error-suppression mechanism in GHC.Tc.Errors In GHC.Tc.Errors.reportWanteds we suppress some errors in favour of others. But the mechanism had grown crufty, and #27331 exposed a bug. This MR makes it simpler and more uniform, by doing everything via the `ei_suppress` field of the ErrorItem. I'm still not happy with `ignoreConstraint` but we can worry about that another day; I have not touched it. - - - - - 5 changed files: - + changelog.d/T27731 - compiler/GHC/Tc/Errors.hs - + testsuite/tests/typecheck/should_fail/T27731.hs - + testsuite/tests/typecheck/should_fail/T27731.stderr - testsuite/tests/typecheck/should_fail/all.T Changes: ===================================== changelog.d/T27731 ===================================== @@ -0,0 +1,9 @@ +section: compiler +synopsis: Fix a compiler crash after typechecking +issues: #27731 +mrs: !16564 +description: { + The type checker was failing to report an error, even though it had found one, + due to over-zealous error suppression. That led to subsequent chaos. This + MR fixes it *and* simplifies the code. +} ===================================== compiler/GHC/Tc/Errors.hs ===================================== @@ -452,16 +452,6 @@ reportBadTelescope ctxt env (ForAllSkol telescope) skols reportBadTelescope _ _ skol_info skols = pprPanic "reportBadTelescope" (ppr skol_info $$ ppr skols) --- | Should we completely ignore this constraint in error reporting? --- It *must* be the case that any constraint for which this returns True --- somehow causes an error to be reported elsewhere. --- See Note [Constraints to ignore]. -ignoreConstraint :: Ct -> Bool -ignoreConstraint ct - = 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: rewriter-sets] -- in GHC.Tc.Types.Constraint. Returns Nothing if we should just ignore @@ -473,34 +463,177 @@ mkErrorItem ct ; return Nothing } -- See Note [Constraints to ignore] | otherwise - = do { let loc = ctLoc ct - flav = ctFlavour ct + = do { let ev = ctEvidence ct + + m_evdest = case ev of + CtGiven {} -> Nothing + CtWanted (WantedCt { ctev_dest = dest }) -> Just dest - -- For this `suppress` stuff see - -- Note [Wanteds rewrite Wanteds: rewriter-sets] in GHC.Tc.Types.Constraint - (suppress, m_evdest) = case ctEvidence ct of - CtGiven {} -> (False, Nothing) - CtWanted (WantedCt { ctev_rewriters = rws, ctev_dest = dest }) - -> (not (isEmptyCoHoleSet rws), Just dest) - ; let m_reason = case ct of + m_reason = case ct of CIrredCan (IrredCt { ir_reason = reason }) -> Just reason _ -> Nothing - insoluble_ct = insolubleCt ct - ; return $ Just $ EI { ei_pred = ctPred ct , ei_evdest = m_evdest - , ei_flavour = flav - , ei_loc = loc + , ei_flavour = ctFlavour ct + , ei_loc = ctLoc ct , ei_m_reason = m_reason - , ei_insoluble = insoluble_ct - , ei_suppress = suppress }} + , ei_insoluble = insolubleCt ct + , ei_suppress = suppressCtError ev }} -- | Actually report this 'ErrorItem'. unsuppressErrorItem :: ErrorItem -> ErrorItem unsuppressErrorItem ei = ei { ei_suppress = False } +-- | Should we completely ignore this constraint in error reporting? +-- It *must* be the case that any constraint for which this returns True +-- somehow causes an error to be reported elsewhere. +-- See Note [Constraints to ignore]. +ignoreConstraint :: Ct -> Bool +ignoreConstraint ct + = case ctOrigin ct of + AssocFamPatOrigin -> True -- See (CIG1) + _ -> False + +suppressCtError :: CtEvidence -> Bool +-- See Note [Suppressing confusing errors] +suppressCtError (CtGiven {}) + = False +suppressCtError (CtWanted (WantedCt { ctev_rewriters = rws, ctev_loc = loc })) + | not (isEmptyCoHoleSet rws) + = True -- See (SCE1) + + | isWantedSuperclassOrigin (ctLocOrigin loc) + = True -- See (SCE2) + + | otherwise + = False + +{- Note [Constraints to ignore] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Some constraints are meant only to aid the solver by unification; a failure +to solve them is not necessarily an error to report to the user. It is critical +that compilation is aborted elsewhere if there are any ignored constraints here; +they will remain unfilled, and might have been used to rewrite another constraint. + +Currently, the constraints to ignore are: + +(CIG1) Constraints generated in order to unify associated type instance parameters + with class parameters. Here are two illustrative examples: + + class C (a :: k) where + type F (b :: k) + + instance C True where + type F a = Int + + instance C Left where + type F (Left :: a -> Either a b) = Bool + + In the first instance, we want to infer that `a` has type Bool. So we emit + a constraint unifying kappa (the guessed type of `a`) with Bool. All is well. + + In the second instance, we process the associated type instance only + after fixing the quantified type variables of the class instance. We thus + have skolems a1 and b1 such that the class instance is for (Left :: a1 -> Either a1 b1). + Unifying a1 and b1 with a and b in the type instance will fail, but harmlessly so. + checkConsistentFamInst checks for this, and will fail if anything has gone + awry. Really the equality constraints emitted are just meant as an aid, not + a requirement. This is test case T13972. + + We detect this case by looking for an origin of AssocFamPatOrigin; constraints + with this origin are dropped entirely during error message reporting. + + 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 [Suppressing confusing errors] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +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. +We achieve this by setting the `ei_suppress` flag in the `ErrorItem`. + +Which errors should be suppressed? + +(SCE1) Non-empty rewriter sets. See Note [Wanteds rewrite Wanteds: rewriter-sets] + in GHC.Tc.Types.Constraint + +(SCE2) 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. + +There are wrinkles + +(SCE3) In rare cases we may suppress /all/ errors. That is catastrophic: GHC proceeds + to desguar and optimise the program, even though it is full of type errors (#22702, + #22793), and/or we fail to bind evidence (#27731). + + If this happens, Unless we are sure that an error will be reported some other way + (details in the defn of `tidy_items` in `reportWanteds) we just un-suppress the lot, + which is brutal but safe. It's a rare case. + + How can it happen that there are /all/ errors are suppressed? + * See test T18851 for an example of how it is (just, barely) possible for the + /only/ errors to be superclass-of-Wanted constraints. + * Similarly #27731, which also involves a superclass-of-Wanted: + class (a ~ F b) => Ren a b + If we have a [W] Ren a b, we'll emit the superclass [W] a ~ F b, which will + rewrite the original class constraint to [W] Ren (F b) b. Now we have two + constraints: one has a non-empty rewriter set (SEC1) and one is a superclass of + a Wanted (SEC2). + * Also see Wrinkle (PER2) in Note [Prioritise Wanteds with empty + CoHoleSet] in GHC.Tc.Types.Constraint. + +Historical note. We used to suppress errors arising from the interaction of two + fundep constraints. But nowadays fundep constraints never "escape" into the main + solver and so never show up in error messages. See (SOLVE-FD) in Note [Overview + of functional dependencies in type inference] in GHC.Tc.Solver.FunDeps. So this + wrinkle is now just a historical note. + + Errors which arise from the interaction of two Wanted fun-dep constraints. + Example: + + class C a b | a -> b where + op :: a -> b -> b + + foo _ = op True Nothing + + bar _ = op False [] + + Here, we could infer + foo :: C Bool (Maybe a) => p -> Maybe a + bar :: C Bool [a] => p -> [a] + + (The unused arguments suppress the monomorphism restriction.) The problem + is that these types can't both be correct, as they violate the functional + dependency. Yet reporting an error here is awkward: we must + non-deterministically choose either foo or bar to reject. We thus want + to report this problem only when there is nothing else to report. + See typecheck/should_fail/T13506 for an example of when to suppress + the error. The case above is actually accepted, because foo and bar + are checked separately, and thus the two fundep constraints never + encounter each other. It is test case typecheck/should_compile/FunDepOrigin1. + + This case applies only when both fundeps are *Wanted* fundeps; when + both are givens, the error represents unreachable code. For + a Given/Wanted case, see #9612. + + End of historical note + +-} + ---------------------------------------------------------------- reportWanteds :: SolverReportErrCtxt -> TcLevel -> WantedConstraints -> TcM () reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics @@ -508,21 +641,9 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics | isEmptyWC wc = traceTc "reportWanteds empty WC" empty | otherwise = do { tidy_items1 <- mapMaybeM mkErrorItem tidy_cts - ; traceTc "reportWanteds 1" (vcat [ text "Simples =" <+> ppr simples - , text "Suppress =" <+> ppr (cec_suppress ctxt) - , text "tidy_cts =" <+> ppr tidy_cts - , text "tidy_items1 =" <+> ppr tidy_items1 - , text "tidy_errs =" <+> ppr tidy_errs ]) -- Catch an awkward (and probably rare) case in which /all/ errors are - -- suppressed: see Wrinkle (PER2) in Note [Prioritise Wanteds with empty - -- CoHoleSet] in GHC.Tc.Types.Constraint. - -- - -- Unless we are sure that an error will be reported some other way - -- (details in the defn of tidy_items) un-suppress the lot. This makes - -- sure we don't forget to report an error at all, which is - -- catastrophic: GHC proceeds to desguar and optimise the program, even - -- though it is full of type errors (#22702, #22793) + -- suppressed: see (SCE3) in Note [Suppressing confusing errors] ; errs_already <- ifErrsM (return True) (return False) ; let tidy_items | not errs_already -- Have not already reported an error (perhaps @@ -530,9 +651,16 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics , not (any ignoreConstraint simples) -- No error is ignorable (is reported elsewhere) , all ei_suppress tidy_items1 -- All errors are suppressed = map unsuppressErrorItem tidy_items1 + | otherwise = tidy_items1 + ; traceTc "reportWanteds 1" (vcat [ text "Simples =" <+> ppr simples + , text "Suppress =" <+> ppr (cec_suppress ctxt) + , text "tidy_cts =" <+> ppr tidy_cts + , text "tidy_items1 =" <+> ppr tidy_items1 + , text "tidy_errs =" <+> ppr tidy_errs ]) + -- First, deal with any out-of-scope errors: ; let (out_of_scope, other_holes, not_conc_errs, mult_co_errs) = partition_errors tidy_errs -- don't suppress out-of-scope errors @@ -558,10 +686,7 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics -- See wrinkle (DME1) in Note [Coercion errors in tcSubMult] in GHC.Tc.Utils.Unify. ; when (null simples) $ reportMultiplicityCoercionErrs ctxt_for_insols mult_co_errs - -- See Note [Suppressing confusing errors] - ; let (suppressed_items, reportable_items) = partition suppressItem tidy_items - ; traceTc "reportWanteds suppressed:" (ppr suppressed_items) - ; (ctxt1, items1) <- tryReporters ctxt_for_insols report1 reportable_items + ; (ctxt1, items1) <- tryReporters ctxt_for_insols report1 tidy_items -- Now all the other constraints. We suppress errors here if -- any of the first batch failed, or if the enclosing context @@ -577,18 +702,7 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics -- NB ctxt2: don't suppress inner insolubles if there's only a -- wanted insoluble here; but do suppress inner insolubles -- if there's a *given* insoluble here (= inaccessible code) - - -- If there are no other errors to report, report suppressed errors. - -- See (SCE3) in 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 tidy_cts = bagToList (mapBag (tidyCt env) simples) @@ -752,15 +866,6 @@ 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) - | otherwise - = False - isSkolemTy :: TcLevel -> Type -> Bool -- The type is a skolem tyvar isSkolemTy tc_lvl ty @@ -778,113 +883,8 @@ isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of Just (tc,_) | isTypeFamilyTyCon tc -> Just tc _ -> Nothing -{- Note [Suppressing confusing errors] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -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 should be 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. - -Historical (SCE2). Fundep constraints never "escape" into the - main solver and so never show up in error messages. - See (SOLVE-FD) in Note [Overview of functional dependencies in type inference] - in GHC.Tc.Solver.FunDeps. So this wrinkle is now just a historical note. - - Errors which arise from the interaction of two Wanted fun-dep constraints. - Example: - - class C a b | a -> b where - op :: a -> b -> b - - foo _ = op True Nothing - - bar _ = op False [] - - Here, we could infer - foo :: C Bool (Maybe a) => p -> Maybe a - bar :: C Bool [a] => p -> [a] - - (The unused arguments suppress the monomorphism restriction.) The problem - is that these types can't both be correct, as they violate the functional - dependency. Yet reporting an error here is awkward: we must - non-deterministically choose either foo or bar to reject. We thus want - to report this problem only when there is nothing else to report. - See typecheck/should_fail/T13506 for an example of when to suppress - the error. The case above is actually accepted, because foo and bar - are checked separately, and thus the two fundep constraints never - encounter each other. It is test case typecheck/should_compile/FunDepOrigin1. - - This case applies only when both fundeps are *Wanted* fundeps; when - both are givens, the error represents unreachable code. For - a Given/Wanted case, see #9612. - - End of historical (SCE2) - -(SCE3) How can it happen that there are /only/ suppressed errors? See test T18851 - for an example of how it is (just, barely) possible for the /only/ errors to - be superclass-of-Wanted constraints. - -Mechanism: - -We use the `suppress` function within reportWanteds to filter out these -"suppress" cases, then report all other errors. After doing so, we return to these -suppressed ones and report them only if there have been no errors so far. - -Note [Constraints to ignore] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Some constraints are meant only to aid the solver by unification; a failure -to solve them is not necessarily an error to report to the user. It is critical -that compilation is aborted elsewhere if there are any ignored constraints here; -they will remain unfilled, and might have been used to rewrite another constraint. - -Currently, the constraints to ignore are: - -(CIG1) Constraints generated in order to unify associated type instance parameters - with class parameters. Here are two illustrative examples: - - class C (a :: k) where - type F (b :: k) - - instance C True where - type F a = Int - - instance C Left where - type F (Left :: a -> Either a b) = Bool - - In the first instance, we want to infer that `a` has type Bool. So we emit - a constraint unifying kappa (the guessed type of `a`) with Bool. All is well. - - In the second instance, we process the associated type instance only - after fixing the quantified type variables of the class instance. We thus - have skolems a1 and b1 such that the class instance is for (Left :: a1 -> Either a1 b1). - Unifying a1 and b1 with a and b in the type instance will fail, but harmlessly so. - checkConsistentFamInst checks for this, and will fail if anything has gone - awry. Really the equality constraints emitted are just meant as an aid, not - a requirement. This is test case T13972. - - We detect this case by looking for an origin of AssocFamPatOrigin; constraints - with this origin are dropped entirely during error message reporting. - - 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] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- 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-u…) See Note [The Unsatisfiable constraint] in GHC.TypeError. ===================================== testsuite/tests/typecheck/should_fail/T27731.hs ===================================== @@ -0,0 +1,36 @@ +{-# LANGUAGE ImplicitParams, TypeFamilies #-} + +module Bug where + +type family St (a :: k) :: * +type family Ev (a :: k) :: * -> * + +data T1 a = C1 a +data T2 h g = C2 (h ()) + +class (h ~ Ev g, s ~ St g) => Ren s h g + +f1 :: + (s ~ St h, Ren s h g, ?settings :: settings) + => (g v -> g ()) -> g v -> g () +f1 form = (\_ a -> a) (C1 (f2 {-@g-})) form + +f2 :: forall g h s. ( s ~ St h, Ren s h g) => T2 h g +f2 = error "urk" + +{- Call of f2 + +[W] s ~ St h --> St g ~ St h --> St g ~ St (Ev g) +[W] Ren s h g +[W] s ~ St g -- Superclass of wanted +[W] h ~ Ev g -- Superclass of wanted +-} + +{- +f3 :: + T1 () + -> (g v -> g ()) + -> g v -> g () +f3 wd form = ((\_ a -> a) wd form) + +-} ===================================== testsuite/tests/typecheck/should_fail/T27731.stderr ===================================== @@ -0,0 +1,16 @@ +T27731.hs:16:28: [GHC-05617] + • Could not deduce ‘St (Ev g0) ~ St g0’ + arising from a superclass required to satisfy ‘Ren + (St (Ev g0)) (Ev g0) g0’, + arising from a use of ‘f2’ + from the context: (s ~ St h, Ren s h g, ?settings::settings) + bound by the type signature for: + f1 :: forall s (h :: * -> *) (g :: * -> *) settings v. + (s ~ St h, Ren s h g, ?settings::settings) => + (g v -> g ()) -> g v -> g () + at T27731.hs:(13,1)-(15,33) + Note: ‘St’ is a non-injective type family. + The type variable ‘g0’ is ambiguous + • In the first argument of ‘C1’, namely ‘(f2)’ + In the first argument of ‘\ _ a -> a’, namely ‘(C1 (f2))’ + In the expression: (\ _ a -> a) (C1 (f2)) form ===================================== testsuite/tests/typecheck/should_fail/all.T ===================================== @@ -763,3 +763,4 @@ test('T26861', normal, compile_fail, ['']) test('T26862', normal, compile_fail, ['']) test('T27210', normal, compile_fail, ['']) test('T26532', normal, compile_fail, ['']) +test('T27731', normal, compile_fail, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4088ec5b50a41c222f306690edc23ad… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4088ec5b50a41c222f306690edc23ad… You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0

[Git][ghc/ghc] Deleted branch wip/az/hie-bios-bat-executable
by Alan Zimmerman (＠alanz) 23 Aug '26

23 Aug '26

Alan Zimmerman deleted branch wip/az/hie-bios-bat-executable at Glasgow Haskell Compiler / GHC -- You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0

[Git][ghc/ghc][wip/az/epa-tidy-locatedxxx-20] EPA: Uses Parsers.parseModule for exactprint tests
by Alan Zimmerman (＠alanz) 23 Aug '26

23 Aug '26

Alan Zimmerman pushed to branch wip/az/epa-tidy-locatedxxx-20 at Glasgow Haskell Compiler / GHC Commits: e3675b4c by Alan Zimmerman at 2026-08-23T09:55:43+01:00 EPA: Uses Parsers.parseModule for exactprint tests Parsers.parseModule is the advertised way to parse for use for exact printing in the ghc-exactprint library. This commit updates the GHC exact print testing to use it. This requires moving the comment balancing that was occurring only in the test path into the advertising parser path, so it moves from Transforms.hs to Utils.hs. Also update the comment adding to honour trailing annotations - - - - - 5 changed files: - utils/check-exact/ExactPrint.hs - utils/check-exact/Main.hs - utils/check-exact/Parsers.hs - utils/check-exact/Transform.hs - utils/check-exact/Utils.hs Changes: ===================================== utils/check-exact/ExactPrint.hs ===================================== @@ -1465,7 +1465,7 @@ instance ExactPrint (HsModule GhcPs) where Just exps -> do let (op,cp,tcs) = am_exports $ anns an0 op' <- markEpToken op - exps' <- mapM markAnnotated exps + exps' <- mapM markAnnotated (filter notIEDoc exps) tcs' <- mapM markEpToken tcs cp' <- markEpToken cp return (Just exps', an0 { anns = (anns an0) { am_exports = (op',cp',tcs')}}) ===================================== utils/check-exact/Main.hs ===================================== @@ -183,7 +183,8 @@ _tt = testOneFile changers "/home/alanz/mysrc/git.haskell.org/ghc/_build/stage1/ -- "../../testsuite/tests/printer/Test17519.hs" Nothing -- "../../testsuite/tests/printer/InTreeAnnotations1.hs" Nothing -- "../../testsuite/tests/printer/Test19798.hs" Nothing - "../../testsuite/tests/printer/Test10309.hs" Nothing + -- "../../testsuite/tests/printer/Test10309.hs" Nothing + "../../testsuite/tests/printer/Haddock1.hs" Nothing -- "../../testsuite/tests/qualifieddo/should_compile/qdocompile001.hs" Nothing -- "../../testsuite/tests/typecheck/should_fail/StrictBinds.hs" Nothing @@ -304,7 +305,7 @@ writeBinFile fpath x = withBinaryFile fpath WriteMode (\h -> hSetEncoding h utf8 testOneFile :: [(String, Changer)] -> FilePath -> String -> Maybe Changer -> IO () testOneFile _ libdir fileName mchanger = do - (p,_toks) <- parseOneFile libdir fileName + p <- parseOneFile libdir fileName let origAst = ppAst p pped = exactPrint p @@ -333,7 +334,7 @@ testOneFile _ libdir fileName mchanger = do changedSource <- readFile newFile return (expectedSource == changedSource, expectedSource, changedSource) - (p',_) <- parseOneFile libdir newFile + p' <- parseOneFile libdir newFile let newAstStr :: String newAstStr = ppAst p' writeBinFile newAstFile newAstStr @@ -364,15 +365,12 @@ testOneFile _ libdir fileName mchanger = do ppAst :: Data a => a -> String ppAst ast = showSDocUnsafe $ showAstData BlankSrcSpanFile NoBlankEpAnnotations ast - -parseOneFile :: FilePath -> FilePath -> IO (ParsedSource, [Located Token]) +parseOneFile :: FilePath -> FilePath -> IO ParsedSource parseOneFile libdir fileName = do - res <- parseModuleEpAnnsWithCpp libdir defaultCppOptions fileName + res <- Parsers.parseModule libdir fileName case res of Left m -> error (internalDebugShowMessages m) - Right (injectedComments, _dflags, pmod) -> do - let !pmodWithComments = insertCppComments pmod injectedComments - return (pmodWithComments, []) + Right pmod -> return pmod -- --------------------------------------------------------------------- @@ -519,8 +517,7 @@ changeLocalDecls libdir (L l p) = do replaceLocalBinds :: LMatch GhcPs (LHsExpr GhcPs) -> Transform (LMatch GhcPs (LHsExpr GhcPs)) replaceLocalBinds (L lm (Match an mln pats (GRHSs _ rhs (HsValBinds (van,w) (ValBinds _ bs))))) = do - let (oldDecls) = map unWrapValBind bs - -- let decls = s:d:oldDecls + let oldDecls = map unWrapValBind bs let oldDecls' = captureLineSpacing oldDecls let (VbSig o:oldBinds) = map wrapValBind oldDecls' o' = setEntryDP o (DifferentLine 2 0) ===================================== utils/check-exact/Parsers.hs ===================================== @@ -46,6 +46,7 @@ module Parsers ( ) where import Preprocess +import Utils import Data.Functor (void) @@ -270,7 +271,10 @@ postParseTransform -> Either a (GHC.ParsedSource) postParseTransform parseRes = fmap mkAnns parseRes where - mkAnns (_cs, _, m) = fixModuleComments m + mkAnns (cs, _, m) = fixModuleComments (insertCppComments (noIEDoc m) cs) + noIEDoc (GHC.L l m) = case GHC.hsmodExports m of + Nothing -> GHC.L l m + Just exps -> GHC.L l m { GHC.hsmodExports = Just $ filter notIEDoc exps } fixModuleComments :: GHC.ParsedSource -> GHC.ParsedSource fixModuleComments p = fixModuleHeaderComments $ fixModuleTrailingComments p ===================================== utils/check-exact/Transform.hs ===================================== @@ -93,7 +93,6 @@ import qualified Control.Monad.Fail as Fail import GHC hiding (parseModule, parsedSource) import GHC.Parser.PostProcess ( wrapValBind ) import GHC.Data.FastString -import GHC.Types.SrcLoc import Data.Data import Data.List (unsnoc) @@ -402,6 +401,14 @@ balanceCommentsList' (a:b:ls) = (a':r) (a',b') = balanceComments a b r = balanceCommentsList' (b':ls) +balanceCommentsListA :: [LocatedA a ] -> [LocatedA a] +balanceCommentsListA [] = [] +balanceCommentsListA [x] = [x] +balanceCommentsListA (a:b:ls) = (a':r) + where + (a',b') = balanceCommentsA a b + r = balanceCommentsListA (b':ls) + -- |The GHC parser puts all comments appearing between the end of one AST -- item and the beginning of the next as 'annPriorComments' for the second one. -- This function takes two adjacent AST items and moves any 'annPriorComments' @@ -507,15 +514,6 @@ pushTrailingComments w cs lb@(HsValBinds (an,wt) _) = (True, HsValBinds (an',wt) (HsValBinds _ vb') -> vb' _ -> ValBinds noExtField [] - -balanceCommentsListA :: [LocatedA a] -> [LocatedA a] -balanceCommentsListA [] = [] -balanceCommentsListA [x] = [x] -balanceCommentsListA (a:b:ls) = (a':r) - where - (a',b') = balanceCommentsA a b - r = balanceCommentsListA (b':ls) - -- |Prior to moving an AST element, make sure any trailing comments belonging to -- it are attached to it, and not the following element. Of necessity this is a -- heuristic process, to be tuned later. Possibly a variant should be provided @@ -591,59 +589,6 @@ priorCommentsDeltas r cs = go r (sortEpaComments cs) -- --------------------------------------------------------------------- --- | Split comments into ones occurring before the end of the reference --- span, and those after it. -splitComments :: RealSrcSpan -> EpAnnComments -> ([LEpaComment], [LEpaComment], [LEpaComment]) -splitComments p cs = (before, middle, after) - where - cmpe (L (EpaSpan (RealSrcSpan l _)) _) = ss2pos l > ss2posEnd p - cmpe (L _ _) = True - - cmpb (L (EpaSpan (RealSrcSpan l _)) _) = ss2pos l > ss2pos p - cmpb (L _ _) = True - - (beforeEnd, after) = break cmpe ((priorComments cs) ++ (getFollowingComments cs)) - (before, middle) = break cmpb beforeEnd - - --- | Split comments into ones occurring before the end of the reference --- span, and those after it. -splitCommentsEnd :: RealSrcSpan -> EpAnnComments -> EpAnnComments -splitCommentsEnd p (EpaComments cs) = cs' - where - cmp (L (EpaSpan (RealSrcSpan l _)) _) = ss2pos l > ss2posEnd p - cmp (L _ _) = True - (before, after) = break cmp cs - cs' = case after of - [] -> EpaComments cs - _ -> epaCommentsBalanced before after -splitCommentsEnd p (EpaCommentsBalanced cs ts) = epaCommentsBalanced cs' ts' - where - cmp (L (EpaSpan (RealSrcSpan l _)) _) = ss2pos l > ss2posEnd p - cmp (L _ _) = True - (before, after) = break cmp cs - cs' = before - ts' = after <> ts - --- | Split comments into ones occurring before the start of the reference --- span, and those after it. -splitCommentsStart :: RealSrcSpan -> EpAnnComments -> EpAnnComments -splitCommentsStart p (EpaComments cs) = cs' - where - cmp (L (EpaSpan (RealSrcSpan l _)) _) = ss2pos l > ss2posEnd p - cmp (L _ _) = True - (before, after) = break cmp cs - cs' = case after of - [] -> EpaComments cs - _ -> epaCommentsBalanced before after -splitCommentsStart p (EpaCommentsBalanced cs ts) = epaCommentsBalanced cs' ts' - where - cmp (L (EpaSpan (RealSrcSpan l _)) _) = ss2pos l > ss2posEnd p - cmp (L _ _) = True - (before, after) = break cmp cs - cs' = before - ts' = after <> ts - moveLeadingComments :: (Data t, Data u, NoAnn t, NoAnn u) => LocatedAn t a -> EpAnn u -> (LocatedAn t a, EpAnn u) moveLeadingComments (L la a) lb = (L la' a, lb') @@ -680,19 +625,6 @@ addCommentOrigDeltasAnn (EpAnn e a cs) = EpAnn e a (addCommentOrigDeltas cs) anchorFromLocatedA :: LocatedA a -> RealSrcSpan anchorFromLocatedA (L (EpAnn anc _ _) _) = epaLocationRealSrcSpan anc --- | Get the full span of interest for comments from a LocatedA. --- This extends up to the last TrailingAnn -fullSpanFromLocatedA :: LocatedA a -> RealSrcSpan -fullSpanFromLocatedA (L (EpAnn anc tas _) _) = rr - where - r = epaLocationRealSrcSpan anc - trailing_loc ta = case ta_location ta of - EpaSpan (RealSrcSpan s _) -> [s] - _ -> [] - rr = case reverse (concatMap trailing_loc tas) of - [] -> r - (s:_) -> combineRealSrcSpans r s - -- --------------------------------------------------------------------- balanceSameLineComments :: LMatch GhcPs (LHsExpr GhcPs) -> (LMatch GhcPs (LHsExpr GhcPs)) ===================================== utils/check-exact/Utils.hs ===================================== @@ -228,7 +228,7 @@ insertCppComments (L l p) cs0 = insertRemainingCppComments (L l p2) remaining (p2, remaining) = insertTopLevelCppComments p1 toplevel addCommentsListItem :: EpAnn [TrailingAnn] -> State [LEpaComment] (EpAnn [TrailingAnn]) - addCommentsListItem = addComments + addCommentsListItem = addCommentsA addCommentsList :: EpAnn AnnList -> State [LEpaComment] (EpAnn AnnList) addCommentsList = addComments @@ -249,6 +249,20 @@ insertCppComments (L l p) cs0 = insertRemainingCppComments (L l p2) remaining _ -> return $ EpAnn anc an ocs + addCommentsA :: EpAnn [TrailingAnn] -> State [LEpaComment] (EpAnn [TrailingAnn]) + addCommentsA ann@(EpAnn anc an ocs) = do + case anc of + EpaSpan (RealSrcSpan s _) -> do + unAllocated <- get + let + (rest, these) = GHC.Parser.Lexer.allocateComments (fullSpanFromEpAnnA ann) unAllocated + balanced = splitCommentsEnd s (EpaComments these) + cs' = sortEpAnnComments (ocs <> balanced) + put rest + return $ EpAnn anc an cs' + + _ -> return $ EpAnn anc an ocs + workInComments :: EpAnnComments -> [LEpaComment] -> EpAnnComments workInComments ocs [] = ocs workInComments ocs new = cs' @@ -264,9 +278,14 @@ workInComments ocs new = cs' = break (\(L ll _) -> (ss2pos $ epaLocationRealSrcSpan ll) > (ss2pos $ epaLocationRealSrcSpan ac) ) new +sortEpAnnComments :: EpAnnComments -> EpAnnComments +sortEpAnnComments (EpaComments cs) = EpaComments (sortEpaComments cs) +sortEpAnnComments (EpaCommentsBalanced pc fc) + = EpaCommentsBalanced (sortEpaComments pc) (sortEpaComments fc) + insertTopLevelCppComments :: HsModule GhcPs -> [LEpaComment] -> (HsModule GhcPs, [LEpaComment]) insertTopLevelCppComments (HsModule (XModulePs an lo mdeprec mbDoc) mmn mexports imports decls) cs - = (HsModule (XModulePs an4 lo mdeprec mbDoc) mmn mexports' imports' decls', cs3) + = (HsModule (XModulePs an4 lo mdeprec mbDoc) mmn mexports imports' decls', cs3) -- `debug` ("insertTopLevelCppComments: (cs2,cs3,hc0,hc1,hc_cs)" ++ showAst (cs2,cs3,hc0,hc1,hc_cs)) -- `debug` ("insertTopLevelCppComments: (cs2,cs3,hc0i,hc0,hc1,hc_cs)" ++ showAst (cs2,cs3,hc0i,hc0,hc1,hc_cs)) where @@ -297,24 +316,7 @@ insertTopLevelCppComments (HsModule (XModulePs an lo mdeprec mbDoc) mmn mexports cs' = workInComments (comments an1) stay _ -> (an1,cs0a) - (mexports', an3, cs1) = - case mexports of - Nothing -> (Nothing, an2, cs0b) - Just exports -> (Just exports', an3', cse) - where - (csh', cs0b') = case am_exports $ anns an2 of - (tokOP, _tokCP, _tokCommas) -> - case tokOP of - (EpTok (EpaSpan (RealSrcSpan s _))) -> (h, n) - where - (h,n) = break (\(L ll _) -> (ss2pos $ epaLocationRealSrcSpan ll) > (ss2pos s) ) - cs0b - - _ -> ([], cs0b) - hc1' = workInComments (comments an2) csh' - an3' = an2 { comments = hc1' } - (exports', cse) = allocPreceding exports cs0b' - (imports0, cs2) = allocPreceding imports cs1 + (imports0, cs2) = allocPreceding imports cs0b (imports', hc0i) = balanceFirstLocatedAComments imports0 (decls0, cs3) = allocPreceding decls cs2 @@ -323,9 +325,9 @@ insertTopLevelCppComments (HsModule (XModulePs an lo mdeprec mbDoc) mmn mexports -- Either hc0i or hc0d should have comments. Combine them hc0 = hc0i ++ hc0d - (hc1,hc_cs) = splitOnWhere After (am_where $ anns an3) hc0 - hc2 = workInComments (comments an3) hc1 - an4 = an3 { anns = (anns an3) {am_cs = hc_cs}, comments = hc2 } + (hc1,hc_cs) = splitOnWhere After (am_where $ anns an2) hc0 + hc2 = workInComments (comments an2) hc1 + an4 = an2 { anns = (anns an2) {am_cs = hc_cs}, comments = hc2 } allocPreceding :: [LocatedA a] -> [LEpaComment] -> ([LocatedA a], [LEpaComment]) allocPreceding [] cs' = ([], cs') @@ -346,7 +348,6 @@ annListBracketsLocs (ListSquare o c) = (getEpTokenLoc o, getEpTokenLoc c) annListBracketsLocs (ListBanana o c) = (getEpUniTokenLoc o, getEpUniTokenLoc c) annListBracketsLocs ListNone = (noAnn, noAnn) - data SplitWhere = Before | After splitOnWhere :: SplitWhere -> EpToken "where" -> [LEpaComment] -> ([LEpaComment], [LEpaComment]) @@ -430,6 +431,79 @@ insertRemainingCppComments (L l p) cs = L l p' -- --------------------------------------------------------------------- +-- | Get the full span of interest for comments from a LocatedA. +-- This extends up to the last TrailingAnn +fullSpanFromLocatedA :: LocatedA a -> RealSrcSpan +fullSpanFromLocatedA (L ann _) = fullSpanFromEpAnnA ann + +-- | Get the full span of interest for comments from a LocatedA. +-- This extends up to the last TrailingAnn +fullSpanFromEpAnnA :: EpAnn [TrailingAnn] -> RealSrcSpan +fullSpanFromEpAnnA (EpAnn anc tas _) = rr + where + r = epaLocationRealSrcSpan anc + trailing_loc ta = case ta_location ta of + EpaSpan (RealSrcSpan s _) -> [s] + _ -> [] + rr = case reverse (concatMap trailing_loc tas) of + [] -> r + (s:_) -> combineRealSrcSpans r s + +-- | Split comments into ones occurring before the end of the reference +-- span, and those after it. +splitComments :: RealSrcSpan -> EpAnnComments -> ([LEpaComment], [LEpaComment], [LEpaComment]) +splitComments p cs = (before, middle, after) + where + cmpe (L (EpaSpan (RealSrcSpan l _)) _) = ss2pos l > ss2posEnd p + cmpe (L _ _) = True + + cmpb (L (EpaSpan (RealSrcSpan l _)) _) = ss2pos l > ss2pos p + cmpb (L _ _) = True + + (beforeEnd, after) = break cmpe ((priorComments cs) ++ (getFollowingComments cs)) + (before, middle) = break cmpb beforeEnd + + +-- | Split comments into ones occurring before the end of the reference +-- span, and those after it. +splitCommentsEnd :: RealSrcSpan -> EpAnnComments -> EpAnnComments +splitCommentsEnd p (EpaComments cs) = cs' + where + cmp (L (EpaSpan (RealSrcSpan l _)) _) = ss2pos l > ss2posEnd p + cmp (L _ _) = True + (before, after) = break cmp cs + cs' = case after of + [] -> EpaComments cs + _ -> epaCommentsBalanced before after +splitCommentsEnd p (EpaCommentsBalanced cs ts) = epaCommentsBalanced cs' ts' + where + cmp (L (EpaSpan (RealSrcSpan l _)) _) = ss2pos l > ss2posEnd p + cmp (L _ _) = True + (before, after) = break cmp cs + cs' = before + ts' = after <> ts + +-- | Split comments into ones occurring before the start of the reference +-- span, and those after it. +splitCommentsStart :: RealSrcSpan -> EpAnnComments -> EpAnnComments +splitCommentsStart p (EpaComments cs) = cs' + where + cmp (L (EpaSpan (RealSrcSpan l _)) _) = ss2pos l > ss2posEnd p + cmp (L _ _) = True + (before, after) = break cmp cs + cs' = case after of + [] -> EpaComments cs + _ -> epaCommentsBalanced before after +splitCommentsStart p (EpaCommentsBalanced cs ts) = epaCommentsBalanced cs' ts' + where + cmp (L (EpaSpan (RealSrcSpan l _)) _) = ss2pos l > ss2posEnd p + cmp (L _ _) = True + (before, after) = break cmp cs + cs' = before + ts' = after <> ts + +-- --------------------------------------------------------------------- + ghcCommentText :: LEpaComment -> String ghcCommentText (L _ (GHC.EpaComment (EpaDocComment s) _)) = exactPrintHsDocString s ghcCommentText (L _ (GHC.EpaComment (EpaDocOptions s) _)) = s View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e3675b4c51182e05e4e8fab92117074… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e3675b4c51182e05e4e8fab92117074… You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0

[Git][ghc/ghc][wip/T26543b] Line up simpleUnifyCheck and check_ty_eq_rhs
by Simon Peyton Jones (＠simonpj) 22 Aug '26

22 Aug '26

Simon Peyton Jones pushed to branch wip/T26543b at Glasgow Haskell Compiler / GHC Commits: defc3eae by Simon Peyton Jones at 2026-08-23T00:01:34+01:00 Line up simpleUnifyCheck and check_ty_eq_rhs Even after #26543 was allegedly fixed, the original repo case in the Description continued to fail. The reason was that the QuickLook unifier, `qlUnify`, used `simpleUnifyCheck` for checking unification invariants; and `simpleUnifyCheck` conservatively rejected any RHS with a coercion hole in it. The upshot was that QuickLook was not as clever as it should be, wrongly failing to do an impredicative instantiation. Interestingly `check_ty_eq_rhs`, which does the same job, only during constraint solving, was more liberal: it just looked at the free vars of the coercion, and allowed coercion holes. This MR lines them up, adding some careful notes. See Note [simpleUnifyCheck] esp (SUC1) Note [Unification preconditions] esp (COERCIONS) Things are better than before, but I am still uncomfortable about the possibilty that a hole might be filled with a coercion that mentions the LHS type variable; for now I have left this discomfort documented in (SUC1). - - - - - 6 changed files: - + changelog.d/T26543 - compiler/GHC/Core/TyCo/FVs.hs - compiler/GHC/Tc/Gen/App.hs - compiler/GHC/Tc/Utils/Unify.hs - + testsuite/tests/typecheck/should_compile/T26543_orig.hs - testsuite/tests/typecheck/should_compile/all.T Changes: ===================================== changelog.d/T26543 ===================================== @@ -0,0 +1,7 @@ +section: compiler +synopsis: Fix a bug in ImpredicativeTypes +description: + The QuickLook algorithm (which implements `ImpredicativeTypes`) was defeated if there + was a kind coercion in the types being unified. That bug is now fixed. +mrs: !16566 +issues: #26543 ===================================== compiler/GHC/Core/TyCo/FVs.hs ===================================== @@ -850,15 +850,15 @@ invisibleVarsOfTypes = foldr (unionVarSet . invisibleVarsOfType) emptyVarSet {-# INLINE afvFolder #-} -- so that specialization to (const True) works afvFolder :: (TyCoVar -> Bool) -> TyCoFolder (FV TyCoVarSet DM.Any) -- 'afvFolder' is short for "any-free-var folder", good for checking --- if any free var of a type satisfies a predicate `check_fv` +-- if any shallow free var of a type satisfies a predicate `check_fv` afvFolder check_fv = TyCoFolder { tcf_view = noView -- See Note [Free vars and synonyms] , tcf_tyvar = do_tcv, tcf_covar = do_tcv , tcf_hole = do_hole , tcf_tycobinder = addBndrFV } where - do_tcv tv = MkFV $ \ bvs -> - Any (not (tv `elemVarSet` bvs) && check_fv tv) - do_hole _ = mempty -- I'm unsure; probably never happens + do_tcv tv = MkFV $ \ bvs -> + Any (not (tv `elemVarSet` bvs) && check_fv tv) + do_hole hole = do_tcv (coHoleCoVar hole) anyFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool anyFreeVarsOfType check_fv ty = DM.getAny (runFVTop (f ty)) ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -631,11 +631,13 @@ tcInstFun :: QLFlag -- plus the modification in Fig 5, of the QL paper: -- "A quick look at impredicativity" (ICFP'20). tcInstFun do_ql inst_final rn_head@(_, fun_lspan) tc_fun fun_sigma rn_args - = do { traceTc "tcInstFun" (vcat [ text "tc_fun" <+> ppr tc_fun + = do { lvl <- getTcLevel + ; traceTc "tcInstFun" (vcat [ text "tc_fun" <+> ppr tc_fun , text "rn_fun" <+> ppr rn_head , text "fun_sigma" <+> ppr fun_sigma , text "args:" <+> ppr rn_args - , text "do_ql" <+> ppr do_ql]) + , text "do_ql" <+> ppr do_ql + , text "lvl:" <+> ppr lvl ]) ; fun_origin <- mk_origin rn_head ; res@(_, fun_ty) <- go fun_origin 1 [] fun_sigma rn_args ; traceTc "tcInstFun:ret" (ppr fun_ty) @@ -1377,13 +1379,15 @@ tc_inst_forall_arg conc_tvs (tvb, inner_ty) hs_ty -- is not fully zonked, because ty_arg is fully zonked. -- See Note [Type application substitution]. + ; lvl <- getTcLevel ; traceTc "tc_inst_forall_arg (VTA/VDQ)" ( vcat [ text "fun_ty" <+> ppr fun_ty , text "tv" <+> ppr tv <+> dcolon <+> debugPprType kind , text "ty_arg" <+> debugPprType ty_arg <+> dcolon <+> debugPprType (typeKind ty_arg) , text "inner_ty" <+> debugPprType inner_ty - , text "insted_ty" <+> debugPprType insted_ty ]) + , text "insted_ty" <+> debugPprType insted_ty + , text "lvl:" <+> ppr lvl ]) ; return (ty_arg, insted_ty) } {- Note [Visible type application and abstraction] @@ -1934,11 +1938,13 @@ quickLookArg1 pos app_lspan rn_head larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_ -- capture and save it in the `EValArgQL`. See (QLA6) in -- Note [Quick Look at value arguments] + ; lvl <- getTcLevel ; traceTc "quickLookArg {" $ vcat [ text "arg:" <+> ppr arg , text "orig_arg_rho:" <+> ppr orig_arg_rho , text "head:" <+> ppr rn_fun_arg <+> dcolon <+> ppr mb_fun_ty - , text "args:" <+> ppr rn_args ] + , text "args:" <+> ppr rn_args + , text "level:" <+> ppr lvl ] ; case mb_fun_ty of { Nothing -> skipQuickLook app_lspan larg sc_arg_ty ; -- fun is too complicated @@ -2158,18 +2164,23 @@ qlUnify :: TcType -> TcType -> TcM () -- * It may return without having made the argument types equal, of course; -- it just makes best efforts. qlUnify ty1 ty2 - = do { traceTc "qlUnify" (ppr ty1 $$ ppr ty2) + = do { lvl <- getTcLevel + ; traceTc "qlUnify" (ppr lvl $$ ppr ty1 $$ ppr ty2) ; go ty1 ty2 } where go :: TcType -> TcType -> TcM () + go t1 t2 = do { traceTc "qlUinfy:go" (ppr t1 <+> char '~' <+> ppr t2) + ; go' t1 t2 } + -- Decompose (arg1 -> res1) ~ (arg2 -> res2) -- and (c1 => res1) ~ (c2 => res2) -- But for the latter we only learn instantiation info from res1~res2 - go (FunTy { ft_af = af1, ft_arg = arg1, ft_res = res1 }) + go' (FunTy { ft_af = af1, ft_arg = arg1, ft_res = res1 }) (FunTy { ft_af = af2, ft_arg = arg2, ft_res = res2 }) | af1 == af2 -- Match the arrow TyCon - = do { when (isVisibleFunArg af1) (go arg1 arg2) + = do { traceTc "go_fun" (ppr arg1 $$ ppr arg2) + ; when (isVisibleFunArg af1) (go arg1 arg2) -- NB: we do not unify the multiplicities; that would be too strong. -- We might only require mult1 ⩽ mult2, as in Note [Multiplicity in deep subsumption]. @@ -2178,30 +2189,30 @@ qlUnify ty1 ty2 ; go res1 res2 } -- Make sure to not unify "kappa := (a %1 -> b)". See (UQL5). - go (FunTy { ft_mult = OneTy }) _ = return () - go _ (FunTy { ft_mult = OneTy }) = return () + go' (FunTy { ft_mult = OneTy }) _ = return () + go' _ (FunTy { ft_mult = OneTy }) = return () -- NB: we do want to be able to unify "kappa := a => b", as that's -- the main point of QuickLook (allowing meta-variables to be unified -- with qualified types). - go (TyVarTy tv) ty2 + go' (TyVarTy tv) ty2 | isMetaTyVar tv = go_kappa tv ty2 - go ty1 (TyVarTy tv) + go' ty1 (TyVarTy tv) | isMetaTyVar tv = go_kappa tv ty1 - go (CastTy ty1 _) ty2 = go ty1 ty2 - go ty1 (CastTy ty2 _) = go ty1 ty2 + go' (CastTy ty1 _) ty2 = go ty1 ty2 + go' ty1 (CastTy ty2 _) = go ty1 ty2 - go (TyConApp tc1 []) (TyConApp tc2 []) + go' (TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2 -- See GHC.Tc.Utils.Unify = return () -- Note [Expanding synonyms during unification] -- Now, and only now, expand synonyms - go rho1 rho2 + go' rho1 rho2 | Just rho1 <- coreView rho1 = go rho1 rho2 | Just rho2 <- coreView rho2 = go rho1 rho2 - go (TyConApp tc1 tys1) (TyConApp tc2 tys2) + go' (TyConApp tc1 tys1) (TyConApp tc2 tys2) | tc1 == tc2 , not (isTypeFamilyTyCon tc1) , tys1 `equalLength` tys2 @@ -2209,14 +2220,14 @@ qlUnify ty1 ty2 -- Don't allow unifying (a => b) with the AppTy 'arr[tau] a b'. -- To ensure this, use 'tcSplitAppTyNoView_maybe' which does not split (=>). - go (AppTy t1a t1b) ty2 + go' (AppTy t1a t1b) ty2 | Just (t2a, t2b) <- tcSplitAppTyNoView_maybe ty2 = do { go t1a t2a; go t1b t2b } - go ty1 (AppTy t2a t2b) + go' ty1 (AppTy t2a t2b) | Just (t1a, t1b) <- tcSplitAppTyNoView_maybe ty1 = do { go t1a t2a; go t1b t2b } - go _ _ = return () + go' _ _ = return () -- Don't look under foralls; see (UQL4) of Note [QuickLook unification] ---------------- @@ -2244,7 +2255,11 @@ qlUnify ty1 ty2 -- Here we are in the TcM monad, which does not track enclosing -- Given equalities; so for quick-look unification we conservatively -- treat /any/ level outside this one as untouchable. Hence cur_lvl. + ; traceTc "go_flexi1" (ppr kappa $$ ppr ty2) ; case simpleUnifyCheck UC_QuickLook cur_lvl kappa ty2 of + -- qlUnify depends, regrettably delicately, on the exact choices made + -- by `simpleUnifyCheck`. See (SUC1) in + -- Note [simpleUnifyCheck] in GHC.Tc.Utils.Unify SUC_CanUnify -> do { co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind -- unifyKind: see (UQL2) in Note [QuickLook unification] @@ -2253,7 +2268,8 @@ qlUnify ty1 ty2 ; traceTc "qlUnify:update" $ ppr kappa <+> text ":=" <+> ppr ty2 ; liftZonkM $ writeMetaTyVar kappa ty2' } - _ -> return () -- e.g. occurs-check or forall-bound variable + suc -> do { traceTc "go_flexi2" (ppr suc $$ ppr kappa $$ ppr ty2) + ; return () } -- e.g. occurs-check or forall-bound variable } where kappa_kind = tyVarKind kappa ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -103,7 +103,6 @@ import GHC.Types.Id( idType ) import GHC.Types.Var as Var import GHC.Types.Var.Set import GHC.Types.Var.Env -import GHC.Types.Var.FV import GHC.Types.Basic import GHC.Types.Unique.Set (nonDetEltsUniqSet) @@ -120,7 +119,6 @@ import GHC.Data.Maybe (firstJusts) import Control.Monad import Data.Functor.Identity (Identity(..)) import qualified Data.List.NonEmpty as NE -import Data.Monoid as DM ( Any(..) ) import qualified Data.Semigroup as S ( (<>) ) import Data.Traversable (for) @@ -3143,6 +3141,7 @@ uUnfilledVar2 env@(UE { u_defer = def_eq_ref, u_given_eq_lvl = given_eq_lvl }) do { traceTc "uUnfilledVar2 not ok" $ vcat [ text "tv1:" <+> ppr tv1 , text "ty2:" <+> ppr ty2 + , text "given_eq_lvl:" <+> ppr given_eq_lvl , text "simple-unify-chk:" <+> ppr (simpleUnifyCheck UC_OnTheFly given_eq_lvl tv1 ty2) ] -- Occurs check or an untouchable: just defer @@ -3246,6 +3245,7 @@ lhsPriority tv ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Question: given a homogeneous equality (alpha ~# ty), when is it OK to unify alpha := ty? + (This note only applies to /homogeneous/ equalities, in which both sides have the same kind.) @@ -3354,6 +3354,14 @@ Needless to say, all there are wrinkles: GHC.Tc.Solver.floatEqualities, around Nov 2020. It's much easier to unify in-place, with no floating. +* (COERCIONS) What if there are coercions in the RHS? E.g. + alpha ~ (ty |> co) + or alpha ~ (ty co) + We only recurse into the `coercionType` of `co` rather than `co` itself. + Why? Mainly because `co` might be a coercion hole, in which case we /can't/ + recurse into the coercion that will eventually fill the hole. This came + up in #26543. + Note [TyVar/TyVar orientation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ See also Note [Fundeps with instances, and equality orientation] @@ -3619,6 +3627,8 @@ simpleUnifyCheck :: UnifyCheckCaller -> TcLevel -> TcTyVar -> TcType -> SimpleUn -- unification might still be OK, but it'll take more work to do -- (use the full 'checkTypeEq'). -- +-- See Note [simpleUnifyCheck] +-- -- * Rejects if lhs_tv occurs in rhs_ty (occurs check) -- * Rejects foralls unless -- lhs_tv is RuntimeUnk (used by GHCi debugger) @@ -3638,10 +3648,7 @@ simpleUnifyCheck caller given_eq_lvl lhs_tv rhs | otherwise = SUC_NotSure where - lhs_info = metaTyVarInfo lhs_tv - - !(occ_in_ty, occ_in_co) = mkOccFolders (tyVarName lhs_tv) - + lhs_info = metaTyVarInfo lhs_tv lhs_tv_lvl = tcTyVarLevel lhs_tv lhs_tv_is_concrete = isConcreteTyVar lhs_tv @@ -3660,11 +3667,12 @@ simpleUnifyCheck caller given_eq_lvl lhs_tv rhs UC_OnTheFly -> False rhs_is_ok (TyVarTy tv) - | lhs_tv == tv = False - | tcTyVarLevel tv `strictlyDeeperThan` lhs_tv_lvl = False - | lhs_tv_is_concrete, not (isConcreteTyVar tv) = False - | occ_in_ty $! (tyVarKind tv) = False - | otherwise = True + | lhs_tv == tv = False -- Occurs check + | tcTyVarLevel tv `strictlyDeeperThan` lhs_tv_lvl = False + | lhs_tv_is_concrete, not (isConcreteTyVar tv) = False + | not (rhs_is_ok $! tyVarKind tv) = False + | otherwise = True + -- Hmm. We probably don't need the level check inside the kind, but no harm rhs_is_ok (FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r}) | not forall_ok, isInvisibleFunArg af = False @@ -3681,33 +3689,44 @@ simpleUnifyCheck caller given_eq_lvl lhs_tv rhs | otherwise = False rhs_is_ok (AppTy t1 t2) = rhs_is_ok t1 && rhs_is_ok t2 - rhs_is_ok (CastTy ty co) = not (occ_in_co co) && rhs_is_ok ty - rhs_is_ok (CoercionTy co) = not (occ_in_co co) + rhs_is_ok (CastTy ty co) = co_is_ok co && rhs_is_ok ty + rhs_is_ok (CoercionTy co) = co_is_ok co rhs_is_ok (LitTy {}) = True + -- For coercions we look only in the /type/ of the coercion + -- See (SUC1) in Note [simpleUnifyCheck] + co_is_ok co = rhs_is_ok (coercionType co) -mkOccFolders :: Name -> (TcType -> Bool, TcCoercion -> Bool) --- These functions return True --- * if lhs_tv occurs (incl deeply, in the kind of variable) --- * if there is a coercion hole --- No expansion of type synonyms -mkOccFolders lhs_tv = ( getAny . runFVTop . check_ty - , getAny . runFVTop . check_co) - where - check_ty :: Type -> FV BoundVars Any - !(check_ty, _, check_co, _) = foldTyCo occ_folder - - occ_folder :: TyCoFolder (FV BoundVars Any) - occ_folder = TyCoFolder { tcf_view = noView -- Don't expand synonyms - , tcf_tyvar = do_tcv, tcf_covar = do_tcv - , tcf_hole = do_hole - , tcf_tycobinder = addBndrFV } - - do_tcv v = (MkFV $ \ bvs -> - Any (not (v `elemVarSet` bvs) && tyVarName v == lhs_tv)) - `mappend` check_ty (varType v) - - do_hole _hole = MkFV $ \ _bvs -> DM.Any True -- Reject coercion holes +{- Note [simpleUnifyCheck] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +The function `simpleUnifyCheck` is asimple, /fast/ check for unifying (tv ~ rhs). +It can return a definite decision (SUC_CannotUnify of SUC_CanUnify), or uncertainty +(SUC_NotSure). In the latter case we will later use `checkTyEqRhs` to resolve. +In particular, `simpleUnifyCheck`: + +* Rejects if lhs_tv occurs in rhs_ty (occurs check) +* Rejects foralls unless + lhs_tv is RuntimeUnk (used by GHCi debugger) + or is a QL instantiation variable +* Rejects a non-concrete type if lhs_tv is concrete +* Rejects type families unless fam_ok=True +* Does a level-check for type variables, to avoid skolem escape + +This function is pretty heavily used, so it's optimised not to allocate. + +(SUC1) `simpleUnifyCheck` used by QuickLook's `qlUnify`, and anything other than + SUC_CanUnify will tell `qlUnify` not to proceed. That makes QuickLook depend + (regrettably, delicately) on the exact choices made by `simpleUnifyCheck`. + + A case in point: in #26543. In the repro case in the Descriptions, `qlUnify` failed + because there was a coercion hole in the RHS; but one that was ultimately Refl. + + So we only look at the /kind/ of a coercion, not the evidence itself. I'm a bit + worried about building a loop, if the evidence mentions the LHS unification + variable; but I can't see how that can happen, and I /really/ don't want to be + super-conservative for coercion holes (#26543). So, for now at least, we look + just at the kind of the coercion. +-} {- ********************************************************************* * * @@ -4337,7 +4356,11 @@ checkCo flags co = -- Occurs check (can promote) | OC_Check lhs_tv occ_prob <- occ , LC_Promote { lc_lvlp = lhs_tv_lvl } <- lc - -> do { reason <- checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl (tyCoVarsOfCo co) + -> do { reason <- checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl $ + tyCoVarsOfCo co + -- Maybe we should just check the free vars of the + -- /type/ of the coercion, to line up with + -- (SUC1) in Note [simpleUnifyCheck] ; return $ if cterHasNoProblem reason then pure co @@ -4697,12 +4720,14 @@ simpleOccursCheck :: OccursCheck -> TcTyVar -> TyVarCheckResult m simpleOccursCheck OC_None _ = TyVarCheck_Success simpleOccursCheck (OC_Check lhs_tv occ_prob) occ_tv - | lhs_tv == tyVarName occ_tv || check_kind (tyVarKind occ_tv) - = TyVarCheck_Error (cteProblem occ_prob) - | otherwise - = TyVarCheck_Success + | check_fv occ_tv = TyVarCheck_Error (cteProblem occ_prob) + | otherwise = TyVarCheck_Success where - (check_kind, _) = mkOccFolders lhs_tv + check_fv :: TyCoVar -> Bool -- True <=> occurs check + check_fv occ_tcv + | lhs_tv == tyVarName occ_tcv = True + | anyFreeVarsOfType check_fv (tyVarKind occ_tcv) = True + | otherwise = False ------------------------- tyVarLevelCheck :: LevelCheck m -> TcTyVar -> TyVarCheckResult m ===================================== testsuite/tests/typecheck/should_compile/T26543_orig.hs ===================================== @@ -0,0 +1,36 @@ +-- This test is from the Description of #26543 + +{-# LANGUAGE GHC2024, TypeAbstractions, AllowAmbiguousTypes, NoImplicitPrelude, + TypeFamilies, UndecidableInstances #-} +module T26543_orig where + +import Data.Kind +import Control.Applicative (Applicative(..)) +import Prelude (type (~), ($)) + +type CAT k = k -> k -> Type + +type family (~>) :: CAT k +type family Ob (a :: k) :: Constraint +type family UN (w :: j -> k) (wa :: k) :: j + +class HasBinaryProducts k where + type (a :: k) && (b :: k) :: k + withObProd :: (Ob (a :: k), Ob b) => ((Ob (a && b)) => r) -> r + (&&&) :: ((a :: k) ~> x) -> (a ~> y) -> (a ~> (x && y)) + +data AP (f :: Type -> Type) k = A k +type instance UN A (A k) = k + +type Ap :: CAT (AP f k) +data Ap a b where + Ap :: forall {k} a b f. (Ob a, Ob b) => f (a ~> b) -> Ap (A a :: AP f k) (A b) + +type instance (~>) = Ap +type instance Ob a = (a ~ A (UN A a), Ob (UN A a)) + +instance (Applicative f, HasBinaryProducts k) => HasBinaryProducts (AP f k) where + type a && b = A (UN A a && UN A b) + withObProd @(A a) @(A b) r = withObProd @k @a @b r + -- (&&&) :: Ap (a :: AP f k) x -> Ap a y -> Ap a (x && y) + Ap @_ @x f &&& Ap @_ @y g = withObProd @k @x @y $ Ap (liftA2 (&&&) f g) ===================================== testsuite/tests/typecheck/should_compile/all.T ===================================== @@ -969,3 +969,4 @@ test('ExpansionQLIm', normal, compile, ['']) test('T23135', normal, compile, ['']) test('LazyFieldAnnotations', normal, compile, ['']) test('T27557', normal, compile, ['']) +test('T26543_orig', normal, compile, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/defc3eae2fd24582516f77f4beab0a3… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/defc3eae2fd24582516f77f4beab0a3… You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0

[Git][ghc/ghc][wip/T27731] Simplify the error-suppression mechanism in GHC.Tc.Errors
by Simon Peyton Jones (＠simonpj) 22 Aug '26

22 Aug '26

Simon Peyton Jones pushed to branch wip/T27731 at Glasgow Haskell Compiler / GHC Commits: 4d537743 by Simon Peyton Jones at 2026-08-22T19:30:48+01:00 Simplify the error-suppression mechanism in GHC.Tc.Errors In GHC.Tc.Errors.reportWanteds we suppress some errors in favour of others. But the mechanism had grown crufty, and #27331 exposed a bug. This MR makes it simpler and more uniform, by doing everything via the `ei_suppress` field of the ErrorItem. I'm still not happy with `ignoreConstraint` but we can worry about that another day; I have not touched it. - - - - - 4 changed files: - compiler/GHC/Tc/Errors.hs - + testsuite/tests/typecheck/should_fail/T27731.hs - + testsuite/tests/typecheck/should_fail/T27731.stderr - testsuite/tests/typecheck/should_fail/all.T Changes: ===================================== compiler/GHC/Tc/Errors.hs ===================================== @@ -452,16 +452,6 @@ reportBadTelescope ctxt env (ForAllSkol telescope) skols reportBadTelescope _ _ skol_info skols = pprPanic "reportBadTelescope" (ppr skol_info $$ ppr skols) --- | Should we completely ignore this constraint in error reporting? --- It *must* be the case that any constraint for which this returns True --- somehow causes an error to be reported elsewhere. --- See Note [Constraints to ignore]. -ignoreConstraint :: Ct -> Bool -ignoreConstraint ct - = 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: rewriter-sets] -- in GHC.Tc.Types.Constraint. Returns Nothing if we should just ignore @@ -473,34 +463,177 @@ mkErrorItem ct ; return Nothing } -- See Note [Constraints to ignore] | otherwise - = do { let loc = ctLoc ct - flav = ctFlavour ct + = do { let ev = ctEvidence ct + + m_evdest = case ev of + CtGiven {} -> Nothing + CtWanted (WantedCt { ctev_dest = dest }) -> Just dest - -- For this `suppress` stuff see - -- Note [Wanteds rewrite Wanteds: rewriter-sets] in GHC.Tc.Types.Constraint - (suppress, m_evdest) = case ctEvidence ct of - CtGiven {} -> (False, Nothing) - CtWanted (WantedCt { ctev_rewriters = rws, ctev_dest = dest }) - -> (not (isEmptyCoHoleSet rws), Just dest) - ; let m_reason = case ct of + m_reason = case ct of CIrredCan (IrredCt { ir_reason = reason }) -> Just reason _ -> Nothing - insoluble_ct = insolubleCt ct - ; return $ Just $ EI { ei_pred = ctPred ct , ei_evdest = m_evdest - , ei_flavour = flav - , ei_loc = loc + , ei_flavour = ctFlavour ct + , ei_loc = ctLoc ct , ei_m_reason = m_reason - , ei_insoluble = insoluble_ct - , ei_suppress = suppress }} + , ei_insoluble = insolubleCt ct + , ei_suppress = suppressCtError ev }} -- | Actually report this 'ErrorItem'. unsuppressErrorItem :: ErrorItem -> ErrorItem unsuppressErrorItem ei = ei { ei_suppress = False } +-- | Should we completely ignore this constraint in error reporting? +-- It *must* be the case that any constraint for which this returns True +-- somehow causes an error to be reported elsewhere. +-- See Note [Constraints to ignore]. +ignoreConstraint :: Ct -> Bool +ignoreConstraint ct + = case ctOrigin ct of + AssocFamPatOrigin -> True -- See (CIG1) + _ -> False + +suppressCtError :: CtEvidence -> Bool +-- See Note [Suppressing confusing errors] +suppressCtError (CtGiven {}) + = False +suppressCtError (CtWanted (WantedCt { ctev_rewriters = rws, ctev_loc = loc })) + | not (isEmptyCoHoleSet rws) + = True -- See (SCE1) + + | isWantedSuperclassOrigin (ctLocOrigin loc) + = True -- See (SCE2) + + | otherwise + = False + +{- Note [Constraints to ignore] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Some constraints are meant only to aid the solver by unification; a failure +to solve them is not necessarily an error to report to the user. It is critical +that compilation is aborted elsewhere if there are any ignored constraints here; +they will remain unfilled, and might have been used to rewrite another constraint. + +Currently, the constraints to ignore are: + +(CIG1) Constraints generated in order to unify associated type instance parameters + with class parameters. Here are two illustrative examples: + + class C (a :: k) where + type F (b :: k) + + instance C True where + type F a = Int + + instance C Left where + type F (Left :: a -> Either a b) = Bool + + In the first instance, we want to infer that `a` has type Bool. So we emit + a constraint unifying kappa (the guessed type of `a`) with Bool. All is well. + + In the second instance, we process the associated type instance only + after fixing the quantified type variables of the class instance. We thus + have skolems a1 and b1 such that the class instance is for (Left :: a1 -> Either a1 b1). + Unifying a1 and b1 with a and b in the type instance will fail, but harmlessly so. + checkConsistentFamInst checks for this, and will fail if anything has gone + awry. Really the equality constraints emitted are just meant as an aid, not + a requirement. This is test case T13972. + + We detect this case by looking for an origin of AssocFamPatOrigin; constraints + with this origin are dropped entirely during error message reporting. + + 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 [Suppressing confusing errors] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +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. +We achieve this by setting the `ei_suppress` flag in the `ErrorItem`. + +Which errors should be suppressed? + +(SCE1) Non-empty rewriter sets. See Note [Wanteds rewrite Wanteds: rewriter-sets] + in GHC.Tc.Types.Constraint + +(SCE2) 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. + +There are wrinkles + +(SCE3) In rare cases we may suppress /all/ errors. That is catastrophic: GHC proceeds + to desguar and optimise the program, even though it is full of type errors (#22702, + #22793), and/or we fail to bind evidence (#27731). + + If this happens, Unless we are sure that an error will be reported some other way + (details in the defn of `tidy_items` in `reportWanteds) we just un-suppress the lot, + which is brutal but safe. It's a rare case. + + How can it happen that there are /all/ errors are suppressed? + * See test T18851 for an example of how it is (just, barely) possible for the + /only/ errors to be superclass-of-Wanted constraints. + * Similarly #27731, which also involves a superclass-of-Wanted: + class (a ~ F b) => Ren a b + If we have a [W] Ren a b, we'll emit the superclass [W] a ~ F b, which will + rewrite the original class constraint to [W] Ren (F b) b. Now we have two + constraints: one has a non-empty rewriter set (SEC1) and one is a superclass of + a Wanted (SEC2). + * Also see Wrinkle (PER2) in Note [Prioritise Wanteds with empty + CoHoleSet] in GHC.Tc.Types.Constraint. + +Historical note. We used to suppress errors arising from the interaction of two + fundep constraints. But nowadays fundep constraints never "escape" into the main + solver and so never show up in error messages. See (SOLVE-FD) in Note [Overview + of functional dependencies in type inference] in GHC.Tc.Solver.FunDeps. So this + wrinkle is now just a historical note. + + Errors which arise from the interaction of two Wanted fun-dep constraints. + Example: + + class C a b | a -> b where + op :: a -> b -> b + + foo _ = op True Nothing + + bar _ = op False [] + + Here, we could infer + foo :: C Bool (Maybe a) => p -> Maybe a + bar :: C Bool [a] => p -> [a] + + (The unused arguments suppress the monomorphism restriction.) The problem + is that these types can't both be correct, as they violate the functional + dependency. Yet reporting an error here is awkward: we must + non-deterministically choose either foo or bar to reject. We thus want + to report this problem only when there is nothing else to report. + See typecheck/should_fail/T13506 for an example of when to suppress + the error. The case above is actually accepted, because foo and bar + are checked separately, and thus the two fundep constraints never + encounter each other. It is test case typecheck/should_compile/FunDepOrigin1. + + This case applies only when both fundeps are *Wanted* fundeps; when + both are givens, the error represents unreachable code. For + a Given/Wanted case, see #9612. + + End of historical note + +-} + ---------------------------------------------------------------- reportWanteds :: SolverReportErrCtxt -> TcLevel -> WantedConstraints -> TcM () reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics @@ -508,21 +641,9 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics | isEmptyWC wc = traceTc "reportWanteds empty WC" empty | otherwise = do { tidy_items1 <- mapMaybeM mkErrorItem tidy_cts - ; traceTc "reportWanteds 1" (vcat [ text "Simples =" <+> ppr simples - , text "Suppress =" <+> ppr (cec_suppress ctxt) - , text "tidy_cts =" <+> ppr tidy_cts - , text "tidy_items1 =" <+> ppr tidy_items1 - , text "tidy_errs =" <+> ppr tidy_errs ]) -- Catch an awkward (and probably rare) case in which /all/ errors are - -- suppressed: see Wrinkle (PER2) in Note [Prioritise Wanteds with empty - -- CoHoleSet] in GHC.Tc.Types.Constraint. - -- - -- Unless we are sure that an error will be reported some other way - -- (details in the defn of tidy_items) un-suppress the lot. This makes - -- sure we don't forget to report an error at all, which is - -- catastrophic: GHC proceeds to desguar and optimise the program, even - -- though it is full of type errors (#22702, #22793) + -- suppressed: see (SCE3) in Note [Suppressing confusing errors] ; errs_already <- ifErrsM (return True) (return False) ; let tidy_items | not errs_already -- Have not already reported an error (perhaps @@ -530,9 +651,16 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics , not (any ignoreConstraint simples) -- No error is ignorable (is reported elsewhere) , all ei_suppress tidy_items1 -- All errors are suppressed = map unsuppressErrorItem tidy_items1 + | otherwise = tidy_items1 + ; traceTc "reportWanteds 1" (vcat [ text "Simples =" <+> ppr simples + , text "Suppress =" <+> ppr (cec_suppress ctxt) + , text "tidy_cts =" <+> ppr tidy_cts + , text "tidy_items1 =" <+> ppr tidy_items1 + , text "tidy_errs =" <+> ppr tidy_errs ]) + -- First, deal with any out-of-scope errors: ; let (out_of_scope, other_holes, not_conc_errs, mult_co_errs) = partition_errors tidy_errs -- don't suppress out-of-scope errors @@ -558,10 +686,7 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics -- See wrinkle (DME1) in Note [Coercion errors in tcSubMult] in GHC.Tc.Utils.Unify. ; when (null simples) $ reportMultiplicityCoercionErrs ctxt_for_insols mult_co_errs - -- See Note [Suppressing confusing errors] - ; let (suppressed_items, reportable_items) = partition suppressItem tidy_items - ; traceTc "reportWanteds suppressed:" (ppr suppressed_items) - ; (ctxt1, items1) <- tryReporters ctxt_for_insols report1 reportable_items + ; (ctxt1, items1) <- tryReporters ctxt_for_insols report1 tidy_items -- Now all the other constraints. We suppress errors here if -- any of the first batch failed, or if the enclosing context @@ -577,18 +702,7 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics -- NB ctxt2: don't suppress inner insolubles if there's only a -- wanted insoluble here; but do suppress inner insolubles -- if there's a *given* insoluble here (= inaccessible code) - - -- If there are no other errors to report, report suppressed errors. - -- See (SCE3) in 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 tidy_cts = bagToList (mapBag (tidyCt env) simples) @@ -752,15 +866,6 @@ 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) - | otherwise - = False - isSkolemTy :: TcLevel -> Type -> Bool -- The type is a skolem tyvar isSkolemTy tc_lvl ty @@ -778,113 +883,8 @@ isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of Just (tc,_) | isTypeFamilyTyCon tc -> Just tc _ -> Nothing -{- Note [Suppressing confusing errors] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -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 should be 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. - -Historical (SCE2). Fundep constraints never "escape" into the - main solver and so never show up in error messages. - See (SOLVE-FD) in Note [Overview of functional dependencies in type inference] - in GHC.Tc.Solver.FunDeps. So this wrinkle is now just a historical note. - - Errors which arise from the interaction of two Wanted fun-dep constraints. - Example: - - class C a b | a -> b where - op :: a -> b -> b - - foo _ = op True Nothing - - bar _ = op False [] - - Here, we could infer - foo :: C Bool (Maybe a) => p -> Maybe a - bar :: C Bool [a] => p -> [a] - - (The unused arguments suppress the monomorphism restriction.) The problem - is that these types can't both be correct, as they violate the functional - dependency. Yet reporting an error here is awkward: we must - non-deterministically choose either foo or bar to reject. We thus want - to report this problem only when there is nothing else to report. - See typecheck/should_fail/T13506 for an example of when to suppress - the error. The case above is actually accepted, because foo and bar - are checked separately, and thus the two fundep constraints never - encounter each other. It is test case typecheck/should_compile/FunDepOrigin1. - - This case applies only when both fundeps are *Wanted* fundeps; when - both are givens, the error represents unreachable code. For - a Given/Wanted case, see #9612. - - End of historical (SCE2) - -(SCE3) How can it happen that there are /only/ suppressed errors? See test T18851 - for an example of how it is (just, barely) possible for the /only/ errors to - be superclass-of-Wanted constraints. - -Mechanism: - -We use the `suppress` function within reportWanteds to filter out these -"suppress" cases, then report all other errors. After doing so, we return to these -suppressed ones and report them only if there have been no errors so far. - -Note [Constraints to ignore] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Some constraints are meant only to aid the solver by unification; a failure -to solve them is not necessarily an error to report to the user. It is critical -that compilation is aborted elsewhere if there are any ignored constraints here; -they will remain unfilled, and might have been used to rewrite another constraint. - -Currently, the constraints to ignore are: - -(CIG1) Constraints generated in order to unify associated type instance parameters - with class parameters. Here are two illustrative examples: - - class C (a :: k) where - type F (b :: k) - - instance C True where - type F a = Int - - instance C Left where - type F (Left :: a -> Either a b) = Bool - - In the first instance, we want to infer that `a` has type Bool. So we emit - a constraint unifying kappa (the guessed type of `a`) with Bool. All is well. - - In the second instance, we process the associated type instance only - after fixing the quantified type variables of the class instance. We thus - have skolems a1 and b1 such that the class instance is for (Left :: a1 -> Either a1 b1). - Unifying a1 and b1 with a and b in the type instance will fail, but harmlessly so. - checkConsistentFamInst checks for this, and will fail if anything has gone - awry. Really the equality constraints emitted are just meant as an aid, not - a requirement. This is test case T13972. - - We detect this case by looking for an origin of AssocFamPatOrigin; constraints - with this origin are dropped entirely during error message reporting. - - 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] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- 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-u…) See Note [The Unsatisfiable constraint] in GHC.TypeError. ===================================== testsuite/tests/typecheck/should_fail/T27731.hs ===================================== @@ -0,0 +1,36 @@ +{-# LANGUAGE ImplicitParams, TypeFamilies #-} + +module Bug where + +type family St (a :: k) :: * +type family Ev (a :: k) :: * -> * + +data T1 a = C1 a +data T2 h g = C2 (h ()) + +class (h ~ Ev g, s ~ St g) => Ren s h g + +f1 :: + (s ~ St h, Ren s h g, ?settings :: settings) + => (g v -> g ()) -> g v -> g () +f1 form = (\_ a -> a) (C1 (f2 {-@g-})) form + +f2 :: forall g h s. ( s ~ St h, Ren s h g) => T2 h g +f2 = error "urk" + +{- Call of f2 + +[W] s ~ St h --> St g ~ St h --> St g ~ St (Ev g) +[W] Ren s h g +[W] s ~ St g -- Superclass of wanted +[W] h ~ Ev g -- Superclass of wanted +-} + +{- +f3 :: + T1 () + -> (g v -> g ()) + -> g v -> g () +f3 wd form = ((\_ a -> a) wd form) + +-} ===================================== testsuite/tests/typecheck/should_fail/T27731.stderr ===================================== @@ -0,0 +1,16 @@ +T27731.hs:16:28: [GHC-05617] + • Could not deduce ‘St (Ev g0) ~ St g0’ + arising from a superclass required to satisfy ‘Ren + (St (Ev g0)) (Ev g0) g0’, + arising from a use of ‘f2’ + from the context: (s ~ St h, Ren s h g, ?settings::settings) + bound by the type signature for: + f1 :: forall s (h :: * -> *) (g :: * -> *) settings v. + (s ~ St h, Ren s h g, ?settings::settings) => + (g v -> g ()) -> g v -> g () + at T27731.hs:(13,1)-(15,33) + Note: ‘St’ is a non-injective type family. + The type variable ‘g0’ is ambiguous + • In the first argument of ‘C1’, namely ‘(f2)’ + In the first argument of ‘\ _ a -> a’, namely ‘(C1 (f2))’ + In the expression: (\ _ a -> a) (C1 (f2)) form ===================================== testsuite/tests/typecheck/should_fail/all.T ===================================== @@ -763,3 +763,4 @@ test('T26861', normal, compile_fail, ['']) test('T26862', normal, compile_fail, ['']) test('T27210', normal, compile_fail, ['']) test('T26532', normal, compile_fail, ['']) +test('T27731', normal, compile_fail, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4d53774327fbbbf7d8295980609ee59… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4d53774327fbbbf7d8295980609ee59… You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0

[Git][ghc/ghc][wip/T26543b] Line up simpleUnifyCheck and check_ty_eq_rhs
by Simon Peyton Jones (＠simonpj) 22 Aug '26

22 Aug '26

Simon Peyton Jones pushed to branch wip/T26543b at Glasgow Haskell Compiler / GHC Commits: 5c48df62 by Simon Peyton Jones at 2026-08-22T19:23:18+01:00 Line up simpleUnifyCheck and check_ty_eq_rhs Even after #26543 was allegedly fixed, the original repo case in the Description continued to fail. The reason was that the QuickLook unifier, `qlUnify`, used `simpleUnifyCheck` for checking unification invariants; and `simpleUnifyCheck` conservatively rejected any RHS with a coercion hole in it. The upshot was that QuickLook was not as clever as it should be, wrongly failing to do an impredicative instantiation. Interestingly `check_ty_eq_rhs`, which does the same job, only during constraint solving, was more liberal: it just looked at the free vars of the coercion, and allowed coercion holes. This MR lines them up, adding some careful notes. See Note [simpleUnifyCheck] esp (SUC1) Note [Unification preconditions] esp (COERCIONS) Things are better than before, but I am still uncomfortable about the possibilty that a hole might be filled with a coercion that mentions the LHS type variable; for now I have left this discomfort documented in (SUC1). - - - - - 5 changed files: - compiler/GHC/Core/TyCo/FVs.hs - compiler/GHC/Tc/Gen/App.hs - compiler/GHC/Tc/Utils/Unify.hs - + testsuite/tests/typecheck/should_compile/T26543_orig.hs - testsuite/tests/typecheck/should_compile/all.T Changes: ===================================== compiler/GHC/Core/TyCo/FVs.hs ===================================== @@ -850,15 +850,15 @@ invisibleVarsOfTypes = foldr (unionVarSet . invisibleVarsOfType) emptyVarSet {-# INLINE afvFolder #-} -- so that specialization to (const True) works afvFolder :: (TyCoVar -> Bool) -> TyCoFolder (FV TyCoVarSet DM.Any) -- 'afvFolder' is short for "any-free-var folder", good for checking --- if any free var of a type satisfies a predicate `check_fv` +-- if any shallow free var of a type satisfies a predicate `check_fv` afvFolder check_fv = TyCoFolder { tcf_view = noView -- See Note [Free vars and synonyms] , tcf_tyvar = do_tcv, tcf_covar = do_tcv , tcf_hole = do_hole , tcf_tycobinder = addBndrFV } where - do_tcv tv = MkFV $ \ bvs -> - Any (not (tv `elemVarSet` bvs) && check_fv tv) - do_hole _ = mempty -- I'm unsure; probably never happens + do_tcv tv = MkFV $ \ bvs -> + Any (not (tv `elemVarSet` bvs) && check_fv tv) + do_hole hole = do_tcv (coHoleCoVar hole) anyFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool anyFreeVarsOfType check_fv ty = DM.getAny (runFVTop (f ty)) ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -631,11 +631,13 @@ tcInstFun :: QLFlag -- plus the modification in Fig 5, of the QL paper: -- "A quick look at impredicativity" (ICFP'20). tcInstFun do_ql inst_final rn_head@(_, fun_lspan) tc_fun fun_sigma rn_args - = do { traceTc "tcInstFun" (vcat [ text "tc_fun" <+> ppr tc_fun + = do { lvl <- getTcLevel + ; traceTc "tcInstFun" (vcat [ text "tc_fun" <+> ppr tc_fun , text "rn_fun" <+> ppr rn_head , text "fun_sigma" <+> ppr fun_sigma , text "args:" <+> ppr rn_args - , text "do_ql" <+> ppr do_ql]) + , text "do_ql" <+> ppr do_ql + , text "lvl:" <+> ppr lvl ]) ; fun_origin <- mk_origin rn_head ; res@(_, fun_ty) <- go fun_origin 1 [] fun_sigma rn_args ; traceTc "tcInstFun:ret" (ppr fun_ty) @@ -1377,13 +1379,15 @@ tc_inst_forall_arg conc_tvs (tvb, inner_ty) hs_ty -- is not fully zonked, because ty_arg is fully zonked. -- See Note [Type application substitution]. + ; lvl <- getTcLevel ; traceTc "tc_inst_forall_arg (VTA/VDQ)" ( vcat [ text "fun_ty" <+> ppr fun_ty , text "tv" <+> ppr tv <+> dcolon <+> debugPprType kind , text "ty_arg" <+> debugPprType ty_arg <+> dcolon <+> debugPprType (typeKind ty_arg) , text "inner_ty" <+> debugPprType inner_ty - , text "insted_ty" <+> debugPprType insted_ty ]) + , text "insted_ty" <+> debugPprType insted_ty + , text "lvl:" <+> ppr lvl ]) ; return (ty_arg, insted_ty) } {- Note [Visible type application and abstraction] @@ -1934,11 +1938,13 @@ quickLookArg1 pos app_lspan rn_head larg@(L _ arg) sc_arg_ty@(Scaled _ orig_arg_ -- capture and save it in the `EValArgQL`. See (QLA6) in -- Note [Quick Look at value arguments] + ; lvl <- getTcLevel ; traceTc "quickLookArg {" $ vcat [ text "arg:" <+> ppr arg , text "orig_arg_rho:" <+> ppr orig_arg_rho , text "head:" <+> ppr rn_fun_arg <+> dcolon <+> ppr mb_fun_ty - , text "args:" <+> ppr rn_args ] + , text "args:" <+> ppr rn_args + , text "level:" <+> ppr lvl ] ; case mb_fun_ty of { Nothing -> skipQuickLook app_lspan larg sc_arg_ty ; -- fun is too complicated @@ -2158,18 +2164,23 @@ qlUnify :: TcType -> TcType -> TcM () -- * It may return without having made the argument types equal, of course; -- it just makes best efforts. qlUnify ty1 ty2 - = do { traceTc "qlUnify" (ppr ty1 $$ ppr ty2) + = do { lvl <- getTcLevel + ; traceTc "qlUnify" (ppr lvl $$ ppr ty1 $$ ppr ty2) ; go ty1 ty2 } where go :: TcType -> TcType -> TcM () + go t1 t2 = do { traceTc "qlUinfy:go" (ppr t1 <+> char '~' <+> ppr t2) + ; go' t1 t2 } + -- Decompose (arg1 -> res1) ~ (arg2 -> res2) -- and (c1 => res1) ~ (c2 => res2) -- But for the latter we only learn instantiation info from res1~res2 - go (FunTy { ft_af = af1, ft_arg = arg1, ft_res = res1 }) + go' (FunTy { ft_af = af1, ft_arg = arg1, ft_res = res1 }) (FunTy { ft_af = af2, ft_arg = arg2, ft_res = res2 }) | af1 == af2 -- Match the arrow TyCon - = do { when (isVisibleFunArg af1) (go arg1 arg2) + = do { traceTc "go_fun" (ppr arg1 $$ ppr arg2) + ; when (isVisibleFunArg af1) (go arg1 arg2) -- NB: we do not unify the multiplicities; that would be too strong. -- We might only require mult1 ⩽ mult2, as in Note [Multiplicity in deep subsumption]. @@ -2178,30 +2189,30 @@ qlUnify ty1 ty2 ; go res1 res2 } -- Make sure to not unify "kappa := (a %1 -> b)". See (UQL5). - go (FunTy { ft_mult = OneTy }) _ = return () - go _ (FunTy { ft_mult = OneTy }) = return () + go' (FunTy { ft_mult = OneTy }) _ = return () + go' _ (FunTy { ft_mult = OneTy }) = return () -- NB: we do want to be able to unify "kappa := a => b", as that's -- the main point of QuickLook (allowing meta-variables to be unified -- with qualified types). - go (TyVarTy tv) ty2 + go' (TyVarTy tv) ty2 | isMetaTyVar tv = go_kappa tv ty2 - go ty1 (TyVarTy tv) + go' ty1 (TyVarTy tv) | isMetaTyVar tv = go_kappa tv ty1 - go (CastTy ty1 _) ty2 = go ty1 ty2 - go ty1 (CastTy ty2 _) = go ty1 ty2 + go' (CastTy ty1 _) ty2 = go ty1 ty2 + go' ty1 (CastTy ty2 _) = go ty1 ty2 - go (TyConApp tc1 []) (TyConApp tc2 []) + go' (TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2 -- See GHC.Tc.Utils.Unify = return () -- Note [Expanding synonyms during unification] -- Now, and only now, expand synonyms - go rho1 rho2 + go' rho1 rho2 | Just rho1 <- coreView rho1 = go rho1 rho2 | Just rho2 <- coreView rho2 = go rho1 rho2 - go (TyConApp tc1 tys1) (TyConApp tc2 tys2) + go' (TyConApp tc1 tys1) (TyConApp tc2 tys2) | tc1 == tc2 , not (isTypeFamilyTyCon tc1) , tys1 `equalLength` tys2 @@ -2209,14 +2220,14 @@ qlUnify ty1 ty2 -- Don't allow unifying (a => b) with the AppTy 'arr[tau] a b'. -- To ensure this, use 'tcSplitAppTyNoView_maybe' which does not split (=>). - go (AppTy t1a t1b) ty2 + go' (AppTy t1a t1b) ty2 | Just (t2a, t2b) <- tcSplitAppTyNoView_maybe ty2 = do { go t1a t2a; go t1b t2b } - go ty1 (AppTy t2a t2b) + go' ty1 (AppTy t2a t2b) | Just (t1a, t1b) <- tcSplitAppTyNoView_maybe ty1 = do { go t1a t2a; go t1b t2b } - go _ _ = return () + go' _ _ = return () -- Don't look under foralls; see (UQL4) of Note [QuickLook unification] ---------------- @@ -2244,7 +2255,11 @@ qlUnify ty1 ty2 -- Here we are in the TcM monad, which does not track enclosing -- Given equalities; so for quick-look unification we conservatively -- treat /any/ level outside this one as untouchable. Hence cur_lvl. + ; traceTc "go_flexi1" (ppr kappa $$ ppr ty2) ; case simpleUnifyCheck UC_QuickLook cur_lvl kappa ty2 of + -- qlUnify depends, regrettably delicately, on the exact choices made + -- by `simpleUnifyCheck`. See (SUC1) in + -- Note [simpleUnifyCheck] in GHC.Tc.Utils.Unify SUC_CanUnify -> do { co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind -- unifyKind: see (UQL2) in Note [QuickLook unification] @@ -2253,7 +2268,8 @@ qlUnify ty1 ty2 ; traceTc "qlUnify:update" $ ppr kappa <+> text ":=" <+> ppr ty2 ; liftZonkM $ writeMetaTyVar kappa ty2' } - _ -> return () -- e.g. occurs-check or forall-bound variable + suc -> do { traceTc "go_flexi2" (ppr suc $$ ppr kappa $$ ppr ty2) + ; return () } -- e.g. occurs-check or forall-bound variable } where kappa_kind = tyVarKind kappa ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -103,7 +103,6 @@ import GHC.Types.Id( idType ) import GHC.Types.Var as Var import GHC.Types.Var.Set import GHC.Types.Var.Env -import GHC.Types.Var.FV import GHC.Types.Basic import GHC.Types.Unique.Set (nonDetEltsUniqSet) @@ -120,7 +119,6 @@ import GHC.Data.Maybe (firstJusts) import Control.Monad import Data.Functor.Identity (Identity(..)) import qualified Data.List.NonEmpty as NE -import Data.Monoid as DM ( Any(..) ) import qualified Data.Semigroup as S ( (<>) ) import Data.Traversable (for) @@ -3143,6 +3141,7 @@ uUnfilledVar2 env@(UE { u_defer = def_eq_ref, u_given_eq_lvl = given_eq_lvl }) do { traceTc "uUnfilledVar2 not ok" $ vcat [ text "tv1:" <+> ppr tv1 , text "ty2:" <+> ppr ty2 + , text "given_eq_lvl:" <+> ppr given_eq_lvl , text "simple-unify-chk:" <+> ppr (simpleUnifyCheck UC_OnTheFly given_eq_lvl tv1 ty2) ] -- Occurs check or an untouchable: just defer @@ -3246,6 +3245,7 @@ lhsPriority tv ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Question: given a homogeneous equality (alpha ~# ty), when is it OK to unify alpha := ty? + (This note only applies to /homogeneous/ equalities, in which both sides have the same kind.) @@ -3354,6 +3354,14 @@ Needless to say, all there are wrinkles: GHC.Tc.Solver.floatEqualities, around Nov 2020. It's much easier to unify in-place, with no floating. +* (COERCIONS) What if there are coercions in the RHS? E.g. + alpha ~ (ty |> co) + or alpha ~ (ty co) + We only recurse into the `coercionType` of `co` rather than `co` itself. + Why? Mainly because `co` might be a coercion hole, in which case we /can't/ + recurse into the coercion that will eventually fill the hole. This came + up in #26543. + Note [TyVar/TyVar orientation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ See also Note [Fundeps with instances, and equality orientation] @@ -3619,6 +3627,8 @@ simpleUnifyCheck :: UnifyCheckCaller -> TcLevel -> TcTyVar -> TcType -> SimpleUn -- unification might still be OK, but it'll take more work to do -- (use the full 'checkTypeEq'). -- +-- See Note [simpleUnifyCheck] +-- -- * Rejects if lhs_tv occurs in rhs_ty (occurs check) -- * Rejects foralls unless -- lhs_tv is RuntimeUnk (used by GHCi debugger) @@ -3638,10 +3648,7 @@ simpleUnifyCheck caller given_eq_lvl lhs_tv rhs | otherwise = SUC_NotSure where - lhs_info = metaTyVarInfo lhs_tv - - !(occ_in_ty, occ_in_co) = mkOccFolders (tyVarName lhs_tv) - + lhs_info = metaTyVarInfo lhs_tv lhs_tv_lvl = tcTyVarLevel lhs_tv lhs_tv_is_concrete = isConcreteTyVar lhs_tv @@ -3660,11 +3667,12 @@ simpleUnifyCheck caller given_eq_lvl lhs_tv rhs UC_OnTheFly -> False rhs_is_ok (TyVarTy tv) - | lhs_tv == tv = False - | tcTyVarLevel tv `strictlyDeeperThan` lhs_tv_lvl = False - | lhs_tv_is_concrete, not (isConcreteTyVar tv) = False - | occ_in_ty $! (tyVarKind tv) = False - | otherwise = True + | lhs_tv == tv = False -- Occurs check + | tcTyVarLevel tv `strictlyDeeperThan` lhs_tv_lvl = False + | lhs_tv_is_concrete, not (isConcreteTyVar tv) = False + | not (rhs_is_ok $! tyVarKind tv) = False + | otherwise = True + -- Hmm. We probably don't need the level check inside the kind, but no harm rhs_is_ok (FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r}) | not forall_ok, isInvisibleFunArg af = False @@ -3681,33 +3689,44 @@ simpleUnifyCheck caller given_eq_lvl lhs_tv rhs | otherwise = False rhs_is_ok (AppTy t1 t2) = rhs_is_ok t1 && rhs_is_ok t2 - rhs_is_ok (CastTy ty co) = not (occ_in_co co) && rhs_is_ok ty - rhs_is_ok (CoercionTy co) = not (occ_in_co co) + rhs_is_ok (CastTy ty co) = co_is_ok co && rhs_is_ok ty + rhs_is_ok (CoercionTy co) = co_is_ok co rhs_is_ok (LitTy {}) = True + -- For coercions we look only in the /type/ of the coercion + -- See (SUC1) in Note [simpleUnifyCheck] + co_is_ok co = rhs_is_ok (coercionType co) -mkOccFolders :: Name -> (TcType -> Bool, TcCoercion -> Bool) --- These functions return True --- * if lhs_tv occurs (incl deeply, in the kind of variable) --- * if there is a coercion hole --- No expansion of type synonyms -mkOccFolders lhs_tv = ( getAny . runFVTop . check_ty - , getAny . runFVTop . check_co) - where - check_ty :: Type -> FV BoundVars Any - !(check_ty, _, check_co, _) = foldTyCo occ_folder - - occ_folder :: TyCoFolder (FV BoundVars Any) - occ_folder = TyCoFolder { tcf_view = noView -- Don't expand synonyms - , tcf_tyvar = do_tcv, tcf_covar = do_tcv - , tcf_hole = do_hole - , tcf_tycobinder = addBndrFV } - - do_tcv v = (MkFV $ \ bvs -> - Any (not (v `elemVarSet` bvs) && tyVarName v == lhs_tv)) - `mappend` check_ty (varType v) - - do_hole _hole = MkFV $ \ _bvs -> DM.Any True -- Reject coercion holes +{- Note [simpleUnifyCheck] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +The function `simpleUnifyCheck` is asimple, /fast/ check for unifying (tv ~ rhs). +It can return a definite decision (SUC_CannotUnify of SUC_CanUnify), or uncertainty +(SUC_NotSure). In the latter case we will later use `checkTyEqRhs` to resolve. +In particular, `simpleUnifyCheck`: + +* Rejects if lhs_tv occurs in rhs_ty (occurs check) +* Rejects foralls unless + lhs_tv is RuntimeUnk (used by GHCi debugger) + or is a QL instantiation variable +* Rejects a non-concrete type if lhs_tv is concrete +* Rejects type families unless fam_ok=True +* Does a level-check for type variables, to avoid skolem escape + +This function is pretty heavily used, so it's optimised not to allocate. + +(SUC1) `simpleUnifyCheck` used by QuickLook's `qlUnify`, and anything other than + SUC_CanUnify will tell `qlUnify` not to proceed. That makes QuickLook depend + (regrettably, delicately) on the exact choices made by `simpleUnifyCheck`. + + A case in point: in #26543. In the repro case in the Descriptions, `qlUnify` failed + because there was a coercion hole in the RHS; but one that was ultimately Refl. + + So we only look at the /kind/ of a coercion, not the evidence itself. I'm a bit + worried about building a loop, if the evidence mentions the LHS unification + variable; but I can't see how that can happen, and I /really/ don't want to be + super-conservative for coercion holes (#26543). So, for now at least, we look + just at the kind of the coercion. +-} {- ********************************************************************* * * @@ -4337,7 +4356,11 @@ checkCo flags co = -- Occurs check (can promote) | OC_Check lhs_tv occ_prob <- occ , LC_Promote { lc_lvlp = lhs_tv_lvl } <- lc - -> do { reason <- checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl (tyCoVarsOfCo co) + -> do { reason <- checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl $ + tyCoVarsOfCo co + -- Maybe we should just check the free vars of the + -- /type/ of the coercion, to line up with + -- (SUC1) in Note [simpleUnifyCheck] ; return $ if cterHasNoProblem reason then pure co @@ -4697,12 +4720,14 @@ simpleOccursCheck :: OccursCheck -> TcTyVar -> TyVarCheckResult m simpleOccursCheck OC_None _ = TyVarCheck_Success simpleOccursCheck (OC_Check lhs_tv occ_prob) occ_tv - | lhs_tv == tyVarName occ_tv || check_kind (tyVarKind occ_tv) - = TyVarCheck_Error (cteProblem occ_prob) - | otherwise - = TyVarCheck_Success + | check_fv occ_tv = TyVarCheck_Error (cteProblem occ_prob) + | otherwise = TyVarCheck_Success where - (check_kind, _) = mkOccFolders lhs_tv + check_fv :: TyCoVar -> Bool -- True <=> occurs check + check_fv occ_tcv + | lhs_tv == tyVarName occ_tcv = True + | anyFreeVarsOfType check_fv (tyVarKind occ_tcv) = True + | otherwise = False ------------------------- tyVarLevelCheck :: LevelCheck m -> TcTyVar -> TyVarCheckResult m ===================================== testsuite/tests/typecheck/should_compile/T26543_orig.hs ===================================== @@ -0,0 +1,36 @@ +-- This test is from the Description of #26543 + +{-# LANGUAGE GHC2024, TypeAbstractions, AllowAmbiguousTypes, NoImplicitPrelude, + TypeFamilies, UndecidableInstances #-} +module T26543_orig where + +import Data.Kind +import Control.Applicative (Applicative(..)) +import Prelude (type (~), ($)) + +type CAT k = k -> k -> Type + +type family (~>) :: CAT k +type family Ob (a :: k) :: Constraint +type family UN (w :: j -> k) (wa :: k) :: j + +class HasBinaryProducts k where + type (a :: k) && (b :: k) :: k + withObProd :: (Ob (a :: k), Ob b) => ((Ob (a && b)) => r) -> r + (&&&) :: ((a :: k) ~> x) -> (a ~> y) -> (a ~> (x && y)) + +data AP (f :: Type -> Type) k = A k +type instance UN A (A k) = k + +type Ap :: CAT (AP f k) +data Ap a b where + Ap :: forall {k} a b f. (Ob a, Ob b) => f (a ~> b) -> Ap (A a :: AP f k) (A b) + +type instance (~>) = Ap +type instance Ob a = (a ~ A (UN A a), Ob (UN A a)) + +instance (Applicative f, HasBinaryProducts k) => HasBinaryProducts (AP f k) where + type a && b = A (UN A a && UN A b) + withObProd @(A a) @(A b) r = withObProd @k @a @b r + -- (&&&) :: Ap (a :: AP f k) x -> Ap a y -> Ap a (x && y) + Ap @_ @x f &&& Ap @_ @y g = withObProd @k @x @y $ Ap (liftA2 (&&&) f g) ===================================== testsuite/tests/typecheck/should_compile/all.T ===================================== @@ -969,3 +969,4 @@ test('ExpansionQLIm', normal, compile, ['']) test('T23135', normal, compile, ['']) test('LazyFieldAnnotations', normal, compile, ['']) test('T27557', normal, compile, ['']) +test('T26543_orig', normal, compile, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5c48df6252b5421cd41c957e410a2aa… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5c48df6252b5421cd41c957e410a2aa… You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0

[Git][ghc/ghc] Pushed new branch wip/T26543b
by Simon Peyton Jones (＠simonpj) 22 Aug '26

22 Aug '26

Simon Peyton Jones pushed new branch wip/T26543b at Glasgow Haskell Compiler / GHC -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/T26543b You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0

[Git][ghc/ghc][wip/T26961] Add Data.RealFloat and Infinity/NegInfinity/NaN pattern synonyms (#26961)
by Brandon Chinn (＠brandonchinn178) 22 Aug '26

22 Aug '26

Brandon Chinn pushed to branch wip/T26961 at Glasgow Haskell Compiler / GHC Commits: 93a67fe4 by Brandon Chinn at 2026-08-22T10:11:56-07:00 Add Data.RealFloat and Infinity/NegInfinity/NaN pattern synonyms (#26961) - - - - - 6 changed files: - libraries/base/base.cabal.in - libraries/base/changelog.md - + libraries/base/src/Data/RealFloat.hs - testsuite/tests/interface-stability/base-exports.stdout - testsuite/tests/interface-stability/base-exports.stdout-javascript-unknown-ghcjs - testsuite/tests/interface-stability/base-exports.stdout-mingw32 Changes: ===================================== libraries/base/base.cabal.in ===================================== @@ -117,6 +117,7 @@ Library , Data.Monoid , Data.Ord , Data.Proxy + , Data.RealFloat , Data.STRef , Data.STRef.Strict , Data.String ===================================== libraries/base/changelog.md ===================================== @@ -9,6 +9,8 @@ * Introduce `Data.Double` and `Data.Float` modules. ([CLC proposal #378](https://github.com/haskell/core-libraries-committee/issues/378)) * Change `Generically a`'s `Monoid` definition to require a `Semigroup` constraint, and define its `mconcat` using `(<>)` from that constraint. ([CLC proposal #413](https://github.com/haskell/core-libraries-committee/issues/413)) * Add `withEmptyCallStack` to `GHC.Stack`. ([CLC proposal #428](https://github.com/haskell/core-libraries-committee/issues/428)) + * Add new `Data.RealFloat` module re-exporting `RealFloat` from `GHC.Float` ([CLC proposal #394](https://github.com/haskell/core-libraries-committee/issues/394)) + * Add `Infinity`, `NegInfinity`, and `NaN` pattern synonyms to `Data.RealFloat` ([CLC proposal #394](https://github.com/haskell/core-libraries-committee/issues/394)) ## 4.23.0.0 *TBA* * Add `System.IO.hGetNewlineMode`. ([CLC proposal #370](https://github.com/haskell/core-libraries-committee/issues/370)) ===================================== libraries/base/src/Data/RealFloat.hs ===================================== @@ -0,0 +1,59 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE ViewPatterns #-} + +-- | +-- +-- Module : Data.RealFloat +-- Copyright : (c) The University of Glasgow 2026 +-- License : BSD-style (see the file libraries/base/LICENSE) +-- +-- Maintainer : libraries(a)haskell.org +-- Stability : stable +-- Portability : portable +-- + +module Data.RealFloat ( + RealFloat (..), + + -- * Infinity + NaN + pattern Infinity, + pattern NegInfinity, + pattern NaN, +) where + +import Data.Bool (Bool (..), (&&)) +import GHC.Internal.Data.Ord ((<), (>)) +import GHC.Internal.Float (RealFloat (..)) +import GHC.Internal.Real ((/)) +#if __GLASGOW_HASKELL__ >= 1001 +import qualified GHC.Essentials as Rebindable +#endif + +pattern Infinity :: (RealFloat a) => a +pattern Infinity <- ((\x -> isInfinite x && x > 0) -> True) where Infinity = 1/0 + +-- | Negative infinity +-- +-- Provided for convenience. Could also use the following instead: +-- * Pattern matching: @(negate -> Infinity)@ +-- * Expressions: @-Infinity@ +pattern NegInfinity :: (RealFloat a) => a +pattern NegInfinity <- ((\x -> isInfinite x && x < 0) -> True) where NegInfinity = -1/0 + +-- | A pattern synonym for NaN values. +-- +-- Note: Per IEEE 754, NaN is never equal to itself, thus these two snippets +-- have different behavior: +-- +-- @ +-- -- foo1 NaN == "a" +-- foo1 NaN = "a" +-- foo1 _ = "b" +-- +-- -- foo2 NaN == "b" +-- foo2 x = if x == NaN then "a" else "b" +-- @ +pattern NaN :: (RealFloat a) => a +pattern NaN <- (isNaN -> True) where NaN = 0/0 ===================================== testsuite/tests/interface-stability/base-exports.stdout ===================================== @@ -1626,6 +1626,29 @@ module Data.Ratio where denominator :: forall a. Ratio a -> a numerator :: forall a. Ratio a -> a +module Data.RealFloat where + -- Safety: Safe + pattern Infinity :: forall a. RealFloat a => a + pattern NaN :: forall a. RealFloat a => a + pattern NegInfinity :: forall a. RealFloat a => a + type RealFloat :: * -> Constraint + class (GHC.Internal.Real.RealFrac a, GHC.Internal.Float.Floating a) => RealFloat a where + floatRadix :: a -> GHC.Internal.Bignum.Integer.Integer + floatDigits :: a -> GHC.Internal.Types.Int + floatRange :: a -> (GHC.Internal.Types.Int, GHC.Internal.Types.Int) + decodeFloat :: a -> (GHC.Internal.Bignum.Integer.Integer, GHC.Internal.Types.Int) + encodeFloat :: GHC.Internal.Bignum.Integer.Integer -> GHC.Internal.Types.Int -> a + exponent :: a -> GHC.Internal.Types.Int + significand :: a -> a + scaleFloat :: GHC.Internal.Types.Int -> a -> a + isNaN :: a -> GHC.Internal.Types.Bool + isInfinite :: a -> GHC.Internal.Types.Bool + isDenormalized :: a -> GHC.Internal.Types.Bool + isNegativeZero :: a -> GHC.Internal.Types.Bool + isIEEE :: a -> GHC.Internal.Types.Bool + atan2 :: a -> a -> a + {-# MINIMAL floatRadix, floatDigits, floatRange, decodeFloat, encodeFloat, isNaN, isInfinite, isDenormalized, isNegativeZero, isIEEE #-} + module Data.STRef where -- Safety: Safe type role STRef nominal representational ===================================== testsuite/tests/interface-stability/base-exports.stdout-javascript-unknown-ghcjs ===================================== @@ -1626,6 +1626,29 @@ module Data.Ratio where denominator :: forall a. Ratio a -> a numerator :: forall a. Ratio a -> a +module Data.RealFloat where + -- Safety: Safe + pattern Infinity :: forall a. RealFloat a => a + pattern NaN :: forall a. RealFloat a => a + pattern NegInfinity :: forall a. RealFloat a => a + type RealFloat :: * -> Constraint + class (GHC.Internal.Real.RealFrac a, GHC.Internal.Float.Floating a) => RealFloat a where + floatRadix :: a -> GHC.Internal.Bignum.Integer.Integer + floatDigits :: a -> GHC.Internal.Types.Int + floatRange :: a -> (GHC.Internal.Types.Int, GHC.Internal.Types.Int) + decodeFloat :: a -> (GHC.Internal.Bignum.Integer.Integer, GHC.Internal.Types.Int) + encodeFloat :: GHC.Internal.Bignum.Integer.Integer -> GHC.Internal.Types.Int -> a + exponent :: a -> GHC.Internal.Types.Int + significand :: a -> a + scaleFloat :: GHC.Internal.Types.Int -> a -> a + isNaN :: a -> GHC.Internal.Types.Bool + isInfinite :: a -> GHC.Internal.Types.Bool + isDenormalized :: a -> GHC.Internal.Types.Bool + isNegativeZero :: a -> GHC.Internal.Types.Bool + isIEEE :: a -> GHC.Internal.Types.Bool + atan2 :: a -> a -> a + {-# MINIMAL floatRadix, floatDigits, floatRange, decodeFloat, encodeFloat, isNaN, isInfinite, isDenormalized, isNegativeZero, isIEEE #-} + module Data.STRef where -- Safety: Safe type role STRef nominal representational ===================================== testsuite/tests/interface-stability/base-exports.stdout-mingw32 ===================================== @@ -1626,6 +1626,29 @@ module Data.Ratio where denominator :: forall a. Ratio a -> a numerator :: forall a. Ratio a -> a +module Data.RealFloat where + -- Safety: Safe + pattern Infinity :: forall a. RealFloat a => a + pattern NaN :: forall a. RealFloat a => a + pattern NegInfinity :: forall a. RealFloat a => a + type RealFloat :: * -> Constraint + class (GHC.Internal.Real.RealFrac a, GHC.Internal.Float.Floating a) => RealFloat a where + floatRadix :: a -> GHC.Internal.Bignum.Integer.Integer + floatDigits :: a -> GHC.Internal.Types.Int + floatRange :: a -> (GHC.Internal.Types.Int, GHC.Internal.Types.Int) + decodeFloat :: a -> (GHC.Internal.Bignum.Integer.Integer, GHC.Internal.Types.Int) + encodeFloat :: GHC.Internal.Bignum.Integer.Integer -> GHC.Internal.Types.Int -> a + exponent :: a -> GHC.Internal.Types.Int + significand :: a -> a + scaleFloat :: GHC.Internal.Types.Int -> a -> a + isNaN :: a -> GHC.Internal.Types.Bool + isInfinite :: a -> GHC.Internal.Types.Bool + isDenormalized :: a -> GHC.Internal.Types.Bool + isNegativeZero :: a -> GHC.Internal.Types.Bool + isIEEE :: a -> GHC.Internal.Types.Bool + atan2 :: a -> a -> a + {-# MINIMAL floatRadix, floatDigits, floatRange, decodeFloat, encodeFloat, isNaN, isInfinite, isDenormalized, isNegativeZero, isIEEE #-} + module Data.STRef where -- Safety: Safe type role STRef nominal representational View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/93a67fe4acd08a1ab434c8f0f10983a… -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/93a67fe4acd08a1ab434c8f0f10983a… You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help

1 0