[commit: ghc] master: Fix deep, dark corner of pattern synonyms (307d1df)
git at git.haskell.org
git at git.haskell.org
Thu Jan 4 17:41:13 UTC 2018
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/307d1dfe1d705379eafad6dba65e651ae3465cda/ghc
>---------------------------------------------------------------
commit 307d1dfe1d705379eafad6dba65e651ae3465cda
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Thu Jan 4 17:18:15 2018 +0000
Fix deep, dark corner of pattern synonyms
Trac #14552 showed a very obscure case where we can't infer a
good pattern-synonym type.
The error message is horrible, but at least we no longer crash
and burn.
>---------------------------------------------------------------
307d1dfe1d705379eafad6dba65e651ae3465cda
compiler/typecheck/TcPatSyn.hs | 50 ++++++++++++++++++++++++
testsuite/tests/patsyn/should_fail/T14552.hs | 43 ++++++++++++++++++++
testsuite/tests/patsyn/should_fail/T14552.stderr | 9 +++++
testsuite/tests/patsyn/should_fail/all.T | 1 +
4 files changed, 103 insertions(+)
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index 7e21af5..0086a83 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -91,6 +91,12 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
univ_tvs = filterOut (`elemVarSet` ex_tv_set) qtvs
req_theta = map evVarPred req_dicts
+ -- See Note [Type variables whose kind is captured]
+ ; let bad_tvs = [ tv | tv <- univ_tvs
+ , tyCoVarsOfType (tyVarKind tv)
+ `intersectsVarSet` ex_tv_set ]
+ ; mapM_ (badUnivTv ex_tvs) bad_tvs
+
; prov_dicts <- mapM zonkId prov_dicts
; let filtered_prov_dicts = mkMinimalBySCs evVarPred prov_dicts
prov_theta = map evVarPred filtered_prov_dicts
@@ -105,6 +111,19 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
(map nlHsVar args, map idType args)
pat_ty rec_fields }
+badUnivTv :: [TyVar] -> TyVar -> TcM ()
+badUnivTv ex_tvs bad_tv
+ = addErrTc $
+ vcat [ text "Universal type variable" <+> quotes (ppr bad_tv)
+ <+> text "has existentially bound kind:"
+ , nest 2 (ppr_with_kind bad_tv)
+ , hang (text "Existentially-bound variables:")
+ 2 (vcat (map ppr_with_kind ex_tvs))
+ , text "Probable fix: give the pattern synoym a type signature"
+ ]
+ where
+ ppr_with_kind tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
+
{- Note [Remove redundant provided dicts]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Recall that
@@ -126,6 +145,37 @@ Similarly consider
The pattern (Bam x y) binds two (Ord a) dictionaries, but we only
need one. Agian mkMimimalWithSCs removes the redundant one.
+
+Note [Type variables whose kind is captured]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ data AST a = Sym [a]
+ class Prj s where { prj :: [a] -> Maybe (s a)
+ pattern P x <= Sym (prj -> Just x)
+
+Here we get a matcher with this type
+ $mP :: forall s a. Prj s => AST a -> (s a -> r) -> r -> r
+
+No problem. But note that 's' is not fixed by the type of the
+pattern (AST a), nor is it existentially bound. It's really only
+fixed by the type of the continuation.
+
+Trac #14552 showed that this can go wrong if the kind of 's' mentions
+existentially bound variables. We obviously can't make a type like
+ $mP :: forall (s::k->*) a. Prj s => AST a -> (forall k. s a -> r)
+ -> r -> r
+But neither is 's' itself existentially bound, so the forall (s::k->*)
+can't go in the inner forall either. (What would the matcher apply
+the continuation to?)
+
+So we just fail in this case, with a pretty terrible error message.
+Maybe we could do better, but I can't see how. (It'd be possible to
+default 's' to (Any k), but that probably isn't what the user wanted,
+and it not straightforward to implement, because by the time we see
+the problem, simplifyInfer has already skolemised 's'.)
+
+This stuff can only happen in the presence of view patterns, with
+TypeInType, so it's a bit of a corner case.
-}
tcCheckPatSynDecl :: PatSynBind GhcRn GhcRn
diff --git a/testsuite/tests/patsyn/should_fail/T14552.hs b/testsuite/tests/patsyn/should_fail/T14552.hs
new file mode 100644
index 0000000..77f0857
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T14552.hs
@@ -0,0 +1,43 @@
+{-# Language RankNTypes, ViewPatterns, PatternSynonyms, TypeOperators, ScopedTypeVariables,
+ KindSignatures, PolyKinds, DataKinds, TypeFamilies, TypeInType, GADTs #-}
+
+module T14552 where
+
+import Data.Kind
+import Data.Proxy
+
+data family Sing a
+
+type a --> b = (a, b) -> Type
+
+type family F (f::a --> b) (x::a) :: b
+
+newtype Limit :: (k --> Type) -> Type where
+ Limit :: (forall xx. Proxy xx -> F f xx) -> Limit f
+
+data Exp :: [Type] -> Type -> Type where
+ TLam :: (forall aa. Proxy aa -> Exp xs (F w aa))
+ -> Exp xs (Limit w)
+
+pattern FOO f <- TLam (($ Proxy) -> f)
+
+
+{-
+TLam :: forall (xs::[Type]) (b::Type). -- Universal
+ forall k (w :: k --> Type). -- Existential
+ (b ~ Limit w) =>
+ => (forall (aa :: k). Proxy aa -> Exp xs (F w aa))
+ -> Exp xs b
+
+-}
+
+{-
+mfoo :: Exp xs b
+ -> (forall k (w :: k --> Type).
+ (b ~ Limit w)
+ => Exp xs (F w aa)
+ -> r)
+ -> r
+mfoo scrut k = case srcut of
+ TLam g -> k (g Proxy)
+-}
diff --git a/testsuite/tests/patsyn/should_fail/T14552.stderr b/testsuite/tests/patsyn/should_fail/T14552.stderr
new file mode 100644
index 0000000..1ead644
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T14552.stderr
@@ -0,0 +1,9 @@
+
+T14552.hs:22:9: error:
+ • Universal type variable ‘aa’ has existentially bound kind:
+ aa :: k
+ Existentially-bound variables:
+ k :: *
+ w :: k --> *
+ Probable fix: give the pattern synoym a type signature
+ • In the declaration for pattern synonym ‘FOO’
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index 4bf631f..d2985d5 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -40,3 +40,4 @@ test('T14112', normal, compile_fail, [''])
test('T14114', normal, compile_fail, [''])
test('T14380', normal, compile_fail, [''])
test('T14498', normal, compile_fail, [''])
+test('T14552', normal, compile_fail, [''])
More information about the ghc-commits
mailing list