Fail fast on pattern synonyms
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 3 Oct 2018 14:53:59 +0000 (15:53 +0100)
committerBen Gamari <ben@smart-cactus.org>
Wed, 17 Oct 2018 18:46:22 +0000 (14:46 -0400)
We were recovering too eagerly from errors in pattern-synonym
type inference, leading to a cascade of confusing follow up errors
(Trac #15685, #15692).

The underlying issue is that a pattern synonym should have a closed,
fixed type, with no unification variables in it.  But it wasn't!

Fixing this made me change the interface to simplifyInfer slightly.
Instead of /emitting/ a residual implication constraint, it
now /returns/ it, so that the caller can decide what to do.

(cherry picked from commit 9ebfa03d9e9cbf79f698b5d4bd39e799e4e9a02c)

12 files changed:
compiler/typecheck/TcBinds.hs
compiler/typecheck/TcExpr.hs
compiler/typecheck/TcPatSyn.hs
compiler/typecheck/TcRnDriver.hs
compiler/typecheck/TcRnMonad.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcSimplify.hs
testsuite/tests/patsyn/should_fail/T15685.hs [new file with mode: 0644]
testsuite/tests/patsyn/should_fail/T15685.stderr [new file with mode: 0644]
testsuite/tests/patsyn/should_fail/T15692.hs [new file with mode: 0644]
testsuite/tests/patsyn/should_fail/T15692.stderr [new file with mode: 0644]
testsuite/tests/patsyn/should_fail/all.T

index 4bd91d8..1442f7d 100644 (file)
@@ -795,8 +795,9 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list
        ; mapM_ (checkOverloadedSig mono) sigs
 
        ; traceTc "simplifyInfer call" (ppr tclvl $$ ppr name_taus $$ ppr wanted)
-       ; (qtvs, givens, ev_binds, insoluble)
+       ; (qtvs, givens, ev_binds, residual, insoluble)
                  <- simplifyInfer tclvl infer_mode sigs name_taus wanted
+       ; emitConstraints residual
 
        ; let inferred_theta = map evVarPred givens
        ; exports <- checkNoErrs $
index a4a005c..4751a20 100644 (file)
@@ -1663,8 +1663,10 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc })
                         = ApplyMR
                         | otherwise
                         = NoRestrictions
-       ; (qtvs, givens, ev_binds, _)
+       ; (qtvs, givens, ev_binds, residual, _)
                  <- simplifyInfer tclvl infer_mode [sig_inst] [(name, tau)] wanted
+       ; emitConstraints residual
+
        ; tau <- zonkTcType tau
        ; let inferred_theta = map evVarPred givens
              tau_tvs        = tyCoVarsOfType tau
index 71050b8..3e3ea34 100644 (file)
@@ -53,7 +53,7 @@ import FieldLabel
 import Bag
 import Util
 import ErrUtils
-import Control.Monad ( zipWithM, when )
+import Control.Monad ( zipWithM )
 import Data.List( partition )
 
 #include "HsVersions.h"
@@ -69,21 +69,23 @@ import Data.List( partition )
 tcPatSynDecl :: PatSynBind GhcRn GhcRn
              -> Maybe TcSigInfo
              -> TcM (LHsBinds GhcTc, TcGblEnv)
-tcPatSynDecl psb@(PSB { psb_id = L _ name, psb_args = details }) mb_sig
-  = recoverM recover $
+tcPatSynDecl psb mb_sig
+  = recoverM (recoverPSB psb) $
     case mb_sig of
       Nothing                 -> tcInferPatSynDecl psb
       Just (TcPatSynSig tpsi) -> tcCheckPatSynDecl psb tpsi
-      _ -> panic "tcPatSynDecl"
-
+      _                       -> panic "tcPatSynDecl"
+
+recoverPSB :: PatSynBind GhcRn GhcRn
+           -> TcM (LHsBinds GhcTc, TcGblEnv)
+-- See Note [Pattern synonym error recovery]
+recoverPSB (PSB { psb_id = L _ name, psb_args = details })
+ = do { matcher_name <- newImplicitBinder name mkMatcherOcc
+      ; let placeholder = AConLike $ PatSynCon $
+                          mk_placeholder matcher_name
+      ; gbl_env <- tcExtendGlobalEnv [placeholder] getGblEnv
+      ; return (emptyBag, gbl_env) }
   where
-    -- See Note [Pattern synonym error recovery]
-    recover = do { matcher_name <- newImplicitBinder name mkMatcherOcc
-                 ; let placeholder = AConLike $ PatSynCon $
-                                     mk_placeholder matcher_name
-                 ; gbl_env <- tcExtendGlobalEnv [placeholder] getGblEnv
-                 ; return (emptyBag, gbl_env) }
-
     (_arg_names, _rec_fields, is_infix) = collectPatSynArgInfo details
     mk_placeholder matcher_name
       = mkPatSyn name is_infix
@@ -98,30 +100,40 @@ tcPatSynDecl psb@(PSB { psb_id = L _ name, psb_args = details }) mb_sig
          matcher_id = mkLocalId matcher_name $
                       mkSpecForAllTys [alphaTyVar] alphaTy
 
-tcPatSynDecl (XPatSynBind {}) _ = panic "tcPatSynDecl"
+recoverPSB (XPatSynBind {}) = panic "recoverPSB"
 
 {- Note [Pattern synonym error recovery]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If type inference for a pattern synonym fails , we can't continue with
+If type inference for a pattern synonym fails, we can't continue with
 the rest of tc_patsyn_finish, because we may get knock-on errors, or
 even a crash.  E.g. from
    pattern What = True :: Maybe
 we get a kind error; and we must stop right away (Trac #15289).
-Hence the 'when insoluble failM' in tcInferPatSyn.
-
-But does that abort compilation entirely?  No -- we can recover
-and carry on, just as we do for value bindings, provided we plug in
-placeholder for the pattern synonym.  The goal of the placeholder
-is not to cause a raft of follow-on errors.  I've used the simplest
-thing for now, but we might need to elaborate it a bit later.  (e.g.
-I've given it zero args, which may cause knock-on errors if it is
-used in a pattern.) But it'll do for now.
+
+We stop if there are /any/ unsolved constraints, not just insoluble
+ones; because pattern synonyms are top-level things, we will never
+solve them later if we can't solve them now.  And if we were to carry
+on, tc_patsyn_finish does zonkTcTypeToType, which defaults any
+unsolved unificatdion variables to Any, which confuses the error
+reporting no end (Trac #15685).
+
+So we use simplifyTop to completely solve the constraint, report
+any errors, throw an exception.
+
+Even in the event of such an error we can recover and carry on, just
+as we do for value bindings, provided we plug in placeholder for the
+pattern synonym: see recoverPSB.  The goal of the placeholder is not
+to cause a raft of follow-on errors.  I've used the simplest thing for
+now, but we might need to elaborate it a bit later.  (e.g.  I've given
+it zero args, which may cause knock-on errors if it is used in a
+pattern.) But it'll do for now.
+
 -}
 
 tcInferPatSynDecl :: PatSynBind GhcRn GhcRn
                   -> TcM (LHsBinds GhcTc, TcGblEnv)
-tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
-                       psb_def = lpat, psb_dir = dir }
+tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details
+                       , psb_def = lpat, psb_dir = dir })
   = addPatSynCtxt lname $
     do { traceTc "tcInferPatSynDecl {" $ ppr name
 
@@ -134,15 +146,12 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
 
        ; let named_taus = (name, pat_ty) : map (\arg -> (getName arg, varType arg)) args
 
-       ; (qtvs, req_dicts, ev_binds, insoluble)
+       ; (qtvs, req_dicts, ev_binds, residual, _)
                <- simplifyInfer tclvl NoRestrictions [] named_taus wanted
+       ; top_ev_binds <- checkNoErrs (simplifyTop residual)
+       ; addTopEvBinds top_ev_binds $
 
-       ; when insoluble failM
-              -- simplifyInfer doesn't fail if there are errors.  But to avoid
-              -- knock-on errors, or even crashes, we want to stop here.
-              -- See Note [Pattern synonym error recovery]
-
-       ; let (ex_tvs, prov_dicts) = tcCollectEx lpat'
+    do { let (ex_tvs, prov_dicts) = tcCollectEx lpat'
              ex_tv_set  = mkVarSet ex_tvs
              univ_tvs   = filterOut (`elemVarSet` ex_tv_set) qtvs
              req_theta  = map evVarPred req_dicts
@@ -176,7 +185,7 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
                             , mkTyVarTys ex_tvs, prov_theta
                             , map (EvExpr . evId) filtered_prov_dicts)
                           (map nlHsVar args, map idType args)
-                          pat_ty rec_fields }
+                          pat_ty rec_fields } }
 tcInferPatSynDecl (XPatSynBind _) = panic "tcInferPatSynDecl"
 
 badUnivTvErr :: [TyVar] -> TyVar -> TcM ()
index c8e168d..4259b04 100644 (file)
@@ -480,11 +480,8 @@ run_th_modfinalizers = do
       -- (see #12777).
       new_ev_binds <- {-# SCC "simplifyTop2" #-}
                       simplifyTop lie
-      updGblEnv (\tcg_env ->
-        tcg_env { tcg_ev_binds = tcg_ev_binds tcg_env `unionBags` new_ev_binds }
-        )
+      addTopEvBinds new_ev_binds run_th_modfinalizers
         -- addTopDecls can add declarations which add new finalizers.
-        run_th_modfinalizers
 
 tc_rn_src_decls :: [LHsDecl GhcPs]
                 -> TcM (TcGblEnv, TcLclEnv)
@@ -2306,17 +2303,15 @@ tcRnExpr hsc_env mode rdr_expr
                   else return expr_ty } ;
 
     -- Generalise
-    ((qtvs, dicts, _, _), lie_top) <- captureTopConstraints $
-                                      {-# SCC "simplifyInfer" #-}
-                                      simplifyInfer tclvl
-                                                 infer_mode
-                                                 []    {- No sig vars -}
-                                                 [(fresh_it, res_ty)]
-                                                 lie ;
+    (qtvs, dicts, _, residual, _)
+         <- simplifyInfer tclvl infer_mode
+                          []    {- No sig vars -}
+                          [(fresh_it, res_ty)]
+                          lie ;
 
     -- Ignore the dictionary bindings
     _ <- perhaps_disable_default_warnings $
-         simplifyInteractive lie_top ;
+         simplifyInteractive residual ;
 
     let { all_expr_ty = mkInvForAllTys qtvs (mkLamTypes dicts res_ty) } ;
     ty <- zonkTcType all_expr_ty ;
index 26f549b..e0989ae 100644 (file)
@@ -89,7 +89,7 @@ module TcRnMonad(
 
   -- * Type constraints
   newTcEvBinds, newNoTcEvBinds,
-  addTcEvBind,
+  addTcEvBind, addTopEvBinds,
   getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap,
   chooseUniqueOccTc,
   getConstraintVar, setConstraintVar,
@@ -1354,6 +1354,13 @@ debugTc thing
 ************************************************************************
 -}
 
+addTopEvBinds :: Bag EvBind -> TcM a -> TcM a
+addTopEvBinds new_ev_binds thing_inside
+  =updGblEnv upd_env thing_inside
+  where
+    upd_env tcg_env = tcg_env { tcg_ev_binds = tcg_ev_binds tcg_env
+                                               `unionBags` new_ev_binds }
+
 newTcEvBinds :: TcM EvBindsVar
 newTcEvBinds = do { binds_ref <- newTcRef emptyEvBindMap
                   ; tcvs_ref  <- newTcRef emptyVarSet
@@ -1425,6 +1432,9 @@ emitStaticConstraints static_lie
 
 emitConstraints :: WantedConstraints -> TcM ()
 emitConstraints ct
+  | isEmptyWC ct
+  = return ()
+  | otherwise
   = do { lie_var <- getConstraintVar ;
          updTcRef lie_var (`andWC` ct) }
 
index e8f0762..3458102 100644 (file)
@@ -93,7 +93,8 @@ module TcRnTypes(
         isDroppableCt, insolubleImplic,
         arisesFromGivens,
 
-        Implication(..), newImplication, implicLclEnv, implicDynFlags,
+        Implication(..), newImplication, implicationPrototype,
+        implicLclEnv, implicDynFlags,
         ImplicStatus(..), isInsolubleStatus, isSolvedStatus,
         SubGoalDepth, initialSubGoalDepth, maxSubGoalDepth,
         bumpSubGoalDepth, subGoalDepthExceeded,
@@ -2551,21 +2552,25 @@ data Implication
 newImplication :: TcM Implication
 newImplication
   = do env <- getEnv
-       pure $ Implic { -- These fields must be initialised
-                       ic_tclvl      = panic "newImplic:tclvl"
-                     , ic_binds      = panic "newImplic:binds"
-                     , ic_info       = panic "newImplic:info"
-
-                       -- The rest have sensible default values
-                     , ic_env        = env
-                     , ic_skols      = []
-                     , ic_telescope  = Nothing
-                     , ic_given      = []
-                     , ic_wanted     = emptyWC
-                     , ic_no_eqs     = False
-                     , ic_status     = IC_Unsolved
-                     , ic_need_inner = emptyVarSet
-                     , ic_need_outer = emptyVarSet }
+       return (implicationPrototype { ic_env = env })
+
+implicationPrototype :: Implication
+implicationPrototype
+   = Implic { -- These fields must be initialised
+              ic_tclvl      = panic "newImplic:tclvl"
+            , ic_binds      = panic "newImplic:binds"
+            , ic_info       = panic "newImplic:info"
+            , ic_env        = panic "newImplic:env"
+
+              -- The rest have sensible default values
+            , ic_skols      = []
+            , ic_telescope  = Nothing
+            , ic_given      = []
+            , ic_wanted     = emptyWC
+            , ic_no_eqs     = False
+            , ic_status     = IC_Unsolved
+            , ic_need_inner = emptyVarSet
+            , ic_need_outer = emptyVarSet }
 
 -- | Retrieve the enclosed 'TcLclEnv' from an 'Implication'.
 implicLclEnv :: Implication -> TcLclEnv
index 30a0cf9..6b593d8 100644 (file)
@@ -613,15 +613,16 @@ simplifyInfer :: TcLevel               -- Used when generating the constraints
               -> TcM ([TcTyVar],    -- Quantify over these type variables
                       [EvVar],      -- ... and these constraints (fully zonked)
                       TcEvBinds,    -- ... binding these evidence variables
-                      Bool)         -- True <=> there was an insoluble type error
-                                    --          in these bindings
+                      WantedConstraints, -- Redidual as-yet-unsolved constraints
+                      Bool)         -- True <=> the residual constraints are insoluble
+
 simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
   | isEmptyWC wanteds
   = do { gbl_tvs <- tcGetGlobalTyCoVars
        ; dep_vars <- zonkTcTypesAndSplitDepVars (map snd name_taus)
        ; qtkvs <- quantifyTyVars gbl_tvs dep_vars
        ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
-       ; return (qtkvs, [], emptyTcEvBinds, False) }
+       ; return (qtkvs, [], emptyTcEvBinds, emptyWC, False) }
 
   | otherwise
   = do { traceTc "simplifyInfer {"  $ vcat
@@ -692,10 +693,9 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
                                       , ctev_loc  = ct_loc }
                            | psig_theta_var <- psig_theta_vars ]
 
-       -- Now we can emil the residual constraints
-       ; emitResidualConstraints rhs_tclvl tc_env ev_binds_var
-                                 name_taus co_vars qtvs
-                                 bound_theta_vars
+       -- Now construct the residual constraint
+       ; residual_wanted <- mkResidualConstraints rhs_tclvl tc_env ev_binds_var
+                                 name_taus co_vars qtvs bound_theta_vars
                                  (wanted_transformed `andWC` mkSimpleWC psig_wanted)
 
          -- All done!
@@ -706,21 +706,23 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
               , text "qtvs ="       <+> ppr qtvs
               , text "definite_error =" <+> ppr definite_error ]
 
-       ; return ( qtvs, bound_theta_vars, TcEvBinds ev_binds_var, definite_error ) }
+       ; return ( qtvs, bound_theta_vars, TcEvBinds ev_binds_var
+                , residual_wanted, definite_error ) }
          -- NB: bound_theta_vars must be fully zonked
 
 
 --------------------
-emitResidualConstraints :: TcLevel -> Env TcGblEnv TcLclEnv -> EvBindsVar
-                        -> [(Name, TcTauType)]
-                        -> VarSet -> [TcTyVar] -> [EvVar]
-                        -> WantedConstraints -> TcM ()
+mkResidualConstraints :: TcLevel -> Env TcGblEnv TcLclEnv -> EvBindsVar
+                      -> [(Name, TcTauType)]
+                      -> VarSet -> [TcTyVar] -> [EvVar]
+                      -> WantedConstraints -> TcM WantedConstraints
 -- Emit the remaining constraints from the RHS.
 -- See Note [Emitting the residual implication in simplifyInfer]
-emitResidualConstraints rhs_tclvl tc_env ev_binds_var
+mkResidualConstraints rhs_tclvl tc_env ev_binds_var
                         name_taus co_vars qtvs full_theta_vars wanteds
   | isEmptyWC wanteds
-  = return ()
+  = return wanteds
+
   | otherwise
   = do { wanted_simple <- TcM.zonkSimples (wc_simple wanteds)
        ; let (outer_simple, inner_simple) = partitionBag is_mono wanted_simple
@@ -728,26 +730,23 @@ emitResidualConstraints rhs_tclvl tc_env ev_binds_var
 
         ; _ <- promoteTyVarSet (tyCoVarsOfCts outer_simple)
 
-        ; unless (isEmptyCts outer_simple) $
-          do { traceTc "emitResidualConstrants:simple" (ppr outer_simple)
-             ; emitSimples outer_simple }
-
-        ; implic <- newImplication
         ; let inner_wanted = wanteds { wc_simple = inner_simple }
-              implic'      = mk_implic inner_wanted implic
-        ; unless (isEmptyWC inner_wanted) $
-          do { traceTc "emitResidualConstraints:implic" (ppr implic')
-             ; emitImplication implic' }
-     }
+        ; return (WC { wc_simple = outer_simple
+                     , wc_impl   = mk_implic inner_wanted })}
   where
-    mk_implic inner_wanted implic
-       = implic { ic_tclvl  = rhs_tclvl
-                , ic_skols  = qtvs
-                , ic_given  = full_theta_vars
-                , ic_wanted = inner_wanted
-                , ic_binds  = ev_binds_var
-                , ic_info   = skol_info
-                , ic_env    = tc_env }
+    mk_implic inner_wanted
+      | isEmptyWC inner_wanted
+      = emptyBag
+      | otherwise
+      = unitBag (implicationPrototype { ic_tclvl  = rhs_tclvl
+                                      , ic_skols  = qtvs
+                                      , ic_telescope = Nothing
+                                      , ic_given  = full_theta_vars
+                                      , ic_wanted = inner_wanted
+                                      , ic_binds  = ev_binds_var
+                                      , ic_no_eqs = False
+                                      , ic_info   = skol_info
+                                      , ic_env    = tc_env })
 
     full_theta = map idType full_theta_vars
     skol_info  = InferSkol [ (name, mkSigmaTy [] full_theta ty)
@@ -783,8 +782,7 @@ put it outside.
 
 That is the reason for the partitionBag in emitResidualConstraints,
 which takes the CoVars free in the inferred type, and pulls their
-constraints out.  (NB: this set of CoVars should be
-closed-over-kinds.)
+constraints out.  (NB: this set of CoVars should be closed-over-kinds.)
 
 All rather subtle; see Trac #14584.
 
diff --git a/testsuite/tests/patsyn/should_fail/T15685.hs b/testsuite/tests/patsyn/should_fail/T15685.hs
new file mode 100644 (file)
index 0000000..6bb84c0
--- /dev/null
@@ -0,0 +1,13 @@
+{-# Language DataKinds, TypeOperators, PolyKinds, GADTs, PatternSynonyms #-}
+
+module T15685 where
+
+import Data.Kind
+
+data NS f as where
+ Here :: f a -> NS f (a:as)
+
+data NP :: (k -> Type) -> ([k] -> Type) where
+ Nil :: NP f '[]
+
+pattern HereNil = Here Nil
diff --git a/testsuite/tests/patsyn/should_fail/T15685.stderr b/testsuite/tests/patsyn/should_fail/T15685.stderr
new file mode 100644 (file)
index 0000000..13fc5a8
--- /dev/null
@@ -0,0 +1,10 @@
+
+T15685.hs:13:24: error:
+    • Kind mismatch: cannot unify (f :: a -> *) with:
+        NP a0 :: [k0] -> *
+      Their kinds differ.
+      Expected type: f a1
+        Actual type: NP a0 b0
+    • In the pattern: Nil
+      In the pattern: Here Nil
+      In the declaration for pattern synonym ‘HereNil’
diff --git a/testsuite/tests/patsyn/should_fail/T15692.hs b/testsuite/tests/patsyn/should_fail/T15692.hs
new file mode 100644 (file)
index 0000000..68c4aea
--- /dev/null
@@ -0,0 +1,9 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+module T15692 where
+
+data F x where
+  FS :: F (f a) -> F a
+
+pattern FS' = FS False
diff --git a/testsuite/tests/patsyn/should_fail/T15692.stderr b/testsuite/tests/patsyn/should_fail/T15692.stderr
new file mode 100644 (file)
index 0000000..42de53b
--- /dev/null
@@ -0,0 +1,13 @@
+
+T15692.hs:9:18: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Couldn't match expected type ‘F (f x)’ with actual type ‘Bool’
+    • In the pattern: False
+      In the pattern: FS False
+      In the declaration for pattern synonym ‘FS'’
+
+T15692.hs:9:18: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Couldn't match expected type ‘F (f0 x)’ with actual type ‘Bool’
+    • In the first argument of ‘FS’, namely ‘False’
+      In the expression: FS False
+      In an equation for ‘FS'’: FS' = FS False
+    • Relevant bindings include $bFS' :: F x (bound at T15692.hs:9:9)
index 81e6644..e726eaa 100644 (file)
@@ -44,3 +44,5 @@ test('T14498', normal, compile_fail, [''])
 test('T14552', normal, compile_fail, [''])
 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