How to limit the open world assumption in Haskell

Question

In order to improve my knowledge of GHC extensions I decided to try and implement numbers with units, and one thing I wanted to work was using numeric literals for unitless values. But that turned out to not be very practical due to the open world assumption that Haskell makes. A minimal example of what I couldn't get to work is the following:

data Unit u a = Unit a

data NoUnit

instance Num a => Num (Unit NoUnit a) where
    -- (+) (*) (-) abs signum not important
    fromInteger = Unit . fromInteger

type family Multiply a b where
    Multiply NoUnit NoUnit = NoUnit

multiply :: Num a => Unit u1 a -> Unit u2 a -> Unit (Multiply u1 u2) a
multiply (Unit a) (Unit b) = Unit $ a * b

Now if I try and do something like multiply 1 1 I expect the resulting value to be unambiguous. Because the only way to get something of type Num (Unit u a) is by setting u to NoUnit. And the remaining a should be taken care of by defaulting rules.

Unfortunately due to the open world assumption of Haskell it is possible that some evil person decided that even a number that has units should be a valid Num instance even though such a thing would violate (*) :: a -> a -> a as multiplication of numbers with units does not fit that type signatures.

Now the open world assumption is not an unreasonable one, particularly since orphan instances are not forbidden by the Haskell report. But in this specific case I really do want to tell GHC that the only valid phantom unit type for a Num instance of Unit is NoUnit.

Is there any way to explicitly state this, and on somewhat of a side note would disallowing orphan instances allow GHC to ease up on the open world assumption at all?

This kind of thing has come up a few times when trying to make my programs more type safe with partial dependent typing. Whenever I want to specify a Num or IsString or IsList instance for the base case and then use custom values or functions to obtain all the other possible cases.

Answer 1

You can't turn off the open-world assumption, but there are ways to limit it, including this time. The problem, in your case, is the way you wrote the Num instance:

instance Num a => Num (Unit NoUnit a)

What you really wanted was

instance (Num a, u ~ NoUnit) => Num (Unit u a)

This way, when GHC sees that it needs Num (Unit u) a, it concludes that it needs both Num a and u ~ NoUnit. The way you wrote it, you left open the possibility of some additional instance somewhere.

The trick of turning type constructors to the right of the => to equality constraints on the left is often useful.