case_is_const.idr

-- succeeds
foo : if False then Nat else Bool
foo = Z

-- fails
-- bar : if False then Nat else Bool
-- bar = False

-- succeeds
baz : case S (S Z) of { Z => Nat; S Z => Bool; _ => Nat -> Bool }
baz = Z

-- fails
-- qux : case S (S Z) of { Z => Nat; S Z => Bool; _ => Nat -> Bool }
-- qux = \case
--   _ => True

-- fails
-- qux : case S Z of { Z => Nat; S Z => Bool; _ => Nat -> Bool }
-- qux = True