## 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 |