Possible totality check bug in Idris 0.9.19 (6fc713d)

reduction.idr

%default total

data KnownSet : Type where
  Control : KnownSet
  Data : KnownSet

dataNotControl : Not (Data = Control)
dataNotControl Refl impossible

data RState : Type where
  Top : RState
  Member : KnownSet -> RState

data RecR : (left, right : RState) -> (answer : RState) -> Type where  
  LeftConstrained : RecR (Member x) Top (Member x)
  RightConstrained : RecR Top (Member x) (Member x)
  -- The case below is manufactured to show the totality failure more clearly.
  Broken : RecR (Member x) (Member y) z

reconcileUnequalSets : {k, j : KnownSet} ->
                       Not (k = j) ->
                       Not (ans ** RecR (Member k) (Member j) ans)
reconcileUnequalSets knotj (_ ** LeftConstrained) impossible
  -- Because `Broken` is a valid case, this ought to be partial.

test : Void
test = reconcileUnequalSets dataNotControl (Top ** Broken)