How to limit open world speculation in Haskell

Question

To improve my knowledge of GHC extensions, I decided to try and implement numbers with units, and one thing I wanted to use was to use numeric literals for dimensionless values. But this turned out to be not very practical due to the open worldview that Haskell does. The minimum example of what I could not get is the following:

data Unit ua = Unit a data NoUnit instance Num a => Num (Unit NoUnit a) where -- (+) (*) (-) abs signum not important fromInteger = Unit . fromInteger type family Multiply ab 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 to do something like multiply 1 1 , I expect the resulting value to be unambiguous. Because the only way to get something like Num (Unit ua) is to set u to NoUnit . The rest of a should be respected by default.

Unfortunately, due to Haskell's open assumption, it is possible that some kind of evil person decided that even a number that has units must be a valid instance of Num , even if such a thing would violate (*) :: a -> a -> a as a multiplication of numbers by ones, signatures of this type are not suitable.

Now the open-world assumption is not unfounded, especially because orphan reports are not prohibited in the Haskell report. But in this particular case, I really want to tell GHC that the only valid phantom type for the Num Unit instance is NoUnit .

Is there any way to explicitly state this, and on one side a note prohibiting orphan instances allows the GHC to weaken altogether under the assumption of an open world?

Similar things occurred several times when they tried to make my programs safer in type with a partial input dependency. Whenever I want to specify an instance of Num or IsString or IsList for the base case, and then use custom values ​​or functions to get all the other possible cases.

Answer 1

You cannot turn off the open world assumption, but there are ways to limit it, including this time. In your case, the problem is how you wrote the Num instance:

 instance Num a => Num (Unit NoUnit a) 

What you really wanted was

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

Thus, when the GHC sees that it needs Num (Unit u) a , it concludes that it needs both Num a and u ~ NoUnit . As you wrote it, you left the opportunity to open some additional instance somewhere.

A trick of constructors such as rotation to the right of => to equality constraints on the left is often useful.