Re: [Caml-list] Late adding of type variable constraints

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2015/09/04 13:28, Markus Mottl <markus.mottl@gmail.com> wrote:
> 
> Hi,
> 
> I wonder whether there is a way to add constraints to type variables
> in signatures after the signature was defined.  E.g.:
> 
> ---
> module type S = sig
>  type 'a t
>  type ('a, 'b) mappers
> 
>  val map : ('a, 'b) mappers -> 'a t -> 'b t
> end
> 
> module type T = sig
>  type 'a t constraint 'a = unit  (* whatever *)
>  include S with type 'a t := 'a t
> end
> ---
> 
> The above will fail, because 'a has additional constraints for type
> "t" in signature "T".  If I write instead e.g. "type 'a t = 'a list",
> this will work and also constrain the signature to something narrower.
> What makes constraints on polymorphic variables special here?

Consider this signature:

module type S = sig
  type 'a t
  type 'a u = U of 'a t constraint 'a = < m: int; .. >
end

Now the signature
   S with type 'a constraint 'a t = unit
is ill-typed, but to see it you must type-check again all of its contents
(not just the definition of t).

This is the reason you cannot do that.

Jacques Garrigue