PatSyn.hs 17.1 KB
Newer Older
Austin Seipp's avatar
Austin Seipp committed
1 2 3 4
{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1998

cactus's avatar
cactus committed
5
\section[PatSyn]{@PatSyn@: Pattern synonyms}
Austin Seipp's avatar
Austin Seipp committed
6
-}
cactus's avatar
cactus committed
7

8
{-# LANGUAGE CPP #-}
cactus's avatar
cactus committed
9

Sylvain Henry's avatar
Sylvain Henry committed
10
module GHC.Core.PatSyn (
cactus's avatar
cactus committed
11 12 13 14
        -- * Main data types
        PatSyn, mkPatSyn,

        -- ** Type deconstruction
15
        patSynName, patSynArity, patSynIsInfix,
16
        patSynArgs,
17
        patSynMatcher, patSynBuilder,
Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
18 19
        patSynUnivTyVarBinders, patSynExTyVars, patSynExTyVarBinders,
        patSynSig, patSynSigBndr,
Matthew Pickering's avatar
Matthew Pickering committed
20 21 22
        patSynInstArgTys, patSynInstResTy, patSynFieldLabels,
        patSynFieldType,

23
        updatePatSynIds, pprPatSynType
cactus's avatar
cactus committed
24 25 26 27
    ) where

#include "HsVersions.h"

28
import GHC.Prelude
29

Sylvain Henry's avatar
Sylvain Henry committed
30 31
import GHC.Core.Type
import GHC.Core.TyCo.Ppr
Sylvain Henry's avatar
Sylvain Henry committed
32 33 34 35 36
import GHC.Types.Name
import GHC.Types.Unique
import GHC.Types.Basic
import GHC.Types.Var
import GHC.Types.FieldLabel
cactus's avatar
cactus committed
37

38 39 40 41
import GHC.Utils.Misc
import GHC.Utils.Outputable
import GHC.Utils.Panic

cactus's avatar
cactus committed
42 43
import qualified Data.Data as Data
import Data.Function
44
import Data.List (find)
cactus's avatar
cactus committed
45

Austin Seipp's avatar
Austin Seipp committed
46 47 48
{-
************************************************************************
*                                                                      *
49
\subsection{Pattern synonyms}
Austin Seipp's avatar
Austin Seipp committed
50 51 52
*                                                                      *
************************************************************************
-}
53

54 55
-- | Pattern Synonym
--
56
-- See Note [Pattern synonym representation]
57
-- See Note [Pattern synonym signature contexts]
58 59 60
data PatSyn
  = MkPatSyn {
        psName        :: Name,
Matthew Pickering's avatar
Matthew Pickering committed
61
        psUnique      :: Unique,       -- Cached from Name
62 63

        psArgs        :: [Type],
Matthew Pickering's avatar
Matthew Pickering committed
64 65 66 67 68 69 70 71
        psArity       :: Arity,        -- == length psArgs
        psInfix       :: Bool,         -- True <=> declared infix
        psFieldLabels :: [FieldLabel], -- List of fields for a
                                       -- record pattern synonym
                                       -- INVARIANT: either empty if no
                                       -- record pat syn or same length as
                                       -- psArgs

72
        -- Universally-quantified type variables
Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
73
        psUnivTyVars  :: [InvisTVBinder],
74 75 76 77 78

        -- Required dictionaries (may mention psUnivTyVars)
        psReqTheta    :: ThetaType,

        -- Existentially-quantified type vars
Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
79
        psExTyVars    :: [InvisTVBinder],
80 81 82 83 84

        -- Provided dictionaries (may mention psUnivTyVars or psExTyVars)
        psProvTheta   :: ThetaType,

        -- Result type
85
        psResultTy   :: Type,  -- Mentions only psUnivTyVars
Ningning Xie's avatar
Ningning Xie committed
86
                               -- See Note [Pattern synonym result type]
87 88 89 90 91 92

        -- See Note [Matchers and builders for pattern synonyms]
        psMatcher     :: (Id, Bool),
             -- Matcher function.
             -- If Bool is True then prov_theta and arg_tys are empty
             -- and type is
93
             --   forall (p :: RuntimeRep) (r :: TYPE p) univ_tvs.
94
             --                          req_theta
95 96 97 98 99 100
             --                       => res_ty
             --                       -> (forall ex_tvs. Void# -> r)
             --                       -> (Void# -> r)
             --                       -> r
             --
             -- Otherwise type is
101
             --   forall (p :: RuntimeRep) (r :: TYPE r) univ_tvs.
102
             --                          req_theta
103 104 105 106 107 108 109 110
             --                       => res_ty
             --                       -> (forall ex_tvs. prov_theta => arg_tys -> r)
             --                       -> (Void# -> r)
             --                       -> r

        psBuilder     :: Maybe (Id, Bool)
             -- Nothing  => uni-directional pattern synonym
             -- Just (builder, is_unlifted) => bi-directional
111
             -- Builder function, of type
112
             --  forall univ_tvs, ex_tvs. (req_theta, prov_theta)
113 114 115 116
             --                       =>  arg_tys -> res_ty
             -- See Note [Builder for pattern synonyms with unboxed type]
  }

117
{- Note [Pattern synonym signature contexts]
118 119 120 121 122 123 124
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In a pattern synonym signature we write
   pattern P :: req => prov => t1 -> ... tn -> res_ty

Note that the "required" context comes first, then the "provided"
context.  Moreover, the "required" context must not mention
existentially-bound type variables; that is, ones not mentioned in
125
res_ty.  See lots of discussion in #10928.
126 127 128 129 130 131 132 133 134 135 136 137 138 139 140

If there is no "provided" context, you can omit it; but you
can't omit the "required" part (unless you omit both).

Example 1:
      pattern P1 :: (Num a, Eq a) => b -> Maybe (a,b)
      pattern P1 x = Just (3,x)

  We require (Num a, Eq a) to match the 3; there is no provided
  context.

Example 2:
      data T2 where
        MkT2 :: (Num a, Eq a) => a -> a -> T2

Rik Steenkamp's avatar
Rik Steenkamp committed
141
      pattern P2 :: () => (Num a, Eq a) => a -> T2
142 143 144 145 146 147 148 149 150 151 152 153 154
      pattern P2 x = MkT2 3 x

  When we match against P2 we get a Num dictionary provided.
  We can use that to check the match against 3.

Example 3:
      pattern P3 :: Eq a => a -> b -> T3 b

   This signature is illegal because the (Eq a) is a required
   constraint, but it mentions the existentially-bound variable 'a'.
   You can see it's existential because it doesn't appear in the
   result type (T3 b).

155 156 157 158 159 160 161 162 163 164 165 166 167 168
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"

Gabor Greif's avatar
Gabor Greif committed
169
This is different to the situation with GADTs:
170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185

   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
Gabor Greif's avatar
Gabor Greif committed
186
to get the instantiation a := ty.
187 188 189 190

This is very unlike DataCons, where univ tyvars match 1-1 the
arguments of the TyCon.

191 192 193 194 195 196 197 198 199 200 201 202 203 204
Side note: I (SG) get the impression that instantiated return types should
generate a *required* constraint for pattern synonyms, rather than a *provided*
constraint like it's the case for GADTs. For example, I'd expect these
declarations to have identical semantics:

    pattern Just42 :: Maybe Int
    pattern Just42 = Just 42

    pattern Just'42 :: (a ~ Int) => Maybe a
    pattern Just'42 = Just 42

The latter generates the proper required constraint, the former does not.
Also rather different to GADTs is the fact that Just42 doesn't have any
universally quantified type variables, whereas Just'42 or MkS above has.
205

206 207
Note [Pattern synonym representation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
cactus's avatar
cactus committed
208 209 210 211 212 213 214 215 216 217 218 219 220 221 222
Consider the following pattern synonym declaration

        pattern P x = MkT [x] (Just 42)

where
        data T a where
              MkT :: (Show a, Ord b) => [b] -> a -> T a

so pattern P has type

        b -> T (Maybe t)

with the following typeclass constraints:

        requires: (Eq t, Num t)
223
        provides: (Show (Maybe t), Ord b)
cactus's avatar
cactus committed
224 225 226

In this case, the fields of MkPatSyn will be set as follows:

227
  psArgs       = [b]
cactus's avatar
cactus committed
228 229 230 231 232
  psArity      = 1
  psInfix      = False

  psUnivTyVars = [t]
  psExTyVars   = [b]
233 234
  psProvTheta  = (Show (Maybe t), Ord b)
  psReqTheta   = (Eq t, Num t)
235
  psResultTy  = T (Maybe t)
cactus's avatar
cactus committed
236

237
Note [Matchers and builders for pattern synonyms]
238
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
239 240 241 242 243 244 245 246 247
For each pattern synonym P, we generate

  * a "matcher" function, used to desugar uses of P in patterns,
    which implements pattern matching

  * A "builder" function (for bidirectional pattern synonyms only),
    used to desugar uses of P in expressions, which constructs P-values.

For the above example, the matcher function has type:
248

249
        $mP :: forall (r :: ?) t. (Eq t, Num t)
250 251
            => T (Maybe t)
            -> (forall b. (Show (Maybe t), Ord b) => b -> r)
252
            -> (Void# -> r)
253 254 255 256
            -> r

with the following implementation:

Austin Seipp's avatar
Austin Seipp committed
257
        $mP @r @t $dEq $dNum scrut cont fail
258 259 260 261 262 263 264
          = case scrut of
              MkT @b $dShow $dOrd [x] (Just 42) -> cont @b $dShow $dOrd x
              _                                 -> fail Void#

Notice that the return type 'r' has an open kind, so that it can
be instantiated by an unboxed type; for example where we see
     f (P x) = 3#
265 266

The extra Void# argument for the failure continuation is needed so that
Austin Seipp's avatar
Austin Seipp committed
267
it is lazy even when the result type is unboxed.
268

269 270 271 272
For the same reason, if the pattern has no arguments, an extra Void#
argument is added to the success continuation as well.

For *bidirectional* pattern synonyms, we also generate a "builder"
273 274 275
function which implements the pattern synonym in an expression
context. For our running example, it will be:

276
        $bP :: forall t b. (Eq t, Num t, Show (Maybe t), Ord b)
277
            => b -> T (Maybe t)
278
        $bP x = MkT [x] (Just 42)
279 280

NB: the existential/universal and required/provided split does not
281
apply to the builder since you are only putting stuff in, not getting
282 283 284 285 286
stuff out.

Injectivity of bidirectional pattern synonyms is checked in
tcPatToExpr which walks the pattern and returns its corresponding
expression when available.
cactus's avatar
cactus committed
287

288 289 290 291 292
Note [Builder for pattern synonyms with unboxed type]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For bidirectional pattern synonyms that have no arguments and have an
unboxed type, we add an extra Void# argument to the builder, else it
would be a top-level declaration with an unboxed type.
293 294 295

        pattern P = 0#

296 297
        $bP :: Void# -> Int#
        $bP _ = 0#
298

299 300
This means that when typechecking an occurrence of P in an expression,
we must remember that the builder has this void argument. This is
Sylvain Henry's avatar
Sylvain Henry committed
301
done by GHC.Tc.TyCl.PatSyn.patSynBuilderOcc.
302

Gabor Greif's avatar
Gabor Greif committed
303
Note [Pattern synonyms and the data type Type]
304 305
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The type of a pattern synonym is of the form (See Note
Sylvain Henry's avatar
Sylvain Henry committed
306
[Pattern synonym signatures] in GHC.Tc.Gen.Sig):
307 308 309 310 311 312 313 314 315 316 317

    forall univ_tvs. req => forall ex_tvs. prov => ...

We cannot in general represent this by a value of type Type:

 - if ex_tvs is empty, then req and prov cannot be distinguished from
   each other
 - if req is empty, then univ_tvs and ex_tvs cannot be distinguished
   from each other, and moreover, prov is seen as the "required" context
   (as it is the only context)

cactus's avatar
cactus committed
318

Austin Seipp's avatar
Austin Seipp committed
319 320
************************************************************************
*                                                                      *
cactus's avatar
cactus committed
321
\subsection{Instances}
Austin Seipp's avatar
Austin Seipp committed
322 323 324
*                                                                      *
************************************************************************
-}
cactus's avatar
cactus committed
325 326 327 328 329 330 331 332 333

instance Eq PatSyn where
    (==) = (==) `on` getUnique
    (/=) = (/=) `on` getUnique

instance Uniquable PatSyn where
    getUnique = psUnique

instance NamedThing PatSyn where
334
    getName = patSynName
cactus's avatar
cactus committed
335 336 337 338 339 340 341 342 343 344 345 346 347 348

instance Outputable PatSyn where
    ppr = ppr . getName

instance OutputableBndr PatSyn where
    pprInfixOcc = pprInfixName . getName
    pprPrefixOcc = pprPrefixName . getName

instance Data.Data PatSyn where
    -- don't traverse?
    toConstr _   = abstractConstr "PatSyn"
    gunfold _ _  = error "gunfold"
    dataTypeOf _ = mkNoRepType "PatSyn"

Austin Seipp's avatar
Austin Seipp committed
349 350 351
{-
************************************************************************
*                                                                      *
cactus's avatar
cactus committed
352
\subsection{Construction}
Austin Seipp's avatar
Austin Seipp committed
353 354 355
*                                                                      *
************************************************************************
-}
cactus's avatar
cactus committed
356 357 358

-- | Build a new pattern synonym
mkPatSyn :: Name
359
         -> Bool                 -- ^ Is the pattern synonym declared infix?
Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
360 361 362 363
         -> ([InvisTVBinder], ThetaType) -- ^ Universially-quantified type
                                         -- variables and required dicts
         -> ([InvisTVBinder], ThetaType) -- ^ Existentially-quantified type
                                         -- variables and provided dicts
364 365
         -> [Type]               -- ^ Original arguments
         -> Type                 -- ^ Original result type
366 367
         -> (Id, Bool)           -- ^ Name of matcher
         -> Maybe (Id, Bool)     -- ^ Name of builder
Matthew Pickering's avatar
Matthew Pickering committed
368 369
         -> [FieldLabel]         -- ^ Names of fields for
                                 --   a record pattern synonym
cactus's avatar
cactus committed
370
         -> PatSyn
371 372
 -- NB: The univ and ex vars are both in TyBinder form and TyVar form for
 -- convenience. All the TyBinders should be Named!
373
mkPatSyn name declared_infix
Simon Peyton Jones's avatar
Simon Peyton Jones committed
374 375
         (univ_tvs, req_theta)
         (ex_tvs, prov_theta)
376
         orig_args
cactus's avatar
cactus committed
377
         orig_res_ty
Matthew Pickering's avatar
Matthew Pickering committed
378
         matcher builder field_labels
379
    = MkPatSyn {psName = name, psUnique = getUnique name,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
380 381
                psUnivTyVars = univ_tvs,
                psExTyVars = ex_tvs,
382
                psProvTheta = prov_theta, psReqTheta = req_theta,
cactus's avatar
cactus committed
383 384 385
                psInfix = declared_infix,
                psArgs = orig_args,
                psArity = length orig_args,
386
                psResultTy = orig_res_ty,
cactus's avatar
cactus committed
387
                psMatcher = matcher,
Matthew Pickering's avatar
Matthew Pickering committed
388 389 390
                psBuilder = builder,
                psFieldLabels = field_labels
                }
cactus's avatar
cactus committed
391 392

-- | The 'Name' of the 'PatSyn', giving it a unique, rooted identification
393 394
patSynName :: PatSyn -> Name
patSynName = psName
cactus's avatar
cactus committed
395 396 397 398 399 400 401 402 403

-- | Should the 'PatSyn' be presented infix?
patSynIsInfix :: PatSyn -> Bool
patSynIsInfix = psInfix

-- | Arity of the pattern synonym
patSynArity :: PatSyn -> Arity
patSynArity = psArity

404
patSynArgs :: PatSyn -> [Type]
cactus's avatar
cactus committed
405 406
patSynArgs = psArgs

Matthew Pickering's avatar
Matthew Pickering committed
407 408 409 410 411 412 413 414 415 416
patSynFieldLabels :: PatSyn -> [FieldLabel]
patSynFieldLabels = psFieldLabels

-- | Extract the type for any given labelled field of the 'DataCon'
patSynFieldType :: PatSyn -> FieldLabelString -> Type
patSynFieldType ps label
  = case find ((== label) . flLabel . fst) (psFieldLabels ps `zip` psArgs ps) of
      Just (_, ty) -> ty
      Nothing -> pprPanic "dataConFieldType" (ppr ps <+> ppr label)

Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
417
patSynUnivTyVarBinders :: PatSyn -> [InvisTVBinder]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
418
patSynUnivTyVarBinders = psUnivTyVars
419

cactus's avatar
cactus committed
420
patSynExTyVars :: PatSyn -> [TyVar]
421
patSynExTyVars ps = binderVars (psExTyVars ps)
cactus's avatar
cactus committed
422

Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
423
patSynExTyVarBinders :: PatSyn -> [InvisTVBinder]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
424
patSynExTyVarBinders = psExTyVars
425

Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
426
patSynSigBndr :: PatSyn -> ([InvisTVBinder], ThetaType, [InvisTVBinder], ThetaType, [Scaled Type], Type)
Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
427
patSynSigBndr (MkPatSyn { psUnivTyVars = univ_tvs, psExTyVars = ex_tvs
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
428 429 430
                        , psProvTheta = prov, psReqTheta = req
                        , psArgs = arg_tys, psResultTy = res_ty })
  = (univ_tvs, req, ex_tvs, prov, map unrestricted arg_tys, res_ty)
Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
431

Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
432
patSynSig :: PatSyn -> ([TyVar], ThetaType, [TyVar], ThetaType, [Scaled Type], Type)
Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
433 434
patSynSig ps = let (u_tvs, req, e_tvs, prov, arg_tys, res_ty) = patSynSigBndr ps
               in (binderVars u_tvs, req, binderVars e_tvs, prov, arg_tys, res_ty)
cactus's avatar
cactus committed
435

436
patSynMatcher :: PatSyn -> (Id,Bool)
cactus's avatar
cactus committed
437 438
patSynMatcher = psMatcher

439 440 441
patSynBuilder :: PatSyn -> Maybe (Id, Bool)
patSynBuilder = psBuilder

442 443
updatePatSynIds :: (Id -> Id) -> PatSyn -> PatSyn
updatePatSynIds tidy_fn ps@(MkPatSyn { psMatcher = matcher, psBuilder = builder })
444 445 446
  = ps { psMatcher = tidy_pr matcher, psBuilder = fmap tidy_pr builder }
  where
    tidy_pr (id, dummy) = (tidy_fn id, dummy)
447

cactus's avatar
cactus committed
448
patSynInstArgTys :: PatSyn -> [Type] -> [Type]
449 450 451 452 453 454 455
-- Return the types of the argument patterns
-- e.g.  data D a = forall b. MkD a b (b->a)
--       pattern P f x y = MkD (x,True) y f
--          D :: forall a. forall b. a -> b -> (b->a) -> D a
--          P :: forall c. forall b. (b->(c,Bool)) -> c -> b -> P c
--   patSynInstArgTys P [Int,bb] = [bb->(Int,Bool), Int, bb]
-- NB: the inst_tys should be both universal and existential
456 457 458
patSynInstArgTys (MkPatSyn { psName = name, psUnivTyVars = univ_tvs
                           , psExTyVars = ex_tvs, psArgs = arg_tys })
                 inst_tys
459
  = ASSERT2( tyvars `equalLength` inst_tys
460
          , text "patSynInstArgTys" <+> ppr name $$ ppr tyvars $$ ppr inst_tys )
461
    map (substTyWith tyvars inst_tys) arg_tys
cactus's avatar
cactus committed
462
  where
463
    tyvars = binderVars (univ_tvs ++ ex_tvs)
464 465 466 467 468 469

patSynInstResTy :: PatSyn -> [Type] -> Type
-- Return the type of whole pattern
-- 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)
470
-- NB: unlike patSynInstArgTys, the inst_tys should be just the *universal* tyvars
471
patSynInstResTy (MkPatSyn { psName = name, psUnivTyVars = univ_tvs
472
                          , psResultTy = res_ty })
473
                inst_tys
474
  = ASSERT2( univ_tvs `equalLength` inst_tys
475
           , text "patSynInstResTy" <+> ppr name $$ ppr univ_tvs $$ ppr inst_tys )
476
    substTyWith (binderVars univ_tvs) inst_tys res_ty
477 478 479 480 481

-- | Print the type of a pattern synonym. The foralls are printed explicitly
pprPatSynType :: PatSyn -> SDoc
pprPatSynType (MkPatSyn { psUnivTyVars = univ_tvs,  psReqTheta  = req_theta
                        , psExTyVars   = ex_tvs,    psProvTheta = prov_theta
482
                        , psArgs       = orig_args, psResultTy = orig_res_ty })
Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
483
  = sep [ pprForAll $ tyVarSpecToBinders univ_tvs
484 485 486 487
        , pprThetaArrowTy req_theta
        , ppWhen insert_empty_ctxt $ parens empty <+> darrow
        , pprType sigma_ty ]
  where
Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
488
    sigma_ty = mkInvisForAllTys ex_tvs $
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
489 490
               mkInvisFunTysMany prov_theta $
               mkVisFunTysMany orig_args orig_res_ty
491
    insert_empty_ctxt = null req_theta && not (null prov_theta && null ex_tvs)