[Caml-list] strange type error with -principal

[Caml-list] strange type error with -principal

[Alexey Egorov]

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!

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

[Gabriel Scherer]

[-- Attachment #1: Type: text/plain, Size: 2802 bytes --]

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
>

[-- Attachment #2: Type: text/html, Size: 4149 bytes --]

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

[Alexey Egorov]

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
>
>

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

[Gabriel Scherer]

If you want to understand the details of GADT type inference, there is
a paper about it whose introduction remains at an informal level and
will get you a good picture:

  Ambivalent Types for Principal Type Inference with GADTs
  Jacques Garrigue and Didier Rémy, 2013
  http://gallium.inria.fr/~remy/gadts/Garrigue-Remy:gadts@aplas2013.pdf

The problem you had, however, is not about the mechanics describe in
this paper which are relatively clear and robust, but how they
interact with propagation of user annotations (which is a more ad-hoc
part of the type-checker). The GADT type inference described in this
paper clearly flags your pattern-matching code as requiring an
annotation in the clause, and the question/issue is whether it gets
pushed there or not by the independent annotation-propagation
mechanism.

On Fri, Aug 18, 2017 at 5:23 PM, Alexey Egorov <alex.only.d@gmail.com> wrote:
> 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
>>
>>