Type error in patricia trees (#8) · Issues · cduce / cduce

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

With the current commit 25b127810a48fae75a795ca3bfc9fe7f388a6c11 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
```