More fun with variants and constraints

More fun with variants and constraints

[Jacques Carette]

[One of my previous difficulties was alleviated by putting variance 
annotations on my variables, which was not at all obvious from the 
documentation, other than a vague hint that these are not automatically 
inferred; I put annotation everywhere in the code below, but +'d is the 
only one that matters].

In my actual code, I now have some routines that take a huge amount of 
time to compile (I gave up after 30 minutes).  Looking into why that 
might be, I have produced the following code which shows the issue:

type +'a a0 = [`A of 'a ]
type +'a a1 = [`B of 'a ]
type +'a a2 = [`C of 'a ]
type    d = [`D of int ]

type +'a f1 = ['a a0 | d]
type +'a f2 = ['a a1 | d]

type (+'a,+'b,+'c) e = ['b a0 | 'a a1 | 'c a2 | d]

type (+'a,+'b,+'c) c = ('a,'b,'c) e
    constraint 'a = [< 'b f1]
    constraint 'b = [< 'a f2]
    constraint 'c = [< 'c a2 ]

type +'d cc = 'd
    constraint 'd = [< ('a,'b,'c) c]

(* This craps out with 'cc' being an inexact variant
let is_cc = function
    | #cc -> true
    | _   -> false 
    *)

let id_cc (x: 'd cc) = x

let build (i:int) : 'd cc = `A (`B (`D i))

let a1 = build 1
;;

The type of a1 is reported as
val a1 :
  [< `A of [< ([< 'a f1 > `D ] as 'b) f2 > `B ] as 'a
   | `B of 'b
   | `C of
       [< 'c a2 ] as 'c &
       [< 'd a2 ] as 'd &
       [< 'e a2 ] as 'e &
       [< 'f a2 ] as 'f
   | `D of int
   > `A ]

What is puzzling is the type in `C.  Why are there 4 (identical!) 
possibilities?  I played around some, and the 4 is equal to the number 
of constraints in the program.

The issue is, in my 'real' code, there are 33 constraints.  Simple 
values now have types that take pages and pages of output.

How do I still get all the polymorphism that I want without getting this 
kind of blow-up?

Jacques Carette