Pattern synonyms: swap provided/required
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 28 Oct 2015 09:41:27 +0000 (09:41 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Wed, 28 Oct 2015 09:46:22 +0000 (09:46 +0000)
This patch swaps the order of provided and required constraints in
a pattern signature, so it now goes

      pattern P :: req => prov => t1 -> ... tn -> res_ty

See the long discussion in Trac #10928.

I think I have found all the places, but I could have missed something
particularly in comments.

There is a Haddock changes; so a submodule update.

16 files changed:
compiler/basicTypes/PatSyn.hs
compiler/hsSyn/HsBinds.hs
compiler/iface/IfaceSyn.hs
compiler/iface/MkIface.hs
compiler/rename/RnBinds.hs
compiler/typecheck/TcBinds.hs
compiler/typecheck/TcPat.hs
docs/users_guide/glasgow_exts.rst
testsuite/tests/ghci/scripts/T8776.stdout
testsuite/tests/patsyn/should_compile/T10997_1a.hs
testsuite/tests/patsyn/should_compile/T10997a.hs
testsuite/tests/patsyn/should_compile/T8584-2.hs
testsuite/tests/patsyn/should_fail/T11010.hs [new file with mode: 0644]
testsuite/tests/patsyn/should_fail/T11010.stderr [new file with mode: 0644]
testsuite/tests/patsyn/should_fail/all.T
utils/haddock

index 503ebd8..2546ff4 100644 (file)
@@ -46,6 +46,7 @@ import Data.Function
 
 -- | A pattern synonym
 -- See Note [Pattern synonym representation]
+-- See Note [Patten synonym signatures]
 data PatSyn
   = MkPatSyn {
         psName        :: Name,
@@ -89,7 +90,44 @@ data PatSyn
   }
   deriving Data.Typeable.Typeable
 
-{-
+{- Note [Patten synonym signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In a pattern synonym signature we write
+   pattern P :: req => prov => t1 -> ... tn -> res_ty
+
+Note that the "required" context comes first, then the "provided"
+context.  Moreover, the "required" context must not mention
+existentially-bound type variables; that is, ones not mentioned in
+res_ty.  See lots of discussion in Trac #10928.
+
+If there is no "provided" context, you can omit it; but you
+can't omit the "required" part (unless you omit both).
+
+Example 1:
+      pattern P1 :: (Num a, Eq a) => b -> Maybe (a,b)
+      pattern P1 x = Just (3,x)
+
+  We require (Num a, Eq a) to match the 3; there is no provided
+  context.
+
+Example 2:
+      data T2 where
+        MkT2 :: (Num a, Eq a) => a -> a -> T2
+
+      patttern P2 :: () => (Num a, Eq a) => a -> T2
+      pattern P2 x = MkT2 3 x
+
+  When we match against P2 we get a Num dictionary provided.
+  We can use that to check the match against 3.
+
+Example 3:
+      pattern P3 :: Eq a => a -> b -> T3 b
+
+   This signature is illegal because the (Eq a) is a required
+   constraint, but it mentions the existentially-bound variable 'a'.
+   You can see it's existential because it doesn't appear in the
+   result type (T3 b).
+
 Note [Pattern synonym representation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider the following pattern synonym declaration
@@ -267,6 +305,7 @@ patSynName = psName
 
 patSynType :: PatSyn -> Type
 -- The full pattern type, used only in error messages
+-- See Note [Patten synonym signatures]
 patSynType (MkPatSyn { psUnivTyVars = univ_tvs, psReqTheta = req_theta
                      , psExTyVars   = ex_tvs,   psProvTheta = prov_theta
                      , psArgs = orig_args, psOrigResTy = orig_res_ty })
@@ -288,11 +327,11 @@ patSynArgs = psArgs
 patSynExTyVars :: PatSyn -> [TyVar]
 patSynExTyVars = psExTyVars
 
-patSynSig :: PatSyn -> ([TyVar], [TyVar], ThetaType, ThetaType, [Type], Type)
+patSynSig :: PatSyn -> ([TyVar], ThetaType, [TyVar], ThetaType, [Type], Type)
 patSynSig (MkPatSyn { psUnivTyVars = univ_tvs, psExTyVars = ex_tvs
                     , psProvTheta = prov, psReqTheta = req
                     , psArgs = arg_tys, psOrigResTy = res_ty })
-  = (univ_tvs, ex_tvs, prov, req, arg_tys, res_ty)
+  = (univ_tvs, req, ex_tvs, prov, arg_tys, res_ty)
 
 patSynMatcher :: PatSyn -> (Id,Bool)
 patSynMatcher = psMatcher
index 4b661ff..18756f6 100644 (file)
@@ -641,8 +641,8 @@ data Sig name
       -- For details on above see note [Api annotations] in ApiAnnotation
   | PatSynSig (Located name)
               (HsExplicitFlag, LHsTyVarBndrs name)
-              (LHsContext name) -- Provided context
               (LHsContext name) -- Required context
+              (LHsContext name) -- Provided context
               (LHsType name)
 
         -- | A type signature for a default method inside a class
@@ -839,23 +839,23 @@ ppr_sig (InlineSig var inl)       = pragBrackets (ppr inl <+> pprPrefixOcc (unLo
 ppr_sig (SpecInstSig _ ty)
   = pragBrackets (ptext (sLit "SPECIALIZE instance") <+> ppr ty)
 ppr_sig (MinimalSig _ bf)         = pragBrackets (pprMinimalSig bf)
-ppr_sig (PatSynSig name (flag, qtvs) (L _ prov) (L _ req) ty)
+ppr_sig (PatSynSig name (flag, qtvs) (L _ req) (L _ prov) ty)
   = pprPatSynSig (unLoc name) False -- TODO: is_bindir
                  (pprHsForAll flag qtvs (noLoc []))
-                 (pprHsContextMaybe prov) (pprHsContextMaybe req)
+                 (pprHsContextMaybe req) (pprHsContextMaybe prov)
                  (ppr ty)
 
 pprPatSynSig :: (OutputableBndr name)
              => name -> Bool -> SDoc -> Maybe SDoc -> Maybe SDoc -> SDoc -> SDoc
-pprPatSynSig ident _is_bidir tvs prov req ty
+pprPatSynSig ident _is_bidir tvs req prov ty
   = ptext (sLit "pattern") <+> pprPrefixOcc ident <+> dcolon <+>
     tvs <+> context <+> ty
   where
-    context = case (prov, req) of
+    context = case (req, prov) of
         (Nothing, Nothing)    -> empty
-        (Nothing, Just req)   -> parens empty <+> darrow <+> req <+> darrow
-        (Just prov, Nothing)  -> prov <+> darrow
-        (Just prov, Just req) -> prov <+> darrow <+> req <+> darrow
+        (Nothing, Just prov)  -> parens empty <+> darrow <+> prov <+> darrow
+        (Just req, Nothing)   -> req <+> darrow
+        (Just req, Just prov) -> req <+> darrow <+> prov <+> darrow
 
 instance OutputableBndr name => Outputable (FixitySig name) where
   ppr (FixitySig names fixity) = sep [ppr fixity, pprops]
index 85210cd..42342ae 100644 (file)
@@ -772,8 +772,8 @@ pprIfaceDecl _ (IfacePatSyn { ifName = name, ifPatBuilder = builder,
                               ifPatTy = pat_ty} )
   = pprPatSynSig name is_bidirectional
                  (pprUserIfaceForAll tvs)
-                 (pprIfaceContextMaybe prov_ctxt)
                  (pprIfaceContextMaybe req_ctxt)
+                 (pprIfaceContextMaybe prov_ctxt)
                  (pprIfaceType ty)
   where
     is_bidirectional = isJust builder
index d4b764b..84d9fd9 100644 (file)
@@ -1524,7 +1524,7 @@ patSynToIfaceDecl ps
                 , ifPatTy         = tidyToIfaceType env2 rhs_ty
                 }
   where
-    (univ_tvs, ex_tvs, prov_theta, req_theta, args, rhs_ty) = patSynSig ps
+    (univ_tvs, req_theta, ex_tvs, prov_theta, args, rhs_ty) = patSynSig ps
     (env1, univ_tvs') = tidyTyVarBndrs emptyTidyEnv univ_tvs
     (env2, ex_tvs')   = tidyTyVarBndrs env1 ex_tvs
     to_if_pr (id, needs_dummy) = (idName id, needs_dummy)
index 10c5b7b..d63808e 100644 (file)
@@ -923,7 +923,7 @@ renameSig ctxt sig@(MinimalSig s bf)
   = do new_bf <- traverse (lookupSigOccRn ctxt sig) bf
        return (MinimalSig s new_bf, emptyFVs)
 
-renameSig ctxt sig@(PatSynSig v (flag, qtvs) prov req ty)
+renameSig ctxt sig@(PatSynSig v (flag, qtvs) req prov ty)
   = do  { v' <- lookupSigOccRn ctxt sig v
         ; let doc = TypeSigCtx $ quotes (ppr v)
         ; loc <- getSrcSpanM
@@ -940,12 +940,12 @@ renameSig ctxt sig@(PatSynSig v (flag, qtvs) prov req ty)
             Qualified -> panic "renameSig: Qualified"
 
         ; bindHsTyVars doc Nothing tv_kvs tv_bndrs $ \ tyvars -> do
-        { (prov', fvs1) <- rnContext doc prov
-        ; (req', fvs2) <- rnContext doc req
+        { (req', fvs2) <- rnContext doc req
+        ; (prov', fvs1) <- rnContext doc prov
         ; (ty', fvs3) <- rnLHsType doc ty
 
         ; let fvs = plusFVs [fvs1, fvs2, fvs3]
-        ; return (PatSynSig v' (flag, tyvars) prov' req' ty', fvs) }}
+        ; return (PatSynSig v' (flag, tyvars) req' prov' ty', fvs) }}
 
 ppr_sig_bndrs :: [Located RdrName] -> SDoc
 ppr_sig_bndrs bs = quotes (pprWithCommas ppr bs)
index f927ffa..d939ad3 100644 (file)
@@ -1621,20 +1621,31 @@ tcTySig (L loc (TypeSig names@(L _ name1 : _) hs_ty wcs))
              ; sig <- instTcTySig ctxt hs_ty sigma_ty (extra_cts hs_ty) wc_prs name
              ; return (TcIdSig sig) }
 
-tcTySig (L loc (PatSynSig (L _ name) (_, qtvs) prov req ty))
+tcTySig (L loc (PatSynSig (L _ name) (_, qtvs) req prov ty))
   = setSrcSpan loc $
-    do { traceTc "tcTySig {" $ ppr name $$ ppr qtvs $$ ppr prov $$ ppr req $$ ppr ty
+    do { traceTc "tcTySig {" $ ppr name $$ ppr qtvs $$ ppr req $$ ppr prov $$ ppr ty
        ; let ctxt = PatSynCtxt name
        ; tcHsTyVarBndrs qtvs $ \ qtvs' -> do
        { ty' <- tcHsSigType ctxt ty
        ; req' <- tcHsContext req
        ; prov' <- tcHsContext prov
 
+       -- These are /signatures/ so we zonk to squeeze out any kind
+       -- unification variables. Thta has happened automatically in tcHsSigType
+       ; req'  <- zonkTcThetaType req'
+       ; prov' <- zonkTcThetaType prov'
+
        ; qtvs' <- mapM zonkQuantifiedTyVar qtvs'
 
        ; let (_, pat_ty) = tcSplitFunTys ty'
              univ_set = tyVarsOfType pat_ty
              (univ_tvs, ex_tvs) = partition (`elemVarSet` univ_set) qtvs'
+             bad_tvs = varSetElems (tyVarsOfTypes req' `minusVarSet` univ_set)
+
+       ; unless (null bad_tvs) $ addErr $
+         hang (ptext (sLit "The 'required' context") <+> quotes (pprTheta req'))
+            2 (ptext (sLit "mentions existential type variable") <> plural bad_tvs
+               <+> pprQuotedList bad_tvs)
 
        ; traceTc "tcTySig }" $ ppr (ex_tvs, prov') $$ ppr (univ_tvs, req') $$ ppr ty'
        ; let tpsi = TPSI{ patsig_name = name,
index 486e5f5..e39b0f5 100644 (file)
@@ -882,7 +882,7 @@ tcPatSynPat :: PatEnv -> Located Name -> PatSyn
             -> HsConPatDetails Name -> TcM a
             -> TcM (Pat TcId, a)
 tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
-  = do  { let (univ_tvs, ex_tvs, prov_theta, req_theta, arg_tys, ty) = patSynSig pat_syn
+  = do  { let (univ_tvs, req_theta, ex_tvs, prov_theta, arg_tys, ty) = patSynSig pat_syn
 
         ; (subst, univ_tvs') <- tcInstTyVars univ_tvs
 
index 5f7a4dc..872eb64 100644 (file)
@@ -830,17 +830,17 @@ it is assigned a *pattern type* of the form
 
 ::
 
-      pattern P :: CProv => CReq => t1 -> t2 -> ... -> tN -> t
+      pattern P :: CReq => CProf => t1 -> t2 -> ... -> tN -> t
 
 where ⟨CProv⟩ and ⟨CReq⟩ are type contexts, and ⟨t1⟩, ⟨t2⟩, ..., ⟨tN⟩
 and ⟨t⟩ are types. Notice the unusual form of the type, with two
 contexts ⟨CProv⟩ and ⟨CReq⟩:
 
--  ⟨CReq⟩ are the constraints *required* to match the pattern.
-
 -  ⟨CProv⟩ are the constraints *made available (provided)* by a
    successful pattern match.
 
+-  ⟨CReq⟩ are the constraints *required* to match the pattern.
+
 For example, consider
 
 ::
@@ -851,7 +851,7 @@ For example, consider
     f1 :: (Eq a, Num a) => T a -> String
     f1 (MkT 42 x) = show x
 
-    pattern ExNumPat :: (Show b) => (Num a, Eq a) => b -> T a
+    pattern ExNumPat :: (Num a, Eq a) => (Show b) => b -> T a
     pattern ExNumPat x = MkT 42 x
 
     f2 :: (Eq a, Num a) => T a -> String
@@ -871,7 +871,7 @@ Exactly the same reasoning applies to ``ExNumPat``: matching against
 
 Note also the following points
 
--  In the common case where ``CReq`` is empty, ``()``, it can be omitted
+-  In the common case where ``Prov`` is empty, ``()``, it can be omitted
    altogether.
 
 -  You may specify an explicit *pattern signature*, as we did for
@@ -892,14 +892,14 @@ Note also the following points
 
    ::
 
-         (CProv, CReq) => t1 -> t2 -> ... -> tN -> t
+         (CReq, CProv) => t1 -> t2 -> ... -> tN -> t
 
    So in the previous example, when used in an expression, ``ExNumPat``
    has type
 
    ::
 
-         ExNumPat :: (Show b, Num a, Eq a) => b -> T t
+         ExNumPat :: (Num a, Eq a, Show b) => b -> T t
 
    Notice that this is a tiny bit more restrictive than the expression
    ``MkT 42 x`` which would not require ``(Eq a)``.
@@ -911,8 +911,8 @@ Note also the following points
        data S a where
           S1 :: Bool -> S Bool
 
-       pattern P1 b = Just b  -- P1 ::             Bool -> Maybe Bool
-       pattern P2 b = S1 b    -- P2 :: (b~Bool) => Bool -> S b
+       pattern P1 b = Just b  -- P1 ::                   Bool -> Maybe Bool
+       pattern P2 b = S1 b    -- P2 :: () => (b~Bool) => Bool -> S b
 
        f :: Maybe a -> String
        f (P1 x) = "no no no"     -- Type-incorrect
index 7f8d57e..937a270 100644 (file)
@@ -1 +1,2 @@
-pattern P :: (Num t, Eq t1) => A t t1  -- Defined at T8776.hs:6:1
+pattern P :: () => (Num t, Eq t1) => A t t1
+       -- Defined at T8776.hs:6:1
index af98f49..f6a292a 100644 (file)
@@ -11,7 +11,7 @@ extractJust :: Maybe a -> (Bool, a)
 extractJust (Just a) = (True, a)
 extractJust _        = (False, undefined)
 
-pattern Just' :: () => (Showable a) => a -> (Maybe a)
+pattern Just' :: Showable a => a -> (Maybe a)
 pattern Just' a <- (extractJust -> (True, a)) where
   Just' a = Just a
 
index bed19f7..ec3c542 100644 (file)
@@ -5,7 +5,7 @@ module T10997a where
 data Exp ty where
   LitB :: Bool -> Exp Bool
 
-pattern Tru :: b ~ Bool => Exp b
+pattern Tru :: () => b ~ Bool => Exp b
 pattern Tru = LitB True
 
 
index 24147a2..379a8c8 100644 (file)
@@ -3,7 +3,7 @@
 
 module ShouldCompile where
 
-pattern Single :: () => (Show a) => a -> [a]
+pattern Single :: Show a => a -> [a]
 pattern Single x = [x]
 
 f :: (Show a) => [a] -> a
diff --git a/testsuite/tests/patsyn/should_fail/T11010.hs b/testsuite/tests/patsyn/should_fail/T11010.hs
new file mode 100644 (file)
index 0000000..c0bdb6e
--- /dev/null
@@ -0,0 +1,18 @@
+{-# LANGUAGE PatternSynonyms, ExistentialQuantification, GADTSyntax #-}
+
+module T11010 where
+
+data Expr a where
+  Fun :: String -> (a -> b) -> (Expr a -> Expr b)
+
+pattern IntFun :: (a ~ Int) => String -> (a -> b) -> (Expr a -> Expr b)
+pattern IntFun str f x = Fun str f x
+
+-- Alternative syntax for pattern synonyms:
+--   pattern
+--     Suc :: () => (a ~ Int) => Expr a -> Expr Int
+--     Suc n <- IntFun _     _     n where
+--     Suc n =  IntFun "suc" (+ 1) n
+pattern Suc :: (a ~ Int) => Expr a -> Expr Int
+pattern Suc n <- IntFun _     _     n where
+         Suc n =  IntFun "suc" (+ 1) n
diff --git a/testsuite/tests/patsyn/should_fail/T11010.stderr b/testsuite/tests/patsyn/should_fail/T11010.stderr
new file mode 100644 (file)
index 0000000..5f62b13
--- /dev/null
@@ -0,0 +1,8 @@
+
+T11010.hs:8:1: error:
+    The 'required' context ‘a ~ Int’
+      mentions existential type variable ‘a’
+
+T11010.hs:16:1: error:
+    The 'required' context ‘a ~ Int’
+      mentions existential type variable ‘a’
index de5d6db..846d2d3 100644 (file)
@@ -8,3 +8,4 @@ test('T9705-1', normal, compile_fail, [''])
 test('T9705-2', normal, compile_fail, [''])
 test('unboxed-bind', normal, compile_fail, [''])
 test('unboxed-wrapper-naked', normal, compile_fail, [''])
+test('T11010', normal, compile_fail, [''])
\ No newline at end of file
index 85b7ed6..18de4f2 160000 (submodule)
@@ -1 +1 @@
-Subproject commit 85b7ed6147c18611b5ef6b606f157086a8203e7d
+Subproject commit 18de4f2f992d3ed41eb83cb073e63304f0271dca