problem with unification

Question

I've faced a problem. I'm not sure how to explain it, so, that is why I'm asking.

Definition sumT (A B : Type) := {x : bool & if x then A else B}.

Definition ind_sum1 {A B}
  : forall (C : sumT A B -> Type),
    (forall (x : bool) (a : if x then A else B), x = true -> C (existT _ x a)) ->
    (forall (x : bool) (b : if x then A else B), x = false -> C (existT _ x b)) ->
    forall x : sumT A B, C x :=
  fun C fa fb s =>
    match s with
    | existT _ x v as s' =>
      (match x as x' return x = x' -> C s' with
       | true => fun ex => fa x v ex
       | false => fun ex => fb x v ex
       end eq_refl)
    end.

Definition ind_sum {A B}
  : forall (C : sumT A B -> Type),
    (forall a:A, C (existT _ true a)) ->
    (forall b:B, C (existT _ false b)) ->
    forall x : sumT A B, C x :=
  fun C fa fb s =>
    (@ind_sum1 A B C
       (fun x a eqx => fa (let 'eq_refl := eqx in a))
       (fun x b eqx => (let 'eq_refl := eqx in fb b))
       s).

The answer is

In environment
A : Type
B : Type
C : sumT A B -> Type
fa : forall a : A, C (existT (fun x : bool => if x then A else B) true a)
fb : forall b : B, C (existT (fun x : bool => if x then A else B) false b)
s : sumT A B
x : bool
a : if x then A else B
eqx : x = true
The term "a" has type "if x then A else B" while it is expected to have type 
"if x then A else ?T" (cannot instantiate "?T" because "B" is not in its scope).

And this is what I do not understand: what is wrong with B? It looks to me like B is actually in the scope. I think this might be one of those cryptic error messages. But how to fix code then?

Answer can be either a good explanation of error or fix the code of ind_sum using ind_sum1 or code of ind_sum without using ind_sum1 (but in programming mode, no tactics).

UPDATE.

Resulting code of ind_sum is

Lemma x_true_x_false_False {x} : x = true -> x = false -> False.
Proof.
  intros Ht Hf.
  rewrite Ht in Hf.
  discriminate Hf.
Qed.

Definition ind_sum {A B}
  : forall (C : sumT A B -> Type),
    (forall a:A, C (existT _ true a)) ->
    (forall b:B, C (existT _ false b)) ->
    forall x : sumT A B, C x :=
  fun C fa fb s =>
    (@ind_sum1 A B C
       (fun x eqx a =>
          (if x as x' return x = x' -> forall (a : if x' then A else B), (C (existT _ x' a))
           then fun eqx' a' => fa a'
           else fun eqx' _ => False_rect _ (x_true_x_false_False eqx eqx'))
            eq_refl a)
       (fun x eqx b =>
          (if x as x' return x = x' -> forall (b : if x' then A else B), (C (existT _ x' b))
           then fun eqx' _ => False_rect _ (x_true_x_false_False eqx' eqx)
           else fun eqx' b' => fb b')
            eq_refl b)
       s).

Thanks again to Andrej Bauer for the advice!

Answer 1

I am not quite sure how to fix your code with bare hands, it's going to take a Frenchman to do that, but I can tell you how I would solve this problem: by switching to tactic mode, getting it done, and then inspecting the result. So here we go:

Definition sumT (A B : Type) := {x : bool & if x then A else B}.

Definition ind_sum1 {A B}
  : forall (C : sumT A B -> Type),
    (forall (x : bool) (a : if x then A else B), x = true -> C (existT _ x a)) ->
    (forall (x : bool) (b : if x then A else B), x = false -> C (existT _ x b)) ->
    forall x : sumT A B, C x :=
  fun C fa fb s =>
    match s with
    | existT _ x v as s' =>
      (match x as x' return x = x' -> C s' with
       | true => fun ex => fa x v ex
       | false => fun ex => fb x v ex
       end eq_refl)
    end.

Definition ind_sum {A B}
  : forall (C : sumT A B -> Type),
    (forall a:A, C (existT _ true a)) ->
    (forall b:B, C (existT _ false b)) ->
    forall x : sumT A B, C x.

Up to here the code is the same. Now we proceed interactively:

Proof.
  intros C fa fb s.
  destruct s as [[|] ?]. (* cross fingers *)
  - apply fa.
  - apply fb.
Defined.

Let us see what Coq came up with. The command Print ind_sum. gives:

ind_sum =
fun (A B : Type) (C : sumT A B -> Type) (fa : forall a : A, C (existT (fun x : bool => if x then A else B) true a))
  (fb : forall b : B, C (existT (fun x : bool => if x then A else B) false b)) (s : sumT A B) =>
let (x, y) as s0 return (C s0) := s in
(fun x0 : bool =>
 if x0 as b return (forall y0 : if b then A else B, C (existT (fun x1 : bool => if x1 then A else B) b y0))
 then fun y0 : A => fa y0
 else fun y0 : B => fb y0) x y
     : forall (A B : Type) (C : sumT A B -> Type),
       (forall a : A, C (existT (fun x : bool => if x then A else B) true a)) ->
       (forall b : B, C (existT (fun x : bool => if x then A else B) false b)) -> forall x : sumT A B, C x

Arguments ind_sum {A B}%type_scope (C _ _)%function_scope x

You can now massage the definition given by Coq.

By the way, you might be suffering from boolean blindness. The idiomatic solution is

Inductive sumT (A B : Type) :=
  | inl : A -> sumT A B
  | inr : B -> sumT A B.

Arguments inl {_} {_} _.
Arguments inr {_} {_} _.

Definition ind_sum {A B}
  : forall (C : sumT A B -> Type),
    (forall a : A, C (inl a)) ->
    (forall b : B, C (inr b)) ->
    forall x : sumT A B, C x :=
  fun C fa fb x =>
  match x with
  | inl a => fa a
  | inr b => fb b
  end.

(And Coq already generates ind_sum for you, it's called sumT_rec (and it's more general than ind_sum.)