Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC Commits: acc70c3a by Simon Peyton Jones at 2025-11-18T16:21:20-05:00 Fix a bug in defaulting Addresses #26582 Defaulting was doing some unification but then failing to iterate. Silly. I discovered that the main solver was unnecessarily iterating even if there was a unification for an /outer/ unification variable, so I fixed that too. - - - - - db17306c by Simon Peyton Jones at 2025-11-18T16:54:13-05:00 Make PmLit be in Ord, and use it in Map This MR addresses #26514, by changing from data PmAltConSet = PACS !(UniqDSet ConLike) ![PmLit] to data PmAltConSet = PACS !(UniqDSet ConLike) !(Map PmLit PmLit) This matters when doing pattern-match overlap checking, when there is a very large set of patterns. For most programs it makes no difference at all. For the N=5000 case of the repro case in #26514, compiler mutator time (with `-fno-code`) goes from 1.9s to 0.43s. All for the price for an Ord instance for PmLit - - - - - 7d33a35f by sheaf at 2025-11-18T16:54:29-05:00 Add passing tests for #26311 and #26072 This commit adds two tests cases that now pass since landing the changes to typechecking of data constructors in b33284c7. Fixes #26072 #26311 - - - - - d3a65832 by sheaf at 2025-11-18T16:54:29-05:00 mkCast: weaken bad cast warning for multiplicity This commit weakens the warning message emitted when constructing a bad cast in mkCast to ignore multiplicity. Justification: since b33284c7, GHC uses sub-multiplicity coercions to typecheck data constructors. The coercion optimiser is free to discard these coercions, both for performance reasons, and because GHC's Core simplifier does not (yet) preserve linearity. We thus weaken 'mkCast' to use 'eqTypeIgnoringMultiplicity' instead of 'eqType', to avoid getting many spurious warnings about mismatched multiplicities. - - - - - 15 changed files: - compiler/GHC/Core/Utils.hs - compiler/GHC/HsToCore/Pmc/Solver/Types.hs - compiler/GHC/Tc/Solver/Default.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Solver/Solve.hs - compiler/GHC/Tc/Utils/TcType.hs - compiler/GHC/Types/SourceText.hs - + testsuite/tests/linear/should_run/T26311.hs - + testsuite/tests/linear/should_run/T26311.stdout - testsuite/tests/linear/should_run/all.T - testsuite/tests/pmcheck/should_compile/pmcOrPats.stderr - + testsuite/tests/rep-poly/T26072b.hs - testsuite/tests/rep-poly/all.T - + testsuite/tests/typecheck/should_compile/T26582.hs - testsuite/tests/typecheck/should_compile/all.T Changes: ===================================== compiler/GHC/Core/Utils.hs ===================================== @@ -78,7 +78,7 @@ import GHC.Core.Type as Type import GHC.Core.Predicate( isEqPred ) import GHC.Core.Predicate( isUnaryClass ) import GHC.Core.FamInstEnv -import GHC.Core.TyCo.Compare( eqType, eqTypeX ) +import GHC.Core.TyCo.Compare( eqType, eqTypeX, eqTypeIgnoringMultiplicity ) import GHC.Core.Coercion import GHC.Core.Reduction import GHC.Core.TyCon @@ -275,7 +275,7 @@ mkCast expr co = assertPpr (coercionRole co == Representational) (text "coercion" <+> ppr co <+> text "passed to mkCast" <+> ppr expr <+> text "has wrong role" <+> ppr (coercionRole co)) $ - warnPprTrace (not (coercionLKind co `eqType` exprType expr)) "Bad cast" + warnPprTrace (not (coercionLKind co `eqTypeIgnoringMultiplicity` exprType expr)) "Bad cast" (vcat [ text "Coercion LHS kind does not match enclosed expression type" , text "co:" <+> ppr co , text "coercionLKind:" <+> ppr (coercionLKind co) ===================================== compiler/GHC/HsToCore/Pmc/Solver/Types.hs ===================================== @@ -2,6 +2,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE TypeFamilies #-} -- | Domain types used in "GHC.HsToCore.Pmc.Solver". -- The ultimate goal is to define 'Nabla', which models normalised refinement @@ -32,7 +33,7 @@ module GHC.HsToCore.Pmc.Solver.Types ( PmEquality(..), eqPmAltCon, -- *** Operations on 'PmLit' - literalToPmLit, negatePmLit, overloadPmLit, + literalToPmLit, negatePmLit, pmLitAsStringLit, coreExprAsPmLit ) where @@ -51,13 +52,12 @@ import GHC.Core.ConLike import GHC.Utils.Outputable import GHC.Utils.Panic.Plain import GHC.Utils.Misc (lastMaybe) -import GHC.Data.List.SetOps (unionLists) import GHC.Data.Maybe import GHC.Core.Type import GHC.Core.TyCon import GHC.Types.Literal import GHC.Core -import GHC.Core.TyCo.Compare( eqType ) +import GHC.Core.TyCo.Compare( eqType, nonDetCmpType ) import GHC.Core.Map.Expr import GHC.Core.Utils (exprType) import GHC.Builtin.Names @@ -69,15 +69,14 @@ import GHC.Types.CompleteMatch import GHC.Types.SourceText (SourceText(..), mkFractionalLit, FractionalLit , fractionalLitFromRational , FractionalExponentBase(..)) + import Numeric (fromRat) -import Data.Foldable (find) import Data.Ratio +import Data.List( find ) +import qualified Data.Map as FM import GHC.Real (Ratio(..)) -import qualified Data.Semigroup as Semi - --- import GHC.Driver.Ppr +import qualified Data.Semigroup as S --- -- * Normalised refinement types -- @@ -358,6 +357,13 @@ lookupSolution nabla x = case vi_pos (lookupVarInfo (nabla_tm_st nabla) x) of | Just sol <- find isDataConSolution pos -> Just sol | otherwise -> Just x + +{- ********************************************************************* +* * + PmLit and PmLitValue +* * +********************************************************************* -} + -------------------------------------------------------------------------------- -- The rest is just providing an IR for (overloaded!) literals and AltCons that -- sits between Hs and Core. We need a reliable way to detect and determine @@ -376,13 +382,64 @@ data PmLitValue = PmLitInt Integer | PmLitRat Rational | PmLitChar Char - -- We won't actually see PmLitString in the oracle since we desugar strings to - -- lists | PmLitString FastString + -- We won't actually see PmLitString in the oracle + -- since we desugar strings to lists + + -- Overloaded literals | PmLitOverInt Int {- How often Negated? -} Integer | PmLitOverRat Int {- How often Negated? -} FractionalLit | PmLitOverString FastString +-- | Syntactic equality. +-- We want (Ord PmLit) so that we can use (Map PmLit x) in `PmAltConSet` +instance Eq PmLit where + a == b = (a `compare` b) == EQ +instance Ord PmLit where + compare = cmpPmLit + +cmpPmLit :: PmLit -> PmLit -> Ordering +-- This function does "syntactic comparison": +-- For overloaded literals, compare the type and value +-- For non-overloaded literals, just compare the values +-- But it treats (say) +-- (PmLit Bool (PmLitOverInt 1)) +-- (PmLit Bool (PmLitOverInt 2)) +-- as un-equal, even through (fromInteger @Bool 1) +-- could be the same as (fromInteger @Bool 2) +cmpPmLit (PmLit { pm_lit_ty = t1, pm_lit_val = val1 }) + (PmLit { pm_lit_ty = t2, pm_lit_val = val2 }) + = case (val1,val2) of + (PmLitInt i1, PmLitInt i2) -> i1 `compare` i2 + (PmLitRat r1, PmLitRat r2) -> r1 `compare` r2 + (PmLitChar c1, PmLitChar c2) -> c1 `compare` c2 + (PmLitString s1, PmLitString s2) -> s1 `uniqCompareFS` s2 + (PmLitOverInt n1 i1, PmLitOverInt n2 i2) -> (n1 `compare` n2) S.<> + (i1 `compare` i2) S.<> + (t1 `nonDetCmpType` t2) + (PmLitOverRat n1 r1, PmLitOverRat n2 r2) -> (n1 `compare` n2) S.<> + (r1 `compare` r2) S.<> + (t1 `nonDetCmpType` t2) + (PmLitOverString s1, PmLitOverString s2) -> (s1 `uniqCompareFS` s2) S.<> + (t1 `nonDetCmpType` t2) + (PmLitInt {}, _) -> LT + (PmLitRat {}, PmLitInt {}) -> GT + (PmLitRat {}, _) -> LT + (PmLitChar {}, PmLitInt {}) -> GT + (PmLitChar {}, PmLitRat {}) -> GT + (PmLitChar {}, _) -> LT + (PmLitString {}, PmLitInt {}) -> GT + (PmLitString {}, PmLitRat {}) -> GT + (PmLitString {}, PmLitChar {}) -> GT + (PmLitString {}, _) -> LT + + (PmLitOverString {}, _) -> GT + (PmLitOverRat {}, PmLitOverString{}) -> LT + (PmLitOverRat {}, _) -> GT + (PmLitOverInt {}, PmLitOverString{}) -> LT + (PmLitOverInt {}, PmLitOverRat{}) -> LT + (PmLitOverInt {}, _) -> GT + -- | Undecidable semantic equality result. -- See Note [Undecidable Equality for PmAltCons] data PmEquality @@ -406,7 +463,10 @@ eqPmLit :: PmLit -> PmLit -> PmEquality eqPmLit (PmLit t1 v1) (PmLit t2 v2) -- no haddock | pprTrace "eqPmLit" (ppr t1 <+> ppr v1 $$ ppr t2 <+> ppr v2) False = undefined | not (t1 `eqType` t2) = Disjoint - | otherwise = go v1 v2 + | otherwise = eqPmLitValue v1 v2 + +eqPmLitValue :: PmLitValue -> PmLitValue -> PmEquality +eqPmLitValue v1 v2 = go v1 v2 where go (PmLitInt i1) (PmLitInt i2) = decEquality (i1 == i2) go (PmLitRat r1) (PmLitRat r2) = decEquality (r1 == r2) @@ -420,10 +480,6 @@ eqPmLit (PmLit t1 v1) (PmLit t2 v2) | s1 == s2 = Equal go _ _ = PossiblyOverlap --- | Syntactic equality. -instance Eq PmLit where - a == b = eqPmLit a b == Equal - -- | Type of a 'PmLit' pmLitType :: PmLit -> Type pmLitType (PmLit ty _) = ty @@ -445,34 +501,47 @@ eqConLike (PatSynCon psc1) (PatSynCon psc2) = Equal eqConLike _ _ = PossiblyOverlap + +{- ********************************************************************* +* * + PmAltCon and PmAltConSet +* * +********************************************************************* -} + -- | Represents the head of a match against a 'ConLike' or literal. -- Really similar to 'GHC.Core.AltCon'. data PmAltCon = PmAltConLike ConLike | PmAltLit PmLit -data PmAltConSet = PACS !(UniqDSet ConLike) ![PmLit] +data PmAltConSet = PACS !(UniqDSet ConLike) + !(FM.Map PmLit PmLit) +-- We use a (FM.Map PmLit PmLit) here, at the cost of requiring an Ord +-- instance for PmLit, because in extreme cases the set of PmLits can be +-- very large. See #26514. emptyPmAltConSet :: PmAltConSet -emptyPmAltConSet = PACS emptyUniqDSet [] +emptyPmAltConSet = PACS emptyUniqDSet FM.empty isEmptyPmAltConSet :: PmAltConSet -> Bool -isEmptyPmAltConSet (PACS cls lits) = isEmptyUniqDSet cls && null lits +isEmptyPmAltConSet (PACS cls lits) + = isEmptyUniqDSet cls && FM.null lits -- | Whether there is a 'PmAltCon' in the 'PmAltConSet' that compares 'Equal' to -- the given 'PmAltCon' according to 'eqPmAltCon'. elemPmAltConSet :: PmAltCon -> PmAltConSet -> Bool elemPmAltConSet (PmAltConLike cl) (PACS cls _ ) = elementOfUniqDSet cl cls -elemPmAltConSet (PmAltLit lit) (PACS _ lits) = elem lit lits +elemPmAltConSet (PmAltLit lit) (PACS _ lits) = isJust (FM.lookup lit lits) extendPmAltConSet :: PmAltConSet -> PmAltCon -> PmAltConSet extendPmAltConSet (PACS cls lits) (PmAltConLike cl) = PACS (addOneToUniqDSet cls cl) lits extendPmAltConSet (PACS cls lits) (PmAltLit lit) - = PACS cls (unionLists lits [lit]) + = PACS cls (FM.insert lit lit lits) pmAltConSetElems :: PmAltConSet -> [PmAltCon] pmAltConSetElems (PACS cls lits) - = map PmAltConLike (uniqDSetToList cls) ++ map PmAltLit lits + = map PmAltConLike (uniqDSetToList cls) ++ + FM.foldr ((:) . PmAltLit) [] lits instance Outputable PmAltConSet where ppr = ppr . pmAltConSetElems ===================================== compiler/GHC/Tc/Solver/Default.hs ===================================== @@ -395,9 +395,11 @@ tryConstraintDefaulting wc | isEmptyWC wc = return wc | otherwise - = do { (unif_happened, better_wc) <- reportCoarseGrainUnifications $ - go_wc False wc - -- We may have done unifications; so solve again + = do { (outermost_unif_lvl, better_wc) <- reportCoarseGrainUnifications $ + go_wc False wc + + -- We may have done unifications; if so, solve again + ; let unif_happened = not (isInfiniteTcLevel outermost_unif_lvl) ; solveAgainIf unif_happened better_wc } where go_wc :: Bool -> WantedConstraints -> TcS WantedConstraints @@ -414,14 +416,17 @@ tryConstraintDefaulting wc else return (Just ct) } go_implic :: Bool -> Implication -> TcS Implication - go_implic encl_eqs implic@(Implic { ic_status = status, ic_wanted = wanteds - , ic_given_eqs = given_eqs, ic_binds = binds }) + go_implic encl_eqs implic@(Implic { ic_tclvl = tclvl + , ic_status = status, ic_wanted = wanteds + , ic_given_eqs = given_eqs, ic_binds = binds }) | isSolvedStatus status = return implic -- Nothing to solve inside here | otherwise = do { let encl_eqs' = encl_eqs || given_eqs /= NoGivenEqs - ; wanteds' <- setEvBindsTcS binds $ + ; wanteds' <- setTcLevelTcS tclvl $ + -- Set the levels so that reportCoarseGrainUnifications works + setEvBindsTcS binds $ -- defaultCallStack sets a binding, so -- we must set the correct binding group go_wc encl_eqs' wanteds @@ -660,7 +665,9 @@ Wrinkles: f x = case x of T1 -> True Should we infer f :: T a -> Bool, or f :: T a -> a. Both are valid, but - neither is more general than the other. + neither is more general than the other. But by the time defaulting takes + place all let-bound variables have got their final types; defaulting won't + affect let-generalisation. (DE2) We still can't unify if there is a skolem-escape check, or an occurs check, or it it'd mean unifying a TyVarTv with a non-tyvar. It's only the ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -1877,18 +1877,18 @@ reportFineGrainUnifications (TcS thing_inside) ; recordUnifications outer_wu unif_tvs ; return (unif_tvs, res) } -reportCoarseGrainUnifications :: TcS a -> TcS (Bool, a) +reportCoarseGrainUnifications :: TcS a -> TcS (TcLevel, a) -- Record whether any useful unifications are done by thing_inside +-- Specifically: return the TcLevel of the outermost (smallest level) +-- unification variable that has been unified, or infiniteTcLevel if none -- Remember to propagate the information to the enclosing context reportCoarseGrainUnifications (TcS thing_inside) = TcS $ \ env@(TcSEnv { tcs_what = outer_what }) -> case outer_what of - WU_None - -> do { (unif_happened, _, res) <- report_coarse_grain_unifs env thing_inside - ; return (unif_happened, res) } + WU_None -> report_coarse_grain_unifs env thing_inside WU_Coarse outer_ul_ref - -> do { (unif_happened, inner_ul, res) <- report_coarse_grain_unifs env thing_inside + -> do { (inner_ul, res) <- report_coarse_grain_unifs env thing_inside -- Propagate to outer_ul_ref ; outer_ul <- TcM.readTcRef outer_ul_ref @@ -1897,31 +1897,32 @@ reportCoarseGrainUnifications (TcS thing_inside) ; TcM.traceTc "reportCoarse(Coarse)" $ vcat [ text "outer_ul" <+> ppr outer_ul - , text "inner_ul" <+> ppr inner_ul - , text "unif_happened" <+> ppr unif_happened ] - ; return (unif_happened, res) } + , text "inner_ul" <+> ppr inner_ul] + ; return (inner_ul, res) } WU_Fine outer_tvs_ref -> do { (unif_tvs,res) <- report_fine_grain_unifs env thing_inside - ; let unif_happened = not (isEmptyVarSet unif_tvs) - ; when unif_happened $ - TcM.updTcRef outer_tvs_ref (`unionVarSet` unif_tvs) + + -- Propagate to outer_tvs_rev + ; TcM.updTcRef outer_tvs_ref (`unionVarSet` unif_tvs) + + ; let outermost_unif_lvl = minTcTyVarSetLevel unif_tvs ; TcM.traceTc "reportCoarse(Fine)" $ vcat [ text "unif_tvs" <+> ppr unif_tvs - , text "unif_happened" <+> ppr unif_happened ] - ; return (unif_happened, res) } + , text "unif_happened" <+> ppr outermost_unif_lvl ] + ; return (outermost_unif_lvl, res) } report_coarse_grain_unifs :: TcSEnv -> (TcSEnv -> TcM a) - -> TcM (Bool, TcLevel, a) --- Returns (unif_happened, coarse_inner_ul, res) + -> TcM (TcLevel, a) +-- Returns the level number of the outermost +-- unification variable that is unified report_coarse_grain_unifs env thing_inside = do { inner_ul_ref <- TcM.newTcRef infiniteTcLevel ; res <- thing_inside (env { tcs_what = WU_Coarse inner_ul_ref }) - ; inner_ul <- TcM.readTcRef inner_ul_ref - ; ambient_lvl <- TcM.getTcLevel - ; let unif_happened = ambient_lvl `deeperThanOrSame` inner_ul - ; return (unif_happened, inner_ul, res) } - + ; inner_ul <- TcM.readTcRef inner_ul_ref + ; TcM.traceTc "report_coarse" $ + text "inner_lvl =" <+> ppr inner_ul + ; return (inner_ul, res) } report_fine_grain_unifs :: TcSEnv -> (TcSEnv -> TcM a) -> TcM (TcTyVarSet, a) ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -118,28 +118,34 @@ simplify_loop n limit definitely_redo_implications , int (lengthBag simples) <+> text "simples to solve" ]) ; traceTcS "simplify_loop: wc =" (ppr wc) - ; (simple_unif_happened, wc1) + ; ambient_lvl <- getTcLevel + ; (simple_unif_lvl, wc1) <- reportCoarseGrainUnifications $ -- See Note [Superclass iteration] solveSimpleWanteds simples -- Any insoluble constraints are in 'simples' and so get rewritten -- See Note [Rewrite insolubles] in GHC.Tc.Solver.InertSet -- Next, solve implications from wc_impl - ; (impl_unif_happened, implics') + ; let simple_unif_happened = ambient_lvl `deeperThanOrSame` simple_unif_lvl + ; (implic_unif_lvl, implics') <- if not (definitely_redo_implications -- See Note [Superclass iteration] || simple_unif_happened) -- for this conditional - then return (False, implics) + then return (infiniteTcLevel, implics) else reportCoarseGrainUnifications $ solveNestedImplications implics ; let wc' = wc1 { wc_impl = wc_impl wc1 `unionBags` implics' } - ; csTraceTcS $ text "unif_happened" <+> ppr impl_unif_happened - -- We iterate the loop only if the /implications/ did some relevant - -- unification. Even if the /simples/ did unifications we don't need - -- to re-do them. - ; maybe_simplify_again (n+1) limit impl_unif_happened wc' } + -- unification, hence looking only at `implic_unif_lvl`. (Even if the + -- /simples/ did unifications we don't need to re-do them.) + -- Also note that we only iterate if `implic_unify_lvl` is /equal to/ + -- the current level; if it is less , we'll iterate some outer level, + -- which will bring us back here anyway. + -- See Note [When to iterate the solver: unifications] + ; let implic_unif_happened = implic_unif_lvl `sameDepthAs` ambient_lvl + ; csTraceTcS $ text "implic_unif_happened" <+> ppr implic_unif_happened + ; maybe_simplify_again (n+1) limit implic_unif_happened wc' } data NextAction = NA_Stop -- Just return the WantedConstraints @@ -148,7 +154,9 @@ data NextAction Bool -- See `definitely_redo_implications` in the comment -- for `simplify_loop` -maybe_simplify_again :: Int -> IntWithInf -> Bool +maybe_simplify_again :: Int -> IntWithInf + -> Bool -- True <=> Solving the implications did some unifications + -- at the current level; so iterate -> WantedConstraints -> TcS WantedConstraints maybe_simplify_again n limit unif_happened wc@(WC { wc_simple = simples }) = do { -- Look for reasons to stop or continue @@ -222,10 +230,10 @@ and if so it seems a pity to waste time iterating the implications (forall b. bl (If we add new Given superclasses it's a different matter: it's really worth looking at the implications.) -Hence the definitely_redo_implications flag to simplify_loop. It's usually -True, but False in the case where the only reason to iterate is new Wanted -superclasses. In that case we check whether the new Wanteds actually led to -any new unifications, and iterate the implications only if so. +Hence the `definitely_redo_implications` flag to `simplify_loop`. It's usually True, +but False in the case where the only reason to iterate is new Wanted superclasses. +In that case we check whether the new Wanteds actually led to any new unifications +(at all), and iterate the implications only if so. Note [When to iterate the solver: unifications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ===================================== compiler/GHC/Tc/Utils/TcType.hs ===================================== @@ -45,7 +45,7 @@ module GHC.Tc.Utils.TcType ( TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel, strictlyDeeperThan, deeperThanOrSame, sameDepthAs, tcTypeLevel, tcTyVarLevel, maxTcLevel, minTcLevel, - infiniteTcLevel, + infiniteTcLevel, isInfiniteTcLevel, -------------------------------- -- MetaDetails @@ -879,6 +879,10 @@ isTopTcLevel :: TcLevel -> Bool isTopTcLevel (TcLevel 0) = True isTopTcLevel _ = False +isInfiniteTcLevel :: TcLevel -> Bool +isInfiniteTcLevel QLInstVar = True +isInfiniteTcLevel _ = False + pushTcLevel :: TcLevel -> TcLevel -- See Note [TcLevel assignment] pushTcLevel (TcLevel us) = TcLevel (us + 1) ===================================== compiler/GHC/Types/SourceText.hs ===================================== @@ -188,6 +188,7 @@ data FractionalLit = FL } deriving (Data, Show) -- The Show instance is required for the derived GHC.Parser.Lexer.Token instance when DEBUG is on + -- Eq and Ord instances are done explicitly -- See Note [FractionalLit representation] in GHC.HsToCore.Match.Literal data FractionalExponentBase ===================================== testsuite/tests/linear/should_run/T26311.hs ===================================== @@ -0,0 +1,23 @@ +{-# LANGUAGE MagicHash #-} + +module Main where + +import GHC.Exts ( Int# ) + +expensive :: Int -> Int# +expensive 0 = 2# +expensive i = expensive (i-1) + +data D = MkD Int# Int + +f :: a -> Bool +f _ = False +{-# NOINLINE f #-} + +{-# RULES "f/MkD" forall x. f (MkD x) = True #-} + +bar :: Bool +bar = f (MkD (expensive 10)) + +main :: IO () +main = print bar ===================================== testsuite/tests/linear/should_run/T26311.stdout ===================================== @@ -0,0 +1 @@ +True ===================================== testsuite/tests/linear/should_run/all.T ===================================== @@ -1,2 +1,3 @@ test('LinearTypeable', normal, compile_and_run, ['']) +test('T26311', normal, compile_and_run, ['-O1']) test('LinearGhci', normal, ghci_script, ['LinearGhci.script']) ===================================== testsuite/tests/pmcheck/should_compile/pmcOrPats.stderr ===================================== @@ -1,4 +1,3 @@ - pmcOrPats.hs:10:1: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)] Pattern match(es) are non-exhaustive In an equation for ‘g’: Patterns of type ‘T’, ‘U’ not matched: A W @@ -18,7 +17,7 @@ pmcOrPats.hs:15:1: warning: [GHC-53633] [-Woverlapping-patterns (in -Wdefault)] pmcOrPats.hs:17:1: warning: [GHC-62161] [-Wincomplete-patterns (in -Wextra)] Pattern match(es) are non-exhaustive In an equation for ‘z’: - Patterns of type ‘a’ not matched: p where p is not one of {3, 1, 2} + Patterns of type ‘a’ not matched: p where p is not one of {1, 2, 3} pmcOrPats.hs:19:1: warning: [GHC-53633] [-Woverlapping-patterns (in -Wdefault)] Pattern match is redundant @@ -43,3 +42,4 @@ pmcOrPats.hs:21:1: warning: [GHC-61505] • Patterns reported as unmatched might actually be matched Suggested fix: Increase the limit or resolve the warnings to suppress this message. + ===================================== testsuite/tests/rep-poly/T26072b.hs ===================================== @@ -0,0 +1,78 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UnboxedTuples #-} + +module T26072b where + +-- base +import Data.Kind +import GHC.TypeNats +import GHC.Exts + ( TYPE, RuntimeRep(..), LiftedRep + , proxy# + ) + +-------------------------------------------------------------------------------- + +-- Stub for functions in 'primitive' (to avoid dependency) +type PrimArray :: Type -> Type +data PrimArray a = MkPrimArray + +indexPrimArray :: PrimArray a -> Int -> a +indexPrimArray _ _ = error "unimplemented" +{-# NOINLINE indexPrimArray #-} + +-------------------------------------------------------------------------------- + +int :: forall n. KnownNat n => Int +int = fromIntegral ( natVal' @n proxy# ) + +type Fin :: Nat -> Type +newtype Fin n = Fin { getFin :: Int } + +-- Vector +type V :: Nat -> Type -> Type +newtype V n a = V ( PrimArray a ) + +-- Matrix +type M :: Nat -> Type -> Type +newtype M n a = M ( PrimArray a ) + +type IndexRep :: (Type -> Type) -> RuntimeRep +type family IndexRep f +class Ix f where + type Index f :: TYPE (IndexRep f) + (!) :: f a -> Index f -> a + infixl 9 ! + +type instance IndexRep ( V n ) = LiftedRep +instance Ix ( V n ) where + type Index ( V n ) = Fin n + V v ! Fin !i = indexPrimArray v i + {-# INLINE (!) #-} + +type instance IndexRep ( M m ) = TupleRep [ LiftedRep, LiftedRep ] + +instance KnownNat n => Ix ( M n ) where + type Index ( M n ) = (# Fin n, Fin n #) + M m ! (# Fin !i, Fin !j #) = indexPrimArray m ( i + j * int @n ) + {-# INLINE (!) #-} + +rowCol :: forall n a. ( KnownNat n, Num a ) => Fin n -> M n a -> V n a -> a +rowCol i m v = go 0 ( Fin 0 ) + where + n = int @n + go :: a -> Fin n -> a + go !acc j@( Fin !j_ ) + | j_ >= n + = acc + | otherwise + = go ( acc + m ! (# i , j #) * v ! j ) ( Fin ( j_ + 1 ) ) ===================================== testsuite/tests/rep-poly/all.T ===================================== @@ -127,6 +127,7 @@ test('T17536b', normal, compile, ['']) ## test('T21650_a', js_broken(26578), compile, ['-Wno-deprecated-flags']) ## test('T21650_b', js_broken(26578), compile, ['-Wno-deprecated-flags']) ## test('T26072', js_broken(26578), compile, ['']) ## +test('T26072b', js_broken(26578), compile, ['']) ## test('RepPolyArgument2', normal, compile, ['']) ## test('RepPolyCase2', js_broken(26578), compile, ['']) ## test('RepPolyRule3', normal, compile, ['']) ## ===================================== testsuite/tests/typecheck/should_compile/T26582.hs ===================================== @@ -0,0 +1,35 @@ +{-# LANGUAGE GADTs #-} + +module T26582 where + +sametype :: a -> a -> Int +sametype = sametype + +f :: Eq a => (a->Int) -> Int +f = f + +data T b where T1 :: T Bool + +g1 :: T b -> Int +g1 v = f (\x -> case v of { T1 -> sametype x True }) + +g2 :: Eq c => c -> T b -> Int +g2 c v = f (\x -> case v of { T1 -> sametype x c }) + +{- The point is that we get something like + + Wanted: [W] d : Eq alpha[1] + Implication + level: 2 + Given: b~Bool + + Wanted: [W] alpha[1]~Bool -- For g1 + Wanted: [W] alpha[1]~c -- For g2 + +So alpha is untouchable under the (b~Bool) from the GADT. +And yet in the end it's easy to solve +via alpha:=Bool, or alpha:=c resp + +But having done that defaulting we must then remember to +solved that `d : Eq alpha`! We forgot to so so in #26582. +-} ===================================== testsuite/tests/typecheck/should_compile/all.T ===================================== @@ -956,3 +956,4 @@ test('T26457', normal, compile, ['']) test('T17705', normal, compile, ['']) test('T14745', normal, compile, ['']) test('T26451', normal, compile, ['']) +test('T26582', normal, compile, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f4ab5d9e1a1ee58ccec3008b0b785ef... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f4ab5d9e1a1ee58ccec3008b0b785ef... You're receiving this email because of your account on gitlab.haskell.org.