I try to write an heterogenous formatter for learning purpose, and i’m stuck on a type variable equality issue i think, here the code :
module IdList = struct type (_, _) t = |  : (_,Peano.zero) t | ( :: ) : 'a * (_, 'n) t -> (_, 'n Peano.succ) t end module FList = struct type _ t = |  : Peano.zero t | Literal : string * 'n t -> 'n t | Hole : ('a -> string) * 'n t -> 'n Peano.succ t let ( ^ ) str fmt = Literal (str, fmt) let string fmt = Hole ((fun x -> x),fmt) let int fmt = Hole (string_of_int,fmt) let bool fmt = Hole (string_of_bool, fmt) let ( ^^ ) f x = f x end let mprintf fmt args = let rec aux : type n a. n FList.t * (a, n) IdList.t -> _ = function | FList., IdList. -> "" | FList.Literal (x, xs), args -> x ^ aux (xs, args) | FList.Hole (to_string,xs), IdList.(x :: args) -> (to_string x) ^ aux (xs, args)
In particular :
| FList.Hole (to_string,xs), IdList.(x :: args) -> (to_string x) ^ aux (xs, args)
I got this error :
This expression has type $::_'a but an expression was expected of type $Hole_'a
What I think I’ve understood from this error is that the type variable introduced by the definition of the Hole constructor, is not equal to the one introduced by the definition of the ( :: ) constructor. This seems normal to me, but how do I tell the compiler that I want these two variables to be equal? Is this feasible?
At first glance, I naively thought that this would be an opportunity to use Refl, which I’ve just learned. But no, the two type variables are hidden inside the two existential types. If I had to take them out, I’d be stuck too, since I’m simulating heterogeneity.
Any help is welcome !