Match a list of gadt based on type

Learning
1

Hi all,

I have some trouble with gadt, I would like to do something along the line of :

 type t1 = T1
type t2 = T2

type _ var = A: t1 var | B : t1 var | C : t2 var

let contains_a: 'a. 'a var list -> bool = function
  | l when List.mem A l -> true
  | _ -> false

The function contains_a does not compile with error
This definition has type t1 var list -> bool
which is less general than 'a. 'a var list -> bool which I kind of expected. There is an easy fix that I applied :

let is_a  ( type a) (v: a var) = match v with
  A -> true
  | _ -> false

let contains_a: 'a. 'a var list -> bool =
  fun l -> List.exists is_a l

But in general I would like to know if the kind of code I originally wanted to write is feasible - discriminate whether I am matching on a t1 var list or a t2 var list and adapt the function behaviour accordlingly.
Thanks

2

Discriminating between types is performed by discriminating between constructors in the match:

let contains_a: type a. a var list -> bool = function
  | (A :: _) as l when List.mem A l -> true
  | _ -> false

Of course, written like this, the when clause is redundant, but it would make sense if A carries some value. The point is that pattern-matching against (A :: _) provides the type equality a = t1.

3

Ok, that was what I suspected - that the compiler could only infer the types from the constructor. So I guess the only way to do what I want would be something like :

let contains_a: type a. a var list -> bool = function
  | (A::_) as l when List.mem A l -> true
  | (B::_) as l when List.mem A l -> true
  | _ -> false

A bit verbose maybe, too bad. Thank you for your answer