Type error in patricia trees
With the current commit 25b12781 patricia trees attached (see also [tests/poly/patricia.cd] in the distribution) [merge] function does not type. The error is
File "tests/poly/patricia.cd", line 69, characters 31-43:
This expression should have type:
Empty
but its inferred type is:
'a
which is not a subtype, as shown by the sample:
'a & Int
The line at issue is
| (<leaf key=k>x , t) -> insert c k x t
And the error message states that at the position of x was wating somethig of an empty type. Let us show why. First notice that
insert : ('a -> 'a -> 'a) -> Caml_int -> 'a -> Dict -> Leaf|Branch
since we have the following declaration
let insert (c: 'a -> 'a -> 'a) (k: Caml_int) (x: 'a) (t: Dict): Leaf|Branch
First of all let us replace the line 69 with the following one:
| (<leaf key=k>x , t) -> insert
we correctly obtain the following error:
File "tests/poly/patricia.cd", line 69, characters 31-37:
This expression should have type:
Branch | Leaf
but its inferred type is:
('_a_0 -> '_a_0 -> '_a_0) -> Caml_int -> '_a_0 -> [ ] | <brch bit=Caml_int
pre=Caml_int>X1 | <leaf key=Caml_int>'_a_0 -> X2 where
X1 = [ X2 X2 ] and
X2 = <brch bit=Caml_int pre=Caml_int>X1 | <leaf key=Caml_int>'_a_0
which is not a subtype, as shown by the sample:
('_a_0 -> '_a_0 -> '_a_0) -> Caml_int -> '_a_0 -> [ ] | <brch bit=Caml_int
pre=Caml_int>X1 | <leaf key=Caml_int>'_a_0 -> X2 where
X1 = [ X2 X2 ] and
X2 = <brch bit=Caml_int pre=Caml_int>X1 | <leaf key=Caml_int>'_a_0
Notice two things: the system expects as result of the matching something of type Leaf|Branch
(perfect!) and the type deduced for @insert@ is exactly the original type where 'a
has been renamed into a fresh variable. If now I use for this line the following definition
| (<leaf key=k>x , t) -> insert c
I expect that the fresh variable '_a_0
is unified with 'a
of the type of c
, and thus that this expression has type Caml_int -> 'a -> Dict -> Leaf|Branch
. Instead we obtain:
File "tests/poly/patricia.cd", line 69, characters 31-39:
This expression should have type:
Branch | Leaf
but its inferred type is:
Caml_int -> Arrow
which is not a subtype, as shown by the sample:
Caml_int -> Arrow
So what did happen? Well the fresh variable '_a_0
was WRONGLY substituted by Empty instead of by 'a
. And therefore the deduced type is
Caml_int -> Empty -> Dict -> Leaf|Branch
(i.e. Caml_int -> Arrow
). This explain why feeding two more arguments to it we obtain the error message that the function was expecting something of type Empty. Indeed with
| (<leaf key=k>x , t) -> insert c k x
we obtain
File "tests/poly/patricia.cd", line 69, characters 31-43:
This expression should have type:
Empty
but its inferred type is:
'a
which is not a subtype, as shown by the sample:
'a & Int