The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Hello,

I tried such code:

Inductive  Tag     : Type := Left | Right.
Inductive  Element : Tag -> Type :=
  | left  : Element Left
  | right : Element Right.
Inductive  Node    : Type :=
  | L : Element Left  -> Node
  | R : Element Right -> Node.
Definition HList   : Type := list Node.
Definition Matching (n : Node) :=
  match n with
  | L left  => True
  | R right => True
  end.

But Coq complains about definition of Matching: it says that pattern matching is non-exhaustive and there are can be branches L right and R left. But we never can construct such objects. Why Coq can't infer that?

Sincerely,
Kirill Taran