summaryrefslogtreecommitdiff
path: root/compiler/GHC
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/GHC')
-rw-r--r--compiler/GHC/Core/Predicate.hs1
-rw-r--r--compiler/GHC/HsToCore/Pmc/Solver.hs112
2 files changed, 106 insertions, 7 deletions
diff --git a/compiler/GHC/Core/Predicate.hs b/compiler/GHC/Core/Predicate.hs
index b3fde40055..9751724d56 100644
--- a/compiler/GHC/Core/Predicate.hs
+++ b/compiler/GHC/Core/Predicate.hs
@@ -243,7 +243,6 @@ isEqPrimPred ty = isCoVarType ty
isCTupleClass :: Class -> Bool
isCTupleClass cls = isTupleTyCon (classTyCon cls)
-
{- *********************************************************************
* *
Implicit parameters
diff --git a/compiler/GHC/HsToCore/Pmc/Solver.hs b/compiler/GHC/HsToCore/Pmc/Solver.hs
index 26dac390b4..b78433283b 100644
--- a/compiler/GHC/HsToCore/Pmc/Solver.hs
+++ b/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@.
-- 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@MkNabla{ nabla_tm_st = ts@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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~