[Git][ghc/ghc][wip/T23162-spj] 2 commits: Wibble static forms

Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC Commits: d70b4bf9 by Simon Peyton Jones at 2025-10-09T17:29:22+01:00 Wibble static forms - - - - - a04df3ea by Simon Peyton Jones at 2025-10-09T17:39:59+01:00 Wibble comments in FunDeps - - - - - 6 changed files: - compiler/GHC/Tc/Errors.hs - compiler/GHC/Tc/Errors/Ppr.hs - compiler/GHC/Tc/Solver/FunDeps.hs - compiler/GHC/Tc/Types/Constraint.hs - testsuite/tests/typecheck/no_skolem_info/T13499.stderr - testsuite/tests/typecheck/should_fail/TcStaticPointersFail03.stderr Changes: ===================================== compiler/GHC/Tc/Errors.hs ===================================== @@ -1658,7 +1658,7 @@ validHoleFits ctxt@(CEC { cec_encl = implics -- See Note [Constraints include ...] givenConstraints :: SolverReportErrCtxt -> [(Type, RealSrcSpan)] givenConstraints ctxt - = do { implic@Implic{ ic_given = given } <- cec_encl ctxt + = do { implic@Implic{ ic_given = given } <- getUserGivens ctxt ; constraint <- given ; return (varType constraint, getCtLocEnvLoc (ic_env implic)) } ===================================== compiler/GHC/Tc/Errors/Ppr.hs ===================================== @@ -5399,10 +5399,14 @@ usefulContext implics pred = go implics where pred_tvs = tyCoVarsOfType pred + go :: [Implication] -> [SkolemInfoAnon] go [] = [] go (ic : ics) - | implausible ic = rest - | otherwise = ic_info ic : rest + | StaticFormSkol <- ic_info ic = [] + -- Stop at a static form, because all outer Givens are irrelevant + -- See (SF3) in Note [Grand plan for static forms] in GHC.Iface.Tidy.StaticPtrTable + | implausible ic = rest + | otherwise = ic_info ic : rest where -- Stop when the context binds a variable free in the predicate rest | any (`elemVarSet` pred_tvs) (ic_skols ic) = [] ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -369,12 +369,13 @@ For /non-built-in/ type families we do not create constraints from: * Given/instance fundep interactions via functional dependencies or type family injectivity annotations. -NB: for /built-in type families/ we DO create constraints, because - we can make evidence for them. +NB: for /built-in type families/ we DO create constraints, + because we can make evidence for them. + See Note [Given/Given fundeps for built-in type families]. In this Note, all these interactions are called just "fundeps". -We ingore such fundeps for several reasons: +We ignore such fundeps for several reasons: 1. These fundeps will never serve a purpose in accepting more programs: Given constraints do not contain metavariables that could @@ -404,7 +405,7 @@ We ingore such fundeps for several reasons: But we don't have a way to produce evidence for fundeps, as a Wanted it is /useless/. - (Historical aside: we used to keep fundep-generate Wanteds around, so + (Historical aside: we used to keep fundep-generated Wanteds around, so this insoluble constraint would generate a (misleading) error message. Nowadays we discard unsolved fundeps. End of historial aside.) @@ -427,8 +428,11 @@ We ingore such fundeps for several reasons: where beta is untouchable (under other equality constraints), leading to other insoluble constraints. End of historical aside.) -The bottom line: since we have no evidence for them, for user-defined type -families we should ignore Given/Given and Given/instance fundeps entirely. +The bottom line: + since we have no evidence for them, we should ignore + Given/Given and Given/instance fundeps entirely, for + * Type-class fundeps + * Fundeps for user-defined type families Note [Given/Given fundeps for built-in type families] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -1631,8 +1631,26 @@ data HasGivenEqs -- See Note [HasGivenEqs] type UserGiven = Implication getUserGivensFromImplics :: [Implication] -> [UserGiven] +-- The argument [Implication] is innermost first; +-- the returned [UserGiven] is outermost first getUserGivensFromImplics implics - = reverse (filterOut (null . ic_given) implics) + = get [] implics + where + get :: [UserGiven] -> [Implication] -> [UserGiven] + -- The accumulator is outermost first + get acc [] = acc + + get acc (implic : implics) + | StaticFormSkol <- ic_info implic + = acc -- For static forms, ignore all outer givens + -- See (SF3) in Note [Grand plan for static forms] in GHC.Iface.Tidy.StaticPtrTable + + | null (ic_given implic) -- No givens, so drop this one + = get acc implics + + | otherwise + = get (implic:acc) implics + {- Note [HasGivenEqs] ~~~~~~~~~~~~~~~~~~~~~ ===================================== testsuite/tests/typecheck/no_skolem_info/T13499.stderr ===================================== @@ -1,14 +1,14 @@ T13499.hs:7:19: error: [GHC-88464] - • Found hole: _ :: a1 - Where: ‘a1’ is a rigid type variable bound by + • Found hole: _ :: a + Where: ‘a’ is a rigid type variable bound by the type signature for: - f :: forall a1. Typeable a1 => StaticPtr (a1 -> a1) + f :: forall a. Typeable a => StaticPtr (a -> a) at T13499.hs:6:1-37 • In the body of a static form: (\ a -> _) In the expression: static (\ a -> _) In an equation for ‘f’: f = static (\ a -> _) • Relevant bindings include - a :: a1 (bound at T13499.hs:7:14) - f :: StaticPtr (a1 -> a1) (bound at T13499.hs:7:1) - Valid hole fits include a :: a1 (bound at T13499.hs:7:14) + a :: a (bound at T13499.hs:7:14) + f :: StaticPtr (a -> a) (bound at T13499.hs:7:1) + Valid hole fits include a :: a (bound at T13499.hs:7:14) ===================================== testsuite/tests/typecheck/should_fail/TcStaticPointersFail03.stderr ===================================== @@ -1,5 +1,5 @@ TcStaticPointersFail03.hs:9:29: error: [GHC-39999] - • No instance for ‘Monad m1’ arising from a use of ‘return’ + • No instance for ‘Monad m’ arising from a use of ‘return’ • In the body of a static form: return In the first argument of ‘deRefStaticPtr’, namely ‘(static return)’ In the expression: deRefStaticPtr (static return) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/3d46320533d41230ad9b6363be656f5... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/3d46320533d41230ad9b6363be656f5... You're receiving this email because of your account on gitlab.haskell.org.
participants (1)
-
Simon Peyton Jones (@simonpj)