Failure of arity trimming leads to simplifer loop
Try compiling typecheck/should_compile/T13458
with -fmax-simplifier-iterations=8
. You'll see
==================== Simplifier iteration=4 ====================
---- Simplifier counts for Simplifier iteration=4
Total ticks: 1
1 EtaExpansion 1 unsafeCoerce'
1 SimplifierDone 1
---- End of simplifier counts for Simplifier iteration=4
==================== Simplifier iteration=5 ====================
---- Simplifier counts for Simplifier iteration=5
Total ticks: 1
1 EtaExpansion 1 unsafeCoerce'
1 SimplifierDone 1
etc, forever. The offending definition is
T13458.unsafeCoerce' :: forall (r :: GHC.Types.RuntimeRep) (a :: TYPE r) (b :: TYPE r). a -> b
T13458.unsafeCoerce'
= \ (@(r_azh :: GHC.Types.RuntimeRep))
(@(a_azi :: TYPE r_azh))
(@(b_azj :: TYPE r_azh)) ->
case Unsafe.Coerce.unsafeEqualityProof
@(*) @(GHC.Types.Any -> GHC.Types.Any) @(a_azi -> b_azj)
of
{ Unsafe.Coerce.UnsafeRefl co_azF ->
(GHC.Base.id @GHC.Types.Any)
`cast` (Sub (Sym co_azF)
:: (GHC.Types.Any -> GHC.Types.Any) ~R# (a_azi -> b_azj))
}
We can't eta-expand this because that would make a runtime-rep-poly lambda. So we don't. But tryEtaExpandRhs
thinks it can, and does a tick. So the simplifier loops.
That is bad.
Also note that we will ultimately use plain id
to make a runtime-rep-poly call, which is bad bad bad. Maybe that's what you get if you use unsafeCorece
, but it's something to bear in mind when in thinking about runtime-rep polymorphism.
Another example of the same problem is typecheck/should_compile/T17723a
(compile this with -O
). Here the offending defn is
T17723a.$dmm
:: forall (r :: RuntimeRep) (a :: TYPE r). (C a, r ~ LiftedRep) => a -> ()
T17723a.$dmm
= \ (@(r_aiH :: RuntimeRep))
(@(a_awy :: TYPE r_aiH))
_ [Occ=Dead]
($d~_aDV :: r_aiH ~ LiftedRep) ->
case GHC.Types.eq_sel @RuntimeRep @r_aiH @LiftedRep $d~_aDV
of co_aE6
{ __DEFAULT ->
(\ _ [Occ=Dead] -> GHC.Tuple.())
`cast` (Sym (GRefl representational a_awy (TYPE co_aE6)_N)
%<'Many>_N ->_R <()>_R
:: ((a_awy |> (TYPE co_aE6)_N) -> ()) ~R# (a_awy -> ()))
}
which again we cannot straightforwardly eta-expand. This time there is no real problem (it's just that the Simplifier can't take advantage of the equality) but we still should not loop.