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

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

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