What causes this Standard-ML type error?

Question

I was trying to make a tail-recursive version of this very simple SML function:

fun suffixes [] = [[]]
  | suffixes (x::xs) = (x::xs) :: suffixes xs;

During the course of this, I was using type annotations on the paramaters. The following code shows this, and causes a type error (given below), whereas if I simply remove the type annotations, SML accepts it with no problem, giving the whole function the same signature as the simpler function above.

fun suffixes_tail xs =
    let
        fun suffixes_helper [] acc = []::acc
          | suffixes_helper (x::xs:'a list) (acc:'b list) =
                suffixes_helper xs ((x::xs)::acc)
    in
        suffixes_helper xs []
    end;

Error:

$ sml typeerror.sml 
Standard ML of New Jersey v110.71 [built: Thu Sep 17 16:48:42 2009]
[opening typeerror.sml]
val suffixes = fn : 'a list -> 'a list list
typeerror.sml:17.81-17.93 Error: operator and operand don't agree [UBOUND match]
  operator domain: 'a list * 'a list list
  operand:         'a list * 'b list
  in expression:
    (x :: xs) :: acc
typeerror.sml:16.13-17.94 Error: types of rules don't agree [UBOUND match]
  earlier rule(s): 'a list * 'Z list list -> 'Z list list
  this rule: 'a list * 'b list -> 'Y
  in rule:
    (x :: xs : 'a list,acc : 'b list) =>
      (suffixes_helper xs) ((x :: xs) :: acc)
/usr/local/smlnj-110.71/bin/sml: Fatal error -- Uncaught exception Error with 0
 raised at ../compiler/TopLevel/interact/evalloop.sml:66.19-66.27

There are two errors given. The latter seems to be less important here, a mismatch between the two clauses of suffixes_helper. The first is the one I don't understand. I annotate to state that the first param is of type 'a:list and that the second param is of type 'b:list. Should not the Hindley-Milner type inference algorithm, which is built of top of general unification as I understand it, be able to unify 'b:list with 'a:list list, using a substitution of 'b ---> 'a list?

EDIT: An answer suggests it may have something to do with the type inference algorithm disallowing inferred types which in some sense are more strict than the ones given by the type annotations. I would guess that such a rule would only apply to annotations on parameters and on a function as a whole. I have no idea if this is correct. In any case, I tried moving the type annotations over to the function body, and I get the same sort of error:

fun suffixes_helper [] acc = []::acc
    | suffixes_helper (x::xs) acc =
          suffixes_helper (xs:'a list) (((x::xs)::acc):'b list);

The error is now:

typeerror.sml:5.67-5.89 Error: expression doesn't match constraint [UBOUND match]
  expression: 'a list list
  constraint: 'b list
  in expression:
    (x :: xs) :: acc: 'b list

Answer 1

I am not sure about SML, but F#, another functional language, gives a warning in this kind of situation. Giving an error may be a bit harsh, but it makes sense: if the programmer introduces an extra type variable 'b, and if 'b must be of type 'a list, the function might not be as generic as the programmer intended, which is worth reporting.

Answer 2

This works:

fun suffixes_tail xs =
    let
        fun suffixes_helper [] acc = []::acc
          | suffixes_helper (x::xs:'a list) (acc:'a list list) =
                suffixes_helper xs ((x::xs)::acc)
    in
        suffixes_helper xs []
    end

As Joh and newacct say, 'b list is too loose. When you give the explicit type annotation

fun suffixes_helper (_ : 'a list) (_ : 'b list) = ...

it is implicitly quantified as

fun suffixes_helper (_ : (All 'a).'a list) (_ : (All 'b).'b list) = ...

and obviously 'b = 'a list cannot be true (All a') and (All b') simultaneously.

Without the explicit type annotation, type inference can do the right thing, which is to unify the types. And really, SML's type system is simple enough that (as far as I am aware) it is never undecidable, so explicit type annotations should never be necessary. Why do you want to put them in here?

Answer 3

When you use type variables like 'a and 'b, that means that 'a and 'b can be set to anything, independently. So for example it should work if I decided that 'b was int and 'a was float; but obviously that is not valid in this case because it turns out that 'b must be 'a list.