What are the practical and theoretical implications of the unit type and the unit value being the same or different entities?
For example, in Haskell the unit type and unit value are both spelled (). In ML, the unit type is spelled unit and it's value is ().
Are there any problems that arise from either option? Are there any significant benefits perhaps to the soundness of the type-system or the ability to reason about programs?
You have been confused by Haskell's notation. The unit type and unit value are of course different, and it just happens that Haskell uses the same notation for both.
As for the consequences: there are none. Notation is irrelevant here. You can call the unit type Dog or BauwnNuYwvb (i.e., nonsense), and it won't change the type system.
If you reason in terms of sets, what you call the "unit type" is really a one element set, and its single element is what you call the "unit value". So they are obviously not the same thing.
There is no theoretic consequence. Even when they are spelled the same, they are different objects.
Instead, from a purely implementation point of view, there might be some cases where one needs to disambiguate them. In Haskell, a () at the left of :: is the unit value, while a () at the right of :: is a unit type. In rare circumstances, using the DataKinds extension, one needs a unit value on the right as well, and this needs to be escaped to disambiguate.
data T (a :: *) (b :: ()) where
...
foo :: T () '()
Above, T is applied to the unit type (1st arg) and to the unit value (2nd arg), the second being quoted to disambiguate.
This is, however, only a notation incident, which is an insignificant matter from a scientific point of view. One could always choose a different notation and avoid the ambiguities completely.
