1{- 2(c) The University of Glasgow 2006 3(c) The GRASP/AQUA Project, Glasgow University, 1998 4 5\section[PatSyn]{@PatSyn@: Pattern synonyms} 6-} 7 8{-# LANGUAGE CPP #-} 9 10module GHC.Core.PatSyn ( 11 -- * Main data types 12 PatSyn, PatSynMatcher, PatSynBuilder, mkPatSyn, 13 14 -- ** Type deconstruction 15 patSynName, patSynArity, patSynIsInfix, patSynResultType, 16 isVanillaPatSyn, 17 patSynArgs, 18 patSynMatcher, patSynBuilder, 19 patSynUnivTyVarBinders, patSynExTyVars, patSynExTyVarBinders, 20 patSynSig, patSynSigBndr, 21 patSynInstArgTys, patSynInstResTy, patSynFieldLabels, 22 patSynFieldType, 23 24 pprPatSynType 25 ) where 26 27#include "GhclibHsVersions.h" 28 29import GHC.Prelude 30 31import GHC.Core.Type 32import GHC.Core.TyCo.Ppr 33import GHC.Types.Name 34import GHC.Types.Unique 35import GHC.Types.Basic 36import GHC.Types.Var 37import GHC.Types.FieldLabel 38 39import GHC.Utils.Misc 40import GHC.Utils.Outputable 41import GHC.Utils.Panic 42 43import qualified Data.Data as Data 44import Data.Function 45import Data.List (find) 46 47{- 48************************************************************************ 49* * 50\subsection{Pattern synonyms} 51* * 52************************************************************************ 53-} 54 55-- | Pattern Synonym 56-- 57-- See Note [Pattern synonym representation] 58-- See Note [Pattern synonym signature contexts] 59data PatSyn 60 = MkPatSyn { 61 psName :: Name, 62 psUnique :: Unique, -- Cached from Name 63 64 psArgs :: [Type], 65 psArity :: Arity, -- == length psArgs 66 psInfix :: Bool, -- True <=> declared infix 67 psFieldLabels :: [FieldLabel], -- List of fields for a 68 -- record pattern synonym 69 -- INVARIANT: either empty if no 70 -- record pat syn or same length as 71 -- psArgs 72 73 -- Universally-quantified type variables 74 psUnivTyVars :: [InvisTVBinder], 75 76 -- Required dictionaries (may mention psUnivTyVars) 77 psReqTheta :: ThetaType, 78 79 -- Existentially-quantified type vars 80 psExTyVars :: [InvisTVBinder], 81 82 -- Provided dictionaries (may mention psUnivTyVars or psExTyVars) 83 psProvTheta :: ThetaType, 84 85 -- Result type 86 psResultTy :: Type, -- Mentions only psUnivTyVars 87 -- See Note [Pattern synonym result type] 88 89 -- See Note [Matchers and builders for pattern synonyms] 90 -- See Note [Keep Ids out of PatSyn] 91 psMatcher :: PatSynMatcher, 92 psBuilder :: PatSynBuilder 93 } 94 95type PatSynMatcher = (Name, Type, Bool) 96 -- Matcher function. 97 -- If Bool is True then prov_theta and arg_tys are empty 98 -- and type is 99 -- forall (p :: RuntimeRep) (r :: TYPE p) univ_tvs. 100 -- req_theta 101 -- => res_ty 102 -- -> (forall ex_tvs. Void# -> r) 103 -- -> (Void# -> r) 104 -- -> r 105 -- 106 -- Otherwise type is 107 -- forall (p :: RuntimeRep) (r :: TYPE r) univ_tvs. 108 -- req_theta 109 -- => res_ty 110 -- -> (forall ex_tvs. prov_theta => arg_tys -> r) 111 -- -> (Void# -> r) 112 -- -> r 113 114type PatSynBuilder = Maybe (Name, Type, Bool) 115 -- Nothing => uni-directional pattern synonym 116 -- Just (builder, is_unlifted) => bi-directional 117 -- Builder function, of type 118 -- forall univ_tvs, ex_tvs. (req_theta, prov_theta) 119 -- => arg_tys -> res_ty 120 -- See Note [Builder for pattern synonyms with unboxed type] 121 122{- Note [Pattern synonym signature contexts] 123~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 124In a pattern synonym signature we write 125 pattern P :: req => prov => t1 -> ... tn -> res_ty 126 127Note that the "required" context comes first, then the "provided" 128context. Moreover, the "required" context must not mention 129existentially-bound type variables; that is, ones not mentioned in 130res_ty. See lots of discussion in #10928. 131 132If there is no "provided" context, you can omit it; but you 133can't omit the "required" part (unless you omit both). 134 135Example 1: 136 pattern P1 :: (Num a, Eq a) => b -> Maybe (a,b) 137 pattern P1 x = Just (3,x) 138 139 We require (Num a, Eq a) to match the 3; there is no provided 140 context. 141 142Example 2: 143 data T2 where 144 MkT2 :: (Num a, Eq a) => a -> a -> T2 145 146 pattern P2 :: () => (Num a, Eq a) => a -> T2 147 pattern P2 x = MkT2 3 x 148 149 When we match against P2 we get a Num dictionary provided. 150 We can use that to check the match against 3. 151 152Example 3: 153 pattern P3 :: Eq a => a -> b -> T3 b 154 155 This signature is illegal because the (Eq a) is a required 156 constraint, but it mentions the existentially-bound variable 'a'. 157 You can see it's existential because it doesn't appear in the 158 result type (T3 b). 159 160Note [Pattern synonym result type] 161~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 162Consider 163 data T a b = MkT b a 164 165 pattern P :: a -> T [a] Bool 166 pattern P x = MkT True [x] 167 168P's psResultTy is (T a Bool), and it really only matches values of 169type (T [a] Bool). For example, this is ill-typed 170 171 f :: T p q -> String 172 f (P x) = "urk" 173 174This is different to the situation with GADTs: 175 176 data S a where 177 MkS :: Int -> S Bool 178 179Now MkS (and pattern synonyms coming from MkS) can match a 180value of type (S a), not just (S Bool); we get type refinement. 181 182That in turn means that if you have a pattern 183 184 P x :: T [ty] Bool 185 186it's not entirely straightforward to work out the instantiation of 187P's universal tyvars. You have to /match/ 188 the type of the pattern, (T [ty] Bool) 189against 190 the psResultTy for the pattern synonym, T [a] Bool 191to get the instantiation a := ty. 192 193This is very unlike DataCons, where univ tyvars match 1-1 the 194arguments of the TyCon. 195 196Side note: I (SG) get the impression that instantiated return types should 197generate a *required* constraint for pattern synonyms, rather than a *provided* 198constraint like it's the case for GADTs. For example, I'd expect these 199declarations to have identical semantics: 200 201 pattern Just42 :: Maybe Int 202 pattern Just42 = Just 42 203 204 pattern Just'42 :: (a ~ Int) => Maybe a 205 pattern Just'42 = Just 42 206 207The latter generates the proper required constraint, the former does not. 208Also rather different to GADTs is the fact that Just42 doesn't have any 209universally quantified type variables, whereas Just'42 or MkS above has. 210 211Note [Keep Ids out of PatSyn] 212~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 213We carefully arrange that PatSyn does not contain the Ids for the matcher 214and builder. We want PatSyn, like TyCon and DataCon, to be completely 215immutable. But, the matcher and builder are relatively sophisticated 216functions, and we want to get their final IdInfo in the same way as 217any other Id, so we'd have to update the Ids in the PatSyn too. 218 219Rather than try to tidy PatSyns (which is easy to forget and is a bit 220tricky, see #19074), it seems cleaner to make them entirely immutable, 221like TyCons and Classes. To that end PatSynBuilder and PatSynMatcher 222contain Names not Ids. Which, it turns out, is absolutely fine. 223 224c.f. DefMethInfo in Class, which contains the Name, but not the Id, 225of the default method. 226 227Note [Pattern synonym representation] 228~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 229Consider the following pattern synonym declaration 230 231 pattern P x = MkT [x] (Just 42) 232 233where 234 data T a where 235 MkT :: (Show a, Ord b) => [b] -> a -> T a 236 237so pattern P has type 238 239 b -> T (Maybe t) 240 241with the following typeclass constraints: 242 243 requires: (Eq t, Num t) 244 provides: (Show (Maybe t), Ord b) 245 246In this case, the fields of MkPatSyn will be set as follows: 247 248 psArgs = [b] 249 psArity = 1 250 psInfix = False 251 252 psUnivTyVars = [t] 253 psExTyVars = [b] 254 psProvTheta = (Show (Maybe t), Ord b) 255 psReqTheta = (Eq t, Num t) 256 psResultTy = T (Maybe t) 257 258Note [Matchers and builders for pattern synonyms] 259~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 260For each pattern synonym P, we generate 261 262 * a "matcher" function, used to desugar uses of P in patterns, 263 which implements pattern matching 264 265 * A "builder" function (for bidirectional pattern synonyms only), 266 used to desugar uses of P in expressions, which constructs P-values. 267 268For the above example, the matcher function has type: 269 270 $mP :: forall (r :: ?) t. (Eq t, Num t) 271 => T (Maybe t) 272 -> (forall b. (Show (Maybe t), Ord b) => b -> r) 273 -> (Void# -> r) 274 -> r 275 276with the following implementation: 277 278 $mP @r @t $dEq $dNum scrut cont fail 279 = case scrut of 280 MkT @b $dShow $dOrd [x] (Just 42) -> cont @b $dShow $dOrd x 281 _ -> fail Void# 282 283Notice that the return type 'r' has an open kind, so that it can 284be instantiated by an unboxed type; for example where we see 285 f (P x) = 3# 286 287The extra Void# argument for the failure continuation is needed so that 288it is lazy even when the result type is unboxed. 289 290For the same reason, if the pattern has no arguments, an extra Void# 291argument is added to the success continuation as well. 292 293For *bidirectional* pattern synonyms, we also generate a "builder" 294function which implements the pattern synonym in an expression 295context. For our running example, it will be: 296 297 $bP :: forall t b. (Eq t, Num t, Show (Maybe t), Ord b) 298 => b -> T (Maybe t) 299 $bP x = MkT [x] (Just 42) 300 301NB: the existential/universal and required/provided split does not 302apply to the builder since you are only putting stuff in, not getting 303stuff out. 304 305Injectivity of bidirectional pattern synonyms is checked in 306tcPatToExpr which walks the pattern and returns its corresponding 307expression when available. 308 309Note [Builder for pattern synonyms with unboxed type] 310~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 311For bidirectional pattern synonyms that have no arguments and have an 312unboxed type, we add an extra Void# argument to the builder, else it 313would be a top-level declaration with an unboxed type. 314 315 pattern P = 0# 316 317 $bP :: Void# -> Int# 318 $bP _ = 0# 319 320This means that when typechecking an occurrence of P in an expression, 321we must remember that the builder has this void argument. This is 322done by GHC.Tc.TyCl.PatSyn.patSynBuilderOcc. 323 324Note [Pattern synonyms and the data type Type] 325~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 326The type of a pattern synonym is of the form (See Note 327[Pattern synonym signatures] in GHC.Tc.Gen.Sig): 328 329 forall univ_tvs. req => forall ex_tvs. prov => ... 330 331We cannot in general represent this by a value of type Type: 332 333 - if ex_tvs is empty, then req and prov cannot be distinguished from 334 each other 335 - if req is empty, then univ_tvs and ex_tvs cannot be distinguished 336 from each other, and moreover, prov is seen as the "required" context 337 (as it is the only context) 338 339 340************************************************************************ 341* * 342\subsection{Instances} 343* * 344************************************************************************ 345-} 346 347instance Eq PatSyn where 348 (==) = (==) `on` getUnique 349 (/=) = (/=) `on` getUnique 350 351instance Uniquable PatSyn where 352 getUnique = psUnique 353 354instance NamedThing PatSyn where 355 getName = patSynName 356 357instance Outputable PatSyn where 358 ppr = ppr . getName 359 360instance OutputableBndr PatSyn where 361 pprInfixOcc = pprInfixName . getName 362 pprPrefixOcc = pprPrefixName . getName 363 364instance Data.Data PatSyn where 365 -- don't traverse? 366 toConstr _ = abstractConstr "PatSyn" 367 gunfold _ _ = error "gunfold" 368 dataTypeOf _ = mkNoRepType "PatSyn" 369 370{- 371************************************************************************ 372* * 373\subsection{Construction} 374* * 375************************************************************************ 376-} 377 378-- | Build a new pattern synonym 379mkPatSyn :: Name 380 -> Bool -- ^ Is the pattern synonym declared infix? 381 -> ([InvisTVBinder], ThetaType) -- ^ Universially-quantified type 382 -- variables and required dicts 383 -> ([InvisTVBinder], ThetaType) -- ^ Existentially-quantified type 384 -- variables and provided dicts 385 -> [Type] -- ^ Original arguments 386 -> Type -- ^ Original result type 387 -> PatSynMatcher -- ^ Matcher 388 -> PatSynBuilder -- ^ Builder 389 -> [FieldLabel] -- ^ Names of fields for 390 -- a record pattern synonym 391 -> PatSyn 392 -- NB: The univ and ex vars are both in TyBinder form and TyVar form for 393 -- convenience. All the TyBinders should be Named! 394mkPatSyn name declared_infix 395 (univ_tvs, req_theta) 396 (ex_tvs, prov_theta) 397 orig_args 398 orig_res_ty 399 matcher builder field_labels 400 = MkPatSyn {psName = name, psUnique = getUnique name, 401 psUnivTyVars = univ_tvs, 402 psExTyVars = ex_tvs, 403 psProvTheta = prov_theta, psReqTheta = req_theta, 404 psInfix = declared_infix, 405 psArgs = orig_args, 406 psArity = length orig_args, 407 psResultTy = orig_res_ty, 408 psMatcher = matcher, 409 psBuilder = builder, 410 psFieldLabels = field_labels 411 } 412 413-- | The 'Name' of the 'PatSyn', giving it a unique, rooted identification 414patSynName :: PatSyn -> Name 415patSynName = psName 416 417-- | Should the 'PatSyn' be presented infix? 418patSynIsInfix :: PatSyn -> Bool 419patSynIsInfix = psInfix 420 421-- | Arity of the pattern synonym 422patSynArity :: PatSyn -> Arity 423patSynArity = psArity 424 425-- | Is this a \'vanilla\' pattern synonym (no existentials, no provided constraints)? 426isVanillaPatSyn :: PatSyn -> Bool 427isVanillaPatSyn ps = null (psExTyVars ps) && null (psProvTheta ps) 428 429patSynArgs :: PatSyn -> [Type] 430patSynArgs = psArgs 431 432patSynFieldLabels :: PatSyn -> [FieldLabel] 433patSynFieldLabels = psFieldLabels 434 435-- | Extract the type for any given labelled field of the 'DataCon' 436patSynFieldType :: PatSyn -> FieldLabelString -> Type 437patSynFieldType ps label 438 = case find ((== label) . flLabel . fst) (psFieldLabels ps `zip` psArgs ps) of 439 Just (_, ty) -> ty 440 Nothing -> pprPanic "dataConFieldType" (ppr ps <+> ppr label) 441 442patSynUnivTyVarBinders :: PatSyn -> [InvisTVBinder] 443patSynUnivTyVarBinders = psUnivTyVars 444 445patSynExTyVars :: PatSyn -> [TyVar] 446patSynExTyVars ps = binderVars (psExTyVars ps) 447 448patSynExTyVarBinders :: PatSyn -> [InvisTVBinder] 449patSynExTyVarBinders = psExTyVars 450 451patSynSigBndr :: PatSyn -> ([InvisTVBinder], ThetaType, [InvisTVBinder], ThetaType, [Scaled Type], Type) 452patSynSigBndr (MkPatSyn { psUnivTyVars = univ_tvs, psExTyVars = ex_tvs 453 , psProvTheta = prov, psReqTheta = req 454 , psArgs = arg_tys, psResultTy = res_ty }) 455 = (univ_tvs, req, ex_tvs, prov, map unrestricted arg_tys, res_ty) 456 457patSynSig :: PatSyn -> ([TyVar], ThetaType, [TyVar], ThetaType, [Scaled Type], Type) 458patSynSig ps = let (u_tvs, req, e_tvs, prov, arg_tys, res_ty) = patSynSigBndr ps 459 in (binderVars u_tvs, req, binderVars e_tvs, prov, arg_tys, res_ty) 460 461patSynMatcher :: PatSyn -> PatSynMatcher 462patSynMatcher = psMatcher 463 464patSynBuilder :: PatSyn -> PatSynBuilder 465patSynBuilder = psBuilder 466 467patSynResultType :: PatSyn -> Type 468patSynResultType = psResultTy 469 470patSynInstArgTys :: PatSyn -> [Type] -> [Type] 471-- Return the types of the argument patterns 472-- e.g. data D a = forall b. MkD a b (b->a) 473-- pattern P f x y = MkD (x,True) y f 474-- D :: forall a. forall b. a -> b -> (b->a) -> D a 475-- P :: forall c. forall b. (b->(c,Bool)) -> c -> b -> P c 476-- patSynInstArgTys P [Int,bb] = [bb->(Int,Bool), Int, bb] 477-- NB: the inst_tys should be both universal and existential 478patSynInstArgTys (MkPatSyn { psName = name, psUnivTyVars = univ_tvs 479 , psExTyVars = ex_tvs, psArgs = arg_tys }) 480 inst_tys 481 = ASSERT2( tyvars `equalLength` inst_tys 482 , text "patSynInstArgTys" <+> ppr name $$ ppr tyvars $$ ppr inst_tys ) 483 map (substTyWith tyvars inst_tys) arg_tys 484 where 485 tyvars = binderVars (univ_tvs ++ ex_tvs) 486 487patSynInstResTy :: PatSyn -> [Type] -> Type 488-- Return the type of whole pattern 489-- E.g. pattern P x y = Just (x,x,y) 490-- P :: a -> b -> Just (a,a,b) 491-- (patSynInstResTy P [Int,Bool] = Maybe (Int,Int,Bool) 492-- NB: unlike patSynInstArgTys, the inst_tys should be just the *universal* tyvars 493patSynInstResTy (MkPatSyn { psName = name, psUnivTyVars = univ_tvs 494 , psResultTy = res_ty }) 495 inst_tys 496 = ASSERT2( univ_tvs `equalLength` inst_tys 497 , text "patSynInstResTy" <+> ppr name $$ ppr univ_tvs $$ ppr inst_tys ) 498 substTyWith (binderVars univ_tvs) inst_tys res_ty 499 500-- | Print the type of a pattern synonym. The foralls are printed explicitly 501pprPatSynType :: PatSyn -> SDoc 502pprPatSynType (MkPatSyn { psUnivTyVars = univ_tvs, psReqTheta = req_theta 503 , psExTyVars = ex_tvs, psProvTheta = prov_theta 504 , psArgs = orig_args, psResultTy = orig_res_ty }) 505 = sep [ pprForAll $ tyVarSpecToBinders univ_tvs 506 , pprThetaArrowTy req_theta 507 , ppWhen insert_empty_ctxt $ parens empty <+> darrow 508 , pprType sigma_ty ] 509 where 510 sigma_ty = mkInvisForAllTys ex_tvs $ 511 mkInvisFunTysMany prov_theta $ 512 mkVisFunTysMany orig_args orig_res_ty 513 insert_empty_ctxt = null req_theta && not (null prov_theta && null ex_tvs) 514