haskell - Haskellには親切な統一がありますか?

Question

シングルトン型が依存型をどの程度シミュレートできるかを研究していて、ある問題にたどり着きました。エラーを再現する最小限のコード:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}

import Data.Kind(Type)

data SBool :: Bool -> Type where
  STrue :: SBool 'True
  SFalse :: SBool 'False

data SSBool :: SBool b -> Type where
  SSFalse :: SSBool 'SFalse
  SSTrue  :: SSBool 'STrue

エラーメッセージは次のとおりです。

種類 ''SBool b' が必要ですが、''SFalse' には種類 ''SBool 'False'' があります</p>