Commit eb9bdaef authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Marge Bot

Add right-to-left rule for pattern bindings

Fix #18323 by adding a few lines of code to handle non-recursive
pattern bindings.  see GHC.Tc.Gen.Bind
Note [Special case for non-recursive pattern bindings]

Alas, this confused the pattern-match overlap checker; see #18323.

Note that this patch only affects pattern bindings like that
for (x,y) in this program

  combine :: (forall a . [a] -> a) -> [forall a. a -> a]
          -> ((forall a . [a] -> a), [forall a. a -> a])

  breaks = let (x,y) = combine head ids
           in x y True

We need ImpredicativeTypes for those [forall a. a->a] types to be
valid. And with ImpredicativeTypes the old, unprincipled "allow
unification variables to unify with a polytype" story actually
works quite well. So this test compiles fine (if delicatedly) with
old GHCs; but not with QuickLook unless we add this patch
parent 731c8d3b
......@@ -317,18 +317,13 @@ data HsBindLR idL idR
| XHsBindsLR !(XXHsBindsLR idL idR)
data NPatBindTc = NPatBindTc {
pat_fvs :: NameSet, -- ^ Free variables
pat_rhs_ty :: Type -- ^ Type of the GRHSs
} deriving Data
type instance XFunBind (GhcPass pL) GhcPs = NoExtField
type instance XFunBind (GhcPass pL) GhcRn = NameSet -- Free variables
type instance XFunBind (GhcPass pL) GhcTc = HsWrapper -- See comments on FunBind.fun_ext
type instance XPatBind GhcPs (GhcPass pR) = NoExtField
type instance XPatBind GhcRn (GhcPass pR) = NameSet -- Free variables
type instance XPatBind GhcTc (GhcPass pR) = NPatBindTc
type instance XPatBind GhcTc (GhcPass pR) = Type -- Type of the GRHSs
type instance XVarBind (GhcPass pL) (GhcPass pR) = NoExtField
type instance XAbsBinds (GhcPass pL) (GhcPass pR) = NoExtField
......
......@@ -182,7 +182,7 @@ dsHsBind dflags b@(FunBind { fun_id = L loc fun
return (force_var, [core_binds]) }
dsHsBind dflags (PatBind { pat_lhs = pat, pat_rhs = grhss
, pat_ext = NPatBindTc _ ty
, pat_ext = ty
, pat_ticks = (rhs_tick, var_ticks) })
= do { rhss_deltas <- checkGRHSs PatBindGuards grhss
; body_expr <- dsGuarded grhss ty rhss_deltas
......
......@@ -212,7 +212,7 @@ dsUnliftedBind (FunBind { fun_id = L l fun
; return (bindNonRec fun rhs' body) }
dsUnliftedBind (PatBind {pat_lhs = pat, pat_rhs = grhss
, pat_ext = NPatBindTc _ ty }) body
, pat_ext = ty }) body
= -- let C x# y# = rhs in body
-- ==> case rhs of C x# y# -> body
do { match_deltas <- checkGRHSs PatBindGuards grhss
......
......@@ -1274,20 +1274,15 @@ tcMonoBinds :: RecFlag -- Whether the binding is recursive for typechecking pur
-> TcSigFun -> LetBndrSpec
-> [LHsBind GhcRn]
-> TcM (LHsBinds GhcTc, [MonoBindInfo])
-- SPECIAL CASE 1: see Note [Inference for non-recursive function bindings]
tcMonoBinds is_rec sig_fn no_gen
[ L b_loc (FunBind { fun_id = L nm_loc name
, fun_matches = matches })]
-- Single function binding,
| NonRecursive <- is_rec -- ...binder isn't mentioned in RHS
, Nothing <- sig_fn name -- ...with no type signature
= -- Note [Single function non-recursive binding special-case]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- In this very special case we infer the type of the
-- right hand side first (it may have a higher-rank type)
-- and *then* make the monomorphic Id for the LHS
-- e.g. f = \(x::forall a. a->a) -> <body>
-- We want to infer a higher-rank type for f
setSrcSpan b_loc $
= setSrcSpan b_loc $
do { ((co_fn, matches'), rhs_ty)
<- tcInfer $ \ exp_ty ->
tcExtendBinderStack [TcIdBndr_ExpType name exp_ty NotTopLevel] $
......@@ -1305,6 +1300,29 @@ tcMonoBinds is_rec sig_fn no_gen
, mbi_sig = Nothing
, mbi_mono_id = mono_id }]) }
-- SPECIAL CASE 2: see Note [Inference for non-recursive pattern bindings]
tcMonoBinds is_rec sig_fn no_gen
[L b_loc (PatBind { pat_lhs = pat, pat_rhs = grhss })]
| NonRecursive <- is_rec -- ...binder isn't mentioned in RHS
, all (isNothing . sig_fn) bndrs
= addErrCtxt (patMonoBindsCtxt pat grhss) $
do { (grhss', pat_ty) <- tcInfer $ \ exp_ty ->
tcGRHSsPat grhss exp_ty
; let exp_pat_ty :: Scaled ExpSigmaType
exp_pat_ty = unrestricted (mkCheckExpType pat_ty)
; (pat', mbis) <- tcLetPat (const Nothing) no_gen pat exp_pat_ty $
mapM lookupMBI bndrs
; return ( unitBag $ L b_loc $
PatBind { pat_lhs = pat', pat_rhs = grhss'
, pat_ext = pat_ty, pat_ticks = ([],[]) }
, mbis ) }
where
bndrs = collectPatBinders pat
-- GENERAL CASE
tcMonoBinds _ sig_fn no_gen binds
= do { tc_binds <- mapM (wrapLocM (tcLhs sig_fn no_gen)) binds
......@@ -1327,6 +1345,66 @@ tcMonoBinds _ sig_fn no_gen binds
; return (listToBag binds', mono_infos) }
{- Note [Special case for non-recursive function bindings]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In the special case of
* A non-recursive FunBind
* With no type signature
we infer the type of the right hand side first (it may have a
higher-rank type) and *then* make the monomorphic Id for the LHS e.g.
f = \(x::forall a. a->a) -> <body>
We want to infer a higher-rank type for f
Note [Special case for non-recursive pattern bindings]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In the special case of
* A pattern binding
* With no type signature for any of the binders
we can /infer/ the type of the RHS, and /check/ the pattern
against that type. For example (#18323)
ids :: [forall a. a -> a]
combine :: (forall a . [a] -> a) -> [forall a. a -> a]
-> ((forall a . [a] -> a), [forall a. a -> a])
(x,y) = combine head ids
with -XImpredicativeTypes we can infer a good type for
(combine head ids), and use that to tell us the polymorphic
types of x and y.
We don't need to check -XImpredicativeTypes beucase without it
these types like [forall a. a->a] are illegal anyway, so this
special case code only really has an effect if -XImpredicativeTypes
is on. Small exception:
(x) = e
is currently treated as a pattern binding so, even absent
-XImpredicativeTypes, we will get a small improvement in behaviour.
But I don't think it's worth an extension flag.
Why do we require no type signatures on /any/ of the binders?
Consider
x :: forall a. a->a
y :: forall a. a->a
(x,y) = (id,id)
Here we should /check/ the RHS with expected type
(forall a. a->a, forall a. a->a).
If we have no signatures, we can the approach of this Note
to /infer/ the type of the RHS.
But what if we have some signatures, but not all? Say this:
p :: forall a. a->a
(p,q) = (id, (\(x::forall b. b->b). x True))
Here we want to push p's signature inwards, i.e. /checking/, to
correctly elaborate 'id'. But we want to /infer/ q's higher rank
type. There seems to be no way to do this. So currently we only
switch to inference when we have no signature for any of the binders.
-}
------------------------
-- tcLhs typechecks the LHS of the bindings, to construct the environment in which
......@@ -1394,7 +1472,7 @@ tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss })
-- The above inferred type get an unrestricted multiplicity. It may be
-- worth it to try and find a finer-grained multiplicity here
-- if examples warrant it.
mapM lookup_info nosig_names
mapM lookupMBI nosig_names
; let mbis = sig_mbis ++ nosig_mbis
......@@ -1412,19 +1490,19 @@ tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss })
Just (TcIdSig sig) -> Right (name, sig)
_ -> Left name
-- After typechecking the pattern, look up the binder
-- names that lack a signature, which the pattern has brought
-- into scope.
lookup_info :: Name -> TcM MonoBindInfo
lookup_info name
= do { mono_id <- tcLookupId name
; return (MBI { mbi_poly_name = name
, mbi_sig = Nothing
, mbi_mono_id = mono_id }) }
tcLhs _ _ other_bind = pprPanic "tcLhs" (ppr other_bind)
-- AbsBind, VarBind impossible
lookupMBI :: Name -> TcM MonoBindInfo
-- After typechecking the pattern, look up the binder
-- names that lack a signature, which the pattern has brought
-- into scope.
lookupMBI name
= do { mono_id <- tcLookupId name
; return (MBI { mbi_poly_name = name
, mbi_sig = Nothing
, mbi_mono_id = mono_id }) }
-------------------
tcLhsSigId :: LetBndrSpec -> (Name, TcIdSigInfo) -> TcM MonoBindInfo
tcLhsSigId no_gen (name, sig)
......@@ -1467,15 +1545,9 @@ tcRhs (TcPatBind infos pat' grhss pat_ty)
tcExtendIdBinderStackForRhs infos $
do { traceTc "tcRhs: pat bind" (ppr pat' $$ ppr pat_ty)
; grhss' <- addErrCtxt (patMonoBindsCtxt pat' grhss) $
tcScalingUsage Many $
-- Like in tcMatchesFun, this scaling happens because all
-- let bindings are unrestricted. A difference, here, is
-- that when this is not the case, any more, we will have to
-- make sure that the pattern is strict, otherwise this will
-- be desugar to incorrect code.
tcGRHSsPat grhss pat_ty
tcGRHSsPat grhss (mkCheckExpType pat_ty)
; return ( PatBind { pat_lhs = pat', pat_rhs = grhss'
, pat_ext = NPatBindTc emptyNameSet pat_ty
, pat_ext = pat_ty
, pat_ticks = ([],[]) } )}
tcExtendTyVarEnvForRhs :: Maybe TcIdSigInst -> TcM a -> TcM a
......
......@@ -157,10 +157,17 @@ tcMatchLambda herald match_ctxt match res_ty
-- @tcGRHSsPat@ typechecks @[GRHSs]@ that occur in a @PatMonoBind@.
tcGRHSsPat :: GRHSs GhcRn (LHsExpr GhcRn) -> TcRhoType
tcGRHSsPat :: GRHSs GhcRn (LHsExpr GhcRn) -> ExpRhoType
-> TcM (GRHSs GhcTc (LHsExpr GhcTc))
-- Used for pattern bindings
tcGRHSsPat grhss res_ty = tcGRHSs match_ctxt grhss (mkCheckExpType res_ty)
tcGRHSsPat grhss res_ty
= tcScalingUsage Many $
-- Like in tcMatchesFun, this scaling happens because all
-- let bindings are unrestricted. A difference, here, is
-- that when this is not the case, any more, we will have to
-- make sure that the pattern is strict, otherwise this will
-- desugar to incorrect code.
tcGRHSs match_ctxt grhss res_ty
where
match_ctxt = MC { mc_what = PatBindRhs,
mc_body = tcBody }
......
......@@ -2,13 +2,13 @@ module GHC.Tc.Gen.Match where
import GHC.Hs ( GRHSs, MatchGroup, LHsExpr )
import GHC.Tc.Types.Evidence ( HsWrapper )
import GHC.Types.Name ( Name )
import GHC.Tc.Utils.TcType( ExpSigmaType, TcRhoType )
import GHC.Tc.Utils.TcType( ExpSigmaType, ExpRhoType )
import GHC.Tc.Types ( TcM )
import GHC.Types.SrcLoc ( Located )
import GHC.Hs.Extension ( GhcRn, GhcTc )
tcGRHSsPat :: GRHSs GhcRn (LHsExpr GhcRn)
-> TcRhoType
-> ExpRhoType
-> TcM (GRHSs GhcTc (LHsExpr GhcTc))
tcMatchesFun :: Located Name
......
......@@ -533,12 +533,12 @@ zonk_lbind env = wrapLocM (zonk_bind env)
zonk_bind :: ZonkEnv -> HsBind GhcTc -> TcM (HsBind GhcTc)
zonk_bind env bind@(PatBind { pat_lhs = pat, pat_rhs = grhss
, pat_ext = NPatBindTc fvs ty})
, pat_ext = ty})
= do { (_env, new_pat) <- zonkPat env pat -- Env already extended
; new_grhss <- zonkGRHSs env zonkLExpr grhss
; new_ty <- zonkTcTypeToTypeX env ty
; return (bind { pat_lhs = new_pat, pat_rhs = new_grhss
, pat_ext = NPatBindTc fvs new_ty }) }
, pat_ext = new_ty }) }
zonk_bind env (VarBind { var_ext = x
, var_id = var, var_rhs = expr })
......
{-# LANGUAGE ImpredicativeTypes #-}
-- Tests SPECIAL CASE 2 in GHC.Tc.Gen.Bind.tcMonoBinds
-- See Note [Special case for non-recursive pattern bindings]
--
-- Doesn't have any useful effect until we have
-- ImpredicativeTypes, but does no harm either
module T18323 where
ids :: [forall a. a -> a]
ids = [id]
combine :: (forall a . [a] -> a)
-> [forall a. a -> a]
-> ((forall a . [a] -> a), [forall a. a -> a])
combine x y = (x,y)
-- This works
works = let t = combine head ids
in (fst t) (snd t) True
-- But this does not typecheck, and it could
breaks = let (x,y) = combine head ids
in x y True
-- And nor does this, but it could too
breaks2 = let (t) = combine head ids
in (fst t) (snd t) True
......@@ -720,3 +720,5 @@ test('T17775-viewpats-d', normal, compile_fail, [''])
test('T18118', normal, multimod_compile, ['T18118', '-v0'])
test('T18412', normal, compile, [''])
test('T18470', normal, compile, [''])
test('T18323', normal, compile, [''])
T8570.hs:6:18:
Constructor ‘Image’ does not have field ‘filepath’
In the pattern: Image {filepath = x}
In a pattern binding: Image {filepath = x} = logo
In the expression: let Image {filepath = x} = logo in x
T8570.hs:6:11: error:
• Couldn't match expected type ‘Image’ with actual type ‘Field’
• In the pattern: Image {filepath = x}
In a pattern binding: Image {filepath = x} = logo
In the expression: let Image {filepath = x} = logo in x
T8570.hs:6:18: error:
• Constructor ‘Image’ does not have field ‘filepath’
• In the pattern: Image {filepath = x}
In a pattern binding: Image {filepath = x} = logo
In the expression: let Image {filepath = x} = logo in x
tcfail004.hs:3:9: error:
• Couldn't match expected type: (a, b)
with actual type: (a0, b0, c0)
• In the expression: (1, 2, 3)
tcfail004.hs:3:1: error:
• Couldn't match expected type: (a0, b0, c0)
with actual type: (a, b)
• In the pattern: (f, g)
In a pattern binding: (f, g) = (1, 2, 3)
• Relevant bindings include
f :: a (bound at tcfail004.hs:3:2)
g :: b (bound at tcfail004.hs:3:4)
tcfail005.hs:3:9: error:
• Couldn't match expected type: [a]
with actual type: (a0, Char)
• In the expression: (1, 'a')
tcfail005.hs:3:2: error:
• Couldn't match expected type: (a0, Char)
with actual type: [a]
• In the pattern: h : i
In a pattern binding: (h : i) = (1, 'a')
• Relevant bindings include
h :: a (bound at tcfail005.hs:3:2)
i :: [a] (bound at tcfail005.hs:3:4)
tcfail012.hs:3:8: error:
• Couldn't match expected type ‘Bool’ with actual type ‘[a0]
• In the expression: []
tcfail012.hs:3:1: error:
• Couldn't match expected type ‘[a0]’ with actual type ‘Bool
• In the pattern: True
In a pattern binding: True = []
......@@ -59,7 +59,7 @@ CaretDiagnostics1.hs:13:7-11: error:
| ^^^^^
CaretDiagnostics1.hs:(13,16)-(14,13): error:
• Couldn't match expected type ‘Char -> p0’ with actual type ‘()’
• Couldn't match expected type ‘Char -> t0’ with actual type ‘()’
• The function ‘()’ is applied to one value argument,
but its type ‘()’ has none
In the expression: () '0'
......
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