[checkSub] encountered MSVar (checking non-whnf substitution)

[ryanakca]

## Type Reconstruction begin: /tmp/mwe.bel ##
Internal error. Please report this as a bug.
[checkSub] encountered MSVar (checking non-whnf substitution)

Compilation exited abnormally with code 1 at Thu Aug  8 17:39:37

mwe.bel has the contents:

tm : type.
tp : type.
oft : tm → tp → type.
msf : ({x:tm} {tx:oft x A} oft (M x tx) B) → type.

msf/var : msf (\x.\tx.tx).

schema ctx = some [A:tp] block (x:tm, tx:oft x A);

inductive msfOft : (g : ctx) {D : [g ⊢ oft M A[]]} {l : ctx} {$W:$[g ⊢ l]}ctype =
  | msfOftNil  : msfOft [g ⊢ D] [] $[g ⊢ ]
  | msfOftCons : msfOft [g, blx:block(x:tm, tx:oft x A[]) ⊢ D] [l] $[g, blx:block(x:tm, tx:oft x A[]) ⊢ $W]
                 → [g ⊢ msf (\x.\tx.D[..,<x;tx>]) ]
                 → msfOft [g, blx:block(x:tm, tx:oft x A[]) ⊢ D]
	                  [l, blx:block(x:tm, tx:oft x A[])]
                          $[g, blx:block(x:tm, tx:oft x A[]) ⊢ $W, blx];

let test1 : msfOft [blx:block(x:tm, tx:oft x A[]) ⊢ blx.tx] [] $[blx:block(x:tm, tx:oft x A[]) ⊢ $W] = msfOftNil;
let test2 = msfOftCons test1 [ ⊢ msf/var ];