summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSimon Peyton Jones <simonpj@microsoft.com>2022-05-06 11:01:01 +0100
committerMarge Bot <ben+marge-bot@smart-cactus.org>2022-05-10 20:47:28 -0400
commitbdc99cc22c903d15eb7f4cd8da4b37d307179808 (patch)
treede5908cae6a57c0bf487b7ddde83d9288377287a
parent35da81f8fb04d905ed7fc2f2a435530b142c983d (diff)
downloadhaskell-bdc99cc22c903d15eb7f4cd8da4b37d307179808.tar.gz
Check for uninferrable variables in tcInferPatSynDecl
This fixes #21479 See Note [Unquantified tyvars in a pattern synonym] While doing this, I found that some error messages pointed at the pattern synonym /name/, rather than the /declaration/ so I widened the SrcSpan to encompass the declaration.
-rw-r--r--compiler/GHC/Tc/Gen/Bind.hs4
-rw-r--r--compiler/GHC/Tc/TyCl/PatSyn.hs57
-rw-r--r--compiler/GHC/Tc/TyCl/PatSyn.hs-boot10
-rw-r--r--compiler/GHC/Tc/Utils/TcMType.hs31
-rw-r--r--testsuite/tests/linear/should_fail/LinearPatSyn2.stderr2
-rw-r--r--testsuite/tests/patsyn/should_fail/T11667.stderr2
-rw-r--r--testsuite/tests/patsyn/should_fail/T14507.stderr2
-rw-r--r--testsuite/tests/patsyn/should_fail/T14552.stderr2
-rw-r--r--testsuite/tests/patsyn/should_fail/T15685.stderr2
-rw-r--r--testsuite/tests/patsyn/should_fail/T21479.hs13
-rw-r--r--testsuite/tests/patsyn/should_fail/T21479.stderr5
-rw-r--r--testsuite/tests/patsyn/should_fail/all.T1
12 files changed, 88 insertions, 43 deletions
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index 4c5fa5aaa8..14f7bbf6b5 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -429,9 +429,9 @@ tc_single :: forall thing.
-> LHsBind GhcRn -> IsGroupClosed -> TcM thing
-> TcM (LHsBinds GhcTc, thing)
tc_single _top_lvl sig_fn prag_fn
- (L _ (PatSynBind _ psb@PSB{ psb_id = L _ name }))
+ (L loc (PatSynBind _ psb))
_ thing_inside
- = do { (aux_binds, tcg_env) <- tcPatSynDecl psb (sig_fn name) prag_fn
+ = do { (aux_binds, tcg_env) <- tcPatSynDecl (L loc psb) sig_fn prag_fn
; thing <- setGblEnv tcg_env thing_inside
; return (aux_binds, thing)
}
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs
index ce3025bafa..45810f5d9f 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs
@@ -76,13 +76,16 @@ import Data.List( partition, mapAccumL )
************************************************************************
-}
-tcPatSynDecl :: PatSynBind GhcRn GhcRn
- -> Maybe TcSigInfo
+tcPatSynDecl :: LocatedA (PatSynBind GhcRn GhcRn)
+ -> TcSigFun
-> TcPragEnv -- See Note [Pragmas for pattern synonyms]
-> TcM (LHsBinds GhcTc, TcGblEnv)
-tcPatSynDecl psb mb_sig prag_fn
- = recoverM (recoverPSB psb) $
- case mb_sig of
+tcPatSynDecl (L loc psb@(PSB { psb_id = L _ name })) sig_fn prag_fn
+ = setSrcSpanA loc $
+ addErrCtxt (text "In the declaration for pattern synonym"
+ <+> quotes (ppr name)) $
+ recoverM (recoverPSB psb) $
+ case (sig_fn name) of
Nothing -> tcInferPatSynDecl psb prag_fn
Just (TcPatSynSig tpsi) -> tcCheckPatSynDecl psb tpsi prag_fn
_ -> panic "tcPatSynDecl"
@@ -145,8 +148,7 @@ tcInferPatSynDecl :: PatSynBind GhcRn GhcRn
tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details
, psb_def = lpat, psb_dir = dir })
prag_fn
- = addPatSynCtxt lname $
- do { traceTc "tcInferPatSynDecl {" $ ppr name
+ = do { traceTc "tcInferPatSynDecl {" $ ppr name
; let (arg_names, is_infix) = collectPatSynArgInfo details
; (tclvl, wanted, ((lpat', args), pat_ty))
@@ -188,6 +190,16 @@ tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details
, not (isEmptyDVarSet bad_cos) ]
; mapM_ dependentArgErr bad_args
+ -- Report un-quantifiable type variables:
+ -- see Note [Unquantified tyvars in a pattern synonym]
+ ; dvs <- candidateQTyVarsOfTypes prov_theta
+ ; let mk_doc tidy_env
+ = do { (tidy_env2, theta) <- zonkTidyTcTypes tidy_env prov_theta
+ ; return ( tidy_env2
+ , sep [ text "the provided context:"
+ , pprTheta theta ] ) }
+ ; doNotQuantifyTyVars dvs mk_doc
+
; traceTc "tcInferPatSynDecl }" $ (ppr name $$ ppr ex_tvs)
; rec_fields <- lookupConstructorFields name
; tc_patsyn_finish lname dir is_infix lpat' prag_fn
@@ -345,6 +357,27 @@ But we simply don't allow that in types. Maybe one day but not now.
How to detect this situation? We just look for free coercion variables
in the types of any of the arguments to the matcher. The error message
is not very helpful, but at least we don't get a Lint error.
+
+Note [Unquantified tyvars in a pattern synonym]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (#21479)
+
+ data T a where MkT :: Int -> T Char -- A GADT
+ foo :: forall b. Bool -> T b -- Somewhat strange type
+
+ pattern T1 <- (foo -> MkT)
+
+In the view pattern, foo is instantiated, let's say b :-> b0
+where b0 is a unification variable. Then matching the GADT
+MkT will add the "provided" constraint b0~Char, so we might infer
+ pattern T1 :: () => (b0~Char) => Int -> Bool
+
+Nothing constrains that `b0`. We don't want to quantify over it.
+We don't want to to zonk to Any (we don't like Any showing up in
+user-visible types). So we want to error here. See
+Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
+
+Hence the call to doNotQuantifyTyVars here.
-}
tcCheckPatSynDecl :: PatSynBind GhcRn GhcRn
@@ -358,8 +391,7 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
, patsig_ex_bndrs = explicit_ex_bndrs, patsig_prov = prov_theta
, patsig_body_ty = sig_body_ty }
prag_fn
- = addPatSynCtxt lname $
- do { traceTc "tcCheckPatSynDecl" $
+ = do { traceTc "tcCheckPatSynDecl" $
vcat [ ppr implicit_bndrs, ppr explicit_univ_bndrs, ppr req_theta
, ppr explicit_ex_bndrs, ppr prov_theta, ppr sig_body_ty ]
@@ -646,13 +678,6 @@ collectPatSynArgInfo details =
InfixCon name1 name2 -> (map unLoc [name1, name2], True)
RecCon names -> (map (unLoc . recordPatSynPatVar) names, False)
-addPatSynCtxt :: LocatedN Name -> TcM a -> TcM a
-addPatSynCtxt (L loc name) thing_inside
- = setSrcSpanA loc $
- addErrCtxt (text "In the declaration for pattern synonym"
- <+> quotes (ppr name)) $
- thing_inside
-
wrongNumberOfParmsErr :: Name -> Arity -> Arity -> TcM a
wrongNumberOfParmsErr name decl_arity missing
= failWithTc $ TcRnUnknownMessage $ mkPlainError noHints $
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs-boot b/compiler/GHC/Tc/TyCl/PatSyn.hs-boot
index 844a4c394d..5a16a55cd7 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs-boot
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs-boot
@@ -1,14 +1,14 @@
module GHC.Tc.TyCl.PatSyn where
import GHC.Hs ( PatSynBind, LHsBinds )
-import GHC.Tc.Types ( TcM, TcSigInfo )
+import GHC.Tc.Types ( TcM )
import GHC.Tc.Utils.Monad ( TcGblEnv)
import GHC.Hs.Extension ( GhcRn, GhcTc )
-import Data.Maybe ( Maybe )
-import GHC.Tc.Gen.Sig ( TcPragEnv )
+import GHC.Tc.Gen.Sig ( TcPragEnv, TcSigFun )
+import GHC.Parser.Annotation( LocatedA )
-tcPatSynDecl :: PatSynBind GhcRn GhcRn
- -> Maybe TcSigInfo
+tcPatSynDecl :: LocatedA (PatSynBind GhcRn GhcRn)
+ -> TcSigFun
-> TcPragEnv
-> TcM (LHsBinds GhcTc, TcGblEnv)
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 21954240d6..5561e9064e 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -1947,35 +1947,34 @@ skolemiseUnboundMetaTyVar skol_info tv
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
- type C :: Type -> Type -> Constraint
+* type C :: Type -> Type -> Constraint
class (forall a. a b ~ a c) => C b c
-or
+* type T = forall a. Proxy a
- type T = forall a. Proxy a
+* data (forall a. a b ~ a c) => T b c
-or
+* type instance F Int = Proxy Any
+ where Any :: forall k. k
- data (forall a. a b ~ a c) => T b c
-
-We will infer a :: Type -> kappa... but then we get no further information
-on kappa. What to do?
+In the first three cases we will infer a :: Type -> kappa, but then
+we get no further information on kappa. In the last, we will get
+ Proxy kappa Any
+but again will get no further info on kappa.
+What do do?
A. We could choose kappa := Type. But this only works when the kind of kappa
is Type (true in this example, but not always).
B. We could default to Any.
C. We could quantify.
D. We could error.
-We choose (D), as described in #17567. Discussion of alternatives is below.
+We choose (D), as described in #17567, and implement this choice in
+doNotQuantifyTyVars. Dicsussion of alternativs A-C is below.
NB: this is all rather similar to, but sadly not the same as
Note [Naughty quantification candidates]
-(One last example: type instance F Int = Proxy Any, where the unconstrained
-kind variable is the inferred kind of Any. The four examples here illustrate
-all cases in which this Note applies.)
-
To do this, we must take an extra step before doing the final zonk to create
e.g. a TyCon. (There is no problem in the final term-level zonk. See the
section on alternative (B) below.) This extra step is needed only for
@@ -1990,7 +1989,7 @@ RuntimeRep and Multiplicity variables.)
Because no meta-variables remain after quantifying or erroring, we perform
the zonk with NoFlexi, which panics upon seeing a meta-variable.
-Alternatives not implemented:
+Alternatives A-C, not implemented:
A. As stated above, this works only sometimes. We might have a free
meta-variable of kind Nat, for example.
@@ -2067,7 +2066,9 @@ doNotQuantifyTyVars dvs where_found
; unless (null leftover_metas) $
do { let (tidy_env1, tidied_tvs) = tidyOpenTyCoVars emptyTidyEnv leftover_metas
; (tidy_env2, where_doc) <- where_found tidy_env1
- ; let msg = TcRnUnknownMessage $ mkPlainError noHints $ pprWithExplicitKindsWhen True $
+ ; let msg = TcRnUnknownMessage $
+ mkPlainError noHints $
+ pprWithExplicitKindsWhen True $
vcat [ text "Uninferrable type variable"
<> plural tidied_tvs
<+> pprWithCommas pprTyVar tidied_tvs
diff --git a/testsuite/tests/linear/should_fail/LinearPatSyn2.stderr b/testsuite/tests/linear/should_fail/LinearPatSyn2.stderr
index 1360983907..78b3ee52f6 100644
--- a/testsuite/tests/linear/should_fail/LinearPatSyn2.stderr
+++ b/testsuite/tests/linear/should_fail/LinearPatSyn2.stderr
@@ -1,5 +1,5 @@
-LinearPatSyn2.hs:6:9: error:
+LinearPatSyn2.hs:6:1: error:
• Pattern synonyms do not support linear fields (GHC #18806):
x %1 -> Maybe x
• In the declaration for pattern synonym ‘J’
diff --git a/testsuite/tests/patsyn/should_fail/T11667.stderr b/testsuite/tests/patsyn/should_fail/T11667.stderr
index f4dafc0f28..e08299b235 100644
--- a/testsuite/tests/patsyn/should_fail/T11667.stderr
+++ b/testsuite/tests/patsyn/should_fail/T11667.stderr
@@ -3,7 +3,7 @@ T11667.hs:12:22: error:
• Could not deduce (Num a) arising from the literal ‘42’
from the context: Eq a
bound by the signature for pattern synonym ‘Pat1’
- at T11667.hs:12:9-12
+ at T11667.hs:12:1-23
Possible fix:
add (Num a) to the "required" context of
the signature for pattern synonym ‘Pat1’
diff --git a/testsuite/tests/patsyn/should_fail/T14507.stderr b/testsuite/tests/patsyn/should_fail/T14507.stderr
index beeb4de685..d3dfa0a04f 100644
--- a/testsuite/tests/patsyn/should_fail/T14507.stderr
+++ b/testsuite/tests/patsyn/should_fail/T14507.stderr
@@ -1,5 +1,5 @@
-T14507.hs:21:9: error:
+T14507.hs:21:1: error:
• Iceland Jack! Iceland Jack! Stop torturing me!
Pattern-bound variable x :: TypeRep a
has a type that mentions pattern-bound coercion: co
diff --git a/testsuite/tests/patsyn/should_fail/T14552.stderr b/testsuite/tests/patsyn/should_fail/T14552.stderr
index 34ee266cdd..92c1adb57b 100644
--- a/testsuite/tests/patsyn/should_fail/T14552.stderr
+++ b/testsuite/tests/patsyn/should_fail/T14552.stderr
@@ -1,5 +1,5 @@
-T14552.hs:22:9: error:
+T14552.hs:22:1: error:
• Cannot generalise type; skolem ‘k’ would escape its scope
if I tried to quantify (t0 :: k) in this type:
forall k (w :: k --> *). Exp a0 (F @k @(*) w t0)
diff --git a/testsuite/tests/patsyn/should_fail/T15685.stderr b/testsuite/tests/patsyn/should_fail/T15685.stderr
index afc6d45de4..204260a9e4 100644
--- a/testsuite/tests/patsyn/should_fail/T15685.stderr
+++ b/testsuite/tests/patsyn/should_fail/T15685.stderr
@@ -9,7 +9,7 @@ T15685.hs:13:24: error:
at T15685.hs:13:19-26
‘k’ is a rigid type variable bound by
the inferred type of HereNil :: NS f as
- at T15685.hs:13:9-15
+ at T15685.hs:13:1-26
• In the pattern: Nil
In the pattern: Here Nil
In the declaration for pattern synonym ‘HereNil’
diff --git a/testsuite/tests/patsyn/should_fail/T21479.hs b/testsuite/tests/patsyn/should_fail/T21479.hs
new file mode 100644
index 0000000000..889e811e88
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T21479.hs
@@ -0,0 +1,13 @@
+{-# Language PatternSynonyms #-}
+{-# Language ViewPatterns #-}
+{-# Language GADTs #-}
+
+module T21479 where
+
+data T a where
+ MkT :: T Int
+
+foo :: () -> T a
+foo = foo
+
+pattern T1 <- (foo -> MkT) \ No newline at end of file
diff --git a/testsuite/tests/patsyn/should_fail/T21479.stderr b/testsuite/tests/patsyn/should_fail/T21479.stderr
new file mode 100644
index 0000000000..07601492a8
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T21479.stderr
@@ -0,0 +1,5 @@
+
+T21479.hs:13:1: error:
+ • Uninferrable type variable a0 in
+ the provided context: (a0 :: *) ~ (Int :: *)
+ • In the declaration for pattern synonym ‘T1’
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index 8993e5c4bf..2db852a35b 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -48,3 +48,4 @@ test('T15694', normal, compile_fail, [''])
test('T16900', normal, compile_fail, ['-fdiagnostics-show-caret'])
test('T14552', normal, compile_fail, [''])
test('T18856', normal, compile_fail, ['-fdiagnostics-show-caret'])
+test('T21479', normal, compile_fail, [''])