Casts get in the way of join points

I was checking which of HLint’s rewirte rules are actually already known to the compiler in the sense that the simplifier can do them (using [ghc-proofs](http://hackage.haskell.org/package/ghc-proofs). I stumbled on this interesting case.

foldr @[] (&&) True xs compiles down to this nice core

        joinrec {
          go [Occ=LoopBreaker] :: [Bool] -> Bool
          [LclId[JoinId(1)],
           Arity=1,
           Unf=Unf{Src=<vanilla>, TopLvl=False, Value=True, ConLike=True,
                   WorkFree=True, Expandable=True, Guidance=IF_ARGS [30] 44 20}]
          go (ds :: [Bool])
            = case ds of {
                [] -> GHC.Types.True;
                : y ys ->
                  case y of {
                    False -> GHC.Types.False;
                    True -> jump go ys
                  }
              }; } in
        jump go xs

But and @[] xs (which HLint suggests to use instead, and we surely want people to use!) compiles down to

          go [Occ=LoopBreaker] :: [Bool] -> All
          [LclId,
           Arity=1,
           Unf=Unf{Src=<vanilla>, TopLvl=False, Value=True, ConLike=True,
                   WorkFree=True, Expandable=True, Guidance=IF_ARGS [30] 60 20}]
          go
            = \ (ds :: [Bool]) ->
                case ds of {
                  [] ->
                    GHC.Types.True
                    `cast` (Sym Data.Monoid.N:All[0] :: Coercible Bool All);
                  : y ys ->
                    case y of {
                      False ->
                        GHC.Types.False
                        `cast` (Nth:3
                                  (Nth:3
                                     ((Sym Data.Monoid.N:All[0]
                                       -> Sym Data.Monoid.N:All[0] -> <Bool>_R)
                                      ; (<All>_R -> <All>_R -> Sym Data.Monoid.N:All[0])))
                                :: Coercible Bool All);
                      True -> go ys
                    }
                }; } in
        (go xs) `cast` (Data.Monoid.N:All[0] :: Coercible All Bool)

If you squint and ignore all the casts, these two expressions are the same. So it would be very desirable to get a joinrec for and xs as well.

Note that all “exit paths” of the return function cast from Bool to All, and the return value of the whole recursion casts back. That looks as if some smart floating of coercions could do the job. Maybe the common context transformation (https://mail.haskell.org/pipermail/ghc-devs/2013-December/003481.html)?

Is this tied to GHC’s deviation of the paper to have a fixed return type for a join point?

Trac metadata

Trac field	Value
Version	8.2.1
Type	Task
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture