Confusing error messages - insufficiently restricted recursive polymorphic datatypes?

[colin-mcd]

The below-referenced code says it prevents recursive polymorphic datatypes from creating types like

data TreeList a = Nil | Cons a (TreeList (a, a));

which correctly throws an error (though perhaps the message could be clearer):

Failed to construct infinite type: a := (a, a), in the definition TreeList

However, it allows using other non-parameter arguments, like

data TreeList a = Nil | Cons a (TreeList (Bool, Bool));

which actually monomorphizes and compiles just fine. You start to get confusing error messages, though, once you try to use such a datatype:

define weigh_length =
  \t. case t of
    | Nil -> fail
    | Cons h t -> amb () (weigh_length t);

weigh_length (Cons () (Cons (False, False) Nil));

Failed to unify () and (Bool, Bool), in the expression Cons ()

I believe the compiler assumes that a is always instantiated to (Bool, Bool), so when you give it the unit type (), it throws that error. I think it would be more helpful if we disallowed data TreeList a = Nil | Cons a (TreeList (Bool, Bool)) instead, because we'll never really be able to use it anyway unless you instantiate a to (Bool, Bool) from the beginning, e.g. weigh_length (Cons (True, True) (Cons (False, False) Nil)).

https://github.com/diprism/perpl/blob/1fbe6226acb336e789c5a08bec102aca4ee546db/src/TypeInf/Solve.hs#L336-L354