## More expressive typechecking for pattern bindings

As part of adding Quick Look impredicativity #18126, Jurriaan produced this example:

```
combine :: (forall a . [a] -> a)
-> [forall a. a -> a]
-> ((forall a . [a] -> a), [forall a. a -> a])
combine x y = (x,y)
-- This does not typecheck
breaks = let (x,y) = combine head ids
in x y True
-- But this does
works = let t = combine head ids
in (fst t) (snd t) True
```

Why does one typecheck but not the other? Well, in `works`

, the defn of `t`

is

- Non-recursive
- Has no signature

so GHC takes a special code path, and

- First infers the type of the RHS
- And then (after generalisation) takes that as the type of
`t`

The code is in `GHC.Tc.Gen.Bind.tcMonoBinds`

:

```
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
...
```

So now it should be clear why `works`

typechecks.

What about `breaks`

? For a *pattern binding* like `(x,y) = rhs`

, GHC has no special case, so it looks at the LHS first, giving every variable in the pattern a monotype. (This is the default because the binding might be recursive.)

This is not just theoretical: this example comes from the `fixed-vector`

package, which somehow limped along with the old `ImpredicativeTypes`

.

Obvious idea: why not extend the special case from `FunBind`

to `PatBind`

. For a non-recursive pattern binding,

- Infer the type of the RHS
- And
*then*typecheck the pattern, pushing the RHS type into it.

This only matters when we have impredicative types, because only then do we have types like `(forall ..., forall ...)`

.