Add `PatSynSigSkol` and modify `PatSynCtxt`
authorRik Steenkamp <rik@ewps.nl>
Wed, 23 Mar 2016 15:17:27 +0000 (16:17 +0100)
committerBen Gamari <ben@smart-cactus.org>
Thu, 24 Mar 2016 09:53:27 +0000 (10:53 +0100)
As the type of a pattern synonym cannot in general be represented by a
value of type Type, we cannot use a value `SigSkol (PatSynCtxt n) (Check
ty)` to represent the signature of a pattern synonym (this causes
incorrect signatures to be printed in error messages). Therefore we now
represent it by a value `PatSynSigSkol n` (instead of incorrect
signatures we simply print no explicit signature).

Furthermore, we rename `PatSynCtxt` to `PatSynBuilderCtxt`, and use
`SigSkol (PatSynBuilderCtxt n) (Check ty)` to represent the type of a
bidirectional pattern synonym when used in an expression context.
Before, this type was represented by a value `SigSkol (PatSynCtxt n)
(Check ty)`, which caused incorrect error messages.

Also, in `mk_dict_err` of `typecheck\TcErrors.hs` we now distinguish
between all enclosing implications and "useful" enclosing implications,
for better error messages concerning pattern synonyms. See `Note [Useful
implications]`.

See the Phabricator page for examples.

Reviewers: mpickering, goldfire, simonpj, austin, bgamari

Reviewed By: bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D1967

GHC Trac Issues: #11667

12 files changed:
compiler/basicTypes/PatSyn.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcPatSyn.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcValidity.hs
testsuite/tests/patsyn/should_fail/T10873.stderr
testsuite/tests/patsyn/should_fail/T11039.stderr
testsuite/tests/patsyn/should_fail/T11667.hs [new file with mode: 0644]
testsuite/tests/patsyn/should_fail/T11667.stderr [new file with mode: 0644]
testsuite/tests/patsyn/should_fail/all.T

index d636430..9e87ecf 100644 (file)
@@ -241,6 +241,21 @@ This means that when typechecking an occurrence of P in an expression,
 we must remember that the builder has this void argument. This is
 done by TcPatSyn.patSynBuilderOcc.
 
+Note [Patterns synonyms and the data type Type]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The type of a pattern synonym is of the form (See Note
+[Pattern synonym signatures]):
+
+    forall univ_tvs. req => forall ex_tvs. prov => ...
+
+We cannot in general represent this by a value of type Type:
+
+ - if ex_tvs is empty, then req and prov cannot be distinguished from
+   each other
+ - if req is empty, then univ_tvs and ex_tvs cannot be distinguished
+   from each other, and moreover, prov is seen as the "required" context
+   (as it is the only context)
+
 
 ************************************************************************
 *                                                                      *
index 4b61575..790635d 100644 (file)
@@ -746,11 +746,14 @@ type UserGiven = ([EvVar], SkolemInfo, Bool, RealSrcSpan)
 
 getUserGivens :: ReportErrCtxt -> [UserGiven]
 -- One item for each enclosing implication
-getUserGivens (CEC {cec_encl = ctxt})
+getUserGivens (CEC {cec_encl = implics}) = getUserGivensFromImplics implics
+
+getUserGivensFromImplics :: [Implication] -> [UserGiven]
+getUserGivensFromImplics implics
   = reverse $
     [ (givens, info, no_eqs, tcl_loc env)
     | Implic { ic_given = givens, ic_env = env
-             , ic_no_eqs = no_eqs, ic_info = info } <- ctxt
+             , ic_no_eqs = no_eqs, ic_info = info } <- implics
     , not (null givens) ]
 
 {-
@@ -1816,7 +1819,7 @@ mk_dict_err :: ReportErrCtxt -> (Ct, ClsInstLookupResult)
             -> TcM (ReportErrCtxt, SDoc)
 -- Report an overlap error if this class constraint results
 -- from an overlap (returning Left clas), otherwise return (Right pred)
-mk_dict_err ctxt (ct, (matches, unifiers, unsafe_overlapped))
+mk_dict_err ctxt@(CEC {cec_encl = implics}) (ct, (matches, unifiers, unsafe_overlapped))
   | null matches  -- No matches but perhaps several unifiers
   = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
        ; candidate_insts <- get_candidate_instances
@@ -1833,8 +1836,16 @@ mk_dict_err ctxt (ct, (matches, unifiers, unsafe_overlapped))
     (clas, tys)   = getClassPredTys pred
     ispecs        = [ispec | (ispec, _) <- matches]
     unsafe_ispecs = [ispec | (ispec, _) <- unsafe_overlapped]
-    givens        = getUserGivens ctxt
+    givens        = getUserGivensFromImplics useful_implics
     all_tyvars    = all isTyVarTy tys
+    useful_implics = filter is_useful_implic implics
+      -- See Note [Useful implications]
+
+    is_useful_implic implic
+      | (PatSynSigSkol name) <- ic_info implic
+      , ProvCtxtOrigin (PSB {psb_id = (L _ name')}) <- orig
+      , name == name' = False
+    is_useful_implic _ = True
 
     get_candidate_instances :: TcM [ClsInst]
     -- See Note [Report candidate instances]
@@ -1907,11 +1918,7 @@ mk_dict_err ctxt (ct, (matches, unifiers, unsafe_overlapped))
 
         in_other_words
           | not lead_with_ambig
-          , ProvCtxtOrigin PSB{ psb_id  = (L _ name)
-                              , psb_def = (L _ pat) } <- orig
-            -- Here we check if the "required" context is empty, otherwise
-            -- the "In other words" is not strictly true
-          , null [ n | (_, SigSkol (PatSynCtxt n) _, _, _) <- givens, name == n ]
+          , ProvCtxtOrigin PSB{ psb_def = (L _ pat) } <- orig
           = vcat [ text "In other words, a successful match on the pattern"
                  , nest 2 $ ppr pat
                  , text "does not provide the constraint" <+> pprParendType pred ]
@@ -1924,7 +1931,7 @@ mk_dict_err ctxt (ct, (matches, unifiers, unsafe_overlapped))
 
     add_to_ctxt_fixes has_ambig_tvs
       | not has_ambig_tvs && all_tyvars
-      , (orig:origs) <- usefulContext ctxt ct
+      , (orig:origs) <- usefulContext useful_implics pred
       = [sep [ text "add" <+> pprParendType pred
                <+> text "to the context of"
              , nest 2 $ ppr_skol orig $$
@@ -2051,18 +2058,48 @@ from being solved:
   - Lastly, I don't want to mess with error reporting for
     unknown runtime types so we just fall back to the old message there.
 Once these conditions are satisfied, we can safely say that ambiguity prevents
-the constraint from being solved. -}
+the constraint from being solved.
+
+Note [Useful implications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+In most situations we call all enclosing implications "useful". There is one
+exception, and that is when the constraint that causes the error is from the
+"provided" context of a pattern synonym declaration. Then we only call the
+enclosing implications that are /not/ from the "required" context of the
+declaration "useful".
+
+The reason for this is that a "provided" constraint should be deducible from
+a successful pattern match, not from the "required" context. Constraints that
+are deducible from the "required" context are already available at every usage
+site of the pattern synonym.
+
+This distinction between all and "useful" implications solves two problems.
+First, we never tell the user that we could not deduce a "provided"
+constraint from the "required" context. Second, we never give a possible fix
+that suggests to add a "provided" constraint to the "required" context.
+
+For example, without this distinction the following code gives a bad error
+message (showing both problems):
 
+  pattern Pat :: Eq a => Show a => a -> Maybe a
+  pattern Pat x <- Just x
 
-usefulContext :: ReportErrCtxt -> Ct -> [SkolemInfo]
-usefulContext ctxt ct
-  = go (cec_encl ctxt)
+  error: Could not deduce (Show a) ... from the context: (Eq a)
+         ... Possible fix: add (Show a) to the context of
+         the type signature for pattern synonym `Pat' ...
+
+-}
+
+
+usefulContext :: [Implication] -> PredType -> [SkolemInfo]
+usefulContext implics pred
+  = go implics
   where
-    pred_tvs = tyCoVarsOfType $ ctPred ct
+    pred_tvs = tyCoVarsOfType pred
     go [] = []
     go (ic : ics)
        | implausible ic = rest
-       | otherwise      = ic_info ic : rest
+       | otherwise      = correct_info (ic_info ic) : rest
        where
           -- Stop when the context binds a variable free in the predicate
           rest | any (`elemVarSet` pred_tvs) (ic_skols ic) = []
@@ -2073,18 +2110,13 @@ usefulContext ctxt ct
       | implausible_info (ic_info ic) = True
       | otherwise                     = False
 
-    implausible_info (SigSkol (InfSigCtxt {}  ) _) = True
-    implausible_info (SigSkol (PatSynCtxt name) _)
-      | (ProvCtxtOrigin PSB{ psb_id = (L _ name') }) <- ctOrigin ct
-      , name == name'                              = True
-    implausible_info _                             = False
-    -- Do not suggest adding constraints to an *inferred* type signature, or to
-    -- a pattern synonym signature when its "provided" context is the origin of
-    -- the wanted constraint.  For example,
-    --   pattern Pat :: () => Show a => a -> Maybe a
-    --   pattern Pat x = Just x
-    -- This declaration should not give the possible fix:
-    --   add (Show a) to the "required" context of the signature for `Pat'
+    implausible_info (SigSkol (InfSigCtxt {}) _) = True
+    implausible_info _                           = False
+    -- Do not suggest adding constraints to an *inferred* type signature
+
+    correct_info (SigSkol (PatSynBuilderCtxt n) _) = PatSynSigSkol n
+    correct_info info                              = info
+    -- See example 4 in ticket #11667
 
 show_fixes :: [SDoc] -> SDoc
 show_fixes []     = empty
index cdc4ca0..8196195 100644 (file)
@@ -242,8 +242,7 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
                       , patsig_arg_tys    = arg_tys,    patsig_body_ty = pat_ty }
   = addPatSynCtxt lname $
     do { let origin     = ProvCtxtOrigin psb
-             skol_info  = SigSkol (PatSynCtxt name) (mkCheckExpType $
-                                                     mkFunTys arg_tys pat_ty)
+             skol_info  = PatSynSigSkol name
              decl_arity = length arg_names
              ty_arity   = length arg_tys
              (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
@@ -710,7 +709,7 @@ get_builder_sig sig_fun name builder_id need_dummy_arg
                  , sig_theta = req ++ prov
                  , sig_tau   = add_void need_dummy_arg $
                                mkFunTys arg_tys body_ty
-                 , sig_ctxt  = PatSynCtxt name
+                 , sig_ctxt  = PatSynBuilderCtxt name
                  , sig_loc   = getSrcSpan name })
   | otherwise
   = -- No signature, so fake up a TcIdSigInfo from the builder Id
index d89ddf2..84bf2db 100644 (file)
@@ -2577,6 +2577,11 @@ data SkolemInfo
             ExpType             -- a programmer-supplied type signature
                                 -- Location of the binding site is on the TyVar
 
+  | PatSynSigSkol Name  -- Bound by a programmer-supplied type signature of a pattern
+                        -- synonym. Here we cannot use a SigSkol, see
+                        -- Note [Patterns synonyms and the data type Type] in
+                        -- basicTypes\PatSyn.hs
+
   | ClsSkol Class       -- Bound at a class decl
 
   | DerivSkol Type      -- Bound by a 'deriving' clause;
@@ -2640,6 +2645,8 @@ pprSkolInfo (InferSkol ids)   = sep [ text "the inferred type of"
                                     , vcat [ ppr name <+> dcolon <+> ppr ty
                                            | (name,ty) <- ids ]]
 pprSkolInfo (UnifyForAllSkol ty) = text "the type" <+> ppr ty
+pprSkolInfo (PatSynSigSkol name) = text "the type signature of pattern synonym"
+                                   <+> quotes (ppr name)
 
 -- UnkSkol
 -- For type variables the others are dealt with by pprSkolTvBinding.
index 9633898..51a3588 100644 (file)
@@ -1297,9 +1297,9 @@ warnRedundantGivens (SigSkol ctxt _)
        FunSigCtxt _ warn_redundant -> warn_redundant
        ExprSigCtxt                 -> True
        _                           -> False
-  -- To think about: do we want to report redundant givens for
-  -- pattern synonyms, PatSynCtxt? c.f Trac #9953, comment:21.
 
+  -- To think about: do we want to report redundant givens for
+  -- pattern synonyms, PatSynSigSkol? c.f Trac #9953, comment:21.
 warnRedundantGivens (InstSkol {}) = True
 warnRedundantGivens _             = False
 
index 08e2335..10bf575 100644 (file)
@@ -473,8 +473,7 @@ data UserTypeCtxt
   | TypeAppCtxt         -- Visible type application
   | ConArgCtxt Name     -- Data constructor argument
   | TySynCtxt Name      -- RHS of a type synonym decl
-  | PatSynCtxt Name     -- Type sig for a pattern synonym
-                        --   eg  pattern C :: Int -> T
+  | PatSynBuilderCtxt Name -- Type sig for the builder of a bidirectional pattern synonym
   | PatSigCtxt          -- Type sig in pattern
                         --   eg  f (x::t) = ...
                         --   or  (x::t, y) = e
@@ -659,7 +658,6 @@ pprUserTypeCtxt ExprSigCtxt       = text "an expression type signature"
 pprUserTypeCtxt TypeAppCtxt       = text "a type argument"
 pprUserTypeCtxt (ConArgCtxt c)    = text "the type of the constructor" <+> quotes (ppr c)
 pprUserTypeCtxt (TySynCtxt c)     = text "the RHS of the type synonym" <+> quotes (ppr c)
-pprUserTypeCtxt (PatSynCtxt c)    = text "the type signature for pattern synonym" <+> quotes (ppr c)
 pprUserTypeCtxt ThBrackCtxt       = text "a Template Haskell quotation [t|...|]"
 pprUserTypeCtxt PatSigCtxt        = text "a pattern type signature"
 pprUserTypeCtxt ResSigCtxt        = text "a result type signature"
@@ -672,6 +670,9 @@ pprUserTypeCtxt GhciCtxt          = text "a type in a GHCi command"
 pprUserTypeCtxt (ClassSCCtxt c)   = text "the super-classes of class" <+> quotes (ppr c)
 pprUserTypeCtxt SigmaCtxt         = text "the context of a polymorphic type"
 pprUserTypeCtxt (DataTyCtxt tc)   = text "the context of the data type declaration for" <+> quotes (ppr tc)
+pprUserTypeCtxt (PatSynBuilderCtxt n)
+  = vcat [ text "the type signature for bidirectional pattern synonym" <+> quotes (ppr n)
+         , text "when used in an expression context" ]
 
 pprSigCtxt :: UserTypeCtxt -> SDoc -> SDoc -> SDoc
 -- (pprSigCtxt ctxt <extra> <type>)
@@ -690,11 +691,11 @@ pprSigCtxt ctxt extra pp_ty
   where
 
 isSigMaybe :: UserTypeCtxt -> Maybe Name
-isSigMaybe (FunSigCtxt n _) = Just n
-isSigMaybe (ConArgCtxt n)   = Just n
-isSigMaybe (ForSigCtxt n)   = Just n
-isSigMaybe (PatSynCtxt n)   = Just n
-isSigMaybe _                = Nothing
+isSigMaybe (FunSigCtxt n _)      = Just n
+isSigMaybe (ConArgCtxt n)        = Just n
+isSigMaybe (ForSigCtxt n)        = Just n
+isSigMaybe (PatSynBuilderCtxt n) = Just n
+isSigMaybe _                     = Nothing
 
 {-
 ************************************************************************
index dbb3d74..9a68c92 100644 (file)
@@ -451,9 +451,9 @@ forAllAllowed _                         = False
 representationPolymorphismForbidden :: UserTypeCtxt -> Bool
 representationPolymorphismForbidden = go
   where
-    go (ConArgCtxt _) = True     -- A rep-polymorphic datacon won't be useful
-    go (PatSynCtxt _) = True     -- Similar to previous case
-    go _              = False    -- Other cases are caught by zonker
+    go (ConArgCtxt _)        = True     -- A rep-polymorphic datacon won't be useful
+    go (PatSynBuilderCtxt _) = True     -- Similar to previous case
+    go _                     = False    -- Other cases are caught by zonker
 
 ----------------------------------------
 -- | Fail with error message if the type is unlifted
@@ -867,22 +867,22 @@ check_class_pred env dflags ctxt pred cls tys
 -------------------------
 okIPCtxt :: UserTypeCtxt -> Bool
   -- See Note [Implicit parameters in instance decls]
-okIPCtxt (FunSigCtxt {})    = True
-okIPCtxt (InfSigCtxt {})    = True
-okIPCtxt ExprSigCtxt        = True
-okIPCtxt TypeAppCtxt        = True
-okIPCtxt PatSigCtxt         = True
-okIPCtxt ResSigCtxt         = True
-okIPCtxt GenSigCtxt         = True
-okIPCtxt (ConArgCtxt {})    = True
-okIPCtxt (ForSigCtxt {})    = True  -- ??
-okIPCtxt ThBrackCtxt        = True
-okIPCtxt GhciCtxt           = True
-okIPCtxt SigmaCtxt          = True
-okIPCtxt (DataTyCtxt {})    = True
-okIPCtxt (PatSynCtxt {})    = True
-okIPCtxt (TySynCtxt {})     = True   -- e.g.   type Blah = ?x::Int
-                                     -- Trac #11466
+okIPCtxt (FunSigCtxt {})        = True
+okIPCtxt (InfSigCtxt {})        = True
+okIPCtxt ExprSigCtxt            = True
+okIPCtxt TypeAppCtxt            = True
+okIPCtxt PatSigCtxt             = True
+okIPCtxt ResSigCtxt             = True
+okIPCtxt GenSigCtxt             = True
+okIPCtxt (ConArgCtxt {})        = True
+okIPCtxt (ForSigCtxt {})        = True  -- ??
+okIPCtxt ThBrackCtxt            = True
+okIPCtxt GhciCtxt               = True
+okIPCtxt SigmaCtxt              = True
+okIPCtxt (DataTyCtxt {})        = True
+okIPCtxt (PatSynBuilderCtxt {}) = True
+okIPCtxt (TySynCtxt {})         = True   -- e.g.   type Blah = ?x::Int
+                                         -- Trac #11466
 
 okIPCtxt (ClassSCCtxt {})  = False
 okIPCtxt (InstDeclCtxt {}) = False
index 766b2e0..6eb925b 100644 (file)
@@ -12,13 +12,12 @@ T10873.hs:10:23: error:
     • Could not deduce (Show a)
         arising from the "provided" constraints claimed by
           the signature of ‘Pat2’
-      from the context: Enum a
-        bound by the type signature for pattern synonym ‘Pat2’:
-                   a -> T a
-        at T10873.hs:10:9-12
-      or from: Ord a
+      from the context: Ord a
         bound by a pattern with constructor:
                    MkT :: forall a. Ord a => a -> T a,
                  in a pattern synonym declaration
         at T10873.hs:10:19-23
+      In other words, a successful match on the pattern
+        MkT x
+      does not provide the constraint (Show a)
     • In the declaration for pattern synonym ‘Pat2’
index 2c7c663..eea6257 100644 (file)
@@ -2,9 +2,7 @@
 T11039.hs:8:15: error:
     • Couldn't match type ‘f’ with ‘A’
       ‘f’ is a rigid type variable bound by
-        the type signature for pattern synonym ‘Q’:
-          forall (f :: * -> *) a. a -> f a
-        at T11039.hs:7:14
+        the type signature of pattern synonym ‘Q’ at T11039.hs:7:14
       Expected type: f a
         Actual type: A a
     • In the pattern: A a
diff --git a/testsuite/tests/patsyn/should_fail/T11667.hs b/testsuite/tests/patsyn/should_fail/T11667.hs
new file mode 100644 (file)
index 0000000..f2437fa
--- /dev/null
@@ -0,0 +1,31 @@
+{-# LANGUAGE PatternSynonyms, GADTs #-}
+module T11667 where
+
+{-
+The following four pattern synonym declarations should give valid
+error messages
+-}
+
+-- Check if we mention no explicit type signature (or the correct
+-- signature "Eq a => Maybe a")
+pattern Pat1 :: Eq a => Maybe a
+pattern Pat1 <- Just 42
+
+-- Check if we mention no explicit type signature (or the correct
+-- signature "forall b. () => forall a. b ~ Bool => a -> b -> (b, T)")
+data T where MkT :: a -> T
+pattern Pat2 :: () => b ~ Bool => a -> b -> (b, T)
+pattern Pat2 x y = (y, MkT x)
+
+-- Check if we do not tell the user that we could not deduce (Show a)
+-- from the "required" context. Also, check if we do not give the
+-- possible fix that suggests to add (Show a) to the "required" context.
+pattern Pat3 :: Eq a => Show a => a -> Maybe a
+pattern Pat3 x <- Just x
+
+-- Check if we return a valid error message concerning the missing
+-- constraint (Num a) when the bidirectional pattern synonym is used
+-- in an expression context
+data S a where MkS :: (Num a, Show a) => a -> S a
+pattern Pat4 :: (Eq a) => (Show a) => S a
+pattern Pat4 = MkS 42
diff --git a/testsuite/tests/patsyn/should_fail/T11667.stderr b/testsuite/tests/patsyn/should_fail/T11667.stderr
new file mode 100644 (file)
index 0000000..6befe13
--- /dev/null
@@ -0,0 +1,43 @@
+
+T11667.hs:12:22: error:
+    • Could not deduce (Num a) arising from the literal ‘42’
+      from the context: Eq a
+        bound by the type signature of pattern synonym ‘Pat1’
+        at T11667.hs:12:9-12
+      Possible fix:
+        add (Num a) to the context of
+          the type signature of pattern synonym ‘Pat1’
+    • In the pattern: 42
+      In the pattern: Just 42
+      In the declaration for pattern synonym ‘Pat1’
+
+T11667.hs:18:28: error:
+    • Couldn't match type ‘b’ with ‘Bool’
+        arising from the "provided" constraints claimed by
+          the signature of ‘Pat2’
+      ‘b’ is a rigid type variable bound by
+        the type signature of pattern synonym ‘Pat2’ at T11667.hs:17:17
+    • In the declaration for pattern synonym ‘Pat2’
+    • Relevant bindings include y :: b (bound at T11667.hs:18:21)
+
+T11667.hs:24:24: error:
+    • No instance for (Show a)
+        arising from the "provided" constraints claimed by
+          the signature of ‘Pat3’
+      In other words, a successful match on the pattern
+        Just x
+      does not provide the constraint (Show a)
+    • In the declaration for pattern synonym ‘Pat3’
+
+T11667.hs:31:16: error:
+    • Could not deduce (Num a) arising from a use of ‘MkS’
+      from the context: (Eq a, Show a)
+        bound by the type signature for bidirectional pattern synonym ‘Pat4’
+                 when used in an expression context:
+                   (Eq a, Show a) => S a
+        at T11667.hs:31:1-21
+      Possible fix:
+        add (Num a) to the context of
+          the type signature of pattern synonym ‘Pat4’
+    • In the expression: MkS 42
+      In an equation for ‘$bPat4’: $bPat4 = MkS 42
index a9ba447..658a5c0 100644 (file)
@@ -30,3 +30,4 @@ test('export-ps-rec-sel', normal, compile_fail, [''])
 test('T11053', normal, compile, ['-fwarn-missing-pattern-synonym-signatures'])
 test('T10426', normal, compile_fail, [''])
 test('T11265', normal, compile_fail, [''])
+test('T11667', normal, compile_fail, [''])