Zonk properly when checkig pattern synonyms

Fixes Trac #10997

Merge to stable branch

7 files changed, 115 insertions, 40 deletions

diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index 5e53ae5f1b..8e97f5b935 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -85,15 +85,6 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L loc name), psb_args = details,
              prov_theta = map evVarPred prov_dicts
              req_theta  = map evVarPred req_dicts
 
-       ; univ_tvs   <- mapM zonkQuantifiedTyVar univ_tvs
-       ; ex_tvs     <- mapM zonkQuantifiedTyVar ex_tvs
-
-       ; prov_theta <- zonkTcThetaType prov_theta
-       ; req_theta  <- zonkTcThetaType req_theta
-
-       ; pat_ty     <- zonkTcType pat_ty
-       ; args       <- mapM zonkId args
-
        ; traceTc "tcInferPatSynDecl }" $ ppr name
        ; tc_patsyn_finish lname dir is_infix lpat'
                           (univ_tvs, req_theta, ev_binds, req_dicts)
@@ -138,8 +129,8 @@ tcCheckPatSynDecl PSB{ psb_id = lname@(L loc name), psb_args = details,
          --  * The arguments, type-coerced to the SigTyVars: wrapped_args
          --  * The instantiation of ex_tvs to pass to the success continuation: ex_tys
          --  * The provided theta substituted with the SigTyVars: prov_theta'
-       ; (req_ev_binds, (lpat', (ex_tys, prov_theta', wrapped_args))) <-
-           checkConstraints skol_info univ_tvs req_dicts $
+       ; (implic1, req_ev_binds, (lpat', (ex_tys, prov_theta', wrapped_args))) <-
+           buildImplication skol_info univ_tvs req_dicts $
            tcPat PatSyn lpat pat_ty $ do
            { ex_sigtvs <- mapM (\tv -> newSigTyVar (getName tv) (tyVarKind tv)) ex_tvs
            ; let subst = mkTvSubst (mkInScopeSet (zipVarEnv ex_sigtvs ex_sigtvs)) $
@@ -157,11 +148,16 @@ tcCheckPatSynDecl PSB{ psb_id = lname@(L loc name), psb_args = details,
        ; let ex_tvs_rhs  = varSetElems ex_vars_rhs
 
          -- Check that prov_theta' can be satisfied with the dicts from the pattern
-       ; (prov_ev_binds, prov_dicts) <-
-           checkConstraints skol_info ex_tvs_rhs prov_dicts_rhs $ do
+       ; (implic2, prov_ev_binds, prov_dicts) <-
+           buildImplication skol_info ex_tvs_rhs prov_dicts_rhs $ do
            { let origin = PatOrigin -- TODO
            ; emitWanteds origin prov_theta' }
 
+       -- Solve the constraints now, because we are about to make a PatSyn,
+       -- which should not contain unification variables and the like (Trac #10997)
+       -- Since all the inputs are implications the returned bindings will be empty
+       ; _ <- simplifyTop (emptyWC `addImplics` (implic1 `unionBags` implic2))
+
        ; traceTc "tcCheckPatSynDecl }" $ ppr name
        ; tc_patsyn_finish lname dir is_infix lpat'
                           (univ_tvs, req_theta, req_ev_binds, req_dicts)
@@ -192,14 +188,36 @@ tc_patsyn_finish lname dir is_infix lpat'
                  (ex_tvs, subst, prov_theta, prov_ev_binds, prov_dicts)
                  wrapped_args
                  pat_ty
-  = do { (matcher_id, matcher_bind) <- tcPatSynMatcher lname lpat'
+  = do { -- Zonk everything.  We are about to build a final PatSyn
+         -- so there had better be no unification variables in there
+         univ_tvs     <- mapM zonkQuantifiedTyVar univ_tvs
+       ; ex_tvs       <- mapM zonkQuantifiedTyVar ex_tvs
+       ; prov_theta   <- zonkTcThetaType prov_theta
+       ; req_theta    <- zonkTcThetaType req_theta
+       ; pat_ty       <- zonkTcType pat_ty
+       ; wrapped_args <- mapM zonk_wrapped_arg wrapped_args
+       ; let qtvs    = univ_tvs ++ ex_tvs
+             theta   = prov_theta ++ req_theta
+             arg_tys = map (varType . fst) wrapped_args
+
+       ; traceTc "tc_patsyn_finish {" $
+           ppr (unLoc lname) $$ ppr (unLoc lpat') $$
+           ppr (univ_tvs, req_theta, req_ev_binds, req_dicts) $$
+           ppr (ex_tvs, subst, prov_theta, prov_ev_binds, prov_dicts) $$
+           ppr wrapped_args $$
+           ppr pat_ty
+
+       -- Make the 'matcher'
+       ; (matcher_id, matcher_bind) <- tcPatSynMatcher lname lpat'
                                          (univ_tvs, req_theta, req_ev_binds, req_dicts)
                                          (ex_tvs, subst, prov_theta, prov_ev_binds, prov_dicts)
-                                         wrapped_args
+                                         wrapped_args  -- Not necessarily zonked
                                          pat_ty
 
+       -- Make the 'builder'
        ; builder_id <- mkPatSynBuilderId dir lname qtvs theta arg_tys pat_ty
 
+       -- Make the PatSyn itself
        ; let patSyn = mkPatSyn (unLoc lname) is_infix
                         (univ_tvs, req_theta)
                         (ex_tvs, prov_theta)
@@ -209,9 +227,10 @@ tc_patsyn_finish lname dir is_infix lpat'
 
        ; return (patSyn, matcher_bind) }
   where
-    qtvs = univ_tvs ++ ex_tvs
-    theta = prov_theta ++ req_theta
-    arg_tys = map (varType . fst) wrapped_args
+    zonk_wrapped_arg :: (Var, HsWrapper) -> TcM (Var, HsWrapper)
+    -- The HsWrapper will get zonked later, as part of the LHsBinds
+    zonk_wrapped_arg (arg_id, wrap) = do { arg_id <- zonkId arg_id
+                                         ; return (arg_id, wrap) }
 
 {-
 ************************************************************************
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index b4a6ada41a..3de91055ca 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -12,7 +12,7 @@ module TcUnify (
   -- Full-blown subsumption
   tcWrapResult, tcGen,
   tcSubType, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_NC,
-  checkConstraints, newImplication,
+  checkConstraints, buildImplication,
 
   -- Various unifications
   unifyType, unifyTypeList, unifyTheta,
@@ -52,6 +52,7 @@ import ErrUtils
 import DynFlags
 import BasicTypes
 import Maybes ( isJust )
+import Bag
 import Util
 import Outputable
 import FastString
@@ -571,17 +572,19 @@ checkConstraints skol_info skol_tvs given thing_inside
       -- tcPolyExpr, which uses tcGen and hence checkConstraints.
 
   | otherwise
-  = newImplication skol_info skol_tvs given thing_inside
+  = do { (implics, ev_binds, result) <- buildImplication skol_info skol_tvs given thing_inside
+       ; emitImplications implics
+       ; return (ev_binds, result) }
 
-newImplication :: SkolemInfo -> [TcTyVar]
-               -> [EvVar] -> TcM result
-               -> TcM (TcEvBinds, result)
-newImplication skol_info skol_tvs given thing_inside
-  = ASSERT2( all isTcTyVar skol_tvs, ppr skol_tvs )
+buildImplication :: SkolemInfo
+                 -> [TcTyVar]           -- Skolems
+                 -> [EvVar]             -- Given
+                 -> TcM result
+                 -> TcM (Bag Implication, TcEvBinds, result)
+buildImplication skol_info skol_tvs given thing_inside
+ =  ASSERT2( all isTcTyVar skol_tvs, ppr skol_tvs )
     ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
-    do { ((result, tclvl), wanted) <- captureConstraints  $
-                                      captureTcLevel $
-                                      thing_inside
+    do { (result, tclvl, wanted) <- pushLevelAndCaptureConstraints thing_inside
 
        ; if isEmptyWC wanted && null given
             -- Optimisation : if there are no wanteds, and no givens
@@ -589,21 +592,21 @@ newImplication skol_info skol_tvs given thing_inside
             -- Reason for the (null given): we don't want to lose
             -- the "inaccessible alternative" error check
          then
-            return (emptyTcEvBinds, result)
+            return (emptyBag, emptyTcEvBinds, result)
          else do
        { ev_binds_var <- newTcEvBinds
        ; env <- getLclEnv
-       ; emitImplication $ Implic { ic_tclvl = tclvl
-                                  , ic_skols = skol_tvs
-                                  , ic_no_eqs = False
-                                  , ic_given = given
-                                  , ic_wanted = wanted
-                                  , ic_insol  = insolubleWC wanted
-                                  , ic_binds = ev_binds_var
-                                  , ic_env = env
-                                  , ic_info = skol_info }
-
-       ; return (TcEvBinds ev_binds_var, result) } }
+       ; let implic = Implic { ic_tclvl = tclvl
+                             , ic_skols = skol_tvs
+                             , ic_no_eqs = False
+                             , ic_given = given
+                             , ic_wanted = wanted
+                             , ic_insol = insolubleWC wanted
+                             , ic_binds = ev_binds_var
+                             , ic_env = env
+                             , ic_info = skol_info }
+
+       ; return (unitBag implic, TcEvBinds ev_binds_var, result) } }
 
 {-
 ************************************************************************
diff --git a/testsuite/tests/patsyn/should_compile/T10997.hs b/testsuite/tests/patsyn/should_compile/T10997.hs
new file mode 100644
index 0000000000..69a7940a5f
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T10997.hs
@@ -0,0 +1,6 @@
+module T10997 where
+
+import T10997a
+
+foo :: Exp a -> String
+foo Tru = "True"
diff --git a/testsuite/tests/patsyn/should_compile/T10997_1.hs b/testsuite/tests/patsyn/should_compile/T10997_1.hs
new file mode 100644
index 0000000000..4cc4b40eec
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T10997_1.hs
@@ -0,0 +1,15 @@
+module T10997_1 where
+
+import T10997_1a
+
+{- With ghc-7.10.2:
+
+    The interface for ‘T10997a’
+    Declaration for Just'
+    Pattern synonym Just':
+    Iface type variable out of scope:  k
+    Cannot continue after interface file error
+-}
+
+bar :: (Showable a) => Maybe a -> Maybe a
+bar (Just' a) = Just' a
diff --git a/testsuite/tests/patsyn/should_compile/T10997_1a.hs b/testsuite/tests/patsyn/should_compile/T10997_1a.hs
new file mode 100644
index 0000000000..af98f495f7
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T10997_1a.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE PatternSynonyms, ViewPatterns, ConstraintKinds, TypeFamilies, PolyKinds, KindSignatures #-}
+module T10997_1a where
+
+import GHC.Exts
+
+type family Showable (a :: k) :: Constraint where
+  Showable (a :: *) = (Show a)
+  Showable a       = ()
+
+extractJust :: Maybe a -> (Bool, a)
+extractJust (Just a) = (True, a)
+extractJust _        = (False, undefined)
+
+pattern Just' :: () => (Showable a) => a -> (Maybe a)
+pattern Just' a <- (extractJust -> (True, a)) where
+  Just' a = Just a
+
diff --git a/testsuite/tests/patsyn/should_compile/T10997a.hs b/testsuite/tests/patsyn/should_compile/T10997a.hs
new file mode 100644
index 0000000000..bed19f74e9
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T10997a.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE GADTs, PatternSynonyms #-}
+
+module T10997a where
+
+data Exp ty where
+  LitB :: Bool -> Exp Bool
+
+pattern Tru :: b ~ Bool => Exp b
+pattern Tru = LitB True
+
+
diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T
index 9529133114..f63076211e 100644
--- a/testsuite/tests/patsyn/should_compile/all.T
+++ b/testsuite/tests/patsyn/should_compile/all.T
@@ -22,3 +22,7 @@ test('ImpExp_Imp', [extra_clean(['ImpExp_Exp.hi', 'ImpExp_Exp.o'])], multimod_co
 test('T9857', normal, compile, [''])
 test('T9889', normal, compile, [''])
 test('T10747', normal, compile, [''])
+test('T10997', [extra_clean(['T10997a.hi', 'T10997a.o'])], multimod_compile, ['T10997', '-v0'])
+test('T10997_1', [extra_clean(['T10997_1a.hi', 'T10997_1a.o'])], multimod_compile, ['T10997_1', '-v0'])
+
+