Comment by harpocrates

Safety in the form of tightly-fitting types is great, but the signatures definitely suffer a bit in readability (otherwise, Haskell signatures are generally quite helpful when deciphering a functions purpose). I understand why it needs to be this way, but this signature is nasty looking:

    makePCATypeSafe
      :: forall d x y. (AllConstrained SingI '[d,x,y], d <= x ~ 'True)
      => Proxy (d :: Nat) -> DimMatrix D y x Double -> TypeSafePCA

In (pseudo code), dependent types would really help out a lot:

    makePCATypeSafe
      :: forall (d :: Natural) (x :: Natural) (y :: Natural). d <= x
      => Proxy d -> DimMatrix D y x Double -> TypeSafePCA

It sometimes feels like GHC is a kitchen sink for type-level extensions. I wish the bar for entry for new extensions of this sort was higher and the language a bit more cohesive.