为派生声明添加约束：确保Dimension类型仅合法实例化

我定义了如下新类型：

newtype Dimension a b = MkDimension b

我的需求是：仅当类型参数a满足Format约束（即格式合法）时，才能为Dimension a b派生一系列类型类，同时完全禁止创建不满足Format约束的Dimension实例。

举个例子，如果直接用下面的方式派生Num类：

newtype Dimension a b = MkDimension b 
    deriving newtype Num

那么fromIntegral仍然可能生成格式不合法的维度实例。类似地，我还希望派生Applicative、Monoid等类，但这些类型类的操作也可能产生无效的维度值。

细节说明 #

为了确保维度相加的结果不受顺序影响，我对Dimension实例有两个硬性要求：

• 实例不能包含幂次为0的项
• 类型参数a必须是完全排序后的形式

比如下面这两种情况都应该触发类型错误：

1. (MkDimension 2 :: Dimension '[ '("Meter",0)] Int) + (MkDimension 4 :: Dimension '[] Int)：二者实际是同一维度，但一个包含幂次0的项，另一个是空列表，格式不匹配
2. (MkDimension 2 :: Dimension '[ '("Meter",1),'("Foot",1)] Int) + (MkDimension 4 :: Dimension '[ '("Foot",1),'("Meter",1)] Int)：两个维度的类型参数顺序不一致，不符合排序要求

为了避免这类问题，我希望只有格式合法的维度才能使用fromIntegral这类操作。

相关类型定义 #

我已经定义了用于检查格式的类型家族和约束：

type family Has0 a where 
    Has0 '[] = 'False
    Has0 '(_,0) ': _ = 'True
    Has0 _ ': b = Has0 b

type Format a = (a ~ Sort a, Has0 a ~ 'False)

注：Sort的具体定义较长，此处省略。

内容的提问来源于stack exchange，提问作者Ashok Kimmel