[commit: ghc] master: Pattern synonyms and higher rank types (c997738)
git at git.haskell.org
git at git.haskell.org
Thu May 25 10:59:35 UTC 2017
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/c9977385dca9536f18374242f713b1048a38dec5/ghc
>---------------------------------------------------------------
commit c9977385dca9536f18374242f713b1048a38dec5
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Thu May 25 09:59:29 2017 +0100
Pattern synonyms and higher rank types
This patch fixes two separate bugs which contributed to making
Trac #13752 go wrong
1. We need to use tcSubType, not tcUnify,
in tcCheckPatSynDecl.tc_arg.
Reason: Note [Pattern synonyms and higher rank types]
2. TcUnify.tc_sub_type had a special case designed to improve error
messages; see Note [Don't skolemise unnecessarily]. But the
special case was too liberal, and ended up using unification
(which led to rejecting the program) when it should instead taken
the normal path (which accepts the program).
I fixed this by making the test more conservative.
>---------------------------------------------------------------
c9977385dca9536f18374242f713b1048a38dec5
compiler/typecheck/TcPatSyn.hs | 24 ++++++++++---
compiler/typecheck/TcUnify.hs | 46 +++++++++++++++++++-----
testsuite/tests/patsyn/should_compile/T13752.hs | 9 +++++
testsuite/tests/patsyn/should_compile/T13752a.hs | 8 +++++
testsuite/tests/patsyn/should_compile/all.T | 2 ++
5 files changed, 75 insertions(+), 14 deletions(-)
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index 4b4b042..dc2c4de 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -192,12 +192,26 @@ tcCheckPatSynDecl psb at PSB{ psb_id = lname@(L _ name), psb_args = details
= do { -- Look up the variable actually bound by lpat
-- and check that it has the expected type
arg_id <- tcLookupId arg_name
- ; coi <- unifyType (Just arg_id)
- (idType arg_id)
- (substTyUnchecked subst arg_ty)
- ; return (mkLHsWrapCo coi $ nlHsVar arg_id) }
+ ; wrap <- tcSubType_NC GenSigCtxt
+ (idType arg_id)
+ (substTyUnchecked subst arg_ty)
+ -- Why do we need tcSubType here?
+ -- See Note [Pattern synonyms and higher rank types]
+ ; return (mkLHsWrap wrap $ nlHsVar arg_id) }
+
+{- [Pattern synonyms and higher rank types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ data T = MkT (forall a. a->a)
+
+ pattern P :: (Int -> Int) -> T
+ pattern P x <- MkT x
+
+This should work. But in the matcher we must match against MkT, and then
+instantiate its argument 'x', to get a functino of type (Int -> Int).
+Equality is not enough! Trac #13752 was an example.
-{- Note [Checking against a pattern signature]
+Note [Checking against a pattern signature]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking the actual supplied pattern against the pattern synonym
signature, we need to be quite careful.
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index 6bb81d9..e103d20 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -638,8 +638,8 @@ tc_sub_tc_type :: CtOrigin -- used when calling uType
-- If wrap = tc_sub_type t1 t2
-- => wrap :: t1 ~> t2
tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected
- | is_poly ty_expected -- See Note [Don't skolemise unnecessarily]
- , not (is_poly ty_actual)
+ | definitely_poly ty_expected -- See Note [Don't skolemise unnecessarily]
+ , not (possibly_poly ty_actual)
= do { traceTc "tc_sub_tc_type (drop to equality)" $
vcat [ text "ty_actual =" <+> ppr ty_actual
, text "ty_expected =" <+> ppr ty_expected ]
@@ -656,13 +656,21 @@ tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected
ty_actual sk_rho
; return (sk_wrap <.> inner_wrap) }
where
- is_poly ty
+ possibly_poly ty
| isForAllTy ty = True
- | Just (_, res) <- splitFunTy_maybe ty = is_poly res
+ | Just (_, res) <- splitFunTy_maybe ty = possibly_poly res
| otherwise = False
-- NB *not* tcSplitFunTy, because here we want
-- to decompose type-class arguments too
+ definitely_poly ty
+ | (tvs, theta, tau) <- tcSplitSigmaTy ty
+ , (tv:_) <- tvs
+ , null theta
+ , isInsolubleOccursCheck NomEq tv tau
+ = True
+ | otherwise
+ = False
{- Note [Don't skolemise unnecessarily]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -674,11 +682,31 @@ error. It's better to say that
(Char->Char) ~ (forall a. a->a)
fails.
-In general,
- * if the RHS type an outermost forall (i.e. skolemisation
- is the next thing we'd do)
- * and the LHS has no top-level polymorphism (but looking deeply)
-then we can revert to simple equality.
+So roughly:
+ * if the ty_expected has an outermost forall
+ (i.e. skolemisation is the next thing we'd do)
+ * and the ty_actual has no top-level polymorphism (but looking deeply)
+then we can revert to simple equality. But we need to be careful.
+These examples are allfine:
+
+ * (Char -> forall a. a->a) <= (forall a. Char -> a -> a)
+ Polymorphism is buried in ty_actual
+
+ * (Char->Char) <= (forall a. Char -> Char)
+ ty_expected isn't really polymorphic
+
+ * (Char->Char) <= (forall a. (a~Char) => a -> a)
+ ty_expected isn't really polymorphic
+
+ * (Char->Char) <= (forall a. F [a] Char -> Char)
+ where type instance F [x] t = t
+ ty_expected isn't really polymorphic
+
+If we prematurely go to equality we'll reject a program we should
+accept (e.g. Grac #13752). So the test (which is only to improve
+error messagse) is very conservative:
+ * ty_actual is /definitely/ monomorphic
+ * ty_expected is /definitely/ polymorphic
-}
---------------
diff --git a/testsuite/tests/patsyn/should_compile/T13752.hs b/testsuite/tests/patsyn/should_compile/T13752.hs
new file mode 100644
index 0000000..f9ff606
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T13752.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies, ConstraintKinds, PatternSynonyms, RankNTypes #-}
+
+module T13752 where
+
+newtype Arrange = Arrange {getArrange :: [Int] -> [Int]}
+
+pattern Heh :: (c ~ ((~) Int)) => (forall a. c a => [a] -> [a]) -> Arrange
+-- pattern Heh :: (forall a. (Int ~ a) => [a] -> [a]) -> Arrange
+pattern Heh f <- Arrange f
diff --git a/testsuite/tests/patsyn/should_compile/T13752a.hs b/testsuite/tests/patsyn/should_compile/T13752a.hs
new file mode 100644
index 0000000..2c417f9
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T13752a.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE PatternSynonyms, RankNTypes #-}
+
+module T13752a where
+
+data T = MkT (forall a. a->a)
+
+pattern P :: (Int -> Int) -> T
+pattern P x <- MkT x
diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T
index fa8a3d8..30319c7 100644
--- a/testsuite/tests/patsyn/should_compile/all.T
+++ b/testsuite/tests/patsyn/should_compile/all.T
@@ -68,3 +68,5 @@ test('T13441', normal, compile, [''])
test('T13441a', normal, compile, [''])
test('T13441b', normal, compile_fail, [''])
test('T13454', normal, compile, [''])
+test('T13752', normal, compile, [''])
+test('T13752a', normal, compile, [''])
More information about the ghc-commits
mailing list