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
-
a04df3ea
by Simon Peyton Jones at 2025-10-09T17:39:59+01:00
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:
| ... | ... | @@ -1658,7 +1658,7 @@ validHoleFits ctxt@(CEC { cec_encl = implics |
| 1658 | 1658 | -- See Note [Constraints include ...]
|
| 1659 | 1659 | givenConstraints :: SolverReportErrCtxt -> [(Type, RealSrcSpan)]
|
| 1660 | 1660 | givenConstraints ctxt
|
| 1661 | - = do { implic@Implic{ ic_given = given } <- cec_encl ctxt
|
|
| 1661 | + = do { implic@Implic{ ic_given = given } <- getUserGivens ctxt
|
|
| 1662 | 1662 | ; constraint <- given
|
| 1663 | 1663 | ; return (varType constraint, getCtLocEnvLoc (ic_env implic)) }
|
| 1664 | 1664 |
| ... | ... | @@ -5399,10 +5399,14 @@ usefulContext implics pred |
| 5399 | 5399 | = go implics
|
| 5400 | 5400 | where
|
| 5401 | 5401 | pred_tvs = tyCoVarsOfType pred
|
| 5402 | + go :: [Implication] -> [SkolemInfoAnon]
|
|
| 5402 | 5403 | go [] = []
|
| 5403 | 5404 | go (ic : ics)
|
| 5404 | - | implausible ic = rest
|
|
| 5405 | - | otherwise = ic_info ic : rest
|
|
| 5405 | + | StaticFormSkol <- ic_info ic = []
|
|
| 5406 | + -- Stop at a static form, because all outer Givens are irrelevant
|
|
| 5407 | + -- See (SF3) in Note [Grand plan for static forms] in GHC.Iface.Tidy.StaticPtrTable
|
|
| 5408 | + | implausible ic = rest
|
|
| 5409 | + | otherwise = ic_info ic : rest
|
|
| 5406 | 5410 | where
|
| 5407 | 5411 | -- Stop when the context binds a variable free in the predicate
|
| 5408 | 5412 | rest | any (`elemVarSet` pred_tvs) (ic_skols ic) = []
|
| ... | ... | @@ -369,12 +369,13 @@ For /non-built-in/ type families we do not create constraints from: |
| 369 | 369 | * Given/instance fundep interactions via functional dependencies or
|
| 370 | 370 | type family injectivity annotations.
|
| 371 | 371 | |
| 372 | -NB: for /built-in type families/ we DO create constraints, because
|
|
| 373 | - we can make evidence for them.
|
|
| 372 | +NB: for /built-in type families/ we DO create constraints,
|
|
| 373 | + because we can make evidence for them.
|
|
| 374 | + See Note [Given/Given fundeps for built-in type families].
|
|
| 374 | 375 | |
| 375 | 376 | In this Note, all these interactions are called just "fundeps".
|
| 376 | 377 | |
| 377 | -We ingore such fundeps for several reasons:
|
|
| 378 | +We ignore such fundeps for several reasons:
|
|
| 378 | 379 | |
| 379 | 380 | 1. These fundeps will never serve a purpose in accepting more
|
| 380 | 381 | programs: Given constraints do not contain metavariables that could
|
| ... | ... | @@ -404,7 +405,7 @@ We ingore such fundeps for several reasons: |
| 404 | 405 | But we don't have a way to produce evidence for fundeps, as a Wanted it
|
| 405 | 406 | is /useless/.
|
| 406 | 407 | |
| 407 | - (Historical aside: we used to keep fundep-generate Wanteds around, so
|
|
| 408 | + (Historical aside: we used to keep fundep-generated Wanteds around, so
|
|
| 408 | 409 | this insoluble constraint would generate a (misleading) error message.
|
| 409 | 410 | Nowadays we discard unsolved fundeps. End of historial aside.)
|
| 410 | 411 | |
| ... | ... | @@ -427,8 +428,11 @@ We ingore such fundeps for several reasons: |
| 427 | 428 | where beta is untouchable (under other equality constraints), leading
|
| 428 | 429 | to other insoluble constraints. End of historical aside.)
|
| 429 | 430 | |
| 430 | -The bottom line: since we have no evidence for them, for user-defined type
|
|
| 431 | -families we should ignore Given/Given and Given/instance fundeps entirely.
|
|
| 431 | +The bottom line:
|
|
| 432 | + since we have no evidence for them, we should ignore
|
|
| 433 | + Given/Given and Given/instance fundeps entirely, for
|
|
| 434 | + * Type-class fundeps
|
|
| 435 | + * Fundeps for user-defined type families
|
|
| 432 | 436 | |
| 433 | 437 | Note [Given/Given fundeps for built-in type families]
|
| 434 | 438 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
| ... | ... | @@ -1631,8 +1631,26 @@ data HasGivenEqs -- See Note [HasGivenEqs] |
| 1631 | 1631 | type UserGiven = Implication
|
| 1632 | 1632 | |
| 1633 | 1633 | getUserGivensFromImplics :: [Implication] -> [UserGiven]
|
| 1634 | +-- The argument [Implication] is innermost first;
|
|
| 1635 | +-- the returned [UserGiven] is outermost first
|
|
| 1634 | 1636 | getUserGivensFromImplics implics
|
| 1635 | - = reverse (filterOut (null . ic_given) implics)
|
|
| 1637 | + = get [] implics
|
|
| 1638 | + where
|
|
| 1639 | + get :: [UserGiven] -> [Implication] -> [UserGiven]
|
|
| 1640 | + -- The accumulator is outermost first
|
|
| 1641 | + get acc [] = acc
|
|
| 1642 | + |
|
| 1643 | + get acc (implic : implics)
|
|
| 1644 | + | StaticFormSkol <- ic_info implic
|
|
| 1645 | + = acc -- For static forms, ignore all outer givens
|
|
| 1646 | + -- See (SF3) in Note [Grand plan for static forms] in GHC.Iface.Tidy.StaticPtrTable
|
|
| 1647 | + |
|
| 1648 | + | null (ic_given implic) -- No givens, so drop this one
|
|
| 1649 | + = get acc implics
|
|
| 1650 | + |
|
| 1651 | + | otherwise
|
|
| 1652 | + = get (implic:acc) implics
|
|
| 1653 | + |
|
| 1636 | 1654 | |
| 1637 | 1655 | {- Note [HasGivenEqs]
|
| 1638 | 1656 | ~~~~~~~~~~~~~~~~~~~~~
|
| 1 | 1 | T13499.hs:7:19: error: [GHC-88464]
|
| 2 | - • Found hole: _ :: a1
|
|
| 3 | - Where: ‘a1’ is a rigid type variable bound by
|
|
| 2 | + • Found hole: _ :: a
|
|
| 3 | + Where: ‘a’ is a rigid type variable bound by
|
|
| 4 | 4 | the type signature for:
|
| 5 | - f :: forall a1. Typeable a1 => StaticPtr (a1 -> a1)
|
|
| 5 | + f :: forall a. Typeable a => StaticPtr (a -> a)
|
|
| 6 | 6 | at T13499.hs:6:1-37
|
| 7 | 7 | • In the body of a static form: (\ a -> _)
|
| 8 | 8 | In the expression: static (\ a -> _)
|
| 9 | 9 | In an equation for ‘f’: f = static (\ a -> _)
|
| 10 | 10 | • Relevant bindings include
|
| 11 | - a :: a1 (bound at T13499.hs:7:14)
|
|
| 12 | - f :: StaticPtr (a1 -> a1) (bound at T13499.hs:7:1)
|
|
| 13 | - Valid hole fits include a :: a1 (bound at T13499.hs:7:14)
|
|
| 11 | + a :: a (bound at T13499.hs:7:14)
|
|
| 12 | + f :: StaticPtr (a -> a) (bound at T13499.hs:7:1)
|
|
| 13 | + Valid hole fits include a :: a (bound at T13499.hs:7:14)
|
|
| 14 | 14 |
| 1 | 1 | TcStaticPointersFail03.hs:9:29: error: [GHC-39999]
|
| 2 | - • No instance for ‘Monad m1’ arising from a use of ‘return’
|
|
| 2 | + • No instance for ‘Monad m’ arising from a use of ‘return’
|
|
| 3 | 3 | • In the body of a static form: return
|
| 4 | 4 | In the first argument of ‘deRefStaticPtr’, namely ‘(static return)’
|
| 5 | 5 | In the expression: deRefStaticPtr (static return)
|