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

Fix #17112

The `mkOneConFull` function of the pattern match checker used to try to
guess the type arguments of the data type's type constructor by looking
at the ambient type of the match. This doesn't work well for Pattern
Synonyms, where the result type isn't even necessarily a TyCon
application, and it shows in #11336 and #17112.

Also the effort seems futile; why try to try hard when the type checker
has already done the hard lifting? After this patch, we instead supply
the type constructors arguments as an argument to the function and
lean on the type-annotated AST.
parent 1c7ec449
Pipeline #9711 failed with stages
in 333 minutes and 51 seconds
......@@ -56,7 +56,6 @@ import TyCoRep
import Type
import UniqSupply
import DsUtils (isTrueLHsExpr)
import Maybes (expectJust)
import qualified GHC.LanguageExtensions as LangExt
import Data.List (find)
......@@ -853,7 +852,7 @@ inhabitationCandidates ty_cs ty = do
alts_to_check :: Type -> Type -> [DataCon]
-> PmM (Either Type (TyCon, [InhabitationCandidate]))
alts_to_check src_ty core_ty dcs = case splitTyConApp_maybe core_ty of
Just (tc, _)
Just (tc, tc_args)
| tc `elem` trivially_inhabited
-> case dcs of
[] -> return (Left src_ty)
......@@ -869,7 +868,7 @@ inhabitationCandidates ty_cs ty = do
-- them extremely misleading.
-> liftD $ do
var <- mkPmId core_ty -- it would be wrong to unify x
alts <- mapM (mkOneConFull var . RealDataCon) (tyConDataCons tc)
alts <- mapM (mkOneConFull var tc_args . RealDataCon) (tyConDataCons tc)
return $ Right
(tc, [ alt{ic_val_abs = build_tm (ic_val_abs alt) dcs}
| alt <- alts ])
......@@ -1616,37 +1615,31 @@ instance Outputable InhabitationCandidate where
-- | Generate an 'InhabitationCandidate' for a given conlike (generate
-- fresh variables of the appropriate type for arguments)
mkOneConFull :: Id -> ConLike -> DsM InhabitationCandidate
-- * x :: T tys, where T is an algebraic data type
-- NB: in the case of a data family, T is the *representation* TyCon
-- e.g. data instance T (a,b) = T1 a b
-- leads to
-- data TPair a b = T1 a b -- The "representation" type
-- It is TPair, not T, that is given to mkOneConFull
mkOneConFull :: Id -> [Type] -> ConLike -> DsM InhabitationCandidate
-- * 'con' K is a conlike of algebraic data type 'T tys'
-- * 'tc_args' are the type arguments of the 'con's TyCon T
--
-- * 'con' K is a conlike of data type T
-- * 'x' is the variable for which we encode an equality constraint
-- in the term oracle
--
-- After instantiating the universal tyvars of K we get
-- K tys :: forall bs. Q => s1 .. sn -> T tys
-- After instantiating the universal tyvars of K to tc_args we get
-- K @tys :: forall bs. Q => s1 .. sn -> T tys
--
-- Suppose y1 is a strict field. Then we get
-- Results: ic_val_abs: K (y1::s1) .. (yn::sn)
-- ic_tm_ct: x ~ K y1..yn
-- ic_ty_cs: Q
-- ic_strict_arg_tys: [s1]
mkOneConFull x con = do
let res_ty = idType x
(univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , arg_tys, con_res_ty)
mkOneConFull x tc_args con = do
let (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , arg_tys, _con_res_ty)
= conLikeFullSig con
arg_is_banged = map isBanged $ conLikeImplBangs con
tc_args = tyConAppArgs res_ty
subst1 = case con of
RealDataCon {} -> zipTvSubst univ_tvs tc_args
PatSynCon {} -> expectJust "mkOneConFull" (tcMatchTy con_res_ty res_ty)
-- See Note [Pattern synonym result type] in PatSyn
subst1 = zipTvSubst univ_tvs tc_args
(subst, ex_tvs') <- cloneTyVarBndrs subst1 ex_tvs <$> getUniqueSupplyM
-- Field types
let arg_tys' = substTys subst arg_tys
-- Fresh term variables (VAs) as arguments to the constructor
arguments <- mapM mkPmVar arg_tys'
......@@ -2094,7 +2087,7 @@ pmcheckHd (p@(PmCon { pm_con_con = con, pm_con_arg_tys = tys }))
(PmVar x) (ValVec vva delta) = do
(prov, complete_match) <- select =<< liftD (allCompleteMatches con tys)
cons_cs <- mapM (liftD . mkOneConFull x) complete_match
cons_cs <- mapM (liftD . mkOneConFull x tys) complete_match
inst_vsa <- flip mapMaybeM cons_cs $
\InhabitationCandidate{ ic_val_abs = va, ic_tm_ct = tm_ct
......@@ -2201,11 +2194,11 @@ Where:
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 pattern variable (pv :: T PV_1 ... PV_p), where PV_1, ..., PV_p
are some types that instantiate u_1, ... u_p. The idea is that we should
substitute PV_1 for u_1, ..., and PV_p for u_p when forming a PmCon (the
mkOneConFull function accomplishes this) and then hand this PmCon off to the
ConCon case.
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,
......
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
import Data.Functor.Identity
data HideArg f where
HideArg :: f a -> HideArg f
data family App :: tF -> tF
data instance App f x = App1 (f x)
class WrappedIn s a | s -> a where
unwrap :: s -> a
instance WrappedIn (App f a) (f a) where
unwrap (App1 fa) = fa
pattern Unwrapped :: WrappedIn s a => a -> s
pattern Unwrapped x <- (unwrap -> x)
{-# COMPLETE Unwrapped :: App #-}
boom :: HideArg (App Identity) -> Bool
boom (HideArg (Unwrapped (Identity _))) = True
main :: IO ()
main = print ":("
......@@ -76,6 +76,8 @@ test('T15884', expect_broken(15884), compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T16289', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T17112', 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