GitLab

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC

Commits:

c052c724

by Simon Peyton Jones at 2025-11-06T21:34:06-05:00

Fix a horrible shadowing bug in implicit parameters

Fixes #26451.  The change is in GHC.Tc.Solver.Monad.updInertDicts
where we now do /not/ delete /Wanted/ implicit-parameeter constraints.

This bug has been in GHC since 9.8!  But it's quite hard to provoke;
I contructed a tests in T26451, but it was hard to do so.

4 changed files:

compiler/GHC/Tc/Solver/Dict.hs
compiler/GHC/Tc/Solver/Monad.hs
+ testsuite/tests/typecheck/should_compile/T26451.hs
testsuite/tests/typecheck/should_compile/all.T

Changes:

compiler/GHC/Tc/Solver/Dict.hs

@@ -263,7 +263,9 @@ in two places:
  * In `updInertDicts`, in this module, when adding [G] (?x :: ty), remove any
    existing [G] (?x :: ty'), regardless of ty'.
 -* Wrinkle (SIP1): we must be careful of superclasses.  Consider
 +There are wrinkles:
++
 +* Wrinkle (SIP1): we must be careful of superclasses (#14218).  Consider
       f,g :: (?x::Int, C a) => a -> a
       f v = let ?x = 4 in g v
@@ -271,24 +273,31 @@ in two places:
    We must /not/ solve this from the Given (?x::Int, C a), because of
    the intervening binding for (?x::Int).  #14218.
 -  We deal with this by arranging that when we add [G] (?x::ty) we delete
 +  We deal with this by arranging that when we add [G] (?x::ty) we /delete/
    * from the inert_cans, and
    * from the inert_solved_dicts
    any existing [G] (?x::ty) /and/ any [G] D tys, where (D tys) has a superclass
    with (?x::ty).  See Note [Local implicit parameters] in GHC.Core.Predicate.
 -  An important special case is constraint tuples like [G] (% ?x::ty, Eq a %).
 -  But it could happen for `class xx => D xx where ...` and the constraint D
 -  (?x :: int).  This corner (constraint-kinded variables instantiated with
 -  implicit parameter constraints) is not well explored.
 +  An very important special case is constraint tuples like [G] (% ?x::ty, Eq a %).
++
 +  But it could also happen for `class xx => D xx where ...` and the constraint
 +  D (?x :: int); again see Note [Local implicit parameters].  This corner
 +  (constraint-kinded variables instantiated with implicit parameter constraints)
 +  is not well explored.
 -  Example in #14218, and #23761
 +  You might worry about whether deleting an /entire/ constraint just because
 +  a distant superclass has an implicit parameter might make another Wanted for
 +  that constraint un-solvable.  Indeed so. But for constraint tuples it doesn't
 +  matter -- their entire payload is their superclasses.  And the other case is
 +  the ill-explored corner above.
    The code that accounts for (SIP1) is in updInertDicts; in particular the call to
    GHC.Core.Predicate.mentionsIP.
  * Wrinkle (SIP2): we must apply this update semantics for `inert_solved_dicts`
 -  as well as `inert_cans`.
 +  as well as `inert_cans` (#23761).
++
    You might think that wouldn't be necessary, because an element of
    `inert_solved_dicts` is never an implicit parameter (see
    Note [Solved dictionaries] in GHC.Tc.Solver.InertSet).
@@ -301,6 +310,19 @@ in two places:
    Now (C (?x::Int)) has a superclass (?x::Int). This may look exotic, but it
    happens particularly for constraint tuples, like `(% ?x::Int, Eq a %)`.
 +* Wrinkle (SIP3)
 +  - Note that for the inert dictionaries, `inert_cans`, we must /only/ delete
 +    existing /Givens/!  Deleting an existing Wanted led to #26451; we just never
 +    solved it!
++
 +  - In contrast, the solved dictionaries, `inert_solved_dicts`, are really like
 +    Givens; they may be "inherited" from outer scopes, so we must delete any
 +    solved dictionaries for this implicit parameter for /both/ Givens /and/
 +    Wanteds.
++
 +    Otherwise the new Given doesn't properly shadow those inherited solved
 +    dictionaries. Test T23761 showed this up.
++
  Example 1:
  Suppose we have (typecheck/should_compile/ImplicitParamFDs)

compiler/GHC/Tc/Solver/Monad.hs

@@ -377,28 +377,53 @@ in GHC.Tc.Solver.Dict.
  -}
  updInertDicts :: DictCt -> TcS ()
 -updInertDicts dict_ct@(DictCt { di_cls = cls, di_ev = ev, di_tys = tys })
 -  = do { traceTcS "Adding inert dict" (ppr dict_ct $$ ppr cls  <+> ppr tys)
+-
 -       ; if | isGiven ev, Just (str_ty, _) <- isIPPred_maybe cls tys
 -            -> -- For [G] ?x::ty, remove any dicts mentioning ?x,
 -              --    from /both/ inert_cans /and/ inert_solved_dicts (#23761)
 -               -- See (SIP1) and (SIP2) in Note [Shadowing of implicit parameters]
 -               updInertSet $ \ inerts@(IS { inert_cans = ics, inert_solved_dicts = solved }) ->
 -               inerts { inert_cans         = updDicts (filterDicts (does_not_mention_ip_for str_ty)) ics
 -                      , inert_solved_dicts = filterDicts (does_not_mention_ip_for str_ty) solved }
 -            | otherwise
 -            -> return ()
 +updInertDicts dict_ct
 +  = do { traceTcS "Adding inert dict" (ppr dict_ct)
++
 +       -- For Given implicit parameters (only), delete any existing
 +       -- Givens for the same implicit parameter.
 +       -- See Note [Shadowing of implicit parameters]
 +       ; deleteGivenIPs dict_ct
++
         -- Add the new constraint to the inert set
         ; updInertCans (updDicts (addDict dict_ct)) }
++
 +deleteGivenIPs :: DictCt -> TcS ()
 +-- Special magic when adding a Given implicit parameter to the inert set
 +-- For [G] ?x::ty, remove any existing /Givens/ mentioning ?x,
 +--    from /both/ inert_cans /and/ inert_solved_dicts (#23761)
 +-- See Note [Shadowing of implicit parameters]
 +deleteGivenIPs (DictCt { di_cls = cls, di_ev = ev, di_tys = tys })
 +  | isGiven ev
 +  , Just (str_ty, _) <- isIPPred_maybe cls tys
 +  = updInertSet $ \ inerts@(IS { inert_cans = ics, inert_solved_dicts = solved }) ->
 +    inerts { inert_cans         = updDicts (filterDicts (keep_can str_ty)) ics
 +           , inert_solved_dicts = filterDicts (keep_solved str_ty) solved }
 +  | otherwise
 +  = return ()
    where
 -    -- Does this class constraint or any of its superclasses mention
 -    -- an implicit parameter (?str :: ty) for the given 'str' and any type 'ty'?
 -    does_not_mention_ip_for :: Type -> DictCt -> Bool
 -    does_not_mention_ip_for str_ty (DictCt { di_cls = cls, di_tys = tys })
 -      = not $ mightMentionIP (not . typesAreApart str_ty) (const True) cls tys
 -        -- See Note [Using typesAreApart when calling mightMentionIP]
 -        -- in GHC.Core.Predicate
 +    keep_can, keep_solved :: Type -> DictCt -> Bool
 +    -- keep_can: we keep an inert dictionary UNLESS
 +    --   (1) it is a Given
 +    --   (2) it binds an implicit parameter (?str :: ty) for the given 'str'
 +    --       regardless of 'ty', possibly via its superclasses
 +    -- The test is a bit conservative, hence `mightMentionIP` and `typesAreApart`
 +    -- See Note [Using typesAreApart when calling mightMentionIP]
 +    -- in GHC.Core.Predicate
 +    --
 +    -- keep_solved: same as keep_can, but for /all/ constraints not just Givens
 +    --
 +    -- Why two functions?  See (SIP3) in Note [Shadowing of implicit parameters]
 +    keep_can str (DictCt { di_ev = ev, di_cls = cls, di_tys = tys })
 +      = not (isGiven ev                -- (1)
 +          && mentions_ip str cls tys)  -- (2)
 +    keep_solved str (DictCt { di_cls = cls, di_tys = tys })
 +      = not (mentions_ip str cls tys)
++
 +    -- mentions_ip: the inert constraint might provide evidence
 +    -- for an implicit parameter (?str :: ty) for the given 'str'
 +    mentions_ip str cls tys
 +      = mightMentionIP (not . typesAreApart str) (const True) cls tys
  updInertIrreds :: IrredCt -> TcS ()
  updInertIrreds irred

testsuite/tests/typecheck/should_compile/T26451.hs

 +{-# LANGUAGE ImplicitParams, TypeFamilies, FunctionalDependencies, ScopedTypeVariables #-}
++
 +module T26451 where
++
 +type family F a
 +type instance F Bool = [Char]
++
 +class C a b | b -> a
 +instance C Bool Bool
 +instance C Char Char
++
 +eq :: forall a b. C a b => a -> b -> ()
 +eq p q = ()
++
 +g :: a -> F a
 +g = g
++
 +f (x::tx) (y::ty)   -- x :: alpha y :: beta
 +  = let ?v = g x   -- ?ip :: F alpha
 +      in (?v::[ty], eq x True)
++
++
 +{- tx, and ty are unification variables
++
 +Inert: [G] dg :: IP "v" (F tx)
 +       [W] dw :: IP "v" [ty]
 +Work-list: [W] dc1 :: C tx Bool
 +           [W] dc2 :: C ty Char
++
 +* Solve dc1, we get tx := Bool from fundep
 +* Kick out dg
 +* Solve dg to get [G] dc : IP "v" [Char]
 +* Add that new dg to the inert set: that simply deletes dw!!!
 +-}

testsuite/tests/typecheck/should_compile/all.T

@@ -955,3 +955,4 @@ test('T26376', normal, compile, [''])
  test('T26457', normal, compile, [''])
  test('T17705', normal, compile, [''])
  test('T14745', normal, compile, [''])
 +test('T26451', normal, compile, [''])