Function which prints truth table for any boolean function in Idris

BooleanFunction.idr

first : (a -> b) -> (a, c) -> (b, c)
first f (x, y) = (f x, y)

interface BooleanFunction a where
  makeTable : a -> List (List Bool, Bool)

BooleanFunction Bool where
    makeTable result = [([], result)]

BooleanFunction a => BooleanFunction (Bool -> a) where
    makeTable f = do
        arg <- [True, False]
        restTable <- makeTable (f arg)
        pure $ first (arg::) restTable

BooleanFunction a => BooleanFunction (Lazy Bool -> a) where
    makeTable f = do
        arg <- [True, False]
        restTable <- makeTable (f arg)
        pure $ first (arg::) restTable

printTruthTable : BooleanFunction a => a -> IO ()
printTruthTable f = do
    let table = makeTable f
    for_ table printRow
  where
    boolToAlignedStr : Bool -> String
    boolToAlignedStr True  = "True  "
    boolToAlignedStr False = "False "

    printRow : (List Bool, Bool) -> IO ()
    printRow (args, ans) = do
        for_ args (putStr . boolToAlignedStr)
        putStr "= "
        print ans
        putStr "\n"