[commit: ghc] master: Solve equalities in a pattern signature (7ea714c)

[git at git.haskell.org]

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

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

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

commit 7ea714cd8d64dd0a7646d71d45e18c9f6a3527cb
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Tue Oct 16 14:47:12 2018 +0100

    Solve equalities in a pattern signature
    
    Trac #15694 showed that we were forgetting to solve
    the equalities of a pattern signature until too late.
    
    Result: WARNINGs and a panic:
      "Type-correct unfilled coercion hole"


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

7ea714cd8d64dd0a7646d71d45e18c9f6a3527cb
 compiler/typecheck/TcSigs.hs                     | 25 ++++++++++++++++++++++--
 testsuite/tests/patsyn/should_fail/T15694.hs     | 25 ++++++++++++++++++++++++
 testsuite/tests/patsyn/should_fail/T15694.stderr |  4 ++++
 testsuite/tests/patsyn/should_fail/all.T         |  1 +
 4 files changed, 53 insertions(+), 2 deletions(-)

diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs
index a371f55..ada9178 100644
--- a/compiler/typecheck/TcSigs.hs
+++ b/compiler/typecheck/TcSigs.hs
@@ -297,6 +297,24 @@ Once we get to type checking, we decompose it into its parts, in tcPatSynSig.
   universal and existential vars.
 
 * After we kind-check the pieces and convert to Types, we do kind generalisation.
+
+Note [solveEqualities in tcPatSynSig]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's important that we solve /all/ the equalities in a pattern
+synonym signature, because we are going to zonk the signature to
+a Type (not a TcType), in TcPatSyn.tc_patsyn_finish, and that
+fails if there are un-filled-in coercion variables mentioned
+in the type (Trac #15694).
+
+The best thing is simply to use solveEqualities to solve all the
+equalites, rather than leaving them in the ambient constraints
+to be solved later.  Pattern synonyms are top-level, so there's
+no problem with completely solving them.
+
+(NB: this solveEqualities wraps tcImplicitTKBndrs, which itself
+does a solveLocalEqualities; so solveEqualities isn't going to
+make any further progress; it'll just report any unsolved ones,
+and fail, as it should.)
 -}
 
 tcPatSynSig :: Name -> LHsSigType GhcRn -> TcM TcPatSynInfo
@@ -307,8 +325,10 @@ tcPatSynSig name sig_ty
          , hsib_body = hs_ty }  <- sig_ty
   , (univ_hs_tvs, hs_req,  hs_ty1)     <- splitLHsSigmaTy hs_ty
   , (ex_hs_tvs,   hs_prov, hs_body_ty) <- splitLHsSigmaTy hs_ty1
-  = do { (implicit_tvs, (univ_tvs, (ex_tvs, (req, prov, body_ty))))
-           <-  -- NB: tcImplicitTKBndrs calls solveLocalEqualities
+  = do {  traceTc "tcPatSynSig 1" (ppr sig_ty)
+       ; (implicit_tvs, (univ_tvs, (ex_tvs, (req, prov, body_ty))))
+           <- solveEqualities                             $
+                -- See Note [solveEqualities in tcPatSynSig]
               tcImplicitTKBndrs skol_info implicit_hs_tvs $
               tcExplicitTKBndrs skol_info univ_hs_tvs     $
               tcExplicitTKBndrs skol_info ex_hs_tvs       $
@@ -324,6 +344,7 @@ tcPatSynSig name sig_ty
 
        -- Kind generalisation
        ; kvs <- kindGeneralize ungen_patsyn_ty
+       ; traceTc "tcPatSynSig" (ppr ungen_patsyn_ty)
 
        -- These are /signatures/ so we zonk to squeeze out any kind
        -- unification variables.  Do this after kindGeneralize which may
diff --git a/testsuite/tests/patsyn/should_fail/T15694.hs b/testsuite/tests/patsyn/should_fail/T15694.hs
new file mode 100644
index 0000000..915ad7e
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T15694.hs
@@ -0,0 +1,25 @@
+{-# Language RankNTypes, PatternSynonyms, TypeOperators, DataKinds, PolyKinds, KindSignatures, GADTs #-}
+
+module T15694 where
+
+import Data.Kind
+import Data.Type.Equality
+
+data Ctx :: Type -> Type where
+ E     :: Ctx(Type)
+ (:&:) :: a -> Ctx(as) -> Ctx(a -> as)
+
+data ApplyT(kind::Type) :: kind ->  Ctx(kind) -> Type where
+ AO :: a -> ApplyT(Type) a E
+ AS :: ApplyT(ks)      (f a) ctx
+    -> ApplyT(k -> ks) f     (a:&:ctx)
+
+
+pattern ASSO :: () => forall ks k (f :: k -> ks) (a1 :: k) (ctx :: Ctx ks)
+                             (ks1 :: Type) k1 (a2 :: k1) (ctx1 :: Ctx ks1) a3.
+                     (kind ~ (k -> ks), a ~~ f, b ~~ (a1 :&: ctx),
+                      ks ~ (k1 -> ks1), ctx ~~ (a2 :&: E),
+                      ks1 ~ Type, f a1 a2 ~~ a3)
+                   => a3 -> ApplyT kind a b
+
+pattern ASSO a = AS (AS (AO a))
diff --git a/testsuite/tests/patsyn/should_fail/T15694.stderr b/testsuite/tests/patsyn/should_fail/T15694.stderr
new file mode 100644
index 0000000..360fb30
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T15694.stderr
@@ -0,0 +1,4 @@
+
+T15694.hs:22:35: error:
+    • Expected kind ‘k1 -> k00’, but ‘f a1’ has kind ‘ks’
+    • In the first argument of ‘(~~)’, namely ‘f a1 a2’
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index e726eaa..099e905 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -46,3 +46,4 @@ test('T14507', normal, compile_fail, ['-dsuppress-uniques'])
 test('T15289', normal, compile_fail, [''])
 test('T15685', normal, compile_fail, [''])
 test('T15692', normal, compile, [''])   # It has -fdefer-type-errors inside
+test('T15694', normal, compile_fail, [''])