Substitution variable splitting doesn't cooperate with dependencies

[tsani]

Load this signature

LF a : type = ;

schema ctx = a;

LF nat : type =
  | zero : nat
  | succ : nat → nat
;

rec len : {g : ctx} {$S : [⊢ g]} [⊢ nat] =
/ total g (len g _) /
mlam g, $S ⇒ case [g] of
  | [] ⇒ [⊢ zero]
  | [g, x : a] ⇒ case [⊢ $S] of
    | [⊢ $S, M] ⇒ ?
;

It produces the following error

## Type Reconstruction: t/code/success/svar-len.bel ##
t/code/success/svar-len.bel, line 14, column 17:

######   COVERAGE FAILURE: Case expression doesn't cover: ######
##       CASE(S) NOT COVERED:
(1)
Z : [g |- a], X : [ |-  g], $S : [ |-  g, x : a], g* : ctx ;  |-
  [g, x1 |-  X[.., x1], Z]

##

The missing case g, x1 |- X[.., x1], Z appears wrong: the substitution sends g to a closed context, so why should the patterns for $S have a nonempty LF context?

[Ailrun]

I'm not sure whether it's normal or not, so I wrote this for recording purpose.

By repeating the last pattern, Beluga repeats the same non-covered cases.

LF a : type = ;

schema ctx = a;

LF nat : type =
  | zero : nat
  | succ : nat → nat
;

rec len : {g : ctx} {$S : [⊢ g]} [⊢ nat] =
/ total g (len g _) /
mlam g, $S ⇒ case [g] of
  | [] ⇒ [⊢ zero]
  | [g, x : a] ⇒ case [⊢ $S] of
    | [⊢ $S, M] ⇒ ?
    | [⊢ $S, M] ⇒ ?
    | [⊢ $S, M] ⇒ ?
;

## Type Reconstruction: t/code/success/svar-len.bel ##
t/code/success/svar-len.bel, line 14, column 17:

######   COVERAGE FAILURE: Case expression doesn't cover: ######
##       CASE(S) NOT COVERED:
(1)
Z : [g |- a], X : [ |-  g], $S : [ |-  g, x : a], g* : ctx ;  |-
  [g, x1 |-  X[.., x1], Z]
(2)
Z : [g |- a], X : [ |-  g], $S : [ |-  g, x : a], g* : ctx ;  |-
  [g, x1 |-  X[.., x1], Z]
(3)
Z : [g |- a], X : [ |-  g], $S : [ |-  g, x : a], g* : ctx ;  |-
  [g, x1 |-  X[.., x1], Z]

##

[tsani]

That definitely seems wrong, and it's probably related. My guess is that coverage checking for substitution variables is plain broken at the moment.