User defined variables wont recognize that its own type list IS the type

Question

For some reason, I'm getting errors claiming that distribute((AndC t),p) is a cnf instead of a cnf list... except a cnf list IS a type of cnf. Why doesn't OCaml recognize this will provide a list eventually?

The trouble spot is lines 11-12.

type cnf
  = AtomC of signed_atom
  | AndC of cnf list    
  | OrC of cnf * cnf

let rec distribute : cnf * cnf -> cnf = 

  let rec aux = function
    | AndC [], _
    | _, AndC [] -> AndC []
    | AndC (h::t), p -> AndC( distribute(h,p) :: distribute((AndC t),p) )
    | p, AndC (h::t) -> AndC( distribute(p,h) :: distribute(p,(AndC t)) )
    | p, q -> OrC(p, q)
  in aux

Answer 1

A value of the form AndC xxx is not a list. It's a value of type cnf, and it contains a list. But it's not a list itself.

A declaration like yours defines one new type cnf, and three new value constructors, AtomC, AndC, OrC. Value constructors (as in the name) are used to construct values. They aren't types.

Every value of type cnf will be constructed by one of the three constructors. So a list of cnf values is not a cnf value itself. The AndC is required.

Update

If you define this function:

let mycons cnf andc =
    match andc with
    | AndC cnfs -> cnf :: cnfs
    | _ -> [cnf] (* Not possible *)

You can replace :: with mycons like this:

AndC( mycons (distribute (h,p)) (distribute ((AndC t), p)) )

(I haven't tested this, but I think the idea is OK. The claim is that the second call to distribute is guaranteed to return an AndC value.)

Update 2

You can define distribute directly without aux like this:

let rec distribute : cnf * cnf -> cnf = function
| AndC [], _
| _, AndC [] -> AndC []
(* Rewrite these ...
| AndC (h::t), p -> AndC( distribute(h,p) :: distribute((AndC t),p) )
| p, AndC (h::t) -> AndC( distribute(p,h) :: distribute(p,(AndC t)) )
 ... *)
| p, q -> OrC(p, q)