Cases and if statements in type signatures incorrectly take first branch

[benwr]

I'm running Idris2 0.2.0, and experiencing a problem where branches in type signatures sometimes seem to incorrectly reduce to the first branch:

Steps to Reproduce

-- 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

(gist here)

Expected Behavior

I'd naively expect that branches in type signatures would act like branches elsewhere (reducing differently, based on their condition or match).

Observed Behavior

Case statements in type signatures seem to (often, though not always) reduce to their first branch. I also get "warning: unreachable branch" about the other branches, which makes sense if those branches can't be taken.

Weirdly, the following seems to correctly choose "Bool":

foo : case Z of { S a => Vect a Bool; _ => Bool }

[ziman]

If I change

foo : if False then Nat else Bool
foo = Z

to

FooTy : Type
FooTy = if False then Nat else Bool

foo : FooTy
foo = Z

the definition of foo no longer typechecks.

The same for baz.

[ziman]

I wonder if it's somehow related to #70.

[edwinb]

Coincidentally, I've just been fixing this one since it came up somewhere else... it's because they're at multiplicity zero and the case compiler thinks they're ignorable, which they're not.

[edwinb]

(It's not related to #70, by the way, just to answer that bit explicitly... that seems to be a different problem.)