diff options
| -rw-r--r-- | compiler/deSugar/Check.hs | 47 | ||||
| -rw-r--r-- | testsuite/tests/pmcheck/should_compile/T17112.hs | 32 | ||||
| -rw-r--r-- | testsuite/tests/pmcheck/should_compile/all.T | 2 |
3 files changed, 54 insertions, 27 deletions
diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs index 4a5d978..602c125 100644 --- a/compiler/deSugar/Check.hs +++ b/compiler/deSugar/Check.hs @@ -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, diff --git a/testsuite/tests/pmcheck/should_compile/T17112.hs b/testsuite/tests/pmcheck/should_compile/T17112.hs new file mode 100644 index 0000000..a6755f7 --- /dev/null +++ b/testsuite/tests/pmcheck/should_compile/T17112.hs @@ -0,0 +1,32 @@ +{-# 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 ":(" diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T index 5fe7d9e..87874f8 100644 --- a/testsuite/tests/pmcheck/should_compile/all.T +++ b/testsuite/tests/pmcheck/should_compile/all.T @@ -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, |