Handle application chains all at once in the simplifier and Core Lint
The implementation of quick look impredicativity refactored the treatment of applications in the typechecker: now in tcApp
we look at an application chain in its entirely before deciding how to proceed.
It seems judicious to extend this treatment to other places in the compiler, such as the simplifier and Core Lint.
One motivation for this is that we want to be able to look through casts when looking at application chains. For example, we might have:
type RR :: RuntimeRep
type family RR where { RR = IntRep }
-- Core
( (# , #) @LiftedRep @RR e1 ) |> co 3#
-- where
-- co :: (ty :: TYPE RR) ~# (Int# :: TYPE IntRep)
Here we can't eta-expand (# , #) @LiftedRep @RR e1
on its own because we would introduce a binder whose type would have kind TYPE RR
, but RR
is not concrete. With the cast, we're OK. However, the simplifier and Core Lint aren't set up to handle application chains of the form (in which casts appear). Without supporting casts in such positions, we can't implement PHASE 2 of the FixedRuntimeRep plan for partial applications of Id
s with representation-polymorphic arguments (such as coerce
, unsafeCoerce#
, rightSection
, newtype constructors with UnliftedNewtypes
).
See this comment, and following, for a discussion of some of the issues here.