Re: [Caml-list] Weird type error involving 'include' and applicative functors

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

On 2015/02/24 13:38, Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote:

>  While logically the T inside C and C.T are the same module,
> the typing rule in Leroy's paper do not say anything like that.
> 
> σ : {1,...,m} 􏰀→ {1,...,n} for all i ∈ {1,...,m}, E;D1;...;Dn ⊢ Dσ(i) <: Di′
> ---------------------------------------------------------------------------------------
>          E ⊢ sig D1;…;Dn end <: sig D1′ ;...;Dm′ end
> 
> The definition in the premise must match without extra equations.
> Here module aliases do not help.
> What could help would be to strengthen the definitions in the premise, so
> that T would be converted to C.T. But I don't know whether this is sound
> or not, since this is not part of the current theory.

More precisely, OCaml actually does a bit more than this rule, as it
strengthens abstract types. However there is no such thing as strengthening
for module aliases, as this would require having both a signature and an
alias for the same module. Allowing that could help solve this problem, but
this is not fixing a bug, rather extending the theory.

Jacques Garrigue