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