[commit: ghc] master: Fix another obscure pattern-synonym crash (40cbab9)
git at git.haskell.org
git at git.haskell.org
Fri Jan 5 09:47:00 UTC 2018
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/40cbab9afe52fbc780310e880912b56370065a62/ghc
>---------------------------------------------------------------
commit 40cbab9afe52fbc780310e880912b56370065a62
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Fri Jan 5 09:12:49 2018 +0000
Fix another obscure pattern-synonym crash
This one, discovered by Iceland Jack (Trac #14507), shows
that a pattern-bound coercion can show up in the argument
type(s) of the matcher of a pattern synonym.
The error message isn't great, but at least we now rightly
reject the program.
>---------------------------------------------------------------
40cbab9afe52fbc780310e880912b56370065a62
compiler/typecheck/TcPatSyn.hs | 69 +++++++++++++++++++++---
testsuite/tests/patsyn/should_fail/T14507.hs | 19 +++++++
testsuite/tests/patsyn/should_fail/T14507.stderr | 8 +++
testsuite/tests/patsyn/should_fail/all.T | 1 +
4 files changed, 90 insertions(+), 7 deletions(-)
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index 0086a83..b89c4be 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -91,16 +91,26 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
univ_tvs = filterOut (`elemVarSet` ex_tv_set) qtvs
req_theta = map evVarPred req_dicts
+ ; prov_dicts <- mapM zonkId prov_dicts
+ ; let filtered_prov_dicts = mkMinimalBySCs evVarPred prov_dicts
+ prov_theta = map evVarPred filtered_prov_dicts
+ -- Filtering: see Note [Remove redundant provided dicts]
+
+ -- Report bad universal type variables
-- 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
+ ; mapM_ (badUnivTvErr 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
- -- Filtering: see Note [Remove redundant provided dicts]
+ -- Report coercions that esacpe
+ -- See Note [Coercions that escape]
+ ; args <- mapM zonkId args
+ ; let bad_args = [ (arg, bad_cos) | arg <- args ++ prov_dicts
+ , let bad_cos = filterDVarSet isId $
+ (tyCoVarsOfTypeDSet (idType arg))
+ , not (isEmptyDVarSet bad_cos) ]
+ ; mapM_ dependentArgErr bad_args
; traceTc "tcInferPatSynDecl }" $ (ppr name $$ ppr ex_tvs)
; tc_patsyn_finish lname dir is_infix lpat'
@@ -111,8 +121,9 @@ 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
+badUnivTvErr :: [TyVar] -> TyVar -> TcM ()
+-- See Note [Type variables whose kind is captured]
+badUnivTvErr ex_tvs bad_tv
= addErrTc $
vcat [ text "Universal type variable" <+> quotes (ppr bad_tv)
<+> text "has existentially bound kind:"
@@ -124,6 +135,22 @@ badUnivTv ex_tvs bad_tv
where
ppr_with_kind tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
+dependentArgErr :: (Id, DTyCoVarSet) -> TcM ()
+-- See Note [Coercions that escape]
+dependentArgErr (arg, bad_cos)
+ = addErrTc $
+ vcat [ text "Iceland Jack! Iceland Jack! Stop torturing me!"
+ , hang (text "Pattern-bound variable")
+ 2 (ppr arg <+> dcolon <+> ppr (idType arg))
+ , nest 2 $
+ hang (text "has a type that mentions pattern-bound coercion"
+ <> plural bad_co_list <> colon)
+ 2 (pprWithCommas ppr bad_co_list)
+ , text "Hint: use -fprint-explicit-coercions to see the coercions"
+ , text "Probable fix: add a pattern signature" ]
+ where
+ bad_co_list = dVarSetElems bad_cos
+
{- Note [Remove redundant provided dicts]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Recall that
@@ -176,6 +203,34 @@ 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.
+
+Note [Coercions that escape]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Trac #14507 showed an example where the inferred type of the matcher
+for the pattern synonym was somethign like
+ $mSO :: forall (r :: TYPE rep) kk (a :: k).
+ TypeRep k a
+ -> ((Bool ~ k) => TypeRep Bool (a |> co_a2sv) -> r)
+ -> (Void# -> r)
+ -> r
+
+What is that co_a2sv :: Bool ~# *?? It was bound (via a superclass
+selection) by the pattern being matched; and indeed it is implicit in
+the context (Bool ~ k). You could imagine trying to extract it like
+this:
+ $mSO :: forall (r :: TYPE rep) kk (a :: k).
+ TypeRep k a
+ -> ( co :: ((Bool :: *) ~ (k :: *)) =>
+ let co_a2sv = sc_sel co
+ in TypeRep Bool (a |> co_a2sv) -> r)
+ -> (Void# -> r)
+ -> r
+
+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.
-}
tcCheckPatSynDecl :: PatSynBind GhcRn GhcRn
diff --git a/testsuite/tests/patsyn/should_fail/T14507.hs b/testsuite/tests/patsyn/should_fail/T14507.hs
new file mode 100644
index 0000000..84166d0
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T14507.hs
@@ -0,0 +1,19 @@
+{-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds, TypeInType, TypeOperators, TypeApplications, TypeFamilies, TypeFamilyDependencies #-}
+
+module T14507 where
+
+import Type.Reflection
+import Data.Kind
+
+foo :: TypeRep a -> (Bool :~~: k, TypeRep a)
+foo rep = error "urk"
+
+type family SING :: k -> Type where
+ SING = (TypeRep :: Bool -> Type)
+
+pattern RepN :: forall (a::kk). () => Bool~kk => SING a -> TypeRep (a::kk)
+pattern RepN tr <- (foo -> ( HRefl :: Bool:~~:kk
+ , tr :: TypeRep (a::Bool)))
+
+pattern SO x <- RepN (id -> x)
+
diff --git a/testsuite/tests/patsyn/should_fail/T14507.stderr b/testsuite/tests/patsyn/should_fail/T14507.stderr
new file mode 100644
index 0000000..2ed89cb
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T14507.stderr
@@ -0,0 +1,8 @@
+
+T14507.hs:18:9: error:
+ • Iceland Jack! Iceland Jack! Stop torturing me!
+ Pattern-bound variable x :: TypeRep a
+ has a type that mentions pattern-bound coercion: co_a2CF
+ Hint: use -fprint-explicit-coercions to see the coercions
+ Probable fix: add a pattern signature
+ • In the declaration for pattern synonym ‘SO’
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index d2985d5..2b3b85b 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -41,3 +41,4 @@ test('T14114', normal, compile_fail, [''])
test('T14380', normal, compile_fail, [''])
test('T14498', normal, compile_fail, [''])
test('T14552', normal, compile_fail, [''])
+test('T14507', normal, compile_fail, [''])
More information about the ghc-commits
mailing list