A failed attempt at prooving that a ^ b * a ^ c = a ^ (b + c) with Liquid Haskell

liquid-proof.hs

{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--no-adt" @-}

import Language.Haskell.Liquid.ProofCombinators


-- | Proof that a ^ b * a ^ c = a ^ (b + c)
--
-- a ^ b * a ^ c corresponds to (b -> a, c -> a)
-- a ^ (b + c) corresponds to Either b c -> a


{-@ reflect f' @-}
f' :: (b -> a, c -> a) -> Either b c -> a
f' (l, r) e =
  case e of
    Left y -> l y
    Right z -> r z

{-@ reflect compose @-}
compose :: (a -> b) -> (c -> a) -> c -> b
compose f g z = f (g z)

{-@ reflect g' @-}
g' :: (Either b c -> a) -> (b -> a, c -> a)
g' h = (compose h Left, compose h Right)

-- Note: f' . g' = id is eta-expanded
-- f' . g' = id <=> (f' . g') h = h <=> (f' . g') h e = h e
{-@
f'_dot_g'_eq_id ::
  h:(Either b c -> a) -> e:(Either b c)
  -> {f' (g' h) e = h e}
@-}
f'_dot_g'_eq_id h e =
  f' (g' h) e
  ==. f' (compose h Left, compose h Right) e
  ==. case e of
        Left y ->
          compose h Left y
          ==. h (Left y)
        Right z ->
          compose h Right z
          ==. h (Right z)
  ==. h e
  *** QED

-- For some reason Liquid Haskell doesn't accept the following proof

-- Note: g' . f' = id is eta-expanded
-- g' . f' = id <=> (g' . f') h = h
{-@
g'_dot_f'_eq_id ::
  l:(b -> a)
  -> r:(c -> a)
  -> {g' (f' (l, r)) = (l, r)}
@-}
g'_dot_f'_eq_id l r =
  g' (f' (l, r))
  ==. (compose (f' (l, r)) Left, compose (f' (l, r)) Right)
  ==. (\y -> f' (l, r) (Left y), \z -> f' (l, r) (Right z))
  ==. (\y -> l y, \z -> r z)
  ==. (l, r)
  *** QED