Commit c5d888d4 authored by Sebastian Graf's avatar Sebastian Graf Committed by Marge Bot

PmCheck: No ConLike instantiation in pmcheck

`pmcheck` used to call `refineToAltCon` which would refine the knowledge
we had about a variable by equating it to a `ConLike` application.
Since we weren't particularly smart about this in the Check module, we
simply freshened the constructors existential and term binders utimately
through a call to `mkOneConFull`.

But that instantiation is unnecessary for when we match against a
concrete pattern! The pattern will already have fresh binders and field
types. So we don't call `refineToAltCon` from `Check` anymore.

Subsequently, we can simplify a couple of call sites and functions in
`PmOracle`. Also implementing `computeCovered` becomes viable and we
don't have to live with the hack that was `addVarPatVecCt` anymore.

A side-effect of not indirectly calling `mkOneConFull` anymore is that
we don't generate the proper strict argument field constraints anymore.
Instead we now desugar ConPatOuts as if they had bangs on their strict
fields. This implies that `PmVar` now carries a `HsImplBang` that we
need to respect by a (somewhat ephemeral) non-void check. We fix #17234
in doing so.
parent 6f9fa0be
Pipeline #10718 failed with stages
in 406 minutes and 21 seconds
This diff is collapsed.
......@@ -7,9 +7,9 @@ Authors: George Karachalias <george.karachalias@cs.kuleuven.be>
{-# LANGUAGE CPP, LambdaCase, TupleSections, PatternSynonyms, ViewPatterns, MultiWayIf #-}
-- | The pattern match oracle. The main export of the module are the functions
-- 'addTmCt', 'refineToAltCon' and 'addRefutableAltCon' for adding
-- facts to the oracle, and 'provideEvidenceForEquation' to turn a 'Delta' into
-- a concrete evidence for an equation.
-- 'addTmCt', 'addVarCoreCt', 'addRefutableAltCon' and 'addTypeEvidence' for
-- adding facts to the oracle, and 'provideEvidenceForEquation' to turn a
-- 'Delta' into a concrete evidence for an equation.
module PmOracle (
DsM, tracePm, mkPmId,
......@@ -21,8 +21,6 @@ module PmOracle (
addRefutableAltCon, -- Add a negative term equality
addTmCt, -- Add a positive term equality x ~ e
addVarCoreCt, -- Add a positive term equality x ~ core_expr
refineToAltCon, -- Add a positive refinement x ~ K _ _
tmOracle, -- Add multiple positive term equalities
provideEvidenceForEquation,
) where
......@@ -149,9 +147,9 @@ getUnmatchedConstructor (PM _tc ms)
-- | Instantiate a 'ConLike' given its universal type arguments. Instantiates
-- existential and term binders with fresh variables of appropriate type.
-- Also returns instantiated evidence variables from the match and the types of
-- strict constructor fields.
mkOneConFull :: [Type] -> ConLike -> DsM ([Id], Bag TyCt, [Type], [TyVar])
-- Returns instantiated term variables from the match, type evidence and the
-- types of strict constructor fields.
mkOneConFull :: [Type] -> ConLike -> DsM ([Id], Bag TyCt, [Type])
-- * 'con' K is a ConLike
-- - In the case of DataCons and most PatSynCons, these
-- are associated with a particular TyCon T
......@@ -160,9 +158,8 @@ mkOneConFull :: [Type] -> ConLike -> DsM ([Id], Bag TyCt, [Type], [TyVar])
-- * 'arg_tys' tys are the types K's universally quantified type
-- variables should be instantiated to.
-- - For DataCons and most PatSyns these are the arguments of their TyCon
-- - For cases like in #11336, #17112, the univ_ts include those variables
-- from the view pattern, so tys will have to come from the type checker.
-- They can't easily be recovered from the result type.
-- - For cases like the PatSyns in #11336, #17112, we can't easily guess
-- these, so don't call this function.
--
-- After instantiating the universal tyvars of K to tys we get
-- K @tys :: forall bs. Q => s1 .. sn -> T tys
......@@ -173,15 +170,15 @@ mkOneConFull :: [Type] -> ConLike -> DsM ([Id], Bag TyCt, [Type], [TyVar])
-- Results: [y1,..,yn]
-- Q
-- [s1]
-- [e1,..,en]
mkOneConFull arg_tys con = do
let (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , field_tys, _con_res_ty)
= conLikeFullSig con
-- pprTrace "mkOneConFull" (ppr con $$ ppr arg_tys $$ ppr univ_tvs $$ ppr _con_res_ty) (return ())
-- Substitute universals for type arguments
let subst_univ = zipTvSubst univ_tvs arg_tys
-- Instantiate fresh existentials as arguments to the contructor
(subst, ex_tvs') <- cloneTyVarBndrs subst_univ ex_tvs <$> getUniqueSupplyM
-- Instantiate fresh existentials as arguments to the contructor. This is
-- important for instantiating the Thetas and field types.
(subst, _) <- cloneTyVarBndrs subst_univ ex_tvs <$> getUniqueSupplyM
let field_tys' = substTys subst field_tys
-- Instantiate fresh term variables (VAs) as arguments to the constructor
vars <- mapM mkPmId field_tys'
......@@ -191,17 +188,7 @@ mkOneConFull arg_tys con = do
-- Figure out the types of strict constructor fields
let arg_is_banged = map isBanged $ conLikeImplBangs con
strict_arg_tys = filterByList arg_is_banged field_tys'
return (vars, listToBag ty_cs, strict_arg_tys, ex_tvs')
equateTyVars :: [TyVar] -> [TyVar] -> Bag TyCt
equateTyVars ex_tvs1 ex_tvs2
= ASSERT(ex_tvs1 `equalLength` ex_tvs2)
listToBag $ catMaybes $ zipWith mb_to_evvar ex_tvs1 ex_tvs2
where
mb_to_evvar tv1 tv2
| tv1 == tv2 = Nothing
| otherwise = Just (to_evvar tv1 tv2)
to_evvar tv1 tv2 = TyCt $ mkPrimEqPred (mkTyVarTy tv1) (mkTyVarTy tv2)
return (vars, listToBag ty_cs, strict_arg_tys)
-------------------------
-- * Pattern match oracle
......@@ -689,11 +676,7 @@ warning messages (which can be alleviated by someone with enough dedication).
-- Returns a new 'Delta' if the new constraints are compatible with existing
-- ones.
tmIsSatisfiable :: Bag TmCt -> SatisfiabilityCheck
tmIsSatisfiable new_tm_cs = SC $ \delta -> tmOracle delta new_tm_cs
-- | External interface to the term oracle.
tmOracle :: Foldable f => Delta -> f TmCt -> DsM (Maybe Delta)
tmOracle delta = runMaybeT . foldlM go delta
tmIsSatisfiable new_tm_cs = SC $ \delta -> runMaybeT $ foldlM go delta new_tm_cs
where
go delta ct = MaybeT (addTmCt delta ct)
......@@ -773,12 +756,14 @@ lookupSolution delta x = case vi_pos (lookupVarInfo (delta_tm_st delta) x) of
-- | A term constraint. Either equates two variables or a variable with a
-- 'PmAltCon' application.
data TmCt
= TmVarVar !Id !Id
| TmVarCon !Id !PmAltCon ![Id]
= TmVarVar !Id !Id
| TmVarCon !Id !PmAltCon ![Id]
| TmVarNonVoid !Id
instance Outputable TmCt where
ppr (TmVarVar x y) = ppr x <+> char '~' <+> ppr y
ppr (TmVarCon x con args) = ppr x <+> char '~' <+> hsep (ppr con : map ppr args)
ppr (TmVarNonVoid x) = ppr x <+> text "/~ ⊥"
-- | Add type equalities to 'Delta'.
addTypeEvidence :: Delta -> Bag EvVar -> DsM (Maybe Delta)
......@@ -791,6 +776,7 @@ addTmCt :: Delta -> TmCt -> DsM (Maybe Delta)
addTmCt delta ct = runMaybeT $ case ct of
TmVarVar x y -> addVarVarCt delta (x, y)
TmVarCon x con args -> addVarConCt delta x con args
TmVarNonVoid x -> addVarNonVoidCt delta x
-- | Record that a particular 'Id' can't take the shape of a 'PmAltCon' in the
-- 'Delta' and return @Nothing@ if that leads to a contradiction.
......@@ -866,7 +852,7 @@ guessConLikeUnivTyArgsFromResTy env res_ty (RealDataCon _) = do
let (_, tc_args', _) = tcLookupDataFamInst env tc tc_args
Just tc_args'
guessConLikeUnivTyArgsFromResTy _ res_ty (PatSynCon ps) = do
-- We were successful if we managed to instantiate *every* univ_tv of con.
-- We are successful if we managed to instantiate *every* univ_tv of con.
-- This is difficult and bound to fail in some cases, see
-- Note [Pattern synonym result type] in PatSyn.hs. So we just try our best
-- here and be sure to return an instantiation when we can substitute every
......@@ -878,6 +864,17 @@ guessConLikeUnivTyArgsFromResTy _ res_ty (PatSynCon ps) = do
subst <- tcMatchTy con_res_ty res_ty
traverse (lookupTyVar subst) univ_tvs
-- | Kind of tries to add a non-void contraint to 'Delta', but doesn't really
-- commit to upholding that constraint in the future. This will be rectified
-- in a follow-up patch. The status quo should work good enough for now.
addVarNonVoidCt :: Delta -> Id -> MaybeT DsM Delta
addVarNonVoidCt delta@MkDelta{ delta_tm_st = TmSt env } x = do
vi <- lift $ initLookupVarInfo delta x
vi' <- MaybeT $ ensureInhabited delta vi
-- vi' has probably constructed and then thinned out some PossibleMatches.
-- We want to cache that work
pure delta{ delta_tm_st = TmSt (setEntrySDIE env x vi')}
ensureInhabited :: Delta -> VarInfo -> DsM (Maybe VarInfo)
-- Returns (Just vi) guarantees that at least one member
-- of each ConLike in the COMPLETE set satisfies the oracle
......@@ -917,7 +914,7 @@ ensureInhabited delta vi = fmap (set_cache vi) <$> test (vi_cache vi) -- This wo
case guessConLikeUnivTyArgsFromResTy env (vi_ty vi) con of
Nothing -> pure True -- be conservative about this
Just arg_tys -> do
(_vars, ty_cs, strict_arg_tys, _ex_tyvars) <- mkOneConFull arg_tys con
(_vars, ty_cs, strict_arg_tys) <- mkOneConFull arg_tys con
-- No need to run the term oracle compared to pmIsSatisfiable
fmap isJust <$> runSatisfiabilityCheck delta $ mconcat
-- Important to pass False to tyIsSatisfiable here, so that we won't
......@@ -938,165 +935,6 @@ ensureAllPossibleMatchesInhabited delta@MkDelta{ delta_tm_st = TmSt env }
set_tm_cs_env delta env = delta{ delta_tm_st = TmSt env }
go vi = MaybeT (ensureInhabited delta vi)
-- | @refineToAltCon delta x con arg_tys ex_tyvars@ instantiates @con@ at
-- @arg_tys@ with fresh variables (equating existentials to @ex_tyvars@).
-- It adds a new term equality equating @x@ is to the resulting 'PmAltCon' app
-- and new type equalities arising from GADT matches.
-- If successful, returns the new @delta@ and the fresh term variables, or
-- @Nothing@ otherwise.
refineToAltCon :: Delta -> Id -> PmAltCon -> [Type] -> [TyVar] -> DsM (Maybe (Delta, [Id]))
refineToAltCon delta x l@PmAltLit{} _arg_tys _ex_tvs1 = runMaybeT $ do
delta' <- addVarConCt delta x l []
pure (delta', [])
refineToAltCon delta x alt@(PmAltConLike con) arg_tys ex_tvs1 = do
-- The plan for ConLikes:
-- Suppose K :: forall a b y z. (y,b) -> z -> T a b
-- where the y,z are the existentials
-- @refineToAltCon delta x K [ex1, ex2]@ extends delta with the
-- positive information x :-> K y' z' p q, for some fresh y', z', p, q.
-- This is done by mkOneConFull.
-- We return the fresh [p,q] args, and bind the existentials [y',z'] to
-- [ex1, ex2].
-- Return Nothing if such a match is contradictory with delta.
(arg_vars, theta_ty_cs, strict_arg_tys, ex_tvs2) <- mkOneConFull arg_tys con
-- If we have identical constructors but different existential
-- tyvars, then generate extra equality constraints to ensure the
-- existential tyvars.
-- See Note [Coverage checking and existential tyvars].
let ex_ty_cs = equateTyVars ex_tvs1 ex_tvs2
let new_ty_cs = theta_ty_cs `unionBags` ex_ty_cs
let new_tm_cs = unitBag (TmVarCon x alt arg_vars)
-- Now check satifiability
mb_delta <- pmIsSatisfiable delta new_tm_cs new_ty_cs strict_arg_tys
tracePm "refineToAltCon" (vcat [ ppr x
, ppr new_tm_cs
, ppr new_ty_cs
, ppr strict_arg_tys
, ppr delta
, ppr mb_delta ])
case mb_delta of
Nothing -> pure Nothing
Just delta' -> pure (Just (delta', arg_vars))
{-
Note [Coverage checking and existential tyvars]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
GHC's implementation of the pattern-match coverage algorithm (as described in
the GADTs Meet Their Match paper) must take some care to emit enough type
constraints when handling data constructors with exisentially quantified type
variables. To better explain what the challenge is, consider a constructor K
of the form:
K @e_1 ... @e_m ev_1 ... ev_v ty_1 ... ty_n :: T u_1 ... u_p
Where:
* e_1, ..., e_m are the existentially bound type variables.
* ev_1, ..., ev_v are evidence variables, which may inhabit a dictionary type
(e.g., Eq) or an equality constraint (e.g., e_1 ~ Int).
* ty_1, ..., ty_n are the types of K's fields.
* T u_1 ... u_p is the return type, where T is the data type constructor, and
u_1, ..., u_p are the universally quantified type variables.
In the ConVar case, the coverage algorithm will have in hand the constructor
K as well as a list of type arguments [t_1, ..., t_n] to substitute T's
universally quantified type variables u_1, ..., u_n for. It's crucial to take
these in as arguments, as it is non-trivial to derive them just from the result
type of a pattern synonym and the ambient type of the match (#11336, #17112).
The type checker already did the hard work, so we should just make use of it.
The presence of existentially quantified type variables adds a significant
wrinkle. We always grab e_1, ..., e_m from the definition of K to begin with,
but we don't want them to appear in the final PmCon, because then
calling (mkOneConFull K) for other pattern variables might reuse the same
existential tyvars, which is certainly wrong.
Previously, GHC's solution to this wrinkle was to always create fresh names
for the existential tyvars and put them into the PmCon. This works well for
many cases, but it can break down if you nest GADT pattern matches in just
the right way. For instance, consider the following program:
data App f a where
App :: f a -> App f (Maybe a)
data Ty a where
TBool :: Ty Bool
TInt :: Ty Int
data T f a where
C :: T Ty (Maybe Bool)
foo :: T f a -> App f a -> ()
foo C (App TBool) = ()
foo is a total program, but with the previous approach to handling existential
tyvars, GHC would mark foo's patterns as non-exhaustive.
When foo is desugared to Core, it looks roughly like so:
foo @f @a (C co1 _co2) (App @a1 _co3 (TBool |> co1)) = ()
(Where `a1` is an existential tyvar.)
That, in turn, is processed by the coverage checker to become:
foo @f @a (C co1 _co2) (App @a1 _co3 (pmvar123 :: f a1))
| TBool <- pmvar123 |> co1
= ()
Note that the type of pmvar123 is `f a1`—this will be important later.
Now, we proceed with coverage-checking as usual. When we come to the
ConVar case for App, we create a fresh variable `a2` to represent its
existential tyvar. At this point, we have the equality constraints
`(a ~ Maybe a2, a ~ Maybe Bool, f ~ Ty)` in scope.
However, when we check the guard, it will use the type of pmvar123, which is
`f a1`. Thus, when considering if pmvar123 can match the constructor TInt,
it will generate the constraint `a1 ~ Int`. This means our final set of
equality constraints would be:
f ~ Ty
a ~ Maybe Bool
a ~ Maybe a2
a1 ~ Int
Which is satisfiable! Freshening the existential tyvar `a` to `a2` doomed us,
because GHC is unable to relate `a2` to `a1`, which really should be the same
tyvar.
Luckily, we can avoid this pitfall. Recall that the ConVar case was where we
generated a PmCon with too-fresh existentials. But after ConVar, we have the
ConCon case, which considers whether each constructor of a particular data type
can be matched on in a particular spot.
In the case of App, when we get to the ConCon case, we will compare our
original App PmCon (from the source program) to the App PmCon created from the
ConVar case. In the former PmCon, we have `a1` in hand, which is exactly the
existential tyvar we want! Thus, we can force `a1` to be the same as `a2` here
by emitting an additional `a1 ~ a2` constraint. Now our final set of equality
constraints will be:
f ~ Ty
a ~ Maybe Bool
a ~ Maybe a2
a1 ~ Int
a1 ~ a2
Which is unsatisfiable, as we desired, since we now have that
Int ~ a1 ~ a2 ~ Bool.
In general, App might have more than one constructor, in which case we
couldn't reuse the existential tyvar for App for a different constructor. This
means that we can only use this trick in ConCon when the constructors are the
same. But this is fine, since this is the only scenario where this situation
arises in the first place!
-}
--------------------------------------
-- * Term oracle unification procedure
......@@ -1203,7 +1041,7 @@ mkInhabitationCandidate :: Id -> DataCon -> DsM InhabitationCandidate
mkInhabitationCandidate x dc = do
let cl = RealDataCon dc
let tc_args = tyConAppArgs (idType x)
(arg_vars, ty_cs, strict_arg_tys, _ex_tyvars) <- mkOneConFull tc_args cl
(arg_vars, ty_cs, strict_arg_tys) <- mkOneConFull tc_args cl
pure InhabitationCandidate
{ ic_tm_cs = unitBag (TmVarCon x (PmAltConLike cl) arg_vars)
, ic_ty_cs = ty_cs
......@@ -1600,8 +1438,6 @@ provideEvidenceForEquation = go init_ts
-> DsM [Delta]
split_at_con rec_ts delta n x xs cl = do
-- This will be really similar to the ConVar case
let (_,ex_tvs,_,_,_,_,_) = conLikeFullSig cl
-- we might need to freshen ex_tvs. Not sure
-- We may need to reduce type famlies/synonyms in x's type first
res <- pmTopNormaliseType (delta_ty_st delta) (idType x)
let res_ty = normalisedSourceType res
......@@ -1609,10 +1445,19 @@ provideEvidenceForEquation = go init_ts
case guessConLikeUnivTyArgsFromResTy env res_ty cl of
Nothing -> pure [delta] -- We can't split this one, so assume it's inhabited
Just arg_tys -> do
ev_pos <- refineToAltCon delta x (PmAltConLike cl) arg_tys ex_tvs >>= \case
Nothing -> pure []
Just (delta', arg_vas) ->
go rec_ts (arg_vas ++ xs) n delta'
(arg_vars, new_ty_cs, strict_arg_tys) <- mkOneConFull arg_tys cl
let new_tm_cs = unitBag (TmVarCon x (PmAltConLike cl) arg_vars)
-- Now check satifiability
mb_delta <- pmIsSatisfiable delta new_tm_cs new_ty_cs strict_arg_tys
tracePm "split_at_con" (vcat [ ppr x
, ppr new_tm_cs
, ppr new_ty_cs
, ppr strict_arg_tys
, ppr delta
, ppr mb_delta ])
ev_pos <- case mb_delta of
Nothing -> pure []
Just delta' -> go rec_ts (arg_vars ++ xs) n delta'
-- Only n' more equations to go...
let n' = n - length ev_pos
......
{-# LANGUAGE BangPatterns #-}
module Lib where
import Data.Void
f :: Void -> ()
f !_ = ()
T17234.hs:8:1: warning: [-Woverlapping-patterns (in -Wdefault)]
Pattern match has inaccessible right hand side
In an equation for ‘f’: f !_ = ...
......@@ -82,6 +82,8 @@ test('T17096', collect_compiler_stats('bytes allocated',10), compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M2G -RTS'])
test('T17112', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17234', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
# Other tests
test('pmc001', [], compile,
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment