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
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
I ran into the above two examples in test cases
T20363b, trying to allow this test case to compile by using PHASE 2 of the
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.