GitLab

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.