Parameters not substituted under `if` when displaying types

[fredrikNordvallForsberg]

Instantiated parameters under an if seem to be displayed as their uninstantiated variable name. (This seems to be a display problem only -- definitions making use of the parameters typecheck -- but it means basically programming blind in these situations.)

Steps to Reproduce

Load the following file in the repl and do :t f

0 Alias : Type -> Type
Alias a = (b : Bool) -> if b then a else a

foo : Alias ()
foo = ?f

Expected Behavior

To get output

Main.f : (b : Bool) -> (if b then () else ())

Observed Behavior

Actual output is

Main.f : (b : Bool) -> (if b then a else a)

Note the variable name a rather than its instantiation ().

[gallais]

Same issue without the if ... then ... else ... sugar:

0 Alias2 : Type -> Type
Alias2 a = (b : Bool) -> case b of
  True => a
  False => a

foo2 : Alias2 ()
foo2 = ?f2

The issue does not show up if the case is not actually matching anything (i.e. using case b of x => a instead).

[gallais]

Pretty sure unelabCase is the culprit here:

LOG unelab.case:20: Unelaborating case ("Alias", 356)
with arguments: [Builtin.Unit, b]
LOG unelab.case:20: Unelaborated to: (%case (b : ?) [Prelude.True = a, Prelude.False = a])