simple_app fails to beta-reduce through casts
simple_app
sometimes misses beta reduction opportunities because of intervening casts.
See also #21346 (closed)
Example 1: casted lambda
simple_app
does not reduce the application of a casted lambda abstraction to an argument, e.g. (lam |> co) arg
. This fails to beta reduce because simple_app
does not look through casts to find lambda expressions. Simply calling exprIsLambda_maybe
instead of pattern matching on Lam
in simple_app
allows beta reduction to take place.
Example 2: lambda, argument, cast, argument
simple_app
fails to collect arguments through casts, e.g. in ( (lam arg1) |> co ) arg2
we will beta reduce lam arg1
but then fail to beta reduce the application of the result to the second argument. This problem persists after fixing the previous issue. I'm not sure what the correct solution is, something like the following perhaps (after the case in simple_app
that deals with lambdas, as we want to push the coercion through the lambda and not into the arguments in that case):
simple_app env (Cast fun co) args
| (envs, as) <- unzip args
, Just (as, mco) <- pushCoArgs co as
= mkCastMCo (simple_app env fun $ zip envs as) mco
Why this matters
We rely on the simple optimiser to beta reduce away the representation-polymorphic lambdas introduced by the desugaring of data constructors, as explained in Note [Typechecking data constructors] in GHC.Tc.Gen.Head
. If we don't properly beta-reduce these representation-polymorphic lambdas, we violate the representation polymorphism invariants, which could cause GHC to crash (e.g. on typePrimRep
).
I ran into the above two examples in test cases T20363
/T20363b
, trying to allow this test case to compile by using PHASE 2 of the FixedRuntimeRep
plan.
Alternatives
I am still wondering whether we can figure out another way to handle the multiplicities in data constructors that would avoid having to perform this dodgy eta expansion. Perhaps @monoidal @rae have some ideas about this, because I really don't like having to rely on fragile optimisations to simplify away invalid Core. I would encourage you to think about hasFixedRuntimeRep_remainingValArgs
: this function precisely checks that we can eta expand, so we should be able to use the information therein to actually perform the correct eta expansion!
I have the following kind of examples in mind here:
type family RR :: RuntimeRep where
RR = LiftedRep
type family C :: TYPE RR where
C = Char
newtype T :: TYPE RR where
MkT :: C -> T
g :: Char -> T
g = MkT
-- Here we should eta-expand 'MkT' to
--
-- \ (ds :: (C |> TYPE RR[O])) -> ...
--
-- and not
--
-- \ (ds :: C) -> ...
--
-- (Even though 'C' is the 'origArgTy' stored in the 'MkT' data constructor,
-- it's not what we should use for eta expansion.)
type Q :: forall (r :: RuntimeRep). TYPE r -> TYPE r
newtype Q a where
MkQ :: forall (r :: RuntimeRep) (a :: TYPE r). a -> MkQ a
q = MkQ @IntRep
-- Here I believe we need to handle the whole application, as if
-- we simply eta-expanded 'MkQ' to lam = /\ (a :: TYPE IntRep). \ (ds :: a) -> ...
-- then the type application "lam @IntRep" wouldn't make sense.