Commit 9ebfa03d authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fail fast on pattern synonyms

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.
parent 02b303ee
......@@ -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 $
......
......@@ -1667,8 +1667,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
......
......@@ -52,7 +52,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"
......@@ -68,21 +68,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
......@@ -97,30 +99,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
......@@ -133,15 +145,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
......@@ -175,7 +184,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 ()
......
......@@ -481,11 +481,8 @@ run_th_modfinalizers = do
-- (see #12777).
new_ev_binds <- {-# SCC "simplifyTop2" #-}
simplifyTop (lie_th `andWC` lie_top_decls)
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, WantedConstraints)
......@@ -2326,17 +2323,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 ;
......
......@@ -90,7 +90,7 @@ module TcRnMonad(
-- * Type constraints
newTcEvBinds, newNoTcEvBinds, cloneEvBindsVar,
addTcEvBind,
addTcEvBind, addTopEvBinds,
getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap,
chooseUniqueOccTc,
getConstraintVar, setConstraintVar,
......@@ -1359,6 +1359,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
......@@ -1442,6 +1449,9 @@ emitStaticConstraints static_lie
emitConstraints :: WantedConstraints -> TcM ()
emitConstraints ct
| isEmptyWC ct
= return ()
| otherwise
= do { lie_var <- getConstraintVar ;
updTcRef lie_var (`andWC` ct) }
......
......@@ -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,
......@@ -2557,21 +2558,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
......
......@@ -668,15 +668,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
......@@ -747,10 +748,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!
......@@ -761,21 +761,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
......@@ -783,26 +785,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)
......@@ -838,8 +837,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.
......
{-# 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
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’
{-# 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
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)
......@@ -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
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment