A purely linear clear bits

LinearClearBits.hs

{-# LANGUAGE GHC2024, LinearTypes #-}
module LinearClearBits where

data With3 a b c where
  With3 :: x %1 -> (x %1 -> a) -> (x %1 -> b) -> (x %1 -> c) -> With3 a b c

w1 :: With3 a b c %1 -> a
w1 (With3 x f _ _) = f x

w2 :: With3 a b c %1 -> b
w2 (With3 x _ g _) = g x

w3 :: With3 a b c %1 -> c
w3 (With3 x _ _ h) = h x

data Bin = Bin { caseBin :: forall r. With3 (Bin %1 -> r) (Bin %1 -> r) r %1 -> r }

clearBitsBin :: Bin %1 -> Bin
clearBitsBin (Bin b) = Bin (\w -> b (With3 w (\w' p -> w1 w' (clearBitsBin p)) (\w' p -> w1 w' (clearBitsBin p)) (\w' -> w3 w')))