Re: [Caml-list] strange type error with -principal

[Alexey Egorov <alex.only.d@gmail.com>]

Thanks for explanation!
Every problem I've had with GADTs was solved placing an annotation in
the right place...

2017-08-18 19:36 GMT+05:00 Gabriel Scherer <gabriel.scherer@gmail.com>:
> These errors on "ambiguous" types come from GADT type checking, which
> requires annotations in certain places (-principal is more picky about
> requiring more annotations; instead sometimes the type-checker makes
> guesses).
>
> Currently the syntactic forms
>   let <variable> : <type> = <expr> in <expr>
> and
>   let <pattern> : <type> = <expr> in <expr>
> are not desugared in the same way. The first is turned into
>   let <variable> = (<expr> : <type>) in <expr>
> and the second into
>   let (<pattern> : <type>) = <expr> in <expr>
>
> In the first case (let <variable>), the body of the definition gets the
> annotation. This is required, in your code, for this body to compile under
> -principal. In the second case (let <pattern>), the body does not get the
> annotation, so type-checking fails (under -principal).
>
> You can fix it yourself by adding the annotation on the right-hand-side
> directly
>
>   let (op, idx) = (begin match ... end : int op * int)
>
> in fact it suffices to write (op : int op), 2 in the second clause's
> right-hand-side.
>
> I don't know whether (let <pattern> : <type> = <expr> in <expr>) could
> instead be desugared into
> (let (<pattern> : <type) = (<expr> : <type>) in <expr>), which would also
> fix the issue. The specifics of how type information is propagated in the
> type-checker is a delicate design aspect of the type-checker which may still
> evolve in the future.
>
> If you wonder what the error message means, you should read the GADT section
> in the Reference Manual, and in particular the "type inference" subsection
> (but it depends on the text before it):
>   http://caml.inria.fr/pub/docs/manual-ocaml-4.05/extn.html#sec236
>
> The problem is that within the Op clause, we know the type equality (a =
> int), but this is not true outside the clause; so when a value that has both
> types (a op) and (int op) is returned by the clause, the type-checker cannot
> know which type to give to the outside (a op, or int op?), and it needs an
> explicit annotation to not make an arbitrary (non-principal) choice.
>
> On Fri, Aug 18, 2017 at 4:09 PM, Alexey Egorov <alex.only.d@gmail.com>
> wrote:
>>
>> Hello,
>>
>> I'm getting very confusing error when compiling with -principal:
>>
>> > Error: This expression has type int op
>> >       but an expression was expected of type 'a
>> >       This instance of int is ambiguous:
>> >       it would escape the scope of its equation
>>
>> What is the "instance of int"?
>>
>> Here is the code - https://pastebin.com/T74haahx
>> I'm mostly confused by the fact that changing pattern from (op, idx)
>> to simple value binding eliminates this error.
>>
>> Thanks!
>>
>> --
>> Caml-list mailing list.  Subscription management and archives:
>> https://sympa.inria.fr/sympa/arc/caml-list
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>