Commit 997312b0 authored by Rik Steenkamp's avatar Rik Steenkamp Committed by Ben Gamari

Add `PatSynSigSkol` and modify `PatSynCtxt`

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
parent 8048d51b
......@@ -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)
************************************************************************
* *
......
......@@ -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
......
......@@ -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
......
......@@ -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.
......
......@@ -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
......
......@@ -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
{-
************************************************************************
......
......@@ -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
......
......@@ -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’
......@@ -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
......
{-# 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
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
......@@ -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, [''])
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment