Typechecker fails to unify

[omegablitz]

I finally got around to implementing an immutable vector type (#472). While implementing it, I ran into a case where the typechecker fails to unify, when it should.

Condensed example:

type Digit a =
    | One a
    | Two a a
    | Three a a a
    | Four a a a a

type Node a =
    | Node2 a a
    | Node3 a a a

type FingerTree a =
    | Empty
    | Single a
    | Deep (Digit a) (FingerTree (Node a)) (Digit a)

type View a =
    | Nil
    | View a (FingerTree a)

rec
let viewl xs : FingerTree a -> View a =
    match xs with
    | Empty -> Nil
    | Single x -> View x Empty
    | Deep (One a) deeper suffix ->
        match viewl deeper with
        | View (Node2 b c) rest -> View a (Deep (Two b c) rest suffix)
        | View (Node3 b c d) rest -> View a (Deep (Three b c d) rest suffix)
        | Nil ->
            match suffix with
            | One w -> View a (Single w)
            | Two w x -> View a (Deep (One w) Empty (One x))
            | Three w x y -> View a (Deep (Two w x) Empty (One y))
            | Four w x y z -> View a (Deep (Three w x y) Empty (One z))
    | Deep (Two a b) deeper suffix -> View a (Deep (One b) deeper suffix)
    | Deep (Three a b c) deeper suffix -> View a (Deep (Two b c) deeper suffix)
    | Deep (Four a b c d) deeper suffix -> View a (Deep (Three b c d) deeper suffix)
in

viewl

The specific lines the typechecker doesn't seem to like are lines 28 - 34, but am not sure for what reason. Full error:

error: Expected the following types to be equal
Expected: .tmp.test.FingerTree a
Found: .tmp.test.FingerTree a
1 errors were found during unification:
Types do not match:
    Expected: a
    Found: a
- <.tmp.test>:28:46
   |
28 |         | View (Node3 b c d) rest -> View a (Deep (Three b c d) rest suffix)
   |                                              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |

error: Expected the following types to be equal
Expected: .tmp.test.FingerTree a
Found: .tmp.test.FingerTree a
1 errors were found during unification:
Types do not match:
    Expected: a
    Found: a
- <.tmp.test>:31:32
   |
31 |             | One w -> View a (Single w)
   |                                ^^^^^^^^
   |

error: Expected the following types to be equal
Expected: .tmp.test.FingerTree a
Found: .tmp.test.FingerTree a
1 errors were found during unification:
Types do not match:
    Expected: a
    Found: a
- <.tmp.test>:32:34
   |
32 |             | Two w x -> View a (Deep (One w) Empty (One x))
   |                                  ^^^^^^^^^^^^^^^^^^^^^^^^^^
   |

error: Expected the following types to be equal
Expected: .tmp.test.FingerTree a
Found: .tmp.test.FingerTree a
1 errors were found during unification:
Types do not match:
    Expected: a
    Found: a
- <.tmp.test>:33:38
   |
33 |             | Three w x y -> View a (Deep (Two w x) Empty (One y))
   |                                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |

error: Expected the following types to be equal
Expected: .tmp.test.FingerTree a
Found: .tmp.test.FingerTree a
1 errors were found during unification:
Types do not match:
    Expected: a
    Found: a
- <.tmp.test>:34:39
   |
34 |             | Four w x y z -> View a (Deep (Three w x y) Empty (One z))
   |                                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |

[Shuenhoy]

This may be helpful to figure out the reason. Use different variables in each place:

type Digit a =
    | One a
    | Two a a
    | Three a a a
    | Four a a a a

type Node b =
    | Node2 b b
    | Node3 b b b

type FingerTree c =
    | Empty
    | Single c
    | Deep (Digit c) (FingerTree (Node c)) (Digit c)

type View d =
    | Nil
    | View d (FingerTree d)

rec
let viewl xs : FingerTree e -> View e =
    match xs with
    | Empty -> Nil
    | Single x -> View x Empty
    | Deep (One a) deeper suffix ->
        match viewl deeper with
        | View (Node2 b c) rest -> View a (Deep (Two b c) rest suffix)
        | View (Node3 b c d) rest -> View a (Deep (Three b c d) rest suffix)
        | Nil ->
            match suffix with
            | One w -> View a (Single w)
            | Two w x -> View a (Deep (One w) Empty (One x))
            | Three w x y -> View a (Deep (Two w x) Empty (One y))
            | Four w x y z -> View a (Deep (Three w x y) Empty (One z))
    | Deep (Two a b) deeper suffix -> View a (Deep (One b) deeper suffix)
    | Deep (Three a b c) deeper suffix -> View a (Deep (Two b c) deeper suffix)
    | Deep (Four a b c d) deeper suffix -> View a (Deep (Three b c d) deeper suffix)
in

viewl

The error would become:

error: Expected the following types to be equal
Expected: test.FingerTree e
Found: test.FingerTree c
1 errors were found during unification:
Types do not match:
    Expected: e
    Found: c
   ┌─ test:28:46
   │
28 │         | View (Node3 b c d) rest -> View a (Deep (Three b c d) rest suffix)
   │                                              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^


error: Expected the following types to be equal
Expected: test.FingerTree e
Found: test.FingerTree c
1 errors were found during unification:
Types do not match:
    Expected: e
    Found: c
   ┌─ test:31:32
   │
31 │             | One w -> View a (Single w)
   │                                ^^^^^^^^


error: Expected the following types to be equal
Expected: test.FingerTree e
Found: test.FingerTree c
1 errors were found during unification:
Types do not match:
    Expected: e
    Found: c
   ┌─ test:32:34
   │
32 │             | Two w x -> View a (Deep (One w) Empty (One x))
   │                                  ^^^^^^^^^^^^^^^^^^^^^^^^^^


error: Expected the following types to be equal
Expected: test.FingerTree e
Found: test.FingerTree c
1 errors were found during unification:
Types do not match:
    Expected: e
    Found: c
   ┌─ test:33:38
   │
33 │             | Three w x y -> View a (Deep (Two w x) Empty (One y))
   │                                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^


error: Expected the following types to be equal
Expected: test.FingerTree e
Found: test.FingerTree c
1 errors were found during unification:
Types do not match:
    Expected: e
    Found: c
   ┌─ test:34:39
   │
34 │             | Four w x y z -> View a (Deep (Three w x y) Empty (One z))
   │