Get really fancy with inference

[treeowl]

I realized that even the Newtype class only gets us to an approximation of the platonic ideal. In particular, my understanding is that n and n' are really supposed to be the same newtype, perhaps with different type arguments. Can we express that? I bet we can, with ConstraintKinds!

class (Sim n n', Sim n' n) => Similar n n'
instance (Sim n n', Sim n' n) => Similar n n'

type family GetArg (x :: j) :: k where
  GetArg (_ a) = a

type family GetFun (x :: j) :: k where
  GetArg (f _) = f

type family Sim (n :: k) (n' :: k) :: Constraint where
  Sim (f a) n' = (Sim f (getFun n'), n' ~ getFun n' (GetArg n'))
  Sim f g = f ~ g

I haven't tried compiling this, So I don't know if it works or even if it can be made to work, but I think it's a pretty interesting possibility.