Re: [Caml-list] GADTs : a type variable cannot be deduced

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

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

The problem is with the assumed injectivity of the abstract type 'a succ.
You should write:

  type 'a succ = Succ

then everything works out.

Injectivity was assumed to hold for types *defined* to be abstract, but
does not hold for types *declared* as abstract (That may have been defined
concretely as just "int" in their implementation). For consistency,
defined-abstract type are no more assumed to be injective, so you should
always use a constructor for that (using a constructor makes your type
nominal/generative/fresh, which enforces injectivity).

Remark: I'll let you work out while it would be problematic to consider a
('a succ succ nat)-matching branch as dead when matching over a ('a succ
nat) value, under the definition (type 'a succ = int).


On Fri, Oct 25, 2013 at 2:08 PM, David RENAULT <renault@labri.fr> wrote:

>
>                 Hi,
>
> I was experimenting on GADTs and phantom types and was using the usual
> encoding for naturals, as well as a classic implementation of the
> associated singleton type :
>
> type zero
> type 'a succ
> type _ nat =
>   | Zero : zero nat
>   | Succ : 'a nat -> ('a succ) nat
>
> With ocamlc 4.01.0, this fails to compile with the following error
> message :
>
> Error: In this definition, a type variable cannot be deduced
>        from the type parameters.
>
> This is strange, because this code compiled pretty well with ocamlc
> 4.00.1. Of course, it is possible to modify the code to make it compile
> by replacing the type variables by underscores, but the resulting type
> is incorrect :
>
> type _ nat =
>   | Zero : zero nat
>   | Succ : _ nat -> (_ succ) nat
> (* type _ nat = Zero : zero nat | Succ : 'b nat -> 'a succ nat *)
>
> Succ Zero;; (* 'a succ nat = Succ Zero, should be "zero succ nat" *)
>
> I failed to find in the Changelog the modification that led to this
> behavior, and nothing really simple about the error message showed up.
> The following file seems to prove that the problem appears in various
> other cases :
>
> http://caml.inria.fr/svn/ocaml/trunk/testsuite/tests/typing-gadts/pr5985.ml
>
> Is the code I am writing incorrect ? (for reference, the same code in
> Haskell (with ghc) works as expected)
>
>                 RENAULT David
>
> --
> 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: 3490 bytes --]