summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSebastian Graf <sebastian.graf@kit.edu>2020-01-15 17:15:58 +0100
committerMarge Bot <ben+marge-bot@smart-cactus.org>2020-01-25 05:21:05 -0500
commit86966d48954db4a8bd40046af259ed60aed535eb (patch)
treed003bee5b0d31af6c867d5ce6a6c8ce0527124d6
parent8038cbd96f444fdba18e8c9fb292c565738b774d (diff)
downloadhaskell-86966d48954db4a8bd40046af259ed60aed535eb.tar.gz
PmCheck: Properly handle constructor-bound type variables
In https://gitlab.haskell.org/ghc/ghc/merge_requests/2192#note_246551 Simon convinced me that ignoring type variables existentially bound by data constructors have to be the same way as value binders. Sadly I couldn't think of a regression test, but I'm confident that this change strictly improves on the status quo.
-rw-r--r--compiler/GHC/HsToCore/PmCheck.hs22
-rw-r--r--compiler/GHC/HsToCore/PmCheck/Oracle.hs185
-rw-r--r--compiler/GHC/HsToCore/PmCheck/Ppr.hs4
-rw-r--r--compiler/GHC/HsToCore/PmCheck/Types.hs2
-rw-r--r--compiler/utils/Util.hs8
5 files changed, 133 insertions, 88 deletions
diff --git a/compiler/GHC/HsToCore/PmCheck.hs b/compiler/GHC/HsToCore/PmCheck.hs
index 99a1236d70..1b98f1afbb 100644
--- a/compiler/GHC/HsToCore/PmCheck.hs
+++ b/compiler/GHC/HsToCore/PmCheck.hs
@@ -95,6 +95,7 @@ data PmGrd
PmCon {
pm_id :: !Id,
pm_con_con :: !PmAltCon,
+ pm_con_tvs :: ![TyVar],
pm_con_dicts :: ![EvVar],
pm_con_args :: ![Id]
}
@@ -113,7 +114,7 @@ data PmGrd
-- | Should not be user-facing.
instance Outputable PmGrd where
- ppr (PmCon x alt _con_dicts con_args)
+ ppr (PmCon x alt _tvs _con_dicts con_args)
= hsep [ppr alt, hsep (map ppr con_args), text "<-", ppr x]
ppr (PmBang x) = char '!' <> ppr x
ppr (PmLet x expr) = hsep [text "let", ppr x, text "=", ppr expr]
@@ -354,7 +355,7 @@ mkPmLetVar x y = [PmLet x (Var y)]
vanillaConGrd :: Id -> DataCon -> [Id] -> PmGrd
vanillaConGrd scrut con arg_ids =
PmCon { pm_id = scrut, pm_con_con = PmAltConLike (RealDataCon con)
- , pm_con_dicts = [], pm_con_args = arg_ids }
+ , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = arg_ids }
-- | Creates a 'GrdVec' refining a match var of list type to a list,
-- where list fields are matched against the incoming tagged 'GrdVec's.
@@ -389,6 +390,7 @@ mkPmLitGrds x (PmLit _ (PmLitString s)) = do
mkPmLitGrds x lit = do
let grd = PmCon { pm_id = x
, pm_con_con = PmAltLit lit
+ , pm_con_tvs = []
, pm_con_dicts = []
, pm_con_args = [] }
pure [grd]
@@ -585,7 +587,7 @@ translateConPatOut fam_insts x con univ_tys ex_tvs dicts = \case
-- 1. the constructor pattern match itself
arg_ids <- zipWithM get_pat_id [0..] arg_tys
- let con_grd = PmCon x (PmAltConLike con) dicts arg_ids
+ let con_grd = PmCon x (PmAltConLike con) ex_tvs dicts arg_ids
-- 2. bang strict fields
let arg_is_banged = map isBanged $ conLikeImplBangs con
@@ -935,14 +937,14 @@ checkGrdTree' (Guard (PmBang x) tree) deltas = do
pure res{ cr_clauses = applyWhen has_diverged mayDiverge (cr_clauses res) }
-- Con: Diverge on x ~ ⊥, fall through on x /~ K and refine with x ~ K ys
-- and type info
-checkGrdTree' (Guard (PmCon x con dicts args) tree) deltas = do
+checkGrdTree' (Guard (PmCon x con tvs dicts args) tree) deltas = do
has_diverged <-
if conMatchForces con
then addPmCtDeltas deltas (PmBotCt x) >>= isInhabited
else pure False
unc_this <- addPmCtDeltas deltas (PmNotConCt x con)
deltas' <- addPmCtsDeltas deltas $
- listToBag (PmTyCt . evVarPred <$> dicts) `snocBag` PmConCt x con args
+ listToBag (PmTyCt . evVarPred <$> dicts) `snocBag` PmConCt x con tvs args
CheckResult tree' unc_inner prec <- checkGrdTree' tree deltas'
limit <- maxPmCheckModels <$> getDynFlags
let (prec', unc') = throttle limit deltas (unc_this Semi.<> unc_inner)
@@ -1032,10 +1034,10 @@ addScrutTmCs (Just scr) [x] k = do
locallyExtendPmDelta (\delta -> addPmCts delta (unitBag (PmCoreCt x scr_e))) k
addScrutTmCs _ _ _ = panic "addScrutTmCs: HsCase with more than one case binder"
-addPmConCts :: Delta -> Id -> PmAltCon -> [EvVar] -> [Id] -> DsM (Maybe Delta)
-addPmConCts delta x con dicts fields = runMaybeT $ do
+addPmConCts :: Delta -> Id -> PmAltCon -> [TyVar] -> [EvVar] -> [Id] -> DsM (Maybe Delta)
+addPmConCts delta x con tvs dicts fields = runMaybeT $ do
delta_ty <- MaybeT $ addPmCts delta (listToBag (PmTyCt . evVarPred <$> dicts))
- delta_tm_ty <- MaybeT $ addPmCts delta_ty (unitBag (PmConCt x con fields))
+ delta_tm_ty <- MaybeT $ addPmCts delta_ty (unitBag (PmConCt x con tvs fields))
pure delta_tm_ty
-- | Add equalities to the local 'DsM' environment when checking the RHS of a
@@ -1068,9 +1070,9 @@ computeCovered (PmLet { pm_id = x, pm_let_expr = e } : ps) delta = do
computeCovered (PmBang{} : ps) delta = do
computeCovered ps delta
computeCovered (p : ps) delta
- | PmCon{ pm_id = x, pm_con_con = con, pm_con_args = args
+ | PmCon{ pm_id = x, pm_con_con = con, pm_con_tvs = tvs, pm_con_args = args
, pm_con_dicts = dicts } <- p
- = addPmConCts delta x con dicts args >>= \case
+ = addPmConCts delta x con tvs dicts args >>= \case
Nothing -> pure Nothing
Just delta' -> computeCovered ps delta'
diff --git a/compiler/GHC/HsToCore/PmCheck/Oracle.hs b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
index 3f135b6664..9843de18b0 100644
--- a/compiler/GHC/HsToCore/PmCheck/Oracle.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
@@ -70,7 +70,7 @@ import DsMonad hiding (foldlM)
import FamInst
import FamInstEnv
-import Control.Monad (guard, mzero)
+import Control.Monad (guard, mzero, when)
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.State.Strict
import Data.Bifunctor (second)
@@ -112,9 +112,9 @@ markMatched con (PM ms) = PM (del_one_con con <$> ms)
-- | Instantiate a 'ConLike' given its universal type arguments. Instantiates
-- existential and term binders with fresh variables of appropriate type.
--- Returns instantiated term variables from the match, type evidence and the
--- types of strict constructor fields.
-mkOneConFull :: [Type] -> ConLike -> DsM ([Id], Bag TyCt, [Type])
+-- Returns instantiated type and term variables from the match, type evidence
+-- and the types of strict constructor fields.
+mkOneConFull :: [Type] -> ConLike -> DsM ([TyVar], [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
@@ -132,11 +132,12 @@ mkOneConFull :: [Type] -> ConLike -> DsM ([Id], Bag TyCt, [Type])
-- be a concrete TyCon.
--
-- Suppose y1 is a strict field. Then we get
--- Results: [y1,..,yn]
+-- Results: bs
+-- [y1,..,yn]
-- Q
-- [s1]
mkOneConFull arg_tys con = do
- let (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , field_tys, _con_res_ty)
+ 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
@@ -158,7 +159,7 @@ mkOneConFull arg_tys con = do
| otherwise
= map isBanged $ conLikeImplBangs con
strict_arg_tys = filterByList arg_is_strict field_tys'
- return (vars, listToBag ty_cs, strict_arg_tys)
+ return (ex_tvs, vars, listToBag ty_cs, strict_arg_tys)
-------------------------
-- * Pattern match oracle
@@ -755,7 +756,7 @@ canDiverge delta@MkDelta{ delta_tm_st = ts } x
| VI _ pos neg _ <- lookupVarInfo ts x
= null neg && all pos_can_diverge pos
where
- pos_can_diverge (PmAltConLike (RealDataCon dc), [y])
+ pos_can_diverge (PmAltConLike (RealDataCon dc), _, [y])
-- See Note [Divergence of Newtype matches]
| isNewTyCon (dataConTyCon dc) = canDiverge delta y
pos_can_diverge _ = False
@@ -795,13 +796,13 @@ lookupRefuts MkDelta{ delta_tm_st = ts@(TmSt (SDIE env) _) } k =
Just (Indirect y) -> vi_neg (lookupVarInfo ts y)
Just (Entry vi) -> vi_neg vi
-isDataConSolution :: (PmAltCon, [Id]) -> Bool
-isDataConSolution (PmAltConLike (RealDataCon _), _) = True
-isDataConSolution _ = False
+isDataConSolution :: (PmAltCon, [TyVar], [Id]) -> Bool
+isDataConSolution (PmAltConLike (RealDataCon _), _, _) = True
+isDataConSolution _ = False
-- @lookupSolution delta x@ picks a single solution ('vi_pos') of @x@ from
-- possibly many, preferring 'RealDataCon' solutions whenever possible.
-lookupSolution :: Delta -> Id -> Maybe (PmAltCon, [Id])
+lookupSolution :: Delta -> Id -> Maybe (PmAltCon, [TyVar], [Id])
lookupSolution delta x = case vi_pos (lookupVarInfo (delta_tm_st delta) x) of
[] -> Nothing
pos
@@ -817,9 +818,9 @@ data TmCt
-- ^ @TmVarCt x y@ encodes "x ~ y", equating @x@ and @y@.
| TmCoreCt !Id !CoreExpr
-- ^ @TmCoreCt x e@ encodes "x ~ e", equating @x@ with the 'CoreExpr' @e@.
- | TmConCt !Id !PmAltCon ![Id]
- -- ^ @TmConCt x K ys@ encodes "x ~ K ys", equating @x@ with the 'PmAltCon'
- -- application @K ys@.
+ | TmConCt !Id !PmAltCon ![TyVar] ![Id]
+ -- ^ @TmConCt x K tvs ys@ encodes "x ~ K @tvs ys", equating @x@ with the 'PmAltCon'
+ -- application @K @tvs ys@.
| TmNotConCt !Id !PmAltCon
-- ^ @TmNotConCt x K@ encodes "x /~ K", asserting that @x@ can't be headed
-- by @K@.
@@ -830,12 +831,15 @@ data TmCt
-- ^ @TmNotBotCt x y@ encodes "x /~ ⊥", asserting that @x@ can't be ⊥.
instance Outputable TmCt where
- ppr (TmVarCt x y) = ppr x <+> char '~' <+> ppr y
- ppr (TmCoreCt x e) = ppr x <+> char '~' <+> ppr e
- ppr (TmConCt x con args) = ppr x <+> char '~' <+> hsep (ppr con : map ppr args)
- ppr (TmNotConCt x con) = ppr x <+> text "/~" <+> ppr con
- ppr (TmBotCt x) = ppr x <+> text "~ ⊥"
- ppr (TmNotBotCt x) = ppr x <+> text "/~ ⊥"
+ ppr (TmVarCt x y) = ppr x <+> char '~' <+> ppr y
+ ppr (TmCoreCt x e) = ppr x <+> char '~' <+> ppr e
+ ppr (TmConCt x con tvs args) = ppr x <+> char '~' <+> hsep (ppr con : pp_tvs ++ pp_args)
+ where
+ pp_tvs = map ((<> char '@') . ppr) tvs
+ pp_args = map ppr args
+ ppr (TmNotConCt x con) = ppr x <+> text "/~" <+> ppr con
+ ppr (TmBotCt x) = ppr x <+> text "~ ⊥"
+ ppr (TmNotBotCt x) = ppr x <+> text "/~ ⊥"
type TyCt = PredType
@@ -849,17 +853,17 @@ data PmCt
type PmCts = Bag PmCt
pattern PmVarCt :: Id -> Id -> PmCt
-pattern PmVarCt x y = PmTmCt (TmVarCt x y)
+pattern PmVarCt x y = PmTmCt (TmVarCt x y)
pattern PmCoreCt :: Id -> CoreExpr -> PmCt
-pattern PmCoreCt x e = PmTmCt (TmCoreCt x e)
-pattern PmConCt :: Id -> PmAltCon -> [Id] -> PmCt
-pattern PmConCt x con args = PmTmCt (TmConCt x con args)
+pattern PmCoreCt x e = PmTmCt (TmCoreCt x e)
+pattern PmConCt :: Id -> PmAltCon -> [TyVar] -> [Id] -> PmCt
+pattern PmConCt x con tvs args = PmTmCt (TmConCt x con tvs args)
pattern PmNotConCt :: Id -> PmAltCon -> PmCt
-pattern PmNotConCt x con = PmTmCt (TmNotConCt x con)
+pattern PmNotConCt x con = PmTmCt (TmNotConCt x con)
pattern PmBotCt :: Id -> PmCt
-pattern PmBotCt x = PmTmCt (TmBotCt x)
+pattern PmBotCt x = PmTmCt (TmBotCt x)
pattern PmNotBotCt :: Id -> PmCt
-pattern PmNotBotCt x = PmTmCt (TmNotBotCt x)
+pattern PmNotBotCt x = PmTmCt (TmNotBotCt x)
{-# COMPLETE PmTyCt, PmVarCt, PmCoreCt, PmConCt, PmNotConCt, PmBotCt, PmNotBotCt #-}
instance Outputable PmCt where
@@ -886,12 +890,12 @@ partitionTyTmCts = partitionEithers . map to_either . toList
-- | Adds a single term constraint by dispatching to the various term oracle
-- functions.
addTmCt :: Delta -> TmCt -> MaybeT DsM Delta
-addTmCt delta (TmVarCt x y) = addVarVarCt delta (x, y)
-addTmCt delta (TmCoreCt x e) = addVarCoreCt delta x e
-addTmCt delta (TmConCt x con args) = addVarConCt delta x con args
-addTmCt delta (TmNotConCt x con) = addRefutableAltCon delta x con
-addTmCt delta (TmBotCt x) = addVarBotCt delta x
-addTmCt delta (TmNotBotCt x) = addVarNonVoidCt delta x
+addTmCt delta (TmVarCt x y) = addVarVarCt delta (x, y)
+addTmCt delta (TmCoreCt x e) = addVarCoreCt delta x e
+addTmCt delta (TmConCt x con tvs args) = addVarConCt delta x con tvs args
+addTmCt delta (TmNotConCt x con) = addRefutableAltCon delta x con
+addTmCt delta (TmBotCt x) = addVarBotCt delta x
+addTmCt delta (TmNotBotCt x) = addVarNonVoidCt delta x
-- | In some future this will actually add a constraint to 'Delta' that we plan
-- to preserve. But for now, we just check if we can add the constraint to the
@@ -908,11 +912,11 @@ addRefutableAltCon :: Delta -> Id -> PmAltCon -> MaybeT DsM Delta
addRefutableAltCon delta@MkDelta{ delta_tm_st = TmSt env reps } x nalt = do
vi@(VI _ pos neg pm) <- lift (initLookupVarInfo delta x)
-- 1. Bail out quickly when nalt contradicts a solution
- let contradicts nalt (cl, _args) = eqPmAltCon cl nalt == Equal
+ let contradicts nalt (cl, _tvs, _args) = eqPmAltCon cl nalt == Equal
guard (not (any (contradicts nalt) pos))
-- 2. Only record the new fact when it's not already implied by one of the
-- solutions
- let implies nalt (cl, _args) = eqPmAltCon cl nalt == Disjoint
+ let implies nalt (cl, _tvs, _args) = eqPmAltCon cl nalt == Disjoint
let neg'
| any (implies nalt) pos = neg
-- See Note [Completeness checking with required Thetas]
@@ -1037,7 +1041,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) <- mkOneConFull arg_tys con
+ (_tvs, _vars, ty_cs, strict_arg_tys) <- mkOneConFull arg_tys con
tracePm "inh_test" (ppr con $$ ppr ty_cs)
-- No need to run the term oracle compared to pmIsSatisfiable
fmap isJust <$> runSatisfiabilityCheck delta $ mconcat
@@ -1102,7 +1106,7 @@ equate delta@MkDelta{ delta_tm_st = TmSt env reps } x y
let env_refs = setEntrySDIE env_ind y vi_y
let delta_refs = delta{ delta_tm_st = TmSt env_refs reps }
-- and then gradually merge every positive fact we have on x into y
- let add_fact delta (cl, args) = addVarConCt delta y cl args
+ let add_fact delta (cl, tvs, args) = addVarConCt delta y cl tvs args
delta_pos <- foldlM add_fact delta_refs (vi_pos vi_x)
-- Do the same for negative info
let add_refut delta nalt = addRefutableAltCon delta y nalt
@@ -1116,27 +1120,40 @@ equate delta@MkDelta{ delta_tm_st = TmSt env reps } x y
-- other solutions, reject (@Nothing@) otherwise.
--
-- See Note [TmState invariants].
-addVarConCt :: Delta -> Id -> PmAltCon -> [Id] -> MaybeT DsM Delta
-addVarConCt delta@MkDelta{ delta_tm_st = TmSt env reps } x alt args = do
+addVarConCt :: Delta -> Id -> PmAltCon -> [TyVar] -> [Id] -> MaybeT DsM Delta
+addVarConCt delta@MkDelta{ delta_tm_st = TmSt env reps } x alt tvs args = do
VI ty pos neg cache <- lift (initLookupVarInfo delta x)
-- First try to refute with a negative fact
guard (all ((/= Equal) . eqPmAltCon alt) neg)
-- Then see if any of the other solutions (remember: each of them is an
-- additional refinement of the possible values x could take) indicate a
-- contradiction
- guard (all ((/= Disjoint) . eqPmAltCon alt . fst) pos)
- -- Now we should be good! Add (alt, args) as a possible solution, or refine an
- -- existing one
- case find ((== Equal) . eqPmAltCon alt . fst) pos of
- Just (_, other_args) -> do
- foldlM addVarVarCt delta (zip args other_args)
+ guard (all ((/= Disjoint) . eqPmAltCon alt . fstOf3) pos)
+ -- Now we should be good! Add (alt, tvs, args) as a possible solution, or
+ -- refine an existing one
+ case find ((== Equal) . eqPmAltCon alt . fstOf3) pos of
+ Just (_con, other_tvs, other_args) -> do
+ -- We must unify existentially bound ty vars and arguments!
+ let ty_cts = equateTyVarsCts tvs other_tvs
+ when (length args /= length other_args) $
+ lift $ tracePm "error" (ppr x <+> ppr alt <+> ppr args <+> ppr other_args)
+ let tm_cts = zipWithEqual "addVarConCt" PmVarCt args other_args
+ MaybeT $ addPmCts delta (listToBag ty_cts `unionBags` listToBag tm_cts)
Nothing -> do
-- Filter out redundant negative facts (those that compare Just False to
-- the new solution)
let neg' = filter ((== PossiblyOverlap) . eqPmAltCon alt) neg
- let pos' = (alt,args):pos
+ let pos' = (alt, tvs, args):pos
pure delta{ delta_tm_st = TmSt (setEntrySDIE env x (VI ty pos' neg' cache)) reps}
+equateTyVarsCts :: [TyVar] -> [TyVar] -> [PmCt]
+equateTyVarsCts as bs
+ = map (\(a, b) -> PmTyCt $ mkPrimEqPred (mkTyVarTy a) (mkTyVarTy b))
+ -- The following line filters out trivial Refl constraints, so that we don't
+ -- need to initialise the type oracle that often
+ $ filter (uncurry (/=))
+ $ zipEqual "equateTyVarsCts" as bs
+
----------------------------------------
-- * Enumerating inhabitation candidates
@@ -1163,9 +1180,9 @@ 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) <- mkOneConFull tc_args cl
+ (ty_vars, arg_vars, ty_cs, strict_arg_tys) <- mkOneConFull tc_args cl
pure InhabitationCandidate
- { ic_cs = PmTyCt <$> ty_cs `snocBag` PmConCt x (PmAltConLike cl) arg_vars
+ { ic_cs = PmTyCt <$> ty_cs `snocBag` PmConCt x (PmAltConLike cl) ty_vars arg_vars
, ic_strict_arg_tys = strict_arg_tys
}
@@ -1187,7 +1204,9 @@ inhabitationCandidates MkDelta{ delta_ty_st = ty_st } ty = do
build_newtype (ty, dc, _arg_ty) x = do
-- ty is the type of @dc x@. It's a @dataConTyCon dc@ application.
y <- mkPmId ty
- pure (y, PmConCt y (PmAltConLike (RealDataCon dc)) [x])
+ -- Newtypes don't have existentials (yet?!), so passing an empty list as
+ -- ex_tvs.
+ pure (y, PmConCt y (PmAltConLike (RealDataCon dc)) [] [x])
build_newtypes :: Id -> [(Type, DataCon, Type)] -> DsM (Id, [PmCt])
build_newtypes x = foldrM (\dc (x, cts) -> go dc x cts) (x, [])
@@ -1508,7 +1527,7 @@ provideEvidence = go
-- where @x@ will have two possibly compatible solutions, @Just y@ for
-- some @y@ and @SomePatSyn z@ for some @z@. We must find evidence for @y@
-- and @z@ that is valid at the same time. These constitute arg_vas below.
- let arg_vas = concatMap (\(_cl, args) -> args) pos
+ let arg_vas = concatMap (\(_cl, _tvs, args) -> args) pos
go (arg_vas ++ xs) n delta
[]
-- When there are literals involved, just print negative info
@@ -1526,7 +1545,9 @@ provideEvidence = go
(_src_ty, dcs, core_ty) <- tntrGuts <$> pmTopNormaliseType (delta_ty_st delta) (idType x)
let build_newtype (x, delta) (_ty, dc, arg_ty) = do
y <- lift $ mkPmId arg_ty
- delta' <- addVarConCt delta x (PmAltConLike (RealDataCon dc)) [y]
+ -- Newtypes don't have existentials (yet?!), so passing an empty
+ -- list as ex_tvs.
+ delta' <- addVarConCt delta x (PmAltConLike (RealDataCon dc)) [] [y]
pure (y, delta')
runMaybeT (foldlM build_newtype (x, delta) dcs) >>= \case
Nothing -> pure []
@@ -1553,8 +1574,8 @@ provideEvidence = go
case guessConLikeUnivTyArgsFromResTy env ty cl of
Nothing -> pure [delta] -- No idea idea how to refine this one, so just finish off with a wildcard
Just arg_tys -> do
- (arg_vars, new_ty_cs, strict_arg_tys) <- mkOneConFull arg_tys cl
- let new_tm_cs = unitBag (TmConCt x (PmAltConLike cl) arg_vars)
+ (tvs, arg_vars, new_ty_cs, strict_arg_tys) <- mkOneConFull arg_tys cl
+ let new_tm_cs = unitBag (TmConCt x (PmAltConLike cl) tvs arg_vars)
-- Now check satifiability
mb_delta <- pmIsSatisfiable delta new_ty_cs new_tm_cs strict_arg_tys
tracePm "instantiate_cons" (vcat [ ppr x
@@ -1625,14 +1646,21 @@ addVarCoreCt delta x e = do
= case unpackFS s of
-- We need this special case to break a loop with coreExprAsPmLit
-- Otherwise we alternate endlessly between [] and ""
- [] -> data_con_app x nilDataCon []
+ [] -> data_con_app x nilDataCon [] []
s' -> core_expr x (mkListExpr charTy (map mkCharExpr s'))
| Just lit <- coreExprAsPmLit e
= pm_lit x lit
- | Just (_in_scope, _empty_floats@[], dc, _arg_tys, args)
+ | Just (in_scope, _empty_floats@[], dc, _arg_tys, args)
<- exprIsConApp_maybe in_scope_env e
- = do { arg_ids <- traverse bind_expr args
- ; data_con_app x dc arg_ids }
+ = do { let dc_ex_tvs = dataConExTyCoVars dc
+ arty = dataConSourceArity dc
+ (_ex_ty_args, val_args) = splitAtList dc_ex_tvs args
+ vis_args = reverse $ take arty $ reverse val_args
+ ; uniq_supply <- lift $ lift $ getUniqueSupplyM
+ ; let (_, ex_tvs) = cloneTyVarBndrs (mkEmptyTCvSubst in_scope) dc_ex_tvs uniq_supply
+ -- See Note [Why we don't record existential type constraints]
+ ; arg_ids <- traverse bind_expr vis_args
+ ; data_con_app x dc ex_tvs arg_ids }
-- See Note [Detecting pattern synonym applications in expressions]
| Var y <- e, Nothing <- isDataConId_maybe x
-- We don't consider DataCons flexible variables
@@ -1663,22 +1691,38 @@ addVarCoreCt delta x e = do
represent_expr e = StateT $ \delta ->
swap <$> lift (representCoreExpr delta e)
- data_con_app :: Id -> DataCon -> [Id] -> StateT Delta (MaybeT DsM) ()
- data_con_app x dc args = pm_alt_con_app x (PmAltConLike (RealDataCon dc)) args
+ data_con_app :: Id -> DataCon -> [TyVar] -> [Id] -> StateT Delta (MaybeT DsM) ()
+ data_con_app x dc tvs args = pm_alt_con_app x (PmAltConLike (RealDataCon dc)) tvs args
pm_lit :: Id -> PmLit -> StateT Delta (MaybeT DsM) ()
- pm_lit x lit = pm_alt_con_app x (PmAltLit lit) []
+ pm_lit x lit = pm_alt_con_app x (PmAltLit lit) [] []
-- | Adds the given constructor application as a solution for @x@.
- pm_alt_con_app :: Id -> PmAltCon -> [Id] -> StateT Delta (MaybeT DsM) ()
- pm_alt_con_app x con args = modifyT $ \delta -> addVarConCt delta x con args
+ pm_alt_con_app :: Id -> PmAltCon -> [TyVar] -> [Id] -> StateT Delta (MaybeT DsM) ()
+ pm_alt_con_app x con tvs args = modifyT $ \delta -> addVarConCt delta 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
-{- Note [Detecting pattern synonym applications in expressions]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Why we don't record existential type constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we have
+
+ data Ex where Ex :: a -> Ex
+ f _ | let x = Ex @Int 15 = case x of Ex -> ...
+
+we see that `Ex`'s existential in the `Ex` application in the RHS of `x` is
+bound to `Int`. Eventually this application will run by `addVarCoreCt`,
+which freshens `a` to `a'` and adds the constraint `x ~ Ex @a' 15`.
+
+Now, we *could* add the constraint @a' ~ Int@, but that is never useful, because
+types are irrelevant. And in fact, if the programmer assumed that @a' ~ Int@
+in the case alt, it would be rejected as a type error. So we simply don't
+include the constraint.
+
+Note [Detecting pattern synonym applications in expressions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
At the moment we fail to detect pattern synonyms in scrutinees and RHS of
guards. This could be alleviated with considerable effort and complexity, but
the returns are meager. Consider:
@@ -1690,12 +1734,11 @@ the returns are meager. Consider:
P 15 ->
Compared to the situation where P and Q are DataCons, the lack of generativity
-means we could never flag Q as redundant.
-(also see Note [Undecidable Equality for PmAltCons] in PmTypes.)
-On the other hand, if we fail to recognise the pattern synonym, we flag the
-pattern match as inexhaustive. That wouldn't happen if we had knowledge about
-the scrutinee, in which case the oracle basically knows "If it's a P, then its
-field is 15".
+means we could never flag Q as redundant. (also see Note [Undecidable Equality
+for PmAltCons] in PmTypes.) On the other hand, if we fail to recognise the
+pattern synonym, we flag the pattern match as inexhaustive. That wouldn't happen
+if we had knowledge about the scrutinee, in which case the oracle basically
+knows "If it's a P, then its field is 15".
This is a pretty narrow use case and I don't think we should to try to fix it
until a user complains energetically.
diff --git a/compiler/GHC/HsToCore/PmCheck/Ppr.hs b/compiler/GHC/HsToCore/PmCheck/Ppr.hs
index 6426251d20..81c7bd74bd 100644
--- a/compiler/GHC/HsToCore/PmCheck/Ppr.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Ppr.hs
@@ -143,7 +143,7 @@ pprPmVar :: PprPrec -> Id -> PmPprM SDoc
pprPmVar prec x = do
delta <- ask
case lookupSolution delta x of
- Just (alt, args) -> pprPmAltCon prec alt args
+ Just (alt, _tvs, args) -> pprPmAltCon prec alt args
Nothing -> fromMaybe typed_wildcard <$> checkRefuts x
where
-- if we have no info about the parameter and would just print a
@@ -203,7 +203,7 @@ pmExprAsList :: Delta -> PmAltCon -> [Id] -> Maybe PmExprList
pmExprAsList delta = go_con []
where
go_var rev_pref x
- | Just (alt, args) <- lookupSolution delta x
+ | Just (alt, _tvs, args) <- lookupSolution delta x
= go_con rev_pref alt args
go_var rev_pref x
| Just pref <- nonEmpty (reverse rev_pref)
diff --git a/compiler/GHC/HsToCore/PmCheck/Types.hs b/compiler/GHC/HsToCore/PmCheck/Types.hs
index e5b9bcf0ef..26e6ffc67e 100644
--- a/compiler/GHC/HsToCore/PmCheck/Types.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Types.hs
@@ -465,7 +465,7 @@ data VarInfo
-- ^ The type of the variable. Important for rejecting possible GADT
-- constructors or incompatible pattern synonyms (@Just42 :: Maybe Int@).
- , vi_pos :: ![(PmAltCon, [Id])]
+ , vi_pos :: ![(PmAltCon, [TyVar], [Id])]
-- ^ Positive info: 'PmAltCon' apps it is (i.e. @x ~ [Just y, PatSyn z]@), all
-- at the same time (i.e. conjunctive). We need a list because of nested
-- pattern matches involving pattern synonym
diff --git a/compiler/utils/Util.hs b/compiler/utils/Util.hs
index 615e869cc4..1837b13e97 100644
--- a/compiler/utils/Util.hs
+++ b/compiler/utils/Util.hs
@@ -323,21 +323,21 @@ zipWith4Equal _ = zipWith4
#else
zipEqual _ [] [] = []
zipEqual msg (a:as) (b:bs) = (a,b) : zipEqual msg as bs
-zipEqual msg _ _ = panic ("zipEqual: unequal lists:"++msg)
+zipEqual msg _ _ = panic ("zipEqual: unequal lists: "++msg)
zipWithEqual msg z (a:as) (b:bs)= z a b : zipWithEqual msg z as bs
zipWithEqual _ _ [] [] = []
-zipWithEqual msg _ _ _ = panic ("zipWithEqual: unequal lists:"++msg)
+zipWithEqual msg _ _ _ = panic ("zipWithEqual: unequal lists: "++msg)
zipWith3Equal msg z (a:as) (b:bs) (c:cs)
= z a b c : zipWith3Equal msg z as bs cs
zipWith3Equal _ _ [] [] [] = []
-zipWith3Equal msg _ _ _ _ = panic ("zipWith3Equal: unequal lists:"++msg)
+zipWith3Equal msg _ _ _ _ = panic ("zipWith3Equal: unequal lists: "++msg)
zipWith4Equal msg z (a:as) (b:bs) (c:cs) (d:ds)
= z a b c d : zipWith4Equal msg z as bs cs ds
zipWith4Equal _ _ [] [] [] [] = []
-zipWith4Equal msg _ _ _ _ _ = panic ("zipWith4Equal: unequal lists:"++msg)
+zipWith4Equal msg _ _ _ _ _ = panic ("zipWith4Equal: unequal lists: "++msg)
#endif
-- | 'zipLazy' is a kind of 'zip' that is lazy in the second list (observe the ~)