[Git][ghc/ghc][master] Pmc: consider any 2 dicts of the same type equal
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Fri Aug 26 19:05:42 UTC 2022
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
4786acf7 by sheaf at 2022-08-26T15:05:23-04:00
Pmc: consider any 2 dicts of the same type equal
This patch massages the keys used in the `TmOracle` `CoreMap` to ensure
that dictionaries of coherent classes give the same key.
That is, whenever we have an expression we want to insert or lookup in
the `TmOracle` `CoreMap`, we first replace any dictionary
`$dict_abcd :: ct` with a value of the form `error @ct`.
This allows us to common-up view pattern functions with required
constraints whose arguments differed only in the uniques of the
dictionaries they were provided, thus fixing #21662.
This is a rather ad-hoc change to the keys used in the
`TmOracle` `CoreMap`. In the long run, we would probably want to use
a different representation for the keys instead of simply using
`CoreExpr` as-is. This more ambitious plan is outlined in #19272.
Fixes #21662
Updates unix submodule
- - - - -
6 changed files:
- compiler/GHC/Core/Predicate.hs
- compiler/GHC/HsToCore/Pmc/Solver.hs
- libraries/unix
- testsuite/tests/pmcheck/should_compile/T11822.stderr
- + testsuite/tests/pmcheck/should_compile/T21662.hs
- testsuite/tests/pmcheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/Predicate.hs
=====================================
@@ -243,7 +243,6 @@ isEqPrimPred ty = isCoVarType ty
isCTupleClass :: Class -> Bool
isCTupleClass cls = isTupleTyCon (classTyCon cls)
-
{- *********************************************************************
* *
Implicit parameters
=====================================
compiler/GHC/HsToCore/Pmc/Solver.hs
=====================================
@@ -58,9 +58,10 @@ import GHC.Types.Var.Set
import GHC.Core
import GHC.Core.FVs (exprFreeVars)
import GHC.Core.Map.Expr
+import GHC.Core.Predicate (typeDeterminesValue)
import GHC.Core.SimpleOpt (simpleOptExpr, exprIsConApp_maybe)
import GHC.Core.Utils (exprType)
-import GHC.Core.Make (mkListExpr, mkCharExpr)
+import GHC.Core.Make (mkListExpr, mkCharExpr, mkRuntimeErrorApp, rUNTIME_ERROR_ID)
import GHC.Types.Unique.Supply
import GHC.Data.FastString
import GHC.Types.SrcLoc
@@ -941,22 +942,121 @@ addCoreCt nabla x e = do
pm_alt_con_app :: Id -> PmAltCon -> [TyVar] -> [Id] -> StateT Nabla (MaybeT DsM) ()
pm_alt_con_app x con tvs args = modifyT $ \nabla -> addConCt nabla x con tvs args
+-- | Like 'modify', but with an effectful modifier action
+modifyT :: Monad m => (s -> m s) -> StateT s m ()
+modifyT f = StateT $ fmap ((,) ()) . f
+
-- | Finds a representant of the semantic equality class of the given @e at .
-- Which is the @x@ of a @let x = e'@ constraint (with @e@ semantically
-- equivalent to @e'@) we encountered earlier, or a fresh identifier if
-- there weren't any such constraints.
representCoreExpr :: Nabla -> CoreExpr -> DsM (Id, Nabla)
representCoreExpr nabla at MkNabla{ nabla_tm_st = ts at TmSt{ ts_reps = reps } } e
- | Just rep <- lookupCoreMap reps e = pure (rep, nabla)
+ | Just rep <- lookupCoreMap reps key = pure (rep, nabla)
| otherwise = do
rep <- mkPmId (exprType e)
- let reps' = extendCoreMap reps e rep
+ let reps' = extendCoreMap reps key rep
let nabla' = nabla{ nabla_tm_st = ts{ ts_reps = reps' } }
pure (rep, nabla')
+ where
+ key = makeDictsCoherent e
+ -- Use a key in which dictionaries for the same type become equal.
+ -- See Note [Unique dictionaries in the TmOracle CoreMap]
--- | Like 'modify', but with an effectful modifier action
-modifyT :: Monad m => (s -> m s) -> StateT s m ()
-modifyT f = StateT $ fmap ((,) ()) . f
+-- | Change out 'Id's which are uniquely determined by their type to a
+-- common value, so that different names for dictionaries of the same type
+-- are considered equal when building a 'CoreMap'.
+--
+-- See Note [Unique dictionaries in the TmOracle CoreMap]
+makeDictsCoherent :: CoreExpr -> CoreExpr
+makeDictsCoherent var@(Var v)
+ | let ty = idType v
+ , typeDeterminesValue ty
+ = mkRuntimeErrorApp rUNTIME_ERROR_ID ty "dictionary"
+ | otherwise
+ = var
+makeDictsCoherent lit@(Lit {})
+ = lit
+makeDictsCoherent (App f a)
+ = App (makeDictsCoherent f) (makeDictsCoherent a)
+makeDictsCoherent (Lam f body)
+ = Lam f (makeDictsCoherent body)
+makeDictsCoherent (Let bndr body)
+ = Let
+ (go_bndr bndr)
+ (makeDictsCoherent body)
+ where
+ go_bndr (NonRec bndr expr) = NonRec bndr (makeDictsCoherent expr)
+ go_bndr (Rec bndrs) = Rec (map ( \(b, expr) -> (b, makeDictsCoherent expr) ) bndrs)
+makeDictsCoherent (Case scrut bndr ty alts)
+ = Case scrut bndr ty
+ [ Alt con bndr expr'
+ | Alt con bndr expr <- alts
+ , let expr' = makeDictsCoherent expr ]
+makeDictsCoherent (Cast expr co)
+ = Cast (makeDictsCoherent expr) co
+makeDictsCoherent (Tick tick expr)
+ = Tick tick (makeDictsCoherent expr)
+makeDictsCoherent ty@(Type {})
+ = ty
+makeDictsCoherent co@(Coercion {})
+ = co
+
+{- Note [Unique dictionaries in the TmOracle CoreMap]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Any two dictionaries for a coherent typeclass should be considered equal
+in the TmOracle CoreMap, as this allows us to report better pattern-match
+warnings.
+
+Consider for example T21662:
+
+ view_fn :: forall (n :: Nat). KnownNat n => Int -> Bool
+
+ foo :: Int -> Int
+ foo (view_fn @12 -> True ) = 0
+ foo (view_fn @12 -> False) = 1
+
+In this example, the pattern match is exhaustive because we have covered
+the range of the view pattern function. However, we may fail to recognise
+the fact that the two cases use the same view function if the KnownNat
+dictionaries aren't syntactically equal:
+
+ eqn 1: [let ds_d1p0 = view_fn @12 $dKnownNat_a1ny ds_d1oR, True <- ds_d1p0]
+ eqn 2: [let ds_d1p6 = view_fn @12 $dKnownNat_a1nC ds_d1oR, False <- ds_d1p6]
+
+Note that the uniques of the KnownNat 12 dictionary differ. If we fail to utilise
+the coherence of the KnownNat constraint, then we have to pessimistically assume
+that we have two function calls with different arguments:
+
+ foo (fn arg1 -> True ) = ...
+ foo (fn arg2 -> False) = ...
+
+In this case we can't determine whether the pattern matches are complete, so we
+emit a pattern match warning.
+
+Solution: replace all 'Id's whose type uniquely determines its value with
+a common value, e.g. in the above example we would replace both
+$dKnownNat_a1ny and $dKnownNat_a1nC with error @(KnownNat 12).
+
+Why did we choose this solution? Here are some alternatives that were considered:
+
+ 1. Perform CSE first. This would common up the dictionaries before we compare
+ using the CoreMap.
+ However, this is architecturally difficult as it would require threading
+ a CSEnv through to desugarPat.
+ 2. Directly modify CoreMap so that any two dictionaries of the same type are
+ considered equal.
+ The problem is that this affects all users of CoreMap. For example, CSE
+ would now assume that any two dictionaries of the same type are equal,
+ but this isn't necessarily true in the presence of magicDict, which
+ violates coherence by design. It seems more prudent to limit the changes
+ to the pattern-match checker only, to avoid undesirable consequences.
+
+In the end, replacing dictionaries with an error value in the pattern-match
+checker was the most self-contained, although we might want to revisit once
+we implement a more robust approach to computing equality in the pattern-match
+checker (see #19272).
+-}
{- Note [The Pos/Neg invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
libraries/unix
=====================================
@@ -1 +1 @@
-Subproject commit 23edd4537e9051824a5683b324e6fb8abed5d6b3
+Subproject commit 2a6079a2b76adf29d3e3ff213dffe66cabcb76c3
=====================================
testsuite/tests/pmcheck/should_compile/T11822.stderr
=====================================
@@ -12,11 +12,3 @@ T11822.hs:33:1: warning: [-Wincomplete-patterns (in -Wextra)]
_ _
_ (Data.Sequence.Internal.Seq Data.Sequence.Internal.EmptyT) _ _
...
-
-T11822.hs:33:1: warning:
- Pattern match checker ran into -fmax-pmcheck-models=30 limit, so
- • Redundant clauses might not be reported at all
- • Redundant clauses might be reported as inaccessible
- • Patterns reported as unmatched might actually be matched
- Suggested fix:
- Increase the limit or resolve the warnings to suppress this message.
=====================================
testsuite/tests/pmcheck/should_compile/T21662.hs
=====================================
@@ -0,0 +1,21 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeApplications #-}
+
+module T21662 where
+
+import GHC.TypeNats (Nat, KnownNat)
+
+view_fn :: forall (n :: Nat). KnownNat n => Int -> Bool
+view_fn i = i > 0
+
+foo :: Int -> Int
+foo (view_fn @12 -> True) = 0
+foo (view_fn @12 -> False) = 0
+
+ -- The point is that the two view pattern functions "view_fn"
+ -- may get different uniques for the KnownNat 12 dictionary,
+ -- which leads to a spurious pattern match warning.
=====================================
testsuite/tests/pmcheck/should_compile/all.T
=====================================
@@ -111,6 +111,7 @@ test('CyclicSubst', [], compile, [overlapping_incomplete])
test('CaseOfKnownCon', [], compile, [overlapping_incomplete])
test('TooManyDeltas', [], compile, [overlapping_incomplete+'-fmax-pmcheck-models=0'])
test('LongDistanceInfo', [], compile, [overlapping_incomplete])
+test('T21662', [], compile, [overlapping_incomplete])
# Series (inspired) by Luke Maranget
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4786acf758ef064d3b79593774d1672e294b0afb
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4786acf758ef064d3b79593774d1672e294b0afb
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20220826/55a563c5/attachment-0001.html>
More information about the ghc-commits
mailing list