Error `unknown free variable: _kernel_fresh` in match block

Stream: lean4

[Anand Rao Tadipatri]

I'm running into a low-level kernel error with a match block on a custom inductive type:

import Lean

inductive BizarreInductive : Bool → Type where
  | pos {pol : Bool} : BizarreInductive pol → BizarreInductive pol
  | pos' {pol : Bool} : BizarreInductive pol → BizarreInductive pol
  | neg {pol : Bool} : BizarreInductive !pol → BizarreInductive pol
  | neg' {pol : Bool} : BizarreInductive !pol → BizarreInductive pol
  | base : BizarreInductive true

structure BizarreInductivePair where
  srcPol : Bool
  srcObj : BizarreInductive srcPol
  tgtPol : Bool
  tgtObj : BizarreInductive tgtPol

def test (pair : BizarreInductivePair) : Bool :=
  match pair with
  | ⟨true, .neg (.pos _), true, .pos _⟩ => true
  | _ => false

Minimizing this example any further, by removing some constructors or erasing one of the objects in the pair, seems to make this behaviour disappear. Does anyone know what could be going on here? Help would be much appreciated!

[Bhavik Mehta]

This is a tiny point but you can remove neg' and it still gives that error. And then I notice that _adding_ another branch in test also makes the error go away:

import Lean

inductive BizarreInductive : Bool → Type where
  | pos {pol : Bool} : BizarreInductive pol → BizarreInductive pol
  | pos' {pol : Bool} : BizarreInductive pol → BizarreInductive pol
  | neg {pol : Bool} : BizarreInductive !pol → BizarreInductive pol
  | base : BizarreInductive true

structure BizarreInductivePair where
  srcPol : Bool
  srcObj : BizarreInductive srcPol
  tgtPol : Bool
  tgtObj : BizarreInductive tgtPol

def test (pair : BizarreInductivePair) : Bool :=
  match pair with
  | ⟨true, .neg (.pos h), true, .pos _⟩ => true
  | ⟨true, _, _, _⟩ => true
  | _ => false

so my best guess is that this is something with the completeness checker