IntersectMBO
Make `matchList` lazy and add a strict version alongside
On current master in the builtinListIndexing.pir.golden test we have the following:
chooseList
{data}
{Unit -> Unit -> data}
xs
(\(ds : Unit) -> error {Unit -> data})
(\(ds : Unit) (ds : Unit) ->
let
!hd : data = headList {data} xs
!tl : list data = tailList {data} xs
in <...>
Clearly we don't need two Unit arguments, how do we get them? This code is a compiled version of
go :: BI.BuiltinList a -> Integer -> a
go xs i =
Builtins.matchList
xs
(\_ -> traceError builtinListIndexTooLargeError)
( \hd tl _ -> <...>)
()
which makes sense, we don't want to evaluate the nil case and fail at the very first element.
But why two Units? That's because matchList has a Unit inside of it to make pattern matching on lists lazy:
matchList :: forall a r . BI.BuiltinList a -> r -> (a -> BI.BuiltinList a -> r) -> r
matchList l nilCase consCase = BI.chooseList l (const nilCase) (\_ -> consCase (BI.head l) (BI.tail l)) ()
But it doesn't make the matching actually lazy! matchList always forces nilCase, so putting () inside of matchList doesn't help with laziness as that point nilCase is already forced. So we have to do the () dance again and end up with two unit arguments, which is kinda ridiculous.
I think we should have two matchList functions instead:
matchList :: forall a r . BI.BuiltinList a -> (() -> r) -> (a -> BI.BuiltinList a -> r) -> r
matchList' :: forall a r . BI.BuiltinList a -> r -> (a -> BI.BuiltinList a -> r) -> r
one for lazy matching and one for strict matching.
Actually, we do have the pointless double Units, so I'm reopening the issue until that is fixed.