[Caml-list] Error: In this definition, a type variable cannot be deduced from the type parameters

[Caml-list] Error: In this definition, a type variable cannot be deduced from the type parameters

[Goswin von Brederlow]

Hi,

I'm stuck trying to solve this error:

    Error: In this definition, a type variable cannot be deduced
           from the type parameters.

The error happens when I use the "type 'a node = InnerNode.t" from the
comment and disapears when I box it in a constructor as shown below.

Can anyone explain what is missing that makes the extra constructor
necessary?

MfG
	Goswin

PS: needs and must work with ocaml 4.01.

----------------------------------------------------------------------

type inode = int
let size_inode = 8
type offset = int
let size_offset = 8
type hash = int
let size_hash = 8
type block = int
let size_block = 8
type cksum = string
let size_cksum = 8

module BTree = struct
  module type KEY_VALUE = sig
    type key
    val size_key : int
    type value
    val size_value : value -> int
  end

  module type NodeType = sig
    type key
    type value
    type t = {
      size : int;
      entries : (key * value) list
    }
    val create : unit -> t
    val insert : t -> key -> value -> t
    val iter : ((key * value) -> unit) -> t -> unit
  end

  module Node = functor (KV : KEY_VALUE) -> (struct
    type key = KV.key
    let size_key = KV.size_key
    type value = KV.value
    let size_value v = KV.size_value v
    type t = {
      size : int;
      entries : (key * value) list
    }
    let create () = {size = 0; entries = [];}
    let insert t k v =
      let kv = (k, v) in
      let rec loop = function
	| [] -> [kv]
	| ((x,_) as t)::ts when x < k -> t::(loop ts)
	| t -> kv::t
      in
      {size = t.size + size_key + size_value v; entries = loop t.entries;}
    let iter fn t = List.iter fn t.entries
  end : NodeType with type key = KV.key and type value = KV.value)

  module Tree = struct
    module Leaf = struct
      type key = string
      let size_key = 16
      type value = string
      let size_value (v : value) = 2 + String.length v
    end
    module LeafNode = Node(Leaf)
    module Inner = struct
      type key = Leaf.key
      let size_key = Leaf.size_key
      type value = block
      let size_value v = size_block
    end
    module InnerNode = Node(Inner)

    type leaf = LeafNode.t
    (* type 'a node = InnerNode.t					*)
    (* Why does this fail in _ tree below?				*)
    (* Error: In this definition, a type variable cannot be deduced	*)
    (*        from the type parameters.					*)
    type 'a node = Node of InnerNode.t

    type _ tree =
    | LeafNode : leaf tree
    | InnerNode : 'a tree -> 'a node tree

    type t = Tree : 'a tree * 'a -> t
  end
end

(*
type inode = int
val size_inode : int
type offset = int
val size_offset : int
type hash = int
val size_hash : int
type block = int
val size_block : int
type cksum = string
val size_cksum : int
module BTree :
  sig
    module type KEY_VALUE =
      sig
        type key
        val size_key : int
        type value
        val size_value : value -> int
      end
    module type NodeType =
      sig
        type key
        type value
        type t = { size : int; entries : (key * value) list; }
        val create : unit -> t
        val insert : t -> key -> value -> t
        val iter : (key * value -> unit) -> t -> unit
      end
    module Node :
      functor (KV : KEY_VALUE) ->
        sig
          type key = KV.key
          type value = KV.value
          type t = { size : int; entries : (key * value) list; }
          val create : unit -> t
          val insert : t -> key -> value -> t
          val iter : (key * value -> unit) -> t -> unit
        end
    module Tree :
      sig
        module Leaf :
          sig
            type key = string
            val size_key : int
            type value = string
            val size_value : value -> int
          end
        module LeafNode :
          sig
            type key = Leaf.key
            type value = Leaf.value
            type t =
              Node(Leaf).t = {
              size : int;
              entries : (key * value) list;
            }
            val create : unit -> t
            val insert : t -> key -> value -> t
            val iter : (key * value -> unit) -> t -> unit
          end
        module Inner :
          sig
            type key = Leaf.key
            val size_key : int
            type value = block
            val size_value : 'a -> int
          end
        module InnerNode :
          sig
            type key = Inner.key
            type value = Inner.value
            type t =
              Node(Inner).t = {
              size : int;
              entries : (key * value) list;
            }
            val create : unit -> t
            val insert : t -> key -> value -> t
            val iter : (key * value -> unit) -> t -> unit
          end
        type leaf = LeafNode.t
        type 'a node = Node of InnerNode.t
        type _ tree =
            LeafNode : leaf tree
          | InnerNode : 'a tree -> 'a node tree
        type t = Tree : 'a tree * 'a -> t
      end
  end
*)

Re: [Caml-list] Error: In this definition, a type variable cannot be deduced from the type parameters

[Jacques Garrigue]

On 2014/02/23 02:54, Goswin von Brederlow wrote:

> Hi,
> 
> I'm stuck trying to solve this error:
> 
>    Error: In this definition, a type variable cannot be deduced
>           from the type parameters.
> 
> The error happens when I use the "type 'a node = InnerNode.t" from the
> comment and disapears when I box it in a constructor as shown below.
> 
> Can anyone explain what is missing that makes the extra constructor
> necessary?
> 
> MfG
> 	Goswin
> 
> PS: needs and must work with ocaml 4.01.

Actually it seems that you have already found the solution:
if a type variable appears in the return type of a gadt, and is used
in the body, injectivity under invariance must be guaranteed for this return type.
This is the famous PR#5985.
Injectivity is broken if the type variable can disappear by expanding
any abbreviation in the type, such as node in your case.
By making node a nominal type, you prevented that.
Note that using a private abbreviation would not be sufficient here,
as a private abbreviation can be used to hide a normal abbreviation.

If you dislike the change in internal representation for node,
you can also define a separate type for the gadt parameter.
Except in very specific cases, there is no strong reason for the
gadt parameter type and the concrete type to coincide.

	Jacques

Re: [Caml-list] Error: In this definition, a type variable cannot be deduced from the type parameters.

[Jacques Garrigue]

2016/03/06 10:33, Goswin von Brederlow <goswin-v-b@web.de>:
> 
> Hi,
> 
> if I use the type aliases in the commented out lines then I get:
> 
>    Error: In this definition, a type variable cannot be deduced
>    from the type parameters.
> 
> To me the types sure do look alike and nothing is private or hidden my
> a signature. So what am I missing?
> 
> MfG
> 	Goswin

The problem is that you are using abstract types in separate modules.
As a result, the type system cannot recognize them as injective, and
gives the above error message.
You should either make it a datatype or a structural type:
  type +'a qObject' = Q of 'a
or
  type +'a qObject' = [`QObject' of 'a]

Jacques Garrigue

> -------------------------------------------------------------------------
> module Proxy = struct
>  type +'a t
> end
> 
> module QObject = struct
>  type +'a qObject'
>  type +'a t = 'a qObject' Proxy.t
> 
>  class ['a] qObject proxy = object
>    constraint 'a = 'b qObject' as 'a
>    method proxy : 'a Proxy.t = proxy
>  end
> end
> 
> module QWidget = struct
>  type +'a qWidget'
>  type +'a t = 'a qWidget' QObject.t
> 
>  external add : 'a qWidget' QObject.qObject' Proxy.t -> 'b qWidget' QObject.qObject' Proxy.t -> unit = "add"
>  (*
>    external add : 'a t -> 'b qWidget' QObject.t -> unit = "add"
>  *)
>  class ['a] qWidget proxy = object
>    constraint 'a = 'b qWidget' QObject.qObject' as 'a
>    inherit ['a] QObject.qObject proxy
>    method add : 'c 'd . ('d qWidget' QObject.qObject' #QObject.qObject as 'c) -> unit = fun w -> add proxy w#proxy
>  end
> end
> 
> module QButton = struct
>  type +'a qButton'
>  type +'a t = 'a qButton' QWidget.t
> 
>  external set : 'a qButton' QWidget.qWidget' QObject.qObject' Proxy.t -> 'b QWidget.qWidget' QObject.qObject' Proxy.t -> unit = "set"
>  (*
>    external set : 'a t -> 'b QWidget.t -> unit = "set"
>  *)
>  class ['a] qButton proxy = object
>    constraint 'a = 'b qButton' QWidget.qWidget' QObject.qObject' as 'a
>    inherit ['a] QWidget.qWidget proxy
>    method set : 'c 'd . ('c QWidget.qWidget' QObject.qObject' #QWidget.qWidget as 'd) -> unit = fun w -> set proxy w#proxy
>    method text = "button"
>  end
> end
> 
> let qObject_proxy : unit QObject.t = Obj.magic 0
> let qWidget_proxy : unit QWidget.t = Obj.magic 0
> let qButton_proxy : unit QButton.t = Obj.magic 0
> let qObject = new QObject.qObject qObject_proxy
> let qWidget = new QWidget.qWidget qWidget_proxy
> let qButton = new QButton.qButton qButton_proxy
> let () = qWidget#add qWidget
> let () = qWidget#add qButton
> let () = qButton#set qWidget
> let () = qButton#set qButton
> let () = qButton#add qWidget
> let () = qButton#add qButton
> 
> -- 
> 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

[Caml-list] Error: In this definition, a type variable cannot be deduced from the type parameters.

[Goswin von Brederlow]

Hi,

if I use the type aliases in the commented out lines then I get:

    Error: In this definition, a type variable cannot be deduced
    from the type parameters.

To me the types sure do look alike and nothing is private or hidden my
a signature. So what am I missing?

MfG
	Goswin
-------------------------------------------------------------------------
module Proxy = struct
  type +'a t
end

module QObject = struct
  type +'a qObject'
  type +'a t = 'a qObject' Proxy.t

  class ['a] qObject proxy = object
    constraint 'a = 'b qObject' as 'a
    method proxy : 'a Proxy.t = proxy
  end
end

module QWidget = struct
  type +'a qWidget'
  type +'a t = 'a qWidget' QObject.t

  external add : 'a qWidget' QObject.qObject' Proxy.t -> 'b qWidget' QObject.qObject' Proxy.t -> unit = "add"
  (*
    external add : 'a t -> 'b qWidget' QObject.t -> unit = "add"
  *)
  class ['a] qWidget proxy = object
    constraint 'a = 'b qWidget' QObject.qObject' as 'a
    inherit ['a] QObject.qObject proxy
    method add : 'c 'd . ('d qWidget' QObject.qObject' #QObject.qObject as 'c) -> unit = fun w -> add proxy w#proxy
  end
end

module QButton = struct
  type +'a qButton'
  type +'a t = 'a qButton' QWidget.t

  external set : 'a qButton' QWidget.qWidget' QObject.qObject' Proxy.t -> 'b QWidget.qWidget' QObject.qObject' Proxy.t -> unit = "set"
  (*
    external set : 'a t -> 'b QWidget.t -> unit = "set"
  *)
  class ['a] qButton proxy = object
    constraint 'a = 'b qButton' QWidget.qWidget' QObject.qObject' as 'a
    inherit ['a] QWidget.qWidget proxy
    method set : 'c 'd . ('c QWidget.qWidget' QObject.qObject' #QWidget.qWidget as 'd) -> unit = fun w -> set proxy w#proxy
    method text = "button"
  end
end

let qObject_proxy : unit QObject.t = Obj.magic 0
let qWidget_proxy : unit QWidget.t = Obj.magic 0
let qButton_proxy : unit QButton.t = Obj.magic 0
let qObject = new QObject.qObject qObject_proxy
let qWidget = new QWidget.qWidget qWidget_proxy
let qButton = new QButton.qButton qButton_proxy
let () = qWidget#add qWidget
let () = qWidget#add qButton
let () = qButton#set qWidget
let () = qButton#set qButton
let () = qButton#add qWidget
let () = qButton#add qButton