Fix explicitly-bidirectional pattern synonyms

This partly fixes Trac #13441, at least for the explicitly
bidirectional case.

See Note [Checking against a pattern signature], the part about
"Existential type variables".

Alas, the implicitly-bidirectional case is still not quite right, but
at least there is a workaround by making it explicitly bidirectional.

3 files changed, 51 insertions, 11 deletions

diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index 15895b5f67..6f7764eb3a 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -149,13 +149,14 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
            pushLevelAndCaptureConstraints            $
            tcExtendTyVarEnv univ_tvs                 $
            tcPat PatSyn lpat (mkCheckExpType pat_ty) $
-           do { let new_tv | isUnidirectional dir = newMetaTyVarX
-                           | otherwise            = newMetaSigTyVarX
+           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)
                     empty_subst = mkEmptyTCvSubst in_scope
               ; (subst, ex_tvs') <- mapAccumLM new_tv empty_subst ex_tvs
-                    -- 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
@@ -240,12 +241,20 @@ 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,
-but obviously not for bidirectional ones.  So in the bidirectional case
-we use SigTv, rather than a generic TauTv, meta-tyvar so that.  And
-we should really check that those SigTvs don't get unified with each
-other.
-
+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?
 -}
 
 collectPatSynArgInfo :: HsPatSynDetails (Located Name) -> ([Name], [Name], Bool)
@@ -519,7 +528,6 @@ tcPatSynBuilderBind (PSB { psb_id = L loc name, psb_def = lpat
 
   | Right match_group <- mb_match_group  -- Bidirectional
   = do { patsyn <- tcLookupPatSyn name
-       ; traceTc "tcPatSynBuilderBind {" $ ppr patsyn
        ; let Just (builder_id, need_dummy_arg) = patSynBuilder patsyn
                    -- Bidirectional, so patSynBuilder returns Just
 
@@ -534,6 +542,8 @@ tcPatSynBuilderBind (PSB { psb_id = L loc name, psb_def = lpat
 
              sig = completeSigFromId (PatSynCtxt name) builder_id
 
+       ; traceTc "tcPatSynBuilderBind {" $
+         ppr patsyn $$ ppr builder_id <+> dcolon <+> ppr (idType builder_id)
        ; (builder_binds, _) <- tcPolyCheck emptyPragEnv sig (noLoc bind)
        ; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds
        ; return builder_binds }
diff --git a/testsuite/tests/patsyn/should_compile/T13441.hs b/testsuite/tests/patsyn/should_compile/T13441.hs
new file mode 100644
index 0000000000..d7a339f782
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T13441.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE ScopedTypeVariables, PatternSynonyms, DataKinds, PolyKinds,
+             GADTs, TypeOperators, TypeFamilies #-}
+
+module T13441 where
+
+import Data.Functor.Identity
+
+data FList f xs where
+  FNil :: FList f '[]
+  (:@) :: f x -> FList f xs -> FList f (x ': xs)
+
+data Nat = Zero | Succ Nat
+
+type family Length (xs :: [k]) :: Nat where
+  Length '[]       = Zero
+  Length (_ ': xs) = Succ (Length xs)
+
+type family Replicate (n :: Nat) (x :: a) = (r :: [a]) where
+  Replicate Zero     _ = '[]
+  Replicate (Succ n) x = x ': Replicate n x
+
+type Vec n a = FList Identity (Replicate n a)
+
+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
diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T
index 87de2f00bb..1f36424640 100644
--- a/testsuite/tests/patsyn/should_compile/all.T
+++ b/testsuite/tests/patsyn/should_compile/all.T
@@ -64,3 +64,4 @@ test('T12698', normal, compile, [''])
 test('T12746', normal, multi_compile, ['T12746', [('T12746A.hs', '-c')],'-v0'])
 test('T12968', normal, compile, [''])
 test('T13349b', normal, compile, [''])
+test('T13441', normal, compile, [''])