PatSyn.hs 16.7 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,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
18
        patSynUnivTyVarBinders, patSynExTyVars, patSynExTyVarBinders, patSynSig,
Matthew Pickering's avatar
Matthew Pickering committed
19 20 21
        patSynInstArgTys, patSynInstResTy, patSynFieldLabels,
        patSynFieldType,

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

#include "HsVersions.h"

27 28
import GhcPrelude

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

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

Austin Seipp's avatar
Austin Seipp committed
43 44 45
{-
************************************************************************
*                                                                      *
46
\subsection{Pattern synonyms}
Austin Seipp's avatar
Austin Seipp committed
47 48 49
*                                                                      *
************************************************************************
-}
50

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

        psArgs        :: [Type],
Matthew Pickering's avatar
Matthew Pickering committed
61 62 63 64 65 66 67 68
        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

69
        -- Universally-quantified type variables
Simon Peyton Jones's avatar
Simon Peyton Jones committed
70
        psUnivTyVars  :: [TyVarBinder],
71 72 73 74 75

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

        -- Existentially-quantified type vars
Simon Peyton Jones's avatar
Simon Peyton Jones committed
76
        psExTyVars    :: [TyVarBinder],
77 78 79 80 81

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

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

        -- 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
90
             --   forall (p :: RuntimeRep) (r :: TYPE p) univ_tvs.
91
             --                          req_theta
92 93 94 95 96 97
             --                       => res_ty
             --                       -> (forall ex_tvs. Void# -> r)
             --                       -> (Void# -> r)
             --                       -> r
             --
             -- Otherwise type is
98
             --   forall (p :: RuntimeRep) (r :: TYPE r) univ_tvs.
99
             --                          req_theta
100 101 102 103 104 105 106 107
             --                       => 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
108
             -- Builder function, of type
109
             --  forall univ_tvs, ex_tvs. (req_theta, prov_theta)
110 111 112 113
             --                       =>  arg_tys -> res_ty
             -- See Note [Builder for pattern synonyms with unboxed type]
  }

114
{- Note [Pattern synonym signature contexts]
115 116 117 118 119 120 121
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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
122
res_ty.  See lots of discussion in #10928.
123 124 125 126 127 128 129 130 131 132 133 134 135 136 137

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
138
      pattern P2 :: () => (Num a, Eq a) => a -> T2
139 140 141 142 143 144 145 146 147 148 149 150 151
      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).

152 153 154 155 156 157 158 159 160 161 162 163 164 165
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
166
This is different to the situation with GADTs:
167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182

   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
183
to get the instantiation a := ty.
184 185 186 187

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

188 189 190 191 192 193 194 195 196 197 198 199 200 201
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.
202

203 204
Note [Pattern synonym representation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
cactus's avatar
cactus committed
205 206 207 208 209 210 211 212 213 214 215 216 217 218 219
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)
220
        provides: (Show (Maybe t), Ord b)
cactus's avatar
cactus committed
221 222 223

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

224
  psArgs       = [b]
cactus's avatar
cactus committed
225 226 227 228 229
  psArity      = 1
  psInfix      = False

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

234
Note [Matchers and builders for pattern synonyms]
235
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
236 237 238 239 240 241 242 243 244
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:
245

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

with the following implementation:

Austin Seipp's avatar
Austin Seipp committed
254
        $mP @r @t $dEq $dNum scrut cont fail
255 256 257 258 259 260 261
          = 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#
262 263

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

266 267 268 269
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"
270 271 272
function which implements the pattern synonym in an expression
context. For our running example, it will be:

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

NB: the existential/universal and required/provided split does not
278
apply to the builder since you are only putting stuff in, not getting
279 280 281 282 283
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
284

285 286 287 288 289
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.
290 291 292

        pattern P = 0#

293 294
        $bP :: Void# -> Int#
        $bP _ = 0#
295

296 297
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
298
done by GHC.Tc.TyCl.PatSyn.patSynBuilderOcc.
299

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

    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
315

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

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

instance Uniquable PatSyn where
    getUnique = psUnique

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

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
346 347 348
{-
************************************************************************
*                                                                      *
cactus's avatar
cactus committed
349
\subsection{Construction}
Austin Seipp's avatar
Austin Seipp committed
350 351 352
*                                                                      *
************************************************************************
-}
cactus's avatar
cactus committed
353 354 355

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

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

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

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

401
patSynArgs :: PatSyn -> [Type]
cactus's avatar
cactus committed
402 403
patSynArgs = psArgs

Matthew Pickering's avatar
Matthew Pickering committed
404 405 406 407 408 409 410 411 412 413
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)

Simon Peyton Jones's avatar
Simon Peyton Jones committed
414 415
patSynUnivTyVarBinders :: PatSyn -> [TyVarBinder]
patSynUnivTyVarBinders = psUnivTyVars
416

cactus's avatar
cactus committed
417
patSynExTyVars :: PatSyn -> [TyVar]
418
patSynExTyVars ps = binderVars (psExTyVars ps)
cactus's avatar
cactus committed
419

Simon Peyton Jones's avatar
Simon Peyton Jones committed
420 421
patSynExTyVarBinders :: PatSyn -> [TyVarBinder]
patSynExTyVarBinders = psExTyVars
422

423
patSynSig :: PatSyn -> ([TyVar], ThetaType, [TyVar], ThetaType, [Type], Type)
424
patSynSig (MkPatSyn { psUnivTyVars = univ_tvs, psExTyVars = ex_tvs
425
                    , psProvTheta = prov, psReqTheta = req
426
                    , psArgs = arg_tys, psResultTy = res_ty })
427
  = (binderVars univ_tvs, req, binderVars ex_tvs, prov, arg_tys, res_ty)
cactus's avatar
cactus committed
428

429
patSynMatcher :: PatSyn -> (Id,Bool)
cactus's avatar
cactus committed
430 431
patSynMatcher = psMatcher

432 433 434
patSynBuilder :: PatSyn -> Maybe (Id, Bool)
patSynBuilder = psBuilder

435 436
updatePatSynIds :: (Id -> Id) -> PatSyn -> PatSyn
updatePatSynIds tidy_fn ps@(MkPatSyn { psMatcher = matcher, psBuilder = builder })
437 438 439
  = ps { psMatcher = tidy_pr matcher, psBuilder = fmap tidy_pr builder }
  where
    tidy_pr (id, dummy) = (tidy_fn id, dummy)
440

cactus's avatar
cactus committed
441
patSynInstArgTys :: PatSyn -> [Type] -> [Type]
442 443 444 445 446 447 448
-- 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
449 450 451
patSynInstArgTys (MkPatSyn { psName = name, psUnivTyVars = univ_tvs
                           , psExTyVars = ex_tvs, psArgs = arg_tys })
                 inst_tys
452
  = ASSERT2( tyvars `equalLength` inst_tys
453
          , text "patSynInstArgTys" <+> ppr name $$ ppr tyvars $$ ppr inst_tys )
454
    map (substTyWith tyvars inst_tys) arg_tys
cactus's avatar
cactus committed
455
  where
456
    tyvars = binderVars (univ_tvs ++ ex_tvs)
457 458 459 460 461 462

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)
463
-- NB: unlike patSynInstArgTys, the inst_tys should be just the *universal* tyvars
464
patSynInstResTy (MkPatSyn { psName = name, psUnivTyVars = univ_tvs
465
                          , psResultTy = res_ty })
466
                inst_tys
467
  = ASSERT2( univ_tvs `equalLength` inst_tys
468
           , text "patSynInstResTy" <+> ppr name $$ ppr univ_tvs $$ ppr inst_tys )
469
    substTyWith (binderVars univ_tvs) inst_tys res_ty
470 471 472 473 474

-- | 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
475
                        , psArgs       = orig_args, psResultTy = orig_res_ty })
Simon Peyton Jones's avatar
Simon Peyton Jones committed
476
  = sep [ pprForAll univ_tvs
477 478 479 480
        , pprThetaArrowTy req_theta
        , ppWhen insert_empty_ctxt $ parens empty <+> darrow
        , pprType sigma_ty ]
  where
Simon Peyton Jones's avatar
Simon Peyton Jones committed
481
    sigma_ty = mkForAllTys ex_tvs  $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
482 483
               mkInvisFunTys prov_theta $
               mkVisFunTys orig_args orig_res_ty
484
    insert_empty_ctxt = null req_theta && not (null prov_theta && null ex_tvs)