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

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

[David RENAULT]

		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

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

[Gabriel Scherer]

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

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

[David RENAULT]

Gabriel Scherer wrote:
> 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).

OK, thank you for your answer, I have taken some time to dive into the
question of injectivity of types, and I believe that there is something
I am missing. With your help, the following code compiles :

====================================================================
type 'a succ = Succ
type _ nat = NS : 'a nat -> ('a succ) nat
====================================================================

If we leave the type abstract, then the type function NS may not be
injective. But if we give a concrete implementation with a constructor,
it works out. To me, the concrete implementation is not injective (it
maps everything on "Succ nat"), but you proclaim that it becomes
automatically injective. Why does mapping everything onto a new type
enforce injectivity ?

		RENAULT David
		

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

[Gabriel Scherer]

The equality we're talking about the following: two types are equal if
they are exactly exchangeable from the type-checking point of view.

From this point of view, (int t) and (bool t) may be equal or
different depending on how (t) is defined.

Consider:
  type 'a u = int
in this case (int u) and (bool u) are equal (to int), but consider an
algebraic datatype (sum or record)
  type 'a t = Foo of bool
in this case (int t) and (bool t) are considered distinct by the type-checker,
even if 'a does not actually appear in the definition of the algebraic
datatype. To wit:

  # type 'a t = Foo of bool;;
  type 'a t = Foo of bool
  # let (x : int t) = Foo true;;
  val x : int t = Foo true
  # let (y : bool t) = Foo false;;
  val y : bool t = Foo false
  # [x; y];;
  Error: This expression has type bool t but an expression
         was expected of type int t
         Type bool is not compatible with type int

So "new" types like variants or records are always injective in all
their parameters, but type synonyms may not be.

(Note: the notion of "equality" we're talking about is distinct from,
and stricter than, the symmetric closure of OCaml's subtyping
relation: here we have (int t ≤ bool t) and conversely)

Now if you have

module Foo : sig
  type 'a t
end = struct
 ...
end

You cannot know (without looking at the implementation) if the
abstract declaration of ('a t) here is more like the (type 'a u = int)
example, or the (type 'a t = Foo of bool) example. So OCaml must
conservatively assume that ('a t) may fail to be injective.

Then consider the definition

  type _ nat = Succ : 'a nat -> ('a succ nat)

OCaml will accept this definition if it can prove that, for any type
foo, if (Succ blah : foo succ nat) holds for any OCaml type (foo),
then (blah : foo) also holds. (Because this implication will then be
used to type-check code that pattern-matches on this type.) This
implication is only true if ('a succ) is injective. Hence, the
definition is rejected when ('a succ) is defined as ('a u) above, or
abstract.

On Tue, Oct 29, 2013 at 3:17 PM, David RENAULT <renault@labri.fr> wrote:
> Gabriel Scherer wrote:
>> 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).
>
> OK, thank you for your answer, I have taken some time to dive into the
> question of injectivity of types, and I believe that there is something
> I am missing. With your help, the following code compiles :
>
> ====================================================================
> type 'a succ = Succ
> type _ nat = NS : 'a nat -> ('a succ) nat
> ====================================================================
>
> If we leave the type abstract, then the type function NS may not be
> injective. But if we give a concrete implementation with a constructor,
> it works out. To me, the concrete implementation is not injective (it
> maps everything on "Succ nat"), but you proclaim that it becomes
> automatically injective. Why does mapping everything onto a new type
> enforce injectivity ?
>
>                 RENAULT David
>