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

14 files changed, 169 insertions, 64 deletions

diff --git a/compiler/GHC/Hs/Binds.hs b/compiler/GHC/Hs/Binds.hs
index 0933e9ba7e..327aeea2c0 100644
--- a/compiler/GHC/Hs/Binds.hs
+++ b/compiler/GHC/Hs/Binds.hs
@@ -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
diff --git a/compiler/GHC/HsToCore/Binds.hs b/compiler/GHC/HsToCore/Binds.hs
index 5e01bc7a8f..8e54489f1e 100644
--- a/compiler/GHC/HsToCore/Binds.hs
+++ b/compiler/GHC/HsToCore/Binds.hs
@@ -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
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index 144a652484..f15434e405 100644
--- a/compiler/GHC/HsToCore/Expr.hs
+++ b/compiler/GHC/HsToCore/Expr.hs
@@ -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
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index 7cf3126bbf..d52b3dd1cd 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -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
diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs
index b68e0db87c..d978f5dbf3 100644
--- a/compiler/GHC/Tc/Gen/Match.hs
+++ b/compiler/GHC/Tc/Gen/Match.hs
@@ -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 }
diff --git a/compiler/GHC/Tc/Gen/Match.hs-boot b/compiler/GHC/Tc/Gen/Match.hs-boot
index 692d04b884..bb194a3cf1 100644
--- a/compiler/GHC/Tc/Gen/Match.hs-boot
+++ b/compiler/GHC/Tc/Gen/Match.hs-boot
@@ -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
diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs
index 42a89cf633..cf25fea60c 100644
--- a/compiler/GHC/Tc/Utils/Zonk.hs
+++ b/compiler/GHC/Tc/Utils/Zonk.hs
@@ -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 })
diff --git a/testsuite/tests/typecheck/should_compile/T18323.hs b/testsuite/tests/typecheck/should_compile/T18323.hs
new file mode 100644
index 0000000000..5f47d783ea
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T18323.hs
@@ -0,0 +1,29 @@
+{-# 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
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 0ef2d9ef34..b2dc105b60 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -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, [''])
+
diff --git a/testsuite/tests/typecheck/should_fail/T8570.stderr b/testsuite/tests/typecheck/should_fail/T8570.stderr
index 75d736cf1d..d79ea6581f 100644
--- a/testsuite/tests/typecheck/should_fail/T8570.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8570.stderr
@@ -1,6 +1,12 @@
 
-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
diff --git a/testsuite/tests/typecheck/should_fail/tcfail004.stderr b/testsuite/tests/typecheck/should_fail/tcfail004.stderr
index 0d4f700910..c64876c6ab 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail004.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail004.stderr
@@ -1,9 +1,6 @@
 
-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)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail005.stderr b/testsuite/tests/typecheck/should_fail/tcfail005.stderr
index 8da93af1e2..5bfaf6a7a1 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail005.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail005.stderr
@@ -1,9 +1,6 @@
 
-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)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail012.stderr b/testsuite/tests/typecheck/should_fail/tcfail012.stderr
index ea5a2a72cd..d2f07f4420 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail012.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail012.stderr
@@ -1,5 +1,5 @@
 
-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 = []
diff --git a/testsuite/tests/warnings/should_fail/CaretDiagnostics1.stderr b/testsuite/tests/warnings/should_fail/CaretDiagnostics1.stderr
index aa02b8655a..c2ff69c9ef 100644
--- a/testsuite/tests/warnings/should_fail/CaretDiagnostics1.stderr
+++ b/testsuite/tests/warnings/should_fail/CaretDiagnostics1.stderr
@@ -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'