• One solution is to utilize an additional type parameter (as described in Section 3.7 of Blume01):

signature C = sig
    type ('t, 'f, 'c) obj
    eqtype ('t, 'f, 'c) obj'
    ...
    type ('o, 'f) ptr   
    eqtype ('o, 'f) ptr'
    ...
    type 'f fptr
    type 'f ptr'
    ...
    structure T : sig
        type ('t, 'f) typ
        ...
    end
end

The rule for ('t, 'f, 'c) obj,('t, 'f, 'c) ptr, and also ('t, 'f) T.typ is that whenever F fptr occurs within the instantiation of 't, then 'f must be instantiated to F. In all other cases, 'f will be instantiated to unit. (In the actual MLton implementation, an abstract type naf (not-a-function) is used instead of unit.)

While this means that type-annotated programs may not type-check under both the SML/NJ implementation and the MLton implementation, this should not be a problem in practice. Tools, like ml-nlffigen, which are necessarily implementation dependent (in order to make calls through a C function pointer), may be easily extended to emit the additional type parameter. Client code which uses such generated glue-code (e.g., Section 1 of Blume01) need rarely write type-annotations, thanks to the magic of type inference.

• The above implementation suffers from two disadvantages. First, it changes the MLNLFFI Library interface, meaning that the same program may not type-check under both the SML/NJ implementation and the MLton implementation (though, in light of type inference and the richer MLRep structure provided by MLton, this point is mostly moot).

  Second, it appears to unecessarily duplicate type information. For example, an external C variable of type int (* f[3])(int) (that is, an array of three function pointers), would be represented by the SML type (((sint -> sint) fptr, dec dg3) arr, sint -> sint, rw) obj. One might well ask why the 'f instantiation (sint -> sint in this case) cannot be extracted from the 't instantiation (((sint -> sint) fptr, dec dg3) arr in this case), obviating the need for a separate function-type type argument. There are a number of components to an complete answer to this question. Foremost is the fact that Standard ML supports neither (general) type-level functions nor intensional polymorphism.

  A more direct answer for MLNLFFI is that in the SML/NJ implemention, the definition of the types ('t, 'c) obj and ('t, 'c) ptr are made in such a way that the type variables 't and 'c are phantom (not contributing to the run-time representation of an ('t, 'c) obj or ('t, 'c) ptr value), despite the fact that the types ((sint -> sint) fptr, rw) ptr and ((double -> double) fptr, rw) ptr necessarily carry distinct (and type incompatible) run-time (C-)type information (RTTI), corresponding to the different calling conventions of the two C functions. The Unsafe.cast "cheat" overcomes the type incompatibility without introducing a new type variable (as in the first solution above).

  Hence, the reason that function-type type cannot be extracted from the 't type variable instantiation is that the type of the representation of RTTI doesn't even see the (phantom) 't type variable. The solution which presents itself is to give up on the phantomness of the 't type variable, making it available to the representation of RTTI.

  This is not without some small drawbacks. Because many of the types used to instatiate 't carry more structure than is strictly necessary for 't's RTTI, it is sometimes necessary to wrap and unwrap RTTI to accomodate the additional structure. (In the other implementations, the corresponding operations can pass along the RTTI unchanged.) However, these coercions contribute miniscule overhead; in fact, in a majority of cases, MLton's optimizations will completely eliminate the RTTI from the final program.

Bonus question: Why can't one use a universal type to eliminate the use of Unsafe.cast?

• Answer: ???

structure MLRep = struct
    structure Char =
       struct
          structure Signed = Int8
          structure Unsigned = Word8
          (* word-style bit-operations on integers... *)
          structure SignedBitops = IntBitOps(structure I = Signed
                                             structure W = Unsigned)
       end
    structure Short =
       struct
          structure Signed = Int16
          structure Unsigned = Word16
          (* word-style bit-operations on integers... *)
          structure SignedBitops = IntBitOps(structure I = Signed
                                             structure W = Unsigned)
       end
    structure Int =
       struct
          structure Signed = Int32
          structure Unsigned = Word32
          (* word-style bit-operations on integers... *)
          structure SignedBitops = IntBitOps(structure I = Signed
                                             structure W = Unsigned)
       end  
    structure Long =
       struct
          structure Signed = Int32
          structure Unsigned = Word32
          (* word-style bit-operations on integers... *)
          structure SignedBitops = IntBitOps(structure I = Signed
                                             structure W = Unsigned)
       end
    structure LongLong =
       struct
          structure Signed = Int64
          structure Unsigned = Word64
          (* word-style bit-operations on integers... *)
          structure SignedBitops = IntBitOps(structure I = Signed
                                             structure W = Unsigned)
       end
    structure Float = Real32
    structure Double = Real64
end