TcPatSyn.hs 36.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, 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 17
import TcHsType( tcImplicitTKBndrs, tcHsTyVarBndrs
               , 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 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 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
{- *********************************************************************
*                                                                      *
        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)
          - prov
          - body_ty
     the existential are the rest

* 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 $
              tcHsTyVarBndrs univ_hs_tvs  $ \ univ_tvs ->
              tcHsTyVarBndrs ex_hs_tvs    $ \ ex_tvs   ->
              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 160 161 162 163 164 165 166 167 168 169 170 171 172
               <+> 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
              , text "ex_tvs_" <+> ppr ex_tvs
              , 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
               do { pat_ty <- newOpenFlexiTyVarTy
193 194 195 196 197
                  ; tcPat PatSyn lpat pat_ty $
               do { args <- mapM tcLookupId arg_names
                  ; return (args, pat_ty) } }

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

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

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

207
       ; traceTc "tcInferPatSynDecl }" $ ppr name
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
208
       ; tc_patsyn_finish lname dir False {- no sig -} is_infix lpat'
209 210 211
                          (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
212 213
                          pat_ty rec_fields }

214 215 216

tcCheckPatSynDecl :: PatSynBind Name Name
                  -> TcPatSynInfo
217
                  -> TcM (LHsBinds Id, TcGblEnv)
218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236
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
             skol_info  = SigSkol (PatSynCtxt name) (mkFunTys arg_tys pat_ty)
             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)

237 238
       ; tcCheckPatSynPat lpat

239 240
       -- Right!  Let's check the pattern against the signature
       -- See Note [Checking against a pattern signature]
241
       ; req_dicts <- newEvVars req_theta
242 243 244
       ; (tclvl, wanted, (lpat', (ex_tvs', prov_dicts, args'))) <-
           ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys )
           pushLevelAndCaptureConstraints $
245
           tcExtendTyVarEnv univ_tvs      $
246 247 248 249 250 251 252 253 254 255 256
           tcPat PatSyn lpat pat_ty $
           do { (subst, ex_tvs') <- if   isUnidirectional dir
                                    then newMetaTyVars    ex_tvs
                                    else newMetaSigTyVars ex_tvs
                    -- See the "Existential type variables part of
                    -- Note [Checking against a pattern signature]
              ; prov_dicts <- mapM (emitWanted origin) (substTheta subst prov_theta)
              ; 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
257

258 259 260
       -- 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
261
       ; _ <- simplifyTop (mkImplicWC implics)
262 263 264 265

       -- 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
266

267
       ; traceTc "tcCheckPatSynDecl }" $ ppr name
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
268
       ; tc_patsyn_finish lname dir True {- has a sig -} is_infix lpat'
269 270 271
                          (univ_tvs, req_theta, ev_binds, req_dicts)
                          (ex_tvs, mkTyVarTys ex_tvs', prov_theta, prov_dicts)
                          (args', arg_tys)
272
                          pat_ty rec_fields }
273
  where
274 275 276 277 278 279 280
    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)
281
                              (substTyUnchecked subst arg_ty)
282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331
           ; 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
make available to matches against P, is derivable from the
acutal pattern.  For example:
    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.

-}
332

Matthew Pickering's avatar
Matthew Pickering committed
333 334 335 336 337 338 339 340 341 342 343 344 345 346 347
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)

348 349 350
addPatSynCtxt :: Located Name -> TcM a -> TcM a
addPatSynCtxt (L loc name) thing_inside
  = setSrcSpan loc $
351
    addErrCtxt (text "In the declaration for pattern synonym"
352 353 354 355 356
                <+> quotes (ppr name)) $
    thing_inside

wrongNumberOfParmsErr :: Name -> Arity -> Arity -> SDoc
wrongNumberOfParmsErr name decl_arity ty_arity
357 358 359
  = hang (text "Patten synonym" <+> quotes (ppr name) <+> ptext (sLit "has")
          <+> speakNOf decl_arity (text "argument"))
       2 (text "but its type signature has" <+> speakN ty_arity)
360

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

389
       ; traceTc "tc_patsyn_finish {" $
390 391
           ppr (unLoc lname) $$ ppr (unLoc lpat') $$
           ppr (univ_tvs, req_theta, req_ev_binds, req_dicts) $$
392 393 394
           ppr (ex_tvs, prov_theta, prov_dicts) $$
           ppr args $$
           ppr arg_tys $$
395
           ppr pat_ty
396 397

       -- Make the 'matcher'
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
398
       ; (matcher_id, matcher_bind) <- tcPatSynMatcher has_sig lname lpat'
399
                                         (univ_tvs, req_theta, req_ev_binds, req_dicts)
400 401
                                         (ex_tvs, ex_tys, prov_theta, prov_dicts)
                                         (args, arg_tys)
Gergő Érdi's avatar
Gergő Érdi committed
402
                                         pat_ty
403

Matthew Pickering's avatar
Matthew Pickering committed
404

405
       -- Make the 'builder'
406 407 408
       ; builder_id <- mkPatSynBuilderId has_sig dir lname
                                         univ_tvs req_theta
                                         ex_tvs   prov_theta
Matthew Pickering's avatar
Matthew Pickering committed
409
                                         arg_tys pat_ty
Matthew Pickering's avatar
Matthew Pickering committed
410 411 412 413 414

         -- 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
415

416
       -- Make the PatSyn itself
Matthew Pickering's avatar
Matthew Pickering committed
417
       ; let patSyn = mkPatSyn (unLoc lname) is_infix
418 419
                        (univ_tvs, req_theta)
                        (ex_tvs, prov_theta)
420
                        arg_tys
Gergő Érdi's avatar
Gergő Érdi committed
421
                        pat_ty
422
                        matcher_id builder_id
Matthew Pickering's avatar
Matthew Pickering committed
423 424 425 426 427 428 429 430 431 432 433
                        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)

434
       ; traceTc "tc_patsyn_finish }" empty
435
       ; return (matcher_bind, tcg_env) }
436

Austin Seipp's avatar
Austin Seipp committed
437 438 439
{-
************************************************************************
*                                                                      *
440
         Constructing the "matcher" Id and its binding
Austin Seipp's avatar
Austin Seipp committed
441 442 443
*                                                                      *
************************************************************************
-}
444

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
445 446
tcPatSynMatcher :: Bool  -- True <=> signature provided
                -> Located Name
Gergő Érdi's avatar
Gergő Érdi committed
447
                -> LPat Id
448
                -> ([TcTyVar], ThetaType, TcEvBinds, [EvVar])
449 450
                -> ([TcTyVar], [TcType], ThetaType, [EvTerm])
                -> ([LHsExpr TcId], [TcType])
Gergő Érdi's avatar
Gergő Érdi committed
451
                -> TcType
452 453
                -> 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
454
tcPatSynMatcher has_sig (L loc name) lpat
455
                (univ_tvs, req_theta, req_ev_binds, req_dicts)
456 457
                (ex_tvs, ex_tys, prov_theta, prov_dicts)
                (args, arg_tys) pat_ty
458 459 460 461 462 463 464
  = 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)
465
             is_unlifted = null args && null prov_dicts
466
             res_ty = mkTyVarTy res_tv
467 468 469
             (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
470 471
             mk_sigma = if has_sig then mkSpecSigmaTy else mkInvSigmaTy
             cont_ty = mk_sigma ex_tvs prov_theta $
472 473
                       mkFunTys cont_arg_tys res_ty

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
474
             fail_ty  = mkFunTy voidPrimTy res_ty
475

476
       ; matcher_name <- newImplicitBinder name mkMatcherOcc
477 478 479 480 481
       ; 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
482
             matcher_sigma = mkInvSigmaTy (lev_tv:res_tv:univ_tvs) req_theta matcher_tau
483
             matcher_id    = mkExportedVanillaId matcher_name matcher_sigma
484
                             -- See Note [Exported LocalIds] in Id
485

486 487
             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
488

489
             fail' = nlHsApps fail [nlHsVar voidPrimId]
Gergő Érdi's avatar
Gergő Érdi committed
490

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

520
       ; let bind = FunBind{ fun_id = L loc matcher_id
Gergő Érdi's avatar
Gergő Érdi committed
521 522 523
                           , fun_matches = mg
                           , fun_co_fn = idHsWrapper
                           , bind_fvs = emptyNameSet
524
                           , fun_tick = [] }
525
             matcher_bind = unitBag (noLoc bind)
Gergő Érdi's avatar
Gergő Érdi committed
526

527
       ; traceTc "tcPatSynMatcher" (ppr name $$ ppr (idType matcher_id))
Gergő Érdi's avatar
Gergő Érdi committed
528 529
       ; traceTc "tcPatSynMatcher" (ppr matcher_bind)

530 531
       ; return ((matcher_id, is_unlifted), matcher_bind) }

Matthew Pickering's avatar
Matthew Pickering committed
532 533 534 535
mkPatSynRecSelBinds :: PatSyn
                    -> [FieldLabel]
                    -- ^ Visible field labels
                    -> [(LSig Name, LHsBinds Name)]
536 537 538 539 540
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)
541 542 543 544 545 546

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

Austin Seipp's avatar
Austin Seipp committed
547 548 549
{-
************************************************************************
*                                                                      *
550
         Constructing the "builder" Id
Austin Seipp's avatar
Austin Seipp committed
551 552 553
*                                                                      *
************************************************************************
-}
554

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
555 556
mkPatSynBuilderId :: Bool  -- True <=> signature provided
                  -> HsPatSynDir a -> Located Name
557 558 559
                  -> [TyVar] -> ThetaType
                  -> [TyVar] -> ThetaType
                  -> [Type] -> Type
560
                  -> TcM (Maybe (Id, Bool))
561 562 563
mkPatSynBuilderId has_sig dir (L _ name)
                  univ_tvs req_theta ex_tvs prov_theta
                  arg_tys pat_ty
564 565 566
  | isUnidirectional dir
  = return Nothing
  | otherwise
567
  = do { builder_name <- newImplicitBinder name mkBuilderOcc
568 569 570 571 572 573 574
       ; let qtvs           = univ_tvs ++ ex_tvs
             theta          = req_theta ++ prov_theta
             mk_sigma       = if has_sig then mkSpecSigmaTy else mkInvSigmaTy
             need_dummy_arg = isUnLiftedType pat_ty && null arg_tys && null theta
             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
575
              -- See Note [Exported LocalIds] in Id
576

577
       ; return (Just (builder_id, need_dummy_arg)) }
578
  where
579

580 581 582 583 584 585 586
add_void :: Bool -> Type -> Type
add_void need_dummy_arg ty
  | need_dummy_arg = mkFunTy voidPrimTy ty
  | otherwise      = ty

tcPatSynBuilderBind :: TcSigFun
                    -> PatSynBind Name Name
587 588
                    -> TcM (LHsBinds Id)
-- See Note [Matchers and builders for pattern synonyms] in PatSyn
589 590
tcPatSynBuilderBind sig_fun PSB{ psb_id = L loc name, psb_def = lpat
                               , psb_dir = dir, psb_args = details }
591 592 593 594 595
  | isUnidirectional dir
  = return emptyBag

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

599
  | otherwise  -- Bidirectional
600
  = do { patsyn <- tcLookupPatSyn name
601
       ; traceTc "tcPatSynBuilderBind {" $ ppr patsyn
602
       ; let Just (builder_id, need_dummy_arg) = patSynBuilder patsyn
603 604 605 606 607
                   -- Bidirectional, so patSynBuilder returns Just

             match_group' | need_dummy_arg = add_dummy_arg match_group
                          | otherwise      = match_group

608
             bind = FunBind { fun_id      = L loc (idName builder_id)
609 610 611 612 613
                            , fun_matches = match_group'
                            , fun_co_fn   = idHsWrapper
                            , bind_fvs    = placeHolderNamesTc
                            , fun_tick    = [] }

614
       ; sig <- get_builder_sig sig_fun name builder_id need_dummy_arg
615

616
       ; (builder_binds, _) <- tcPolyCheck NonRecursive emptyPragEnv sig (noLoc bind)
617 618
       ; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds
       ; return builder_binds }
619
  where
620
    Just match_group = mb_match_group
621
    mb_match_group
622 623 624 625
       = case dir of
           Unidirectional                    -> Nothing
           ExplicitBidirectional explicit_mg -> Just explicit_mg
           ImplicitBidirectional             -> fmap mk_mg (tcPatToExpr args lpat)
626 627

    mk_mg :: LHsExpr Name -> MatchGroup Name (LHsExpr Name)
628
    mk_mg body = mkMatchGroupName Generated [builder_match]
629
             where
630
               builder_args  = [L loc (VarPat (L loc n)) | L loc n <- args]
631
               builder_match = mkMatch builder_args body (noLoc EmptyLocalBinds)
632 633

    args = case details of
634
              PrefixPatSyn args     -> args
635
              InfixPatSyn arg1 arg2 -> [arg1, arg2]
Matthew Pickering's avatar
Matthew Pickering committed
636
              RecordPatSyn args     -> map recordPatSynPatVar args
637

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
638 639
    add_dummy_arg :: MatchGroup Name (LHsExpr Name)
                  -> MatchGroup Name (LHsExpr Name)
640 641 642 643
    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)] }
644 645 646
    add_dummy_arg other_mg = pprPanic "add_dummy_arg" $
                             pprMatches (PatSyn :: HsMatchContext Name) other_mg

647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673
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
674 675 676
tcPatSynBuilderOcc :: PatSyn -> TcM (HsExpr TcId, TcSigmaType)
-- monadic only for failure
tcPatSynBuilderOcc ps
677
  | Just (builder_id, add_void_arg) <- builder
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
678 679 680 681 682 683 684
  , 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)
685 686

  | otherwise  -- Unidirectional
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
687
  = nonBidirectionalErr name
688 689 690
  where
    name    = patSynName ps
    builder = patSynBuilder ps
Gergő Érdi's avatar
Gergő Érdi committed
691

Austin Seipp's avatar
Austin Seipp committed
692
{-
693 694 695 696 697 698
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
699 700
(Just 34) we need only (Num a).  Fortunately instTcSigFromId sets
sig_warn_redundant to False.
701

Austin Seipp's avatar
Austin Seipp committed
702 703
************************************************************************
*                                                                      *
704
         Helper functions
Austin Seipp's avatar
Austin Seipp committed
705 706
*                                                                      *
************************************************************************
707

708 709
Note [As-patterns in pattern synonym definitions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
710 711 712
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:
713 714 715 716 717 718

        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
719

720 721
or
        g (K (Just True) False) = ...
722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741

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
742 743 744 745 746 747 748 749

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!
750
 -}
751

752 753 754 755 756 757 758 759 760 761
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 ()
762
    go1 p@(AsPat _ _)         = asPatInPatSynErr p
763 764 765 766 767 768
    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
769 770
    go1   LitPat{}            = return ()
    go1   NPat{}              = return ()
771 772 773 774 775 776 777 778 779 780 781
    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 $
782
    hang (text "Pattern synonym definition cannot contain as-patterns (@):")
783 784 785 786 787
       2 (ppr pat)

thInPatSynErr :: OutputableBndr name => Pat name -> TcM a
thInPatSynErr pat
  = failWithTc $
788
    hang (text "Pattern synonym definition cannot contain Template Haskell:")
789 790 791 792 793
       2 (ppr pat)

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

Matthew Pickering's avatar
Matthew Pickering committed
797 798
nonBidirectionalErr :: Outputable name => name -> TcM a
nonBidirectionalErr name = failWithTc $
799 800
    text "non-bidirectional pattern synonym"
    <+> quotes (ppr name) <+> text "used in an expression"
Matthew Pickering's avatar
Matthew Pickering committed
801

802 803
tcPatToExpr :: [Located Name] -> LPat Name -> Maybe (LHsExpr Name)
tcPatToExpr args = go
Gergő Érdi's avatar
Gergő Érdi committed
804
  where
805 806
    lhsVars = mkNameSet (map unLoc args)

807
    go :: LPat Name -> Maybe (LHsExpr Name)
808 809 810
    go (L loc (ConPatIn (L _ con) info))
      = do { exprs <- mapM go (hsConPatArgs info)
           ; return $ L loc $
811
             foldl (\x y -> HsApp (L loc x) y) (HsVar (L loc con)) exprs }
812 813 814 815

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

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

818
    go1 :: Pat Name -> Maybe (HsExpr Name)
819 820
    go1   (VarPat (L l var))
      | var `elemNameSet` lhsVars     = return $ HsVar (L l var)
821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838
      | 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
    go1   (NPat (L _ n) Nothing _)    = return $ HsOverLit n
    go1   (NPat (L _ n) (Just neg) _) = return $ noLoc neg `HsApp` noLoc (HsOverLit n)
    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
839

840 841 842 843 844 845
-- 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.
846 847
tcCollectEx :: LPat Id -> (TyVarSet, [EvVar])
tcCollectEx pat = go pat
Gergő Érdi's avatar
Gergő Érdi committed
848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874
  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
    go1 (NPlusKPat n k geq subtract)
      = 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

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