TcPatSyn.hs 36.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, 1992-1998

Gergő Érdi's avatar
Gergő Érdi committed
5
\section[TcPatSyn]{Typechecking pattern synonym declarations}
Austin Seipp's avatar
Austin Seipp committed
6
-}
Gergő Érdi's avatar
Gergő Érdi committed
7

8 9
{-# LANGUAGE CPP #-}

10
module TcPatSyn ( tcPatSynSig, tcInferPatSynDecl, tcCheckPatSynDecl
Matthew Pickering's avatar
Matthew Pickering committed
11
                , tcPatSynBuilderBind, tcPatSynBuilderOcc, nonBidirectionalErr
12
  ) where
Gergő Érdi's avatar
Gergő Érdi committed
13 14 15

import HsSyn
import TcPat
16
import TcHsType( tcImplicitTKBndrs, tcExplicitTKBndrs
17
               , tcHsContext, tcHsLiftedType, tcHsOpenType )
Gergő Érdi's avatar
Gergő Érdi committed
18 19 20 21
import TcRnMonad
import TcEnv
import TcMType
import TysPrim
22
import TysWiredIn  ( levityTy )
Gergő Érdi's avatar
Gergő Érdi committed
23 24 25 26 27 28 29 30 31
import Name
import SrcLoc
import PatSyn
import NameSet
import Panic
import Outputable
import FastString
import Var
import Id
32
import IdInfo( RecSelParent(..))
Gergő Érdi's avatar
Gergő Érdi committed
33 34 35
import TcBinds
import BasicTypes
import TcSimplify
36
import TcUnify
Gergő Érdi's avatar
Gergő Érdi committed
37
import TcType
38 39
import TcEvidence
import BuildTyCl
Gergő Érdi's avatar
Gergő Érdi committed
40
import VarSet
41
import MkId
42
import TcTyDecls
Matthew Pickering's avatar
Matthew Pickering committed
43 44
import ConLike
import FieldLabel
Gergő Érdi's avatar
Gergő Érdi committed
45
import Bag
46
import Util
47
import Data.Maybe
48 49 50
import Control.Monad ( unless, zipWithM )
import Data.List( partition )
import Pair( Pair(..) )
Gergő Érdi's avatar
Gergő Érdi committed
51 52 53

#include "HsVersions.h"

54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
{- *********************************************************************
*                                                                      *
        Type checking a pattern synonym signature
*                                                                      *
************************************************************************

Note [Pattern synonym signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Pattern synonym signatures are surprisingly tricky (see Trac #11224 for example).
In general they look like this:

   pattern P :: forall univ_tvs. req
             => forall ex_tvs. prov
             => arg1 -> .. -> argn -> body_ty

For parsing and renaming we treat the signature as an ordinary LHsSigType.

Once we get to type checking, we decompose it into its parts, in tcPatSynSig.

* Note that 'forall univ_tvs' and 'req =>'
        and 'forall ex_tvs'   and 'prov =>'
  are all optional.  We gather the pieces at the the top of tcPatSynSig

* Initially the implicitly-bound tyvars (added by the renamer) include both
  universal and existential vars.

* After we kind-check the pieces and convert to Types, we do kind generalisation.

* Note [Splitting the implicit tyvars in a pattern synonym]
  Now the tricky bit: we must split
     the implicitly-bound variables, and
     the kind-generalised variables
  into universal and existential.  We do so as follows:

     Note [The pattern-synonym signature splitting rule]
     the universals are the ones mentioned in
          - univ_tvs (and the kinds thereof)
Rik Steenkamp's avatar
Rik Steenkamp committed
91
          - req
92
          - body_ty
Rik Steenkamp's avatar
Rik Steenkamp committed
93
     the existentials are the rest
94 95 96 97 98 99 100 101 102 103 104 105 106 107

* Moreover see Note
-}

tcPatSynSig :: Name -> LHsSigType Name -> TcM TcPatSynInfo
tcPatSynSig name sig_ty
  | HsIB { hsib_vars = implicit_hs_tvs
         , hsib_body = hs_ty }  <- sig_ty
  , (univ_hs_tvs, hs_req,  hs_ty1) <- splitLHsSigmaTy hs_ty
  , (ex_hs_tvs,   hs_prov, hs_ty2) <- splitLHsSigmaTy hs_ty1
  , (hs_arg_tys, hs_body_ty)       <- splitHsFunType  hs_ty2
  = do { (implicit_tvs, (univ_tvs, req, ex_tvs, prov, arg_tys, body_ty))
           <- solveEqualities $
              tcImplicitTKBndrs implicit_hs_tvs $
108 109
              tcExplicitTKBndrs univ_hs_tvs  $ \ univ_tvs ->
              tcExplicitTKBndrs ex_hs_tvs    $ \ ex_tvs   ->
110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143
              do { req     <- tcHsContext hs_req
                 ; prov    <- tcHsContext hs_prov
                 ; arg_tys <- mapM tcHsOpenType (hs_arg_tys :: [LHsType Name])
                 ; body_ty <- tcHsLiftedType hs_body_ty
                 ; let bound_tvs
                         = unionVarSets [ allBoundVariabless req
                                        , allBoundVariabless prov
                                        , allBoundVariabless (body_ty : arg_tys)
                                        ]
                 ; return ( (univ_tvs, req, ex_tvs, prov, arg_tys, body_ty)
                          , bound_tvs) }

       -- These are /signatures/ so we zonk to squeeze out any kind
       -- unification variables.
       -- ToDo: checkValidType?
       ; implicit_tvs <- mapM zonkTcTyCoVarBndr implicit_tvs
       ; univ_tvs     <- mapM zonkTcTyCoVarBndr univ_tvs
       ; ex_tvs       <- mapM zonkTcTyCoVarBndr ex_tvs
       ; req          <- zonkTcTypes req
       ; prov         <- zonkTcTypes prov
       ; arg_tys      <- zonkTcTypes arg_tys
       ; body_ty      <- zonkTcType  body_ty

       -- Kind generalisation; c.f. kindGeneralise
       ; let free_kvs = tyCoVarsOfTelescope (implicit_tvs ++ univ_tvs ++ ex_tvs) $
                        tyCoVarsOfTypes (body_ty : req ++ prov ++ arg_tys)

       ; kvs <- quantifyTyVars emptyVarSet (Pair free_kvs emptyVarSet)

       -- Complain about:  pattern P :: () => forall x. x -> P x
       -- The renamer thought it was fine, but the existential 'x'
       -- should not appear in the result type
       ; let bad_tvs = filter (`elemVarSet` tyCoVarsOfType body_ty) ex_tvs
       ; unless (null bad_tvs) $ addErr $
144 145
         hang (text "The result type" <+> quotes (ppr body_ty))
            2 (text "mentions existential type variable" <> plural bad_tvs
146 147 148 149 150 151 152 153 154 155 156 157 158 159
               <+> pprQuotedList bad_tvs)

         -- Split [Splitting the implicit tyvars in a pattern synonym]
       ; let univ_fvs = closeOverKinds $
                        (tyCoVarsOfTypes (body_ty : req) `extendVarSetList` univ_tvs)
             (extra_univ, extra_ex) = partition (`elemVarSet` univ_fvs) $
                                      kvs ++ implicit_tvs
       ; traceTc "tcTySig }" $
         vcat [ text "implicit_tvs" <+> ppr implicit_tvs
              , text "kvs" <+> ppr kvs
              , text "extra_univ" <+> ppr extra_univ
              , text "univ_tvs" <+> ppr univ_tvs
              , text "req" <+> ppr req
              , text "extra_ex" <+> ppr extra_ex
Rik Steenkamp's avatar
Rik Steenkamp committed
160
              , text "ex_tvs" <+> ppr ex_tvs
161 162 163 164 165 166 167 168 169 170 171 172
              , text "prov" <+> ppr prov
              , text "arg_tys" <+> ppr arg_tys
              , text "body_ty" <+> ppr body_ty ]
       ; return (TPSI { patsig_name = name
                      , patsig_univ_tvs = extra_univ ++ univ_tvs
                      , patsig_req      = req
                      , patsig_ex_tvs   = extra_ex   ++ ex_tvs
                      , patsig_prov     = prov
                      , patsig_arg_tys  = arg_tys
                      , patsig_body_ty  = body_ty }) }


Austin Seipp's avatar
Austin Seipp committed
173 174 175
{-
************************************************************************
*                                                                      *
176
                    Type checking a pattern synonym
Austin Seipp's avatar
Austin Seipp committed
177 178 179
*                                                                      *
************************************************************************
-}
180

181
tcInferPatSynDecl :: PatSynBind Name Name
182
                  -> TcM (LHsBinds Id, TcGblEnv)
183
tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
184
                       psb_def = lpat, psb_dir = dir }
185
  = addPatSynCtxt lname $
186
    do { traceTc "tcInferPatSynDecl {" $ ppr name
187
       ; tcCheckPatSynPat lpat
Gergő Érdi's avatar
Gergő Érdi committed
188

Matthew Pickering's avatar
Matthew Pickering committed
189
       ; let (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
190
       ; (tclvl, wanted, ((lpat', args), pat_ty))
191
            <- pushLevelAndCaptureConstraints  $
192 193 194 195 196
               do { pat_ty <- newOpenInferExpType
                  ; stuff <- tcPat PatSyn lpat pat_ty $
                             mapM tcLookupId arg_names
                  ; pat_ty <- readExpType pat_ty
                  ; return (stuff, pat_ty) }
197 198

       ; let named_taus = (name, pat_ty) : map (\arg -> (getName arg, varType arg)) args
Gergő Érdi's avatar
Gergő Érdi committed
199

200
       ; (qtvs, req_dicts, ev_binds) <- simplifyInfer tclvl False [] named_taus wanted
Gergő Érdi's avatar
Gergő Érdi committed
201

202 203
       ; let (ex_vars, prov_dicts) = tcCollectEx lpat'
             univ_tvs   = filter (not . (`elemVarSet` ex_vars)) qtvs
204 205 206
             ex_tvs     = varSetElems ex_vars
             prov_theta = map evVarPred prov_dicts
             req_theta  = map evVarPred req_dicts
Gergő Érdi's avatar
Gergő Érdi committed
207

208
       ; traceTc "tcInferPatSynDecl }" $ ppr name
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
209
       ; tc_patsyn_finish lname dir False {- no sig -} is_infix lpat'
210 211 212
                          (univ_tvs, req_theta,  ev_binds, req_dicts)
                          (ex_tvs,   mkTyVarTys ex_tvs, prov_theta, map EvId prov_dicts)
                          (map nlHsVar args, map idType args)
Matthew Pickering's avatar
Matthew Pickering committed
213 214
                          pat_ty rec_fields }

215 216 217

tcCheckPatSynDecl :: PatSynBind Name Name
                  -> TcPatSynInfo
218
                  -> TcM (LHsBinds Id, TcGblEnv)
219 220 221 222 223 224 225
tcCheckPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details
                     , psb_def = lpat, psb_dir = dir }
                  TPSI{ patsig_univ_tvs = univ_tvs, patsig_prov = prov_theta
                      , patsig_ex_tvs   = ex_tvs,   patsig_req  = req_theta
                      , patsig_arg_tys  = arg_tys,  patsig_body_ty = pat_ty }
  = addPatSynCtxt lname $
    do { let origin     = PatOrigin -- TODO
226 227
             skol_info  = SigSkol (PatSynCtxt name) (mkCheckExpType $
                                                     mkFunTys arg_tys pat_ty)
228 229 230 231 232 233 234 235 236 237 238
             decl_arity = length arg_names
             ty_arity   = length arg_tys
             (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details

       ; traceTc "tcCheckPatSynDecl" $
         vcat [ ppr univ_tvs, ppr req_theta, ppr ex_tvs
              , ppr prov_theta, ppr arg_tys, ppr pat_ty ]

       ; checkTc (decl_arity == ty_arity)
                 (wrongNumberOfParmsErr name decl_arity ty_arity)

239 240
       ; tcCheckPatSynPat lpat

241 242
       -- Right!  Let's check the pattern against the signature
       -- See Note [Checking against a pattern signature]
243
       ; req_dicts <- newEvVars req_theta
244 245
       ; (tclvl, wanted, (lpat', (ex_tvs', prov_dicts, args'))) <-
           ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys )
246 247 248
           pushLevelAndCaptureConstraints            $
           tcExtendTyVarEnv univ_tvs                 $
           tcPat PatSyn lpat (mkCheckExpType pat_ty) $
249 250 251
           do { (subst, ex_tvs') <- if   isUnidirectional dir
                                    then newMetaTyVars    ex_tvs
                                    else newMetaSigTyVars ex_tvs
Rik Steenkamp's avatar
Rik Steenkamp committed
252
                    -- See the "Existential type variables" part of
253
                    -- Note [Checking against a pattern signature]
254 255 256 257 258 259 260
              ; prov_dicts <- mapM (emitWanted origin)
                  (substTheta (extendTCvInScopeList subst univ_tvs) prov_theta)
                  -- Add the free vars of 'prov_theta' to the in_scope set to
                  -- satisfy the substition invariant. There's no need to
                  -- add 'ex_tvs' as they are already in the domain of the
                  -- substitution.
                  -- See also Note [The substitution invariant] in TyCoRep.
261 262 263 264
              ; args'      <- zipWithM (tc_arg subst) arg_names arg_tys
              ; return (ex_tvs', prov_dicts, args') }

       ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info univ_tvs req_dicts wanted
265

266 267 268
       -- Solve the constraints now, because we are about to make a PatSyn,
       -- which should not contain unification variables and the like (Trac #10997)
       -- Since all the inputs are implications the returned bindings will be empty
269
       ; _ <- simplifyTop (mkImplicWC implics)
270 271 272 273

       -- ToDo: in the bidirectional case, check that the ex_tvs' are all distinct
       -- Otherwise we may get a type error when typechecking the builder,
       -- when that should be impossible
274

275
       ; traceTc "tcCheckPatSynDecl }" $ ppr name
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
276
       ; tc_patsyn_finish lname dir True {- has a sig -} is_infix lpat'
277 278 279
                          (univ_tvs, req_theta, ev_binds, req_dicts)
                          (ex_tvs, mkTyVarTys ex_tvs', prov_theta, prov_dicts)
                          (args', arg_tys)
280
                          pat_ty rec_fields }
281
  where
282 283 284 285 286 287 288
    tc_arg :: TCvSubst -> Name -> Type -> TcM (LHsExpr TcId)
    tc_arg subst arg_name arg_ty
      = do {   -- Look up the variable actually bound by lpat
               -- and check that it has the expected type
             arg_id <- tcLookupId arg_name
           ; coi <- unifyType (Just arg_id)
                              (idType arg_id)
289
                              (substTyUnchecked subst arg_ty)
290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306
           ; return (mkLHsWrapCo coi $ nlHsVar arg_id) }

{- Note [Checking against a pattern signature]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking the actual supplied pattern against the pattern synonym
signature, we need to be quite careful.

----- Provided constraints
Example

    data T a where
      MkT :: Ord a => a -> T a

    pattern P :: () => Eq a => a -> [T a]
    pattern P x = [MkT x]

We must check that the (Eq a) that P claims to bind (and to
Rik Steenkamp's avatar
Rik Steenkamp committed
307 308
make available to matches against P), is derivable from the
actual pattern.  For example:
309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339
    f (P (x::a)) = ...here (Eq a) should be available...
And yes, (Eq a) is derivable from the (Ord a) bound by P's rhs.

----- Existential type variables
Unusually, we instantiate the existential tyvars of the pattern with
*meta* type variables.  For example

    data S where
      MkS :: Eq a => [a] -> S

    pattern P :: () => Eq x => x -> S
    pattern P x <- MkS x

The pattern synonym conceals from its client the fact that MkS has a
list inside it.  The client just thinks it's a type 'x'.  So we must
unify x := [a] during type checking, and then use the instantiating type
[a] (called ex_tys) when building the matcher.  In this case we'll get

   $mP :: S -> (forall x. Ex x => x -> r) -> r -> r
   $mP x k = case x of
               MkS a (d:Eq a) (ys:[a]) -> let dl :: Eq [a]
                                              dl = $dfunEqList d
                                          in k [a] dl ys

This "concealing" story works for /uni-directional/ pattern synonmys,
but obviously not for bidirectional ones.  So in the bidirectional case
we use SigTv, rather than a generic TauTv, meta-tyvar so that.  And
we should really check that those SigTvs don't get unified with each
other.

-}
340

Matthew Pickering's avatar
Matthew Pickering committed
341 342 343 344 345 346 347 348 349 350 351 352 353 354 355
collectPatSynArgInfo :: HsPatSynDetails (Located Name) -> ([Name], [Name], Bool)
collectPatSynArgInfo details =
  case details of
    PrefixPatSyn names      -> (map unLoc names, [], False)
    InfixPatSyn name1 name2 -> (map unLoc [name1, name2], [], True)
    RecordPatSyn names ->
      let (vars, sels) = unzip (map splitRecordPatSyn names)
      in (vars, sels, False)

  where
    splitRecordPatSyn :: RecordPatSynField (Located Name) -> (Name, Name)
    splitRecordPatSyn (RecordPatSynField { recordPatSynPatVar = L _ patVar
                                         , recordPatSynSelectorId = L _ selId })
      = (patVar, selId)

356 357 358
addPatSynCtxt :: Located Name -> TcM a -> TcM a
addPatSynCtxt (L loc name) thing_inside
  = setSrcSpan loc $
359
    addErrCtxt (text "In the declaration for pattern synonym"
360 361 362 363 364
                <+> quotes (ppr name)) $
    thing_inside

wrongNumberOfParmsErr :: Name -> Arity -> Arity -> SDoc
wrongNumberOfParmsErr name decl_arity ty_arity
365
  = hang (text "Pattern synonym" <+> quotes (ppr name) <+> ptext (sLit "has")
366 367
          <+> speakNOf decl_arity (text "argument"))
       2 (text "but its type signature has" <+> speakN ty_arity)
368

369 370
-------------------------
-- Shared by both tcInferPatSyn and tcCheckPatSyn
Matthew Pickering's avatar
Matthew Pickering committed
371 372
tc_patsyn_finish :: Located Name  -- ^ PatSyn Name
                 -> HsPatSynDir Name  -- ^ PatSyn type (Uni/Bidir/ExplicitBidir)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
373
                 -> Bool              -- ^ True <=> signature provided
Matthew Pickering's avatar
Matthew Pickering committed
374 375
                 -> Bool              -- ^ Whether infix
                 -> LPat Id           -- ^ Pattern of the PatSyn
376
                 -> ([TcTyVar], [PredType], TcEvBinds, [EvVar])
377 378
                 -> ([TcTyVar], [TcType], [PredType], [EvTerm])
                 -> ([LHsExpr TcId], [TcType])   -- ^ Pattern arguments and types
Matthew Pickering's avatar
Matthew Pickering committed
379 380 381
                 -> TcType              -- ^ Pattern type
                 -> [Name]              -- ^ Selector names
                 -- ^ Whether fields, empty if not record PatSyn
382
                 -> TcM (LHsBinds Id, TcGblEnv)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
383
tc_patsyn_finish lname dir has_sig is_infix lpat'
384
                 (univ_tvs, req_theta, req_ev_binds, req_dicts)
385 386
                 (ex_tvs, ex_tys, prov_theta, prov_dicts)
                 (args, arg_tys)
Matthew Pickering's avatar
Matthew Pickering committed
387
                 pat_ty field_labels
388 389
  = do { -- Zonk everything.  We are about to build a final PatSyn
         -- so there had better be no unification variables in there
390 391 392 393
         univ_tvs     <- mapMaybeM zonkQuantifiedTyVar univ_tvs
       ; ex_tvs       <- mapMaybeM zonkQuantifiedTyVar ex_tvs
       ; prov_theta   <- zonkTcTypes prov_theta
       ; req_theta    <- zonkTcTypes req_theta
394
       ; pat_ty       <- zonkTcType pat_ty
395
       ; arg_tys      <- zonkTcTypes arg_tys
396

397
       ; traceTc "tc_patsyn_finish {" $
398 399
           ppr (unLoc lname) $$ ppr (unLoc lpat') $$
           ppr (univ_tvs, req_theta, req_ev_binds, req_dicts) $$
400 401 402
           ppr (ex_tvs, prov_theta, prov_dicts) $$
           ppr args $$
           ppr arg_tys $$
403
           ppr pat_ty
404 405

       -- Make the 'matcher'
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
406
       ; (matcher_id, matcher_bind) <- tcPatSynMatcher has_sig lname lpat'
407
                                         (univ_tvs, req_theta, req_ev_binds, req_dicts)
408 409
                                         (ex_tvs, ex_tys, prov_theta, prov_dicts)
                                         (args, arg_tys)
Gergő Érdi's avatar
Gergő Érdi committed
410
                                         pat_ty
411

Matthew Pickering's avatar
Matthew Pickering committed
412

413
       -- Make the 'builder'
414 415 416
       ; builder_id <- mkPatSynBuilderId has_sig dir lname
                                         univ_tvs req_theta
                                         ex_tvs   prov_theta
Matthew Pickering's avatar
Matthew Pickering committed
417
                                         arg_tys pat_ty
Matthew Pickering's avatar
Matthew Pickering committed
418 419 420 421 422

         -- TODO: Make this have the proper information
       ; let mkFieldLabel name = FieldLabel (occNameFS (nameOccName name)) False name
             field_labels' = (map mkFieldLabel field_labels)

Gergő Érdi's avatar
Gergő Érdi committed
423

424
       -- Make the PatSyn itself
Matthew Pickering's avatar
Matthew Pickering committed
425
       ; let patSyn = mkPatSyn (unLoc lname) is_infix
426 427
                        (univ_tvs, req_theta)
                        (ex_tvs, prov_theta)
428
                        arg_tys
Gergő Érdi's avatar
Gergő Érdi committed
429
                        pat_ty
430
                        matcher_id builder_id
Matthew Pickering's avatar
Matthew Pickering committed
431 432 433 434 435 436 437 438 439 440 441
                        field_labels'

       -- Selectors
       ; let (sigs, selector_binds) =
                unzip (mkPatSynRecSelBinds patSyn (patSynFieldLabels patSyn))
       ; let tything = AConLike (PatSynCon patSyn)
       ; tcg_env <-
          tcExtendGlobalEnv [tything] $
            tcRecSelBinds
              (ValBindsOut (zip (repeat NonRecursive) selector_binds) sigs)

442
       ; traceTc "tc_patsyn_finish }" empty
443
       ; return (matcher_bind, tcg_env) }
444

Austin Seipp's avatar
Austin Seipp committed
445 446 447
{-
************************************************************************
*                                                                      *
448
         Constructing the "matcher" Id and its binding
Austin Seipp's avatar
Austin Seipp committed
449 450 451
*                                                                      *
************************************************************************
-}
452

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
453 454
tcPatSynMatcher :: Bool  -- True <=> signature provided
                -> Located Name
Gergő Érdi's avatar
Gergő Érdi committed
455
                -> LPat Id
456
                -> ([TcTyVar], ThetaType, TcEvBinds, [EvVar])
457 458
                -> ([TcTyVar], [TcType], ThetaType, [EvTerm])
                -> ([LHsExpr TcId], [TcType])
Gergő Érdi's avatar
Gergő Érdi committed
459
                -> TcType
460 461
                -> TcM ((Id, Bool), LHsBinds Id)
-- See Note [Matchers and builders for pattern synonyms] in PatSyn
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
462
tcPatSynMatcher has_sig (L loc name) lpat
463
                (univ_tvs, req_theta, req_ev_binds, req_dicts)
464 465
                (ex_tvs, ex_tys, prov_theta, prov_dicts)
                (args, arg_tys) pat_ty
466 467 468 469 470 471 472
  = do { lev_uniq <- newUnique
       ; tv_uniq  <- newUnique
       ; let lev_name = mkInternalName lev_uniq (mkTyVarOcc "rlev") loc
             tv_name  = mkInternalName tv_uniq (mkTyVarOcc "r") loc
             lev_tv   = mkTcTyVar lev_name levityTy   (SkolemTv False)
             lev      = mkTyVarTy lev_tv
             res_tv   = mkTcTyVar tv_name  (tYPE lev) (SkolemTv False)
473
             is_unlifted = null args && null prov_dicts
474
             res_ty = mkTyVarTy res_tv
475 476 477
             (cont_args, cont_arg_tys)
               | is_unlifted = ([nlHsVar voidPrimId], [voidPrimTy])
               | otherwise   = (args,                 arg_tys)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
478 479
             mk_sigma = if has_sig then mkSpecSigmaTy else mkInvSigmaTy
             cont_ty = mk_sigma ex_tvs prov_theta $
480 481
                       mkFunTys cont_arg_tys res_ty

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
482
             fail_ty  = mkFunTy voidPrimTy res_ty
483

484
       ; matcher_name <- newImplicitBinder name mkMatcherOcc
485 486 487 488 489
       ; scrutinee    <- newSysLocalId (fsLit "scrut") pat_ty
       ; cont         <- newSysLocalId (fsLit "cont")  cont_ty
       ; fail         <- newSysLocalId (fsLit "fail")  fail_ty

       ; let matcher_tau   = mkFunTys [pat_ty, cont_ty, fail_ty] res_ty
490
             matcher_sigma = mkInvSigmaTy (lev_tv:res_tv:univ_tvs) req_theta matcher_tau
491
             matcher_id    = mkExportedVanillaId matcher_name matcher_sigma
492
                             -- See Note [Exported LocalIds] in Id
493

494 495
             inst_wrap = mkWpEvApps prov_dicts <.> mkWpTyApps ex_tys
             cont' = foldl nlHsApp (mkLHsWrap inst_wrap (nlHsVar cont)) cont_args
Gergő Érdi's avatar
Gergő Érdi committed
496

497
             fail' = nlHsApps fail [nlHsVar voidPrimId]
Gergő Érdi's avatar
Gergő Érdi committed
498

499
             args = map nlVarPat [scrutinee, cont, fail]
Gergő Érdi's avatar
Gergő Érdi committed
500 501 502 503 504
             lwpat = noLoc $ WildPat pat_ty
             cases = if isIrrefutableHsPat lpat
                     then [mkSimpleHsAlt lpat  cont']
                     else [mkSimpleHsAlt lpat  cont',
                           mkSimpleHsAlt lwpat fail']
505
             body = mkLHsWrap (mkWpLet req_ev_binds) $
Gergő Érdi's avatar
Gergő Érdi committed
506 507
                    L (getLoc lpat) $
                    HsCase (nlHsVar scrutinee) $
508
                    MG{ mg_alts = L (getLoc lpat) cases
Gergő Érdi's avatar
Gergő Érdi committed
509 510
                      , mg_arg_tys = [pat_ty]
                      , mg_res_ty = res_ty
511
                      , mg_origin = Generated
Gergő Érdi's avatar
Gergő Érdi committed
512 513 514
                      }
             body' = noLoc $
                     HsLam $
515
                     MG{ mg_alts = noLoc [mkSimpleMatch args body]
Gergő Érdi's avatar
Gergő Érdi committed
516 517
                       , mg_arg_tys = [pat_ty, cont_ty, res_ty]
                       , mg_res_ty = res_ty
518
                       , mg_origin = Generated
Gergő Érdi's avatar
Gergő Érdi committed
519
                       }
520
             match = mkMatch [] (mkHsLams (lev_tv:res_tv:univ_tvs) req_dicts body')
521 522
                             (noLoc EmptyLocalBinds)
             mg = MG{ mg_alts = L (getLoc match) [match]
Gergő Érdi's avatar
Gergő Érdi committed
523 524
                    , mg_arg_tys = []
                    , mg_res_ty = res_ty
525
                    , mg_origin = Generated
Gergő Érdi's avatar
Gergő Érdi committed
526 527
                    }

528
       ; let bind = FunBind{ fun_id = L loc matcher_id
Gergő Érdi's avatar
Gergő Érdi committed
529 530 531
                           , fun_matches = mg
                           , fun_co_fn = idHsWrapper
                           , bind_fvs = emptyNameSet
532
                           , fun_tick = [] }
533
             matcher_bind = unitBag (noLoc bind)
Gergő Érdi's avatar
Gergő Érdi committed
534

535
       ; traceTc "tcPatSynMatcher" (ppr name $$ ppr (idType matcher_id))
Gergő Érdi's avatar
Gergő Érdi committed
536 537
       ; traceTc "tcPatSynMatcher" (ppr matcher_bind)

538 539
       ; return ((matcher_id, is_unlifted), matcher_bind) }

Matthew Pickering's avatar
Matthew Pickering committed
540 541 542 543
mkPatSynRecSelBinds :: PatSyn
                    -> [FieldLabel]
                    -- ^ Visible field labels
                    -> [(LSig Name, LHsBinds Name)]
544 545 546 547 548
mkPatSynRecSelBinds ps fields = map mkRecSel fields
  where
    mkRecSel fld_lbl =
      case mkOneRecordSelector [PatSynCon ps] (RecSelPatSyn ps) fld_lbl of
        (name, (_rec_flag, binds)) -> (name, binds)
549 550 551 552 553 554

isUnidirectional :: HsPatSynDir a -> Bool
isUnidirectional Unidirectional          = True
isUnidirectional ImplicitBidirectional   = False
isUnidirectional ExplicitBidirectional{} = False

Austin Seipp's avatar
Austin Seipp committed
555 556 557
{-
************************************************************************
*                                                                      *
558
         Constructing the "builder" Id
Austin Seipp's avatar
Austin Seipp committed
559 560 561
*                                                                      *
************************************************************************
-}
562

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
563 564
mkPatSynBuilderId :: Bool  -- True <=> signature provided
                  -> HsPatSynDir a -> Located Name
565 566 567
                  -> [TyVar] -> ThetaType
                  -> [TyVar] -> ThetaType
                  -> [Type] -> Type
568
                  -> TcM (Maybe (Id, Bool))
569 570 571
mkPatSynBuilderId has_sig dir (L _ name)
                  univ_tvs req_theta ex_tvs prov_theta
                  arg_tys pat_ty
572 573 574
  | isUnidirectional dir
  = return Nothing
  | otherwise
575
  = do { builder_name <- newImplicitBinder name mkBuilderOcc
576 577 578
       ; let qtvs           = univ_tvs ++ ex_tvs
             theta          = req_theta ++ prov_theta
             mk_sigma       = if has_sig then mkSpecSigmaTy else mkInvSigmaTy
579
             need_dummy_arg = isUnliftedType pat_ty && null arg_tys && null theta
580 581 582
             builder_sigma  = add_void need_dummy_arg $
                              mk_sigma qtvs theta (mkFunTys arg_tys pat_ty)
             builder_id     = mkExportedVanillaId builder_name builder_sigma
Matthew Pickering's avatar
Matthew Pickering committed
583
              -- See Note [Exported LocalIds] in Id
584

585
       ; return (Just (builder_id, need_dummy_arg)) }
586
  where
587

588 589 590 591 592 593 594
add_void :: Bool -> Type -> Type
add_void need_dummy_arg ty
  | need_dummy_arg = mkFunTy voidPrimTy ty
  | otherwise      = ty

tcPatSynBuilderBind :: TcSigFun
                    -> PatSynBind Name Name
595 596
                    -> TcM (LHsBinds Id)
-- See Note [Matchers and builders for pattern synonyms] in PatSyn
597 598
tcPatSynBuilderBind sig_fun PSB{ psb_id = L loc name, psb_def = lpat
                               , psb_dir = dir, psb_args = details }
599 600 601 602 603
  | isUnidirectional dir
  = return emptyBag

  | isNothing mb_match_group       -- Can't invert the pattern
  = setSrcSpan (getLoc lpat) $ failWithTc $
604
    hang (text "Right-hand side of bidirectional pattern synonym cannot be used as an expression")
605 606
       2 (ppr lpat)

607
  | otherwise  -- Bidirectional
608
  = do { patsyn <- tcLookupPatSyn name
609
       ; traceTc "tcPatSynBuilderBind {" $ ppr patsyn
610
       ; let Just (builder_id, need_dummy_arg) = patSynBuilder patsyn
611 612 613 614 615
                   -- Bidirectional, so patSynBuilder returns Just

             match_group' | need_dummy_arg = add_dummy_arg match_group
                          | otherwise      = match_group

616
             bind = FunBind { fun_id      = L loc (idName builder_id)
617 618 619 620 621
                            , fun_matches = match_group'
                            , fun_co_fn   = idHsWrapper
                            , bind_fvs    = placeHolderNamesTc
                            , fun_tick    = [] }

622
       ; sig <- get_builder_sig sig_fun name builder_id need_dummy_arg
623

624
       ; (builder_binds, _) <- tcPolyCheck NonRecursive emptyPragEnv sig (noLoc bind)
625 626
       ; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds
       ; return builder_binds }
627
  where
628
    Just match_group = mb_match_group
629
    mb_match_group
630 631 632 633
       = case dir of
           Unidirectional                    -> Nothing
           ExplicitBidirectional explicit_mg -> Just explicit_mg
           ImplicitBidirectional             -> fmap mk_mg (tcPatToExpr args lpat)
634 635

    mk_mg :: LHsExpr Name -> MatchGroup Name (LHsExpr Name)
636
    mk_mg body = mkMatchGroupName Generated [builder_match]
637
             where
638
               builder_args  = [L loc (VarPat (L loc n)) | L loc n <- args]
639
               builder_match = mkMatch builder_args body (noLoc EmptyLocalBinds)
640 641

    args = case details of
642
              PrefixPatSyn args     -> args
643
              InfixPatSyn arg1 arg2 -> [arg1, arg2]
Matthew Pickering's avatar
Matthew Pickering committed
644
              RecordPatSyn args     -> map recordPatSynPatVar args
645

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
646 647
    add_dummy_arg :: MatchGroup Name (LHsExpr Name)
                  -> MatchGroup Name (LHsExpr Name)
648 649 650 651
    add_dummy_arg mg@(MG { mg_alts
                            = L l [L loc (Match NonFunBindMatch [] ty grhss)] })
      = mg { mg_alts
                = L l [L loc (Match NonFunBindMatch [nlWildPatName] ty grhss)] }
652 653 654
    add_dummy_arg other_mg = pprPanic "add_dummy_arg" $
                             pprMatches (PatSyn :: HsMatchContext Name) other_mg

655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681
get_builder_sig :: TcSigFun -> Name -> Id -> Bool -> TcM TcIdSigInfo
get_builder_sig sig_fun name builder_id need_dummy_arg
  | Just (TcPatSynSig sig) <- sig_fun name
  , TPSI { patsig_univ_tvs = univ_tvs
         , patsig_req      = req
         , patsig_ex_tvs   = ex_tvs
         , patsig_prov     = prov
         , patsig_arg_tys  = arg_tys
         , patsig_body_ty  = body_ty } <- sig
  = -- Constuct a TcIdSigInfo from a TcPatSynInfo
    -- This does unfortunately mean that we have to know how to
    -- make the builder Id's type from the TcPatSynInfo, which
    -- duplicates the construction in mkPatSynBuilderId
    -- But we really want to use the scoped type variables from
    -- the actual sigature, so this is really the Right Thing
    return (TISI { sig_bndr  = CompleteSig builder_id
                 , sig_skols = [(tyVarName tv, tv) | tv <- univ_tvs ++ ex_tvs]
                 , sig_theta = req ++ prov
                 , sig_tau   = add_void need_dummy_arg $
                               mkFunTys arg_tys body_ty
                 , sig_ctxt  = PatSynCtxt name
                 , sig_loc   = getSrcSpan name })
  | otherwise
  = -- No signature, so fake up a TcIdSigInfo from the builder Id
    instTcTySigFromId builder_id
    -- See Note [Redundant constraints for builder]

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
682 683 684
tcPatSynBuilderOcc :: PatSyn -> TcM (HsExpr TcId, TcSigmaType)
-- monadic only for failure
tcPatSynBuilderOcc ps
685
  | Just (builder_id, add_void_arg) <- builder
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
686 687 688 689 690 691 692
  , let builder_expr = HsVar (noLoc builder_id)
        builder_ty   = idType builder_id
  = return $
    if add_void_arg
    then ( HsApp (noLoc $ builder_expr) (nlHsVar voidPrimId)
         , tcFunResultTy builder_ty )
    else (builder_expr, builder_ty)
693 694

  | otherwise  -- Unidirectional
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
695
  = nonBidirectionalErr name
696 697 698
  where
    name    = patSynName ps
    builder = patSynBuilder ps
Gergő Érdi's avatar
Gergő Érdi committed
699

Austin Seipp's avatar
Austin Seipp committed
700
{-
701 702 703 704 705 706
Note [Redundant constraints for builder]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The builder can have redundant constraints, which are awkard to eliminate.
Consider
   pattern P = Just 34
To match against this pattern we need (Eq a, Num a).  But to build
707 708
(Just 34) we need only (Num a).  Fortunately instTcSigFromId sets
sig_warn_redundant to False.
709

Austin Seipp's avatar
Austin Seipp committed
710 711
************************************************************************
*                                                                      *
712
         Helper functions
Austin Seipp's avatar
Austin Seipp committed
713 714
*                                                                      *
************************************************************************
715

716 717
Note [As-patterns in pattern synonym definitions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
718 719 720
The rationale for rejecting as-patterns in pattern synonym definitions
is that an as-pattern would introduce nonindependent pattern synonym
arguments, e.g. given a pattern synonym like:
721 722 723 724 725 726

        pattern K x y = x@(Just y)

one could write a nonsensical function like

        f (K Nothing x) = ...
Gergő Érdi's avatar
Gergő Érdi committed
727

728 729
or
        g (K (Just True) False) = ...
730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749

Note [Type signatures and the builder expression]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
   pattern L x = Left x :: Either [a] [b]

In tc{Infer/Check}PatSynDecl we will check that the pattern has the
specified type.  We check the pattern *as a pattern*, so the type
signature is a pattern signature, and so brings 'a' and 'b' into
scope.  But we don't have a way to bind 'a, b' in the LHS, as we do
'x', say.  Nevertheless, the sigature may be useful to constrain
the type.

When making the binding for the *builder*, though, we don't want
  $buildL x = Left x :: Either [a] [b]
because that wil either mean (forall a b. Either [a] [b]), or we'll
get a complaint that 'a' and 'b' are out of scope. (Actually the
latter; Trac #9867.)  No, the job of the signature is done, so when
converting the pattern to an expression (for the builder RHS) we
simply discard the signature.
Matthew Pickering's avatar
Matthew Pickering committed
750 751 752 753 754 755 756 757

Note [Record PatSyn Desugaring]
-------------------------------
It is important that prov_theta comes before req_theta as this ordering is used
when desugaring record pattern synonym updates.

Any change to this ordering should make sure to change deSugar/DsExpr.hs if you
want to avoid difficult to decipher core lint errors!
758
 -}
759

760 761 762 763 764 765 766 767 768 769
tcCheckPatSynPat :: LPat Name -> TcM ()
tcCheckPatSynPat = go
  where
    go :: LPat Name -> TcM ()
    go = addLocM go1

    go1 :: Pat Name -> TcM ()
    go1   (ConPatIn _ info)   = mapM_ go (hsConPatArgs info)
    go1   VarPat{}            = return ()
    go1   WildPat{}           = return ()
770
    go1 p@(AsPat _ _)         = asPatInPatSynErr p
771 772 773 774 775 776
    go1   (LazyPat pat)       = go pat
    go1   (ParPat pat)        = go pat
    go1   (BangPat pat)       = go pat
    go1   (PArrPat pats _)    = mapM_ go pats
    go1   (ListPat pats _ _)  = mapM_ go pats
    go1   (TuplePat pats _ _) = mapM_ go pats
777 778
    go1   LitPat{}            = return ()
    go1   NPat{}              = return ()
779 780 781 782 783 784 785 786 787 788 789
    go1   (SigPatIn pat _)    = go pat
    go1   (ViewPat _ pat _)   = go pat
    go1 p@SplicePat{}         = thInPatSynErr p
    go1 p@NPlusKPat{}         = nPlusKPatInPatSynErr p
    go1   ConPatOut{}         = panic "ConPatOut in output of renamer"
    go1   SigPatOut{}         = panic "SigPatOut in output of renamer"
    go1   CoPat{}             = panic "CoPat in output of renamer"

asPatInPatSynErr :: OutputableBndr name => Pat name -> TcM a
asPatInPatSynErr pat
  = failWithTc $
790
    hang (text "Pattern synonym definition cannot contain as-patterns (@):")
791 792 793 794 795
       2 (ppr pat)

thInPatSynErr :: OutputableBndr name => Pat name -> TcM a
thInPatSynErr pat
  = failWithTc $
796
    hang (text "Pattern synonym definition cannot contain Template Haskell:")
797 798 799 800 801
       2 (ppr pat)

nPlusKPatInPatSynErr :: OutputableBndr name => Pat name -> TcM a
nPlusKPatInPatSynErr pat
  = failWithTc $
802
    hang (text "Pattern synonym definition cannot contain n+k-pattern:")
803 804
       2 (ppr pat)

Matthew Pickering's avatar
Matthew Pickering committed
805 806
nonBidirectionalErr :: Outputable name => name -> TcM a
nonBidirectionalErr name = failWithTc $
807 808
    text "non-bidirectional pattern synonym"
    <+> quotes (ppr name) <+> text "used in an expression"
Matthew Pickering's avatar
Matthew Pickering committed
809

810 811
tcPatToExpr :: [Located Name] -> LPat Name -> Maybe (LHsExpr Name)
tcPatToExpr args = go
Gergő Érdi's avatar
Gergő Érdi committed
812
  where
813 814
    lhsVars = mkNameSet (map unLoc args)

815
    go :: LPat Name -> Maybe (LHsExpr Name)
816 817 818
    go (L loc (ConPatIn (L _ con) info))
      = do { exprs <- mapM go (hsConPatArgs info)
           ; return $ L loc $
819
             foldl (\x y -> HsApp (L loc x) y) (HsVar (L loc con)) exprs }
820 821 822 823

    go (L _ (SigPatIn pat _)) = go pat
        -- See Note [Type signatures and the builder expression]

824
    go (L loc p) = fmap (L loc) $ go1 p
Gergő Érdi's avatar
Gergő Érdi committed
825

826
    go1 :: Pat Name -> Maybe (HsExpr Name)
827 828
    go1   (VarPat (L l var))
      | var `elemNameSet` lhsVars     = return $ HsVar (L l var)
829 830 831 832 833 834 835 836 837 838 839 840
      | otherwise                     = Nothing
    go1   (LazyPat pat)               = fmap HsPar $ go pat
    go1   (ParPat pat)                = fmap HsPar $ go pat
    go1   (BangPat pat)               = fmap HsPar $ go pat
    go1   (PArrPat pats ptt)          = do { exprs <- mapM go pats
                                           ; return $ ExplicitPArr ptt exprs }
    go1   (ListPat pats ptt reb)      = do { exprs <- mapM go pats
                                           ; return $ ExplicitList ptt (fmap snd reb) exprs }
    go1   (TuplePat pats box _)       = do { exprs <- mapM go pats
                                           ; return $ ExplicitTuple
                                                (map (noLoc . Present) exprs) box }
    go1   (LitPat lit)                = return $ HsLit lit
841 842
    go1   (NPat (L _ n) Nothing _ _)  = return $ HsOverLit n
    go1   (NPat (L _ n) (Just neg) _ _)= return $ unLoc $ nlHsSyntaxApps neg [noLoc (HsOverLit n)]
843 844 845 846
    go1   (ConPatOut{})               = panic "ConPatOut in output of renamer"
    go1   (SigPatOut{})               = panic "SigPatOut in output of renamer"
    go1   (CoPat{})                   = panic "CoPat in output of renamer"
    go1   _                           = Nothing
Gergő Érdi's avatar
Gergő Érdi committed
847

848 849 850 851 852 853
-- Walk the whole pattern and for all ConPatOuts, collect the
-- existentially-bound type variables and evidence binding variables.
--
-- These are used in computing the type of a pattern synonym and also
-- in generating matcher functions, since success continuations need
-- to be passed these pattern-bound evidences.
854 855
tcCollectEx :: LPat Id -> (TyVarSet, [EvVar])
tcCollectEx pat = go pat
Gergő Érdi's avatar
Gergő Érdi committed
856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872
  where
    go :: LPat Id -> (TyVarSet, [EvVar])
    go = go1 . unLoc

    go1 :: Pat Id -> (TyVarSet, [EvVar])
    go1 (LazyPat p)         = go p
    go1 (AsPat _ p)         = go p
    go1 (ParPat p)          = go p
    go1 (BangPat p)         = go p
    go1 (ListPat ps _ _)    = mconcat . map go $ ps
    go1 (TuplePat ps _ _)   = mconcat . map go $ ps
    go1 (PArrPat ps _)      = mconcat . map go $ ps
    go1 (ViewPat _ p _)     = go p
    go1 con@ConPatOut{}     = mappend (mkVarSet (pat_tvs con), pat_dicts con) $
                                 goConDetails $ pat_args con
    go1 (SigPatOut p _)     = go p
    go1 (CoPat _ p _)       = go1 p
873
    go1 (NPlusKPat n k _ geq subtract _)
Gergő Érdi's avatar
Gergő Érdi committed
874 875 876 877 878 879 880 881 882
      = pprPanic "TODO: NPlusKPat" $ ppr n $$ ppr k $$ ppr geq $$ ppr subtract
    go1 _                   = mempty

    goConDetails :: HsConPatDetails Id -> (TyVarSet, [EvVar])
    goConDetails (PrefixCon ps) = mconcat . map go $ ps
    goConDetails (InfixCon p1 p2) = go p1 `mappend` go p2
    goConDetails (RecCon HsRecFields{ rec_flds = flds })
      = mconcat . map goRecFd $ flds

883 884
    goRecFd :: LHsRecField Id (LPat Id) -> (TyVarSet, [EvVar])
    goRecFd (L _ HsRecField{ hsRecFieldArg = p }) = go p