diff options
| -rw-r--r-- | compiler/basicTypes/PatSyn.hs | 54 | ||||
| -rw-r--r-- | compiler/deSugar/Check.hs | 17 | ||||
| -rw-r--r-- | testsuite/tests/patsyn/should_compile/T13768.hs | 33 | ||||
| -rw-r--r-- | testsuite/tests/patsyn/should_compile/all.T | 1 |
4 files changed, 89 insertions, 16 deletions
diff --git a/compiler/basicTypes/PatSyn.hs b/compiler/basicTypes/PatSyn.hs index 0e218a39c1..176bb9f590 100644 --- a/compiler/basicTypes/PatSyn.hs +++ b/compiler/basicTypes/PatSyn.hs @@ -63,7 +63,7 @@ data PatSyn -- record pat syn or same length as -- psArgs - -- Universially-quantified type variables + -- Universally-quantified type variables psUnivTyVars :: [TyVarBinder], -- Required dictionaries (may mention psUnivTyVars) @@ -76,7 +76,8 @@ data PatSyn psProvTheta :: ThetaType, -- Result type - psOrigResTy :: Type, -- Mentions only psUnivTyVars + psResultTy :: Type, -- Mentions only psUnivTyVars + -- See Note [Pattern synonym result type] -- See Note [Matchers and builders for pattern synonyms] psMatcher :: (Id, Bool), @@ -145,6 +146,43 @@ Example 3: You can see it's existential because it doesn't appear in the result type (T3 b). +Note [Pattern synonym result type] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + data T a b = MkT b a + + pattern P :: a -> T [a] Bool + pattern P x = MkT True [x] + +P's psResultTy is (T a Bool), and it really only matches values of +type (T [a] Bool). For example, this is ill-typed + + f :: T p q -> String + f (P x) = "urk" + +This is differnet to the situation with GADTs: + + data S a where + MkS :: Int -> S Bool + +Now MkS (and pattern synonyms coming from MkS) can match a +value of type (S a), not just (S Bool); we get type refinement. + +That in turn means that if you have a pattern + + P x :: T [ty] Bool + +it's not entirely straightforward to work out the instantiation of +P's universal tyvars. You have to /match/ + the type of the pattern, (T [ty] Bool) +against + the psResultTy for the pattern synonym, T [a] Bool +to get the insantiation a := ty. + +This is very unlike DataCons, where univ tyvars match 1-1 the +arguments of the TyCon. + + Note [Pattern synonym representation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider the following pattern synonym declaration @@ -174,7 +212,7 @@ In this case, the fields of MkPatSyn will be set as follows: psExTyVars = [b] psProvTheta = (Show (Maybe t), Ord b) psReqTheta = (Eq t, Num t) - psOrigResTy = T (Maybe t) + psResultTy = T (Maybe t) Note [Matchers and builders for pattern synonyms] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -325,7 +363,7 @@ mkPatSyn name declared_infix psInfix = declared_infix, psArgs = orig_args, psArity = length orig_args, - psOrigResTy = orig_res_ty, + psResultTy = orig_res_ty, psMatcher = matcher, psBuilder = builder, psFieldLabels = field_labels @@ -368,7 +406,7 @@ patSynExTyVarBinders = psExTyVars patSynSig :: PatSyn -> ([TyVar], ThetaType, [TyVar], ThetaType, [Type], Type) patSynSig (MkPatSyn { psUnivTyVars = univ_tvs, psExTyVars = ex_tvs , psProvTheta = prov, psReqTheta = req - , psArgs = arg_tys, psOrigResTy = res_ty }) + , psArgs = arg_tys, psResultTy = res_ty }) = (binderVars univ_tvs, req, binderVars ex_tvs, prov, arg_tys, res_ty) patSynMatcher :: PatSyn -> (Id,Bool) @@ -405,9 +443,9 @@ patSynInstResTy :: PatSyn -> [Type] -> Type -- E.g. pattern P x y = Just (x,x,y) -- P :: a -> b -> Just (a,a,b) -- (patSynInstResTy P [Int,Bool] = Maybe (Int,Int,Bool) --- NB: unlikepatSynInstArgTys, the inst_tys should be just the *universal* tyvars +-- NB: unlike patSynInstArgTys, the inst_tys should be just the *universal* tyvars patSynInstResTy (MkPatSyn { psName = name, psUnivTyVars = univ_tvs - , psOrigResTy = res_ty }) + , psResultTy = res_ty }) inst_tys = ASSERT2( univ_tvs `equalLength` inst_tys , text "patSynInstResTy" <+> ppr name $$ ppr univ_tvs $$ ppr inst_tys ) @@ -417,7 +455,7 @@ patSynInstResTy (MkPatSyn { psName = name, psUnivTyVars = univ_tvs pprPatSynType :: PatSyn -> SDoc pprPatSynType (MkPatSyn { psUnivTyVars = univ_tvs, psReqTheta = req_theta , psExTyVars = ex_tvs, psProvTheta = prov_theta - , psArgs = orig_args, psOrigResTy = orig_res_ty }) + , psArgs = orig_args, psResultTy = orig_res_ty }) = sep [ pprForAll univ_tvs , pprThetaArrowTy req_theta , ppWhen insert_empty_ctxt $ parens empty <+> darrow diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs index cb9837ed0c..ce114e727b 100644 --- a/compiler/deSugar/Check.hs +++ b/compiler/deSugar/Check.hs @@ -18,7 +18,7 @@ module Check ( #include "HsVersions.h" import TmOracle - +import Unify( tcMatchTy ) import BasicTypes import DynFlags import HsSyn @@ -45,6 +45,7 @@ import Var (EvVar) import Type import UniqSupply import DsGRHSs (isTrueLHsExpr) +import Maybes ( expectJust ) import Data.List (find) import Data.Maybe (isJust, fromMaybe) @@ -971,14 +972,14 @@ mkOneConFull :: Id -> ConLike -> DsM (ValAbs, ComplexEq, Bag EvVar) -- ComplexEq: x ~ K y1..yn -- [EvVar]: Q mkOneConFull x con = do - let -- res_ty == TyConApp (ConLikeTyCon cabs_con) cabs_arg_tys - res_ty = idType x - (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , arg_tys, _) + let res_ty = idType x + (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , arg_tys, con_res_ty) = conLikeFullSig con - tc_args = case splitTyConApp_maybe res_ty of - Just (_, tys) -> tys - Nothing -> pprPanic "mkOneConFull: Not TyConApp:" (ppr res_ty) - subst1 = zipTvSubst univ_tvs tc_args + 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 (subst, ex_tvs') <- cloneTyVarBndrs subst1 ex_tvs <$> getUniqueSupplyM diff --git a/testsuite/tests/patsyn/should_compile/T13768.hs b/testsuite/tests/patsyn/should_compile/T13768.hs new file mode 100644 index 0000000000..c4510bd20a --- /dev/null +++ b/testsuite/tests/patsyn/should_compile/T13768.hs @@ -0,0 +1,33 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} +module T13768 where + +data NS (f :: k -> *) (xs :: [k]) = NS Int + +data IsNS (f :: k -> *) (xs :: [k]) where + IsZ :: f x -> IsNS f (x ': xs) + IsS :: NS f xs -> IsNS f (x ': xs) + +isNS :: NS f xs -> IsNS f xs +isNS = undefined + +pattern Z :: () => (xs' ~ (x ': xs)) => f x -> NS f xs' +pattern Z x <- (isNS -> IsZ x) + +pattern S :: () => (xs' ~ (x ': xs)) => NS f xs -> NS f xs' +pattern S p <- (isNS -> IsS p) + +{-# COMPLETE Z, S #-} + +data SList :: [k] -> * where + SNil :: SList '[] + SCons :: SList (x ': xs) + +go :: SList ys -> NS f ys -> Int +go SCons (Z _) = 0 +go SCons (S _) = 1 +go SNil _ = error "inaccessible" diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T index 30319c7050..286f735ac6 100644 --- a/testsuite/tests/patsyn/should_compile/all.T +++ b/testsuite/tests/patsyn/should_compile/all.T @@ -70,3 +70,4 @@ test('T13441b', normal, compile_fail, ['']) test('T13454', normal, compile, ['']) test('T13752', normal, compile, ['']) test('T13752a', normal, compile, ['']) +test('T13768', normal, compile, ['']) |