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

[Gabriel Scherer <gabriel.scherer@gmail.com>]

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