TcPatSyn.hs 34.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 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
Matthew Pickering's avatar
Matthew Pickering committed
32
import IdInfo( IdDetails(..), 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 144 145 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
{- *********************************************************************
*                                                                      *
        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 $
         hang (ptext (sLit "The result type") <+> quotes (ppr body_ty))
            2 (ptext (sLit "mentions existential type variable") <> plural bad_tvs
               <+> 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 245 246 247 248 249 250 251 252 253 254 255
       ; (tclvl, wanted, (lpat', (ex_tvs', prov_dicts, args'))) <-
           ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys )
           pushLevelAndCaptureConstraints $
           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
256

257 258 259
       -- 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
260 261 262 263 264
       ; _ <- simplifyTop (emptyWC `addImplics` implics)

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

266
       ; traceTc "tcCheckPatSynDecl }" $ ppr name
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
267
       ; tc_patsyn_finish lname dir True {- has a sig -} is_infix lpat'
268 269 270
                          (univ_tvs, req_theta, ev_binds, req_dicts)
                          (ex_tvs, mkTyVarTys ex_tvs', prov_theta, prov_dicts)
                          (args', arg_tys)
271
                          pat_ty rec_fields }
272
  where
273 274 275 276 277 278 279 280 281 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
    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)
                              (substTy subst arg_ty)
           ; 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.

-}
331

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

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

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

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

Matthew Pickering's avatar
Matthew Pickering committed
391
       ;
Matthew Pickering's avatar
Matthew Pickering committed
392 393

        traceTc "tc_patsyn_finish {" $
394 395
           ppr (unLoc lname) $$ ppr (unLoc lpat') $$
           ppr (univ_tvs, req_theta, req_ev_binds, req_dicts) $$
396 397 398
           ppr (ex_tvs, prov_theta, prov_dicts) $$
           ppr args $$
           ppr arg_tys $$
399
           ppr pat_ty
400 401

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

Matthew Pickering's avatar
Matthew Pickering committed
408

409
       -- Make the 'builder'
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
410
       ; builder_id <- mkPatSynBuilderId has_sig dir lname qtvs theta
Matthew Pickering's avatar
Matthew Pickering committed
411
                                         arg_tys pat_ty
Matthew Pickering's avatar
Matthew Pickering committed
412 413 414 415 416

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

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

436
       ; traceTc "tc_patsyn_finish }" empty
437
       ; return (matcher_bind, tcg_env) }
438

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

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

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
476
             fail_ty  = mkFunTy voidPrimTy res_ty
477

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

488 489
             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
490

491
             fail' = nlHsApps fail [nlHsVar voidPrimId]
Gergő Érdi's avatar
Gergő Érdi committed
492

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

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

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

532 533
       ; return ((matcher_id, is_unlifted), matcher_bind) }

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

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

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

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
557 558
mkPatSynBuilderId :: Bool  -- True <=> signature provided
                  -> HsPatSynDir a -> Located Name
Matthew Pickering's avatar
Matthew Pickering committed
559
                  -> [TyVar] -> ThetaType -> [Type] -> Type
560
                  -> TcM (Maybe (Id, Bool))
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
561
mkPatSynBuilderId has_sig dir  (L _ name) qtvs theta arg_tys pat_ty
562 563 564
  | isUnidirectional dir
  = return Nothing
  | otherwise
565
  = do { builder_name <- newImplicitBinder name mkBuilderOcc
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
566 567 568
       ; let mk_sigma      = if has_sig then mkSpecSigmaTy else mkInvSigmaTy
             builder_sigma = add_void $
                             mk_sigma qtvs theta (mkFunTys arg_tys pat_ty)
Matthew Pickering's avatar
Matthew Pickering committed
569 570
             builder_id    =
              -- See Note [Exported LocalIds] in Id
Matthew Pickering's avatar
Matthew Pickering committed
571
              mkExportedLocalId VanillaId builder_name builder_sigma
572
       ; return (Just (builder_id, need_dummy_arg)) }
573
  where
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
574 575
    add_void | need_dummy_arg = mkFunTy voidPrimTy
             | otherwise      = id
576 577 578 579 580 581 582 583 584 585 586 587 588 589 590
    need_dummy_arg = isUnLiftedType pat_ty && null arg_tys && null theta

tcPatSynBuilderBind :: PatSynBind Name Name
                    -> TcM (LHsBinds Id)
-- See Note [Matchers and builders for pattern synonyms] in PatSyn
tcPatSynBuilderBind PSB{ psb_id = L loc name, psb_def = lpat
                       , psb_dir = dir, psb_args = details }
  | isUnidirectional dir
  = return emptyBag

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

591
  | otherwise  -- Bidirectional
592
  = do { patsyn <- tcLookupPatSyn name
593
       ; traceTc "tcPatSynBuilderBind {" $ ppr patsyn
594
       ; let Just (builder_id, need_dummy_arg) = patSynBuilder patsyn
595 596 597 598 599
                   -- Bidirectional, so patSynBuilder returns Just

             match_group' | need_dummy_arg = add_dummy_arg match_group
                          | otherwise      = match_group

600
             bind = FunBind { fun_id      = L loc (idName builder_id)
601 602 603 604 605
                            , fun_matches = match_group'
                            , fun_co_fn   = idHsWrapper
                            , bind_fvs    = placeHolderNamesTc
                            , fun_tick    = [] }

606
       ; sig <- instTcTySigFromId builder_id
607
                -- See Note [Redundant constraints for builder]
608

609
       ; (builder_binds, _) <- tcPolyCheck NonRecursive emptyPragEnv sig (noLoc bind)
610 611
       ; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds
       ; return builder_binds }
612
  where
613
    Just match_group = mb_match_group
614
    mb_match_group
615 616 617 618
       = case dir of
           Unidirectional                    -> Nothing
           ExplicitBidirectional explicit_mg -> Just explicit_mg
           ImplicitBidirectional             -> fmap mk_mg (tcPatToExpr args lpat)
619 620

    mk_mg :: LHsExpr Name -> MatchGroup Name (LHsExpr Name)
621
    mk_mg body = mkMatchGroupName Generated [builder_match]
622
             where
623
               builder_args  = [L loc (VarPat (L loc n)) | L loc n <- args]
624
               builder_match = mkMatch builder_args body (noLoc EmptyLocalBinds)
625 626

    args = case details of
627
              PrefixPatSyn args     -> args
628
              InfixPatSyn arg1 arg2 -> [arg1, arg2]
Matthew Pickering's avatar
Matthew Pickering committed
629
              RecordPatSyn args     -> map recordPatSynPatVar args
630

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
631 632
    add_dummy_arg :: MatchGroup Name (LHsExpr Name)
                  -> MatchGroup Name (LHsExpr Name)
633 634 635 636
    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)] }
637 638 639
    add_dummy_arg other_mg = pprPanic "add_dummy_arg" $
                             pprMatches (PatSyn :: HsMatchContext Name) other_mg

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
640 641 642
tcPatSynBuilderOcc :: PatSyn -> TcM (HsExpr TcId, TcSigmaType)
-- monadic only for failure
tcPatSynBuilderOcc ps
643
  | Just (builder_id, add_void_arg) <- builder
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
644 645 646 647 648 649 650
  , 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)
651 652

  | otherwise  -- Unidirectional
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
653
  = nonBidirectionalErr name
654 655 656
  where
    name    = patSynName ps
    builder = patSynBuilder ps
Gergő Érdi's avatar
Gergő Érdi committed
657

Austin Seipp's avatar
Austin Seipp committed
658
{-
659 660 661 662 663 664
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
665 666
(Just 34) we need only (Num a).  Fortunately instTcSigFromId sets
sig_warn_redundant to False.
667

Austin Seipp's avatar
Austin Seipp committed
668 669
************************************************************************
*                                                                      *
670
         Helper functions
Austin Seipp's avatar
Austin Seipp committed
671 672
*                                                                      *
************************************************************************
673

674 675
Note [As-patterns in pattern synonym definitions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
676 677 678
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:
679 680 681 682 683 684

        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
685

686 687
or
        g (K (Just True) False) = ...
688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707

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
708 709 710 711 712 713 714 715

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!
716
 -}
717

718 719 720 721 722 723 724 725 726 727
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 ()
728
    go1 p@(AsPat _ _)         = asPatInPatSynErr p
729 730 731 732 733 734
    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
735 736
    go1   LitPat{}            = return ()
    go1   NPat{}              = return ()
737 738 739 740 741 742 743 744 745 746 747
    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 $
748
    hang (ptext (sLit "Pattern synonym definition cannot contain as-patterns (@):"))
749 750 751 752 753 754 755 756 757 758 759 760 761 762
       2 (ppr pat)

thInPatSynErr :: OutputableBndr name => Pat name -> TcM a
thInPatSynErr pat
  = failWithTc $
    hang (ptext (sLit "Pattern synonym definition cannot contain Template Haskell:"))
       2 (ppr pat)

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

Matthew Pickering's avatar
Matthew Pickering committed
763 764 765 766 767
nonBidirectionalErr :: Outputable name => name -> TcM a
nonBidirectionalErr name = failWithTc $
    ptext (sLit "non-bidirectional pattern synonym")
    <+> quotes (ppr name) <+> ptext (sLit "used in an expression")

768 769
tcPatToExpr :: [Located Name] -> LPat Name -> Maybe (LHsExpr Name)
tcPatToExpr args = go
Gergő Érdi's avatar
Gergő Érdi committed
770
  where
771 772
    lhsVars = mkNameSet (map unLoc args)

773
    go :: LPat Name -> Maybe (LHsExpr Name)
774 775 776
    go (L loc (ConPatIn (L _ con) info))
      = do { exprs <- mapM go (hsConPatArgs info)
           ; return $ L loc $
777
             foldl (\x y -> HsApp (L loc x) y) (HsVar (L loc con)) exprs }
778 779 780 781

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

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

784
    go1 :: Pat Name -> Maybe (HsExpr Name)
785 786
    go1   (VarPat (L l var))
      | var `elemNameSet` lhsVars     = return $ HsVar (L l var)
787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804
      | 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
805

806 807 808 809 810 811
-- 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.
812 813
tcCollectEx :: LPat Id -> (TyVarSet, [EvVar])
tcCollectEx pat = go pat
Gergő Érdi's avatar
Gergő Érdi committed
814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840
  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

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