[Agda] exhaustive patterns

[Serge D. Mechveliani]

Dear all,

I have a question about the fragment
 
  inverse : (a : C) -> Inverse {M = Mg} e a
  inverse a  with  invMb a | inversionIsTotal a _
  ...      | just (yes inv) | _  = inv
  ...      | just (no _)    | ()
  ...      | nothing        | ()

It is type-checked in  Agda-2.3.2 MAlonzo,

while changing the last line to      ...  | _ | ()
leads to the report

" Checking AlgClasses1 (/home/mechvel/doconA/0.01/source/AlgClasses1.agda).
  Finished AlgClasses1.

Failed to solve the following constraints:
  [0] Is empty: justYes? .w \equiv┴║ Data.Bool.true
"

(without printing the line number).

This looks strange, because the pattern set
                            {just (yes inv), just (no _), nothing}

is exhaustive for the type of  Maybe $ Dec $ Inverse {M = Mg} e a
of  invMb a,
hence the last wildcard needs to be replaced with `nothing'.

Am I missing something?

Regards,

------
Sergei