Implement scoped type variables in pattern synonyms

This fixes Trac #11351.   The implementation is pretty
simple, happily.

I took the opportunity to re-order the prov/req context
in builder-ids, which was confusingly backwards.

compiler/basicTypes/PatSyn.hs

@@ -99,7 +99,7 @@ data PatSyn
              -- Nothing  => uni-directional pattern synonym
              -- Just (builder, is_unlifted) => bi-directional
              -- Builder function, of type
-             --  forall univ_tvs, ex_tvs. (prov_theta, req_theta)
+             --  forall univ_tvs, ex_tvs. (req_theta, prov_theta)
              --                       =>  arg_tys -> res_ty
              -- See Note [Builder for pattern synonyms with unboxed type]
   }
@@ -213,7 +213,7 @@ For *bidirectional* pattern synonyms, we also generate a "builder"
 function which implements the pattern synonym in an expression
 context. For our running example, it will be:
 
-        $bP :: forall t b. (Show (Maybe t), Ord b, Eq t, Num t)
+        $bP :: forall t b. (Eq t, Num t, Show (Maybe t), Ord b)
             => b -> T (Maybe t)
         $bP x = MkT [x] (Just 42)
 

compiler/deSugar/DsExpr.hs

@@ -619,7 +619,7 @@ dsExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = fields
           let tycon = dataConTyCon data_con in
           (mkTyConApp tycon in_inst_tys, mkFamilyTyConApp tycon out_inst_tys)
         PatSynCon pat_syn ->
-          (patSynInstResTy pat_syn in_inst_tys
+          ( patSynInstResTy pat_syn in_inst_tys
           , patSynInstResTy pat_syn out_inst_tys)
     mk_alt upd_fld_env con
       = do { let (univ_tvs, ex_tvs, eq_spec,
@@ -641,8 +641,8 @@ dsExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = fields
                  inst_con = noLoc $ HsWrap wrap (HsVar (noLoc wrap_id))
                         -- Reconstruct with the WrapId so that unpacking happens
                  -- The order here is because of the order in `TcPatSyn`.
-                 wrap = dict_req_wrap                                           <.>
-                        mkWpEvVarApps theta_vars                                <.>
+                 wrap = mkWpEvVarApps theta_vars                                <.>
+                        dict_req_wrap                                           <.>
                         mkWpTyApps    (mkTyVarTys ex_tvs)                       <.>
                         mkWpTyApps    [ ty
                                       | (tv, ty) <- univ_tvs `zip` out_inst_tys

compiler/rename/RnBinds.hs

@@ -563,6 +563,8 @@ mkSigTvFn sigs
       = add_scoped_tvs names (hsScopedTvs sig_ty) env
     add_scoped_sig (L _ (TypeSig names sig_ty)) env
       = add_scoped_tvs names (hsWcScopedTvs sig_ty) env
+    add_scoped_sig (L _ (PatSynSig name sig_ty)) env
+      = add_scoped_tvs [name] (hsScopedTvs sig_ty) env
     add_scoped_sig _ env = env
 
     add_scoped_tvs :: [Located Name] -> [Name] -> NameEnv [Name] -> NameEnv [Name]
@@ -615,29 +617,33 @@ dupFixityDecl loc rdr_name
 rnPatSynBind :: (Name -> [Name])                -- Signature tyvar function
              -> PatSynBind Name RdrName
              -> RnM (PatSynBind Name Name, [Name], Uses)
-rnPatSynBind _sig_fn bind@(PSB { psb_id = L _ name
-                               , psb_args = details
-                               , psb_def = pat
-                               , psb_dir = dir })
+rnPatSynBind sig_fn bind@(PSB { psb_id = L _ name
+                              , psb_args = details
+                              , psb_def = pat
+                              , psb_dir = dir })
        -- invariant: no free vars here when it's a FunBind
   = do  { pattern_synonym_ok <- xoptM LangExt.PatternSynonyms
         ; unless pattern_synonym_ok (addErr patternSynonymErr)
+        ; let sig_tvs = sig_fn name
 
-        ; ((pat', details'), fvs1) <- rnPat PatSyn pat $ \pat' -> do
+        ; ((pat', details'), fvs1) <- bindSigTyVarsFV sig_tvs $
+                                      rnPat PatSyn pat $ \pat' ->
          -- We check the 'RdrName's instead of the 'Name's
          -- so that the binding locations are reported
          -- from the left-hand side
-        { (details', fvs) <- case details of
+            case details of
                PrefixPatSyn vars ->
                    do { checkDupRdrNames vars
                       ; names <- mapM lookupVar vars
-                      ; return (PrefixPatSyn names, mkFVs (map unLoc names)) }
+                      ; return ( (pat', PrefixPatSyn names)
+                               , mkFVs (map unLoc names)) }
                InfixPatSyn var1 var2 ->
                    do { checkDupRdrNames [var1, var2]
                       ; name1 <- lookupVar var1
                       ; name2 <- lookupVar var2
                       -- ; checkPrecMatch -- TODO
-                      ; return (InfixPatSyn name1 name2, mkFVs (map unLoc [name1, name2])) }
+                      ; return ( (pat', InfixPatSyn name1 name2)
+                               , mkFVs (map unLoc [name1, name2])) }
                RecordPatSyn vars ->
                    do { checkDupRdrNames (map recordPatSynSelectorId vars)
                       ; let rnRecordPatSynField
@@ -646,16 +652,15 @@ rnPatSynBind _sig_fn bind@(PSB { psb_id = L _ name
                               ; hidden'  <- lookupVar hidden
                               ; return $ RecordPatSynField visible' hidden' }
                       ; names <- mapM rnRecordPatSynField  vars
-                      ; return (RecordPatSyn names
+                      ; return ( (pat', RecordPatSyn names)
                                , mkFVs (map (unLoc . recordPatSynPatVar) names)) }
 
-
-        ; return ((pat', details'), fvs) }
         ; (dir', fvs2) <- case dir of
             Unidirectional -> return (Unidirectional, emptyFVs)
             ImplicitBidirectional -> return (ImplicitBidirectional, emptyFVs)
             ExplicitBidirectional mg ->
-                do { (mg', fvs) <- rnMatchGroup PatSyn rnLExpr mg
+                do { (mg', fvs) <- bindSigTyVarsFV sig_tvs $
+                                   rnMatchGroup PatSyn rnLExpr mg
                    ; return (ExplicitBidirectional mg', fvs) }
 
         ; mod <- getModule

compiler/typecheck/TcBinds.hs

@@ -359,7 +359,7 @@ tcValBinds top_lvl binds sigs thing_inside
             { (binds', (extra_binds', thing)) <- tcBindGroups top_lvl sig_fn prag_fn binds $ do
                    { thing <- thing_inside
                      -- See Note [Pattern synonym builders don't yield dependencies]
-                   ; patsyn_builders <- mapM tcPatSynBuilderBind patsyns
+                   ; patsyn_builders <- mapM (tcPatSynBuilderBind sig_fn) patsyns
                    ; let extra_binds = [ (NonRecursive, builder) | builder <- patsyn_builders ]
                    ; return (extra_binds, thing) }
             ; return (binds' ++ extra_binds', thing) }}
@@ -1885,12 +1885,15 @@ instTcTySigFromId id
        ; (tvs, theta, tau) <- tcInstType (tcInstSigTyVarsLoc loc)
                                          (idType id)
        ; return $ TISI { sig_bndr  = CompleteSig id
-                          -- False: do not report redundant constraints
-                          -- The user has no control over the signature!
                        , sig_skols = [(tyVarName tv, tv) | tv <- tvs]
+                          -- These are freshly instantiated, so although
+                          -- we put them in the type envt, doing so has
+                          -- no effect
                        , sig_theta = theta
                        , sig_tau   = tau
                        , sig_ctxt  = FunSigCtxt name False
+                          -- False: do not report redundant constraints
+                          -- The user has no control over the signature!
                        , sig_loc   = loc } }
 
 instTcTySig :: UserTypeCtxt

compiler/typecheck/TcHsType.hs

@@ -1440,7 +1440,7 @@ tcHsTyVarBndrs orig_hs_tvs thing_inside
              thing (tv : tvs) }
 
 tcHsTyVarBndr :: HsTyVarBndr Name -> TcM TcTyVar
--- Return a type variable initialised with a kind variable.
+-- Return a SkolemTv TcTyVar, initialised with a kind variable.
 -- Typically the Kind inside the HsTyVarBndr will be a tyvar
 -- with a mutable kind in it.
 -- NB: These variables must not be in scope. This function

compiler/typecheck/TcPat.hs

@@ -8,7 +8,7 @@ TcPat: Typechecking patterns
 
 {-# LANGUAGE CPP, RankNTypes #-}
 
-module TcPat ( tcLetPat, TcSigFun
+module TcPat ( tcLetPat
              , TcPragEnv, lookupPragEnv, emptyPragEnv
              , LetBndrSpec(..), addInlinePrags
              , tcPat, tcPat_O, tcPats, newNoSigLetBndr
@@ -145,7 +145,6 @@ inPatBind (PE { pe_ctxt = LamPat {} }) = False
 
 ---------------
 type TcPragEnv = NameEnv [LSig Name]
-type TcSigFun  = Name -> Maybe TcSigInfo
 
 emptyPragEnv :: TcPragEnv
 emptyPragEnv = emptyNameEnv

compiler/typecheck/TcPatSyn.hs

@@ -29,7 +29,7 @@ import Outputable
 import FastString
 import Var
 import Id
-import IdInfo( IdDetails(..), RecSelParent(..))
+import IdInfo( RecSelParent(..))
 import TcBinds
 import BasicTypes
 import TcSimplify
@@ -242,6 +242,7 @@ tcCheckPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details
        ; (tclvl, wanted, (lpat', (ex_tvs', prov_dicts, args'))) <-
            ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys )
            pushLevelAndCaptureConstraints $
+           tcExtendTyVarEnv univ_tvs      $
            tcPat PatSyn lpat pat_ty $
            do { (subst, ex_tvs') <- if   isUnidirectional dir
                                     then newMetaTyVars    ex_tvs
@@ -384,13 +385,8 @@ tc_patsyn_finish lname dir has_sig is_infix lpat'
        ; req_theta    <- zonkTcTypes req_theta
        ; pat_ty       <- zonkTcType pat_ty
        ; arg_tys      <- zonkTcTypes arg_tys
-       ; let qtvs    = univ_tvs ++ ex_tvs
-             -- See Note [Record PatSyn Desugaring]
-             theta   = prov_theta ++ req_theta
 
-       ;
-
-        traceTc "tc_patsyn_finish {" $
+       ; traceTc "tc_patsyn_finish {" $
            ppr (unLoc lname) $$ ppr (unLoc lpat') $$
            ppr (univ_tvs, req_theta, req_ev_binds, req_dicts) $$
            ppr (ex_tvs, prov_theta, prov_dicts) $$
@@ -407,7 +403,9 @@ tc_patsyn_finish lname dir has_sig is_infix lpat'
 
 
        -- Make the 'builder'
-       ; builder_id <- mkPatSynBuilderId has_sig dir lname qtvs theta
+       ; builder_id <- mkPatSynBuilderId has_sig dir lname
+                                         univ_tvs req_theta
+                                         ex_tvs   prov_theta
                                          arg_tys pat_ty
 
          -- TODO: Make this have the proper information
@@ -482,7 +480,7 @@ tcPatSynMatcher has_sig (L loc name) lpat
 
        ; let matcher_tau   = mkFunTys [pat_ty, cont_ty, fail_ty] res_ty
              matcher_sigma = mkInvSigmaTy (lev_tv:res_tv:univ_tvs) req_theta matcher_tau
-             matcher_id    = mkExportedLocalId PatSynId matcher_name matcher_sigma
+             matcher_id    = mkExportedVanillaId matcher_name matcher_sigma
                              -- See Note [Exported LocalIds] in Id
 
              inst_wrap = mkWpEvApps prov_dicts <.> mkWpTyApps ex_tys
@@ -556,30 +554,40 @@ isUnidirectional ExplicitBidirectional{} = False
 
 mkPatSynBuilderId :: Bool  -- True <=> signature provided
                   -> HsPatSynDir a -> Located Name
-                  -> [TyVar] -> ThetaType -> [Type] -> Type
+                  -> [TyVar] -> ThetaType
+                  -> [TyVar] -> ThetaType
+                  -> [Type] -> Type
                   -> TcM (Maybe (Id, Bool))
-mkPatSynBuilderId has_sig dir  (L _ name) qtvs theta arg_tys pat_ty
+mkPatSynBuilderId has_sig dir (L _ name)
+                  univ_tvs req_theta ex_tvs prov_theta
+                  arg_tys pat_ty
   | isUnidirectional dir
   = return Nothing
   | otherwise
   = do { builder_name <- newImplicitBinder name mkBuilderOcc
-       ; let mk_sigma      = if has_sig then mkSpecSigmaTy else mkInvSigmaTy
-             builder_sigma = add_void $
-                             mk_sigma qtvs theta (mkFunTys arg_tys pat_ty)
-             builder_id    =
+       ; 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
               -- See Note [Exported LocalIds] in Id
-              mkExportedLocalId VanillaId builder_name builder_sigma
+
        ; return (Just (builder_id, need_dummy_arg)) }
   where
-    add_void | need_dummy_arg = mkFunTy voidPrimTy
-             | otherwise      = id
-    need_dummy_arg = isUnLiftedType pat_ty && null arg_tys && null theta
 
-tcPatSynBuilderBind :: PatSynBind Name Name
+add_void :: Bool -> Type -> Type
+add_void need_dummy_arg ty
+  | need_dummy_arg = mkFunTy voidPrimTy ty
+  | otherwise      = ty
+
+tcPatSynBuilderBind :: TcSigFun
+                    -> 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 }
+tcPatSynBuilderBind sig_fun PSB{ psb_id = L loc name, psb_def = lpat
+                               , psb_dir = dir, psb_args = details }
   | isUnidirectional dir
   = return emptyBag
 
@@ -603,8 +611,7 @@ tcPatSynBuilderBind PSB{ psb_id = L loc name, psb_def = lpat
                             , bind_fvs    = placeHolderNamesTc
                             , fun_tick    = [] }
 
-       ; sig <- instTcTySigFromId builder_id
-                -- See Note [Redundant constraints for builder]
+       ; sig <- get_builder_sig sig_fun name builder_id need_dummy_arg
 
        ; (builder_binds, _) <- tcPolyCheck NonRecursive emptyPragEnv sig (noLoc bind)
        ; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds
@@ -637,6 +644,33 @@ tcPatSynBuilderBind PSB{ psb_id = L loc name, psb_def = lpat
     add_dummy_arg other_mg = pprPanic "add_dummy_arg" $
                              pprMatches (PatSyn :: HsMatchContext Name) other_mg
 
+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]
+
 tcPatSynBuilderOcc :: PatSyn -> TcM (HsExpr TcId, TcSigmaType)
 -- monadic only for failure
 tcPatSynBuilderOcc ps

compiler/typecheck/TcPatSyn.hs-boot

@@ -3,7 +3,7 @@ module TcPatSyn where
 import Name      ( Name )
 import Id        ( Id )
 import HsSyn     ( PatSynBind, LHsBinds, LHsSigType )
-import TcRnTypes ( TcM, TcPatSynInfo )
+import TcRnTypes ( TcM, TcSigFun, TcPatSynInfo )
 import TcRnMonad ( TcGblEnv)
 import Outputable ( Outputable )
 
@@ -17,7 +17,7 @@ tcCheckPatSynDecl :: PatSynBind Name Name
                   -> TcPatSynInfo
                   -> TcM (LHsBinds Id, TcGblEnv)
 
-tcPatSynBuilderBind :: PatSynBind Name Name
+tcPatSynBuilderBind :: TcSigFun -> PatSynBind Name Name
                     -> TcM (LHsBinds Id)
 
 nonBidirectionalErr :: Outputable name => name -> TcM a

compiler/typecheck/TcRnTypes.hs

@@ -56,9 +56,11 @@ module TcRnTypes(
         ArrowCtxt(..),
 
         -- TcSigInfo
-        TcSigInfo(..), TcIdSigInfo(..), TcPatSynInfo(..), TcIdSigBndr(..),
+        TcSigFun, TcSigInfo(..), TcIdSigInfo(..),
+        TcPatSynInfo(..), TcIdSigBndr(..),
         findScopedTyVars, isPartialSig, noCompleteSig, tcSigInfoName,
-        completeIdSigPolyId, completeSigPolyId_maybe, completeIdSigPolyId_maybe,
+        completeIdSigPolyId, completeSigPolyId_maybe,
+        completeIdSigPolyId_maybe,
 
         -- Canonical constraints
         Xi, Ct(..), Cts, emptyCts, andCts, andManyCts, pprCts,
@@ -1133,6 +1135,8 @@ instance Outputable WhereFrom where
 *                                                                      *
 ********************************************************************* -}
 
+type TcSigFun  = Name -> Maybe TcSigInfo
+
 data TcSigInfo = TcIdSig     TcIdSigInfo
                | TcPatSynSig TcPatSynInfo
 

testsuite/tests/patsyn/should_compile/T11351.hs

+{-# LANGUAGE PatternSynonyms, TypeApplications, ScopedTypeVariables, ViewPatterns #-}
+
+module T11351 where
+
+import GHC.TypeLits
+import Data.Proxy
+
+symbol :: forall s. KnownSymbol s => String
+symbol = symbolVal @s Proxy
+
+-- Not in scope: type variable ‘s’
+-- Not in scope: type variable ‘s’
+pattern Symbol :: forall s. KnownSymbol s => String
+pattern Symbol <- ((== symbol @s) -> True) where
+         Symbol = symbol @s
+
+-- • Could not deduce (KnownSymbol n0)
+--     arising from a use of ‘symbolVal’
+--   from the context: KnownSymbol s
+--     bound by the type signature for pattern synonym ‘Symbol’:
+--                String
+pattern Symbol2 :: forall s. KnownSymbol s => String
+pattern Symbol2 <- ((== symbolVal (Proxy :: Proxy s)) -> True)

testsuite/tests/patsyn/should_compile/all.T

@@ -49,3 +49,4 @@ test('MoreEx', normal, compile, [''])
 test('T11283', normal, compile, [''])
 test('T11336', normal, compile, [''])
 test('T11367', normal, compile, [''])
+test('T11351', normal, compile, [''])