[commit: ghc] master: Complete the fix for #13441 (pattern synonyms) (b5c8120)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/b5c81203d047293f54c4e89ac70d505197968cb3/ghc

>---------------------------------------------------------------

commit b5c81203d047293f54c4e89ac70d505197968cb3
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Tue Mar 28 08:23:44 2017 +0100

    Complete the fix for #13441 (pattern synonyms)
    
    Do not attempt to typecheck both directions of an
    implicitly-bidirectional pattern synonym simultanously,
    as we were before.  Instead, the builder is typechecked
    when we typecheck the code for the builder, which was
    of course happening already, even in both bidirectional
    cases.
    
    See Note [Checking against a pattern signature], under
    "Existential type variables".


>---------------------------------------------------------------

b5c81203d047293f54c4e89ac70d505197968cb3
 compiler/typecheck/TcPatSyn.hs                     | 45 ++++++++++++----------
 testsuite/tests/patsyn/should_compile/T13441.hs    |  7 ++++
 testsuite/tests/patsyn/should_compile/T13441a.hs   | 11 ++++++
 testsuite/tests/patsyn/should_compile/T13441b.hs   | 12 ++++++
 .../tests/patsyn/should_compile/T13441b.stderr     | 11 ++++++
 testsuite/tests/patsyn/should_compile/all.T        |  2 +
 6 files changed, 67 insertions(+), 21 deletions(-)

diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index 6f7764e..01cb542 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -149,14 +149,11 @@ tcCheckPatSynDecl psb at PSB{ psb_id = lname@(L _ name), psb_args = details
            pushLevelAndCaptureConstraints            $
            tcExtendTyVarEnv univ_tvs                 $
            tcPat PatSyn lpat (mkCheckExpType pat_ty) $
-           do { let new_tv = case dir of
-                               ImplicitBidirectional -> newMetaSigTyVarX
-                               _                     -> newMetaTyVarX
-                    -- new_tv: see the "Existential type variables"
-                    -- part of Note [Checking against a pattern signature]
-                    in_scope    = mkInScopeSet (mkVarSet univ_tvs)
+           do { let in_scope    = mkInScopeSet (mkVarSet univ_tvs)
                     empty_subst = mkEmptyTCvSubst in_scope
-              ; (subst, ex_tvs') <- mapAccumLM new_tv empty_subst ex_tvs
+              ; (subst, ex_tvs') <- mapAccumLM newMetaTyVarX empty_subst ex_tvs
+                    -- newMetaTyVarX: see the "Existential type variables"
+                    -- part of Note [Checking against a pattern signature]
               ; traceTc "tcpatsyn1" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs])
               ; traceTc "tcpatsyn2" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs'])
               ; let prov_theta' = substTheta subst prov_theta
@@ -241,20 +238,26 @@ unify x := [a] during type checking, and then use the instantiating type
                                               dl = $dfunEqList d
                                           in k [a] dl ys
 
-This "concealing" story works for /uni-directional/ pattern synonyms.
-It also works for /explicitly-bidirectional/ pattern synonyms, where
-the constructor direction is typecheked entirely separately.
-
-But for /implicitly-bidirecitonal/ ones like
-  pattern P x = MkS x
-we are trying to typecheck both directions at once.  So for this we
-use SigTv, rather than a generic TauTv.  But it's not quite done:
- - We should really check that those SigTvs don't get unified
-   with each other.
- - Trac #13441 is rejected if you use an implicitly-bidirectional
-   pattern.
-Maybe it'd be better to treat it like an explicitly-bidirectional
-pattern?
+All this applies when type-checking the /matching/ side of
+a pattern synonym.  What about the /building/ side?
+
+* For Unidirectional, there is no builder
+
+* For ExplicitBidirectional, the builder is completely separate
+  code, typechecked in tcPatSynBuilderBind
+
+* For ImplicitBidirectional, the builder is still typechecked in
+  tcPatSynBuilderBind, by converting the pattern to an expression and
+  typechecking it.
+
+  At one point, for ImplicitBidirectional I used SigTvs (instead of
+  TauTvs) in tcCheckPatSynDecl.  But (a) strengthening the check here
+  is redundant since tcPatSynBuilderBind does the job, (b) it was
+  still incomplete (SigTvs can unify with each other), and (c) it
+  didn't even work (Trac #13441 was accepted with
+  ExplicitBidirectional, but rejected if expressed in
+  ImplicitBidirectional form.  Conclusion: trying to be too clever is
+  a bad idea.
 -}
 
 collectPatSynArgInfo :: HsPatSynDetails (Located Name) -> ([Name], [Name], Bool)
diff --git a/testsuite/tests/patsyn/should_compile/T13441.hs b/testsuite/tests/patsyn/should_compile/T13441.hs
index d7a339f..7380175 100644
--- a/testsuite/tests/patsyn/should_compile/T13441.hs
+++ b/testsuite/tests/patsyn/should_compile/T13441.hs
@@ -21,9 +21,16 @@ type family Replicate (n :: Nat) (x :: a) = (r :: [a]) where
 
 type Vec n a = FList Identity (Replicate n a)
 
+-- Using explicitly-bidirectional pattern
 pattern (:>) :: forall n a. n ~ Length (Replicate n a)
              => forall m. n ~ Succ m
              => a -> Vec m a -> Vec n a
 pattern x :> xs <- Identity x :@ xs
   where
     x :> xs = Identity x :@ xs
+
+-- Using implicitly-bidirectional pattern
+pattern (:>>) :: forall n a. n ~ Length (Replicate n a)
+             => forall m. n ~ Succ m
+             => a -> Vec m a -> Vec n a
+pattern x :>> xs = Identity x :@ xs
diff --git a/testsuite/tests/patsyn/should_compile/T13441a.hs b/testsuite/tests/patsyn/should_compile/T13441a.hs
new file mode 100644
index 0000000..7736094
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T13441a.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE PatternSynonyms, GADTs #-}
+module T13441a where
+
+data S where
+  MkS :: Eq a => [a] -> S
+
+-- Unidirectional pattern binding;
+-- the existential is more specific than needed
+-- c.f. T13441b
+pattern P :: () => Eq x => x -> S
+pattern P x <- MkS x
diff --git a/testsuite/tests/patsyn/should_compile/T13441b.hs b/testsuite/tests/patsyn/should_compile/T13441b.hs
new file mode 100644
index 0000000..8f8d2ba
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T13441b.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE PatternSynonyms, GADTs #-}
+module T13441a where
+
+data S where
+  MkS :: Eq a => [a] -> S
+
+-- Implicitly-bidirectional pattern binding;
+-- the existential is more specific than needed,
+-- and hence should be rejected
+-- c.f. T13441a
+pattern P :: () => Eq x => x -> S
+pattern P x = MkS x
diff --git a/testsuite/tests/patsyn/should_compile/T13441b.stderr b/testsuite/tests/patsyn/should_compile/T13441b.stderr
new file mode 100644
index 0000000..4469086
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T13441b.stderr
@@ -0,0 +1,11 @@
+
+T13441b.hs:12:19: error:
+    • Couldn't match expected type ‘[a0]’ with actual type ‘x’
+      ‘x’ is a rigid type variable bound by
+        the signature for pattern synonym ‘P’ at T13441b.hs:12:1-19
+    • In the first argument of ‘MkS’, namely ‘x’
+      In the expression: MkS x
+      In an equation for ‘P’: P x = MkS x
+    • Relevant bindings include
+        x :: x (bound at T13441b.hs:12:19)
+        $bP :: x -> S (bound at T13441b.hs:12:9)
diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T
index 1f36424..8fce7e9 100644
--- a/testsuite/tests/patsyn/should_compile/all.T
+++ b/testsuite/tests/patsyn/should_compile/all.T
@@ -65,3 +65,5 @@ test('T12746', normal, multi_compile, ['T12746', [('T12746A.hs', '-c')],'-v0'])
 test('T12968', normal, compile, [''])
 test('T13349b', normal, compile, [''])
 test('T13441', normal, compile, [''])
+test('T13441a', normal, compile, [''])
+test('T13441b', normal, compile_fail, [''])